[TC] local binders in evar scope during precompile + link.cs

Author: FissoreD

apps/tc/elpi/base.elpi

@@ -163,3 +163,8 @@ pred close-term-no-prune-ty i:(term -> list prop), i:term, o:list prop.
 close-term-no-prune-ty (x\ []) _ [] :- !.
 close-term-no-prune-ty (x\ [X x | Xs x]) Ty [@pi-decl `x` Ty x\ X x | Xs'] :- !, 
   close-term-no-prune-ty Xs Ty Xs'. 
+
+pred close-term-no-prune-fun i:(term -> list term), i:term, o:list term.
+close-term-no-prune-fun (x\ []) _ [] :- !.
+close-term-no-prune-fun (x\ [X x | Xs x]) Ty [fun _ Ty X | Xs'] :- 
+  close-term-no-prune-fun Xs Ty Xs'.

apps/tc/elpi/ho_compile.elpi

@@ -24,10 +24,15 @@ namespace tc {
         decompile-term-aux (sort _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (uvar as X) L X L :- !.
         decompile-term-aux (primitive _ as X) L X L :- !.
+        decompile-term-aux (tc.coercion T S) (pr [X|Xs] L1) Y (pr Xs' L3) :- !,
+          name Y X S,
+          decompile-term-aux T (pr Xs L1) T' (pr Xs' L2),
+          P = tc.link.cs Y T',
+          L3 = [P | L2].
         decompile-term-aux (tc.canonical-projection T S _) (pr [X|Xs] L1) Y (pr Xs' L3) :- !,
           name Y X S,
           decompile-term-aux T (pr Xs L1) T' (pr Xs' L2),
-          P = coq.unify-eq Y T' ok,
+          P = tc.link.cs Y T',
           L3 = [P | L2].
 
         decompile-term-aux (tc.maybe-eta-tm T S) (pr [X|XS] L1) Y (pr XS' [NL | L2]) :- !,
@@ -124,6 +129,7 @@ namespace tc {
         (pi t s r \ copy (tc.canonical-projection t s _) r :- !, copy t r, !) =>
         (pi t s r \ copy (tc.prod-range t s) r :- !, copy t r, !) =>
         (pi t s r \ copy (tc.maybe-llam-tm t s) r :- !, copy t r, !) =>
+        (pi t s r \ copy (tc.coercion t s) r :- !, copy t r, !) =>
           std.assert!  (copy A B) "[TC] clean-term error".
 
       pred main 
@@ -316,6 +322,8 @@ namespace tc {
 
       %                    Type     Var    Cnt    uvar-pair-list
       pred make-pairs-aux i:term, i:term, o:list prop.
+      make-pairs-aux Ty (fun _ _ IBo) L' :- !,
+        pi x\ make-pairs-aux Ty (IBo x) (L x), close-prop-no-prune L L'.
       make-pairs-aux (prod _ Ty Bo) V [pi x\ uvar-pair x Ty X' :- x == V, ! | L] :- !,
         pi x\ make-pairs-aux (Bo x) X' L.
       make-pairs-aux _ _ [].
@@ -335,11 +343,18 @@ namespace tc {
 
       pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
       decompile-problematic-term (primitive _ as C) A C A :- !.
-      
-      decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :-
-        prune V S, !, fold-map T L T' L2.
 
-      decompile-problematic-term (tc.prod-range T _) A T' A' :-
+      % there is no need to decompile T since no precompilation is done inside coercions
+      decompile-problematic-term (tc.coercion T S) L1 Y [tc.link.cs Y T|L1] :- !,
+        prune Y S.
+      % there is no need to decompile T since no precompilation is done inside CS
+      decompile-problematic-term (tc.canonical-projection T S _) L1 Y [tc.link.cs Y T|L1] :- !,
+        prune Y S.
+
+      decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :- !,
+        prune V S, fold-map T L T' L2.
+
+      decompile-problematic-term (tc.prod-range T _) A T' A' :- !,
         fold-map T A T' A'.
 
       decompile-problematic-term (tc.maybe-llam-tm (app [app[H|S] | NPF]) Sc) L Z [NL|L'] :- !,
@@ -399,6 +414,10 @@ namespace tc {
         build-eta-links-of-vars-aux Hd S L',
         build-eta-links-of-vars Vars L'',
         std.append L' L'' L.
+      build-eta-links-of-vars [fun _ Ty Bo|Vars] L :-
+        (pi x\ build-eta-links-of-vars [Bo x] (L' x), close-term-no-prune-ty L' Ty L''),
+        build-eta-links-of-vars Vars L''',
+        std.append L'' L''' L.
     }
 
     %          Goal    Goal'      Links

apps/tc/elpi/ho_link.elpi

@@ -130,6 +130,34 @@ namespace tc {
       }
     }
 
+    namespace cs {
+      pred cs i:term, i:term.
+      % TODO: suspend link on vars in T
+      cs V T :- var V, !, get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
+      cs T1 T2 :- coq.unify-eq T1 T2 ok.
+
+      % pred unify-rebinding-names i:list prop, i:list prop, i:term, i:term.
+      % unify-rebinding-names [] T1 [] T2 (unify-eq T1V T2) :- !, copy T1 T1V.
+      % unify-rebinding-names [N|NS] T1 [V|VS] T2 C :- !, copy N V => unify-rebinding-names NS T1 VS T2 C.
+      % unify-rebinding-names [] T1 VS T2 C :- !, unify-rebinding-names [] {coq.subst-prod VS T1} [] T2 C. % FIXME: reduction
+      % unify-rebinding-names [_|NS] (prod _ _ F) [] T2 C :- !,                      % FIXME: reduction
+      %   assert! (pi x\ F x = F1) "restriction bug", unify-rebinding-names NS F1 [] T2 C.
+
+      pred unify-under-ctx i:list term, i:list term, i:term, i:term, i:term, i:term.
+      unify-under-ctx [] [] A B V1 V2 :- copy A A', copy V1 V1', !, coq.unify-eq A' B ok, !, V1' = V2.
+      unify-under-ctx [X|XS] [Y|YS] A B V1 V2:- (copy X Y :- !) => unify-under-ctx XS YS A B V1 V2.
+
+      % TODO: there could be two same variables suspended on non unifyable
+      % terms, this should be detected and raise a failure.
+      % An example of this is in test/canonical_struct.v
+      constraint cache def decl coq.unify-eq ?- solve-cs cs {
+        rule solve-cs \ (Ctx ?- cs A B) <=> (Ctx => coq.unify-eq A B ok).
+        rule (Ctx1 ?- cs (uvar A L1 as X) T1) \ (Ctx2 ?- cs (uvar A L2 as Y) T2) <=>
+          (Ctx2 => unify-under-ctx L1 L2 T1 T2 X Y).
+        rule \ solve-cs.
+      }
+    }
+
     pred eta i:term, o:term.
     eta A B :- eta.eta A B.
 
@@ -141,5 +169,11 @@ namespace tc {
 
     pred solve-llam.
     solve-llam :- declare_constraint solve-llam [_].
+
+    pred cs i:term, i:term.
+    cs A B :- cs.cs A B.
+
+    pred solve-cs.
+    solve-cs :- declare_constraint solve-cs [_].
   }
 }

apps/tc/elpi/ho_precompile.elpi

@@ -106,6 +106,7 @@ namespace tc {
       precompile-aux _ (pglobal _ _ as C) A C A :- !.
       precompile-aux _ (sort _ as C) A C A :- !.
       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.
 
@@ -229,12 +230,20 @@ namespace tc {
       precompile-aux (pglobal _ _ as C) A C A :- !.
       precompile-aux (sort _ as C) A C A :- !.
       precompile-aux (primitive _ as C) A C A :- !.
+      
+      precompile-aux T A (tc.coercion T Scope) A :- 
+        coq.safe-dest-app T HD _, tc.coercion-unify HD, !, names Scope.
+      precompile-aux (app [global (const C) | _] as T) A (tc.canonical-projection T Scope N) A :- 
+        coq.env.projection? C N, !, names Scope.
+      precompile-aux (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) A :- 
+        coq.env.primitive-projection? P _, !, names Scope.
+
 
       % Detect maybe-eta term
       precompile-aux (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty' B') Scope) M :-
         maybe-eta T, !,
         names Scope,
-        (pi x\ precompile-aux (B x) N (B' x) M'),
+        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-no-prune-fun MM Ty M') "[TC] should not fail1",
         precompile-aux Ty M' Ty' M.
 
       % Detect maybe-beta term
@@ -244,10 +253,9 @@ namespace tc {
         names Scope1,
         std.fold-map NPF N precompile-aux NPF1 M. 
 
-      % In the goal there are 
       precompile-aux (prod Name Ty B) N (tc.prod-range (prod Name Ty' B') (r-ar z MaxAr)) P :- !,
         count-prod Ty MaxAr,
-        std.assert! (pi x\ precompile-aux (B x) N (B' x) M) "[TC] should not fail",
+        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-no-prune-fun MM Ty M) "[TC] should not fail2",
         precompile-aux Ty M Ty' P.
 
       % Working with fun

apps/tc/elpi/solver.elpi

@@ -32,6 +32,7 @@ namespace tc {
     if-true print-compiled-goal (coq.say "[TC] the compiled goal is" Q), !,
     tc.time-it tc.oTC-time-instance-search (
       do PostProcess, Q,
+      tc.link.solve-cs,
       tc.link.solve-eta, % Trigger eta links
       tc.link.solve-llam % Trigger llam links
     ) "instance search".

apps/tc/elpi/tc_aux.elpi

@@ -219,4 +219,12 @@ namespace tc {
     list term ->  % The list of FV in the precomp subterm
     int ->
     term.
+
+  :index (5)
+  pred coercion-unify i:term.
+
+  type coercion
+    term ->
+    list term ->
+    term.
 }

apps/tc/tests/canonical_struct.v

@@ -99,4 +99,133 @@ Module CS5.
     Unshelve.
     apply (ofe_any nat).
   Qed.
-End CS5.
+End CS5.
+
+Module CS6.
+  Structure ofe := Ofe { ofe_car :> Type; }.
+  Structure cmra := Cmra { cmra_car :> Type; }.
+
+  Coercion cmra_ofeO (A : cmra) := Ofe A.
+
+  Elpi Accumulate tc.db lp:{{
+    tc.coercion-unify {{cmra_ofeO}}.
+  }}.
+
+  Canonical Structure ofe_nat := Ofe nat.
+  Canonical Structure cmra_nat := Cmra nat.
+
+  Class C (i: ofe).
+
+  Instance i: forall (c : cmra), C (cmra_ofeO c) := {}.
+
+  Goal C ofe_nat.
+    apply _.
+  Qed.
+End CS6.
+
+Module CS7.
+  Structure ofe := Ofe { ofe_car :> Type; }.
+  Structure cmra := Cmra { cmra_car :> Type; }.
+
+  Coercion cmra_ofeO (A : cmra) := Ofe A.
+
+  Elpi Accumulate tc.db lp:{{
+    tc.coercion-unify {{cmra_ofeO}}.
+  }}.
+
+  Canonical Structure ofe_bool := Ofe bool.
+  Canonical Structure cmra_bool := Cmra bool.
+
+  Class C (i: ofe).
+
+  Class D (i: Type).
+  Instance d : D bool := {}.
+
+  Instance i: forall (c : cmra), D (cmra_car c) -> C (cmra_ofeO c) := {}.
+  Elpi Print TC.Solver.
+
+  Goal C ofe_bool.
+    apply _.
+  Qed.
+
+  Canonical Structure ofe_nat := Ofe nat.
+  Canonical Structure cmra_nat := Cmra nat.
+
+  Goal exists a, C a.
+    eexists.
+    apply _.
+  Qed.
+End CS7.
+
+Module CS8.
+  Structure ofe := Ofe { ofe_car :> Type; }.
+  Canonical Structure ofe_bool := Ofe bool.
+  Class C (i : Type).
+  Instance i : C ofe_bool := {}.
+
+  (* 
+    Test for constraint activation using tc.link.solve-cs: After
+    tc-instance-search, we have the suspended goal `tc.link.cs X ofe_bool` that
+    must be activated. This activation need to load the context before the 
+    call to unify-eq since we need to load the type of `x`
+  *)
+  Goal forall (x: nat), exists X, C X.
+    eexists. apply _.
+  Qed.
+
+  (* TODO: error in llam link *)
+  (* Goal forall (x: nat), exists X, C (X x).
+    eexists.
+    Elpi Trace Browser.
+    (* Elpi TC Solver Deactivate TC.Solver. *)
+    apply _.
+  Qed *)
+End CS8.
+
+Module CS9.
+  Structure ofe := Ofe { ofe_car :> Type; }.
+  Canonical Structure ofe_bool := Ofe bool.
+  Canonical Structure ofe_nat := Ofe nat.
+
+  Class loop.
+  Instance l : loop -> loop := {}.
+  Class C (i : Type) (i : Type).
+  Instance i : loop -> C ofe_bool ofe_nat := {}.
+
+  (* 
+    Here we have two suspended goal on X with cs links. The same variable
+    is linked with ofe_bool and ofe_nat. Since they don't unfy, the instance
+    `i` cannot be used.
+  *)
+  Goal exists X, C X X.
+    eexists.
+    Fail apply _.
+  Abort.
+End CS9.
+
+Module CS10.
+  Structure ofe := Ofe { ofe_car :> Type; }.
+  Canonical Structure ofe_bool := Ofe bool.
+
+  Class C (i : Type).
+  Instance i : C bool := {}.
+
+  (* Here the projection is in the goal *)
+  Goal C (ofe_car ofe_bool). apply _. Qed.
+End CS10.
+
+Module CS11.
+  Structure ofe := Ofe { ofe_car :> Type; }.
+  Canonical Structure ofe_bool := Ofe bool.
+
+  Class D (i : ofe).
+  Instance d : D (ofe_bool) := {}.
+
+  Class C (i : Type).
+  Instance i X:  D X -> C (ofe_car X) := {}.
+
+  (* Here the projection is in the goal *)
+  Goal exists X, C (ofe_car X). eexists.
+    apply _.
+    Show Proof.
+  Qed.

apps/tc/tests/test.v

@@ -277,6 +277,54 @@ Module HO_10.
   Qed.
 End HO_10.
 
+Module HO_11.
+  Class Unit (i : Prop).
+  Instance i F : Unit (forall (f : Prop), F f) := {}.
+  Goal Unit (forall x, x).
+    apply _.
+  Qed.
+End HO_11.
+
+Module HO_12.
+  Class Unit (i : Prop).
+  Instance i : Unit (forall x, x) := {}.
+  Set Printing Existential Instances.
+  Goal forall (y: Prop), exists (F: Prop -> Prop), Unit (forall x, F x).
+    intros.
+    eexists ?[F].
+    Unshelve.
+    2: { refine (fun x => _); shelve. }
+    simpl.
+    Set Printing Existential Instances.
+    apply _.
+  Qed.
+End HO_12.
+
+Module HO_13.
+  Class Unit (i : Prop).
+  Class PP (i : Prop -> Prop -> Prop).
+  Axiom f : Prop -> Prop -> Prop.
+  Instance i F : PP (fun x y => F y x) -> Unit (forall (x y: Prop), F y x) := {}.
+  Instance j : PP (fun x y => f y x) := {}.
+  Check _ : (Unit (forall x y, _)).
+
+  Goal exists (X: Prop -> Prop -> Prop), Unit (forall x y, X x y).
+    eexists.
+    Unshelve.
+    2: { refine (fun _ _ => _); shelve. }
+    simpl.
+    apply _.
+  Qed.
+
+  Elpi Query TC.Solver lp:{{
+    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"].
+  }}.
+End HO_13.
+
+
 Module HO_scope_check1.
   Axiom f : Type -> (Type -> Type) -> Type.
   Axiom g : Type -> Type -> Type.
@@ -565,7 +613,4 @@ Module CoqUvar4.
     do 1 eexists.
     apply _.
   Qed.
-End CoqUvar4.
-
-(* TODO: add test with negative premise having a variable with type (M A) where M and A are coq uvar,
-         this is in order to clean-term with llam *)
+End CoqUvar4.