diff options
| author | Maxime Dénès | 2019-11-01 15:53:30 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-11-01 15:53:30 +0100 |
| commit | fdabd4dbd6bfd60ad46fc8c945ed063860498e53 (patch) | |
| tree | 01edf91f8b536ad4acfbba39e114daa06b40f3f8 /dev | |
| parent | d00c0b93ec4cb5ca48a9dc2ddf2cfd2038208ee2 (diff) | |
| parent | acdaab2a8c2ccb63df364bb75de8a515b2cef484 (diff) | |
Merge PR #9867: Add primitive floats (binary64 floating-point numbers)
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/09867-primitive-floats.sh | 12 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 | ||||
| -rw-r--r-- | dev/vm_printers.ml | 1 |
3 files changed, 17 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/09867-primitive-floats.sh b/dev/ci/user-overlays/09867-primitive-floats.sh new file mode 100644 index 0000000000..a0e9085afd --- /dev/null +++ b/dev/ci/user-overlays/09867-primitive-floats.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "9867" ] || [ "$CI_BRANCH" = "primitive-floats" ]; then + + unicoq_CI_REF=primitive-floats + unicoq_CI_GITURL=https://github.com/validsdp/unicoq + + elpi_CI_REF=primitive-floats + elpi_CI_GITURL=https://github.com/validsdp/coq-elpi + + coqhammer_CI_REF=primitive-floats + coqhammer_CI_GITURL=https://github.com/validsdp/coqhammer + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index aa28bce018..ccb8658eee 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -307,6 +307,8 @@ let constr_display csr = ^(array_display bl)^")" | Int i -> "Int("^(Uint63.to_string i)^")" + | Float f -> + "Float("^(Float64.to_string f)^")" and array_display v = "[|"^ @@ -439,6 +441,8 @@ let print_pure_constr csr = in print_string"{"; print_fix (); print_string"}" | Int i -> print_string ("Int("^(Uint63.to_string i)^")") + | Float f -> + print_string ("Float("^(Float64.to_string f)^")") and box_display c = open_hovbox 1; term_display c; close_box() 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 |