diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..e181b66 --- /dev/null +++ b/.gitattributes @@ -0,0 +1 @@ +*.elpi linguist-language=prolog diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..ed0d8ae --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,13 @@ +{ + "files.exclude": { + "**/*.d": true, + "**/*.vo": true, + "**/*.vok": true, + "**/*.vos": true, + "**/*.glob": true, + "**/*.aux": true, + "**/Makefile.coq": true, + "**/Makefile.coq.conf": true + }, + "coqtop.binPath": "/nix/store/bfygibqxf976p49svngbkzkls6fqwywz-coq-8.14.0/bin/" +} \ No newline at end of file diff --git a/Makefile.coq.local b/Makefile.coq.local new file mode 100644 index 0000000..b1c7a79 --- /dev/null +++ b/Makefile.coq.local @@ -0,0 +1,5 @@ +src/tag.vo : src/tag.elpi +src/fields.vo : src/fields.elpi +src/eqb.vo : src/eqb.elpi src/fields.elpi +src/eqbcorrect.vo : src/eqbcorrect.elpi src/fields.elpi src/eqb.elpi +src/eqbP.vo : src/eqbP.elpi src/eqbcorrect.elpi src/fields.elpi src/eqb.elpi \ No newline at end of file diff --git a/_CoqProject b/_CoqProject index 9f8ae50..e3b2845 100644 --- a/_CoqProject +++ b/_CoqProject @@ -17,4 +17,10 @@ src/option_defs.v src/list_defs.v src/nested_defs.v src/nested_list_defs.v -src/large_defs.v \ No newline at end of file +src/large_defs.v +src/large_defs2.v +src/tag.v +src/fields.v +src/eqb.v +src/eqbcorrect.v +src/eqbP.v \ No newline at end of file diff --git a/coqword.nix b/coqword.nix new file mode 100644 index 0000000..8b01b86 --- /dev/null +++ b/coqword.nix @@ -0,0 +1,49 @@ +{ stdenv, lib, fetchFromGitHub, coqPackages, ocaml, dune_2 }: + +let inherit (coqPackages) coq; in + +let mathcomp = + (if coqPackages ? mathcomp_ + then coqPackages.mathcomp_ "1.12.0" + else coqPackages.mathcomp.override { version = "1.12.0"; } + ).algebra +; in + +let rev = "e39e96d51aa96f386222fd1b38776f2117f325c5"; in + +stdenv.mkDerivation rec { + version = "1.0-git-${builtins.substring 0 8 rev}"; + name = "coq${coq.coq-version}-coqword-${version}"; + + src = fetchFromGitHub { + owner = "jasmin-lang"; + repo = "coqword"; + inherit rev; + sha256 = "sha256:0703m97rnivcbc7vvbd9rl2dxs6l8n52cbykynw61c6w9rhxspcg"; + }; + + buildInputs = [ coq ocaml dune_2 ]; + + propagatedBuildInputs = [ mathcomp ]; + + buildPhase = '' + runHook preBuild + dune build -p coq-mathcomp-word + runHook postBuild + ''; + + installPhase = '' + runHook preInstall + dune install --prefix=$out + mkdir -p $out/lib/coq/${coq.coq-version}/ + mv $out/lib/coq/user-contrib $out/lib/coq/${coq.coq-version}/ + runHook postInstall + ''; + + meta = { + description = "Yet Another Coq Library on Machine Words"; + license = lib.licenses.cecill-b; + inherit (src.meta) homepage; + inherit (coq.meta) platforms; + }; +} diff --git a/default.nix b/default.nix index d0fb24b..c0fc220 100644 --- a/default.nix +++ b/default.nix @@ -11,7 +11,7 @@ with pkgs; let inherit (lib) optionals; in -let coqPackages = coqPackages_8_12; in +let coqPackages = coqPackages_8_14; in let coqword = callPackage ./coqword.nix { inherit coqPackages; }; in @@ -35,7 +35,7 @@ stdenv.mkDerivation { name = "jasmin-0"; src = null; buildInputs = [] - ++ optionals coqDeps [ coqPackages.coq coqword coqPackages.coq.ocamlPackages.ocaml ] + ++ optionals coqDeps [ coqPackages.coq coqPackages.coq-elpi coqword coqPackages.coq.ocamlPackages.ocaml ] ++ optionals testDeps ([ ocamlPackages.apron.out ] ++ (with python3Packages; [ python pyyaml ])) ++ optionals ocamlDeps ([ mpfr ppl ] ++ (with oP; [ ocaml findlib ocamlbuild diff --git a/src/core_defs.v b/src/core_defs.v index 4d64207..ec24887 100644 --- a/src/core_defs.v +++ b/src/core_defs.v @@ -14,19 +14,28 @@ Definition eqb_correct_on (eqb : A -> A -> bool) (a1:A) := forall a2, eqb a1 a2 -> a1 = a2. Definition eqb_refl_on (eqb : A -> A -> bool) (a:A) := - eqb a a. + is_true (eqb a a). + +Definition eqb_correct (eqb : A -> A -> bool) := + forall (a1:A), eqb_correct_on eqb a1. + +Definition eqb_reflexive (eqb : A -> A -> bool) := + forall (a:A), eqb_refl_on eqb a. + +Lemma iffP2 (f : A -> A -> bool) (H1 : eqb_correct f) (H2 : eqb_reflexive f) + (x1 x2 : A) : reflect (x1 = x2) (f x1 x2). +Proof. apply (iffP idP);[ apply H1 | move->; apply H2 ]. Qed. Definition eqax_on (eqb : A -> A -> bool) (a1:A) := forall a2, reflect (a1 = a2) (eqb a1 a2). -Class obj := - { tag : A -> positive - ; fields_t : positive -> Type - ; fields : forall a, fields_t (tag a) - ; construct : forall t, fields_t t -> option A - ; constructP : forall a, construct (fields a) = Some a }. +Variable tag : A -> positive. +Variable fields_t : positive -> Type. +Variable fields : forall a, fields_t (tag a). +Variable construct : forall t, fields_t t -> option A. +Variable constructP : forall a, construct (fields a) = Some a. -Context {o:obj} (eqb_fields : forall t, fields_t t -> fields_t t -> bool). +Variable eqb_fields : forall t, fields_t t -> fields_t t -> bool. Definition eqb_body (t1:positive) (f1:fields_t t1) (x2:A) := let t2 := tag x2 in diff --git a/src/elpi-ltac.elpi b/src/elpi-ltac.elpi new file mode 100644 index 0000000..8ff9564 --- /dev/null +++ b/src/elpi-ltac.elpi @@ -0,0 +1,111 @@ +/* elpi-ltac: building blocks for tactics */ +/* license: GNU Lesser General Public License Version 2.1 or later */ +/* ------------------------------------------------------------------------- */ +typeabbrev tactic (sealed-goal -> (list sealed-goal -> prop)). +typeabbrev open-tactic (goal -> (list sealed-goal -> prop)). + +% The one tactic ------------------------------------------------------------ +pred refine i:term, i:goal, o:list sealed-goal. +refine T G GS :- refine.elaborate T G GS. + +pred refine.elaborate i:term, i:goal, o:list sealed-goal. +refine.elaborate T (goal _ RawEv _ Ev _) GS :- + RawEv = T, coq.ltac.collect-goals Ev GS _. + +pred refine.typecheck i:term, i:goal, o:list sealed-goal. +refine.typecheck T (goal _ _ Ty Ev _) GS :- + coq.typecheck T Ty ok, + Ev = T, coq.ltac.collect-goals Ev GS _. + +pred refine.no_check i:term, i:goal, o:list sealed-goal. +refine.no_check T (goal _ _ _ Ev _) GS :- + Ev = T, coq.ltac.collect-goals Ev GS _. + +% calling other tactics, with arguments --------------------------------------- + +pred coq.ltac i:string, i:sealed-goal, o:list sealed-goal. +coq.ltac Tac G GS :- coq.ltac.open (coq.ltac.call-ltac1 Tac) G GS. + +namespace coq.ltac { + +pred call i:string, i:list argument, i:goal, o:list sealed-goal. +call Tac Args G GS :- + set-goal-arguments Args G (seal G) (seal G1), + coq.ltac.call-ltac1 Tac G1 GS. + +pred set-goal-arguments i:list argument, i:goal, i:sealed-goal, o:sealed-goal. +set-goal-arguments A G (nabla SG) (nabla R) :- pi x\ set-goal-arguments A G (SG x) (R x). +set-goal-arguments A (goal Ctx1 _ _ _ _) (seal (goal Ctx2 REv2 Ty2 Ev2 _)) (seal (goal Ctx2 REv2 Ty2 Ev2 I)) :- + std.map A (private.move-goal-argument Ctx1 Ctx2) I. + +% Tacticals ---------------------------------------------------------------- + +pred try i:tactic, i:sealed-goal, o:list sealed-goal. +try T G GS :- T G GS. +try _ G [G]. + +:index(_ 1) +pred all i:tactic, i:list sealed-goal, o:list sealed-goal. +all T [G|Gs] O :- T G O1, all T Gs O2, std.append O1 O2 O. +all _ [] []. + +pred thenl i:list tactic, i:sealed-goal, o:list sealed-goal. +thenl [] G [G]. +thenl [T|Ts] G GS :- T G NG, all (thenl Ts) NG GS. + +pred repeat i:tactic, i:sealed-goal, o:list sealed-goal. +repeat T G GS :- T G GS1, all (repeat T) GS1 GS. +repeat _ G [G]. + +pred repeat! i:tactic, i:sealed-goal, o:list sealed-goal. +repeat! T G GS :- T G GS1, !, all (repeat T) GS1 GS. +repeat! _ G [G]. + +pred or i:list tactic, i:sealed-goal, o:list sealed-goal. +or TL G GS :- std.exists TL (t\ t G GS). + +:index(_ 1) +pred open i:open-tactic, i:sealed-goal, o:list sealed-goal. +open T (nabla G) O :- (pi x\ open T (G x) (NG x)), private.distribute-nabla NG O. +open _ (seal (goal _ _ _ Solution _)) [] :- not (var Solution), !. % solved by side effect +open T (seal (goal Ctx _ _ _ _ as G)) O :- + std.filter Ctx private.not-already-assumed Ctx1, + Ctx1 => T G O, + if (var O) + (G = goal _ _ _ P _, coq.ltac.collect-goals P O1 O2, std.append O1 O2 O) + true. + +% helper code --------------------------------------------------------------- + +namespace private { + +:index(_ _ 1) +pred move-goal-argument i:list prop, i:list prop, i:argument, o:argument. +move-goal-argument _ _ (int _ as A) A. +move-goal-argument _ _ (str _ as A) A. +move-goal-argument C D (trm T) (trm T1) :- + std.rev C Cr, std.rev D Dr, + std.assert! (move-term Cr Dr T T1) "cannot move goal argument to the right context", !. + +:index(2) +pred move-term i:list prop, i:list prop, i:term, o:term. +move-term [] _ T T1 :- copy T T1. +move-term [decl X _ TX|C1] [decl Y _ TY|C2] T T1 :- std.do! [ copy TX TX1, same_term TX1 TY ], !, + copy X Y => move-term C1 C2 T T1. +move-term [def X _ TX BX|C1] [def Y _ TY BY|C2] T T1 :- std.do! [ copy TX TX1, same_term TX1 TY, copy BX BX1, same_term BX1 BY ], !, + copy X Y => move-term C1 C2 T T1. +move-term [decl X _ _|C1] C2 T T1 :- not(occurs X T), !, move-term C1 C2 T T1. +move-term [def X _ _ _|C1] C2 T T1 :- not(occurs X T), !, move-term C1 C2 T T1. +move-term C1 [_|C2] T T1 :- move-term C1 C2 T T1. + +pred distribute-nabla i:(term -> list sealed-goal), o:list sealed-goal. +distribute-nabla (_\ []) []. +distribute-nabla (x\ [X x| XS x]) [nabla X|R] :- (pi x\ occurs x (X x)), !, + distribute-nabla XS R. +distribute-nabla (x\ [X| XS x]) [X|R] :- distribute-nabla XS R. + +pred not-already-assumed i:prop. +not-already-assumed (decl X _ _Ty) :- not(decl X _ _ ; def X _ _ _). +not-already-assumed (def X _ _Ty _Bo) :- not(decl X _ _ ; def X _ _ _). + +}} \ No newline at end of file diff --git a/src/eqb.elpi b/src/eqb.elpi new file mode 100644 index 0000000..44863c1 --- /dev/null +++ b/src/eqb.elpi @@ -0,0 +1,128 @@ + +pred eqb.main i:inductive, i:string, o:list prop. +eqb.main I Prefix CL :- std.do! [ + coq.env.indt I _ _ N Arity _ _, + Ind = global (indt I), + + % the non recursive code comparing all fields according to their types + eqbf.do-params N Arity Ind R, + std.assert-ok! (coq.typecheck R Rty) "eqbf generates illtyped term", + Name is Prefix ^ "eqb_fields", + coq.env.add-const Name R Rty ff C, + EQBF = global (const C), + + % the fix + eqb.do-params N Arity Ind EQBF R1, + std.assert-ok! (coq.typecheck R1 R1ty) "eqb generates illtyped term", + Name1 is Prefix ^ "eqb", + coq.env.add-const Name1 R1 R1ty ff C1, + EQB = global (const C1), + + % populate dbs + eqbf.do-clause N Arity Ind EQBF [] CL1, + eqb.do-clause N Arity Ind EQB [] CL2, + CL = [CL1,CL2], + std.forall CL (x\ coq.elpi.accumulate _ "eqb.db" (clause _ _ x)), +]. + +namespace eqb { + +pred do-params i:int, i:term, i:term, i:term, o:term. +do-params N {{ forall x : lp:T, lp:(F x) }} I EF {{ fun (x : lp:T) (eqx : x -> x -> bool) => lp:(R x eqx) }} :- N > 0, !, M is N - 1, + @pi-decl `x` T x\ + @pi-decl `eqx` {{ lp:x -> lp:x -> bool }} eqx\ + do-params M (F x) {coq.mk-app I [x]} {coq.mk-app EF [x,eqx]} (R x eqx). +do-params 0 _ I EF {{ fix rec (x1 x2 : lp:I) {struct x1} : bool := lp:(R rec x1 x2) }} :- + @pi-decl `rec` {{ lp:I -> lp:I -> bool }} rec\ + @pi-decl `x1` I x1\ + @pi-decl `x2` I x2\ + do-match x1 I x2 {coq.mk-app EF [rec]} (R rec x1 x2). + +pred do-match i:term, i:term, i:term, i:term, o:term. +do-match X1 I X2 F R :- + coq.build-match X1 I + (_\_\_\r\ r = {{ bool }}) + (do-branch X2 F) + R. + +pred do-branch i:term, i:term, i:term, i:term, i:list term, i:A, o:term. +do-branch X2 F K KTY Vars _ {{ @eqb_body _ _ _ lp:FLDP lp:F lp:TAG lp:X lp:X2 }} :- std.do! [ + coq.safe-dest-app KTY (global (indt I)) Params, + fields-for I _ FLD _ _, + tag-for I T, + coq.mk-app (global (const FLD)) Params FLDP, + coq.mk-app (global (const T)) Params TA, + coq.mk-app TA [{coq.mk-app K Vars}] TAG, + to-tuple Vars X, +]. + +pred to-tuple i:list term, o:term. +to-tuple [] {{ tt }}. +to-tuple [X] X. +to-tuple [X|XS] {{ ( lp:X, lp:R ) }} :- to-tuple XS R. + +% example: eqb-for {{ list lp:A }} {{ @list_eqb lp:A lp:F }} :- eqb-for A F. +pred do-clause i:int, i:term, i:term, i:term, i:list prop, o:prop. +do-clause N {{ forall p, lp:(A p) }} I F Todo (pi a ea\ C a ea) :- N > 0, !, M is N - 1, + pi a ea\ + do-clause M (A a) {coq.mk-app I [a]} {coq.mk-app F [a,ea]} [eqb-for a ea|Todo] (C a ea). +do-clause 0 _ I F Todo (eqb-for I F :- Todo). + +} + +% ----------------------------------------------------------------------------- + +namespace eqbf { + +pred do-params i:int, i:term, i:term, o:term. +do-params J {{ forall p : lp:T, lp:(F p) }} I {{ fun (p : lp:T) (eqp : p -> p -> bool) => lp:(R p eqp) }} :- J > 0, !, K is J - 1, + @pi-decl `P` T p\ + @pi-decl `eqP` {{ lp:p -> lp:p -> bool }} eqP\ + eqb-for p eqP => + do-params K (F p) {coq.mk-app I [p]} (R p eqP). +do-params 0 _ Ind {{ fun (rec : lp:Ind -> lp:Ind -> bool) (x : positive) => lp:(R rec x) }} :- std.do! [ + coq.safe-dest-app Ind (global (indt I)) Params, + coq.env.indt I _ _ _ _ _ KT, + std.map KT (coq.subst-prod Params) L, + fields-for I F_t _ _ _, + coq.mk-app (global (const F_t)) Params Fields_t, + (@pi-decl `rec` {{ lp:Ind -> lp:Ind -> bool }} rec\ + @pi-decl `x` {{ positive }} x\ + eqb-for Ind rec => + fields.splay-over-positive x L {{ fun x => lp:Fields_t x -> lp:Fields_t x -> bool }} + {{ fun _ _ => true }} + do-fields + (R rec x)), +]. +pred do-fields i:term, o:term. +do-fields Ty {{ fun a b => lp:(R a b) }} :- + @pi-decl `x` _ x\ + @pi-decl `y` _ y\ + do-fields.aux Ty x y (R x y). + +pred do-fields.aux i:term, i:term, i:term, o:term. +do-fields.aux {{ forall p : lp:T, lp:(F p) }} P1 P2 {{ lp:X && lp:R }} :- F = (x\prod _ _ _), !, % not the last one + eqb-for T EQB, + X = {{ lp:EQB (fst lp:P1) (fst lp:P2) }}, + (pi x\ if (occurs x (F x)) (coq.error "dependent type not supported yet") true), + @pi-decl `p` T n\ + do-fields.aux (F n) {{ snd lp:P1 }} {{ snd lp:P2 }} R. +do-fields.aux {{ lp:T -> _ }} P1 P2 X :- + eqb-for T EQB, + coq.mk-app EQB [P1, P2] X. +do-fields.aux _ _ _ {{ 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:int, i:term, i:term, i:term, i:list prop, o:prop. +do-clause N (prod _ _ A) I F Todo (pi a ea\ C a ea) :- N > 0, !, M is N - 1, + pi a ea\ + do-clause M (A a) {coq.mk-app I [a]} {coq.mk-app F [a,ea]} [eqb-for a ea|Todo] (C a ea). +do-clause 0 _ I F Todo (pi ela\ eqb-fields I (F1 ela) :- [C ela|Todo]) :- + pi ela\ + (coq.mk-app F [ela] (F1 ela), + C ela = eqb-for I ela). + + +} \ No newline at end of file diff --git a/src/eqb.v b/src/eqb.v new file mode 100644 index 0000000..f3b2c2b --- /dev/null +++ b/src/eqb.v @@ -0,0 +1,37 @@ +From elpi Require Import elpi. +From Coq Require Import PArith. + +Require Import core_defs. +Require Export tag fields. + +Open Scope positive_scope. +Open Scope bool_scope. + +Elpi Db eqb.db lp:{{ + +pred eqb-for + o:term, % type + o:term. % eqb_type + +pred eqb-fields + o:term, % type + o:term. % eq_fields_type + + +}}. + +Elpi Command eqb. +Elpi Accumulate File "src/fields.elpi". +Elpi Accumulate File "src/eqb.elpi". +Elpi Accumulate Db tag.db. +Elpi Accumulate Db fields.db. +Elpi Accumulate Db eqb.db. +Elpi Accumulate lp:{{ + + main [str S] :- + std.assert! (coq.locate S (indt I)) "Not an inductive type", + Prefix is S ^ "_", + eqb.main I Prefix _. + +}}. +Elpi Typecheck. diff --git a/src/eqbP.elpi b/src/eqbP.elpi new file mode 100644 index 0000000..c86b7de --- /dev/null +++ b/src/eqbP.elpi @@ -0,0 +1,48 @@ +namespace eqbP { + +pred add-reflect i:term, i:term, i:term, o:term. +add-reflect (prod N T F) Correct Refl + {{fun (a:lp:T) (eqA:a -> a -> bool) (H: forall x1 x2, reflect (x1 = x2) (eqA x1 x2)) => lp:(R a eqA H) }} :- !, +@pi-decl N T a\ +@pi-decl `eqA` {{ lp:a -> lp:a -> bool }} eqA\ +@pi-decl `H` {{ forall x1 x2, reflect (x1 = x2) (lp:eqA x1 x2)}} H\ +add-reflect (F a) + {{lp:Correct lp:a lp:eqA (fun (a1 a2 : lp:a) => @elimT (@eq lp:a a1 a2) (lp:eqA a1 a2) (lp:H a1 a2))}} + {{lp:Refl lp:a lp:eqA (fun (a1: lp:a) => @introT (@eq lp:a a1 a1) (lp:eqA a1 a1) (lp:H a1 a1) (@erefl lp:a a1))}} + (R a eqA H). + +add-reflect _T Correct Refl {{iffP2 lp:Correct lp:Refl}}. + +pred add-eqP i:term, i:term, i:term, o:term. +add-eqP (prod N T F) Ty Reflect {{fun (a:eqType) => lp:(R a)}} :- !, + @pi-decl N {{eqType}} a\ + eqb-for {{Equality.sort lp:a}} {{@eq_op lp:a}} => + add-eqP (F a) + {{lp:Ty (Equality.sort lp:a)}} + {{lp:Reflect (Equality.sort lp:a) (@eq_op lp:a) (@eqP lp:a)}} (R a). + +add-eqP _ Ty Reflect {{ @Equality.Pack lp:Ty (@Equality.Mixin lp:Ty lp:Cmp lp:Reflect) }} :- + eqb-for Ty Cmp. + +pred main i:inductive, i:string, o:list prop. +main I Prefix [] :- std.do! [ + % Add error msg if not a inductive ? + coq.env.indt I _ _ N TI Ks KTs, + + std.assert! (eqcorrect-for I Correct Refl) "run eqcorrect before", + + add-reflect TI (global (const Correct)) (global (const Refl)) Breflect, + std.assert-ok! (coq.typecheck Breflect Treflect) "fail demande a JC", + Namerf is Prefix ^ "eqb_reflect", + coq.env.add-const Namerf Breflect Treflect @transparent! Reflect, + + add-eqP TI (global (indt I)) (global (const Reflect)) BeqP, + std.assert-ok! (coq.typecheck BeqP TeqP) "fail demande a JC", + NameeqP is Prefix ^ "eqbP", + coq.env.add-const NameeqP BeqP TeqP @transparent! EqP, + + coq.CS.declare-instance (const EqP), + +]. + +} diff --git a/src/eqbP.v b/src/eqbP.v new file mode 100644 index 0000000..36662e4 --- /dev/null +++ b/src/eqbP.v @@ -0,0 +1,15 @@ +Require Import core_defs. +Require Export eqb eqbcorrect. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype. + +Elpi Command eqbP. +Elpi Accumulate Db eqcorrect.db. +Elpi Accumulate Db eqb.db. +Elpi Accumulate File "src/eqbP.elpi". +Elpi Accumulate lp:{{ + main [str S] :- + std.assert! (coq.locate S (indt I)) "Not an inductive type", + Prefix is S ^ "_", + eqbP.main I Prefix _. +}}. +Elpi Typecheck. diff --git a/src/eqbcorrect.elpi b/src/eqbcorrect.elpi new file mode 100644 index 0000000..6b893cf --- /dev/null +++ b/src/eqbcorrect.elpi @@ -0,0 +1,278 @@ + +namespace eqbcorrect { + +pred main i:inductive, i:string, o:list prop. +main I Prefix CLs :- std.do! [ + % Add error msg if not a inductive ? + coq.env.indt I _ _ N TI Ks KTs, + + coq.say {gettimeofday} "0", + + % std.map2 KTs Ks (add-decl-correct-ty Prefix N I) Lt-correct-ty, + + coq.say {gettimeofday} "0.1", + + std.map2 KTs Ks (add-decl-correct Prefix N (global (indt I))) Lt-correct, + + coq.say {gettimeofday} "0.5", + + std.map2 KTs Ks (add-decl-refl Prefix N (global (indt I))) Lt-refl, + + coq.say {gettimeofday} "1", + + induction-db I Indu, + reali (global (indt I)) IR, % param1-db, really + + add-indu-correct TI Indu IR Lt-correct R, + std.assert-ok! (coq.typecheck R Ty) "fail demande a JC", + Name is Prefix ^ "eqb_correct", + coq.env.add-const Name R Ty @opaque! Correct, + + add-indu-correct-aux TI Indu IR Lt-correct Rx, + std.assert-ok! (coq.typecheck Rx Tyx) "fail demande a JC", + Namex is Prefix ^ "eqb_correct_aux", + coq.env.add-const Namex Rx Tyx @opaque! Correctx, + + coq.say {gettimeofday} "2", + + add-indu-refl TI Indu IR Lt-refl Rr, + std.assert-ok! (coq.typecheck Rr Tyr) "fail demande a JC", + Namer is Prefix ^ "eqb_refl", + coq.env.add-const Namer Rr Tyr @opaque! Refl, + + coq.say {gettimeofday} "3", + + CLs = [ + eqcorrect-for I Correct Refl, + correct-lemma-for (indt I) (global (const Correctx)), + ], + std.forall CLs (x\ coq.elpi.accumulate _ "eqcorrect.db" (clause _ _ x)), + +]. + +pred what-for i:(gref -> term -> prop), i:(term -> term -> prop), i:term, o:term. +pred eqb-correct-aux-for i:term, o:term. +eqb-correct-aux-for T R :- + what-for correct-lemma-for eqb-correct-aux-for T R. + +what-for What Rec (app [global GR|L]) R :- std.spy-do! [ + What GR Aux, + functor-lemma-for GR Funct, + std.map L Rec Recs, + apply-functor Funct Recs TOTO, + R = {{ fun x H => lp:Aux _ _ x (lp:TOTO x H) }}, +]. + + pred apply-functor i:term, i:list term, o:term. + apply-functor X [] X. + apply-functor X [R|RS] TOTO :- apply-functor {{ lp:X _ _ _ lp:R }} RS TOTO. + + + +pred run-solver i:sealed-goal, i:string. +run-solver G Name :- + if (coq.ltac.open (coq.ltac.call Name []) G []) true + (coq.sealed-goal->string G SG, + std.fatal-error {calc ( "solver " ^ Name ^ " fails on goal:\n" ^ SG )}). + +coq.sealed-goal->string (nabla G) R :- pi x\ coq.sealed-goal->string (G x) R. +coq.sealed-goal->string (seal (goal Ctx _ Ty _ _)) R :- + Ctx => (std.map {std.rev Ctx} coq.ctx->string L, coq.term->string Ty G, R is {std.string.concat "\n" L} ^ "\n===============\n" ^ G). + +coq.ctx->string (decl X _ Ty) R :- R is {coq.term->string X} ^ " : " ^ {coq.term->string Ty}. +coq.ctx->string (def X _ Ty B) R :- R is {coq.term->string X} ^ " : " ^ {coq.term->string Ty} ^ " := " ^ {coq.term->string B}. + +/************************** correct *********************************************/ + +/* Build the type + +pred add-decl-correct-ty i:string, i:int, i:inductive, i:term, i:constructor, o:term. +add-decl-correct-ty Prefix N I KT K R /*(global (const P))*/ :- std.do![ + do-params-correct-ty N KT (global (indt I)) (global (indc K)) R, + coq.term->string R RS, + coq.say "R=" RS, + std.assert-ok! (coq.typecheck R Ty) "R casse", + Name is Prefix ^ "eqb_correct_on_" ^ {coq.gref->id (indc K)} ^ "_t", + coq.env.add-const Name R Ty @opaque! P, + % coq.say {gettimeofday} ".", +]. + +pred do-params-correct-ty i:int, i:term, i:term, i:term, o:term. +do-params-correct-ty 0 T I K R :- !, + eqb-for I Cmp, + reali I {{ @eqb_correct_on lp:I lp:Cmp }} => + do-args-correct-ty T K R. +do-params-correct-ty NP (prod N T F) I K {{ forall (a : lp:T) (eqA : a -> a -> bool), lp:(R a eqA) }} :- NP > 0, !, NP1 is NP - 1, + @pi-decl N T a\ + @pi-decl `eqA` {{ lp:a -> lp:a -> bool }} eqA\ + eqb-for a eqA => + reali a {{ @eqb_correct_on lp:a lp:eqA }} => + do-params-correct-ty NP1 (F a) {{ lp:I lp:a }} {{ lp:K lp:a }} (R a eqA). + +pred do-args-correct-ty i:term, i:term, o:term. +do-args-correct-ty (prod N T F) K {{ forall (x : lp:T) (Px : lp:EqbOn x), lp:(R x Px) }} :- !, + reali T EqbOn, + @pi-decl N T x\ + @pi-decl `px` {{ lp:EqbOn lp:x }} px\ + do-args-correct-ty (F x) {{ lp:K lp:x }} (R x px). + +do-args-correct-ty T K {{ eqb_correct_on lp:Cmp lp:K }} :- std.do! [ + eqb-for T Cmp, +% coq.safe-dest-app T (global (indt I)) Args, +% fields-for I _ _ _ ConstructPC, +% coq.mk-app (global (const ConstructPC)) Args ConstructP, +% eqb-fields T Fields, +% B = {{ @eqb_body_correct _ _ _ _ _ lp:ConstructP lp:Fields lp:K (fun f => _) }}, +% coq.typecheck {{ lp:B : eqb_correct_on lp:Cmp lp:K }} _ _, +% coq.ltac.collect-goals B [G] _, +% run-solver G "eqb_correct_on__solver", +% +]. + +*/ + +pred add-decl-correct i:string, i:int, i:term, i:term, i:constructor, o:term. +add-decl-correct Prefix N I KT K R /*(global (const P))*/ :- std.do![ + do-params-correct N I KT (global (indc K)) R, + std.assert-ok! (coq.typecheck R Ty) "R casse", + % Name is Prefix ^ "eqb_correct_on_" ^ {coq.gref->id (indc K)}, + % coq.env.add-const Name R Ty @opaque! P, + % coq.say {gettimeofday} ".", +]. + +% forall T : Type, T -> list T -> list T ---> forall a eqA, ..R.. +% T : Type |- T -> list T -> list T ---> +pred do-params-correct i:int, i:term, i:term, i:term, o:term. +do-params-correct 0 I T K R :- !, + eqb-for I Cmp, + reali I {{ @eqb_correct_on lp:I lp:Cmp }} => + eqb-correct-aux-for I {{ fun x H => H }} => + do-args-correct T K R. +do-params-correct NP I (prod N T F) K {{ fun (a : lp:T) (eqA : a -> a -> bool) => lp:(R a eqA) }} :- NP > 0, !, NP1 is NP - 1, + @pi-decl N T a\ + @pi-decl `eqA` {{ lp:a -> lp:a -> bool }} eqA\ + eqb-for a eqA => + eqb-correct-aux-for a {{ fun (x: lp:a) (H : @eqb_correct_on lp:a lp:eqA x) => H }} => + reali a {{ @eqb_correct_on lp:a lp:eqA }} => + do-params-correct NP1 {{ lp:I lp:a }} (F a) {{ lp:K lp:a }} (R a eqA). + +pred do-args-correct i:term, i:term, o:term. + +do-args-correct (prod N T F) K {{ fun (x : lp:T) (px : lp:EqbOn x) (h : @eqb_correct_on lp:T lp:Cmp x := lp:View x px) => lp:(R x px h) }} :- !, std.spy-do! [ + reali T EqbOn, + eqb-for T Cmp, + eqb-correct-aux-for T View, + @pi-decl N T x\ + @pi-decl `px` {{ lp:EqbOn lp:x }} px\ + @pi-def `H` {{ @eqb_correct_on lp:T lp:Cmp lp:x }} {{ lp:View lp:x lp:px }} h\ + do-args-correct (F x) {{ lp:K lp:x }} (R x px h) +]. + +do-args-correct T K {{ lp:B : eqb_correct_on lp:Cmp lp:K }} :- std.do! [ + eqb-for T Cmp, + coq.safe-dest-app T (global (indt I)) Args, + fields-for I _ _ _ ConstructPC, + coq.mk-app (global (const ConstructPC)) Args ConstructP, + eqb-fields T Fields, + B = {{ @eqb_body_correct _ _ _ _ _ lp:ConstructP lp:Fields lp:K (fun f => _) }}, + coq.typecheck {{ lp:B : eqb_correct_on lp:Cmp lp:K }} _ _, + coq.ltac.collect-goals B [G] _, + run-solver G "eqb_correct_on__solver", +]. + +pred add-indu-correct i:term, i:term, i:term, i:list term, o:term. +add-indu-correct (prod N T F) Indu IR LS {{ fun (a : lp:T) (eqA : a -> a -> bool) (eqAc : eqb_correct eqA) => lp:(R a eqA eqAc) }} :- !, + @pi-decl N T a\ + @pi-decl `eqA` {{ lp:a -> lp:a -> bool }} eqA\ + @pi-decl `eqAc` {{ @eqb_correct lp:a lp:eqA }} eqAc\ % super nasty "bug", the _ does not see a, if you write lp:{{ FOO a }} it works. Elaborating the skeleton is also ok, but then param1-inhab-db does not work well :-/ + param1-inhab-db {{ @eqb_correct_on lp:a lp:eqA }} eqAc => + add-indu-correct (F a) + {{ lp:Indu lp:a (@eqb_correct_on lp:a lp:eqA)}} + {{ lp:IR lp:a (@eqb_correct_on lp:a lp:eqA)}} + {std.map LS (t\coq.mk-app t [a, eqA])} (R a eqA eqAc). + +add-indu-correct _T Indu IR LS {{ fun x => lp:(R x) }} :- + std.assert! (param1-inhab-db IR Is_full) "not trivially inhabited", + @pi-decl `x` _ x\ + std.append LS [x, app[Is_full,x]] (Args x), + R x = app [Indu, _ | Args x]. + + +pred add-indu-correct-aux i:term, i:term, i:term, i:list term, o:term. +add-indu-correct-aux (prod N T F) Indu IR LS {{ fun (a : lp:T) (eqA : a -> a -> bool) => lp:(R a eqA) }} :- !, + @pi-decl N T a\ + @pi-decl `eqA` {{ lp:a -> lp:a -> bool }} eqA\ + add-indu-correct-aux (F a) + {{ lp:Indu lp:a (@eqb_correct_on lp:a lp:eqA)}} + {{ lp:IR lp:a (@eqb_correct_on lp:a lp:eqA)}} + {std.map LS (t\coq.mk-app t [a, eqA])} (R a eqA). +add-indu-correct-aux _T Indu IR LS R :- + R = app [Indu, _ | LS]. + +/******************************** Refl **************************************************************/ +pred add-decl-refl i:string, i:int, i:term, i:term, i:constructor, o:term. +add-decl-refl Prefix N I KT K R /*(global (const P))*/ :- std.do![ + do-params-refl N I KT (global (indc K)) R, + std.assert-ok! (coq.typecheck R Ty) "R casse", + % Name is Prefix ^ "eqb_refl_on_" ^ {coq.gref->id (indc K)}, + % coq.env.add-const Name R Ty @opaque! P, +]. + +% forall T : Type, T -> list T -> list T ---> forall a eqA, ..R.. +% T : Type |- T -> list T -> list T ---> +pred do-params-refl i:int, i:term, i:term, i:term, o:term. +do-params-refl 0 I T K R :- !, + eqb-for I Cmp, + reali I {{ @eqb_refl_on lp:I lp:Cmp }} => + do-args-refl T K R. +do-params-refl NP I (prod N T F) K {{ fun (a : lp:T) (eqA : a -> a -> bool) => lp:(R a eqA) }} :- NP > 0, !, NP1 is NP - 1, + @pi-decl N T a\ + @pi-decl `eqA` {{ lp:a -> lp:a -> bool }} eqA\ + eqb-for a eqA => + reali a {{ @eqb_refl_on lp:a lp:eqA }} => + do-params-refl NP1 {{ lp:I lp:a }} (F a) {{ lp:K lp:a }} (R a eqA). + +pred do-args-refl i:term, i:term, o:term. + +do-args-refl (prod N T F) K {{ fun (x : lp:T) (px : lp:EqbOn x) (h : @eqb_refl_on lp:T lp:Cmp x := lp:View x px) => lp:(R x px h) }} :- !, + reali T EqbOn, + eqb-for T Cmp, + eqb-refl-aux-for T View, + @pi-decl N T x\ + @pi-decl `px` {{ eqb_refl_on lp:Cmp lp:x }} px\ + @pi-def `H` {{ @eqb_refl_on lp:T lp:Cmp lp:x }} {{ lp:View lp:x lp:px }} h\ + do-args-refl (F x) {{ lp:K lp:x }} (R x px h). + +do-args-refl T K {{ lp:B : eqb_refl_on lp:Cmp lp:K }} :- std.do! [ + coq.safe-dest-app T (global (indt I)) Args, + tag-for I TagC, + fields-for I Fields_tC FieldsC _ _, + coq.mk-app (global (const TagC)) Args Tag, + coq.mk-app (global (const Fields_tC)) Args Fields_t, + coq.mk-app (global (const FieldsC)) Args Fields, + eqb-for T Cmp, + eqb-fields T EqbFields, + B = {{ @eqb_body_refl lp:T lp:Tag lp:Fields_t lp:Fields lp:EqbFields lp:K _ }}, + std.assert-ok! (coq.typecheck {{ lp:B (*: eqb_refl_on lp:Cmp lp:K*) }} _) "illtyped", + coq.ltac.collect-goals B [G] _, + run-solver G "eqb_refl_on__solver", +]. + +pred add-indu-refl i:term, i:term, i:term, i:list term, o:term. +add-indu-refl (prod N T F) Indu IR LS {{ fun (a : lp:T) (eqA : a -> a -> bool) (eqAc : eqb_reflexive eqA) => lp:(R a eqA eqAc) }} :- !, + @pi-decl N T a\ + @pi-decl `eqA` {{ lp:a -> lp:a -> bool }} eqA\ + @pi-decl `eqAr` {{ @eqb_reflexive lp:a lp:eqA }} eqAr\ % super nasty "bug", the _ does not see a, if you write lp:{{ FOO a }} it works. Elaborating the skeleton is also ok, but then param1-inhab-db does not work well :-/ + param1-inhab-db {{ @eqb_refl_on lp:a lp:eqA }} eqAr => + add-indu-refl (F a) + {{ lp:Indu lp:a (@eqb_refl_on lp:a lp:eqA)}} + {{ lp:IR lp:a (@eqb_refl_on lp:a lp:eqA)}} + {std.map LS (t\coq.mk-app t [a, eqA])} (R a eqA eqAr). + +add-indu-refl _T Indu IR LS {{ fun x => lp:(R x) }} :- + std.assert! (param1-inhab-db IR Is_full) "not trivially inhabited", + @pi-decl `x` _ x\ + std.append LS [x, app[Is_full,x]] (Args x), + R x = app [Indu, _ | Args x]. + +} diff --git a/src/eqbcorrect.v b/src/eqbcorrect.v new file mode 100644 index 0000000..4ab7613 --- /dev/null +++ b/src/eqbcorrect.v @@ -0,0 +1,78 @@ +From elpi Require Import elpi. +From elpi.apps Require Import derive. + +From Coq Require Import PArith ssreflect ssrfun ssrbool. +Open Scope positive_scope. + +Require Import core_defs. +Require Export tag fields eqb. + +Export ssreflect ssrbool ssrfun. (* otherwise the tactic fails *) +Ltac eqb_correct_on__solver := + by repeat (try case/andP; match reverse goal with H : @eqb_correct_on _ _ _ |- _ => move=> /=/H{H}-> end). +Ltac eqb_refl_on__solver := + rewrite /eqb_fields_refl_on /=; + by repeat (reflexivity || apply/andP; split; assumption). + +Elpi Db eqcorrect.db lp:{{ + + pred eqcorrect-for + o:inductive, + o:constant, % correct + o:constant. % reflexive + + pred eqb-refl-aux-for i:term, o:term. + + /* JC HERE + + pred eqb-correct-aux-for o:term, o:term. + eqb-correct-aux-for + {{ @eq_correct_on lp:T lp:F }} + {{ (fun (a : lp:T) (H : @eq_correct_on lp:T lp:F) => H) }}. + % + eqb-correct-aux-for + {{ option_is_option lp:T (@eqb_correct_on _ _) }} + {{ (fun (a : lp:T) (H : option_eqb_correct_aux lp:T lp:Cmp }}. + eqb-correct-aux-for + {{ option_is_option lp:T lp:P }} + {{ fun x H => option_is_option_functor lp:T _ (@eqb_correct_on _ _) (lp:Rec x H) }} :- + eqb-correct-aux-for P Rec. + + + eqb-correct-aux-for {{ list_is_list lp:A lp:P }} {{ list_eqb_correct_aux ... }} :- + eqb-correct-aux-for P X. + + option_is_option (list A) (list_is_list A (eqb_correct_on A FA)) + + :name "eqb-correct-aux-for:default" + eqb-correct-aux-for T {{ fun (x : lp:T) H => H }}. + */ + :name "eqb-refl-aux-for:default" + eqb-refl-aux-for T {{ fun (x : lp:T) H => H }}. + + + +}}. + +Elpi Command eqbcorrect. +Elpi Accumulate Db tag.db. +Elpi Accumulate Db eqb.db. +Elpi Accumulate Db fields.db. +Elpi Accumulate Db eqcorrect.db. +Elpi Accumulate Db derive.induction.db. +Elpi Accumulate Db derive.param1.inhab.db. +(*Elpi Accumulate Db derive.param1.functor.db. bad db shape *) +Elpi Accumulate File "src/elpi-ltac.elpi". +Elpi Accumulate File "src/eqbcorrect.elpi". +Elpi Accumulate File "src/paramX-lib.elpi". +Elpi Accumulate File "src/param1.elpi". +Elpi Accumulate Db derive.param1.db. +Elpi Accumulate lp:{{ + main [str S] :- + std.assert! (coq.locate S (indt I)) "Not an inductive type", + Prefix is S ^ "_", + eqbcorrect.main I Prefix _. +}}. +Elpi Typecheck. + +Elpi Print eqbcorrect. \ No newline at end of file diff --git a/src/fields.elpi b/src/fields.elpi new file mode 100644 index 0000000..9480a95 --- /dev/null +++ b/src/fields.elpi @@ -0,0 +1,155 @@ +namespace fields { + +pred fields_t. % chose between fields_t and construct +pred self o:term. + +pred main i:inductive, i:string, o:list prop. +main I Prefix CL :- std.do! [ + + std.assert! (tag-for I Tag) "no tag for this inductive, run that derivation first", + + coq.bind-ind-parameters I (_\ params\ _\ kty->tuple I params) Body_t, + std.assert-ok! (coq.typecheck Body_t Ty_t) "fields generates illtyped fields_t", + Name_t is Prefix ^ "fields_t", + coq.env.add-const Name_t Body_t Ty_t ff Fields_t, + + coq.env.indt I _ _ _ Arity _ _, + coq.bind-ind-arity (global (indt I)) Arity (repack-as-tuple Fields_t Tag) Body, + std.assert-ok! (coq.typecheck Body Ty) "fields generates illtyped fields", + Name is Prefix ^ "fields", + coq.env.add-const Name Body Ty ff Fields, + + coq.bind-ind-parameters I (_\ params\ _\ fun-tuple->kapp-proj Fields_t I params) Body_c, + std.assert-ok! (coq.typecheck Body_c Ty_c) "fields generates illtyped construct", + Name_c is Prefix ^ "construct", + coq.env.add-const Name_c Body_c Ty_c ff Construct, + + coq.bind-ind-arity (global (indt I)) Arity (case-refl Fields Construct) Body_P, + std.assert-ok! (coq.typecheck Body_P Ty_P) "fields generates illtyped constructP", + Name_P is Prefix ^ "constructP", + coq.env.add-const Name_P Body_P Ty_P @opaque! ConstructP, + + CL = [fields-for I Fields_t Fields Construct ConstructP], + std.forall CL (x\ coq.elpi.accumulate _ "fields.db" (clause _ _ x)), + +]. + +% match x return construct (fields x) = Some x with _ => erefl +pred case-refl i:constant, i:constant, i:term, i:list term, i:list term, o:term. +case-refl Fields Construct _ ParamsX Tys R :- + std.appendR Params [X] ParamsX, + coq.mk-app (global (const Fields)) Params FP, + coq.mk-app (global (const Construct)) Params CP, + coq.build-match X {std.last Tys} + (case-refl-rty FP CP) + case-refl-branch + R. + +pred case-refl-rty i:term, i:term, i:term, i:list term,i:list term, o:term. +case-refl-rty Fields Construct _ Vs _ {{ lp:Construct _ (lp:Fields lp:X) = Some lp:X }} :- + std.last Vs X. + +pred case-refl-branch i:term, i:term, i:list term,i:list term, o:term. +case-refl-branch _ _ _ _ {{ refl_equal }}. + +% match p with ... n => TyKn.1 * TyKn.2 ... +pred kty->tuple i:inductive, i:list term, o:term. +kty->tuple I Params {{ fun p : positive => lp:(R p) }} :- + coq.env.indt I _ _ _ _ _ KT, + std.map KT (coq.subst-prod Params) L, + @pi-decl `p` {{ positive }} p\ + splay-over-positive p L {{ fun _ => Type }} + {{ unit }} + prod->tuple + (R p). + +% match p with ... n => fun x => Kn x.1 x.2 ... +pred fun-tuple->kapp-proj i:constant, i:inductive, i:list term, o:term. +fun-tuple->kapp-proj C_t I Params {{ fun p : positive => lp:(R p) }} :- + coq.env.indt I _ _ _ _ KS KT, + coq.mk-app (global (const C_t)) Params Fields_t, + coq.mk-app (global (indt I)) Params Ind, + std.map KS (c\coq.mk-app (global (indc c)) Params) L1, + std.map KT (coq.subst-prod Params) L2, + std.zip L1 L2 L, + @pi-decl `p` {{ positive }} p\ + splay-over-positive p L {{ fun x => lp:Fields_t x -> option lp:Ind }} + {{ fun _ => None }} + fun-tuple->kapp + (R p). + +pred fun-tuple->kapp i:(pair term term), o:term. +fun-tuple->kapp (pr K Ty) {{ fun p => lp:(R p) }} :- + @pi-decl `p` _ p\ tuple->kapp Ty K p (R p). + +pred tuple->kapp i:term, i:term, i:term, o:term. +tuple->kapp (prod N T F) K P R :- F = (x\prod _ _ _), !, % not the last one + @pi-decl N T x\ tuple->kapp (F x) {coq.mk-app K [{{ fst lp:P }}]} {{ snd lp:P }} R. +tuple->kapp (prod N T F) K P R :- + @pi-decl N T x\ tuple->kapp (F x) {coq.mk-app K [P]} {{ snd lp:P }} R. +tuple->kapp _ K _ {{ Some lp:K }}. + +pred splay-over-positive i:term, i:list A, i:term, i:term, i:(A -> term -> prop), o:term. +splay-over-positive X L DoRty Def DoBranch R :- + splay-over-positive.aux X (x\x) L DoRty DoBranch Def R. +pred splay-over-positive.aux i:term, i:(term -> term), i:list A, i:term, i:(A -> term -> prop), i:term, o:term. +splay-over-positive.aux _ _ [] _ _ Def Def. +splay-over-positive.aux X XCtx KL DoRty DoBranch Def R :- + coq.build-match X {{ positive }} (do-rty XCtx DoRty) (do-branch XCtx DoRty DoBranch Def KL) R. + +pred do-rty i:(term -> term), i:term, i:term, i:list term,i:list term, o:term. +do-rty Ctx DoRty _ Vs _ R :- P = Ctx {std.last Vs}, whd1 {{ lp:DoRty lp:P }} R. + +pred list-bitmask i:list A, o:list A, o:list A. +list-bitmask [] [] []. +list-bitmask [X] [X] []. +list-bitmask [X,Y|L] [X|A] [Y|B] :- list-bitmask L A B. + +pred do-branch i:(term -> term), i:term, i:(A -> term -> prop), i:term, i:list A, i:term, i:term, i:list term, i:list term, o:term. +do-branch PCtx DoRty DoBranch Def [_|KS] {{ xO }} _ [P] _ R :- + list-bitmask KS KODD _, + splay-over-positive.aux P (x\ PCtx {{ xO lp:x }}) KODD DoRty DoBranch Def R. +do-branch PCtx DoRty DoBranch Def [_|KS] {{ xI }} _ [P] _ R :- + list-bitmask KS _ KEVEN, + splay-over-positive.aux P (x\ PCtx {{ xI lp:x }}) KEVEN DoRty DoBranch Def R. +do-branch _ _ DoBranch _ [X|_] {{ xH }} _ _ _ R :- DoBranch X R. + +pred prod->tuple i:term, o:term. +prod->tuple (prod N Ty F) {{ (lp:Ty * lp:X)%type }} :- (F = x\prod _ _ _), !, % not the last one + @pi-decl N Ty x\ prod->tuple (F x) X. +prod->tuple (prod _ Ty _) Ty. +prod->tuple _ {{ unit }}. % other branches + +pred repack-as-tuple i:constant, i:constant, i:term, i:list term, i:list term, o:term. +repack-as-tuple C_t Tag _ Vars Tys R :- + std.appendR Params [X] Vars, + std.last Tys XTy, + coq.mk-app (global (const C_t)) Params C_tp, + coq.mk-app (global (const Tag)) Params Tagp, + coq.build-match X XTy (do-rty_t C_tp Tagp) args->tuple R. + +pred do-rty_t i:term, i:term, i:term, i:list term,i:list term, o:term. +do-rty_t C_t Tag _ Vars _ {{ lp:C_t (lp:Tag lp:X) }} :- std.last Vars X. + +pred args->tuple i:term, i:term, i:list term, i:list term, o:term. +args->tuple _ _ [] _ {{ tt }}. +args->tuple _ _ [X] _ X. +args->tuple A B [X|XS] C {{ ( lp:X , lp:R ) }} :- + args->tuple A B XS C R. + +% TODO: move in coq-lib.elpi +pred coq.bind-ind-parameters i:inductive, i:(term -> list term -> list term -> term -> prop), o:term. +coq.bind-ind-parameters I K O :- + coq.env.indt I _ _ N A _ _, + coq.bind-ind-parameters.aux N A [] [] K O. +coq.bind-ind-parameters.aux 0 Ty Vars Tys K O :- !, K Ty {std.rev Vars} {std.rev Tys} O. +coq.bind-ind-parameters.aux I (prod N T F) Vs Ts K (fun N T G) :- I > 0, !, J is I - 1, + @pi-decl N T x\ + coq.bind-ind-parameters.aux J (F x) [x|Vs] [T|Ts] K (G x). +coq.bind-ind-parameters.aux I (let N T B F) Vs Ts K (fun N T G) :- I > 0, !, J is I - 1, + @pi-def N T B x\ + coq.bind-ind-parameters.aux J (F x) [x|Vs] [T|Ts] K (G x). +coq.bind-ind-parameters.aux I T Vs Ts K O :- I > 0, whd1 T T', !, + coq.bind-ind-parameters.aux I T' Vs Ts K O. + +} \ No newline at end of file diff --git a/src/fields.v b/src/fields.v new file mode 100644 index 0000000..2a04a61 --- /dev/null +++ b/src/fields.v @@ -0,0 +1,31 @@ +From elpi Require Import elpi. +From Coq Require Import PArith. +Require Export tag. +Open Scope positive_scope. + +Elpi Db fields.db lp:{{ + +% this is how one registers the fields_t, fields and construct[P] +% constants to an inductive and let other elpi commands use that piece of info +pred fields-for + o:inductive, + o:constant, % fields_t + o:constant, % fields + o:constant, % construct + o:constant. % constructP + +}}. + +Elpi Command fields. +Elpi Accumulate File "src/fields.elpi". +Elpi Accumulate Db tag.db. +Elpi Accumulate Db fields.db. +Elpi Accumulate lp:{{ + + main [str S] :- + std.assert! (coq.locate S (indt I)) "Not an inductive type", + Prefix is S ^ "_", + fields.main I Prefix _. + +}}. +Elpi Typecheck. diff --git a/src/large_defs.v b/src/large_defs.v index c3f6903..ecc17e0 100644 --- a/src/large_defs.v +++ b/src/large_defs.v @@ -1,13 +1,6 @@ -Require Import Eqdep_dec. - -From mathcomp Require Import all_ssreflect. -Require Import core_defs. +From elpi.apps Require Import derive. Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. -Require Import PArith. -Open Scope positive_scope. Inductive t := | T1 @@ -208,655 +201,206 @@ Inductive t := | T196 | T197 | T198 -| T199. - -Module AUX. - -Definition tag (x : t) := - match x with - | T1 => 1 - | T2 => 2 - | T3 => 3 - | T4 => 4 - | T5 => 5 - | T6 => 6 - | T7 => 7 - | T8 => 8 - | T9 => 9 - | T10 => 10 - | T11 => 11 - | T12 => 12 - | T13 => 13 - | T14 => 14 - | T15 => 15 - | T16 => 16 - | T17 => 17 - | T18 => 18 - | T19 => 19 - | T20 => 20 - | T21 => 21 - | T22 => 22 - | T23 => 23 - | T24 => 24 - | T25 => 25 - | T26 => 26 - | T27 => 27 - | T28 => 28 - | T29 => 29 - | T30 => 30 - | T31 => 31 - | T32 => 32 - | T33 => 33 - | T34 => 34 - | T35 => 35 - | T36 => 36 - | T37 => 37 - | T38 => 38 - | T39 => 39 - | T40 => 40 - | T41 => 41 - | T42 => 42 - | T43 => 43 - | T44 => 44 - | T45 => 45 - | T46 => 46 - | T47 => 47 - | T48 => 48 - | T49 => 49 - | T50 => 50 - | T51 => 51 - | T52 => 52 - | T53 => 53 - | T54 => 54 - | T55 => 55 - | T56 => 56 - | T57 => 57 - | T58 => 58 - | T59 => 59 - | T60 => 60 - | T61 => 61 - | T62 => 62 - | T63 => 63 - | T64 => 64 - | T65 => 65 - | T66 => 66 - | T67 => 67 - | T68 => 68 - | T69 => 69 - | T70 => 70 - | T71 => 71 - | T72 => 72 - | T73 => 73 - | T74 => 74 - | T75 => 75 - | T76 => 76 - | T77 => 77 - | T78 => 78 - | T79 => 79 - | T80 => 80 - | T81 => 81 - | T82 => 82 - | T83 => 83 - | T84 => 84 - | T85 => 85 - | T86 => 86 - | T87 => 87 - | T88 => 88 - | T89 => 89 - | T90 => 90 - | T91 => 91 - | T92 => 92 - | T93 => 93 - | T94 => 94 - | T95 => 95 - | T96 => 96 - | T97 => 97 - | T98 => 98 - | T99 => 99 - | T100 => 100 - | T101 => 101 - | T102 => 102 - | T103 => 103 - | T104 => 104 - | T105 => 105 - | T106 => 106 - | T107 => 107 - | T108 => 108 - | T109 => 109 - | T110 => 110 - | T111 => 111 - | T112 => 112 - | T113 => 113 - | T114 => 114 - | T115 => 115 - | T116 => 116 - | T117 => 117 - | T118 => 118 - | T119 => 119 - | T120 => 120 - | T121 => 121 - | T122 => 122 - | T123 => 123 - | T124 => 124 - | T125 => 125 - | T126 => 126 - | T127 => 127 - | T128 => 128 - | T129 => 129 - | T130 => 130 - | T131 => 131 - | T132 => 132 - | T133 => 133 - | T134 => 134 - | T135 => 135 - | T136 => 136 - | T137 => 137 - | T138 => 138 - | T139 => 139 - | T140 => 140 - | T141 => 141 - | T142 => 142 - | T143 => 143 - | T144 => 144 - | T145 => 145 - | T146 => 146 - | T147 => 147 - | T148 => 148 - | T149 => 149 - | T150 => 150 - | T151 => 151 - | T152 => 152 - | T153 => 153 - | T154 => 154 - | T155 => 155 - | T156 => 156 - | T157 => 157 - | T158 => 158 - | T159 => 159 - | T160 => 160 - | T161 => 161 - | T162 => 162 - | T163 => 163 - | T164 => 164 - | T165 => 165 - | T166 => 166 - | T167 => 167 - | T168 => 168 - | T169 => 169 - | T170 => 170 - | T171 => 171 - | T172 => 172 - | T173 => 173 - | T174 => 174 - | T175 => 175 - | T176 => 176 - | T177 => 177 - | T178 => 178 - | T179 => 179 - | T180 => 180 - | T181 => 181 - | T182 => 182 - | T183 => 183 - | T184 => 184 - | T185 => 185 - | T186 => 186 - | T187 => 187 - | T188 => 188 - | T189 => 189 - | T190 => 190 - | T191 => 191 - | T192 => 192 - | T193 => 193 - | T194 => 194 - | T195 => 195 - | T196 => 196 - | T197 => 197 - | T198 => 198 - | T199 => 199 - end. - -Definition fields_t (p:positive) : Type := unit. - -Definition fields (x:t) : fields_t (tag x) := tt. - -Definition construct (p:positive) : fields_t p -> option t := - match p with - | 1 => fun _ => Some T1 - | 2 => fun _ => Some T2 - | 3 => fun _ => Some T3 - | 4 => fun _ => Some T4 - | 5 => fun _ => Some T5 - | 6 => fun _ => Some T6 - | 7 => fun _ => Some T7 - | 8 => fun _ => Some T8 - | 9 => fun _ => Some T9 - | 10 => fun _ => Some T10 - | 11 => fun _ => Some T11 - | 12 => fun _ => Some T12 - | 13 => fun _ => Some T13 - | 14 => fun _ => Some T14 - | 15 => fun _ => Some T15 - | 16 => fun _ => Some T16 - | 17 => fun _ => Some T17 - | 18 => fun _ => Some T18 - | 19 => fun _ => Some T19 - | 20 => fun _ => Some T20 - | 21 => fun _ => Some T21 - | 22 => fun _ => Some T22 - | 23 => fun _ => Some T23 - | 24 => fun _ => Some T24 - | 25 => fun _ => Some T25 - | 26 => fun _ => Some T26 - | 27 => fun _ => Some T27 - | 28 => fun _ => Some T28 - | 29 => fun _ => Some T29 - | 30 => fun _ => Some T30 - | 31 => fun _ => Some T31 - | 32 => fun _ => Some T32 - | 33 => fun _ => Some T33 - | 34 => fun _ => Some T34 - | 35 => fun _ => Some T35 - | 36 => fun _ => Some T36 - | 37 => fun _ => Some T37 - | 38 => fun _ => Some T38 - | 39 => fun _ => Some T39 - | 40 => fun _ => Some T40 - | 41 => fun _ => Some T41 - | 42 => fun _ => Some T42 - | 43 => fun _ => Some T43 - | 44 => fun _ => Some T44 - | 45 => fun _ => Some T45 - | 46 => fun _ => Some T46 - | 47 => fun _ => Some T47 - | 48 => fun _ => Some T48 - | 49 => fun _ => Some T49 - | 50 => fun _ => Some T50 - | 51 => fun _ => Some T51 - | 52 => fun _ => Some T52 - | 53 => fun _ => Some T53 - | 54 => fun _ => Some T54 - | 55 => fun _ => Some T55 - | 56 => fun _ => Some T56 - | 57 => fun _ => Some T57 - | 58 => fun _ => Some T58 - | 59 => fun _ => Some T59 - | 60 => fun _ => Some T60 - | 61 => fun _ => Some T61 - | 62 => fun _ => Some T62 - | 63 => fun _ => Some T63 - | 64 => fun _ => Some T64 - | 65 => fun _ => Some T65 - | 66 => fun _ => Some T66 - | 67 => fun _ => Some T67 - | 68 => fun _ => Some T68 - | 69 => fun _ => Some T69 - | 70 => fun _ => Some T70 - | 71 => fun _ => Some T71 - | 72 => fun _ => Some T72 - | 73 => fun _ => Some T73 - | 74 => fun _ => Some T74 - | 75 => fun _ => Some T75 - | 76 => fun _ => Some T76 - | 77 => fun _ => Some T77 - | 78 => fun _ => Some T78 - | 79 => fun _ => Some T79 - | 80 => fun _ => Some T80 - | 81 => fun _ => Some T81 - | 82 => fun _ => Some T82 - | 83 => fun _ => Some T83 - | 84 => fun _ => Some T84 - | 85 => fun _ => Some T85 - | 86 => fun _ => Some T86 - | 87 => fun _ => Some T87 - | 88 => fun _ => Some T88 - | 89 => fun _ => Some T89 - | 90 => fun _ => Some T90 - | 91 => fun _ => Some T91 - | 92 => fun _ => Some T92 - | 93 => fun _ => Some T93 - | 94 => fun _ => Some T94 - | 95 => fun _ => Some T95 - | 96 => fun _ => Some T96 - | 97 => fun _ => Some T97 - | 98 => fun _ => Some T98 - | 99 => fun _ => Some T99 - | 100 => fun _ => Some T100 - | 101 => fun _ => Some T101 - | 102 => fun _ => Some T102 - | 103 => fun _ => Some T103 - | 104 => fun _ => Some T104 - | 105 => fun _ => Some T105 - | 106 => fun _ => Some T106 - | 107 => fun _ => Some T107 - | 108 => fun _ => Some T108 - | 109 => fun _ => Some T109 - | 110 => fun _ => Some T110 - | 111 => fun _ => Some T111 - | 112 => fun _ => Some T112 - | 113 => fun _ => Some T113 - | 114 => fun _ => Some T114 - | 115 => fun _ => Some T115 - | 116 => fun _ => Some T116 - | 117 => fun _ => Some T117 - | 118 => fun _ => Some T118 - | 119 => fun _ => Some T119 - | 120 => fun _ => Some T120 - | 121 => fun _ => Some T121 - | 122 => fun _ => Some T122 - | 123 => fun _ => Some T123 - | 124 => fun _ => Some T124 - | 125 => fun _ => Some T125 - | 126 => fun _ => Some T126 - | 127 => fun _ => Some T127 - | 128 => fun _ => Some T128 - | 129 => fun _ => Some T129 - | 130 => fun _ => Some T130 - | 131 => fun _ => Some T131 - | 132 => fun _ => Some T132 - | 133 => fun _ => Some T133 - | 134 => fun _ => Some T134 - | 135 => fun _ => Some T135 - | 136 => fun _ => Some T136 - | 137 => fun _ => Some T137 - | 138 => fun _ => Some T138 - | 139 => fun _ => Some T139 - | 140 => fun _ => Some T140 - | 141 => fun _ => Some T141 - | 142 => fun _ => Some T142 - | 143 => fun _ => Some T143 - | 144 => fun _ => Some T144 - | 145 => fun _ => Some T145 - | 146 => fun _ => Some T146 - | 147 => fun _ => Some T147 - | 148 => fun _ => Some T148 - | 149 => fun _ => Some T149 - | 150 => fun _ => Some T150 - | 151 => fun _ => Some T151 - | 152 => fun _ => Some T152 - | 153 => fun _ => Some T153 - | 154 => fun _ => Some T154 - | 155 => fun _ => Some T155 - | 156 => fun _ => Some T156 - | 157 => fun _ => Some T157 - | 158 => fun _ => Some T158 - | 159 => fun _ => Some T159 - | 160 => fun _ => Some T160 - | 161 => fun _ => Some T161 - | 162 => fun _ => Some T162 - | 163 => fun _ => Some T163 - | 164 => fun _ => Some T164 - | 165 => fun _ => Some T165 - | 166 => fun _ => Some T166 - | 167 => fun _ => Some T167 - | 168 => fun _ => Some T168 - | 169 => fun _ => Some T169 - | 170 => fun _ => Some T170 - | 171 => fun _ => Some T171 - | 172 => fun _ => Some T172 - | 173 => fun _ => Some T173 - | 174 => fun _ => Some T174 - | 175 => fun _ => Some T175 - | 176 => fun _ => Some T176 - | 177 => fun _ => Some T177 - | 178 => fun _ => Some T178 - | 179 => fun _ => Some T179 - | 180 => fun _ => Some T180 - | 181 => fun _ => Some T181 - | 182 => fun _ => Some T182 - | 183 => fun _ => Some T183 - | 184 => fun _ => Some T184 - | 185 => fun _ => Some T185 - | 186 => fun _ => Some T186 - | 187 => fun _ => Some T187 - | 188 => fun _ => Some T188 - | 189 => fun _ => Some T189 - | 190 => fun _ => Some T190 - | 191 => fun _ => Some T191 - | 192 => fun _ => Some T192 - | 193 => fun _ => Some T193 - | 194 => fun _ => Some T194 - | 195 => fun _ => Some T195 - | 196 => fun _ => Some T196 - | 197 => fun _ => Some T197 - | 198 => fun _ => Some T198 - | 199 => fun _ => Some T199 - | _ => fun _ => None - end. - -Lemma constructP x : construct (fields x) = Some x. -Proof. by case: x. Qed. - -End AUX. - -Local Instance t_obj : @obj t := - {| tag := AUX.tag - ; fields_t := AUX.fields_t - ; fields := AUX.fields - ; construct := AUX.construct - ; constructP := AUX.constructP |}. - -Definition eqb_fields (t:positive) : fields_t t -> fields_t t -> bool := - eq_op. - -(* Remark this is unusefull for this kind of type. - This pattern is usefull only for recursive type or for polymorphic type (this allows to use the definition for nested inductive *) -Definition eqb (x1 x2:t) := - match x1 with - | T1 => eqb_body eqb_fields (t1:=1 ) tt x2 - | T2 => eqb_body eqb_fields (t1:=2 ) tt x2 - | T3 => eqb_body eqb_fields (t1:=3 ) tt x2 - | T4 => eqb_body eqb_fields (t1:=4 ) tt x2 - | T5 => eqb_body eqb_fields (t1:=5 ) tt x2 - | T6 => eqb_body eqb_fields (t1:=6 ) tt x2 - | T7 => eqb_body eqb_fields (t1:=7 ) tt x2 - | T8 => eqb_body eqb_fields (t1:=8 ) tt x2 - | T9 => eqb_body eqb_fields (t1:=9 ) tt x2 - | T10 => eqb_body eqb_fields (t1:=10 ) tt x2 - | T11 => eqb_body eqb_fields (t1:=11 ) tt x2 - | T12 => eqb_body eqb_fields (t1:=12 ) tt x2 - | T13 => eqb_body eqb_fields (t1:=13 ) tt x2 - | T14 => eqb_body eqb_fields (t1:=14 ) tt x2 - | T15 => eqb_body eqb_fields (t1:=15 ) tt x2 - | T16 => eqb_body eqb_fields (t1:=16 ) tt x2 - | T17 => eqb_body eqb_fields (t1:=17 ) tt x2 - | T18 => eqb_body eqb_fields (t1:=18 ) tt x2 - | T19 => eqb_body eqb_fields (t1:=19 ) tt x2 - | T20 => eqb_body eqb_fields (t1:=20 ) tt x2 - | T21 => eqb_body eqb_fields (t1:=21 ) tt x2 - | T22 => eqb_body eqb_fields (t1:=22 ) tt x2 - | T23 => eqb_body eqb_fields (t1:=23 ) tt x2 - | T24 => eqb_body eqb_fields (t1:=24 ) tt x2 - | T25 => eqb_body eqb_fields (t1:=25 ) tt x2 - | T26 => eqb_body eqb_fields (t1:=26 ) tt x2 - | T27 => eqb_body eqb_fields (t1:=27 ) tt x2 - | T28 => eqb_body eqb_fields (t1:=28 ) tt x2 - | T29 => eqb_body eqb_fields (t1:=29 ) tt x2 - | T30 => eqb_body eqb_fields (t1:=30 ) tt x2 - | T31 => eqb_body eqb_fields (t1:=31 ) tt x2 - | T32 => eqb_body eqb_fields (t1:=32 ) tt x2 - | T33 => eqb_body eqb_fields (t1:=33 ) tt x2 - | T34 => eqb_body eqb_fields (t1:=34 ) tt x2 - | T35 => eqb_body eqb_fields (t1:=35 ) tt x2 - | T36 => eqb_body eqb_fields (t1:=36 ) tt x2 - | T37 => eqb_body eqb_fields (t1:=37 ) tt x2 - | T38 => eqb_body eqb_fields (t1:=38 ) tt x2 - | T39 => eqb_body eqb_fields (t1:=39 ) tt x2 - | T40 => eqb_body eqb_fields (t1:=40 ) tt x2 - | T41 => eqb_body eqb_fields (t1:=41 ) tt x2 - | T42 => eqb_body eqb_fields (t1:=42 ) tt x2 - | T43 => eqb_body eqb_fields (t1:=43 ) tt x2 - | T44 => eqb_body eqb_fields (t1:=44 ) tt x2 - | T45 => eqb_body eqb_fields (t1:=45 ) tt x2 - | T46 => eqb_body eqb_fields (t1:=46 ) tt x2 - | T47 => eqb_body eqb_fields (t1:=47 ) tt x2 - | T48 => eqb_body eqb_fields (t1:=48 ) tt x2 - | T49 => eqb_body eqb_fields (t1:=49 ) tt x2 - | T50 => eqb_body eqb_fields (t1:=50 ) tt x2 - | T51 => eqb_body eqb_fields (t1:=51 ) tt x2 - | T52 => eqb_body eqb_fields (t1:=52 ) tt x2 - | T53 => eqb_body eqb_fields (t1:=53 ) tt x2 - | T54 => eqb_body eqb_fields (t1:=54 ) tt x2 - | T55 => eqb_body eqb_fields (t1:=55 ) tt x2 - | T56 => eqb_body eqb_fields (t1:=56 ) tt x2 - | T57 => eqb_body eqb_fields (t1:=57 ) tt x2 - | T58 => eqb_body eqb_fields (t1:=58 ) tt x2 - | T59 => eqb_body eqb_fields (t1:=59 ) tt x2 - | T60 => eqb_body eqb_fields (t1:=60 ) tt x2 - | T61 => eqb_body eqb_fields (t1:=61 ) tt x2 - | T62 => eqb_body eqb_fields (t1:=62 ) tt x2 - | T63 => eqb_body eqb_fields (t1:=63 ) tt x2 - | T64 => eqb_body eqb_fields (t1:=64 ) tt x2 - | T65 => eqb_body eqb_fields (t1:=65 ) tt x2 - | T66 => eqb_body eqb_fields (t1:=66 ) tt x2 - | T67 => eqb_body eqb_fields (t1:=67 ) tt x2 - | T68 => eqb_body eqb_fields (t1:=68 ) tt x2 - | T69 => eqb_body eqb_fields (t1:=69 ) tt x2 - | T70 => eqb_body eqb_fields (t1:=70 ) tt x2 - | T71 => eqb_body eqb_fields (t1:=71 ) tt x2 - | T72 => eqb_body eqb_fields (t1:=72 ) tt x2 - | T73 => eqb_body eqb_fields (t1:=73 ) tt x2 - | T74 => eqb_body eqb_fields (t1:=74 ) tt x2 - | T75 => eqb_body eqb_fields (t1:=75 ) tt x2 - | T76 => eqb_body eqb_fields (t1:=76 ) tt x2 - | T77 => eqb_body eqb_fields (t1:=77 ) tt x2 - | T78 => eqb_body eqb_fields (t1:=78 ) tt x2 - | T79 => eqb_body eqb_fields (t1:=79 ) tt x2 - | T80 => eqb_body eqb_fields (t1:=80 ) tt x2 - | T81 => eqb_body eqb_fields (t1:=81 ) tt x2 - | T82 => eqb_body eqb_fields (t1:=82 ) tt x2 - | T83 => eqb_body eqb_fields (t1:=83 ) tt x2 - | T84 => eqb_body eqb_fields (t1:=84 ) tt x2 - | T85 => eqb_body eqb_fields (t1:=85 ) tt x2 - | T86 => eqb_body eqb_fields (t1:=86 ) tt x2 - | T87 => eqb_body eqb_fields (t1:=87 ) tt x2 - | T88 => eqb_body eqb_fields (t1:=88 ) tt x2 - | T89 => eqb_body eqb_fields (t1:=89 ) tt x2 - | T90 => eqb_body eqb_fields (t1:=90 ) tt x2 - | T91 => eqb_body eqb_fields (t1:=91 ) tt x2 - | T92 => eqb_body eqb_fields (t1:=92 ) tt x2 - | T93 => eqb_body eqb_fields (t1:=93 ) tt x2 - | T94 => eqb_body eqb_fields (t1:=94 ) tt x2 - | T95 => eqb_body eqb_fields (t1:=95 ) tt x2 - | T96 => eqb_body eqb_fields (t1:=96 ) tt x2 - | T97 => eqb_body eqb_fields (t1:=97 ) tt x2 - | T98 => eqb_body eqb_fields (t1:=98 ) tt x2 - | T99 => eqb_body eqb_fields (t1:=99 ) tt x2 - | T100 => eqb_body eqb_fields (t1:=100) tt x2 - | T101 => eqb_body eqb_fields (t1:=101) tt x2 - | T102 => eqb_body eqb_fields (t1:=102) tt x2 - | T103 => eqb_body eqb_fields (t1:=103) tt x2 - | T104 => eqb_body eqb_fields (t1:=104) tt x2 - | T105 => eqb_body eqb_fields (t1:=105) tt x2 - | T106 => eqb_body eqb_fields (t1:=106) tt x2 - | T107 => eqb_body eqb_fields (t1:=107) tt x2 - | T108 => eqb_body eqb_fields (t1:=108) tt x2 - | T109 => eqb_body eqb_fields (t1:=109) tt x2 - | T110 => eqb_body eqb_fields (t1:=110) tt x2 - | T111 => eqb_body eqb_fields (t1:=111) tt x2 - | T112 => eqb_body eqb_fields (t1:=112) tt x2 - | T113 => eqb_body eqb_fields (t1:=113) tt x2 - | T114 => eqb_body eqb_fields (t1:=114) tt x2 - | T115 => eqb_body eqb_fields (t1:=115) tt x2 - | T116 => eqb_body eqb_fields (t1:=116) tt x2 - | T117 => eqb_body eqb_fields (t1:=117) tt x2 - | T118 => eqb_body eqb_fields (t1:=118) tt x2 - | T119 => eqb_body eqb_fields (t1:=119) tt x2 - | T120 => eqb_body eqb_fields (t1:=120) tt x2 - | T121 => eqb_body eqb_fields (t1:=121) tt x2 - | T122 => eqb_body eqb_fields (t1:=122) tt x2 - | T123 => eqb_body eqb_fields (t1:=123) tt x2 - | T124 => eqb_body eqb_fields (t1:=124) tt x2 - | T125 => eqb_body eqb_fields (t1:=125) tt x2 - | T126 => eqb_body eqb_fields (t1:=126) tt x2 - | T127 => eqb_body eqb_fields (t1:=127) tt x2 - | T128 => eqb_body eqb_fields (t1:=128) tt x2 - | T129 => eqb_body eqb_fields (t1:=129) tt x2 - | T130 => eqb_body eqb_fields (t1:=130) tt x2 - | T131 => eqb_body eqb_fields (t1:=131) tt x2 - | T132 => eqb_body eqb_fields (t1:=132) tt x2 - | T133 => eqb_body eqb_fields (t1:=133) tt x2 - | T134 => eqb_body eqb_fields (t1:=134) tt x2 - | T135 => eqb_body eqb_fields (t1:=135) tt x2 - | T136 => eqb_body eqb_fields (t1:=136) tt x2 - | T137 => eqb_body eqb_fields (t1:=137) tt x2 - | T138 => eqb_body eqb_fields (t1:=138) tt x2 - | T139 => eqb_body eqb_fields (t1:=139) tt x2 - | T140 => eqb_body eqb_fields (t1:=140) tt x2 - | T141 => eqb_body eqb_fields (t1:=141) tt x2 - | T142 => eqb_body eqb_fields (t1:=142) tt x2 - | T143 => eqb_body eqb_fields (t1:=143) tt x2 - | T144 => eqb_body eqb_fields (t1:=144) tt x2 - | T145 => eqb_body eqb_fields (t1:=145) tt x2 - | T146 => eqb_body eqb_fields (t1:=146) tt x2 - | T147 => eqb_body eqb_fields (t1:=147) tt x2 - | T148 => eqb_body eqb_fields (t1:=148) tt x2 - | T149 => eqb_body eqb_fields (t1:=149) tt x2 - | T150 => eqb_body eqb_fields (t1:=150) tt x2 - | T151 => eqb_body eqb_fields (t1:=151) tt x2 - | T152 => eqb_body eqb_fields (t1:=152) tt x2 - | T153 => eqb_body eqb_fields (t1:=153) tt x2 - | T154 => eqb_body eqb_fields (t1:=154) tt x2 - | T155 => eqb_body eqb_fields (t1:=155) tt x2 - | T156 => eqb_body eqb_fields (t1:=156) tt x2 - | T157 => eqb_body eqb_fields (t1:=157) tt x2 - | T158 => eqb_body eqb_fields (t1:=158) tt x2 - | T159 => eqb_body eqb_fields (t1:=159) tt x2 - | T160 => eqb_body eqb_fields (t1:=160) tt x2 - | T161 => eqb_body eqb_fields (t1:=161) tt x2 - | T162 => eqb_body eqb_fields (t1:=162) tt x2 - | T163 => eqb_body eqb_fields (t1:=163) tt x2 - | T164 => eqb_body eqb_fields (t1:=164) tt x2 - | T165 => eqb_body eqb_fields (t1:=165) tt x2 - | T166 => eqb_body eqb_fields (t1:=166) tt x2 - | T167 => eqb_body eqb_fields (t1:=167) tt x2 - | T168 => eqb_body eqb_fields (t1:=168) tt x2 - | T169 => eqb_body eqb_fields (t1:=169) tt x2 - | T170 => eqb_body eqb_fields (t1:=170) tt x2 - | T171 => eqb_body eqb_fields (t1:=171) tt x2 - | T172 => eqb_body eqb_fields (t1:=172) tt x2 - | T173 => eqb_body eqb_fields (t1:=173) tt x2 - | T174 => eqb_body eqb_fields (t1:=174) tt x2 - | T175 => eqb_body eqb_fields (t1:=175) tt x2 - | T176 => eqb_body eqb_fields (t1:=176) tt x2 - | T177 => eqb_body eqb_fields (t1:=177) tt x2 - | T178 => eqb_body eqb_fields (t1:=178) tt x2 - | T179 => eqb_body eqb_fields (t1:=179) tt x2 - | T180 => eqb_body eqb_fields (t1:=180) tt x2 - | T181 => eqb_body eqb_fields (t1:=181) tt x2 - | T182 => eqb_body eqb_fields (t1:=182) tt x2 - | T183 => eqb_body eqb_fields (t1:=183) tt x2 - | T184 => eqb_body eqb_fields (t1:=184) tt x2 - | T185 => eqb_body eqb_fields (t1:=185) tt x2 - | T186 => eqb_body eqb_fields (t1:=186) tt x2 - | T187 => eqb_body eqb_fields (t1:=187) tt x2 - | T188 => eqb_body eqb_fields (t1:=188) tt x2 - | T189 => eqb_body eqb_fields (t1:=189) tt x2 - | T190 => eqb_body eqb_fields (t1:=190) tt x2 - | T191 => eqb_body eqb_fields (t1:=191) tt x2 - | T192 => eqb_body eqb_fields (t1:=192) tt x2 - | T193 => eqb_body eqb_fields (t1:=193) tt x2 - | T194 => eqb_body eqb_fields (t1:=194) tt x2 - | T195 => eqb_body eqb_fields (t1:=195) tt x2 - | T196 => eqb_body eqb_fields (t1:=196) tt x2 - | T197 => eqb_body eqb_fields (t1:=197) tt x2 - | T198 => eqb_body eqb_fields (t1:=198) tt x2 - | T199 => eqb_body eqb_fields (t1:=199) tt x2 - end. - -Lemma eqb_correct (x : t) : eqb_correct_on eqb x. -Proof. - by case: x; - rewrite /eqb_correct_on /eqb => ha htt; - apply (@eqb_body_correct _ t_obj eqb_fields). -Qed. - -Lemma eqb_refl (x:t) : eqb_refl_on eqb x. -Proof. - by case: x; apply (@eqb_body_refl _ t_obj eqb_fields). -Qed. - -Lemma eqbP (x1 x2 : t) : reflect (x1 = x2) (eqb x1 x2). -Proof. apply (iffP idP);[ apply eqb_correct | move=> ->; apply eqb_refl]. Qed. - - +| T199 +| U1 +| U2 +| U3 +| U4 +| U5 +| U6 +| U7 +| U8 +| U9 +| U10 +| U11 +| U12 +| U13 +| U14 +| U15 +| U16 +| U17 +| U18 +| U19 +| U20 +| U21 +| U22 +| U23 +| U24 +| U25 +| U26 +| U27 +| U28 +| U29 +| U30 +| U31 +| U32 +| U33 +| U34 +| U35 +| U36 +| U37 +| U38 +| U39 +| U40 +| U41 +| U42 +| U43 +| U44 +| U45 +| U46 +| U47 +| U48 +| U49 +| U50 +| U51 +| U52 +| U53 +| U54 +| U55 +| U56 +| U57 +| U58 +| U59 +| U60 +| U61 +| U62 +| U63 +| U64 +| U65 +| U66 +| U67 +| U68 +| U69 +| U70 +| U71 +| U72 +| U73 +| U74 +| U75 +| U76 +| U77 +| U78 +| U79 +| U80 +| U81 +| U82 +| U83 +| U84 +| U85 +| U86 +| U87 +| U88 +| U89 +| U90 +| U91 +| U92 +| U93 +| U94 +| U95 +| U96 +| U97 +| U98 +| U99 +| U100 +| U101 +| U102 +| U103 +| U104 +| U105 +| U106 +| U107 +| U108 +| U109 +| U110 +| U111 +| U112 +| U113 +| U114 +| U115 +| U116 +| U117 +| U118 +| U119 +| U120 +| U121 +| U122 +| U123 +| U124 +| U125 +| U126 +| U127 +| U128 +| U129 +| U130 +| U131 +| U132 +| U133 +| U134 +| U135 +| U136 +| U137 +| U138 +| U139 +| U140 +| U141 +| U142 +| U143 +| U144 +| U145 +| U146 +| U147 +| U148 +| U149 +| U150 +| U151 +| U152 +| U153 +| U154 +| U155 +| U156 +| U157 +| U158 +| U159 +| U160 +| U161 +| U162 +| U163 +| U164 +| U165 +| U166 +| U167 +| U168 +| U169 +| U170 +| U171 +| U172 +| U173 +| U174 +| U175 +| U176 +| U177 +| U178 +| U179 +| U180 +| U181 +| U182 +| U183 +| U184 +| U185 +| U186 +| U187 +| U188 +| U189 +| U190 +| U191 +| U192 +| U193 +| U194 +| U195 +| U196 +| U197 +| U198 +| U199 +. +Time #[only(induction,param1_trivial)] derive t. \ No newline at end of file diff --git a/src/large_defs2.v b/src/large_defs2.v new file mode 100644 index 0000000..3394d88 --- /dev/null +++ b/src/large_defs2.v @@ -0,0 +1,8 @@ +Require Import large_defs. +Require Import core_defs tag fields eqb eqbcorrect eqbP. + +Time Elpi tag t. +Time Elpi fields t. +Time Elpi eqb t. +Time Elpi eqbcorrect t. +Time Elpi eqbP t. diff --git a/src/list_defs.v b/src/list_defs.v index 8bdf5a7..599017b 100644 --- a/src/list_defs.v +++ b/src/list_defs.v @@ -1,144 +1,29 @@ -Require Import Eqdep_dec. - -From mathcomp Require Import all_ssreflect. -Require Import core_defs. +From elpi.apps Require Import derive. +Require Import core_defs tag fields eqb eqbcorrect eqbP. Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. -Require Import PArith. -Open Scope positive_scope. - -Section Ind. - - Context (A : Type) (PA : A -> Prop) (P : list A -> Prop). - Context (A_ind : forall a, PA a) (Hnil : P [::]) (Hcons : forall a l, PA a -> P l -> P (a::l)). - - Fixpoint list_Ind (l : list A) : P l := - match l with - | [::] => Hnil - | a :: l => Hcons (A_ind a) (list_Ind l) - end. - -End Ind. - -Module AUX. - -Section Section. -Context {A : Type}. - -Definition tag (x : list A) := - match x with - | [::] => 1 - | _ :: _ => 2 - end. - -Definition fields_t (t : positive) : Type := - match t with - | 2 => (A * list A)%type - | _ => unit - end. - -Definition fields (x : list A) : fields_t (tag x) := - match x return fields_t (tag x) with - | [::] => tt - | a::l => (a, l) - end. - -Definition construct (t:positive) : fields_t t -> option (list A) := - match t with - | 1 => fun _ => Some [::] - | 2 => fun p => Some (p.1 :: p.2) - | _ => fun _ => None - end. - -Lemma constructP x : construct (fields x) = Some x. -Proof. by case: x. Qed. - -End Section. End AUX. - -Local Instance list_obj (A:Type) : @obj (list A) := - {| tag := AUX.tag - ; fields_t := AUX.fields_t - ; fields := AUX.fields - ; construct := AUX.construct - ; constructP := AUX.constructP |}. - -Section Section. - -Context (A:Type) (Aeqb : A -> A -> bool). - -Section Fields. - -Context (eqb : list A -> list A -> bool). - -Definition eqb_fields (t:positive) : fields_t t -> fields_t t -> bool := - match t return fields_t t -> fields_t t -> bool with - | 1 => eq_op - | 2 => fun p1 p2 => Aeqb p1.1 p2.1 && eqb p1.2 p2.2 - | _ => eq_op - end. - -End Fields. - -Fixpoint eqb (x1 x2 : list A) := - match x1 with - | [::] => eqb_body (eqb_fields eqb) (t1:=1) tt x2 - | a::l => eqb_body (eqb_fields eqb) (t1:=2) (a,l) x2 - end. - -Lemma eqb_correct_on_nil : eqb_correct_on eqb nil. -Proof. - rewrite /eqb_correct_on /eqb. - by apply (@eqb_body_correct _ (list_obj A) (eqb_fields eqb) [::]). -Qed. - -Lemma eqb_correct_on_cons a l: - eqb_correct_on Aeqb a -> - eqb_correct_on eqb l -> - eqb_correct_on eqb (a :: l). -Proof. - rewrite /eqb_correct_on => ha hl. - apply (@eqb_body_correct _ (list_obj A) (eqb_fields eqb) (a :: l)). - by move=> a2 /andP[] /= /ha -> /hl ->. -Qed. - -Lemma eqb_refl_on_nil : eqb_refl_on eqb [::]. -Proof. done. Qed. - -Lemma eqb_refl_on_cons a l: - eqb_refl_on Aeqb a -> - eqb_refl_on eqb l -> - eqb_refl_on eqb (a :: l). -Proof. - rewrite /eqb_refl_on=> ha hl. - apply (@eqb_body_refl _ (list_obj A) (eqb_fields eqb) (a :: l)). - by rewrite /eqb_fields_refl_on /= ha hl. -Qed. - -End Section. - -Section EqType. - -Context (A:eqType). -Lemma eqb_correct (x:list A) : eqb_correct_on (eqb eq_op) x. -Proof. - elim: x => [ | a l hrec]. - + by apply eqb_correct_on_nil. - by apply eqb_correct_on_cons => // a'; apply /eqP. -Qed. +#[only(induction,param1_full,param1_trivial)] derive list. +Elpi tag list. +Elpi fields list. +Elpi eqb list. +Elpi eqbcorrect list. +Elpi eqbP list. -Lemma eqb_refl (x:list A) : eqb_refl_on (eqb eq_op) x. -Proof. - elim x => [ | a l hrec]. - + by apply eqb_refl_on_nil. - apply eqb_refl_on_cons => //; apply /eqxx. -Qed. +Check list_eqbP : eqtype.Equality.type -> eqtype.Equality.type. -Lemma eqbP (x1 x2 : list A) : reflect (x1 = x2) (eqb eq_op x1 x2). -Proof. apply (iffP idP);[ apply eqb_correct | move=> ->; apply eqb_refl]. Qed. +#[only(induction,param1_full,param1_trivial)] derive nat. +Elpi tag nat. +Elpi fields nat. +Elpi eqb nat. +Elpi eqbcorrect nat. +Elpi eqbP nat. -End EqType. +Check nat_eqbP : eqtype.Equality.type. +Import eqtype. +Goal (cons 1 nil == nil). +unfold eq_op. +unfold list_eqbP, list_eqb. +Abort. diff --git a/src/nested_defs.v b/src/nested_defs.v index ad85358..f5a63f6 100644 --- a/src/nested_defs.v +++ b/src/nested_defs.v @@ -1,18 +1,93 @@ -Require Import Eqdep_dec. -From mathcomp Require Import all_ssreflect. -Require Import PArith core_defs. -Require option_defs. -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. +From elpi.apps Require Import derive. +Require Import core_defs tag fields eqb eqbcorrect eqbP. -Open Scope positive_scope. +Require Import option_defs. Inductive t := | T0 | T1 of option t. + +#[only(induction,param1_functor,param1_trivial)] derive t. +About t_induction. +Elpi tag t. +Elpi fields t. +Elpi eqb t. + +Lemma option_some_correct : + forall (A : Type) (eqA : A -> A -> bool), + let PA := @eqb_correct_on A eqA in + let P := @eqb_correct_on (option A) (@option_eqb A eqA) in + forall s1 : option A, option_is_option A PA s1 -> P s1. +move=> A eqA PA P o. +apply: option_induction. + move=> x Px. +Admitted. + +reali A PA => + reali (list A) P => + + option (list A) ----< option_is_option A P + option (box A) ----< option_is_option A (box_is_box A PA) + + + +Lemma T1_correct : + let P := @eqb_correct_on t t_eqb in + forall s1 : t, t_is_t s1 -> P s1. +move=> P s1. +apply: t_induction. + move=> x Px. admit. + move=> x Px. + have H := @option_some_correct t t_eqb _ Px. + rewrite /P. + apply: @eqb_body_correct _ _ _ _ t_construct _ _ _ _. + apply: t_constructP. + rewrite /eqb_fields_correct_on /= -/t_eqb => y H1. + by rewrite (H _ H1). + + +About option_induction. + + + +About option_eqb_correct. +About t_induction. + + + + + (forall x : option t, option_is_option t (eqb_correct_on t_eqb) x -> + (eqb_correct_on t_eqb) (T1 x)) -> + + (forall x : option t, option_is_option (option_eqb t t_eqb) x -> + (eqb_correct_on t_eqb) (T1 x) + + + + +Elpi eqbcorrect t. +Elpi eqbP t. + (* +rec (t -> P) +IH : list t -> list_is_list P +bool -> bool_is_bool + +x : T +rec : P x + +IH -> (list_is_list P -> list_is_list Q) +*) + +(* + + + + + + + Section Ind. Context (Po : option t -> Prop) (P : t -> Prop). @@ -127,3 +202,4 @@ Qed. Lemma eqbP x1 x2 : reflect (x1 = x2) (eqb x1 x2). Proof. apply (iffP idP);[ apply eqb_correct | move=> ->; apply eqb_refl]. Qed. +*) diff --git a/src/option_defs.v b/src/option_defs.v index 22cf892..3b047a2 100644 --- a/src/option_defs.v +++ b/src/option_defs.v @@ -1,131 +1,83 @@ -Require Import Eqdep_dec. - -From mathcomp Require Import all_ssreflect. -Require Import core_defs. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. -Require Import PArith. -Open Scope positive_scope. - -Section Ind. - - Context (A : Type) (PA : A -> Prop) (P : option A -> Prop). - Context (A_ind : forall a, PA a) (Hnone : P None) (Hsome : forall a, PA a -> P (Some a)). - - Definition option_Ind (o : option A) : P o := - match o with - | None => Hnone - | Some a => Hsome (A_ind a) - end. - -End Ind. - -Module AUX. - -Section Section. -Context {A : Type}. - -Definition tag (x : option A) := - match x with - | None => 1 - | Some _ => 2 - end. - -Definition fields_t (t:positive) : Type := - match t with - | 2 => A - | _ => unit - end. - -Definition fields (x:option A) : fields_t (tag x) := - match x return fields_t (tag x) with - | None => tt - | Some a => a - end. - -Definition construct (t:positive) : fields_t t -> option (option A) := - match t with - | 1 => fun _ => Some None - | 2 => fun a => Some (Some a) - | _ => fun _ => None - end. - -Lemma constructP x : construct (fields x) = Some x. -Proof. by case: x. Qed. - -End Section. End AUX. - -Local Instance option_obj (A:Type) : @obj (option A) := - {| tag := AUX.tag - ; fields_t := AUX.fields_t - ; fields := AUX.fields - ; construct := AUX.construct - ; constructP := AUX.constructP |}. - -Section Section. - -Context (A:Type) (Aeqb : A -> A -> bool). - -Definition eqb_fields (t:positive) : fields_t t -> fields_t t -> bool := - match t return fields_t t -> fields_t t -> bool with - | 1 => eq_op - | 2 => Aeqb - | _ => eq_op - end. - -Definition eqb (x1 x2:option A) := - match x1 with - | None => eqb_body eqb_fields (t1:=1) tt x2 - | Some a => eqb_body eqb_fields (t1:=2) a x2 - end. - -Lemma eqb_correct_on_None : eqb_correct_on eqb None. +From elpi.apps Require Import derive. +Require Import core_defs tag fields eqb eqbcorrect eqbP. + +#[verbose,only(induction,param1_functor,param1_trivial)] derive option. +Elpi tag option. +Elpi fields option. +Elpi eqb option. +Elpi eqbcorrect option. +Elpi eqbP option. + +#[verbose,only(induction,param1_functor,param1_trivial)] derive list. +Elpi tag list. +Elpi fields list. +Elpi eqb list. +Elpi eqbcorrect list. +Elpi eqbP list. + +Lemma list_eqb_refl_aux (A : Type) (eqA : A -> A -> bool) (o : list A) : + @list_is_list A (@eqb_refl_on A eqA) o -> + @eqb_refl_on (list A) (list_eqb A eqA) o. +Admitted. + +Lemma option_eqb_refl_aux (A : Type) (eqA : A -> A -> bool) (o : option A) : + @option_is_option A (@eqb_refl_on A eqA) o -> + @eqb_refl_on (option A) (option_eqb A eqA) o. Proof. - rewrite /eqb_correct_on /eqb. - by apply (@eqb_body_correct _ (option_obj A) eqb_fields None). -Qed. +Admitted. -Lemma eqb_correct_on_Some a : - eqb_correct_on Aeqb a -> - eqb_correct_on eqb (Some a). -Proof. - rewrite /eqb_correct_on /eqb => ha. - apply (@eqb_body_correct _ (option_obj A) eqb_fields (Some a)). - by move=> a2 /ha ->. -Qed. -Lemma eqb_refl_on_None : eqb_refl_on eqb None. -Proof. done. Qed. +Inductive t := + | T0 + | T1 of option (list (option t)). -Lemma eqb_refl_on_Some a : - eqb_refl_on Aeqb a -> - eqb_refl_on eqb (Some a). -Proof. apply (@eqb_body_refl _ (option_obj A) eqb_fields (Some a)). Qed. -End Section. -Section EqType. +Elpi Accumulate eqcorrect.db lp:{{ -Context (A:eqType). -Lemma eqb_correct (x:option A) : eqb_correct_on (eqb eq_op) x. -Proof. - case: x => [ a | ]. - + by apply/eqb_correct_on_Some => x'; apply /eqP. - apply eqb_correct_on_None. -Qed. + % correct-lemma-for {{:gref list }} {{ list_eqb_correct_aux }}. + % correct-lemma-for {{:gref option }} {{ option_eqb_correct_aux }}. -Lemma eqb_refl (x:option A) : eqb_refl_on (eqb eq_op) x. -Proof. - case: x => [ a | ]. - + by apply/eqb_refl_on_Some/eqxx. - apply eqb_refl_on_None. -Qed. + functor-lemma-for {{:gref list }} {{ list_is_list_functor }}. + functor-lemma-for {{:gref option }} {{ option_is_option_functor }}. + + + +/* + :before "eqb-correct-aux-for:default" + eqb-correct-aux-for {{ list lp:X }} + {{ fun x H => list_eqb_correct_aux _ _ x (list_is_list_functor _ _ _ lp:Rec x H) }} :- + eqb-correct-aux-for X Rec. + + :before "eqb-correct-aux-for:default" + eqb-correct-aux-for {{ option lp:X }} + {{ fun x H => option_eqb_correct_aux _ _ x (option_is_option_functor _ _ _ lp:Rec x H) }} :- + eqb-correct-aux-for X Rec. + +*/ + + :before "eqb-refl-aux-for:default" + eqb-refl-aux-for {{ list lp:X }} + {{ fun x H => list_eqb_refl_aux _ _ x (list_is_list_functor _ _ _ lp:Rec x H) }} :- + eqb-refl-aux-for X Rec. + + :before "eqb-refl-aux-for:default" + eqb-refl-aux-for {{ option lp:X }} + {{ fun x H => option_eqb_refl_aux _ _ x (option_is_option_functor _ _ _ lp:Rec x H) }} :- + eqb-refl-aux-for X Rec. + +}}. + +#[only(induction,param1_functor,param1_trivial)] derive t. +Elpi tag t. +Elpi fields t. +Elpi eqb t. +Elpi eqbcorrect t. +Elpi eqbP t. + +Import eqtype. -Lemma eqbP (x1 x2 : option A) : reflect (x1 = x2) (eqb eq_op x1 x2). -Proof. apply (iffP idP);[ apply eqb_correct | move=> ->; apply eqb_refl]. Qed. +Check (forall x : t, x == x). -End EqType. diff --git a/src/param1.elpi b/src/param1.elpi new file mode 100644 index 0000000..4a250b7 --- /dev/null +++ b/src/param1.elpi @@ -0,0 +1,221 @@ +/* Unary parametricity translation (Realizability) */ +/* license: GNU Lesser General Public License Version 2.1 or later */ +/* ------------------------------------------------------------------------- */ + +% Author: Cyril Cohen + +shorten std.{forall, forall2, do!, rev, map2, map}. + +:before "subst-fun:fail" +coq.subst-fun XS T TXS :- !, coq.mk-app T XS TXS. + +% this is outside the namespace since the predicate is also the db-one +reali (sort prop as P) (fun `s` P x\ prod `s1` x _\ P) :- !. +reali (sort _) (fun `s` (sort (typ U)) x\ prod `s1` x _\ (sort (typ V))) :- !, + coq.univ.new [] U, coq.univ.new [] V. + +reali (fun N T B) (fun N T x\ fun N1 (TRsubst x) xR\ BR x xR) :- !, do! [ + coq.name-suffix `P` N N1, + reali T TR, + (pi x xR\ reali x xR => reali (B x) (BR x xR)), + (TRsubst = x\ {coq.subst-fun [x] TR}) +]. + +reali (prod N T P as Prod) ProdR :- !, do! [ + coq.name-suffix `P` N N1, + reali T TR, + (pi x xR\ reali x xR => reali (P x) (PR x xR)), + ProdR = fun `f` Prod f\ + prod N T x\ prod N1 {coq.subst-fun [x] TR} xR\ + {coq.subst-fun [{coq.mk-app f [x]}] (PR x xR)} +]. + +reali (app [A|Bs]) ARBsR :- !, do! [ + reali A AR, + derive.param1.reali-args Bs BsR, + coq.mk-app AR BsR ARBsR +]. + +reali (let N T V B) LetR :- !, std.do! [ + coq.name-suffix `P` N N1, + reali T TR, + reali V VR, + (pi x xR\ reali x xR => reali (B x) (BR x xR)), + LetR = let N T V x\ let N1 {coq.mk-app TR [x]} VR xR\ BR x xR +]. + +reali (match T P Bs) MR :- !, do! [ + reali T TR, + derive.param1.reali-match P PRM, + reali T TR => derive.param1.reali-map Bs BsR, + MR = match TR (PRM (x\ match x P Bs)) BsR +]. + +reali (fix N Rno T F as Fix) FixR :- !, std.do! [ + RnoR is 2 * Rno + 1, + RnoR1 is RnoR + 1, + reali T TR, + (pi x xR\ reali x xR => reali (F x) (FR x xR)), + (TRsubst = f\ {coq.subst-fun [f] TR}), + (pi f xR\ FixBody f xR = let N (TRsubst (F f)) (FR f xR) fr\ + {paramX.mk-trivial-match RnoR (TRsubst f) [] fr}), + (pi f xR\ coq.mk-eta RnoR1 (TRsubst f) (FixBody f xR) (EtaFixBody f xR)), + coq.name-suffix N 1 N1, + FixR = (let N T Fix f\ fix N1 RnoR (TRsubst f) xR\ EtaFixBody f xR), +]. + +namespace derive.param1 { + +pred reali-args o:list term, o:list term. +reali-args [] []. +reali-args [X|Xs] [X,XR|XsR] :- do! [ + reali X XR, + reali-args Xs XsR +]. + +pred reali-map o:list term, o:list term. +reali-map [] []. +reali-map [X|Xs] [XR|XsR] :- do! [ + reali X XR, + reali-map Xs XsR +]. + +% helpers for match return type +pred reali-match i:term, o:((term -> term) -> term). +reali-match (fun N T B) PRM :- pi x\ not (B x = fun _ _ _), !, do! [ + reali T TR, + (pi x xR\ reali x xR => reali (B x) (BR x xR)), + coq.name-suffix `P` N N1, + (pi z z1\ PRM z = + fun N T x\ fun N1 {coq.subst-fun [x] TR} xR\ {coq.mk-app (BR x xR) [z x]}) +]. + +reali-match (fun N T B) PRM :- do! [ + reali T TR, + (pi x xR\ reali x xR => reali-match (B x) (BR x xR)), + coq.name-suffix N 1 N1, + (pi z \ PRM z = fun N T x\ fun N1 {coq.subst-fun [x] TR} xR\ BR x xR z) +]. + +% Storage: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +pred reali-store + i:string, % Name suffix for the type class + i:term, % Term + i:term. % Translation +reali-store N X XR :- !, + Nreali is "reali_" ^ N, + Args = [_, _, X, XR], + T1 = app [{{ lib:@param1.store_reali }}|Args], + std.assert-ok! (coq.typecheck T1 T2) "reali-store: T1 illtyped", + coq.env.add-const Nreali T1 T2 _ GR, + @global! => coq.TC.declare-instance (const GR) 0. + +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)). + +% toplevel predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +pred dispatch + i:gref, % input of the translation + i:string, % the name + o:list prop. % the clause + +dispatch (const GR) Prefix Clauses :- !, do! [ + Term = global (const GR), + Name is Prefix ^ {coq.gref->id (const GR)}, + std.assert! (coq.env.const GR (some V) Ty) "param1: cannot handle axioms", + + reali V VR, + reali Ty TyR, + coq.mk-app TyR [V] TyRV, + % apparently calling the type checker with the expected type is weaker in this case + std.assert-ok! (coq.typecheck VR VRTy) "param1: illtyped constant", + std.assert-ok! (coq.unify-leq VRTy TyRV) "param1: constant does not have the right type", + + coq.env.add-const Name VR TyRV _ TermR, + + reali-store Name Term (global (const TermR)), + + C1 = (reali Term (global (const TermR)) :- !), + coq.elpi.accumulate _ "derive.param1.db" (clause _ (before "reali:fail") C1), + C2 = (realiR Term (global (const TermR)) :- !), + coq.elpi.accumulate _ "derive.param1.db" (clause _ (before "realiR:fail") C2), + Clauses = [C1, C2] +]. + +pred prefix-indc i:string, i:constructor, o:pair constructor id. +prefix-indc Prefix K (pr K NewName) :- + coq.gref->id (indc K) Name, NewName is Prefix ^ Name. + +dispatch (indt GR) Prefix Clauses :- !, do! [ + Ind = global (indt GR), + coq.env.indt GR _ _ Lno Ty Knames Ktypes, + + LnoR is 2 * Lno, + + pi new_name\ sigma KnamesR KtypesR TyR\ ( + reali Ind (global (indt new_name)) => reali Ty TyR, + reali Ind (global (indt new_name)) => + map2 Knames Ktypes (k\ ty\ r\ sigma tyr\ + reali ty tyr, coq.subst-fun [global (indc k)] tyr r) + KtypesR, + map Knames (prefix-indc Prefix) KnamesR, + + NewName is Prefix ^ {coq.gref->id (indt GR)}, + + coq.build-indt-decl + (pr new_name NewName) tt LnoR LnoR {coq.subst-fun [Ind] TyR} KnamesR KtypesR DeclR + ), + + std.assert-ok! (coq.typecheck-indt-decl DeclR) "derive.param1 generates illtyped inductive", + + coq.env.add-indt DeclR GRR, + + reali-store NewName Ind (global (indt GRR)), + coq.env.indt GRR _ _ _ _ RealNamesR _, + forall2 Knames RealNamesR (reali-store-indc NewName), + C1 = (reali Ind (global (indt GRR)) :- !), + coq.elpi.accumulate _ "derive.param1.db" (clause _ (before "reali:fail") C1), + C2 = (realiR Ind (global (indt GRR)) :- !), + coq.elpi.accumulate _ "derive.param1.db" (clause _ (before "realiR:fail") C2), + map2 Knames RealNamesR (a\ b\ r\ r = reali (global (indc a)) (global (indc b))) CK, + forall CK (c\ + coq.elpi.accumulate _ "derive.param1.db" (clause _ (before "reali:fail") c)), + Clauses = [C1,C2|CK] +]. + +dispatch (indc _) _ _ :- + coq.error "derive.param1: cannot translate a constructor". + +pred main i:gref, i:string, o:list prop. +main T Out Clauses :- dispatch T Out Clauses. + +} + +/* +%%%%%%%%%%%%%%%%%%%%% +% Tactic entrypoint % +%%%%%%%%%%%%%%%%%%%%% + +% We disable coq-refiner +:before "refiner-assign-evar" + evar _ _ _ :- !. + +pred ctx->TC i:(list prop), o:(list (pair term term)). +ctx->TC [] [] :- !. +ctx->TC [decl X _ Ty |Xs] [pr X Ty|Is] :- !, ctx->TC Xs Is. +ctx->TC [def X _ _ _ Ty |Xs] [pr X Ty|Is] :- !, ctx->TC Xs Is. + +solve _ [goal Ctx Ev (app[{{@reali}}, T, TR, X, XR]) _] _ :- !, + coq.sigma.print, + coq.say "goal->TC" {ctx->TC Ctx}, + coq.say "searching reali for" X, + reali T TR, + reali X XR, + Ev = app [{{@Reali}}, T, TR, X, XR], + coq.typecheck Ev Ty ok, + coq.say "Ty=" Ty. + +*/ diff --git a/src/paramX-lib.elpi b/src/paramX-lib.elpi new file mode 100644 index 0000000..ac1e744 --- /dev/null +++ b/src/paramX-lib.elpi @@ -0,0 +1,78 @@ +/* coq-elpi: Coq terms as the object language of elpi */ +/* license: GNU Lesser General Public License Version 2.1 or later */ +/* ------------------------------------------------------------------------- */ + +namespace paramX { + +pred mk-trivial-match i:int, i:term, i:list term, i:term, o:term. +mk-trivial-match Rno (prod N T P) Args F (fun N T B) :- Rno >= 0, !, std.do! [ + Rno' is Rno - 1, + (pi x\ decl x N T => mk-trivial-match Rno' (P x) [x|Args] F (B x)), +]. + +mk-trivial-match Rno Prod Args F R :- Rno >= 0, whd1 Prod Prod1, !, + mk-trivial-match Rno Prod1 Args F R. + +mk-trivial-match -1 P RArgs F Match :- std.do! [ + RArgs = [RecArg|ROtherArgs], + (decl RecArg _ T, unwind {whd T []} Twhd), % unneeded with elpi 1.13.7 + coq.safe-dest-app Twhd (global (indt I)) IndArgs, + coq.env.indt I _ Lno _ _ _ _, + std.drop Lno IndArgs RIndArgs, + coq.build-match RecArg T + (mk-trivial-match.rty {std.append RIndArgs [RecArg]} P) + (mk-trivial-match.branch Lno RIndArgs {std.rev ROtherArgs} F) Match, +]. + +pred mk-trivial-match.rty i:list term, i:term, i:term, i:list term, i:list term, o:term. +mk-trivial-match.rty Args P _ Vars _ R :- std.do! [ + std.map2 Args Vars (x\y\r\ r = copy x y) Subst, + Subst => copy P R, +]. + +pred mk-trivial-match.branch i:int, i:list term, i:list term, i:term, i:term, i:term, i:list term, i:list term, o:term. +mk-trivial-match.branch Lno Args OtherArgs F K KTy Vars _ R1 :- std.do! [ + coq.mk-app K Vars KArgs, + coq.safe-dest-app KTy _ KTyArgs, + std.drop Lno KTyArgs IdxVals, + std.map2 Args IdxVals (x\y\r\ r = copy x y) Subst, + (R = let `K` KTy KArgs x\ {coq.mk-app F {std.append OtherArgs [x]}}), + Subst => copy R R1, +]. + + +% prove H G P finds a P : H => G +pred prove i:term, i:term, o:term. +pred cross i:term. + +% prove-arg AppliedHyp AppliedGoal Argument ProofAppliedHyp Proof. +pred prove-arg i:term, i:term, i:term, i:term, o:term. + +prove-arg X X _ P P :- !. + +prove-arg (app [H|Hs]) (app[G|Gs]) X PHX PGX :- + std.appendR HArgs [X] Hs, coq.mk-app H HArgs Hyp, + std.appendR GArgs [X] Gs, coq.mk-app G GArgs Goal, + prove Hyp Goal Proof, + coq.mk-app Proof [X,PHX] PGX. + +prove-arg (prod _ X x\ prod _ (PX x) (H x)) (prod _ _ y\ prod _ (PX y) (G y)) A PA (fun `x` X x\ fun `px` (PX x) (Proof x)) :- + pi x px\ + prove-arg (H x px) (G x px) {coq.mk-app A [x]} {coq.mk-app PA [x,px]} (Proof x px). + +pred prove-args i:list term, i:list term, o:list term. +prove-args [] [] []. +prove-args [X,Pr|Args] [_,PX|ArgsT] [X,Proof|QArgs] :- + coq.safe-dest-app PX HD _, cross HD, !, + copy PX Goal, + (prove-arg PX Goal X Pr Proof ; Proof = Pr), !, + prove-args Args ArgsT QArgs. +prove-args [X|Args] [PX|ArgsT] [ProofX|QArgs] :- + copy PX Goal, + prove PX Goal Proof, !, + coq.mk-app Proof [X] ProofX, + prove-args Args ArgsT QArgs. +prove-args [X|Args] [_|ArgsT] [X|QArgs] :- + prove-args Args ArgsT QArgs. + +} \ No newline at end of file diff --git a/src/tag.elpi b/src/tag.elpi new file mode 100644 index 0000000..7d147f2 --- /dev/null +++ b/src/tag.elpi @@ -0,0 +1,56 @@ + +% not necessary, but gives pointers to relevant files +shorten std.{ fold-map , do! , spy-do!, last }. % from elpi-builtin.elpi +shorten coq.{ build-match , bind-ind-arity }. % from coq-lib.elpi +shorten coq.{ typecheck }. % from coq-builtin.elpi + +% if we load this file together with others files, we avoid chlashes +namespace tag { + +% we return the clauses for the tag.db since we may need them right away +% if we run other derivations immediately +pred main i:inductive, i:string, o:list prop. +main I Prefix CL :- do! [ + + % build fun params (x : I params) => ... do-match ... + coq.env.indt I _ _ _ Arity _ _, + bind-ind-arity (global (indt I)) Arity do-match Body, + + % typecheck (and infer univ constraints) + std.assert-ok! (typecheck Body Ty) "tag generates illtyped code", + + % save constant + Name is Prefix ^ "tag", + coq.env.add-const Name Body Ty ff C, + + % store in the DB the tag function, so that other Elpi commands can find it + CL = [tag-for I C], + std.forall CL (x\ coq.elpi.accumulate _ "tag.db" (clause _ _ x)), +]. + +% We build the match with dummy branches (you get the lambdas for the +% arguments of constructors, then Prop). Then we put the right number in place. +pred do-match i:term, i:list term, i:list term, o:term. +do-match _ Vars Tys (match X Rty BL1) :- do! [ + last Vars X, % the last variable is the one for the inductive type + last Tys XTy, + build-match X XTy do-rty do-dummy-branch (match X Rty BL), + fold-map BL {{ 1 }} do-branch BL1 _, +]. + +% builds the return clause of the match +pred do-rty i:term, i:list term,i:list term, o:term. +do-rty _ _ _ _. % we leave a hole + +% build each branch +pred do-dummy-branch i:term, i:term, i:list term, i:list term, o:term. +do-dummy-branch _ _ _ _ {{ Prop }}. % dummy + +% [do-branch InTerm Acc NewTem NewAcc] descends into a branch and puts Acc +% in place of the dummy +pred do-branch i:term, i:term, o:term, o:term. +do-branch {{ Prop }} X X Y :- coq.reduction.lazy.norm {{ lp:X + 1 }} Y. +do-branch (fun N T F) X (fun N T R) Y :- + @pi-decl N T x\ do-branch (F x) X (R x) Y. + +} \ No newline at end of file diff --git a/src/tag.v b/src/tag.v new file mode 100644 index 0000000..a08f96c --- /dev/null +++ b/src/tag.v @@ -0,0 +1,24 @@ +From elpi Require Import elpi. +From Coq Require Import PArith. +Open Scope positive_scope. + +Elpi Db tag.db lp:{{ + +% this is how one registers the tag function to an inductive and let other +% elpi commands use that piece of info +pred tag-for o:inductive, o:constant. + +}}. + +Elpi Command tag. +Elpi Accumulate File "src/tag.elpi". +Elpi Accumulate Db tag.db. +Elpi Accumulate lp:{{ + + main [str S] :- + std.assert! (coq.locate S (indt I)) "Not an inductive type", + Prefix is S ^ "_", + tag.main I Prefix _. + +}}. +Elpi Typecheck.