From 028d3ed4593655e45d8da2c1689cc056a9704ec4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 7 Dec 2024 15:10:25 +0100 Subject: [PATCH 1/2] fix opam --- coq-elpi.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq-elpi.opam b/coq-elpi.opam index 24e5577d7..f1df1b4b8 100644 --- a/coq-elpi.opam +++ b/coq-elpi.opam @@ -17,7 +17,6 @@ bug-reports: "https://github.com/LPCIC/coq-elpi/issues" depends: [ "dune" {>= "3.13"} "ocaml" {>= "4.10.0"} - "stdlib-shims" "elpi" {>= "2.0.3" & < "2.1.0~"} "coq" {>= "8.20+rc1" & < "8.21~"} "ppx_optcomp" @@ -26,6 +25,7 @@ depends: [ ] build: [ ["dune" "subst"] {dev} + [ make "elpi/dune"] [ "dune" "build" From 650ca3ddb88d50cc66cc8624a82414e62b8b2972 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 7 Dec 2024 16:41:20 +0100 Subject: [PATCH 2/2] put the eqb ast into a namespace --- apps/derive/elpi/eqType.elpi | 98 ++++++++++++------------ apps/derive/elpi/eqb.elpi | 56 +++++++------- apps/derive/elpi/eqbOK.elpi | 12 +-- apps/derive/elpi/eqbcorrect.elpi | 52 ++++++------- apps/derive/elpi/fields.elpi | 62 +++++++-------- apps/derive/theories/derive/eqType_ast.v | 30 ++++---- 6 files changed, 155 insertions(+), 155 deletions(-) diff --git a/apps/derive/elpi/eqType.elpi b/apps/derive/elpi/eqType.elpi index 1e83dfdbf..8737d5acf 100644 --- a/apps/derive/elpi/eqType.elpi +++ b/apps/derive/elpi/eqType.elpi @@ -4,82 +4,82 @@ namespace derive.eqType.ast { -pred translate-indt i:inductive, o:eqType, o:diagnostic. +pred translate-indt i:inductive, o:eqb.eqType, o:diagnostic. translate-indt I O D :- coq.env.indt-decl I Decl, coq.env.indt I _ _ _ _ KN _, translate-param Decl I KN O D. -pred translate-param i:indt-decl, i:inductive, i:list constructor, o:eqType, o:diagnostic. -translate-param (parameter ID _ Ty F) I KS (type-param F1) D :- whd Ty [] {{ Type }} _, !, +pred translate-param i:indt-decl, i:inductive, i:list constructor, o:eqb.eqType, o:diagnostic. +translate-param (parameter ID _ Ty F) I KS (eqb.type-param F1) D :- whd Ty [] {{ Type }} _, !, @pi-parameter ID Ty x\ pi y\ term->trm x y ok => translate-param (F x) I KS (F1 y) D. -translate-param (parameter ID _ Ty F) I KS (value-param Ty1 F1) D :- term->trm Ty Ty1 ok, !, +translate-param (parameter ID _ Ty F) I KS (eqb.value-param Ty1 F1) D :- term->trm Ty Ty1 ok, !, @pi-parameter ID Ty x\ pi y\ term->trm x y ok => translate-param (F x) I KS (F1 y) D. translate-param (parameter ID _ _ _) _ _ _ (error S) :- S is "unsupported parameter " ^ ID. -translate-param (inductive ID tt (arity (sort S)) F) I KS (inductive I F1) D :- +translate-param (inductive ID tt (arity (sort S)) F) I KS (eqb.inductive I F1) D :- @pi-inductive ID (arity (sort S)) x\ pi y\ term->trm x y ok => translate-constructors (F x) KS (F1 y) D. -translate-param (record _ _ _ F) I [K] (inductive I (y\ [constructor K (F1 y)])) D :- !, +translate-param (record _ _ _ F) I [K] (eqb.inductive I (y\ [eqb.constructor K (F1 y)])) D :- !, pi y\ self y => translate-record-constructor F (F1 y) D. translate-param _ _ _ _ (error S) :- S is "unsupported inductive arity". -pred translate-constructors i:list indc-decl, i:list constructor, o:list constructor, o:diagnostic. +pred translate-constructors i:list indc-decl, i:list constructor, o:list eqb.constructor, o:diagnostic. translate-constructors [] [] [] ok. -translate-constructors [constructor _ A|KS] [K|KK] [constructor K Args|KS1] D :- std.do-ok! D [ +translate-constructors [constructor _ A|KS] [K|KK] [eqb.constructor K Args|KS1] D :- std.do-ok! D [ translate-arguments {coq.arity->term A} Args, translate-constructors KS KK KS1, ]. -pred translate-arguments i:term, o:arguments, o:diagnostic. +pred translate-arguments i:term, o:eqb.arguments, o:diagnostic. translate-arguments T T2 D :- whd1 T T1, !, translate-arguments T1 T2 D. -translate-arguments (prod N Ty F) (irrelevant Ty1 F1) D :- not(pi x\ occurs x (F x)), irrelevant? Ty Ty1 ok, !, +translate-arguments (prod N Ty F) (eqb.irrelevant Ty1 F1) D :- not(pi x\ occurs x (F x)), irrelevant? Ty Ty1 ok, !, @pi-decl N Ty x\ translate-arguments (F x) F1 D. -translate-arguments (prod N Ty F) (regular Ty1 F1) D :- not(pi x\ occurs x (F x)), !, std.do-ok! D [ +translate-arguments (prod N Ty F) (eqb.regular Ty1 F1) D :- not(pi x\ occurs x (F x)), !, std.do-ok! D [ term->trm Ty Ty1, (d\ @pi-decl N Ty x\ translate-arguments (F x) F1 d), ]. -translate-arguments (prod N Ty F) (dependent Ty1 F1) D :- !, std.do-ok! D [ +translate-arguments (prod N Ty F) (eqb.dependent Ty1 F1) D :- !, std.do-ok! D [ term->trm Ty Ty1, (d\ @pi-decl N Ty x\ pi y\ term->trm x y ok => translate-arguments (F x) (F1 y) d), ]. -translate-arguments Ty (stop Ty1) D :- name Ty, term->trm Ty Ty1 D. -translate-arguments (app [N|_] as Ty) (stop Ty1) D :- name N, term->trm Ty Ty1 D. +translate-arguments Ty (eqb.stop Ty1) D :- name Ty, term->trm Ty Ty1 D. +translate-arguments (app [N|_] as Ty) (eqb.stop Ty1) D :- name N, term->trm Ty Ty1 D. translate-arguments T _ (error S) :- S is "unsupported argument " ^ {coq.term->string T}. -pred translate-record-constructor i:record-decl, o:arguments, o:diagnostic. -translate-record-constructor end-record (stop X) ok :- self X. -translate-record-constructor (field _ ID Ty F) (irrelevant Ty1 F1) D :- not(pi x\ occurs x (F x)), irrelevant? Ty Ty1 ok, !, +pred translate-record-constructor i:record-decl, o:eqb.arguments, o:diagnostic. +translate-record-constructor end-record (eqb.stop X) ok :- self X. +translate-record-constructor (field _ ID Ty F) (eqb.irrelevant Ty1 F1) D :- not(pi x\ occurs x (F x)), irrelevant? Ty Ty1 ok, !, @pi-parameter ID Ty x\ translate-record-constructor (F x) F1 D. -translate-record-constructor (field _ ID Ty F) (regular Ty1 F1) D :- not(pi x\ occurs x (F x)), !, std.do-ok! D [ +translate-record-constructor (field _ ID Ty F) (eqb.regular Ty1 F1) D :- not(pi x\ occurs x (F x)), !, std.do-ok! D [ term->trm Ty Ty1, (d\ @pi-parameter ID Ty x\ translate-record-constructor (F x) F1 d), ]. -translate-record-constructor (field _ ID Ty F) (dependent Ty1 F1) D :- !, std.do-ok! D [ +translate-record-constructor (field _ ID Ty F) (eqb.dependent Ty1 F1) D :- !, std.do-ok! D [ term->trm Ty Ty1, (d\ @pi-parameter ID Ty x\ pi y\ term->trm x y ok => translate-record-constructor (F x) (F1 y) d), ]. translate-record-constructor (field _ ID _ _) _ (error S) :- S is "unsupported record field " ^ ID. -pred self o:trm. +pred self o:eqb.trm. -pred valid i:trm, o:diagnostic. -valid {{ PrimInt63.int }} ok :- !. -valid (global (indt I)) ok :- eqType I _, !. -valid (app (indt I) A Args) D :- eqType I EQT, !, valid-eqType EQT [A|Args] D. +pred valid i:eqb.trm, o:diagnostic. +valid (eqb.global X) ok :- global X = {{ PrimInt63.int }}, !. +valid (eqb.global (indt I)) ok :- eqType I _, !. +valid (eqb.app (indt I) A Args) D :- eqType I EQT, !, valid-eqType EQT [A|Args] D. valid T (error S) :- S is "not an eqType: " ^ {std.any->string T}. -pred valid-eqType i:eqType, i:list trm, o:diagnostic. -valid-eqType (inductive _ _) [] ok. -valid-eqType (type-param F) [T|TS] D :- std.do-ok! D [ +pred valid-eqType i:eqb.eqType, i:list eqb.trm, o:diagnostic. +valid-eqType (eqb.inductive _ _) [] ok. +valid-eqType (eqb.type-param F) [T|TS] D :- std.do-ok! D [ valid T, (d\ pi x\ valid-eqType (F x) TS d), ]. -valid-eqType (value-param _ F) [_|TS] D :- std.do-ok! D [ +valid-eqType (eqb.value-param _ F) [_|TS] D :- std.do-ok! D [ (d\ pi x\ valid-eqType (F x) TS d), ]. -pred irrelevant? i:term, o:trm, o:diagnostic. -irrelevant? (app [{{ @eq }}, global (indt EqType), A, B]) (app EQ EQTYPE [A1,B1]) D :- std.do-ok! D [ +pred irrelevant? i:term, o:eqb.trm, o:diagnostic. +irrelevant? (app [{{ @eq }}, global (indt EqType), A, B]) (eqb.app EQ EQTYPE [A1,B1]) D :- std.do-ok! D [ std.lift-ok (eqType EqType _) "Not an eqType", %eqb-for Bool Bool _, std.lift-ok ({{ @eq }} = global EQ) "", term->trm (global (indt EqType)) EQTYPE, @@ -88,17 +88,17 @@ irrelevant? (app [{{ @eq }}, global (indt EqType), A, B]) (app EQ EQTYPE [A1,B1] ]. irrelevant? T R D :- whd1 T T1, coq.say "whd" T T1, irrelevant? T1 R D. -pred term->trm i:term, o:trm, o:diagnostic. -term->trm (global GR) (global GR) ok :- !. -term->trm (app [global GRF,A|As]) (app GRF A1 As1) D :- !, std.do-ok! D [ +pred term->trm i:term, o:eqb.trm, o:diagnostic. +term->trm (global GR) (eqb.global GR) ok :- !. +term->trm (app [global GRF,A|As]) (eqb.app GRF A1 As1) D :- !, std.do-ok! D [ term->trm A A1, map-ok! As term->trm As1, ]. -term->trm {{ lp:A -> lp:B }} (app {{:gref lib:elpi.derive.arrow }} A1 [B1]) D :- std.do-ok! D [ +term->trm {{ lp:A -> lp:B }} (eqb.app {{:gref lib:elpi.derive.arrow }} A1 [B1]) D :- std.do-ok! D [ term->trm A A1, term->trm B B1, ]. -term->trm (app [N|As]) (app {{:gref lib:elpi.derive.apply }} N1 As1) D :- name N, !, std.do-ok! D [ +term->trm (app [N|As]) (eqb.app {{:gref lib:elpi.derive.apply }} N1 As1) D :- name N, !, std.do-ok! D [ term->trm N N1, map-ok! As term->trm As1, ]. @@ -108,28 +108,28 @@ pred map-ok! i:list A, i:(A -> B -> diagnostic -> prop), o:list B, o:diagnostic. map-ok! [] _ [] ok. map-ok! [X|XS] F [Y|YS] D :- F X Y D1, if (D1 = ok) (map-ok! XS F YS D) (D = D1). -pred validate-eqType i:eqType, o:diagnostic. -validate-eqType (type-param F) D :- pi x\ valid x ok => validate-eqType (F x) D. -validate-eqType (value-param _ F) D :- +pred validate-eqType i:eqb.eqType, o:diagnostic. +validate-eqType (eqb.type-param F) D :- pi x\ valid x ok => validate-eqType (F x) D. +validate-eqType (eqb.value-param _ F) D :- pi x\ validate-eqType (F x) D. -validate-eqType (inductive _ F) D :- +validate-eqType (eqb.inductive _ F) D :- pi x\ valid x ok => validate-constructors (F x) D. -pred validate-constructors i:list constructor, o:diagnostic. +pred validate-constructors i:list eqb.constructor, o:diagnostic. validate-constructors [] ok. -validate-constructors [constructor _ Args|Ks] D :- std.do-ok! D [ +validate-constructors [eqb.constructor _ Args|Ks] D :- std.do-ok! D [ validate-arguments Args, validate-constructors Ks ]. -pred validate-arguments i:arguments, o:diagnostic. -validate-arguments (stop _) ok. -validate-arguments (regular T Args) D :- std.do-ok! D [ +pred validate-arguments i:eqb.arguments, o:diagnostic. +validate-arguments (eqb.stop _) ok. +validate-arguments (eqb.regular T Args) D :- std.do-ok! D [ valid T, validate-arguments Args, ]. -validate-arguments (irrelevant _ Args) D :- validate-arguments Args D. -validate-arguments (dependent T Args) D :- std.do-ok! D [ +validate-arguments (eqb.irrelevant _ Args) D :- validate-arguments Args D. +validate-arguments (eqb.dependent T Args) D :- std.do-ok! D [ valid T, (d\ pi x\ validate-arguments (Args x) d), ]. @@ -145,9 +145,9 @@ main I [C] :- namespace feqb { -pred trm->term i:trm, o:term. -trm->term (global GR) (global GR) :- !. -trm->term (app GR A AS) (app[global GR,A1|AS1]) :- !, +pred trm->term i:eqb.trm, o:term. +trm->term (eqb.global GR) (global GR) :- !. +trm->term (eqb.app GR A AS) (app[global GR,A1|AS1]) :- !, trm->term A A1, std.map AS trm->term AS1. trm->term T _ :- coq.error "cannot translate trm" T "to term, did you forget to assume feqb.trm->term ?". diff --git a/apps/derive/elpi/eqb.elpi b/apps/derive/elpi/eqb.elpi index a97671577..620fdc1a1 100644 --- a/apps/derive/elpi/eqb.elpi +++ b/apps/derive/elpi/eqb.elpi @@ -2,7 +2,7 @@ /* license: GNU Lesser General Public License Version 2.1 or later */ /* ------------------------------------------------------------------------- */ -type feqb.trm->term trm -> term -> prop. +type feqb.trm->term eqb.trm -> term -> prop. macro @pi-trm N T F :- pi x xx\ decl x N T => (feqb.trm->term xx x :- !) => F xx x. @@ -46,21 +46,21 @@ derive.eqb.main (const C) Prefix CL :- std.do! [ namespace derive.eqb.eqb { % ----------------------------------------------------------------------------- -pred main i:eqType, i:eqType, i:list term, i:list term, i:term, o:term. +pred main i:eqb.eqType, i:eqb.eqType, i:list term, i:list term, i:term, o:term. -main (type-param FI) (type-param FJ) PI PJ EF {{ fun (x : Type) (eqx : x -> x -> bool) => lp:(R x eqx) }} :- +main (eqb.type-param FI) (eqb.type-param FJ) PI PJ EF {{ fun (x : Type) (eqx : x -> x -> bool) => lp:(R x eqx) }} :- @pi-trm `x` {{ Type }} y\x\ @pi-decl `eqx` {{ lp:x -> lp:x -> bool }} eqx\ main (FI y) (FJ y) [x|PI] [x|PJ] {coq.mk-app EF [x,eqx]} (R x eqx). -main (value-param TYI FI) (value-param TYJ FJ) PI PJ EF {{ fun (x : lp:TI) (y : lp:TJ) => lp:(R x y) }} :- +main (eqb.value-param TYI FI) (eqb.value-param TYJ FJ) PI PJ EF {{ fun (x : lp:TI) (y : lp:TJ) => lp:(R x y) }} :- feqb.trm->term TYI TI, feqb.trm->term TYJ TJ, @pi-trm `x` TI xx\x\ @pi-trm `y` TJ yy\y\ main (FI xx) (FJ yy) [x|PI] [y|PJ] {coq.mk-app EF [x,y]} (R x y). -main (inductive Ind _) (inductive Ind _) PI PJ EF {{ fix rec (x1 : lp:I) (x2 : lp:J) {struct x1} : bool := lp:(R rec x1 x2) }} :- coq.env.recursive? Ind, !, +main (eqb.inductive Ind _) (eqb.inductive Ind _) PI PJ EF {{ fix rec (x1 : lp:I) (x2 : lp:J) {struct x1} : bool := lp:(R rec x1 x2) }} :- coq.env.recursive? Ind, !, coq.mk-app (global (indt Ind)) {std.rev PI} I, coq.mk-app (global (indt Ind)) {std.rev PJ} J, @pi-decl `rec` {{ lp:I -> lp:J -> bool }} rec\ @@ -68,7 +68,7 @@ main (inductive Ind _) (inductive Ind _) PI PJ EF {{ fix rec (x1 : lp:I) (x2 : l @pi-decl `x2` J x2\ do-match x1 I x2 J {coq.mk-app EF [rec]} (R rec x1 x2). -main (inductive Ind _) (inductive Ind _) PI PJ EF {{ fun (x1 : lp:I) (x2 : lp:J) => lp:(R x1 x2) }} :- +main (eqb.inductive Ind _) (eqb.inductive Ind _) PI PJ EF {{ fun (x1 : lp:I) (x2 : lp:J) => lp:(R x1 x2) }} :- coq.mk-app (global (indt Ind)) {std.rev PI} I, coq.mk-app (global (indt Ind)) {std.rev PJ} J, @pi-decl `x1` I x1\ @@ -102,17 +102,17 @@ do-branch X2 J F K KTY Vars _ {{ @eqb_core_defs.eqb_body _ _ _ _ lp:FLDP lp:F lp % ----------------------------------------------------------------------------- % example: eqb-for {{ list lp:A }} {{ @list_eqb lp:A lp:F }} :- eqb-for A F. -pred do-clause i:eqType, i:eqType, i:list term, i:list term, i:term, i:list prop, o:prop. +pred do-clause i:eqb.eqType, i:eqb.eqType, i:list term, i:list term, i:term, i:list prop, o:prop. -do-clause (type-param AI) (type-param AJ) PI PJ F Todo (pi a ea\ C a ea) :- !, +do-clause (eqb.type-param AI) (eqb.type-param AJ) PI PJ F Todo (pi a ea\ C a ea) :- !, pi x a ea\ do-clause (AI x) (AJ x) [a|PI] [a|PJ] {coq.mk-app F [a,ea]} [eqb-for a a ea|Todo] (C a ea). -do-clause (value-param _ AI) (value-param _ AJ) PI PJ F Todo (pi a b\ C a b) :- !, +do-clause (eqb.value-param _ AI) (eqb.value-param _ AJ) PI PJ F Todo (pi a b\ C a b) :- !, pi x a b\ do-clause (AI x) (AJ x) [a|PI] [b|PJ] {coq.mk-app F [a,b]} Todo (C a b). -do-clause (inductive Ind _) (inductive Ind _) PI PJ F Todo (eqb-for I J F :- Todo) :- +do-clause (eqb.inductive Ind _) (eqb.inductive Ind _) PI PJ F Todo (eqb-for I J F :- Todo) :- coq.mk-app (global (indt Ind)) {std.rev PI} I, coq.mk-app (global (indt Ind)) {std.rev PJ} J. @@ -122,22 +122,22 @@ do-clause (inductive Ind _) (inductive Ind _) PI PJ F Todo (eqb-for I J F :- Tod namespace derive.eqb.eqbf { % ----------------------------------------------------------------------------- -pred main i:eqType, i:eqType, i:list term, i:list term, o:term. +pred main i:eqb.eqType, i:eqb.eqType, i:list term, i:list term, o:term. -main (type-param FI) (type-param FJ) PI PJ {{ fun (p : Type) (eqp : p -> p -> bool) => lp:(R p eqp) }} :- +main (eqb.type-param FI) (eqb.type-param FJ) PI PJ {{ fun (p : Type) (eqp : p -> p -> bool) => lp:(R p eqp) }} :- @pi-trm `P` {{ Type }} x\p\ @pi-decl `eqP` {{ lp:p -> lp:p -> bool }} eqP\ eqb-for p p eqP => main (FI x) (FJ x) [p|PI] [p|PJ] (R p eqP). -main (value-param TYI FI) (value-param TYJ FJ) PI PJ {{ fun (x y : lp:T) => lp:(R x y) }} :- +main (eqb.value-param TYI FI) (eqb.value-param TYJ FJ) PI PJ {{ fun (x y : lp:T) => lp:(R x y) }} :- feqb.trm->term TYI TI, feqb.trm->term TYJ TJ, @pi-trm `P` TI xx\x\ @pi-trm `P` TJ yy\y\ main (FI xx) (FJ yy) [x|PI] [y|PJ] (R x y). -main (inductive Ind F) (inductive Ind G) PI PJ {{ fun (rec : lp:I -> lp:J -> bool) (x : positive) => lp:(R rec x) }} :- std.do! [ +main (eqb.inductive Ind F) (eqb.inductive Ind G) PI PJ {{ fun (rec : lp:I -> lp:J -> bool) (x : positive) => lp:(R rec x) }} :- std.do! [ std.rev PI ParamsI, std.rev PJ ParamsJ, coq.mk-app (global (indt Ind)) ParamsI I, @@ -160,15 +160,15 @@ pred rty i:term, i:term, i:term, o:term. rty Fields_t_I Fields_t_J X {{ lp:Fields_t_I lp:X -> lp:Fields_t_J lp:X -> bool }}. % ----------------------------------------------------------------------------- -pred fields i:list term, i:list term, i:pair constructor constructor, o:term. +pred fields i:list term, i:list term, i:pair eqb.constructor eqb.constructor, o:term. -fields ParamsI ParamsJ (pr (constructor K (stop _)) (constructor K (stop _))) {{ fun (a : lp:BoxTy1) (b : lp:BoxTy2) => true }} :- std.do! [ +fields ParamsI ParamsJ (pr (eqb.constructor K (eqb.stop _)) (eqb.constructor K (eqb.stop _))) {{ fun (a : lp:BoxTy1) (b : lp:BoxTy2) => true }} :- std.do! [ std.assert! (box-for K IB _) "derive.eqb: run derive.fields before", coq.mk-app (global (indt IB)) ParamsI BoxTy1, coq.mk-app (global (indt IB)) ParamsJ BoxTy2, ]. -fields ParamsI ParamsJ (pr (constructor K Args) (constructor K Args2)) {{ fun (a : lp:BoxTy1) (b : lp:BoxTy2) => lp:(R a b) }} :- std.do! [ +fields ParamsI ParamsJ (pr (eqb.constructor K Args) (eqb.constructor K Args2)) {{ fun (a : lp:BoxTy1) (b : lp:BoxTy2) => lp:(R a b) }} :- std.do! [ std.assert! (box-for K IB _) "derive.eqb: run derive.fields before", coq.mk-app (global (indt IB)) ParamsI BoxTy1, coq.mk-app (global (indt IB)) ParamsJ BoxTy2, @@ -180,14 +180,14 @@ fields ParamsI ParamsJ (pr (constructor K Args) (constructor K Args2)) {{ fun (a pred fields.rty1 i:term, i:list term, i:list term, o:term. fields.rty1 _ _ _ {{ bool }}. -pred fields.branch1 i:term, i:term, i:arguments, i:arguments, i:term, i:term, i:list term, i:list term, o:term. +pred fields.branch1 i:term, i:term, i:eqb.arguments, i:eqb.arguments, i:term, i:term, i:list term, i:list term, o:term. fields.branch1 B BoxTy2 Args Args2 _ _ VarsA _ R :- coq.build-match B BoxTy2 fields.rty2 (fields.branch2 Args Args2 VarsA) R. pred fields.rty2 i:term, i:list term, i:list term, o:term. fields.rty2 _ _ _ {{ bool }}. -pred fields.branch2 i:arguments, i:arguments, i:list term, i:term, i:term, i:list term, i:list term, o:term. +pred fields.branch2 i:eqb.arguments, i:eqb.arguments, i:list term, i:term, i:term, i:list term, i:list term, o:term. fields.branch2 Args Args2 VarsA _ _ VarsB _ R :- fields.aux Args Args2 VarsA VarsB R. @@ -198,9 +198,9 @@ mk-eqb-for T1 _ _ :- Msg is "derive.eqb: missing boolean equality for " ^ {coq.term->string T1} ^ ", maybe use derive.eqb first", stop Msg. -pred fields.aux i:arguments, i:arguments, i:list term, i:list term, o:term. +pred fields.aux i:eqb.arguments, i:eqb.arguments, i:list term, i:list term, o:term. -fields.aux (dependent TYX FX) (dependent TYY FY) [X|XS] [Y|YS] {{ lib:elpi.andb (lp:EQB lp:X lp:Y) lp:R1 }} :- +fields.aux (eqb.dependent TYX FX) (eqb.dependent TYY FY) [X|XS] [Y|YS] {{ lib:elpi.andb (lp:EQB lp:X lp:Y) lp:R1 }} :- feqb.trm->term TYX TX, feqb.trm->term TYY TY, mk-eqb-for TX TY EQB, @@ -209,31 +209,31 @@ fields.aux (dependent TYX FX) (dependent TYY FY) [X|XS] [Y|YS] {{ lib:elpi.andb fields.aux (FX a) (FY b) XS YS (R n m)), R1 = R X Y. -fields.aux (regular TYX FX) (regular TYY FY) [X|XS] [Y|YS] {{ lib:elpi.andb (lp:EQB lp:X lp:Y) lp:R }} :- +fields.aux (eqb.regular TYX FX) (eqb.regular TYY FY) [X|XS] [Y|YS] {{ lib:elpi.andb (lp:EQB lp:X lp:Y) lp:R }} :- feqb.trm->term TYX TX, feqb.trm->term TYY TY, mk-eqb-for TX TY EQB, fields.aux FX FY XS YS R. -fields.aux (irrelevant _ FX) (irrelevant _ FY) [_|XS] [_|YS] R :- fields.aux FX FY XS YS R. +fields.aux (eqb.irrelevant _ FX) (eqb.irrelevant _ FY) [_|XS] [_|YS] R :- fields.aux FX FY XS YS R. -fields.aux (stop _) (stop _) [] [] {{ true }}. +fields.aux (eqb.stop _) (eqb.stop _) [] [] {{ true }}. % ----------------------------------------------------------------------------- % example: % eqb-fields {{ list lp:A }} {{ @list_eqb_fields lp:A lp:EA lp:ELA }} :- % eqb-for A EA, eqb-for {{ list lp:A }} ELA. -pred do-clause i:eqType, i:eqType, i:list term, i:list term, i:term, i:list prop, o:prop. +pred do-clause i:eqb.eqType, i:eqb.eqType, i:list term, i:list term, i:term, i:list prop, o:prop. -do-clause (type-param AI) (type-param AJ) PI PJ F Todo (pi a ea\ C a ea) :- !, +do-clause (eqb.type-param AI) (eqb.type-param AJ) PI PJ F Todo (pi a ea\ C a ea) :- !, pi x a ea\ do-clause (AI x) (AJ x) [a|PI] [a|PJ] {coq.mk-app F [a,ea]} [eqb-for a a ea|Todo] (C a ea). -do-clause (value-param _ AI) (value-param _ AJ) PI PJ F Todo (pi a b\ C a b) :- !, +do-clause (eqb.value-param _ AI) (eqb.value-param _ AJ) PI PJ F Todo (pi a b\ C a b) :- !, pi x a b\ do-clause (AI x) (AJ x) [a|PI] [b|PJ] {coq.mk-app F [a,b]} Todo (C a b). -do-clause (inductive Ind _) (inductive Ind _) PI PJ F Todo (pi ela\ eqb-fields I J (F1 ela) :- [C ela|Todo]) :- !, +do-clause (eqb.inductive Ind _) (eqb.inductive Ind _) PI PJ F Todo (pi ela\ eqb-fields I J (F1 ela) :- [C ela|Todo]) :- !, coq.mk-app (global (indt Ind)) {std.rev PI} I, coq.mk-app (global (indt Ind)) {std.rev PJ} J, pi ela\ diff --git a/apps/derive/elpi/eqbOK.elpi b/apps/derive/elpi/eqbOK.elpi index a997d72e5..b31683c17 100644 --- a/apps/derive/elpi/eqbOK.elpi +++ b/apps/derive/elpi/eqbOK.elpi @@ -3,15 +3,15 @@ /* ------------------------------------------------------------------------- */ -type feqb.trm->term trm -> term -> prop. +type feqb.trm->term eqb.trm -> term -> prop. macro @pi-trm N T F :- pi x xx\ decl x N T => (feqb.trm->term xx x :- !) => F xx x. namespace derive.eqbOK { -pred add-reflect i:eqType, i:term, i:term, o:term. -add-reflect (type-param F) Correct Refl {{ +pred add-reflect i:eqb.eqType, i:term, i:term, o:term. +add-reflect (eqb.type-param F) Correct Refl {{ fun (a : lp:Type) (eqA: a -> a -> bool) (heqA : lp:(HeqA a eqA)) => lp:(R a eqA heqA) }} :- Type = sort (typ {coq.univ.new}), @@ -23,14 +23,14 @@ add-reflect (type-param F) Correct Refl {{ {{lp:Correct lp:a lp:eqA (fun (a1 a2 : lp:a) => @elimT (@eq lp:a a1 a2) (lp:eqA a1 a2) (lp:heqA a1 a2))}} {{lp:Refl lp:a lp:eqA (fun (a1: lp:a) => @introT (@eq lp:a a1 a1) (lp:eqA a1 a1) (lp:heqA a1 a1) (@refl_equal lp:a a1))}} (R a eqA heqA). -add-reflect (value-param TY F) Correct Refl {{ fun x : lp:Ty => lp:(R x) }} :- +add-reflect (eqb.value-param TY F) Correct Refl {{ fun x : lp:Ty => lp:(R x) }} :- feqb.trm->term TY Ty, @pi-trm `x` Ty xx\x\ add-reflect (F xx) {{lp:Correct lp:x}} {{lp:Refl lp:x}} (R x). -add-reflect (inductive _ _) Correct Refl {{iffP2 lp:Correct lp:Refl}}. +add-reflect (eqb.inductive _ _) Correct Refl {{iffP2 lp:Correct lp:Refl}}. pred main i:gref, i:string, o:list prop. main (indt I) Prefix [CL] :- std.do! [ @@ -51,7 +51,7 @@ main (indt I) Prefix [CL] :- std.do! [ main (const C) Prefix [CL] :- std.do! [ std.assert! (eqb-for (global (const C)) (global (const C)) F) "run eqb before", std.assert! (eqcorrect-for (const C) Correct Refl) "run eqbcorrect before", - add-reflect (inductive _ _) (global (const Correct)) (global (const Refl)) Breflect, + add-reflect (eqb.inductive _ _) (global (const Correct)) (global (const Refl)) Breflect, std.assert-ok! (coq.typecheck Breflect _) "eqbOK generates illtyped term", coq.ensure-fresh-global-id (Prefix ^ "eqb_OK") Namerf, diff --git a/apps/derive/elpi/eqbcorrect.elpi b/apps/derive/elpi/eqbcorrect.elpi index 5b72c7a4b..be7de60f4 100644 --- a/apps/derive/elpi/eqbcorrect.elpi +++ b/apps/derive/elpi/eqbcorrect.elpi @@ -2,16 +2,16 @@ /* license: GNU Lesser General Public License Version 2.1 or later */ /* ------------------------------------------------------------------------- */ -type feqb.trm->term trm -> term -> prop. +type feqb.trm->term eqb.trm -> term -> prop. macro @pi-trm N T F :- pi x xx\ decl x N T => (feqb.trm->term xx x :- !) => F xx x. namespace derive.eqbcorrect { -pred has-params? i:eqType. -has-params? (type-param _). -has-params? (value-param _ _). +pred has-params? i:eqb.eqType. +has-params? (eqb.type-param _). +has-params? (eqb.value-param _ _). % use: % config Pred Pred_on Pred_body Solver Db @@ -102,7 +102,7 @@ main (indc _) _ _ :- stop "derive.eqbcorrect does not work on a constructor". pred search-eqcorrect-for i:term, o:term, o:term. search-eqcorrect-for (global (indt I)) (global (const C)) (global (const R)) :- - std.assert! (eqType I (inductive _ _)) "unknown or not applied enough type", + std.assert! (eqType I (eqb.inductive _ _)) "unknown or not applied enough type", eqcorrect-for (indt I) C R. search-eqcorrect-for (app[global (indt I)|Args]) CArgs RArgs :- @@ -110,15 +110,15 @@ search-eqcorrect-for (app[global (indt I)|Args]) CArgs RArgs :- eqcorrect-for (indt I) C R, search-eqcorrect-apply F Args (global (const C)) (global (const R)) CArgs RArgs. -pred search-eqcorrect-apply i:eqType, i:list term, i:term, i:term, o:term, o:term. -search-eqcorrect-apply (type-param F) [T|Args] C R C1 R1 :- +pred search-eqcorrect-apply i:eqb.eqType, i:list term, i:term, i:term, o:term, o:term. +search-eqcorrect-apply (eqb.type-param F) [T|Args] C R C1 R1 :- search-eqcorrect-for T CT RT, pi x\ search-eqcorrect-apply (F x) Args {coq.mk-app C [T,_,CT]} {coq.mk-app R [T,_,RT]} C1 R1. -search-eqcorrect-apply (value-param _ F) [T|Args] C R C1 R1 :- +search-eqcorrect-apply (eqb.value-param _ F) [T|Args] C R C1 R1 :- pi x\ search-eqcorrect-apply (F x) Args {coq.mk-app C [T]} {coq.mk-app R [T]} C1 R1. -search-eqcorrect-apply (inductive _ _) [] C R C R. +search-eqcorrect-apply (eqb.inductive _ _) [] C R C R. %--------------------------------------------------------------------------- @@ -141,8 +141,8 @@ pred common-body o:term. pred fields-t o:term, o:term, o:term, o:term. %--------------------------------------------------------------------------- -pred common i:eqType, i:list term, i:term, o:term. -common (type-param F) Params Ind O :- std.do! [ +pred common i:eqb.eqType, i:list term, i:term, o:term. +common (eqb.type-param F) Params Ind O :- std.do! [ config Pred Pred_on _Pred_body _Solver Db, O = {{ fun (a : lp:Type) (eqA : a -> a -> bool) (eqAc : lp:Pred a eqA) => lp:(R a eqA eqAc) }}, Type = sort (typ {coq.univ.new}), @@ -158,7 +158,7 @@ common (type-param F) Params Ind O :- std.do! [ (R a eqA eqAc) ]. -common (value-param TY F) Params Ind O :- std.do! [ +common (eqb.value-param TY F) Params Ind O :- std.do! [ feqb.trm->term TY T, O = {{ fun (a : lp:T) => lp:(R a) }}, mk-reali T TR, @@ -170,7 +170,7 @@ common (value-param TY F) Params Ind O :- std.do! [ (R a) ]. -common (inductive I Ks) ParamsRev Ind O :- std.do! [ +common (eqb.inductive I Ks) ParamsRev Ind O :- std.do! [ config _Pred Pred_on Pred_body _Solver Db, std.rev ParamsRev Params, coq.mk-app (global (indt I)) Params Ty, @@ -207,8 +207,8 @@ common (inductive I Ks) ParamsRev Ind O :- std.do! [ %--------------------------------------------------------------------------- -pred common-aux i:eqType, i:list term, i:term, o:term. -common-aux (type-param F) Params Ind O :- std.do! [ +pred common-aux i:eqb.eqType, i:list term, i:term, o:term. +common-aux (eqb.type-param F) Params Ind O :- std.do! [ config _Pred Pred_on _Pred_body _Solver Db, O = {{ fun (a : lp:Type) (eqA : a -> a -> bool) => lp:(R a eqA) }}, Type = sort (typ {coq.univ.new}), @@ -222,7 +222,7 @@ common-aux (type-param F) Params Ind O :- std.do! [ (R a eqA) ]. -common-aux (value-param TY F) Params Ind O :- std.do! [ +common-aux (eqb.value-param TY F) Params Ind O :- std.do! [ feqb.trm->term TY T, O = {{ fun (a : lp:T) (pa : lp:TR a) => lp:(R a pa) }}, mk-reali T TR, @@ -233,7 +233,7 @@ common-aux (value-param TY F) Params Ind O :- std.do! [ {{ lp:Ind lp:a lp:pa }} (R a pa) ]. -common-aux (inductive I Ks) ParamsRev Ind O :- std.do! [ +common-aux (eqb.inductive I Ks) ParamsRev Ind O :- std.do! [ config _Pred Pred_on Pred_body _Solver Db, std.rev ParamsRev Params, coq.mk-app (global (indt I)) Params Ty, @@ -258,13 +258,13 @@ common-aux (inductive I Ks) ParamsRev Ind O :- std.do! [ %--------------------------------------------------------------------------- -pred branch i:list term, i:constructor, o:term. -branch Params (constructor K Args) R :- +pred branch i:list term, i:eqb.constructor, o:term. +branch Params (eqb.constructor K Args) R :- coq.mk-app (global (indc K)) Params KParams, args Args KParams [] [] [] 0 R. -pred args i:arguments, i:term, i:list term,i:list term, i:list term, i:int, o:term. -args (irrelevant TY Args) K As Hs Bs N O :- std.do! [ +pred args i:eqb.arguments, i:term, i:list term,i:list term, i:list term, i:int, o:term. +args (eqb.irrelevant TY Args) K As Hs Bs N O :- std.do! [ O = {{ fun (x : lp:T) (px : lp:EqbOn x) => lp:(R x px) }}, feqb.trm->term TY T, mk-reali T EqbOn, @@ -273,7 +273,7 @@ args (irrelevant TY Args) K As Hs Bs N O :- std.do! [ args Args {coq.mk-app K [x]} [x|As] Hs Bs {calc (N + 1)} (R x px) ]. -args (regular TY Args) K As Hs Bs N O :- std.do! [ +args (eqb.regular TY Args) K As Hs Bs N O :- std.do! [ config _Pred Pred_on _Pred_body _Solver Db, O = {{ fun (x : lp:T) (px : lp:EqbOn x) (h : lp:EqbOn' x := lp:View x px) => lp:(R x px h) }}, feqb.trm->term TY T, @@ -287,7 +287,7 @@ args (regular TY Args) K As Hs Bs N O :- std.do! [ args Args {coq.mk-app K [x]} [x|As] [h|Hs] [{{ lp:Cmp lp:x }}|Bs] N (R x px h) ]. -args (dependent TY Args) K As Hs Bs N O :- std.do! [ +args (eqb.dependent TY Args) K As Hs Bs N O :- std.do! [ config _Pred Pred_on _Pred_body _Solver Db, O = {{ fun (x : lp:T) (px : lp:EqbOn x) (h : lp:EqbOn' x := lp:View x px) => lp:(R x px h) }}, feqb.trm->term TY T, @@ -301,7 +301,7 @@ args (dependent TY Args) K As Hs Bs N O :- std.do! [ args (Args xx) {coq.mk-app K [x]} [x|As] [h|Hs] [{{ lp:Cmp lp:x }}|Bs] {calc (N + 1)} (R x px h) ]. -args (stop TY) K As Hs Bs 0 {{ lp:B : lp:Pred_on lp:T lp:Cmp lp:K }} :- % no tricky arguments +args (eqb.stop TY) K As Hs Bs 0 {{ lp:B : lp:Pred_on lp:T lp:Cmp lp:K }} :- % no tricky arguments config {{ @eqb_correct }} Pred_on _Pred_body _Solver _Db, !, std.do! [ feqb.trm->term TY T, mk-eqb-for T Cmp, @@ -314,7 +314,7 @@ args (stop TY) K As Hs Bs 0 {{ lp:B : lp:Pred_on lp:T lp:Cmp lp:K }} :- % no tri GOAL = (x\ {{ @eq (option lp:T) (@Some lp:T lp:K) (lp:Construct (lp:Tag lp:K) lp:x) }} : term -> term), correct-proof x {{ lp:Fields_t (lp:Tag lp:K) }} HYP GOAL As Bs Hs (Proof x) ]. -args (stop TY) K _As _Hs _Bs _ {{ lp:B : lp:Pred_on lp:T lp:Cmp lp:K }} :- +args (eqb.stop TY) K _As _Hs _Bs _ {{ lp:B : lp:Pred_on lp:T lp:Cmp lp:K }} :- config {{ @eqb_correct }} Pred_on _Pred_body Solver _Db, !, std.do! [ feqb.trm->term TY T, mk-eqb-for T Cmp, @@ -376,7 +376,7 @@ mkblistcorrect [X|XS] [V|VS] ACC R :- coq.mk-app X [V] E, mkblistcorrect XS VS {{ bcons lp:E lp:ACC }} R. -args (stop TY) K _As Hs Bs _ {{ lp:B : lp:Pred_on lp:T lp:Cmp lp:K }} :- +args (eqb.stop TY) K _As Hs Bs _ {{ lp:B : lp:Pred_on lp:T lp:Cmp lp:K }} :- config {{ @eqb_reflexive }} Pred_on _Pred_body _Solver _Db, !, std.do! [ feqb.trm->term TY T, mk-eqb-for T Cmp, diff --git a/apps/derive/elpi/fields.elpi b/apps/derive/elpi/fields.elpi index cc12b9a13..7cd15a6cf 100644 --- a/apps/derive/elpi/fields.elpi +++ b/apps/derive/elpi/fields.elpi @@ -58,17 +58,17 @@ main I Prefix AllCL :- std.do! [ % ---------------------------------------------------------------------- -pred fields_t.main i:eqType, i:term, o:term. -fields_t.main (type-param F) I {{ fun p : Type => lp:(R p) }} :- !, +pred fields_t.main i:eqb.eqType, i:term, o:term. +fields_t.main (eqb.type-param F) I {{ fun p : Type => lp:(R p) }} :- !, @pi-trm `p` {{ Type }} x\p\ fields_t.main (F x) {coq.mk-app I [p]} (R p). -fields_t.main (value-param TY F) I {{ fun p : lp:Ty => lp:(R p) }} :- !, +fields_t.main (eqb.value-param TY F) I {{ fun p : lp:Ty => lp:(R p) }} :- !, feqb.trm->term TY Ty, @pi-trm `p` Ty x\p\ fields_t.main (F x) {coq.mk-app I [p]} (R p). -fields_t.main (inductive _ F) I {{ fun p : lib:elpi.derive.positive => lp:(R p) }} :- +fields_t.main (eqb.inductive _ F) I {{ fun p : lib:elpi.derive.positive => lp:(R p) }} :- coq.safe-dest-app I _ Params, @pi-decl `p` {{ lib:elpi.derive.positive }} p\ pi i\ splay-over-positive p (F i) fields_t.rty @@ -79,22 +79,22 @@ fields_t.main (inductive _ F) I {{ fun p : lib:elpi.derive.positive => lp:(R p) pred fields_t.rty i:term, o:term. fields_t.rty _ {{ Type }}. -pred fields_t.k i:list term, i:constructor, o:term. -fields_t.k Params (constructor K _) T :- +pred fields_t.k i:list term, i:eqb.constructor, o:term. +fields_t.k Params (eqb.constructor K _) T :- box-for K I _, coq.mk-app (global (indt I)) Params T. % ---------------------------------------------------------------------- -pred fields.main i:eqType, i:term, i:term, i:term, o:term. -fields.main (type-param F) I F_t Tag {{ fun p : Type => lp:(R p) }} :- !, +pred fields.main i:eqb.eqType, i:term, i:term, i:term, o:term. +fields.main (eqb.type-param F) I F_t Tag {{ fun p : Type => lp:(R p) }} :- !, @pi-trm `p` {{ Type }} x\p\ fields.main (F x) {coq.mk-app I [p]} {coq.mk-app F_t [p]} {coq.mk-app Tag [p]} (R p). -fields.main (value-param TY F) I F_t Tag {{ fun p : lp:Ty => lp:(R p) }} :- !, +fields.main (eqb.value-param TY F) I F_t Tag {{ fun p : lp:Ty => lp:(R p) }} :- !, feqb.trm->term TY Ty, @pi-trm `p` Ty x\p\ fields.main (F x) {coq.mk-app I [p]} {coq.mk-app F_t [p]} {coq.mk-app Tag [p]} (R p). -fields.main (inductive _ _) I F_t Tag {{ fun i : lp:I => lp:(R i) }} :- +fields.main (eqb.inductive _ _) I F_t Tag {{ fun i : lp:I => lp:(R i) }} :- @pi-trm `i` I _\i\ coq.build-match i I (fields.rty F_t Tag) @@ -111,7 +111,7 @@ fields.branch K _ Vars _ R :- coq.mk-app (global (indc B)) {std.append Params Vars} R. % ------------------------------------------------------------------------ -pred box i:term, i:list constructor, i:eqType, o:list prop. +pred box i:term, i:list constructor, i:eqb.eqType, o:list prop. box I KL Decl CL :- std.do! [ box.aux Decl I ILDr, box.declare KL ILDr CL, @@ -133,39 +133,39 @@ kind box-spec type. type real-box indt-decl -> box-spec. type same-box constructor -> box-spec. -pred box.aux i:eqType, i:term, o:list box-spec. -box.aux (type-param F) I L :- +pred box.aux i:eqb.eqType, i:term, o:list box-spec. +box.aux (eqb.type-param F) I L :- (@pi-trm `p` {{ Type }} x\y\ box.aux (F x) {coq.mk-app I [y]} (L1 y)), distribute L1 (f\r\ sigma U\ r = parameter "A" explicit (sort (typ U)) f) L. -box.aux (value-param TY F) I L :- +box.aux (eqb.value-param TY F) I L :- feqb.trm->term TY Ty, (@pi-trm `p` Ty x\y\ box.aux (F x) {coq.mk-app I [y]} (L1 y)), distribute L1 (f\r\ r = parameter "v" explicit Ty f) L. -box.aux (inductive Ind F) I L :- pi x\ box.aux2 I Ind x (F x) L. +box.aux (eqb.inductive Ind F) I L :- pi x\ box.aux2 I Ind x (F x) L. -pred args-of o:constructor, o:arguments. +pred args-of o:constructor, o:eqb.arguments. -pred box.aux2 i:term, i:inductive, i:trm, o:list constructor, o:list box-spec. +pred box.aux2 i:term, i:inductive, i:eqb.trm, o:list eqb.constructor, o:list box-spec. box.aux2 _ _ _ [] []. -box.aux2 I Ind X [constructor _ Args|MoreKs] [same-box K|MoreBoxes] :- args-of K Args, !, +box.aux2 I Ind X [eqb.constructor _ Args|MoreKs] [same-box K|MoreBoxes] :- args-of K Args, !, box.aux2 I Ind X MoreKs MoreBoxes. -box.aux2 I Ind X [constructor K Args|MoreKs] [real-box (record ID1 S ID2 Fields)|MoreBoxes] :- +box.aux2 I Ind X [eqb.constructor K Args|MoreKs] [real-box (record ID1 S ID2 Fields)|MoreBoxes] :- if (coq.env.informative? Ind) (S = {{ Type }}) (S = {{ Prop }}), ID1 is "box_" ^ {coq.gref->id (indt Ind)} ^ "_" ^ {coq.gref->id (indc K)}, ID2 is "Box_" ^ {coq.gref->id (indt Ind)} ^ "_" ^ {coq.gref->id (indc K)}, ((feqb.trm->term X I :- !) ==> box.box-argument ID2 0 Args Fields), args-of K Args ==> box.aux2 I Ind X MoreKs MoreBoxes. -pred box.box-argument i:string, i:int, i:arguments, o:record-decl. -box.box-argument _ _ (stop _) end-record. -box.box-argument S M (regular T Args) (field [] N TY _\A) :- N is S ^ "_" ^ {std.any->string M}, +pred box.box-argument i:string, i:int, i:eqb.arguments, o:record-decl. +box.box-argument _ _ (eqb.stop _) end-record. +box.box-argument S M (eqb.regular T Args) (field [] N TY _\A) :- N is S ^ "_" ^ {std.any->string M}, feqb.trm->term T TY, box.box-argument S {calc (M + 1)} Args A. -box.box-argument S M (irrelevant T Args) (field [] N TY _\A) :- N is S ^ "_" ^ {std.any->string M}, +box.box-argument S M (eqb.irrelevant T Args) (field [] N TY _\A) :- N is S ^ "_" ^ {std.any->string M}, feqb.trm->term T TY, box.box-argument S {calc (M + 1)} Args A. -box.box-argument S M (dependent T Args) (field [] N TY A) :- N is S ^ "_" ^ {std.any->string M}, +box.box-argument S M (eqb.dependent T Args) (field [] N TY A) :- N is S ^ "_" ^ {std.any->string M}, feqb.trm->term T TY, pi x y\ (feqb.trm->term x y :- !) ==> box.box-argument S {calc (M + 1)} (Args x) (A y). @@ -175,17 +175,17 @@ distribute (x\ [real-box (X x)| XS x]) F [real-box F_X|R] :- F X F_X, distribute distribute (x\ [same-box K| XS x]) F [same-box K|R] :- distribute XS F R. % ---------------------------------------------------------------------- -pred construct.main i:eqType, i:term, i:constant, o:term. -construct.main (type-param F) I F_t {{ fun p : Type => lp:(R p) }} :- +pred construct.main i:eqb.eqType, i:term, i:constant, o:term. +construct.main (eqb.type-param F) I F_t {{ fun p : Type => lp:(R p) }} :- @pi-trm `p` {{ Type }} x\p\ construct.main (F x) {coq.mk-app I [p]} F_t (R p). -construct.main (value-param TY F) I F_t {{ fun p : lp:Ty => lp:(R p) }} :- +construct.main (eqb.value-param TY F) I F_t {{ fun p : lp:Ty => lp:(R p) }} :- feqb.trm->term TY Ty, @pi-trm `p` Ty x\p\ construct.main (F x) {coq.mk-app I [p]} F_t (R p). -construct.main (inductive _ F) I F_t {{ fun p : lib:elpi.derive.positive => lp:(R p) }} :- +construct.main (eqb.inductive _ F) I F_t {{ fun p : lib:elpi.derive.positive => lp:(R p) }} :- coq.safe-dest-app I _ Params, coq.mk-app (global (const F_t)) Params Fields_t, @pi-decl `p` {{ lib:elpi.derive.positive }} p\ pi i\ @@ -197,12 +197,12 @@ construct.main (inductive _ F) I F_t {{ fun p : lib:elpi.derive.positive => lp:( pred construct.rty1 i:term, i:term, i:term, o:term. construct.rty1 Fields_t I X {{ lp:Fields_t lp:X -> option lp:I }}. -pred construct.k i:term, i:list term, i:constructor, o:term. -construct.k _ Params (constructor K (stop _)) {{ fun b : lp:BoxTy => Some lp:B }} :- !, +pred construct.k i:term, i:list term, i:eqb.constructor, o:term. +construct.k _ Params (eqb.constructor K (eqb.stop _)) {{ fun b : lp:BoxTy => Some lp:B }} :- !, box-for K BT _, coq.mk-app (global (indt BT)) Params BoxTy, coq.mk-app (global (indc K)) Params B. -construct.k I Params (constructor K _) {{ fun b : lp:BoxTy => lp:(R b) }} :- +construct.k I Params (eqb.constructor K _) {{ fun b : lp:BoxTy => lp:(R b) }} :- box-for K BT _, coq.mk-app (global (indt BT)) Params BoxTy, @pi-decl `b` BoxTy b\ diff --git a/apps/derive/theories/derive/eqType_ast.v b/apps/derive/theories/derive/eqType_ast.v index 1aff8e359..325fabf1b 100644 --- a/apps/derive/theories/derive/eqType_ast.v +++ b/apps/derive/theories/derive/eqType_ast.v @@ -8,26 +8,26 @@ From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive Elpi Db derive.eqType.db lp:{{ -kind arguments type. -kind trm type. -kind eqType type. -kind constructor type. +kind eqb.arguments type. +kind eqb.trm type. +kind eqb.eqType type. +kind eqb.constructor type. -type app gref -> trm -> list trm -> trm. -type global gref -> trm. +type eqb.app gref -> eqb.trm -> list eqb.trm -> eqb.trm. +type eqb.global gref -> eqb.trm. -type regular trm -> arguments -> arguments. -type irrelevant trm -> arguments -> arguments. -type dependent trm -> (trm -> arguments) -> arguments. -type stop trm -> arguments. +type eqb.regular eqb.trm -> eqb.arguments -> eqb.arguments. +type eqb.irrelevant eqb.trm -> eqb.arguments -> eqb.arguments. +type eqb.dependent eqb.trm -> (eqb.trm -> eqb.arguments) -> eqb.arguments. +type eqb.stop eqb.trm -> eqb.arguments. -type type-param (trm -> eqType) -> eqType. -type value-param trm -> (trm -> eqType) -> eqType. -type inductive inductive -> (trm -> list constructor) -> eqType. +type eqb.type-param (eqb.trm -> eqb.eqType) -> eqb.eqType. +type eqb.value-param eqb.trm -> (eqb.trm -> eqb.eqType) -> eqb.eqType. +type eqb.inductive inductive -> (eqb.trm -> list eqb.constructor) -> eqb.eqType. -type constructor constructor -> arguments -> constructor. +type eqb.constructor constructor -> eqb.arguments -> eqb.constructor. -pred eqType i:inductive, o:eqType. +pred eqType i:inductive, o:eqb.eqType. }}.