diff --git a/elpi/param-class.elpi b/elpi/param-class.elpi index f6aee8b..aee7b85 100644 --- a/elpi/param-class.elpi +++ b/elpi/param-class.elpi @@ -102,6 +102,15 @@ weakenings-to map2b [map3]. weakenings-to map3 [map4]. weakenings-to map4 []. +% lower/higher levels at distance 1 from a given level +pred all-weakenings-from i:map-class, o:list map-class. +all-weakenings-from map0 []. +all-weakenings-from map1 [map0]. +all-weakenings-from map2a [map1, map0]. +all-weakenings-from map2b [map1, map0]. +all-weakenings-from map3 [map2a, map2b, map1, map0]. +all-weakenings-from map4 [map3, map2a, map2b, map1, map0]. + % all possible parametricity classes that can be created by combinations of 2 lists of map classes pred product i:list map-class, i:list map-class, o:list param-class. product Ms Ns Classes :- @@ -176,10 +185,6 @@ dep-arrow map4 (pc map0 map4) (pc map4 map0). } % map-class -pred do-not-fail. -:before "term->gref:fail" -coq.term->gref _ _ :- do-not-fail, !, false. - namespace param-class { % extensions of functions over map classes to parametricity classes @@ -196,6 +201,15 @@ weakenings-to (pc M N) Classes :- map-class.weakenings-to N Ns, map-class.product Ms Ns Classes. +pred all-weakenings-from i:param-class, o:list param-class. +all-weakenings-from (pc M N) Classes :- + map-class.all-weakenings-from M Ms, + map-class.all-weakenings-from N Ns, + map-class.product Ms Ns StrictClasses, + map-class.product [M] Ns MClasses, + map-class.product Ms [N] NClasses, + std.flatten [StrictClasses, MClasses, NClasses] Classes. + pred negate i:param-class, o:param-class. negate (pc M N) (pc N M). @@ -229,6 +243,13 @@ dep-arrow (pc M N) ClassA ClassB :- union ClassAM {param-class.negate ClassAN} ClassA, union ClassBM {param-class.negate ClassBN} ClassB. +pred to-string i:param-class, o:string. +to-string (pc M N) String :- std.do! [ + map-class->string M MStr, + map-class->string N NStr, + String is MStr ^ NStr +]. + % generate a weakening function from a parametricity class to another, by forgetting fields 1 by 1 pred forget i:param-class, i:param-class, o:univ-instance -> term -> term -> term -> term. forget (pc M N) (pc M N) (_\ _\ _\ r\ r) :- !. @@ -247,6 +268,29 @@ forget (pc M N) (pc M' N') ForgetF :- {calc ("forget_" ^ {map-class->string M} ^ NStr ^ "_" ^ {map-class->string M1} ^ NStr)} Forget1, ForgetF = (ui\ a\ b\ r\ ForgetF' ui a b (app [pglobal Forget1 ui, a, b, r])). +% weaking of the out class of a gref. +% e.g. if GR has type `forall A B, R A B -> Param21 X Y` +% then `weaken-out (pc map1 map0) GR T` +% where `T` has type `forall A B, R A B -> Param10 X Y` +pred weaken-out i:param-class, i:gref, o:term. +weaken-out OutC GR WT :- std.do! [ + coq.env.global GR T, + coq.env.typeof GR Ty, + replace-out-ty OutC Ty WTy, + std.assert-ok! (coq.elaborate-skeleton T WTy WT) + "weaken-out: failed to weaken" +]. + +pred replace-out-ty i:param-class, i:term, o:term. +replace-out-ty OutC (prod N A B) (prod N A B') :- !, + pi x\ replace-out-ty OutC (B x) (B' x). +replace-out-ty OutC InT OutT :- std.do! [ + coq.safe-dest-app InT HD Ts, + trocq.db.gref->class OutGRClass OutC, + util.subst-gref HD OutGRClass HD', + coq.mk-app HD' Ts OutT + ]. + % succeed if the parametricity class contains a map class over 2b % this means that a translation of a sort at this class will require univalence, % and the translation of a dependent product will require funext diff --git a/elpi/util.elpi b/elpi/util.elpi index 2141a24..4f64f09 100644 --- a/elpi/util.elpi +++ b/elpi/util.elpi @@ -14,6 +14,10 @@ % utility predicates % ----------------------------------------------------------------------------- +pred do-not-fail. +:before "term->gref:fail" +coq.term->gref _ _ :- do-not-fail, !, false. + kind or type -> type -> type. type inl A -> or A B. type inr B -> or A B. @@ -79,4 +83,11 @@ delete A [A|Xs] Xs :- !. delete A [X|Xs] [X|Xs'] :- delete A Xs Xs'. delete _ [] []. +% subst-gref T GR' T' +% substitutes GR for GR' in T if T = (global GR) or (pglobal GR I) +pred subst-gref i:term, i:gref, o:term. +subst-gref (global _) GR' (global GR'). +subst-gref (pglobal _ I) GR' (pglobal GR' I). +subst-gref T _ _ :- coq.error T "is not a gref". + } % util diff --git a/examples/Vector_tuple.v b/examples/Vector_tuple.v index 2ed7ee4..f1aa5af 100644 --- a/examples/Vector_tuple.v +++ b/examples/Vector_tuple.v @@ -209,7 +209,6 @@ Defined. Module AppendConst. -Trocq Use Param00_nat. Trocq Use Param2a0_nat. Trocq Use Param_add. Trocq Use Param02b_tuple_vector. @@ -240,19 +239,14 @@ Axiom Param_head : forall Module HeadConst. Axiom (int : Type) (Zp : Type) (Rp42b : Param42b.Rel Zp int). -Definition Rp00 : Param00.Rel Zp int := Rp42b. -Definition Rp2a0 : Param2a0.Rel Zp int := Rp42b. -Definition Rp02b : Param02b.Rel Zp int := Rp42b. +Definition Rp2a2b : Param2a2b.Rel Zp int := Rp42b. Lemma head_const {n : nat} : forall (i : int), Vector.hd (Vector.const i (S n)) = i. Proof. destruct n; simpl; reflexivity. Qed. -Trocq Use Param00_nat. Trocq Use Param2a0_nat. Trocq Use SR. -Trocq Use Rp00. -Trocq Use Rp2a0. -Trocq Use Rp02b. +Trocq Use Rp2a2b. Trocq Use Param_head. Trocq Use Param_const. Trocq Use Param01_paths. @@ -464,13 +458,9 @@ Axiom setBitThenGetSame : forall {k : nat} (bv : bitvector k) (i : nat) (b : Bool), (i < k)%nat -> getBit_bv (setBit_bv bv i b) i = b. -Definition Param2a0_Bool : Param2a0.Rel Bool Bool := Param44_Bool. -Definition Param02b_Bool : Param02b.Rel Bool Bool := Param44_Bool. -Trocq Use Param00_nat. Trocq Use Param2a0_nat. -Trocq Use Param2a0_Bool. -Trocq Use Param02b_Bool. +Trocq Use Param44_Bool. Trocq Use Param2a0_bnat_bv. Trocq Use getBitR. Trocq Use setBitR. diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v index 84f34bf..5006788 100644 --- a/examples/int_to_Zp.v +++ b/examples/int_to_Zp.v @@ -76,12 +76,7 @@ Axiom Rzero : Rp zerop zero. Variable Radd : binop_param Rp Rp Rp addp add. Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp. -Trocq Use Rp00. -Trocq Use Rp01. -Trocq Use Rp10. -Trocq Use Rp02b. -Trocq Use Rp2a0. - +Trocq Use Rp2a2b. Trocq Use Param01_paths. Trocq Use Param10_paths. Trocq Use Radd. @@ -109,13 +104,6 @@ Module IntToZmodp. Definition Rp n x := modp n = x. Definition Rp42a@{i} : Param42a.Rel int@{i} Zmodp@{i} := SplitSurj.toParam (SplitSurj.Build_type modp reprp reprpK). -Definition Rp00 : Param00.Rel int Zmodp := Rp42a. -Definition Rp01 : Param01.Rel int Zmodp := Rp42a. -Definition Rp40 : Param40.Rel int Zmodp := Rp42a. -Definition Rp10 : Param10.Rel int Zmodp := Rp42a. -Definition Rp02a : Param02a.Rel int Zmodp := Rp42a. -Definition Rp2a0 : Param2a0.Rel int Zmodp := Rp42a. -Definition Rp2b0 : Param2b0.Rel int Zmodp := Rp42a. Axiom Rzero' : Rp zero zerop. Variable Radd' : binop_param Rp Rp Rp add addp. @@ -124,8 +112,7 @@ Variable Rmul' : binop_param Rp Rp Rp mul mulp. Trocq Use Rmul'. Trocq Use Rzero'. Trocq Use Param10_paths. -Trocq Use Rp2a0. -Trocq Use Rp2b0. +Trocq Use Rp42a. Definition eq_Zmodp (x y : Zmodp) := (x = y). (* Bug if we inline the previous def in the following axiom *) diff --git a/examples/peano_bin_nat.v b/examples/peano_bin_nat.v index ff1e1b9..b5a9ac9 100644 --- a/examples/peano_bin_nat.v +++ b/examples/peano_bin_nat.v @@ -141,10 +141,6 @@ Definition RN2a3 : Param2a3.Rel@{Set} N nat := SplitSurj.toParamSym@{Set} {| that do not need this field, so that it is not imported before forgetting, and the lower instances can be declared without the axiom *) -Definition RN02b : Param02b.Rel N nat := RN2a3. -Definition RN02a : Param02a.Rel N nat := RN2a3. -Definition RN2a0 : Param2a0.Rel N nat := RN2a3. - (* as 0 and Nsucc appear in the goal, we need to link them with nat constructors *) (* NB: as these are not type formers, only class (0,0) is required, so these proofs amount to what would be done in the context of raw parametricity *) @@ -153,9 +149,7 @@ Definition RN0 : RN N0 0. Proof. done. Qed. Definition RNS : forall m n, RN m n -> RN (Nsucc m) (S n). Proof. by move=> _ + <-; case=> //=. Qed. -Trocq Use RN02b. -Trocq Use RN02a. -Trocq Use RN2a0. +Trocq Use RN2a3. Trocq Use RN0. Trocq Use RNS. diff --git a/theories/Database.v b/theories/Database.v index 45aa564..4c414c7 100644 --- a/theories/Database.v +++ b/theories/Database.v @@ -64,5 +64,6 @@ Elpi Db trocq.db lp:{{ pred trocq.db.gref o:gref, o:param-class, o:list param-class, o:gref, o:gref. :name "default-gref" + trocq.db.gref _ _ _ _ _ :- do-not-fail, !, false. trocq.db.gref GR Out _ _ _ :- coq.error "cannot find" GR "at out class" Out. }}. diff --git a/theories/Hierarchy.v b/theories/Hierarchy.v index accc31c..900aeaa 100644 --- a/theories/Hierarchy.v +++ b/theories/Hierarchy.v @@ -17,6 +17,7 @@ Require Import HoTT_additions Database. From elpi Require Import elpi. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. +From Trocq.Elpi Extra Dependency "util.elpi" as util. Set Universe Polymorphism. Unset Universe Minimization ToSet. @@ -75,6 +76,7 @@ End Map4. (********************) Elpi Command genhierarchy. +Elpi Accumulate File util. Elpi Accumulate Db trocq.db. Elpi Accumulate File param_class. Elpi Accumulate lp:{{ diff --git a/theories/Param.v b/theories/Param.v index 30a3049..04778c0 100644 --- a/theories/Param.v +++ b/theories/Param.v @@ -35,8 +35,8 @@ Inductive map_class : Set := map0 | map1 | map2a | map2b | map3 | map4. Elpi Command genpparam. Elpi Accumulate File util. -Elpi Accumulate File param_class. Elpi Accumulate Db trocq.db. +Elpi Accumulate File param_class. Definition PType@{i} (m n : map_class) (* : Type@{i+1} *) := Type@{i}. Definition weaken@{i} (m n m' n' : map_class) {A : Type@{i}} (a : A) : A := a. @@ -55,8 +55,8 @@ Elpi Query lp:{{ Elpi Command genpparamtype. Elpi Accumulate File util. -Elpi Accumulate File param_class. Elpi Accumulate Db trocq.db. +Elpi Accumulate File param_class. Elpi Accumulate lp:{{ pred generate-branch i:univ-instance, i:param-class, i:param-class, o:term. generate-branch UI2 Class RClass (pglobal ParamType UI2) :- @@ -141,9 +141,9 @@ Elpi Query lp:{{ }}. Elpi Tactic trocq. +Elpi Accumulate File util. Elpi Accumulate Db trocq.db. Elpi Accumulate File annot. -Elpi Accumulate File util. Elpi Accumulate File param_class. Elpi Accumulate File simple_graph. Elpi Accumulate File constraint_graph. diff --git a/theories/Param_Type.v b/theories/Param_Type.v index 104eaff..3297fc7 100644 --- a/theories/Param_Type.v +++ b/theories/Param_Type.v @@ -15,6 +15,7 @@ From elpi Require Import elpi. From Coq Require Import ssreflect. From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy Database. +From Trocq.Elpi Extra Dependency "util.elpi" as util. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. Set Universe Polymorphism. @@ -28,6 +29,8 @@ Local Open Scope param_scope. + symmetry MapM_Type_symNP *) Elpi Command genmaptype. +Elpi Accumulate File util. +Elpi Accumulate Db trocq.db. Elpi Accumulate File param_class. Elpi Accumulate lp:{{ pred generate-fields @@ -166,6 +169,7 @@ Defined. (for M or N in [2b, 3, 4] PQ is always 44) *) Elpi Command genparamtype. +Elpi Accumulate File util. Elpi Accumulate Db trocq.db. Elpi Accumulate File param_class. Elpi Accumulate lp:{{ diff --git a/theories/Param_arrow.v b/theories/Param_arrow.v index c52a334..c1f3cdb 100644 --- a/theories/Param_arrow.v +++ b/theories/Param_arrow.v @@ -15,6 +15,7 @@ From elpi Require Import elpi. From Coq Require Import ssreflect. From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy Database. +From Trocq.Elpi Extra Dependency "util.elpi" as util. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. Set Universe Polymorphism. @@ -23,6 +24,7 @@ Unset Universe Minimization ToSet. Local Open Scope param_scope. Elpi Command genparamarrow. +Elpi Accumulate File util. Elpi Accumulate Db trocq.db. Elpi Accumulate File param_class. diff --git a/theories/Param_forall.v b/theories/Param_forall.v index 5c82ab8..e77953a 100644 --- a/theories/Param_forall.v +++ b/theories/Param_forall.v @@ -15,6 +15,7 @@ From elpi Require Import elpi. From Coq Require Import ssreflect. From HoTT Require Import HoTT. Require Import HoTT_additions Hierarchy Database. +From Trocq.Elpi Extra Dependency "util.elpi" as util. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. Set Universe Polymorphism. @@ -23,6 +24,7 @@ Unset Universe Minimization ToSet. Local Open Scope param_scope. Elpi Command genparamforall. +Elpi Accumulate File util. Elpi Accumulate Db trocq.db. Elpi Accumulate File param_class. diff --git a/theories/Param_option.v b/theories/Param_option.v index ec39169..3b099d6 100644 --- a/theories/Param_option.v +++ b/theories/Param_option.v @@ -83,18 +83,18 @@ Definition option_map_in_R : | Some a' => fun e => someR A A' AR a a' (map_in_R AR a a' (some_inj1 A' (map AR a) a' e)) - | none => + | None => fun e => exfalso_option_some_none (optionR A A' AR (Some a) (None)) A' (map AR a) e end - | none => + | None => match oa' with | Some a' => fun e => exfalso_option_none_some (optionR A A' AR (None) (Some a')) A' a' e - | none => fun e => noneR A A' AR + | None => fun e => noneR A A' AR end end. diff --git a/theories/Vernac.v b/theories/Vernac.v index 57a733e..7a62c3b 100644 --- a/theories/Vernac.v +++ b/theories/Vernac.v @@ -27,8 +27,8 @@ From Trocq.Elpi Extra Dependency "util.elpi" as util. From Trocq.Elpi Extra Dependency "param-class.elpi" as param_class. Elpi Command Trocq. -Elpi Accumulate Db trocq.db. Elpi Accumulate File util. +Elpi Accumulate Db trocq.db. Elpi Accumulate File annot. Elpi Accumulate File param_class. Elpi Accumulate File simple_graph. @@ -86,7 +86,22 @@ Elpi Accumulate lp:{{ coq.say "accumultating" GR "@" Class "(" CList ") ~" GR' ":." GRR, coq.elpi.accumulate _ "trocq.db" (clause _ (before "default-gref") - (trocq.db.gref GR Class CList GR' GRR)) + (trocq.db.gref GR Class CList GR' GRR)), + std.forall {param-class.all-weakenings-from Class} subclass\ + sigma WTRR BaseName Suffix WName WCRR \ + if (do-not-fail => trocq.db.gref GR subclass _ _ _) true (std.do! [ + param-class.weaken-out subclass GRR WTRR, + coq.gref->id GRR BaseName, + param-class.to-string subclass Suffix, + WName is BaseName ^ "_weakened_to_" ^ Suffix, + @udecl! [] tt [] tt => + coq.env.add-const WName WTRR _ @transparent! WCRR, + coq.elpi.accumulate _ "trocq.db" + (clause _ (before "default-gref") + (trocq.db.gref GR subclass CList GR' (const WCRR))), + coq.say "accumultating" GR "@" subclass "(" CList ") ~" GR' + ":." (const WCRR), + ]) ]. % coq.elpi.accumulate _ "trocq.db" % (clause _ (before "default-gref")