aboutsummaryrefslogtreecommitdiff
path: root/dev/vm_printers.ml
diff options
context:
space:
mode:
authorGuillaume Bertholon2018-07-19 13:33:17 +0200
committerPierre Roux2019-11-01 10:20:19 +0100
commitcc7dfa82705b64d1cf43408244ef6c7dd930a6e9 (patch)
tree27ed520687e72b029a083ce5bafb15e15b7187f4 /dev/vm_printers.ml
parent1b0bd3a9e3a913a4928b68546a134a1a4448f9e8 (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 'dev/vm_printers.ml')
-rw-r--r--dev/vm_printers.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 863d930968..11565b99eb 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -84,6 +84,7 @@ and ppwhd whd =
| Vconstr_const i -> print_string "C(";print_int i;print_string")"
| Vconstr_block b -> ppvblock b
| Vint64 i -> printf "int64(%LiL)" i
+ | Vfloat64 f -> printf "float64(%.17g)" f
| Vatom_stk(a,s) ->
open_hbox();ppatom a;close_box();
print_string"@";ppstack s