Add primitive [char] and [string] types.

checker/validate.ml

@@ -66,6 +66,10 @@ let is_int _mem o = match o with
 | Int _ -> true
 | Fun _ | Ptr _ | Atm _ -> false
 
+let is_char _mem o = match o with
+| Int i when 0 <= i && i < 256 -> true
+| Int _ | Fun _ | Ptr _ | Atm _ -> false
+
 let is_int64 mem o = match o with
 | Int _ | Fun _ | Atm _ -> false
 | Ptr p ->
@@ -147,6 +151,7 @@ let rec val_gen v mem ctx o = match v with
   | Proxy { contents = v } -> val_gen v mem ctx o
   | Int64 -> val_int64 mem ctx o
   | Float64 -> val_float64 mem ctx o
+  | Char -> if not (is_char mem o) then fail mem ctx o "expected a char"
 
 (* Check that an object is a tuple (or a record). vs is an array of
    value representation for each field. Its size corresponds to the

checker/values.ml

@@ -36,6 +36,7 @@ type value =
   | Proxy of value ref
   | Int64
   | Float64
+  | Char
 
 let fix (f : value -> value) : value =
   let self = ref Any in
@@ -158,6 +159,8 @@ let rec v_constr =
     [|v_proj;v_relevance;v_constr|]; (* Proj *)
     [|v_uint63|]; (* Int *)
     [|Float64|]; (* Float *)
+    [|Char|]; (* Char *)
+    [|String|]; (* String *)
     [|v_instance;Array v_constr;v_constr;v_constr|] (* Array *)
   |])
 
@@ -240,7 +243,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" 65 (* Number of constructors of the CPrimitives.t type *)
 
 let v_cst_def =
   v_sum "constant_def" 0
@@ -380,7 +383,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" 5
 (* Number of constructors of prim_type in "kernel/cPrimitives.ml" *)
 
 let v_retro_action =

checker/values.mli

@@ -40,6 +40,7 @@ type value =
 
   | Int64
   | Float64
+  | Char
 
 (** NB: List and Opt have their own constructors to make it easy to
    define eg [let rec foo = List foo]. *)

checker/votour.ml

@@ -180,6 +180,7 @@ let rec get_name ?(extra=false) = function
   | Proxy v -> get_name ~extra !v
   | Int64 -> "Int64"
   | Float64 -> "Float64"
+  | Char -> "Char"
 
 (** For tuples, its quite handy to display the inner 1st string (if any).
     Cf. [structure_body] for instance *)
@@ -286,6 +287,7 @@ let rec get_children v o pos = match v with
   | Proxy v -> get_children !v o pos
   | Int64 -> raise_notrace Exit
   | Float64 -> raise_notrace Exit
+  | Char -> raise_notrace Exit
 
 let get_children v o pos =
   try get_children v o pos

dev/top_printers.ml

@@ -368,6 +368,10 @@ let constr_display csr =
       "Int("^(Uint63.to_string i)^")"
   | Float f ->
       "Float("^(Float64.to_string f)^")"
+  | Char c ->
+      Printf.sprintf "Char(%C)" c
+  | String s ->
+      Printf.sprintf "Char(%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 +531,10 @@ let print_pure_constr csr =
      print_string ("Int("^(Uint63.to_string i)^")")
   | Float f ->
       print_string ("Float("^(Float64.to_string f)^")")
+  | Char c ->
+      print_string (Printf.sprintf "Char(%C)" c)
+  | 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;

doc/stdlib/index-list.html.template

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

engine/eConstr.ml

@@ -122,6 +122,8 @@ 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 mkChar c = of_kind (Char c)
+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 +563,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 _ | Char _ | 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 +802,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 _ | Char _ | String _ | Array _ -> acc
 
   | Prod (na,_,_) | Lambda (na,_,_) | LetIn (na,_,_,_) ->
     fold_annot_relevance f acc na
@@ -1144,7 +1146,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 _ | Char _ | String _ | Array _) -> failwith "Not a type"
 
 module Unsafe =
 struct

engine/eConstr.mli

@@ -183,6 +183,8 @@ val mkArrow : t -> ERelevance.t  -> t -> t
 val mkArrowR : t -> t -> t
 val mkInt : Uint63.t -> t
 val mkFloat : Float64.t -> t
+val mkChar : Char.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 _ | Char _ | String _ | Array _ -> None
   in
   hdrec c
 
@@ -171,6 +172,8 @@ let hdchar env sigma c =
     | Meta _ | Case _ -> "y"
     | Int _ -> "i"
     | Float _ -> "f"
+    | Char _ -> "c"
+    | 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 _ | Char _ | 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 _ | Char _ | 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 _ | Char _ | 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,16 @@ let rec extern inctx scopes vars r =
 
   | GFloat f -> extern_float f (snd scopes)
 
+  | GChar c ->
+     extern_prim_token_delimiter_if_required
+       (String (String.make 1 c))
+       "pchar" "pchar_scope" (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 +1560,8 @@ let rec glob_of_pat
   | PSort (Sorts.InType | Sorts.InQSort) -> GSort (UAnonymous {rigid=UnivRigid})
   | PInt i -> GInt i
   | PFloat f -> GFloat f
+  | PChar c -> GChar c
+  | 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 _ | NChar _ | 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 _ | Char _ | String _ | Array _ -> assert false
 
 let is_rigid env sigma t =
   let open Context.Rel.Declaration in

interp/notation.ml

@@ -448,6 +448,8 @@ type 'a token_kind =
 | TConstruct of constructor * 'a list
 | TInt of Uint63.t
 | TFloat of Float64.t
+| TChar of Char.t
+| TString of String.t
 | TArray of 'a array * 'a * 'a
 | TOther
 
@@ -472,6 +474,8 @@ let kind c =
   | Construct (c, _) -> TConstruct (c, args)
   | Int i -> TInt i
   | Float f -> TFloat f
+  | Char c -> TChar c
+  | 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,8 @@ 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)
+  | TChar c -> DAst.make ?loc (Glob_term.GChar c)
+  | 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

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 _ | NChar _ | NString _ | NArray _), _ -> raise_notrace Exit in
   try
     let _ = aux (vars1,vars2) [] t1 t2 in
     if not lt then
@@ -468,6 +468,8 @@ 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
+  | NChar c -> GChar c
+  | 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 +705,8 @@ let notation_constr_and_vars_of_glob_constr recvars a =
   | GSort s -> NSort s
   | GInt i -> NInt i
   | GFloat f -> NFloat f
+  | GChar c -> NChar c
+  | 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 +913,8 @@ let rec subst_notation_constr subst bound raw =
   | NSort _ -> raw
   | NInt _ -> raw
   | NFloat _ -> raw
+  | NChar _ -> raw
+  | NString _ -> raw
 
   | NHole knd ->
     let nknd = match knd with
@@ -1572,6 +1578,8 @@ 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
+  | GChar c1, NChar c2 when Char.equal c1 c2 -> 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 +1614,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 _ | GChar _ | GString _ | GArray _), _ -> raise No_match
 
 and match_in_type u alp metas sigma t = function
   | None -> sigma

interp/notation_term.mli

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