Machine arithmetic operations for native compiler.

This completes the port of the native compiler to retroknowledge.
However, some testing and optimizations are still to be done.

13 files changed, 669 insertions, 71 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index c56982d99..1e2764997 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -62,6 +62,7 @@ Cbytecodes
 Copcodes
 Cemitcodes
 Nativevalues
+Primitives
 Nativeinstr
 Future
 Opaqueproof
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5a40b1c2a..be0b65d91 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -477,8 +477,11 @@ let register =
   (* subfunction which adds the compiling information of an
      int31 operation which has a specific vm instruction (associates
      it to the name of the coq definition in the reactive retroknowledge) *)
-  let add_int31_op retroknowledge v n op kn =
-    add_vm_compiling_info retroknowledge v (Cbytegen.op_compilation n op kn)
+  let add_int31_op retroknowledge v n op prim kn =
+    let rk =
+      add_vm_compiling_info retroknowledge v (Cbytegen.op_compilation n op kn)
+    in
+    add_native_compiling_info rk v (Nativelambda.compile_prim prim kn)
   in
 
   let add_int31_before_match rk v =
@@ -490,16 +493,16 @@ let register =
 fun env field value ->
   (* subfunction which shortens the (very often use) registration of binary
      operators to the reactive retroknowledge. *)
-  let add_int31_binop_from_const op =
+  let add_int31_binop_from_const op prim =
     match kind_of_term value with
       | Const kn ->  retroknowledge add_int31_op env value 2
-	                               op kn
+	                               op prim kn
       | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
   in
-  let add_int31_unop_from_const op =
+  let add_int31_unop_from_const op prim =
     match kind_of_term value with
       | Const kn ->  retroknowledge add_int31_op env value 1
-	                               op kn
+	                               op prim kn
       | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
   in
   (* subfunction which completes the function constr_of_int31 above
@@ -531,33 +534,47 @@ fun env field value ->
 	  (add_int31_before_match
 	     (retroknowledge add_int31c env i31c) value)
     | KInt31 (_, Int31Plus) -> add_int31_binop_from_const Cbytecodes.Kaddint31
+							  Primitives.Int31add
     | KInt31 (_, Int31PlusC) -> add_int31_binop_from_const Cbytecodes.Kaddcint31
+							   Primitives.Int31addc
     | KInt31 (_, Int31PlusCarryC) -> add_int31_binop_from_const Cbytecodes.Kaddcarrycint31
+								Primitives.Int31addcarryc
     | KInt31 (_, Int31Minus) -> add_int31_binop_from_const Cbytecodes.Ksubint31
+							   Primitives.Int31sub
     | KInt31 (_, Int31MinusC) -> add_int31_binop_from_const Cbytecodes.Ksubcint31
+							    Primitives.Int31subc
     | KInt31 (_, Int31MinusCarryC) -> add_int31_binop_from_const
-	                                           Cbytecodes.Ksubcarrycint31
+	                                Cbytecodes.Ksubcarrycint31 Primitives.Int31subcarryc
     | KInt31 (_, Int31Times) -> add_int31_binop_from_const Cbytecodes.Kmulint31
+							   Primitives.Int31mul
     | KInt31 (_, Int31TimesC) -> add_int31_binop_from_const Cbytecodes.Kmulcint31
+							    Primitives.Int31mulc
     | KInt31 (_, Int31Div21) -> (* this is a ternary operation *)
                                 (match kind_of_term value with
 				 | Const kn ->
 				     retroknowledge add_int31_op env value 3
-	                               Cbytecodes.Kdiv21int31 kn
+	                               Cbytecodes.Kdiv21int31 Primitives.Int31div21 kn
 				 | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant"))
     | KInt31 (_, Int31Div) -> add_int31_binop_from_const Cbytecodes.Kdivint31
+							 Primitives.Int31div
     | KInt31 (_, Int31AddMulDiv) -> (* this is a ternary operation *)
                                 (match kind_of_term value with
 				 | Const kn ->
 				     retroknowledge add_int31_op env value 3
-	                               Cbytecodes.Kaddmuldivint31 kn
+	                               Cbytecodes.Kaddmuldivint31 Primitives.Int31addmuldiv kn
 				 | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant"))
     | KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31
+							     Primitives.Int31compare
     | KInt31 (_, Int31Head0) -> add_int31_unop_from_const Cbytecodes.Khead0int31
+							  Primitives.Int31head0
     | KInt31 (_, Int31Tail0) -> add_int31_unop_from_const Cbytecodes.Ktail0int31
+							  Primitives.Int31tail0
     | KInt31 (_, Int31Lor) -> add_int31_binop_from_const Cbytecodes.Klorint31
+							 Primitives.Int31lor
     | KInt31 (_, Int31Land) -> add_int31_binop_from_const Cbytecodes.Klandint31
+							  Primitives.Int31land
     | KInt31 (_, Int31Lxor) -> add_int31_binop_from_const Cbytecodes.Klxorint31
+							  Primitives.Int31lxor
     | _ -> env.retroknowledge
   in
   Retroknowledge.add_field retroknowledge_with_reactive_info field value
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 3267b7e75..0d0adf9a7 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -13,6 +13,7 @@ Cbytecodes
 Copcodes
 Cemitcodes
 Nativevalues
+Primitives
 Nativeinstr
 Opaqueproof
 Declareops
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c4ede775e..c8572eec3 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -12,6 +12,7 @@ open Context
 open Declarations
 open Util
 open Nativevalues
+open Primitives
 open Nativeinstr
 open Nativelambda
 open Pre_env
@@ -255,14 +256,32 @@ type primitive =
   | Mk_rel of int
   | Mk_var of identifier
   | Is_accu
+  | Is_int
   | Cast_accu
   | Upd_cofix
   | Force_cofix
   | Mk_uint
+  | Mk_int
+  | Mk_bool
+  | Val_to_int
   | Mk_I31_accu
   | Decomp_uint
   | Mk_meta
   | Mk_evar
+  | MLand
+  | MLle
+  | MLlt
+  | MLinteq
+  | MLlsl
+  | MLlsr
+  | MLland
+  | MLlor
+  | MLlxor
+  | MLadd
+  | MLsub
+  | MLmul
+  | MLmagic
+  | Coq_primitive of Primitives.t * (prefix * constant) option
 
 let eq_primitive p1 p2 =
   match p1, p2 with
@@ -284,29 +303,49 @@ let eq_primitive p1 p2 =
   | _ -> false
 
 let primitive_hash = function
-| Mk_prod -> 1
-| Mk_sort -> 2
-| Mk_ind -> 3
-| Mk_const -> 4
-| Mk_sw -> 5
-| Mk_fix (r, i) ->
-  let h = Array.fold_left (fun h i -> combine h (Int.hash i)) 0 r in
-  combinesmall 6 (combine h (Int.hash i))
-| Mk_cofix i ->
-  combinesmall 7 (Int.hash i)
-| Mk_rel i ->
-  combinesmall 8 (Int.hash i)
-| Mk_var id ->
-  combinesmall 9 (Id.hash id)
-| Is_accu -> 10
-| Cast_accu -> 11
-| Upd_cofix -> 12
-| Force_cofix -> 13
-| Mk_uint -> 14
-| Mk_I31_accu -> 15
-| Decomp_uint -> 16
-| Mk_meta -> 17
-| Mk_evar -> 18
+  | Mk_prod -> 1
+  | Mk_sort -> 2
+  | Mk_ind -> 3
+  | Mk_const -> 4
+  | Mk_sw -> 5
+  | Mk_fix (r, i) ->
+     let h = Array.fold_left (fun h i -> combine h (Int.hash i)) 0 r in
+     combinesmall 6 (combine h (Int.hash i))
+  | Mk_cofix i ->
+     combinesmall 7 (Int.hash i)
+  | Mk_rel i ->
+     combinesmall 8 (Int.hash i)
+  | Mk_var id ->
+     combinesmall 9 (Id.hash id)
+  | Is_accu -> 10
+  | Is_int -> 11
+  | Cast_accu -> 12
+  | Upd_cofix -> 13
+  | Force_cofix -> 14
+  | Mk_uint -> 15
+  | Mk_int -> 16
+  | Mk_bool -> 17
+  | Val_to_int -> 18
+  | Mk_I31_accu -> 19
+  | Decomp_uint -> 20
+  | Mk_meta -> 21
+  | Mk_evar -> 22
+  | MLand -> 23
+  | MLle -> 24
+  | MLlt -> 25
+  | MLinteq -> 26
+  | MLlsl -> 27
+  | MLlsr -> 28
+  | MLland -> 29
+  | MLlor -> 30
+  | MLlxor -> 31
+  | MLadd -> 32
+  | MLsub -> 33
+  | MLmul -> 34
+  | MLmagic -> 35
+  | Coq_primitive (prim, None) -> combinesmall 36 (Primitives.hash prim)
+  | Coq_primitive (prim, Some (prefix,kn)) ->
+     combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (Primitives.hash prim))
 
 type mllambda =
   | MLlocal        of lname 
@@ -828,6 +867,113 @@ let merge_branches t =
   Array.iter (fun (c,args,body) -> insert (c,args) body newt) t;
   Array.of_list (to_list newt)
 
+
+type prim_aux = 
+  | PAprim of string * constant * Primitives.t * prim_aux array
+  | PAml of mllambda
+
+let add_check cond args =
+  let aux cond a = 
+    match a with
+    | PAml(MLint _) -> cond
+    | PAml ml ->
+       (* FIXME: use explicit equality function *)
+       if List.mem ml cond then cond else ml::cond 
+    | _ -> cond
+  in
+  Array.fold_left aux cond args
+  
+let extract_prim ml_of l =
+  let decl = ref [] in
+  let cond = ref [] in
+  let rec aux l = 
+    match l with
+    | Lprim(prefix,kn,p,args) ->
+	let args = Array.map aux args in
+	cond := add_check !cond args;
+	PAprim(prefix,kn,p,args)
+    | Lrel _ | Lvar _ | Luint _ | Lval _ | Lconst _ -> PAml (ml_of l)
+    | _ -> 
+	let x = fresh_lname Anonymous in
+	decl := (x,ml_of l)::!decl;
+	PAml (MLlocal x) in
+  let res = aux l in
+  (!decl, !cond, res)
+
+let app_prim p args = MLapp(MLprimitive p, args)
+
+let to_int v =
+  match v with
+  | MLapp(MLprimitive Mk_uint, t) ->
+     begin match t.(0) with
+     | MLuint i -> MLint (Uint31.to_int i)
+     | _ -> MLapp(MLprimitive Val_to_int, [|v|])
+     end
+  | MLapp(MLprimitive Mk_int, t) -> t.(0)
+  | _ -> MLapp(MLprimitive Val_to_int, [|v|]) 
+
+let of_int v = 
+  match v with
+  | MLapp(MLprimitive Val_to_int, t) -> t.(0)
+  | _ -> MLapp(MLprimitive Mk_int,[|v|]) 
+
+let compile_prim decl cond paux =
+(*
+  let args_to_int args = 
+    for i = 0 to Array.length args - 1 do
+      args.(i) <- to_int args.(i)
+    done;
+    args in
+ *)
+  let rec opt_prim_aux paux =
+    match paux with
+    | PAprim(prefix, kn, op, args) ->
+	let args = Array.map opt_prim_aux args in
+	app_prim (Coq_primitive(op,None)) args
+(*
+    TODO: check if this inling was useful
+	begin match op with
+        | Int31lt -> 
+           if Sys.word_size = 64 then
+             app_prim Mk_bool [|(app_prim MLlt (args_to_int args))|]
+           else app_prim (Coq_primitive (Primitives.Int31lt,None)) args
+        | Int31le ->
+           if Sys.word_size = 64 then
+             app_prim Mk_bool [|(app_prim MLle (args_to_int args))|]
+           else app_prim (Coq_primitive (Primitives.Int31le, None)) args
+	| Int31lsl  -> of_int (mk_lsl (args_to_int args))
+	| Int31lsr  -> of_int (mk_lsr (args_to_int args))
+	| Int31land -> of_int (mk_land (args_to_int args))
+	| Int31lor  -> of_int (mk_lor (args_to_int args))
+	| Int31lxor -> of_int (mk_lxor (args_to_int args))
+	| Int31add  -> of_int (mk_add (args_to_int args))
+	| Int31sub  -> of_int (mk_sub (args_to_int args))
+	| Int31mul  -> of_int (mk_mul (args_to_int args))
+	| _ -> app_prim (Coq_primitive(op,None)) args
+	end *)
+    | PAml ml -> ml 
+  and naive_prim_aux paux = 
+    match paux with
+    | PAprim(prefix, kn, op, args) ->
+        app_prim (Coq_primitive(op, Some (prefix, kn))) (Array.map naive_prim_aux args)
+    | PAml ml -> ml in
+
+  let compile_cond cond paux = 
+    match cond with
+    | [] -> opt_prim_aux paux 
+    | [c1] ->
+        MLif(app_prim Is_int [|c1|], opt_prim_aux paux, naive_prim_aux paux) 
+    | c1::cond ->
+	let cond = 
+	  List.fold_left 
+	    (fun ml c -> app_prim MLland [| ml; to_int c|])
+            (app_prim MLland [|to_int c1; MLint 0 |]) cond in
+        let cond = app_prim MLmagic [|cond|] in
+	MLif(cond, naive_prim_aux paux, opt_prim_aux paux) in
+  let add_decl decl body =
+    List.fold_left (fun body (x,d) -> MLlet(x,d,body)) body decl in
+  add_decl decl (compile_cond cond paux)
+
  let rec ml_of_lam env l t =
   match t with
   | Lrel(id ,i) -> get_rel env id i
@@ -858,6 +1004,9 @@ let merge_branches t =
   | Lapp(f,args) ->
       MLapp(ml_of_lam env l f, Array.map (ml_of_lam env l) args)
   | Lconst (prefix,c) -> MLglobal(Gconstant (prefix,c))
+  | Lprim _ ->
+      let decl,cond,paux = extract_prim (ml_of_lam env l) t in
+      compile_prim decl cond paux
   | Lcase (annot,p,a,bs) ->
       (* let predicate_uid fv_pred = compilation of p 
          let rec case_uid fv a_uid = 
@@ -1482,14 +1631,36 @@ let pp_mllam fmt l =
     | Mk_var id ->
         Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id)
     | Is_accu -> Format.fprintf fmt "is_accu"
+    | Is_int -> Format.fprintf fmt "is_int"
     | Cast_accu -> Format.fprintf fmt "cast_accu"
     | Upd_cofix -> Format.fprintf fmt "upd_cofix"
     | Force_cofix -> Format.fprintf fmt "force_cofix"
     | Mk_uint -> Format.fprintf fmt "mk_uint"
+    | Mk_int -> Format.fprintf fmt "mk_int"
+    | Mk_bool -> Format.fprintf fmt "mk_bool"
+    | Val_to_int -> Format.fprintf fmt "val_to_int"
     | Mk_I31_accu -> Format.fprintf fmt "mk_I31_accu"
     | Decomp_uint -> Format.fprintf fmt "decomp_uint"
     | Mk_meta -> Format.fprintf fmt "mk_meta_accu"
     | Mk_evar -> Format.fprintf fmt "mk_evar_accu"
+    | MLand -> Format.fprintf fmt "(&&)"
+    | MLle -> Format.fprintf fmt "(<=)"
+    | MLlt -> Format.fprintf fmt "(<)"
+    | MLinteq -> Format.fprintf fmt "(==)"
+    | MLlsl -> Format.fprintf fmt "(lsl)"
+    | MLlsr -> Format.fprintf fmt "(lsr)"
+    | MLland -> Format.fprintf fmt "(land)"
+    | MLlor -> Format.fprintf fmt "(lor)"
+    | MLlxor -> Format.fprintf fmt "(lxor)"
+    | MLadd -> Format.fprintf fmt "(+)"
+    | MLsub -> Format.fprintf fmt "(-)"
+    | MLmul -> Format.fprintf fmt "( * )"
+    | MLmagic -> Format.fprintf fmt "Obj.magic"
+    | Coq_primitive (op,None) ->
+       Format.fprintf fmt "no_check_%s" (Primitives.to_string op)
+    | Coq_primitive (op, Some (prefix,kn)) ->
+        Format.fprintf fmt "%s %a" (Primitives.to_string op)
+		       pp_mllam (MLglobal (Gconstant (prefix,kn)))
   in
   Format.fprintf fmt "@[%a@]" pp_mllam l
   
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index bba011475..13d61841f 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -29,6 +29,7 @@ and lambda =
   | Llet          of name * lambda * lambda
   | Lapp          of lambda * lambda array
   | Lconst        of prefix * constant
+  | Lprim         of prefix * constant * Primitives.t * lambda array
   | Lcase         of annot_sw * lambda * lambda * lam_branches 
                   (* annotations, term being matched, accu, branches *)
   | Lif           of lambda * lambda * lambda
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index f6fb25ab0..631349c07 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -101,6 +101,9 @@ let map_lam_with_binders g f n lam =
       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'
+  | Lprim(prefix,kn,op,args) ->
+      let args' = Array.smartmap (f n) args in
+      if args == args' then lam else Lprim(prefix,kn,op,args')
   | Lcase(annot,t,a,br) ->
       let t' = f n t in
       let a' = f n a in
@@ -297,7 +300,7 @@ let rec occurence k kind lam =
       occurence (k+1) (occurence k kind def) body
   | Lapp(f, args) ->
       occurence_args k (occurence k kind f) args
-  | Lmakeblock(_,_,_,args) ->
+  | Lprim(_,_,_,args) | Lmakeblock(_,_,_,args) ->
       occurence_args k kind args
   | Lcase(_,t,a,br) ->
       let kind = occurence k (occurence k kind t) a in
@@ -626,6 +629,12 @@ and lambda_of_app env sigma f args =
   | Const kn ->
       let kn = get_allias !global_env kn in
       let cb = lookup_constant kn !global_env in
+      (try
+          let prefix = get_const_prefix !global_env kn in
+	  let args = lambda_of_args env sigma 0 args in
+	  Retroknowledge.get_native_compiling_info
+		    (!global_env).retroknowledge (mkConst kn) prefix args
+      with Not_found ->
       begin match cb.const_body with
       | Def csubst ->
           if cb.const_inline_code then
@@ -641,7 +650,7 @@ and lambda_of_app env sigma f args =
       | OpaqueDef _ | Undef _ ->
           let prefix = get_const_prefix !global_env kn in
           mkLapp (Lconst (prefix, kn)) (lambda_of_args env sigma 0 args)
-      end
+      end)
   | Construct c ->
       let tag, nparams, arity = Renv.get_construct_info env c in
       let expected = nparams + arity in
@@ -726,3 +735,8 @@ let before_match_int31 fc prefix c t =
   | Luint (UintVal i) -> assert false
   | Luint (UintDigits (prefix,c,args)) -> assert false
   | _ -> Luint (UintDecomp (prefix,c,t))
+
+let compile_prim prim kn fc prefix args =
+  if not fc then raise Not_found
+  else
+    Lprim(prefix, kn, prim, args)
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 8ff0d727c..afebf8087 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -37,3 +37,5 @@ val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array ->
 
 val before_match_int31 : bool -> prefix -> constructor -> lambda -> lambda
 
+val compile_prim : Primitives.t -> constant -> bool -> prefix -> lambda array ->
+		   lambda
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 7f2785cf9..ab56c4be0 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -222,6 +222,8 @@ let dummy_value : unit -> t =
 let cast_accu v = (Obj.magic v:accumulator)
 
 let mk_int (x : int) = (Obj.magic x : t)
+(* Coq's booleans are reversed... *)
+let mk_bool (b : bool) = (Obj.magic (not b) : t)
 let mk_uint (x : Uint31.t) = (Obj.magic x : t)
 
 type block
@@ -260,7 +262,223 @@ let is_int (x:t) =
   let o = Obj.repr x in
   Obj.is_int o
 
-let to_int (x:t) = (Obj.magic x : int)
+let val_to_int (x:t) = (Obj.magic x : int)
+
+let to_uint (x:t) = (Obj.magic x : Uint31.t)
+let of_uint (x: Uint31.t) = (Obj.magic x : t)
+
+let no_check_head0 x =
+ of_uint (Uint31.head0 (to_uint x))
+
+let head0 accu x =
+ if is_int x then  no_check_head0 x
+ else accu x
+
+let no_check_tail0 x =
+  of_uint (Uint31.tail0 (to_uint x))
+
+let tail0 accu x =
+ if is_int x then no_check_tail0 x
+ else accu x
+
+let no_check_add  x y =
+  of_uint (Uint31.add (to_uint x) (to_uint y))
+
+let add accu x y =
+  if is_int x && is_int y then no_check_add x y 
+  else accu x y
+
+let no_check_sub x y =
+     of_uint (Uint31.sub (to_uint x) (to_uint y))
+
+let sub accu x y =
+  if is_int x && is_int y then no_check_sub x y
+  else accu x y
+
+let no_check_mul x y =
+  of_uint (Uint31.mul (to_uint x) (to_uint y))
+
+let mul accu x y =
+  if is_int x && is_int y then no_check_mul x y
+  else accu x y
+
+let no_check_div x y =
+  of_uint (Uint31.div (to_uint x) (to_uint y))
+
+let div accu x y =
+  if is_int x && is_int y then no_check_div x y 
+  else accu x y
+
+let no_check_rem x y =
+  of_uint (Uint31.rem (to_uint x) (to_uint y))
+
+let rem accu x y =
+  if is_int x && is_int y then no_check_rem x y
+  else accu x y
+
+let no_check_l_sr x y =
+  of_uint (Uint31.l_sr (to_uint x) (to_uint y))
+
+let l_sr accu x y =
+  if is_int x && is_int y then no_check_l_sr x y
+  else accu x y
+
+let no_check_l_sl x y =
+  of_uint (Uint31.l_sl (to_uint x) (to_uint y))
+
+let l_sl accu x y =
+  if is_int x && is_int y then no_check_l_sl x y
+  else accu x y
+
+let no_check_l_and x y =
+  of_uint (Uint31.l_and (to_uint x) (to_uint y))
+
+let l_and accu x y =
+  if is_int x && is_int y then no_check_l_and x y
+  else accu x y
+
+let no_check_l_xor x y =
+  of_uint (Uint31.l_xor (to_uint x) (to_uint y))
+
+let l_xor accu x y =
+  if is_int x && is_int y then no_check_l_xor x y
+  else accu x y
+
+let no_check_l_or x y =
+  of_uint (Uint31.l_or (to_uint x) (to_uint y))
+
+let l_or accu x y =
+  if is_int x && is_int y then no_check_l_or x y
+  else accu x y
+
+type coq_carry = 
+  | Caccu of t
+  | C0 of t
+  | C1 of t
+
+type coq_pair = 
+  | Paccu of t
+  | PPair of t * t
+
+let mkCarry b i =
+  if b then (Obj.magic (C1(of_uint i)):t)
+  else (Obj.magic (C0(of_uint i)):t)
+
+let no_check_addc x y =
+  let s = Uint31.add (to_uint x) (to_uint y) in
+  mkCarry (Uint31.lt s (to_uint x)) s
+
+let addc accu x y =
+  if is_int x && is_int y then no_check_addc x y
+  else accu x y
+
+let no_check_subc x y =
+  let s = Uint31.sub (to_uint x) (to_uint y) in
+  mkCarry (Uint31.lt (to_uint x) (to_uint y)) s
+
+let subc accu x y =
+  if is_int x && is_int y then no_check_subc x y
+  else accu x y
+
+let no_check_addCarryC x y =
+  let s = 
+    Uint31.add (Uint31.add (to_uint x) (to_uint y))
+      (Uint31.of_int 1) in
+  mkCarry (Uint31.le s (to_uint x)) s
+
+let addCarryC accu x y =
+  if is_int x && is_int y then no_check_addCarryC x y
+  else accu x y 
+
+let no_check_subCarryC x y =
+  let s = 
+    Uint31.sub (Uint31.sub (to_uint x) (to_uint y))
+      (Uint31.of_int 1) in
+  mkCarry (Uint31.le (to_uint x) (to_uint y)) s
+
+let subCarryC accu x y =
+  if is_int x && is_int y then no_check_subCarryC x y
+  else accu x y 
+
+let of_pair (x, y) =
+  (Obj.magic (PPair(of_uint x, of_uint y)):t)
+
+let no_check_mulc x y =
+    of_pair(Uint31.mulc (to_uint x) (to_uint y))
+
+let mulc accu x y =
+  if is_int x && is_int y then no_check_mulc x y
+  else accu x y
+
+let no_check_diveucl x y =
+  let i1, i2 = to_uint x, to_uint y in
+  of_pair(Uint31.div i1 i2, Uint31.rem i1 i2)
+
+let diveucl accu x y =
+  if is_int x && is_int y then no_check_diveucl x y
+  else accu x y
+
+let no_check_div21 x y z =
+  let i1, i2, i3 = to_uint x, to_uint y, to_uint z in
+  of_pair (Uint31.div21 i1 i2 i3)
+
+let div21 accu x y z =
+  if is_int x && is_int y && is_int z then no_check_div21 x y z
+  else accu x y z
+
+let no_check_addMulDiv x y z =
+  let p, i, j = to_uint x, to_uint y, to_uint z in
+  let p' = Uint31.to_int p in
+  of_uint (Uint31.l_or 
+	     (Uint31.l_sl i p) 
+	     (Uint31.l_sr j (Uint31.of_int (31 - p'))))
+
+let addMulDiv accu x y z =
+  if is_int x && is_int y && is_int z then no_check_addMulDiv x y z
+  else accu x y z
+
+
+type coq_bool =
+  | Baccu of t
+  | Btrue
+  | Bfalse
+
+type coq_cmp =
+  | CmpAccu of t
+  | CmpEq 
+  | CmpLt
+  | CmpGt
+
+let no_check_eq x y =     
+  mk_bool (Uint31.equal (to_uint x) (to_uint y))
+
+let eq accu x y =
+  if is_int x && is_int y then no_check_eq x y
+  else accu x y
+
+let no_check_lt x y =
+  mk_bool (Uint31.lt (to_uint x) (to_uint y))
+
+let lt accu x y =
+  if is_int x && is_int y then no_check_lt x y
+  else accu x y
+
+let no_check_le x y =
+  mk_bool (Uint31.le (to_uint x) (to_uint y))
+
+let le accu x y =
+  if is_int x && is_int y then no_check_le x y
+  else accu x y
+
+let no_check_compare x y =
+  match Uint31.compare (to_uint x) (to_uint y) with
+  | x when x < 0 -> (Obj.magic CmpLt:t)
+  | 0 -> (Obj.magic CmpEq:t)
+  | _ -> (Obj.magic CmpGt:t)
+
+let compare accu x y =
+  if is_int x && is_int y then no_check_compare x y
+  else accu x y
 
 let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%.2x" i)
 let bohcnv = Array.init 256 (fun i -> i -
@@ -340,7 +558,7 @@ let mk_I31_accu c x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17
 let decomp_uint c v =
   if is_int v then
     let r = ref c in
-    let v = to_int v in
+    let v = val_to_int v in
     for i = 30 downto 0 do
       r := (!r) (mk_int ((v lsr i) land 1));
     done;
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 821b23168..9b0ce8e82 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -73,7 +73,7 @@ val force_cofix : t -> t
 val mk_const : tag -> t
 val mk_block : tag -> t array -> t
 
-
+val mk_bool : bool -> t
 val mk_int : int -> t
 val mk_uint : Uint31.t -> t
 
@@ -112,5 +112,74 @@ val is_accu : t -> bool
 val str_encode : 'a -> string
 val str_decode : string -> 'a
 
+(** Support for machine integers *)
+
+val val_to_int : t -> int
+val is_int : t -> bool
+
+(* function with check *)
+val head0 : t -> t -> t
+val tail0 : t -> t -> t
+
+val add : t -> t -> t -> t
+val sub : t -> t -> t -> t
+val mul : t -> t -> t -> t
+val div : t -> t -> t -> t
+val rem : t -> t -> t -> t
+
+val l_sr  : t -> t -> t -> t
+val l_sl  : t -> t -> t -> t
+val l_and : t -> t -> t -> t
+val l_xor : t -> t -> t -> t
+val l_or  : t -> t -> t -> t
+
+val addc      : t -> t -> t -> t
+val subc      : t -> t -> t -> t
+val addCarryC : t -> t -> t -> t
+val subCarryC : t -> t -> t -> t
+
+val mulc    : t -> t -> t -> t
+val diveucl : t -> t -> t -> t
+
+val div21     : t -> t -> t -> t -> t
+val addMulDiv : t -> t -> t -> t -> t
+
+val eq      : t -> t -> t -> t
+val lt      : t -> t -> t -> t
+val le      : t -> t -> t -> t
+val compare : t -> t -> t -> t 
+
+(* Function without check *)
+val no_check_head0 : t -> t
+val no_check_tail0 : t -> t
+
+val no_check_add : t -> t -> t
+val no_check_sub : t -> t -> t
+val no_check_mul : t -> t -> t
+val no_check_div : t -> t -> t
+val no_check_rem : t -> t -> t
+
+val no_check_l_sr  : t -> t -> t
+val no_check_l_sl  : t -> t -> t
+val no_check_l_and : t -> t -> t
+val no_check_l_xor : t -> t -> t
+val no_check_l_or  : t -> t -> t
+
+val no_check_addc      : t -> t -> t
+val no_check_subc      : t -> t -> t
+val no_check_addCarryC : t -> t -> t
+val no_check_subCarryC : t -> t -> t
+
+val no_check_mulc    : t -> t -> t
+val no_check_diveucl : t -> t -> t
+
+val no_check_div21     : t -> t -> t -> t
+val no_check_addMulDiv : t -> t -> t -> t
+
+val no_check_eq      : t -> t -> t
+val no_check_lt      : t -> t -> t
+val no_check_le      : t -> t -> t
+val no_check_compare : t -> t -> t 
+
 val mk_I31_accu : t
 val decomp_uint : t -> t -> t
diff --git a/kernel/primitives.ml b/kernel/primitives.ml
new file mode 100644
index 000000000..64c486220
--- /dev/null
+++ b/kernel/primitives.ml
@@ -0,0 +1,91 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type t =
+  | Int31head0
+  | Int31tail0
+  | Int31add
+  | Int31sub
+  | Int31mul
+  | Int31div
+  | Int31mod
+(*
+  | Int31lsr
+  | Int31lsl
+ *)
+  | Int31land
+  | Int31lor
+  | Int31lxor
+  | Int31addc
+  | Int31subc
+  | Int31addcarryc
+  | Int31subcarryc
+  | Int31mulc
+  | Int31diveucl
+  | Int31div21
+  | Int31addmuldiv
+  | Int31eq
+  | Int31lt
+  | Int31le
+  | Int31compare
+
+let hash = function
+  | Int31head0 -> 1
+  | Int31tail0 -> 2
+  | Int31add -> 3
+  | Int31sub -> 4
+  | Int31mul -> 5
+  | Int31div -> 6
+  | Int31mod -> 7
+(*
+  | Int31lsr -> 8
+  | Int31lsl -> 9
+ *)
+  | Int31land -> 10
+  | Int31lor -> 11
+  | Int31lxor -> 12
+  | Int31addc -> 13
+  | Int31subc -> 14
+  | Int31addcarryc -> 15
+  | Int31subcarryc -> 16
+  | Int31mulc -> 17
+  | Int31diveucl -> 18
+  | Int31div21 -> 19
+  | Int31addmuldiv -> 20
+  | Int31eq -> 21
+  | Int31lt -> 22
+  | Int31le -> 23
+  | Int31compare -> 24
+
+let to_string = function
+  | Int31head0 -> "head0"
+  | Int31tail0 -> "tail0"
+  | Int31add -> "add"
+  | Int31sub -> "sub"
+  | Int31mul -> "mul"
+  | Int31div -> "div"
+  | Int31mod -> "mod"
+(*
+  | Int31lsr -> "l_sr"
+  | Int31lsl -> "l_sl"
+ *)
+  | Int31land -> "l_and"
+  | Int31lor -> "l_or"
+  | Int31lxor -> "l_xor"
+  | Int31addc -> "addc"
+  | Int31subc -> "subc"
+  | Int31addcarryc -> "addcarryc"
+  | Int31subcarryc -> "subcarryc"
+  | Int31mulc -> "mulc"
+  | Int31diveucl -> "diveucl"
+  | Int31div21 -> "div21"
+  | Int31addmuldiv -> "addmuldiv"
+  | Int31eq -> "eq"
+  | Int31lt -> "lt"
+  | Int31le -> "le"
+  | Int31compare -> "compare"
diff --git a/kernel/primitives.mli b/kernel/primitives.mli
new file mode 100644
index 000000000..1b70a9be8
--- /dev/null
+++ b/kernel/primitives.mli
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type t =
+  | Int31head0
+  | Int31tail0
+  | Int31add
+  | Int31sub
+  | Int31mul
+  | Int31div
+  | Int31mod
+(*
+  | Int31lsr
+  | Int31lsl
+ *)
+  | Int31land
+  | Int31lor
+  | Int31lxor
+  | Int31addc
+  | Int31subc
+  | Int31addcarryc
+  | Int31subcarryc
+  | Int31mulc
+  | Int31diveucl
+  | Int31div21
+  | Int31addmuldiv
+  | Int31eq
+  | Int31lt
+  | Int31le
+  | Int31compare
+
+val hash : t -> int
+
+val to_string : t -> string
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index f4b57d085..466380f2d 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -130,9 +130,8 @@ type reactive_end = {(*information required by the compiler of the VM *)
   vm_decompile_const : (int -> Term.constr) option;
 
   native_compiling :
-      (bool->Cbytecodes.comp_env->constr array ->
-       int->Cbytecodes.bytecodes->Cbytecodes.bytecodes)
-      option;
+      (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array ->
+       Nativeinstr.lambda) option;
 
   native_constant_static :
       (bool -> constr array -> Nativeinstr.lambda) option;
@@ -142,9 +141,8 @@ type reactive_end = {(*information required by the compiler of the VM *)
        Nativeinstr.lambda array -> Nativeinstr.lambda) option;
 
   native_before_match : (bool -> Nativeinstr.prefix -> constructor ->
-			 Nativeinstr.lambda -> Nativeinstr.lambda) option;
+			 Nativeinstr.lambda -> Nativeinstr.lambda) option
 
-  native_decompile_const : (int -> Term.constr) option
 }
 
 
@@ -186,7 +184,6 @@ let empty_reactive_end =
     native_constant_static = None;
     native_constant_dynamic = None;
     native_before_match = None;
-    native_decompile_const = None
   }
 
 
@@ -270,12 +267,6 @@ let get_native_before_match_info knowledge key =
     | None -> raise Not_found
     | Some f -> f knowledge.flags.fastcomputation
 
-let get_native_decompile_constant_info knowledge key =
-  match (Reactive.find key knowledge.reactive).native_decompile_const
-  with
-    | None -> raise Not_found
-    | Some f -> f
-
 (* functions manipulating reactive knowledge *)
 let add_vm_compiling_info knowledge value nfo =
   {knowledge with reactive =
@@ -376,16 +367,5 @@ let add_native_before_match_info knowledge value nfo =
        knowledge.reactive
   }
 
-let add_native_decompile_constant_info knowledge value nfo =
-  {knowledge with reactive =
-   try
-     Reactive.add value
-       {(Reactive.find value (knowledge.reactive)) with native_decompile_const = Some nfo}
-       knowledge.reactive
-   with Not_found ->
-     Reactive.add value {empty_reactive_end with native_decompile_const = Some nfo}
-       knowledge.reactive
-  }
-
 let clear_info knowledge value =
   {knowledge with reactive = Reactive.remove value knowledge.reactive}
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 644fb7074..30d824a9b 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -118,9 +118,8 @@ val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes
 val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr
 
 
-val get_native_compiling_info  : retroknowledge -> entry -> Cbytecodes.comp_env ->
-                             constr array ->
-                             int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes
+val get_native_compiling_info  : retroknowledge -> entry -> Nativeinstr.prefix ->
+				 Nativeinstr.lambda array -> Nativeinstr.lambda
 
 val get_native_constant_static_info : retroknowledge -> entry ->
                                       constr array -> Nativeinstr.lambda
@@ -134,8 +133,6 @@ val get_native_before_match_info : retroknowledge -> entry ->
 				   Nativeinstr.prefix -> constructor ->
 				   Nativeinstr.lambda -> Nativeinstr.lambda
 
-val get_native_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr
-
 (** the following functions are solely used in Pre_env and Environ to implement
    the functions  register and unregister (and mem) of Environ *)
 val add_field : retroknowledge -> field -> entry -> retroknowledge
@@ -167,9 +164,9 @@ val add_vm_decompile_constant_info : retroknowledge -> entry ->
                                     (int -> constr) -> retroknowledge
 
 val add_native_compiling_info : retroknowledge-> entry ->
-                            (bool -> Cbytecodes.comp_env -> constr array -> int ->
-                            Cbytecodes.bytecodes -> Cbytecodes.bytecodes) ->
-                            retroknowledge
+				(bool -> Nativeinstr.prefix ->
+			         Nativeinstr.lambda array -> Nativeinstr.lambda) ->
+				retroknowledge
 
 val add_native_constant_static_info : retroknowledge -> entry ->
                                   (bool -> constr array ->
@@ -187,9 +184,6 @@ val add_native_before_match_info : retroknowledge -> entry ->
 				      Nativeinstr.lambda -> Nativeinstr.lambda) ->
 				   retroknowledge
 
-val add_native_decompile_constant_info : retroknowledge -> entry ->
-                                    (int -> constr) -> retroknowledge
-
 val clear_info : retroknowledge-> entry -> retroknowledge