From f93684a412f067622a5026c406bc76032c30b6e9 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 2 Apr 2019 22:39:32 +0200
Subject: Declare type of primitives in CPrimitives

Rather than in typeops
---
 kernel/cPrimitives.ml | 72 +++++++++++++++++++++++++++------------------------
 1 file changed, 38 insertions(+), 34 deletions(-)

(limited to 'kernel/cPrimitives.ml')

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index d854cadd15..d433cdc1ba 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -90,58 +90,62 @@ let to_string = function
   | Int63le -> "le"
   | Int63compare -> "compare"
 
-type arg_kind =
-  | Kparam (* not needed for the evaluation of the primitive when it reduces *)
-  | Kwhnf  (* need to be reduced in whnf before reducing the primitive *)
-  | Karg   (* no need to be reduced in whnf. example: [v] in [Array.set t i v] *)
+type prim_type =
+  | PT_int63
 
-type args_red = arg_kind list
+type 'a prim_ind =
+  | PIT_bool : unit prim_ind
+  | PIT_carry : prim_type prim_ind
+  | PIT_pair : (prim_type * prim_type) prim_ind
+  | PIT_cmp : unit prim_ind
 
-(* Invariant only argument of type int63 or an inductive can
-   have kind Kwhnf *)
+type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
 
-let kind = function
-  | Int63head0 | Int63tail0 -> [Kwhnf]
+type ind_or_type =
+  | PITT_ind : 'a prim_ind * 'a -> ind_or_type
+  | PITT_type : prim_type -> ind_or_type
 
+let types =
+  let int_ty = PITT_type PT_int63 in
+  function
+  | Int63head0 | Int63tail0 -> [int_ty; int_ty]
   | Int63add | Int63sub | Int63mul
   | Int63div | Int63mod
   | Int63lsr | Int63lsl
-  | Int63land | Int63lor | Int63lxor
-  | Int63addc | Int63subc
-  | Int63addCarryC | Int63subCarryC  | Int63mulc | Int63diveucl
-  | Int63eq | Int63lt | Int63le | Int63compare -> [Kwhnf; Kwhnf]
+  | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty]
+  | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC ->
+     [int_ty; int_ty; PITT_ind (PIT_carry, PT_int63)]
+  | Int63mulc | Int63diveucl ->
+     [int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))]
+  | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())]
+  | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())]
+  | Int63div21 ->
+     [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))]
+  | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty]
 
-  | Int63div21 | Int63addMulDiv -> [Kwhnf; Kwhnf; Kwhnf]
+type arg_kind =
+  | Kparam (* not needed for the evaluation of the primitive when it reduces *)
+  | Kwhnf  (* need to be reduced in whnf before reducing the primitive *)
+  | Karg   (* no need to be reduced in whnf. example: [v] in [Array.set t i v] *)
 
-let arity = function
-  | Int63head0 | Int63tail0 -> 1
-  | Int63add | Int63sub | Int63mul
-  | Int63div | Int63mod
-  | Int63lsr | Int63lsl
-  | Int63land | Int63lor | Int63lxor
-  | Int63addc | Int63subc
-  | Int63addCarryC | Int63subCarryC | Int63mulc | Int63diveucl
-  | Int63eq | Int63lt | Int63le
-  | Int63compare -> 2
+type args_red = arg_kind list
 
-  | Int63div21 | Int63addMulDiv -> 3
+(* Invariant only argument of type int63 or an inductive can
+   have kind Kwhnf *)
 
-(** Special Entries for Register **)
+let arity t = List.length (types t) - 1
 
-type prim_ind =
-  | PIT_bool
-  | PIT_carry
-  | PIT_pair
-  | PIT_cmp
+let kind t =
+  let rec aux n = if n <= 0 then [] else Kwhnf :: aux (n - 1) in
+  aux (arity t)
 
-type prim_type =
-  | PT_int63
+(** Special Entries for Register **)
 
 type op_or_type =
   | OT_op of t
   | OT_type of prim_type
 
-let prim_ind_to_string = function
+let prim_ind_to_string (type a) (p : a prim_ind) = match p with
   | PIT_bool -> "bool"
   | PIT_carry -> "carry"
   | PIT_pair -> "pair"
-- 
cgit v1.2.3


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.
---
 kernel/cPrimitives.ml | 51 ++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 50 insertions(+), 1 deletion(-)

(limited to 'kernel/cPrimitives.ml')

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index d433cdc1ba..3154ee8c75 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -33,6 +33,18 @@ type t =
   | Int63lt
   | Int63le
   | Int63compare
+  | Float64opp
+  | Float64abs
+  | Float64compare
+  | Float64add
+  | Float64sub
+  | Float64mul
+  | Float64div
+  | Float64sqrt
+  | Float64ofInt63
+  | Float64normfr_mantissa
+  | Float64frshiftexp
+  | Float64ldshiftexp
 
 let equal (p1 : t) (p2 : t) =
   p1 == p2
@@ -62,6 +74,18 @@ let hash = function
   | Int63lt -> 22
   | Int63le -> 23
   | Int63compare -> 24
+  | Float64opp -> 25
+  | Float64abs -> 26
+  | Float64compare -> 27
+  | Float64add -> 28
+  | Float64sub -> 29
+  | Float64mul -> 30
+  | Float64div -> 31
+  | Float64sqrt -> 32
+  | Float64ofInt63 -> 33
+  | Float64normfr_mantissa -> 34
+  | Float64frshiftexp -> 35
+  | Float64ldshiftexp -> 36
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -89,15 +113,29 @@ let to_string = function
   | Int63lt -> "lt"
   | Int63le -> "le"
   | Int63compare -> "compare"
+  | Float64opp -> "fopp"
+  | Float64abs -> "fabs"
+  | Float64compare -> "fcompare"
+  | Float64add -> "fadd"
+  | Float64sub -> "fsub"
+  | Float64mul -> "fmul"
+  | Float64div -> "fdiv"
+  | Float64sqrt -> "fsqrt"
+  | Float64ofInt63 -> "float_of_int"
+  | Float64normfr_mantissa -> "normfr_mantissa"
+  | Float64frshiftexp -> "frshiftexp"
+  | Float64ldshiftexp -> "ldshiftexp"
 
 type prim_type =
   | PT_int63
+  | PT_float64
 
 type 'a prim_ind =
   | PIT_bool : unit prim_ind
   | PIT_carry : prim_type prim_ind
   | PIT_pair : (prim_type * prim_type) prim_ind
   | PIT_cmp : unit prim_ind
+  | PIT_option : unit prim_ind
 
 type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
 
@@ -107,6 +145,7 @@ type ind_or_type =
 
 let types =
   let int_ty = PITT_type PT_int63 in
+  let float_ty = PITT_type PT_float64 in
   function
   | Int63head0 | Int63tail0 -> [int_ty; int_ty]
   | Int63add | Int63sub | Int63mul
@@ -122,6 +161,14 @@ let types =
   | Int63div21 ->
      [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))]
   | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty]
+  | Float64opp | Float64abs | Float64sqrt -> [float_ty; float_ty]
+  | Float64ofInt63 -> [int_ty; float_ty]
+  | Float64normfr_mantissa -> [float_ty; int_ty]
+  | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))]
+  | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_option, ())]
+  | Float64add | Float64sub | Float64mul
+  | Float64div -> [float_ty; float_ty; float_ty]
+  | Float64ldshiftexp -> [float_ty; int_ty; float_ty]
 
 type arg_kind =
   | Kparam (* not needed for the evaluation of the primitive when it reduces *)
@@ -130,7 +177,7 @@ type arg_kind =
 
 type args_red = arg_kind list
 
-(* Invariant only argument of type int63 or an inductive can
+(* Invariant only argument of type int63, float or an inductive can
    have kind Kwhnf *)
 
 let arity t = List.length (types t) - 1
@@ -150,9 +197,11 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with
   | PIT_carry -> "carry"
   | PIT_pair -> "pair"
   | PIT_cmp -> "cmp"
+  | PIT_option -> "option"
 
 let prim_type_to_string = function
   | PT_int63 -> "int63_type"
+  | PT_float64 -> "float64_type"
 
 let op_or_type_to_string = function
   | OT_op op -> to_string op
-- 
cgit v1.2.3


From 79605dabb10e889ae998bf72c8483f095277e693 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 28 Aug 2018 14:31:37 +0200
Subject: Change return type of primitive float comparison

Replace `option comparison` with `float_comparison` (:= `FEq | FLt |
FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid
boxing and an extra match when using primitive float comparison.
---
 kernel/cPrimitives.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/cPrimitives.ml')

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 3154ee8c75..d5ed2c1a06 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -135,7 +135,7 @@ type 'a prim_ind =
   | PIT_carry : prim_type prim_ind
   | PIT_pair : (prim_type * prim_type) prim_ind
   | PIT_cmp : unit prim_ind
-  | PIT_option : unit prim_ind
+  | PIT_f_cmp : unit prim_ind
 
 type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
 
@@ -165,7 +165,7 @@ let types =
   | Float64ofInt63 -> [int_ty; float_ty]
   | Float64normfr_mantissa -> [float_ty; int_ty]
   | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))]
-  | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_option, ())]
+  | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
   | Float64add | Float64sub | Float64mul
   | Float64div -> [float_ty; float_ty; float_ty]
   | Float64ldshiftexp -> [float_ty; int_ty; float_ty]
@@ -197,7 +197,7 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with
   | PIT_carry -> "carry"
   | PIT_pair -> "pair"
   | PIT_cmp -> "cmp"
-  | PIT_option -> "option"
+  | PIT_f_cmp -> "f_cmp"
 
 let prim_type_to_string = function
   | PT_int63 -> "int63_type"
-- 
cgit v1.2.3


From d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 28 Aug 2018 18:56:07 +0200
Subject: Implement classify on primitive float

---
 kernel/cPrimitives.ml | 24 +++++++++++++++---------
 1 file changed, 15 insertions(+), 9 deletions(-)

(limited to 'kernel/cPrimitives.ml')

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index d5ed2c1a06..02a5351ccf 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -36,6 +36,7 @@ type t =
   | Float64opp
   | Float64abs
   | Float64compare
+  | Float64classify
   | Float64add
   | Float64sub
   | Float64mul
@@ -77,15 +78,16 @@ let hash = function
   | Float64opp -> 25
   | Float64abs -> 26
   | Float64compare -> 27
-  | Float64add -> 28
-  | Float64sub -> 29
-  | Float64mul -> 30
-  | Float64div -> 31
-  | Float64sqrt -> 32
-  | Float64ofInt63 -> 33
-  | Float64normfr_mantissa -> 34
-  | Float64frshiftexp -> 35
-  | Float64ldshiftexp -> 36
+  | Float64classify -> 28
+  | Float64add -> 29
+  | Float64sub -> 30
+  | Float64mul -> 31
+  | Float64div -> 32
+  | Float64sqrt -> 33
+  | Float64ofInt63 -> 34
+  | Float64normfr_mantissa -> 35
+  | Float64frshiftexp -> 36
+  | Float64ldshiftexp -> 37
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -116,6 +118,7 @@ let to_string = function
   | Float64opp -> "fopp"
   | Float64abs -> "fabs"
   | Float64compare -> "fcompare"
+  | Float64classify -> "fclassify"
   | Float64add -> "fadd"
   | Float64sub -> "fsub"
   | Float64mul -> "fmul"
@@ -136,6 +139,7 @@ type 'a prim_ind =
   | PIT_pair : (prim_type * prim_type) prim_ind
   | PIT_cmp : unit prim_ind
   | PIT_f_cmp : unit prim_ind
+  | PIT_f_class : unit prim_ind
 
 type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
 
@@ -166,6 +170,7 @@ let types =
   | Float64normfr_mantissa -> [float_ty; int_ty]
   | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))]
   | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
+  | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())]
   | Float64add | Float64sub | Float64mul
   | Float64div -> [float_ty; float_ty; float_ty]
   | Float64ldshiftexp -> [float_ty; int_ty; float_ty]
@@ -198,6 +203,7 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with
   | PIT_pair -> "pair"
   | PIT_cmp -> "cmp"
   | PIT_f_cmp -> "f_cmp"
+  | PIT_f_class -> "f_class"
 
 let prim_type_to_string = function
   | PT_int63 -> "int63_type"
-- 
cgit v1.2.3


From 5f1270242f71a0a1da7c868967e1071d28ed83fb Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 28 Aug 2018 23:37:49 +0200
Subject: Add next_{up,down} primitive float functions

---
 kernel/cPrimitives.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'kernel/cPrimitives.ml')

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 02a5351ccf..342cc29a22 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -46,6 +46,8 @@ type t =
   | Float64normfr_mantissa
   | Float64frshiftexp
   | Float64ldshiftexp
+  | Float64next_up
+  | Float64next_down
 
 let equal (p1 : t) (p2 : t) =
   p1 == p2
@@ -88,6 +90,8 @@ let hash = function
   | Float64normfr_mantissa -> 35
   | Float64frshiftexp -> 36
   | Float64ldshiftexp -> 37
+  | Float64next_up -> 38
+  | Float64next_down -> 39
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -128,6 +132,8 @@ let to_string = function
   | Float64normfr_mantissa -> "normfr_mantissa"
   | Float64frshiftexp -> "frshiftexp"
   | Float64ldshiftexp -> "ldshiftexp"
+  | Float64next_up    -> "next_up"
+  | Float64next_down  -> "next_down"
 
 type prim_type =
   | PT_int63
@@ -165,7 +171,8 @@ let types =
   | Int63div21 ->
      [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))]
   | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty]
-  | Float64opp | Float64abs | Float64sqrt -> [float_ty; float_ty]
+  | Float64opp | Float64abs | Float64sqrt
+  | Float64next_up | Float64next_down -> [float_ty; float_ty]
   | Float64ofInt63 -> [int_ty; float_ty]
   | Float64normfr_mantissa -> [float_ty; int_ty]
   | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))]
-- 
cgit v1.2.3


From f155ba664a782f000e278d97ee5666e2e7d2adea Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 3 Jul 2019 15:08:44 +0200
Subject: Add "==", "<", "<=" in PrimFloat.v

* Add a related test-suite in compare.v (generated by a bash script)

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
---
 kernel/cPrimitives.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'kernel/cPrimitives.ml')

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 342cc29a22..9ff7f69203 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -35,6 +35,9 @@ type t =
   | Int63compare
   | Float64opp
   | Float64abs
+  | Float64eq
+  | Float64lt
+  | Float64le
   | Float64compare
   | Float64classify
   | Float64add
@@ -92,6 +95,9 @@ let hash = function
   | Float64ldshiftexp -> 37
   | Float64next_up -> 38
   | Float64next_down -> 39
+  | Float64eq -> 40
+  | Float64lt -> 41
+  | Float64le -> 42
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -121,6 +127,9 @@ let to_string = function
   | Int63compare -> "compare"
   | Float64opp -> "fopp"
   | Float64abs -> "fabs"
+  | Float64eq -> "feq"
+  | Float64lt -> "flt"
+  | Float64le -> "fle"
   | Float64compare -> "fcompare"
   | Float64classify -> "fclassify"
   | Float64add -> "fadd"
@@ -176,6 +185,7 @@ let types =
   | Float64ofInt63 -> [int_ty; float_ty]
   | Float64normfr_mantissa -> [float_ty; int_ty]
   | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))]
+  | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())]
   | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
   | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())]
   | Float64add | Float64sub | Float64mul
-- 
cgit v1.2.3