Adapt to coq/coq#18973.

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

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

template-coq/gen-src/metacoq_template_plugin.mlpack

@@ -74,6 +74,8 @@ Zpower
 SpecFloat
 PrimFloat
 FloatOps
+PrimString
+PString
 MCString
 Sint63
 Show

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 =

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 =
@@ -376,7 +380,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 ! *)

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)

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 |])
 

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

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

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
@@ -359,6 +361,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

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
 

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
 

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)

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

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

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,14 +364,15 @@ 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 ->
   P Γ ty ->
   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.

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

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.

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.

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.

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' ->