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.

1 files changed, 65 insertions, 25 deletions

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 "(==)"