Add primitive floats to 'native_compute'

* Float added to is_value/get_value to avoid stack overflows
  (cf. #7646)

* beware of the use of Array.map with floats (cf. comment in the
  makeblock function)

NB: From here one, the configure option "-native-compiler no"
is no longer needed.

8 files changed, 374 insertions, 36 deletions

diff --git a/kernel/float64.ml b/kernel/float64.ml
index 351661f44d..c0611f37a0 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -13,12 +13,21 @@
 type t = float
 
 let is_nan f = f <> f
+let is_infinity f = f = infinity
+let is_neg_infinity f = f = neg_infinity
 
 (* OCaml give a sign to nan values which should not be displayed as all nan are
  * considered equal *)
 let to_string f = if is_nan f then "nan" else string_of_float f
 let of_string = float_of_string
 
+(* Compiles a float to OCaml code *)
+let compile f =
+  let s =
+    if is_nan f then "nan" else if is_neg_infinity f then "neg_infinity"
+    else Printf.sprintf "%h" f in
+  Printf.sprintf "Float64.of_float (%s)" s
+
 let of_float f = f
 
 let opp = ( ~-. )
@@ -37,6 +46,7 @@ let compare x y =
       else FNotComparable (* NaN case *)
     )
   )
+[@@ocaml.inline always]
 
 type float_class =
   | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN
@@ -48,19 +58,32 @@ let classify x =
   | FP_zero -> if 0. < 1. /. x then PZero else NZero
   | FP_infinite -> if 0. < x then PInf else NInf
   | FP_nan -> NaN
+[@@ocaml.inline always]
+
+let mul x y = x *. y
+[@@ocaml.inline always]
+
+let add x y = x +. y
+[@@ocaml.inline always]
+
+let sub x y = x -. y
+[@@ocaml.inline always]
+
+let div x y = x /. y
+[@@ocaml.inline always]
+
+let sqrt x = sqrt x
+[@@ocaml.inline always]
 
-let mul = ( *. )
-let add = ( +. )
-let sub = ( -. )
-let div = ( /. )
-let sqrt = sqrt
+let of_int63 x = Uint63.to_float x
+[@@ocaml.inline always]
 
-let of_int63 = Uint63.to_float
 let prec = 53
 let normfr_mantissa f =
   let f = abs f in
   if f >= 0.5 && f < 1. then Uint63.of_float (ldexp f prec)
   else Uint63.zero
+[@@ocaml.inline always]
 
 let eshift = 2101 (* 2*emax + prec *)
 
@@ -73,8 +96,10 @@ let frshiftexp f =
   | FP_normal | FP_subnormal ->
     let (m, e) = frexp f in
     m, Uint63.of_int (e + eshift)
+[@@ocaml.inline always]
 
 let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift)
+[@@ocaml.inline always]
 
 let eta_float = ldexp 1. (-1074) (* smallest positive float (subnormal) *)
 
@@ -91,14 +116,17 @@ let next_up f =
        ldexp (f +. epsilon_float /. 2.) e
      else
        ldexp (-0.5 +. epsilon_float /. 4.) e
+[@@ocaml.inline always]
 
 let next_down f = -.(next_up (-.f))
+[@@ocaml.inline always]
 
 let equal f1 f2 =
   match classify_float f1 with
   | FP_normal | FP_subnormal | FP_infinite -> (f1 = f2)
   | FP_nan -> is_nan f2
   | FP_zero -> f1 = f2 && 1. /. f1 = 1. /. f2 (* OCaml consider 0. = -0. *)
+[@@ocaml.inline always]
 
 let hash =
   (* Hashtbl.hash already considers all NaNs as equal,
diff --git a/kernel/float64.mli b/kernel/float64.mli
index 580004126d..1e6ea8bb96 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -15,10 +15,14 @@ indistinguishable from Coq's perspective. *)
 type t
 
 val is_nan : t -> bool
+val is_infinity : t -> bool
+val is_neg_infinity : t -> bool
 
 val to_string : t -> string
 val of_string : string -> t
 
+val compile : t -> string
+
 val of_float : float -> t
 
 val opp : t -> t
@@ -29,32 +33,55 @@ type float_comparison = FEq | FLt | FGt | FNotComparable
 (** The IEEE 754 float comparison.
  * NotComparable is returned if there is a NaN in the arguments *)
 val compare : t -> t -> float_comparison
+[@@ocaml.inline always]
 
 type float_class =
   | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN
 
 val classify : t -> float_class
+[@@ocaml.inline always]
 
 val mul : t -> t -> t
+[@@ocaml.inline always]
+
 val add : t -> t -> t
+[@@ocaml.inline always]
+
 val sub : t -> t -> t
+[@@ocaml.inline always]
+
 val div : t -> t -> t
+[@@ocaml.inline always]
+
 val sqrt : t -> t
+[@@ocaml.inline always]
 
 (** Link with integers *)
 val of_int63 : Uint63.t -> t
+[@@ocaml.inline always]
+
 val normfr_mantissa : t -> Uint63.t
+[@@ocaml.inline always]
 
 (** Shifted exponent extraction *)
+val eshift : int
+
 val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *)
+[@@ocaml.inline always]
+
 val ldshiftexp : t -> Uint63.t -> t
+[@@ocaml.inline always]
 
 val next_up : t -> t
+[@@ocaml.inline always]
+
 val next_down : t -> t
+[@@ocaml.inline always]
 
 (** Return true if two floats are equal.
  * All NaN values are considered equal. *)
 val equal : t -> t -> bool
+[@@ocaml.inline always]
 
 val hash : t -> int
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 1a5455cf3a..63dc49ba57 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -258,16 +258,19 @@ type primitive =
   | Mk_var of Id.t
   | Mk_proj
   | Is_int
+  | Is_float
   | Cast_accu
   | Upd_cofix
   | Force_cofix
   | Mk_uint
+  | Mk_float
   | Mk_int
   | Mk_bool
   | Val_to_int
   | Mk_meta
   | Mk_evar
   | MLand
+  | MLnot
   | MLle
   | MLlt
   | MLinteq
@@ -349,6 +352,9 @@ let primitive_hash = function
   | Mk_proj -> 36
   | MLarrayget -> 37
   | Mk_empty_instance -> 38
+  | Mk_float -> 39
+  | Is_float -> 40
+  | MLnot -> 41
 
 type mllambda =
   | MLlocal        of lname 
@@ -365,6 +371,7 @@ type mllambda =
                    (* prefix, inductive name, tag, arguments *)
   | MLint          of int
   | MLuint         of Uint63.t
+  | MLfloat        of Float64.t
   | MLsetref       of string * mllambda
   | MLsequence     of mllambda * mllambda
   | MLarray        of mllambda array
@@ -436,6 +443,8 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
       Int.equal i1 i2
   | MLuint i1, MLuint i2 ->
       Uint63.equal i1 i2
+  | MLfloat f1, MLfloat f2 ->
+      Float64.equal f1 f2
   | MLsetref (id1, ml1), MLsetref (id2, ml2) ->
       String.equal id1 id2 &&
       eq_mllambda gn1 gn2 n env1 env2 ml1 ml2
@@ -450,7 +459,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
     eq_mllambda gn1 gn2 n env1 env2 ml1 ml2
   | (MLlocal _ | MLglobal _ | MLprimitive _ | MLlam _ | MLletrec _ | MLlet _ |
     MLapp _ | MLif _ | MLmatch _ | MLconstruct _ | MLint _ | MLuint _ |
-    MLsetref _ | MLsequence _ | MLarray _ | MLisaccu _), _ -> false
+    MLfloat _ | MLsetref _ | MLsequence _ | MLarray _ | MLisaccu _), _ -> false
 
 and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 =
   let eq_def (_,args1,ml1) (_,args2,ml2) =
@@ -535,6 +544,8 @@ let rec hash_mllambda gn n env t =
       combinesmall 15 (hash_mllambda_array gn n env 1 arr)
   | MLisaccu (s, ind, c) ->
       combinesmall 16 (combine (String.hash s) (combine (ind_hash ind) (hash_mllambda gn n env c)))
+  | MLfloat f ->
+      combinesmall 17 (Float64.hash f)
 
 and hash_mllambda_letrec gn n env init defs =
   let hash_def (_,args,ml) =
@@ -568,7 +579,7 @@ let fv_lam l =
     match l with
     | MLlocal l ->
 	if LNset.mem l bind then fv else LNset.add l fv
-    | MLglobal _ | MLprimitive _  | MLint _ | MLuint _ -> fv
+    | MLglobal _ | MLprimitive _  | MLint _ | MLuint _ | MLfloat _ -> fv
     | MLlam (ln,body) ->
 	let bind = Array.fold_right LNset.add ln bind in
 	aux body bind fv
@@ -757,7 +768,7 @@ type env =
       env_named : (Id.t * mllambda) list ref;
       env_univ : lname option}
 
-let empty_env univ () =
+let empty_env univ =
   { env_rel = [];
     env_bound = 0;
     env_urel = ref [];
@@ -958,25 +969,29 @@ type prim_aux =
   | PAprim of string * pconstant * CPrimitives.t * prim_aux array
   | PAml of mllambda
 
-let add_check cond args =
-  let aux cond a = 
+let add_check cond targs args =
+  let aux cond t a =
     match a with
     | PAml(MLint _) -> cond
     | PAml ml ->
        (* FIXME: use explicit equality function *)
-       if List.mem ml cond then cond else ml::cond 
+       if List.mem (t, ml) cond then cond else (t, ml)::cond
     | _ -> cond
   in
-  Array.fold_left aux cond args
+  Array.fold_left2 aux cond targs args
 
 let extract_prim ml_of l =
   let decl = ref [] in
   let cond = ref [] in
+  let type_args p =
+    let rec aux = function [] | [_] -> [] | h :: t -> h :: aux t in
+    Array.of_list (aux (CPrimitives.types p)) in
   let rec aux l =
     match l with
     | Lprim(prefix,kn,p,args) ->
+      let targs = type_args p in
       let args = Array.map aux args in
-      cond := add_check !cond args;
+      cond := add_check !cond targs args;
       PAprim(prefix,kn,p,args)
     | Lrel _ | Lvar _ | Luint _ | Lval _ | Lconst _ -> PAml (ml_of l)
     | _ ->
@@ -1010,15 +1025,35 @@ let compile_prim decl cond paux =
   let compile_cond cond paux =
     match cond with
     | [] -> opt_prim_aux paux
-    | [c1] ->
+    | [CPrimitives.(PITT_type PT_int63), 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; cast_to_int c|])
-          (app_prim MLland [| cast_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 ci, cf =
+        let is_int =
+          function CPrimitives.(PITT_type PT_int63), _ -> true | _ -> false in
+        List.partition is_int cond in
+      let condi =
+        let cond =
+          List.fold_left
+            (fun ml (_, c) -> app_prim MLland [| ml; cast_to_int c|])
+            (MLint 0) ci in
+        app_prim MLmagic [|cond|] in
+      let condf = match cf with
+        | [] -> MLint 0
+        | [_, c1] -> app_prim Is_float [|c1|]
+        | (_, c1) :: condf ->
+           List.fold_left
+             (fun ml (_, c) -> app_prim MLand [| ml; app_prim Is_float [|c|]|])
+             (app_prim Is_float [|c1|]) condf in
+      match ci, cf with
+      | [], [] -> opt_prim_aux paux
+      | _ :: _, [] ->
+         MLif(condi, naive_prim_aux paux, opt_prim_aux paux)
+      | [], _ :: _ ->
+         MLif(condf, opt_prim_aux paux, naive_prim_aux paux)
+      | _ :: _, _ :: _ ->
+         let cond = app_prim MLand [|condf; app_prim MLnot [|condi|]|] in
+         MLif(cond, opt_prim_aux paux, naive_prim_aux paux) in
 
   let add_decl decl body =
     List.fold_left (fun body (x,d) -> MLlet(x,d,body)) body decl in
@@ -1095,14 +1130,14 @@ let ml_of_instance instance u =
          (* Remark: if we do not want to compile the predicate we 
             should a least compute the fv, then store the lambda representation
             of the predicate (not the mllambda) *)
-      let env_p = empty_env env.env_univ () in
+      let env_p = empty_env env.env_univ in
       let pn = fresh_gpred l in
       let mlp = ml_of_lam env_p l p in
       let mlp = generalize_fv env_p mlp in
       let (pfvn,pfvr) = !(env_p.env_named), !(env_p.env_urel) in
       let pn = push_global_let pn mlp in
       (* Compilation of the case *)
-      let env_c = empty_env env.env_univ () in
+      let env_c = empty_env env.env_univ in
       let a_uid = fresh_lname Anonymous in
       let la_uid = MLlocal a_uid in
       (* compilation of branches *)
@@ -1158,7 +1193,7 @@ let ml_of_instance instance u =
 	   start
       *)
       (* Compilation of type *)
-      let env_t = empty_env env.env_univ () in
+      let env_t = empty_env env.env_univ in
       let ml_t = Array.map (ml_of_lam env_t l) tt in
       let params_t = fv_params env_t in
       let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in
@@ -1167,7 +1202,7 @@ let ml_of_instance instance u =
       let mk_type = MLapp(MLglobal gft, args_t) in
       (* Compilation of norm_i *)
       let ndef = Array.length ids in
-      let lf,env_n = push_rels (empty_env env.env_univ ()) ids in
+      let lf,env_n = push_rels (empty_env env.env_univ) ids in
       let t_params = Array.make ndef [||] in
       let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
       let mk_let _envi (id,def) t = MLlet (id,def,t) in
@@ -1224,7 +1259,7 @@ let ml_of_instance instance u =
       MLletrec(Array.mapi mkrec lf, lf_args.(start))
   | Lcofix (start, (ids, tt, tb)) -> 
       (* Compilation of type *)
-      let env_t = empty_env env.env_univ () in
+      let env_t = empty_env env.env_univ in
       let ml_t = Array.map (ml_of_lam env_t l) tt in
       let params_t = fv_params env_t in
       let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in
@@ -1233,7 +1268,7 @@ let ml_of_instance instance u =
       let mk_type = MLapp(MLglobal gft, args_t) in
       (* Compilation of norm_i *) 
       let ndef = Array.length ids in
-      let lf,env_n = push_rels (empty_env env.env_univ ()) ids in
+      let lf,env_n = push_rels (empty_env env.env_univ) ids in
       let t_params = Array.make ndef [||] in
       let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
       let ml_of_fix i body =
@@ -1297,6 +1332,7 @@ let ml_of_instance instance u =
      let args = Array.map (ml_of_lam env l) args in
      MLconstruct(prefix,cn,tag,args)
   | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
+  | Lfloat f -> MLapp(MLprimitive Mk_float, [|MLfloat f|])
   | Lval v ->
       let i = push_symbol (SymbValue v) in get_value_code i
   | Lsort s ->
@@ -1314,7 +1350,7 @@ let ml_of_instance instance u =
   | Lforce -> MLglobal (Ginternal "Lazy.force")
 
 let mllambda_of_lambda univ auxdefs l t =
-  let env = empty_env univ () in
+  let env = empty_env univ in
   global_stack := auxdefs;
   let ml = ml_of_lam env l t in
   let fv_rel = !(env.env_urel) in
@@ -1347,7 +1383,7 @@ let subst s l =
     let rec aux l =
       match l with
       | MLlocal id -> (try LNmap.find id s with Not_found -> l)
-      | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ -> l
+      | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ | MLfloat _ -> l
       | MLlam(params,body) -> MLlam(params, aux body)
       | MLletrec(defs,body) ->
 	let arec (f,params,body) = (f,params,aux body) in
@@ -1417,7 +1453,7 @@ let optimize gdef l =
   let rec optimize s l =
     match l with
     | MLlocal id -> (try LNmap.find id s with Not_found -> l)
-    | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ -> l
+    | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ | MLfloat _ -> l
     | MLlam(params,body) -> 
 	MLlam(params, optimize s body)
     | MLletrec(decls,body) ->
@@ -1623,6 +1659,7 @@ let pp_mllam fmt l =
           (string_of_construct prefix ~constant:false ind tag) pp_cargs args
     | MLint i -> pp_int fmt i
     | MLuint i -> Format.fprintf fmt "(%s)" (Uint63.compile i)
+    | MLfloat f -> Format.fprintf fmt "(%s)" (Float64.compile f)
     | MLsetref (s, body) ->
 	Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body
     | MLsequence(l1,l2) ->
@@ -1739,16 +1776,19 @@ let pp_mllam fmt l =
         Format.fprintf fmt "mk_var_accu (Names.Id.of_string \"%s\")" (string_of_id id)
     | Mk_proj -> Format.fprintf fmt "mk_proj_accu"
     | Is_int -> Format.fprintf fmt "is_int"
+    | Is_float -> Format.fprintf fmt "is_float"
     | 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_float -> Format.fprintf fmt "mk_float"
     | Mk_int -> Format.fprintf fmt "mk_int"
     | Mk_bool -> Format.fprintf fmt "mk_bool"
     | Val_to_int -> Format.fprintf fmt "val_to_int"
     | Mk_meta -> Format.fprintf fmt "mk_meta_accu"
     | Mk_evar -> Format.fprintf fmt "mk_evar_accu"
     | MLand -> Format.fprintf fmt "(&&)"
+    | MLnot -> Format.fprintf fmt "not"
     | MLle -> Format.fprintf fmt "(<=)"
     | MLlt -> Format.fprintf fmt "(<)"
     | MLinteq -> Format.fprintf fmt "(==)"
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index dd010e5cad..ef610ce7e9 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -35,6 +35,9 @@ let rec conv_val env pb lvl v1 v2 cu =
 	if Int.equal i1 i2 then cu else raise NotConvertible
     | Vint64 i1, Vint64 i2 ->
       if Int64.equal i1 i2 then cu else raise NotConvertible
+    | Vfloat64 f1, Vfloat64 f2 ->
+        if Float64.(equal (of_float f1) (of_float f2)) then cu
+        else raise NotConvertible
     | Vblock b1, Vblock b2 ->
 	let n1 = block_size b1 in
         let n2 = block_size b2 in
@@ -48,7 +51,7 @@ let rec conv_val env pb lvl v1 v2 cu =
 	    aux lvl max b1 b2 (i+1) cu
 	in
 	aux lvl (n1-1) b1 b2 0 cu
-    | Vaccu _, _ | Vconst _, _ | Vint64 _, _ | Vblock _, _ -> raise NotConvertible
+    | (Vaccu _ | Vconst _ | Vint64 _ | Vfloat64 _ | Vblock _), _ -> raise NotConvertible
 
 and conv_accu env pb lvl k1 k2 cu =
   let n1 = accu_nargs k1 in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 301773143c..7a4e62cdfe 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -44,6 +44,7 @@ type lambda =
                   (* prefix, inductive name, constructor tag, arguments *)
         (* A fully applied non-constant constructor *)
   | Luint         of Uint63.t
+  | Lfloat        of Float64.t
   | Lval          of Nativevalues.t
   | Lsort         of Sorts.t
   | Lind          of prefix * pinductive
@@ -123,7 +124,7 @@ let get_const_prefix env c =
 let map_lam_with_binders g f n lam =
   match lam with
   | Lrel _ | Lvar _  | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Luint _
-  | Llazy | Lforce | Lmeta _ | Lint _ -> lam
+  | Llazy | Lforce | Lmeta _ | Lint _ | Lfloat _ -> lam
   | Lprod(dom,codom) -> 
       let dom' = f n dom in
       let codom' = f n codom in
@@ -331,7 +332,7 @@ and reduce_lapp substf lids body substa largs =
 
 let is_value lc =
   match lc with
-  | Lval _ | Lint _ | Luint _ -> true
+  | Lval _ | Lint _ | Luint _ | Lfloat _ -> true
   | _ -> false
 
 let get_value lc =
@@ -339,6 +340,7 @@ let get_value lc =
   | Lval v -> v
   | Lint tag -> Nativevalues.mk_int tag
   | Luint i -> Nativevalues.mk_uint i
+  | Lfloat f -> Nativevalues.mk_float f
   | _ -> raise Not_found
 
 let make_args start _end =
@@ -364,7 +366,12 @@ let makeblock env ind tag nparams arity args =
   if Int.equal arity 0 then Lint tag
   else
   if Array.for_all is_value args then
-    let args = Array.map get_value args in
+    let dummy_val = Obj.magic 0 in
+    let args =
+      (* Don't simplify this to Array.map, cf. the related comment in
+         function eval_to_patch, file kernel/csymtable.ml *)
+      let a = Array.make (Array.length args) dummy_val in
+      Array.iteri (fun i v -> a.(i) <- get_value v) args; a in
     Lval (Nativevalues.mk_block tag args)
   else
     let prefix = get_mind_prefix env (fst ind) in
@@ -580,7 +587,7 @@ let rec lambda_of_constr cache env sigma c =
 
   | Int i -> Luint i
 
-  | Float _ -> assert false  (* native computed for primitive float not yet implemented *)
+  | Float f -> Lfloat f
 
 and lambda_of_app cache env sigma f args =
   match kind f with
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index f17339f84d..1d7bf5343a 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -38,6 +38,7 @@ type lambda =
                   (* prefix, inductive name, constructor tag, arguments *)
         (* A fully applied non-constant constructor *)
   | Luint         of Uint63.t
+  | Lfloat        of Float64.t
   | Lval          of Nativevalues.t
   | Lsort         of Sorts.t
   | Lind          of prefix * pinductive
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index f788832d5b..1d4fb5d39c 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -225,6 +225,9 @@ let mk_bool (b : bool) = (Obj.magic (not b) : t)
 let mk_uint (x : Uint63.t) = (Obj.magic x : t)
 [@@ocaml.inline always]
 
+let mk_float (x : Float64.t) = (Obj.magic x : t)
+[@@ocaml.inline always]
+
 type block
 
 let block_size (b:block) =
@@ -240,16 +243,19 @@ type kind_of_value =
   | Vfun of (t -> t)
   | Vconst of int
   | Vint64 of int64
+  | Vfloat64 of float
   | Vblock of block
 
 let kind_of_value (v:t) =
   let o = Obj.repr v in
   if Obj.is_int o then Vconst (Obj.magic v)
+  else if Obj.tag o == Obj.double_tag then Vfloat64 (Obj.magic v)
   else
     let tag = Obj.tag o in
     if Int.equal tag accumulate_tag then
       Vaccu (Obj.magic v)
     else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
+    else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
     else if (tag < Obj.lazy_tag) then Vblock (Obj.magic v)
       else
         (* assert (tag = Obj.closure_tag || tag = Obj.infix_tag); 
@@ -261,6 +267,7 @@ let kind_of_value (v:t) =
 let is_int (x:t) =
   let o = Obj.repr x in
   Obj.is_int o || Int.equal (Obj.tag o) Obj.custom_tag
+[@@ocaml.inline always]
 
 let val_to_int (x:t) = (Obj.magic x : int)
 [@@ocaml.inline always]
@@ -508,6 +515,158 @@ let print x =
   flush stderr;
   x
 
+(** Support for machine floating point values *)
+
+let is_float (x:t) =
+  let o = Obj.repr x in
+  Int.equal (Obj.tag o) Obj.double_tag
+[@@ocaml.inline always]
+
+let to_float (x:t) = (Obj.magic x : Float64.t)
+[@@ocaml.inline always]
+
+let no_check_fopp x =
+  mk_float (Float64.opp (to_float x))
+[@@ocaml.inline always]
+
+let fopp accu x =
+  if is_float x then no_check_fopp x
+  else accu x
+
+let no_check_fabs x =
+  mk_float (Float64.abs (to_float x))
+[@@ocaml.inline always]
+
+let fabs accu x =
+  if is_float x then no_check_fabs x
+  else accu x
+
+type coq_fcmp =
+  | CFcmpAccu of t
+  | CFcmpEq
+  | CFcmpLt
+  | CFcmpGt
+  | CFcmpNotComparable
+
+let no_check_fcompare x y =
+  let c = Float64.compare (to_float x) (to_float y) in
+  (Obj.magic c:t)
+[@@ocaml.inline always]
+
+let fcompare accu x y =
+  if is_float x && is_float y then no_check_fcompare x y
+  else accu x y
+
+type coq_fclass =
+  | CFclassAccu of t
+  | CFclassPNormal
+  | CFclassNNormal
+  | CFclassPSubn
+  | CFclassNSubn
+  | CFclassPZero
+  | CFclassNZero
+  | CFclassPInf
+  | CFclassNInf
+  | CFclassNaN
+
+let no_check_fclassify x =
+  let c = Float64.classify (to_float x) in
+  (Obj.magic c:t)
+[@@ocaml.inline always]
+
+let fclassify accu x =
+  if is_float x then no_check_fclassify x
+  else accu x
+
+let no_check_fadd x y =
+  mk_float (Float64.add (to_float x) (to_float y))
+[@@ocaml.inline always]
+
+let fadd accu x y =
+  if is_float x && is_float y then no_check_fadd x y
+  else accu x y
+
+let no_check_fsub x y =
+  mk_float (Float64.sub (to_float x) (to_float y))
+[@@ocaml.inline always]
+
+let fsub accu x y =
+  if is_float x && is_float y then no_check_fsub x y
+  else accu x y
+
+let no_check_fmul x y =
+  mk_float (Float64.mul (to_float x) (to_float y))
+[@@ocaml.inline always]
+
+let fmul accu x y =
+  if is_float x && is_float y then no_check_fmul x y
+  else accu x y
+
+let no_check_fdiv x y =
+  mk_float (Float64.div (to_float x) (to_float y))
+[@@ocaml.inline always]
+
+let fdiv accu x y =
+  if is_float x && is_float y then no_check_fdiv x y
+  else accu x y
+
+let no_check_fsqrt x =
+  mk_float (Float64.sqrt (to_float x))
+[@@ocaml.inline always]
+
+let fsqrt accu x =
+  if is_float x then no_check_fsqrt x
+  else accu x
+
+let no_check_float_of_int x =
+  mk_float (Float64.of_int63 (to_uint x))
+[@@ocaml.inline always]
+
+let float_of_int accu x =
+  if is_int x then no_check_float_of_int x
+  else accu x
+
+let no_check_normfr_mantissa x =
+  mk_uint (Float64.normfr_mantissa (to_float x))
+[@@ocaml.inline always]
+
+let normfr_mantissa accu x =
+  if is_float x then no_check_normfr_mantissa x
+  else accu x
+
+let no_check_frshiftexp x =
+  let f, e = Float64.frshiftexp (to_float x) in
+  (Obj.magic (PPair(mk_float f, mk_uint e)):t)
+[@@ocaml.inline always]
+
+let frshiftexp accu x =
+  if is_float x then no_check_frshiftexp x
+  else accu x
+
+let no_check_ldshiftexp x e =
+  mk_float (Float64.ldshiftexp (to_float x) (to_uint e))
+[@@ocaml.inline always]
+
+let ldshiftexp accu x e =
+  if is_float x && is_int e then no_check_ldshiftexp x e
+  else accu x e
+
+let no_check_next_up x =
+  mk_float (Float64.next_up (to_float x))
+[@@ocaml.inline always]
+
+let next_up accu x =
+  if is_float x then no_check_next_up x
+  else accu x
+
+let no_check_next_down x =
+  mk_float (Float64.next_down (to_float x))
+[@@ocaml.inline always]
+
+let next_down accu x =
+  if is_float x then no_check_next_down x
+  else accu x
+
 let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%02x" i)
 let bohcnv = Array.init 256 (fun i -> i -
                                       (if 0x30 <= i then 0x30 else 0) -
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index b54f437e73..d19877c121 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -102,6 +102,9 @@ val mk_int : int -> t
 val mk_uint : Uint63.t -> t
 [@@ocaml.inline always]
 
+val mk_float : Float64.t -> t
+[@@ocaml.inline always]
+
 val napply : t -> t array -> t
 (* Functions over accumulators *)
 
@@ -130,6 +133,7 @@ type kind_of_value =
   | Vfun of (t -> t)
   | Vconst of int
   | Vint64 of int64
+  | Vfloat64 of float
   | Vblock of block
 
 val kind_of_value : t -> kind_of_value
@@ -140,7 +144,9 @@ val str_decode : string -> 'a
 (** Support for machine integers *)
 
 val val_to_int : t -> int
+
 val is_int : t -> bool
+[@@ocaml.inline always]
 
 (* function with check *)
 val head0 : t -> t -> t
@@ -247,3 +253,70 @@ val no_check_le      : t -> t -> t
 [@@ocaml.inline always]
 
 val no_check_compare : t -> t -> t
+
+(** Support for machine floating point values *)
+
+val is_float : t -> bool
+[@@ocaml.inline always]
+
+val fopp : t -> t -> t
+val fabs : t -> t -> t
+val fcompare : t -> t -> t -> t
+val fclassify : t -> t -> t
+val fadd : t -> t -> t -> t
+val fsub : t -> t -> t -> t
+val fmul : t -> t -> t -> t
+val fdiv : t -> t -> t -> t
+val fsqrt : t -> t -> t
+val float_of_int : t -> t -> t
+val normfr_mantissa : t -> t -> t
+val frshiftexp : t -> t -> t
+val ldshiftexp : t -> t -> t -> t
+val next_up : t -> t -> t
+val next_down : t -> t -> t
+
+(* Function without check *)
+val no_check_fopp : t -> t
+[@@ocaml.inline always]
+
+val no_check_fabs : t -> t
+[@@ocaml.inline always]
+
+val no_check_fcompare : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fclassify : t -> t
+[@@ocaml.inline always]
+
+val no_check_fadd : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fsub : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fmul : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fdiv : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_fsqrt : t -> t
+[@@ocaml.inline always]
+
+val no_check_float_of_int : t -> t
+[@@ocaml.inline always]
+
+val no_check_normfr_mantissa : t -> t
+[@@ocaml.inline always]
+
+val no_check_frshiftexp : t -> t
+[@@ocaml.inline always]
+
+val no_check_ldshiftexp : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_next_up : t -> t
+[@@ocaml.inline always]
+
+val no_check_next_down : t -> t
+[@@ocaml.inline always]