Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

derive: put eqb ast into a namespace #731

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
+156 −156
Open

derive: put eqb ast into a namespace #731

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
028d3ed
fix opam
gares Dec 7, 2024
650ca3d
put the eqb ast into a namespace
gares Dec 7, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
98 changes: 49 additions & 49 deletions apps/derive/elpi/eqType.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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,
].
Expand All @@ -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),
].
Expand All @@ -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 ?".
Expand Down
56 changes: 28 additions & 28 deletions apps/derive/elpi/eqb.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -46,29 +46,29 @@ 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\
@pi-decl `x1` I x1\
@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\
Expand Down Expand Up @@ -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.

Expand All @@ -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,
Expand All @@ -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,
Expand All @@ -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.

Expand All @@ -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,
Expand All @@ -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\
Expand Down
Loading
Loading