diff options
| author | Guillaume Bertholon | 2018-07-19 13:33:17 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:19 +0100 |
| commit | cc7dfa82705b64d1cf43408244ef6c7dd930a6e9 (patch) | |
| tree | 27ed520687e72b029a083ce5bafb15e15b7187f4 /kernel/vconv.ml | |
| parent | 1b0bd3a9e3a913a4928b68546a134a1a4448f9e8 (diff) | |
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.
Diffstat (limited to 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 414c443c4e..5d36ad54a2 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -73,6 +73,9 @@ and conv_whd env pb k whd1 whd2 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 | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom env pb k a1 stk1 a2 stk2 cu | Vfun _, _ | _, Vfun _ -> @@ -80,7 +83,7 @@ and conv_whd env pb k whd1 whd2 cu = conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ | Vint64 _, _ - | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible + | Vfloat64 _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible and conv_atom env pb k a1 stk1 a2 stk2 cu = |