[VM] Inject structured constants in values without reallocating them.

6 files changed, 72 insertions, 40 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 4c9ffc891e..6dabfee4ef 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -491,7 +491,9 @@ let rec compile_lam env cenv lam sz cont =
   match lam with
   | Lrel(_, i) -> pos_rel i cenv sz :: cont
 
-  | Lval v -> compile_structured_constant cenv v sz cont
+  | Lint i -> compile_structured_constant cenv (Const_b0 i) sz cont
+
+  | Lval v -> compile_structured_constant cenv (Const_val v) sz cont
 
   | Lproj (p,arg) ->
      compile_lam env cenv arg sz (Kproj p :: cont)
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index d4e35efa78..50f5607e31 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -358,10 +358,9 @@ let rec emit env insns remaining = match insns with
 type to_patch = emitcodes * patches * fv
 
 (* Substitution *)
-let rec subst_strcst s sc =
+let subst_strcst s sc =
   match sc with
-  | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc
-  | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
+  | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ -> sc
   | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
 
 let subst_reloc s ri =
diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli
index 29bfe4c731..dca1757b7d 100644
--- a/kernel/cinstr.mli
+++ b/kernel/cinstr.mli
@@ -34,10 +34,11 @@ and lambda =
   | Lfix          of (int array * int) * fix_decl
   | Lcofix        of int * fix_decl (* must be in eta-expanded form *)
   | Lmakeblock    of int * lambda array
-  | Lval          of structured_constant
+  | Lval          of structured_values
   | Lsort         of Sorts.t
   | Lind          of pinductive
   | Lproj         of Projection.Repr.t * lambda
+  | Lint          of int
   | Luint         of uint
 
 (* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index eace0ea13d..cc50e375f4 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -116,6 +116,8 @@ let rec pp_lam lam =
     hov 1
       (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg
        ++ str ")")
+  | Lint i ->
+    Pp.(str "(int:" ++ int i ++ str ")")
   | Luint _ ->
     str "(uint)"
 
@@ -151,7 +153,7 @@ let shift subst = subs_shft (1, subst)
 
 let rec map_lam_with_binders g f n lam =
   match lam with
-  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam
+  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ -> lam
   | Levar (evk, args) ->
     let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Levar (evk, args')
@@ -350,7 +352,7 @@ let rec occurrence k kind lam =
     if n = k then
       if kind then false else raise Not_found
     else kind
-  | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _ -> kind
+  | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _ | Lint _ -> kind
   | Levar (_, args) ->
     occurrence_args k kind args
   | Lprod(dom, codom) ->
@@ -437,23 +439,22 @@ let check_compilable ib =
 
 let is_value lc =
   match lc with
-  | Lval _ -> true
+  | Lval _ | Lint _ -> true
   | _ -> false
 
 let get_value lc =
   match lc with
   | Lval v -> v
+  | Lint i -> val_of_int i
   | _ -> raise Not_found
 
-let mkConst_b0 n = Lval (Const_b0 n)
-
 let make_args start _end =
   Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))
 
 (* Translation of constructors *)
 let expand_constructor tag nparams arity =
   let ids = Array.make (nparams + arity) Anonymous in
-  if arity = 0 then mkLlam ids (mkConst_b0 tag)
+  if arity = 0 then mkLlam ids (Lint tag)
   else
     let args = make_args arity 1 in
     Llam(ids, Lmakeblock (tag, args))
@@ -464,15 +465,15 @@ let makeblock tag nparams arity args =
     mkLapp (expand_constructor tag nparams arity) args
   else
     (* The constructor is fully applied *)
-  if arity = 0 then mkConst_b0 tag
+  if arity = 0 then Lint tag
   else
   if Array.for_all is_value args then
     if tag < last_variant_tag then
-      Lval(Const_bn(tag, Array.map get_value args))
+      Lval(val_of_block tag (Array.map get_value args))
     else
       let args = Array.map get_value args in
-      let args = Array.append [|Const_b0 (tag - last_variant_tag) |] args in
-      Lval(Const_bn(last_variant_tag, args))
+      let args = Array.append [| val_of_int (tag - last_variant_tag) |] args in
+      Lval(val_of_block last_variant_tag args)
   else Lmakeblock(tag, args)
 
 
@@ -837,8 +838,8 @@ let dynamic_int31_compilation fc args =
 
 (* We are relying here on the tags of digits constructors *)
 let digits_from_uint i =
-  let d0 = mkConst_b0 0 in
-  let d1 = mkConst_b0 1 in
+  let d0 = Lint 0 in
+  let d1 = Lint 1 in
   let digits = Array.make 31 d0 in
   for k = 0 to 30 do
     if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 490fabc6a5..d6970c35aa 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -27,6 +27,7 @@ let _ = init_vm ()
 
 (* Values of the abstract machine *)
 type values
+type structured_values = values
 let val_of_obj v = ((Obj.obj v):values)
 let crazy_val = (val_of_obj (Obj.repr 0))
 
@@ -46,42 +47,64 @@ let cofix_evaluated_tag = 7
    So fixme if this happens in a new version of OCaml *)
 let last_variant_tag = 245
 
+(** Structured constants are constants whose construction is done once. Their
+occurrences share the same value modulo kernel name substitutions (for functor
+application). Structured values have the additional property that no
+substitution will need to be performed, so their runtime value can directly be
+shared without reallocating a more structured representation. *)
 type structured_constant =
   | Const_sort of Sorts.t
   | Const_ind of inductive
   | Const_b0 of tag
-  | Const_bn of tag * structured_constant array
   | Const_univ_level of Univ.Level.t
+  | Const_val of structured_values
 
 type reloc_table = (tag * int) array
 
 type annot_switch =
    {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
 
-let rec eq_structured_constant c1 c2 = match c1, c2 with
+let rec eq_structured_values v1 v2 =
+  v1 == v2 ||
+  let o1 = Obj.repr v1 in
+  let o2 = Obj.repr v2 in
+  if Obj.is_int o1 && Obj.is_int o2 then o1 == o2
+  else if Int.equal (Obj.tag o1) (Obj.tag o2) &&
+          Int.equal (Obj.size o1) (Obj.size o2)
+  then
+    let i = ref 0 in
+    while (!i < Obj.size o1 && eq_structured_values
+             (Obj.magic (Obj.field o1 !i) : structured_values)
+             (Obj.magic (Obj.field o2 !i) : structured_values)) do
+      incr i
+    done;
+    !i >= Obj.size o1
+  else false
+
+let hash_structured_values (v : structured_values) =
+  (* We may want a better hash function here *)
+  Hashtbl.hash v
+
+let eq_structured_constant c1 c2 = match c1, c2 with
 | Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2
 | Const_sort _, _ -> false
 | Const_ind i1, Const_ind i2 -> eq_ind i1 i2
 | Const_ind _, _ -> false
 | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
 | Const_b0 _, _ -> false
-| Const_bn (t1, a1), Const_bn (t2, a2) ->
-  Int.equal t1 t2 && CArray.equal eq_structured_constant a1 a2
-| Const_bn _, _ -> false
 | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2
 | Const_univ_level _ , _ -> false
+| Const_val v1, Const_val v2 -> eq_structured_values v1 v2
+| Const_val v1, _ -> false
 
-let rec hash_structured_constant c =
+let hash_structured_constant c =
   let open Hashset.Combine in
   match c with
   | Const_sort s -> combinesmall 1 (Sorts.hash s)
   | Const_ind i -> combinesmall 2 (ind_hash i)
   | Const_b0 t -> combinesmall 3 (Int.hash t)
-  | Const_bn (t, a) ->
-    let fold h c = combine h (hash_structured_constant c) in
-    let h = Array.fold_left fold 0 a in
-    combinesmall 4 (combine (Int.hash t) h)
-  | Const_univ_level l -> combinesmall 5 (Univ.Level.hash l)
+  | Const_univ_level l -> combinesmall 4 (Univ.Level.hash l)
+  | Const_val v -> combinesmall 5 (hash_structured_values v)
 
 let eq_annot_switch asw1 asw2 =
   let eq_ci ci1 ci2 =
@@ -108,13 +131,12 @@ let pp_sort s =
   | Set -> Pp.str "Set"
   | Type u -> Pp.(str "Type@{" ++ Univ.pr_uni u ++ str "}")
 
-let rec pp_struct_const = function
+let pp_struct_const = function
   | Const_sort s -> pp_sort s
   | Const_ind (mind, i) -> Pp.(MutInd.print mind ++ str"#" ++ int i)
   | Const_b0 i -> Pp.int i
-  | Const_bn (i,t) ->
-     Pp.(int i ++ surround (prvect_with_sep pr_comma pp_struct_const t))
   | Const_univ_level l -> Univ.Level.pr l
+  | Const_val _ -> Pp.str "(value)"
 
 (* Abstract data *)
 type vprod
@@ -379,19 +401,21 @@ let obj_of_atom : atom -> Obj.t =
     res
 
 (* obj_of_str_const : structured_constant -> Obj.t *)
-let rec obj_of_str_const str =
+let obj_of_str_const str =
   match str with
   | Const_sort s -> obj_of_atom (Asort s)
   | Const_ind ind -> obj_of_atom (Aind ind)
   | Const_b0 tag -> Obj.repr tag
-  | Const_bn(tag, args) ->
-      let len = Array.length args in
-      let res = Obj.new_block tag len in
-      for i = 0 to len - 1 do
-        Obj.set_field res i (obj_of_str_const args.(i))
-      done;
-      res
   | Const_univ_level l -> Obj.repr (Vuniv_level l)
+  | Const_val v -> Obj.repr v
+
+let val_of_block tag (args : structured_values array) =
+  let nargs = Array.length args in
+  let r = Obj.new_block tag nargs in
+  for i = 0 to nargs - 1 do
+    Obj.set_field r i (Obj.repr args.(i))
+  done;
+  (Obj.magic r : structured_values)
 
 let val_of_obj o = ((Obj.obj o) : values)
 
@@ -399,6 +423,8 @@ let val_of_str_const str = val_of_obj (obj_of_str_const str)
 
 let val_of_atom a = val_of_obj (obj_of_atom a)
 
+let val_of_int i = (Obj.magic i : values)
+
 let atom_of_proj kn v =
   let r = Obj.new_block proj_tag 2 in
   Obj.set_field r 0 (Obj.repr kn);
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 2604d50fe6..c7540ae249 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -14,6 +14,7 @@ open Constr
 (** Values *)
 
 type values
+type structured_values
 type vm_env
 type vm_global
 type vprod
@@ -43,8 +44,8 @@ type structured_constant =
   | Const_sort of Sorts.t
   | Const_ind of inductive
   | Const_b0 of tag
-  | Const_bn of tag * structured_constant array
   | Const_univ_level of Univ.Level.t
+  | Const_val of structured_values
 
 val pp_struct_const : structured_constant -> Pp.t
 
@@ -144,6 +145,8 @@ val val_of_constant : Constant.t -> values
 val val_of_evar : Evar.t -> values
 val val_of_proj : Projection.Repr.t -> values -> values
 val val_of_atom : atom -> values
+val val_of_int : int -> structured_values
+val val_of_block : tag -> structured_values array -> structured_values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
 external val_of_proj_name : Projection.Repr.t -> values = "%identity"