[TC] clean link code + unification with cs links only after a call to tc.compile.

Author: FissoreD

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.

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.
 

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 :- 

apps/tc/theories/tc.v

@@ -74,7 +74,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:{{
 

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.19" || coq = "8.20"]
 let feedback_error loc ei = Feedback.(feedback (Message(Error,loc,CErrors.iprint ei)))