diff --git a/apps/derive/elpi/param1.elpi b/apps/derive/elpi/param1.elpi index 2bd583169..9c11583ad 100644 --- a/apps/derive/elpi/param1.elpi +++ b/apps/derive/elpi/param1.elpi @@ -4,7 +4,7 @@ % Author: Cyril Cohen -shorten std.{forall, forall2, do!, rev, map2, map}. +shorten std.{forall, forall2, do!, rev, map2, map, append}. :before "subst-fun:fail" coq.subst-fun XS T TXS :- !, coq.mk-app T XS TXS. @@ -99,10 +99,10 @@ reali-match (fun N T B) PRM :- do! [ % Storage: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -pred reali-store - i:string, % Name suffix for the type class - i:term, % Term - i:term. % Translation +func reali-store + string, % Name suffix for the type class + term, % Term + term -> . % Translation reali-store N X XR :- !, Nreali is "reali_" ^ N, Args = [_, _, X, XR], @@ -116,6 +116,88 @@ pred reali-store-indc i:string, i:constructor, i:constructor. reali-store-indc Prefix K XR :- reali-store {calc (Prefix ^ {coq.gref->id (indc K)})} (global (indc K)) (global (indc XR)). +kind raw-mindt-spec type. +type raw-mindt-spec inductive -> id -> bool -> term -> list constructor -> list (pair constructor id) -> list term -> raw-mindt-spec. + +func build-raw-mutual-spec string, inductive -> raw-mindt-spec. +build-raw-mutual-spec Prefix GR (raw-mindt-spec GR FNewName IsInd Ty KNames KNamesR KTypes) :- + coq.env.indt GR IsInd _ _ Ty KNames KTypes, + coq.gref->id (indt GR) ID, + std.map KNames (prefix-indc Prefix) KNamesR, + NewName is Prefix ^ ID, + coq.ensure-fresh-global-id NewName FNewName. + +func translate-mutual-spec raw-mindt-spec, inductive -> coq.indt-spec. +translate-mutual-spec (raw-mindt-spec GR FNewName IsInd Ty KNames KNamesR KTypes) NewGR + (coq.indt-spec NewGR FNewName IsInd TyOut KNamesR KTypesR) :- + Ind = global (indt GR), + reali Ty TyR, + coq.mk-app TyR [Ind] TyOut, + map2 KNames KTypes (k\ ty\ r\ sigma tyr\ + reali ty tyr, + coq.mk-app tyr [global (indc k)] r) KTypesR. + +func main-mblock list raw-mindt-spec, list raw-mindt-spec, list inductive -> list prop. +main-mblock All [] Acc Clauses :- !, + rev Acc NewGRs, + main-mblock-aux All NewGRs Clauses. +main-mblock All [raw-mindt-spec GR _ _ _ _ _ _|Rest] Acc Clauses :- + % a fresh name for each inductive + pi newGR\ (reali (global (indt GR)) (global (indt newGR)) :- !) => main-mblock All Rest [newGR|Acc] Clauses. + +func reali-store-mutual-indt list raw-mindt-spec, list inductive -> . +reali-store-mutual-indt [] []. +reali-store-mutual-indt [raw-mindt-spec GR FNewName _ _ _ _ _|MoreInd] [RealGR|MoreGR] :- + reali-store FNewName (global (indt GR)) (global (indt RealGR)), + reali-store-mutual-indt MoreInd MoreGR. + +func reali-store-mutual-indcs string, list constructor, list constructor -> . +reali-store-mutual-indcs _ [] []. +reali-store-mutual-indcs Prefix [K|KS] [KR|KRS] :- + N is Prefix ^ {coq.gref->id (indc K)}, + reali-store N (global (indc K)) (global (indc KR)), + reali-store-mutual-indcs Prefix KS KRS. + +func reali-store-mutual-indc list raw-mindt-spec, list inductive -> . +reali-store-mutual-indc [] []. +reali-store-mutual-indc [raw-mindt-spec _ FNewName _ _ KNames _ _|Raws] [RealGR|RealGRs] :- + coq.env.indt RealGR _ _ _ _ RealKNames _, + Prefix1 is FNewName ^ "_", + reali-store-mutual-indcs Prefix1 KNames RealKNames, + reali-store-mutual-indc Raws RealGRs. + +func build-and-accumulate-clauses list raw-mindt-spec, list inductive -> list prop. +build-and-accumulate-clauses [] [] []. +build-and-accumulate-clauses [raw-mindt-spec GR _ _ _ KNames _ _|Raws] [RealGR|RealGRs] Clauses :- + coq.env.indt RealGR _ _ _ _ RealKNames _, + map2 KNames RealKNames (a\ b\ r\ r = (reali (global (indc a)) (global (indc b)) :- !)) CK, + CDone = reali-done (indt GR), + CReali = (reali (global (indt GR)) (global (indt RealGR)) :- !), + CRealiR = (realiR (global (indt GR)) (global (indt RealGR)) :- !), + coq.elpi.accumulate _ "derive.param1.db" (clause _ _ CDone), + coq.elpi.accumulate _ "derive.param1.db" (clause _ (before "realiR:fail") CRealiR), + std.forall [CReali|CK] (x\coq.elpi.accumulate _ "derive.param1.db" (clause _ (before "reali:fail") x)), + build-and-accumulate-clauses Raws RealGRs Rest, + append[CDone, CReali, CRealiR | CK] Rest Clauses. + +func main-mblock-aux list raw-mindt-spec, list inductive -> list prop. +main-mblock-aux Raws NewGRs Clauses :- std.do! [ + map2 Raws NewGRs translate-mutual-spec Specs, + coq.build-mindt-decl Specs 0 0 DeclR, + std.assert-ok! (coq.typecheck-indt-decl DeclR) "derive.param1 generates illtyped mutual inductive", + coq.env.add-indt DeclR RealGR, + coq.env.indt-block RealGR _ _ _ RealGRs _ _ _, + reali-store-mutual-indt Raws RealGRs, + reali-store-mutual-indc Raws RealGRs, + build-and-accumulate-clauses Raws RealGRs Clauses, +]. + +func prefix-indc string, constructor -> pair constructor id. +prefix-indc Prefix K (pr K FNewName) :- + coq.gref->id (indc K) Name, + NewName is Prefix ^ Name, + coq.ensure-fresh-global-id NewName FNewName. + % toplevel predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :index (1) @@ -151,11 +233,11 @@ dispatch (const GR) Prefix Clauses :- !, do! [ Clauses = [C1, C2, reali-done (const GR)] ]. -func prefix-indc string, constructor -> pair constructor id. -prefix-indc Prefix K (pr K FNewName) :- - coq.gref->id (indc K) Name, - NewName is Prefix ^ Name, - coq.ensure-fresh-global-id NewName FNewName. +dispatch (indt GR) Prefix Clauses :- coq.env.indt-block GR _ Lno Luno GRS _ _ _, std.length GRS N, N > 1, !, do! [ + map GRS (build-raw-mutual-spec Prefix) Raws, + std.assert! (Lno = Luno) "derive.param1: Non-uniform parameters not supported", + main-mblock Raws Raws [] Clauses +]. dispatch (indt GR) Prefix Clauses :- !, do! [ Ind = global (indt GR), diff --git a/apps/derive/tests/test_induction.v b/apps/derive/tests/test_induction.v index 1ca7f1848..83951b567 100644 --- a/apps/derive/tests/test_induction.v +++ b/apps/derive/tests/test_induction.v @@ -42,9 +42,9 @@ Elpi derive.induction ord2. Elpi derive.induction val. Elpi derive.induction mempty. Elpi derive.induction munit. -Fail Elpi derive.induction mpeano. +Elpi derive.induction mpeano. Elpi derive.induction moption. -Fail Elpi derive.induction mtree. +Elpi derive.induction mtree. End Coverage. Import Coverage. @@ -75,3 +75,5 @@ Redirect "tmp" Check sigma_bool_induction. Redirect "tmp" Check sigma_bool2_induction. Redirect "tmp" Check ord_induction : forall p Pp P, (forall n Pn l, is_eq bool is_bool (is_leq n p) (is_is_leq n Pn p Pp) true is_true l -> P (mkOrd p n l)) -> forall (o : ord p), is_ord p Pp o -> P o. Redirect "tmp" Check ord2_induction : forall p Pp P, (forall (o1 : ord p), is_ord p Pp o1 -> forall (o2 : ord p), is_ord p Pp o2 -> P (mkOrd2 p o1 o2)) -> forall (o : ord2 p), is_ord2 p Pp o -> P o. +Fail Redirect "tmp" Check mpeano'_induction. +Fail Redirect "tmp" Check mforest_induction. \ No newline at end of file diff --git a/apps/derive/tests/test_param1.v b/apps/derive/tests/test_param1.v index c2b5ffb52..29b7261cd 100644 --- a/apps/derive/tests/test_param1.v +++ b/apps/derive/tests/test_param1.v @@ -45,9 +45,9 @@ Elpi derive.param1 val. Elpi derive.param1 alias. Elpi derive.param1 mempty. Elpi derive.param1 munit. -Fail Elpi derive.param1 mpeano. +Elpi derive.param1 mpeano. Elpi derive.param1 moption. -Fail Elpi derive.param1 mtree. +Elpi derive.param1 mtree. End Coverage. @@ -83,12 +83,15 @@ Redirect "tmp" Check is_val : pred val. Redirect "tmp" Check is_alias : pred alias. Redirect "tmp" Check is_mempty : pred mempty. -Fail Redirect "tmp" Check is_mempty' : pred mempty'. +Redirect "tmp" Check is_mempty' : pred mempty'. Redirect "tmp" Check is_munit : pred munit. -Fail Redirect "tmp" Check is_munit' : pred munit'. - +Redirect "tmp" Check is_munit' : pred munit'. Redirect "tmp" Check is_moption : forall A, pred A -> pred (moption A). -Fail Redirect "tmp" Check is_moption' : forall A, pred A -> pred (moption' A). +Redirect "tmp" Check is_moption' : forall A, pred A -> pred (moption' A). +Redirect "tmp" Check is_mpeano : pred mpeano. +Redirect "tmp" Check is_mpeano' : pred mpeano'. +Redirect "tmp" Check is_mtree : forall A, pred A -> pred (mtree A). +Redirect "tmp" Check is_mforest : forall A, pred A -> pred (mforest A). End Test. @@ -205,4 +208,9 @@ Inductive Acc {A : Type} (R : A -> A -> Prop) | (x : A) : Prop := Acc_intro : (forall y : A, R y x -> Acc y) -> Acc x. Elpi derive.param1 Acc. +Inductive a := ka with b := kb. +Elpi derive.param1 a. +Inductive c := kc : a -> kb = kb -> c. +Elpi derive.param1 c. + End OtherTests. diff --git a/apps/derive/tests/test_param1_congr.v b/apps/derive/tests/test_param1_congr.v index b02860a83..625933ff9 100644 --- a/apps/derive/tests/test_param1_congr.v +++ b/apps/derive/tests/test_param1_congr.v @@ -43,9 +43,9 @@ Elpi derive.param1.congr is_ord. Elpi derive.param1.congr is_val. Elpi derive.param1.congr is_mempty. Elpi derive.param1.congr is_munit. -Fail Elpi derive.param1.congr is_mpeano. +Elpi derive.param1.congr is_mpeano. Elpi derive.param1.congr is_moption. -Fail Elpi derive.param1.congr is_mtree. +Elpi derive.param1.congr is_mtree. End Coverage. @@ -92,3 +92,7 @@ Redirect "tmp" Check congr_is_Build_fo_record : forall n p1 p2, p1 = p2 -> foral Redirect "tmp" Check congr_is_Build_pa_record : forall A PA n p1 p2, p1 = p2 -> forall b q1 q2, q1 = q2 -> is_Build_pa_record A PA n p1 b q1= is_Build_pa_record A PA n p2 b q2. Redirect "tmp" Check congr_is_Build_pr_record : forall A pr n p1 p2, p1 = p2 -> forall b q1 q2, q1 = q2 -> is_Build_pr_record A pr n p1 b q1= is_Build_pr_record A pr n p2 b q2. Redirect "tmp" Check congr_is_E1 : is_E1 = is_E1. + + +Fail Redirect "tmp" Check congr_is_mpeano'. +Fail Redirect "tmp" Check congr_is_mforest. \ No newline at end of file diff --git a/apps/derive/tests/test_param1_trivial.v b/apps/derive/tests/test_param1_trivial.v index ec7ab6786..8745df116 100644 --- a/apps/derive/tests/test_param1_trivial.v +++ b/apps/derive/tests/test_param1_trivial.v @@ -47,7 +47,7 @@ Elpi derive.param1.trivial is_alias. Elpi derive.param1.trivial is_mempty. Elpi derive.param1.trivial is_munit. Fail Elpi derive.param1.trivial is_mpeano. -Elpi derive.param1.trivial is_moption. +Fail Elpi derive.param1.trivial is_moption. Fail Elpi derive.param1.trivial is_mtree.