From b0b3cc67e01b165272588b2d8bc178840ba83945 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Fri, 13 Jul 2018 16:22:35 +0200
Subject: Add primitive float computation in Coq kernel

Beware of 0. = -0. issue for primitive floats

The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
---
 dev/top_printers.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'dev')

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()
 
-- 
cgit v1.2.3


From cc7dfa82705b64d1cf43408244ef6c7dd930a6e9 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Thu, 19 Jul 2018 13:33:17 +0200
Subject: 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.
---
 dev/vm_printers.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

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
-- 
cgit v1.2.3


From 40df8d4c451a09e82a5da29a2c3309dedebc64de Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 10 May 2019 16:05:12 +0200
Subject: Add overlays

---
 dev/ci/user-overlays/09867-primitive-floats.sh | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 dev/ci/user-overlays/09867-primitive-floats.sh

(limited to 'dev')

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
-- 
cgit v1.2.3