Merge pull request #1088 from rlepigre/br/prim-string

Adapt to coq/coq#18973.

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_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 =>

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.

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.
+Qed.

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.
+  end.

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 *.

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.*)
+End TermSpineView.*)

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.
 

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.compare_eq in Hcmp.
+    - intros Heq%PString.compare_eq. rewrite Heq in Hcmp. inversion Hcmp.
+    - intros Heq%PString.compare_eq. 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,18 +135,15 @@ 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]
@@ -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.

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.

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