From 6105b05d35bb8cfc0846258768d3445c2db0aaca Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 2 Jul 2024 11:22:36 +0200
Subject: [PATCH 01/32] [TC] primitive constructor for fold in instance
 (pre-)compilation

---
 apps/tc/elpi/ho_compile.elpi    | 3 +++
 apps/tc/elpi/ho_precompile.elpi | 3 ++-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 498883ed1..e99dce65e 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -23,6 +23,7 @@ namespace tc {
         decompile-term-aux (pglobal _ _ as T) L T' L :- !, copy T T', !.
         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.maybe-eta-tm T S) (pr [X|XS] L1) Y (pr XS' [NL | L2]) :- !,
           name Y X S,
@@ -327,6 +328,8 @@ namespace tc {
         get-uva-pair-arity Y L Z.
 
       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.
 
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index dd5bf3a28..e424996d2 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/apps/tc/elpi/ho_precompile.elpi
@@ -105,6 +105,7 @@ namespace tc {
       precompile-aux _ (global _ as C) A C A :- !.
       precompile-aux _ (pglobal _ _ as C) A C A :- !.
       precompile-aux _ (sort _ as C) A C A :- !.
+      precompile-aux _ (primitive _ as C) A C A :- !.
 
       % Detect maybe-eta term
       % TODO: should I precompile also the type of the fun and put it in the output term
@@ -142,7 +143,6 @@ namespace tc {
       %   precompile-aux IsP Ty A Ty1 A1, pi x\ is-name x => precompile-aux IsP (F x) A1 (F1 x) A2.
       % precompile-aux IsP (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
       %   precompile-aux IsP T A T1 A1, precompile-aux IsP Rty A1 Rty1 A2, std.fold-map B A2 (precompile-aux IsP) B1 A3.
-      % precompile-aux _ (primitive _ as C) A C A :- !.
       % precompile-aux IsP (uvar M L as X) A W A1 :- var X, !, std.fold-map L A (precompile-aux IsP) L1 A1, coq.mk-app-uvar M L1 W.
       % % when used in CHR rules
       % precompile-aux IsP (uvar X L) A (uvar X L1) A1 :- std.fold-map L A (precompile-aux IsP) L1 A1.
@@ -226,6 +226,7 @@ namespace tc {
       precompile-aux (global _ as C) A C A :- !.
       precompile-aux (pglobal _ _ as C) A C A :- !.
       precompile-aux (sort _ as C) A C A :- !.
+      precompile-aux (primitive _ as C) A C A :- !.
 
       % Detect maybe-eta term
       precompile-aux (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty' B') Scope) M :-

From d01790e94ade10710764e660d791f2c3b25e9615 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 2 Jul 2024 16:54:44 +0200
Subject: [PATCH 02/32] [TC] canonical proj solved with coq.unify-eq

---
 apps/tc/elpi/ho_compile.elpi     |   5 ++
 apps/tc/elpi/ho_precompile.elpi  |   4 +-
 apps/tc/elpi/tc_aux.elpi         |   6 ++
 apps/tc/tests/canonical_struct.v | 102 +++++++++++++++++++++++++++++++
 4 files changed, 116 insertions(+), 1 deletion(-)
 create mode 100644 apps/tc/tests/canonical_struct.v

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index e99dce65e..88635f290 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -24,6 +24,11 @@ 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.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,
+          L3 = [P | L2].
 
         decompile-term-aux (tc.maybe-eta-tm T S) (pr [X|XS] L1) Y (pr XS' [NL | L2]) :- !,
           name Y X S,
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index e424996d2..b59a8c74e 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/apps/tc/elpi/ho_precompile.elpi
@@ -106,6 +106,8 @@ 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 _ (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.
 
       % Detect maybe-eta term
       % TODO: should I precompile also the type of the fun and put it in the output term
@@ -173,7 +175,7 @@ namespace tc {
                 (tc.prod-range (prod _ T Bo) 3)
               since x is applied at most 3 times in Bo
                 ==> This helps charging the right number of `eta-link` for map-deduplication rule
-        N is the number of problematic terms in T
+        N is the number of problematic terms in T + nb of projections
     */
     pred instance i:term, o:term, o:nat, o:list univ, o:list univ-instance.
     instance T T' N UnivConstL UnivInstL :-
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index b1583a20c..f8d1c8835 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -215,3 +215,9 @@ namespace tc {
     list term ->     % The eta-expanded version of X, from X^{len(PF)} to X^{len(PF)+len(NPF)}
     term.
 }
+
+type tc.canonical-projection
+  term ->       % The current precompiled subterm
+  list term ->  % The list of FV in the precomp subterm
+  int ->
+  term.
\ No newline at end of file
diff --git a/apps/tc/tests/canonical_struct.v b/apps/tc/tests/canonical_struct.v
new file mode 100644
index 000000000..838c10d3d
--- /dev/null
+++ b/apps/tc/tests/canonical_struct.v
@@ -0,0 +1,102 @@
+From elpi.apps Require Import tc.
+
+Module CS1.
+
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_nat : ofe := Ofe nat.
+
+  Class C (I : Type).
+
+  Instance c : C (ofe_car ofe_nat). Qed.
+  Goal C (Ofe nat). apply _. Qed. (* No CS search *)
+  Goal exists x, C (Ofe x). eexists. apply _. Qed. (* CS Search to assign x *)
+  Goal C (ofe_car ofe_nat). apply _. Qed.
+
+End CS1.
+
+Module CS2.
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_nat : ofe := Ofe nat.
+
+  Class C (I : Type).
+
+  Instance c : C (Ofe nat). Qed.
+  Goal C (Ofe nat). apply _. Qed. (* No CS search *)
+  Goal exists x, C (Ofe x). eexists. apply _. Qed. (* CS Search to assign x *)
+  Goal C (ofe_car ofe_nat). apply _. Qed.
+
+End CS2.
+
+(* With primitive projection *)
+Module CS3.
+  Class C (I : Type).
+
+  #[local] Set Primitive Projections.
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_nat : ofe := Ofe nat.
+
+  Instance c : C ofe_nat.(ofe_car). Qed.
+  Goal C (Ofe nat). apply _. Qed. (* No CS search *)
+  Goal exists x, C (Ofe x). eexists. apply _. Qed. (* CS Search to assign x *)
+  Goal C (ofe_car ofe_nat). apply _. Qed.
+
+End CS3.
+
+Module CS4.
+  Class C (I : Type).
+
+  #[local] Set Primitive Projections.
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_nat : ofe := Ofe nat.
+
+  Instance c : C (Ofe nat).(ofe_car). Qed.
+  Goal C (Ofe nat). apply _. Qed. (* No CS search *)
+  Goal exists x, C (Ofe x). eexists. apply _. Qed. (* CS Search to assign x *)
+  Goal C (ofe_car ofe_nat). apply _. Qed.
+
+End CS4.
+
+(* With bound variables *)
+Module CS5.
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_any x : ofe := Ofe x.
+
+  Class C (I : Type -> Type).
+  Axiom f : ofe -> Type.
+
+  Instance c X : C (fun x => (Ofe (f (X x)))). Qed.
+  Goal C (fun x => (Ofe (f x))). apply _. Qed. (* No CS search *)
+  Goal C (fun (_: Type) => Ofe (f nat)). apply _. Qed. (* CS Search to assign x *)
+  Goal exists X, C (fun y => ofe_car (X y)). eexists.
+    apply _.
+    Unshelve.
+    apply (ofe_any nat).
+  Qed.
+
+  Lemma coq_unif_fail: exists X Y, (fun (y: Type) => ofe_car (X y)) = (fun _ => Y).
+    do 2 eexists.
+    Fail reflexivity.
+  Abort.
+    
+  Goal exists Z, C (fun _ => Z). eexists.
+    (* 
+      Note that here, coq8.20 unification algorithm would fail to unify
+      with error 
+        Unable to unify "?Y" with "ofe_car (?X x)" as "ofe_car (?X x)" 
+        contains local variables.
+    *)
+    apply _.
+    Unshelve.
+    apply (ofe_any nat).
+  Qed.
+End CS5.
\ No newline at end of file

From 681e9c19a3124a8316a27d692d606a14c3c6ab44 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 3 Jul 2024 13:17:45 +0200
Subject: [PATCH 03/32] [TC] clean-term also for tc.canonical-projection

---
 apps/tc/elpi/ho_compile.elpi | 1 +
 1 file changed, 1 insertion(+)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 88635f290..2ce8b11d7 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -121,6 +121,7 @@ namespace tc {
       pred clean-term i:term, o:term.
       clean-term A B :-
         (pi t s r \ copy (tc.maybe-eta-tm  t s) r :- !, copy t r, !) =>
+        (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, !) =>
           std.assert!  (copy A B) "[TC] clean-term error".

From f8f6439260b7140fd6add1627befce3ea8f35750 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 10 Jul 2024 14:08:18 +0200
Subject: [PATCH 04/32] [TC] compilation of primitive projections to their
 compatibility constants

---
 apps/tc/elpi/ho_compile.elpi     |  5 +++--
 apps/tc/tests/canonical_struct.v | 21 ++++++++++++++++++++-
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 2ce8b11d7..2d3b388a6 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -23,7 +23,7 @@ namespace tc {
         decompile-term-aux (pglobal _ _ as T) L T' L :- !, copy T T', !.
         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 (primitive (proj P _)) L (global (const Y)) L :- !, coq.env.primitive-projection? P Y.
         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),
@@ -334,7 +334,8 @@ namespace tc {
         get-uva-pair-arity Y L Z.
 
       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 (primitive (proj P _)) A (global (const Y)) A :- !, 
+        coq.env.primitive-projection? P Y.
       
       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.
diff --git a/apps/tc/tests/canonical_struct.v b/apps/tc/tests/canonical_struct.v
index 838c10d3d..1a36e4330 100644
--- a/apps/tc/tests/canonical_struct.v
+++ b/apps/tc/tests/canonical_struct.v
@@ -99,4 +99,23 @@ Module CS5.
     Unshelve.
     apply (ofe_any nat).
   Qed.
-End CS5.
\ No newline at end of file
+End CS5.
+
+Module CS6.
+  #[projections(primitive=yes)]
+  Structure ofe := Ofe { ofe_car : Type; }.
+
+  #[projections(primitive=no)] (* TODO: Putting primitive to yes leads to a unification error. Why? *)
+  Structure cmra := { cmra_car :> Type; }.
+  Canonical Structure cmra_ofeO (A : cmra) : ofe := Ofe A.
+
+  Class C (I : Type).
+  Instance c : forall (A : ofe), C ((A).(ofe_car)) := {}.
+
+  Section s.
+    Context {cmra : cmra}.
+    Goal C (cmra_car cmra).
+      apply _.
+    Qed.
+  End s.
+End CS6.

From 5564012059f20beeedb49693890f45bdadd05803 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 10 Jul 2024 16:26:57 +0200
Subject: [PATCH 05/32] Revert "[TC] compilation of primitive projections to
 their compatibility constants"

This reverts commit 6c639781fd4e3818332fc73fe205e1d52eeb321d.
---
 apps/tc/elpi/ho_compile.elpi     |  5 ++---
 apps/tc/tests/canonical_struct.v | 21 +--------------------
 2 files changed, 3 insertions(+), 23 deletions(-)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 2d3b388a6..2ce8b11d7 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -23,7 +23,7 @@ namespace tc {
         decompile-term-aux (pglobal _ _ as T) L T' L :- !, copy T T', !.
         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 (proj P _)) L (global (const Y)) L :- !, coq.env.primitive-projection? P Y.
+        decompile-term-aux (primitive _ as X) L X L :- !.
         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),
@@ -334,8 +334,7 @@ namespace tc {
         get-uva-pair-arity Y L Z.
 
       pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
-      decompile-problematic-term (primitive (proj P _)) A (global (const Y)) A :- !, 
-        coq.env.primitive-projection? P Y.
+      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.
diff --git a/apps/tc/tests/canonical_struct.v b/apps/tc/tests/canonical_struct.v
index 1a36e4330..838c10d3d 100644
--- a/apps/tc/tests/canonical_struct.v
+++ b/apps/tc/tests/canonical_struct.v
@@ -99,23 +99,4 @@ Module CS5.
     Unshelve.
     apply (ofe_any nat).
   Qed.
-End CS5.
-
-Module CS6.
-  #[projections(primitive=yes)]
-  Structure ofe := Ofe { ofe_car : Type; }.
-
-  #[projections(primitive=no)] (* TODO: Putting primitive to yes leads to a unification error. Why? *)
-  Structure cmra := { cmra_car :> Type; }.
-  Canonical Structure cmra_ofeO (A : cmra) : ofe := Ofe A.
-
-  Class C (I : Type).
-  Instance c : forall (A : ofe), C ((A).(ofe_car)) := {}.
-
-  Section s.
-    Context {cmra : cmra}.
-    Goal C (cmra_car cmra).
-      apply _.
-    Qed.
-  End s.
-End CS6.
+End CS5.
\ No newline at end of file

From 11e5ae9b7e84c3155f2bead7e988a5b03ce1aa1e Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Fri, 12 Jul 2024 14:16:22 +0200
Subject: [PATCH 06/32] [TC] put cnonical projection in tc namespace

---
 apps/tc/elpi/tc_aux.elpi | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index f8d1c8835..5091b8fcd 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -214,10 +214,10 @@ namespace tc {
     term ->          % The current precompiled subterm: shape is app[app[X,PF],NPF]
     list term ->     % The eta-expanded version of X, from X^{len(PF)} to X^{len(PF)+len(NPF)}
     term.
-}
 
-type tc.canonical-projection
-  term ->       % The current precompiled subterm
-  list term ->  % The list of FV in the precomp subterm
-  int ->
-  term.
\ No newline at end of file
+  type canonical-projection
+    term ->       % The current precompiled subterm
+    list term ->  % The list of FV in the precomp subterm
+    int ->
+    term.
+}
\ No newline at end of file

From d182f9f56170810ab926e275da51b3a9ae1802d4 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Fri, 12 Jul 2024 15:45:07 +0200
Subject: [PATCH 07/32] remove reduntant calls to Elpi Typecheck

---
 apps/tc/theories/add_commands.v | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index fcecf6d33..5d942fdad 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -19,25 +19,15 @@ Set Warnings "+elpi".
 
 Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
-Elpi Typecheck.
 Elpi Accumulate Db tc_options.db.
-Elpi Typecheck.
 Elpi Accumulate File base.
-Elpi Typecheck.
 Elpi Accumulate File tc_aux.
-Elpi Typecheck.
 Elpi Accumulate File ho_precompile.
-Elpi Typecheck.
 Elpi Accumulate File unif.
-Elpi Typecheck.
 Elpi Accumulate File ho_link.
-Elpi Typecheck.
 Elpi Accumulate File ho_compile.
-Elpi Typecheck.
 Elpi Accumulate File compiler1.
-Elpi Typecheck.
 Elpi Accumulate File modes.
-Elpi Typecheck.
 Elpi Accumulate lp:{{  
   main L :- 
     args->str-list L L1,

From fc58cf4b64a3dd49eda52271bd4738d24ad92ff1 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 30 Jul 2024 12:39:14 +0200
Subject: [PATCH 08/32] [TC] local binders in evar scope during precompile +
 link.cs

---
 apps/tc/elpi/base.elpi           |   5 ++
 apps/tc/elpi/ho_compile.elpi     |  29 +++++--
 apps/tc/elpi/ho_link.elpi        |  34 ++++++++
 apps/tc/elpi/ho_precompile.elpi  |  14 +++-
 apps/tc/elpi/solver.elpi         |   1 +
 apps/tc/elpi/tc_aux.elpi         |   8 ++
 apps/tc/tests/canonical_struct.v | 131 ++++++++++++++++++++++++++++++-
 apps/tc/tests/test.v             |  53 ++++++++++++-
 8 files changed, 262 insertions(+), 13 deletions(-)

diff --git a/apps/tc/elpi/base.elpi b/apps/tc/elpi/base.elpi
index 537331ef8..d1ca5f72c 100644
--- a/apps/tc/elpi/base.elpi
+++ b/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'.
diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 2ce8b11d7..fbc3824e8 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/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
diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
index 5a7afff00..91a601495 100644
--- a/apps/tc/elpi/ho_link.elpi
+++ b/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 [_].
   }
 }
\ No newline at end of file
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index b59a8c74e..ba936a74d 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/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
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 97596e4ed..7a61aed70 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/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".
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index 5091b8fcd..1b90f7b6c 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -220,4 +220,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.
 }
\ No newline at end of file
diff --git a/apps/tc/tests/canonical_struct.v b/apps/tc/tests/canonical_struct.v
index 838c10d3d..8df1b417a 100644
--- a/apps/tc/tests/canonical_struct.v
+++ b/apps/tc/tests/canonical_struct.v
@@ -99,4 +99,133 @@ Module CS5.
     Unshelve.
     apply (ofe_any nat).
   Qed.
-End CS5.
\ No newline at end of file
+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.
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index 92a6a614e..3bb6e175c 100644
--- a/apps/tc/tests/test.v
+++ b/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 *)
\ No newline at end of file
+End CoqUvar4.
\ No newline at end of file

From a9525a1a73738884ea6d8157f60f25ce89237178 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Fri, 2 Aug 2024 17:19:23 +0200
Subject: [PATCH 09/32] [TC] add TC.AddRecordFields command + better chr for
 canon struct

---
 apps/cs/README.md                |  2 +-
 apps/tc/elpi/ho_link.elpi        | 20 +++++++++++++++++---
 apps/tc/elpi/ho_precompile.elpi  | 15 +++++++++++++--
 apps/tc/elpi/solver.elpi         |  2 ++
 apps/tc/tests/canonical_struct.v |  8 ++++++--
 apps/tc/tests/test.v             |  8 ++++++++
 apps/tc/theories/add_commands.v  | 28 ++++++++++++++++++++++++++++
 apps/tc/theories/db.v            |  3 +++
 8 files changed, 78 insertions(+), 8 deletions(-)

diff --git a/apps/cs/README.md b/apps/cs/README.md
index 852b063a1..898a23491 100644
--- a/apps/cs/README.md
+++ b/apps/cs/README.md
@@ -16,7 +16,7 @@ The `cs` predicate lives in the database `cs.db`
 pred cs i:goal-ctx, o:term, o:term.
 ```
 
-By addings rules for this predicate one can recover from a CS instance search failure
+By adding rules for this predicate one can recover from a CS instance search failure
 error, that is when `Lhs` and `Rhs` are not unifiable using a canonical structure registered
 by Coq.
 
diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
index 91a601495..1173abb26 100644
--- a/apps/tc/elpi/ho_link.elpi
+++ b/apps/tc/elpi/ho_link.elpi
@@ -131,10 +131,24 @@ namespace tc {
     }
 
     namespace cs {
+      pred reduce-cs i:term, i:term, i:term, i:constant.
+      reduce-cs V (app [ProjT, T]) Record Proj :-
+        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',
+        not (V' = match _ _ _), !,
+        cs V V'.
+      reduce-cs V T _ _ :- V = T.
+
       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.
+      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 | _] as T) :- 
+        if (HD = global (const Proj), tc.proj->record Proj Record)
+          (reduce-cs V T Record Proj)
+          (coq.unify-eq V T ok).
+      cs T1 T2 :- not (T2 = app _), !, 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.
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index ba936a74d..6d9c42763 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/apps/tc/elpi/ho_precompile.elpi
@@ -224,6 +224,17 @@ namespace tc {
       split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
       split-pf Xs _ [] Xs.
 
+      pred used i:term, i:term.
+      used X (uvar _ S) :- std.mem! S X, !.
+      used X (fun _ _ Bo) :- pi x\ used X (Bo x).
+
+      pred close-term-prune-safe-fun i:(term -> list term), i:term, o:list term.
+      close-term-prune-safe-fun (x\ []) _ [] :- !.
+      close-term-prune-safe-fun (x\ [X x | Xs x]) Ty [fun _ _ X | Xs'] :- 
+        pi x\ used x (X x), !, close-term-prune-safe-fun Xs Ty Xs'.
+      close-term-prune-safe-fun (x\ [X | Xs x]) Ty [X | Xs'] :-
+        close-term-prune-safe-fun Xs Ty Xs'.
+
       pred precompile-aux i:term, i:list term, o:term, o:list term.
       precompile-aux X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
       precompile-aux (global _ as C) A C A :- !.
@@ -243,7 +254,7 @@ namespace tc {
       precompile-aux (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty' B') Scope) M :-
         maybe-eta T, !,
         names Scope,
-        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",
+        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-prune-safe-fun MM Ty M') "[TC] should not fail1",
         precompile-aux Ty M' Ty' M.
 
       % Detect maybe-beta term
@@ -255,7 +266,7 @@ namespace tc {
 
       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) (MM x), close-term-no-prune-fun MM Ty M) "[TC] should not fail2",
+        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-prune-safe-fun MM Ty M) "[TC] should not fail2",
         precompile-aux Ty M Ty' P.
 
       % Working with fun
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 7a61aed70..6e4a8b932 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -18,6 +18,7 @@ namespace tc {
   pred refine-proof i:term, i:goal, o:list sealed-goal.
   refine-proof tc.mode_fail G [seal G] :- !.
   refine-proof Proof G GL :-
+    if-true print-goal-after-search (coq.say "[TC] The goal after instance search is <<<" G ">>>"),
     if-true print-solution (coq.say "[TC] The proof is <<<" Proof ">>>"),
     if-true print-solution-pp (coq.say "[TC] The proof is <<<" {coq.term->string Proof} ">>>"),
       
@@ -65,6 +66,7 @@ namespace tc {
   pred print-solution-pp.   % Print the solution in coq pp
   pred print-goal.          % Print the goal in HOAS
   pred print-goal-pp.       % Print the goal with coq pp
+  pred print-goal-after-search.          % Print the goal in HOAS after instance search
   pred print-compiled-goal.
 
 }
\ No newline at end of file
diff --git a/apps/tc/tests/canonical_struct.v b/apps/tc/tests/canonical_struct.v
index 8df1b417a..86783b855 100644
--- a/apps/tc/tests/canonical_struct.v
+++ b/apps/tc/tests/canonical_struct.v
@@ -7,6 +7,8 @@ Module CS1.
   }.
   Canonical ofe_nat : ofe := Ofe nat.
 
+  TC.AddRecordFields (ofe) (Ofe) 1.
+
   Class C (I : Type).
 
   Instance c : C (ofe_car ofe_nat). Qed.
@@ -126,6 +128,8 @@ End CS6.
 Module CS7.
   Structure ofe := Ofe { ofe_car :> Type; }.
   Structure cmra := Cmra { cmra_car :> Type; }.
+  TC.AddRecordFields (ofe) (Ofe) 1.
+  TC.AddRecordFields (cmra) (Cmra) 1.
 
   Coercion cmra_ofeO (A : cmra) := Ofe A.
 
@@ -142,7 +146,6 @@ Module CS7.
   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 _.
@@ -206,6 +209,7 @@ End CS9.
 Module CS10.
   Structure ofe := Ofe { ofe_car :> Type; }.
   Canonical Structure ofe_bool := Ofe bool.
+  TC.AddRecordFields (ofe) (Ofe) 1.
 
   Class C (i : Type).
   Instance i : C bool := {}.
@@ -227,5 +231,5 @@ Module CS11.
   (* Here the projection is in the goal *)
   Goal exists X, C (ofe_car X). eexists.
     apply _.
-    Show Proof.
   Qed.
+End CS11.
\ No newline at end of file
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index 3bb6e175c..f8570b09d 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -289,6 +289,14 @@ Module HO_12.
   Class Unit (i : Prop).
   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].
diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index 5d942fdad..db1a54834 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -150,8 +150,36 @@ Elpi Accumulate lp:{{
 }}.
 Elpi Typecheck.
 
+Elpi Command TC.AddRecordFields.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate Db tc_options.db.
+Elpi Accumulate File base.
+Elpi Accumulate File tc_aux.
+Elpi Accumulate  lp:{{
+  pred tc.add_tc.records_unif.aux i:int, i:term, i:list term, i:constant, o:prop.
+  tc.add_tc.records_unif.aux 0 T Args ProjConstant P :- !,
+    coq.mk-app T Args T',
+    P = tc.proj->record ProjConstant T'.
+  tc.add_tc.records_unif.aux N T Args ProjConstant (pi x\ P x) :- N > 0, !,
+    N1 is N - 1, pi x\ tc.add_tc.records_unif.aux N1 T [x|Args] ProjConstant (P x).
+
+  pred tc.add_tc.records_unif.aux' i:option constant, i:term, i:int.
+  tc.add_tc.records_unif.aux' none _ _.
+  tc.add_tc.records_unif.aux' (some ProjConstant) RecordConstr N :-
+    tc.add_tc.records_unif.aux N RecordConstr [] ProjConstant P, tc.add-tc-db _ _ P.
+
+  pred tc.add_tc.records_unif i:term, o:term, i:int.
+  tc.add_tc.records_unif (global (indt K)) RecordConstr N :-
+    coq.env.projections K Projs,
+    std.forall Projs (x\ tc.add_tc.records_unif.aux' x RecordConstr N).
+
+  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.
 Elpi Export TC.AddAllInstances.
 Elpi Export TC.AddClasses.
 Elpi Export TC.AddInstances.
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index 45d152d99..6fb9948b3 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -99,5 +99,8 @@ Elpi Db tc.db lp:{{
     pred dummy.
 
     pred ho-link o:term, i:term, o:A.
+
+    % relates a projection to the its record
+    pred proj->record i:constant, o:term.
   }
 }}.

From d860b4c61b13507c816d503ed9e812bee2a94dfb Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 8 Aug 2024 12:25:23 +0200
Subject: [PATCH 10/32] [TC] mode ground with ground_term check + tc.link for
 coercions

---
 apps/tc/elpi/ho_link.elpi         | 4 ++++
 apps/tc/elpi/modes.elpi           | 2 ++
 apps/tc/tests/test_pending_mode.v | 8 ++++----
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
index 1173abb26..35f23a35f 100644
--- a/apps/tc/elpi/ho_link.elpi
+++ b/apps/tc/elpi/ho_link.elpi
@@ -144,6 +144,10 @@ namespace tc {
       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) :- 
+        tc.coercion-unify HD, !, 
+        get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
+
       cs (uvar _ as V) (app [HD | _] as T) :- 
         if (HD = global (const Proj), tc.proj->record Proj Record)
           (reduce-cs V T Record Proj)
diff --git a/apps/tc/elpi/modes.elpi b/apps/tc/elpi/modes.elpi
index d3e72aaec..c72313d9d 100644
--- a/apps/tc/elpi/modes.elpi
+++ b/apps/tc/elpi/modes.elpi
@@ -97,8 +97,10 @@ namespace tc {
   action-to-accumulate _ _ [].
 
   pred mode-check i:string, i:term.
+  mode-check "+" T :- !, ground_term T.
   % heuristic: if we are in "+" mode, then all evars in T should only be 
   %            in that argument
+  % note: this rule is never applied, the previous having a cut.
   mode-check "+" T :- !, 
     std.findall-unary evars L,
     get-evars T EV,
diff --git a/apps/tc/tests/test_pending_mode.v b/apps/tc/tests/test_pending_mode.v
index 9639a611a..ae38e4caf 100644
--- a/apps/tc/tests/test_pending_mode.v
+++ b/apps/tc/tests/test_pending_mode.v
@@ -36,7 +36,7 @@ Module ground1.
 
   Goal exists (x : Type), C (list x). 
     eexists.
-    apply _.
+    Fail apply _.
   Abort.
 End ground1.
 
@@ -47,7 +47,7 @@ Module ground2.
 
   Goal exists (x : Type), C (list x). 
     eexists. 
-    apply _.
+    Fail apply _.
   Abort.
 End ground2.
 
@@ -64,14 +64,14 @@ Module ground3.
 End ground3.
 
 Module ground4.
-  Elpi TC.Pending_mode - +.
+  Elpi TC.Pending_mode ! !.
   Class C {i : Type} (f : i -> i -> Prop).
   Instance i {X : Type}: C (@eq X). Qed.
   Hint Mode C ! ! : typeclass_instances.
 
   Goal exists (X : Type), @C (list X) eq. 
     eexists.
-     apply _.
+    apply _.
   Abort.
 End ground4.
 

From 9dbf2f14a1fea8ebba0be4f823b9090f1eba4852 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 8 Aug 2024 12:28:15 +0200
Subject: [PATCH 11/32] [TC] clean term in decompilation of goal

---
 apps/tc/elpi/ho_compile.elpi | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index fbc3824e8..372ac7dec 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -375,13 +375,13 @@ namespace tc {
 
       decompile-problematic-term (fun N Ty Bo) L (fun N Ty' Bo') L3 :-
         (pi x\ fold-map (Bo x) [] (Bo' x) (Lx x)),
-        close-term-no-prune-ty Lx Ty L1,
+        close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
         fold-map Ty L Ty' L2,
         std.append L2 L1 L3.
 
       decompile-problematic-term (prod N Ty Bo) L (prod N Ty' Bo') L3 :-
         (pi x\ fold-map (Bo x) [] (Bo' x) (Lx x)),
-        close-term-no-prune-ty Lx Ty L1,
+        close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
         fold-map Ty L Ty' L2,
         std.append L2 L1 L3.
 

From 431e9ba6d8f4015d1ce3cebf06b6de92b0790d8a Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 8 Aug 2024 12:35:00 +0200
Subject: [PATCH 12/32] [TC] add file deps in
 tests/importOrder/sameOrderCommand.v

---
 apps/tc/tests/importOrder/sameOrderCommand.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v
index 9ab9126ab..c291768cb 100644
--- a/apps/tc/tests/importOrder/sameOrderCommand.v
+++ b/apps/tc/tests/importOrder/sameOrderCommand.v
@@ -1,6 +1,7 @@
 From elpi.apps Require Export tc.
 
 From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
+From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc.elpi Extra Dependency "ho_link.elpi" as ho_link.
 From elpi.apps.tc.elpi Extra Dependency "tc_same_order.elpi" as tc_same_order.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
@@ -8,7 +9,9 @@ From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 Set Warnings "+elpi".
 Elpi Command SameOrderImport.
 Elpi Accumulate Db tc.db.
+Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif.
 Elpi Accumulate File ho_link.
 Elpi Accumulate File tc_same_order.

From 82ef7530c3397b78e78f6a7acad967dd82075c36 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 8 Aug 2024 14:57:28 +0200
Subject: [PATCH 13/32] [TC] perf: fold-map fully implemented in precompile
 goal

---
 apps/tc/elpi/ho_compile.elpi    | 41 +++++++++++++++++++--------------
 apps/tc/elpi/ho_precompile.elpi | 11 ++++-----
 2 files changed, 29 insertions(+), 23 deletions(-)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 372ac7dec..580d48e21 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -342,8 +342,6 @@ namespace tc {
         get-uva-pair-arity Y L Z.
 
       pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
-      decompile-problematic-term (primitive _ as C) A C 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.
@@ -352,18 +350,17 @@ namespace tc {
         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.
+        prune V S, decompile-problematic-term T L T' L2.
 
       decompile-problematic-term (tc.prod-range T _) A T' A' :- !,
-        fold-map T A T' A'.
+        decompile-problematic-term T A T' A'.
 
       decompile-problematic-term (tc.maybe-llam-tm (app [app[H|S] | NPF]) Sc) L Z [NL|L'] :- !,
         prune Z Sc,
         get-uva-pair-arity H S Y,
-        std.fold-map NPF L fold-map Tl L',
+        std.fold-map NPF L decompile-problematic-term Tl L',
         NL = tc.link.llam Z (app[Y | Tl]).
 
-      % TODO: complete this fold
       decompile-problematic-term (app[X|S]) L Z L :-
         var X _ Scope, 
         std.append Scope S Scope',
@@ -371,24 +368,34 @@ namespace tc {
         get-uva-pair-arity X S Y,
         prune Z Scope', var Z Y Scope'.
       
-      decompile-problematic-term A L A L :- var A, !.
-
-      decompile-problematic-term (fun N Ty Bo) L (fun N Ty' Bo') L3 :-
-        (pi x\ fold-map (Bo x) [] (Bo' x) (Lx x)),
+      decompile-problematic-term (fun N Ty Bo) L (fun N Ty' Bo') L3 :- !,
+        (pi x\ decompile-problematic-term (Bo x) [] (Bo' x) (Lx x)),
         close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
-        fold-map Ty L Ty' L2,
+        decompile-problematic-term Ty L Ty' L2,
         std.append L2 L1 L3.
 
-      decompile-problematic-term (prod N Ty Bo) L (prod N Ty' Bo') L3 :-
-        (pi x\ fold-map (Bo x) [] (Bo' x) (Lx x)),
+      decompile-problematic-term (prod N Ty Bo) L (prod N Ty' Bo') L3 :- !,
+        (pi x\ decompile-problematic-term (Bo x) [] (Bo' x) (Lx x)),
         close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
-        fold-map Ty L Ty' L2,
+        decompile-problematic-term Ty L Ty' L2,
         std.append L2 L1 L3.
 
+      decompile-problematic-term (global _ as C) A C A :- !.
+      decompile-problematic-term (pglobal _ _ as C) A C A :- !.
+      decompile-problematic-term (sort _ as C) A C A :- !.
+      decompile-problematic-term (let N T B F) A (let N T1 B1 F1) A3 :- !,
+        decompile-problematic-term T A T1 A1, decompile-problematic-term B A1 B1 A2, pi x\ decompile-problematic-term (F x) A2 (F1 x) A3.
+      decompile-problematic-term (app L) A (app L1) A1 :- !, std.fold-map L A decompile-problematic-term L1 A1.
+      decompile-problematic-term (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
+        decompile-problematic-term Ty A Ty1 A1, pi x\ decompile-problematic-term (F x) A1 (F1 x) A2.
+      decompile-problematic-term (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
+        decompile-problematic-term T A T1 A1, decompile-problematic-term Rty A1 Rty1 A2, std.fold-map B A2 decompile-problematic-term B1 A3.
+      decompile-problematic-term (primitive _ as C) A C A :- !.
+      decompile-problematic-term (uvar _ _ as V) A V A :- !.
+      decompile-problematic-term X A Y A :- name X, !, X = Y, !.
+
       pred compile i:term, i:list prop, o:term, o:list prop.
-      compile T L T' L' :-
-        (pi t l t' l'\ fold-map t l t' l' :- decompile-problematic-term t l t' l', !) =>
-          fold-map T L T' L'.
+      compile T L T' L' :- decompile-problematic-term T L T' L'.
 
       %                                  Uva      Binders      LinkEta 
       pred build-eta-links-of-vars-aux i:term, i:list term, o:list prop.
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index 6d9c42763..218f1d99b 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/apps/tc/elpi/ho_precompile.elpi
@@ -236,20 +236,18 @@ namespace tc {
         close-term-prune-safe-fun Xs Ty Xs'.
 
       pred precompile-aux i:term, i:list term, o:term, o:list term.
-      precompile-aux X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
       precompile-aux (global _ as C) A C A :- !.
       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 [HD | _] as T) A (tc.coercion T Scope) A :- 
+        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, !,
@@ -257,7 +255,7 @@ namespace tc {
         std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-prune-safe-fun MM Ty M') "[TC] should not fail1",
         precompile-aux Ty M' Ty' M.
 
-      % Detect maybe-beta term
+      % Detect maybe-llam term
       precompile-aux (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope1) [X|M] :-
         var X _ Scope, split-pf XS Scope PF NPF, 
         not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
@@ -281,7 +279,8 @@ namespace tc {
       precompile-aux (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
         precompile-aux T A T1 A1, precompile-aux Rty A1 Rty1 A2, std.fold-map B A2 precompile-aux B1 A3.
       precompile-aux (primitive _ as C) A C A :- !.
-      precompile-aux X A X [X|A] :- var X, !.
+      precompile-aux (uvar _ _ as X) A X [X|A] :- !.
+      precompile-aux X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
     }
 
     pred goal i:term, o:term, o:list term.

From 1aa4bae88207402d6457286d0b570c13873860ce Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Sat, 10 Aug 2024 12:43:24 +0200
Subject: [PATCH 14/32] [TC] improve perf of goal compilation

---
 apps/tc/elpi/base.elpi         |  17 +++-
 apps/tc/elpi/compile_goal.elpi | 178 +++++++++++++++++++++++++++++++++
 apps/tc/elpi/ho_link.elpi      |  50 ++++-----
 apps/tc/elpi/solver.elpi       |  14 ++-
 apps/tc/tests/bigTest.v        |   2 +
 apps/tc/tests/test.v           |  17 +---
 apps/tc/theories/tc.v          |   2 +
 7 files changed, 228 insertions(+), 52 deletions(-)
 create mode 100644 apps/tc/elpi/compile_goal.elpi

diff --git a/apps/tc/elpi/base.elpi b/apps/tc/elpi/base.elpi
index d1ca5f72c..6da2f0d0b 100644
--- a/apps/tc/elpi/base.elpi
+++ b/apps/tc/elpi/base.elpi
@@ -90,10 +90,13 @@ split-at-not-fatal N [X|XS] [X|LN] LM :- !, N1 is N - 1,
 
 pred undup-same i:list A, o:list A.
 undup-same [] [].
-undup-same [X|Xs] [X|Ys] :-
-  std.forall Xs (x\ not (x == X)), !,
-  undup-same Xs Ys.
-undup-same [_|Xs] Ys :- undup-same Xs Ys.
+undup-same [X|Xs] Ys :- std.exists Xs (x\ x == X), !, undup-same Xs Ys.
+undup-same [X|Xs] [X|Ys] :- undup-same Xs Ys.
+
+pred undup i:list A, o:list A.
+undup [] [].
+undup [X|Xs] Ys :- std.mem! Xs X, !, undup Xs Ys.
+undup [X|Xs] [X|Ys] :- undup Xs Ys.
 
 :index (1)
 pred is-coq-term i:A.
@@ -168,3 +171,9 @@ 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'.
+
+pred free-names i:term, o:list term.
+free-names T L :-
+  names N,
+  (pi T L\ fold-map T L T [T|L] :- name T, std.mem! N T, !) => fold-map T [] _ L',
+  undup {std.rev L'} L.
\ No newline at end of file
diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
new file mode 100644
index 000000000..bea5e93a5
--- /dev/null
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -0,0 +1,178 @@
+namespace tc {
+  shorten tc.{r-ar, range-arity}.
+
+  namespace compile {
+    namespace goall {
+      :index (_ _ 1)
+      pred may-contract-to i:list term, i:term, i:term.
+      may-contract-to _ N N :- !.
+      % TODO: here we should do var V _ Scope and use scope: N can be in Scope but not in S
+      may-contract-to L N (app [V|S]) :- var V, !,
+        std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
+      may-contract-to L N (app [N|A]) :-
+        std.length A {std.length L},
+        std.forall2 {std.rev L} A (may-contract-to []).
+      may-contract-to L N (fun _ _ B) :-
+        pi x\ may-contract-to [x|L] N (B x).
+
+      :index (_ 1)
+      pred occurs-rigidly i:term, i:term.
+      occurs-rigidly N N :- name N, !.
+      occurs-rigidly _ (app [N|_]) :- var N, !, fail.
+      occurs-rigidly N (app A) :- exists! A (occurs-rigidly N).
+      occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
+
+      pred maybe-eta-aux i:term, i:list term.
+      % TODO: here we should do var V _ Scope and use Scope: an elt in L can appear in Scope
+      maybe-eta-aux (app[V|S]) L :- var V, !,
+        std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
+      maybe-eta-aux (app [_|A]) L :-
+        SplitLen is {std.length A} - {std.length L},
+        split-at-not-fatal SplitLen A HD TL,
+        std.forall L (x\ not (exists! HD (occurs-rigidly x))),
+        std.forall2 {std.rev L} TL (may-contract-to []). 
+      maybe-eta-aux (fun _ _ B) L :-
+        pi x\ maybe-eta-aux (B x) [x|L].
+
+      pred maybe-eta i:term.
+      maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].
+
+      pred split-pf i:list term, i:list term, o:list term, o:list term.
+      split-pf [] _ [] [] :- !.
+      split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
+      split-pf Xs _ [] Xs.
+
+      pred used i:term, i:term.
+      used X (uvar _ S) :- std.mem! S X, !.
+      used X (fun _ _ Bo) :- pi x\ used X (Bo x).
+
+      pred close-term-prune-safe-fun i:(term -> list term), i:term, o:list term.
+      close-term-prune-safe-fun (x\ []) _ [] :- !.
+      close-term-prune-safe-fun (x\ [X x | Xs x]) Ty [fun _ _ X | Xs'] :-
+        pi x\ used x (X x), !, close-term-prune-safe-fun Xs Ty Xs'.
+      close-term-prune-safe-fun (x\ [X | Xs x]) Ty [X | Xs'] :-
+        close-term-prune-safe-fun Xs Ty Xs'.
+
+      pred compile-full-aux-close i:(term -> term), i:term, i:list prop, o:(term -> term), o:list prop.
+      compile-full-aux-close Bo Ty L Bo' L' :-
+        (pi x\ compile-full-aux (Bo x) [] (Bo' x) (BoL x)),
+      % TODO: maybe attach to the links the list of used binders, to simply make this check?
+      % Maybe L' is a pair list links and list binders per link, this way we can easily prune
+        close-term-no-prune-ty BoL Ty BoL',
+        std.append L BoL' L'.
+
+      pred compile-full-aux i:term, i:list prop, o:term, o:list prop.
+      compile-full-aux (global _ as G) L G L :- !.
+      compile-full-aux (pglobal _ _ as G) L G L :- !.
+      compile-full-aux (sort _ as G) L G L :- !.
+
+      % Link for coercion
+      compile-full-aux (app [HD|_] as G) L G' [tc.link.cs G' G | L] :- tc.coercion-unify HD, !.
+      
+      % Link for canonical structure
+      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 _, !.
+
+      % Link for eta-redex
+      compile-full-aux (fun Name Ty Bo as G) L G' [tc.link.eta G' (fun Name Ty' Bo') | L'] :- maybe-eta G, !,
+        compile-full-aux Ty L Ty' LTy,
+        compile-full-aux-close Bo Ty LTy Bo' L'.
+
+      compile-full-aux (fun Name Ty Bo) L (fun Name Ty' Bo') L' :- !,
+        compile-full-aux Ty L Ty' LTy,
+        compile-full-aux-close Bo Ty LTy Bo' L'.
+
+      compile-full-aux (prod Name Ty Bo) L (prod Name Ty' Bo') L' :- !,
+        compile-full-aux Ty L Ty' LTy,
+        compile-full-aux-close Bo Ty LTy Bo' L'.
+
+      % NOTE: when compiling t = (app [X, x, y]) and [x,y] are distinct_names,
+      %       then the coq variable has not [x,y] in scope, it is applied to
+      %       them. Note also that t is a problematic term that cannot be
+      %       exposed to the else unification algorithm.  
+      %       The solution is to build the following links:  
+      %       X =η (λa.Y a)
+      %       a |- Y a =η (λb.Z a b)
+      %       and expose a variable W at toplevel having Z has head and [x, y]
+      %       as scope
+
+      % NOTE: when compiling t = (app [X, a, x]) where a is a constant and x a
+      %       name, we build a llam link.  
+      %       The link will be: T x =L X a x  
+      %       the exposed variable in the term will be T x
+
+      % NOTE: here a combination of eta and llam:  
+      %       let t = (app [X x y, z, c, w, d]) where X is a coq var with x and
+      %       y in scope, z and w are names and c, d are constants.  
+      %       In this case, the links should be:  
+      %       X x y =η (λa.Y x y a)  
+      %       a |- Z x y a w =L (app[Y x y a, c w d])  
+      %       The returned variable is Z x y a w
+
+      pred free-names i:term, o:list term.
+      free-names T L :-
+        names N,
+        (pi T L\ fold-map T L T [T|L] :- name T, std.mem! N T, !) => fold-map T [] _ L',
+        undup {std.rev L'} L.
+
+      :index(_ _ _ _ 3)
+      % TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
+      %                           LHS      Scope      Ty          Names        PF         NPF        OLDLINKS    NEW_VAR
+      pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
+      build-eta-llam-links LHS _ _       Names []  NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
+        std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
+        prune T Names,
+        var T HD _. 
+      build-eta-llam-links LHS SC _Ty       _    [X] []  OL HD [tc.link.eta LHS (fun _ _ (x\ V x)) | OL] :- !,
+        prune V SC, var (V X) HD _. % TODO...
+      build-eta-llam-links LHS SC _Ty Names [X|XS] NPF OL HD [tc.link.eta LHS (fun _ _ (x\ LHS' x)) | L] :- !,
+      % TODO: unfold Ty if needed...
+        std.append SC [X] SC',
+        prune LHS' SC, build-eta-llam-links (LHS' X) SC' _ Names XS NPF OL HD L.
+
+      % Link for beta-redex (Uvar in PF)
+      % BUILD CHAIN OF LINKS-ETA from X to V...
+      % TODO: to avoid too many chain for the same var, maybe pass a list into the fold
+      compile-full-aux (app [(uvar _ Scope as V) | S] as T) L G' L'' :- !,
+        % By construction the scope of a uvar is a list of distinct name
+        std.fold-map S L compile-full-aux S' L', % LS = Links built for S
+        % std.assert-ok! (coq.typecheck V Ty) "Not typecheckable variable",
+        split-pf S' Scope PF NPF,
+        free-names T Names,
+        build-eta-llam-links V Scope _ Names PF NPF L' G'' L'',
+        prune G' Names,
+        var G' G'' Names.
+
+      compile-full-aux (app L) A (app L1) A1 :- !, std.fold-map L A compile-full-aux L1 A1.
+
+      compile-full-aux (let N T B F) A (let N T1 B1 F1) A3 :- !,
+        compile-full-aux T A T1 A1, compile-full-aux B A1 B1 A2,
+        compile-full-aux-close F T A2 F1 A3.
+      
+      compile-full-aux (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
+        compile-full-aux Ty A Ty1 A1, 
+        compile-full-aux-close F Ty A1 F1 A2.
+      
+      compile-full-aux (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
+        compile-full-aux T A T1 A1,
+        compile-full-aux Rty A1 Rty1 A2,
+        std.fold-map B A2 compile-full-aux B1 A3.
+      
+      compile-full-aux (uvar _ _ as X) A X A :- !.
+      compile-full-aux X A X A :- name X, !.
+
+      compile-full-aux A B _ _ :- coq.error "Fail to compile-full-aux" A B.
+
+      % takes a term t and returns a term t' and a list of links.
+      pred compile-full i:term, o:term, o:list prop.
+      compile-full Goal Goal' Links :- compile-full-aux Goal [] Goal' Links.
+    }
+
+    pred goal' i:term, o:term, o:list prop.
+    :name "compile-goal'"
+    goal' Goal Goal' Links :- 
+      goall.compile-full-aux Goal [] Goal' Links.
+  }
+}
diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
index 35f23a35f..dbebb908a 100644
--- a/apps/tc/elpi/ho_link.elpi
+++ b/apps/tc/elpi/ho_link.elpi
@@ -1,5 +1,9 @@
 namespace tc {
   namespace link {
+    pred relocate i:list term, i:list term, i:term, o:term.
+    relocate [] [] T T' :- copy T T'.
+    relocate [X|Xs] [Y|Ys] T T' :- (copy Y X :- !) => relocate Xs Ys T T'.
+
     pred get-vars i:term, o:list term.
     get-vars T R :-
       (pi X H L Ign\ fold-map X L X [H|L] :- var X H Ign, !) => 
@@ -61,12 +65,6 @@ namespace tc {
       pred scope-check i:term, i:term.
       scope-check (uvar _ L) T :- prune A L, A = T, !.
 
-      pred relocate i:list term, i:list term, i:term, o:term.
-      relocate [] [] T T' :- copy T T', coq.say "Copy result is" T T'.
-      relocate [X|Xs] [Y|Ys] T T' :-
-        coq.say "Charging" (copy Y X),
-        (copy Y X :- !) => relocate Xs Ys T T'.
-
       pred collect-store o:list prop.
       pred collect-store-aux i:list prop, o:list prop.
 
@@ -80,24 +78,14 @@ namespace tc {
       unify-eta A (fun _ _ _ as B) :- !, eta-expand A A', unify-eta A' B.
       unify-eta A B :- A = B.
 
-      constraint eta uvar relocate fun collect-store-aux solve-eta {
+      constraint eta solve-eta {
         rule solve-eta \ (eta A B) <=> (unify-eta A B).
         rule \ solve-eta.
-        % 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)
-        %       % coq.say "Deduplicating" 
-        %       %   (eta (uvar X L1) (fun _ T1 B1)) 
-        %       %   (eta (uvar X L2) (fun _ T2 B2))
-        %       %   "B2' is" (B2')
-        %     )  
-        % <=> (N1 : G1 ?- B1 = B2').
-
-        % TODO: link collect do not work since it closes links and 
-        %       therefore variables are prune
-        % rule \ (tc.link.eta A B) (collect-store-aux L R) | (coq.say A B {names}) <=> (collect-store-aux [tc.link.eta A B|L] R).
-        % rule \ (collect-store-aux L R) <=> (R = L).
+        % 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)) 
+            | (pi x\ relocate L1 L2 (B2 x) (B2' x))  
+        <=> (N1 : G1 ?- B1 = B2').
       }
 
       pred eta i:term, i:term.
@@ -114,7 +102,9 @@ namespace tc {
     namespace llam {
       pred llam i:term, i:term.
       llam A (uvar _ S as T) :- distinct_names S, !, A = T.
-      llam A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, declare_constraint (llam A (app [H|L])) [_,A|Vars].
+      llam A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, 
+        coq.say "Declaring constraint" (llam A (app [H|L])) [_,A|Vars],
+        declare_constraint (llam A (app [H|L])) [_,A|Vars].
       llam (fun _ _ _ as F) (app [H | TL]) :- 
         var H _ Scope, !, 
           std.drop-last 1 TL TL', 
@@ -124,9 +114,14 @@ namespace tc {
           pi x\ llam F Bo'.
       llam A B :- !, tc.unify-eq A B.
 
-      constraint solve-llam solve-llam-t llam {
+      constraint solve-llam llam {
         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) 
+            | (pi x\ relocate L1 L2 T2 T2')  
+        <=> (N1 : G1 ?- T1 = T2'). % TODO: instead of elpi unif, should use heuristics...
       }
     }
 
@@ -154,13 +149,6 @@ namespace tc {
           (coq.unify-eq V T ok).
       cs T1 T2 :- not (T2 = app _), !, 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.
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 6e4a8b932..160e91ab9 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -7,8 +7,8 @@ msolve L _ :- coq.ltac.fail _ "[TC] fail to solve" L.
 
 namespace tc {
   pred build-query-from-goal i:term, i:term, o:prop, o:list prop.
-  build-query-from-goal Goal Proof Q PostProcess :-
-    tc.compile.goal Goal Goal' PostProcess, !,
+  build-query-from-goal Goal Proof Q Links :-
+    tc.compile.goal' Goal Goal' Links, !,
     coq.safe-dest-app Goal' (global TC) TL',
     std.append TL' [Proof] TL, !,
     coq.elpi.predicate {tc.gref->pred-name TC} TL Q.
@@ -29,10 +29,11 @@ namespace tc {
 
   pred solve-under-context i:term, o:term.
   solve-under-context Ty Proof :-
-    tc.time-it tc.oTC-time-compile-goal (build-query-from-goal Ty Proof Q PostProcess) "build query", !,
-    if-true print-compiled-goal (coq.say "[TC] the compiled goal is" Q), !,
+    tc.time-it tc.oTC-time-compile-goal (build-query-from-goal Ty Proof Q Links) "build query", !,
+    if-true print-compiled-goal (coq.say "[TC] the compiled goal is" Q),
+    if-true print-links (coq.say "[TC] the links are" Links),
     tc.time-it tc.oTC-time-instance-search (
-      do PostProcess, Q,
+      do Links, Q,
       tc.link.solve-cs,
       tc.link.solve-eta, % Trigger eta links
       tc.link.solve-llam % Trigger llam links
@@ -59,6 +60,7 @@ namespace tc {
     if-true print-goal-pp (coq.say "The goal is <<<" {coq.term->string Ty} ">>>"),
     tc.time-it tc.oTC-time-mode-check (tc.modes-check Ty) "mode check", !,
     tc.time-it _ (tc.compile.context Ctx CtxClause) "compile context", !,
+    if-true print-ctx (coq.say "The context is" CtxClause),
     CtxClause => solve-under-context Ty Proof.
   solve-aux1 _ _ tc.mode_fail :- if-true (print-solution; print-solution-pp) (coq.say "Invalid mode call").
 
@@ -68,5 +70,7 @@ namespace tc {
   pred print-goal-pp.       % Print the goal with coq pp
   pred print-goal-after-search.          % Print the goal in HOAS after instance search
   pred print-compiled-goal.
+  pred print-links.
+  pred print-ctx.
 
 }
\ No newline at end of file
diff --git a/apps/tc/tests/bigTest.v b/apps/tc/tests/bigTest.v
index 52d8bd617..4daa744a8 100644
--- a/apps/tc/tests/bigTest.v
+++ b/apps/tc/tests/bigTest.v
@@ -1,3 +1,5 @@
+Set Warnings "-elpi.TC.hints".
+
 From elpi.apps Require Import tc.
 Elpi TC Solver Override TC.Solver All.
 
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index f8570b09d..9152507e8 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -1,4 +1,5 @@
 From elpi Require Import tc.
+Set Warnings "+elpi".
 
 Section test_max_arity.
   Elpi Query TC.Solver lp:{{
@@ -207,23 +208,15 @@ Module HO_81.
   Class c1 (T : Type).
   Instance i1 F : c1 F. Qed.
 
-  Elpi Accumulate TC.Solver lp:{{
-    :before "compile-goal"
-    tc.compile.goal Goal _ _ :-
-      Goal = {{HO_81.c1 lp:_}}, !,
-      tc.precomp.goal Goal _ Vars, !,
-      tc.compile.goal.make-pairs Vars Pairs,
-      std.assert! (Pairs = []) "", fail.
-  }}.
-  Elpi Typecheck TC.Solver.
-
   Goal exists X, c1 X.
     eexists.
     (* 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) *)
-    Fail apply _.
-  Abort.
+    apply _.
+    Unshelve.
+    apply nat.
+  Qed.
 End HO_81.
 
 Module HO_8.
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index fb02013c5..180abce83 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -8,6 +8,7 @@ From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 (* From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler. *)
 From elpi.apps.tc.elpi Extra Dependency "ho_precompile.elpi" as ho_precompile.
 From elpi.apps.tc.elpi Extra Dependency "ho_compile.elpi" as ho_compile.
+From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 From elpi.apps.tc.elpi Extra Dependency "compiler1.elpi" as compiler1.
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
@@ -57,6 +58,7 @@ Elpi Accumulate File ho_precompile.
 Elpi Accumulate File ho_compile.
 Elpi Accumulate File compiler1.
 Elpi Accumulate File create_tc_predicate.
+Elpi Accumulate File compile_goal.
 Elpi Accumulate File modes.
 Elpi Accumulate File solver.
 Elpi Query lp:{{

From b7ea708dd461468a6b102dc035d34f60cd7250cc Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Sat, 10 Aug 2024 16:26:16 +0200
Subject: [PATCH 15/32] [TC] remove goal precomp and goal compile (all is done
 in ycompile_goal.elpi)

---
 apps/tc/elpi/compile_goal.elpi  |  29 +-----
 apps/tc/elpi/ho_compile.elpi    | 172 ++++----------------------------
 apps/tc/elpi/ho_link.elpi       |  26 ++++-
 apps/tc/elpi/ho_precompile.elpi | 102 -------------------
 apps/tc/elpi/solver.elpi        |   2 +-
 apps/tc/tests/test.v            |  12 +--
 6 files changed, 49 insertions(+), 294 deletions(-)

diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
index bea5e93a5..33ec8eef8 100644
--- a/apps/tc/elpi/compile_goal.elpi
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -1,6 +1,4 @@
 namespace tc {
-  shorten tc.{r-ar, range-arity}.
-
   namespace compile {
     namespace goall {
       :index (_ _ 1)
@@ -76,7 +74,7 @@ namespace tc {
       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 Name Ty' Bo') | L'] :- maybe-eta G, !,
+      compile-full-aux (fun Name_ Ty Bo as G) L G' [tc.link.eta G' (fun `_` Ty' Bo') | L'] :- maybe-eta G, !,
         compile-full-aux Ty L Ty' LTy,
         compile-full-aux-close Bo Ty LTy Bo' L'.
 
@@ -111,37 +109,16 @@ namespace tc {
       %       a |- Z x y a w =L (app[Y x y a, c w d])  
       %       The returned variable is Z x y a w
 
-      pred free-names i:term, o:list term.
-      free-names T L :-
-        names N,
-        (pi T L\ fold-map T L T [T|L] :- name T, std.mem! N T, !) => fold-map T [] _ L',
-        undup {std.rev L'} L.
-
-      :index(_ _ _ _ 3)
-      % TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
-      %                           LHS      Scope      Ty          Names        PF         NPF        OLDLINKS    NEW_VAR
-      pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
-      build-eta-llam-links LHS _ _       Names []  NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
-        std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
-        prune T Names,
-        var T HD _. 
-      build-eta-llam-links LHS SC _Ty       _    [X] []  OL HD [tc.link.eta LHS (fun _ _ (x\ V x)) | OL] :- !,
-        prune V SC, var (V X) HD _. % TODO...
-      build-eta-llam-links LHS SC _Ty Names [X|XS] NPF OL HD [tc.link.eta LHS (fun _ _ (x\ LHS' x)) | L] :- !,
-      % TODO: unfold Ty if needed...
-        std.append SC [X] SC',
-        prune LHS' SC, build-eta-llam-links (LHS' X) SC' _ Names XS NPF OL HD L.
-
       % Link for beta-redex (Uvar in PF)
       % BUILD CHAIN OF LINKS-ETA from X to V...
       % TODO: to avoid too many chain for the same var, maybe pass a list into the fold
       compile-full-aux (app [(uvar _ Scope as V) | S] as T) L G' L'' :- !,
         % By construction the scope of a uvar is a list of distinct name
         std.fold-map S L compile-full-aux S' L', % LS = Links built for S
-        % std.assert-ok! (coq.typecheck V Ty) "Not typecheckable variable",
+        coq.typecheck V Ty ok,
         split-pf S' Scope PF NPF,
         free-names T Names,
-        build-eta-llam-links V Scope _ Names PF NPF L' G'' L'',
+        tc.link.build-eta-llam-links V Scope Ty Names PF NPF L' G'' L'',
         prune G' Names,
         var G' G'' Names.
 
diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 580d48e21..4ac3d2ba5 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -59,18 +59,23 @@ namespace tc {
         % This happens when the instance to be compiled comes from the context
         % Example: Goal exists (X : T1 -> T2), forall a, c (X a) -> ...
         %            intros; eexists. (* In the context we have the instance `H: c (?X a)` *)
-        decompile-term-aux (tc.maybe-llam-tm (app[app[H | PF] | NPF]) S) A Z (pr XS' [NL | L3]) :-  !,
-          var H _ Scope, !,
-          std.append Scope S S',
-          prune Z S',
-          tc.compile.goal.make-pairs [T] Pairs,
-          % We build on the fly the eta-links for T
-          Pairs =>
-            (tc.compile.goal.build-eta-links-of-vars [T] P,
-              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]).
+        decompile-term-aux (tc.maybe-llam-tm (app[app[V | PF] | NPF] as T) S_) L G'' (pr XS' L'') :-  !,
+          var V _ Scope, !,
+          std.fold-map NPF L decompile-term-aux NPF' (pr XS' L'),
+          free-names T Names,
+          coq.typecheck V Ty ok,
+          tc.link.build-eta-llam-links V Scope Ty Names PF NPF' L' G' L'',
+          prune G'' Names,
+          var G'' G' Names.
+
+        % HO var when H is a hole appearing in the shelved goals
+        decompile-term-aux (app [V|PF] as T) (pr XS' L') G'' (pr XS' L'') :-
+          var V _ Scope, !,
+          free-names T Names,
+          coq.typecheck V Ty ok,
+          tc.link.build-eta-llam-links V Scope Ty Names PF [] L' G' L'',
+          prune G'' Names,
+          var G'' G' Names.
 
         decompile-term-aux (fun Name Ty Bo) (pr XS L) (fun Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
@@ -96,21 +101,6 @@ namespace tc {
           std.assert! (name-pair H V Len) "[TC] name-pair not found",
           name R V L.
 
-        % HO var when H is a hole appearing in the shelved goals
-        decompile-term-aux (app [T|L]) (pr A B) Z (pr A B') :-
-          var T _ Scope,
-          std.forall L is-name,     % Not needed, since decompile for llam leaves only PF
-          distinct_names L, !,      % Not needed, since decompile for llam leaves only PF
-          std.append Scope L Scope',
-          prune Z Scope',
-          tc.compile.goal.make-pairs [T] Pairs,
-          % We build on the fly the eta-links for `T`
-          Pairs =>
-            (tc.compile.goal.build-eta-links-of-vars [T] P,
-              tc.compile.goal.get-uva-pair-arity T L Y),
-          var Z Y Scope',
-          std.append P B B'.
-
         decompile-term-aux (app L) PR (app L') PR' :- !,
           std.fold-map L PR decompile-term-aux L' PR'.
 
@@ -174,10 +164,10 @@ namespace tc {
         o:prop,            % Link         : The new eta-link
         o:term,            % Ty'          : The cleaned version of the binder in Ty
         o:(term -> term).  % Bo           : the body of the type of A
-      make-eta-link-aux A (prod _ Ty Bo) (pr B Name) L Link Ty' Bo :- !,
+      make-eta-link-aux A (prod _ Ty Bo) (pr B Name_) L Link Ty' Bo :- !,
         clean-term Ty Ty',
         name A' A {std.rev L},
-        Link = tc.link.eta A' (fun Name Ty' B'),
+        Link = tc.link.eta A' (fun `_` Ty' B'),
         pi x\ sigma L'\ std.rev [x|L] L', name (B' x) B L'.
       % Going under prod-range
       make-eta-link-aux A (tc.prod-range Prod _) BN L Link Ty' Bo :- !,
@@ -313,129 +303,5 @@ namespace tc {
     instance-gr InstGR Clause :-
       coq.env.typeof InstGR Ty,
       tc.compile.instance Ty (global InstGR) Clause.
-    
-    namespace goal {
-      % [uvar-pair V1 Ty V2] List of uvar for link-eta-dedup
-      %                      V1 has arity n and V2 has arity n+1
-      %                      If V1 has type A -> B, then A = Ty
-      pred uvar-pair i:term, o:term, o:term.
-
-      %                    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 _ _ [].
-
-      pred make-pairs i:list term, o:list prop.
-      make-pairs [] [] :- !.
-      make-pairs [X|Xs] L :- !,
-        coq.typecheck X Ty ok,
-        make-pairs-aux Ty X L',
-        make-pairs Xs L'',
-        std.append L' L'' L.
-
-      pred get-uva-pair-arity i:term, i:list term, o:term.
-      get-uva-pair-arity X [] X :- !.
-      get-uva-pair-arity X [_|L] Z :- uvar-pair X _ Y, !, 
-        get-uva-pair-arity Y L Z.
-
-      pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
-      % 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, decompile-problematic-term T L T' L2.
-
-      decompile-problematic-term (tc.prod-range T _) A T' A' :- !,
-        decompile-problematic-term T A T' A'.
-
-      decompile-problematic-term (tc.maybe-llam-tm (app [app[H|S] | NPF]) Sc) L Z [NL|L'] :- !,
-        prune Z Sc,
-        get-uva-pair-arity H S Y,
-        std.fold-map NPF L decompile-problematic-term Tl L',
-        NL = tc.link.llam Z (app[Y | Tl]).
-
-      decompile-problematic-term (app[X|S]) L Z L :-
-        var X _ Scope, 
-        std.append Scope S Scope',
-        distinct_names Scope', !,
-        get-uva-pair-arity X S Y,
-        prune Z Scope', var Z Y Scope'.
-      
-      decompile-problematic-term (fun N Ty Bo) L (fun N Ty' Bo') L3 :- !,
-        (pi x\ decompile-problematic-term (Bo x) [] (Bo' x) (Lx x)),
-        close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
-        decompile-problematic-term Ty L Ty' L2,
-        std.append L2 L1 L3.
-
-      decompile-problematic-term (prod N Ty Bo) L (prod N Ty' Bo') L3 :- !,
-        (pi x\ decompile-problematic-term (Bo x) [] (Bo' x) (Lx x)),
-        close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
-        decompile-problematic-term Ty L Ty' L2,
-        std.append L2 L1 L3.
-
-      decompile-problematic-term (global _ as C) A C A :- !.
-      decompile-problematic-term (pglobal _ _ as C) A C A :- !.
-      decompile-problematic-term (sort _ as C) A C A :- !.
-      decompile-problematic-term (let N T B F) A (let N T1 B1 F1) A3 :- !,
-        decompile-problematic-term T A T1 A1, decompile-problematic-term B A1 B1 A2, pi x\ decompile-problematic-term (F x) A2 (F1 x) A3.
-      decompile-problematic-term (app L) A (app L1) A1 :- !, std.fold-map L A decompile-problematic-term L1 A1.
-      decompile-problematic-term (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
-        decompile-problematic-term Ty A Ty1 A1, pi x\ decompile-problematic-term (F x) A1 (F1 x) A2.
-      decompile-problematic-term (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
-        decompile-problematic-term T A T1 A1, decompile-problematic-term Rty A1 Rty1 A2, std.fold-map B A2 decompile-problematic-term B1 A3.
-      decompile-problematic-term (primitive _ as C) A C A :- !.
-      decompile-problematic-term (uvar _ _ as V) A V A :- !.
-      decompile-problematic-term X A Y A :- name X, !, X = Y, !.
-
-      pred compile i:term, i:list prop, o:term, o:list prop.
-      compile T L T' L' :- decompile-problematic-term T L T' L'.
-
-      %                                  Uva      Binders      LinkEta 
-      pred build-eta-links-of-vars-aux i:term, i:list term, o:list prop.
-      build-eta-links-of-vars-aux Old L [Hd | Xs] :- 
-        uvar-pair Old Ty Next, !,
-        prune OldScope L,
-        prune Name L,
-        var OldScope Old L,
-        Hd = tc.link.eta OldScope (fun Name Ty (x\ NextScope x)),
-        pi x\ sigma L'\
-          std.append L [x] L',
-          prune (NextScope x) L',
-          var (NextScope x) Next L',
-          build-eta-links-of-vars-aux Next L' (Ys x), !,
-        sigma Closed\ (close-term-no-prune-ty Ys Ty Closed),
-        Xs = Closed.
-      build-eta-links-of-vars-aux _ _ [].
-
-      pred build-eta-links-of-vars i:list term, o:list prop.
-      build-eta-links-of-vars [] [].
-      build-eta-links-of-vars [V|Vars] L :-
-        var V Hd S,
-        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
-    pred goal i:term, o:term, o:list prop.
-    :name "compile-goal"
-    goal Goal Goal' Links :-
-      tc.precomp.goal Goal GoalPrecomp Vars, !,
-      goal.make-pairs Vars Pairs,
-      Pairs => (
-        std.assert!(goal.build-eta-links-of-vars Vars EtaLinks) "[TC] cannot build eta-links",
-        std.assert!(goal.compile GoalPrecomp EtaLinks Goal' Links) "[TC] cannot compile goal"
-      ).
   }
 }
\ No newline at end of file
diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
index dbebb908a..e0d43131a 100644
--- a/apps/tc/elpi/ho_link.elpi
+++ b/apps/tc/elpi/ho_link.elpi
@@ -9,6 +9,29 @@ namespace tc {
       (pi X H L Ign\ fold-map X L X [H|L] :- var X H Ign, !) => 
         fold-map T [] _ R.
 
+    % [build-eta-llam-links LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
+    % Builds the eta/llam links at runtime for a term having the shape 
+    % `app[(uvar X Scope as V) | L]`.
+    % LHS should be V, Scope the scope of V, TODO: finish to document this...
+    :index(_ _ _ _ 3)
+    % TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
+    %                           LHS      Scope      Ty          Names        PF         NPF        OldLinks    NewVar
+    pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
+    build-eta-llam-links LHS _ _       Names []  NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
+      std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
+      prune T Names,
+      var T HD _. 
+    build-eta-llam-links LHS SC (prod _ Ty _)       _    [X] []  OL HD [tc.link.eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
+      prune V SC, var (V X) HD _.
+    build-eta-llam-links LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [tc.link.eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
+    % TODO: unfold Ty if needed...
+      std.append SC [X] SC',
+      prune LHS' SC, build-eta-llam-links (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
+    build-eta-llam-links LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
+      Ty' = prod _ _ _, coq.unify-eq Ty Ty' ok, !,
+      build-eta-llam-links LHS SC Ty' Names PF NPF OL HD L.
+
+
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     % ETA LINK                                                                 %
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -73,7 +96,7 @@ namespace tc {
 
       pred unify-eta i:term, i:term.
       % unify-eta A B :- coq.say "Unify-eta" "A"A"B"B, fail.
-      unify-eta A B :- var A, !, A = B, !.
+      unify-eta (uvar _ _ as A) B :- !, A = B, !.
       unify-eta (fun _ _ A) (fun _ _ B) :- !, pi x\ unify-eta (A x) (B x).
       unify-eta A (fun _ _ _ as B) :- !, eta-expand A A', unify-eta A' B.
       unify-eta A B :- A = B.
@@ -103,7 +126,6 @@ namespace tc {
       pred llam i:term, i:term.
       llam A (uvar _ S as T) :- distinct_names S, !, A = T.
       llam A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, 
-        coq.say "Declaring constraint" (llam A (app [H|L])) [_,A|Vars],
         declare_constraint (llam A (app [H|L])) [_,A|Vars].
       llam (fun _ _ _ as F) (app [H | TL]) :- 
         var H _ Scope, !, 
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index 218f1d99b..db5852b87 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/apps/tc/elpi/ho_precompile.elpi
@@ -183,107 +183,5 @@ namespace tc {
       tc.precomp.instance.get-univ T UnivConstL,
       tc.precomp.instance.get-univ-instances T UnivInstL,
       std.assert!(instance.precompile-aux instance.is_pos T z T' N) "[TC] cannot precompile instance".
-
-    namespace goal {
-      :index (_ _ 1)
-      pred may-contract-to i:list term, i:term, i:term.
-      may-contract-to _ N N :- !.
-      % TODO: here we should do var V _ Scope and use scope: N can be in Scope but not in S
-      may-contract-to L N (app [V|S]) :- var V, !,
-        std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
-      may-contract-to L N (app [N|A]) :-
-        std.length A {std.length L},
-        std.forall2 {std.rev L} A (may-contract-to []).
-      may-contract-to L N (fun _ _ B) :-
-        pi x\ may-contract-to [x|L] N (B x).
-
-      :index (_ 1)
-      pred occurs-rigidly i:term, i:term.
-      occurs-rigidly N N :- name N, !.
-      occurs-rigidly _ (app [N|_]) :- var N, !, fail.
-      occurs-rigidly N (app A) :- exists! A (occurs-rigidly N).
-      occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
-
-      pred maybe-eta-aux i:term, i:list term.
-      % TODO: here we should do var V _ Scope and use Scope: an elt in L can appear in Scope
-      maybe-eta-aux (app[V|S]) L :- var V, !,
-        std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
-      maybe-eta-aux (app [_|A]) L :-
-        SplitLen is {std.length A} - {std.length L},
-        split-at-not-fatal SplitLen A HD TL,
-        std.forall L (x\ not (exists! HD (occurs-rigidly x))),
-        std.forall2 {std.rev L} TL (may-contract-to []). 
-      maybe-eta-aux (fun _ _ B) L :-
-        pi x\ maybe-eta-aux (B x) [x|L].
-
-      pred maybe-eta i:term.
-      maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].
-
-      pred split-pf i:list term, i:list term, o:list term, o:list term.
-      split-pf [] _ [] [] :- !.
-      split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
-      split-pf Xs _ [] Xs.
-
-      pred used i:term, i:term.
-      used X (uvar _ S) :- std.mem! S X, !.
-      used X (fun _ _ Bo) :- pi x\ used X (Bo x).
-
-      pred close-term-prune-safe-fun i:(term -> list term), i:term, o:list term.
-      close-term-prune-safe-fun (x\ []) _ [] :- !.
-      close-term-prune-safe-fun (x\ [X x | Xs x]) Ty [fun _ _ X | Xs'] :- 
-        pi x\ used x (X x), !, close-term-prune-safe-fun Xs Ty Xs'.
-      close-term-prune-safe-fun (x\ [X | Xs x]) Ty [X | Xs'] :-
-        close-term-prune-safe-fun Xs Ty Xs'.
-
-      pred precompile-aux i:term, i:list term, o:term, o:list term.
-      precompile-aux (global _ as C) A C A :- !.
-      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 (app [HD | _] as T) A (tc.coercion T Scope) A :- 
-        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,
-        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-prune-safe-fun MM Ty M') "[TC] should not fail1",
-        precompile-aux Ty M' Ty' M.
-
-      % Detect maybe-llam term
-      precompile-aux (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope1) [X|M] :-
-        var X _ Scope, split-pf XS Scope PF NPF, 
-        not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
-        names Scope1,
-        std.fold-map NPF N precompile-aux NPF1 M. 
-
-      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) (MM x), close-term-prune-safe-fun MM Ty M) "[TC] should not fail2",
-        precompile-aux Ty M Ty' P.
-
-      % Working with fun
-      precompile-aux (fun N T F) A (fun N T F1) A2 :- !, A = A1,
-        /*precompile-aux IsP T A T1 A1,*/ pi x\ precompile-aux (F x) A1 (F1 x) A2.
-      
-      precompile-aux (app L) A (app L1) A1 :- !, std.fold-map L A precompile-aux L1 A1.
-      precompile-aux (let N T B F) A (let N T1 B1 F1) A3 :- !,
-        precompile-aux T A T1 A1, precompile-aux B A1 B1 A2, pi x\ precompile-aux (F x) A2 (F1 x) A3.
-      precompile-aux (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
-        precompile-aux Ty A Ty1 A1, pi x\ precompile-aux (F x) A1 (F1 x) A2.
-      precompile-aux (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
-        precompile-aux T A T1 A1, precompile-aux Rty A1 Rty1 A2, std.fold-map B A2 precompile-aux B1 A3.
-      precompile-aux (primitive _ as C) A C A :- !.
-      precompile-aux (uvar _ _ as X) A X [X|A] :- !.
-      precompile-aux X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
-    }
-
-    pred goal i:term, o:term, o:list term.
-    goal T T' Vars' :- std.assert!(goal.precompile-aux T [] T' Vars) "[TC] cannot precompile goal", undup-same Vars Vars'. 
   }
 }
\ No newline at end of file
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 160e91ab9..4e19a490c 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -34,7 +34,7 @@ namespace tc {
     if-true print-links (coq.say "[TC] the links are" Links),
     tc.time-it tc.oTC-time-instance-search (
       do Links, Q,
-      tc.link.solve-cs,
+      tc.link.solve-cs,  % Trigger cs links (coercions + canonical structures)
       tc.link.solve-eta, % Trigger eta links
       tc.link.solve-llam % Trigger llam links
     ) "instance search".
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index 9152507e8..96e8fd442 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -227,7 +227,7 @@ Module HO_8.
     eexists.
     apply _.
     Unshelve.
-    apply nat.
+    auto.
   Qed.
 End HO_8.
 
@@ -559,14 +559,6 @@ Module CoqUvar3.
 
   Class c1 (T : Type -> Type -> Type).
   Instance i1 A: c1 (fun x y => f (A x y) (A x y)). Qed.
-  
-  Elpi Query TC.Solver lp:{{
-    tc.precomp.goal {{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\ tc.maybe-llam-tm (app [app [X], (Y x y), y]) [x,y]),
-    std.assert! (C = Expected) "[TC] invalid compilation".
-  }}.
 
   (* Note: here interesting link-dedup *)
   Goal exists X (A: Type -> Type -> Type), c1 (fun x y => X (A x y) y).
@@ -608,7 +600,7 @@ Module CoqUvar4.
     std.assert! (C = Expected) "[TC] invalid compilation".
   }}.
 
-  (* Note: here interesting failtc-c1ing link-dedup *)
+  (* Note: here interesting fail link-dedup *)
   Goal forall f, exists X, c1 (X nat) -> 
     c1 (f nat nat).
     do 1 eexists.

From 33973cab52f1bda22c6b369403fd1feddf51b059 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Sat, 10 Aug 2024 17:10:19 +0200
Subject: [PATCH 16/32] [TC] refactor filenames + reorder import

---
 apps/tc/elpi/WIP/force_llam.elpi              | 131 ------------
 apps/tc/elpi/WIP/modes.elpi                   |  44 ----
 apps/tc/elpi/base.elpi                        |  30 +--
 apps/tc/elpi/compile_goal.elpi                |  12 +-
 ...{ho_compile.elpi => compile_instance.elpi} | 190 +++++++++++++++++-
 .../tc/elpi/{compiler1.elpi => compiler.elpi} |   0
 apps/tc/elpi/ho_precompile.elpi               | 187 -----------------
 apps/tc/elpi/{ho_link.elpi => link.elpi}      |   0
 apps/tc/elpi/solver.elpi                      |   2 +-
 apps/tc/src/coq_elpi_tc_register.ml           |   4 -
 apps/tc/tests/importOrder/sameOrderCommand.v  |   4 +-
 apps/tc/theories/add_commands.v               |  51 ++---
 apps/tc/theories/tc.v                         |  54 ++---
 apps/tc/theories/wip.v                        |  21 +-
 14 files changed, 243 insertions(+), 487 deletions(-)
 delete mode 100644 apps/tc/elpi/WIP/force_llam.elpi
 delete mode 100644 apps/tc/elpi/WIP/modes.elpi
 rename apps/tc/elpi/{ho_compile.elpi => compile_instance.elpi} (61%)
 rename apps/tc/elpi/{compiler1.elpi => compiler.elpi} (100%)
 delete mode 100644 apps/tc/elpi/ho_precompile.elpi
 rename apps/tc/elpi/{ho_link.elpi => link.elpi} (100%)

diff --git a/apps/tc/elpi/WIP/force_llam.elpi b/apps/tc/elpi/WIP/force_llam.elpi
deleted file mode 100644
index d89f2a239..000000000
--- a/apps/tc/elpi/WIP/force_llam.elpi
+++ /dev/null
@@ -1,131 +0,0 @@
-% This is an effort for forcing llam links when used as input variables
-% in a premise call. However, this brings several issues to find
-% the right variable to activate the right link.s
-namespace force-llam {
-  pred is-uvar-destruct i:term, o:term.
-  is-uvar-destruct T R :- name T Hd _, name-pair R Hd _, !.
-  is-uvar-destruct T T :- is-uvar T.
-
-  % At compile time, given a premise p with a flexible argument X.
-  % If X is expected to be in input mode, we add the auxiliary clause 
-  % `solve-llam-t X`, so that, if any suspended
-  % llam link on X exists, then it is forced before solving p 
-  pred modes i:list string, i:list term, o:list prop.
-  modes ["o"] [] [] :- !.
-  modes ["+" | Ms] [X | Xs] [P | Ps] :- is-uvar-destruct X R, !, 
-    P = tc.link.solve-llam-t R, modes Ms Xs Ps.
-  modes ["!" | Ms] [X | Xs] [P | Ps] :- is-uvar-destruct X R, !, 
-    P = tc.link.solve-llam-t R, modes Ms Xs Ps.
-  modes [_ | Ms] [_ | Xs] Ps :- 
-    modes Ms Xs Ps.
-
-  % The following rule represents a try to force llam links when input of
-  % of other premises. 
-  compile-conclusion ff Goal Proof HOPremisesIn HOPremisesOut Premises Clause :-
-    coq.safe-dest-app Goal Class Args,
-    tc.get-mode {tc.get-TC-of-inst-type Class} Modes,
-    force-llam.modes Modes Args ForceLlam,
-    tc.make-tc Goal Proof Premises ff Clause1, 
-    Prems = [HOPremisesIn, ForceLlam, [Clause1], HOPremisesOut],
-    std.flatten Prems AllPremises,
-    Clause = do AllPremises.
-
-  %                            Scope        Var     Args       Rhs
-  pred progress-llam-refine i:list term, i:term, i:list term, o:term.
-  progress-llam-refine S V [A|As] R :- name A, not (std.mem! S A), !,
-    % prune (V' A) [A|S],
-    eta V (fun _ _ (x\ V' x)),
-    progress-llam-refine [A|S] (V' A) As R.
-  progress-llam-refine _ V [] V.
-  progress-llam-refine _ V As (app [V|As]).
-
-  pred split-pf i:list term, i:list term, o:list term, o:list term.
-  split-pf [] _ [] [] :- !.
-  split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
-  split-pf Xs _ [] Xs.
-
-  pred lam->fun i:term, i:list term, i:any.
-  lam->fun T [] R :- !, std.unsafe-cast R R', copy T T', R' = T'.
-  lam->fun Hd [H|L] R :- !,
-    pi x\ (copy H x :- !) => lam->fun Hd L (R' x),
-    std.unsafe-cast R Rx, Rx = R'.
-
-  pred unify-align i:term, i:term, i:list term, i:list term.
-  unify-align (app L) Hd PF NPF :-
-    Len is {std.length L} - {std.length NPF}, Len >= 0,
-    std.split-at Len L L' NPF,
-    Z = app L',
-    coq.mk-app Z NPF TT,
-    lam->fun TT {std.append PF NPF} Hd.
-
-  pred unify-const i:term, i:term, i:list term.
-  unify-const N R [] :- !, copy N X, R = X.
-  unify-const N R [A|As] :- not found.aux, A == N, !,
-    pi x\ found.aux => (copy N x :- !) => unify-const N (R' x) As,
-    std.unsafe-cast R Rx, Rx = R'.
-  unify-const N R [_|As] :- 
-    pi x\ unify-const N (R' x) As,
-    std.unsafe-cast R Rx, Rx = R'.
-
-  pred unify-heuristics i:term, i:term.
-  unify-heuristics A T :- tc.unify-eq A T.
-  % unify-heuristics (app _ as A) (fun _ _ B) :- !,
-  %   coq.error "A",
-  %   eta-expand A (fun _ _ A'), pi x\ unify-heuristics (A' x) (B x).
-  % unify-heuristics (app _ as A) B :- var B Hd Tl, !,
-  %   split-pf Tl [] PF NPF, 
-  %   unify-align A Hd PF NPF.
-  % unify-heuristics A B :- name A, var B Hd Tl, !, % TODO: also const
-  %   unify-const A Hd Tl.
-  % unify-heuristics (app L) (app[X|L']) :-
-  %   var X, !,
-  %   Len is {std.length L} - {std.length L'}, Len > 0,
-  %   std.split-at Len L Hd L',
-  %   if (Hd = [X]) true (X = app Hd).
-  % unify-heuristics (app L) (app L') :-
-  %   std.forall2 L L' unify-heuristics. 
-  % % The following rule leaves elpi uvars outside PF in coq
-  % % unify-heuristics A B :- A = B.
-  % % The following seems to solve the problem of the previous rule
-  % % TODO: I don't understand why the following rule cant be written as:
-  % % unify-heuristics A B :- var B Hb Lb, A = app[Hb|Lb] 
-  % % without breaking test CoqUvar2
-  % unify-heuristics (uvar Ha []) (uvar Hb Lb) :- !,
-  %     Ha = app[Hb|Lb].
-  % unify-heuristics (fun _ _ Bo) (uvar Hb_ Lb1) :- not (distinct_names Lb1), !,
-  %   Lb1 = [_ | Lb],
-  %   std.spy-do![prune Z Lb,
-  %   % std.unsafe-cast Hb Hb1,
-  %   (pi x\ unify-heuristics (Bo x) Z),
-  %   Hb_ = 
-  %   coq.error "TODO" Z].
-  % unify-heuristics A B :- A = B.
-
-  pred llam-aux i:term, i:term.
-  llam-aux A (uvar _ S as T) :- distinct_names S, !, A = T. % Here, both A and T are in PF
-  llam-aux A (uvar _ _ as T) :- !, A = T.
-  llam-aux A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, declare_constraint (llam A (app [H|L])) [_,A|Vars].
-  llam-aux A (app [H|L] as T) :- var H, !, get-vars T Vars, declare_constraint (llam A (app [H|L])) [_|Vars].
-  llam-aux A (app [H|L]) :- coq.mk-app H L T, !, unify-heuristics A T.
-
-  llam L (app [H|As]) :- var H _ S, !,
-    progress-llam-refine S H As Rhs,
-    llam-aux L Rhs.
-  llam L Rhs :- llam-aux L Rhs.
-
-  pred solve-llam-t-cond i:term, i:term.
-  :name "solve-llam-t-cond"
-  solve-llam-t-cond (uvar A _) (app [uvar B _ | _]) :- A = B.
-
-  % Aims to force a llam link suspended on the given variable
-  pred solve-llam-t o:term.
-  solve-llam-t X :- var X, !, declare_constraint (solve-llam-t X) [X].
-  solve-llam-t _.
-
-  constraint solve-llam solve-llam-t llam {
-    rule \ (solve-llam-t X) (llam A B) | (solve-llam-t-cond X B) <=> (unify-heuristics A B).
-    rule solve-llam \ (llam A B) <=> (unify-heuristics A B).
-    rule \ solve-llam.
-  }
-}
-
diff --git a/apps/tc/elpi/WIP/modes.elpi b/apps/tc/elpi/WIP/modes.elpi
deleted file mode 100644
index a7f1d58fc..000000000
--- a/apps/tc/elpi/WIP/modes.elpi
+++ /dev/null
@@ -1,44 +0,0 @@
-/* license: GNU Lesser General Public License Version 2.1 or later           */
-/* ------------------------------------------------------------------------- */
-
-% pred make-modes-cl i:gref, i:list term, i:term, i:list (list hint-mode), i:list (list term), o:prop.
-% make-modes-cl T V (prod _ _ X) HintModes L (pi x\ C x):-
-%   std.map HintModes (x\r\ [r|_] = x) FST,
-%   std.map HintModes (x\r\ [_|r] = x) LAST,
-%   pi x\ sigma NewL\
-%     std.map2 L FST (l\m\r\ if (m = mode-input) (r = [x | l]) (r = l)) NewL,
-%     make-modes-cl T [x | V] (X x) LAST NewL (C x).
-% make-modes-cl T V _ _ L Clause :-
-%   Ty = {coq.mk-app (global T) {std.rev V}},
-%   Clause = (pi s\ tc T Ty s :- std.forall L (x\ std.exists x var), !, coq.error "Invalid mode for" Ty).
-
-% takes the type of a class and build a list
-% of hint mode where the last element is mandatory
-pred make-last-hint-mode-input i:term, o:list hint-mode.
-make-last-hint-mode-input (prod _ _ (x\ (prod _ _ _) as T)) [mode-output | L] :-
-  pi x\ make-last-hint-mode-input (T x) L. 
-make-last-hint-mode-input (prod _ _ _) [mode-input].
-make-last-hint-mode-input (sort _) [].
-
-% build a list of the seme langht as the the passed one
-% where all the elements are []
-pred build-empty-list i:list B, o:list (list A).
-build-empty-list [] [].
-build-empty-list [_ | TL] [[] | L] :- 
-  build-empty-list TL L.
-
-% add the hint modes of a Class to the database.
-% note that if the Class has not specified hint mode
-% then we assume the hint mode to be - - - ... !
-pred add-modes i:gref.
-:if "add-modes"
-add-modes GR :-
-  % the hint mode is added only if not exists
-  if (not (tc.class GR _ _)) (
-    coq.env.typeof GR Ty,
-    coq.hints.modes GR "typeclass_instances" ModesProv,
-    if (ModesProv = []) (Modes = [{make-last-hint-mode-input Ty}]) (Modes = ModesProv),
-    % make-modes-cl GR [] Ty Modes {build-empty-list Modes} Cl,
-    % add-tc-db _ (after "firstHook") Cl,
-  ) true.
-add-modes _.
\ No newline at end of file
diff --git a/apps/tc/elpi/base.elpi b/apps/tc/elpi/base.elpi
index 6da2f0d0b..ca8b38b48 100644
--- a/apps/tc/elpi/base.elpi
+++ b/apps/tc/elpi/base.elpi
@@ -145,32 +145,10 @@ pred count-prod i:term , o:nat.
 count-prod (prod _ _ B) (s N) :- !, pi x\ count-prod (B x) N.
 count-prod _ z.
 
-pred close-prop i:(A -> list prop), o:list prop.
-close-prop (x\ []) [] :- !.
-close-prop (x\ [X | Xs x]) [X| Xs'] :- !, close-prop Xs Xs'.
-close-prop (x\ [X x | Xs x]) [pi x\ X x | Xs'] :- !, close-prop Xs Xs'. 
-
-pred close-prop-no-prune i:(A -> list prop), o:list prop.
-close-prop-no-prune (x\ []) [] :- !.
-close-prop-no-prune (x\ [X x | Xs x]) [pi x\ X x | Xs'] :- !, 
-  close-prop-no-prune Xs Xs'. 
-
-% [close-term-ty (x\ L) Ty R] Ty is the type of x
-pred close-term-ty i:(term -> list prop), i:term, o:list prop.
-close-term-ty (x\ []) _ [] :- !.
-close-term-ty (x\ [X | Xs x]) Ty [X| Xs'] :- !, close-term-ty Xs Ty Xs'.
-close-term-ty (x\ [X x | Xs x]) Ty [@pi-decl `x` Ty x\ X x | Xs'] :- !, 
-  close-term-ty Xs Ty Xs'. 
-
-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'.
+pred close-prop-no-prune-pi-decl i:(term -> list prop), i:term, o:list prop.
+close-prop-no-prune-pi-decl (x\ []) _ [] :- !.
+close-prop-no-prune-pi-decl (x\ [X x | Xs x]) Ty [@pi-decl `x` Ty x\ X x | Xs'] :- !, 
+  close-prop-no-prune-pi-decl Xs Ty Xs'. 
 
 pred free-names i:term, o:list term.
 free-names T L :-
diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
index 33ec8eef8..5e9e8bf94 100644
--- a/apps/tc/elpi/compile_goal.elpi
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -1,6 +1,6 @@
 namespace tc {
   namespace compile {
-    namespace goall {
+    namespace goal {
       :index (_ _ 1)
       pred may-contract-to i:list term, i:term, i:term.
       may-contract-to _ N N :- !.
@@ -56,7 +56,7 @@ namespace tc {
         (pi x\ compile-full-aux (Bo x) [] (Bo' x) (BoL x)),
       % TODO: maybe attach to the links the list of used binders, to simply make this check?
       % Maybe L' is a pair list links and list binders per link, this way we can easily prune
-        close-term-no-prune-ty BoL Ty BoL',
+        close-prop-no-prune-pi-decl BoL Ty BoL',
         std.append L BoL' L'.
 
       pred compile-full-aux i:term, i:list prop, o:term, o:list prop.
@@ -147,9 +147,9 @@ namespace tc {
       compile-full Goal Goal' Links :- compile-full-aux Goal [] Goal' Links.
     }
 
-    pred goal' i:term, o:term, o:list prop.
-    :name "compile-goal'"
-    goal' Goal Goal' Links :- 
-      goall.compile-full-aux Goal [] Goal' Links.
+    pred goal i:term, o:term, o:list prop.
+    :name "compile-goal"
+    goal Goal Goal' Links :- 
+      goal.compile-full-aux Goal [] Goal' Links.
   }
 }
diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/compile_instance.elpi
similarity index 61%
rename from apps/tc/elpi/ho_compile.elpi
rename to apps/tc/elpi/compile_instance.elpi
index 4ac3d2ba5..adb7a78e7 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/compile_instance.elpi
@@ -1,6 +1,190 @@
 namespace tc {
   shorten tc.{r-ar, range-arity}.
 
+  namespace precomp {
+
+    namespace instance {
+      % Tells if the current name is a bound variables
+      pred is-name o:term.
+      % Tells if the current name stands for a uvar
+      pred is-uvar o:term.
+
+      :index (_ _ 1)
+      pred may-contract-to i:list term, i:term, i:term.
+      may-contract-to _ N N :- !.
+      may-contract-to L N (app [V|S]) :- var V, !,
+        std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
+      may-contract-to L N (app [V|S]) :- is-uvar V, !,
+        std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
+      may-contract-to L N (app [N|A]) :-
+        std.length A {std.length L},
+        std.forall2 {std.rev L} A (may-contract-to []).
+      may-contract-to L N (fun _ _ B) :-
+        pi x\ may-contract-to [x|L] N (B x).
+
+      :index (_ 1)
+      pred occurs-rigidly i:term, i:term.
+      occurs-rigidly N N :- name N, !.
+      occurs-rigidly _ (app [N|_]) :- is-uvar N, !, fail.
+      occurs-rigidly _ (app [N|_]) :- var N, !, fail.
+      occurs-rigidly N (app A) :- exists! A (occurs-rigidly N).
+      occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
+
+      pred maybe-eta-aux i:term, i:list term.
+      maybe-eta-aux (app[V|S]) L :- is-uvar V, !,
+        std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
+      maybe-eta-aux (app[V|S]) L :- var V, !,
+        std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
+      maybe-eta-aux (app [_|A]) L :-
+        SplitLen is {std.length A} - {std.length L},
+        split-at-not-fatal SplitLen A HD TL,
+        std.forall L (x\ not (exists! HD (occurs-rigidly x))),
+        std.forall2 {std.rev L} TL (may-contract-to []). 
+      maybe-eta-aux (fun _ _ B) L :-
+        pi x\ maybe-eta-aux (B x) [x|L].
+
+      pred maybe-eta i:term.
+      maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].
+
+      pred free-var o:list term.
+      free-var L :-
+        std.findall (is-name _) T,
+        std.map T (x\y\ x = is-name y) L.
+
+      pred split-pf i:list term, i:list term, o:list term, o:list term.
+      split-pf [] _ [] [] :- !.
+      split-pf [X|Xs] Old [X|Ys] L :- is-name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
+      split-pf Xs _ [] Xs.
+
+      kind positivity type.
+      type is_pos positivity.
+      type is_neg positivity.
+      type is_neg_fix positivity.
+
+      :index (1 _)
+      pred neg i:positivity, o:positivity.
+      neg is_pos is_neg :- !.
+      neg is_neg is_pos :- !.
+      neg is_neg_fix is_neg_fix :- !.
+
+      macro @max-min :- r-ar inf z.
+
+      pred min-max-nat i:range-arity, i:range-arity, o:range-arity.
+      min-max-nat (r-ar A B) (r-ar A' B') (r-ar A'' B'') :- !,
+        min-nat A A' A'', max-nat B B' B''.
+
+      % TODO: this is incomplete: it lacks of some term constructors
+      pred get-range-arity-aux i:term, i:term, o:range-arity.
+      get-range-arity-aux N N (r-ar z z) :- !.
+      get-range-arity-aux _ N @max-min :- name N, !.
+      get-range-arity-aux T (app [T|L]) R :- !,
+        length-nat L Len,
+        std.fold L (r-ar Len Len) (x\y\w\ sigma M\ get-range-arity-aux T x M, min-max-nat y M w) R.
+      get-range-arity-aux T (app [_|L]) R :- !,
+        std.fold L @max-min (x\y\w\ sigma M\ get-range-arity-aux T x M, min-max-nat y M w) R.
+      get-range-arity-aux T (fun _ Ty B) R2 :- !,
+        get-range-arity-aux T Ty R,
+        (pi x\ get-range-arity-aux T (B x) R1),
+        min-max-nat R R1 R2.
+      get-range-arity-aux T (prod _ Ty B) R2 :- !,
+        get-range-arity-aux T Ty R,
+        (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 _ (sort _) @max-min :- !.
+      get-range-arity-aux _ (pglobal _ _) @max-min :- !.
+      get-range-arity-aux A B _ :- coq.error "Count maximal arity failure" A B.
+
+      pred get-range-arity i:term, i:term, i:term, o:range-arity.
+      get-range-arity _ Ty _ (r-ar z N) :- tc.get-TC-of-inst-type Ty _, !, count-prod Ty N.
+      get-range-arity B _ T N :- !, get-range-arity-aux B T N. 
+
+      pred precompile-aux i:positivity, i:term, i:nat, o:term, o:nat.
+      precompile-aux _ X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
+      precompile-aux _ (global _ as C) A C A :- !.
+      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.
+
+      % Detect maybe-eta term
+      % TODO: should I precompile also the type of the fun and put it in the output term
+      precompile-aux _ (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty B') Scope) (s M) :-
+        maybe-eta T, !,
+        free-var Scope,
+        precompile-aux is_neg_fix Ty N _ N',
+        (pi x\ is-name x => precompile-aux is_neg_fix (B x) N' (B' x) M).
+
+      precompile-aux _ (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope) (s M) :-
+        if (is-uvar X) (Sc = []) (var X _ Sc), split-pf XS Sc PF NPF, 
+        not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
+        free-var Scope,
+        std.fold-map NPF N (precompile-aux is_neg_fix) NPF1 M. 
+
+      % Charge if we work with unification variable or local name
+      % And returns the subterms is a prod-range
+      precompile-aux IsP (prod Name Ty B) N (tc.prod-range (prod Name Ty' B') MaxAr) P :- !,
+        std.assert! (pi x\ get-range-arity x Ty (B x) MaxAr) "[TC] get-range-arity should not fail",
+        if (IsP = is_pos) (C = x\ is-uvar x) (C = x\ is-name x),
+        std.assert! (pi x\ C x => precompile-aux IsP (B x) N (B' x) M) "[TC] should not fail",
+        precompile-aux {neg IsP} Ty M Ty' P.
+
+      % Working with fun
+      precompile-aux _ (fun N T F) A (fun N T1 F1) A2 :- !,
+        precompile-aux _ T A T1 A1, pi x\ is-name x => precompile-aux is_neg_fix (F x) A1 (F1 x) A2.
+      
+      precompile-aux _ (app L) A (app L1) A1 :- !, std.fold-map L A (precompile-aux is_neg_fix) L1 A1.
+      precompile-aux _ X A X A :- var X, !.
+
+      % TODO: what about the following constructors?
+      % precompile-aux IsP (let N T B F) A (let N T1 B1 F1) A3 :- !,
+      %   precompile-aux IsP T A T1 A1, precompile-aux IsP B A1 B1 A2, pi x\ is-name x => precompile-aux IsP (F x) A2 (F1 x) A3.
+      % precompile-aux IsP (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
+      %   precompile-aux IsP Ty A Ty1 A1, pi x\ is-name x => precompile-aux IsP (F x) A1 (F1 x) A2.
+      % precompile-aux IsP (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
+      %   precompile-aux IsP T A T1 A1, precompile-aux IsP Rty A1 Rty1 A2, std.fold-map B A2 (precompile-aux IsP) B1 A3.
+      % precompile-aux IsP (uvar M L as X) A W A1 :- var X, !, std.fold-map L A (precompile-aux IsP) L1 A1, coq.mk-app-uvar M L1 W.
+      % % when used in CHR rules
+      % precompile-aux IsP (uvar X L) A (uvar X L1) A1 :- std.fold-map L A (precompile-aux IsP) L1 A1.
+
+      pred get-univ-instances i:term, o:list univ-instance.
+      get-univ-instances T L :-
+        (pi x L\ fold-map (pglobal _ x) L _ [x | L] :- !) => fold-map T [] _ L, !.
+
+      pred get-univ i:term, o:list univ.
+      get-univ T L :-
+        coq.univ.variable.set.elements {coq.univ.variable.of-term T} Vars,
+        std.map Vars (x\r\ coq.univ.variable r x) L.
+
+    }
+
+    /*
+      [tc.precomp.instance T T' N] 
+      Returns T' N from T, where: 
+        T' is obtained by the replacement of
+          - all maybe-eta term `t1` with (tc.maybe-eta-tm `t1` `s`) where `s` = FV(`t1`)
+              ==> This helps knowing if a subterm should be replaced with a `eta-link`
+          - all `prod _ Ty (x\ Bo x)` with (tc.prod-range (prod _ Ty (x\ Bo x)) N), 
+            where N is represent the "maximal" application of `x` in `Bo`
+              for example:
+                let Ty = {{Type -> Type -> Type -> Type -> Type}},
+                and Bo = x\ c1 (x nat bool) (x nat) (x nat nat bool)
+              the term `prod _ Ty Bo` is replaced with
+                (tc.prod-range (prod _ T Bo) 3)
+              since x is applied at most 3 times in Bo
+                ==> This helps charging the right number of `eta-link` for map-deduplication rule
+        N is the number of problematic terms in T + nb of projections
+    */
+    pred instance i:term, o:term, o:nat, o:list univ, o:list univ-instance.
+    instance T T' N UnivConstL UnivInstL :-
+      tc.precomp.instance.get-univ T UnivConstL,
+      tc.precomp.instance.get-univ-instances T UnivInstL,
+      std.assert!(instance.precompile-aux instance.is_pos T z T' N) "[TC] cannot precompile instance".
+  }
+
   namespace compile {
 
     namespace instance {
@@ -12,8 +196,6 @@ namespace tc {
       % applied Ar times.
       pred name-pair o:term, o:term, o:nat.
 
-      pred force-llam-mem i:term, o:term.
-
       namespace decompile {
 
         pred decompile-term-aux i:term, i:pair (list term) (list prop), o:term, o:pair (list term) (list prop).
@@ -79,13 +261,13 @@ namespace tc {
 
         decompile-term-aux (fun Name Ty Bo) (pr XS L) (fun Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
-          close-term-no-prune-ty L1x Ty L1,
+          close-prop-no-prune-pi-decl L1x Ty L1,
           decompile-term-aux Ty (pr XS1 L) Ty' (pr XS2 L2),
           std.append L1 L2 L3.
 
         decompile-term-aux (prod Name Ty Bo) (pr XS L) (prod Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
-          close-term-no-prune-ty L1x Ty L1,
+          close-prop-no-prune-pi-decl L1x Ty L1,
           decompile-term-aux Ty (pr XS1 L) Ty' (pr XS2 L2),
           std.append L1 L2 L3.
 
diff --git a/apps/tc/elpi/compiler1.elpi b/apps/tc/elpi/compiler.elpi
similarity index 100%
rename from apps/tc/elpi/compiler1.elpi
rename to apps/tc/elpi/compiler.elpi
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
deleted file mode 100644
index db5852b87..000000000
--- a/apps/tc/elpi/ho_precompile.elpi
+++ /dev/null
@@ -1,187 +0,0 @@
-namespace tc {
-  shorten tc.{r-ar, range-arity}.
-
-  namespace precomp {
-
-    namespace instance {
-      % Tells if the current name is a bound variables
-      pred is-name o:term.
-      % Tells if the current name stands for a uvar
-      pred is-uvar o:term.
-
-      :index (_ _ 1)
-      pred may-contract-to i:list term, i:term, i:term.
-      may-contract-to _ N N :- !.
-      may-contract-to L N (app [V|S]) :- var V, !,
-        std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
-      may-contract-to L N (app [V|S]) :- is-uvar V, !,
-        std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
-      may-contract-to L N (app [N|A]) :-
-        std.length A {std.length L},
-        std.forall2 {std.rev L} A (may-contract-to []).
-      may-contract-to L N (fun _ _ B) :-
-        pi x\ may-contract-to [x|L] N (B x).
-
-      :index (_ 1)
-      pred occurs-rigidly i:term, i:term.
-      occurs-rigidly N N :- name N, !.
-      occurs-rigidly _ (app [N|_]) :- is-uvar N, !, fail.
-      occurs-rigidly _ (app [N|_]) :- var N, !, fail.
-      occurs-rigidly N (app A) :- exists! A (occurs-rigidly N).
-      occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
-
-      pred maybe-eta-aux i:term, i:list term.
-      maybe-eta-aux (app[V|S]) L :- is-uvar V, !,
-        std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
-      maybe-eta-aux (app[V|S]) L :- var V, !,
-        std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
-      maybe-eta-aux (app [_|A]) L :-
-        SplitLen is {std.length A} - {std.length L},
-        split-at-not-fatal SplitLen A HD TL,
-        std.forall L (x\ not (exists! HD (occurs-rigidly x))),
-        std.forall2 {std.rev L} TL (may-contract-to []). 
-      maybe-eta-aux (fun _ _ B) L :-
-        pi x\ maybe-eta-aux (B x) [x|L].
-
-      pred maybe-eta i:term.
-      maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].
-
-      pred free-var o:list term.
-      free-var L :-
-        std.findall (is-name _) T,
-        std.map T (x\y\ x = is-name y) L.
-
-      pred split-pf i:list term, i:list term, o:list term, o:list term.
-      split-pf [] _ [] [] :- !.
-      split-pf [X|Xs] Old [X|Ys] L :- is-name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
-      split-pf Xs _ [] Xs.
-
-      kind positivity type.
-      type is_pos positivity.
-      type is_neg positivity.
-      type is_neg_fix positivity.
-
-      :index (1 _)
-      pred neg i:positivity, o:positivity.
-      neg is_pos is_neg :- !.
-      neg is_neg is_pos :- !.
-      neg is_neg_fix is_neg_fix :- !.
-
-      macro @max-min :- r-ar inf z.
-
-      pred min-max-nat i:range-arity, i:range-arity, o:range-arity.
-      min-max-nat (r-ar A B) (r-ar A' B') (r-ar A'' B'') :- !,
-        min-nat A A' A'', max-nat B B' B''.
-
-      % TODO: this is incomplete: it lacks of some term constructors
-      pred get-range-arity-aux i:term, i:term, o:range-arity.
-      get-range-arity-aux N N (r-ar z z) :- !.
-      get-range-arity-aux _ N @max-min :- name N, !.
-      get-range-arity-aux T (app [T|L]) R :- !,
-        length-nat L Len,
-        std.fold L (r-ar Len Len) (x\y\w\ sigma M\ get-range-arity-aux T x M, min-max-nat y M w) R.
-      get-range-arity-aux T (app [_|L]) R :- !,
-        std.fold L @max-min (x\y\w\ sigma M\ get-range-arity-aux T x M, min-max-nat y M w) R.
-      get-range-arity-aux T (fun _ Ty B) R2 :- !,
-        get-range-arity-aux T Ty R,
-        (pi x\ get-range-arity-aux T (B x) R1),
-        min-max-nat R R1 R2.
-      get-range-arity-aux T (prod _ Ty B) R2 :- !,
-        get-range-arity-aux T Ty R,
-        (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 _ (sort _) @max-min :- !.
-      get-range-arity-aux _ (pglobal _ _) @max-min :- !.
-      get-range-arity-aux A B _ :- coq.error "Count maximal arity failure" A B.
-
-      pred get-range-arity i:term, i:term, i:term, o:range-arity.
-      get-range-arity _ Ty _ (r-ar z N) :- tc.get-TC-of-inst-type Ty _, !, count-prod Ty N.
-      get-range-arity B _ T N :- !, get-range-arity-aux B T N. 
-
-      pred precompile-aux i:positivity, i:term, i:nat, o:term, o:nat.
-      precompile-aux _ X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
-      precompile-aux _ (global _ as C) A C A :- !.
-      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.
-
-      % Detect maybe-eta term
-      % TODO: should I precompile also the type of the fun and put it in the output term
-      precompile-aux _ (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty B') Scope) (s M) :-
-        maybe-eta T, !,
-        free-var Scope,
-        precompile-aux is_neg_fix Ty N _ N',
-        (pi x\ is-name x => precompile-aux is_neg_fix (B x) N' (B' x) M).
-
-      precompile-aux _ (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope) (s M) :-
-        if (is-uvar X) (Sc = []) (var X _ Sc), split-pf XS Sc PF NPF, 
-        not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
-        free-var Scope,
-        std.fold-map NPF N (precompile-aux is_neg_fix) NPF1 M. 
-
-      % Charge if we work with unification variable or local name
-      % And returns the subterms is a prod-range
-      precompile-aux IsP (prod Name Ty B) N (tc.prod-range (prod Name Ty' B') MaxAr) P :- !,
-        std.assert! (pi x\ get-range-arity x Ty (B x) MaxAr) "[TC] get-range-arity should not fail",
-        if (IsP = is_pos) (C = x\ is-uvar x) (C = x\ is-name x),
-        std.assert! (pi x\ C x => precompile-aux IsP (B x) N (B' x) M) "[TC] should not fail",
-        precompile-aux {neg IsP} Ty M Ty' P.
-
-      % Working with fun
-      precompile-aux _ (fun N T F) A (fun N T1 F1) A2 :- !,
-        precompile-aux _ T A T1 A1, pi x\ is-name x => precompile-aux is_neg_fix (F x) A1 (F1 x) A2.
-      
-      precompile-aux _ (app L) A (app L1) A1 :- !, std.fold-map L A (precompile-aux is_neg_fix) L1 A1.
-      precompile-aux _ X A X A :- var X, !.
-
-      % TODO: what about the following constructors?
-      % precompile-aux IsP (let N T B F) A (let N T1 B1 F1) A3 :- !,
-      %   precompile-aux IsP T A T1 A1, precompile-aux IsP B A1 B1 A2, pi x\ is-name x => precompile-aux IsP (F x) A2 (F1 x) A3.
-      % precompile-aux IsP (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
-      %   precompile-aux IsP Ty A Ty1 A1, pi x\ is-name x => precompile-aux IsP (F x) A1 (F1 x) A2.
-      % precompile-aux IsP (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
-      %   precompile-aux IsP T A T1 A1, precompile-aux IsP Rty A1 Rty1 A2, std.fold-map B A2 (precompile-aux IsP) B1 A3.
-      % precompile-aux IsP (uvar M L as X) A W A1 :- var X, !, std.fold-map L A (precompile-aux IsP) L1 A1, coq.mk-app-uvar M L1 W.
-      % % when used in CHR rules
-      % precompile-aux IsP (uvar X L) A (uvar X L1) A1 :- std.fold-map L A (precompile-aux IsP) L1 A1.
-
-      pred get-univ-instances i:term, o:list univ-instance.
-      get-univ-instances T L :-
-        (pi x L\ fold-map (pglobal _ x) L _ [x | L] :- !) => fold-map T [] _ L, !.
-
-      pred get-univ i:term, o:list univ.
-      get-univ T L :-
-        coq.univ.variable.set.elements {coq.univ.variable.of-term T} Vars,
-        std.map Vars (x\r\ coq.univ.variable r x) L.
-
-    }
-
-    /*
-      [tc.precomp.instance T T' N] 
-      Returns T' N from T, where: 
-        T' is obtained by the replacement of
-          - all maybe-eta term `t1` with (tc.maybe-eta-tm `t1` `s`) where `s` = FV(`t1`)
-              ==> This helps knowing if a subterm should be replaced with a `eta-link`
-          - all `prod _ Ty (x\ Bo x)` with (tc.prod-range (prod _ Ty (x\ Bo x)) N), 
-            where N is represent the "maximal" application of `x` in `Bo`
-              for example:
-                let Ty = {{Type -> Type -> Type -> Type -> Type}},
-                and Bo = x\ c1 (x nat bool) (x nat) (x nat nat bool)
-              the term `prod _ Ty Bo` is replaced with
-                (tc.prod-range (prod _ T Bo) 3)
-              since x is applied at most 3 times in Bo
-                ==> This helps charging the right number of `eta-link` for map-deduplication rule
-        N is the number of problematic terms in T + nb of projections
-    */
-    pred instance i:term, o:term, o:nat, o:list univ, o:list univ-instance.
-    instance T T' N UnivConstL UnivInstL :-
-      tc.precomp.instance.get-univ T UnivConstL,
-      tc.precomp.instance.get-univ-instances T UnivInstL,
-      std.assert!(instance.precompile-aux instance.is_pos T z T' N) "[TC] cannot precompile instance".
-  }
-}
\ No newline at end of file
diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/link.elpi
similarity index 100%
rename from apps/tc/elpi/ho_link.elpi
rename to apps/tc/elpi/link.elpi
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 4e19a490c..9163960ff 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -8,7 +8,7 @@ msolve L _ :- coq.ltac.fail _ "[TC] fail to solve" L.
 namespace tc {
   pred build-query-from-goal i:term, i:term, o:prop, o:list prop.
   build-query-from-goal Goal Proof Q Links :-
-    tc.compile.goal' Goal Goal' Links, !,
+    tc.compile.goal Goal Goal' Links, !,
     coq.safe-dest-app Goal' (global TC) TL',
     std.append TL' [Proof] TL, !,
     coq.elpi.predicate {tc.gref->pred-name TC} TL Q.
diff --git a/apps/tc/src/coq_elpi_tc_register.ml b/apps/tc/src/coq_elpi_tc_register.ml
index 93b054332..6d92147fe 100644
--- a/apps/tc/src/coq_elpi_tc_register.ml
+++ b/apps/tc/src/coq_elpi_tc_register.ml
@@ -23,9 +23,6 @@ let gref2elpi_term (gref: GlobRef.t) : Cmd.raw =
 let observer_class (x : Typeclasses.typeclass) : Coq_elpi_arg_HOAS.Cmd.raw list = 
   [Cmd.String "new_class"; gref2elpi_term x.cl_impl]
 
-let observer_default_instance (x : Typeclasses.typeclass) : Coq_elpi_arg_HOAS.Cmd.raw list = 
-  [Cmd.String "default_instance";gref2elpi_term x.cl_impl]
-
 let observer_coercion add (x : Typeclasses.typeclass) : Coq_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
@@ -63,7 +60,6 @@ let class_runner f cl =
     observer_coercion false; 
     observer_class; 
     observer_coercion true; 
-    (* observer_default_instance *)
   ] in
   List.iter (fun obs -> f (obs cl)) actions
 
diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v
index c291768cb..c088da84f 100644
--- a/apps/tc/tests/importOrder/sameOrderCommand.v
+++ b/apps/tc/tests/importOrder/sameOrderCommand.v
@@ -2,7 +2,7 @@ From elpi.apps Require Export tc.
 
 From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
-From elpi.apps.tc.elpi Extra Dependency "ho_link.elpi" as ho_link.
+From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
 From elpi.apps.tc.elpi Extra Dependency "tc_same_order.elpi" as tc_same_order.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 
@@ -13,7 +13,7 @@ Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif.
-Elpi Accumulate File ho_link.
+Elpi Accumulate File link.
 Elpi Accumulate File tc_same_order.
 Elpi Typecheck.
 
diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index db1a54834..d9060725f 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -5,12 +5,11 @@ From elpi.apps.tc Require Import db.
 
 From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
-From elpi.apps.tc.elpi Extra Dependency "ho_precompile.elpi" as ho_precompile.
-From elpi.apps.tc.elpi Extra Dependency "ho_compile.elpi" as ho_compile.
-From elpi.apps.tc.elpi Extra Dependency "compiler1.elpi" as compiler1.
+From elpi.apps.tc.elpi Extra Dependency "compile_instance.elpi" as compile_instance.
+From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler.
 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 "ho_link.elpi" as ho_link.
+From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
 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,14 +19,9 @@ Set Warnings "+elpi".
 Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File ho_precompile.
-Elpi Accumulate File unif.
-Elpi Accumulate File ho_link.
-Elpi Accumulate File ho_compile.
-Elpi Accumulate File compiler1.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux.
+Elpi Accumulate File unif modes link.
+Elpi Accumulate File compile_instance compiler.
 Elpi Accumulate lp:{{  
   main L :- 
     args->str-list L L1,
@@ -38,14 +32,9 @@ Elpi Typecheck.
 Elpi Command TC.AddInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File ho_precompile.
-Elpi Accumulate File ho_compile.
-Elpi Accumulate File unif.
-Elpi Accumulate File ho_link.
-Elpi Accumulate File compiler1.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux.
+Elpi Accumulate File unif modes link.
+Elpi Accumulate File compile_instance compiler.
 Elpi Accumulate File parser_addInstances.
 Elpi Accumulate lp:{{
   main Arguments :- 
@@ -56,9 +45,7 @@ Elpi Typecheck.
 Elpi Command TC.AddAllClasses.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   % Ignore is the list of classes we do not want to add
@@ -71,9 +58,7 @@ Elpi Typecheck.
 Elpi Command TC.AddClasses.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   pred tc.add-all-classes i:list argument , i:tc.search-mode.
@@ -91,8 +76,7 @@ Elpi Typecheck.
 Elpi Command TC.AddHook.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
+Elpi Accumulate File base tc_aux.
 Elpi Accumulate lp:{{
   pred tc.addHook i:grafting, i:string. 
   tc.addHook Grafting NewName :- 
@@ -122,9 +106,7 @@ Elpi Typecheck.
 Elpi Command TC.Declare.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   main _ :- coq.warning "TC.Declare" {tc.warning-name} 
@@ -138,9 +120,7 @@ Elpi Typecheck.
 Elpi Command TC.Pending_mode.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   main M :- 
@@ -153,8 +133,7 @@ Elpi Typecheck.
 Elpi Command TC.AddRecordFields.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
+Elpi Accumulate File base tc_aux.
 Elpi Accumulate  lp:{{
   pred tc.add_tc.records_unif.aux i:int, i:term, i:list term, i:constant, o:prop.
   tc.add_tc.records_unif.aux 0 T Args ProjConstant P :- !,
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 180abce83..761ced06d 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -5,14 +5,15 @@ Declare ML Module "coq-elpi.tc".
 
 From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
-(* From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler. *)
-From elpi.apps.tc.elpi Extra Dependency "ho_precompile.elpi" as ho_precompile.
-From elpi.apps.tc.elpi Extra Dependency "ho_compile.elpi" as ho_compile.
-From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
-From elpi.apps.tc.elpi Extra Dependency "compiler1.elpi" as compiler1.
+
 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 "ho_link.elpi" as ho_link.
+
+From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
+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.
+
 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.
 
@@ -49,17 +50,9 @@ Elpi Typecheck.
 Elpi Tactic TC.Solver.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File unif.
-Elpi Accumulate File ho_link.
-(* Elpi Accumulate File compiler. *)
-Elpi Accumulate File ho_precompile.
-Elpi Accumulate File ho_compile.
-Elpi Accumulate File compiler1.
-Elpi Accumulate File create_tc_predicate.
-Elpi Accumulate File compile_goal.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux.
+Elpi Accumulate File unif modes link.
+Elpi Accumulate File compile_instance compile_goal.
 Elpi Accumulate File solver.
 Elpi Query lp:{{
   sigma Options\ 
@@ -82,15 +75,10 @@ Elpi Query lp:{{
 Elpi Command TC.Compiler.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
+Elpi Accumulate File base tc_aux.
+Elpi Accumulate File unif modes link.
+Elpi Accumulate File compile_instance compiler.
 Elpi Accumulate File create_tc_predicate.
-Elpi Accumulate File ho_precompile.
-Elpi Accumulate File ho_compile.
-Elpi Accumulate File unif.
-Elpi Accumulate File ho_link.
-Elpi Accumulate File compiler1.
-Elpi Accumulate File modes.
 Elpi Accumulate lp:{{
 
   /* 
@@ -126,11 +114,6 @@ Elpi Accumulate lp:{{
       coq.locate Cl GR, tc.add-class-gr tc.classic GR
     ) "Compiler for Class".
 
-  % used to build ad-hoc instance for eta-reduction on the argument of 
-  % Cl that have function type
-  main [str "default_instance", str Cl] :- !,
-    tc.eta-reduction-aux.main Cl.
-
   main A :- coq.error "Fail in TC.Compiler: not a valid input entry" A.
 }}.
 Elpi Typecheck.
@@ -139,8 +122,7 @@ Elpi Typecheck.
 Elpi Command TC.Set_deterministic.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
+Elpi Accumulate File base tc_aux.
 Elpi Accumulate lp:{{
   main [str ClassStr] :- 
     coq.locate ClassStr ClassGR, 
@@ -154,8 +136,7 @@ Elpi Typecheck.
 Elpi Command TC.Get_class_info.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
+Elpi Accumulate File base tc_aux.
 Elpi Accumulate lp:{{
   main [str ClassStr] :- 
     coq.locate ClassStr ClassGR, 
@@ -175,8 +156,7 @@ Elpi Typecheck.
 Elpi Command TC.Unfold.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate Db tc.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
+Elpi Accumulate File base tc_aux.
 Elpi Accumulate lp:{{
   pred tc.add-unfold i:gref.
   tc.add-unfold (const C) :-
@@ -191,6 +171,8 @@ Elpi Accumulate lp:{{
 }}.
 Elpi Typecheck.
 
+(* Registering, activating the new tactic TC.Solver for TC resolution
+   + overriding all TC resolution *)
 Elpi TC Solver Register TC.Solver.
 Elpi TC Solver Activate TC.Solver.
 Elpi TC Solver Override TC.Solver All.
diff --git a/apps/tc/theories/wip.v b/apps/tc/theories/wip.v
index 39ecc7c73..5055a9585 100644
--- a/apps/tc/theories/wip.v
+++ b/apps/tc/theories/wip.v
@@ -1,21 +1,22 @@
 (* license: GNU Lesser General Public License Version 2.1 or later           *)
 (* --------------------------------------------------------------------------*)
 
-Declare ML Module "coq-elpi.tc".
+(* Declare ML Module "coq-elpi.tc".
 From elpi Require Import elpi.
 
 From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
-From elpi.apps.tc.elpi Extra Dependency "ho_precompile.elpi" as ho_precompile.
-From elpi.apps.tc.elpi Extra Dependency "ho_compile.elpi" as ho_compile.
-From elpi.apps.tc.elpi Extra Dependency "compiler1.elpi" as compiler1.
-From elpi.apps.tc.elpi Extra Dependency "ho_link.elpi" as ho_link.
+
+From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
+From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler.
+From elpi.apps.tc.elpi Extra Dependency "compile_instance.elpi" as compile_instance.
+
 From elpi.apps.tc.elpi Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc.elpi Extra Dependency "alias.elpi" as alias.
 From elpi.apps.tc.elpi Extra Dependency "solver.elpi" as solver.
 From elpi.apps.tc.elpi Extra Dependency "rewrite_forward.elpi" as rforward.
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
-From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
+From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate. *)
 
 (* From elpi.apps Require Import tc.
 Set Warnings "+elpi".
@@ -25,10 +26,10 @@ Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
-Elpi Accumulate File ho_link.
+Elpi Accumulate File link.
 Elpi Accumulate File modes.
-Elpi Accumulate File ho_precompile.
-Elpi Accumulate File compiler1.
+Elpi Accumulate File compile_instance.
+Elpi Accumulate File compiler.
 Elpi Accumulate File ho_compile.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate File solver.
@@ -49,7 +50,7 @@ Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
-Elpi Accumulate File ho_link.
+Elpi Accumulate File link.
 Elpi Accumulate File alias.
 Elpi Accumulate lp:{{
   main [trm New, trm Old] :-

From 1c77fec92de05582f2febebdd74fed0e1406c647 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Sat, 10 Aug 2024 18:04:40 +0200
Subject: [PATCH 17/32] [TC] refactor of build-eta-llam-links

---
 apps/tc/elpi/compile_goal.elpi     | 42 ++--------------------
 apps/tc/elpi/compile_instance.elpi | 28 ++++-----------
 apps/tc/elpi/link.elpi             | 58 ++++++++++++++++++++++--------
 apps/tc/tests/test.v               |  2 +-
 4 files changed, 54 insertions(+), 76 deletions(-)

diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
index 5e9e8bf94..340c76f60 100644
--- a/apps/tc/elpi/compile_goal.elpi
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -35,11 +35,6 @@ namespace tc {
       pred maybe-eta i:term.
       maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].
 
-      pred split-pf i:list term, i:list term, o:list term, o:list term.
-      split-pf [] _ [] [] :- !.
-      split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
-      split-pf Xs _ [] Xs.
-
       pred used i:term, i:term.
       used X (uvar _ S) :- std.mem! S X, !.
       used X (fun _ _ Bo) :- pi x\ used X (Bo x).
@@ -86,41 +81,10 @@ namespace tc {
         compile-full-aux Ty L Ty' LTy,
         compile-full-aux-close Bo Ty LTy Bo' L'.
 
-      % NOTE: when compiling t = (app [X, x, y]) and [x,y] are distinct_names,
-      %       then the coq variable has not [x,y] in scope, it is applied to
-      %       them. Note also that t is a problematic term that cannot be
-      %       exposed to the else unification algorithm.  
-      %       The solution is to build the following links:  
-      %       X =η (λa.Y a)
-      %       a |- Y a =η (λb.Z a b)
-      %       and expose a variable W at toplevel having Z has head and [x, y]
-      %       as scope
-
-      % NOTE: when compiling t = (app [X, a, x]) where a is a constant and x a
-      %       name, we build a llam link.  
-      %       The link will be: T x =L X a x  
-      %       the exposed variable in the term will be T x
-
-      % NOTE: here a combination of eta and llam:  
-      %       let t = (app [X x y, z, c, w, d]) where X is a coq var with x and
-      %       y in scope, z and w are names and c, d are constants.  
-      %       In this case, the links should be:  
-      %       X x y =η (λa.Y x y a)  
-      %       a |- Z x y a w =L (app[Y x y a, c w d])  
-      %       The returned variable is Z x y a w
-
-      % Link for beta-redex (Uvar in PF)
-      % BUILD CHAIN OF LINKS-ETA from X to V...
       % TODO: to avoid too many chain for the same var, maybe pass a list into the fold
-      compile-full-aux (app [(uvar _ Scope as V) | S] as T) L G' L'' :- !,
-        % By construction the scope of a uvar is a list of distinct name
-        std.fold-map S L compile-full-aux S' L', % LS = Links built for S
-        coq.typecheck V Ty ok,
-        split-pf S' Scope PF NPF,
-        free-names T Names,
-        tc.link.build-eta-llam-links V Scope Ty Names PF NPF L' G'' L'',
-        prune G' Names,
-        var G' G'' Names.
+      compile-full-aux (app [(uvar _ _ as V) | S]) L G' L'' :- !,
+        std.fold-map S L compile-full-aux S' L', % L' = Links built for S
+        tc.link.build-eta-llam-links (app [V|S']) L' G' L''.
 
       compile-full-aux (app L) A (app L1) A1 :- !, std.fold-map L A compile-full-aux L1 A1.
 
diff --git a/apps/tc/elpi/compile_instance.elpi b/apps/tc/elpi/compile_instance.elpi
index adb7a78e7..ac94c44bf 100644
--- a/apps/tc/elpi/compile_instance.elpi
+++ b/apps/tc/elpi/compile_instance.elpi
@@ -119,7 +119,7 @@ namespace tc {
         (pi x\ is-name x => precompile-aux is_neg_fix (B x) N' (B' x) M).
 
       precompile-aux _ (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope) (s M) :-
-        if (is-uvar X) (Sc = []) (var X _ Sc), split-pf XS Sc PF NPF, 
+        is-uvar X, split-pf XS [] PF NPF, 
         not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
         free-var Scope,
         std.fold-map NPF N (precompile-aux is_neg_fix) NPF1 M. 
@@ -237,27 +237,11 @@ namespace tc {
           std.fold-map NPF (pr XS L1) decompile-term-aux Tl (pr XS' L2), 
           NL = tc.link.llam Y (app [Hd|Tl]).
 
-        % Maybe-llam when H is a hole appearing in the shelved goals
-        % This happens when the instance to be compiled comes from the context
-        % Example: Goal exists (X : T1 -> T2), forall a, c (X a) -> ...
-        %            intros; eexists. (* In the context we have the instance `H: c (?X a)` *)
-        decompile-term-aux (tc.maybe-llam-tm (app[app[V | PF] | NPF] as T) S_) L G'' (pr XS' L'') :-  !,
-          var V _ Scope, !,
-          std.fold-map NPF L decompile-term-aux NPF' (pr XS' L'),
-          free-names T Names,
-          coq.typecheck V Ty ok,
-          tc.link.build-eta-llam-links V Scope Ty Names PF NPF' L' G' L'',
-          prune G'' Names,
-          var G'' G' Names.
-
-        % HO var when H is a hole appearing in the shelved goals
-        decompile-term-aux (app [V|PF] as T) (pr XS' L') G'' (pr XS' L'') :-
-          var V _ Scope, !,
-          free-names T Names,
-          coq.typecheck V Ty ok,
-          tc.link.build-eta-llam-links V Scope Ty Names PF [] L' G' L'',
-          prune G'' Names,
-          var G'' G' Names.
+        % Here we have a coq evar applied to some terms. In this case, we build
+        % eta-llam links after the decompilation of S.
+        decompile-term-aux (app [(uvar _ _ as V)|S]) PR H (pr XS L') :- !,
+          std.fold-map S PR decompile-term-aux S' (pr XS L),
+          tc.link.build-eta-llam-links (app [V|S']) L H L'.
 
         decompile-term-aux (fun Name Ty Bo) (pr XS L) (fun Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
diff --git a/apps/tc/elpi/link.elpi b/apps/tc/elpi/link.elpi
index e0d43131a..0cadfdecd 100644
--- a/apps/tc/elpi/link.elpi
+++ b/apps/tc/elpi/link.elpi
@@ -9,28 +9,58 @@ namespace tc {
       (pi X H L Ign\ fold-map X L X [H|L] :- var X H Ign, !) => 
         fold-map T [] _ R.
 
-    % [build-eta-llam-links LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
-    % Builds the eta/llam links at runtime for a term having the shape 
-    % `app[(uvar X Scope as V) | L]`.
-    % LHS should be V, Scope the scope of V, TODO: finish to document this...
+    pred split-pf i:list term, i:list term, o:list term, o:list term.
+    split-pf [] _ [] [] :- !.
+    split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
+    split-pf Xs _ [] Xs.
+
+    % [build-eta-llam-links.aux LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
     :index(_ _ _ _ 3)
-    % TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
-    %                           LHS      Scope      Ty          Names        PF         NPF        OldLinks    NewVar
-    pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
-    build-eta-llam-links LHS _ _       Names []  NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
+    pred build-eta-llam-links.aux i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
+    build-eta-llam-links.aux LHS _ _       Names []  NPF OL HD [llam T (app [LHS | NPF]) | OL] :- !,
       std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
       prune T Names,
       var T HD _. 
-    build-eta-llam-links LHS SC (prod _ Ty _)       _    [X] []  OL HD [tc.link.eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
+    build-eta-llam-links.aux LHS SC (prod _ Ty _)       _    [X] []  OL HD [eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
       prune V SC, var (V X) HD _.
-    build-eta-llam-links LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [tc.link.eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
+    build-eta-llam-links.aux LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
     % TODO: unfold Ty if needed...
       std.append SC [X] SC',
-      prune LHS' SC, build-eta-llam-links (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
-    build-eta-llam-links LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
+      prune LHS' SC, build-eta-llam-links.aux (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
+    build-eta-llam-links.aux LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
       Ty' = prod _ _ _, coq.unify-eq Ty Ty' ok, !,
-      build-eta-llam-links LHS SC Ty' Names PF NPF OL HD L.
-
+      build-eta-llam-links.aux LHS SC Ty' Names PF NPF OL HD L.
+    
+    % [build-eta-llam-links T OldLinks X NewLinks]  
+    % T = app[(uvar _ Scope) | S] this term is problematic and asks for the
+    % creation of eta- and/or llam-links. Below some examples:
+
+    % eta: when compiling t = (app [X, x, y]) and [x,y] are distinct_names, then
+    %     the coq variable has not [x,y] in scope: it is applied to them.  
+    %     The solution is to build the following links:  
+    %     NewLinks = [X =η (λa.Y a),     a |- Y a =η (λb.Z a b)]
+    %     and the exposed variable is G, given by `var G Z [x, y]`
+
+    % llam: when compiling t = (app [X, a, x]) where a is a constant and x a
+    %       name, we build a llam link.  
+    %       The link will be: NewLinks ] = [T x =L X a x]  
+    %       and the exposed variable is G, given by `var G T [x]`
+
+    % eta-llam: here a combination of eta and llam:  
+    %       let t = (app [X x y, z, c, w, d]) where X is a coq var with x and y
+    %       in scope, z and w are names and c, d are constants.  
+    %       In this case, the links should be:  
+    %       NewLinks = [X x y =η (λa.Y x y a),   a |- Z x y a w =L (app[Y x y a, c w d])]  
+    %       and the exposed variable is G, given by `var Z T [x, y, z, w]`  
+    pred build-eta-llam-links i:term, i:list prop, o:term, o:list prop.
+    build-eta-llam-links (app[(uvar _ Scope as V) | S] as T) Links G NewLinks :- !,
+      coq.typecheck V Ty ok,
+      split-pf S Scope PF NPF,
+      free-names T Names,
+      build-eta-llam-links.aux V Scope Ty Names PF NPF Links LhsHd NewLinks,
+      prune G Names,
+      var G LhsHd Names.
+    build-eta-llam-links T _ _ _ :- coq.error "[TC] invalid call to build-eta-llam-links:" T.
 
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     % ETA LINK                                                                 %
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index 96e8fd442..228748ba7 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -596,7 +596,7 @@ Module CoqUvar4.
     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\ tc.maybe-llam-tm (app [app [X], (Y x y), y]) [y,x]),
+    Body2 = (x\y\ app [X, (Y x y), y]),
     std.assert! (C = Expected) "[TC] invalid compilation".
   }}.
 

From a496c70e3b5aa6f46544a5f2985cd9bbfd374bda Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 20 Aug 2024 11:07:16 +0200
Subject: [PATCH 18/32] [TC] avoid a backtrack

---
 apps/tc/elpi/link.elpi | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/apps/tc/elpi/link.elpi b/apps/tc/elpi/link.elpi
index 0cadfdecd..37a79e119 100644
--- a/apps/tc/elpi/link.elpi
+++ b/apps/tc/elpi/link.elpi
@@ -198,7 +198,7 @@ namespace tc {
       cs (uvar _ as V) (app [HD | _] as T) :- 
         if (HD = global (const Proj), tc.proj->record Proj Record)
           (reduce-cs V T Record Proj)
-          (coq.unify-eq V T ok).
+          (coq.unify-eq V T ok), !.
       cs T1 T2 :- not (T2 = app _), !, coq.unify-eq T1 T2 ok.
 
       pred unify-under-ctx i:list term, i:list term, i:term, i:term, i:term, i:term.

From b4a4dd28fbd910cf2e7a6ed4dc6bba058ca68ef4 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 19 Sep 2024 16:04:54 +0200
Subject: [PATCH 19/32] [TC] clean compile-conclusion predicate

---
 _opam                                        |  1 +
 apps/tc/elpi/compile_instance.elpi           | 47 ++++++++++----------
 apps/tc/tests/test.v                         |  4 +-
 apps/tc/tests/test_HO.v                      |  4 +-
 apps/tc/tests/test_backtrack_several_goals.v |  4 +-
 apps/tc/tests/test_scope.v                   |  1 -
 apps/tc/tests/test_tc.v                      |  2 -
 7 files changed, 31 insertions(+), 32 deletions(-)
 create mode 120000 _opam

diff --git a/_opam b/_opam
new file mode 120000
index 000000000..343b677d2
--- /dev/null
+++ b/_opam
@@ -0,0 +1 @@
+/home/dfissore/Documents/github/COQ_ELPI_DEV/_opam
\ No newline at end of file
diff --git a/apps/tc/elpi/compile_instance.elpi b/apps/tc/elpi/compile_instance.elpi
index ac94c44bf..a06857943 100644
--- a/apps/tc/elpi/compile_instance.elpi
+++ b/apps/tc/elpi/compile_instance.elpi
@@ -371,6 +371,10 @@ namespace tc {
         pi x y\ name-pair P x (s N) => is-uvar x => add-link-eta-dedup F (r-ar M N) P PTy [pr x y|Acc] PremR (Clause x y).
       add-link-eta-dedup _ Ar P PTy _ _ _ :- coq.error "[TC] add-link-eta-dedup error" Ar P PTy. 
 
+      pred deterministic-prem i:gref, i:prop, o:prop.
+      deterministic-prem TC P (do-once P) :- tc.class TC _ tc.deterministic _, !.
+      deterministic-prem _ P P.
+
       pred compile-premise
         i:list term,
         o:list term,
@@ -382,16 +386,14 @@ namespace tc {
         i:list term,
         i:list prop,
         o:prop.
-      compile-premise L L2 P PTy ProofHd IsPositive ITy ProofTlR PremR Clause :-
+      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, !,
         compile-ty L L1 P {neg IsPositive} PTy [] [] NewPrem,
-        if (tc.class TC _ tc.deterministic _)
-          (NewPrem' = do-once NewPrem)
-          (NewPrem' = NewPrem),
-        compile-ty L1 L2 ProofHd IsPositive ITy ProofTlR [NewPrem' | PremR] Clause.
-      compile-premise L L1 _ _ ProofHd IsPositive ITy ProofTlR PremR Clause :-
-        compile-ty L L1 ProofHd IsPositive ITy ProofTlR PremR Clause. 
+        deterministic-prem TC NewPrem NewPrem',
+        compile-ty L1 L2 ProofHd IsPositive ITy ProofArgsR [NewPrem' | PremR] Clause.
+      compile-premise L L1 _ _ ProofHd IsPositive ITy ProofArgsR PremR Clause :-
+        compile-ty L L1 ProofHd IsPositive ITy ProofArgsR PremR Clause. 
 
       pred compile-ty 
         i:list term,
@@ -402,39 +404,38 @@ namespace tc {
         i:list term,
         i:list prop,
         o:prop.
-      compile-ty L L1 ProofHd IsPositive (tc.prod-range (prod N Ty Bo) Arity) ProofTlR PremR Clause :- !,
+      compile-ty L L1 ProofHd IsPositive (tc.prod-range (prod N Ty Bo) Arity) ProofArgsR PremR Clause :- !,
         std.do![
           if (IsPositive = tt) 
             (Clause = (pi x\ C x), E = is-uvar) 
             (clean-term Ty Ty', Clause = (pi x\ decl x N Ty' => C x), E = is-name),
           pi p\ sigma F\
-            F = compile-premise L L1 p Ty ProofHd IsPositive (Bo p) [p|ProofTlR],
+            F = compile-premise L L1 p Ty ProofHd IsPositive (Bo p) [p|ProofArgsR],
             decl p N Ty' =>
             name-pair p p z => E p => add-link-eta-dedup F Arity p Ty [] PremR (C p)
         ].
-      compile-ty L L2 ProofHd IsPositive Goal ProofTlR PremR Clause :-
+      compile-ty L L2 ProofHd IsPositive Goal ProofArgsR PremR Clause :-
         std.do![    
-          coq.mk-app ProofHd {std.rev ProofTlR} Proof,
-          decompile.decompile-term L L1 Proof Proof' Prem1,
-          decompile.decompile-term L1 L2 Goal Goal' Prem2,
-          compile-conclusion IsPositive Goal' Proof' Prem2 Prem1 {std.rev PremR} Clause
+          coq.mk-app ProofHd {std.rev ProofArgsR} Proof,
+          decompile.decompile-term L L1 Proof Proof' EmptyLinks,
+          std.assert! (EmptyLinks = []) "[TC] should be empty", 
+          decompile.decompile-term L1 L2 Goal Goal' Links,
+          compile-conclusion IsPositive Goal' Proof' Links {std.rev PremR} Clause
         ].
 
       pred compile-conclusion 
         i:bool,             % tt if the term is in positive position
         i:term,             % the goal (invariant: it is a constant or a application)
         i:term,             % the proof
-        i:list prop,        % the list of HOPremises in input mode
-        i:list prop,        % the list of HOPremises in output mode
+        i:list prop,        % the list of links
         i:list prop,        % the premises
         o:prop.             % the compiled clause for the instance
 
-      compile-conclusion tt Goal Proof HOPremisesIn HOPremisesOut Premises Clause :-
-        std.append {std.append HOPremisesIn Premises} HOPremisesOut AllPremises,
+      compile-conclusion tt Goal Proof Links Premises Clause :-
+        std.append Links Premises AllPremises,
         tc.make-tc Goal Proof AllPremises tt Clause.
-      compile-conclusion ff Goal Proof HOPremisesIn HOPremisesOut Premises Clause :-
-        tc.make-tc Goal Proof Premises ff Clause1, 
-        Clause = (do HOPremisesIn, Clause1, do HOPremisesOut).
+      compile-conclusion ff Goal Proof Links Premises (do Links, Clause) :-
+        tc.make-tc Goal Proof Premises ff Clause.
 
       pred context i:goal-ctx, o:list prop.
       context [] [].
@@ -465,9 +466,9 @@ namespace tc {
     % If the instance is polymorphic, we wrap its gref into the pglobal constructor
     instance-gr InstGR (pi x\ Clause x) :- coq.env.univpoly? InstGR _, !,
       coq.env.typeof InstGR Ty,
-      pi x\ tc.compile.instance Ty (pglobal InstGR x) (Clause x).
+      pi x\ instance Ty (pglobal InstGR x) (Clause x).
     instance-gr InstGR Clause :-
       coq.env.typeof InstGR Ty,
-      tc.compile.instance Ty (global InstGR) Clause.
+      instance Ty (global InstGR) Clause.
   }
 }
\ No newline at end of file
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index 228748ba7..2b9e8f308 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -17,7 +17,7 @@ Module test_link_eta_generation.
   Class d (T : Type) (T : Type -> Type -> Type -> Type).
   Elpi Accumulate TC.Solver lp:{{
     :after "0" 
-    tc.compile.instance.compile-conclusion _ (app [H|_]) _ _ _ Premises _ :-
+    tc.compile.instance.compile-conclusion _ (app [H|_]) _ _ Premises _ :-
       H = {{test_link_eta_generation.c}}, !,
       std.assert! (Premises = [do [tc.link.eta _ _] | _]) "[TC] Wrong number of eta links",
       coq.say "Good padding from here",
@@ -25,7 +25,7 @@ Module test_link_eta_generation.
   }}.
   Elpi Query TC.Solver lp:{{
     ToCompile = {{forall (T : Type -> Type -> Type -> Type), (forall (a: Type), d a T) -> c T}},
-    not (tc.compile.instance ToCompile _ _).
+    pi x\ not (tc.compile.instance ToCompile x _).
   }}.
 End test_link_eta_generation.
 
diff --git a/apps/tc/tests/test_HO.v b/apps/tc/tests/test_HO.v
index 037a95482..7ffc76571 100644
--- a/apps/tc/tests/test_HO.v
+++ b/apps/tc/tests/test_HO.v
@@ -200,7 +200,7 @@ Module HO_PF1.
     Proof.
       eexists; intros.
       Elpi Bound Steps 30000.
-      Set Typeclasses Debug.
+      (* Set Typeclasses Debug. *)
       apply _.
       Unshelve.
       auto.
@@ -321,7 +321,7 @@ Module F.
 
   Goal forall (T : Type -> Type) (H : forall x, T x), C1 T H -> D.
     intros.
-    Set Typeclasses Debug.
+    (* Set Typeclasses Debug. *)
     Set Debug "tactic-unification".
     Elpi TC Solver Override TC.Solver None.
     Fail apply _. (* Here coq's unfication algorithm fails: 
diff --git a/apps/tc/tests/test_backtrack_several_goals.v b/apps/tc/tests/test_backtrack_several_goals.v
index 8e146a704..085bbc316 100644
--- a/apps/tc/tests/test_backtrack_several_goals.v
+++ b/apps/tc/tests/test_backtrack_several_goals.v
@@ -12,7 +12,7 @@ Module M.
 
   Goal exists i, C i.
     eexists.
-    Set Typeclasses Debug.
+    (* Set Typeclasses Debug. *)
     (* Here backtracking is done *)
     apply m.
   Qed.
@@ -32,7 +32,7 @@ Module M1.
 
   Goal exists i, C i.
     eexists.
-    Set Typeclasses Debug.
+    (* Set Typeclasses Debug. *)
     apply m.
     (* 
       Note: in coq the following command fails since apply is a single entry
diff --git a/apps/tc/tests/test_scope.v b/apps/tc/tests/test_scope.v
index 5c4d00b35..e651d1325 100644
--- a/apps/tc/tests/test_scope.v
+++ b/apps/tc/tests/test_scope.v
@@ -10,7 +10,6 @@ Goal C Q ->  exists (T : Type -> Type), forall R, C R -> C (T).
   intros.
   Set Printing Existential Instances.
   assert (C Q) by auto.
-  Elpi Trace Browser.
   apply _.
   Show Proof.
 Abort.
diff --git a/apps/tc/tests/test_tc.v b/apps/tc/tests/test_tc.v
index 79556281a..b2b3280d0 100644
--- a/apps/tc/tests/test_tc.v
+++ b/apps/tc/tests/test_tc.v
@@ -1,7 +1,5 @@
 From elpi.apps Require Import tc.
 
-Elpi TC Solver Override TC.Solver All.
-
 Class a (N: nat).
 Instance b : a 3. Qed.
 Instance c : a 4. Qed.

From 35e25ee9a3b8ea6a93655cd4fe53d5474484efca Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 22 Aug 2024 11:19:36 +0200
Subject: [PATCH 20/32] [TC] link small refactor

---
 apps/tc/elpi/link.elpi | 68 +++++++++++++++++++++++-------------------
 1 file changed, 38 insertions(+), 30 deletions(-)

diff --git a/apps/tc/elpi/link.elpi b/apps/tc/elpi/link.elpi
index 37a79e119..24e52f636 100644
--- a/apps/tc/elpi/link.elpi
+++ b/apps/tc/elpi/link.elpi
@@ -17,17 +17,17 @@ namespace tc {
     % [build-eta-llam-links.aux LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
     :index(_ _ _ _ 3)
     pred build-eta-llam-links.aux i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
+    build-eta-llam-links.aux _   _ _       _     []  []  _  _  _ :-coq.error "MH?".
     build-eta-llam-links.aux LHS _ _       Names []  NPF OL HD [llam T (app [LHS | NPF]) | OL] :- !,
-      std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
-      prune T Names,
-      var T HD _. 
+      prune T Names, var T HD _. 
     build-eta-llam-links.aux LHS SC (prod _ Ty _)       _    [X] []  OL HD [eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
       prune V SC, var (V X) HD _.
     build-eta-llam-links.aux LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
-    % TODO: unfold Ty if needed...
       std.append SC [X] SC',
       prune LHS' SC, build-eta-llam-links.aux (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
     build-eta-llam-links.aux LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
+      % Ty is expected to be of (forall x, ...), however, this can be hidden 
+      % under a definition to be unfolded. The unify-eq below is to perform the unfold
       Ty' = prod _ _ _, coq.unify-eq Ty Ty' ok, !,
       build-eta-llam-links.aux LHS SC Ty' Names PF NPF OL HD L.
     
@@ -73,7 +73,7 @@ namespace tc {
       :index (_ _ 1)
       pred may-contract-to i:list term, i:term, i:term.
       may-contract-to _ N N :- name N, !.
-      may-contract-to L N V :- var V _ S, !,
+      may-contract-to L N (uvar _ S) :- !,
           std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
       may-contract-to L N (app [N|A]) :-
         std.length A {std.length L},
@@ -81,14 +81,15 @@ namespace tc {
       may-contract-to L N (fun _ _ B) :-
         pi x\ may-contract-to [x|L] N (B x).
 
+      :index (_ 1)
       pred occurs-rigidly i:term, i:term.
       occurs-rigidly N N :- name N, !.
-      occurs-rigidly _ V :- var V, !, 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).
 
       pred maybe-eta-aux i:term, i:list term.
-      maybe-eta-aux V L :- var V _ S, std.forall L (std.mem! S).
+      maybe-eta-aux (uvar _ S) L :- std.forall L (std.mem! S).
       maybe-eta-aux (app [_|A]) L :-
         SplitLen is {std.length A} - {std.length L},
         split-at-not-fatal SplitLen A HD TL,
@@ -106,7 +107,7 @@ namespace tc {
       unify-left-right A A' :- A = A'.
 
       pred progress-eta-left i:term, o:term.
-      progress-eta-left A _ :- var A, !, fail.
+      progress-eta-left (uvar _) _ :- !, fail.
       progress-eta-left (fun _ _ A) (fun _ _ A).
       progress-eta-left A A' :- (name A; is-coq-term A), !, eta-expand A A'.
 
@@ -118,12 +119,6 @@ namespace tc {
       pred scope-check i:term, i:term.
       scope-check (uvar _ L) T :- prune A L, A = T, !.
 
-      pred collect-store o:list prop.
-      pred collect-store-aux i:list prop, o:list prop.
-
-      collect-store L :- collect-store-aux [] L.
-      collect-store-aux X L :- declare_constraint (collect-store-aux X L) [_].
-
       pred unify-eta i:term, i:term.
       % unify-eta A B :- coq.say "Unify-eta" "A"A"B"B, fail.
       unify-eta (uvar _ _ as A) B :- !, A = B, !.
@@ -132,33 +127,39 @@ namespace tc {
       unify-eta A B :- A = B.
 
       constraint eta solve-eta {
-        rule solve-eta \ (eta A B) <=> (unify-eta A B).
+        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)) 
-            | (pi x\ relocate L1 L2 (B2 x) (B2' x))  
+        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').
       }
 
-      pred eta i:term, i:term.
-      eta _ B :- var B, coq.error "[TC] link.eta error, flexible rhs".
-      eta A (fun _ _ B as T) :- not (var A), not (var B), !, unify-left-right A T. 
-      eta A B :- progress-eta-right B B', !, A = B'. 
-      eta A B :- progress-eta-left A A', !, A' = B.
-      eta A B :- scope-check A B, get-vars B Vars, declare_constraint (eta A B) [_,A|Vars].
+      :index (0 1)
+      pred eta i:term, i:term, i:list term.
+      eta _ uvar _ :- coq.error "[TC] link.eta error, flexible rhs".
+      eta A (fun _ _ B as T) _ :- not (var A), not (var B), !, unify-left-right A T.
+      eta A B _ :- progress-eta-right B B', !, A = B'. 
+      eta A B _ :- progress-eta-left A A', !, A' = B.
+      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'].
     }
 
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     % LLAM LINK                                                                %
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     namespace llam {
+      % A llam link is suspended on its lhs and the head of its rhs
+      % Note: to avoid not pf elpi variable, the coq term `app[A, x, t]` where
+      % A is a uvar, x a name and t a term, is represented with the llam rhs:
+      % 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 A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, 
-        declare_constraint (llam A (app [H|L])) [_,A|Vars].
-      llam (fun _ _ _ as F) (app [H | TL]) :- 
-        var H _ Scope, !, 
+      llam (uvar _ as A) (app [(uvar 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', 
           H = fun _ _Ty (x\ Bo'),  % TODO give a valid _Ty: should be: (Ty of dropped -> Ty of F)
           prune H' Scope,
@@ -177,6 +178,9 @@ namespace tc {
       }
     }
 
+    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+    % CS LINK                                                                  %
+    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     namespace cs {
       pred reduce-cs i:term, i:term, i:term, i:constant.
       reduce-cs V (app [ProjT, T]) Record Proj :-
@@ -216,8 +220,12 @@ namespace tc {
       }
     }
 
-    pred eta i:term, o:term.
-    eta A B :- eta.eta A B.
+    % The last argument contain the list of vars on which the link is
+    % suspended. In order to avoid a call to get-vars if the link is to be 
+    % re-suspended, we explicetely pass this list once when the link is 
+    % created
+    pred eta i:term, i:term.
+    eta A B :- !, get-vars B V, eta.eta A B [A|V].
 
     pred solve-eta.
     solve-eta :- declare_constraint solve-eta [_].

From a59eca0f4909070624e56194f35061ef194d559b Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Mon, 2 Sep 2024 11:14:17 +0200
Subject: [PATCH 21/32] [TC] clean link code + unification with cs links only
 after a call to tc.compile.

---
 apps/tc/elpi/link.elpi                       | 27 ++++++++++----------
 apps/tc/tests/importOrder/sameOrderCommand.v |  2 ++
 apps/tc/theories/add_commands.v              |  5 ++--
 apps/tc/theories/tc.v                        |  2 +-
 src/coq_elpi_vernacular.ml                   |  4 +--
 5 files changed, 22 insertions(+), 18 deletions(-)

diff --git a/apps/tc/elpi/link.elpi b/apps/tc/elpi/link.elpi
index 24e52f636..a1dc97138 100644
--- a/apps/tc/elpi/link.elpi
+++ b/apps/tc/elpi/link.elpi
@@ -67,8 +67,7 @@ namespace tc {
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     namespace eta {
       pred eta-expand i:term, o:term.  
-      eta-expand T1 (fun _ _ B) :- (name T1; is-coq-term T1), !, pi x\ coq.mk-app T1 [x] (B x). 
-      eta-expand T1 (fun _ _ R) :- pi x\ name (R x) T1 [x].
+      eta-expand T1 (fun _ _ B) :- pi x\ coq.mk-app T1 [x] (B x). 
 
       :index (_ _ 1)
       pred may-contract-to i:list term, i:term, i:term.
@@ -107,14 +106,12 @@ namespace tc {
       unify-left-right A A' :- A = A'.
 
       pred progress-eta-left i:term, o:term.
-      progress-eta-left (uvar _) _ :- !, fail.
-      progress-eta-left (fun _ _ A) (fun _ _ A).
-      progress-eta-left A A' :- (name A; is-coq-term A), !, eta-expand A A'.
+      progress-eta-left (fun _ _ _ as A) B :- !, A = B.
+      progress-eta-left A B :- eta-expand A A', !, A' = B.
 
-      pred progress-eta-right i:term, o:term.
-      progress-eta-right (fun _ _ B as T) T :- pi x\ var (B x), !, fail.
-      progress-eta-right A A' :- coq.reduction.eta-contract A A', not (A = A'), !.
-      progress-eta-right A A :- not (maybe-eta A), !.
+      pred progress-eta-right? i:term, o:term.
+      progress-eta-right? A A' :- coq.reduction.eta-contract A A', not (A = A'), !.
+      progress-eta-right? A A :- not (maybe-eta A), !.
 
       pred scope-check i:term, i:term.
       scope-check (uvar _ L) T :- prune A L, A = T, !.
@@ -140,8 +137,8 @@ namespace tc {
       pred eta i:term, i:term, i:list term.
       eta _ uvar _ :- coq.error "[TC] link.eta error, flexible rhs".
       eta A (fun _ _ B as T) _ :- not (var A), not (var B), !, unify-left-right A T.
-      eta A B _ :- progress-eta-right B B', !, A = B'. 
-      eta A B _ :- progress-eta-left A A', !, A' = B.
+      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 :- 
         scope-check A B, std.filter Vars (x\ var x) Vars', 
         declare_constraint (eta A B Vars') [_,A|Vars'].
@@ -199,10 +196,14 @@ namespace tc {
         tc.coercion-unify HD, !, 
         get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
 
-      cs (uvar _ as V) (app [HD | _] 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)
-          (coq.unify-eq V T ok), !.
+          % Note: Below we cannot unify V and T since T may contain
+          %       deep projections which must be considered as problematic terms
+          %       To avoid the problem, we compile all subterms in TL, the probl
+          %       subterms are replaced with variables put into links
+          (tc.compile.goal (app TL) (app TL') Links, do Links, V = app [HD|TL']), !.
       cs T1 T2 :- not (T2 = app _), !, coq.unify-eq T1 T2 ok.
 
       pred unify-under-ctx i:list term, i:list term, i:term, i:term, i:term, i:term.
diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v
index c088da84f..ebb15c982 100644
--- a/apps/tc/tests/importOrder/sameOrderCommand.v
+++ b/apps/tc/tests/importOrder/sameOrderCommand.v
@@ -5,6 +5,7 @@ From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
 From elpi.apps.tc.elpi Extra Dependency "tc_same_order.elpi" as tc_same_order.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
+From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 
 Set Warnings "+elpi".
 Elpi Command SameOrderImport.
@@ -14,6 +15,7 @@ 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 tc_same_order.
 Elpi Typecheck.
 
diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index d9060725f..3d6f5d54c 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -7,6 +7,7 @@ From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc.elpi Extra Dependency "compile_instance.elpi" as compile_instance.
 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 "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.
@@ -21,7 +22,7 @@ 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.
+Elpi Accumulate File compile_instance compiler compile_goal.
 Elpi Accumulate lp:{{  
   main L :- 
     args->str-list L L1,
@@ -34,7 +35,7 @@ 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.
+Elpi Accumulate File compile_instance compiler compile_goal.
 Elpi Accumulate File parser_addInstances.
 Elpi Accumulate lp:{{
   main Arguments :- 
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 761ced06d..22e734a90 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -77,7 +77,7 @@ 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.
+Elpi Accumulate File compile_instance compiler compile_goal.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
 
diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index 91caa85d7..fc1cba021 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -191,8 +191,8 @@ let get_and_compile ?even_if_empty name : (EC.program * bool) option =
       | Program { raw_args } -> raw_args
       | Tactic -> true in
       (prog, raw_args)) in
-    Coq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: get_and_compile %1.4f" (Unix.gettimeofday () -. t))));
-    res
+  Coq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: get_and_compile %1.4f" (Unix.gettimeofday () -. t))));
+  res
 
 [%%if coq = "8.20"]
 let feedback_error loc ei = Feedback.(feedback (Message(Error,loc,CErrors.iprint ei)))

From 02dc4cbd990180995c063d6d35ddc4aca4aea846 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 3 Sep 2024 11:34:10 +0200
Subject: [PATCH 22/32] add _opam to .gitignore

---
 .gitignore | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index df9c20014..952b6282c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -55,4 +55,5 @@ _build
 tmp.out
 coq-elpi-tests.opam
 coq-elpi-tests.install
-coq-elpi.install
\ No newline at end of file
+coq-elpi.install
+_opam

From 9b149b4b65a8784d6168ac95a00690e636af9f5d Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 3 Sep 2024 11:35:17 +0200
Subject: [PATCH 23/32] [TC] clearn-term on pi-decl in decompile-term-aux

---
 apps/tc/elpi/compile_instance.elpi | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/apps/tc/elpi/compile_instance.elpi b/apps/tc/elpi/compile_instance.elpi
index a06857943..9ba9af8f1 100644
--- a/apps/tc/elpi/compile_instance.elpi
+++ b/apps/tc/elpi/compile_instance.elpi
@@ -1,6 +1,16 @@
 namespace tc {
   shorten tc.{r-ar, range-arity}.
 
+  % TODO: also replace (sort (typ X)) and (pglobal _ X) with holes in the place of X
+  pred clean-term i:term, o:term.
+  clean-term A B :-
+    (pi t s r \ copy (tc.maybe-eta-tm  t s) r :- !, copy t r, !) =>
+    (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".
+
   namespace precomp {
 
     namespace instance {
@@ -245,13 +255,13 @@ namespace tc {
 
         decompile-term-aux (fun Name Ty Bo) (pr XS L) (fun Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
-          close-prop-no-prune-pi-decl L1x Ty L1,
+          close-prop-no-prune-pi-decl L1x {clean-term Ty} L1,
           decompile-term-aux Ty (pr XS1 L) Ty' (pr XS2 L2),
           std.append L1 L2 L3.
 
         decompile-term-aux (prod Name Ty Bo) (pr XS L) (prod Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
-          close-prop-no-prune-pi-decl L1x Ty L1,
+          close-prop-no-prune-pi-decl L1x {clean-term Ty} L1,
           decompile-term-aux Ty (pr XS1 L) Ty' (pr XS2 L2),
           std.append L1 L2 L3.
 
@@ -278,16 +288,6 @@ namespace tc {
 
       }
 
-      % TODO: also replace (sort (typ X)) and (pglobal _ X) with holes in the place of X
-      pred clean-term i:term, o:term.
-      clean-term A B :-
-        (pi t s r \ copy (tc.maybe-eta-tm  t s) r :- !, copy t r, !) =>
-        (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 
         i:nat,                % the number of problematic terms
         i:term,               % the type of the instance

From 568fc98d914ccea09ab022bc6cd798ca5120c569 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 19 Sep 2024 16:05:46 +0200
Subject: [PATCH 24/32] [TC] dummy clauses are local to sections

This aims to solve the compilation error produced by the compilation of

```
Module foo.
  Class B (i : nat).

  Section s.
    (* Class with coercion depending on section parameters *)
    Context (A : Type).
    Class C (i : A) : Set := {
      x (x : A) :: B 3
    }.
  End s.
End foo.
```
---
 apps/tc/theories/tc.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 22e734a90..998db8083 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -89,10 +89,11 @@ Elpi Accumulate lp:{{
       Class Bird := IsAnimal :> Animal.
     ```
     The instance IsAnimal of type Bird -> Animal, is compiled before the
-    predicate for Bird; hence, Bird is not recognize as a premise of IsAnimal.
+    predicate for Bird; hence, it is not possible to add the premise
+    tc-Bird for the IsAnimal instance...
     This problem is due to the order in which the registers for Instance and
     Class creation are run.
-    The solution is to do the following two jobs when a class C is created:
+    The solution is to do the following jobs when a class C is created:
       1: for every projection P of C, if P is a coercion, the wrongly 
         compiled instance is replaced with a `dummy` clause.
       2: the predicate for the class is created

From 9fe73be2f961f7223f5ed60eaed3c27731501ee1 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 25 Sep 2024 16:12:59 +0200
Subject: [PATCH 25/32] [TC] add comment

---
 apps/tc/elpi/compile_goal.elpi | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
index 340c76f60..0abf16517 100644
--- a/apps/tc/elpi/compile_goal.elpi
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -111,6 +111,9 @@ namespace tc {
       compile-full Goal Goal' Links :- compile-full-aux Goal [] Goal' Links.
     }
 
+    % [goal T T' L] takes a term T and returns a new term T' where problematic
+    % subterms (see this: https://dl.acm.org/doi/10.1145/3678232.3678233)
+    % are replaced with fresh variables. The list of links is L
     pred goal i:term, o:term, o:list prop.
     :name "compile-goal"
     goal Goal Goal' Links :- 

From 459da6e3da5be18cda8559f08ceead3ccad044b2 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 25 Sep 2024 16:13:34 +0200
Subject: [PATCH 26/32] [TC] move time-is-active and coercion-unify in db.v

---
 apps/tc/elpi/tc_aux.elpi | 4 ----
 apps/tc/theories/db.v    | 5 +++++
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index 1b90f7b6c..104660e88 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -174,7 +174,6 @@ namespace tc {
   section-var->decl L :-
     section-var->decl.aux {coq.env.section} L.
 
-  pred time-is-active i:(list string -> prop).
   :name "time-is-active"
   time-is-active _ :- coq.option.get ["Time", "TC", "Bench"] (coq.option.bool tt), !.
   time-is-active Opt :- tc.is-option-active Opt. 
@@ -221,9 +220,6 @@ namespace tc {
     int ->
     term.
 
-  :index (5)
-  pred coercion-unify i:term.
-
   type coercion
     term ->
     list term ->
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index 6fb9948b3..90618d9e2 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -102,5 +102,10 @@ Elpi Db tc.db lp:{{
 
     % relates a projection to the its record
     pred proj->record i:constant, o:term.
+    
+    :index (5)
+    pred coercion-unify i:term.
+
+    pred time-is-active i:(list string -> prop).
   }
 }}.

From 711ff60ab576fc2d27a1dc323b984a5265fcead4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 2 Oct 2024 13:05:50 +0200
Subject: [PATCH 27/32] cleanup

---
 _opam | 1 -
 1 file changed, 1 deletion(-)
 delete mode 120000 _opam

diff --git a/_opam b/_opam
deleted file mode 120000
index 343b677d2..000000000
--- a/_opam
+++ /dev/null
@@ -1 +0,0 @@
-/home/dfissore/Documents/github/COQ_ELPI_DEV/_opam
\ No newline at end of file

From 279e3218891bf71242d66cdd858b6d177f7840f5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 2 Oct 2024 13:06:23 +0200
Subject: [PATCH 28/32] cleanup

---
 .gitignore | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 952b6282c..0d053adbd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -56,4 +56,3 @@ tmp.out
 coq-elpi-tests.opam
 coq-elpi-tests.install
 coq-elpi.install
-_opam

From 2f03fa823834329b679b213123fa958f0f48da7f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 2 Oct 2024 13:14:13 +0200
Subject: [PATCH 29/32] cleanup

---
 apps/tc/theories/db.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index 90618d9e2..94497ced2 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -100,7 +100,8 @@ Elpi Db tc.db lp:{{
 
     pred ho-link o:term, i:term, o:A.
 
-    % relates a projection to the its record
+    % 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}})
     pred proj->record i:constant, o:term.
     
     :index (5)

From 7986110a42524dfc8d05e238c04276b497e71b72 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 2 Oct 2024 13:16:47 +0200
Subject: [PATCH 30/32] cleanup

---
 apps/tc/theories/db.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index 94497ced2..ca3c94dba 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -102,11 +102,15 @@ Elpi Db tc.db lp:{{
 
     % 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}})
+    % MANUALLY INSERTED by TC.AddRecordFields
     pred proj->record i:constant, o:term.
     
+    % tells if a term is a coercion
+    % MANUALLY INSERTED by Elpi Accumulate
     :index (5)
     pred coercion-unify i:term.
 
+    % Used to print bench infos
     pred time-is-active i:(list string -> prop).
   }
 }}.

From eb81aa4c7ccd6c2e6ffcc62c6ca321a2009bc9ec Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 2 Oct 2024 13:28:50 +0200
Subject: [PATCH 31/32] ci

---
 .github/workflows/doc.yml  | 4 +++-
 .github/workflows/main.yml | 4 +++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml
index 958a3fd30..706ec0015 100644
--- a/.github/workflows/doc.yml
+++ b/.github/workflows/doc.yml
@@ -9,7 +9,9 @@ on:
     branches: [ master ]
   pull_request:
     branches: [ master ]
-
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 jobs:
   build:
     name: Build doc
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 609b027bf..88fab1ef1 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -20,7 +20,9 @@ on:
         options:
         - released
         - extra-dev
-
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 env:
   OPAM_SUITE: ${{ inputs.suite }}
 

From 5ac62d2129ca191e2732bb5ca213c5e511736f17 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 2 Oct 2024 13:35:33 +0200
Subject: [PATCH 32/32] nix

---
 .github/workflows/nix-action-coq-8.20.yml | 122 ++++++++++++++++++++++
 .nix/config.nix                           |   2 +-
 .nix/coq-nix-toolbox.nix                  |   2 +-
 3 files changed, 124 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/nix-action-coq-8.20.yml b/.github/workflows/nix-action-coq-8.20.yml
index b40e380e4..ca320c749 100644
--- a/.github/workflows/nix-action-coq-8.20.yml
+++ b/.github/workflows/nix-action-coq-8.20.yml
@@ -1,4 +1,126 @@
 jobs:
+  QuickChick:
+    needs:
+    - coq
+    - mathcomp-ssreflect
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
+        \ }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
+        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
+        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
+        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
+        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v27
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq-elpi
+      uses: cachix/cachix-action@v15
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, coq-community, math-comp
+        name: coq-elpi
+    - id: stepCheck
+      name: Checking presence of CI target QuickChick
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-8.20\" --argstr job \"QuickChick\" \\\n   --dry-run 2>&1 >\
+        \ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\
+        \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
+        --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
+        --argstr job "mathcomp-ssreflect"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq-ext-lib'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
+        --argstr job "coq-ext-lib"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: simple-io'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
+        --argstr job "simple-io"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: Building/fetching current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
+        --argstr job "QuickChick"
+  autosubst:
+    needs:
+    - coq
+    - mathcomp-ssreflect
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
+        \ }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
+        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
+        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
+        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
+        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v27
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq-elpi
+      uses: cachix/cachix-action@v15
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, coq-community, math-comp
+        name: coq-elpi
+    - id: stepCheck
+      name: Checking presence of CI target autosubst
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-8.20\" --argstr job \"autosubst\" \\\n   --dry-run 2>&1 > /dev/null)\n\
+        echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
+        s/.*/built/\") >> $GITHUB_OUTPUT\n"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
+        --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
+        --argstr job "mathcomp-ssreflect"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: Building/fetching current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
+        --argstr job "autosubst"
   coq:
     needs: []
     runs-on: ubuntu-latest
diff --git a/.nix/config.nix b/.nix/config.nix
index c77e3a2e1..a65fde6e2 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -52,7 +52,7 @@ let master = [
       ocamlPackages = {
         # when updating this, don't forget to update dune-project
         # then use it to regenerate coq-elpi.opam
-        elpi.override.version = "v1.18.2";
+        elpi.override.version = "v1.19.5";
       };
     };
 
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
index 9b872206b..657441985 100644
--- a/.nix/coq-nix-toolbox.nix
+++ b/.nix/coq-nix-toolbox.nix
@@ -1 +1 @@
-"24e96b4870378d5e87fd2d0dd46405b471c286ab"
+"42eecc8a0f642b84bd179859d708ddc710c92004"