1 files changed, 167 insertions, 36 deletions

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 0e0cb4e5..8edd49f7 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 ***)
@@ -25,11 +25,124 @@ 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
 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
+
+(** 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_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_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
+    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 <= 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)
+               (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 *)
+  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_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 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_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 =
+    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 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_univ_level l -> Univ.Level.pr l
+  | Const_val _ -> Pp.str "(value)"
+
 (* Abstract data *)
 type vprod
 type vfun
@@ -43,6 +156,7 @@ let fix_val v = (Obj.magic v : values)
 let cofix_upd_val v = (Obj.magic v : values)
 
 type vm_env
+type vm_global
 let fun_env v = (Obj.magic v : vm_env)
 let fix_env v = (Obj.magic v : vm_env)
 let cofix_env v = (Obj.magic v : vm_env)
@@ -51,19 +165,24 @@ type vstack = values array
 
 let fun_of_val v = (Obj.magic v : vfun)
 
+let vm_global (v : values array) = (Obj.magic v : vm_global)
+
 (*******************************************)
 (* Machine code *** ************************)
 (*******************************************)
 
 type tcode
+(** A block whose first field is a C-allocated VM bytecode, encoded as char*.
+    This is compatible with the representation of the Coq VM closures. *)
+
+type tcode_array
 
 external mkAccuCode : int -> tcode = "coq_makeaccu"
 external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode"
 
-let tcode_of_obj v = ((Obj.obj v):tcode)
-let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0)
-let fix_code v = fun_code v
-let cofix_upd_code v = fun_code v
+let fun_code v = (Obj.magic v : tcode)
+let fix_code = fun_code
+let cofix_upd_code = fun_code
 
 
 type vswitch = {
@@ -144,7 +263,7 @@ type zipper =
   | Zapp of arguments
   | Zfix of vfix*arguments  (* Possibly empty *)
   | Zswitch of vswitch
-  | Zproj of Constant.t (* name of the projection *)
+  | Zproj of Projection.Repr.t (* name of the projection *)
 
 type stack = zipper list
 
@@ -252,6 +371,7 @@ external kind_of_closure : Obj.t -> int = "coq_kind_of_closure"
 external is_accumulate : tcode -> bool = "coq_is_accumulate_code"
 external int_tcode : tcode -> int -> int = "coq_int_tcode"
 external accumulate : unit -> tcode = "accumulate_code"
+external set_bytecode_field : Obj.t -> int -> tcode -> unit = "coq_set_bytecode_field"
 let accumulate = accumulate ()
 
 let whd_val : values -> whd =
@@ -281,25 +401,26 @@ let whd_val : values -> whd =
 let obj_of_atom : atom -> Obj.t =
   fun a ->
     let res = Obj.new_block accu_tag 2 in
-    Obj.set_field res 0 (Obj.repr accumulate);
+    set_bytecode_field res 0 accumulate;
     Obj.set_field res 1 (Obj.repr a);
     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_proj p -> Obj.repr p
   | 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)
 
@@ -307,6 +428,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);
@@ -348,6 +471,7 @@ let val_of_constant c = val_of_idkey (ConstKey c)
 let val_of_evar evk = val_of_idkey (EvarKey evk)
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
+external val_of_proj_name : Projection.Repr.t -> values = "%identity"
 
 (*************************************************)
 (** Operations manipulating data types ***********)
@@ -367,17 +491,20 @@ external closure_arity : vfun -> int = "coq_closure_arity"
 external offset : Obj.t -> int = "coq_offset"
 external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
 external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure"
+external tcode_array : tcode_array -> tcode array = "coq_tcode_array"
 
 let first o = (offset_closure o (offset o))
 let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix)
 
 let last o = (Obj.field o (Obj.size o - 1))
-let fix_types (v:vfix) = (Obj.magic (last (Obj.repr v)) : tcode array)
-let cofix_types (v:vcofix) = (Obj.magic (last (Obj.repr v)) : tcode array)
+let fix_types (v:vfix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array)
+let cofix_types (v:vcofix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array)
 
 let current_fix vf = - (offset (Obj.repr vf) / 2)
 
-let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i))
+let unsafe_fb_code fb i =
+  let off = (2 * i) * (Sys.word_size / 8) in
+  Obj.obj (Obj.add_offset (Obj.repr fb) (Int32.of_int off))
 
 let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1
 
@@ -407,13 +534,20 @@ let check_fix f1 f2 =
     else false
   else false
 
-external atom_rel : unit -> atom array = "get_coq_atom_tbl"
-external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl"
+let atom_rel : atom array ref =
+  let init i = Aid (RelKey i) in
+  ref (Array.init 40 init)
+
+let get_atom_rel () = !atom_rel
+
+let realloc_atom_rel n =
+  let n = min (2 * n + 0x100) Sys.max_array_length in
+  let init i = Aid (RelKey i) in
+  let ans = Array.init n init in
+  atom_rel := ans
 
 let relaccu_tbl =
-  let atom_rel = atom_rel() in
-  let len = Array.length atom_rel in
-  for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done;
+  let len = Array.length !atom_rel in
   ref (Array.init len mkAccuCode)
 
 let relaccu_code i =
@@ -422,9 +556,7 @@ let relaccu_code i =
   else
     begin
       realloc_atom_rel i;
-      let atom_rel = atom_rel () in
-      let nl = Array.length atom_rel in
-      for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done;
+      let nl = Array.length !atom_rel in
       relaccu_tbl :=
         Array.init nl
           (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j);
@@ -434,13 +566,12 @@ let relaccu_code i =
 let mk_fix_body k ndef fb =
   let e = Obj.dup (Obj.repr fb) in
   for i = 0 to ndef - 1 do
-    Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i)))
+    set_bytecode_field e (2 * i) (relaccu_code (k + i))
   done;
   let fix_body i =
-    let jump_grabrec c = offset_tcode c 2 in
-    let c = jump_grabrec (unsafe_fb_code fb i)  in
+    let c = offset_tcode (unsafe_fb_code fb i) 2 in
     let res = Obj.new_block Obj.closure_tag 2 in
-    Obj.set_field res 0 (Obj.repr c);
+    set_bytecode_field res 0 c;
     Obj.set_field res 1 (offset_closure e (2*i));
     ((Obj.obj res) : vfun)  in
   Array.init ndef fix_body
@@ -478,7 +609,7 @@ let mk_cofix_body apply_varray k ndef vcf =
     Obj.set_field e 0 c;
     let atom = Obj.new_block cofix_tag 1 in
     let self = Obj.new_block accu_tag 2 in
-    Obj.set_field self 0 (Obj.repr accumulate);
+    set_bytecode_field self 0 accumulate;
     Obj.set_field self 1 (Obj.repr atom);
     apply_varray (Obj.obj e) [|Obj.obj self|] in
   Array.init ndef cofix_body
@@ -500,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)))
@@ -539,4 +670,4 @@ and pr_zipper z =
   | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")"
   | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")"
   | Zswitch s -> str "Zswitch(...)"
-  | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")")
+  | Zproj c -> str "Zproj(" ++ Projection.Repr.print c ++ str ")")