diff --git a/apps/tc/elpi/base.elpi b/apps/tc/elpi/base.elpi index a62ecfab3..cfaa7e3c4 100644 --- a/apps/tc/elpi/base.elpi +++ b/apps/tc/elpi/base.elpi @@ -150,3 +150,8 @@ func close-term-no-prune-ty (term -> list prop), term -> 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'. + + +func fold-map2 list A, B, C, (func A, B, C -> A', B, C) -> list A', B, C. +fold-map2 [] A B _ [] A B. +fold-map2 [X|XS] A B F [Y|YS] A2 B2 :- F X A B Y A1 B1, fold-map2 XS A1 B1 F YS A2 B2. diff --git a/apps/tc/elpi/compiler1.elpi b/apps/tc/elpi/compiler1.elpi index 2075f1f56..f33b4deb1 100644 --- a/apps/tc/elpi/compiler1.elpi +++ b/apps/tc/elpi/compiler1.elpi @@ -94,7 +94,7 @@ namespace tc { remove-inst InstGR :- tc.get-full-path InstGR ClauseName, std.once(tc.instance _ InstGR ClassGR Locality), - tc.gref->pred-name ClassGR PredName, + tc.gref->pred-name "tc" ClassGR PredName, coq.env.typeof ClassGR ClassTy, coq.elpi.predicate PredName {build-args ClassTy} Clause, tc.remove-clause ClauseName Clause Locality. diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi index 6f204f353..68fa86989 100644 --- a/apps/tc/elpi/create_tc_predicate.elpi +++ b/apps/tc/elpi/create_tc_predicate.elpi @@ -21,7 +21,7 @@ add-class-gr SearchMode ClassGR SMR :- tc.get-elpi-mode ClassGR SMR EM SM, if (std.forall EM (m\ sigma a s\ m = pr a s, a = out)) (true) ( std.fold EM "" (m\s\r\ sigma a s'\ m = pr a s', if (a = in) (calc (s ^ " 10") r) (calc (s ^ " _") r)) Indexing), - tc.gref->pred-name ClassGR PredName, + tc.gref->pred-name "tc" ClassGR PredName, get-class-locality Locality, Locality => ( coq.elpi.add-predicate "tc.db" Indexing PredName EM, @@ -64,7 +64,7 @@ declare-class-in-coq ClassGR :- % CAVEAT: this triggers the observer coq.TC.declare-class ClassGR, attr->search-mode SearchMode, - tc.gref->pred-name ClassGR PredName, + tc.gref->pred-name "tc" ClassGR PredName, % HACK: we override the clauses added by the observer, since it does not know % the SearchMode. get-class-locality Locality, @@ -106,7 +106,7 @@ namespace eta-reduction-aux { compile ClassGR (sort _) tt L (pi sol new-term\ Cl new-term sol) :- pi solution new-term\ sigma Args Args' Q Q'\ std.do![ - tc.gref->pred-name ClassGR PredName, + tc.gref->pred-name "tc" ClassGR PredName, std.rev [solution | L] Args, replace Args new-term Args' T, coq.elpi.predicate PredName Args Q, diff --git a/apps/tc/elpi/cs.elpi b/apps/tc/elpi/cs.elpi new file mode 100644 index 000000000..a40d6ab18 --- /dev/null +++ b/apps/tc/elpi/cs.elpi @@ -0,0 +1,265 @@ +namespace cs { + namespace compiler { + func ocan (func constant ->), option constant. + ocan F (some C) :- coq.CS.canonical-projection? C, !, F C. + ocan _ _. + + func forall-ocan (func constant ->), list (option constant) ->. + forall-ocan F L :- std.forall L (ocan F). + + + % NOTE: the following code is to build a predicate name canstr-projx + % the problem is that we need to awake all links for CS projection + % after the execution of a tc resolution. Rules for constraints seems + % not to be dynamically extensible, therefore tc.link.solver-proj will + % not be capable of awaking new dynamically declared predicates. + % We use a single predicate tc.link.proj with three arguments for each + % projection: tc.link.proj PNAME CAR CS + % func proj-to-pname constant -> string. + % proj-to-pname P S :- tc.gref->pred-name "canstr" (const P) S. + + % namespace record { + % % each cs goal has three argument: + % % - N the name of the projection + % % - A the argument of the projection + % % - the canonical structure of N applied to A + % func proj-to-args constant -> list (pair argument_mode string). + % proj-to-args _ [pr in "term", pr in "term", pr out "term"]. + % % coq.env.projection? C N, + % % std.list.init N (x\y\ y = MT) L, + % % std.append L [MT, MT] R. + + % % [make-pred-sig C Db] + % % C the projection's constant + % % Db the name of the database in which adding the predicate + % func make-pred-sig string, constant ->. + % make-pred-sig Db C :- !, + % proj-to-pname C S, + % proj-to-args C A, + % coq.elpi.add-predicate Db _ S A. + + % func create-cs-pred i:term. + % create-cs-pred (global (indt R)) :- + % coq.env.projections R LP, + % forall-ocan (make-pred-sig "tc.db") LP. + % } + + namespace cs { + :index (_ 1) + func get-projn int, list (option constant) -> list (pair int constant). + get-projn _ [] []. + get-projn M [some C|Xs] [pr M C|Ys] :- coq.CS.canonical-projection? C, !, N is M + 1, get-projn N Xs Ys. + get-projn M [_|Xs] Ys :- N is M + 1, get-projn N Xs Ys. + + func get-proj term -> list (pair int constant). + get-proj (prod _ _ B) Pg :- !, pi x\ get-proj (B x) Pg. + get-proj (app [X|_]) Pg :- !, get-proj X Pg. + get-proj (global (indt R)) Pg :- + coq.env.indt R _ N _ _ _ _, + coq.env.projections R P, get-projn N P Pg. + + func is-uvar term ->. + + % [compile C P Ag T R] + % P = projection + % Ag = args list of the can struct + % I = carrier + % CS = canonical structure + % R = the compiled rule for the cs + func compile constant, term, term -> prop. + % compile P I CS R :- + % proj-to-pname P PN, + % coq.elpi.predicate PN [I, CS] R. + compile P I CS (tc.link.proj P I CS :- !). + + :index (1 _ 1) + func mk-rule bool, prop, list prop -> prop. + mk-rule tt P [] (P :- !) :- !. + mk-rule ff P [] P :- !. + mk-rule tt P R (P :- [! | R]). + mk-rule ff P R (R => P). + + func work-proj constant, int, list term, term, nat -> term, nat. + work-proj P PN Ag R N (tc.maybe-proj P PN Ag R []) (s N) :- is-uvar R, !. + work-proj P PN Ag R N T' N :- tc.proj-reducer P PN Ag R T', !. + work-proj P PN Ag R N (tc.maybe-proj P PN Ag R []) (s N) :- !. + + func precompile term, nat -> term, nat. + :name "cs-precompile" + precompile T N T' N' :- + tc.maybe-projection T P PN Ag R, !, + work-proj P PN Ag R N T' N'. + + precompile X A Y A :- name X, !, X = Y, !. % avoid loading "precompile x A x A" at binders + precompile (global _ as C) A C A :- !. + precompile (pglobal _ _ as C) A C A :- !. + precompile (sort _ as C) A C A :- !. + precompile (fun N T F) A (fun N T1 F1) A2 :- !, + precompile T A T1 A1, pi x\ precompile (F x) A1 (F1 x) A2. + precompile (let N T B F) A (let N T1 B1 F1) A3 :- !, + precompile T A T1 A1, precompile B A1 B1 A2, pi x\ precompile (F x) A2 (F1 x) A3. + precompile (prod N T F) A (prod N T1 F1) A2 :- !, + precompile T A T1 A1, (pi x\ precompile (F x) A1 (F1 x) A2). + precompile (app L) A (app L1) A1 :- !, std.fold-map L A precompile L1 A1. + precompile (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !, + precompile Ty A Ty1 A1, pi x\ precompile (F x) A1 (F1 x) A2. + precompile (match T Rty B) A (match T1 Rty1 B1) A3 :- !, + precompile T A T1 A1, precompile Rty A1 Rty1 A2, std.fold-map B A2 precompile B1 A3. + precompile (primitive _ as C) A C A :- !. + precompile (uvar M L as X) A W A1 :- var X, !, std.fold-map L A precompile L1 A1, coq.mk-app-uvar M L1 W. + % when used in CHR rules + precompile (uvar X L) A (uvar X L1) A1 :- std.fold-map L A precompile L1 A1. + + + func decompile term, pair (list term) (list prop) -> term, pair (list term) (list prop). + :name "cs-decompile" + decompile (tc.maybe-proj C _ _ R S) (pr [X|XS] L1) Y (pr XS [tc.link.proj C Y R|L1]) :- !, + name Y X S. + % proj-to-pname C PN, + % coq.elpi.predicate PN [R, Y] NL. + + decompile X A Y A :- name X, !, X = Y, !. % avoid loading "decompile x A x A" at binders + decompile (global _ as C) A C A :- !. + decompile (pglobal _ _ as C) A C A :- !. + decompile (sort _ as C) A C A :- !. + decompile (fun N T F) A (fun N T1 F1) A2 :- !, + decompile T A T1 A1, pi x\ decompile (F x) A1 (F1 x) A2. + decompile (let N T B F) A (let N T1 B1 F1) A3 :- !, + decompile T A T1 A1, decompile B A1 B1 A2, pi x\ decompile (F x) A2 (F1 x) A3. + decompile (prod N T F) A (prod N T1 F1) A2 :- !, + decompile T A T1 A1, (pi x\ decompile (F x) A1 (F1 x) A2). + decompile (app L) A (app L1) A1 :- !, std.fold-map L A decompile L1 A1. + decompile (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !, + decompile Ty A Ty1 A1, pi x\ decompile (F x) A1 (F1 x) A2. + decompile (match T Rty B) A (match T1 Rty1 B1) A3 :- !, + decompile T A T1 A1, decompile Rty A1 Rty1 A2, std.fold-map B A2 decompile B1 A3. + decompile (primitive _ as C) A C A :- !. + decompile (uvar M L as X) A W A1 :- var X, !, std.fold-map L A decompile L1 A1, coq.mk-app-uvar M L1 W. + % when used in CHR rules + decompile (uvar X L) A (uvar X L1) A1 :- std.fold-map L A decompile L1 A1. + + % [load-nestedp N B S T P L C] + % N is the number of pi to load + % B is the pos/neg position of the term being compiled + % C is the name of the predicate + % T is the argument (with N problematic subterms) + % P is the instance of the record to be used + % L is the list of pi accumulated terms + % Pr is the list of premises accumulated so far + % R is the created clause + func load-nestedp nat, bool, constant, term, term, list term, list prop -> prop. + load-nestedp z B C T P L Pr R :- + decompile T (pr L []) T' (pr _ Pm), + % coq.elpi.predicate C [T', P] Hd, + mk-rule B (tc.link.proj C T' P) {std.rev.aux Pm {std.rev [!|Pr]}} R. + load-nestedp (s N) B C T P L Pr (pi x\ R x) :- pi x\ load-nestedp N B C T P [x|L] Pr (R x). + + % [compiler B IC CS Ag P L C] + % B is the pos/neg position of the term + % IC is the projection being compiled together with its number + % CS is the instance of the structure + % Ag is the term being consumed for compilation (i.e. the implementation of CS) + % L is the list of premises (TODO: should be removed?) + % PT is the list of pi-quantified variables for problematic subterms + % A is the list of abstractions: the arguments of CS + % C is the final rule + % NOTE: differently from type-class compilation, we are not compiling + % types of terms, but their implementation. That is we need to cross + % fun instead of prod + :index (_ _ _ 1) + func compiler bool, (pair int constant), term, term, list prop, list term, list term -> prop. + compiler B (pr N P) CS (app[_|Ag]) L _ A Rs :- + coq.mk-app CS {std.rev A} CS', + std.nth N Ag I, + precompile I z I' NPb, + load-nestedp NPb B P I' CS' [] L Rs. + compiler B P CS (fun N Ty Bo') L PT A (pi x\ R x) :- tc.get-TC-of-inst-type Ty TC, !, + @pi-decl N Ty x\ (is-uvar x :- !) ==> + tc.compile.instance Ty x (Pr x), + compiler B P CS (Bo' x) [Pr x|L] PT [x|A] (R x). + compiler B P CS (fun N Ty Bo') L PT A (pi x\ R x) :- + @pi-decl N Ty x\ (is-uvar x :- !) ==> + compiler B P CS (Bo' x) L PT [x|A] (R x). + + :index (_ _ _ 1) + func compiler-record bool, (pair int constant), term, term, list prop, list term, list term -> prop. + compiler-record B P CS (prod N Ty Bo') L PT A (pi x\ R x) :- tc.get-TC-of-inst-type Ty TC, !, + @pi-decl N Ty x\ (is-uvar x :- !) ==> + tc.compile.instance Ty x (Pr x), + compiler-record B P CS (Bo' x) [Pr x|L] PT [x|A] (R x). + compiler-record B P CS (prod N Ty Bo') L PT A (pi x\ R x) :- !, + @pi-decl N Ty x\ (is-uvar x :- !) ==> + compiler-record B P CS (Bo' x) L PT [x|A] (R x). + compiler-record B (pr N P) CS _ L _ A Rs :- + std.rev A Ar, + coq.mk-app CS Ar CS', + std.nth N Ar I, + precompile I z I' NPb, + load-nestedp NPb B P I' CS' [] L Rs. + + % func compiler-pt nat, (pair int constant), term, term, list term -> prop. + % compiler-pt z IC CS T L R :- compiler tt IC CS T [] L [] R. + % compiler-pt (s N) IC CS T L (pi x\ R x) :- + % pi x\ is-uvar x => compiler-pt N IC CS T [x|L] (R x). + + % :index (_ _ _ _ 1 1) + % func compiler-univ nat, (pair int constant), term, term, list univ, list univ-instance -> prop. + % compiler-univ N IC CS T [] [] R :- compiler-pt N IC CS T [] R. + % compiler-univ N IC CS T [X|Xs] L (pi x\ R x) :- + % pi x\ (copy (sort (typ X)) (sort (typ x)) :- !) => + % compiler-univ N IC CS T Xs L (R x). + % compiler-univ N IC CS T [] [X|Xs] (pi x\ R x) :- + % pi x\ (copy (pglobal A UnivInst) (pglobal A x) :- !) => + % compiler-univ N IC CS T [] Xs (R x). + + func main.aux + (func bool, (pair int constant), term, term, list prop, list term, list term -> prop), + (pair int constant), term, term -> . + main.aux F IC I T :- + F tt IC I T [] [] [] R, + tc.add-tc-db _ (after "0") R. + + :index (4) + func main term ->. + :name "cs.compiler.main" + main (global (const C) as T) :- + coq.env.const C (some Bo) Ty, + get-proj Ty P, + std.forall P (x\ main.aux compiler x T Bo). + main (global (indc C) as T) :- + coq.typecheck T Ty ok, + get-proj Ty P, + std.forall P (x\ main.aux compiler-record x T Ty). + } + + % namespace default { + % func build-default constant ->. + % build-default D :- + % R = (pi x y z \ tc.link.proj D (uvar as x) y :- declare_constraint (tc.link.proj D x y) [x,z]), + % tc.add-tc-db _ _ R. + + % func main term ->. + % main (global (indt C)) :- + % coq.env.projections C P, + % cs.compiler.forall-ocan build-default P. + % } + } + + namespace solver { + func solve goal ->. + solve (goal Ctx _ _ T [trm P, trm R] as G) :- + tc.compile.context Ctx CtxR, + coq.safe-dest-app P (global (const H)) _, + CtxR => tc.link.proj H R T. + } + + pred main list argument. + :name "cs-main" + % main [str "class", trm T] :- !, std.assert! (cs.compiler.record.create-cs-pred T) "Cannot compile record projection". + main [str "cs", trm T] :- !, std.assert! (cs.compiler.cs.main T) "Cannot compile canonical structure". + % main [str "default", trm T] :- !, std.assert! (cs.compiler.default.main T) "Cannot compile canonical structure". + main L :- coq.error " + Invalid input for command cs\n + Expected:\n \tElpi cs cs (CANSTR)". + % \tElpi class (STRU)\n +} \ No newline at end of file diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi index 00b02f9c8..403c2d753 100644 --- a/apps/tc/elpi/ho_compile.elpi +++ b/apps/tc/elpi/ho_compile.elpi @@ -1,425 +1,430 @@ -namespace tc { - shorten tc.{r-ar, range-arity}. - - namespace compile { - - namespace instance { - func is-name term ->. - func is-uvar 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 { - - func decompile-term-aux term, pair (list term) (list prop) -> term, 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 (let N T Ty Bo) PR (let N T' Ty' Bo') PR3 :- !, - decompile-term-aux T PR T' PR1, - decompile-term-aux Ty PR1 Ty' PR2, - (pi x\ is-name x => decompile-term-aux (Bo x) PR2 (Bo' x) PR3). - - decompile-term-aux A B _ _ :- coq.error "[TC] cannot decompile-term-aux of" A B. - - :functional - 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 - func clean-term term -> 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". - - func main - nat, % the number of problematic terms - term, % the type of the instance - term, % the global gref of the instance - list univ, % the list of univ variable to be replaced with elpi fresh vars - list univ-instance % the list of univ-instance to be replaced with elpi fresh vars - -> 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 _ _` - func add-pi-problematic-terms - nat, % the number of pi to quantify - list term, % the list of quantified pi - term, % the fuel of the compilation (the type of the instance) - term % the global gref of the current instance - -> 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) - func make-eta-link-aux - term, % A : The variable to eta-expand - term, % prod _ Ty Bo : The type of A - pair term name, % pr B Bn : The eta-expanded version of B with its name (they are fresh names) - list term % L : The list of name in the scope of A and B - -> prop, % Link : The new eta-link - term, % Ty' : The cleaned version of the binder in Ty - (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 - :index (_ _ 1) - func make-eta-link term, term, list (pair term name), list term, list prop -> 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 - :index (_ 1) - func add-link-eta-dedup - (func list prop -> prop), - range-arity, term, term, (list (pair term name)), list prop -> 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. +namespace tc.compile { + % [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 + func make-pairs-aux term, term -> 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 _ _ []. + + func make-pairs list term -> 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. + + % Uva Binders LinkEta + func build-eta-links-of-vars-aux term, list term -> 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 _ _ []. + + func build-eta-links-of-vars list term -> 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. + + func get-uva-pair-arity term, list term -> 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. + + namespace instance { + func is-name term ->. + func is-uvar 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 { + + func decompile-term-aux term, list term, list prop -> term, list term, list prop. + + decompile-term-aux X A L Y A L :- name X, !, X = Y, !. % avoid loading "decompile-term-aux x A x A" at binders + decompile-term-aux (global _ as C) A L C A L :- !. + decompile-term-aux (pglobal _ _ as T) A L T' A L :- !, copy T T', !. + decompile-term-aux (sort _ as T) A L T' A L :- !, copy T T', !. + decompile-term-aux (uvar as X) A L X A L :- !. + decompile-term-aux (primitive _ as P) A L P A L :- !. + + :name "decompile-inst-maybe-proj" + decompile-term-aux (tc.maybe-proj P _ _ T S) [X|XS] L1 Y XS [tc.link.proj P Y T|L1] :- !, name Y X S. + + decompile-term-aux (tc.maybe-eta-tm T S) [X|XS] L1 Y XS' [NL | L2] :- !, + name Y X S, + decompile-term-aux T XS L1 T' XS' L2, + NL = tc.link.eta Y T'. + + % 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 H PF NPF S) [X|XS] L1 Y 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, + fold-map2 NPF XS L1 decompile-term-aux Tl 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 H PF NPF S) A L Z XS' [NL | L3] :- !, + var H _ Scope, !, + std.append Scope S S', + prune Z S', + make-pairs [T] Pairs, + % We build on the fly the eta-links for T + (Pairs ==> build-eta-links-of-vars [T] P, get-uva-pair-arity T PF Y), + fold-map2 NPF A L decompile-term-aux Tl XS' L2, + std.append P L2 L3, + NL = tc.link.llam Z (app [Y|Tl]). + + decompile-term-aux (fun Name Ty Bo) XS L (fun Name Ty' Bo') XS2 L3 :- !, + (pi x\ is-name x => decompile-term-aux (Bo x) XS [] (Bo' x) XS1 (L1x x)), + close-term-no-prune-ty L1x {clean-term Ty} L1, + decompile-term-aux Ty XS1 L Ty' XS2 L2, + std.append L1 L2 L3. + + decompile-term-aux (prod Name Ty Bo) XS L (prod Name Ty' Bo') XS2 L3 :- !, + (pi x\ is-name x => decompile-term-aux (Bo x) XS [] (Bo' x) XS1 (L1x x)), + close-term-no-prune-ty L1x {clean-term Ty} L1, + decompile-term-aux Ty XS1 L Ty' 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 A R N A :- + 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]) A B Z 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', + make-pairs [T] Pairs, + % We build on the fly the eta-links for `T` + (Pairs ==> build-eta-links-of-vars [T] P, get-uva-pair-arity T L Y), + var Z Y Scope', + std.append P B B'. + + decompile-term-aux (app L) A PR (app L') A' PR' :- !, + fold-map2 L A PR decompile-term-aux L' A' PR'. + + decompile-term-aux (let N T Ty Bo) A PR (let N T' Ty' Bo') A3 PR3 :- !, + decompile-term-aux T A PR T' A1 PR1, + decompile-term-aux Ty A1 PR1 Ty' A2 PR2, + (pi x\ is-name x => decompile-term-aux (Bo x) A2 PR2 (Bo' x) A3 PR3). + + decompile-term-aux A B C _ _ _ :- coq.error "[TC] cannot decompile-term-aux of" A B C. + :functional - 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' = std.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. - - :index (_ _ _ _ 1) - func compile-ty - list term, - list term, - term, - bool, - term, - list term, - list prop - -> 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 L1 ProofHd IsPositive (let _ Ty T Bo) ProofTlR PremR Clause :- !, + 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 L [] R L' Links. + + } + + % TODO: also replace (sort (typ X)) and (pglobal _ X) with holes in the place of X + func clean-term term -> term. + clean-term A B :- + (pi c n a s sc r \ copy (tc.maybe-proj c n a s sc) r :- !, sigma X\ std.append a [s] X, copy (app[global(const c) | X]) r) => + (pi t s r \ copy (tc.maybe-eta-tm t s) r :- !, copy t r, !) => + (pi a p n s r \ copy (tc.maybe-llam-tm a p n s) r :- !, sigma X\ std.append p n X, copy (app[a|X]) r, !) => + std.assert! (copy A B) "[TC] clean-term error". + + :index (_ _ _ 1 1) + func main + nat, % the number of problematic terms + term, % the type of the instance + term, % the global gref of the instance + list univ, % the list of univ variable to be replaced with elpi fresh vars + list univ-instance % the list of univ-instance to be replaced with elpi fresh vars + -> 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 _ _` + func add-pi-problematic-terms + nat, % the number of pi to quantify + list term, % the list of quantified pi + term, % the fuel of the compilation (the type of the instance) + term % the global gref of the current instance + -> 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) + func make-eta-link-aux + term, % A : The variable to eta-expand + term, % prod _ Ty Bo : The type of A + pair term name, % pr B Bn : The eta-expanded version of B with its name (they are fresh names) + list term % L : The list of name in the scope of A and B + -> prop, % Link : The new eta-link + term, % Ty' : The cleaned version of the binder in Ty + (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'. + % 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 + :index (_ _ 1) + func make-eta-link term, term, list (pair term name), list term, list prop -> 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 + :index (_ 1) + func add-link-eta-dedup + (func list prop -> prop), + nat, term, term, (list (pair term name)), list prop -> prop. + % Base case when the variable is always used at same arity + add-link-eta-dedup F z _ _ [] PremR Clause :- !, + F PremR Clause. + add-link-eta-dedup F z P Pty Acc PremR Clause :- !, + make-eta-link P Pty Acc [] [] LinkEtaDedup, + F [LinkEtaDedup|PremR] Clause. + add-link-eta-dedup F (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 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. + + :functional + pred compile-premise + i:list term, % L : a list of pi-quantified variables (used as elpi unification variables when building links) + o:list term, % L' : a suffix of L containing the still unused variables + i:term, % P : the premise of an instance whose applicative head is a class + i:term, % Pt : the type of P + i:term, % I : the instance at toplevel that triggered the instance compilation + i:bool, % B : tells if the premise P is in positive or negative position + i:term, % It : the type of I that has not yet been explored + i:list term, % Ag : the arguments of I that will be part of the proof + i:list prop, % Pr : the premises of the rule + o:prop. % C : the final clause corresponding to the compilation of I + compile-premise L L2 P PTy ProofHd IsPositive ITy ProofTlR PremR Clause :- + tc.get-TC-of-inst-type PTy TC, !, + compile-ty L L1 P {neg IsPositive} PTy [] [] NewPrem, + if (tc.class TC _ tc.deterministic _) + (NewPrem' = std.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. + + :index (_ _ _ _ 1) + func compile-ty + list term, % L : a list of pi-quantified variables (used as elpi unification variables when building links) + list term, % L' : a suffix of L containing the still unused variables + term, % I : the premise of an instance whose applicative head is a class + bool, % B : tells if the premise P is in positive or negative position + term, % It : the type of I that has not yet been explored + list term, % Ag : the arguments of I that will be part of the proof + list prop % Pr : the premises of the rule + -> prop. % C : the final clause corresponding to the compilation of I + compile-ty L L1 ProofHd IsPositive (prod N Ty Bo) ProofTlR PremR Clause :- !, + std.do![ + std.assert! (pi x\ tc.precomp.instance.get-max-arity x Ty (Bo x) Arity) "[TC] get-max-arity should not fail", 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 NewPrem\ - (decl p N Ty' :- !) => (E p :- !) => ( - NewPrem = tc.link.unif-eq T p, - compile-premise L L1 p Ty ProofHd IsPositive (Bo p) ProofTlR [NewPrem | 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 - ]. - - func compile-conclusion - bool, % tt if the term is in positive position - term, % the goal (invariant: it is a constant or a application) - term, % the proof - list prop, % the list of HOPremises in input mode - list prop, % the list of HOPremises in output mode - list prop % the premises - -> 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). - - func context goal-ctx -> 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. - } + (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 L1 ProofHd IsPositive (let _ Ty T Bo) ProofTlR PremR Clause :- !, + 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 NewPrem\ + (decl p N Ty' :- !) => (E p :- !) => ( + NewPrem = tc.link.unif-eq T p, + compile-premise L L1 p Ty ProofHd IsPositive (Bo p) ProofTlR [NewPrem | 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 + ]. + + func compile-conclusion + bool, % tt if the term is in positive position + term, % the goal (invariant: it is a constant or a application) + term, % the proof + list prop, % the list of HOPremises in input mode + list prop, % the list of HOPremises in output mode + list prop % the premises + -> 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). - % build a list of Clauses of type tc to be temporarly added to the - % database, used in theorems having assumptions. func context goal-ctx -> list prop. - :name "tc-compile-context" - context Ctx Clauses :- - std.assert! (instance.context Ctx Clauses) "[TC] cannot compile context". - - func instance term, term -> 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", !. - - func instance-gr gref -> 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 - func make-pairs-aux term, term -> 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 _ _ []. - - func make-pairs list term -> 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. - - func get-uva-pair-arity term, list term -> 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. - - func decompile-problematic-term term, list prop -> term, 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 :- - fold-map Ty L Ty' L1, - (pi x\ fold-map (Bo x) [] (Bo' x) (Lx x)), - close-term-no-prune-ty Lx Ty' L2, - std.append L1 L2 L3. + context [] []. + % if the hyp is for a TC we compile before its insertion in the context + context [X | Xs] [Clause | ResTl] :- + (decl Var _ Ty = X; def Var _ Ty _ = X), + tc.is-instance-term Ty, !, + std.assert! (instance Ty Var Clause) "[TC] cannot compile instance of context", + context Xs ResTl. + context [_ | Tl] L :- context Tl L. + } - 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. - - func compile term, list prop -> term, 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 - func build-eta-links-of-vars-aux term, list term -> 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 _ _ []. - - func build-eta-links-of-vars list term -> list prop. - build-eta-links-of-vars [] []. - build-eta-links-of-vars [V|Vars] L :- - var V Hd S, - build-eta-links-of-vars-aux Hd S L', - build-eta-links-of-vars Vars L'', - std.append L' L'' L. - } + % build a list of Clauses of type tc to be temporarly added to the + % database, used in theorems having assumptions. + func context goal-ctx -> list prop. + :name "tc-compile-context" + context Ctx Clauses :- + std.assert! (instance.context Ctx Clauses) "[TC] cannot compile context". + + func instance term, term -> 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", !. + + func instance-gr gref -> 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 { + func decomp-term term, list prop -> term, list prop. + decomp-term X A Y A :- name X, !, X = Y, !. + decomp-term (global _ as C) A C A :- !. + decomp-term (pglobal _ _ as C) A C A :- !. + decomp-term (sort _ as C) A C A :- !. + + decomp-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :- + prune V S, !, decomp-term T L T' L2. + + decomp-term (tc.maybe-proj P _ _ T S) L Y [tc.link.proj P Y T|L] :- !, prune Y S. + + decomp-term (tc.maybe-llam-tm H S NPF Sc) L Z [NL|L'] :- !, + prune Z Sc, + get-uva-pair-arity H S Y, + std.fold-map NPF L decomp-term Tl L', + NL = tc.link.llam Z (app[Y | Tl]). + + % TODO: complete this fold + decomp-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'. - % Goal Goal' Links - func goal term -> term, 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" - ). + decomp-term A L A L :- var A, !. + + decomp-term (fun N Ty Bo) L (fun N Ty' Bo') L3 :- + decomp-term Ty L Ty' L1, + (pi x\ decomp-term (Bo x) [] (Bo' x) (Lx x)), + close-term-no-prune-ty Lx Ty' L2, + std.append L1 L2 L3. + + decomp-term (prod N Ty Bo) L (prod N Ty' Bo') L3 :- + (pi x\ decomp-term (Bo x) [] (Bo' x) (Lx x)), + close-term-no-prune-ty Lx Ty L1, + decomp-term Ty L Ty' L2, + std.append L2 L1 L3. + + decomp-term (let N T B F) A (let N T1 B1 F1) A3 :- !, + decomp-term T A T1 A1, decomp-term B A1 B1 A2, + pi x\ decomp-term (F x) A2 (F1 x) A3. + decomp-term (app L) A (app L1) A1 :- !, + std.fold-map L A decomp-term L1 A1. + decomp-term (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !, + decomp-term Ty A Ty1 A1, + pi x\ decomp-term (F x) A1 (F1 x) A2. + decomp-term (match T Rty B) A (match T1 Rty1 B1) A3 :- !, + decomp-term T A T1 A1, decomp-term Rty A1 Rty1 A2, + std.fold-map B A2 decomp-term B1 A3. + decomp-term (primitive _ as C) A C A :- !. + decomp-term (uvar M L as X) A W A1 :- var X, !, + std.fold-map L A decomp-term L1 A1, coq.mk-app-uvar M L1 W. } + + % Goal Goal' Links + func goal term -> term, list prop. + :name "compile-goal" + goal Goal Goal' Links :- + tc.precomp.goal Goal GoalPrecomp Vars, !, + make-pairs Vars Pairs, + Pairs => ( + std.assert!(build-eta-links-of-vars Vars EtaLinks) "[TC] cannot build eta-links", + std.assert!(goal.decomp-term GoalPrecomp EtaLinks Goal' Links) "[TC] cannot compile goal" + ). } + diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi index 7541330d6..d8b630a64 100644 --- a/apps/tc/elpi/ho_link.elpi +++ b/apps/tc/elpi/ho_link.elpi @@ -1,158 +1,196 @@ -namespace tc { - namespace link { - func get-vars term -> 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 { - func eta-expand term -> 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) - func may-contract-to list term, term, term ->. - may-contract-to _ N N :- name N, !. - may-contract-to L N V :- var V _ S, !, - std.forall [N|L] (x\ std.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) - func occurs-rigidly term, term ->. - occurs-rigidly N N :- name N, !. - occurs-rigidly _ V :- var V, !, fail. - occurs-rigidly N (app A) :- std.exists! A (occurs-rigidly N). - occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x). - - :index (1) - func maybe-eta-aux term, 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 (std.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]. - - func maybe-eta term ->. - maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x]. - - func unify-left-right term, 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'. - - func progress-eta-left term -> 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'. - - func progress-eta-right term -> 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), !. - - func scope-check term, term ->. - scope-check (uvar _ L) T :- prune A L, A = T, !. - - :index (1) - func relocate list term, list term, term -> 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. - func collect-store-aux list prop -> list prop. - - collect-store L :- collect-store-aux [] L. - collect-store-aux X L :- declare_constraint (collect-store-aux X L) [_]. - - func unify-eta term, 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). - } - - func eta term, term ->. - eta _ uvar :- !, coq.error "[TC] link.eta error, flexible rhs". - eta A (fun _ _ B as T) :- not (var A), not (var B), !, unify-left-right A T. - eta A B :- progress-eta-right B B', !, A = B'. - eta A B :- progress-eta-left A A', !, A' = B. - eta A B :- scope-check A B, get-vars B Vars, declare_constraint (eta A B) [_,A|Vars]. +namespace tc.link { + shorten tc.{get-vars}. + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + % ETA LINK % + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + namespace eta { + func eta-expand term -> 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) + func may-contract-to list term, term, term ->. + may-contract-to _ N N :- name N, !. + may-contract-to L N V :- var V _ S, !, + std.forall [N|L] (x\ std.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) + func occurs-rigidly term, term ->. + occurs-rigidly N N :- name N, !. + occurs-rigidly _ V :- var V, !, fail. + occurs-rigidly N (app A) :- std.exists! A (occurs-rigidly N). + occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x). + + :index (1) + func maybe-eta-aux term, 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 (std.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]. + + func maybe-eta term ->. + maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x]. + + func unify-left-right term, 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'. + + func progress-eta-left term -> 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'. + + func progress-eta-right term -> 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), !. + + func scope-check term, term ->. + scope-check (uvar _ L) T :- prune A L, A = T, !. + + :index (1) + func relocate list term, list term, term -> 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. + func collect-store-aux list prop -> list prop. + + collect-store L :- collect-store-aux [] L. + collect-store-aux X L :- declare_constraint (collect-store-aux X L) [_]. + + func unify-eta term, 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). } - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - % LLAM LINK % - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - namespace llam { - func llam term, 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 :- !, std.once(tc.unify-eq A B). - - constraint solve-llam llam { - rule solve-llam \ (llam A B) <=> (A = B). - rule \ solve-llam. - } + func eta term, term ->. + eta _ uvar :- !, coq.error "[TC] link.eta error, flexible rhs". + eta A (fun _ _ B as T) :- not (var A), not (var B), !, unify-left-right A T. + eta A B :- progress-eta-right B B', !, A = B'. + eta A B :- progress-eta-left A A', !, A' = B. + eta A B :- scope-check A B, get-vars B Vars, declare_constraint (eta A B) [_,A|Vars]. + } + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + % LLAM LINK % + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + namespace llam { + func llam term, 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 :- !, std.once(tc.unify-eq A B). + + constraint solve-llam llam { + rule solve-llam \ (llam A B) <=> (A = B). + rule \ solve-llam. } + } - namespace unif-eq { - func unif-eq term, term. - unif-eq T1 (uvar as T2) :- !, declare_constraint (unif-eq T1 T2) [_,T2]. - unif-eq T1 T2 :- !, coq.unify-eq T1 T2 ok. + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + % Projection LINK % + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + namespace proj { + % func proj term, term ->. + % proj T V :- var V, !, get-vars T Vars, declare_constraint (proj T V) [_,V|Vars]. + % :name "proj-unif" + % proj T R :- coq.unify-eq T R ok. + + % TODO: this recreates the application of C to T adding the record arguments + % as unification variables (via the _ symbol), we could pass them as a + % parameter of tc.link.proj + func build-proj-app constant, term -> term. + build-proj-app C T (app[global(const C) | L']) :- + coq.env.projection? C N, + std.list.make N _ L, + std.append L [T] L'. + + func force-unify list prop, term, term ->. + :name "force-proj" + % If B is a variale we launch elpi unification + force-unify _ A B :- var B, !, A = B. + force-unify Ctx A B :- Ctx => coq.unify-eq A B ok. + + + constraint decl def ?- solve-proj tc.link.proj force-unify { + % TODO: should add a dedup constraint + rule solve-proj \ (Ctx ?- tc.link.proj C B A) <=> (build-proj-app C A T, force-unify Ctx T B). + % rule solve-proj \ (Ctx ?- proj A B) <=> (A = B). + rule \ solve-proj. } + } - func unif-eq term, term ->. - unif-eq T1 T2 :- unif-eq.unif-eq T1 T2. + proj C (app[global(const C)| Ag]) L :- !, std.last Ag L. + proj C (uvar as T) X :- declare_constraint (proj C T X) [T, _]. + namespace unif-eq { + func unif-eq term, term. + unif-eq T1 (uvar as T2) :- !, declare_constraint (unif-eq T1 T2) [_,T2]. + unif-eq T1 T2 :- !, coq.unify-eq T1 T2 ok. + } - func eta term, term -> . - eta A B :- eta.eta A B. + func unif-eq term, term ->. + unif-eq T1 T2 :- unif-eq.unif-eq T1 T2. - func solve-eta. - solve-eta :- declare_constraint solve-eta [_]. - func llam term, term ->. - llam A B :- llam.llam A B. + func eta term, term -> . + eta A B :- eta.eta A B. - func solve-llam. - solve-llam :- declare_constraint solve-llam [_]. - } -} \ No newline at end of file + func solve-eta. + solve-eta :- declare_constraint solve-eta [_]. + + func llam term, term ->. + llam A B :- llam.llam A B. + + func solve-llam. + solve-llam :- declare_constraint solve-llam [_]. + + % func proj constant, term -> term. + % proj A B :- proj.proj A B. + + func solve-proj. + solve-proj :- declare_constraint solve-proj [_]. + +} diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi index 70fce53ed..95a753598 100644 --- a/apps/tc/elpi/ho_precompile.elpi +++ b/apps/tc/elpi/ho_precompile.elpi @@ -1,282 +1,251 @@ -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) - func may-contract-to list term, term, term ->. - may-contract-to _ N N :- !. - may-contract-to L N (app [V|S]) :- var V, !, - std.forall [N|L] (x\ std.exists! S (may-contract-to [] x)). - may-contract-to L N (app [V|S]) :- is-uvar V, !, - std.forall [N|L] (x\ std.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) - func occurs-rigidly term, 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) :- std.exists! A (occurs-rigidly N). - occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x). - - func maybe-eta-aux term, list term ->. - maybe-eta-aux (app[V|S]) L :- is-uvar V, !, - std.forall L (x\ std.exists! S (y\ may-contract-to [] x y)). - maybe-eta-aux (app[V|S]) L :- var V, !, - std.forall L (x\ std.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 (std.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]. - - func maybe-eta term ->. - maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x]. - - func free-var -> list term. - free-var L :- - std.findall (is-name _) T, - std.map T (x\y\ x = is-name y) L. - - func split-pf list term, list term -> list term, 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 _) - func neg positivity -> 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. - - func min-max-nat range-arity, range-arity -> 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 - :index (_ 1) - func get-range-arity-aux term, term -> 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 X (let _ T Ty B) R4 :- !, - get-range-arity-aux X Ty R1, - get-range-arity-aux X T R2, - (pi x\ get-range-arity-aux T (B x) R3), - min-max-nat R1 R2 R12, - min-max-nat R12 R3 R4. - get-range-arity-aux A B _ :- coq.error "Count maximal arity failure" A B. - - func get-range-arity term, term, term -> 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. - - :index (_ 1) - func precompile-aux positivity, term, nat -> term, 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 is_neg_fix 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, !. - - precompile-aux _ (let N T Ty Bo) A (let N T' Ty' Bo') A3 :- !, - precompile-aux is_neg_fix T A T' A1, - precompile-aux is_neg_fix Ty A1 Ty' A2, - pi x\ is-name x => precompile-aux is_neg_fix (Bo x) A2 (Bo' x) A3. - - - % 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. - - func get-univ-instances term -> list univ-instance. - get-univ-instances T L :- - (pi x L\ fold-map (pglobal _ x) L _ [x | L] :- !) => fold-map T [] _ L, !. - - func get-univ term -> 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 - */ - func instance term -> term, nat, list univ, 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) - func may-contract-to list term, term, 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\ std.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) - func occurs-rigidly term, term ->. - occurs-rigidly N N :- name N, !. - occurs-rigidly _ (app [N|_]) :- var N, !, fail. - occurs-rigidly N (app A) :- std.exists! A (occurs-rigidly N). - occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x). - - func maybe-eta-aux term, 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\ std.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 (std.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]. - - func maybe-eta term ->. - maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x]. - - func split-pf list term, list term -> list term, 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. - - func precompile-aux term, list term -> term, 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, !. - } +namespace tc.precomp { + % 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) + func may-contract-to list term, term, term ->. + may-contract-to [] N N :- !. + may-contract-to L N (app [V|S]) :- (var V; is-uvar V), !, + std.forall [N|L] (x\ std.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) + func occurs-rigidly term, term ->. + occurs-rigidly N N :- name N, !. + occurs-rigidly _ (app [N|_]) :- (var N; is-uvar N), !, fail. + occurs-rigidly _ (app [N|_]) :- var N, !, fail. + occurs-rigidly N (app A) :- std.exists! A (occurs-rigidly N). + occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x). + + func maybe-eta-aux term, list term ->. + % TODO: maybe var V _ X succeeds and X is not empty, should therefore + % also take into account X? + maybe-eta-aux (app[V|S]) L :- (var V; is-uvar V), !, + std.forall L (x\ std.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 (std.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]. + + func maybe-eta term ->. + maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x]. + + % [split-pf B L1 L2 L3 L4] + % splits the list of L1 into L3 and L4, so that: + % **∀ e \in L3, F i** and **L2 ∩ L3 = ∅** + func split-pf (pred term ->), list term, list term -> list term, list term. + split-pf F [] _ [] [] :- !. + split-pf F [X|Xs] Old [X|Ys] L :- F X, not (std.mem! Old X), !, split-pf F Xs [X|Old] Ys L. + split-pf F Xs _ [] Xs. + + % [work-proj F P PN Ag R N T N'] + % F is a function returning the scope of the current term + % P, PN are the constant and the proj number + % Ag are the argument of the projector (except for the record) + % R is the record + % N is the hole counter + % T is the new term + % N' is the updated counter + func work-proj (func -> list term), constant, int, list term, term, nat -> term, nat. + work-proj F P PN Ag R N (tc.maybe-proj P PN Ag R X) (s N) :- (var R; is-uvar R), !, F X. + work-proj _ P PN Ag R N T' N :- tc.proj-reducer P PN Ag R T', !. + work-proj F P _ Ag R N (tc.maybe-proj P PN Ag R X) (s N) :- !, F X. + + namespace instance { + + func free-var -> list term. + free-var L :- + std.findall (is-name _) T, + std.map T (x\y\ x = is-name y) L. + + kind positivity type. + type is_pos positivity. + type is_neg positivity. + type is_neg_fix positivity. + + :index (1 _) + func neg positivity -> positivity. + neg is_pos is_neg :- !. + neg is_neg is_pos :- !. + neg is_neg_fix is_neg_fix :- !. + + % [max-arity-aux X T N] + % returns the maximal application of X in T + % for example, max-arity-aux x (f (x 1 2) (g (x 4 5 6))) returns 3 + :index (_ 1) + func get-max-arity-aux term, term -> nat. + get-max-arity-aux _ N z :- name N, !. + get-max-arity-aux _ (tc.maybe-proj _ _ _ _ _) z :- !. + get-max-arity-aux X (tc.maybe-llam-tm H PF NPF _) R :- !, + if (H == X) (length-nat {std.append PF NPF} Len) (Len = z), + std.fold PF Len (x\y\w\ sigma M\ get-max-arity-aux X x M, max-nat y M w) R', + std.fold NPF R' (x\y\w\ sigma M\ get-max-arity-aux X x M, max-nat y M w) R. + get-max-arity-aux X (tc.maybe-eta-tm T _) R :- !, get-max-arity-aux X T R. + get-max-arity-aux T (app [H|L]) R :- !, + if (T == H) (length-nat L Len) (Len = z), + std.fold L Len (x\y\w\ sigma M\ get-max-arity-aux T x M, max-nat y M w) R. + get-max-arity-aux T (fun _ Ty B) R2 :- !, + get-max-arity-aux T Ty R, + (pi x\ get-max-arity-aux T (B x) R1), + max-nat R R1 R2. + get-max-arity-aux T (prod _ Ty B) R2 :- !, + get-max-arity-aux T Ty R, + (pi x\ get-max-arity-aux T (B x) R1), + max-nat R R1 R2. + get-max-arity-aux _ (global _) z :- !. + get-max-arity-aux _ uvar z :- !. + get-max-arity-aux _ (sort _) z :- !. + get-max-arity-aux _ (pglobal _ _) z :- !. + get-max-arity-aux X (let _ T Ty B) R4 :- !, + get-max-arity-aux X Ty R1, + get-max-arity-aux X T R2, + (pi x\ get-max-arity-aux T (B x) R3), + max-nat {max-nat R1 R2} R3 R4. + get-max-arity-aux A B _ :- coq.error "TC: get-max-arity-aux failure with" A B. + + % [get-max-arity T Ty T' N] + % Invariant = T is of type Ty and T is a name + % returns the number of variables that shoud be quantified + % when compiling T, in particular: + % - if Ty a type-class, then we return the number of arguments of the class + % - otherwise, we count at which arity T is used in T' + func get-max-arity term, term, term -> nat. + get-max-arity _ Ty _ N :- tc.get-TC-of-inst-type Ty _, !, count-prod Ty N. + get-max-arity T _ T' N :- !, get-max-arity-aux T T' N. + + % [precompile-aux P T N T' N'] + % P tells if we are in positive or negative position + % takes a term T and a nat N + % returns a tagged term T and an unpdated nat N' + % the tags are for problematic subterms and N' is for how many problamatic subterms exists + :index (_ 1) + func precompile-aux positivity, term, nat -> term, 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 :- !. + :name "precomp-proj-inst" + precompile-aux _ T N T' N' :- + tc.maybe-projection T P PN Ag R, !, + % TODO: should precompile Ag? + work-proj free-var P PN Ag R N T' N'. + + % 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 => decl x Name Ty => precompile-aux is_neg_fix (B x) N' (B' x) M). + + precompile-aux _ (app [X|XS]) N (tc.maybe-llam-tm X PF NPF1 Scope) (s M) :- + if (is-uvar X) (Sc = []) (var X _ Sc), split-pf is-name 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. + + precompile-aux IsP (prod Name Ty B) N (prod Name Ty' B') P :- !, + std.assert! (pi x\ get-max-arity x Ty (B x) MaxAr) "[TC] get-max-arity should not fail", + if (IsP = is_pos) (C = x\ is-uvar x) (C = x\ is-name x), + std.assert! (pi x\ C x => decl x Name Ty => 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 is_neg_fix T A T1 A1, pi x\ is-name x => decl x N T => 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, !. + + precompile-aux _ (let N T Ty Bo) A (let N T' Ty' Bo') A3 :- !, + precompile-aux is_neg_fix T A T' A1, + precompile-aux is_neg_fix Ty A1 Ty' A2, + pi x\ is-name x => def x N T Ty => precompile-aux is_neg_fix (Bo x) A2 (Bo' x) A3. + + + precompile-aux B (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !, + precompile-aux B Ty A Ty1 A1, pi x\ precompile-aux is_neg_fix (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 :- !. + + func get-univ-instances term -> list univ-instance. + get-univ-instances T L :- + (pi x L\ fold-map (pglobal _ x) L _ [x | L] :- !) => fold-map T [] _ L, !. + + func get-univ term -> 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. + } - func goal term -> term, list term. - goal T T' Vars' :- std.assert!(goal.precompile-aux T [] T' Vars) "[TC] cannot precompile goal", undup-same Vars Vars'. + /* + [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` + N is the number of problematic terms in T + */ + func instance term -> term, nat, list univ, 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 { + func precompile-aux term, list term -> term, 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 :- !. + :name "precomp-proj-goal" + precompile-aux T A T' A :- + tc.maybe-projection T P PN Ag R, !, + work-proj names P PN Ag R z T' _. + + % 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\ decl x Name Ty => 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 X PF NPF1 Scope1) [X|M] :- + var X _ Scope, split-pf name XS Scope PF NPF, + not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF + names Scope1, + std.fold-map NPF N precompile-aux NPF1 M. + + precompile-aux (prod Name Ty B) N (prod Name Ty' B') P :- !, + std.assert! (pi x\ decl x Name Ty => 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\ decl x N Ty => 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\ def x N T1 B1 => 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, !. } + + func goal term -> term, list term. + goal T T' Vars' :- std.assert!(goal.precompile-aux T [] T' Vars) "[TC] cannot precompile goal", undup-same Vars Vars'. } \ No newline at end of file diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi index fb77502ff..af22a19ba 100644 --- a/apps/tc/elpi/solver.elpi +++ b/apps/tc/elpi/solver.elpi @@ -1,6 +1,5 @@ /* license: GNU Lesser General Public License Version 2.1 or later */ /* ------------------------------------------------------------------------- */ -main _. msolve L N :- tc.time-it tc.oTC-time-msolve (coq.ltac.all (coq.ltac.open tc.solve-aux) L N) "msolve". msolve L _ :- coq.ltac.fail _ "[TC] fail to solve" L. @@ -11,7 +10,7 @@ namespace tc { tc.compile.goal Goal Goal' PostProcess, !, coq.safe-dest-app Goal' (global TC) TL', std.append TL' [Proof] TL, !, - coq.elpi.predicate {tc.gref->pred-name TC} TL Q. + coq.elpi.predicate {tc.gref->pred-name "tc" TC} TL Q. type tc.mode_fail term. @@ -33,7 +32,8 @@ namespace tc { tc.time-it tc.oTC-time-instance-search ( do PostProcess, Q, tc.link.solve-eta, % Trigger eta links - tc.link.solve-llam % Trigger llam links + tc.link.solve-llam, % Trigger llam links + tc.link.solve-proj % Trigger proj links ) "instance search". pred solve-aux i:goal, o:list sealed-goal. diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi index d723e7c57..bfc84e42b 100644 --- a/apps/tc/elpi/tc_aux.elpi +++ b/apps/tc/elpi/tc_aux.elpi @@ -3,6 +3,11 @@ namespace tc { + func get-vars term -> 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. + namespace lettify { func replace-args term, list term, list term, (func term -> term) -> term. replace-args Hd [] L K R :- std.rev L L1, K (app [Hd|L1]) R. @@ -78,6 +83,7 @@ namespace tc { % adds a clause to the tc.db DB at the passed grafting func add-tc-db id, grafting, prop ->. + :name "tc-adder" add-tc-db _ _ Clause :- not (ground_term Clause), coq.error "[TC] anomaly: open rule:" Clause, !. add-tc-db ClauseName Graft Clause :- coq.elpi.accumulate _ "tc.db" (clause ClauseName Graft Clause), !. add-tc-db _ _ Clause :- coq.error "cannot add " PR " to tc.db". @@ -98,19 +104,28 @@ namespace tc { get-TC-of-inst-type T Hd, coq.TC.class? Hd. - % TC preds are on the form tc-[PATH_TO_TC].tc-[TC-Name] - func gref->pred-name gref -> string. - gref->pred-name Gr S :- + func check-pname string, gref ->. + check-pname N _ :- coq.elpi.predicate? N, !. + check-pname _ G :- + MSG is "Found an undeclared class in Elpi.\nPlease add it via: Elpi TC.AddClasses " ^ {coq.gref->id G}, + coq.say MSG, coq.error MSG. + + % [gref->pred-name P G S] + % takes a prefix P and a gref G + % returns S = P-[PATH_TO_G].P-[TC-Name] + % NOTE: P should start with lower case letter + func gref->pred-name string, gref -> string. + gref->pred-name P G S :- if (tc.is-option-active tc.oTC-clauseNameShortName) (Path = "") - (coq.gref->path Gr [Hd | Tl], + (coq.gref->path G [Hd | Tl], if (Hd = "Coq") (Hd' = "Corelib") (Hd' = Hd), std.string.concat "." [Hd'|Tl] Path', - Path is Path' ^ ".tc-"), + Path is Path' ^ "." ^ P ^ "-"), % CAVEAT : Non-ascii caractars can't be part of a pred % name, we replace ö with o - rex.replace "ö" "o" {coq.gref->id Gr} GrStr, - S is "tc-" ^ Path ^ GrStr. + rex.replace "ö" "o" {coq.gref->id G} GrStr, + S is P ^ "-" ^ Path ^ GrStr. func get-mode gref -> list string. get-mode ClassGR M :- tc.class ClassGR _ _ M, !. @@ -137,8 +152,9 @@ namespace tc { make-tc Goal Sol RuleBody IsPositive Rule :- coq.safe-dest-app Goal Class Args, get-TC-of-inst-type Class ClassGR, - gref->pred-name ClassGR ClassStr, + gref->pred-name "tc" ClassGR ClassStr, std.append Args [Sol] ArgsSol, + tc.check-pname ClassStr ClassGR, coq.elpi.predicate ClassStr ArgsSol RuleHead, make-tc.aux IsPositive Sol RuleHead RuleBody Rule. @@ -207,21 +223,106 @@ namespace tc { time-it Opt P Msg :- time-is-active Opt, !, time-res P Time Res, build-msg Res Msg Msg', time-pp Msg' Time, Res. time-it _ P _ :- P. - kind range-arity type. - type r-ar nat -> nat -> range-arity. - - type prod-range - term -> % The current qunatified uvar - range-arity -> % Its minimum and maximal application - term. + func split-last list A -> list A, A. + split-last [X] [] X :- !. + split-last [X|Xs] [X|Y] Z :- split-last Xs Y Z. + + func list.pos list A, A -> int. + list.pos [A|_] A 0 :- !. + list.pos [_|L] A N :- list.pos L A N', N is N' + 1. + + func get-record int, term -> inductive. + get-record 0 (prod _ (app [global (indt I) | _]) _) I :- !. + get-record 0 (prod _ (global (indt I)) _) I :- !. + get-record N (prod _ _ Bo) T :- N > 0, N' is N - 1, + pi x\ get-record N' (Bo x) T, !. + + func get-proj-nb constant -> int. + get-proj-nb C N :- + coq.env.projection? C Nx, + coq.env.const C _ Ty, + get-record Nx Ty I, + coq.env.projections I P, + list.pos P (some C) M, + N is M + Nx. + + % [maybe-projection T C N A R] + % check if the head of T is the application of a projection + % for example T = app[P, ARGS..., R] + % where P is the projector, ARGS are the parameter of the projector + % R is the record to project + % C is the compatibily constant of the projector P + % N is the number position of C + % A is the list of argument applied to the projection (except for the record itself) + % R is the record + func maybe-projection term -> constant, int, list term, term. + :name "maybe-projection" + maybe-projection (app [primitive (proj P N), R]) C N A R :- + coq.env.primitive-projection? P C _, coq.CS.canonical-projection? C, + std.assert-ok!(coq.typecheck R Ty) "err", + coq.safe-dest-app Ty _ A. + % TODO: should check that C is fully applied + maybe-projection (app [global (const C) | Args]) C N A R :- + coq.CS.canonical-projection? C, !, + get-proj-nb C N, std.assert!(split-last Args A R) "err: empty list". + + func build-proj-term constant, list term, term -> term. + build-proj-term P Ag C (app[global (const P) | Ag']) :- + std.append Ag [C] Ag'. + + + % [proj-reducer-aux R P N O L T] + % R is the record constant + % P is the compatibility constant of the projector + % N is the projection number + % O is the optional body of the projected constant + % L are the arguments of the projection + % T is the projected terms + :index(_ _ _ 1) + func proj-reducer-aux constant, constant, int, option term, list term -> term. + :name "proj-reducer-aux" + proj-reducer-aux _ _ N (some (app [_|L])) _ T :- std.nth N L T. + proj-reducer-aux R P _ none Ag T :- build-proj-term P Ag (global (const R)) T. + + % [proj-reducer P N Ag R T] + % P is the projector constant + % N is the number of P + % Ag is the arguments applied to the projector (except for the record) + % R is the record + % T is the reduced term + func proj-reducer constant, int, list term, term -> term. + :name "proj-reducer" + proj-reducer P N _ (global (const R)) T :- !, + coq.env.const R O Ty, + coq.safe-dest-app Ty _ TyAg, + proj-reducer-aux R P N O TyAg T. + proj-reducer P _ Ag X T :- name X, !, build-proj-term P Ag X T. type maybe-eta-tm term -> % The current precompiled subterm list term -> % The list of FV in the precomp subterm term. + % [maybe-llam-tm H PF NPF L] + % the original term is (app[H|{append PF NPF}]) + % H is a variable, PF is a list of distinct names and NPF is a list of terms + % a maybe-llam-tm is (F x y (H z) (K w)) when H and K become both (x\x) + % in this case the term becomes (maybe-llam F [x,y] [H z,K w] [V3,V4]) + % where V3 and V4 are elpi variables of arity 3 and 4, used to represent the + % term when applied to 3 or 4 arguments type maybe-llam-tm - term -> % The current precompiled subterm: shape is app[app[X,PF],NPF] + term -> % The head of the term + list term -> % The list of arguments in the PF + list term -> % The list of argument not in the PF list term -> % The eta-expanded version of X, from X^{len(PF)} to X^{len(PF)+len(NPF)} term. + + type maybe-proj + constant -> % The canonical constant of a projection (INVARIANT: it is the canonical projection of a CS) + int -> % The position of the CS in the record + list term -> % The arguments of the projection + term -> % The record which is projected + list term -> % The list of FV in the scope of the problematic term + term. + } diff --git a/apps/tc/src/rocq_elpi_tc_register.ml b/apps/tc/src/rocq_elpi_tc_register.ml index 07764aeab..97f97fc88 100644 --- a/apps/tc/src/rocq_elpi_tc_register.ml +++ b/apps/tc/src/rocq_elpi_tc_register.ml @@ -145,4 +145,4 @@ let activate_observer (observer : qualified_name) = Lib.add_leaf (inTakeover (Activate observer)) let deactivate_observer (observer : qualified_name) = - Lib.add_leaf (inTakeover (Deactivate observer)) + Lib.add_leaf (inTakeover (Deactivate observer)) \ No newline at end of file diff --git a/apps/tc/tests-stdlib/bench/bench_inj.py b/apps/tc/tests-stdlib/bench/bench_inj.py index 9a44376ab..ebe740cec 100644 --- a/apps/tc/tests-stdlib/bench/bench_inj.py +++ b/apps/tc/tests-stdlib/bench/bench_inj.py @@ -3,6 +3,7 @@ import sys import os import re +import random """ About this file: @@ -19,23 +20,33 @@ """ INJ_BASE_FUN = "f" -KEYS = "coqT, elpiT, tcSearch, refineT, compilT, runtimeT, buildQuery".split(", ") +TOT_COQ_TIME = "coqT" +TOT_ELPI_TIME = "elpiT" +TOT_NORMALIZE = "normalize" +TOT_COMPILE_CTX = "compile context" +TOT_BUILD_QUERY = "build query" +TOT_INSTANCE_SEARCH = "instance search" +TOT_FULL_INSTANCE_SEARCH = "full instance search" +TOT_REFINE = "refine" +MSOLVE = "msolve" -def buildDict(): - res = dict() - for key in KEYS: - res[key] = [] - return res +COMPILT = "compilT" +RUNTIMET = "runtimeT" + +KEYL = [TOT_COQ_TIME, TOT_ELPI_TIME, TOT_NORMALIZE, TOT_COMPILE_CTX, TOT_BUILD_QUERY, TOT_INSTANCE_SEARCH, TOT_FULL_INSTANCE_SEARCH, TOT_REFINE, MSOLVE, COMPILT, RUNTIMET] +HEADER = re.sub(r'\s+', ' ', "Height, Coq, Elpi, normalize, ctx, BuildQuery, TC search, TC Search Full, Refine, msolve, ElpiCompil, ElpiRuntime, DIFF, Ratio(Coq/Elpi), Ratio(Elpi/Coq)") def printDict(d): - for key in KEYS: - d[key] = sum(d[key])/len(d[key]) - L = [d[k] for k in KEYS] - L.append(d["elpiT"] - d["refineT"] - d["buildQuery"]) - L.append(d["coqT"] / d["elpiT"]) - L.append(d["elpiT"] / d["coqT"] if d["coqT"] > 0 else 100) + # for key in KEYS: + # d[key] = sum(d[key])/len(d[key]) + # L = [d[k] for k in KEYS] + L = [] + for k in KEYL: L.append(d[k]) + L.append(d[TOT_ELPI_TIME] - d[MSOLVE]) + L.append(d[TOT_COQ_TIME] / d[TOT_ELPI_TIME]) + L.append(d[TOT_ELPI_TIME] / d[TOT_COQ_TIME] if d[TOT_COQ_TIME] > 0 else 100) print(", ".join(map(lambda x: str(round(x, 5)), L))) @@ -44,31 +55,32 @@ def findFloats(s): def filterLines(lines): - #print(lines) - validStarts = ["Finished", "Refine", "Elpi:", "Instance search", "Time build query"] + with open("xxx.txt", "w") as f: + f.write(lines) + DEBUG_STR = "Debug: [TC] - Time of " + r = {} for line in lines.split("\n"): - for start in validStarts: - if start in line: - yield line - - -def parseFile(s): - lines = [findFloats(x) for x in filterLines(s)] - #print(lines) - base = 0 - coqT = lines[base][0] - buildQuery = lines[base + 1][0] - tcSearch = lines[base + 2][0] - refineT = lines[base + 3][0] - elpiStats = lines[base + 4] - compilT, runtimeT = elpiStats[0], elpiStats[-1] - elpiT = lines[base + 5][0] - res = buildDict() - for key in KEYS: - res[key].append(eval(key)) - #print(res) - return res - + fl = findFloats(line) + if line.startswith("Finished transaction"): + if TOT_COQ_TIME in r: r[TOT_ELPI_TIME] = fl[0] + else: r[TOT_COQ_TIME] = fl[0] + elif line.strip().startswith("Elpi: query-compilation"): + r[COMPILT] = fl[0] + r[RUNTIMET] = fl[-1] + elif line.startswith(DEBUG_STR): + def check_(n): return line.startswith(DEBUG_STR + n) + def set_(n): r[n] = fl[0] + if check_(TOT_NORMALIZE): set_(TOT_NORMALIZE) + elif check_(TOT_COMPILE_CTX): set_(TOT_COMPILE_CTX) + elif check_(TOT_BUILD_QUERY): set_(TOT_BUILD_QUERY) + elif check_(TOT_INSTANCE_SEARCH): set_(TOT_INSTANCE_SEARCH) + elif check_(TOT_FULL_INSTANCE_SEARCH): set_(TOT_FULL_INSTANCE_SEARCH) + elif check_(TOT_REFINE): set_(TOT_REFINE) + elif check_(MSOLVE): set_(MSOLVE) + else: raise "Not found" + line + with open("zzz.txt", "w") as f: + f.write(str(r)) + return r def buildTree(len): if len == 0: @@ -87,22 +99,44 @@ def buildTree(len): }}. """ +refine_no_check = """ +Elpi Accumulate TC.Solver lp:{{ + :after "0" + tc.refine-proof Proof G GL :- !, + + /*********** CHECK IF THE PROOF TYPECHECKS ***********/ + tc.time-it tc.oTC-time-refine (@no-tc! => refine.no_check Proof G GL) "refine.typecheck", + + if-true tc.print-solution (coq.say "[TC] The proof typechecks"). +}}. +""" if False else "" + def writeFile(fileName: str, composeLen: int, isCoq: bool): - PREAMBLE = f"""\ -From elpi_apps_tc_tests_stdlib Require Import {"stdppInjClassic" if isCoq else "stdppInj"}. -{"" if isCoq else 'Elpi TC.Solver. Set TC Time Refine. Set TC Time Instance Search. Set TC Time Build Query. Set Debug "elpitime".'} -""" + TXT = f"(* {random.random()} *)\n" GOAL = buildTree(composeLen) + if isCoq: + TXT += "From elpi_apps_tc_tests_stdlib Require Import stdppInjClassic.\n" + TXT += f"Goal Inj eq eq({GOAL}). Time apply _. Qed.\n" + else: + TXT += "From elpi_apps_tc_tests_stdlib Require Import stdppInj.\n" + TXT += refine_no_check # (Un)Comment this for using refine or refine.no_check + TXT += f"Goal Inj eq eq({GOAL}).\n" + # TXT += "Elpi Command time_it. Elpi Accumulate lp:{{ main _ :- coq.say {gettimeofday}. }}. Elpi time_it.\n" + TXT += 'Set Time TC Bench. Set Debug "elpitime".\n' + TXT += "Time apply _.\n" + # TXT += "Unset Time TC Bench. Set Debug \"-elpitime\". Elpi time_it.\n" + TXT += "Qed.\n" with open(fileName + ".v", "w") as fd: - fd.write(PREAMBLE) - fd.write(f"Goal Inj eq eq({GOAL}). Time apply _. Qed.\n") - + fd.write(TXT) def runCoqMake(fileName): fileName = fileName + ".vo" - if (os.path.exists(file_name)): + if (os.path.exists(fileName)): subprocess.run(["rm", fileName]) - return subprocess.check_output(["make", fileName]).decode() + r = subprocess.run(["dune" , "build", fileName], capture_output=True, text=True) + out = r.stdout + err = r.stderr + return f"{out}\n---\n f{err}" def run(file_name, height): @@ -112,22 +146,43 @@ def partialFun(isCoq: bool): return partialFun +def plot_dict(i, d): + L = [2**i, d[TOT_INSTANCE_SEARCH]] + L.append(L[-1] + d[TOT_INSTANCE_SEARCH] + d[TOT_BUILD_QUERY] + d[TOT_COMPILE_CTX] + d[TOT_NORMALIZE]) + L.append(L[-1] + d[TOT_REFINE]) + L.append(d[TOT_ELPI_TIME]) + L.append(d[TOT_COQ_TIME]) + return L + +def print_plot(pl): + l = "" + for i in pl: + l += ",".join(map(lambda x: str(round(x, 5)), i)) + "\n" + return l + def loopTreeDepth(file_name: str, maxHeight: int, makeCoq=True, onlyOne=False): - print("Height, Coq, Elpi, TC search, Refine, ElpiCompil, ElpiRuntime, BuildQuery, ElpiNoRefine, Ratio(Coq/Elpi), Ratio(Elpi/Coq)") + plot = [] + print(HEADER) for i in range(1 if not onlyOne else maxHeight, maxHeight+1): FUN = run(file_name, i) - x = FUN(True) if makeCoq else "Finished 0.0" + x = FUN(True) if makeCoq else "Finished transaction in 0.0" y = FUN(False) - print(i, ", ", end="", sep="") + print(2**i, ", ", end="", sep="") # print("The xx result is " , x) - dic = parseFile(x + y) + dic = filterLines(x + y) + plot.append(plot_dict(i, dic)) printDict(dic) - + return plot if __name__ == "__main__": print(os.curdir) - file_name = "tests/bench/bench_inj" + file_name = "tests-stdlib/bench/bench_inj" height = int(sys.argv[1]) - loopTreeDepth(file_name, height, makeCoq=not ( + pl = loopTreeDepth(file_name, height, makeCoq=not ( "-nocoq" in sys.argv), onlyOne=("-onlyOne" in sys.argv)) + + print("\n\n ELPI STATS") + print("HEIGHT, TC, BUILD, REFINE, COQ") + + print(print_plot((pl))) #writeFile(file_name, 1, False) diff --git a/apps/tc/tests-stdlib/bench/bench_inj.v b/apps/tc/tests-stdlib/bench/bench_inj.v index 43dde51ab..1202e9df0 100644 --- a/apps/tc/tests-stdlib/bench/bench_inj.v +++ b/apps/tc/tests-stdlib/bench/bench_inj.v @@ -1,3 +1,3 @@ From elpi_apps_tc_tests_stdlib Require Import stdppInj. -Elpi TC.Solver. Set TC Time Refine. Set TC Time Instance Search. Set Debug "elpitime". +Set TC Time Refine. Set TC Time Instance Search. Set Debug "elpitime". Goal Inj eq eq((compose f f )). Time apply _. Qed. diff --git a/apps/tc/tests/dune b/apps/tc/tests/dune index aa17dd497..8f3390bff 100644 --- a/apps/tc/tests/dune +++ b/apps/tc/tests/dune @@ -2,7 +2,7 @@ (name elpi.apps.tc.tests) (flags :standard -async-proofs-cache force) (package rocq-elpi-tests) - (theories elpi elpi.apps.tc)) + (theories elpi elpi.apps.tc elpi.apps.cs)) (include_subdirs qualified) (dirs :standard \ WIP) diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v index 8ecbe3094..20ab61f84 100644 --- a/apps/tc/tests/test.v +++ b/apps/tc/tests/test.v @@ -7,7 +7,7 @@ Section test_max_arity. (prod `a` _ c3 \ app [global _, app [c1, c3], c2]) c3 \ app [global _, c1, c2]), - pi x\ tc.precomp.instance.get-range-arity x _ (T x) (tc.r-ar z (s z)). + pi x\ tc.precomp.instance.get-max-arity x _ (T x) (s z). }}. End test_max_arity. @@ -126,7 +126,7 @@ Module HO_swap. Class c2 (T : (Type -> Type -> Type)). Elpi Query TC.Solver lp:{{ - @pi-decl `x` {{Type -> Type}} f\ tc.precomp.instance.is-uvar f => + @pi-decl `x` {{Type -> Type}} f\ tc.precomp.is-uvar f => sigma T\ 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". @@ -212,7 +212,7 @@ Module HO_81. tc.compile.goal Goal _ _ :- Goal = {{HO_81.c1 lp:_}}, !, tc.precomp.goal Goal _ Vars, !, - tc.compile.goal.make-pairs Vars Pairs, + tc.compile.make-pairs Vars Pairs, std.assert! (Pairs = []) "", fail. }}. @@ -245,7 +245,7 @@ Module HO_9. Instance i1 A: c1 (fun x => f (A x) (A x)). Qed. Elpi Query TC.Solver lp:{{ - pi F\ sigma T\ decl F `x` {{Type -> Type}} ==> tc.precomp.instance.is-uvar F ==> + pi F\ sigma T\ decl F `x` {{Type -> Type}} ==> tc.precomp.is-uvar F ==> 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". }}. @@ -334,11 +334,11 @@ Module Llam_1. Class B (i: nat -> nat). Elpi Query TC.Solver lp:{{ - @pi-decl `x` {{Type -> Type}} f\ tc.precomp.instance.is-uvar f => - @pi-decl `x` {{Type -> Type}} g\ tc.precomp.instance.is-uvar g => + @pi-decl `x` {{Type -> Type}} f\ tc.precomp.is-uvar f => + @pi-decl `x` {{Type -> Type}} g\ tc.precomp.is-uvar g => sigma T\ 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". + std.assert! (T = app[{{A}}, tc.maybe-eta-tm (fun _ _ (x\ tc.maybe-llam-tm _ _ _ _)) _]) "[TC] invalid precomp". }}. Instance I1: forall F G, B G -> A (fun x => F (G x)). Qed. @@ -515,7 +515,7 @@ Module CoqUvar3. 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]), + Body2 = (x\y\ tc.maybe-llam-tm X [] [Y x y, y] [x,y]), std.assert! (C = Expected) "[TC] invalid compilation". }}. @@ -555,7 +555,7 @@ Module CoqUvar4. tc.precomp.instance {{c1 (fun x y => lp:X (lp:A x y) y)}} C _ _ _, Expected = app [{{c1}}, tc.maybe-eta-tm (fun _ _ Body1) _], Body1 = (x\ tc.maybe-eta-tm (fun _ _ (Body2 x)) [x]), - Body2 = (x\y\ tc.maybe-llam-tm (app [app [X], (Y x y), y]) [y,x]), + Body2 = (x\y\ tc.maybe-llam-tm X [] [Y x y, y] [y,x]), std.assert! (C = Expected) "[TC] invalid compilation". }}. diff --git a/apps/tc/tests/test_pending_mode.v b/apps/tc/tests/test_pending_mode.v index 623f5b143..0bce4b271 100644 --- a/apps/tc/tests/test_pending_mode.v +++ b/apps/tc/tests/test_pending_mode.v @@ -274,4 +274,4 @@ Module force_input_link_HO_var3. Fail Timeout 1 apply _. Abort. -End force_input_link_HO_var3. +End force_input_link_HO_var3. \ No newline at end of file diff --git a/apps/tc/tests/test_proj.v b/apps/tc/tests/test_proj.v new file mode 100644 index 000000000..87f96ec35 --- /dev/null +++ b/apps/tc/tests/test_proj.v @@ -0,0 +1,293 @@ +From elpi Require Import tc. +From elpi Require Import elpi. + +Global Set TC NameShortPath. +Class C (T : Type) := mkC {f : T -> T}. +Class D (T : nat -> nat) := {g : unit}. +Class E (T : nat) := {ge : unit}. +Record r := mkr {car : Type; #[canonical=no] rf : car -> car}. +Canonical Structure c := mkr nat (fun x => x). + + +(* Elpi cs default (r). *) +Elpi cs cs (c). + +Elpi Accumulate TC.Compiler lp:{{ + % the goal is to check instances for C are correctly compiled + func is-class-C prop ->. + is-class-C (pi x\ X x) :- !, pi x\ is-class-C (X x). + is-class-C (tc.instance _ _ _ _) :- !. + :name "is-class-C" + is-class-C (tc.class _ _ _ _) :- !. + is-class-C C :- + coq.error + "Fail to verify the shape of compiled instance." + "Received:\n" C + "\nTo fix the issue either the class is compiled wrongly\n" + "or you forgot to load. A is-class-C rule in the database". + + :before "tc-adder" + tc.add-tc-db _I _G C :- % coq.say "Compiled term is" C, + is-class-C C, fail, !. +}}. + +Module m1. + Elpi Accumulate TC.Compiler lp:{{ + :after "is-class-C" is-class-C (tc-C {{nat}} _) :- !. + }}. + + (* reducing the projection statically *) + Local Instance inst_red: C (car c). now constructor. Qed. + + Elpi Accumulate TC.Compiler lp:{{ + % removing the previous expected (best should be that the previous rule is local to the module) + :after "is-class-C" is-class-C C :- coq.error "FAIL" C, !. + }}. + (* Elpi Print TC.Compiler "elpi.apps.derive.tests/xxx". *) + + Goal C nat. apply _. Qed. + Goal C (car c). apply _. Qed. +End m1. + +Module m1'. + Elpi Accumulate TC.Compiler lp:{{ + % NOTE: rf is not canonical, therefore no reduced nor linked + :after "is-class-C" is-class-C (tc-D {{rf c}} _) :- !. + }}. + + Local Instance inst_red: D (rf c). now constructor. Qed. + + Elpi Accumulate TC.Compiler lp:{{ :after "is-class-C" is-class-C C :- coq.error "FAIL" C, !. }}. + (* NOTE: The failure here is due to delta and beta conversion rules *) + Goal D (fun x => x). Fail apply _. Abort. +End m1'. + +Module m1''. + Elpi Accumulate TC.Compiler lp:{{ + :after "is-class-C" is-class-C (tc-E {{rf c 3}} _) :- !. + }}. + + Local Instance inst_red: E (rf c 3). now constructor. Qed. + Elpi Accumulate TC.Compiler lp:{{ :after "is-class-C" is-class-C C :- coq.error "FAIL" C, !. }}. + + (* NOTE: similarly to previous test, this fails due to delta-beta conv rules *) + Goal E 3. Fail apply _. Abort. +End m1''. + +Module m2. + Elpi Accumulate TC.Compiler lp:{{ + :after "is-class-C" is-class-C (tc-C X (app[_,W]) :- [tc.link.proj CAR X W]) :- !, const CAR = {{:gref car}}, name X. + }}. + + (* cannot reduce the projection: c is quantified *) + Local Instance inst c: C (car c). now constructor. Qed. + Elpi Accumulate TC.Compiler lp:{{ :after "is-class-C" is-class-C C :- coq.error "FAIL" C, !. }}. + + (* need to use the chr *) + Goal C nat. apply _. Qed. + Goal C (car c). apply _. Qed. +End m2. + + +Module m3. + Elpi Accumulate TC.Compiler lp:{{ + :after "is-class-C" is-class-C (tc-C X _) :- !, name X, coq.say K_. + }}. + + (* cannot reduce the projection: c is quantified *) + Local Instance inst X: C X. now constructor. Qed. + Elpi Accumulate TC.Compiler lp:{{ :after "is-class-C" is-class-C C :- coq.error "FAIL" C, !. }}. + + (* need to use the chr *) + Goal C nat. apply _. Qed. + Goal C (car c). apply _. Qed. + (* with local instance for c *) + Goal forall x, C (car x). intros. apply _. Qed. +End m3. + +Module m4. + (* test using primitive projection and parametrized record *) + Set Primitive Projections. + Record ofe (SI : Type) := Ofe { + ofe_car1 :> Type; + ofe_car2 :> Type -> Type; + }. + + Canonical Structure ss := Ofe nat nat (fun x => x). + + Definition p := Ofe nat bool (fun x => x). + + Check (eq_refl : (p.(ofe_car1 _)) = bool). + + Elpi Query TC.Solver lp:{{ + % destruct application with primitive projection + % and retrieving the projector number and the record constant + app[primitive (proj P N), (global (const X))] = {{p.(ofe_car1 _)}}, + % get the body of the constant + coq.env.const X (some (app[H | Args])) XTy, + coq.safe-dest-app XTy _ XTyAg, + % getting the projection of the constant + std.assert! (std.nth N Args {{bool}}) "Invalid proj", + % creating a rocq-term in elpi equivalent to the original one + % but using its canonical projection + coq.env.primitive-projection? P C _, + std.append ([global (const C) | XTyAg]) [global (const X)] RR, + std.assert-ok!(coq.typecheck (app RR) _) "error", + true. + }}. + + (* Elpi Accumulate TC.Compiler lp:{{ + :after "x" expected-rule (tc-C N (app[_, N])) :- !, name N. + }}. *) + + Local Instance inst2 c: C c. now constructor. Qed. + + Goal forall x y, C (@ofe_car1 x y). apply _. Qed. + + Goal forall x y, C (@ofe_car2 x y x). apply _. Qed. +End m4. + +(* Elpi Accumulate TC.Compiler lp:{{ :after "is-class-C" is-class-C _ :- !. }}. *) +Set Printing All. + +Module M. + + Definition fcs1 (H1 H2 : r) := (fun '(x,y) => (rf H1 x, rf H2 y)). + Local Canonical Structure cs1 (H1 H2 H3 : r) := mkr (car H1 * car H2) (fcs1 H1 H2). + + Goal exists x, car x = (nat * nat)%type. + Proof. eexists. auto. Unshelve. apply c. Qed. + + Local Canonical Structure cs2 (T : Type) (c : C T) := mkr T (@f _ c). + + Local Instance i : C bool. apply (mkC _ (fun x => x)). Qed. + + Elpi Accumulate solve_cs lp:{{ + solve (goal _ _ {{@eq lp:T_ lp:P lp:T}} _ _ as G) GL :- + % coq.say "The goal is"G, + P = app [global (const Proj), A], + cs.compiler.cs.compiler ff (pr 0 Proj) A (app[_, T]) [] [] [] R, + % R, coq.say "The rule is"R, + @no-tc! => refine {{eq_refl}} G GL. + }}. + + Goal exists x, car x = bool. + Proof. + eexists. + elpi solve_cs. + Abort. (*TODO:*) +End M. + +Module M1. + Class C (T : Type) := {f : T -> Prop}. + Local Instance i x : C (car x). Admitted. + Goal forall x, C (car x). apply _. Qed. +End M1. + +Module M1'. + Record r A := mkr {car1 : A}. + + Class C (T : Type) := {f : T -> Prop}. + Local Instance i x : C (car1 _ x). Admitted. + Goal forall x, C (car1 _ x). apply _. Qed. +End M1'. + +Module M2. + Inductive to_prop (T: Type) : Prop := tp : T -> to_prop T. + + Record r1 := mkr1 {car : Type; #[canonical=no] rf : C car}. + Local Instance i : C bool. Admitted. + Local Canonical Structure c1 := mkr1 bool i. + Elpi cs cs (c1). + + Goal exists x, to_prop (C (car x)). + Proof. + eexists; constructor. + + apply _. + Qed. +End M2. + +From elpi Require Import cs. + +Elpi CS cs. + +Module M3. + + Set Printing All. + Structure set (T : Type) := MkSet { + set_to_pred : T -> Prop + }. + Arguments set_to_pred : simpl never. + + Class mem T X (x : T) := mkMem { IsMem : set_to_pred _ X x }. + + (* memType is the type of elements of a given set. *) + Module Mem. + Record type T (X : set T) := Pack { elt : T; memP : mem _ X elt }. + End Mem. + + (* Canonical Structure s T X E (I: @mem T X E) := Mem.Pack _ _ _ I. *) + Elpi cs cs (Mem.Pack). + + Section X. + Parameter SN : set nat. + Elpi Trace Browser. + Time Check ((fun x => eq_refl _) : (forall (x : mem nat SN 0), Mem.elt _ SN _ = 0)). + End X. + + (* checking valididy of built rule *) + Elpi Accumulate TC.Compiler lp:{{ :after "is-class-C" is-class-C (tc-mem Ty S T {{@Mem.memP lp:Ty lp:S lp:Z}} :- [tc.link.proj X T Z]) :- !, const X = {{:gref Mem.elt}}. }}. + Existing Instance Mem.memP. + (* Goal forall SN, + mem nat SN 0 -> exists X, Mem.elt _ SN X = 0. + Proof. + intros SN I. + eexists. + (* eexists (Mem.Pack _ _ _ I). *) + apply eq_refl. *) +End M3. + +(* from stdpp/definitions.v *) +Module bv_bool. + Axiom N Z : Type. + Axiom zero : Z. + Axiom two one : N. + Axiom leq lt : Z -> Z -> bool. + Axiom pow : N -> Z -> Z. + Axiom ZofN : N -> Z. + Axiom Is_true : bool -> Prop. + Axiom Zeqdec : forall (x y:Z), sumbool (x = y) (not (x = y)). + + Class Decision (P : Prop) := decide : sumbool P (not P). + + Elpi Accumulate TC.Compiler lp:{{ :after "is-class-C" is-class-C _ :- !. }}. + + Class EqDecision A := + decide_rel x y :: Decision (@eq A x y). + + Definition bool_decide (P : Prop) {dec : Decision P} : bool := + if dec then true else false. + + Definition bv_modulus (n : N) : Z := pow two (ZofN n). + + Class BvWf (n : N) (z : Z) : Prop := + bv_wf : Is_true (andb (leq zero z) (lt z (bv_modulus n))). + + Record bv (n : N) := BV { + bv_unsigned : Z; + bv_is_wf : BvWf n bv_unsigned; + }. + + Axiom bool_to_bv : forall (n : N) (b : bool), bv n. + + Global Instance eq_dec: EqDecision Z := Zeqdec. + + Goal forall x b, Decision (@eq Z (bv_unsigned x (bool_to_bv x b)) zero). + Proof. intros. apply _. Qed. + + Lemma bool_decide_bool_to_bv_0 b: + bool_decide (bv_unsigned _ (bool_to_bv one b) = zero) = negb b. + Abort. + +End bv_bool. diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v index 6781bc8ba..6f9ad9dcf 100644 --- a/apps/tc/theories/add_commands.v +++ b/apps/tc/theories/add_commands.v @@ -13,6 +13,7 @@ From elpi.apps.tc.elpi Extra Dependency "ho_link.elpi" as ho_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. +From elpi.apps.tc.elpi Extra Dependency "cs.elpi" as cs. (* Set Warnings "+elpi". *) @@ -26,6 +27,7 @@ Elpi Accumulate File ho_link. Elpi Accumulate File ho_compile. Elpi Accumulate File compiler1. Elpi Accumulate File modes. +Elpi Accumulate File cs. Elpi Accumulate lp:{{ main L :- args->str-list L L1, diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v index 26ece59d5..78fd2919b 100644 --- a/apps/tc/theories/db.v +++ b/apps/tc/theories/db.v @@ -56,8 +56,7 @@ Elpi Db tc_options.db lp:{{ func is-option-active (func (list string) ->) ->. is-option-active uvar :- !, fail. - is-option-active Opt :- - Opt X, coq.option.get X (coq.option.bool tt). + is-option-active Opt :- Opt X, coq.option.get X (coq.option.bool tt). func warning-name -> string. warning-name "[TC] Warning". @@ -101,6 +100,13 @@ Elpi Db tc.db lp:{{ func link.llam term, term ->. func link.unif-eq term, term ->. + % a goal `p ?X = A` is translated into link.proj «p» X A + % link.proj is deterministic: this unification is deterministic. + % note that link.proj may have tc premises, that can be non deterministic. + % to avoid this issue, we wrap the non-deterministic call in std.once + :index (1 2) + func link.proj constant, term -> term. + } }}. 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 31cc2d4b9..2342b4f39 100644 --- a/apps/tc/theories/tc.v +++ b/apps/tc/theories/tc.v @@ -13,6 +13,7 @@ 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 "solver.elpi" as solver. From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate. +From elpi.apps.tc.elpi Extra Dependency "cs.elpi" as cs. From elpi.apps Require Import db. From elpi.apps Require Export add_commands. @@ -50,13 +51,13 @@ 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 modes. Elpi Accumulate File create_tc_predicate. Elpi Accumulate File solver. +Elpi Accumulate File cs. Elpi Query lp:{{ sigma Options\ tc.all-options Options, @@ -86,6 +87,7 @@ Elpi Accumulate File ho_compile. Elpi Accumulate File unif. Elpi Accumulate File ho_link. Elpi Accumulate File compiler1. +Elpi Accumulate File cs. Elpi Accumulate lp:{{ /* @@ -200,3 +202,28 @@ Set Warnings "elpi". Elpi TC.AddAllClasses. Elpi TC.AddAllInstances. + +Elpi Tactic cs. +Elpi Accumulate Db tc_options.db. +Elpi Accumulate Db tc.db. +Elpi Accumulate File tc_aux. +Elpi Accumulate File ho_precompile. +Elpi Accumulate File ho_compile. +Elpi Accumulate File cs. +Elpi Accumulate lp:{{ + main L :- cs.main L. + + solve G _ :- + cs.solver.solve G. +}}. + +Elpi Tactic solve_cs. +Elpi Accumulate Db tc_options.db. +Elpi Accumulate Db tc.db. +Elpi Accumulate File tc_aux. +Elpi Accumulate File ho_precompile. +Elpi Accumulate File ho_compile. +Elpi Accumulate File cs. +(* Elpi Accumulate lp:{{ + main L :- cs.main L. +}}. *) \ No newline at end of file