Merge pull request #15 from gares/elpi-2.0

adapt to elpi 2.0

elpi/commands.elpi

@@ -107,7 +107,7 @@ add-embedding Args :-
       "expected: ", {coq.term->string ExpectedEmbedThenInvIdT},
       "\ngot: ", {coq.term->string EmbedThenInvIdT}, "\n\n"
     ]},
-    pi y\ pi z\ copy (app [Embed, y]) z => copy (CondF y) (CondFE z),
+    pi y\ pi z\ (copy (app [Embed, y]) z => copy (CondF y) (CondFE z)),
     ExpectedInvThenEmbedCondIdT =
       {{ forall (x' : lp:T'), lp:(CondFE x') -> @eq lp:T' (lp:Embed (lp:EmbedInv x')) x' }},
     pi x'\

elpi/generalise_free_variables.elpi

@@ -56,7 +56,7 @@ find-free-variables.aux {{ lp:A -> lp:B }} ETargetOpt Context FVInfoSet :- !,
   set-merge FVInfoSetA FVInfoSetB FVInfoSet.
 
 find-free-variables.aux (prod _ T F) ETargetOpt Context FVInfoSet' :- !,
-  pi x\ decl x _ T => find-free-variables.aux (F x) ETargetOpt Context (FVInfoSet x),
+  pi x\ (decl x _ T => find-free-variables.aux (F x) ETargetOpt Context (FVInfoSet x)),
   std.set.remove (pr x _) (FVInfoSet x) FVInfoSet'.
 
 find-free-variables.aux (app [F|Args]) ETargetOpt Context FVInfoSet' :- !,

elpi/preprocess.elpi

@@ -118,11 +118,11 @@ preprocess (prod N T F) ETargetOpt LTarget TVar _ PreprocEquiv OutTerm Proof :-
         % inverse lemmas, but some embedding identities must be removed
         make-reverse-embedding-context FunT ETarget REF,
         std.map.make cmp_term EmptyMap,
-        pi x'\ decl x' _ T' => (
+        pi x'\ (decl x' _ T' ==>
           beta-reduce (F' (REF x')) (BF x'),
           if (CondFOpt = some CondF) (
             % there will be a condition in the final proof
-            pi c\ decl c _ (CondF x') => (
+            pi c\ (decl c _ (CondF x') ==>
               std.map.add x' c EmptyMap (CondProofs x' c),
               rewrite-identities (BF x') ETarget LTarget (CondProofs x' c) (RwProofC x' c),
               clear-custom-terms-in-proof (RwProofC x' c) (RwProofC' x' c),
@@ -738,7 +738,7 @@ pred generalise
 generalise X Term FT ETarget F' :-
   pi x\
     % first replace X with a fresh variable
-    copy X x => copy Term (F x),
+    (copy X x => copy Term (F x)),
     % then remove embedding functions around this variable everywhere in the term
     remove-embeddings-around x (F x) FT ETarget (F' x).
 

elpi/proof.elpi

@@ -59,7 +59,7 @@ build.aux (proof.none T) {{ @id lp:T }}.
 build.aux (proof.of-term Term) Term.
 
 build.aux (proof.forall T PF CoqProofF) CoqProof :-
-  pi x\ decl x _ T =>
+  pi x\ decl x _ T ==>
     build.aux (PF x) (CoqPF x),
     if (CoqPF x = {{ id }}) (
       copy (app [{{ id }}, X]) X => copy (CoqProofF CoqPF) CoqProof
@@ -68,8 +68,8 @@ build.aux (proof.forall T PF CoqProofF) CoqProof :-
     ).
 
 build.aux (proof.forall2 T U PF CoqProofF) CoqProof :-
-  pi x\ decl x _ T =>
-    pi y\ decl y _ (U x) =>
+  pi x\ decl x _ T ==>
+    pi y\ decl y _ (U x) ==>
       build.aux (PF x y) (CoqPF x y),
       if (CoqPF x y = {{ id }}) (
         copy (app [{{ id }}, X]) X => copy (CoqProofF CoqPF) CoqProof

elpi/reorder_quantifiers.elpi

@@ -76,7 +76,7 @@ pred bind-back i:list term, i:term, o:term.
 bind-back [] Term Term.
 
 bind-back [X|Xs] Term Term' :-
-  pi x\ copy X x => copy Term (F x), !,
+  (pi x\ copy X x => copy Term (F x)), !,
   bind-back Xs (fun _ _ F) Term'.
 
 % pop a list of hypotheses in front of a type

theories/Commands.v

@@ -24,7 +24,6 @@ Elpi Query lp:{{
 }}.
 
 Elpi Accumulate File types.
-Elpi Typecheck.
 
 From Trakt Require Export Database.
 Elpi Accumulate Db embeddings.db.
@@ -33,10 +32,8 @@ Elpi Accumulate Db relations.db.
 Elpi Accumulate Db conversion.db.
 
 Elpi Accumulate File common.
-Elpi Typecheck.
 
 Elpi Accumulate File commands.
-Elpi Typecheck.
 
 Elpi Accumulate lp:{{
   pred elaborate-argument i:argument, o:argument.
@@ -68,5 +65,4 @@ Elpi Accumulate lp:{{
       "     | Trakt Set Verbosity (0|1|2)", "", ""
     ]}.
 }}.
-Elpi Typecheck.
 Elpi Export Trakt.

theories/Database.v

@@ -72,7 +72,11 @@ Proof.
   intros []; cbv [negb]; auto.
 Qed.
 
-Elpi Db logic.db lp:{{
+From Trakt.Elpi Extra Dependency "types.elpi" as types.
+
+Elpi Db logic.db lp:{{ }}.
+Elpi Accumulate logic.db File Signature types.
+Elpi Accumulate logic.db lp:{{
   logical-connector
     {{ and }} {{ andb }} [covariant, covariant]
     {{ and_impl_morphism }} {{ andb_and_impl }} {{ and_andb_impl }}.
@@ -106,6 +110,13 @@ Proof.
 Qed.
 
 Elpi Db embeddings.db lp:{{ }}.
+Elpi Accumulate embeddings.db File Signature types.
+
 Elpi Db symbols.db lp:{{ }}.
+Elpi Accumulate symbols.db File Signature types.
+
 Elpi Db relations.db lp:{{ }}.
-Elpi Db conversion.db lp:{{ }}.
+Elpi Accumulate relations.db File Signature types.
+
+Elpi Db conversion.db lp:{{ }}.
+Elpi Accumulate conversion.db File Signature types.

theories/Tactic.v

@@ -47,36 +47,35 @@ Elpi Accumulate lp:{{
     std.assert! (format-runtime-relation-data RuntimeRelData RuntimeRelCtx)
       "wrong runtime relations format",
     RuntimeRelCtx =>
-      preprocess-extra InitialGoalTy Context (some ETarget) LTarget covariant true EndGoalTy Proof,
-      refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals.
+      (preprocess-extra InitialGoalTy Context (some ETarget) LTarget covariant true EndGoalTy Proof,
+      refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals).
 
   solve InitialGoal NewGoals :-
     InitialGoal = goal Context _ InitialGoalTy _ [trm ETarget, trm LTarget],
     (LTarget = {{ Prop }} ; LTarget = {{ bool }}), !,
     [] =>
-      preprocess-extra InitialGoalTy Context (some ETarget) LTarget covariant true EndGoalTy Proof,
-      refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals.
+      (preprocess-extra InitialGoalTy Context (some ETarget) LTarget covariant true EndGoalTy Proof,
+      refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals).
 
   solve InitialGoal NewGoals :-
     InitialGoal = goal Context _ InitialGoalTy _ [trm LTarget, trm RuntimeRelData],
     (LTarget = {{ Prop }} ; LTarget = {{ bool }}), !,
     std.assert! (format-runtime-relation-data RuntimeRelData RuntimeRelCtx)
       "wrong runtime relations format",
     RuntimeRelCtx =>
-      preprocess-extra InitialGoalTy Context none LTarget covariant true EndGoalTy Proof,
-      refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals.
+      (preprocess-extra InitialGoalTy Context none LTarget covariant true EndGoalTy Proof,
+      refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals).
 
   solve InitialGoal NewGoals :-
     InitialGoal = goal Context _ InitialGoalTy _ [trm LTarget],
     (LTarget = {{ Prop }} ; LTarget = {{ bool }}), !,
     [] =>
-      preprocess-extra InitialGoalTy Context none LTarget covariant true EndGoalTy Proof,
-      refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals.
+      (preprocess-extra InitialGoalTy Context none LTarget covariant true EndGoalTy Proof,
+      refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals).
 
   solve _ _ :-
     coq.error "usage: trakt [target embedding type] <bool|Prop> [with rel <relations>]".
 }}.
-Elpi Typecheck.
 
 Tactic Notation "trakt" constr(target) constr(logic_target) "with" "rel" constr(l) :=
   elpi trakt ltac_term:(target) ltac_term:(logic_target) ltac_term:(l).
@@ -115,8 +114,8 @@ Elpi Accumulate lp:{{
       "wrong runtime relations format",
     coq.typecheck H T ok,
     RuntimeRelCtx =>
-      preprocess-extra T [] (some ETarget) LTarget contravariant false T' P,
-      refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals.
+      (preprocess-extra T [] (some ETarget) LTarget contravariant false T' P,
+      refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals).
 
   solve Goal NewGoals :-
     Goal = goal _ _ GoalTy _ [trm ETarget, trm LTarget, trm H, str S],
@@ -125,8 +124,8 @@ Elpi Accumulate lp:{{
     coq.string->name S Name,
     coq.typecheck H T ok,
     [] =>
-      preprocess-extra T [] (some ETarget) LTarget contravariant false T' P,
-      refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals.
+      (preprocess-extra T [] (some ETarget) LTarget contravariant false T' P,
+      refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals).
 
   solve Goal NewGoals :-
     Goal = goal _ _ GoalTy _ [trm LTarget, trm H, str S, trm RuntimeRelData],
@@ -137,8 +136,8 @@ Elpi Accumulate lp:{{
       "wrong runtime relations format",
     coq.typecheck H T ok,
     RuntimeRelCtx =>
-      preprocess-extra T [] none LTarget contravariant false T' P,
-      refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals.
+      (preprocess-extra T [] none LTarget contravariant false T' P,
+      refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals).
 
   solve Goal NewGoals :-
     Goal = goal _ _ GoalTy _ [trm LTarget, trm H, str S],
@@ -147,8 +146,8 @@ Elpi Accumulate lp:{{
     coq.string->name S Name,
     coq.typecheck H T ok,
     [] =>
-      preprocess-extra T [] none LTarget contravariant false T' P,
-      refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals.
+      (preprocess-extra T [] none LTarget contravariant false T' P,
+      refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals).
 
   solve _ _ :-
     coq.error {std.string.concat "\n" [
@@ -158,7 +157,6 @@ Elpi Accumulate lp:{{
       "             [with rel <relations>]"
     ]}.
 }}.
-Elpi Typecheck.
 
 Tactic Notation "trakt_pose" constr(et) constr(lt) ":" constr(h) "as" ident(s) :=
   elpi trakt_pose ltac_term:(et) ltac_term:(lt) ltac_term:(h) ltac_string:(s).
@@ -192,7 +190,6 @@ Elpi Accumulate lp:{{
   solve _ _ :-
     coq.error "usage: trakt_boolify_arrows.".
 }}.
-Elpi Typecheck.
 
 Tactic Notation "trakt_boolify_arrows" := elpi trakt_boolify_arrows.
 
@@ -212,6 +209,5 @@ Elpi Accumulate lp:{{
   solve _ _ :-
     coq.error "usage: trakt_reorder_quantifiers.".
 }}.
-Elpi Typecheck.
 
 Tactic Notation "trakt_reorder_quantifiers" := elpi trakt_reorder_quantifiers.