New IR in VM: Clambda.

This intermediate representation serves two purposes:
1- It is a preliminary step for primitive machine integers, as iterators
will be compiled to Clambda.
2- It makes the VM compilation passes closer to the ones of
native_compute. Once we unifiy the representation of values, we should
be able to factorize the lambda-code generation between the two
compilers, as well as the reification code.

This code was written by Benjamin Grégoire and myself.

15 files changed, 1198 insertions, 521 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 6d91c3ec9..aa6c49bc7 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -350,16 +350,3 @@ and pp_bytecodes c =
       pp_bytecodes l1 ++ pp_bytecodes l2 ++  pp_bytecodes c
   | i :: c ->
       pp_instr i ++ fnl () ++ pp_bytecodes c
-
-(*spiwack: moved this type in this file  because I needed it for
-  retroknowledge which can't depend from cbytegen *)
-type block =
-  | Bconstr of constr
-  | Bstrconst of structured_constant
-  | Bmakeblock of int * block array
-  | Bconstruct_app of int * int * int * block array
-                  (* tag , nparams, arity *)
-  | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
-                (* spiwack: compilation given by a function *)
-                (* compilation function (see get_vm_constant_dynamic_info in
-                   retroknowledge.mli for more info) , argument array  *)
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index bf2e462e8..c8fbb27a9 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -171,14 +171,3 @@ type comp_env = {
 
 val pp_bytecodes : bytecodes -> Pp.t
 val pp_fv_elem : fv_elem -> Pp.t
-
-(*spiwack: moved this here because I needed it for retroknowledge *)
-type block =
-  | Bconstr of constr
-  | Bstrconst of structured_constant
-  | Bmakeblock of int * block array
-  | Bconstruct_app of int * int * int * block array
-                  (** tag , nparams, arity *)
-  | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
-                (** compilation function (see get_vm_constant_dynamic_info in
-                   retroknowledge.mli for more info) , argument array  *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 4a34dbcff..3104d5751 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -14,6 +14,8 @@ open Util
 open Names
 open Cbytecodes
 open Cemitcodes
+open Cinstr
+open Clambda
 open Constr
 open Declarations
 open Pre_env
@@ -96,7 +98,7 @@ module Config = struct
   let stack_safety_margin = 15
 end
 
-type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t
+type argument = ArgLambda of lambda | ArgUniv of Univ.Level.t
 
 let empty_fv = { size= 0;  fv_rev = []; fv_fwd = FvMap.empty }
 let push_fv d e = {
@@ -356,13 +358,6 @@ let cont_cofix arity =
     Kreturn (arity+2) ]
 
 
-(*i Global environment *)
-
-let global_env = ref empty_env
-
-let set_global_env env = global_env := env
-
-
 (* Code of closures *)
 let fun_code = ref []
 
@@ -370,31 +365,8 @@ let init_fun_code () = fun_code := []
 
 (* Compilation of constructors and inductive types *)
 
-
-(* Limitation due to OCaml's representation of non-constant
-  constructors: limited to 245 + 1 (0 tag) cases. *)
-
-exception TooLargeInductive of Id.t
-
-let max_nb_const = 0x1000000 
-let max_nb_block = 0x1000000 + last_variant_tag - 1
-
-let str_max_constructors = 
-  Format.sprintf 
-    " which has more than %i constant constructors or more than %i non-constant constructors" max_nb_const max_nb_block
-
-let check_compilable ib = 
-  
-  if not (ib.mind_nb_args <= max_nb_block && ib.mind_nb_constant <= max_nb_const) then 
-    raise (TooLargeInductive ib.mind_typename)
-
 (* Inv: arity > 0 *)
 
-let const_bn tag args = 
-  if tag < last_variant_tag then Const_bn(tag, args)
-  else
-    Const_bn(last_variant_tag, Array.append [|Const_b0 (tag - last_variant_tag) |] args)
-
 (*
 If [tag] hits the OCaml limitation for non constant constructors, we switch to
 another representation for the remaining constructors:
@@ -415,126 +387,9 @@ let code_makeblock ~stack_size ~arity ~tag cont =
     Kpush :: nest_block tag arity cont
   end
 
-(* [code_construct] compiles an abstracted constructor dropping parameters and
-   updates [fun_code] *)
-(* Inv : nparam + arity > 0 *)
-let code_construct tag nparams arity cont =
-  let f_cont =
-      add_pop nparams
-      (if Int.equal arity 0 then
-	[Kconst (Const_b0 tag); Kreturn 0]
-       else if tag < last_variant_tag then
-         [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0]
-       else
-         nest_block tag arity [Kreturn 0])
-    in
-    let lbl = Label.create() in
-    (* No need to grow the stack here, as the function does not push stuff. *)
-    fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)];
-    Kclosure(lbl,0) :: cont
-
-let get_strcst = function
-  | Bstrconst sc -> sc
-  | _ -> raise Not_found
-
-let rec str_const c =
-  match kind c with
-  | Sort s -> Bstrconst (Const_sorts s)
-  | Cast(c,_,_) -> str_const c
-  | App(f,args) ->
-      begin
-	match kind f with
-	| Construct(((kn,j),i),u) -> 
-            begin
-	    let oib = lookup_mind kn !global_env in
-	    let oip = oib.mind_packets.(j) in
-	    let () = check_compilable oip in
-	    let tag,arity = oip.mind_reloc_tbl.(i-1) in
-	    let nparams = oib.mind_nparams in
-	    if Int.equal (nparams + arity) (Array.length args) then
-              (* spiwack: *)
-              (* 1/ tries to compile the constructor in an optimal way,
-                    it is supposed to work only if the arguments are
-                    all fully constructed, fails with Cbytecodes.NotClosed.
-                    it can also raise Not_found when there is no special
-                    treatment for this constructor
-                    for instance: tries to to compile an integer of the
-                        form I31 D1 D2 ... D31 to [D1D2...D31] as
-                        a processor number (a caml number actually) *)
-              try
-		try
-		  Bstrconst (Retroknowledge.get_vm_constant_static_info
-                                              (!global_env).retroknowledge
-                                              f args)
-                with NotClosed ->
-		  (* 2/ if the arguments are not all closed (this is
-                        expectingly (and it is currently the case) the only
-                        reason why this exception is raised) tries to
-                        give a clever, run-time behavior to the constructor.
-                        Raises Not_found if there is no special treatment
-                        for this integer.
-                        this is done in a lazy fashion, using the constructor
-                        Bspecial because it needs to know the continuation
-                        and such, which can't be done at this time.
-                        for instance, for int31: if one of the digit is
-                            not closed, it's not impossible that the number
-                            gets fully instanciated at run-time, thus to ensure
-                            uniqueness of the representation in the vm
-                            it is necessary to try and build a caml integer
-                            during the execution *)
-		  let rargs = Array.sub args nparams arity in
-		  let b_args = Array.map str_const rargs in
-		  Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
-                                           (!global_env).retroknowledge
-                                           f),
-                           b_args)
-              with Not_found ->
-		(* 3/ if no special behavior is available, then the compiler
-		      falls back to the normal behavior *)
-		if Int.equal arity 0 then Bstrconst(Const_b0 tag)
-		else
-		  let rargs = Array.sub args nparams arity in
-		  let b_args = Array.map str_const rargs in
-		  try
-		    let sc_args = Array.map get_strcst b_args in
-		    Bstrconst(const_bn tag sc_args)
-		  with Not_found ->
-		    Bmakeblock(tag,b_args)
-	    else
-              let b_args = Array.map str_const args in
-	     (* spiwack: tries first to apply the run-time compilation
-                behavior of the constructor, as in 2/ above *)
-	      try
-		Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
-                                           (!global_env).retroknowledge
-                                           f),
-                         b_args)
-	      with Not_found ->
-	        Bconstruct_app(tag, nparams, arity, b_args)
-              end
-	| _ -> Bconstr c
-      end
-  | Ind (ind,u) when Univ.Instance.is_empty u ->
-    Bstrconst (Const_ind ind)
-  | Construct (((kn,j),i),_) ->
-      begin
-      (* spiwack: tries first to apply the run-time compilation
-           behavior of the constructor, as in 2/ above *)
-      try
-	Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
-                                           (!global_env).retroknowledge
-                                           c),
-                         [| |])
-      with Not_found ->
-	let oib = lookup_mind kn !global_env in
-	let oip = oib.mind_packets.(j) in
-	let () = check_compilable oip in
-	let num,arity = oip.mind_reloc_tbl.(i-1) in
-	let nparams = oib.mind_nparams in
-	if Int.equal (nparams + arity) 0 then Bstrconst(Const_b0 num)
-	else Bconstruct_app(num,nparams,arity,[||])
-      end
-  | _ -> Bconstr c
+let compile_structured_constant reloc sc sz cont =
+  set_max_stack_size sz;
+  Kconst sc :: cont
 
 (* compiling application *)
 let comp_args comp_expr reloc args sz cont =
@@ -545,9 +400,10 @@ let comp_args comp_expr reloc args sz cont =
   done;
   !c
 
-(* Precondition: args not empty *)
 let comp_app comp_fun comp_arg reloc f args sz cont =
   let nargs = Array.length args in
+  if Int.equal nargs 0 then comp_fun reloc f sz cont
+  else
   match is_tailcall cont with
   | Some k ->
       comp_args comp_arg reloc args sz
@@ -593,37 +449,39 @@ let rec get_alias env kn =
 	| BCalias kn' -> get_alias env kn'
 	| _ -> kn)
 
+(* spiwack: additional function which allow different part of compilation of the
+      31-bit integers *)
+
+let make_areconst n else_lbl cont =
+  if n <= 0 then
+    cont
+  else
+    Kareconst (n, else_lbl)::cont
+
 (* sz is the size of the local stack *)
-let rec compile_constr reloc c sz cont =
+let rec compile_lam env reloc lam sz cont =
   set_max_stack_size sz;
-  match kind c with
-  | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta"
-  | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
-  | Proj (p,c) ->
-     let kn = Projection.constant p in
-     let cb = lookup_constant kn !global_env in
-     let pb = Option.get cb.const_proj in
-     let n = pb.proj_arg in
-     compile_constr reloc c sz (Kproj (n,kn) :: cont)
-
-  | Cast(c,_,_) -> compile_constr reloc c sz cont
-
-  | Rel i -> pos_rel i reloc sz :: cont
-  | Var id -> pos_named id reloc :: cont
-  | Const (kn,u) -> compile_const reloc kn u [||] sz cont
-  | Ind (ind,u) ->
-     let bcst = Bstrconst (Const_ind ind) in
+  match lam with
+  | Lrel(_, i) -> pos_rel i reloc sz :: cont
+
+  | Lval v -> compile_structured_constant reloc v sz cont
+
+  | Lproj (n,kn,arg) ->
+     compile_lam env reloc arg sz (Kproj (n,kn) :: cont)
+
+  | Lvar id -> pos_named id reloc :: cont
+
+  | Lconst (kn,u) -> compile_constant env reloc kn u [||] sz cont
+
+  | Lind (ind,u) ->
     if Univ.Instance.is_empty u then
-      compile_str_cst reloc bcst sz cont
-    else
-      comp_app compile_str_cst compile_universe reloc
-	   bcst
-	   (Univ.Instance.to_array u)
-	   sz
-	   cont
-  | Sort (Sorts.Prop _) | Construct _ ->
-      compile_str_cst reloc (str_const c) sz cont
-  | Sort (Sorts.Type u) ->
+      compile_structured_constant reloc (Const_ind ind) sz cont
+    else comp_app compile_structured_constant compile_universe reloc
+        (Const_ind ind) (Univ.Instance.to_array u) sz cont
+
+  | Lsort (Sorts.Prop _ as s) ->
+    compile_structured_constant reloc (Const_sorts s) sz cont
+  | Lsort (Sorts.Type u) ->
      (* We separate global and local universes in [u]. The former will be part
         of the structured constant, while the later (if any) will be applied as
         arguments. *)
@@ -631,64 +489,65 @@ let rec compile_constr reloc c sz cont =
       let u,s = Universe.compact u in
       (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *)
       if List.is_empty s then
-        compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type u))) sz cont
+        compile_structured_constant reloc (Const_sorts (Sorts.Type u)) sz cont
       else
 	let compile_get_univ reloc idx sz cont =
           set_max_stack_size sz;
 	  compile_fv_elem reloc (FVuniv_var idx) sz cont
 	in
-        comp_app compile_str_cst compile_get_univ reloc
-          (Bstrconst (Const_type u)) (Array.of_list s) sz cont
+        comp_app compile_structured_constant compile_get_univ reloc
+          (Const_type u) (Array.of_list s) sz cont
     end
-  | LetIn(_,xb,_,body) ->
-      compile_constr reloc xb sz
-	(Kpush ::
-	(compile_constr (push_local sz reloc) body (sz+1) (add_pop 1 cont)))
-  | Prod(id,dom,codom) ->
-      let cont1 =
-	Kpush :: compile_constr reloc dom (sz+1) (Kmakeprod :: cont) in
-      compile_constr reloc (mkLambda(id,dom,codom)) sz cont1
-  | Lambda _ ->
-      let params, body = Term.decompose_lam c in
-      let arity = List.length params in
-      let r_fun = comp_env_fun arity in
-      let lbl_fun = Label.create() in
-      let cont_fun =
-        ensure_stack_capacity (compile_constr r_fun body arity) [Kreturn arity]
-      in
-      fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)];
-      let fv = fv r_fun in
-      compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont)
-
-  | App(f,args) ->
-      begin
-	match kind f with
-	| Construct _ -> compile_str_cst reloc (str_const c) sz cont
-        | Const (kn,u) -> compile_const reloc kn u args sz cont
-	| _ -> comp_app compile_constr compile_constr reloc f args sz cont
-      end
-  | Fix ((rec_args,init),(_,type_bodies,rec_bodies)) ->
-      let ndef = Array.length type_bodies in
+
+  | Llet (id,def,body) ->
+      compile_lam env reloc def sz
+        (Kpush ::
+         compile_lam env (push_local sz reloc) body (sz+1) (add_pop 1 cont))
+
+  | Lprod (dom,codom) ->
+     let cont1 =
+       Kpush :: compile_lam env reloc dom (sz+1) (Kmakeprod :: cont) in
+     compile_lam env reloc codom sz cont1
+
+  | Llam (ids,body) ->
+     let arity = Array.length ids in
+     let r_fun = comp_env_fun arity in
+     let lbl_fun = Label.create() in
+     let cont_fun =
+       ensure_stack_capacity (compile_lam env r_fun body arity) [Kreturn arity]
+     in
+     fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)];
+     let fv = fv r_fun in
+     compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont)
+
+  | Lapp (f, args) ->
+    begin match f with
+    | Lconst (kn,u) -> compile_constant env reloc kn u args sz cont
+    | _ -> comp_app (compile_lam env) (compile_lam env) reloc f args sz cont
+    end
+
+  | Lfix ((rec_args, init), (decl, types, bodies)) ->
+      let ndef = Array.length types in
       let rfv = ref empty_fv in
       let lbl_types = Array.make ndef Label.no in
       let lbl_bodies = Array.make ndef Label.no in
-      (* Compilation des types *)
+      (* Compiling types *)
       let env_type = comp_env_fix_type rfv in
       for i = 0 to ndef - 1 do
         let fcode =
-          ensure_stack_capacity (compile_constr env_type type_bodies.(i) 0) [Kstop]
+          ensure_stack_capacity (compile_lam env env_type types.(i) 0) [Kstop]
         in
-	let lbl,fcode = label_code fcode in
-	lbl_types.(i) <- lbl;
+        let lbl,fcode = label_code fcode in
+        lbl_types.(i) <- lbl;
 	fun_code := [Ksequence(fcode,!fun_code)]
       done;
       (* Compiling bodies *)
       for i = 0 to ndef - 1 do
-	let params,body = Term.decompose_lam rec_bodies.(i) in
-	let arity = List.length params in
+        let params,body = decompose_Llam bodies.(i) in
+        let arity = Array.length params in
 	let env_body = comp_env_fix ndef i arity rfv in
-	let cont1 =
-	  ensure_stack_capacity (compile_constr env_body body arity) [Kreturn arity]
+        let cont1 =
+          ensure_stack_capacity (compile_lam env env_body body arity) [Kreturn arity]
         in
 	let lbl = Label.create () in
 	lbl_bodies.(i) <- lbl;
@@ -699,8 +558,9 @@ let rec compile_constr reloc c sz cont =
       compile_fv reloc fv.fv_rev sz
 	(Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont)
 
-  | CoFix(init,(_,type_bodies,rec_bodies)) ->
-      let ndef = Array.length type_bodies in
+
+  | Lcofix(init, (decl,types,bodies)) ->
+      let ndef = Array.length types in
       let lbl_types = Array.make ndef Label.no in
       let lbl_bodies = Array.make ndef Label.no in
       (* Compiling types *)
@@ -708,22 +568,22 @@ let rec compile_constr reloc c sz cont =
       let env_type = comp_env_cofix_type ndef rfv in
       for i = 0 to ndef - 1 do
         let fcode =
-          ensure_stack_capacity (compile_constr env_type type_bodies.(i) 0) [Kstop]
+          ensure_stack_capacity (compile_lam env env_type types.(i) 0) [Kstop]
         in
-	let lbl,fcode = label_code fcode in
-	lbl_types.(i) <- lbl;
+        let lbl,fcode = label_code fcode in
+        lbl_types.(i) <- lbl;
 	fun_code := [Ksequence(fcode,!fun_code)]
       done;
       (* Compiling bodies *)
       for i = 0 to ndef - 1 do
-	let params,body = Term.decompose_lam rec_bodies.(i) in
-	let arity = List.length params in
+        let params,body = decompose_Llam bodies.(i) in
+        let arity = Array.length params in
 	let env_body = comp_env_cofix ndef arity rfv in
 	let lbl = Label.create () in
         let comp arity =
           (* 4 stack slots are needed to update the cofix when forced *)
           set_max_stack_size (arity + 4);
-          compile_constr env_body body (arity+1) (cont_cofix arity)
+          compile_lam env env_body body (arity+1) (cont_cofix arity)
         in
 	let cont = ensure_stack_capacity comp arity in
 	lbl_bodies.(i) <- lbl;
@@ -734,33 +594,34 @@ let rec compile_constr reloc c sz cont =
       compile_fv reloc fv.fv_rev sz
 	(Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont)
 
-  | Case(ci,t,a,branchs) ->
+
+  | Lcase(ci,rtbl,t,a,branches) ->
       let ind = ci.ci_ind in
-      let mib = lookup_mind (fst ind) !global_env in
+      let mib = lookup_mind (fst ind) env in
       let oib = mib.mind_packets.(snd ind) in
-      let () = check_compilable oib in
-      let tbl = oib.mind_reloc_tbl in
       let lbl_consts = Array.make oib.mind_nb_constant Label.no in
       let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *)
+      let nconst = Array.length branches.constant_branches in
       let nblock = min nallblock (last_variant_tag + 1) in
       let lbl_blocks = Array.make nblock Label.no in
       let neblock = max 0 (nallblock - last_variant_tag) in
       let lbl_eblocks = Array.make neblock Label.no in 
-      let branch1,cont = make_branch cont in
-      (* Compiling return type *)
+      let branch1, cont = make_branch cont in
+      (* Compilation of the return type *)
       let fcode =
-        ensure_stack_capacity (compile_constr reloc t sz) [Kpop sz; Kstop]
+        ensure_stack_capacity (compile_lam env reloc t sz) [Kpop sz; Kstop]
       in
       let lbl_typ,fcode = label_code fcode in
       fun_code := [Ksequence(fcode,!fun_code)];
-      (* Compiling branches *)
+      (* Compilation of the branches *)
       let lbl_sw = Label.create () in
       let sz_b,branch,is_tailcall =
-	match branch1 with
-	| Kreturn k ->
-	  assert (Int.equal k sz) ;
-	  sz, branch1, true
-	| _ -> sz+3, Kjump, false
+        match branch1 with
+        | Kreturn k ->
+          assert (Int.equal k sz) ;
+          sz, branch1, true
+        | Kbranch _ -> sz+3, Kjump, false
+        | _ -> assert false
       in
 
       let c = ref cont in
@@ -771,29 +632,26 @@ let rec compile_constr reloc c sz cont =
             Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in
         lbl_blocks.(last_variant_tag) <- lbl_b;
         c := code_b
-      end;  
-      
-      (* Compiling regular constructor branches *)
-      for i = 0 to Array.length tbl - 1 do
-	let tag, arity = tbl.(i) in
-	if Int.equal arity 0 then
-	  let lbl_b,code_b =
-	    label_code(compile_constr reloc branchs.(i) sz_b (branch :: !c)) in
-	  lbl_consts.(tag) <- lbl_b;
-	  c := code_b
-	else
-	  let args, body = Term.decompose_lam branchs.(i) in
-	  let nargs = List.length args in
-         
-          let code_b =  
-            if Int.equal nargs arity then
-	      compile_constr (push_param arity sz_b reloc)
-		body (sz_b+arity) (add_pop arity (branch :: !c))
-	    else
-	      let sz_appterm = if is_tailcall then sz_b + arity else arity in
-	      compile_constr reloc branchs.(i) (sz_b+arity)
-		(Kappterm(arity,sz_appterm) :: !c) in
-          let code_b = 
+      end;
+
+      (* Compilation of constant branches *)
+      for i = nconst - 1 downto 0 do
+        let aux =
+          compile_lam env reloc branches.constant_branches.(i) sz_b (branch::!c)
+        in
+        let lbl_b,code_b = label_code aux in
+        lbl_consts.(i) <- lbl_b;
+        c := code_b
+      done;
+      (* -1 for accu branch *)
+      for i = nallblock - 2 downto 0 do
+        let tag = i + 1 in
+        let (ids, body) = branches.nonconstant_branches.(i) in
+        let arity = Array.length ids in
+        let code_b =
+          compile_lam env (push_param arity sz_b reloc)
+            body (sz_b+arity) (add_pop arity (branch::!c)) in
+        let code_b =
             if tag < last_variant_tag then begin
                 set_max_stack_size (sz_b + arity);
                 Kpushfields arity :: code_b
@@ -802,15 +660,15 @@ let rec compile_constr reloc c sz cont =
                 set_max_stack_size (sz_b + arity + 1);
                 Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b
               end
-          in
-          let lbl_b,code_b = label_code code_b in
-          if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b
+        in
+        let lbl_b, code_b = label_code code_b in
+        if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b
           else lbl_eblocks.(tag - last_variant_tag) <- lbl_b;
-	  c := code_b
+        c := code_b
       done;
 
       let annot =
-        {ci = ci; rtbl = tbl; tailcall = is_tailcall;
+        {ci = ci; rtbl = rtbl; tailcall = is_tailcall;
          max_stack_size = !max_stack_size - sz}
       in
 
@@ -829,38 +687,50 @@ let rec compile_constr reloc c sz cont =
         | Kbranch lbl -> Kpush_retaddr lbl ::  !c
 	| _ -> !c
       in
-      compile_constr reloc a sz
-      (try
-	let entry = mkInd ind in
-	Retroknowledge.get_vm_before_match_info (!global_env).retroknowledge
-	                                       entry code_sw
-      with Not_found ->
-	code_sw)
-
-and compile_str_cst reloc sc sz cont =
-  set_max_stack_size sz;
-  match sc with
-  | Bconstr c -> compile_constr reloc c sz cont
-  | Bstrconst sc -> Kconst sc :: cont
-  | Bmakeblock(tag,args) ->
-      let arity = Array.length args in
-      let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
-      comp_args compile_str_cst reloc args sz cont
-  | Bconstruct_app(tag,nparams,arity,args) ->
-      if Int.equal (Array.length args) 0 then
-        code_construct tag nparams arity cont
-      else
-	comp_app
-	  (fun _ _ _ cont -> code_construct tag nparams arity cont)
-	  compile_str_cst reloc () args sz cont
-  | Bspecial (comp_fx, args) -> comp_fx reloc args sz cont
+      compile_lam env reloc a sz code_sw
+
+  | Lmakeblock (tag,args) ->
+    let arity = Array.length args in
+    let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
+    comp_args (compile_lam env) reloc args sz cont
+
+  | Lprim (kn, ar, op, args) ->
+    op_compilation env ar op kn reloc args sz cont
+
+  | Luint v ->
+     (match v with
+     | UintVal i -> compile_structured_constant reloc (Const_b0 (Uint31.to_int i)) sz cont
+     | UintDigits ds ->
+       let nargs = Array.length ds in
+       if Int.equal nargs 31 then
+         let (escape,labeled_cont) = make_branch cont in
+         let else_lbl = Label.create() in
+         comp_args (compile_lam env) reloc ds sz
+           ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont)
+       else
+         let code_construct cont = (* spiwack: variant of the global code_construct
+                                             which handles dynamic compilation of
+                                             integers *)
+           let f_cont =
+             let else_lbl = Label.create () in
+             [Kacc 0; Kpop 1; Kisconst else_lbl; Kareconst(30,else_lbl);
+              Kcompint31; Kreturn 0; Klabel else_lbl; Kmakeblock(31, 1); Kreturn 0]
+           in
+           let lbl = Label.create() in
+           fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)];
+           Kclosure(lbl,0) :: cont
+         in
+         comp_app (fun _ _ _ cont -> code_construct cont)
+           (compile_lam env) reloc () ds sz cont
+     | UintDecomp t ->
+       let escape_lbl, labeled_cont = label_code cont in
+       compile_lam env  reloc t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont))
 
 
 (* spiwack : compilation of constants with their arguments.
    Makes a special treatment with 31-bit integer addition *)
 and compile_get_global reloc (kn,u) sz cont =
   set_max_stack_size sz;
-  let kn = get_alias !global_env kn in
   if Univ.Instance.is_empty u then
     Kgetglobal kn :: cont
   else
@@ -870,41 +740,67 @@ and compile_get_global reloc (kn,u) sz cont =
 and compile_universe reloc uni sz cont =
   set_max_stack_size sz;
   match Univ.Level.var_index uni with
-  | None -> Kconst (Const_univ_level uni) :: cont
+  | None -> compile_structured_constant reloc (Const_univ_level uni) sz cont
   | Some idx -> pos_universe_var idx reloc sz :: cont
 
-and compile_const reloc kn u args sz cont =
+and compile_constant env reloc kn u args sz cont =
   set_max_stack_size sz;
+  if Univ.Instance.is_empty u then
+    (* normal compilation *)
+    comp_app (fun _ _ sz cont ->
+        compile_get_global reloc (kn,u) sz cont)
+      (compile_lam env) reloc () args sz cont
+  else
+    let compile_arg reloc constr_or_uni sz cont =
+      match constr_or_uni with
+      | ArgLambda t -> compile_lam env reloc t sz cont
+      | ArgUniv uni -> compile_universe reloc uni sz cont
+    in
+    let u = Univ.Instance.to_array u in
+    let lu = Array.length u in
+    let all =
+      Array.init (lu + Array.length args)
+        (fun i -> if i < lu then ArgUniv u.(i) else ArgLambda args.(i-lu))
+    in
+    comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
+      compile_arg reloc () all sz cont
+
+(*template for n-ary operation, invariant: n>=1,
+  the operations does the following :
+  1/ checks if all the arguments are constants (i.e. non-block values)
+  2/ if they are, uses the "op" instruction to execute
+  3/ if at least one is not, branches to the normal behavior:
+      Kgetglobal (get_alias !global_env kn) *)
+and op_compilation env n op =
+  let code_construct reloc kn sz cont =
+     let f_cont =
+         let else_lbl = Label.create () in
+         Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
+          op:: Kreturn 0:: Klabel else_lbl::
+         (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*)
+          compile_get_global reloc kn sz (
+            Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *)
+     in
+     let lbl = Label.create () in
+     fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)];
+     Kclosure(lbl, 0)::cont
+  in
+  fun kn reloc args sz cont ->
   let nargs = Array.length args in
-  (* spiwack: checks if there is a specific way to compile the constant
-              if there is not, Not_found is raised, and the function
-              falls back on its normal behavior *)
-  try
-    Retroknowledge.get_vm_compiling_info (!global_env).retroknowledge
-                  (mkConstU (kn,u)) reloc args sz cont
-  with Not_found ->
-    if Int.equal nargs 0 then
-      compile_get_global reloc (kn,u) sz cont
-    else
-      if Univ.Instance.is_empty u then
-        (* normal compilation *)
-        comp_app (fun _ _ sz cont ->
-            compile_get_global reloc (kn,u) sz cont)
-          compile_constr reloc () args sz cont
-      else
-        let compile_arg reloc constr_or_uni sz cont =
-          match constr_or_uni with
-          | ArgConstr cst -> compile_constr reloc cst sz cont
-          | ArgUniv uni -> compile_universe reloc uni sz cont
-        in
-	let u = Univ.Instance.to_array u in
-	let lu = Array.length u in
-	let all =
-	  Array.init (lu + Array.length args) 
-	    (fun i -> if i < lu then ArgUniv u.(i) else ArgConstr args.(i-lu))
-	in
-        comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
-          compile_arg reloc () all sz cont
+  if Int.equal nargs n then (*if it is a fully applied addition*)
+    let (escape, labeled_cont) = make_branch cont in
+    let else_lbl = Label.create () in
+    assert (n < 4);
+    comp_args (compile_lam env) reloc args sz
+      (Kisconst else_lbl::(make_areconst (n-1) else_lbl
+         (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
+         (op::escape::Klabel else_lbl::Kpush::
+         (* works as comp_app with nargs < 4 and non-tailcall cont*)
+         compile_get_global reloc kn (sz+n) (Kapply n::labeled_cont))))
+  else
+    comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont)
+      (compile_lam env) reloc () args sz cont
+
 
 let is_univ_copy max u =
   let u = Univ.Instance.to_array u in
@@ -927,33 +823,29 @@ let dump_bytecodes init code fvs =
      prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++
      fnl ())
 
-let compile fail_on_error ?universes:(universes=0) env c =
-  set_global_env env;
+let compile ~fail_on_error ?universes:(universes=0) env c =
   init_fun_code ();
   Label.reset_label_counter ();
   let cont = [Kstop] in
   try
     let reloc, init_code =
       if Int.equal universes 0 then
+        let lam = lambda_of_constr ~optimize:true env c in
         let reloc = empty_comp_env () in
-        reloc, ensure_stack_capacity (compile_constr reloc c 0) cont
+        reloc, ensure_stack_capacity (compile_lam env reloc lam 0) cont
       else
         (* We are going to generate a lambda, but merge the universe closure
          * with the function closure if it exists.
          *)
+        let lam = lambda_of_constr ~optimize:true env c in
+        let params, body = decompose_Llam lam in
+        let arity = Array.length params in
         let reloc = empty_comp_env () in
-        let arity , body =
-          match kind c with
-          | Lambda _ ->
-            let params, body = Term.decompose_lam c in
-            List.length params , body
-          | _ -> 0 , c
-        in
         let full_arity = arity + universes in
         let r_fun = comp_env_fun ~univs:universes arity in
         let lbl_fun = Label.create () in
         let cont_fun =
-          ensure_stack_capacity (compile_constr r_fun body full_arity)
+          ensure_stack_capacity (compile_lam env r_fun body full_arity)
                          [Kreturn full_arity]
         in
         fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)];
@@ -968,15 +860,12 @@ let compile fail_on_error ?universes:(universes=0) env c =
     (if !Flags.dump_bytecode then
       Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
-  with TooLargeInductive tname ->
+  with TooLargeInductive msg ->
     let fn = if fail_on_error then CErrors.user_err ?loc:None ~hdr:"compile" else
-	       (fun x -> Feedback.msg_warning x) in
-      (Pp.(fn
-	   (str "Cannot compile code for virtual machine as it uses inductive " ++
-	    Id.print tname ++ str str_max_constructors));
-       None)
+        (fun x -> Feedback.msg_warning x) in
+    fn msg; None
 
-let compile_constant_body fail_on_error env univs = function
+let compile_constant_body ~fail_on_error env univs = function
   | Undef _ | OpaqueDef _ -> Some BCconstant
   | Def sb ->
       let body = Mod_subst.force_constr sb in
@@ -991,65 +880,13 @@ let compile_constant_body fail_on_error env univs = function
 	    let con= Constant.make1 (Constant.canonical kn') in
 	      Some (BCalias (get_alias env con))
 	| _ ->
-	    let res = compile fail_on_error ~universes:instance_size env body in
+            let res = compile ~fail_on_error ~universes:instance_size env body in
 	      Option.map (fun x -> BCdefined (to_memory x)) res
 
 (* Shortcut of the previous function used during module strengthening *)
 
 let compile_alias kn = BCalias (Constant.make1 (Constant.canonical kn))
 
-(* spiwack: additional function which allow different part of compilation of the
-      31-bit integers *)
-
-let make_areconst n else_lbl cont =
-  if n <= 0 then
-    cont
-  else
-    Kareconst (n, else_lbl)::cont
-
-
-(* try to compile int31 as a const_b0. Succeed if all the arguments are closed
-   fails otherwise by raising NotClosed*)
-let compile_structured_int31 fc args =
-  if not fc then raise Not_found else
-  Const_b0
-    (Array.fold_left
-       (fun temp_i -> fun t -> match kind t with
-          | Construct ((_,d),_) -> 2*temp_i+d-1
-          | _ -> raise NotClosed)
-       0 args
-    )
-
-(* this function is used for the compilation of the constructor of
-   the int31, it is used when it appears not fully applied, or
-   applied to at least one non-closed digit *)
-let dynamic_int31_compilation fc reloc args sz cont =
-  if not fc then raise Not_found else
-    let nargs = Array.length args in
-      if Int.equal nargs 31 then
-	let (escape,labeled_cont) = make_branch cont in
-	let else_lbl = Label.create() in
-	  comp_args compile_str_cst reloc args sz
-            ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont)
-      else
-	let code_construct cont = (* spiwack: variant of the global code_construct
-                                     which handles dynamic compilation of
-                                     integers *)
-          let f_cont =
-            let else_lbl = Label.create () in
-	      [Kacc 0; Kpop 1; Kisconst else_lbl; Kareconst(30,else_lbl);
-               Kcompint31; Kreturn 0; Klabel else_lbl; Kmakeblock(31, 1); Kreturn 0]
-	  in
-	  let lbl = Label.create() in
-	    fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)];
-	    Kclosure(lbl,0) :: cont
-	in
-	  if Int.equal nargs 0 then
-	    code_construct cont
-	  else
-	    comp_app (fun _ _ _ cont -> code_construct cont)
-              compile_str_cst reloc () args sz cont
-
 (*(* template compilation for 2ary operation, it probably possible
    to make a generic such function with arity abstracted *)
 let op2_compilation op =
@@ -1087,47 +924,3 @@ let op2_compilation op =
     comp_app (fun _ _ _ cont -> code_construct normal cont)
       compile_constr reloc () args sz cont *)
 
-(*template for n-ary operation, invariant: n>=1,
-  the operations does the following :
-  1/ checks if all the arguments are constants (i.e. non-block values)
-  2/ if they are, uses the "op" instruction to execute
-  3/ if at least one is not, branches to the normal behavior:
-      Kgetglobal (get_alias !global_env kn) *)
-let op_compilation n op =
-  let code_construct reloc kn sz cont =
-     let f_cont =
-         let else_lbl = Label.create () in
-         Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
-          op:: Kreturn 0:: Klabel else_lbl::
-         (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*)
-          compile_get_global reloc kn sz (
-            Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *)
-     in
-     let lbl = Label.create () in
-     fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)];
-     Kclosure(lbl, 0)::cont
-  in
-  fun kn fc reloc args sz cont ->
-  if not fc then raise Not_found else
-  let nargs = Array.length args in
-  if Int.equal nargs n then (*if it is a fully applied addition*)
-    let (escape, labeled_cont) = make_branch cont in
-    let else_lbl = Label.create () in
-      comp_args compile_constr reloc args sz
-	(Kisconst else_lbl::(make_areconst (n-1) else_lbl
-           (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
-           (op::escape::Klabel else_lbl::Kpush::
-           (* works as comp_app with nargs = n and non-tailcall cont*)
-           compile_get_global reloc kn sz (Kapply n::labeled_cont))))
-  else if Int.equal nargs 0 then
-    code_construct reloc kn sz cont
-  else
-    comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont)
-      compile_constr reloc () args sz cont
-
-let int31_escape_before_match fc cont =
-  if not fc then
-    raise Not_found
-  else
-    let escape_lbl, labeled_cont = label_code cont in
-      (Kisconst escape_lbl)::Kdecompint31::labeled_cont
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index c117d3fb5..99f2a3c01 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -13,38 +13,13 @@ open Declarations
 open Pre_env
 
 (** Should only be used for monomorphic terms *)
-val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *)
+val compile : fail_on_error:bool ->
 	      ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
 (** init, fun, fv *)
 
-val compile_constant_body : bool ->
+val compile_constant_body : fail_on_error:bool ->
 			    env -> constant_universes -> constant_def -> body_code option
 
 (** Shortcut of the previous function used during module strengthening *)
 
 val compile_alias : Names.Constant.t -> body_code
-
-(** spiwack: this function contains the information needed to perform
-            the static compilation of int31 (trying and obtaining
-            a 31-bit integer in processor representation at compile time) *)
-val compile_structured_int31 : bool -> constr array ->
-                               structured_constant
-
-(** this function contains the information needed to perform
-        the dynamic compilation of int31 (trying and obtaining a
-        31-bit integer in processor representation at runtime when
-        it failed at compile time *)
-val dynamic_int31_compilation : bool -> comp_env ->
-                                block array ->
-                                int -> bytecodes -> bytecodes
-
-(*spiwack: template for the compilation n-ary operation, invariant: n>=1.
-           works as follow: checks if all the arguments are non-pointers
-           if they are applies the operation (second argument) if not
-           all of them are, returns to a coq definition (third argument) *)
-val op_compilation : int -> instruction -> pconstant -> bool -> comp_env ->
-                             constr array -> int -> bytecodes-> bytecodes
-
-(*spiwack: compiling function to insert dynamic decompilation before
-           matching integers (in case they are in processor representation) *)
-val int31_escape_before_match : bool -> bytecodes -> bytecodes
diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli
new file mode 100644
index 000000000..2d9ec6050
--- /dev/null
+++ b/kernel/cinstr.mli
@@ -0,0 +1,43 @@
+(************************************************************************)
+(*  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 Constr
+open Cbytecodes
+
+(** This file defines the lambda code for the bytecode compiler. It has been
+extracted from Clambda.ml because of the retroknowledge architecture. *)
+
+type uint =
+  | UintVal of Uint31.t
+  | UintDigits of lambda array
+  | UintDecomp of lambda
+
+and lambda =
+  | Lrel          of Name.t * int
+  | Lvar          of Id.t
+  | Lprod         of lambda * lambda
+  | Llam          of Name.t array * lambda
+  | Llet          of Name.t * lambda * lambda
+  | Lapp          of lambda * lambda array
+  | Lconst        of pconstant
+  | Lprim         of pconstant * int (* arity *) * instruction * lambda array
+  | Lcase         of case_info * reloc_table * lambda * lambda * lam_branches
+  | Lfix          of (int array * int) * fix_decl
+  | Lcofix        of int * fix_decl
+  | Lmakeblock    of int * lambda array
+  | Lval          of structured_constant
+  | Lsort         of Sorts.t
+  | Lind          of pinductive
+  | Lproj         of int * Constant.t * lambda
+  | Luint         of uint
+
+and lam_branches =
+  { constant_branches : lambda array;
+    nonconstant_branches : (Name.t array * lambda) array }
+
+and fix_decl =  Name.t array * lambda array * lambda array
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
new file mode 100644
index 000000000..636ed3510
--- /dev/null
+++ b/kernel/clambda.ml
@@ -0,0 +1,853 @@
+open Util
+open Names
+open Esubst
+open Term
+open Constr
+open Declarations
+open Cbytecodes
+open Cinstr
+open Pre_env
+open Pp
+
+let pr_con sp = str(Names.Label.to_string (Constant.label sp))
+
+(** Printing **)
+
+let pp_names ids =
+  prlist_with_sep (fun _ -> brk(1,1)) Name.print (Array.to_list ids)
+
+let pp_rel name n =
+  Name.print name ++  str "##" ++ int n
+
+let pp_sort s =
+  match Sorts.family s with
+  | InSet -> str "Set"
+  | InProp -> str "Prop"
+  | InType -> str "Type"
+
+let rec pp_lam lam =
+  match lam with
+  | Lrel (id,n) -> pp_rel id n
+  | Lvar id -> Id.print id
+  | Lprod(dom,codom) -> hov 1
+                          (str "forall(" ++
+                           pp_lam dom ++
+                           str "," ++ spc() ++
+                           pp_lam codom ++
+                           str ")")
+  | Llam(ids,body) -> hov 1
+                        (str "(fun " ++
+                         pp_names ids ++
+                         str " =>" ++
+                         spc() ++
+                         pp_lam body ++
+                         str ")")
+  | Llet(id,def,body) -> hov 0
+                           (str "let " ++
+                            Name.print id ++
+                            str ":=" ++
+                            pp_lam def  ++
+                            str " in" ++
+                            spc() ++
+                            pp_lam body)
+  | Lapp(f, args) -> hov 1
+                       (str "(" ++ pp_lam f ++ spc() ++
+                        prlist_with_sep spc pp_lam (Array.to_list args) ++
+                        str")")
+  | Lconst (kn,_) -> pr_con kn
+  | Lcase(_ci, _rtbl, t, a, branches) ->
+    let ic = ref (-1) in
+    let ib = ref 0 in
+    v 0 (str"<" ++ pp_lam t ++ str">" ++ cut() ++
+         str "Case" ++ spc () ++ pp_lam a ++ spc() ++ str "of" ++ cut() ++
+         v 0
+           ((prlist_with_sep (fun _ -> str "")
+               (fun c ->
+                  cut () ++ str "| " ++
+                  int (incr ic; !ic) ++ str " => " ++ pp_lam c)
+               (Array.to_list branches.constant_branches)) ++
+            (prlist_with_sep (fun _ -> str "")
+               (fun (ids,c) ->
+                  cut () ++ str "| " ++
+                  int (incr ib; !ib) ++ str " " ++
+                  pp_names ids ++ str " => " ++ pp_lam c)
+               (Array.to_list branches.nonconstant_branches)))
+         ++ cut() ++ str "end")
+  | Lfix((t,i),(lna,tl,bl)) ->
+    let fixl = Array.mapi (fun i id -> (id,t.(i),tl.(i),bl.(i))) lna in
+    hov 1
+      (str"fix " ++ int i ++ spc() ++  str"{" ++
+       v 0
+         (prlist_with_sep spc
+            (fun (na,i,ty,bd) ->
+               Name.print na ++ str"/" ++ int i ++ str":" ++
+               pp_lam ty ++ cut() ++ str":=" ++
+               pp_lam bd) (Array.to_list fixl)) ++
+       str"}")
+
+  | Lcofix (i,(lna,tl,bl)) ->
+    let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
+    hov 1
+      (str"cofix " ++ int i ++ spc() ++  str"{" ++
+       v 0
+         (prlist_with_sep spc
+            (fun (na,ty,bd) ->
+               Name.print na ++ str":" ++ pp_lam ty ++
+               cut() ++ str":=" ++ pp_lam bd) (Array.to_list fixl)) ++
+       str"}")
+  | Lmakeblock(tag, args) ->
+    hov 1
+      (str "(makeblock " ++ int tag ++ spc() ++
+       prlist_with_sep spc pp_lam (Array.to_list args) ++
+       str")")
+  | Lval _ -> str "values"
+  | Lsort s -> pp_sort s
+  | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i
+  | Lprim((kn,_u),ar,op,args) ->
+    hov 1
+      (str "(PRIM " ++ pr_con kn ++  spc() ++
+       prlist_with_sep spc pp_lam  (Array.to_list args) ++
+       str")")
+  | Lproj(i,kn,arg) ->
+    hov 1
+      (str "(proj#" ++ int i ++ spc() ++ pr_con kn ++ str "(" ++ pp_lam arg
+       ++ str ")")
+  | Luint _ ->
+    str "(uint)"
+
+(*s Constructors *)
+
+let mkLapp f args =
+  if Array.length args = 0 then f
+  else
+    match f with
+    | Lapp(f', args') -> Lapp (f', Array.append args' args)
+    | _ -> Lapp(f, args)
+
+let mkLlam ids body =
+  if Array.length ids = 0 then body
+  else
+    match body with
+    | Llam(ids', body) -> Llam(Array.append ids ids', body)
+    | _ -> Llam(ids, body)
+
+let decompose_Llam lam =
+  match lam with
+  | Llam(ids,body) -> ids, body
+  | _ -> [||], lam
+
+(*s Operators on substitution *)
+let subst_id = subs_id 0
+let lift = subs_lift
+let liftn = subs_liftn
+let cons v subst = subs_cons([|v|], subst)
+let shift subst = subs_shft (1, subst)
+
+(* A generic map function *)
+
+let rec map_lam_with_binders g f n lam =
+  match lam with
+  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam
+  | Lprod(dom,codom) ->
+    let dom' = f n dom in
+    let codom' = f n codom in
+    if dom == dom' && codom == codom' then lam else Lprod(dom',codom')
+  | Llam(ids,body) ->
+    let body' = f (g (Array.length ids) n) body in
+    if body == body' then lam else mkLlam ids body'
+  | Llet(id,def,body) ->
+    let def' = f n def in
+    let body' = f (g 1 n) body in
+    if body == body' && def == def' then lam else Llet(id,def',body')
+  | Lapp(fct,args) ->
+    let fct' = f n fct in
+    let args' = Array.smartmap (f n) args in
+    if fct == fct' && args == args' then lam else mkLapp fct' args'
+  | Lcase(ci,rtbl,t,a,branches) ->
+    let const = branches.constant_branches in
+    let nonconst = branches.nonconstant_branches in
+    let t' = f n t in
+    let a' = f n a in
+    let const' = Array.smartmap (f n) const in
+    let on_b b =
+      let (ids,body) = b in
+      let body' = f (g (Array.length ids) n) body in
+      if body == body' then b else (ids,body') in
+    let nonconst' = Array.smartmap on_b nonconst in
+    let branches' =
+      if const == const' && nonconst == nonconst' then
+        branches
+      else
+        { constant_branches = const';
+          nonconstant_branches = nonconst' }
+    in
+    if t == t' && a == a' && branches == branches' then lam else
+      Lcase(ci,rtbl,t',a',branches')
+  | Lfix(init,(ids,ltypes,lbodies)) ->
+    let ltypes' = Array.smartmap (f n) ltypes in
+    let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+    if ltypes == ltypes' && lbodies == lbodies' then lam
+    else Lfix(init,(ids,ltypes',lbodies'))
+  | Lcofix(init,(ids,ltypes,lbodies)) ->
+    let ltypes' = Array.smartmap (f n) ltypes in
+    let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+    if ltypes == ltypes' && lbodies == lbodies' then lam
+    else Lcofix(init,(ids,ltypes',lbodies'))
+  | Lmakeblock(tag,args) ->
+    let args' = Array.smartmap (f n) args in
+    if args == args' then lam else Lmakeblock(tag,args')
+  | Lprim(kn,ar,op,args) ->
+    let args' = Array.smartmap (f n) args in
+    if args == args' then lam else Lprim(kn,ar,op,args')
+  | Lproj(i,kn,arg) ->
+    let arg' = f n arg in
+    if arg == arg' then lam else Lproj(i,kn,arg')
+  | Luint u ->
+    let u' = map_uint g f n u in
+    if u == u' then lam else Luint u'
+
+and map_uint g f n u =
+  match u with
+  | UintVal _ -> u
+  | UintDigits(args) ->
+    let args' = Array.smartmap (f n) args in
+    if args == args' then u else UintDigits(args')
+  | UintDecomp(a) ->
+    let a' = f n a in
+    if a == a' then u else UintDecomp(a')
+
+(*s Lift and substitution *)
+
+
+let rec lam_exlift el lam =
+  match lam with
+  | Lrel(id,i) ->
+    let i' = reloc_rel i el in
+    if i == i' then lam else Lrel(id,i')
+  | _ -> map_lam_with_binders el_liftn lam_exlift el lam
+
+let lam_lift k lam =
+  if k = 0 then lam
+  else lam_exlift (el_shft k el_id) lam
+
+let lam_subst_rel lam id n subst =
+  match expand_rel n subst with
+  | Inl(k,v) -> lam_lift k v
+  | Inr(n',_) ->
+    if n == n' then lam
+    else Lrel(id, n')
+
+let rec lam_exsubst subst lam =
+  match lam with
+  | Lrel(id,i) -> lam_subst_rel lam id i subst
+  | _ -> map_lam_with_binders liftn lam_exsubst subst lam
+
+let lam_subst_args subst args =
+  if is_subs_id subst then args
+  else Array.smartmap (lam_exsubst subst) args
+
+(** Simplification of lambda expression *)
+
+(* [simplify subst lam] simplify the expression [lam_subst subst lam] *)
+(* that is :                                                          *)
+(* - Reduce [let] is the definition can be substituted i.e:           *)
+(*    - a variable (rel or identifier)                                *)
+(*    - a constant                                                    *)
+(*    - a structured constant                                         *)
+(*    - a function                                                    *)
+(* - Transform beta redex into [let] expression                       *)
+(* - Move arguments under [let]                                       *)
+(* Invariant : Terms in [subst] are already simplified and can be     *)
+(*             substituted                                            *)
+
+let can_subst lam =
+  match lam with
+  | Lrel _ | Lvar _ | Lconst _
+  | Lval _ | Lsort _ | Lind _ | Llam _ -> true
+  | _ -> false
+
+let rec simplify subst lam =
+  match lam with
+  | Lrel(id,i) -> lam_subst_rel lam id i subst
+
+  | Llet(id,def,body) ->
+    let def' = simplify subst def in
+    if can_subst def' then simplify (cons def' subst) body
+    else
+      let body' = simplify (lift subst) body in
+      if def == def' && body == body' then lam
+      else Llet(id,def',body')
+
+  | Lapp(f,args) ->
+    begin match simplify_app subst f subst args with
+      | Lapp(f',args') when f == f' && args == args' -> lam
+      | lam' -> lam'
+    end
+
+  | _ -> map_lam_with_binders liftn simplify subst lam
+
+and simplify_app substf f substa args =
+  match f with
+  | Lrel(id, i) ->
+    begin match lam_subst_rel f id i substf with
+      | Llam(ids, body) ->
+        reduce_lapp
+          subst_id (Array.to_list ids) body
+          substa (Array.to_list args)
+      | f' -> mkLapp f' (simplify_args substa args)
+    end
+  | Llam(ids, body) ->
+    reduce_lapp substf (Array.to_list ids) body substa (Array.to_list args)
+  | Llet(id, def, body) ->
+    let def' = simplify substf def in
+    if can_subst def' then
+      simplify_app (cons def' substf) body substa args
+    else
+      Llet(id, def', simplify_app (lift substf) body (shift substa) args)
+  | Lapp(f, args') ->
+    let args = Array.append
+        (lam_subst_args substf args') (lam_subst_args substa args) in
+    simplify_app substf f subst_id args
+  | _ -> mkLapp (simplify substf f) (simplify_args substa args)
+
+and simplify_args subst args = Array.smartmap (simplify subst) args
+
+and reduce_lapp substf lids body substa largs =
+  match lids, largs with
+  | id::lids, a::largs ->
+    let a = simplify substa a in
+    if can_subst a then
+      reduce_lapp (cons a substf) lids body substa largs
+    else
+      let body = reduce_lapp (lift substf) lids body (shift substa) largs in
+      Llet(id, a, body)
+  | [], [] -> simplify substf body
+  | _::_, _ ->
+    Llam(Array.of_list lids,  simplify (liftn (List.length lids) substf) body)
+  | [], _::_ -> simplify_app substf body substa (Array.of_list largs)
+
+
+
+
+(* [occurrence kind k lam]:
+   If [kind] is [true] return [true] if the variable [k] does not appear in
+   [lam], return [false] if the variable appear one time and not
+   under a lambda, a fixpoint, a cofixpoint; else raise Not_found.
+   If [kind] is [false] return [false] if the variable does not appear in [lam]
+   else raise [Not_found]
+*)
+
+let rec occurrence k kind lam =
+  match lam with
+  | Lrel (_,n) ->
+    if n = k then
+      if kind then false else raise Not_found
+    else kind
+  | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _ -> kind
+  | Lprod(dom, codom) ->
+    occurrence k (occurrence k kind dom) codom
+  | Llam(ids,body) ->
+    let _ = occurrence (k+Array.length ids) false body in kind
+  | Llet(_,def,body) ->
+    occurrence (k+1) (occurrence k kind def) body
+  | Lapp(f, args) ->
+    occurrence_args k (occurrence k kind f) args
+  | Lprim(_,_,_,args) | Lmakeblock(_,args) ->
+    occurrence_args k kind args
+  | Lcase(_ci,_rtbl,t,a,branches) ->
+    let kind = occurrence k (occurrence k kind t) a in
+    let r = ref kind in
+    Array.iter (fun c -> r := occurrence k kind c  && !r) branches.constant_branches;
+    let on_b (ids,c) =
+      r := occurrence (k+Array.length ids) kind c && !r
+    in
+    Array.iter on_b branches.nonconstant_branches;
+    !r
+  | Lfix(_,(ids,ltypes,lbodies))
+  | Lcofix(_,(ids,ltypes,lbodies)) ->
+    let kind = occurrence_args k kind ltypes in
+    let _ = occurrence_args (k+Array.length ids) false lbodies in
+    kind
+  | Lproj(_,_,arg) ->
+    occurrence k kind arg
+  | Luint u -> occurrence_uint k kind u
+
+and occurrence_args k kind args =
+  Array.fold_left (occurrence k) kind args
+
+and occurrence_uint k kind u =
+  match u with
+  | UintVal _ -> kind
+  | UintDigits args -> occurrence_args k kind args
+  | UintDecomp t -> occurrence k kind t
+
+let occur_once lam =
+  try let _ = occurrence 1 true lam in true
+  with Not_found -> false
+
+(* [remove_let lam] remove let expression in [lam] if the variable is *)
+(* used at most once time in the body, and does not appear under      *)
+(* a lambda or a fix or a cofix                                       *)
+
+let rec remove_let subst lam =
+  match lam with
+  | Lrel(id,i) -> lam_subst_rel lam id i subst
+  | Llet(id,def,body) ->
+    let def' = remove_let subst def in
+    if occur_once body then remove_let (cons def' subst) body
+    else
+      let body' = remove_let (lift subst) body in
+      if def == def' && body == body' then lam else Llet(id,def',body')
+  | _ -> map_lam_with_binders liftn remove_let subst lam
+
+
+(*s Translation from [constr] to [lambda] *)
+
+(* Translation of constructor *)
+
+(* Limitation due to OCaml's representation of non-constant
+  constructors: limited to 245 + 1 (0 tag) cases. *)
+
+exception TooLargeInductive of Pp.t
+
+let max_nb_const = 0x1000000
+let max_nb_block = 0x1000000 + last_variant_tag - 1
+
+let str_max_constructors =
+  Format.sprintf
+    " which has more than %i constant constructors or more than %i non-constant constructors" max_nb_const max_nb_block
+
+let check_compilable ib =
+
+  if not (ib.mind_nb_args <= max_nb_block && ib.mind_nb_constant <= max_nb_const) then
+    let msg =
+      Pp.(str "Cannot compile code for virtual machine as it uses inductive "
+          ++ Id.print ib.mind_typename ++ str str_max_constructors)
+    in
+    raise (TooLargeInductive msg)
+
+let is_value lc =
+  match lc with
+  | Lval _ -> true
+  | _ -> false
+
+let get_value lc =
+  match lc with
+  | Lval v -> v
+  | _ -> raise Not_found
+
+let mkConst_b0 n = Lval (Cbytecodes.Const_b0 n)
+
+let make_args start _end =
+  Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))
+
+(* Translation of constructors *)
+let expand_constructor tag nparams arity =
+  let ids = Array.make (nparams + arity) Anonymous in
+  if arity = 0 then mkLlam ids (mkConst_b0 tag)
+  else
+    let args = make_args arity 1 in
+    Llam(ids, Lmakeblock (tag, args))
+
+let makeblock tag nparams arity args =
+  let nargs = Array.length args in
+  if nparams > 0 || nargs < arity then
+    mkLapp (expand_constructor tag nparams arity) args
+  else
+    (* The constructor is fully applied *)
+  if arity = 0 then mkConst_b0 tag
+  else
+  if Array.for_all is_value args then
+    if tag < last_variant_tag then
+      Lval(Cbytecodes.Const_bn(tag, Array.map get_value args))
+    else
+      let args = Array.map get_value args in
+      let args = Array.append [|Cbytecodes.Const_b0 (tag - last_variant_tag) |] args in
+      Lval(Cbytecodes.Const_bn(last_variant_tag, args))
+  else Lmakeblock(tag, args)
+
+
+(* Compiling constants *)
+
+let rec get_alias env kn =
+  let cb = lookup_constant kn env in
+  let tps = cb.const_body_code in
+  match tps with
+  | None -> kn
+  | Some tps ->
+    (match Cemitcodes.force tps with
+     | Cemitcodes.BCalias kn' -> get_alias env kn'
+     | _ -> kn)
+
+(* Compilation of primitive *)
+
+let _h =  Name(Id.of_string "f")
+
+(*
+let expand_prim kn op arity =
+  let ids = Array.make arity Anonymous in
+  let args = make_args arity 1 in
+  Llam(ids, prim kn op args)
+*)
+
+let compile_prim n op kn fc args =
+  if not fc then raise Not_found
+  else
+    Lprim(kn, n, op, args)
+
+    (*
+  let (nparams, arity) = CPrimitives.arity op in
+  let expected = nparams + arity in
+  if Array.length args >= expected then prim kn op args
+  else mkLapp (expand_prim kn op expected) args
+*)
+
+(*i Global environment *)
+
+let get_names decl =
+  let decl = Array.of_list decl in
+  Array.map fst decl
+
+
+(* Rel Environment *)
+module Vect =
+struct
+  type 'a t = {
+    mutable elems : 'a array;
+    mutable size : int;
+  }
+
+  let make n a = {
+    elems = Array.make n a;
+    size = 0;
+  }
+
+  let extend v =
+    if v.size = Array.length v.elems then
+      let new_size = min (2*v.size) Sys.max_array_length in
+      if new_size <= v.size then raise (Invalid_argument "Vect.extend");
+      let new_elems = Array.make new_size v.elems.(0) in
+      Array.blit v.elems 0 new_elems 0 (v.size);
+      v.elems <- new_elems
+
+  let push v a =
+    extend v;
+    v.elems.(v.size) <- a;
+    v.size <- v.size + 1
+
+  let popn v n =
+    v.size <- max 0 (v.size - n)
+
+  let pop v = popn v 1
+
+  let get_last v n =
+    if v.size <= n then raise
+        (Invalid_argument "Vect.get:index out of bounds");
+    v.elems.(v.size - n - 1)
+
+end
+
+let dummy_lambda = Lrel(Anonymous, 0)
+
+let empty_args = [||]
+
+module Renv =
+struct
+
+  type constructor_info = tag * int * int (* nparam nrealargs *)
+
+  type t = {
+    global_env : env;
+    name_rel : Name.t Vect.t;
+    construct_tbl : (constructor, constructor_info) Hashtbl.t;
+  }
+
+  let make env = {
+    global_env = env;
+    name_rel = Vect.make 16 Anonymous;
+    construct_tbl = Hashtbl.create 111
+  }
+
+  let push_rel env id = Vect.push env.name_rel id
+
+  let push_rels env ids =
+    Array.iter (push_rel env) ids
+
+  let pop env = Vect.pop env.name_rel
+
+  let popn env n =
+    for _i = 1 to n do pop env done
+
+  let get env n =
+    Lrel (Vect.get_last env.name_rel (n-1), n)
+
+  let get_construct_info env c =
+    try Hashtbl.find env.construct_tbl c
+    with Not_found ->
+      let ((mind,j), i) = c in
+      let oib = lookup_mind mind env.global_env in
+      let oip = oib.mind_packets.(j) in
+      check_compilable oip;
+      let tag,arity = oip.mind_reloc_tbl.(i-1) in
+      let nparams = oib.mind_nparams in
+      let r = (tag, nparams, arity) in
+      Hashtbl.add env.construct_tbl c r;
+      r
+end
+
+open Renv
+
+let rec lambda_of_constr env c =
+  match Constr.kind c with
+  | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta")
+  | Evar _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr : Evar")
+
+  | Cast (c, _, _) -> lambda_of_constr env c
+
+  | Rel i -> Renv.get env i
+
+  | Var id -> Lvar id
+
+  | Sort s -> Lsort s
+  | Ind ind -> Lind ind
+
+  | Prod(id, dom, codom) ->
+    let ld = lambda_of_constr env dom in
+    Renv.push_rel env id;
+    let lc = lambda_of_constr env codom in
+    Renv.pop env;
+    Lprod(ld,  Llam([|id|], lc))
+
+  | Lambda _ ->
+    let params, body = decompose_lam c in
+    let ids = get_names (List.rev params) in
+    Renv.push_rels env ids;
+    let lb = lambda_of_constr env body in
+    Renv.popn env (Array.length ids);
+    mkLlam ids lb
+
+  | LetIn(id, def, _, body) ->
+    let ld = lambda_of_constr env def in
+    Renv.push_rel env id;
+    let lb = lambda_of_constr env body in
+    Renv.pop env;
+    Llet(id, ld, lb)
+
+  | App(f, args) -> lambda_of_app env f args
+
+  | Const _ -> lambda_of_app env c empty_args
+
+  | Construct _ ->  lambda_of_app env c empty_args
+
+  | Case(ci,t,a,branches) ->
+    let ind = ci.ci_ind in
+    let mib = lookup_mind (fst ind) env.global_env in
+    let oib = mib.mind_packets.(snd ind) in
+    let () = check_compilable oib in
+    let rtbl = oib.mind_reloc_tbl in
+
+
+    (* translation of the argument *)
+    let la = lambda_of_constr env a in
+    let entry = mkInd ind in
+    let la =
+      try
+        Retroknowledge.get_vm_before_match_info env.global_env.retroknowledge
+          entry la
+      with Not_found -> la
+    in
+    (* translation of the type *)
+    let lt = lambda_of_constr env t in
+    (* translation of branches *)
+    let consts = Array.make oib.mind_nb_constant dummy_lambda in
+    let blocks = Array.make oib.mind_nb_args ([||],dummy_lambda) in
+    for i = 0 to Array.length rtbl - 1 do
+      let tag, arity = rtbl.(i) in
+      let b = lambda_of_constr env branches.(i) in
+      if arity = 0 then consts.(tag) <- b
+      else
+        let b =
+          match b with
+          | Llam(ids, body) when Array.length ids = arity -> (ids, body)
+          | _ ->
+            let ids = Array.make arity Anonymous in
+            let args = make_args arity 1 in
+            let ll = lam_lift arity b in
+            (ids, mkLapp  ll args)
+        in blocks.(tag-1) <- b
+    done;
+    let branches =
+      { constant_branches = consts;
+        nonconstant_branches = blocks }
+    in
+    Lcase(ci, rtbl, lt, la, branches)
+
+  | Fix(rec_init,(names,type_bodies,rec_bodies)) ->
+    let ltypes = lambda_of_args env 0 type_bodies in
+    Renv.push_rels env names;
+    let lbodies = lambda_of_args env 0 rec_bodies in
+    Renv.popn env (Array.length names);
+    Lfix(rec_init, (names, ltypes, lbodies))
+
+  | CoFix(init,(names,type_bodies,rec_bodies)) ->
+    let ltypes = lambda_of_args env 0 type_bodies in
+    Renv.push_rels env names;
+    let lbodies = lambda_of_args env 0 rec_bodies in
+    Renv.popn env (Array.length names);
+    Lcofix(init, (names, ltypes, lbodies))
+
+  | Proj (p,c) ->
+    let kn = Projection.constant p in
+    let cb = lookup_constant kn env.global_env in
+    let pb = Option.get cb.const_proj in
+    let n = pb.proj_arg in
+    let lc = lambda_of_constr env c in
+    Lproj (n,kn,lc)
+
+and lambda_of_app env f args =
+  match Constr.kind f with
+  | Const (kn,u as c) ->
+    let kn = get_alias env.global_env kn in
+    (* spiwack: checks if there is a specific way to compile the constant
+                if there is not, Not_found is raised, and the function
+                falls back on its normal behavior *)
+    (try
+      (* We delay the compilation of arguments to avoid an exponential behavior *)
+      let f = Retroknowledge.get_vm_compiling_info env.global_env.retroknowledge
+          (mkConstU (kn,u)) in
+      let args = lambda_of_args env 0 args in
+      f args
+    with Not_found ->
+    let cb = lookup_constant kn env.global_env in
+    begin match cb.const_body with
+      | Def csubst when cb.const_inline_code ->
+        lambda_of_app env (Mod_subst.force_constr csubst) args
+      | Def _ | OpaqueDef _ | Undef _ -> mkLapp (Lconst c) (lambda_of_args env 0 args)
+    end)
+  | Construct (c,_) ->
+    let tag, nparams, arity = Renv.get_construct_info env c in
+    let nargs = Array.length args in
+    if Int.equal (nparams + arity) nargs then (* fully applied *)
+      (* spiwack: *)
+      (* 1/ tries to compile the constructor in an optimal way,
+            it is supposed to work only if the arguments are
+            all fully constructed, fails with Cbytecodes.NotClosed.
+            it can also raise Not_found when there is no special
+            treatment for this constructor
+            for instance: tries to to compile an integer of the
+                form I31 D1 D2 ... D31 to [D1D2...D31] as
+                a processor number (a caml number actually) *)
+      try
+        try
+          Retroknowledge.get_vm_constant_static_info
+            env.global_env.retroknowledge
+            f args
+        with NotClosed ->
+          (* 2/ if the arguments are not all closed (this is
+                              expectingly (and it is currently the case) the only
+                              reason why this exception is raised) tries to
+                              give a clever, run-time behavior to the constructor.
+                              Raises Not_found if there is no special treatment
+                              for this integer.
+                              this is done in a lazy fashion, using the constructor
+                              Bspecial because it needs to know the continuation
+                              and such, which can't be done at this time.
+                              for instance, for int31: if one of the digit is
+                                  not closed, it's not impossible that the number
+                                  gets fully instanciated at run-time, thus to ensure
+                                  uniqueness of the representation in the vm
+                                  it is necessary to try and build a caml integer
+                                  during the execution *)
+          let rargs = Array.sub args nparams arity in
+          let args = lambda_of_args env nparams rargs in
+          Retroknowledge.get_vm_constant_dynamic_info
+            env.global_env.retroknowledge
+            f args
+      with Not_found ->
+        (* 3/ if no special behavior is available, then the compiler
+           falls back to the normal behavior *)
+        let args = lambda_of_args env nparams args in
+        makeblock tag 0 arity args
+    else
+      let args = lambda_of_args env nparams args in
+      (* spiwack: tries first to apply the run-time compilation
+                behavior of the constructor, as in 2/ above *)
+      (try
+         (Retroknowledge.get_vm_constant_dynamic_info
+            env.global_env.retroknowledge
+            f) args
+       with Not_found ->
+         if nparams <= nargs then (* got all parameters *)
+           makeblock tag 0 arity args
+         else (* still expecting some parameters *)
+           makeblock tag (nparams - nargs) arity empty_args)
+  | _ ->
+    let f = lambda_of_constr env f in
+    let args = lambda_of_args env 0 args in
+    mkLapp f args
+
+and lambda_of_args env start args =
+  let nargs = Array.length args in
+  if start < nargs then
+    Array.init (nargs - start)
+      (fun i -> lambda_of_constr env args.(start + i))
+  else empty_args
+
+
+
+
+(*********************************)
+
+
+let optimize_lambda lam =
+  let lam = simplify subst_id lam in
+  remove_let subst_id lam
+
+let lambda_of_constr ~optimize genv c =
+  let env = Renv.make genv in
+  let ids = List.rev_map Context.Rel.Declaration.get_name genv.env_rel_context.env_rel_ctx in
+  Renv.push_rels env (Array.of_list ids);
+  let lam = lambda_of_constr env c in
+  let lam = if optimize then optimize_lambda lam else lam in
+  if !Flags.dump_lambda then
+    Feedback.msg_debug (pp_lam lam);
+  lam
+
+(** Retroknowledge, to be removed once we move to primitive machine integers *)
+let compile_structured_int31 fc args =
+  if not fc then raise Not_found else
+    Luint (UintVal
+    (Uint31.of_int (Array.fold_left
+       (fun temp_i -> fun t -> match kind t with
+          | Construct ((_,d),_) -> 2*temp_i+d-1
+          | _ -> raise NotClosed)
+       0 args)))
+
+let dynamic_int31_compilation fc args =
+  if not fc then raise Not_found else
+  Luint (UintDigits args)
+
+(* We are relying here on the tags of digits constructors *)
+let digits_from_uint i =
+  let d0 = mkConst_b0 0 in
+  let d1 = mkConst_b0 1 in
+  let digits = Array.make 31 d0 in
+  for k = 0 to 30 do
+    if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then
+      digits.(30-k) <- d1
+  done;
+  digits
+
+let int31_escape_before_match fc t =
+  if not fc then
+    raise Not_found
+  else
+  match t with
+  | Luint (UintVal i) ->
+    let digits = digits_from_uint i in
+    Lmakeblock (1, digits)
+  | Luint (UintDigits args) ->
+    Lmakeblock (1,args)
+  | Luint (UintDecomp _) ->
+    assert false
+  | _ -> Luint (UintDecomp t)
diff --git a/kernel/clambda.mli b/kernel/clambda.mli
new file mode 100644
index 000000000..89b7fd8e3
--- /dev/null
+++ b/kernel/clambda.mli
@@ -0,0 +1,27 @@
+open Names
+open Cinstr
+
+exception TooLargeInductive of Pp.t
+
+val lambda_of_constr : optimize:bool -> Pre_env.env -> Constr.t -> lambda
+
+val decompose_Llam : lambda -> Name.t array * lambda
+
+val get_alias : Pre_env.env -> Constant.t -> Constant.t
+
+val compile_prim : int -> Cbytecodes.instruction -> Constr.pconstant -> bool -> lambda array -> lambda
+
+(** spiwack: this function contains the information needed to perform
+            the static compilation of int31 (trying and obtaining
+            a 31-bit integer in processor representation at compile time) *)
+val compile_structured_int31 : bool -> Constr.t array -> lambda
+
+(** this function contains the information needed to perform
+        the dynamic compilation of int31 (trying and obtaining a
+        31-bit integer in processor representation at runtime when
+        it failed at compile time *)
+val dynamic_int31_compilation : bool -> lambda array -> lambda
+
+(*spiwack: compiling function to insert dynamic decompilation before
+           matching integers (in case they are in processor representation) *)
+val int31_escape_before_match : bool -> lambda -> lambda
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 55430a9d8..236d83576 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -164,7 +164,7 @@ and eval_to_patch env (buff,pl,fv) =
   eval_tcode tc vm_env
 
 and val_of_constr env c =
-  match compile true env c with
+  match compile ~fail_on_error:true env c with
   | Some v -> eval_to_patch env (to_memory v)
   | None -> assert false
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 738ecc6e1..fe5a7dfb5 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -468,7 +468,7 @@ type unsafe_type_judgment = types punsafe_type_judgment
 
 (*s Compilation of global declaration *)
 
-let compile_constant_body = Cbytegen.compile_constant_body false
+let compile_constant_body = Cbytegen.compile_constant_body ~fail_on_error:false
 
 exception Hyp_not_found
 
@@ -560,7 +560,7 @@ let dispatch =
      it to the name of the coq definition in the reactive retroknowledge) *)
   let int31_op n op prim kn =
     { empty_reactive_info with
-      vm_compiling = Some (Cbytegen.op_compilation n op kn);
+      vm_compiling = Some (Clambda.compile_prim n op kn);
       native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn));
     }
   in
@@ -599,13 +599,13 @@ fun rk value field ->
         in
         { empty_reactive_info with
           vm_decompile_const = Some int31_decompilation;
-          vm_before_match = Some Cbytegen.int31_escape_before_match;
+          vm_before_match = Some Clambda.int31_escape_before_match;
           native_before_match = Some (Nativelambda.before_match_int31 i31bit_type);
         }
     | KInt31 (_, Int31Constructor) ->
         { empty_reactive_info with
-          vm_constant_static = Some Cbytegen.compile_structured_int31;
-          vm_constant_dynamic = Some Cbytegen.dynamic_int31_compilation;
+          vm_constant_static = Some Clambda.compile_structured_int31;
+          vm_constant_dynamic = Some Clambda.dynamic_int31_compilation;
           native_constant_static = Some Nativelambda.compile_static_int31;
           native_constant_dynamic = Some Nativelambda.compile_dynamic_int31;
         }
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 749854b8c..370185a72 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -23,8 +23,9 @@ Declareops
 Retroknowledge
 Conv_oracle
 Pre_env
-Cbytegen
+Clambda
 Nativelambda
+Cbytegen
 Nativecode
 Nativelib
 Environ
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 88cf93acc..24d022d69 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -102,20 +102,18 @@ module Reactive = Map.Make (EntryOrd)
 type reactive_info = {(*information required by the compiler of the VM *)
   vm_compiling :
       (*fastcomputation flag -> continuation -> result *)
-      (bool -> Cbytecodes.comp_env -> constr array ->
-       int->Cbytecodes.bytecodes->Cbytecodes.bytecodes)
+      (bool -> Cinstr.lambda array -> Cinstr.lambda)
       option;
   vm_constant_static :
       (*fastcomputation flag -> constructor -> args -> result*)
-      (bool->constr array->Cbytecodes.structured_constant)
+      (bool -> constr array -> Cinstr.lambda)
       option;
   vm_constant_dynamic :
       (*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *)
-      (bool->Cbytecodes.comp_env->Cbytecodes.block array->int->
-         Cbytecodes.bytecodes->Cbytecodes.bytecodes)
+      (bool -> Cinstr.lambda array -> Cinstr.lambda)
       option;
   (* fastcomputation flag -> cont -> result *)
-  vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
+  vm_before_match : (bool -> Cinstr.lambda -> Cinstr.lambda) option;
   (* tag (= compiled int for instance) -> result *)
   vm_decompile_const : (int -> constr) option;
 
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index e4d78ba14..134b4b4f7 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -82,9 +82,8 @@ val initial_retroknowledge : retroknowledge
    and the continuation cont of the bytecode compilation
    returns the compilation of id in cont if it has a specific treatment
    or raises Not_found if id should be compiled as usual *)
-val get_vm_compiling_info  : retroknowledge -> entry -> Cbytecodes.comp_env ->
-                             constr array ->
-                             int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes
+val get_vm_compiling_info  : retroknowledge -> entry ->
+                             Cinstr.lambda array -> Cinstr.lambda
 (*Given an identifier id (usually Construct _)
    and its argument array, returns a function that tries an ad-hoc optimisated
    compilation (in the case of the 31-bit integers it means compiling them
@@ -93,8 +92,7 @@ val get_vm_compiling_info  : retroknowledge -> entry -> Cbytecodes.comp_env ->
    CBytecodes.NotClosed if the term is not a closed constructor pattern
    (a constant for the compiler) *)
 val get_vm_constant_static_info : retroknowledge -> entry ->
-                                   constr array ->
-                                   Cbytecodes.structured_constant
+                                   constr array -> Cinstr.lambda
 
 (*Given an identifier id (usually Construct _ )
    its argument array and a continuation, returns the compiled version
@@ -102,16 +100,14 @@ val get_vm_constant_static_info : retroknowledge -> entry ->
    31-bit integers, that would be the dynamic compilation into integers)
    or raises Not_found if id should be compiled as usual *)
 val get_vm_constant_dynamic_info : retroknowledge -> entry ->
-                                Cbytecodes.comp_env ->
-                                Cbytecodes.block array ->
-                                int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes
+                                   Cinstr.lambda array -> Cinstr.lambda
 
 (** Given a type identifier, this function is used before compiling a match
    over this type. In the case of 31-bit integers for instance, it is used
    to add the instruction sequence which would perform a dynamic decompilation
    in case the argument of the match is not in coq representation *)
-val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes
-                                                       -> Cbytecodes.bytecodes
+val get_vm_before_match_info : retroknowledge -> entry -> Cinstr.lambda
+                                                       -> Cinstr.lambda
 
 (** Given a type identifier, this function is used by pretyping/vnorm.ml to
    recover the elements of that type from their compiled form if it's non
@@ -148,20 +144,18 @@ val find : retroknowledge -> field -> entry
 type reactive_info = {(*information required by the compiler of the VM *)
   vm_compiling :
       (*fastcomputation flag -> continuation -> result *)
-      (bool->Cbytecodes.comp_env->constr array ->
-       int->Cbytecodes.bytecodes->Cbytecodes.bytecodes)
+      (bool -> Cinstr.lambda array -> Cinstr.lambda)
       option;
   vm_constant_static :
       (*fastcomputation flag -> constructor -> args -> result*)
-      (bool->constr array->Cbytecodes.structured_constant)
+      (bool -> constr array -> Cinstr.lambda)
       option;
   vm_constant_dynamic :
       (*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *)
-      (bool->Cbytecodes.comp_env->Cbytecodes.block array->int->
-         Cbytecodes.bytecodes->Cbytecodes.bytecodes)
+      (bool -> Cinstr.lambda array -> Cinstr.lambda)
       option;
   (* fastcomputation flag -> cont -> result *)
-  vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
+  vm_before_match : (bool -> Cinstr.lambda -> Cinstr.lambda) option;
   (* tag (= compiled int for instance) -> result *)
   vm_decompile_const : (int -> constr) option;
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 415e4399a..5da131020 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -170,3 +170,7 @@ let profile_ltac_cutoff = ref 2.0
 let dump_bytecode = ref false
 let set_dump_bytecode = (:=) dump_bytecode
 let get_dump_bytecode () = !dump_bytecode
+
+let dump_lambda = ref false
+let set_dump_lambda = (:=) dump_lambda
+let get_dump_lambda () = !dump_lambda
diff --git a/lib/flags.mli b/lib/flags.mli
index c82410f07..bc07dec80 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -132,3 +132,8 @@ val profile_ltac_cutoff : float ref
 val dump_bytecode : bool ref
 val set_dump_bytecode : bool -> unit
 val get_dump_bytecode : unit -> bool
+
+(** Dump the VM lambda code after compilation (for debugging purposes) *)
+val dump_lambda : bool ref
+val set_dump_lambda : bool -> unit
+val get_dump_lambda : unit -> bool
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 35ef4bfa4..ca904d50b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1466,6 +1466,14 @@ let _ =
 let _ =
   declare_bool_option
     { optdepr  = false;
+      optname  = "dumping VM lambda code after compilation";
+      optkey   = ["Dump";"Lambda"];
+      optread  = Flags.get_dump_lambda;
+      optwrite = Flags.set_dump_lambda }
+
+let _ =
+  declare_bool_option
+    { optdepr  = false;
       optname  = "explicitly parsing implicit arguments";
       optkey   = ["Parsing";"Explicit"];
       optread  = (fun () -> !Constrintern.parsing_explicit);