[VM] Move structured_constant to Vmvalues

12 files changed, 136 insertions, 132 deletions

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