Skip to content

Commit

Permalink
Merge pull request #731 from LPCIC/eqtype-ns
Browse files Browse the repository at this point in the history 
derive: put eqb ast into a namespace
  • Loading branch information
@gares
gares authored Feb 15, 2025
2 parents a857b5b + 3855618 commit 8d3f28e
Show file tree
Hide file tree
Showing 6 changed files with 155 additions and 155 deletions.
98 changes: 49 additions & 49 deletions apps/derive/elpi/eqType.elpi
View file
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
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 */
/* ------------------------------------------------------------------------- */

pred feqb.trm->term i:trm, o:term.
pred feqb.trm->term i:eqb.trm, o:term.

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

0 comments on commit 8d3f28e

Please sign in to comment.