Safer VM interfaces

We separate functions dealing with VM values (vmvalues.ml) and
interfaces of the bytecode interpreter (vm.ml). Only the former relies
on untyped constructions.

This also makes the VM architecture closer to the one of native_compute,
another patch could probably try to share more code between the two for
conversion and reification (not trivial, though).

This is also preliminary work for integers and arrays.

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 ->