[TC] add TC.AddRecordFields command + better chr for canon struct

Author: FissoreD

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.
 

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.

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

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.
 
 }

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.

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].

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.

apps/tc/theories/db.v

@@ -98,5 +98,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.
   }
 }}.