VM/native: primitive strings can be included in values

cf https://coq.zulipchat.com/#narrow/channel/237656-Coq-devs-.26-plugin-devs/topic/VM.20bytecode.20size.20of.20Primitive.20String.20Literals

kernel/nativelambda.ml

@@ -21,7 +21,7 @@ type lambda = Nativevalues.t Genlambda.lambda
 
 let is_value lc =
   match lc with
-  | Lval _ | Lint _ | Luint _ | Lfloat _ -> true
+  | Lval _ | Lint _ | Luint _ | Lfloat _ | Lstring _ -> true
   | _ -> false
 
 let get_value lc =
@@ -30,6 +30,7 @@ let get_value lc =
   | Lint tag -> Nativevalues.mk_int tag
   | Luint i -> Nativevalues.mk_uint i
   | Lfloat f -> Nativevalues.mk_float f
+  | Lstring s -> Nativevalues.mk_string s
   | _ -> raise Not_found
 
 let as_value tag args =

kernel/vmlambda.ml

@@ -16,7 +16,7 @@ let get_lval (_, v) = v
 
 let is_value lc =
   match lc with
-  | Lval _ | Lint _ | Luint _ | Lfloat _ -> true
+  | Lval _ | Lint _ | Luint _ | Lfloat _ | Lstring _ -> true
   | _ -> false
 
 let get_value lc =
@@ -25,6 +25,7 @@ let get_value lc =
   | Lval (_, v) -> v
   | Lint i -> val_of_int i
   | Lfloat f -> val_of_float f
+  | Lstring s -> val_of_string s
   | _ -> assert false
 
 let hash_block tag args =
@@ -34,6 +35,7 @@ let hash_block tag args =
     | Luint i -> Uint63.hash i
     | Lint i -> Hashtbl.hash (i : int)
     | Lfloat f -> Float64.hash f
+    | Lstring s -> Pstring.hash s
     | Lval (h, _) -> h
     | _ -> assert false
     in

kernel/vmvalues.ml

@@ -78,6 +78,8 @@ let rec eq_structured_values v1 v2 =
       then Int64.equal (Obj.magic v1 : int64) (Obj.magic v2 : int64)
     else if Int.equal t1 Obj.double_tag
       then Float64.(equal (of_float (Obj.magic v1)) (of_float (Obj.magic v2)))
+    else if Int.equal t1 Obj.string_tag
+      then String.equal (Obj.magic v1) (Obj.magic v2)
     else begin
       assert (t1 <= Obj.last_non_constant_constructor_tag &&
               t2 <= Obj.last_non_constant_constructor_tag);
@@ -434,6 +436,8 @@ let val_of_uint i = (Obj.magic i : structured_values)
 
 let val_of_float f = (Obj.magic f : structured_values)
 
+let val_of_string s = (Obj.magic s : structured_values)
+
 let atom_of_proj kn v =
   let r = Obj.new_block proj_tag 2 in
   Obj.set_field r 0 (Obj.repr kn);

kernel/vmvalues.mli

@@ -140,6 +140,7 @@ val val_of_int : int -> structured_values
 val val_of_block : tag -> structured_values array -> structured_values
 val val_of_uint : Uint63.t -> structured_values
 val val_of_float : Float64.t -> structured_values
+val val_of_string : Pstring.t -> structured_values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"