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, 2 insertions, 1 deletions

diff --git a/kernel/vm.ml b/kernel/vm.ml
index 319a26d824..5f08720f77 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -169,7 +169,8 @@ let rec apply_stack a stk v =
 let apply_whd k whd =
   let v = val_of_rel k in
   match whd with
-  | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ -> assert false
+  | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ | Vfloat64 _ ->
+     assert false
   | Vfun f -> reduce_fun k f
   | Vfix(f, None) -> 
       push_ra stop;