Add primitive floats to 'vm_compute'

* This commit add float instructions to the VM, their encoding in bytecode
  and the interpretation of primitive float values after the reduction.

* The flag '-std=c99' could be added to the C compiler flags to ensure
  that float computation strictly follows the norm (ie. i387 80-bits
  format is not used as an optimization).

  Actually, we use '-fexcess-precision=standard' instead of '-std=c99'
  because the latter would disable GNU asm used in the VM.

1 files changed, 8 insertions, 0 deletions

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index fe3c76c960..5acdd964b1 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -76,6 +76,8 @@ let rec eq_structured_values v1 v2 =
        Int.equal (Obj.size o1) (Obj.size o2)
     then if Int.equal t1 Obj.custom_tag
       then Int64.equal (Obj.magic v1 : int64) (Obj.magic v2 : int64)
+    else if Int.equal t1 Obj.double_tag
+      then Float64.(equal (of_float (Obj.magic v1)) (of_float (Obj.magic v2)))
     else begin
       assert (t1 <= Obj.last_non_constant_constructor_tag &&
               t2 <= Obj.last_non_constant_constructor_tag);
@@ -289,6 +291,7 @@ type whd =
   | Vconstr_const of int
   | Vconstr_block of vblock
   | Vint64 of int64
+  | Vfloat64 of float
   | Vatom_stk of atom * stack
   | Vuniv_level of Univ.Level.t
 
@@ -320,6 +323,7 @@ let uni_lvl_val (v : values) : Univ.Level.t =
         | Vconstr_const _i -> str "Vconstr_const"
         | Vconstr_block _b -> str "Vconstr_block"
         | Vint64 _ -> str "Vint64"
+        | Vfloat64 _ -> str "Vfloat64"
         | Vatom_stk (_a,_stk) -> str "Vatom_stk"
         | Vuniv_level _ -> assert false
       in
@@ -379,6 +383,8 @@ let rec whd_accu a stk =
       end
   | i when Int.equal i Obj.custom_tag ->
     Vint64 (Obj.magic i)
+  | i when Int.equal i Obj.double_tag ->
+    Vfloat64 (Obj.magic i)
   | tg ->
     CErrors.anomaly
       Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".")
@@ -408,6 +414,7 @@ let whd_val : values -> whd =
            | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
            | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work."))
         else 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
            Vconstr_block(Obj.obj o)
 
@@ -681,6 +688,7 @@ and pr_whd w =
   | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")"
   | Vconstr_block _b -> str "Vconstr_block"
   | Vint64 i -> i |> Format.sprintf "Vint64(%LiL)" |> str
+  | Vfloat64 f -> str "Vfloat64(" ++ str (Float64.(to_string (of_float f))) ++ str ")"
   | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")"
   | Vuniv_level _ -> assert false)
 and pr_stack stk =