Fix for new compiler (#692)

gares · FissoreD · web-flow · commit 9ae1653c39e7 · 2024-09-19T15:13:45.000+02:00
Mainly declare types before clauses

---------

Co-authored-by: Davide Fissore &lt;fisso9900@gmail.com&gt;
diff --git a/apps/derive/elpi/param1.elpi b/apps/derive/elpi/param1.elpi
@@ -3,6 +3,11 @@
 /* ------------------------------------------------------------------------- */
 
 % Author: Cyril Cohen
+pred reali-done i:gref.
+
+:index(3)
+pred reali i:term, o:term.
+type realiR term -> term -> prop.
 
 shorten std.{forall, forall2, do!, rev, map2, map}.
 
diff --git a/apps/derive/elpi/param1_functor.elpi b/apps/derive/elpi/param1_functor.elpi
@@ -1,6 +1,8 @@
 /* map over a container                                                      */
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
+pred param1-functor-db i:term, i:term, o:term.
+pred param1-functor-for i:inductive, o:gref, o:list bool.
 
 shorten std.{assert!, do!, length, split-at, drop-last, rev, append}.
 
diff --git a/apps/derive/elpi/param2.elpi b/apps/derive/elpi/param2.elpi
@@ -3,6 +3,10 @@
 /* ------------------------------------------------------------------------- */
 
 % Author: Cyril Cohen
+pred param-done i:gref.
+:index(3)
+pred param i:term, o:term, o:term.
+type paramR term -> term -> term -> prop.
 
 shorten std.{forall, forall2, do!, rev, map2, map}.
 
diff --git a/apps/derive/tests/test_derive.v b/apps/derive/tests/test_derive.v
@@ -121,7 +121,8 @@ Inductive rtree A : Type :=
   Leaf (n : A) | Node (l : list rtree).
 
 Module XXX.
-Elpi derive rtree.
+derive list.
+derive rtree.
 End XXX.
 
 Fail Check XXX.rtree_is_rtree_map.
@@ -161,8 +162,10 @@ Redirect "tmp" Check Pred.Pred_to_Predinv : forall T, Pred T -> Pred.Predinv T.
 (* #286 *)
 Module Import derive_container.
 Unset Implicit Arguments.
+Import XXX.
 derive
 Inductive wimpls {A} `{rtree A} := Kwi (x:A) (y : x = x) : wimpls | Kwa.
+
 End derive_container.
 About wimpls.wimpls.
 About wimpls.Kwi.
diff --git a/apps/derive/theories/derive/param1.v b/apps/derive/theories/derive/param1.v
@@ -92,7 +92,6 @@ Elpi Accumulate lp:{{
   usage :- coq.error "Usage: derive.param1 <object name>".
 }}. 
 Elpi Typecheck.
-
 Module Export exports.
 Elpi derive.param1 eq.
 End exports.
diff --git a/apps/tc/elpi/compiler1.elpi b/apps/tc/elpi/compiler1.elpi
@@ -28,7 +28,7 @@ namespace tc {
     tc.get-full-path Inst ClauseName,
     Locality => (
       tc.add-tc-db ClauseName Grafting Clause, 
-      tc.add-tc-db _ Grafting (tc.instance SectionPath Inst TC)).
+      tc.add-tc-db _ Grafting (tc.instance SectionPath Inst TC Locality)).
   add-inst.aux Inst _ _ _ :- 
     @global! => tc.add-tc-db _ _ (tc.banned Inst),
     coq.error "Not-added" "TC_solver" "[TC] Not yet able to compile" Inst "...".
@@ -51,7 +51,7 @@ namespace tc {
     %       TC.AddAllInstances or TC.AddInstances InstName
     if (is-local; has-context-deps Inst) 
       (LocalityStr = "Local") 
-      (LocalityStr = "Global"),
+      (LocalityStr = "Export"),
     add-inst Inst TC LocalityStr Prio.
 
   % [add-inst->db IgnoreClassDepL ForceAdd Inst] compiles and add the Inst to
@@ -61,7 +61,7 @@ namespace tc {
   add-inst->db _ tt Inst :- !, add-inst>db.aux Inst.
   add-inst->db _ _ Inst :- 
     tc.banned Inst, !, (coq.warning "tc.banned-inst" "TC-warning" Inst "is tc.banned").
-  add-inst->db _ _ Inst :- tc.instance _ Inst _, !. % the instance has already been added
+  add-inst->db _ _ Inst :- tc.instance _ Inst _ _, !. % the instance has already been added
   add-inst->db IgnoreClassDepL _ Inst :-
     get-class-dependencies Inst Dep,
     std.exists Dep (std.mem IgnoreClassDepL), !,
@@ -85,11 +85,19 @@ namespace tc {
           (coq.warning "not-inst-nor-tc" "TC-warning" GR "is neither a TC nor a instance")
     ).
 
+  pred build-args i:term, o:list term.
+  build-args (prod _ _ Bo) [{{0}} | TL] :- !, build-args (Bo _) TL.
+  build-args _ [{{0}}].
+
   % [remove-inst GR] remove an instance from the DB by replacing it with `dummy`
   pred remove-inst i:gref.
   remove-inst InstGR :- 
     tc.get-full-path InstGR ClauseName,
-    tc.remove-clause ClauseName.
+    tc.instance _ InstGR ClassGR Locality,
+    tc.gref->pred-name ClassGR PredName,
+    coq.env.typeof ClassGR ClassTy,
+    coq.elpi.predicate PredName {build-args ClassTy} Clause,
+    tc.remove-clause ClauseName Clause Locality.
 
   pred is-in-path i:string, i:gref. 
   is-in-path Path GR :- 
diff --git a/apps/tc/elpi/modes.elpi b/apps/tc/elpi/modes.elpi
@@ -66,7 +66,7 @@ namespace tc {
 
   pred remove-pending-mode.
   remove-pending-mode :-
-    tc.remove-clause @pending-mode!.
+    tc.remove-clause @pending-mode! (pending-mode []) [].
 
   pred check-pending-mode-arity i:gref, i:list A.
   check-pending-mode-arity GR L :-
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
@@ -42,9 +42,9 @@ namespace tc {
   :name "MySectionEndHook"
   instances-of-current-section InstsFiltered :-
     coq.env.current-section-path SectionPath,
-    std.findall (tc.instance SectionPath _ _) Insts,
+    std.findall (tc.instance SectionPath _ _ _) Insts,
     coq.env.section SectionVars,
-    std.map-filter Insts (x\r\ sigma X\ tc.instance _ r _ = x, const X = r, not(std.mem SectionVars X)) InstsFiltered.
+    std.map-filter Insts (x\r\ sigma X\ tc.instance _ r _ _ = x, const X = r, not(std.mem SectionVars X)) InstsFiltered.
 
   pred is-instance-gr i:gref.
   is-instance-gr GR :-
@@ -156,9 +156,9 @@ namespace tc {
 
   pred dummy.
 
-  pred remove-clause i:string.
-  remove-clause ClauseName :-
-    add-tc-db _ (replace ClauseName) dummy.
+  pred remove-clause i:string, i:prop, i:list prop.
+  remove-clause ClauseName P Locality :-
+    Locality => add-tc-db _ (remove ClauseName) P.
 
   % [section-var->decl.aux L R] auxiliary function for `section-var->decl`
   pred section-var->decl.aux i:list constant, o:list prop.
diff --git a/apps/tc/elpi/tc_same_order.elpi b/apps/tc/elpi/tc_same_order.elpi
@@ -12,13 +12,13 @@ pred correct_instance_order i:(list gref), i:(list prop).
 correct_instance_order [] _.
 correct_instance_order [TC | TL] ElpiInst :-
   coq.TC.db-for TC CoqInst,
-  std.map-filter ElpiInst (x\r\ sigma I\ x = tc.instance _ I TC, r = I) ElpiInstTC,
+  std.map-filter ElpiInst (x\r\ sigma I\ x = tc.instance _ I TC _, r = I) ElpiInstTC,
   if (correct_instance_order_aux TC CoqInst ElpiInstTC) 
     (correct_instance_order TL ElpiInst)
     (coq.error "Error in import order\n" 
     "Expected :" CoqInst "\nFound   :" ElpiInstTC).
 
 :name "tc-same-order-main"
 main _ :-
-  std.findall (tc.instance _ _ _) ElpiInst,
+  std.findall (tc.instance _ _ _ _) ElpiInst,
   correct_instance_order {coq.TC.db-tc} ElpiInst.
diff --git a/apps/tc/tests/auto_compile.v b/apps/tc/tests/auto_compile.v
@@ -48,8 +48,8 @@ Goal M.B 10. apply _. Qed.
 Elpi Query TC.Solver lp:{{
   % Small test for instance order
   sigma I L\
-  std.findall (tc.instance _ _ _) I,
-  std.map-filter I (x\y\ x = tc.instance _ y {{:gref M.B}}) 
+  std.findall (tc.instance _ _ _ _) I,
+  std.map-filter I (x\y\ x = tc.instance _ y {{:gref M.B}} _) 
     [{{:gref M.W}}, {{:gref M.Y}}, {{:gref M.Z}}].
 }}.
 
diff --git a/apps/tc/tests/hook_test.v b/apps/tc/tests/hook_test.v
@@ -10,8 +10,8 @@ Instance Inst2 : A 100 | 1512. Qed.
 
 Elpi Query TC.Solver lp:{{
   sigma InstL GrefL\
-  std.findall (tc.instance _ _ {{:gref A}}) InstL, 
-  std.map InstL (x\r\ x = tc.instance _ r _) GrefL, 
+  std.findall (tc.instance _ _ {{:gref A}} _) InstL, 
+  std.map InstL (x\r\ x = tc.instance _ r _ _) GrefL, 
   GrefL = [{{:gref Inst2}}, {{:gref Inst1}}].
 }}.
 
diff --git a/apps/tc/tests/section_in_out.v b/apps/tc/tests/section_in_out.v
@@ -12,8 +12,8 @@ Elpi Accumulate lp:{{
   % contains the number of instances that are not 
   % imported from other files
   main [int Len] :-
-    std.findall (tc.instance _ _ _) Insts,
-    std.map Insts (x\r\ tc.instance _ r _ = x) R,
+    std.findall (tc.instance _ _ _ _) Insts,
+    std.map Insts (x\r\ tc.instance _ r _ _ = x) R,
     WantedLength is {origial_tc} + Len,
     std.assert! ({std.length R} = WantedLength) 
       "Unexpected number of instances",
@@ -22,7 +22,7 @@ Elpi Accumulate lp:{{
 }}.
 
 Elpi Query TC.Solver lp:{{
-  std.findall (tc.instance _ _ _) Rules,
+  std.findall (tc.instance _ _ _ _) Rules,
   std.length Rules Len,
   coq.elpi.accumulate _ "tc.db" (clause _ _ (origial_tc Len)).
 }}.
diff --git a/apps/tc/tests/test_coercion.v b/apps/tc/tests/test_coercion.v
@@ -49,21 +49,60 @@ Module Vehicle.
 
   Class Wheels (i: nat).
 
-  Class Boat.
-
-  Class NoWheels `{Wheels 0} := {
+  Class NoWheels := {
     (* the first argument of no_wheels is implicit! *)
-    no_wheels : Boat;
+    wheels0 :: Wheels 0;
   }.
 
-  Arguments no_wheels {_}.
-
-  Instance f `{H : Wheels 0} : NoWheels. Admitted.
+  Class Boat := {
+    wheels :: NoWheels
+  }.
 
-  Goal Wheels 0 -> Boat.
+  Goal Boat -> Wheels 0.
     intros.
-    apply no_wheels.
     apply _.
   Qed.
 
 End Vehicle.
+
+Module foo.
+  Class B (i : nat).
+
+  Section s.
+    (* Class with coercion depending on section parameters *)
+    Context (A : Type).
+    Class C (i : nat) : Set := {
+      f (x : A) :: B i
+    }.
+  End s.
+End foo.
+
+Module foo1.
+  Class B (i : nat).
+
+  Section s.
+    (* Class with coercion not depending on section parameters *)
+    Class C (i : nat) : Set := {
+      f :: B i
+    }.
+  End s.
+
+  Goal C 3 -> B 3.
+    apply _.
+  Abort.
+End foo1.
+
+Module localCoercion.
+  Class B (i : nat).
+  Section s.
+    Class C (i : nat) : Set := {
+      #[local] f :: B i
+    }.
+    Goal C 3 -> B 3.
+      apply _.
+    Qed.
+  End s.
+  Goal C 3 -> B 3.
+    Fail apply _.
+  Abort.
+End localCoercion.
diff --git a/apps/tc/tests/test_coercion_import.v b/apps/tc/tests/test_coercion_import.v
@@ -0,0 +1,8 @@
+From elpi.apps.tc.tests Require Import test_coercion.
+
+Import Animals.Bird1.
+
+
+Elpi Query TC.Solver lp:{{
+  true.
+}}.
diff --git a/apps/tc/tests/test_commands_API.v b/apps/tc/tests/test_commands_API.v
@@ -7,7 +7,7 @@ Elpi Accumulate lp:{{
   pred count i:gref, i:int.
   count GR Len :-
     if (const _ = GR)
-      (std.findall (tc.instance _ _ GR) Cl,
+      (std.findall (tc.instance _ _ GR _) Cl,
       std.assert! ({std.length Cl} = Len) 
       "Unexpected number of instances")
       true. 
diff --git a/apps/tc/tests/test_unfold.v b/apps/tc/tests/test_unfold.v
@@ -5,7 +5,7 @@ Module NAT.
   TC.Unfold Nat.succ.
   Class nat2 (T : nat -> nat).
 
-  Elpi Accumulate tc.db lp:{{
+  Elpi Accumulate TC.Solver lp:{{
     % Just to print what is beeing normalized
     :after "firstHook"
     tc.normalize-ty T _ :- coq.say "Normalizing" T, fail.
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
@@ -73,8 +73,9 @@ Elpi Db tc.db lp:{{
     type deterministic  search-mode.
     type classic        search-mode.
 
-    % [instance Path InstGR ClassGR], ClassGR is the class implemented by InstGR
-    pred instance o:list string, o:gref, o:gref.
+    % [instance Path InstGR ClassGR Locality], ClassGR is the class implemented by InstGR
+    % Locality is either the empty list, or [@local!], or [@global!]
+    pred instance o:list string, o:gref, o:gref, o:list prop.
 
     % [class ClassGR PredName SearchMode Modes], for each class GR, it contains
     % the name of its predicate and its SearchMode 
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
@@ -23,20 +23,23 @@ Set Warnings "+elpi".
 Elpi Command TC.Print_instances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate lp:{{
+  pred tc.list-printer-aux i:prop.
+  tc.list-printer-aux (tc.instance _ InstGR _ Locality) :-
+    coq.say InstGR "with locality" Locality.
+
   pred tc.list-printer i:gref, i:list prop.
   tc.list-printer _ [].
   tc.list-printer ClassGR Instances :- 
-    std.map Instances (x\r\ x = tc.instance _ r _) InstancesGR,
     coq.say "Instances list for" ClassGR "is:",
-    std.forall InstancesGR (x\ coq.say " " x). 
+    std.forall Instances tc.list-printer-aux. 
 
   main [str Class] :-
     std.assert! (coq.locate Class ClassGR) "The entered TC not exists",
-    std.findall (tc.instance _ _ ClassGR) Rules,
+    std.findall (tc.instance _ _ ClassGR _) Rules,
     tc.list-printer ClassGR Rules. 
   main [] :-
     std.forall {coq.TC.db-tc} (ClassGR\ sigma Rules\
-      std.findall (tc.instance _ _ ClassGR) Rules,
+      std.findall (tc.instance _ _ ClassGR _) Rules,
       tc.list-printer ClassGR Rules
     ).  
 }}.
@@ -141,7 +144,7 @@ Elpi Accumulate lp:{{
     coq.locate ClassStr ClassGR, 
     std.assert! (coq.TC.class? ClassGR) "Should pass the name of a type class",
     std.assert! (tc.class ClassGR PredName _ Modes) "Cannot find `class ClassGR _ _` in the db",
-    std.assert! (not (tc.instance _ _ ClassGR)) "Cannot set deterministic a class with an already existing instance",
+    std.assert! (not (tc.instance _ _ ClassGR _)) "Cannot set deterministic a class with an already existing instance",
     tc.add-tc-db _ (after "0") (tc.class ClassGR PredName tc.deterministic Modes :- !).
 }}.
 Elpi Typecheck.
diff --git a/builtin-doc/coq-builtin-synterp.elpi b/builtin-doc/coq-builtin-synterp.elpi
@@ -314,6 +314,7 @@ type clause id -> grafting -> prop -> clause.
 kind grafting type.
 type before id -> grafting.
 type after id -> grafting.
+type remove id -> grafting.
 type replace id -> grafting.
 
 % Specify to which module the clause should be attached to
diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi
@@ -558,8 +558,8 @@ external pred coq.version o:string, o:int, o:int, o:int.
 
 % To make the API more precise we use different data types for the names
 % of global objects.
-% Note: [ctype \"bla\"] is an opaque data type and by convention it is
-% written [@bla].
+% Note: [ctype "bla"] is an opaque data type and by convention it is written
+% [@bla].
 
 % Global constant name
 typeabbrev constant (ctype "constant").
@@ -1758,6 +1758,7 @@ type clause id -> grafting -> prop -> clause.
 kind grafting type.
 type before id -> grafting.
 type after id -> grafting.
+type remove id -> grafting.
 type replace id -> grafting.
 
 % Specify to which module the clause should be attached to
diff --git a/builtin-doc/elpi-builtin.elpi b/builtin-doc/elpi-builtin.elpi
@@ -449,6 +449,9 @@ pred ignore-failure! i:prop.
 ignore-failure! P :- P, !.
 ignore-failure! _.
 
+pred once i:prop.
+once P :- P, !.
+
 % [assert! C M] takes the first success of C or fails with message M 
 pred assert! i:prop, i:string.
 assert! Cond Msg :- (Cond ; fatal-error-w-data Msg Cond), !.
diff --git a/src/coq_elpi_builtins_synterp.ml b/src/coq_elpi_builtins_synterp.ml
diff --git a/src/coq_elpi_builtins_synterp.mli b/src/coq_elpi_builtins_synterp.mli
diff --git a/tests/test_tactic.v b/tests/test_tactic.v
