TC Solver: prim-proj and canonical struct

.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

.github/workflows/release.yml

@@ -22,7 +22,9 @@ on:
         options:
         - released
         - extra-dev
-
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 env:
   OPAM_SUITE: ${{ inputs.suite }}
 

.gitignore

@@ -57,5 +57,7 @@ rocq-elpi-tests.opam
 rocq-elpi-tests.install
 rocq-elpi.install
 coq-elpi.install
+_opam
+
 
 theories-stdlib/dune

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/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:any.
@@ -142,24 +145,13 @@ 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-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 :-
+  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.

apps/tc/elpi/compile_goal.elpi

@@ -0,0 +1,122 @@
+namespace tc {
+  namespace compile {
+    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 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-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.
+      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 `_` 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'.
+
+      % TODO: to avoid too many chain for the same var, maybe pass a list into the fold
+      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.
+
+      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.
+    }
+
+    % [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 :- 
+      goal.compile-full-aux Goal [] Goal' Links.
+  }
+}