Add primitive string types.

checker/values.ml

@@ -158,6 +158,7 @@ let rec v_constr =
     [|v_proj;v_relevance;v_constr|]; (* Proj *)
     [|v_uint63|]; (* Int *)
     [|Float64|]; (* Float *)
+    [|String|]; (* String *)
     [|v_instance;Array v_constr;v_constr;v_constr|] (* Array *)
   |])
 
@@ -240,7 +241,7 @@ let v_template_universes =
   v_tuple "template_universes" [|List(Opt v_level);v_context_set|]
 
 let v_primitive =
-  v_enum "primitive" 55 (* Number of constructors of the CPrimitives.t type *)
+  v_enum "primitive" 63 (* Number of constructors of the CPrimitives.t type *)
 
 let v_cst_def =
   v_sum "constant_def" 0
@@ -378,7 +379,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
 let v_prim_ind = v_enum "prim_ind" 6
 (* Number of "Register ... as kernel.ind_..." in PrimInt63.v and PrimFloat.v *)
 
-let v_prim_type = v_enum "prim_type" 3
+let v_prim_type = v_enum "prim_type" 4
 (* Number of constructors of prim_type in "kernel/cPrimitives.ml" *)
 
 let v_retro_action =

dev/top_printers.ml

@@ -368,6 +368,8 @@ let constr_display csr =
       "Int("^(Uint63.to_string i)^")"
   | Float f ->
       "Float("^(Float64.to_string f)^")"
+  | String s ->
+      Printf.sprintf "String(%S)" s
   | Array (u,t,def,ty) -> "Array("^(array_display t)^","^(term_display def)^","^(term_display ty)^")@{" ^universes_display u^"\n"
 
   and array_display v =
@@ -527,6 +529,8 @@ let print_pure_constr csr =
      print_string ("Int("^(Uint63.to_string i)^")")
   | Float f ->
       print_string ("Float("^(Float64.to_string f)^")")
+  | String s ->
+      print_string (Printf.sprintf "String(%S)" s)
   | Array (u,t,def,ty) ->
       print_string "Array(";
       Array.iter (fun x -> box_display x; print_space()) t;

dev/vm_printers.ml

@@ -78,6 +78,7 @@ and ppwhd whd =
   | Vblock b -> ppvblock b
   | Vint64 i -> printf "int64(%LiL)" i
   | Vfloat64 f -> printf "float64(%.17g)" f
+  | Vstring s -> printf "string(%S)" s
   | Varray t -> ppvarray t
   | Vaccu (a, s) ->
       open_hbox();ppatom a;close_box();

doc/stdlib/index-list.html.template

@@ -714,4 +714,11 @@ through the <tt>Require Import</tt> command.</p>
   <dd>
     theories/Array/PArray.v
   </dd>
+
+  <dt> <b>Primitive strings</b>
+    Native string type
+  </dt>
+  <dd>
+    theories/Strings/PString.v
+  </dd>
 </dl>

engine/eConstr.ml

@@ -122,6 +122,7 @@ let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2))
 let mkArrowR t1 t2 = mkArrow t1 ERelevance.relevant t2
 let mkInt i = of_kind (Int i)
 let mkFloat f = of_kind (Float f)
+let mkString s = of_kind (String s)
 let mkArray (u,t,def,ty) = of_kind (Array (u,t,def,ty))
 
 let mkRef (gr,u) = let open GlobRef in match gr with
@@ -561,7 +562,7 @@ let iter_with_full_binders env sigma g f n c =
   let open Context.Rel.Declaration in
   match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _ | Float _) -> ()
+    | Construct _ | Int _ | Float _ | String _) -> ()
   | Cast (c,_,t) -> f n c; f n t
   | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
@@ -800,7 +801,7 @@ let fold_constr_relevance sigma f acc c =
   | Rel _ | Var _ | Meta _ | Evar _
   |  Sort _ | Cast _ | App _
   | Const _ | Ind _ | Construct _ | Proj _
-  | Int _ | Float _ | Array _ -> acc
+  | Int _ | Float _ | String _ | Array _ -> acc
 
   | Prod (na,_,_) | Lambda (na,_,_) | LetIn (na,_,_,_) ->
     fold_annot_relevance f acc na
@@ -1144,7 +1145,7 @@ let kind_of_type sigma t = match kind sigma t with
   | (Rel _ | Meta _ | Var _ | Evar _ | Const _
   | Proj _ | Case _ | Fix _ | CoFix _ | Ind _)
     -> AtomicType (t,[||])
-  | (Lambda _ | Construct _ | Int _ | Float _ | Array _) -> failwith "Not a type"
+  | (Lambda _ | Construct _ | Int _ | Float _ | String _ | Array _) -> failwith "Not a type"
 
 module Unsafe =
 struct

engine/eConstr.mli

@@ -183,6 +183,7 @@ val mkArrow : t -> ERelevance.t  -> t -> t
 val mkArrowR : t -> t -> t
 val mkInt : Uint63.t -> t
 val mkFloat : Float64.t -> t
+val mkString : String.t -> t
 val mkArray : EInstance.t * t array * t * t -> t
 
 module UnsafeMonomorphic : sig

engine/namegen.ml

@@ -123,7 +123,8 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
         Some (Nametab.basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
         Some (match lna.(i).binder_name with Name id -> id | _ -> assert false)
-    | Sort _ | Rel _ | Meta _|Evar _|Case _ | Int _ | Float _ | Array _ -> None
+    | Sort _ | Rel _ | Meta _ | Evar _ | Case _
+    | Int _ | Float _ | String _ | Array _ -> None
   in
   hdrec c
 
@@ -171,6 +172,7 @@ let hdchar env sigma c =
     | Meta _ | Case _ -> "y"
     | Int _ -> "i"
     | Float _ -> "f"
+    | String _ -> "s"
     | Array _ -> "a"
   in
   hdrec 0 c

engine/termops.ml

@@ -608,7 +608,7 @@ let map_constr_with_binders_left_to_right env sigma g f l c =
   let open EConstr in
   match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _ | Float _) -> c
+    | Construct _ | Int _ | Float _ | String _) -> c
   | Cast (b,k,t) ->
     let b' = f l b in
     let t' = f l t in
@@ -684,7 +684,7 @@ let map_constr_with_full_binders env sigma g f l cstr =
   let open EConstr in
   match EConstr.kind sigma cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _ | Float _) -> cstr
+    | Construct _ | Int _ | Float _ | String _) -> cstr
   | Cast (c,k, t) ->
       let c' = f l c in
       let t' = f l t in
@@ -756,7 +756,7 @@ let fold_constr_with_full_binders env sigma g f n acc c =
   let open EConstr.Vars in
   let open Context.Rel.Declaration in
   match EConstr.kind sigma c with
-  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _  | Int _ | Float _ -> acc
+  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _  | Int _ | Float _ | String _ -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
   | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
   | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c

interp/constrextern.ml

@@ -1118,6 +1118,11 @@ let rec extern inctx scopes vars r =
 
   | GFloat f -> extern_float f (snd scopes)
 
+  | GString s ->
+     extern_prim_token_delimiter_if_required
+       (String s)
+       "pstring" "pstring_scope" (snd scopes)
+
   | GArray(u,t,def,ty) ->
     CArray(extern_instance (snd vars) u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty)
 
@@ -1550,6 +1555,7 @@ let rec glob_of_pat
   | PSort (Sorts.InType | Sorts.InQSort) -> GSort (UAnonymous {rigid=UnivRigid})
   | PInt i -> GInt i
   | PFloat f -> GFloat f
+  | PString s -> GString s
   | PArray(t,def,ty) ->
     let glob_of = glob_of_pat avoid env sigma in
     GArray (None, Array.map glob_of t, glob_of def, glob_of ty)

interp/constrintern.ml

@@ -873,7 +873,7 @@ let rec adjust_env env = function
   | NCast (c,_,_) -> adjust_env env c
   | NApp _ -> restart_no_binders env
   | NVar _ | NRef _ | NHole _ | NGenarg _ | NCases _ | NLetTuple _ | NIf _
-  | NRec _ | NSort _ | NProj _ | NInt _ | NFloat _ | NArray _
+  | NRec _ | NSort _ | NProj _ | NInt _ | NFloat _ | NString _ | NArray _
   | NList _ | NBinderList _ -> env (* to be safe, but restart should be ok *)
 
 let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =

interp/impargs.ml

@@ -247,7 +247,7 @@ let rec is_rigid_head sigma t = match kind sigma t with
         | Fix ((fi,i),_) -> is_rigid_head sigma (args.(fi.(i)))
         | _ -> is_rigid_head sigma f)
   | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
-  | Prod _ | Meta _ | Cast _ | Int _ | Float _ | Array _ -> assert false
+  | Prod _ | Meta _ | Cast _ | Int _ | Float _ | String _ | Array _ -> assert false
 
 let is_rigid env sigma t =
   let open Context.Rel.Declaration in

interp/notation.ml

@@ -408,6 +408,8 @@ type target_kind =
 type string_target_kind =
   | ListByte
   | Byte
+  | PString
+  | IntCharCode
 
 type option_kind = Option | Direct
 type 'target conversion_kind = 'target * option_kind
@@ -448,6 +450,7 @@ type 'a token_kind =
 | TConstruct of constructor * 'a list
 | TInt of Uint63.t
 | TFloat of Float64.t
+| TString of String.t
 | TArray of 'a array * 'a * 'a
 | TOther
 
@@ -472,6 +475,7 @@ let kind c =
   | Construct (c, _) -> TConstruct (c, args)
   | Int i -> TInt i
   | Float f -> TFloat f
+  | String s -> TString s
   | Array (_, t, u, v) -> TArray (t, u, v)
   | Rel _ | Meta _ | Evar _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
   | Proj _ | Case _ | Fix _ | CoFix _ -> TOther
@@ -676,6 +680,7 @@ let rec glob_of_token token_kind ?loc env sigma c = match TokenValue.kind c with
     mkGApp ?loc ce cel
   | TInt i -> DAst.make ?loc (Glob_term.GInt i)
   | TFloat f -> DAst.make ?loc (Glob_term.GFloat f)
+  | TString s -> DAst.make ?loc (Glob_term.GString s)
   | TArray (t,def,ty) ->
     let def' = glob_of_token token_kind ?loc env sigma def
     and t' = Array.map (glob_of_token token_kind ?loc env sigma) t
@@ -1112,20 +1117,32 @@ let locate_byte () = unsafe_locate_ind (q_byte ())
 let coqbyte_of_char_code esig byte c =
   mkConstruct esig (byte, 1 + c)
 
+let char_of_string ?loc s =
+  let len = String.length s in
+  if Int.equal len 1 then s.[0] else
+  let n =
+    if Int.equal len 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
+    then int_of_string s else 256
+  in
+  if n < 256 then Char.chr n else
+  user_err ?loc (str "Expects a single character or a three-digit ASCII code.")
+
 let coqbyte_of_string ?loc esig byte s =
-  let p =
-    if Int.equal (String.length s) 1 then int_of_char s.[0]
-    else
-      let n =
-        if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
-        then int_of_string s else 256 in
-      if n < 256 then n else
-       user_err ?loc
-         (str "Expects a single character or a three-digit ASCII code.") in
+  let p = Char.code (char_of_string ?loc s) in
   coqbyte_of_char_code esig byte p
 
 let coqbyte_of_char esig byte c = coqbyte_of_char_code esig byte (Char.code c)
 
+let pstring_of_string ?loc s =
+  if String.length s > Pstring.max_length_int then
+    user_err ?loc (str "String literal would be too large on a 32-bits system.")
+  else
+    Constr.mkString s
+
+let intcharcode_of_string ?loc s =
+  let c = char_of_string ?loc s in
+  Constr.mkInt (Uint63.of_int (Char.code c))
+
 let make_ascii_string n =
   if n>=32 && n<=126 then String.make 1 (char_of_int n)
   else Printf.sprintf "%03d" n
@@ -1136,6 +1153,17 @@ let char_code_of_coqbyte c = match TokenValue.kind c with
 
 let string_of_coqbyte c = make_ascii_string (char_code_of_coqbyte c)
 
+let string_of_pstring c =
+  match TokenValue.kind c with
+  | TString s -> s
+  | _ -> raise NotAValidPrimToken
+
+let string_of_intcharcode c =
+  match TokenValue.kind c with
+  | TInt i when Uint63.lt i (Uint63.of_int 256) ->
+      String.make 1 (Char.chr (Uint63.to_int_min i 256))
+  | _ -> raise NotAValidPrimToken
+
 let coqlist_byte_of_string esig byte_ty list_ty str =
   let cbyte = mkInd esig byte_ty in
   let nil = mkApp (mkConstruct esig (list_ty, 1), [|cbyte|]) in
@@ -1171,6 +1199,8 @@ let interp o ?loc n =
   let c = match fst o.to_kind with
     | ListByte -> coqlist_byte_of_string esig byte_ty list_ty n
     | Byte -> coqbyte_of_string ?loc esig byte_ty n
+    | PString -> pstring_of_string ?loc n
+    | IntCharCode -> intcharcode_of_string ?loc n
   in
   let sigma = !sigma in
   let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in
@@ -1185,6 +1215,8 @@ let uninterp o n =
     begin function
       | (ListByte, c) -> string_of_coqlist_byte c
       | (Byte, c) -> string_of_coqbyte c
+      | (PString, c) -> string_of_pstring c
+      | (IntCharCode, c) -> string_of_intcharcode c
     end o n
 end
 

interp/notation.mli

@@ -152,6 +152,8 @@ type target_kind =
 type string_target_kind =
   | ListByte
   | Byte
+  | PString
+  | IntCharCode
 
 type option_kind = Option | Direct
 type 'target conversion_kind = 'target * option_kind

interp/notation_ops.ml

@@ -263,7 +263,7 @@ let compare_notation_constr lt var_eq_hole (vars1,vars2) t1 t2 =
     aux vars renaming ty1 ty2
   | (NRef _ | NVar _ | NApp _ | NProj _ | NHole _ | NGenarg _ | NList _ | NLambda _ | NProd _
     | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
-    | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> raise_notrace Exit in
+    | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NString _ | NArray _), _ -> raise_notrace Exit in
   try
     let _ = aux (vars1,vars2) [] t1 t2 in
     if not lt then
@@ -468,6 +468,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
   | NRef (x,u) -> GRef (x,u)
   | NInt i -> GInt i
   | NFloat f -> GFloat f
+  | NString s -> GString s
   | NArray (t,def,ty) -> GArray(None, Array.map (f e) t, f e def, f e ty)
 
 let glob_constr_of_notation_constr ?loc x =
@@ -703,6 +704,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
   | GSort s -> NSort s
   | GInt i -> NInt i
   | GFloat f -> NFloat f
+  | GString s -> NString s
   | GHole w -> NHole w
   | GGenarg arg -> forgetful := { !forgetful with forget_ltac = true }; NGenarg arg
   | GRef (r,u) -> NRef (r,u)
@@ -909,6 +911,7 @@ let rec subst_notation_constr subst bound raw =
   | NSort _ -> raw
   | NInt _ -> raw
   | NFloat _ -> raw
+  | NString _ -> raw
 
   | NHole knd ->
     let nknd = match knd with
@@ -1572,6 +1575,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma
   | GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma
   | GFloat f1, NFloat f2 when Float64.equal f1 f2 -> sigma
+  | GString s1, NString s2 when String.equal s1 s2 -> sigma
   | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
   | a, NHole _ -> sigma
 
@@ -1606,7 +1610,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
 
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GProj _ | GLambda _ | GProd _
      | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GGenarg _
-     | GCast _ | GInt _ | GFloat _ | GArray _), _ -> raise No_match
+     | GCast _ | GInt _ | GFloat _ | GString _ | GArray _), _ -> raise No_match
 
 and match_in_type u alp metas sigma t = function
   | None -> sigma

interp/notation_term.mli

@@ -47,6 +47,7 @@ type notation_constr =
   | NCast of notation_constr * Constr.cast_kind option * notation_constr
   | NInt of Uint63.t
   | NFloat of Float64.t
+  | NString of String.t
   | NArray of notation_constr array * notation_constr * notation_constr
 
 (** Note concerning NList: first constr is iterator, second is terminator;

kernel/byterun/coq_interp.c

@@ -1964,6 +1964,26 @@ value coq_interprete
         Next;
       }
 
+      Instruct(CHECKCAMLCALL3) {
+        // arity-3 callback, no argument can be an accumulator
+        value arg1;
+        value arg2;
+        print_instr("CHECKCAMLCALL3");
+        if (!Is_accu(accu) && !Is_accu(sp[0]) && !Is_accu(sp[1])) {
+          pc++;
+          arg1 = sp[0];
+          arg2 = sp[1];
+          Setup_for_caml_call;
+          print_int(*pc);
+          accu = caml_callback3_exn(Field(coq_global_data, *pc), accu, arg1, arg2);
+          Restore_after_caml_call;
+          Handle_potential_exception(accu);
+          sp += 2;
+          pc++;
+        } else pc += *pc;
+        Next;
+      }
+
       Instruct(CHECKCAMLCALL3_1) {
         // arity-3 callback, the last argument can be an accumulator
         value arg1;