fix.#627

_CoqProject

@@ -57,7 +57,6 @@
 -Q _build/default/apps/tc/elpi elpi.apps.tc.elpi
 -Q apps/tc/examples elpi.apps.tc.examples
 -Q _build/default/apps/tc/examples elpi.apps.tc.examples
--Q apps/tc/tests elpi.apps.tc.tests
 -Q _build/default/apps/tc/tests elpi.apps.tc.tests
 -Q apps/tc/theories elpi.apps.tc
 -Q _build/default/apps/tc/theories elpi.apps.tc

apps/tc/elpi/compiler1.elpi

@@ -26,11 +26,11 @@ namespace tc {
     coq.env.current-section-path SectionPath,
     tc.compile.instance-gr Inst Clause, 
     tc.get-full-path Inst ClauseName,
-    Locality => (
+    (Locality => (
       tc.add-tc-db ClauseName Grafting Clause, 
-      tc.add-tc-db _ Grafting (tc.instance SectionPath Inst TC Locality)).
+      tc.add-tc-db _ Grafting (tc.instance SectionPath Inst TC Locality))).
   add-inst.aux Inst _ _ _ :- 
-    @global! => tc.add-tc-db _ _ (tc.banned Inst),
+    (@global! => tc.add-tc-db _ _ (tc.banned Inst)),
     coq.error "Not-added" "TC_solver" "[TC] Not yet able to compile" Inst "...".
 
   pred add-inst i:gref, i:gref, i:string, i:int.

apps/tc/elpi/ho_compile.elpi

@@ -54,9 +54,9 @@ namespace tc {
           prune Z S',
           tc.compile.goal.make-pairs [T] Pairs,
           % We build on the fly the eta-links for T
-          Pairs =>
+          (Pairs =>
             (tc.compile.goal.build-eta-links-of-vars [T] P,
-              tc.compile.goal.get-uva-pair-arity T PF Y),
+              tc.compile.goal.get-uva-pair-arity T PF Y)),
           std.fold-map NPF A decompile-term-aux Tl (pr XS' L2), 
           std.append P L2 L3,
           NL = tc.link.llam Z (app [Y|Tl]).
@@ -94,9 +94,9 @@ namespace tc {
           prune Z Scope',
           tc.compile.goal.make-pairs [T] Pairs,
           % We build on the fly the eta-links for `T`
-          Pairs =>
+          (Pairs =>
             (tc.compile.goal.build-eta-links-of-vars [T] P,
-              tc.compile.goal.get-uva-pair-arity T L Y),
+              tc.compile.goal.get-uva-pair-arity T L Y)),
           var Z Y Scope',
           std.append P B B'.
 
@@ -173,7 +173,7 @@ namespace tc {
       % In this case we unfold this definition to get the prod constructor
       make-eta-link-aux A T BN L Link Ty' Bo :-
         coq.safe-dest-app T Hd Ag,
-        @redflags! coq.redflags.delta => coq.reduction.lazy.whd Hd Hd',
+        (@redflags! coq.redflags.delta => coq.reduction.lazy.whd Hd Hd'),
         not (Hd = Hd'), !,
         coq.mk-app Hd' Ag TT',
         make-eta-link-aux A TT' BN L Link Ty' Bo.
@@ -214,8 +214,8 @@ namespace tc {
         i:list prop,
         o:prop.
       compile-premise L L2 P PTy ProofHd IsPositive ITy ProofTlR PremR Clause :-
-        (pi a b c\ tc.get-TC-of-inst-type (tc.prod-range a c) b :- tc.get-TC-of-inst-type a b) => 
-          tc.get-TC-of-inst-type PTy TC, !,
+        ((pi a b c\ tc.get-TC-of-inst-type (tc.prod-range a c) b :- tc.get-TC-of-inst-type a b) => 
+          tc.get-TC-of-inst-type PTy TC), !,
         compile-ty L L1 P {neg IsPositive} PTy [] [] NewPrem,
         if (tc.class TC _ tc.deterministic _)
           (NewPrem' = do-once NewPrem)

builtin-doc/elpi-builtin.elpi

@@ -247,6 +247,21 @@ pred snd  i:pair A B, o:B.
 
 snd (pr _ B) B.
 
+
+kind triple type -> type -> type -> type.
+type triple A -> B -> C -> triple A B C.
+
+pred triple_1 i:triple A B C, o:A.
+triple_1 (triple A _ _) A.
+
+pred triple_2 i:triple A B C, o:B.
+triple_2 (triple _ B _) B.
+
+pred triple_3 i:triple A B C, o:C.
+triple_3 (triple _ _ C) C.
+
+
+
 % The option type (aka Maybe)
 kind option type -> type.
 type none option A.

elpi/elpi-ltac.elpi

@@ -11,7 +11,7 @@ refine T G GS :- refine.elaborate T G GS.
 pred refine.elaborate i:term, i:goal, o:list sealed-goal.
 refine.elaborate T (goal _ RawEv Ty Ev _) GS :-
   rm-evar RawEv Ev,
-  @keepunivs! => coq.elaborate-skeleton T Ty TR ok,
+  (@keepunivs! => coq.elaborate-skeleton T Ty TR ok),
   coq.ltac.collect-goals TR GS _,
   RawEv = T,
   Ev = TR.
@@ -82,7 +82,7 @@ open T (nabla G) O :- (pi x\ open T (G x) (NG x)), private.distribute-nabla NG O
 open _ (seal (goal _ _ _ Solution _)) [] :- not (var Solution), !. % solved by side effect
 open T (seal (goal Ctx _ _ _ _ as G)) O :-
   std.filter Ctx private.not-already-assumed Ctx1,
-  Ctx1 => T G O,
+  (Ctx1 => T G O),
   if (var O)
      (G = goal _ _ _ P _, coq.ltac.collect-goals P O1 O2, std.append O1 O2 O)
      true.

src/coq_elpi_programs.ml

@@ -143,6 +143,7 @@ type nature = Command of { raw_args : bool } | Tactic | Program of { raw_args :
 
 type program = {
   sources_rev : qualified_name Code.t;
+  files : CString.Set.t;
   units : Names.KNset.t;
   dbs : SLSet.t;
   empty : bool; (* it is empty, if it only contains default code *)
@@ -414,32 +415,32 @@ let get ?(fail_if_not_exists=false) p =
   let _elpi = ensure_initialized () in
   let nature = get_nature p in
   try
-  let { sources_rev; units; dbs; empty } = SLMap.find p !program_src in
-  units, dbs, Some nature, Some sources_rev, empty
+  let { sources_rev; files; units; dbs; empty } = SLMap.find p !program_src in
+  files, units, dbs, Some nature, Some sources_rev, empty
   with Not_found ->
   if fail_if_not_exists then
     CErrors.user_err
       Pp.(str "No Elpi Program named " ++ pr_qualified_name p)
   else
-    Names.KNset.empty, SLSet.empty, None, None, true
+    CString.Set.empty, Names.KNset.empty, SLSet.empty, None, None, true
 
   let append_to_prog from name src =
-    let units, dbs, _, prog, empty = get name in
-    let units, dbs, prog =
+    let files, units, dbs, _, prog, empty = get name in
+    let files, units, dbs, prog =
       match src with
       (* undup *)
-      | File { fast = (kn,_) } when Names.KNset.mem kn units -> units, dbs, prog
-      | EmbeddedString { sast = (kn,_) } when Names.KNset.mem kn units -> units, dbs, prog
-      | DatabaseHeader { dast = (kn,_) } when Names.KNset.mem kn units -> units, dbs, prog
-      | DatabaseBody n  when SLSet.mem n dbs -> units, dbs, prog
+      | File { fname; fast = (kn,_) } when CString.Set.mem fname files || Names.KNset.mem kn units -> files, units, dbs, prog
+      | EmbeddedString { sast = (kn,_) } when Names.KNset.mem kn units -> files, units, dbs, prog
+      | DatabaseHeader { dast = (kn,_) } when Names.KNset.mem kn units -> files, units, dbs, prog
+      | DatabaseBody n  when SLSet.mem n dbs -> files, units, dbs, prog
       (* add *)
-      | File { fast = (kn,_ as u) } -> (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog)
-      | EmbeddedString { sast = (kn,_ as u) } -> (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog)
-      | DatabaseHeader { dast = (kn,_ as u) } ->  (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog)
-      | DatabaseBody n ->  units, SLSet.add n dbs, Some (Code.snoc_db_opt Hashtbl.hash n prog)
+      | File { fname; fast = (kn,_ as u) } -> CString.Set.add fname files, (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog)
+      | EmbeddedString { sast = (kn,_ as u) } -> files, (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog)
+      | DatabaseHeader { dast = (kn,_ as u) } ->  files, (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog)
+      | DatabaseBody n ->  files, units, SLSet.add n dbs, Some (Code.snoc_db_opt Hashtbl.hash n prog)
       in
     let prog = Option.get prog in
-    { units; dbs; sources_rev = prog; empty = empty && from = Initialization }
+    { files; units; dbs; sources_rev = prog; empty = empty && from = Initialization }
 
 
   let in_program : qualified_name * src * from -> Libobject.obj =
@@ -461,7 +462,7 @@ let get ?(fail_if_not_exists=false) p =
     Lib.add_leaf obj
 
   let code ?(even_if_empty=false) n : Chunk.t Code.t option =
-    let _,_,_,sources, empty = get n in
+    let _,_,_,_,sources, empty = get n in
     if empty && not even_if_empty then None else
     sources |> Option.map (fun sources -> sources |> Code.map (fun name ->
     try

tests/dune

@@ -4,3 +4,9 @@
  (theories elpi))
 
 (include_subdirs qualified)
+
+(rule
+ (target dummy.v)
+ (deps (glob_files_rec *.elpi))
+ (action
+  (with-stdout-to %{target} (echo "(* copy elpi files to _build *)"))))