ltac: any/simple APIs with sealed/unsealed goals

Author: gares

apps/coercion/README.md

@@ -61,7 +61,7 @@ coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
   Solution = {{ @exist lp:Ty lp:P lp:X1 _ }},
   % we call the solver
   coq.ltac.collect-goals Solution [G] [],
-  coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [],
+  coq.ltac.open (x\y\coq.ltac.call-any-ltac1 "my_solver" x y ok) G [],
 ].
 
 }}.

apps/coercion/tests/test_open.v

@@ -12,7 +12,7 @@ coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
   Solution = {{ @exist lp:Ty lp:P lp:X1 _ }},
   % we call the solver
   coq.ltac.collect-goals Solution [G] [],
-  coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [],
+  coq.ltac.open (x\y\coq.ltac.call-any-ltac1 "my_solver" x y ok) G [],
 ].
 
 }}.

builtin-doc/coq-builtin.elpi

@@ -1634,7 +1634,7 @@ kind ltac1-tactic type.
 % Level can be left unspecified and defaults to 0
 external type coq.ltac.fail int -> variadic any (func).
 
-% [coq.ltac.collect-goals T Goals ShelvedGoals] 
+% [coq.ltac.collect-any-goals T Goals ShelvedGoals] 
 % Turns the holes in T into Goals.
 % Goals are closed with nablas.
 % ShelvedGoals are goals which can be solved by side effect (they occur
@@ -1643,11 +1643,23 @@ external type coq.ltac.fail int -> variadic any (func).
 % (a
 % fold_left over the terms, letin body comes before the type).
 % 
-external func coq.ltac.collect-goals term -> list sealed-goal, 
-                                    list sealed-goal.
+external func coq.ltac.collect-any-goals term -> list sealed-goal, 
+                                        list sealed-goal.
 
-% [coq.ltac.call-mltac PluginName BlockName BlockIndex G GL] Calls OCaml
-% code bound via TACTIC EXTEND. For example the
+
+func coq.ltac.collect-goals term -> list sealed-goal, list sealed-goal.
+coq.ltac.collect-goals T GA GB :- coq.ltac.collect-any-goals T GA GB.
+
+
+% [coq.ltac.collect-simple-goals T Goals ShelvedGoals] Like
+% coq.ltac.collect-goals turns the holes in T into
+% Goals but fails if the goals do not live in the current context.
+% 
+external func coq.ltac.collect-simple-goals term -> list goal, 
+                                           list sealed-goal.
+
+% [coq.ltac.call-any-mltac PluginName BlockName BlockIndex G GL Diagnostic]
+% Calls OCaml code bound via TACTIC EXTEND. For example the
 % OCaml code for lia looks like:
 % 
 %   DECLARE PLUGIN "rocq-runtime.plugins.micromega"
@@ -1665,13 +1677,27 @@ external func coq.ltac.collect-goals term -> list sealed-goal,
 % numbering
 % starts from 0. Also, each block has a name, "Lia" in this case.
 %     
+% When the diagnostic is (error Msg), then GL is not set.
+% 
+% Supported attributes:
+% - @no-tc! (default false, do not infer typeclasses)
+external func coq.ltac.call-any-mltac string, string, int, 
+                                     goal -> list sealed-goal, diagnostic.
+
+% [coq.ltac.call-simple-mltac PluginName BlockName BlockIndex G GL
+% Diagnostic] Like coq.ltac.call-any-mltac but Tac is not allowed to
+% generate new goals GL in different contexts. For example "intro" does
+% not
+% obey this restriction.
+% 
 % Supported attributes:
 % - @no-tc! (default false, do not infer typeclasses)
-external func coq.ltac.call-mltac string, string, int, 
-                                 goal -> list sealed-goal.
+external func coq.ltac.call-simple-mltac string, string, int, 
+                                        goal -> list goal, diagnostic.
 
-% [coq.ltac.call-ltac1 Tac G GL] Calls Ltac1 tactic Tac on goal G (passing
-% the arguments of G, see coq.ltac.call for a handy wrapper).
+% [coq.ltac.call-any-ltac1 Tac G GL Diagnostic] Calls Ltac1 tactic Tac on
+% goal G (passing the arguments of G, see coq.ltac.call for a handy
+% wrapper).
 % Tac can either be a string (the tactic name), or a value
 % of type ltac1-tactic, see the tac argument constructor
 % and the ltac_tactic:(...) syntax to pass arguments to
@@ -1681,9 +1707,31 @@ external func coq.ltac.call-mltac string, string, int,
 %   "Ltac name := body", it cannot be a builtin one. For example
 %   "Ltac myapply x := apply x." lets one call apply by running
 %   coq.ltac.call-ltac1 "myapply" G GL.
+% 
+% When the diagnostic is (error Msg), then GL is not set.
+% 
+% Supported attributes:
+% - @no-tc! (default false, do not infer typeclasses)
+external func coq.ltac.call-any-ltac1 any, goal -> list sealed-goal, 
+                                     diagnostic.
+
+
+  func coq.ltac.call-ltac1 any, goal -> list sealed-goal.
+  coq.ltac.call-ltac1 Tac G GL :-
+    coq.warning "elpi.deprecated" "elpi.ltac.call-ltac1" "use ltac.call-any-ltac1 with an extra diagnostic argument",
+    coq.ltac.call-any-ltac1 Tac G GL ok.
+  
+
+% [coq.ltac.call-simple-ltac1 Tac G GL Diagnostic] Like
+% coq.ltac.call-any-ltac1 but Tac is not allowed to
+% generate new goals GL in different contexts. For example "intro" does
+% not
+% obey this restriction.
+% 
 % Supported attributes:
 % - @no-tc! (default false, do not infer typeclasses)
-external func coq.ltac.call-ltac1 any, goal -> list sealed-goal.
+external func coq.ltac.call-simple-ltac1 any, goal -> list goal, 
+                                        diagnostic.
 
 % [coq.ltac.id-free? ID G] 
 %     Fails if ID is already used in G. Note that ids which are taken are