From f02e6260f1cf1f49121860cfd95b6adb97db48ee Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 1 Mar 2018 14:43:07 +0100
Subject: [VM] Move structured_constant to Vmvalues

---
 kernel/cbytecodes.ml   | 88 +-------------------------------------------------
 kernel/cbytecodes.mli  | 36 +--------------------
 kernel/cbytegen.ml     |  1 +
 kernel/cemitcodes.ml   |  1 +
 kernel/cemitcodes.mli  |  1 +
 kernel/cinstr.mli      |  1 +
 kernel/clambda.ml      |  9 +++---
 kernel/declarations.ml |  2 +-
 kernel/kernel.mllib    |  2 +-
 kernel/vm.ml           |  1 -
 kernel/vmvalues.ml     | 88 +++++++++++++++++++++++++++++++++++++++++++++++++-
 kernel/vmvalues.mli    | 38 ++++++++++++++++++++--
 12 files changed, 136 insertions(+), 132 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 9a1224aab2..ed3bd866a4 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -15,78 +15,7 @@
 (* This file defines the type of bytecode instructions *)
 
 open Names
-open Constr
-
-type tag = int
-
-let accu_tag = 0
-
-let type_atom_tag = 2
-let max_atom_tag = 2
-let proj_tag = 3
-let fix_app_tag = 4
-let switch_tag = 5
-let cofix_tag = 6
-let cofix_evaluated_tag = 7
-
-(* It would be great if OCaml exported this value,
-   So fixme if this happens in a new version of OCaml *)
-let last_variant_tag = 245 
-
-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
-
-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
-| 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
-
-let rec 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)
-
-let eq_annot_switch asw1 asw2 =
-  let eq_ci ci1 ci2 =
-    eq_ind ci1.ci_ind ci2.ci_ind &&
-    Int.equal ci1.ci_npar ci2.ci_npar &&
-    CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
-  in
-  let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
-  eq_ci asw1.ci asw2.ci &&
-  CArray.equal eq_rlc asw1.rtbl asw2.rtbl &&
-  (asw1.tailcall : bool) == asw2.tailcall
-
-let hash_annot_switch asw =
-  let open Hashset.Combine in
-  let h1 = Constr.case_info_hash asw.ci in
-  let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
-  let h3 = if asw.tailcall then 1 else 0 in
-  combine3 h1 h2 h3
+open Vmvalues
 
 module Label =
   struct
@@ -232,21 +161,6 @@ type comp_env = {
 open Pp
 open Util
 
-let pp_sort s =
-  let open Sorts in
-  match s with
-  | Prop -> str "Prop"
-  | Set -> str "Set"
-  | Type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}"
-
-let rec pp_struct_const = function
-  | Const_sort s -> pp_sort s
-  | Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i
-  | Const_b0 i -> int i
-  | Const_bn (i,t) ->
-     int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
-  | Const_univ_level l -> Univ.Level.pr l
-
 let pp_lbl lbl = str "L" ++ int lbl
 
 let pp_fv_elem = function
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index f17a1e657e..9c04c166a2 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -11,41 +11,7 @@
 (* $Id$ *)
 
 open Names
-open Constr
-
-type tag = int
-
-val accu_tag : tag
-
-val type_atom_tag : tag
-val max_atom_tag : tag
-val proj_tag : tag
-val fix_app_tag : tag
-val switch_tag : tag
-val cofix_tag : tag
-val cofix_evaluated_tag : tag
-
-val last_variant_tag : tag
-
-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
-
-val pp_struct_const : structured_constant -> Pp.t
-
-type reloc_table = (tag * int) array
-
-type annot_switch =
-   {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
-
-val eq_structured_constant : structured_constant -> structured_constant -> bool
-val hash_structured_constant : structured_constant -> int
-
-val eq_annot_switch : annot_switch -> annot_switch -> bool
-val hash_annot_switch : annot_switch -> int
+open Vmvalues
 
 module Label :
   sig
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index e336ea922d..4c9ffc891e 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -14,6 +14,7 @@
 
 open Util
 open Names
+open Vmvalues
 open Cbytecodes
 open Cemitcodes
 open Cinstr
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index ca24f9b689..d4e35efa78 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -14,6 +14,7 @@
 
 open Names
 open Constr
+open Vmvalues
 open Cbytecodes
 open Copcodes
 open Mod_subst
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 9009926bdb..39ddf4a047 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -1,4 +1,5 @@
 open Names
+open Vmvalues
 open Cbytecodes
 
 type reloc_info =
diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli
index 171ca38830..29bfe4c731 100644
--- a/kernel/cinstr.mli
+++ b/kernel/cinstr.mli
@@ -9,6 +9,7 @@
 (************************************************************************)
 open Names
 open Constr
+open Vmvalues
 open Cbytecodes
 
 (** This file defines the lambda code for the bytecode compiler. It has been
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 961036d3c5..eace0ea13d 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -4,6 +4,7 @@ open Esubst
 open Term
 open Constr
 open Declarations
+open Vmvalues
 open Cbytecodes
 open Cinstr
 open Environ
@@ -444,7 +445,7 @@ let get_value lc =
   | Lval v -> v
   | _ -> raise Not_found
 
-let mkConst_b0 n = Lval (Cbytecodes.Const_b0 n)
+let mkConst_b0 n = Lval (Const_b0 n)
 
 let make_args start _end =
   Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))
@@ -467,11 +468,11 @@ let makeblock tag nparams arity args =
   else
   if Array.for_all is_value args then
     if tag < last_variant_tag then
-      Lval(Cbytecodes.Const_bn(tag, Array.map get_value args))
+      Lval(Const_bn(tag, Array.map get_value args))
     else
       let args = Array.map get_value args in
-      let args = Array.append [|Cbytecodes.Const_b0 (tag - last_variant_tag) |] args in
-      Lval(Cbytecodes.Const_bn(last_variant_tag, args))
+      let args = Array.append [|Const_b0 (tag - last_variant_tag) |] args in
+      Lval(Const_bn(last_variant_tag, args))
   else Lmakeblock(tag, args)
 
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 1d49550442..61fcb4832a 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -164,7 +164,7 @@ type one_inductive_body = {
 
     mind_nb_args : int; (** number of no constant constructor *)
 
-    mind_reloc_tbl :  Cbytecodes.reloc_table;
+    mind_reloc_tbl :  Vmvalues.reloc_table;
   }
 
 type abstract_inductive_universes =
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 07a02f6ef5..a18c5d1e20 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -10,13 +10,13 @@ Constr
 Vars
 Term
 Mod_subst
+Vmvalues
 Cbytecodes
 Copcodes
 Cemitcodes
 Opaqueproof
 Declarations
 Entries
-Vmvalues
 Nativevalues
 CPrimitives
 Declareops
diff --git a/kernel/vm.ml b/kernel/vm.ml
index d7eedc226c..9917e94a35 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Cbytecodes
 open Vmvalues
 
 external set_drawinstr : unit -> unit = "coq_set_drawinstr"
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index d6d9312938..490fabc6a5 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -9,8 +9,8 @@
 (************************************************************************)
 open Names
 open Sorts
-open Cbytecodes
 open Univ
+open Constr
 
 (*******************************************)
 (* Initalization of the abstract machine ***)
@@ -30,6 +30,92 @@ type values
 let val_of_obj v = ((Obj.obj v):values)
 let crazy_val = (val_of_obj (Obj.repr 0))
 
+type tag = int
+
+let accu_tag = 0
+
+let type_atom_tag = 2
+let max_atom_tag = 2
+let proj_tag = 3
+let fix_app_tag = 4
+let switch_tag = 5
+let cofix_tag = 6
+let cofix_evaluated_tag = 7
+
+(* It would be great if OCaml exported this value,
+   So fixme if this happens in a new version of OCaml *)
+let last_variant_tag = 245
+
+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
+
+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
+| 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
+
+let rec 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)
+
+let eq_annot_switch asw1 asw2 =
+  let eq_ci ci1 ci2 =
+    eq_ind ci1.ci_ind ci2.ci_ind &&
+    Int.equal ci1.ci_npar ci2.ci_npar &&
+    CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
+  in
+  let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
+  eq_ci asw1.ci asw2.ci &&
+  CArray.equal eq_rlc asw1.rtbl asw2.rtbl &&
+  (asw1.tailcall : bool) == asw2.tailcall
+
+let hash_annot_switch asw =
+  let open Hashset.Combine in
+  let h1 = Constr.case_info_hash asw.ci in
+  let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
+  let h3 = if asw.tailcall then 1 else 0 in
+  combine3 h1 h2 h3
+
+let pp_sort s =
+  let open Sorts in
+  match s with
+  | Prop -> Pp.str "Prop"
+  | Set -> Pp.str "Set"
+  | Type u -> Pp.(str "Type@{" ++ Univ.pr_uni u ++ str "}")
+
+let rec 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
+
 (* Abstract data *)
 type vprod
 type vfun
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 6eedcf1d37..2604d50fe6 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 open Names
-open Cbytecodes
+open Constr
 
 (** Values *)
 
@@ -25,6 +25,40 @@ type arguments
 type vstack = values array
 type to_update
 
+type tag = int
+
+val accu_tag : tag
+
+val type_atom_tag : tag
+val max_atom_tag : tag
+val proj_tag : tag
+val fix_app_tag : tag
+val switch_tag : tag
+val cofix_tag : tag
+val cofix_evaluated_tag : tag
+
+val last_variant_tag : tag
+
+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
+
+val pp_struct_const : structured_constant -> Pp.t
+
+type reloc_table = (tag * int) array
+
+type annot_switch =
+   {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
+
+val eq_structured_constant : structured_constant -> structured_constant -> bool
+val hash_structured_constant : structured_constant -> int
+
+val eq_annot_switch : annot_switch -> annot_switch -> bool
+val hash_annot_switch : annot_switch -> int
+
 val fun_val : vfun -> values
 val fix_val : vfix -> values
 val cofix_upd_val : to_update -> values
@@ -158,4 +192,4 @@ val bfield : vblock -> int -> values
 (** Switch *)
 
 val check_switch : vswitch -> vswitch -> bool
-val branch_arg : int -> Cbytecodes.tag * int -> values
+val branch_arg : int -> tag * int -> values
-- 
cgit v1.2.3


From 00a63b73f267ae90cc868f14ab4f36db8185b3e0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 2 Mar 2018 21:46:55 +0100
Subject: [VM] Inject structured constants in values without reallocating them.

---
 kernel/cbytegen.ml   |  4 ++-
 kernel/cemitcodes.ml |  5 ++--
 kernel/cinstr.mli    |  3 ++-
 kernel/clambda.ml    | 25 ++++++++++---------
 kernel/vmvalues.ml   | 70 +++++++++++++++++++++++++++++++++++-----------------
 kernel/vmvalues.mli  |  5 +++-
 6 files changed, 72 insertions(+), 40 deletions(-)

(limited to 'kernel')

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"
-- 
cgit v1.2.3


From 7a4b3edf1a4299c7813668515ad1b8fa6cf99dd3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 11 Jun 2018 10:02:57 +0200
Subject: [VM] Allocate a bit less in digits_from_uint

---
 kernel/clambda.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index cc50e375f4..0a3fb44cbe 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -836,10 +836,11 @@ let dynamic_int31_compilation fc args =
   if not fc then raise Not_found else
   Luint (UintDigits args)
 
+let d0 = Lint 0
+let d1 = Lint 1
+
 (* We are relying here on the tags of digits constructors *)
 let digits_from_uint i =
-  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
-- 
cgit v1.2.3


From 42706b1cd101f389f3e704f859200a35316bd97e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 14 Sep 2018 17:37:01 +0200
Subject: Add assertion on tags in eq_structured_constants

---
 kernel/vmvalues.ml | 27 ++++++++++++++++-----------
 1 file changed, 16 insertions(+), 11 deletions(-)

(limited to 'kernel')

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index d6970c35aa..a972803ce4 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -69,17 +69,22 @@ let rec eq_structured_values 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
+  else
+    let t1 = Obj.tag o1 in
+    let t2 = Obj.tag o2 in
+    if Int.equal t1 t2 &&
+       Int.equal (Obj.size o1) (Obj.size o2)
+    then begin
+      assert (t1 <= last_variant_tag && t2 <= last_variant_tag);
+      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
+    end
+    else false
 
 let hash_structured_values (v : structured_values) =
   (* We may want a better hash function here *)
-- 
cgit v1.2.3


From a8bf1cab3f21de4a350737ef5c933af1746f54a1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 14 Sep 2018 17:42:54 +0200
Subject: OCaml now exports the min and max non-constant tags, let's use it

---
 kernel/cbytegen.ml  | 22 +++++++++++-----------
 kernel/clambda.ml   |  8 ++++----
 kernel/vmvalues.ml  | 16 ++++++++--------
 kernel/vmvalues.mli |  2 --
 4 files changed, 23 insertions(+), 25 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 6dabfee4ef..5362f9a814 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -396,17 +396,17 @@ let init_fun_code () = fun_code := []
 (*
 If [tag] hits the OCaml limitation for non constant constructors, we switch to
 another representation for the remaining constructors:
-[last_variant_tag|tag - last_variant_tag|args]
+[last_variant_tag|tag - Obj.last_non_constant_constructor_tag|args]
 
-We subtract last_variant_tag for efficiency of match interpretation.
+We subtract Obj.last_non_constant_constructor_tag for efficiency of match interpretation.
  *)
 
 let nest_block tag arity cont =
-  Kconst (Const_b0 (tag - last_variant_tag)) ::
-    Kmakeblock(arity+1, last_variant_tag) :: cont
+  Kconst (Const_b0 (tag - Obj.last_non_constant_constructor_tag)) ::
+    Kmakeblock(arity+1, Obj.last_non_constant_constructor_tag) :: cont
 
 let code_makeblock ~stack_size ~arity ~tag cont = 
-  if tag < last_variant_tag then
+  if tag < Obj.last_non_constant_constructor_tag then
     Kmakeblock(arity, tag) :: cont
   else begin
     set_max_stack_size (stack_size + 1);
@@ -637,9 +637,9 @@ let rec compile_lam env cenv lam sz cont =
       let lbl_consts = Array.make oib.mind_nb_constant Label.no in
       let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *)
       let nconst = Array.length branches.constant_branches in
-      let nblock = min nallblock (last_variant_tag + 1) in
+      let nblock = min nallblock (Obj.last_non_constant_constructor_tag + 1) in
       let lbl_blocks = Array.make nblock Label.no in
-      let neblock = max 0 (nallblock - last_variant_tag) in
+      let neblock = max 0 (nallblock - Obj.last_non_constant_constructor_tag) in
       let lbl_eblocks = Array.make neblock Label.no in 
       let branch1, cont = make_branch cont in
       (* Compilation of the return type *)
@@ -665,7 +665,7 @@ let rec compile_lam env cenv lam sz cont =
         let lbl_b, code_b = 
           label_code (
             Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in
-        lbl_blocks.(last_variant_tag) <- lbl_b;
+        lbl_blocks.(Obj.last_non_constant_constructor_tag) <- lbl_b;
         c := code_b
       end;
 
@@ -687,7 +687,7 @@ let rec compile_lam env cenv lam sz cont =
           compile_lam env (push_param arity sz_b cenv)
             body (sz_b+arity) (add_pop arity (branch::!c)) in
         let code_b =
-            if tag < last_variant_tag then begin
+            if tag < Obj.last_non_constant_constructor_tag then begin
                 set_max_stack_size (sz_b + arity);
                 Kpushfields arity :: code_b
               end
@@ -697,8 +697,8 @@ let rec compile_lam env cenv lam sz cont =
               end
         in
         let lbl_b, code_b = label_code code_b in
-        if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b
-          else lbl_eblocks.(tag - last_variant_tag) <- lbl_b;
+        if tag < Obj.last_non_constant_constructor_tag then lbl_blocks.(tag) <- lbl_b
+          else lbl_eblocks.(tag - Obj.last_non_constant_constructor_tag) <- lbl_b;
         c := code_b
       done;
 
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 0a3fb44cbe..ff977416df 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -422,7 +422,7 @@ let rec remove_let subst lam =
 exception TooLargeInductive of Pp.t
 
 let max_nb_const = 0x1000000
-let max_nb_block = 0x1000000 + last_variant_tag - 1
+let max_nb_block = 0x1000000 + Obj.last_non_constant_constructor_tag - 1
 
 let str_max_constructors =
   Format.sprintf
@@ -468,12 +468,12 @@ let makeblock tag nparams arity args =
   if arity = 0 then Lint tag
   else
   if Array.for_all is_value args then
-    if tag < last_variant_tag then
+    if tag < Obj.last_non_constant_constructor_tag then
       Lval(val_of_block tag (Array.map get_value args))
     else
       let args = Array.map get_value args in
-      let args = Array.append [| val_of_int (tag - last_variant_tag) |] args in
-      Lval(val_of_block last_variant_tag args)
+      let args = Array.append [| val_of_int (tag - Obj.last_non_constant_constructor_tag) |] args in
+      Lval(val_of_block Obj.last_non_constant_constructor_tag args)
   else Lmakeblock(tag, args)
 
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index a972803ce4..8edd49f77f 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -25,6 +25,9 @@ let _ = init_vm ()
 (* Abstract data types and utility functions **********)
 (******************************************************)
 
+(* The representation of values relies on this assertion *)
+let _ = assert (Int.equal Obj.first_non_constant_constructor_tag 0)
+
 (* Values of the abstract machine *)
 type values
 type structured_values = values
@@ -43,10 +46,6 @@ let switch_tag = 5
 let cofix_tag = 6
 let cofix_evaluated_tag = 7
 
-(* It would be great if OCaml exported this value,
-   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
@@ -75,7 +74,8 @@ let rec eq_structured_values v1 v2 =
     if Int.equal t1 t2 &&
        Int.equal (Obj.size o1) (Obj.size o2)
     then begin
-      assert (t1 <= last_variant_tag && t2 <= last_variant_tag);
+      assert (t1 <= Obj.last_non_constant_constructor_tag &&
+              t2 <= Obj.last_non_constant_constructor_tag);
       let i = ref 0 in
       while (!i < Obj.size o1 && eq_structured_values
                (Obj.magic (Obj.field o1 !i) : structured_values)
@@ -631,10 +631,10 @@ let branch_arg k (tag,arity) =
   if Int.equal arity 0 then  ((Obj.magic tag):values)
   else
     let b, ofs =
-      if tag < last_variant_tag then Obj.new_block tag arity, 0
+      if tag < Obj.last_non_constant_constructor_tag then Obj.new_block tag arity, 0
       else
-        let b = Obj.new_block last_variant_tag (arity+1) in
-        Obj.set_field b 0 (Obj.repr (tag-last_variant_tag));
+        let b = Obj.new_block Obj.last_non_constant_constructor_tag (arity+1) in
+        Obj.set_field b 0 (Obj.repr (tag-Obj.last_non_constant_constructor_tag));
         b,1 in
     for i = ofs to ofs + arity - 1 do
       Obj.set_field b i (Obj.repr (val_of_rel (k+i)))
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index c7540ae249..ae1d416ed5 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -38,8 +38,6 @@ val switch_tag : tag
 val cofix_tag : tag
 val cofix_evaluated_tag : tag
 
-val last_variant_tag : tag
-
 type structured_constant =
   | Const_sort of Sorts.t
   | Const_ind of inductive
-- 
cgit v1.2.3