diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml index e80a9b629..6c54098d2 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/release.yml b/.github/workflows/release.yml index c212889c0..52d84898f 100644 --- a/.github/workflows/release.yml +++ b/.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 }} diff --git a/.gitignore b/.gitignore index 1a1d6e358..44b205805 100644 --- a/.gitignore +++ b/.gitignore @@ -57,5 +57,7 @@ rocq-elpi-tests.opam rocq-elpi-tests.install rocq-elpi.install coq-elpi.install +_opam + theories-stdlib/dune diff --git a/apps/cs/README.md b/apps/cs/README.md index 7c3679444..4693b7d93 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/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 b0df94dca..85a1c6047 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: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. \ 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..0053d84c0 --- /dev/null +++ b/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. + } +} diff --git a/apps/tc/elpi/compile_instance.elpi b/apps/tc/elpi/compile_instance.elpi new file mode 100644 index 000000000..1d4448345 --- /dev/null +++ b/apps/tc/elpi/compile_instance.elpi @@ -0,0 +1,479 @@ +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 { + % 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, % Positive or negaive position of the term being pre-compiled + i:term, % Term being explored + i:nat, % Number of pi to quantified accumulated + o:term, % Precompiled term: problematic sub-terms are tagged with custom constructors + o:nat. % Final number of pi to quantify + 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) :- + 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. + + % 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 { + pred is-name o:term. + pred is-uvar o:term. + + % [name-pair H0 Hn Ar] + % the variable H0 (applied 0 time) is associated to the variable Hn which is + % applied Ar times. + pred name-pair o:term, o:term, o:nat. + + namespace decompile { + + pred decompile-term-aux i:term, i:pair (list term) (list prop), o:term, o:pair (list term) (list prop). + + decompile-term-aux X A Y A :- name X, !, X = Y, !. % avoid loading "decompile-term-aux x A x A" at binders + decompile-term-aux (global _ as C) A C A :- !. + 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.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 = 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]) :- !, + name Y X S, + decompile-term-aux T (pr XS L1) T' (pr XS' L2), + NL = tc.link.eta Y T'. + + decompile-term-aux (tc.prod-range T _) A T' A' :- !, + decompile-term-aux T A T' A'. + + % Maybe-llam when H is a coq unif variable quantified in the instance type + % In the following instance, X is a HO variable applied to a constant (not a name) + % Instance i : forall (X : T1 -> T2) (a : T1), c (X a). + decompile-term-aux (tc.maybe-llam-tm (app[app[H | PF] | NPF]) S) (pr [X|XS] L1) Y (pr XS' [NL | L2]) :- + not (var H), !, % is-uvar H, holds + name Y X S, + length-nat PF Len, + std.assert!(name-pair H V Len) "[TC] fail to find name-pair", + name Hd V PF, + std.fold-map NPF (pr XS L1) decompile-term-aux Tl (pr XS' L2), + NL = tc.link.llam Y (app [Hd|Tl]). + + % 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))), + 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 {clean-term Ty} L1, + decompile-term-aux Ty (pr XS1 L) Ty' (pr XS2 L2), + std.append L1 L2 L3. + + % HO var when H is a quantified variable in the instance type being in PF + % Example: Instance i: forall (X : T1 -> T2), (forall a, c1 (X a)) -> c2. + % Note: X is the HO var taken into account which is applied to the list of + % distinct_names [a] + decompile-term-aux (app [H|L]) N R N :- + is-uvar H, + std.forall L is-name, % Not needed, since precompile does this check + distinct_names L, !, % Not needed, since precompile does this check + length-nat L Len, + std.assert! (name-pair H V Len) "[TC] name-pair not found", + name R V L. + + decompile-term-aux (app L) PR (app L') PR' :- !, + std.fold-map L PR decompile-term-aux L' PR'. + + decompile-term-aux A B _ _ :- coq.error "[TC] cannot decompile-term-aux of" A B. + + pred decompile-term i:list term, o:list term, i:term, o:term, o:list prop. + decompile-term L L' T R Links :- + decompile-term-aux T (pr L []) R (pr L' Links). + + } + + pred main + i:nat, % the number of problematic terms + i:term, % the type of the instance + i:term, % the global gref of the instance + i:list univ, % the list of univ variable to be replaced with elpi fresh vars + i:list univ-instance, % the list of univ-instance to be replaced with elpi fresh vars + o:prop. % the compiled clause for the instance + + main N Ty ProofHd [] [] Clause :- + add-pi-problematic-terms N [] Ty ProofHd Clause. + main N Ty ProofHd [Univ | UnivL] UnivInstL (pi x\ Clause x) :- !, + pi x\ (copy (sort (typ Univ)) (sort (typ x)) :- !) => + main N Ty ProofHd UnivL UnivInstL (Clause x). + main N Ty ProofHd [] [UnivInst | UnivInstL] (pi x\ Clause x) :- !, + pi x\ (copy (pglobal A UnivInst) (pglobal A x) :- !) => + main N Ty ProofHd [] UnivInstL (Clause x). + + + % Start to charge the right number of pi for the resulting clause: + % This number is equal to the number of problematic terms + number of subterms with shape `sort _` and `pglobal _ _` + pred add-pi-problematic-terms + i:nat, % the number of pi to quantify + i:list term, % the list of quantified pi + i:term, % the fuel of the compilation (the type of the instance) + i:term, % the global gref of the current instance + o:prop. % the compiled clause for the instance + + add-pi-problematic-terms z L Ty ProofHd Clause :- + compile-ty L _ ProofHd tt Ty [] [] Clause. + add-pi-problematic-terms (s N) L Ty ProofHd (pi x\ Clause x) :- + pi x\ is-uvar x => add-pi-problematic-terms N [x|L] Ty ProofHd (Clause x). + + % Builds a eta link between the varibale A whose type _must_ be of type `prod` + % A is linked with B : A =_eta (fun (x : Ty) => B_x) + pred make-eta-link-aux + i:term, % A : The variable to eta-expand + i:term, % prod _ Ty Bo : The type of A + i:pair term name, % pr B Bn : The eta-expanded version of B with its name (they are fresh names) + i:list term, % L : The list of name in the scope of A and B + 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 :- !, + clean-term Ty Ty', + name A' A {std.rev L}, + 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 :- !, + make-eta-link-aux A Prod BN L Link Ty' Bo. + % The type of a higher order variable can be hidden behind a definition + % In this case we unfold this definition to get the prod constructor + make-eta-link-aux A T BN L Link Ty' Bo :- + coq.safe-dest-app T Hd Ag, + (@redflags! coq.redflags.delta => coq.reduction.lazy.whd Hd Hd'), + not (Hd = Hd'), !, + coq.mk-app Hd' Ag TT', + make-eta-link-aux A TT' BN L Link Ty' Bo. + make-eta-link-aux _ T _ _ _ _ _ :- coq.error "[TC] make-eta-link-aux of" T. + + % Create spine of eta-links + pred make-eta-link i:term, i:term, i:list (pair term name), i:list term, i:list prop, o:prop. + make-eta-link P PTy [Hd] L Links (do [Link1|Links]) :- !, + make-eta-link-aux P PTy Hd L Link1 _ _. + make-eta-link P PTy [(pr B _ as Hd)|Tl] L Links (pi x\ decl x `x` PTy' => Res x) :- !, + make-eta-link-aux P PTy Hd L Link1 PTy' Bo, + pi x\ make-eta-link B (Bo x) Tl [x|L] [Link1|Links] (Res x). + make-eta-link P PTy _ _ _ _ :- coq.error "[TC] make-eta-link error : empty list of pairs" P PTy. + + % Accumulates pi for eta-links + pred add-link-eta-dedup + i:(list prop -> prop -> prop), + i:range-arity, i:term, i:term, i:(list (pair term name)), i:list prop, o:prop. + % Base case when the variable is always used at same arity + add-link-eta-dedup F (r-ar _ z) _ _ [] PremR Clause :- !, + F PremR Clause. + add-link-eta-dedup F (r-ar _ z) P Pty Acc PremR Clause :- !, + make-eta-link P Pty Acc [] [] LinkEtaDedup, + F [LinkEtaDedup|PremR] Clause. + add-link-eta-dedup F (r-ar M (s N)) P PTy Acc PremR (pi x y\ Clause x y) :- !, + 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, % List of pi-quantified vars to consume + o:list term, % List of remaining pi-quantified variables + i:term, % (Local) Name of the proof of the premise + i:term, % Type of the local premise being consumed by compile-ty + i:term, % Name of the instance being compiled (global {{:gref InstName}}) + i:bool, % Positive or negative position of the term + i:term, % Type of InstName to compile + i:list term, % List of the name of all local proofs + i:list prop, % List of premises to add to the fianal clause + o:prop. % The final 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, + 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, % List of pi-quantified vars to consume + o:list term, % List of remaining pi-quantified variables + i:term, % Name of the instance being compiled (global {{:gref InstName}}) + i:bool, % Positive or negative position of the term + i:term, % Type of InstName to compile + i:list term, % List of the name of all local proofs + i:list prop, % List of premises to add to the fianal clause + o:prop. % The final 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|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 ProofArgsR PremR Clause :- + std.do![ + 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 links + i:list prop, % the premises + o:prop. % the compiled clause for the instance + + 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 Links Premises (do Links, Clause) :- + tc.make-tc Goal Proof Premises ff Clause. + + pred context i:goal-ctx, o:list prop. + context [] []. + context [X | Xs] [Clause | ResTl] :- + (decl Var _ Ty = X; def Var _ Ty _ = X), + tc.is-instance-term Ty, !, + std.assert! (compile.instance Ty Var Clause) "[TC] cannot compile instance of context", + context Xs ResTl. + context [_ | Tl] L :- context Tl L. + } + + % build a list of Clauses of type tc to be temporarly added to the + % database, used in theorems having assumptions. + pred context i:goal-ctx, o:list prop. + :name "tc-compile-context" + context Ctx Clauses :- + std.assert! (instance.context Ctx Clauses) "[TC] cannot compile context". + + pred instance i:term, i:term, o:prop. + instance Ty ProofHd Clause :- + tc.time-it tc.oTC-time-compile-instance ( + tc.normalize-ty Ty Ty', + tc.precomp.instance Ty' Ty'' N UnivConst UnivInst, + instance.main N Ty'' ProofHd UnivConst UnivInst Clause + ) "Compile Instance". + + pred instance-gr i:gref, o:prop. + % 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\ instance Ty (pglobal InstGR x) (Clause x). + instance-gr InstGR Clause :- + coq.env.typeof InstGR Ty, + instance Ty (global InstGR) Clause. + } +} \ No newline at end of file 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_compile.elpi b/apps/tc/elpi/ho_compile.elpi deleted file mode 100644 index fd6b6f599..000000000 --- a/apps/tc/elpi/ho_compile.elpi +++ /dev/null @@ -1,407 +0,0 @@ -namespace tc { - shorten tc.{r-ar, range-arity}. - - namespace compile { - - namespace instance { - pred is-name o:term. - pred is-uvar o:term. - - % [name-pair H0 Hn Ar] - % the variable H0 (applied 0 time) is associated to the variable Hn which is - % 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). - - decompile-term-aux X A Y A :- name X, !, X = Y, !. % avoid loading "decompile-term-aux x A x A" at binders - decompile-term-aux (global _ as C) A C A :- !. - 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 P) L P L :- !. - - decompile-term-aux (tc.maybe-eta-tm T S) (pr [X|XS] L1) Y (pr XS' [NL | L2]) :- !, - name Y X S, - decompile-term-aux T (pr XS L1) T' (pr XS' L2), - NL = tc.link.eta Y T'. - - decompile-term-aux (tc.prod-range T _) A T' A' :- !, - decompile-term-aux T A T' A'. - - % Maybe-llam when H is a coq unif variable quantified in the instance type - % In the following instance, X is a HO variable applied to a constant (not a name) - % Instance i : forall (X : T1 -> T2) (a : T1), c (X a). - decompile-term-aux (tc.maybe-llam-tm (app[app[H | PF] | NPF]) S) (pr [X|XS] L1) Y (pr XS' [NL | L2]) :- - not (var H), !, % is-uvar H, holds - name Y X S, - length-nat PF Len, - std.assert!(name-pair H V Len) "[TC] fail to find name-pair", - name Hd V PF, - 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[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 (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, - 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, - decompile-term-aux Ty (pr XS1 L) Ty' (pr XS2 L2), - std.append L1 L2 L3. - - % HO var when H is a quantified variable in the instance type being in PF - % Example: Instance i: forall (X : T1 -> T2), (forall a, c1 (X a)) -> c2. - % Note: X is the HO var taken into account which is applied to the list of - % distinct_names [a] - decompile-term-aux (app [H|L]) N R N :- - is-uvar H, - std.forall L is-name, % Not needed, since precompile does this check - distinct_names L, !, % Not needed, since precompile does this check - length-nat L Len, - 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'. - - decompile-term-aux A B _ _ :- coq.error "[TC] cannot decompile-term-aux of" A B. - - pred decompile-term i:list term, o:list term, i:term, o:term, o:list prop. - decompile-term L L' T R Links :- - decompile-term-aux T (pr L []) R (pr L' Links). - - } - - % 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.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". - - pred main - i:nat, % the number of problematic terms - i:term, % the type of the instance - i:term, % the global gref of the instance - i:list univ, % the list of univ variable to be replaced with elpi fresh vars - i:list univ-instance, % the list of univ-instance to be replaced with elpi fresh vars - o:prop. % the compiled clause for the instance - - main N Ty ProofHd [] [] Clause :- - add-pi-problematic-terms N [] Ty ProofHd Clause. - main N Ty ProofHd [Univ | UnivL] UnivInstL (pi x\ Clause x) :- !, - pi x\ (copy (sort (typ Univ)) (sort (typ x)) :- !) => - main N Ty ProofHd UnivL UnivInstL (Clause x). - main N Ty ProofHd [] [UnivInst | UnivInstL] (pi x\ Clause x) :- !, - pi x\ (copy (pglobal A UnivInst) (pglobal A x) :- !) => - main N Ty ProofHd [] UnivInstL (Clause x). - - - % Start to charge the right number of pi for the resulting clause: - % This number is equal to the number of problematic terms + number of subterms with shape `sort _` and `pglobal _ _` - pred add-pi-problematic-terms - i:nat, % the number of pi to quantify - i:list term, % the list of quantified pi - i:term, % the fuel of the compilation (the type of the instance) - i:term, % the global gref of the current instance - o:prop. % the compiled clause for the instance - - add-pi-problematic-terms z L Ty ProofHd Clause :- - compile-ty L _ ProofHd tt Ty [] [] Clause. - add-pi-problematic-terms (s N) L Ty ProofHd (pi x\ Clause x) :- - pi x\ is-uvar x => add-pi-problematic-terms N [x|L] Ty ProofHd (Clause x). - - % Builds a eta link between the varibale A whose type _must_ be of type `prod` - % A is linked with B : A =_eta (fun (x : Ty) => B_x) - pred make-eta-link-aux - i:term, % A : The variable to eta-expand - i:term, % prod _ Ty Bo : The type of A - i:pair term name, % pr B Bn : The eta-expanded version of B with its name (they are fresh names) - i:list term, % L : The list of name in the scope of A and B - 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 :- !, - clean-term Ty Ty', - name A' A {std.rev L}, - Link = tc.link.eta A' (fun Name 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 :- !, - make-eta-link-aux A Prod BN L Link Ty' Bo. - % The type of a higher order variable can be hidden behind a definition - % In this case we unfold this definition to get the prod constructor - make-eta-link-aux A T BN L Link Ty' Bo :- - coq.safe-dest-app T Hd Ag, - (@redflags! coq.redflags.delta => coq.reduction.lazy.whd Hd Hd'), - not (Hd = Hd'), !, - coq.mk-app Hd' Ag TT', - make-eta-link-aux A TT' BN L Link Ty' Bo. - make-eta-link-aux _ T _ _ _ _ _ :- coq.error "[TC] make-eta-link-aux of" T. - - % Create spine of eta-links - pred make-eta-link i:term, i:term, i:list (pair term name), i:list term, i:list prop, o:prop. - make-eta-link P PTy [Hd] L Links (do [Link1|Links]) :- !, - make-eta-link-aux P PTy Hd L Link1 _ _. - make-eta-link P PTy [(pr B _ as Hd)|Tl] L Links (pi x\ decl x `x` PTy' => Res x) :- !, - make-eta-link-aux P PTy Hd L Link1 PTy' Bo, - pi x\ make-eta-link B (Bo x) Tl [x|L] [Link1|Links] (Res x). - make-eta-link P PTy _ _ _ _ :- coq.error "[TC] make-eta-link error : empty list of pairs" P PTy. - - % Accumulates pi for eta-links - pred add-link-eta-dedup - i:(list prop -> prop -> prop), - i:range-arity, i:term, i:term, i:(list (pair term name)), i:list prop, o:prop. - % Base case when the variable is always used at same arity - add-link-eta-dedup F (r-ar _ z) _ _ [] PremR Clause :- !, - F PremR Clause. - add-link-eta-dedup F (r-ar _ z) P Pty Acc PremR Clause :- !, - make-eta-link P Pty Acc [] [] LinkEtaDedup, - F [LinkEtaDedup|PremR] Clause. - add-link-eta-dedup F (r-ar M (s N)) P PTy Acc PremR (pi x y\ Clause x y) :- !, - 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 compile-premise - i:list term, - o:list term, - i:term, - i:term, - i:term, - i:bool, - i:term, - i:list term, - i:list prop, - o:prop. - compile-premise L L2 P PTy ProofHd IsPositive ITy ProofTlR 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. - - pred compile-ty - i:list term, - i:list term, - i:term, - i:bool, - i:term, - 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 :- !, - 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], - 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 :- - 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 - ]. - - 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 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, - 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). - - pred context i:goal-ctx, o:list prop. - context [] []. - context [X | Xs] [Clause | ResTl] :- - (decl Var _ Ty = X; def Var _ Ty _ = X), - tc.is-instance-term Ty, !, - std.assert! (compile.instance Ty Var Clause) "[TC] cannot compile instance of context", - context Xs ResTl. - context [_ | Tl] L :- context Tl L. - } - - % build a list of Clauses of type tc to be temporarly added to the - % database, used in theorems having assumptions. - pred context i:goal-ctx, o:list prop. - :name "tc-compile-context" - context Ctx Clauses :- - std.assert! (instance.context Ctx Clauses) "[TC] cannot compile context". - - pred instance i:term, i:term, o:prop. - instance Ty ProofHd Clause :- - tc.time-it tc.oTC-time-compile-instance ( - tc.normalize-ty Ty Ty', - tc.precomp.instance Ty' Ty'' N UnivConst UnivInst, - instance.main N Ty'' ProofHd UnivConst UnivInst Clause - ) "Compile Instance". - - pred instance-gr i:gref, o:prop. - % 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). - 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 (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. - 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'] :- !, - prune Z Sc, - get-uva-pair-arity H S Y, - std.fold-map NPF L fold-map 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', - distinct_names Scope', !, - 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)), - close-term-no-prune-ty Lx 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, - fold-map Ty L Ty' L2, - std.append L2 L1 L3. - - 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'. - - % 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. - } - - % 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 deleted file mode 100644 index fe4105019..000000000 --- a/apps/tc/elpi/ho_link.elpi +++ /dev/null @@ -1,145 +0,0 @@ -namespace tc { - namespace link { - 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, !) => - fold-map T [] _ R. - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - % ETA LINK % - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - 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]. - - :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, !, - 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). - - pred occurs-rigidly i:term, i:term. - occurs-rigidly N N :- name N, !. - occurs-rigidly _ V :- var V, !, 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 (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 unify-left-right i:term, i:term. - unify-left-right (fun _ _ A) (fun _ _ A') :- !, pi x\ unify-left-right (A x) (A' x). - unify-left-right A (fun _ _ _ as T) :- !, eta-expand A Ae, pi x\ unify-left-right Ae T. - 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 (fun _ _ A) (fun _ _ A). - progress-eta-left A A' :- (name A; is-coq-term A), !, eta-expand A A'. - - 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 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. - - 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 A B :- var A, !, 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. - - constraint eta uvar relocate fun collect-store-aux 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). - } - - 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]. - } - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - % LLAM LINK % - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - 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 (fun _ _ _ as F) (app [H | TL]) :- - var H _ Scope, !, - 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, - coq.mk-app H' TL' Bo', - pi x\ llam F Bo'. - llam A B :- !, tc.unify-eq A B. - - constraint solve-llam solve-llam-t llam { - rule solve-llam \ (llam A B) <=> (A = B). - rule \ solve-llam. - } - } - - pred eta i:term, i:term. - eta A B :- eta.eta A B. - - pred solve-eta. - solve-eta :- declare_constraint solve-eta [_]. - - pred llam i:term, i:term. - llam A B :- llam.llam A B. - - pred solve-llam. - solve-llam :- declare_constraint solve-llam [_]. - } -} \ No newline at end of file diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi deleted file mode 100644 index f2bf4a9f4..000000000 --- a/apps/tc/elpi/ho_precompile.elpi +++ /dev/null @@ -1,268 +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 :- !. - - % 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 _ (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. - - 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 - */ - 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 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 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 :- !. - - % 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'), - precompile-aux Ty M' Ty' M. - - % Detect maybe-beta 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. - - % 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", - 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 X A X [X|A] :- var X, !. - } - - 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/link.elpi b/apps/tc/elpi/link.elpi new file mode 100644 index 000000000..a041dd868 --- /dev/null +++ b/apps/tc/elpi/link.elpi @@ -0,0 +1,246 @@ +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, !) => + fold-map T [] _ R. + + 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) + 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] :- !, + 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] :- !, + 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. + + % [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 % + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + namespace eta { + pred eta-expand i:term, o:term. + 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. + may-contract-to _ N N :- name N, !. + 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}, + 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 _ 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 (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, + 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 unify-left-right i:term, i:term. + unify-left-right (fun _ _ A) (fun _ _ A') :- !, pi x\ unify-left-right (A x) (A' x). + unify-left-right A (fun _ _ _ as T) :- !, eta-expand A Ae, pi x\ unify-left-right Ae T. + unify-left-right A A' :- A = A'. + + pred progress-eta-left i:term, o:term. + 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? 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, !. + + 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, !. + 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. + + constraint eta solve-eta { + 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)) + <=> (N1 :> G1 ?- B1 = B2'). + } + + :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 (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']. + } + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + % 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 (uvar as A) (app [(uvar as 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, + coq.mk-app H' TL' Bo', + pi x\ llam F Bo'. + llam A B :- !, tc.unify-eq A B. + + 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... + } + } + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + % CS LINK % + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + 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. + 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 | TL] as T) :- + if (HD = global (const Proj), tc.proj->record Proj Record) + (reduce-cs V T Record Proj) + % 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. + 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. + } + } + + % 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 [_]. + + pred llam i:term, i:term. + llam A B :- llam.llam A B. + + 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/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/elpi/solver.elpi b/apps/tc/elpi/solver.elpi index 97596e4ed..9163960ff 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. @@ -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} ">>>"), @@ -28,10 +29,12 @@ 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, % Trigger cs links (coercions + canonical structures) tc.link.solve-eta, % Trigger eta links tc.link.solve-llam % Trigger llam links ) "instance search". @@ -57,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"). @@ -64,6 +68,9 @@ 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. + pred print-links. + pred print-ctx. } \ No newline at end of file diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi index 940c0d442..f165afb14 100644 --- a/apps/tc/elpi/tc_aux.elpi +++ b/apps/tc/elpi/tc_aux.elpi @@ -181,7 +181,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,4 +220,15 @@ 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 canonical-projection + term -> % The current precompiled subterm + list term -> % The list of FV in the precomp subterm + int -> + term. + + type coercion + term -> + list term -> + term. +} \ No newline at end of file diff --git a/apps/tc/src/rocq_elpi_tc_register.ml b/apps/tc/src/rocq_elpi_tc_register.ml index a952b9416..22f94ab62 100644 --- a/apps/tc/src/rocq_elpi_tc_register.ml +++ b/apps/tc/src/rocq_elpi_tc_register.ml @@ -23,9 +23,6 @@ let gref2elpi_term (gref: GlobRef.t) : Cmd.raw = let observer_class (x : Typeclasses.typeclass) : Rocq_elpi_arg_HOAS.Cmd.raw list = [Cmd.String "new_class"; gref2elpi_term x.cl_impl] -let observer_default_instance (x : Typeclasses.typeclass) : Rocq_elpi_arg_HOAS.Cmd.raw list = - [Cmd.String "default_instance";gref2elpi_term x.cl_impl] - let observer_coercion add (x : Typeclasses.typeclass) : Rocq_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-stdlib/bigTest.v b/apps/tc/tests-stdlib/bigTest.v index 89de2c8b3..42825e83f 100644 --- a/apps/tc/tests-stdlib/bigTest.v +++ b/apps/tc/tests-stdlib/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/canonical_struct.v b/apps/tc/tests/canonical_struct.v new file mode 100644 index 000000000..86783b855 --- /dev/null +++ b/apps/tc/tests/canonical_struct.v @@ -0,0 +1,235 @@ +From elpi.apps Require Import tc. + +Module CS1. + + Structure ofe := Ofe { + ofe_car :> Type; + }. + Canonical ofe_nat : ofe := Ofe nat. + + TC.AddRecordFields (ofe) (Ofe) 1. + + 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. + +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; }. + TC.AddRecordFields (ofe) (Ofe) 1. + TC.AddRecordFields (cmra) (Cmra) 1. + + 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) := {}. + + 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. + TC.AddRecordFields (ofe) (Ofe) 1. + + 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 _. + Qed. +End CS11. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v index 7a0b8e185..631b08620 100644 --- a/apps/tc/tests/importOrder/sameOrderCommand.v +++ b/apps/tc/tests/importOrder/sameOrderCommand.v @@ -1,14 +1,19 @@ From elpi.apps Require Export tc. -From elpi.apps.tc.elpi Extra Dependency "ho_link.elpi" as ho_link. +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. Elpi Accumulate Db tc.db. +Elpi Accumulate Db tc_options.db. +Elpi Accumulate File tc_aux. Elpi Accumulate File unif. -Elpi Accumulate File ho_link. +Elpi Accumulate File compile_goal. +Elpi Accumulate File link. Elpi Accumulate File tc_same_order. diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v index 8ecbe3094..37cf891db 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:{{ @@ -16,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", @@ -24,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. @@ -118,7 +119,7 @@ Module HO_swap. Axiom (f : Type -> Type -> Type). Elpi Query TC.Solver lp:{{ tc.link.eta.maybe-eta (fun `x` _ c0 \ fun `y` _ c1 \ A2 c1 c0), - tc.link.eta.maybe-eta (fun `x` _ c0 \ fun `y` _ c1 \ A2 (A c1) c0), + tc.link.eta.maybe-eta (fun `x` _ c0 \ fun `y` _ c1 \ A2 (A_ c1) c0), tc.link.eta.maybe-eta {{fun x y => f x y}}. }}. @@ -128,7 +129,7 @@ Module HO_swap. Elpi Query TC.Solver lp:{{ @pi-decl `x` {{Type -> Type}} f\ tc.precomp.instance.is-uvar f => sigma T\ - tc.precomp.instance {{c1 (fun x y => lp:f y x)}} T N _ _, + tc.precomp.instance {{c1 (fun x y => lp:f y x)}} T N_ _ _, std.assert! (T = app[{{c1}}, tc.maybe-eta-tm _ _]) "[TC] invalid precomp". }}. @@ -203,7 +204,7 @@ Module HO_7. Qed. End HO_7. -Module HO_81. +(* Module HO_81. Class c1 (T : Type). Instance i1 F : c1 F. Qed. @@ -224,7 +225,7 @@ Module HO_81. of ?X is Type (i.e. it has `arity` zero) *) Fail apply _. Abort. -End HO_81. +End HO_81. *) Module HO_8. Class c1 (T : Type -> Type -> Type). @@ -234,7 +235,7 @@ Module HO_8. eexists. apply _. Unshelve. - apply nat. + auto. Qed. End HO_8. @@ -246,7 +247,7 @@ Module HO_9. Elpi Query TC.Solver lp:{{ pi F\ sigma T\ decl F `x` {{Type -> Type}} ==> tc.precomp.instance.is-uvar F ==> - tc.precomp.instance {{c1 (fun x => f (lp:F x) (lp:F x))}} T N _ _, + tc.precomp.instance {{c1 (fun x => f (lp:F x) (lp:F x))}} T _N _ _, std.assert! (T = app [{{c1}}, tc.maybe-eta-tm _ _]) "Invalid precompilation". }}. @@ -277,6 +278,55 @@ 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. @@ -337,7 +387,7 @@ Module Llam_1. @pi-decl `x` {{Type -> Type}} f\ tc.precomp.instance.is-uvar f => @pi-decl `x` {{Type -> Type}} g\ tc.precomp.instance.is-uvar g => sigma T\ - tc.precomp.instance {{A (fun x => lp:f (lp:g x))}} T N _ _, + tc.precomp.instance {{A (fun x => lp:f (lp:g x))}} T _N _ _, std.assert! (T = app[{{A}}, tc.maybe-eta-tm (fun _ _ (x\ tc.maybe-llam-tm _ _)) _]) "[TC] invalid precomp". }}. @@ -453,12 +503,12 @@ Module CoqUvar. Class c1 (i:Type -> Type -> Type). Elpi Query TC.Solver lp:{{ - tc.precomp.instance {{c1 (fun x y => lp:F y x)}} T _ _ _, + tc.precomp.instance {{c1 (fun x y => lp:F_ y x)}} T _ _ _, coq.say T, Expected = app[{{c1}}, tc.maybe-eta-tm (fun _ _ Inn) []], std.assert! (T = Expected) "[TC] invalid precompile1", pi x\ sigma ExpectedInn\ - ExpectedInn = tc.maybe-eta-tm (A x) [x], + ExpectedInn = tc.maybe-eta-tm (A_ x) [x], std.assert! ((Inn x) = ExpectedInn) "[TC] invalid precompile2". }}. @@ -510,14 +560,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). @@ -552,20 +594,17 @@ Module CoqUvar4. Class c1 (T : Type -> Type -> Type). Elpi Query TC.Solver lp:{{ - tc.precomp.instance {{c1 (fun x y => lp:X (lp:A x y) y)}} C _ _ _, + 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". }}. - (* 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. 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 diff --git a/apps/tc/tests/test_HO.v b/apps/tc/tests/test_HO.v index ac52081a7..408b92332 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 06e5280f9..3981bcca2 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_pending_mode.v b/apps/tc/tests/test_pending_mode.v index 527f15ac0..50f0c2474 100644 --- a/apps/tc/tests/test_pending_mode.v +++ b/apps/tc/tests/test_pending_mode.v @@ -35,7 +35,7 @@ Module ground1. Goal exists (x : Type), C (list x). eexists. - apply _. + Fail apply _. Abort. End ground1. @@ -46,7 +46,7 @@ Module ground2. Goal exists (x : Type), C (list x). eexists. - apply _. + Fail apply _. Abort. End ground2. @@ -63,14 +63,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. 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. diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v index 822436593..91df74131 100644 --- a/apps/tc/theories/add_commands.v +++ b/apps/tc/theories/add_commands.v @@ -4,12 +4,12 @@ From elpi.apps.tc Require Import db. 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 "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 "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,12 +20,8 @@ Elpi Command TC.AddAllInstances. Elpi Accumulate Db tc.db. Elpi Accumulate Db tc_options.db. 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 compile_instance compiler compile_goal. +Elpi Accumulate File unif modes link. Elpi Accumulate lp:{{ main L :- args->str-list L L1, @@ -37,12 +33,8 @@ Elpi Command TC.AddInstances. Elpi Accumulate Db tc.db. Elpi Accumulate Db tc_options.db. 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 compile_instance compiler compile_goal. +Elpi Accumulate File unif modes link. Elpi Accumulate File parser_addInstances. Elpi Accumulate lp:{{ main Arguments :- @@ -53,8 +45,7 @@ Elpi Accumulate lp:{{ Elpi Command TC.AddAllClasses. Elpi Accumulate Db tc.db. Elpi Accumulate Db tc_options.db. -Elpi Accumulate File tc_aux. -Elpi Accumulate File modes. +Elpi Accumulate File tc_aux modes. Elpi Accumulate File create_tc_predicate. Elpi Accumulate lp:{{ % Ignore is the list of classes we do not want to add @@ -67,8 +58,7 @@ Elpi Accumulate lp:{{ Elpi Command TC.AddClasses. Elpi Accumulate Db tc.db. Elpi Accumulate Db tc_options.db. -Elpi Accumulate File tc_aux. -Elpi Accumulate File modes. +Elpi Accumulate File tc_aux modes. Elpi Accumulate File create_tc_predicate. Elpi Accumulate lp:{{ pred tc.add-all-classes i:list argument , i:tc.search-mode. @@ -116,8 +106,7 @@ Elpi Accumulate lp:{{ Elpi Command TC.Declare. Elpi Accumulate Db tc.db. Elpi Accumulate Db tc_options.db. -Elpi Accumulate File tc_aux. -Elpi Accumulate File modes. +Elpi Accumulate File tc_aux modes. Elpi Accumulate File create_tc_predicate. Elpi Accumulate lp:{{ main _ :- coq.warning "TC.Declare" {tc.warning-name} @@ -131,8 +120,7 @@ with implicit arguments (those implicits will be neglected)", fail. Elpi Command TC.Pending_mode. Elpi Accumulate Db tc.db. Elpi Accumulate Db tc_options.db. -Elpi Accumulate File tc_aux. -Elpi Accumulate File modes. +Elpi Accumulate File tc_aux modes. Elpi Accumulate File create_tc_predicate. Elpi Accumulate lp:{{ main M :- @@ -142,8 +130,34 @@ Elpi Accumulate lp:{{ }}. +Elpi Command TC.AddRecordFields. +Elpi Accumulate Db tc.db. +Elpi Accumulate Db tc_options.db. +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 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 b8571dd2b..9ab27f703 100644 --- a/apps/tc/theories/db.v +++ b/apps/tc/theories/db.v @@ -101,7 +101,21 @@ Elpi Db tc.db lp:{{ pred ho-link o:term, i:term, o:A. pred link.eta i:term, i:term. pred link.llam i:term, i:term. + pred link.cs i:term, i:term. + pred link.build-eta-llam-links i:term, i:list prop, o:term, o:list prop. + % 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 elpi.apps.tc.elpi Extra Dependency "base.elpi" as base. diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v index a9cd831b8..350331dd6 100644 --- a/apps/tc/theories/tc.v +++ b/apps/tc/theories/tc.v @@ -4,13 +4,15 @@ Declare ML Module "rocq-elpi.tc". 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 "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. @@ -48,14 +50,8 @@ Elpi Tactic TC.Solver. Elpi Accumulate Db tc.db. Elpi Accumulate Db tc_options.db. 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 modes. +Elpi Accumulate File unif modes link. +Elpi Accumulate File compile_instance compile_goal. Elpi Accumulate File solver. Elpi Query lp:{{ sigma Options\ @@ -79,13 +75,9 @@ Elpi Command TC.Compiler. Elpi Accumulate Db tc.db. Elpi Accumulate Db tc_options.db. Elpi Accumulate File tc_aux. +Elpi Accumulate File unif modes link. +Elpi Accumulate File compile_instance compiler compile_goal. 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:{{ /* @@ -96,10 +88,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 @@ -121,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. }}. @@ -183,6 +171,8 @@ Elpi Accumulate lp:{{ }}. +(* 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 d7060d727..6b88f79d2 100644 --- a/apps/tc/theories/wip.v +++ b/apps/tc/theories/wip.v @@ -1,20 +1,21 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* --------------------------------------------------------------------------*) -Declare ML Module "rocq-elpi.tc". +(* Declare ML Module "coq-elpi.tc". From elpi Require Import elpi. 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". @@ -24,10 +25,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. @@ -48,7 +49,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] :- diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi index 7f1af9eb9..0900983f4 100644 --- a/builtin-doc/coq-builtin.elpi +++ b/builtin-doc/coq-builtin.elpi @@ -934,9 +934,11 @@ external pred coq.env.projection? i:constant, o:int. external pred coq.env.primitive-projections i:inductive, o:list (option (pair projection int)). -% [coq.env.primitive-projection? Projection Compatibility constant] relates -% a projection to its compatibility constant. -external pred coq.env.primitive-projection? i:projection, o:constant. +% [coq.env.primitive-projection? Projection Compatibility constant Index] +% Relates a primitive projection to its compatibility constant. Index is set +% to the constructor argument extracted by the projection (starting from 0). +external pred coq.env.primitive-projection? o:projection, o:constant, + o:int. % -- Sorts (and their universe level, if applicable) ---------------- @@ -1178,6 +1180,10 @@ external pred coq.CS.db o:list cs-instance. % or canonical Value, or both external pred coq.CS.db-for i:gref, i:cs-pattern, o:list cs-instance. +% [coq.CS.canonical-projection? Projection] Tells if the projection can be +% used for CS inference. +external pred coq.CS.canonical-projection? i:constant. + % [coq.TC.declare-class GR] Declare GR as a type class external pred coq.TC.declare-class i:gref. @@ -1372,13 +1378,6 @@ external pred coq.arguments.simplification i:gref, external pred coq.arguments.set-simplification i:gref, i:simplification_strategy. -% [coq.arguments.reset-simplification GR] resets the behavior of the -% simplification tactics. -% Also resets the ! and / modifiers for the Arguments command. -% Supported attributes: -% - @global! (default: false) -external pred coq.arguments.reset-simplification i:gref. - % [coq.locate-abbreviation Name Abbreviation] locates an abbreviation. It's % a fatal error if Name cannot be located. external pred coq.locate-abbreviation i:id, o:abbreviation.