Merge PR #6605: Safer VM interfaces

17 files changed, 723 insertions, 645 deletions

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 8e43bf6ed..f819d2e6a 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -3,7 +3,7 @@ open Term
 open Names
 open Cbytecodes
 open Cemitcodes
-open Vm
+open Vmvalues
 
 let ppripos (ri,pos) =
   (match ri with
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 5930cfadc..1ff1fcc4c 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -1178,8 +1178,3 @@ let hcons =
      Id.hcons)
 
 (* let hcons_types = hcons_constr *)
-
-(*******)
-(* Type of abstract machine values *)
-(** FIXME: nothing to do there *)
-type values
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 98bf71308..19ffa8fe3 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -459,7 +459,3 @@ val case_info_hash : case_info -> int
 (*********************************************************************)
 
 val hcons : constr -> constr
-
-(**************************************)
-
-type values
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 712c66f11..2bbb867cd 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -15,7 +15,7 @@
 open Util
 open Names
 open Constr
-open Vm
+open Vmvalues
 open Cemitcodes
 open Cbytecodes
 open Declarations
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index 91bb30e7e..fc935f6ee 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -12,7 +12,7 @@ open Names
 open Constr
 open Pre_env
 
-val val_of_constr : env -> constr -> values
+val val_of_constr : env -> constr -> Vmvalues.values
 
 val set_opaque_const      : Constant.t -> unit
 val set_transparent_const : Constant.t -> unit
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 917e4f6f1..749854b8c 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -16,6 +16,7 @@ Cemitcodes
 Opaqueproof
 Declarations
 Entries
+Vmvalues
 Nativevalues
 CPrimitives
 Declareops
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 3ef15105a..6c5e1cde5 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -15,7 +15,6 @@
 
 open Util
 open Names
-open Constr
 open Declarations
 
 module NamedDecl = Context.Named.Declaration
@@ -50,7 +49,7 @@ type stratification = {
 }
 
 type val_kind =
-    | VKvalue of (values * Id.Set.t) CEphemeron.key
+    | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key
     | VKnone
 
 type lazy_val = val_kind ref
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 335ca1057..a6b57bd1b 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -36,9 +36,9 @@ type stratification = {
 
 type lazy_val
 
-val force_lazy_val : lazy_val -> (values * Id.Set.t) option
+val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option
 val dummy_lazy_val : unit -> lazy_val
-val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit
+val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit
 
 type named_context_val = private {
   env_named_ctx : Context.Named.t;
diff --git a/kernel/term.ml b/kernel/term.ml
index aa8805952..fae990d45 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of projection * 'constr
 
-type values = Constr.values
+type values = Vmvalues.values
 
 (**********************************************************************)
 (**         Redeclaration of functions from module Constr             *)
diff --git a/kernel/term.mli b/kernel/term.mli
index f5cb72f4e..c9a8cf6e1 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -572,8 +572,8 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Proj      of projection * 'constr
 [@@ocaml.deprecated "Alias for Constr.kind_of_term"]
 
-type values = Constr.values
-[@@ocaml.deprecated "Alias for Constr.values"]
+type values = Vmvalues.values
+[@@ocaml.deprecated "Alias for Vmvalues.values"]
 
 val hash_constr : Constr.constr -> int
 [@@ocaml.deprecated "Alias for Constr.hash"]
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 3ef297b1f..8c7658147 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -3,6 +3,7 @@ open Names
 open Environ
 open Reduction
 open Vm
+open Vmvalues
 open Csymtable
 
 let val_of_constr env c =
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 7f727df47..c3c9636e8 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -19,4 +19,4 @@ val vm_conv : conv_pb -> types kernel_conversion_function
 val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function
 
 (** Precompute a VM value from a constr *)
-val val_of_constr : env -> constr -> values
+val val_of_constr : env -> constr -> Vmvalues.values
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 51101f88e..352ea74a4 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -6,47 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Sorts
-open Constr
 open Cbytecodes
+open Vmvalues
 
 external set_drawinstr : unit -> unit = "coq_set_drawinstr"
 
-(******************************************)
-(* Utility Functions about Obj ************)
-(******************************************)
-
-external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
-external offset : Obj.t -> int = "coq_offset"
-
-(*******************************************)
-(* Initalization of the abstract machine ***)
-(*******************************************)
-
-external init_vm : unit -> unit = "init_coq_vm"
-
-let _ = init_vm ()
-
-(*******************************************)
-(* Machine code *** ************************)
-(*******************************************)
-
-type tcode
-let tcode_of_obj v = ((Obj.obj v):tcode)
-let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0)
-
-external mkAccuCode : int -> tcode = "coq_makeaccu"
 external mkPopStopCode : int -> tcode = "coq_pushpop"
 
-external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode"
-external int_tcode : tcode -> int -> int = "coq_int_tcode"
-
-external accumulate : unit -> tcode = "accumulate_code"
-let accumulate = accumulate ()
-
-external is_accumulate : tcode -> bool = "coq_is_accumulate_code"
-
 let popstop_tbl =  ref (Array.init 30 mkPopStopCode)
 
 let popstop_code i =
@@ -62,106 +28,6 @@ let popstop_code i =
 
 let stop = popstop_code 0
 
-(******************************************************)
-(* Abstract data types and utility functions **********)
-(******************************************************)
-
-(* Values of the abstract machine *)
-let val_of_obj v = ((Obj.obj v):values)
-let crazy_val = (val_of_obj (Obj.repr 0))
-
-(* Abstract data *)
-type vprod
-type vfun
-type vfix
-type vcofix
-type vblock 
-type arguments
-
-type vm_env
-type vstack = values array
-
-type vswitch = {
-    sw_type_code : tcode;
-    sw_code : tcode;
-    sw_annot : annot_switch;
-    sw_stk : vstack;
-    sw_env : vm_env
-  }
-
-(* Representation of values *)
-(* + Products : *)
-(*   -   vprod = 0_[ dom | codom]                                         *)
-(*             dom : values, codom : vfun                                 *)
-(*                                                                        *)
-(* + Functions have two representations :                                 *)
-(*   - unapplied fun :  vf = Ct_[ C | fv1 | ... | fvn]                    *)
-(*                                       C:tcode, fvi : values            *)
-(*     Remark : a function and its environment is the same value.         *)
-(*   - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn]       *)
-(*                                                                        *)
-(* + Fixpoints :                                                          *)
-(*   -        Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn]               *)
-(*     One single block to represent all of the fixpoints, each fixpoint  *)
-(*     is the pointer to the field holding the pointer to its code, and   *)
-(*     the infix tag is used to know where the block starts.              *)
-(*   - Partial application follows the scheme of partially applied        *)
-(*     functions. Note: only fixpoints not having been applied to its     *)
-(*     recursive argument are coded this way. When the rec. arg. is       *)
-(*     applied, either it's a constructor and the fix reduces, or it's    *)
-(*     and the fix is coded as an accumulator.                            *)
-(*                                                                        *)
-(* + Cofixpoints : see cbytegen.ml                                        *)
-(*                                                                        *)
-(* + vblock's encode (non constant) constructors as in Ocaml, but         *)
-(*   starting from 0 up. tag 0 ( = accu_tag) is reserved for              *)
-(*   accumulators.                                                        *)
-(*                                                                        *)
-(* + vm_env is the type of the machine environments (i.e. a function or   *)
-(*   a fixpoint)                                                          *)
-(*                                                                        *)
-(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ]            *)
-(*   - representation of [accu] : tag_[....]                              *)
-(*     -- tag <= 3 : encoding atom type (sorts, free vars, etc.)          *)
-(*     -- 10_[accu|proj name] : a projection blocked by an accu           *)
-(*     -- 11_[accu|fix_app] : a fixpoint blocked by an accu               *)
-(*     -- 12_[accu|vswitch] : a match blocked by an accu                  *)
-(*     -- 13_[fcofix]       : a cofix function                            *)
-(*     -- 14_[fcofix|val]   : a cofix function, val represent the value   *)
-(*        of the function applied to arg1 ... argn                        *)
-(* The [arguments] type, which is abstracted as an array, represents :    *)
-(*          tag[ _ | _ |v1|... | vn]                                      *)
-(* Generally the first field is a code pointer.                           *)
-
-(* Do not edit this type without editing C code, especially "coq_values.h" *)
-
-type atom =
-  | Aid of Vars.id_key
-  | Aind of inductive
-  | Atype of Univ.Universe.t
-
-(* Zippers *)
-
-type zipper =
-  | Zapp of arguments
-  | Zfix of vfix*arguments  (* Possibly empty *)
-  | Zswitch of vswitch
-  | Zproj of Constant.t (* name of the projection *)
-
-type stack = zipper list
-
-type to_up = values
-
-type whd =
-  | Vsort of Sorts.t
-  | Vprod of vprod
-  | Vfun of vfun
-  | Vfix of vfix * arguments option
-  | Vcofix of vcofix * to_up * arguments option
-  | Vconstr_const of int
-  | Vconstr_block of vblock
-  | Vatom_stk of atom * stack
-  | Vuniv_level of Univ.Level.t
 
 (************************************************)
 (* Abstract machine *****************************)
@@ -178,389 +44,72 @@ external push_vstack : vstack -> int -> unit = "coq_push_vstack"
 external interprete : tcode -> values -> vm_env -> int -> values =
   "coq_interprete_ml"
 
-
-
 (* Functions over arguments *)
-let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
-let arg args i =
-  if  0 <= i && i < (nargs args) then
-    val_of_obj (Obj.field (Obj.repr args) (i+2))
-  else invalid_arg
-		("Vm.arg size = "^(string_of_int (nargs args))^
-		 " acces "^(string_of_int i))
 
 (* Apply a value to arguments contained in [vargs] *)
 let apply_arguments vf vargs =
   let n = nargs vargs in
-  if Int.equal n 0 then vf
+  if Int.equal n 0 then fun_val vf
   else
    begin
      push_ra stop;
      push_arguments vargs;
-     interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
+     interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1)
    end
 
 (* Apply value [vf] to an array of argument values [varray] *)
 let apply_varray vf varray =
   let n = Array.length varray in
-  if Int.equal n 0 then vf
+  if Int.equal n 0 then fun_val vf
   else
     begin
       push_ra stop;
       (* The fun code of [vf] will make sure we have enough stack, so we put 0
          here. *)
       push_vstack varray 0;
-      interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
+      interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1)
     end
 
-(*************************************************)
-(* Destructors ***********************************)
-(*************************************************)
-
-let uni_lvl_val (v : values) : Univ.Level.t =
-    let whd = Obj.magic v in
-    match whd with
-    | Vuniv_level lvl -> lvl
-    | _ ->
-      let pr =
-        let open Pp in
-        match whd with
-        | Vsort _ -> str "Vsort"
-        | Vprod _ -> str "Vprod"
-        | Vfun _ -> str "Vfun"
-        | Vfix _ -> str "Vfix"
-        | Vcofix _ -> str "Vcofix"
-        | Vconstr_const i -> str "Vconstr_const"
-        | Vconstr_block b -> str "Vconstr_block"
-        | Vatom_stk (a,stk) -> str "Vatom_stk"
-        | _ -> assert false
-      in
-      CErrors.anomaly
-        Pp.(   strbrk "Parsing virtual machine value expected universe level, got "
-            ++ pr ++ str ".")
-
-let rec whd_accu a stk =
-  let stk =
-    if Int.equal (Obj.size a) 2 then stk
-    else Zapp (Obj.obj a) :: stk in
-  let at = Obj.field a 1 in
-  match Obj.tag at with
-  | i when Int.equal i type_atom_tag ->
-     begin match stk with
-     | [Zapp args] ->
-	let u = ref (Obj.obj (Obj.field at 0)) in
-	for i = 0 to nargs args - 1 do
-	  u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i)))
-	done;
-	Vsort (Type !u)
-     | _ -> assert false
-     end
-  | i when i <= max_atom_tag ->
-      Vatom_stk(Obj.magic at, stk)
-  | i when Int.equal i proj_tag ->
-     let zproj = Zproj (Obj.obj (Obj.field at 0)) in
-     whd_accu (Obj.field at 1) (zproj :: stk)
-  | i when Int.equal i fix_app_tag ->
-      let fa = Obj.field at 1 in
-      let zfix  =
-	Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
-      whd_accu (Obj.field at 0) (zfix :: stk)
-  | i when Int.equal i switch_tag ->
-      let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
-      whd_accu (Obj.field at 0) (zswitch :: stk)
-  | i when Int.equal i cofix_tag ->
-      let vcfx = Obj.obj (Obj.field at 0) in
-      let to_up = Obj.obj a in
-      begin match stk with
-      | []          -> Vcofix(vcfx, to_up, None)
-      | [Zapp args] -> Vcofix(vcfx, to_up, Some args)
-      | _           -> assert false
-      end
-  | i when Int.equal i cofix_evaluated_tag ->
-      let vcofix = Obj.obj (Obj.field at 0) in
-      let res = Obj.obj a in
-      begin match stk with
-      | []          -> Vcofix(vcofix, res, None)
-      | [Zapp args] -> Vcofix(vcofix, res, Some args)
-      | _           -> assert false
-      end
-  | tg ->
-    CErrors.anomaly
-      Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".")
-
-external kind_of_closure : Obj.t -> int = "coq_kind_of_closure"
-
-let whd_val : values -> whd =
-  fun v ->
-    let o = Obj.repr v in
-    if Obj.is_int o then Vconstr_const (Obj.obj o)
-    else
-      let tag = Obj.tag o in
-      if tag = accu_tag then
-	(
-	if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *)
-        else
-	  if is_accumulate (fun_code o) then whd_accu o []
-	  else Vprod(Obj.obj o))
-      else
-	if tag = Obj.closure_tag || tag = Obj.infix_tag then
-	  (match kind_of_closure o with
-	   | 0 -> Vfun(Obj.obj o)
-	   | 1 -> Vfix(Obj.obj o, None)
-	   | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
-	   | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
-	   | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work."))
-	else
-           Vconstr_block(Obj.obj o)
-
-(**********************************************)
-(* Constructors *******************************)
-(**********************************************)
-
-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);
-    Obj.set_field res 1 (Obj.repr a);
-    res
-
-(* obj_of_str_const : structured_constant -> Obj.t *)
-let rec obj_of_str_const str =
-  match str with
-  | Const_sorts s -> Obj.repr (Vsort 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_type u -> obj_of_atom (Atype u)
-
-let val_of_obj o = ((Obj.obj o) : values)
-
-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 atom_of_proj kn v =
-  let r = Obj.new_block proj_tag 2 in
-  Obj.set_field r 0 (Obj.repr kn);
-  Obj.set_field r 1 (Obj.repr v);
-  ((Obj.obj r) : atom)
-
-let val_of_proj kn v =
-  val_of_atom (atom_of_proj kn v)
-
-module IdKeyHash =
-struct
-  type t = Constant.t tableKey
-  let equal = Names.eq_table_key Constant.equal
-  open Hashset.Combine
-  let hash = function
-  | ConstKey c -> combinesmall 1 (Constant.hash c)
-  | VarKey id -> combinesmall 2 (Id.hash id)
-  | RelKey i -> combinesmall 3 (Int.hash i)
-end
-
-module KeyTable = Hashtbl.Make(IdKeyHash)
-
-let idkey_tbl = KeyTable.create 31
-
-let val_of_idkey key =
-  try KeyTable.find idkey_tbl key
-  with Not_found ->
-    let v = val_of_atom (Aid key) in
-    KeyTable.add idkey_tbl key v;
-    v
-
-let val_of_rel k = val_of_idkey (RelKey k)
-
-let val_of_named id = val_of_idkey (VarKey id)
-
-let val_of_constant c = val_of_idkey (ConstKey c)
-
-external val_of_annot_switch : annot_switch -> values = "%identity"
-
+(* Functions over vfun *)
 let mkrel_vstack k arity =
   let max = k + arity - 1 in
   Array.init arity (fun i -> val_of_rel (max - i))
 
-
-(*************************************************)
-(** Operations manipulating data types ***********)
-(*************************************************)
-
-(* Functions over products *)
-
-let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0)
-let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1))
-
-(* Functions over vfun *)
-
-external closure_arity : vfun -> int = "coq_closure_arity"
-
-let body_of_vfun k vf =
+let reduce_fun k vf =
   let vargs = mkrel_vstack k 1 in
-  apply_varray (Obj.magic vf) vargs
+  apply_varray vf vargs
 
 let decompose_vfun2 k vf1 vf2 =
   let arity = min (closure_arity vf1) (closure_arity vf2) in
   assert (0 < arity && arity < Sys.max_array_length);
   let vargs = mkrel_vstack k arity in
-  let v1 = apply_varray (Obj.magic vf1) vargs in
-  let v2 = apply_varray (Obj.magic vf2) vargs in
+  let v1 = apply_varray vf1 vargs in
+  let v2 = apply_varray vf2 vargs in
   arity, v1, v2
 
-(* Functions over fixpoint *)
-
-let first o = (offset_closure o (offset o))
-let last o = (Obj.field o (Obj.size o - 1))
-
-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_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1
-
-let rec_args vf =
-  let fb = first (Obj.repr vf) in
-  let size = Obj.size (last fb) in
-  Array.init size (unsafe_rec_arg fb)
-
-exception FALSE
-
-let check_fix f1 f2 =
-  let i1, i2 = current_fix f1, current_fix f2 in
-  (* Checking starting point *)
-  if i1 = i2 then
-    let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in
-    let n = Obj.size (last fb1) in
-    (* Checking number of definitions *)
-    if n = Obj.size (last fb2) then
-      (* Checking recursive arguments *)
-      try
-	for i = 0 to n - 1 do
-	  if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i
-	  then raise FALSE
-	done;
-	true
-      with FALSE -> false
-    else false
-  else false
-
 (* Functions over vfix *)
-external atom_rel : unit -> atom array = "get_coq_atom_tbl"
-external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl"
-
-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;
-  ref (Array.init len mkAccuCode)
-
-let relaccu_code i =
-  let len = Array.length !relaccu_tbl in
-  if i < len then !relaccu_tbl.(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;
-      relaccu_tbl :=
-	Array.init nl
-	  (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j);
-      !relaccu_tbl.(i)
-    end
 
 let reduce_fix k vf =
-  let fb = first (Obj.repr vf) in
+  let fb = first_fix vf in
   (* computing types *)
-  let fc_typ = ((Obj.obj (last fb)) : tcode array) in
+  let fc_typ = fix_types fb in
   let ndef = Array.length fc_typ in
-  let et = offset_closure fb (2*(ndef - 1)) in
+  let et = offset_closure_fix fb (2*(ndef - 1)) in
   let ftyp =
     Array.map
-      (fun c -> interprete c crazy_val (Obj.magic et) 0) fc_typ in
+      (fun c -> interprete c crazy_val et 0) fc_typ in
   (* Construction of the environment of fix bodies *)
-  let e = Obj.dup fb in
-  for i = 0 to ndef - 1 do
-    Obj.set_field e (2 * i) (Obj.repr (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 res = Obj.new_block Obj.closure_tag 2 in
-    Obj.set_field res 0 (Obj.repr c);
-    Obj.set_field res 1 (offset_closure e (2*i));
-    ((Obj.obj res) : vfun)  in
-  (Array.init ndef fix_body, ftyp)
-
-(* Functions over vcofix *)
-
-let get_fcofix vcf i =
-  match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with
-  | Vcofix(vcfi, _, _) -> vcfi
-  | _ -> assert false
-
-let current_cofix vcf =
-  let ndef = Obj.size (last (Obj.repr vcf)) in
-  let rec find_cofix pos =
-    if pos < ndef then
-      if get_fcofix vcf pos == vcf then pos
-      else find_cofix (pos+1)
-    else raise Not_found in
-  try find_cofix 0
-  with Not_found -> assert false
-
-let check_cofix vcf1 vcf2 =
-  (current_cofix vcf1 = current_cofix vcf2) &&
-  (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2)))
+  (mk_fix_body k ndef fb, ftyp)
 
 let reduce_cofix k vcf =
-  let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in
+  let fc_typ = cofix_types vcf in
   let ndef = Array.length fc_typ in
   let ftyp =
     (* Evaluate types *)
-    Array.map (fun c -> interprete c crazy_val (Obj.magic vcf) 0) fc_typ in
+    Array.map (fun c -> interprete c crazy_val (cofix_env vcf) 0) fc_typ in
 
   (* Construction of the environment of cofix bodies *)
-  let e = Obj.dup (Obj.repr vcf) in
-  for i = 0 to ndef - 1 do
-    Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i)))
-  done;
-
-  let cofix_body i =
-    let vcfi = get_fcofix vcf i in
-    let c = Obj.field (Obj.repr vcfi) 0 in
-    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);
-    Obj.set_field self 1 (Obj.repr atom);
-    apply_varray (Obj.obj e) [|Obj.obj self|] in
-  (Array.init ndef cofix_body, ftyp)
-
-
-(* Functions over vblock *)
-
-let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b)
-let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b)
-let bfield b i =
-  if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i)
-  else invalid_arg "Vm.bfield"
-
-
-(* Functions over vswitch *)
-
-let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl
-
-let case_info sw = sw.sw_annot.ci
+  (mk_cofix_body apply_varray k ndef vcf, ftyp)
 
 let type_of_switch sw =
   (* The fun code of types will make sure we have enough stack, so we put 0
@@ -568,20 +117,6 @@ let type_of_switch sw =
   push_vstack sw.sw_stk 0;
   interprete sw.sw_type_code crazy_val sw.sw_env 0
 
-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
-      else
-        let b = Obj.new_block last_variant_tag (arity+1) in
-        Obj.set_field b 0 (Obj.repr (tag-last_variant_tag));
-        b,1 in
-    for i = ofs to ofs + arity - 1 do
-      Obj.set_field b i (Obj.repr (val_of_rel (k+i)))
-    done;
-    val_of_obj b
-
 let apply_switch sw arg =
   let tc = sw.sw_annot.tailcall in
   if tc then
@@ -603,8 +138,8 @@ let branch_of_switch k sw =
 (* t = a stk --> t v *)
 let rec apply_stack a stk v =
   match stk with
-  | [] -> apply_varray a [|v|]
-  | Zapp args :: stk -> apply_stack (apply_arguments a args) stk v
+  | [] -> apply_varray (fun_of_val a) [|v|]
+  | Zapp args :: stk -> apply_stack (apply_arguments (fun_of_val a) args) stk v
   | Zproj kn :: stk -> apply_stack (val_of_proj kn a) stk v
   | Zfix(f,args) :: stk ->
       let a,stk = 
@@ -615,7 +150,7 @@ let rec apply_stack a stk v =
 	    push_val a;
 	    push_arguments args;
 	    let a =
-	      interprete (fun_code f) (Obj.magic f) (Obj.magic f)
+              interprete (fix_code f) (fix_val f) (fix_env f)
 		(nargs args+ nargs args') in
 	    a, stk
 	| _ -> 
@@ -623,7 +158,7 @@ let rec apply_stack a stk v =
 	    push_val a;
 	    push_arguments args;
 	    let a =
-	      interprete (fun_code f) (Obj.magic f) (Obj.magic f)
+              interprete (fix_code f) (fix_val f) (fix_env f)
 		(nargs args) in
 	    a, stk in
       apply_stack a stk v
@@ -634,50 +169,21 @@ let apply_whd k whd =
   let v = val_of_rel k in
   match whd with
   | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false
-  | Vfun f -> body_of_vfun k f
+  | Vfun f -> reduce_fun k f
   | Vfix(f, None) -> 
       push_ra stop;
       push_val v;
-      interprete (fun_code f) (Obj.magic f) (Obj.magic f) 0
+      interprete (fix_code f) (fix_val f) (fix_env f) 0
   | Vfix(f, Some args) ->
       push_ra stop;
       push_val v;
       push_arguments args;
-      interprete (fun_code f) (Obj.magic f) (Obj.magic f) (nargs args) 
+      interprete (fix_code f) (fix_val f) (fix_env f) (nargs args)
   | Vcofix(_,to_up,_) ->
       push_ra stop;
       push_val v;
-      interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0
+      interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0
   | Vatom_stk(a,stk) ->
       apply_stack (val_of_atom a) stk v 
   | Vuniv_level lvl -> assert false
 
-let rec pr_atom a =
-  Pp.(match a with
-  | Aid c -> str "Aid(" ++ (match c with
-                            | ConstKey c -> Constant.print c
-			    | RelKey i -> str "#" ++ int i
-			    | _ -> str "...") ++ str ")"
-  | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")"
-  | Atype _ -> str "Atype(")
-and pr_whd w =
-  Pp.(match w with
-  | Vsort _ -> str "Vsort"
-  | Vprod _ -> str "Vprod"
-  | Vfun _ -> str "Vfun"
-  | Vfix _ -> str "Vfix"
-  | Vcofix _ -> str "Vcofix"
-  | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")"
-  | Vconstr_block b -> str "Vconstr_block"
-  | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")"
-  | Vuniv_level _ -> assert false)
-and pr_stack stk =
-  Pp.(match stk with
-      | [] -> str "[]"
-      | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk)
-and pr_zipper z =
-  Pp.(match z with
-  | 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 ")")
diff --git a/kernel/vm.mli b/kernel/vm.mli
index bc38452d4..c6d92ba26 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -6,118 +6,28 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Constr
-open Cbytecodes
+open Vmvalues
 
 (** Debug printing *)
 
 val set_drawinstr : unit -> unit
 
-(** Machine code *)
-
-type tcode
-
-(** Values *)
-
-type vprod
-type vfun
-type vfix
-type vcofix
-type vblock
-type vswitch
-type arguments
-
-type atom =
-  | Aid of Vars.id_key
-  | Aind of inductive
-  | Atype of Univ.Universe.t
-
-(** Zippers *)
-
-type zipper =
-  | Zapp of arguments
-  | Zfix of vfix * arguments  (** might be empty *)
-  | Zswitch of vswitch
-  | Zproj of Constant.t (* name of the projection *)
-
-type stack = zipper list
-
-type to_up
-
-type whd =
-  | Vsort of Sorts.t
-  | Vprod of vprod
-  | Vfun of vfun
-  | Vfix of vfix * arguments option
-  | Vcofix of vcofix * to_up * arguments option
-  | Vconstr_const of int
-  | Vconstr_block of vblock
-  | Vatom_stk of atom * stack
-  | Vuniv_level of Univ.Level.t
-
-(** For debugging purposes only *)
-
-val pr_atom : atom -> Pp.t
-val pr_whd : whd -> Pp.t
-val pr_stack : stack -> Pp.t
-
-(** Constructors *)
-
-val val_of_str_const : structured_constant -> values
-val val_of_rel : int -> values
-val val_of_named : Id.t -> values
-val val_of_constant : Constant.t -> values
-
-external val_of_annot_switch : annot_switch -> values = "%identity"
-
-(** Destructors *)
-
-val whd_val : values -> whd
-val uni_lvl_val : values -> Univ.Level.t
-
-(** Arguments *)
-
-val nargs : arguments -> int
-val arg : arguments -> int -> values
-
-(** Product *)
-
-val dom : vprod -> values
-val codom : vprod -> vfun
-
-(** Function *)
-
-val body_of_vfun : int -> vfun -> values
-val decompose_vfun2  : int -> vfun -> vfun -> int * values * values
-
-(** Fix *)
-
-val current_fix : vfix -> int
-val check_fix : vfix -> vfix -> bool
-val rec_args : vfix -> int array
 val reduce_fix : int -> vfix -> vfun array * values array
                               (** bodies ,  types *)
 
-(** CoFix *)
-
-val current_cofix : vcofix -> int
-val check_cofix : vcofix -> vcofix -> bool
 val reduce_cofix : int -> vcofix -> values array * values array
                                       (** bodies , types *)
 
-(** Block *)
+val type_of_switch : vswitch -> values
 
-val btag  : vblock -> int
-val bsize : vblock -> int
-val bfield : vblock -> int -> values
+val branch_of_switch : int -> vswitch -> (int * values) array
 
-(** Switch *)
+val reduce_fun : int -> vfun -> values
 
-val check_switch : vswitch -> vswitch -> bool
-val case_info : vswitch -> case_info
-val type_of_switch : vswitch -> values
-val branch_of_switch : int -> vswitch -> (int * values) array
+(** [decompose_vfun2 k f1 f2] takes two functions [f1] and [f2] at current
+    DeBruijn level [k], with [n] lambdas in common, returns [n] and the reduced
+    bodies under those lambdas. *)
+val decompose_vfun2  : int -> vfun -> vfun -> int * values * values
 
 (** Apply a value *)
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
new file mode 100644
index 000000000..1102cdec1
--- /dev/null
+++ b/kernel/vmvalues.ml
@@ -0,0 +1,525 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+open Names
+open Sorts
+open Cbytecodes
+
+(*******************************************)
+(* Initalization of the abstract machine ***)
+(* Necessary for [relaccu_tbl]             *)
+(*******************************************)
+
+external init_vm : unit -> unit = "init_coq_vm"
+
+let _ = init_vm ()
+
+(******************************************************)
+(* Abstract data types and utility functions **********)
+(******************************************************)
+
+(* Values of the abstract machine *)
+type values
+let val_of_obj v = ((Obj.obj v):values)
+let crazy_val = (val_of_obj (Obj.repr 0))
+
+(* Abstract data *)
+type vprod
+type vfun
+type vfix
+type vcofix
+type vblock
+type arguments
+
+let fun_val v = (Obj.magic v : values)
+let fix_val v = (Obj.magic v : values)
+let cofix_upd_val v = (Obj.magic v : values)
+
+type vm_env
+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)
+let cofix_upd_env v = (Obj.magic v : vm_env)
+type vstack = values array
+
+let fun_of_val v = (Obj.magic v : vfun)
+
+(*******************************************)
+(* Machine code *** ************************)
+(*******************************************)
+
+type tcode
+
+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
+
+
+type vswitch = {
+    sw_type_code : tcode;
+    sw_code : tcode;
+    sw_annot : annot_switch;
+    sw_stk : vstack;
+    sw_env : vm_env
+  }
+
+(* Representation of values *)
+(* + Products : *)
+(*   -   vprod = 0_[ dom | codom]                                         *)
+(*             dom : values, codom : vfun                                 *)
+(*                                                                        *)
+(* + Functions have two representations :                                 *)
+(*   - unapplied fun :  vf = Ct_[ C | fv1 | ... | fvn]                    *)
+(*                                       C:tcode, fvi : values            *)
+(*     Remark : a function and its environment is the same value.         *)
+(*   - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn]       *)
+(*                                                                        *)
+(* + Fixpoints :                                                          *)
+(*   -        Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn]               *)
+(*     One single block to represent all of the fixpoints, each fixpoint  *)
+(*     is the pointer to the field holding the pointer to its code, and   *)
+(*     the infix tag is used to know where the block starts.              *)
+(*   - Partial application follows the scheme of partially applied        *)
+(*     functions. Note: only fixpoints not having been applied to its     *)
+(*     recursive argument are coded this way. When the rec. arg. is       *)
+(*     applied, either it's a constructor and the fix reduces, or it's    *)
+(*     and the fix is coded as an accumulator.                            *)
+(*                                                                        *)
+(* + Cofixpoints : see cbytegen.ml                                        *)
+(*                                                                        *)
+(* + vblock's encode (non constant) constructors as in Ocaml, but         *)
+(*   starting from 0 up. tag 0 ( = accu_tag) is reserved for              *)
+(*   accumulators.                                                        *)
+(*                                                                        *)
+(* + vm_env is the type of the machine environments (i.e. a function or   *)
+(*   a fixpoint)                                                          *)
+(*                                                                        *)
+(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ]            *)
+(*   - representation of [accu] : tag_[....]                              *)
+(*     -- tag <= 3 : encoding atom type (sorts, free vars, etc.)          *)
+(*     -- 10_[accu|proj name] : a projection blocked by an accu           *)
+(*     -- 11_[accu|fix_app] : a fixpoint blocked by an accu               *)
+(*     -- 12_[accu|vswitch] : a match blocked by an accu                  *)
+(*     -- 13_[fcofix]       : a cofix function                            *)
+(*     -- 14_[fcofix|val]   : a cofix function, val represent the value   *)
+(*        of the function applied to arg1 ... argn                        *)
+(* The [arguments] type, which is abstracted as an array, represents :    *)
+(*          tag[ _ | _ |v1|... | vn]                                      *)
+(* Generally the first field is a code pointer.                           *)
+
+(* Do not edit this type without editing C code, especially "coq_values.h" *)
+
+type atom =
+  | Aid of Vars.id_key
+  | Aind of inductive
+  | Atype of Univ.Universe.t
+
+(* Zippers *)
+
+type zipper =
+  | Zapp of arguments
+  | Zfix of vfix*arguments  (* Possibly empty *)
+  | Zswitch of vswitch
+  | Zproj of Constant.t (* name of the projection *)
+
+type stack = zipper list
+
+type to_update = values
+
+type whd =
+  | Vsort of Sorts.t
+  | Vprod of vprod
+  | Vfun of vfun
+  | Vfix of vfix * arguments option
+  | Vcofix of vcofix * to_update * arguments option
+  | Vconstr_const of int
+  | Vconstr_block of vblock
+  | Vatom_stk of atom * stack
+  | Vuniv_level of Univ.Level.t
+
+(* Functions over arguments *)
+let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
+let arg args i =
+  if  0 <= i && i < (nargs args) then
+    val_of_obj (Obj.field (Obj.repr args) (i+2))
+  else invalid_arg
+                ("Vm.arg size = "^(string_of_int (nargs args))^
+                 " acces "^(string_of_int i))
+
+(*************************************************)
+(* Destructors ***********************************)
+(*************************************************)
+
+let uni_lvl_val (v : values) : Univ.Level.t =
+    let whd = Obj.magic v in
+    match whd with
+    | Vuniv_level lvl -> lvl
+    | _ ->
+      let pr =
+        let open Pp in
+        match whd with
+        | Vsort _ -> str "Vsort"
+        | Vprod _ -> str "Vprod"
+        | Vfun _ -> str "Vfun"
+        | Vfix _ -> str "Vfix"
+        | Vcofix _ -> str "Vcofix"
+        | Vconstr_const i -> str "Vconstr_const"
+        | Vconstr_block b -> str "Vconstr_block"
+        | Vatom_stk (a,stk) -> str "Vatom_stk"
+        | _ -> assert false
+      in
+      CErrors.anomaly
+        Pp.(   strbrk "Parsing virtual machine value expected universe level, got "
+            ++ pr ++ str ".")
+
+let rec whd_accu a stk =
+  let stk =
+    if Int.equal (Obj.size a) 2 then stk
+    else Zapp (Obj.obj a) :: stk in
+  let at = Obj.field a 1 in
+  match Obj.tag at with
+  | i when Int.equal i type_atom_tag ->
+     begin match stk with
+     | [Zapp args] ->
+        let u = ref (Obj.obj (Obj.field at 0)) in
+        for i = 0 to nargs args - 1 do
+          u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i)))
+        done;
+        Vsort (Type !u)
+     | _ -> assert false
+     end
+  | i when i <= max_atom_tag ->
+      Vatom_stk(Obj.magic at, stk)
+  | i when Int.equal i proj_tag ->
+     let zproj = Zproj (Obj.obj (Obj.field at 0)) in
+     whd_accu (Obj.field at 1) (zproj :: stk)
+  | i when Int.equal i fix_app_tag ->
+      let fa = Obj.field at 1 in
+      let zfix  =
+        Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
+      whd_accu (Obj.field at 0) (zfix :: stk)
+  | i when Int.equal i switch_tag ->
+      let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
+      whd_accu (Obj.field at 0) (zswitch :: stk)
+  | i when Int.equal i cofix_tag ->
+      let vcfx = Obj.obj (Obj.field at 0) in
+      let to_up = Obj.obj a in
+      begin match stk with
+      | []          -> Vcofix(vcfx, to_up, None)
+      | [Zapp args] -> Vcofix(vcfx, to_up, Some args)
+      | _           -> assert false
+      end
+  | i when Int.equal i cofix_evaluated_tag ->
+      let vcofix = Obj.obj (Obj.field at 0) in
+      let res = Obj.obj a in
+      begin match stk with
+      | []          -> Vcofix(vcofix, res, None)
+      | [Zapp args] -> Vcofix(vcofix, res, Some args)
+      | _           -> assert false
+      end
+  | tg ->
+    CErrors.anomaly
+      Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".")
+
+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"
+let accumulate = accumulate ()
+
+let whd_val : values -> whd =
+  fun v ->
+    let o = Obj.repr v in
+    if Obj.is_int o then Vconstr_const (Obj.obj o)
+    else
+      let tag = Obj.tag o in
+      if tag = accu_tag then
+        (
+        if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *)
+        else
+          if is_accumulate (fun_code o) then whd_accu o []
+          else Vprod(Obj.obj o))
+      else
+        if tag = Obj.closure_tag || tag = Obj.infix_tag then
+          (match kind_of_closure o with
+           | 0 -> Vfun(Obj.obj o)
+           | 1 -> Vfix(Obj.obj o, None)
+           | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
+           | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
+           | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work."))
+        else
+           Vconstr_block(Obj.obj o)
+
+(**********************************************)
+(* Constructors *******************************)
+(**********************************************)
+
+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);
+    Obj.set_field res 1 (Obj.repr a);
+    res
+
+(* obj_of_str_const : structured_constant -> Obj.t *)
+let rec obj_of_str_const str =
+  match str with
+  | Const_sorts s -> Obj.repr (Vsort 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_type u -> obj_of_atom (Atype u)
+
+let val_of_obj o = ((Obj.obj o) : values)
+
+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 atom_of_proj kn v =
+  let r = Obj.new_block proj_tag 2 in
+  Obj.set_field r 0 (Obj.repr kn);
+  Obj.set_field r 1 (Obj.repr v);
+  ((Obj.obj r) : atom)
+
+let val_of_proj kn v =
+  val_of_atom (atom_of_proj kn v)
+
+module IdKeyHash =
+struct
+  type t = Constant.t tableKey
+  let equal = Names.eq_table_key Constant.equal
+  open Hashset.Combine
+  let hash = function
+  | ConstKey c -> combinesmall 1 (Constant.hash c)
+  | VarKey id -> combinesmall 2 (Id.hash id)
+  | RelKey i -> combinesmall 3 (Int.hash i)
+end
+
+module KeyTable = Hashtbl.Make(IdKeyHash)
+
+let idkey_tbl = KeyTable.create 31
+
+let val_of_idkey key =
+  try KeyTable.find idkey_tbl key
+  with Not_found ->
+    let v = val_of_atom (Aid key) in
+    KeyTable.add idkey_tbl key v;
+    v
+
+let val_of_rel k = val_of_idkey (RelKey k)
+
+let val_of_named id = val_of_idkey (VarKey id)
+
+let val_of_constant c = val_of_idkey (ConstKey c)
+
+external val_of_annot_switch : annot_switch -> values = "%identity"
+
+(*************************************************)
+(** Operations manipulating data types ***********)
+(*************************************************)
+
+(* Functions over products *)
+
+let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0)
+let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1))
+
+(* Functions over vfun *)
+
+external closure_arity : vfun -> int = "coq_closure_arity"
+
+(* Functions over fixpoint *)
+
+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"
+
+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 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_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1
+
+let rec_args vf =
+  let fb = first (Obj.repr vf) in
+  let size = Obj.size (last fb) in
+  Array.init size (unsafe_rec_arg fb)
+
+exception FALSE
+
+let check_fix f1 f2 =
+  let i1, i2 = current_fix f1, current_fix f2 in
+  (* Checking starting point *)
+  if i1 = i2 then
+    let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in
+    let n = Obj.size (last fb1) in
+    (* Checking number of definitions *)
+    if n = Obj.size (last fb2) then
+      (* Checking recursive arguments *)
+      try
+        for i = 0 to n - 1 do
+          if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i
+          then raise FALSE
+        done;
+        true
+      with FALSE -> false
+    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 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;
+  ref (Array.init len mkAccuCode)
+
+let relaccu_code i =
+  let len = Array.length !relaccu_tbl in
+  if i < len then !relaccu_tbl.(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;
+      relaccu_tbl :=
+        Array.init nl
+          (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j);
+      !relaccu_tbl.(i)
+    end
+
+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)))
+  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 res = Obj.new_block Obj.closure_tag 2 in
+    Obj.set_field res 0 (Obj.repr c);
+    Obj.set_field res 1 (offset_closure e (2*i));
+    ((Obj.obj res) : vfun)  in
+  Array.init ndef fix_body
+
+(* Functions over vcofix *)
+
+let get_fcofix vcf i =
+  match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with
+  | Vcofix(vcfi, _, _) -> vcfi
+  | _ -> assert false
+
+let current_cofix vcf =
+  let ndef = Obj.size (last (Obj.repr vcf)) in
+  let rec find_cofix pos =
+    if pos < ndef then
+      if get_fcofix vcf pos == vcf then pos
+      else find_cofix (pos+1)
+    else raise Not_found in
+  try find_cofix 0
+  with Not_found -> assert false
+
+let check_cofix vcf1 vcf2 =
+  (current_cofix vcf1 = current_cofix vcf2) &&
+  (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2)))
+
+let mk_cofix_body apply_varray k ndef vcf =
+  let e = Obj.dup (Obj.repr vcf) in
+  for i = 0 to ndef - 1 do
+    Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i)))
+  done;
+
+  let cofix_body i =
+    let vcfi = get_fcofix vcf i in
+    let c = Obj.field (Obj.repr vcfi) 0 in
+    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);
+    Obj.set_field self 1 (Obj.repr atom);
+    apply_varray (Obj.obj e) [|Obj.obj self|] in
+  Array.init ndef cofix_body
+
+(* Functions over vblock *)
+
+let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b)
+let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b)
+let bfield b i =
+  if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i)
+  else invalid_arg "Vm.bfield"
+
+
+(* Functions over vswitch *)
+
+let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl
+
+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
+      else
+        let b = Obj.new_block last_variant_tag (arity+1) in
+        Obj.set_field b 0 (Obj.repr (tag-last_variant_tag));
+        b,1 in
+    for i = ofs to ofs + arity - 1 do
+      Obj.set_field b i (Obj.repr (val_of_rel (k+i)))
+    done;
+    val_of_obj b
+
+(* Printing *)
+
+let rec pr_atom a =
+  Pp.(match a with
+  | Aid c -> str "Aid(" ++ (match c with
+                            | ConstKey c -> Constant.print c
+                            | RelKey i -> str "#" ++ int i
+                            | _ -> str "...") ++ str ")"
+  | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")"
+  | Atype _ -> str "Atype(")
+and pr_whd w =
+  Pp.(match w with
+  | Vsort _ -> str "Vsort"
+  | Vprod _ -> str "Vprod"
+  | Vfun _ -> str "Vfun"
+  | Vfix _ -> str "Vfix"
+  | Vcofix _ -> str "Vcofix"
+  | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")"
+  | Vconstr_block b -> str "Vconstr_block"
+  | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")"
+  | Vuniv_level _ -> assert false)
+and pr_stack stk =
+  Pp.(match stk with
+      | [] -> str "[]"
+      | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk)
+and pr_zipper z =
+  Pp.(match z with
+  | 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 ")")
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
new file mode 100644
index 000000000..350f71372
--- /dev/null
+++ b/kernel/vmvalues.mli
@@ -0,0 +1,144 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Cbytecodes
+
+(** Values *)
+
+type values
+type vm_env
+type vprod
+type vfun
+type vfix
+type vcofix
+type vblock
+type arguments
+type vstack = values array
+type to_update
+
+val fun_val : vfun -> values
+val fix_val : vfix -> values
+val cofix_upd_val : to_update -> values
+
+val fun_env : vfun -> vm_env
+val fix_env : vfix -> vm_env
+val cofix_env : vcofix -> vm_env
+val cofix_upd_env : to_update -> vm_env
+
+(** Cast a value known to be a function, unsafe in general *)
+val fun_of_val : values -> vfun
+
+val crazy_val : values
+
+(** Machine code *)
+
+type tcode
+
+type vswitch = {
+    sw_type_code : tcode;
+    sw_code : tcode;
+    sw_annot : annot_switch;
+    sw_stk : vstack;
+    sw_env : vm_env
+  }
+
+external mkAccuCode : int -> tcode = "coq_makeaccu"
+
+val fun_code : vfun -> tcode
+val fix_code : vfix -> tcode
+val cofix_upd_code : to_update -> tcode
+
+type atom =
+  | Aid of Vars.id_key
+  | Aind of inductive
+  | Atype of Univ.Universe.t
+
+(** Zippers *)
+
+type zipper =
+  | Zapp of arguments
+  | Zfix of vfix * arguments  (** might be empty *)
+  | Zswitch of vswitch
+  | Zproj of Constant.t (* name of the projection *)
+
+type stack = zipper list
+
+type whd =
+  | Vsort of Sorts.t
+  | Vprod of vprod
+  | Vfun of vfun
+  | Vfix of vfix * arguments option
+  | Vcofix of vcofix * to_update * arguments option
+  | Vconstr_const of int
+  | Vconstr_block of vblock
+  | Vatom_stk of atom * stack
+  | Vuniv_level of Univ.Level.t
+
+(** For debugging purposes only *)
+
+val pr_atom : atom -> Pp.t
+val pr_whd : whd -> Pp.t
+val pr_stack : stack -> Pp.t
+
+(** Constructors *)
+
+val val_of_str_const : structured_constant -> values
+val val_of_rel : int -> values
+val val_of_named : Id.t -> values
+val val_of_constant : Constant.t -> values
+val val_of_proj : Constant.t -> values -> values
+val val_of_atom : atom -> values
+
+external val_of_annot_switch : annot_switch -> values = "%identity"
+
+(** Destructors *)
+
+val whd_val : values -> whd
+val uni_lvl_val : values -> Univ.Level.t
+
+(** Arguments *)
+
+val nargs : arguments -> int
+val arg : arguments -> int -> values
+
+(** Product *)
+
+val dom : vprod -> values
+val codom : vprod -> vfun
+
+(** Fun *)
+external closure_arity : vfun -> int = "coq_closure_arity"
+
+(** Fix *)
+
+val current_fix : vfix -> int
+val check_fix : vfix -> vfix -> bool
+val rec_args : vfix -> int array
+val first_fix : vfix -> vfix
+val fix_types : vfix -> tcode array
+val cofix_types : vcofix -> tcode array
+external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure"
+val mk_fix_body : int -> int -> vfix -> vfun array
+
+(** CoFix *)
+
+val current_cofix : vcofix -> int
+val check_cofix : vcofix -> vcofix -> bool
+val mk_cofix_body : (vfun -> vstack -> values) -> int -> int -> vcofix -> values array
+
+(** Block *)
+
+val btag  : vblock -> int
+val bsize : vblock -> int
+val bfield : vblock -> int -> values
+
+(** Switch *)
+
+val check_switch : vswitch -> vswitch -> bool
+val branch_arg : int -> Cbytecodes.tag * int -> values
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index e395bdbc6..b21fbf0eb 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -15,6 +15,7 @@ open Vars
 open Environ
 open Inductive
 open Reduction
+open Vmvalues
 open Vm
 open Context.Rel.Declaration
 
@@ -134,7 +135,7 @@ let build_case_type dep p realargs c =
 
 (* La fonction de normalisation *)
 
-let rec nf_val env sigma v t = nf_whd env sigma (whd_val v) t
+let rec nf_val env sigma v t = nf_whd env sigma (Vmvalues.whd_val v) t
 
 and nf_vtype env sigma v =  nf_val env sigma v crazy_type
 
@@ -144,7 +145,7 @@ and nf_whd env sigma whd typ =
   | Vprod p ->
       let dom = nf_vtype env sigma (dom p) in
       let name = Name (Id.of_string "x") in
-      let vc = body_of_vfun (nb_rel env) (codom p) in
+      let vc = reduce_fun (nb_rel env) (codom p) in
       let codom = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vc  in
       mkProd(name,dom,codom)
   | Vfun f -> nf_fun env sigma f typ
@@ -191,7 +192,7 @@ and nf_univ_args ~nb_univs mk env sigma stk =
     else match stk with
     | Zapp args :: _ ->
        let inst =
-	 Array.init nb_univs (fun i -> Vm.uni_lvl_val (arg args i))
+         Array.init nb_univs (fun i -> uni_lvl_val (arg args i))
        in
        Univ.Instance.of_array inst
     | _ -> assert false
@@ -254,7 +255,7 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type dep p realargs c in
-      let ci = case_info sw in
+      let ci = sw.sw_annot.Cbytecodes.ci in
       nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk
   | Zproj p :: stk ->
      assert (from = 0) ;
@@ -266,14 +267,14 @@ and nf_predicate env sigma ind mip params v pT =
   match whd_val v, kind pT with
   | Vfun f, Prod _ ->
       let k = nb_rel env in
-      let vb = body_of_vfun k f in
+      let vb = reduce_fun k f in
       let name,dom,codom = decompose_prod env pT in
       let dep,body =
 	nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
       dep, mkLambda(name,dom,body)
   | Vfun f, _ ->
       let k = nb_rel env in
-      let vb = body_of_vfun k f in
+      let vb = reduce_fun k f in
       let name = Name (Id.of_string "c") in
       let n = mip.mind_nrealargs in
       let rargs = Array.init n (fun i -> mkRel (n-i)) in
@@ -307,7 +308,7 @@ and nf_bargs env sigma b ofs t =
 
 and nf_fun env sigma f typ =
   let k = nb_rel env in
-  let vb = body_of_vfun k f in
+  let vb = reduce_fun k f in
   let name,dom,codom =
     try decompose_prod env typ
     with DestKO ->