Merge pull request #249 from LPCIC/multigoal

msolve

Changelog.md

@@ -1,5 +1,20 @@
 # Changelog
 
+## [1.10.1] - 24-05-2021
+
+Requires Elpi 1.13.5 and Coq 8.13.
+
+### HOAS
+- Fix (reverse) the order of the context argument of `goal`. The head of
+  the list is the most recent hypothesis and in the last to be loaded (the
+  one with higher precedence) by implication when one writes `Ctx => ...`.
+- New `msolve` entry point for (possibly multi goal) tactics
+
+### API
+- Fix argument interpretation for `coq.ltac.call-ltac1`, the context is now the
+  one of the goal alone (and not the one of the goal plus the current one)
+- Rename `coq.ltac.then` to `coq.ltac.all`
+
 ## [1.10.0] - 21-05-2021
 
 Requires Elpi 1.13.5 and Coq 8.13.

apps/eltac/_CoqProject

@@ -16,4 +16,5 @@ theories/discriminate.v
 theories/injection.v
 theories/case.v
 theories/generalize.v
+theories/cycle.v
 theories/tactics.v

apps/eltac/_CoqProject.test

@@ -18,5 +18,6 @@ tests/test_discriminate.v
 tests/test_injection.v
 tests/test_case.v
 tests/test_generalize.v
+tests/test_cycle.v
 
 examples/usage_eltac.v

apps/eltac/tests/test_cycle.v

@@ -0,0 +1,22 @@
+From elpi.apps Require Import eltac.cycle.
+
+Goal True /\ False /\ 1=1.
+split;[|split].
+all: eltac.cycle 1.
+admit.
+reflexivity.
+exact I.
+Abort.
+
+Goal True /\ False /\ 1=1.
+split;[|split].
+all: eltac.cycle -1.
+reflexivity.
+exact I.
+admit.
+Abort.
+
+Goal True /\ False /\ 1=1.
+split;[|split].
+Fail all: eltac.cycle 3.
+Abort.

apps/eltac/theories/clear.v

@@ -7,8 +7,8 @@ Elpi Accumulate lp:{{
   not-hyp X (def Y _ Ty Bo) Y :- not (occurs X Ty ; occurs X Bo), not (X = Y).
 
   solve (goal Ctx R T E [trm X]) [seal (goal Ctx R T E [])] :- name X, !, std.do! [
-    std.map-filter Ctx (not-hyp X) Visible,
-    prune E1 Visible,
+    std.map-filter Ctx (not-hyp X) VisibleRev,
+    prune E1 {std.rev VisibleRev}, % preserve the order
     std.assert-ok! (coq.typecheck E1 T) "cannot clear",
     E = E1
   ].

apps/eltac/theories/cycle.v

@@ -0,0 +1,30 @@
+From elpi Require Export elpi.
+
+Elpi Tactic cycle.
+Elpi Accumulate lp:{{
+
+  pred read-arg i:sealed-goal, o:list argument.
+  read-arg (nabla G) X :- pi x\ read-arg (G x) X.
+  read-arg (seal (goal _ _ _ _ A)) A.
+
+  pred cycle i:int, i:list sealed-goal, o:list sealed-goal.
+  cycle N L PL :- N > 0,
+    std.length L M,
+    std.assert! (N < M) "not enough goals",
+    std.split-at N L B A,
+    std.append A B PL.
+  cycle N L PL :- N < 0,
+    std.length L M,
+    N' is M + N,
+    cycle N' L PL.
+
+  msolve GL GS :-
+    GL = [G|_],
+    read-arg G [int N],
+    if (N = 0) (GS = GL) (cycle N GL GS).
+
+}}.
+
+Elpi Typecheck.
+
+Tactic Notation "eltac.cycle" int(n) := elpi cycle ltac_int:(n).

apps/eltac/theories/tactics.v

@@ -8,4 +8,5 @@ From elpi.apps.eltac Require Export
   generalize
   fail
   clear
+  cycle
 .

coq-builtin.elpi

@@ -43,6 +43,7 @@ pred attributes o:list attribute.
 % Where [str "foo", int 3, trm (app[f,x])] is part of <goal>.
 % The encoding of goals is described below.
 pred solve i:goal, o:list sealed-goal.
+pred msolve i:list sealed-goal, o:list sealed-goal.
 
 % The data type of arguments (for commands or tactics)
 kind argument type.
@@ -145,7 +146,7 @@ type uvar  evarkey -> list term -> term.
 % pi x1\ decl x1 `x` <t> =>
 %  pi x2\ def x2 `y` x1 <v> =>
 %   declare-evar
-%      [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%      [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %      (RawEvar x1 x2) (<p> x1 x2) (Ev x1 x2)
 %
 % where, by default, declare-evar creates a syntactic constraint as
@@ -246,7 +247,7 @@ macro @holes! :- get-option "HOAS:holes" tt.
 %   nabla x2\
 %    seal
 %      (goal
-%         [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%         [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %         (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)
 %         (Arguments x1 x2))
 
@@ -287,12 +288,12 @@ type goal goal-ctx -> term -> term -> term -> list argument -> goal.
 % (pi x1\ decl x1 `x` <t> =>
 %   pi x2\ def x2 `y` x1 <v> =>
 %    declare-evar
-%       [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%       [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %       (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)),
 % (coq.ltac.open solve
 %  (nabla x1\ nabla x2\ seal
 %   (goal
-%     [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%     [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %     (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)
 %     [int 3, str `x`, str`y`, trm (app[const `h`,x1])]))
 %   NewGoals)
@@ -1035,10 +1036,15 @@ external pred coq.strategy.get i:constant, o:conversion_strategy.
 % fail Level Msg, where Msg is the printing of the remaining arguments
 external type coq.ltac.fail int -> variadic any prop.
 
-% [coq.ltac.collect-goals T Goals ShelvedGoals] Turns the holes in T into
-% Goals. Goals are closed with nablas and equipped with GoalInfo (can be
-% left unspecified). ShelvedGoals are goals which can be solved by side
-% effect (they occur in the type of the other goals)
+% [coq.ltac.collect-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
+% in the type of the other goals).
+% The order of Goals is given by the traversal order of EConstr.fold
+% (a
+% fold_left over the terms, letin body comes before the type).
+% 
 external pred coq.ltac.collect-goals i:term, o:list sealed-goal, 
                                      o:list sealed-goal.
 

elpi/coq-HOAS.elpi

@@ -27,7 +27,9 @@ pred attributes o:list attribute.
 %   solve <goal> <new goals>
 % Where [str "foo", int 3, trm (app[f,x])] is part of <goal>.
 % The encoding of goals is described below.
+% msolve is for tactics that operate on multiple goals (called via all: ).
 pred solve i:goal, o:list sealed-goal.
+pred msolve i:list sealed-goal, o:list sealed-goal.
 
 % The data type of arguments (for commands or tactics)
 kind argument type.
@@ -130,7 +132,7 @@ type uvar  evarkey -> list term -> term.
 % pi x1\ decl x1 `x` <t> =>
 %  pi x2\ def x2 `y` x1 <v> =>
 %   declare-evar
-%      [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%      [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %      (RawEvar x1 x2) (<p> x1 x2) (Ev x1 x2)
 %
 % where, by default, declare-evar creates a syntactic constraint as
@@ -231,7 +233,7 @@ macro @holes! :- get-option "HOAS:holes" tt.
 %   nabla x2\
 %    seal
 %      (goal
-%         [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%         [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %         (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)
 %         (Arguments x1 x2))
 
@@ -272,12 +274,12 @@ type goal goal-ctx -> term -> term -> term -> list argument -> goal.
 % (pi x1\ decl x1 `x` <t> =>
 %   pi x2\ def x2 `y` x1 <v> =>
 %    declare-evar
-%       [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%       [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %       (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)),
 % (coq.ltac.open solve
 %  (nabla x1\ nabla x2\ seal
 %   (goal
-%     [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%     [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %     (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)
 %     [int 3, str `x`, str`y`, trm (app[const `h`,x1])]))
 %   NewGoals)
@@ -307,6 +309,22 @@ type goal goal-ctx -> term -> term -> term -> list argument -> goal.
 % Ltac1 code on that term (e.g. to call vm_compute, see also the example
 % on the reflexive tactic).
 
+% ----- Multi goals tactics. ----
+% Coq provides goal selectors, such as all:, to pass to a tactic more than one
+% goal. In order to write such a tactic, Coq-Elpi provides another entry point
+% called msolve. To be precise, if there are two goals under focus, say <g1> and
+% <g2>, then all: elpi tac <t> runs the following query
+%
+%   msolve [<g1>,<g2>] NewGoals ;                         % note the disjunction
+%   coq.ltac.all (coq.ltac.open solve) [<g1>,<g2>] NewGoals
+%
+% So, if msolve has no clause, Coq-Elpi will use solve on all the goals
+% independently. If msolve has a cluse, then it can manipulate the entire list
+% of sealed goals. Note that the argument <t> is in both <g1> and <g2> but
+% it is interpreted in both contexts independently. If both goals have a proof
+% variable named "x" then passing (@eq_refl _ x) as <t> equips both goals with
+% a (raw) proof that "x = x", no matter what their type is.
+
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Declarations for Coq's API (environment read/write access, etc).
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

elpi/elpi-ltac.elpi

@@ -45,20 +45,20 @@ try T G GS :- T G GS.
 try _ G [G].
 
 :index(_ 1)
-pred then i:tactic, i:list sealed-goal, o:list sealed-goal.
-then T [G|Gs] O :- T G O1, then T Gs O2, std.append O1 O2 O.
-then _ [] [].
+pred all i:tactic, i:list sealed-goal, o:list sealed-goal.
+all T [G|Gs] O :- T G O1, all T Gs O2, std.append O1 O2 O.
+all _ [] [].
 
 pred thenl i:list tactic, i:sealed-goal, o:list sealed-goal.
 thenl [] G [G].
-thenl [T|Ts] G GS :- T G NG, then (thenl Ts) NG GS.
+thenl [T|Ts] G GS :- T G NG, all (thenl Ts) NG GS.
 
 pred repeat i:tactic, i:sealed-goal, o:list sealed-goal.
-repeat T G GS :- T G GS1, then (repeat T) GS1 GS.
+repeat T G GS :- T G GS1, all (repeat T) GS1 GS.
 repeat _ G [G].
 
 pred repeat! i:tactic, i:sealed-goal, o:list sealed-goal.
-repeat! T G GS :- T G GS1, !, then (repeat T) GS1 GS.
+repeat! T G GS :- T G GS1, !, all (repeat T) GS1 GS.
 repeat! _ G [G].
 
 pred or i:list tactic, i:sealed-goal, o:list sealed-goal.
@@ -84,12 +84,19 @@ pred move-goal-argument i:list prop, i:list prop, i:argument, o:argument.
 move-goal-argument _ _ (int _ as A) A.
 move-goal-argument _ _ (str _ as A) A.
 move-goal-argument C D (trm T) (trm T1) :-
-  std.assert! (move-term C D T T1) "cannot move goal argument to the right context", !.
+  std.rev C Cr, std.rev D Dr,
+  std.assert! (move-term Cr Dr T T1) "cannot move goal argument to the right context", !.
 
+:index(2)
 pred move-term i:list prop, i:list prop, i:term, o:term.
 move-term [] _ T T1 :- copy T T1.
-move-term [decl X _ TX|C1] [decl Y _ TY|C2] T T1 :- same_term TX TY, !,
+move-term [decl X _ TX|C1] [decl Y _ TY|C2] T T1 :- std.do! [ copy TX TX1, same_term TX1 TY ], !,
   copy X Y => move-term C1 C2 T T1.
+move-term [def X _ TX BX|C1] [def Y _ TY BY|C2] T T1 :- std.do! [ copy TX TX1, same_term TX1 TY, copy BX BX1, same_term BX1 BY ], !,
+  copy X Y => move-term C1 C2 T T1.
+move-term [decl X _ _|C1] C2 T T1 :- not(occurs X T), !, move-term C1 C2 T T1.
+move-term [def X _ _ _|C1] C2 T T1 :- not(occurs X T), !, move-term C1 C2 T T1.
+move-term C1 [_|C2] T T1 :- move-term C1 C2 T T1.
 
 pred distribute-nabla i:(term -> list sealed-goal), o:list sealed-goal.
 distribute-nabla (_\ []) [].