fix

Author: FissoreD

apps/tc/elpi/compile_goal.elpi

@@ -66,7 +66,7 @@ namespace tc {
       compile-full-aux (app [global (const C) | _] as G) L G' [tc.link.cs G' G | L] :- coq.env.projection? C _, !.
 
       % Link for primitive projection
-      compile-full-aux (app [primitive (proj P _) | _] as G) L G' [tc.link.cs G' G | L] :- coq.env.primitive-projection? P _, !.
+      compile-full-aux (app [primitive (proj P _) | _] as G) L G' [tc.link.cs G' G | L] :- coq.env.primitive-projection? P _ _, !.
 
       % Link for eta-redex
       compile-full-aux (fun Name_ Ty Bo as G) L G' [tc.link.eta G' (fun `_` Ty' Bo') | L'] :- maybe-eta G, !,

apps/tc/elpi/compile_instance.elpi

@@ -101,7 +101,7 @@ namespace tc {
         (pi x\ get-range-arity-aux T (B x) R1),
         min-max-nat R R1 R2.
       get-range-arity-aux _ (global _) @max-min :- !.
-      get-range-arity-aux _ (uvar _) @max-min :- !.
+      get-range-arity-aux _ uvar @max-min :- !.
       get-range-arity-aux _ (sort _) @max-min :- !.
       get-range-arity-aux _ (pglobal _ _) @max-min :- !.
       get-range-arity-aux A B _ :- coq.error "Count maximal arity failure" A B.
@@ -118,7 +118,7 @@ namespace tc {
       precompile-aux _ (primitive _ as C) A C A :- !.
       precompile-aux _ T A (tc.coercion T Scope) (s A) :- coq.safe-dest-app T HD _, tc.coercion-unify HD, !, free-var Scope.
       precompile-aux _ (app [global (const C) | _] as T) A (tc.canonical-projection T Scope N) (s A) :- coq.env.projection? C N, !, free-var Scope.
-      precompile-aux _ (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) (s A) :- coq.env.primitive-projection? P _, !, free-var Scope.
+      precompile-aux _ (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) (s A) :- coq.env.primitive-projection? P _ _, !, free-var Scope.
 
       % Detect maybe-eta term
       % TODO: should I precompile also the type of the fun and put it in the output term
@@ -387,8 +387,8 @@ namespace tc {
         i:list prop,
         o:prop.
       compile-premise L L2 P PTy ProofHd IsPositive ITy ProofArgsR 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,
         deterministic-prem TC NewPrem NewPrem',
         compile-ty L1 L2 ProofHd IsPositive ITy ProofArgsR [NewPrem' | PremR] Clause.

apps/tc/elpi/link.elpi

@@ -83,7 +83,7 @@ namespace tc {
       :index (_ 1)
       pred occurs-rigidly i:term, i:term.
       occurs-rigidly N N :- name N, !.
-      occurs-rigidly _ (uvar _) :- !, fail.
+      occurs-rigidly _ uvar :- !, fail.
       occurs-rigidly N (app A) :- exists! A (occurs-rigidly N).
       occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
 
@@ -127,10 +127,10 @@ namespace tc {
         rule solve-eta \ (eta A B _) <=> (unify-eta A B).
         rule \ solve-eta.
         % If two eta links have same lhs they rhs should unify
-        rule (N1 : G1 ?- eta (uvar X L1) (fun _ T1 B1) _) 
-            \ (N2 : G2 ?- eta (uvar X L2) (fun _ T2 B2) _) 
+        rule (N1 :> G1 ?- eta (uvar X L1) (fun _ T1 B1) _) 
+            \ (N2 :> G2 ?- eta (uvar X L2) (fun _ T2 B2) _) 
             | (pi x\ relocate L1 L2 (B2 x) (B2' x))
-        <=> (N1 : G1 ?- B1 = B2').
+        <=> (N1 :> G1 ?- B1 = B2').
       }
 
       :index (0 1)
@@ -139,7 +139,7 @@ namespace tc {
       eta A (fun _ _ B as T) _ :- not (var A), not (var B), !, unify-left-right A T.
       eta A (fun _ _ B as T) _ :- not (var (B _)), progress-eta-right? T T', !, A = T'. 
       eta A B                _ :- not (var A), !, progress-eta-left A B.
-      eta (uvar _ as A) B Vars :- 
+      eta (uvar as A) B Vars :- 
         scope-check A B, std.filter Vars (x\ var x) Vars', 
         declare_constraint (eta A B Vars') [_,A|Vars'].
     }
@@ -154,7 +154,7 @@ namespace tc {
       % app[A' x, t] instead of (A' x t).
       pred llam i:term, i:term.
       llam A (uvar _ S as T) :- distinct_names S, !, A = T.
-      llam (uvar _ as A) (app [(uvar HD _)|_] as T) :- !, 
+      llam (uvar as A) (app [(uvar as HD)|_] as T) :- !, 
         declare_constraint (llam A T) [_,A,HD].
       llam (fun _ _ _ as F) (app [(uvar _ Scope as H) | TL]) :- !, 
           std.drop-last 1 TL TL', 
@@ -168,10 +168,10 @@ namespace tc {
         rule solve-llam \ (llam A B) <=> (A = B).
         rule \ solve-llam.
         % If two llam links have same lhs they rhs should unify
-        rule (N1 : G1 ?- llam (uvar X L1) T1) 
-            \ (N2 : G2 ?- llam (uvar X L2) T2) 
+        rule (N1 :> G1 ?- llam (uvar X L1) T1) 
+            \ (N2 :> G2 ?- llam (uvar X L2) T2) 
             | (pi x\ relocate L1 L2 T2 T2')  
-        <=> (N1 : G1 ?- T1 = T2'). % TODO: instead of elpi unif, should use heuristics...
+        <=> (N1 :> G1 ?- T1 = T2'). % TODO: instead of elpi unif, should use heuristics...
       }
     }
 
@@ -184,19 +184,19 @@ namespace tc {
         coq.unify-eq T Record Err, Err = ok,
         Q = [coq.redflags.const Proj],
         coq.redflags.add coq.redflags.nored [coq.redflags.delta, coq.redflags.beta, coq.redflags.match | Q] RF,
-        @redflags! RF => coq.reduction.lazy.whd (app [ProjT, Record]) V',
+        (@redflags! RF => coq.reduction.lazy.whd (app [ProjT, Record]) V'),
         not (V' = match _ _ _), !,
         cs V V'.
       reduce-cs V T _ _ :- V = T.
 
       pred cs i:term, i:term.
       cs T1 T2 :- not (var T1), !, coq.unify-eq T1 T2 ok.
-      cs (uvar _ as V) (app [_, Arg] as T) :- not (ground_term Arg), !, get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
-      cs (uvar _ as V) (app [HD, _Arg] as T) :- 
+      cs (uvar as V) (app [_, Arg] as T) :- not (ground_term Arg), !, get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
+      cs (uvar as V) (app [HD, _Arg] as T) :- 
         tc.coercion-unify HD, !, 
         get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
 
-      cs (uvar _ as V) (app [HD | TL] as T) :- 
+      cs (uvar as V) (app [HD | TL] as T) :- 
         if (HD = global (const Proj), tc.proj->record Proj Record)
           (reduce-cs V T Record Proj)
           % Note: Below we cannot unify V and T since T may contain

apps/tc/src/rocq_elpi_tc_register.ml

@@ -23,7 +23,7 @@ let gref2elpi_term (gref: GlobRef.t) : Cmd.raw =
 let observer_class (x : Typeclasses.typeclass) : Rocq_elpi_arg_HOAS.Cmd.raw list = 
   [Cmd.String "new_class"; gref2elpi_term x.cl_impl]
 
-let observer_coercion add (x : Typeclasses.typeclass) : Coq_elpi_arg_HOAS.Cmd.raw list = 
+let observer_coercion add (x : Typeclasses.typeclass) : Rocq_elpi_arg_HOAS.Cmd.raw list = 
   let name2str x = Cmd.String (Names.Name.print x |> Pp.string_of_ppcmds) in
   let proj = x.cl_projs |> List.map (fun (x: Typeclasses.class_method) -> x.meth_name) in
   let mode = if add then "add_coercions" else "remove_coercions" in

apps/tc/tests/importOrder/sameOrderCommand.v

@@ -14,8 +14,8 @@ Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif.
-Elpi Accumulate File link.
 Elpi Accumulate File compile_goal.
+Elpi Accumulate File link.
 Elpi Accumulate File tc_same_order.
 
 

apps/tc/tests/test.v

@@ -119,7 +119,7 @@ Module HO_swap.
   Axiom (f : Type -> Type -> Type).
   Elpi Query TC.Solver lp:{{
     tc.link.eta.maybe-eta (fun `x` _ c0 \ fun `y` _ c1 \ A2 c1 c0),
-    tc.link.eta.maybe-eta (fun `x` _ c0 \ fun `y` _ c1 \ A2 (A c1) c0),
+    tc.link.eta.maybe-eta (fun `x` _ c0 \ fun `y` _ c1 \ A2 (A_ c1) c0),
     tc.link.eta.maybe-eta {{fun x y => f x y}}.
   }}.
 
@@ -129,7 +129,7 @@ Module HO_swap.
   Elpi Query TC.Solver lp:{{
     @pi-decl `x` {{Type -> Type}} f\ tc.precomp.instance.is-uvar f => 
       sigma T\
-        tc.precomp.instance {{c1 (fun x y => lp:f y x)}} T N _ _,
+        tc.precomp.instance {{c1 (fun x y => lp:f y x)}} T N_ _ _,
         std.assert! (T = app[{{c1}}, tc.maybe-eta-tm _ _]) "[TC] invalid precomp".
   }}.
 
@@ -204,7 +204,7 @@ Module HO_7.
   Qed.
 End HO_7.
 
-Module HO_81.
+(* Module HO_81.
   Class c1 (T : Type).
   Instance i1 F : c1 F. Qed.
 
@@ -223,11 +223,9 @@ Module HO_81.
     (* Failure is good, since here we simply check that the number of 
       uvar-pair built by tc.precomp is zero. This is because the type
       of ?X is Type (i.e. it has `arity` zero) *)
-    apply _.
-    Unshelve.
-    apply nat.
-  Qed.
-End HO_81.
+    Fail apply _.
+  Abort.
+End HO_81. *)
 
 Module HO_8.
   Class c1 (T : Type -> Type -> Type).
@@ -249,7 +247,7 @@ Module HO_9.
 
   Elpi Query TC.Solver lp:{{
     pi F\ sigma T\ decl F `x` {{Type -> Type}} ==> tc.precomp.instance.is-uvar F ==> 
-      tc.precomp.instance {{c1 (fun x => f (lp:F x) (lp:F x))}} T N _ _,
+      tc.precomp.instance {{c1 (fun x => f (lp:F x) (lp:F x))}} T _N _ _,
       std.assert! (T = app [{{c1}}, tc.maybe-eta-tm _ _]) "Invalid precompilation".
   }}.
 
@@ -293,13 +291,6 @@ Module HO_12.
   Instance i : Unit (forall x, x) := {}.
   Set Printing Existential Instances.
 
-  Elpi Accumulate TC.Solver lp:{{
-    % TODO: this rule should be removed if https://github.com/LPCIC/elpi/issues/256
-    % is solved
-    tc-elpi.apps.tc.tests.test.HO_12.tc-Unit {{forall (x:Prop), lp:(X x)}} {{i}} :-
-      X = (x\x).
-  }}.
-
   Goal forall (y: Prop), exists (F: Prop -> Prop), Unit (forall x, F x).
     intros.
     eexists ?[F].
@@ -328,7 +319,7 @@ Module HO_13.
   Qed.
 
   Elpi Query TC.Solver lp:{{
-    std.spy-do![Goal = {{Unit (forall x y, lp:(F x y))}},
+    std.spy-do![Goal = {{Unit (forall x y, lp:(F_ x y))}},
     tc.build-query-from-goal Goal Proof Q PP,
     do PP, Q,
     std.assert! (Proof = {{i f j}}) "Error"].
@@ -396,7 +387,7 @@ Module Llam_1.
     @pi-decl `x` {{Type -> Type}} f\ tc.precomp.instance.is-uvar f => 
       @pi-decl `x` {{Type -> Type}} g\ tc.precomp.instance.is-uvar g => 
         sigma T\
-          tc.precomp.instance {{A (fun x => lp:f (lp:g x))}} T N _ _,
+          tc.precomp.instance {{A (fun x => lp:f (lp:g x))}} T _N _ _,
           std.assert! (T = app[{{A}}, tc.maybe-eta-tm (fun _ _ (x\ tc.maybe-llam-tm _ _)) _]) "[TC] invalid precomp".
   }}.
 
@@ -512,12 +503,12 @@ Module CoqUvar.
   Class c1 (i:Type -> Type -> Type).
 
   Elpi Query TC.Solver lp:{{
-    tc.precomp.instance {{c1 (fun x y => lp:F y x)}} T _ _ _,
+    tc.precomp.instance {{c1 (fun x y => lp:F_ y x)}} T _ _ _,
     coq.say T,
     Expected = app[{{c1}}, tc.maybe-eta-tm (fun _ _ Inn) []],
     std.assert! (T = Expected) "[TC] invalid precompile1",
     pi x\ sigma ExpectedInn\
-      ExpectedInn = tc.maybe-eta-tm (A x) [x],
+      ExpectedInn = tc.maybe-eta-tm (A_ x) [x],
       std.assert! ((Inn x) = ExpectedInn) "[TC] invalid precompile2".
   }}.
 
@@ -603,10 +594,10 @@ Module CoqUvar4.
   Class c1 (T : Type -> Type -> Type).
 
   Elpi Query TC.Solver lp:{{
-    tc.precomp.instance {{c1 (fun x y => lp:X (lp:A x y) y)}} C _ _ _,
+    tc.precomp.instance {{c1 (fun x y => lp:X (lp:A_ x y) y)}} C _ _ _,
     Expected = app [{{c1}}, tc.maybe-eta-tm (fun _ _ Body1) _],
     Body1 = (x\ tc.maybe-eta-tm (fun _ _ (Body2 x)) [x]),
-    Body2 = (x\y\ app [X, (Y x y), y]),
+    Body2 = (x\y\ app [X, (Y_ x y), y]),
     std.assert! (C = Expected) "[TC] invalid compilation".
   }}.
 

apps/tc/theories/add_commands.v

@@ -10,6 +10,7 @@ From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
+From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc.elpi Extra Dependency "solver.elpi" as solver.
 From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
@@ -20,8 +21,8 @@ Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base tc_aux.
-Elpi Accumulate File unif modes link.
 Elpi Accumulate File compile_instance compiler compile_goal.
+Elpi Accumulate File unif modes link.
 Elpi Accumulate lp:{{  
   main L :- 
     args->str-list L L1,
@@ -33,8 +34,8 @@ Elpi Command TC.AddInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base tc_aux.
-Elpi Accumulate File unif modes link.
 Elpi Accumulate File compile_instance compiler compile_goal.
+Elpi Accumulate File unif modes link.
 Elpi Accumulate File parser_addInstances.
 Elpi Accumulate lp:{{
   main Arguments :- 
@@ -155,7 +156,6 @@ Elpi Accumulate  lp:{{
   main [trm T1, trm T2, int N] :- !, tc.add_tc.records_unif T1 T2 N.
   main L :- coq.error L.
 }}.
-Elpi Typecheck.
 
 Elpi Export TC.AddAllClasses.
 Elpi Export TC.AddRecordFields.

apps/tc/theories/db.v

@@ -101,7 +101,8 @@ Elpi Db tc.db lp:{{
     pred ho-link o:term, i:term, o:A.
     pred link.eta i:term, i:term.
     pred link.llam i:term, i:term.
-
+    pred link.cs i:term, i:term.
+    pred link.build-eta-llam-links i:term, i:list prop, o:term, o:list prop.
 
     % relates a projection to the its record type fully applied to fresh
     % variables, eg, rules have the shape: (pi P1 ... PN\ proj->record {{p}} {{r P1 .. PN}})

apps/tc/theories/tc.v

@@ -9,6 +9,7 @@ From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
+From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler.
 From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 From elpi.apps.tc.elpi Extra Dependency "compile_instance.elpi" as compile_instance.

builtin-doc/coq-builtin.elpi

@@ -934,9 +934,11 @@ external pred coq.env.projection? i:constant, o:int.
 external pred coq.env.primitive-projections i:inductive, 
                                             o:list (option (pair projection int)).
 
-% [coq.env.primitive-projection? Projection Compatibility constant] relates
-% a projection to its compatibility constant.
-external pred coq.env.primitive-projection? i:projection, o:constant.
+% [coq.env.primitive-projection? Projection Compatibility constant Index]
+% Relates a primitive projection to its compatibility constant. Index is set
+% to the constructor argument extracted by the projection (starting from 0).
+external pred coq.env.primitive-projection? o:projection, o:constant, 
+                                            o:int.
 
 % -- Sorts (and their universe level, if applicable) ----------------
 
@@ -1178,6 +1180,10 @@ external pred coq.CS.db o:list cs-instance.
 % or canonical Value, or both
 external pred coq.CS.db-for i:gref, i:cs-pattern, o:list cs-instance.
 
+% [coq.CS.canonical-projection? Projection] Tells if the projection can be
+% used for CS inference.
+external pred coq.CS.canonical-projection? i:constant.
+
 % [coq.TC.declare-class GR] Declare GR as a type class
 external pred coq.TC.declare-class i:gref.
 
@@ -1372,13 +1378,6 @@ external pred coq.arguments.simplification i:gref,
 external pred coq.arguments.set-simplification i:gref, 
                                                i:simplification_strategy.
 
-% [coq.arguments.reset-simplification GR] resets the behavior of the
-% simplification tactics.
-% Also resets the ! and / modifiers for the Arguments command.
-% Supported attributes:
-% - @global! (default: false)
-external pred coq.arguments.reset-simplification i:gref.
-
 % [coq.locate-abbreviation Name Abbreviation] locates an abbreviation.  It's
 % a fatal error if Name cannot be located.
 external pred coq.locate-abbreviation i:id, o:abbreviation.