From 1ba8c661664c7304bd33ca97697313ec79f583c7 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Tue, 4 Jun 2024 16:35:41 +0200 Subject: [PATCH] Adapt to coq/coq#18973. --- common/theories/Environment.v | 19 ++++--- common/theories/Primitive.v | 1 + erasure/theories/EArities.v | 12 ++++- erasure/theories/EAstUtils.v | 3 +- erasure/theories/EDeps.v | 1 + erasure/theories/EInduction.v | 3 +- erasure/theories/EPretty.v | 1 + erasure/theories/EPrimitive.v | 54 ++++++++++++++----- erasure/theories/EReflect.v | 1 + erasure/theories/ERemoveParams.v | 1 + erasure/theories/EWcbvEval.v | 21 +++++--- .../EWcbvEvalCstrsAsBlocksFixLambdaInd.v | 1 + erasure/theories/EWcbvEvalCstrsAsBlocksInd.v | 1 + erasure/theories/EWcbvEvalEtaInd.v | 1 + erasure/theories/EWellformed.v | 3 ++ erasure/theories/ErasureCorrectness.v | 4 +- erasure/theories/ErasureFunction.v | 2 + erasure/theories/Extract.v | 3 ++ erasure/theories/Typed/Certifying.v | 1 + erasure/theories/Typed/WcbvEvalAux.v | 2 +- pcuic/theories/Bidirectional/BDFromPCUIC.v | 2 +- pcuic/theories/Bidirectional/BDUnique.v | 1 + pcuic/theories/PCUICAlpha.v | 2 +- pcuic/theories/PCUICAst.v | 1 + pcuic/theories/PCUICClassification.v | 4 +- pcuic/theories/PCUICConversion.v | 20 ++++--- pcuic/theories/PCUICCumulProp.v | 12 ++--- pcuic/theories/PCUICEtaExpand.v | 1 + pcuic/theories/PCUICNormal.v | 2 +- .../PCUICParallelReductionConfluence.v | 1 + pcuic/theories/PCUICPrincipality.v | 2 +- pcuic/theories/PCUICProgress.v | 3 +- pcuic/theories/PCUICTyping.v | 3 ++ pcuic/theories/PCUICValidity.v | 2 +- pcuic/theories/PCUICWcbvEval.v | 3 ++ pcuic/theories/Syntax/PCUICPosition.v | 6 +-- pcuic/theories/Syntax/PCUICReflect.v | 1 + pcuic/theories/Typing/PCUICWeakeningEnvTyp.v | 3 +- pcuic/theories/utils/PCUICPretty.v | 1 + pcuic/theories/utils/PCUICPrimitive.v | 52 +++++++++++++----- pcuic/theories/utils/PCUICSize.v | 3 +- quotation/theories/CommonUtils.v | 1 + .../ToPCUIC/PCUIC/utils/PCUICPrimitive.v | 2 + quotation/theories/ToTemplate/Init.v | 2 + quotation/theories/ToTemplate/Template/Ast.v | 2 + safechecker/theories/PCUICEqualityDec.v | 2 +- safechecker/theories/PCUICSafeConversion.v | 41 ++++++++++++++ safechecker/theories/PCUICTypeChecker.v | 18 +++---- template-coq/_PluginProject | 4 ++ template-coq/_PluginProject.in | 4 ++ .../gen-src/metacoq_template_plugin.mlpack | 2 + template-coq/src/ast_denoter.ml | 6 ++- template-coq/src/ast_quoter.ml | 8 ++- template-coq/src/constr_denoter.ml | 11 +++- template-coq/src/constr_quoter.ml | 8 ++- template-coq/src/constr_reification.ml | 1 + template-coq/src/denoter.ml | 4 +- template-coq/src/quoter.ml | 5 ++ template-coq/src/reification.ml | 1 + template-coq/src/tm_util.ml | 3 +- template-coq/theories/Ast.v | 5 +- template-coq/theories/AstUtils.v | 3 +- template-coq/theories/Checker.v | 2 +- template-coq/theories/EtaExpand.v | 6 ++- template-coq/theories/Extraction.v | 2 +- template-coq/theories/Induction.v | 2 + template-coq/theories/Pretty.v | 1 + template-coq/theories/ReflectAst.v | 10 ++++ template-coq/theories/TermEquality.v | 1 + template-coq/theories/Typing.v | 17 +++++- template-coq/theories/WfAst.v | 6 ++- template-pcuic/theories/PCUICToTemplate.v | 1 + .../theories/PCUICToTemplateCorrectness.v | 7 ++- .../theories/TemplateMonadToPCUIC.v | 1 + template-pcuic/theories/TemplateToPCUIC.v | 1 + .../theories/TemplateToPCUICCorrectness.v | 11 ++++ .../theories/TemplateToPCUICExpanded.v | 1 + utils/theories/Show.v | 15 +++++- 78 files changed, 373 insertions(+), 104 deletions(-) diff --git a/common/theories/Environment.v b/common/theories/Environment.v index 6ae92df47..9d3ca8ece 100644 --- a/common/theories/Environment.v +++ b/common/theories/Environment.v @@ -42,25 +42,28 @@ Module Retroknowledge. Record t := mk_retroknowledge { retro_int63 : option kername; retro_float64 : option kername; + retro_string : option kername; retro_array : option kername; }. - Definition empty := {| retro_int63 := None; retro_float64 := None; retro_array := None |}. + Definition empty := {| retro_int63 := None; retro_float64 := None; retro_string := None; retro_array := None |}. Definition extends (x y : t) := option_extends x.(retro_int63) y.(retro_int63) /\ option_extends x.(retro_float64) y.(retro_float64) /\ + option_extends x.(retro_string) y.(retro_string) /\ option_extends x.(retro_array) y.(retro_array). Existing Class extends. Definition extendsb (x y : t) := option_extendsb x.(retro_int63) y.(retro_int63) && option_extendsb x.(retro_float64) y.(retro_float64) && - option_extendsb x.(retro_array) y.(retro_array). + option_extendsb x.(retro_string) y.(retro_string) && + option_extendsb x.(retro_array) y.(retro_array). Lemma extendsT x y : reflect (extends x y) (extendsb x y). Proof. - rewrite /extends/extendsb; do 3 case: option_extendsT; cbn; constructor; intuition auto. + rewrite /extends/extendsb; do 4 case: option_extendsT; cbn; constructor; intuition auto. Qed. Lemma extends_spec x y : extendsb x y <-> extends x y. @@ -76,22 +79,24 @@ Module Retroknowledge. #[global] Instance extends_trans : RelationClasses.Transitive Retroknowledge.extends. Proof. - intros x y z [? []] [? []]; repeat split; cbn; now etransitivity; tea. + intros x y z [? [? []]] [? [? []]]; repeat split; cbn; now etransitivity; tea. Qed. #[export,program] Instance reflect_t : ReflectEq t := { eqb x y := (x.(retro_int63) == y.(retro_int63)) && (x.(retro_float64) == y.(retro_float64)) && + (x.(retro_string) == y.(retro_string)) && (x.(retro_array) == y.(retro_array)) }. Next Obligation. - do 3 case: eqb_spec; destruct x, y; cbn; intros; subst; constructor; congruence. + do 4 case: eqb_spec; destruct x, y; cbn; intros; subst; constructor; congruence. Qed. (** This operation is asymmetric; it perfers the first argument when the arguments are incompatible, but otherwise takes the join *) Definition merge (r1 r2 : t) : t := {| retro_int63 := match r1.(retro_int63) with Some v => Some v | None => r2.(retro_int63) end ; retro_float64 := match r1.(retro_float64) with Some v => Some v | None => r2.(retro_float64) end + ; retro_string := match r1.(retro_string) with Some v => Some v | None => r2.(retro_string) end ; retro_array := match r1.(retro_array) with Some v => Some v | None => r2.(retro_array) end |}. @@ -112,6 +117,7 @@ Module Retroknowledge. Definition compatible (x y : t) : bool := match x.(retro_int63), y.(retro_int63) with Some x, Some y => x == y | _, _ => true end && match x.(retro_float64), y.(retro_float64) with Some x, Some y => x == y | _, _ => true end + && match x.(retro_string), y.(retro_string) with Some x, Some y => x == y | _, _ => true end && match x.(retro_array), y.(retro_array) with Some x, Some y => x == y | _, _ => true end. Lemma extends_r_merge r1 r2 @@ -846,6 +852,7 @@ Module Environment (T : Term). match p with | primInt => Σ.(retroknowledge).(Retroknowledge.retro_int63) | primFloat => Σ.(retroknowledge).(Retroknowledge.retro_float64) + | primString => Σ.(retroknowledge).(Retroknowledge.retro_string) | primArray => Σ.(retroknowledge).(Retroknowledge.retro_array) end. @@ -857,7 +864,7 @@ Module Environment (T : Term). Definition primitive_invariants (p : prim_tag) (cdecl : constant_body) := match p with - | primInt | primFloat => + | primInt | primFloat | primString => [/\ cdecl.(cst_type) = tSort Sort.type0, cdecl.(cst_body) = None & cdecl.(cst_universes) = Monomorphic_ctx] | primArray => diff --git a/common/theories/Primitive.v b/common/theories/Primitive.v index f8283f6fc..278f9d056 100644 --- a/common/theories/Primitive.v +++ b/common/theories/Primitive.v @@ -7,5 +7,6 @@ Local Open Scope bs. Variant prim_tag := | primInt | primFloat + | primString | primArray. Derive NoConfusion EqDec for prim_tag. diff --git a/erasure/theories/EArities.v b/erasure/theories/EArities.v index f80d881f6..052269c0e 100644 --- a/erasure/theories/EArities.v +++ b/erasure/theories/EArities.v @@ -1010,13 +1010,14 @@ Proof. destruct p as [? []]; simp prim_type. - eexists [], []. reflexivity. - eexists [], []; reflexivity. + - eexists [], []; reflexivity. - eexists [_], [_]; reflexivity. Qed. Lemma primitive_invariants_axiom t decl : primitive_invariants t decl -> cst_body decl = None. Proof. destruct t; cbn => //. - 1-2:now intros [? []]. + 1-3:now intros [? []]. now intros []. Qed. @@ -1052,6 +1053,13 @@ Proof. rewrite hd in hs'. cbn in hs'. eapply ws_cumul_pb_Sort_inv in hs'. red in hs'. destruct s => //. + * destruct p0 as [hd hb hu]. + eapply inversion_Const in hs as [decl' [wf [decl'' [cu hs']]]]; eauto. + unshelve eapply declared_constant_to_gen in d, decl''. 3,6:eapply wfΣ. + eapply declared_constant_inj in d; tea. subst decl'. + rewrite hd in hs'. cbn in hs'. + eapply ws_cumul_pb_Sort_inv in hs'. red in hs'. + destruct s => //. * destruct p0 as [hd hb hu]. eapply inversion_App in hs as [na [A [B [hp [harg hres]]]]]; eauto. eapply inversion_Const in hp as [decl' [wf [decl'' [cu hs']]]]; eauto. @@ -1064,4 +1072,4 @@ Proof. pose proof (ws_cumul_pb_trans _ _ _ w1 hres) as X0. eapply ws_cumul_pb_Sort_inv in X0. destruct s => //. -Qed. \ No newline at end of file +Qed. diff --git a/erasure/theories/EAstUtils.v b/erasure/theories/EAstUtils.v index de7c2655c..2058db50c 100644 --- a/erasure/theories/EAstUtils.v +++ b/erasure/theories/EAstUtils.v @@ -386,6 +386,7 @@ Section PrimDeps. Equations prim_global_deps (p : prim_val term) : KernameSet.t := | (primInt; primIntModel i) => KernameSet.empty | (primFloat; primFloatModel f) => KernameSet.empty + | (primString; primStringModel s) => KernameSet.empty | (primArray; primArrayModel a) => List.fold_left (fun acc x => KernameSet.union (deps x) acc) a.(array_value) (deps a.(array_default)). @@ -414,4 +415,4 @@ Fixpoint term_global_deps (t : term) := | tLazy t => term_global_deps t | tForce t => term_global_deps t | _ => KernameSet.empty - end. \ No newline at end of file + end. diff --git a/erasure/theories/EDeps.v b/erasure/theories/EDeps.v index b1180b5cc..9f6c273d8 100644 --- a/erasure/theories/EDeps.v +++ b/erasure/theories/EDeps.v @@ -455,6 +455,7 @@ Proof. constructor; [now apply f|now apply f']. - eapply Hprim; tea; constructor. - eapply Hprim; tea; constructor. + - eapply Hprim; tea; constructor. - eapply Hprim; tea; constructor. intuition auto; solve_all. split. auto. destruct a as [d v]. cbn in *. diff --git a/erasure/theories/EInduction.v b/erasure/theories/EInduction.v index 53d4d9bc0..a399afa00 100644 --- a/erasure/theories/EInduction.v +++ b/erasure/theories/EInduction.v @@ -101,6 +101,7 @@ Definition prim_size (f : term -> nat) (p : prim_val term) : nat := match p.π2 with | primIntModel _ => 0 | primFloatModel _ => 0 + | primStringModel _ => 0 | primArrayModel a => f a.(array_default) + list_size f a.(array_value) end. @@ -404,4 +405,4 @@ Proof. | _ => 1 end. -End TermSpineView.*) \ No newline at end of file +End TermSpineView.*) diff --git a/erasure/theories/EPretty.v b/erasure/theories/EPretty.v index 9c99f2e64..c5016220b 100644 --- a/erasure/theories/EPretty.v +++ b/erasure/theories/EPretty.v @@ -88,6 +88,7 @@ Module PrintTermTree. match p.π2 return Tree.t with | primIntModel f => "(int: " ^ show f ^ ")" | primFloatModel f => "(float: " ^ show f ^ ")" + | primStringModel f => "(string: " ^ show f ^ ")" | primArrayModel a => "(array:" ^ soft a.(array_default) ^ " , " ^ string_of_list soft a.(array_value) ^ ")" end. diff --git a/erasure/theories/EPrimitive.v b/erasure/theories/EPrimitive.v index 769949f18..658f1293f 100644 --- a/erasure/theories/EPrimitive.v +++ b/erasure/theories/EPrimitive.v @@ -30,6 +30,7 @@ Section PrimModel. Inductive prim_model : prim_tag -> Type@{i} := | primIntModel (i : PrimInt63.int) : prim_model primInt | primFloatModel (f : PrimFloat.float) : prim_model primFloat + | primStringModel (s : PrimString.string) : prim_model primString | primArrayModel (a : array_model) : prim_model primArray. Derive Signature NoConfusion NoConfusionHom for prim_model. @@ -38,6 +39,7 @@ Section PrimModel. match p with | primInt => PrimInt63.int | primFloat => PrimFloat.float + | primString => PrimString.string | primArray => array_model end. @@ -47,12 +49,14 @@ Section PrimModel. Definition prim_int i : prim_val := (primInt; primIntModel i). Definition prim_float f : prim_val := (primFloat; primFloatModel f). + Definition prim_string s : prim_val := (primString; primStringModel s). Definition prim_array a : prim_val := (primArray; primArrayModel a). Definition prim_model_val (p : prim_val) : prim_model_of (prim_val_tag p) := match prim_val_model p in prim_model t return prim_model_of t with | primIntModel i => i | primFloatModel f => f + | primStringModel s => s | primArrayModel a => a end. @@ -85,9 +89,23 @@ Section PrimModel. all:constructor; congruence. Qed. + #[program,global] + Instance reflect_eq_pstring : ReflectEq PrimString.string := + { eqb := (fun s1 s2 => match PrimString.compare s1 s2 with Eq => true | _ => false end) }. + Next Obligation. discriminate. Qed. + Next Obligation. discriminate. Qed. + Next Obligation. + intros s1 s2. simpl. + destruct (PrimString.compare s1 s2) eqn:Hcmp; constructor. + - by apply PString.string_eq_spec in Hcmp. + - intros Heq%PString.string_eq_spec. rewrite Heq in Hcmp. inversion Hcmp. + - intros Heq%PString.string_eq_spec. rewrite Heq in Hcmp. inversion Hcmp. + Qed. + Equations eqb_prim_model {req : term -> term -> bool} {t : prim_tag} (x y : prim_model t) : bool := | primIntModel x, primIntModel y := ReflectEq.eqb x y | primFloatModel x, primFloatModel y := ReflectEq.eqb x y + | primStringModel x, primStringModel y := ReflectEq.eqb x y | primArrayModel x, primArrayModel y := eqb_array (eqt:=req) x y. #[global, program] @@ -97,6 +115,7 @@ Section PrimModel. intros. depelim x; depelim y; simp eqb_prim_model. case: ReflectEq.eqb_spec; constructor; subst; auto. congruence. case: ReflectEq.eqb_spec; constructor; subst; auto. congruence. + case: ReflectEq.eqb_spec; constructor; subst; auto. congruence. change (eqb_array a a0) with (eqb a a0). case: ReflectEq.eqb_spec; constructor; subst; auto. congruence. Qed. @@ -107,6 +126,7 @@ Section PrimModel. Equations eqb_prim_val {req : term -> term -> bool} (x y : prim_val) : bool := | (primInt; i), (primInt; i') := eqb_prim_model (req := req) i i' | (primFloat; f), (primFloat; f') := eqb_prim_model (req := req) f f' + | (primString; s), (primString; s') := eqb_prim_model (req := req) s s' | (primArray; a), (primArray; a') := eqb_prim_model (req := req) a a' | x, y := false. @@ -115,22 +135,19 @@ Section PrimModel. {| ReflectEq.eqb := eqb_prim_val (req := eqb) |}. Next Obligation. intros. funelim (eqb_prim_val x y); simp eqb_prim_val. - change (eqb_prim_model i i') with (eqb i i'). - case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H. cbn in n. auto. - constructor. intros H; noconf H; auto. - constructor. intros H; noconf H; auto. - constructor. intros H; noconf H; auto. - change (eqb_prim_model f f') with (eqb f f'). - case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto. - constructor. intros H; noconf H; auto. - constructor. intros H; noconf H; auto. - constructor. intros H; noconf H; auto. - change (eqb_prim_model a a') with (eqb a a'). - case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto. + all: try by constructor; intros H; noconf H; auto. + - change (eqb_prim_model i i') with (eqb i i'). + case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H. cbn in n. auto. + - change (eqb_prim_model f f') with (eqb f f'). + case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto. + - change (eqb_prim_model s s') with (eqb s s'). + case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto. + - change (eqb_prim_model a a') with (eqb a a'). + case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto. Qed. #[global] - Instance prim_tag_model_eqdec {req : ReflectEq term} : EqDec (prim_val) := _. + Instance prim_tag_model_eqdec {req : ReflectEq term} : EqDec (prim_val) := _. (** Printing *) @@ -138,6 +155,7 @@ Section PrimModel. match p.π2 return string with | primIntModel f => "(int: " ^ string_of_prim_int f ^ ")" | primFloatModel f => "(float: " ^ string_of_float f ^ ")" + | primStringModel s => "(string: " ^ string_of_pstring s ^ ")" | primArrayModel a => "(array:" ^ soft a.(array_default) ^ " , " ^ string_of_list soft a.(array_value) ^ ")" end. @@ -148,12 +166,14 @@ Section PrimModel. match p.π2 return bool with | primIntModel f => true | primFloatModel f => true + | primStringModel f => true | primArrayModel a => test_array_model f a end. Inductive primProp P : prim_val -> Type := | primPropInt i : primProp P (primInt; primIntModel i) | primPropFloat f : primProp P (primFloat; primFloatModel f) + | primPropString s : primProp P (primString; primStringModel s) | primPropArray a : P a.(array_default) × All P a.(array_value) -> primProp P (primArray; primArrayModel a). Derive Signature NoConfusion for primProp. @@ -162,6 +182,7 @@ Section PrimModel. match p.π2 return A with | primIntModel f => acc | primFloatModel f => acc + | primStringModel f => acc | primArrayModel a => fold_left f a.(array_value) (f acc a.(array_default)) end. End PrimModel. @@ -181,6 +202,7 @@ Section PrimOps. match p.π2 return prim_val term' with | primIntModel f => (primInt; primIntModel f) | primFloatModel f => (primFloat; primFloatModel f) + | primStringModel f => (primString; primStringModel f) | primArrayModel a => (primArray; primArrayModel (map_array_model f a)) end. End PrimOps. @@ -343,6 +365,7 @@ Section PrimIn. Equations InPrim (x : term) (p : prim_val term) : Prop := | x | (primInt; primIntModel i) := False | x | (primFloat; primFloatModel _) := False + | x | (primString; primStringModel _) := False | x | (primArray; primArrayModel a) := x = a.(array_default) \/ In x a.(array_value). @@ -360,6 +383,7 @@ Section PrimIn. Equations test_primIn (p : prim_val term) (f : forall x : term, InPrim x p -> bool) : bool := | (primInt; primIntModel i) | _ := true | (primFloat; primFloatModel _) | _ := true + | (primString; primStringModel _) | _ := true | (primArray; primArrayModel a) | f := f a.(array_default) (or_introl eq_refl) && forallb_InP a.(array_value) (fun x H => f x (or_intror H)). @@ -373,6 +397,7 @@ Section PrimIn. Equations map_primIn (p : prim_val term) (f : forall x : term, InPrim x p -> term) : prim_val term := | (primInt; primIntModel i) | _ := (primInt; primIntModel i) | (primFloat; primFloatModel f) | _ := (primFloat; primFloatModel f) + | (primString; primStringModel f) | _ := (primString; primStringModel f) | (primArray; primArrayModel a) | f := (primArray; primArrayModel {| array_default := f a.(array_default) (or_introl eq_refl); @@ -455,6 +480,7 @@ Section onPrims. Inductive onPrims {term term' : Set} (R : term -> term' -> Set) : prim_val term -> prim_val term' -> Type := | onPrimsInt i : onPrims R (primInt; primIntModel i) (primInt; primIntModel i) | onPrimsFloat f : onPrims R (primFloat; primFloatModel f) (primFloat; primFloatModel f) + | onPrimsString s : onPrims R (primString; primStringModel s) (primString; primStringModel s) | onPrimsArray v def v' def' : R def def' -> All2_Set R v v' -> @@ -466,6 +492,7 @@ Section onPrims. Variant onPrims_dep {term term' : Set} (R : term -> term' -> Set) (P : forall x y, R x y -> Type) : forall x y, onPrims R x y -> Type := | onPrimsIntDep i : onPrims_dep R P (prim_int i) (prim_int i) (onPrimsInt R i) | onPrimsFloatDep f : onPrims_dep R P (prim_float f) (prim_float f) (onPrimsFloat R f) + | onPrimsStringDep s : onPrims_dep R P (prim_string s) (prim_string s) (onPrimsString R s) | onPrimsArrayDep v def v' def' (ed : R def def') (ev : All2_Set R v v') : @@ -485,6 +512,7 @@ Section onPrims. Equations map_onPrims {p : prim_val term} {p' : prim_val term'} (ev : onPrims R p p') : onPrims_dep R P p p' ev := | @onPrimsInt _ _ _ _ := onPrimsIntDep _ _ i; | @onPrimsFloat _ _ _ _ := onPrimsFloatDep _ _ f; + | @onPrimsString _ _ _ _ := onPrimsStringDep _ _ s; | @onPrimsArray v def v' def' ed ev := onPrimsArrayDep _ _ v def v' def' ed ev (F _ _ ed) (map_All2_dep _ F ev). End map_onPrims. diff --git a/erasure/theories/EReflect.v b/erasure/theories/EReflect.v index 70bb89dc6..b784392b6 100644 --- a/erasure/theories/EReflect.v +++ b/erasure/theories/EReflect.v @@ -115,6 +115,7 @@ Proof. - destruct prim as [? []]; destruct p as [? []]; cbn ; nodec. + destruct (eq_dec i i0); nodec; subst; eauto. + destruct (eq_dec f f0); nodec; subst; eauto. + + destruct (eq_dec s s0); nodec; subst; eauto. + destruct a as [? ?], a0 as [? ?]; cbn. depelim X. destruct p as [hd hv]. cbn in *. destruct (hd array_default); nodec; subst; eauto. diff --git a/erasure/theories/ERemoveParams.v b/erasure/theories/ERemoveParams.v index 8a7344d94..2810058df 100644 --- a/erasure/theories/ERemoveParams.v +++ b/erasure/theories/ERemoveParams.v @@ -569,6 +569,7 @@ Module Fast. | None => mkApps (EAst.tConstruct kn c block_args) app } | app, tPrim (primInt; primIntModel i) => mkApps (tPrim (primInt; primIntModel i)) app | app, tPrim (primFloat; primFloatModel f) => mkApps (tPrim (primFloat; primFloatModel f)) app + | app, tPrim (primString; primStringModel f) => mkApps (tPrim (primString; primStringModel f)) app | app, tPrim (primArray; primArrayModel a) => mkApps (tPrim (primArray; primArrayModel {| array_default := strip [] a.(array_default); array_value := strip_args a.(array_value) |})) app | app, tLazy t => mkApps (tLazy (strip [] t)) app diff --git a/erasure/theories/EWcbvEval.v b/erasure/theories/EWcbvEval.v index 3080d7fde..36058cee8 100644 --- a/erasure/theories/EWcbvEval.v +++ b/erasure/theories/EWcbvEval.v @@ -77,6 +77,7 @@ Section Wcbv. Variant eval_primitive {term term' : Set} (eval : term -> term' -> Set) : prim_val term -> prim_val term' -> Set := | evalPrimInt i : eval_primitive eval (prim_int i) (prim_int i) | evalPrimFloat f : eval_primitive eval (prim_float f) (prim_float f) + | evalPrimString s : eval_primitive eval (prim_string s) (prim_string s) | evalPrimArray v def v' def' (ev : All2_Set eval v v') (ed : eval def def') : @@ -88,6 +89,7 @@ Section Wcbv. Variant eval_primitive_ind {term term' : Set} (eval : term -> term' -> Set) (P : forall x y, eval x y -> Type) : forall x y, eval_primitive eval x y -> Type := | evalPrimIntDep i : eval_primitive_ind eval P (prim_int i) (prim_int i) (evalPrimInt eval i) | evalPrimFloatDep f : eval_primitive_ind eval P (prim_float f) (prim_float f) (evalPrimFloat eval f) + | evalPrimStringDep s : eval_primitive_ind eval P (prim_string s) (prim_string s) (evalPrimString eval s) | evalPrimArrayDep v def v' def' (ev : All2_Set eval v v') (ed : eval def def') : @@ -106,6 +108,7 @@ Section Wcbv. Equations map_eval_primitive {p : prim_val term} {p' : prim_val term'} (ev : eval_primitive eval p p') : eval_primitive_ind eval P p p' ev := | @evalPrimInt _ _ _ _ := evalPrimIntDep _ _ i; | @evalPrimFloat _ _ _ _ := evalPrimFloatDep _ _ f; + | @evalPrimString _ _ _ _ := evalPrimStringDep _ _ s; | @evalPrimArray v def v' def' ev ed := evalPrimArrayDep _ _ v def v' def' ev ed (map_All2_dep _ F ev) (F _ _ ed). End map_eval_prim. @@ -313,6 +316,7 @@ Section Wcbv. Variant primitive_value (value : term -> Type) : prim_val term -> Type := | primIntValue i : primitive_value value (prim_int i) | primFloatValue f : primitive_value value (prim_float f) + | primStringValue s : primitive_value value (prim_string s) | primArrayValue a : All value a.(array_value) -> value a.(array_default) -> @@ -343,8 +347,9 @@ Definition eval_primitive_depth {eval : term -> term -> Set} (size : forall x y, match e with | evalPrimInt _ => 0 | evalPrimFloat _ => 0 + | evalPrimString _ => 0 | evalPrimArray v d v' d' aev ed => - all2_size _ size aev + size _ _ ed + all2_size _ size aev + size _ _ ed end. Fixpoint eval_depth {wfl : WcbvFlags} {Σ : EAst.global_declarations} {t1 t2 : EAst.term} (ev : eval Σ t1 t2) { struct ev } : nat. @@ -352,12 +357,12 @@ Proof. rename eval_depth into aux. destruct ev. all:try match goal with - | [ H : eval _ _ _, H' : eval _ _ _, H'' : eval _ _ _ |- _ ] => - apply aux in H; apply aux in H'; apply aux in H''; exact (S (Nat.max H (Nat.max H' H''))) - | [ H : eval _ _ _, H' : eval _ _ _ |- _ ] => - apply aux in H; apply aux in H'; exact (S (Nat.max H H')) - | [ H : eval _ _ _ |- _ ] => apply aux in H; exact (S H) - end. + | [ H : eval _ _ _, H' : eval _ _ _, H'' : eval _ _ _ |- _ ] => + apply aux in H; apply aux in H'; apply aux in H''; exact (S (Nat.max H (Nat.max H' H''))) + | [ H : eval _ _ _, H' : eval _ _ _ |- _ ] => + apply aux in H; apply aux in H'; exact (S (Nat.max H H')) + | [ H : eval _ _ _ |- _ ] => apply aux in H; exact (S H) + end. exact (S (all2_size _ (fun x y ev => aux wfl Σ x y ev) a)). exact (S (eval_primitive_depth (aux wfl Σ) e)). exact 1. @@ -1833,7 +1838,7 @@ Proof. { induction a; cbn; try lia. destruct iha. destruct s. cbn. specialize (IHa a0). lia. } - unshelve eexists. eapply eval_app_cong; eauto. eapply IHHe1. eapply IHHe2. cbn. destruct IHHe1, IHHe2. lia. - - depelim X. 1-2:unshelve eexists; cbn; repeat constructor. + - depelim X. 1-3:unshelve eexists; cbn; repeat constructor. destruct s as [hev evd]. unshelve eexists. do 2 econstructor. clear -a. induction ev; constructor. apply a. apply IHev, a. tea. diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v index 5e4479327..891283ac8 100644 --- a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v +++ b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v @@ -551,6 +551,7 @@ Proof. 1,3:(apply and_assum; [ih|hp' P'Q]). intros. apply and_assum; [ih|hp' P'Q]. - unshelve eapply Qprim; tea. depelim e. + * constructor. * constructor. * constructor. * eapply Qpres in qt. depelim qt. now cbn in i. constructor; eauto. diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v index 111033e35..c4b52691a 100644 --- a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v +++ b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v @@ -451,6 +451,7 @@ Proof. 1,3:(apply and_assum; [ih|hp' P'Q]). intros. apply and_assum; [ih|hp' P'Q]. - unshelve eapply Qprim; tea. depelim e. + * constructor. * constructor. * constructor. * eapply Qpres in qt. depelim qt. now cbn in i. constructor; eauto. diff --git a/erasure/theories/EWcbvEvalEtaInd.v b/erasure/theories/EWcbvEvalEtaInd.v index 126667ae3..d048beb4d 100644 --- a/erasure/theories/EWcbvEvalEtaInd.v +++ b/erasure/theories/EWcbvEvalEtaInd.v @@ -692,6 +692,7 @@ Proof. depelim e. * split; simp_eta. unshelve eapply Qprim. constructor. constructor. * split; simp_eta. unshelve eapply Qprim. constructor. constructor. + * split; simp_eta. unshelve eapply Qprim. constructor. constructor. * eapply Qpres in qt. depelim qt. now cbn in i. split; simp_eta. unshelve eapply Qprim. constructor; eauto. constructor. + apply All2_over_undep. cbn in IH. diff --git a/erasure/theories/EWellformed.v b/erasure/theories/EWellformed.v index 78e3a6422..0ad7268a3 100644 --- a/erasure/theories/EWellformed.v +++ b/erasure/theories/EWellformed.v @@ -23,12 +23,14 @@ Definition isSome {A} (o : option A) := Class EPrimitiveFlags := { has_primint : bool; has_primfloat : bool; + has_primstring : bool; has_primarray : bool }. Definition has_prim {epfl : EPrimitiveFlags} (p : prim_val term) := match p.π1 with | primInt => has_primint | primFloat => has_primfloat + | primString => has_primstring | primArray => has_primarray end. @@ -60,6 +62,7 @@ Class EEnvFlags := { Definition all_primitive_flags := {| has_primint := true; has_primfloat := true; + has_primstring := true; has_primarray := true |}. Lemma has_prim_all_primitive_flags p : @has_prim all_primitive_flags p. diff --git a/erasure/theories/ErasureCorrectness.v b/erasure/theories/ErasureCorrectness.v index 6cd516743..db6bc66a7 100644 --- a/erasure/theories/ErasureCorrectness.v +++ b/erasure/theories/ErasureCorrectness.v @@ -1165,6 +1165,8 @@ Proof. depelim X. constructor. + exists (EAst.tPrim (EPrimitive.prim_float f)); split => //; repeat constructor. depelim X. constructor. + + exists (EAst.tPrim (EPrimitive.prim_string s)); split => //; repeat constructor. + depelim X. constructor. + depelim X. subst a0 a'; cbn in *. depelim Hed; cbn in *. eapply inversion_Prim in Hty as [prim_ty [cdecl []]]; cbn in *; eauto. @@ -1409,7 +1411,7 @@ Proof. solve_all. - intros Γ0 v etaΣ er. depelim er; eauto. depelim H1. - depelim H0. 1-2:depelim X; repeat constructor. + depelim H0. 1-3:depelim X; repeat constructor. depelim X0. eapply expanded_tPrim. constructor; split => //; cbn. eapply H0; tea. now depelim etaΣ; cbn in *. eapply Forall_All. depelim etaΣ. cbn in *. diff --git a/erasure/theories/ErasureFunction.v b/erasure/theories/ErasureFunction.v index 75efbea4f..89edfe784 100644 --- a/erasure/theories/ErasureFunction.v +++ b/erasure/theories/ErasureFunction.v @@ -1026,6 +1026,7 @@ Section Erase. E.tCoFix mfix' n | tPrim (primInt; PCUICPrimitive.primIntModel i) := E.tPrim (primInt; EPrimitive.primIntModel i) ; | tPrim (primFloat; PCUICPrimitive.primFloatModel f) := E.tPrim (primFloat; EPrimitive.primFloatModel f) ; + | tPrim (primString; PCUICPrimitive.primStringModel s) := E.tPrim (primString; EPrimitive.primStringModel s) ; | tPrim (primArray; PCUICPrimitive.primArrayModel a) := E.tPrim (primArray; EPrimitive.primArrayModel {| EPrimitive.array_default := erase Γ a.(PCUICPrimitive.array_default) _; @@ -1276,6 +1277,7 @@ Proof. intros isp. eapply isErasable_Proof in isp. eapply H'; intros. now rewrite (abstract_env_ext_irr _ H0 H). + - repeat constructor. - repeat constructor. - repeat constructor. - repeat constructor; eauto. diff --git a/erasure/theories/Extract.v b/erasure/theories/Extract.v index 3a3f72ee9..c5ca0ec26 100644 --- a/erasure/theories/Extract.v +++ b/erasure/theories/Extract.v @@ -71,6 +71,7 @@ Inductive erase_prim_model (erase : term -> E.term -> Prop) : forall {t : prim_t @PCUICPrimitive.prim_model term t -> @prim_model E.term t -> Type := | erase_primInt i : @erase_prim_model erase primInt (PCUICPrimitive.primIntModel i) (primIntModel i) | erase_primFloat f : @erase_prim_model erase primFloat (PCUICPrimitive.primFloatModel f) (primFloatModel f) +| erase_primString s : @erase_prim_model erase primString (PCUICPrimitive.primStringModel s) (primStringModel s) | erase_primArray a ed ev : erase a.(PCUICPrimitive.array_default) ed -> All2 erase a.(PCUICPrimitive.array_value) ev -> @@ -357,6 +358,8 @@ Inductive erases_deps (Σ : global_env) (Σ' : E.global_declarations) : E.term - erases_deps Σ Σ' (E.tPrim (primInt; primIntModel i)) | erases_deps_tPrimFloat f : erases_deps Σ Σ' (E.tPrim (primFloat; primFloatModel f)) +| erases_deps_tPrimString s : + erases_deps Σ Σ' (E.tPrim (primString; primStringModel s)) | erases_deps_tPrimArray a : erases_deps Σ Σ' a.(array_default) -> Forall (erases_deps Σ Σ') a.(array_value) -> diff --git a/erasure/theories/Typed/Certifying.v b/erasure/theories/Typed/Certifying.v index e2c693743..64920a579 100644 --- a/erasure/theories/Typed/Certifying.v +++ b/erasure/theories/Typed/Certifying.v @@ -51,6 +51,7 @@ Definition change_modpath (mpath : modpath) (suffix : string) (to_rename : kerna | tCoFix mfix idx => tCoFix (map (map_def go go) mfix) idx | tInt n => tInt n | tFloat n => tFloat n + | tString n => tString n | tArray l v def ty => tArray l (map go v) (go def) (go ty) end. diff --git a/erasure/theories/Typed/WcbvEvalAux.v b/erasure/theories/Typed/WcbvEvalAux.v index 7f3a7d649..616729500 100644 --- a/erasure/theories/Typed/WcbvEvalAux.v +++ b/erasure/theories/Typed/WcbvEvalAux.v @@ -279,7 +279,7 @@ Qed. Definition eval_prim_length {wfl : WcbvFlags} {Σ p p'} (len : forall t v, Σ e⊢ t ⇓ v -> nat) (d : eval_primitive (eval Σ) p p') : nat := match d with - | evalPrimInt _ | evalPrimFloat _ => 0 + | evalPrimInt _ | evalPrimFloat _ | evalPrimString _ => 0 | evalPrimArray v d v' d' av ev => len _ _ ev + EPrimitive.all2_size _ len av end. diff --git a/pcuic/theories/Bidirectional/BDFromPCUIC.v b/pcuic/theories/Bidirectional/BDFromPCUIC.v index d92a5a6fb..e8f2d5220 100644 --- a/pcuic/theories/Bidirectional/BDFromPCUIC.v +++ b/pcuic/theories/Bidirectional/BDFromPCUIC.v @@ -362,7 +362,7 @@ Proof. - intros p prim_ty cdecl wfΓ' hp hdecl pinv. eexists. split; [econstructor; tea|]. - destruct X0. 1-2:constructor; eauto. + destruct X0. 1-3:constructor; eauto. eapply conv_check in hty; tea. eapply conv_check in hdef; tea. constructor; eauto. solve_all. diff --git a/pcuic/theories/Bidirectional/BDUnique.v b/pcuic/theories/Bidirectional/BDUnique.v index 13bb91a57..baba70a9f 100644 --- a/pcuic/theories/Bidirectional/BDUnique.v +++ b/pcuic/theories/Bidirectional/BDUnique.v @@ -241,6 +241,7 @@ Proof using wfΣ. - depelim X; depelim X0. * inversion X2 ; subst. rewrite H3 in H; noconf H. eexists. split; eapply closed_red_refl; fvs. * inversion X2 ; subst. rewrite H3 in H; noconf H. eexists. split; eapply closed_red_refl; fvs. + * inversion X2 ; subst. rewrite H3 in H; noconf H. eexists. split; eapply closed_red_refl; fvs. * inversion X2 ; subst. rewrite H3 in H; noconf H. eexists. split; eapply closed_red_refl; fvs. all:simp prim_type; cbn. cbn in hty. all:eapply type_is_open_term, checking_typing; tea. diff --git a/pcuic/theories/PCUICAlpha.v b/pcuic/theories/PCUICAlpha.v index 763e5da3f..b0d746fbe 100644 --- a/pcuic/theories/PCUICAlpha.v +++ b/pcuic/theories/PCUICAlpha.v @@ -880,7 +880,7 @@ Section Alpha. + apply eq_term_upto_univ_cumulSpec, eq_term_leq_term, upto_names_impl_eq_term. now symmetry. - intros p prim_ty cdecl IH prim decl pinv pty ptyIH Δ v e e'. - depelim e. depelim o. 1-2:econstructor; eauto; constructor. + depelim e. depelim o. 1-3:econstructor; eauto; constructor. pose proof (validity (type_Prim Σ Γ _ _ _ wfΓ prim decl pinv pty)) as (_ & s & Hs & _). eapply type_Cumul. econstructor; eauto. * depelim ptyIH. constructor; eauto. now rewrite -e. rewrite -e; eauto. diff --git a/pcuic/theories/PCUICAst.v b/pcuic/theories/PCUICAst.v index c6f0f19c6..7c802bfcd 100644 --- a/pcuic/theories/PCUICAst.v +++ b/pcuic/theories/PCUICAst.v @@ -216,6 +216,7 @@ Notation prim_val := (prim_val term). Notation tInt i := (tPrim (_; primIntModel i)) (only parsing). Notation tFloat f := (tPrim (_; primFloatModel f)) (only parsing). +Notation tString s := (tPrim (_; primStringModel s)) (only parsing). Fixpoint mkApps t us := match us with diff --git a/pcuic/theories/PCUICClassification.v b/pcuic/theories/PCUICClassification.v index b67bb8e05..c76e23e21 100644 --- a/pcuic/theories/PCUICClassification.v +++ b/pcuic/theories/PCUICClassification.v @@ -813,7 +813,7 @@ Section classification. - now rewrite head_mkApps /head /=. - eapply inversion_Prim in typed as [prim_ty [cdecl [? ? ? ? hp]]]; eauto. destruct p as [? []]; simp prim_type in w. - 1-2:eapply (invert_cumul_axiom_ind (args := [])) in w; eauto; destruct p0 as [s []]; eauto. + 1-3:eapply (invert_cumul_axiom_ind (args := [])) in w; eauto; destruct p0 as [? []]; eauto. eapply (invert_cumul_axiom_ind (args := [array_type a0])) in w; eauto. destruct p0 as [s []]; eauto. Qed. @@ -1082,7 +1082,7 @@ Section classification. now eapply red_app. - eapply inversion_Prim in Ht as [prim_type [decl []]]; eauto. - depelim X. 1-2:reflexivity. + depelim X. 1-3:reflexivity. depelim p1. specialize (r _ hdef). eapply red_primArray_congr; eauto. eapply All2_undep in a. solve_all. diff --git a/pcuic/theories/PCUICConversion.v b/pcuic/theories/PCUICConversion.v index 0f23a2563..84bb27af6 100644 --- a/pcuic/theories/PCUICConversion.v +++ b/pcuic/theories/PCUICConversion.v @@ -847,6 +847,7 @@ Section ConvCongruences. Σ ;;; Γ ⊢ tPrim p ⇝ T -> (∑ i, p = (primInt; primIntModel i) /\ T = tPrim p) + (∑ f, p = (primFloat; primFloatModel f) /\ T = tPrim p) + + (∑ s, p = (primString; primStringModel s) /\ T = tPrim p) + ∑ a a', [× p = (primArray; primArrayModel a), T = tPrim (primArray; primArrayModel a'), a.(array_level) = a'.(array_level), @@ -859,6 +860,7 @@ Section ConvCongruences. apply: closed_red_ind; intros; subst. - destruct p as [? []]. * now left. + * left. left. now right. * left. now right. * right. exists a, a. cbn in H0; rtoProp; intuition auto. @@ -882,14 +884,17 @@ Section ConvCongruences. * eapply into_closed_red; eauto. * toAll; eapply All_All2; tea; cbn; intuition eauto using into_closed_red. - specialize (X1 _ eq_refl) as []. - * destruct s as [[? []]|[? []]]; subst; + * destruct s as [[[? []]|[? []]]|[? []]]; subst; specialize (X2 _ eq_refl) as []. + left. destruct s; [left|right]; eauto. + destruct s as [? [? []]]. subst. noconf e. + left; destruct s; [left|right]; eauto. + destruct s as [? [? []]]; subst; noconf e. + + left; destruct s; [left|right]; eauto. + + destruct s as [? [? []]]; subst; noconf e. * right. destruct s as [a [a' []]]. - subst. specialize (X2 _ eq_refl) as [[|]|]. + subst. specialize (X2 _ eq_refl) as [[[|]|]|]. + + destruct s as [? []]; congruence. + destruct s as [? []]; congruence. + destruct s as [? []]; congruence. + destruct s as [a2 [a2' []]]; subst. @@ -1461,7 +1466,7 @@ Section Inversions. Proof using wfΣ. intros hd hb ht. destruct p as [? []]; simp prim_type in ht. - 1-2:eapply (invert_cumul_axiom_ind (args := [])) in ht; tea; now destruct hb as [s []]. + 1-3:eapply (invert_cumul_axiom_ind (args := [])) in ht; tea; now destruct hb as [? []]. eapply (invert_cumul_axiom_ind (args := [_])) in ht; tea. apply hb. Qed. @@ -1472,7 +1477,7 @@ Section Inversions. Proof using wfΣ. intros hd hb ht. destruct p as [? []]; simp prim_type in ht. - 1-2:eapply (invert_cumul_axiom_prod (args := [])) in ht; tea; now destruct hb as [s []]. + 1-3:eapply (invert_cumul_axiom_prod (args := [])) in ht; tea; now destruct hb as [? []]. eapply (invert_cumul_axiom_prod (args := [_])) in ht; tea. apply hb. Qed. @@ -1485,8 +1490,9 @@ Section Inversions. move/ws_cumul_pb_alt_closed: hd => [v [v' []]]. move/invert_red_tPrim => hl. move/invert_red_tPrim => hr. - destruct hl as [[[i []]|[f []]]|[a [a' []]]], - hr as [[[i' []]|[f' []]]|[a1 [a2' []]]]; subst; try congruence; + + destruct hl as [[[[i []]|[f []]]|[s []]]|[a [a' []]]], + hr as [[[[i' []]|[f' []]]|[s' []]]|[a1 [a2' []]]]; subst; try congruence; intros eq; depelim eq; depelim o; cbn in cl', cl''; rtoProp; intuition eauto; constructor; eauto. - rewrite e1 e4 //. @@ -3903,7 +3909,7 @@ Lemma ws_cumul_pb_Prim {pb Γ p p'} : Σ;;; Γ ⊢ tPrim p ≤[pb] tPrim p'. Proof. intros Hp HΓ. - depelim Hp. 1-2:constructor; eauto; trea. + depelim Hp. 1-3:constructor; eauto; trea. apply ws_cumul_pb_terms_alt in a0 as [args0 [args0' [Hargs0 Hargs0' Hargs0args0']]]. pose proof (Hargs0_c := closed_red_terms_open_right Hargs0). pose proof (Hargs0'_c := closed_red_terms_open_right Hargs0'). diff --git a/pcuic/theories/PCUICCumulProp.v b/pcuic/theories/PCUICCumulProp.v index 3f5ce1201..129f87810 100644 --- a/pcuic/theories/PCUICCumulProp.v +++ b/pcuic/theories/PCUICCumulProp.v @@ -819,7 +819,7 @@ Qed. Lemma untyped_subslet_inds Γ ind u u' mdecl : untyped_subslet Γ (inds (inductive_mind ind) u (ind_bodies mdecl)) (subst_instance u' (arities_context (ind_bodies mdecl))). -Proof using Type. +Proof using Type Hcf cf. generalize (le_n #|ind_bodies mdecl|). generalize (ind_bodies mdecl) at 1 3 4. unfold inds. @@ -894,7 +894,7 @@ Lemma cumul_prop_mkApps {Σ Γ f args f' args'} {wfΣ : wf_ext Σ} : eq_term Σ.1 Σ f f' -> All2 (cumul_prop Σ Γ) args args' -> Σ ;;; Γ |- mkApps f args ~~ mkApps f' args'. -Proof using Type. +Proof using Type Hcf cf. intros clΓ clf clf' eq eq'. eapply cumul_prop_alt. eapply cumul_prop_args in eq' as (nf & nf' & [redl redr eq']). @@ -997,7 +997,7 @@ Lemma typing_leq_term_prop_gen : forall pb n, compare_term_napp Σ Σ pb n t' t -> Σ ;;; Γ |- T ~~ T') j) (fun Σ Γ => wf_local Σ Γ). -Proof using Type. +Proof using Type Hcf cf. eapply typing_ind_env. { intros ???? H ?. apply lift_typing_impl with (1 := H) => ?? [] ?? ?? //. eauto. } 1: now auto. @@ -1227,7 +1227,7 @@ Proof using Type. - depelim X3. eapply inversion_Prim in X2 as [prim_ty' [cdecl' []]]; tea. depelim o. - 1-2:rewrite H in e; noconf e; eapply cumul_pb_cumul_prop; eauto; pcuic. + 1-3:rewrite H in e; noconf e; eapply cumul_pb_cumul_prop; eauto; pcuic. depelim X1. cbn in H, e2. rewrite H in e2. noconf e2. eapply cumul_pb_cumul_prop; eauto; pcuic. move: w; simp prim_type. intro. etransitivity; tea. constructor; fvs. cbn. @@ -1241,7 +1241,7 @@ Lemma typing_leq_term_prop (Σ : global_env_ext) Γ t t' T T' : Σ ;;; Γ |- t' : T' -> forall pb n, compare_term_napp Σ Σ pb n t' t -> Σ ;;; Γ |- T ~~ T'. -Proof using Type. +Proof using Type Hcf cf. intros. now eapply (env_prop_typing typing_leq_term_prop_gen). Qed. @@ -1251,7 +1251,7 @@ Lemma typing_cumul_term_prop {Σ : global_env_ext} {wfΣ : wf_ext Σ} pb Γ t t' Σ ;;; Γ |- t' : T' -> Σ ;;; Γ |- t' <=[pb] t -> Σ ;;; Γ |- T ~~ T'. -Proof using Type. +Proof using Type Hcf cf. intros. apply cumul_alt in X1 as (v & v' & r & r' & leq). eapply typing_leq_term_prop. 5: eassumption. 1,3: apply wfΣ. diff --git a/pcuic/theories/PCUICEtaExpand.v b/pcuic/theories/PCUICEtaExpand.v index 03e6336be..4da68699b 100644 --- a/pcuic/theories/PCUICEtaExpand.v +++ b/pcuic/theories/PCUICEtaExpand.v @@ -58,6 +58,7 @@ Section map_onPrim. match o with | onPrimInt i => onPrimInt _ i | onPrimFloat f => onPrimFloat _ f + | onPrimString s => onPrimString _ s | onPrimArray a def ty v => onPrimArray _ _ (ont _ def) (ont _ ty) (map_All _ _ ont v) end. diff --git a/pcuic/theories/PCUICNormal.v b/pcuic/theories/PCUICNormal.v index b84636432..afeafcc68 100644 --- a/pcuic/theories/PCUICNormal.v +++ b/pcuic/theories/PCUICNormal.v @@ -1048,7 +1048,7 @@ Proof. cbn. intros ? ? (->&->&r1&r2). eauto. - - depelim o. 1-2: reflexivity. + - depelim o. 1-3: reflexivity. eapply red_primArray_congr; eauto. now eapply Universe.make'_inj in e. Qed. diff --git a/pcuic/theories/PCUICParallelReductionConfluence.v b/pcuic/theories/PCUICParallelReductionConfluence.v index 886f13f3c..8b7611754 100644 --- a/pcuic/theories/PCUICParallelReductionConfluence.v +++ b/pcuic/theories/PCUICParallelReductionConfluence.v @@ -501,6 +501,7 @@ Section Rho. Equations? map_prim_wf (p : PCUICPrimitive.prim_val term) (rho : context -> forall x, depth x < depth (tPrim p) -> term) (Γ : context) : prim_val := | (primInt; primIntModel i), _, _ := (primInt; primIntModel i); | (primFloat; primFloatModel f), _, _ := (primFloat; primFloatModel f); + | (primString; primStringModel s), _, _ := (primString; primStringModel s); | (primArray; primArrayModel a), rho, Γ := let default := rho Γ a.(array_default) _ in let ty := rho Γ a.(array_type) _ in diff --git a/pcuic/theories/PCUICPrincipality.v b/pcuic/theories/PCUICPrincipality.v index 81654c126..7838e1513 100644 --- a/pcuic/theories/PCUICPrincipality.v +++ b/pcuic/theories/PCUICPrincipality.v @@ -716,7 +716,7 @@ Proof. - epose proof (type_Prim _ _ _ _ _ X H H0 H1 X0). eapply validity in X4. depelim X1; depelim X3; depelim o. - 1-2:econstructor; tea. + 1-3:econstructor; tea. depelim X0. destruct X4 as (_ & s & ? & _). econstructor; tea. eapply inversion_Prim in X2 as [prim_ty' [cdecl' []]]; eauto. diff --git a/pcuic/theories/PCUICProgress.v b/pcuic/theories/PCUICProgress.v index cefec7006..522e886eb 100644 --- a/pcuic/theories/PCUICProgress.v +++ b/pcuic/theories/PCUICProgress.v @@ -587,7 +587,7 @@ Proof. intros hdecl hb. induction args => //. destruct prim as [? []]; cbn in *; intros sp; destruct hb; simp prim_type in *. - 1-2:eapply (typing_spine_axiom _ _ _ _ []) in sp; tea. + 1-3:eapply (typing_spine_axiom _ _ _ _ []) in sp; tea. eapply (typing_spine_axiom _ _ _ _ [array_type a0]) in sp; tea. Qed. @@ -782,6 +782,7 @@ Proof with eauto with wcbv; try congruence. eapply value_mkApps_inv in Hval as [[-> ]|[]]; eauto. - intros Σ wfΣ Γ _ p c u mdecl idecl cdecl pdecl Hcon args Hargs -> hp. depelim args... 1-2:right; constructor; constructor 2; constructor. + right. constructor. constructor 2. constructor. depelim Hcon. destruct hdef; eauto. + left. destruct s as [t' hred]. exists (tPrim (prim_array (set_array_default a t'))). now constructor. diff --git a/pcuic/theories/PCUICTyping.v b/pcuic/theories/PCUICTyping.v index 6d66e1f6a..8ea666590 100644 --- a/pcuic/theories/PCUICTyping.v +++ b/pcuic/theories/PCUICTyping.v @@ -178,6 +178,7 @@ Variant primitive_typing_hyps `{checker_flags} Σ Γ : prim_val term -> Type := | prim_int_hyps i : primitive_typing_hyps typing Σ Γ (primInt; primIntModel i) | prim_float_hyps f : primitive_typing_hyps typing Σ Γ (primFloat; primFloatModel f) +| prim_string_hyps s : primitive_typing_hyps typing Σ Γ (primString; primStringModel s) | prim_array_hyps a (wfl : wf_universe Σ (Universe.make' a.(array_level))) (hty : typing Σ Γ a.(array_type) (tSort (sType (Universe.make' a.(array_level))))) @@ -189,6 +190,7 @@ Derive Signature for primitive_typing_hyps. Equations prim_type (p : prim_val term) (cst : kername) : term := prim_type (primInt; _) cst := tConst cst []; prim_type (primFloat; _) cst := tConst cst []; +prim_type (primString; _) cst := tConst cst []; prim_type (primArray; primArrayModel a) cst := tApp (tConst cst [a.(array_level)]) a.(array_type). Transparent prim_type. @@ -409,6 +411,7 @@ Section PrimitiveSize. destruct h. - exact 0. - exact 0. + - exact 0. - exact (Nat.max (typing_size _ _ _ _ hty) (Nat.max (typing_size _ _ _ _ hdef) (all_size _ (fun x p => typing_size _ _ _ _ p) hvalue))). Defined. diff --git a/pcuic/theories/PCUICValidity.v b/pcuic/theories/PCUICValidity.v index ca255c23c..817c746b1 100644 --- a/pcuic/theories/PCUICValidity.v +++ b/pcuic/theories/PCUICValidity.v @@ -340,7 +340,7 @@ Section Validity. - (* Primitive *) depelim X0; depelim X1; simp prim_type; cbn in *. - 1-2:destruct H1 as [hty hbod huniv]; eapply has_sort_isType with (s := _@[[]]); change (tSort ?s@[[]]) with (tSort s)@[[]]; + 1-3:destruct H1 as [hty hbod huniv]; eapply has_sort_isType with (s := _@[[]]); change (tSort ?s@[[]]) with (tSort s)@[[]]; rewrite <- hty; refine (type_Const _ _ _ [] _ wfΓ H0 _); rewrite huniv //. set (s := sType (Universe.make' (array_level a))). destruct H1 as [hty' hbod huniv]. diff --git a/pcuic/theories/PCUICWcbvEval.v b/pcuic/theories/PCUICWcbvEval.v index 56d56895d..d04ba3361 100644 --- a/pcuic/theories/PCUICWcbvEval.v +++ b/pcuic/theories/PCUICWcbvEval.v @@ -205,6 +205,7 @@ Section Wcbv. Variant eval_primitive (eval : term -> term -> Type) : prim_val -> prim_val -> Type := | evalPrimInt i : eval_primitive eval (prim_int i) (prim_int i) | evalPrimFloat f : eval_primitive eval (prim_float f) (prim_float f) + | evalPrimString s : eval_primitive eval (prim_string s) (prim_string s) | evalPrimArray u v def ty v' def' (ev : All2 eval v v') (ed : eval def def') : @@ -216,6 +217,7 @@ Section Wcbv. Variant eval_primitive_ind (eval : term -> term -> Type) (P : forall x y, eval x y -> Type) : forall x y, eval_primitive eval x y -> Type := | evalPrimIntDep i : eval_primitive_ind eval P (prim_int i) (prim_int i) (evalPrimInt eval i) | evalPrimFloatDep f : eval_primitive_ind eval P (prim_float f) (prim_float f) (evalPrimFloat eval f) + | evalPrimStringDep s : eval_primitive_ind eval P (prim_string s) (prim_string s) (evalPrimString eval s) | evalPrimArrayDep u v def ty v' def' (ev : All2 eval v v') (ed : eval def def') : @@ -482,6 +484,7 @@ Section Wcbv. Variant primitive_value (value : term -> Type) : prim_val -> Type := | primIntValue i : primitive_value value (prim_int i) | primFloatValue f : primitive_value value (prim_float f) + | primStringValue s : primitive_value value (prim_string s) | primArrayValue a : All value a.(array_value) -> value a.(array_default) -> diff --git a/pcuic/theories/Syntax/PCUICPosition.v b/pcuic/theories/Syntax/PCUICPosition.v index 39638242b..476804ef7 100644 --- a/pcuic/theories/Syntax/PCUICPosition.v +++ b/pcuic/theories/Syntax/PCUICPosition.v @@ -857,11 +857,11 @@ Proof. + simpl. destruct nth_error as [[na ty bo ra]|] eqn:e. * apply IHp. * rewrite hh. reflexivity. - + destruct prim as [? []]; simpl. 1-2:now rewrite hh. + + destruct prim as [? []]; simpl. 1-3:now rewrite hh. now rewrite IHp. - + destruct prim as [? []]; simpl. 1-2:now rewrite hh. + + destruct prim as [? []]; simpl. 1-3:now rewrite hh. now rewrite IHp. - + destruct prim as [? []]; simpl. 1-2:now rewrite hh. + + destruct prim as [? []]; simpl. 1-3:now rewrite hh. destruct nth_error eqn:e. * now rewrite IHp. * now rewrite hh. diff --git a/pcuic/theories/Syntax/PCUICReflect.v b/pcuic/theories/Syntax/PCUICReflect.v index 15a6b788e..d9b2c0cb2 100644 --- a/pcuic/theories/Syntax/PCUICReflect.v +++ b/pcuic/theories/Syntax/PCUICReflect.v @@ -246,6 +246,7 @@ Proof. destruct (eqb_spec rarg rarg0); t'. destruct (eqb_spec dname dname0); t'. } - destruct p, p; cbn in *; destruct prim, p; cbn; nodec. + case: eqb_spec; intros; subst; nodec. constructor; auto. case: eqb_spec; intros; subst; nodec. constructor; auto. case: eqb_spec; intros; subst; nodec. constructor; auto. destruct X as [eqty [eqd eqv]]. unfold eqb_array. diff --git a/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v b/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v index f4cb79137..721fe0a39 100644 --- a/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v +++ b/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v @@ -86,11 +86,12 @@ Lemma extends_primitive_constant Σ Σ' p t : Proof. intros [_ _ ext]. unfold primitive_constant. - case: ext => o [] o' o''. + case: ext => o [] o' [] o'' o'''. destruct p => //. - intros hr. now rewrite hr in o; depelim o. - intros hr. now rewrite hr in o'; depelim o'. - intros hr. now rewrite hr in o''; depelim o''. + - intros hr. now rewrite hr in o'''; depelim o'''. Qed. Local Hint Resolve extends_primitive_constant : extends. diff --git a/pcuic/theories/utils/PCUICPretty.v b/pcuic/theories/utils/PCUICPretty.v index 94065d591..72444c3cf 100644 --- a/pcuic/theories/utils/PCUICPretty.v +++ b/pcuic/theories/utils/PCUICPretty.v @@ -121,6 +121,7 @@ Module PrintTermTree. match p.π2 return Tree.t with | primIntModel f => "(int: " ^ show f ^ ")" | primFloatModel f => "(float: " ^ show f ^ ")" + | primStringModel s => "(string: " ^ show s ^ ")" | primArrayModel a => "(array:" ^ string_of_list soft a.(array_value) ^ ")" end. diff --git a/pcuic/theories/utils/PCUICPrimitive.v b/pcuic/theories/utils/PCUICPrimitive.v index 9807da587..ea6b9dc42 100644 --- a/pcuic/theories/utils/PCUICPrimitive.v +++ b/pcuic/theories/utils/PCUICPrimitive.v @@ -25,10 +25,12 @@ Proof. eqdec_proof. Qed. Inductive prim_model (term : Type) : prim_tag -> Type := | primIntModel (i : PrimInt63.int) : prim_model term primInt | primFloatModel (f : PrimFloat.float) : prim_model term primFloat +| primStringModel (s : PrimString.string) : prim_model term primString | primArrayModel (a : array_model term) : prim_model term primArray. Arguments primIntModel {term}. Arguments primFloatModel {term}. +Arguments primStringModel {term}. Arguments primArrayModel {term}. Derive Signature NoConfusion NoConfusionHom for prim_model. @@ -37,6 +39,7 @@ Definition prim_model_of (term : Type) (p : prim_tag) : Type := match p with | primInt => PrimInt63.int | primFloat => PrimFloat.float + | primString => PrimString.string | primArray => array_model term end. @@ -46,12 +49,14 @@ Definition prim_val_model {term} (s : prim_val term) : prim_model term (prim_val Definition prim_int {term} i : prim_val term := (primInt; primIntModel i). Definition prim_float {term} f : prim_val term := (primFloat; primFloatModel f). +Definition prim_string {term} s : prim_val term := (primString; primStringModel s). Definition prim_array {term} a : prim_val term := (primArray; primArrayModel a). Definition prim_model_val {term} (p : prim_val term) : prim_model_of term (prim_val_tag p) := match prim_val_model p in prim_model _ t return prim_model_of term t with | primIntModel i => i | primFloatModel f => f + | primStringModel s => s | primArrayModel a => a end. @@ -101,9 +106,23 @@ Next Obligation. all:constructor; congruence. Qed. +#[program,global] +Instance reflect_eq_pstring : ReflectEq PrimString.string := + { eqb := (fun s1 s2 => match PrimString.compare s1 s2 with Eq => true | _ => false end) }. +Next Obligation. discriminate. Qed. +Next Obligation. discriminate. Qed. +Next Obligation. + intros s1 s2. simpl. + destruct (PrimString.compare s1 s2) eqn:Hcmp; constructor. + - by apply PString.string_eq_spec in Hcmp. + - intros Heq%PString.string_eq_spec. rewrite Heq in Hcmp. inversion Hcmp. + - intros Heq%PString.string_eq_spec. rewrite Heq in Hcmp. inversion Hcmp. +Qed. + Equations eqb_prim_model {term} {equ : Level.t -> Level.t -> bool} {req : term -> term -> bool} {t : prim_tag} (x y : prim_model term t) : bool := | primIntModel x, primIntModel y := ReflectEq.eqb x y | primFloatModel x, primFloatModel y := ReflectEq.eqb x y + | primStringModel x, primStringModel y := ReflectEq.eqb x y | primArrayModel x, primArrayModel y := eqb_array (equ := equ) (eqt:=req) x y. #[global, program] @@ -113,6 +132,7 @@ Next Obligation. intros. depelim x; depelim y; simp eqb_prim_model. case: ReflectEq.eqb_spec; constructor; subst; auto. congruence. case: ReflectEq.eqb_spec; constructor; subst; auto. congruence. + case: ReflectEq.eqb_spec; constructor; subst; auto. congruence. change (eqb_array a a0) with (eqb a a0). case: ReflectEq.eqb_spec; constructor; subst; auto. congruence. Qed. @@ -123,6 +143,7 @@ Instance prim_model_eqdec {term} {req : ReflectEq term} : forall p : prim_tag, E Equations eqb_prim_val {term} {equ : Level.t -> Level.t -> bool} {req : term -> term -> bool} (x y : prim_val term) : bool := | (primInt; i), (primInt; i') := eqb_prim_model (equ := equ) (req := req) i i' | (primFloat; f), (primFloat; f') := eqb_prim_model (equ := equ) (req := req) f f' + | (primString; s), (primString; s') := eqb_prim_model (equ := equ) (req := req) s s' | (primArray; a), (primArray; a') := eqb_prim_model (equ := equ) (req := req) a a' | x, y := false. @@ -131,22 +152,19 @@ Instance prim_val_reflect_eq {term} {req : ReflectEq term} : ReflectEq (prim_val {| ReflectEq.eqb := eqb_prim_val (equ := eqb) (req := eqb) |}. Next Obligation. intros. funelim (eqb_prim_val x y); simp eqb_prim_val. - change (eqb_prim_model i i') with (eqb i i'). - case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H. cbn in n. auto. - constructor. intros H; noconf H; auto. - constructor. intros H; noconf H; auto. - constructor. intros H; noconf H; auto. - change (eqb_prim_model f f') with (eqb f f'). - case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto. - constructor. intros H; noconf H; auto. - constructor. intros H; noconf H; auto. - constructor. intros H; noconf H; auto. - change (eqb_prim_model a a') with (eqb a a'). - case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto. + all: try by constructor; intros H; noconf H; auto. + - change (eqb_prim_model i i') with (eqb i i'). + case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H. cbn in n. auto. + - change (eqb_prim_model f f') with (eqb f f'). + case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto. + - change (eqb_prim_model s s') with (eqb s s'). + case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto. + - change (eqb_prim_model a a') with (eqb a a'). + case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto. Qed. #[global] -Instance prim_tag_model_eqdec term {req : ReflectEq term} : EqDec (prim_val term) := _. + Instance prim_tag_model_eqdec term {req : ReflectEq term} : EqDec (prim_val term) := _. (** Printing *) @@ -154,6 +172,7 @@ Definition string_of_prim {term} (soft : term -> string) (p : prim_val term) : s match p.π2 return string with | primIntModel f => "(int: " ^ string_of_prim_int f ^ ")" | primFloatModel f => "(float: " ^ string_of_float f ^ ")" + | primStringModel s => "(string: " ^ string_of_pstring s ^ ")" | primArrayModel a => "(array:" ^ string_of_list soft a.(array_value) ^ ")" end. @@ -162,6 +181,7 @@ Definition string_of_prim {term} (soft : term -> string) (p : prim_val term) : s Inductive onPrim {term} (P : term -> Prop) : prim_val term -> Prop := | onPrimInt i : onPrim P (primInt; primIntModel i) | onPrimFloat f : onPrim P (primFloat; primFloatModel f) + | onPrimString s : onPrim P (primString; primStringModel s) | onPrimArray a : P a.(array_default) -> P a.(array_type) -> @@ -172,6 +192,7 @@ Derive Signature for onPrim. Inductive onPrims {term} (eq_term : term -> term -> Type) Re : prim_val term -> prim_val term -> Type := | onPrimsInt i : onPrims eq_term Re (primInt; primIntModel i) (primInt; primIntModel i) | onPrimsFloat f : onPrims eq_term Re (primFloat; primFloatModel f) (primFloat; primFloatModel f) + | onPrimsString s : onPrims eq_term Re (primString; primStringModel s) (primString; primStringModel s) | onPrimsArray a a' : Re (Universe.make' a.(array_level)) (Universe.make' a'.(array_level)) -> eq_term a.(array_default) a'.(array_default) -> @@ -184,6 +205,7 @@ Definition tPrimProp {term} (P : term -> Type) (p : PCUICPrimitive.prim_val term match p.π2 return Type with | primIntModel f => unit | primFloatModel f => unit + | primStringModel s => unit | primArrayModel a => P a.(array_type) × P a.(array_default) × All P a.(array_value) end. @@ -191,6 +213,7 @@ Definition tPrimProp {term} (P : term -> Type) (p : PCUICPrimitive.prim_val term Inductive onPrims_dep {term} (eq_term : term -> term -> Type) (Re : Universe.t -> Universe.t -> Prop) (eq_term_dep : forall x y, eq_term x y -> Type) (Re' : forall a b, Re a b -> Type) : forall x y : prim_val term, onPrims eq_term Re x y -> Type := | onPrimsInt_dep i : onPrims_dep eq_term Re eq_term_dep Re' (primInt; primIntModel i) (primInt; primIntModel i) (onPrimsInt eq_term Re i) | onPrimsFloat_dep f : onPrims_dep eq_term Re eq_term_dep Re' (primFloat; primFloatModel f) (primFloat; primFloatModel f) (onPrimsFloat _ _ f) + | onPrimsString_dep s : onPrims_dep eq_term Re eq_term_dep Re' (primString; primStringModel s) (primString; primStringModel s) (onPrimsString _ _ s) | onPrimsArray_dep a a' : forall (hre : Re (Universe.make' a.(array_level)) (Universe.make' a'.(array_level))) (eqdef : eq_term a.(array_default) a'.(array_default)) @@ -217,6 +240,7 @@ Equations mapu_prim {term term'} (f : Level.t -> Level.t) (g : term -> term') (p : PCUICPrimitive.prim_val term) : PCUICPrimitive.prim_val term' := | _, _, (primInt; primIntModel i) => (primInt; primIntModel i) | _, _, (primFloat; primFloatModel fl) => (primFloat; primFloatModel fl) +| _, _, (primString; primStringModel s) => (primString; primStringModel s) | f, g, (primArray; primArrayModel ar) => (primArray; primArrayModel (mapu_array_model f g ar)). @@ -226,12 +250,14 @@ Notation map_prim := (mapu_prim id). Equations test_prim {term} (p : term -> bool) (p : prim_val term) : bool := | p, (primInt; _) => true | p, (primFloat; _) => true +| p, (primString; _) => true | p, (primArray; primArrayModel ar) => List.forallb p ar.(array_value) && p ar.(array_default) && p ar.(array_type). Equations test_primu {term} (p : Level.t -> bool) (t : term -> bool) (p : prim_val term) : bool := | _, _, (primInt; _) => true | _, _, (primFloat; _) => true +| _, _, (primString; _) => true | p, pt, (primArray; primArrayModel ar) => p ar.(array_level) && forallb pt ar.(array_value) && pt ar.(array_default) && pt ar.(array_type). diff --git a/pcuic/theories/utils/PCUICSize.v b/pcuic/theories/utils/PCUICSize.v index 3822c0b0d..0d62b37da 100644 --- a/pcuic/theories/utils/PCUICSize.v +++ b/pcuic/theories/utils/PCUICSize.v @@ -27,6 +27,7 @@ Definition prim_size (size : term -> nat) (p : prim_val) : nat := match p.π2 return nat with | primIntModel f => 0 | primFloatModel f => 0 + | primStringModel s => 0 | primArrayModel a => size a.(array_type) + size a.(array_default) + list_size size a.(array_value) end. @@ -60,4 +61,4 @@ Proof. induction l in n |- *; destruct n; simpl => //; auto. - intros [= <-]. lia. - intros hnth. specialize (IHl _ hnth). lia. -Qed. \ No newline at end of file +Qed. diff --git a/quotation/theories/CommonUtils.v b/quotation/theories/CommonUtils.v index 2bc1f6380..bbb28c74a 100644 --- a/quotation/theories/CommonUtils.v +++ b/quotation/theories/CommonUtils.v @@ -188,6 +188,7 @@ Module WithTemplate. | tVar _ | tInt _ | tFloat _ + | tString _ | tArray _ _ _ _ | tConst _ _ | tInd _ _ diff --git a/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v b/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v index eb1225ab6..d3244177a 100644 --- a/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v +++ b/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v @@ -17,6 +17,8 @@ From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) All_Forall. #[export] Instance quote_prim_model {term tag} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (prim_model term tag) := ltac:(destruct 1; eauto). +#[global] Instance quote_pstring : ground_quotable PrimString.string := fun s => PCUICAst.tString s. + #[export] Instance quote_prim_model_of {term tag} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (prim_model_of term tag) := ltac:(cbv [prim_model_of]; destruct tag; exact _). #[export] Instance quote_prim_val {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (prim_val term) := ltac:(cbv [prim_val]; exact _). diff --git a/quotation/theories/ToTemplate/Init.v b/quotation/theories/ToTemplate/Init.v index bc994b34c..b0f730bc3 100644 --- a/quotation/theories/ToTemplate/Init.v +++ b/quotation/theories/ToTemplate/Init.v @@ -109,6 +109,7 @@ Proof. | tSort _ | tInt _ | tFloat _ + | tString _ | tArray _ _ _ _ | tConst _ _ => if head_term_is_bound cur_modpath qt @@ -214,6 +215,7 @@ Proof. | tConstruct _ _ _ | tInt _ | tFloat _ + | tString _ | tArray _ _ _ _ | tInd _ _ => ret qt diff --git a/quotation/theories/ToTemplate/Template/Ast.v b/quotation/theories/ToTemplate/Template/Ast.v index 28de2e3df..925d6c009 100644 --- a/quotation/theories/ToTemplate/Template/Ast.v +++ b/quotation/theories/ToTemplate/Template/Ast.v @@ -6,6 +6,8 @@ From MetaCoq.Quotation.ToTemplate.Common Require Import Environment EnvironmentT From MetaCoq.Quotation.ToTemplate.QuotationOf.Common Require Import Environment.Sig EnvironmentTyping.Sig. From MetaCoq.Quotation.ToTemplate.QuotationOf.Template Require Import Ast.Instances ReflectAst.Instances. +#[export] Instance quote_pstring : ground_quotable PrimString.string := fun s => Ast.tString s. + #[export] Instance quote_predicate {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (predicate term) := ltac:(destruct 1; exact _). #[export] Instance quote_branch {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (branch term) := ltac:(destruct 1; exact _). #[local] Hint Extern 1 => assumption : typeclass_instances. diff --git a/safechecker/theories/PCUICEqualityDec.v b/safechecker/theories/PCUICEqualityDec.v index 9980add1c..40014fa3b 100644 --- a/safechecker/theories/PCUICEqualityDec.v +++ b/safechecker/theories/PCUICEqualityDec.v @@ -520,7 +520,7 @@ Proof. cbn in X, ht, ht'; rewrite /eqb_prim_val /eqb_prim_model; cbn -[eqb]; try eqspecs; try repeat constructor. - 1-8:intros e; depelim e; try depelim o; intuition eauto. + 1-15:intros e; depelim e; try depelim o; intuition eauto. rtoProp. destruct X as (hty & hdef & harr). eapply reflectT_change_left. { split; intros XE. 1: constructor; now apply XE. now depelim XE. } eapply reflectT_change_left4. { split; intros XE. 1: destruct XE as [XE1 XE2 XE3 XE4]; constructor; [apply XE1|apply XE3|apply XE4|apply XE2]. now depelim XE. } diff --git a/safechecker/theories/PCUICSafeConversion.v b/safechecker/theories/PCUICSafeConversion.v index 4c294d059..a4ebfc55a 100644 --- a/safechecker/theories/PCUICSafeConversion.v +++ b/safechecker/theories/PCUICSafeConversion.v @@ -3586,6 +3586,9 @@ Equations (noeqns) isconv_array_values_aux | (primFloat; primFloatModel f) | (primFloat; primFloatModel f') with inspect (eqb f f') := { | @exist true eqf := yes | @exist false neqf := no (DistinctPrimValues (Γ ,,, stack_context π1) p (Γ ,,, stack_context π2) p') } + | (primString; primStringModel f) | (primString; primStringModel f') with inspect (eqb f f') := + { | @exist true eqf := yes + | @exist false neqf := no (DistinctPrimValues (Γ ,,, stack_context π1) p (Γ ,,, stack_context π2) p') } | (primArray; primArrayModel a) | (primArray; primArrayModel a') with inspect (abstract_env_compare_universe X Conv (Universe.make' (array_level a)) (Universe.make' (array_level a'))) := { | @exist false neql := no (ArrayNotConvertibleLevels (Γ ,,, stack_context π1) a (Γ ,,, stack_context π2) a') @@ -4765,6 +4768,44 @@ Qed. now rewrite eqb_refl in neqf. Qed. + Next Obligation. + Proof. + symmetry in eqf. + apply eqb_eq in eqf; subst f'. + rename H into wfΣ. pose proof (hΣ _ wfΣ) as [hΣ]. + clear aux. + specialize (hx Σ wfΣ). + specialize (h1 Σ wfΣ). + specialize (h2 Σ wfΣ). + apply welltyped_zipc_zipp in h1; eauto. + eapply welltyped_zipc_zipp in h2; eauto. + rewrite !zipp_as_mkApps in h1, h2 |- *. + apply mkApps_Prim_nil in h1; auto. + apply mkApps_Prim_nil in h2; auto. + rewrite h1 h2; cbn. + red. sq. eapply ws_cumul_pb_Prim; eauto; fvs. + constructor. + Qed. + + Next Obligation. + Proof. + destruct (abstract_env_ext_exists X) as [[Σ wfΣ]]. + pose proof (hΣ _ wfΣ) as [hΣ]. + specialize (H _ wfΣ). + specialize (hx Σ wfΣ). + specialize (h1 Σ wfΣ). + apply welltyped_zipc_zipp in h1; eauto. + clear aux. + eapply welltyped_zipc_zipp in h2; eauto. + rewrite !zipp_as_mkApps in h1, h2, H |- *. + apply mkApps_Prim_nil in h1; auto. + apply mkApps_Prim_nil in h2; auto. + rewrite h1 h2 in H. + destruct H as [H]. cbn in H. + eapply invert_cumul_Prim in H; depelim H. + now rewrite eqb_refl in neqf. + Qed. + Next Obligation. Proof. destruct a; eauto. diff --git a/safechecker/theories/PCUICTypeChecker.v b/safechecker/theories/PCUICTypeChecker.v index 75d642aaf..b968cc1bc 100644 --- a/safechecker/theories/PCUICTypeChecker.v +++ b/safechecker/theories/PCUICTypeChecker.v @@ -1318,6 +1318,11 @@ Section Typecheck. check_eq_true (eqb decl.(cst_universes) Monomorphic_ctx) (Msg "primitive type for floats is registered to non-monomorphic constant") ;; check_eq_true (eqb decl.(cst_type) (tSort Sort.type0)) (Msg "primitive type for floats is registered to an axiom whose type is not the sort Set") ;; ret _ + | primString | decl := + check_eq_true (eqb decl.(cst_body) None) (Msg "primitive type is registered to a defined constant") ;; + check_eq_true (eqb decl.(cst_universes) Monomorphic_ctx) (Msg "primitive type for strings is registered to non-monomorphic constant") ;; + check_eq_true (eqb decl.(cst_type) (tSort Sort.type0)) (Msg "primitive type for strings is registered to an axiom whose type is not the sort Set") ;; + ret _ | primArray | decl := let s := sType (Universe.make' (Level.lvar 0)) in check_eq_true (eqb decl.(cst_body) None) (Msg "primitive type is registered to a defined constant") ;; @@ -1328,15 +1333,7 @@ Section Typecheck. all:try eapply eqb_eq in i. all:try apply eqb_eq in i0. all:try apply eqb_eq in i1 => //. - - destruct H as []. rewrite H in absurd; eauto. - - destruct H as []. apply absurd. now rewrite H1; apply eqb_refl. - - destruct H as []. apply absurd; rewrite H0; apply eqb_refl. - - destruct H as []. rewrite H in absurd; eauto. - - destruct H as []. apply absurd. now rewrite H1; apply eqb_refl. - - destruct H as []. apply absurd; rewrite H0; apply eqb_refl. - - destruct H as []. rewrite H in absurd; eauto. - - destruct H as []. apply absurd. now rewrite H1; apply eqb_refl. - - destruct H as []. apply absurd; rewrite H0; apply eqb_refl. + all:destruct H as []; apply absurd; rewrite ?H ?H0 ?H1; eauto. Qed. Section make_All. @@ -1362,6 +1359,7 @@ Section Typecheck. Equations? check_primitive_typing (p : prim_val) : typing_result_comp (forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ primitive_typing_hyps checking Σ Γ p ∥) := | (primInt; primIntModel i) := ret _ | (primFloat; primFloatModel f) := ret _ + | (primString; primStringModel f) := ret _ | (primArray; primArrayModel a) := check_eq_true (abstract_env_ext_wf_universeb X (Universe.make' a.(array_level))) (Msg "primitive array level is not well-formed") ;; check_type <- bdcheck infer Γ wfΓ a.(array_type) (tSort (sType (Universe.make' a.(array_level)))) _ ;; @@ -1372,7 +1370,7 @@ Section Typecheck. all:intros. all:try pose proof (abstract_env_ext_wf _ wfΣ) as [wfΣ']. all:try specialize (wfΓ _ wfΣ). - 1-2:do 2 constructor. + 1-3:do 2 constructor. - eauto. - sq. erewrite <- abstract_env_ext_wf_universeb_correct in i; tea. eapply has_sort_isType; eapply type_Sort; eauto. diff --git a/template-coq/_PluginProject b/template-coq/_PluginProject index 314e020ac..b1fc2531f 100644 --- a/template-coq/_PluginProject +++ b/template-coq/_PluginProject @@ -195,8 +195,12 @@ gen-src/primFloat.ml gen-src/primFloat.mli gen-src/primInt63.ml gen-src/primInt63.mli +gen-src/primString.ml +gen-src/primString.mli gen-src/primitive.ml gen-src/primitive.mli +gen-src/pString.ml +gen-src/pString.mli gen-src/quoter.ml gen-src/reflect.ml gen-src/reflect.mli diff --git a/template-coq/_PluginProject.in b/template-coq/_PluginProject.in index dcecb5541..740a83958 100644 --- a/template-coq/_PluginProject.in +++ b/template-coq/_PluginProject.in @@ -193,8 +193,12 @@ gen-src/primFloat.ml gen-src/primFloat.mli gen-src/primInt63.ml gen-src/primInt63.mli +gen-src/primString.ml +gen-src/primString.mli gen-src/primitive.ml gen-src/primitive.mli +gen-src/pString.ml +gen-src/pString.mli gen-src/quoter.ml gen-src/reflect.ml gen-src/reflect.mli diff --git a/template-coq/gen-src/metacoq_template_plugin.mlpack b/template-coq/gen-src/metacoq_template_plugin.mlpack index 78da99ee2..0f93f7515 100644 --- a/template-coq/gen-src/metacoq_template_plugin.mlpack +++ b/template-coq/gen-src/metacoq_template_plugin.mlpack @@ -74,6 +74,8 @@ Zpower SpecFloat PrimFloat FloatOps +PrimString +PString MCString Sint63 Show diff --git a/template-coq/src/ast_denoter.ml b/template-coq/src/ast_denoter.ml index f5f349413..4accda36a 100644 --- a/template-coq/src/ast_denoter.ml +++ b/template-coq/src/ast_denoter.ml @@ -13,6 +13,7 @@ struct type quoted_int = Datatypes.nat type quoted_int63 = Uint63.t type quoted_float64 = Float64.t + type quoted_pstring = Pstring.t type quoted_bool = bool type quoted_name = name type quoted_aname = name binder_annot @@ -104,7 +105,7 @@ struct let inspect_term (tt: t):(t, quoted_int, quoted_ident, quoted_aname, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_level, quoted_univ_instance, quoted_proj, - quoted_int63, quoted_float64) structure_of_term = + quoted_int63, quoted_float64, quoted_pstring) structure_of_term = match tt with | Coq_tRel n -> ACoq_tRel n | Coq_tVar v -> ACoq_tVar v @@ -125,6 +126,7 @@ struct | Coq_tCoFix (a,b) -> ACoq_tCoFix (List.map unquote_def a,b) | Coq_tInt i -> ACoq_tInt i | Coq_tFloat f -> ACoq_tFloat f + | Coq_tString s -> ACoq_tString s | Coq_tArray (u, arr, def, ty) -> ACoq_tArray (u, Array.of_list arr, def, ty) let unquote_string = Caml_bytestring.caml_string_of_bytestring @@ -161,6 +163,8 @@ struct let unquote_float64 i = i + let unquote_pstring s = s + (* val unquote_sort : quoted_sort -> Sorts.t *) (* val unquote_sort_family : quoted_sort_family -> Sorts.family *) let unquote_cast_kind (q : quoted_cast_kind) : Constr.cast_kind = diff --git a/template-coq/src/ast_quoter.ml b/template-coq/src/ast_quoter.ml index bae47d447..b287cf827 100644 --- a/template-coq/src/ast_quoter.ml +++ b/template-coq/src/ast_quoter.ml @@ -14,6 +14,7 @@ struct type quoted_int = Datatypes.nat type quoted_int63 = Uint63.t type quoted_float64 = Float64.t + type quoted_pstring = Pstring.t type quoted_bool = bool type quoted_name = BasicAst.name type quoted_aname = BasicAst.aname @@ -80,6 +81,8 @@ struct let quote_float64 x = x + let quote_pstring x = x + let quote_level (l : Univ.Level.t) : Universes0.Level.t = if Univ.Level.is_set l then Universes0.Level.Coq_lzero else match Univ.Level.var_index l with @@ -240,6 +243,7 @@ struct let mkLetIn na b t t' = Coq_tLetIn (na,b,t,t') let mkInt i = Coq_tInt i let mkFloat f = Coq_tFloat f + let mkString s = Coq_tString s let mkArray u arr ~default ~ty = Coq_tArray (u, Array.to_list arr, default, ty) let rec seq f t = @@ -320,11 +324,13 @@ struct type pre_quoted_retroknowledge = { retro_int63 : quoted_kernel_name option; retro_float64 : quoted_kernel_name option; + retro_string : quoted_kernel_name option; retro_array : quoted_kernel_name option } let quote_retroknowledge r = { Environment.Retroknowledge.retro_int63 = r.retro_int63; Environment.Retroknowledge.retro_float64 = r.retro_float64; + Environment.Retroknowledge.retro_string = r.retro_string; Environment.Retroknowledge.retro_array = r.retro_array } let mk_global_env universes declarations retroknowledge = { universes; declarations; retroknowledge } @@ -376,7 +382,7 @@ struct let inspectTerm (t : term) : (term, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_level, quoted_univ_instance, quoted_proj, - quoted_int63, quoted_float64) structure_of_term = + quoted_int63, quoted_float64, quoted_pstring) structure_of_term = match t with | Coq_tRel n -> ACoq_tRel n (* todo ! *) diff --git a/template-coq/src/constr_denoter.ml b/template-coq/src/constr_denoter.ml index a8095b373..c0cbc21e4 100644 --- a/template-coq/src/constr_denoter.ml +++ b/template-coq/src/constr_denoter.ml @@ -79,6 +79,11 @@ struct | Constr.Float f -> f | _ -> not_supported_verb trm "unquote_float64" + let unquote_pstring trm = + match Constr.kind trm with + | Constr.String s -> s + | _ -> not_supported_verb trm "unquote_pstring" + let unquote_char trm = let (h,args) = app_full trm [] in match Constr.kind h with @@ -378,7 +383,7 @@ struct let inspect_term (t:Constr.t) : (Constr.t, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_level, quoted_univ_instance, quoted_proj, - quoted_int63, quoted_float64) structure_of_term = + quoted_int63, quoted_float64, quoted_pstring) structure_of_term = (* debug (fun () -> Pp.(str "denote_term" ++ spc () ++ print_term t)) ; *) let (h,args) = app_full t [] in if constr_equall h tRel then @@ -480,6 +485,10 @@ struct match args with t::_ -> ACoq_tFloat t | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if constr_equall h tString then + match args with + t::_ -> ACoq_tString t + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) else if constr_equall h tArray then match args with u::v::def::ty::_ -> ACoq_tArray (u, Array.of_list (unquote_list v), def, ty) diff --git a/template-coq/src/constr_quoter.ml b/template-coq/src/constr_quoter.ml index 24c317e04..fff2a8d20 100644 --- a/template-coq/src/constr_quoter.ml +++ b/template-coq/src/constr_quoter.ml @@ -95,6 +95,7 @@ struct let mkInt i = i let mkFloat f = f + let mkString s = s let mkArray u arr ~default ~ty = constr_mkApp (tArray, [| u; to_coq_listl tTerm (Array.to_list arr); default; ty |]) @@ -129,6 +130,9 @@ struct let quote_int63 i = constr_mkApp (tInt, [| Constr.mkInt i |]) let quote_float64 f = constr_mkApp (tFloat, [| Constr.mkFloat f |]) + + let quote_pstring s = constr_mkApp (tString, [| Constr.mkString s |]) + let quote_inductive (kn, i) = constr_mkApp (tmkInd, [| kn; i |]) @@ -423,13 +427,15 @@ struct type pre_quoted_retroknowledge = { retro_int63 : quoted_kernel_name option; retro_float64 : quoted_kernel_name option; + retro_string : quoted_kernel_name option; retro_array : quoted_kernel_name option } let quote_retroknowledge r = let rint63 = to_coq_option (Lazy.force tkername) (fun x -> x) r.retro_int63 in let rfloat64 = to_coq_option (Lazy.force tkername) (fun x -> x) r.retro_float64 in + let rstring = to_coq_option (Lazy.force tkername) (fun x -> x) r.retro_string in let rarray = to_coq_option (Lazy.force tkername) (fun x -> x) r.retro_array in - constr_mkApp (tmk_retroknowledge, [| rint63; rfloat64; rarray |]) + constr_mkApp (tmk_retroknowledge, [| rint63; rfloat64; rstring; rarray |]) let mk_global_env univs decls retro = constr_mkApp (tBuild_global_env, [| univs; decls; retro |]) diff --git a/template-coq/src/constr_reification.ml b/template-coq/src/constr_reification.ml index ff8c9f665..c590bb610 100644 --- a/template-coq/src/constr_reification.ml +++ b/template-coq/src/constr_reification.ml @@ -17,6 +17,7 @@ struct type quoted_proj = Constr.t (* of type Ast.projection *) type quoted_int63 = Constr.t (* of type UInt63.t *) type quoted_float64 = Constr.t (* of type Float64.t *) + type quoted_pstring = Constr.t (* of type Float64.t *) type quoted_global_reference = Constr.t (* of type Ast.global_reference *) type quoted_sort_family = Constr.t (* of type Ast.sort_family *) diff --git a/template-coq/src/denoter.ml b/template-coq/src/denoter.ml index f84405bc4..5e4bcdfb2 100644 --- a/template-coq/src/denoter.ml +++ b/template-coq/src/denoter.ml @@ -15,6 +15,7 @@ sig val unquote_bool : quoted_bool -> bool val unquote_int63 : quoted_int63 -> Uint63.t val unquote_float64 : quoted_float64 -> Float64.t + val unquote_pstring : quoted_pstring -> Pstring.t val unquote_cast_kind : quoted_cast_kind -> Constr.cast_kind val unquote_kn : quoted_kernel_name -> KerName.t val unquote_inductive : quoted_inductive -> Names.inductive @@ -28,7 +29,7 @@ sig (* val representsIndConstuctor : quoted_inductive -> Term.constr -> bool *) val inspect_term : t -> (t, quoted_int, quoted_ident, quoted_aname, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_level, quoted_univ_instance, quoted_proj, - quoted_int63, quoted_float64) structure_of_term + quoted_int63, quoted_float64, quoted_pstring) structure_of_term end @@ -165,6 +166,7 @@ struct evm, Constr.mkProj (p', r, t') | ACoq_tInt x -> evm, Constr.mkInt (D.unquote_int63 x) | ACoq_tFloat x -> evm, Constr.mkFloat (D.unquote_float64 x) + | ACoq_tString x -> evm, Constr.mkString (D.unquote_pstring x) | ACoq_tArray (u, arr, def, ty) -> let evm, u = D.unquote_universe_level evm u in let evm, arr = CArray.fold_left_map (fun evm a -> aux env evm a) evm arr in diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml index a523f3367..6b2bc9630 100644 --- a/template-coq/src/quoter.ml +++ b/template-coq/src/quoter.ml @@ -85,6 +85,7 @@ sig val mkCoFix : (quoted_int array * quoted_int) * (quoted_aname array * t array * t array) -> t val mkInt : quoted_int63 -> t val mkFloat : quoted_float64 -> t + val mkString : quoted_pstring -> t val mkArray : quoted_univ_level -> t array -> default:t -> ty:t -> t val mkBindAnn : quoted_name -> quoted_relevance -> quoted_aname @@ -107,6 +108,7 @@ sig (* Primitive objects *) val quote_int63 : Uint63.t -> quoted_int63 val quote_float64 : Float64.t -> quoted_float64 + val quote_pstring : Pstring.t -> quoted_pstring val quote_constraint_type : Univ.constraint_type -> quoted_constraint_type val quote_univ_constraint : Univ.univ_constraint -> quoted_univ_constraint @@ -174,6 +176,7 @@ sig type pre_quoted_retroknowledge = { retro_int63 : quoted_kernel_name option; retro_float64 : quoted_kernel_name option; + retro_string : quoted_kernel_name option; retro_array : quoted_kernel_name option } val quote_retroknowledge : pre_quoted_retroknowledge -> quoted_retroknowledge @@ -359,6 +362,7 @@ struct (Q.mkProj p' t', add_inductive (Projection.inductive p) mib acc) | Constr.Int i -> (Q.mkInt (Q.quote_int63 i), acc) | Constr.Float f -> (Q.mkFloat (Q.quote_float64 f), acc) + | Constr.String s -> (Q.mkString (Q.quote_pstring s), acc) | Constr.Meta _ -> failwith "Meta not supported by TemplateCoq" | Constr.Array (u, ar, def, ty) -> let u = match UVars.Instance.to_array u with (_, [| u |]) -> u | _ -> assert false in @@ -610,6 +614,7 @@ struct let pre = { Q.retro_int63 = quote_retro retro.Retroknowledge.retro_int63 ; Q.retro_float64 = quote_retro retro.Retroknowledge.retro_float64 ; + Q.retro_string = quote_retro retro.Retroknowledge.retro_string ; Q.retro_array = quote_retro retro.Retroknowledge.retro_array } in Q.quote_retroknowledge pre in diff --git a/template-coq/src/reification.ml b/template-coq/src/reification.ml index 5eae5f27e..1f5e77788 100644 --- a/template-coq/src/reification.ml +++ b/template-coq/src/reification.ml @@ -16,6 +16,7 @@ sig type quoted_proj type quoted_int63 type quoted_float64 + type quoted_pstring type quoted_global_reference diff --git a/template-coq/src/tm_util.ml b/template-coq/src/tm_util.ml index 6a13c0cb0..aef445e47 100644 --- a/template-coq/src/tm_util.ml +++ b/template-coq/src/tm_util.ml @@ -338,7 +338,7 @@ type ('nat, 'inductive, 'relevance) acase_info = aci_npar : 'nat; aci_relevance : 'relevance } -type ('term, 'nat, 'ident, 'name, 'quoted_sort, 'cast_kind, 'kername, 'inductive, 'relevance, 'universe_level, 'universe_instance, 'projection, 'int63, 'float64) structure_of_term = +type ('term, 'nat, 'ident, 'name, 'quoted_sort, 'cast_kind, 'kername, 'inductive, 'relevance, 'universe_level, 'universe_instance, 'projection, 'int63, 'float64, 'pstring) structure_of_term = | ACoq_tRel of 'nat | ACoq_tVar of 'ident | ACoq_tEvar of 'nat * 'term list @@ -359,5 +359,6 @@ type ('term, 'nat, 'ident, 'name, 'quoted_sort, 'cast_kind, 'kername, 'inductive | ACoq_tCoFix of ('term, 'name, 'nat) amfixpoint * 'nat | ACoq_tInt of 'int63 | ACoq_tFloat of 'float64 + | ACoq_tString of 'pstring | ACoq_tArray of 'universe_level * 'term array * 'term * 'term diff --git a/template-coq/theories/Ast.v b/template-coq/theories/Ast.v index c29d1e03b..a892e9228 100644 --- a/template-coq/theories/Ast.v +++ b/template-coq/theories/Ast.v @@ -3,7 +3,7 @@ From Equations Require Import Equations. From MetaCoq.Utils Require Import utils. From MetaCoq.Common Require Export Environment EnvironmentTyping Universes BasicAst. (* For primitive integers and floats *) -From Coq Require Uint63 Floats.PrimFloat Floats.SpecFloat PArray. +From Coq Require Uint63 Floats.PrimFloat Floats.SpecFloat PArray PrimString. From Coq Require Import ssreflect Morphisms. (** * AST of Coq kernel terms and kernel data structures @@ -416,6 +416,7 @@ Inductive term : Type := | tCoFix (mfix : mfixpoint term) (idx : nat) | tInt (i : PrimInt63.int) | tFloat (f : PrimFloat.float) +| tString (s : PrimString.string) | tArray (u : Level.t) (arr : list term) (default : term) (type : term). (** This can be used to represent holes, that, when unquoted, turn into fresh existential variables. @@ -565,7 +566,7 @@ Fixpoint noccur_between k n (t : term) : bool := fix subst_instance_constr u c {struct c} : term := match c with | tRel _ | tVar _ => c - | tInt _ | tFloat _ => c + | tInt _ | tFloat _ | tString _ => c | tArray u' arr def ty => tArray (subst_instance_level u u') (List.map (subst_instance_constr u) arr) (subst_instance_constr u def) (subst_instance_constr u ty) | tEvar ev args => tEvar ev (List.map (subst_instance_constr u) args) diff --git a/template-coq/theories/AstUtils.v b/template-coq/theories/AstUtils.v index f0776280c..13a19a57b 100644 --- a/template-coq/theories/AstUtils.v +++ b/template-coq/theories/AstUtils.v @@ -68,6 +68,7 @@ Module string_of_term_tree. | tCoFix l n => "CoFix(" ^ (string_of_list (string_of_def string_of_term) l) ^ "," ^ string_of_nat n ^ ")" | tInt i => "Int(" ^ string_of_prim_int i ^ ")" | tFloat f => "Float(" ^ string_of_float f ^ ")" + | tString s => "String(" ^ string_of_pstring s ^ ")" | tArray u arr def ty => "Array(" ^ string_of_level u ^ "," ^ string_of_list string_of_term arr ^ "," ^ string_of_term def ^ "," ^ string_of_term ty ^ ")" end. @@ -257,7 +258,7 @@ Fixpoint strip_casts t := | tArray u arr def ty => tArray u (List.map strip_casts arr) (strip_casts def) (strip_casts ty) | tRel _ | tVar _ | tSort _ | tConst _ _ | tInd _ _ | tConstruct _ _ _ => t - | tInt _ | tFloat _ => t + | tInt _ | tFloat _ | tString _ => t end. Fixpoint decompose_prod_assum (Γ : context) (t : term) : context * term := diff --git a/template-coq/theories/Checker.v b/template-coq/theories/Checker.v index 6b5c7b1fc..128511517 100644 --- a/template-coq/theories/Checker.v +++ b/template-coq/theories/Checker.v @@ -800,7 +800,7 @@ Section Typecheck. | None => raise (IllFormedFix mfix n) end - | tInt _ | tFloat _ | tArray _ _ _ _ => raise (NotSupported "primitive types") + | tInt _ | tFloat _ | tString _ | tArray _ _ _ _ => raise (NotSupported "primitive types") end. Definition check (Γ : context) (t : term) (ty : term) : typing_result unit := diff --git a/template-coq/theories/EtaExpand.v b/template-coq/theories/EtaExpand.v index 7e9c2b03b..a36212f92 100644 --- a/template-coq/theories/EtaExpand.v +++ b/template-coq/theories/EtaExpand.v @@ -138,7 +138,7 @@ Section Eta. end | tCast t1 k t2 => tCast (eta_expand Γ t1) k (eta_expand Γ t2) | tArray u arr def ty => tArray u (List.map (eta_expand Γ) arr) (eta_expand Γ def) (eta_expand Γ ty) - | tInt _ | tFloat _ => t + | tInt _ | tFloat _ | tString _ => t end. End Eta. @@ -294,6 +294,7 @@ Inductive expanded (Γ : list nat): term -> Prop := expanded Γ (tApp (tConstruct ind c u) args) | expanded_tInt i : expanded Γ (tInt i) | expanded_tFloat f : expanded Γ (tFloat f) +| expanded_tString s : expanded Γ (tString s) | expanded_tArray u arr def ty : Forall (expanded Γ) arr -> expanded Γ def -> @@ -363,6 +364,7 @@ forall (Σ : global_env) (P : list nat -> term -> Prop), P Γ(tApp (tConstruct ind c u) args)) -> (forall Γ i, P Γ (tInt i)) -> (forall Γ f, P Γ (tFloat f)) -> +(forall Γ s, P Γ (tString s)) -> (forall Γ u arr def ty, Forall (P Γ) arr -> P Γ def -> @@ -370,7 +372,7 @@ forall (Σ : global_env) (P : list nat -> term -> Prop), P Γ (tArray u arr def ty)) -> forall Γ, forall t : term, expanded Σ Γ t -> P Γ t. Proof. - intros Σ P HRel HRel_app HVar HEvar HSort HCast HProd HLamdba HLetIn HApp HConst HInd HConstruct HCase HProj HFix HCoFix HConstruct_app Hint Hfloat Harr. + intros Σ P HRel HRel_app HVar HEvar HSort HCast HProd HLamdba HLetIn HApp HConst HInd HConstruct HCase HProj HFix HCoFix HConstruct_app Hint Hfloat Hstring Harr. fix f 3. intros Γ t Hexp. destruct Hexp; eauto. all: match goal with [H : Forall _ _ |- _] => let all := fresh "all" in rename H into all end. diff --git a/template-coq/theories/Extraction.v b/template-coq/theories/Extraction.v index 2315f833f..9af1bba3f 100644 --- a/template-coq/theories/Extraction.v +++ b/template-coq/theories/Extraction.v @@ -10,7 +10,7 @@ From Coq Require Ascii Extraction ZArith NArith. From MetaCoq.Utils Require Import utils. From MetaCoq.Common Require Import Reflect config. From MetaCoq.Template Require Import Ast Induction. -From Coq Require Import FSets ExtrOcamlBasic ExtrOCamlFloats ExtrOCamlInt63. +From Coq Require Import FSets ExtrOcamlBasic ExtrOCamlFloats ExtrOCamlInt63 ExtrOCamlPString. Extract Inductive Equations.Init.sigma => "( * )" ["(,)"]. Extract Constant Equations.Init.pr1 => "fst". diff --git a/template-coq/theories/Induction.v b/template-coq/theories/Induction.v index d484cef7c..cabd504fb 100644 --- a/template-coq/theories/Induction.v +++ b/template-coq/theories/Induction.v @@ -34,6 +34,7 @@ Lemma term_forall_list_ind : (forall (m : mfixpoint term) (n : nat), tFixProp P P m -> P (tCoFix m n)) -> (forall i, P (tInt i)) -> (forall f, P (tFloat f)) -> + (forall s, P (tString s)) -> (forall u arr def ty, Forall P arr -> P def -> P ty -> P (tArray u arr def ty)) -> forall t : term, P t. Proof. @@ -78,6 +79,7 @@ Lemma term_forall_list_rect : (forall (m : mfixpoint term) (n : nat), tFixType P P m -> P (tCoFix m n)) -> (forall i, P (tInt i)) -> (forall f, P (tFloat f)) -> + (forall s, P (tString s)) -> (forall u arr def ty, All P arr -> P def -> P ty -> P (tArray u arr def ty)) -> forall t : term, P t. Proof. diff --git a/template-coq/theories/Pretty.v b/template-coq/theories/Pretty.v index 2a16201f6..eb0171d30 100644 --- a/template-coq/theories/Pretty.v +++ b/template-coq/theories/Pretty.v @@ -252,6 +252,7 @@ Module PrintTermTree. " in " ^ List.nth_default (string_of_nat n) (map (string_of_name ∘ binder_name ∘ dname) l) n) | tInt i => "Int(" ^ string_of_prim_int i ^ ")" | tFloat f => "Float(" ^ string_of_float f ^ ")" + | tString s => "Float(" ^ string_of_pstring s ^ ")" | tArray u arr def ty => "Array(" ^ string_of_level u ^ "," ^ string_of_list string_of_term arr ^ "," ^ string_of_term def ^ "," ^ string_of_term ty ^ ")" end. diff --git a/template-coq/theories/ReflectAst.v b/template-coq/theories/ReflectAst.v index f2decc81a..283fcb460 100644 --- a/template-coq/theories/ReflectAst.v +++ b/template-coq/theories/ReflectAst.v @@ -57,6 +57,14 @@ Defined. Derive NoConfusion NoConfusionHom for term. +#[global] Instance EqDec_pstring : EqDec PrimString.string. +Proof. + intros s1 s2. destruct (PrimString.compare s1 s2) eqn:Hcmp; [left|right|right]. + - by apply PString.string_eq_spec. + - intros Heq%PString.string_eq_spec. rewrite Heq in Hcmp. discriminate Hcmp. + - intros Heq%PString.string_eq_spec. rewrite Heq in Hcmp. discriminate Hcmp. +Qed. + #[global] Instance EqDec_term : EqDec term. Proof. intro x; induction x using term_forall_list_rect ; intro t ; @@ -158,6 +166,8 @@ Proof. subst. left. reflexivity. - destruct (eq_dec f f0) ; nodec. subst. left. reflexivity. + - destruct (eq_dec s s0) ; nodec. + subst. left. reflexivity. - destruct (IHx1 t1); subst; nodec. destruct (IHx2 t2); subst; nodec. destruct (eq_dec u u0); nodec; subst. diff --git a/template-coq/theories/TermEquality.v b/template-coq/theories/TermEquality.v index a6cb5f424..d37bd614c 100644 --- a/template-coq/theories/TermEquality.v +++ b/template-coq/theories/TermEquality.v @@ -296,6 +296,7 @@ Inductive eq_term_upto_univ_napp Σ | eq_Int i : eq_term_upto_univ_napp Σ cmp_universe cmp_sort pb napp (tInt i) (tInt i) | eq_Float f : eq_term_upto_univ_napp Σ cmp_universe cmp_sort pb napp (tFloat f) (tFloat f) +| eq_String s : eq_term_upto_univ_napp Σ cmp_universe cmp_sort pb napp (tString s) (tString s) | eq_Array u u' arr arr' def def' ty ty' : cmp_universe_instance (cmp_universe Conv) [u] [u'] -> All2 (eq_term_upto_univ_napp Σ cmp_universe cmp_sort Conv 0) arr arr' -> diff --git a/template-coq/theories/Typing.v b/template-coq/theories/Typing.v index 24a8e6682..055c2f289 100644 --- a/template-coq/theories/Typing.v +++ b/template-coq/theories/Typing.v @@ -879,6 +879,13 @@ Inductive typing `{checker_flags} (Σ : global_env_ext) (Γ : context) : term -> primitive_invariants primFloat cdecl -> Σ ;;; Γ |- tFloat p : tConst prim_ty [] +| type_String p prim_ty cdecl : + wf_local Σ Γ -> + primitive_constant Σ primString = Some prim_ty -> + declared_constant Σ prim_ty cdecl -> + primitive_invariants primString cdecl -> + Σ ;;; Γ |- tString p : tConst prim_ty [] + | type_Array prim_ty cdecl u arr def ty : wf_local Σ Γ -> primitive_constant Σ primArray = Some prim_ty -> @@ -1009,6 +1016,7 @@ Proof. (all_size (on_def_body (lift_typing typing _) _ _) (fun x p => on_def_body_size (typing_size Σ) _ _ _ p) a1))). - exact (S (All_local_env_size (typing_size _) _ a)). - exact (S (All_local_env_size (typing_size _) _ a)). + - exact (S (All_local_env_size (typing_size _) _ a)). - exact (S (Nat.max (All_local_env_size (typing_size _) _ a) (Nat.max d2 (Nat.max d3 (all_size _ (fun t p => typing_size Σ Γ t ty p) a0))))). Defined. @@ -1285,6 +1293,13 @@ Lemma typing_ind_env `{cf : checker_flags} : primitive_invariants primFloat cdecl -> P Σ Γ (tFloat p) (tConst prim_ty [])) -> + (forall Σ (wfΣ : wf Σ) (Γ : context) (wfΓ : wf_local Σ Γ) p prim_ty cdecl, + PΓ Σ Γ wfΓ -> + primitive_constant Σ primString = Some prim_ty -> + declared_constant Σ prim_ty cdecl -> + primitive_invariants primString cdecl -> + P Σ Γ (tString p) (tConst prim_ty [])) -> + (forall Σ (wfΣ : wf Σ) (Γ : context) (wfΓ : wf_local Σ Γ) u arr def ty prim_ty cdecl, PΓ Σ Γ wfΓ -> primitive_constant Σ primArray = Some prim_ty -> @@ -1311,7 +1326,7 @@ Lemma typing_ind_env `{cf : checker_flags} : Proof. intros P Pj Pdecl PΓ; unfold env_prop. intros Xj XΓ. - intros X X0 Xcast X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 Xint Xfloat Xarr X12 Σ wfΣ Γ wfΓ t T H. + intros X X0 Xcast X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 Xint Xfloat Xstring Xarr X12 Σ wfΣ Γ wfΓ t T H. (* NOTE (Danil): while porting to 8.9, I had to split original "pose" into 2 pieces, otherwise it takes forever to execure the "pose", for some reason *) pose (@Fix_F ({ Σ : global_env_ext & { wfΣ : wf Σ & { Γ & { t & { T & Σ ;;; Γ |- t : T }}}}})) as p0. diff --git a/template-coq/theories/WfAst.v b/template-coq/theories/WfAst.v index cf6739816..d2a757eed 100644 --- a/template-coq/theories/WfAst.v +++ b/template-coq/theories/WfAst.v @@ -58,6 +58,7 @@ Inductive wf {Σ} : term -> Type := | wf_tCoFix mfix k : All (fun def => wf def.(dtype) × wf def.(dbody)) mfix -> wf (tCoFix mfix k) | wf_tInt i : wf (tInt i) | wf_tFloat f : wf (tFloat f) +| wf_tString s : wf (tString s) | wf_tArray u arr def ty : All wf arr -> wf def -> wf ty -> wf (tArray u arr def ty). Arguments wf : clear implicits. Derive Signature for wf. @@ -67,7 +68,7 @@ Derive Signature for wf. Definition wf_Inv Σ (t : term) : Type := match t with | tRel _ | tVar _ | tSort _ => unit - | tInt _ | tFloat _ => unit + | tInt _ | tFloat _ | tString _ => unit | tArray u arr def ty => All (wf Σ) arr * wf Σ def * wf Σ ty | tEvar n l => All (wf Σ) l | tCast t k t' => wf Σ t * wf Σ t' @@ -152,10 +153,11 @@ Lemma term_wf_forall_list_ind Σ : (forall (m : mfixpoint term) (n : nat), tFixProp P P m -> P (tCoFix m n)) -> (forall i, P (tInt i)) -> (forall f, P (tFloat f)) -> + (forall s, P (tString s)) -> (forall u arr def ty, All P arr -> P def -> P ty -> P (tArray u arr def ty)) -> forall t : term, wf Σ t -> P t. Proof. - intros P H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H15 H16 H17 H18 H19 Harr. + intros P H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H15 H16 H17 H18 H19 H20 Harr. intros until t. revert t. apply (term_forall_list_rect (fun t => wf Σ t -> P t)); intros; try solve [match goal with diff --git a/template-pcuic/theories/PCUICToTemplate.v b/template-pcuic/theories/PCUICToTemplate.v index a1f4d1933..f97a7ffda 100644 --- a/template-pcuic/theories/PCUICToTemplate.v +++ b/template-pcuic/theories/PCUICToTemplate.v @@ -17,6 +17,7 @@ Definition trans_prim (trans : PCUICAst.term -> Ast.term) (t : prim_val) : Ast.t match t.π2 with | primIntModel i => Ast.tInt i | primFloatModel f => Ast.tFloat f + | primStringModel s => Ast.tString s | primArrayModel a => Ast.tArray (array_level a) (map trans (array_value a)) (trans (array_default a)) (trans (array_type a)) end. diff --git a/template-pcuic/theories/PCUICToTemplateCorrectness.v b/template-pcuic/theories/PCUICToTemplateCorrectness.v index fcbbf40bd..cbcdb506f 100644 --- a/template-pcuic/theories/PCUICToTemplateCorrectness.v +++ b/template-pcuic/theories/PCUICToTemplateCorrectness.v @@ -2364,13 +2364,12 @@ Proof. + fold trans;subst types. now apply trans_mfix_All2. + now rewrite trans_wf_cofixpoint. - - cbn. destruct p as [? []]; simp prim_type; cbn; econstructor; eauto. - 1,3,5: eapply trans_declared_constant; tea. + - destruct p as [? []]; simp prim_type; cbn; econstructor; eauto. + 1,3,5,7: eapply trans_declared_constant; tea. all:cbn in *. all:move: H1; rewrite /Ast.Env.primitive_invariants /primitive_invariants. - 1-2:intros []; split => //; + all: try by intros []; split => //; destruct cdecl as [ty [?|] ?]; cbn in *; subst; auto => //. - intros []; split => //. rewrite H1 //. rewrite H2 //. all:depelim X1; eauto. intros _. solve_all. - eapply TT.type_Conv. + eassumption. diff --git a/template-pcuic/theories/TemplateMonadToPCUIC.v b/template-pcuic/theories/TemplateMonadToPCUIC.v index ecf5d6711..fedee03ed 100644 --- a/template-pcuic/theories/TemplateMonadToPCUIC.v +++ b/template-pcuic/theories/TemplateMonadToPCUIC.v @@ -163,6 +163,7 @@ Section with_tc. ret (tCoFix mfix' idx) | Ast.tInt n => ret (tPrim (primInt; primIntModel n)) | Ast.tFloat n => ret (tPrim (primFloat; primFloatModel n)) + | Ast.tString n => ret (tPrim (primString; primStringModel n)) | Ast.tArray l v d ty => v' <- monad_map@{t u t t} monad_trans' v ;; d' <- monad_trans' d ;; diff --git a/template-pcuic/theories/TemplateToPCUIC.v b/template-pcuic/theories/TemplateToPCUIC.v index 7df5f442f..f7ec265c8 100644 --- a/template-pcuic/theories/TemplateToPCUIC.v +++ b/template-pcuic/theories/TemplateToPCUIC.v @@ -103,6 +103,7 @@ Section Trans. tCoFix mfix' idx | Ast.tInt n => tPrim (primInt; primIntModel n) | Ast.tFloat n => tPrim (primFloat; primFloatModel n) + | Ast.tString n => tPrim (primString; primStringModel n) | Ast.tArray l v d ty => tPrim (primArray; primArrayModel {| array_level := l; array_value := List.map trans v; diff --git a/template-pcuic/theories/TemplateToPCUICCorrectness.v b/template-pcuic/theories/TemplateToPCUICCorrectness.v index 00c3e3bd9..8bd267daf 100644 --- a/template-pcuic/theories/TemplateToPCUICCorrectness.v +++ b/template-pcuic/theories/TemplateToPCUICCorrectness.v @@ -383,6 +383,7 @@ Proof. - f_equal; auto; solve_all. - f_equal; auto. - f_equal; auto. + - f_equal; auto. - cbn; do 4 f_equal; auto. rewrite /map_array_model. f_equal; eauto. cbn. solve_all. Qed. @@ -443,6 +444,7 @@ Proof. - f_equal; auto; solve_list. - f_equal; auto. - f_equal; auto. + - f_equal; auto. - cbn; f_equal; auto. rewrite /map_array_model; cbn; do 3 f_equal; eauto. solve_all. Qed. @@ -482,6 +484,7 @@ Proof. - rewrite /id /map_predicate /=. f_equal; solve_all. - f_equal; auto. - f_equal; auto. + - f_equal; auto. - cbn. rewrite /mapu_array_model; cbn; do 4 f_equal; auto; solve_all. Qed. @@ -2489,6 +2492,14 @@ Proof. intros []; split => //; destruct cdecl as [ty [?|] ?]; cbn in *; subst; auto => //. + constructor. + - cbn. replace (tConst prim_ty []) with (prim_type (primString; primStringModel p) prim_ty) by now simp prim_type. + econstructor; cbn; eauto. + + rewrite trans_env_retroknowledge //. + + now apply forall_decls_declared_constant. + + move: H1; rewrite /Ast.Env.primitive_invariants /primitive_invariants. + intros []; split => //; + destruct cdecl as [ty [?|] ?]; cbn in *; subst; auto => //. + + constructor. - cbn. set (a := {| array_level := _ |}). replace (tApp (tConst prim_ty [u]) (trans (trans_global_env Σ.1) ty)) with (prim_type (primArray; primArrayModel a) prim_ty) by now simp prim_type. econstructor; cbn; eauto. diff --git a/template-pcuic/theories/TemplateToPCUICExpanded.v b/template-pcuic/theories/TemplateToPCUICExpanded.v index 1e5443085..402aff766 100644 --- a/template-pcuic/theories/TemplateToPCUICExpanded.v +++ b/template-pcuic/theories/TemplateToPCUICExpanded.v @@ -237,6 +237,7 @@ Proof with eauto using expanded. eapply expanded_tConstruct_app. eauto. cbn. unfold trans_local. now rewrite length_map context_assumptions_map. solve_all. - repeat constructor. - repeat constructor. + - repeat constructor. - wf_inv wf [[] ?]. repeat cbn; constructor. constructor; cbn; eauto. solve_all. Qed. diff --git a/utils/theories/Show.v b/utils/theories/Show.v index 9f3f38704..1c5d5dca5 100644 --- a/utils/theories/Show.v +++ b/utils/theories/Show.v @@ -1,4 +1,4 @@ -From Coq Require Import PArith Sint63 String Uint63 PrimFloat SpecFloat FloatOps. +From Coq Require Import PArith Sint63 String Uint63 PrimFloat SpecFloat FloatOps PString. From MetaCoq.Utils Require Import bytestring MCString. Local Open Scope bs_scope. @@ -56,9 +56,22 @@ Definition string_of_prim_int (i:Uint63.int) : string := Definition string_of_float (f : PrimFloat.float) : string := string_of_specfloat (FloatOps.Prim2SF f). +Definition char63_to_string (c : PrimString.char63) : string := + let b := + match Byte.of_N (BinInt.Z.to_N (Uint63.to_Z c)) with + | None => Byte.x00 + | Some b => b + end + in + String.String b String.EmptyString. + +Definition string_of_pstring (s : PrimString.string) : string := + string_of_list char63_to_string (PString.to_list s). + #[export] Instance show_uint : Show PrimInt63.int := string_of_prim_int. #[export] Instance show_sint : Show int_wrapper := { show x := string_of_Z (Sint63.to_Z (x.(int_wrap))) }. #[export] Instance show_specfloat : Show SpecFloat.spec_float := string_of_specfloat. #[export] Instance show_float : Show PrimFloat.float := string_of_float. #[export] Instance show_positive : Show positive := string_of_positive. #[export] Instance show_Z : Show Z := string_of_Z. +#[export] Instance show_pstring : Show PrimString.string := string_of_pstring.