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

1 files changed, 111 insertions, 35 deletions

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index d854cadd15..9ff7f69203 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -33,6 +33,24 @@ type t =
   | Int63lt
   | Int63le
   | Int63compare
+  | Float64opp
+  | Float64abs
+  | Float64eq
+  | Float64lt
+  | Float64le
+  | Float64compare
+  | Float64classify
+  | Float64add
+  | Float64sub
+  | Float64mul
+  | Float64div
+  | Float64sqrt
+  | Float64ofInt63
+  | Float64normfr_mantissa
+  | Float64frshiftexp
+  | Float64ldshiftexp
+  | Float64next_up
+  | Float64next_down
 
 let equal (p1 : t) (p2 : t) =
   p1 == p2
@@ -62,6 +80,24 @@ let hash = function
   | Int63lt -> 22
   | Int63le -> 23
   | Int63compare -> 24
+  | Float64opp -> 25
+  | Float64abs -> 26
+  | Float64compare -> 27
+  | Float64classify -> 28
+  | Float64add -> 29
+  | Float64sub -> 30
+  | Float64mul -> 31
+  | Float64div -> 32
+  | Float64sqrt -> 33
+  | Float64ofInt63 -> 34
+  | Float64normfr_mantissa -> 35
+  | Float64frshiftexp -> 36
+  | Float64ldshiftexp -> 37
+  | Float64next_up -> 38
+  | Float64next_down -> 39
+  | Float64eq -> 40
+  | Float64lt -> 41
+  | Float64le -> 42
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -89,6 +125,72 @@ let to_string = function
   | Int63lt -> "lt"
   | Int63le -> "le"
   | Int63compare -> "compare"
+  | Float64opp -> "fopp"
+  | Float64abs -> "fabs"
+  | Float64eq -> "feq"
+  | Float64lt -> "flt"
+  | Float64le -> "fle"
+  | Float64compare -> "fcompare"
+  | Float64classify -> "fclassify"
+  | Float64add -> "fadd"
+  | Float64sub -> "fsub"
+  | Float64mul -> "fmul"
+  | Float64div -> "fdiv"
+  | Float64sqrt -> "fsqrt"
+  | Float64ofInt63 -> "float_of_int"
+  | Float64normfr_mantissa -> "normfr_mantissa"
+  | Float64frshiftexp -> "frshiftexp"
+  | Float64ldshiftexp -> "ldshiftexp"
+  | Float64next_up    -> "next_up"
+  | Float64next_down  -> "next_down"
+
+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_f_cmp : unit prim_ind
+  | PIT_f_class : unit prim_ind
+
+type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
+
+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
+  let float_ty = PITT_type PT_float64 in
+  function
+  | Int63head0 | Int63tail0 -> [int_ty; int_ty]
+  | Int63add | Int63sub | Int63mul
+  | Int63div | Int63mod
+  | Int63lsr | Int63lsl
+  | 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]
+  | 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))]
+  | 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
+  | 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 *)
@@ -97,58 +199,32 @@ 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 kind = function
-  | Int63head0 | Int63tail0 -> [Kwhnf]
-
-  | Int63add | Int63sub | Int63mul
-  | Int63div | Int63mod
-  | Int63lsr | Int63lsl
-  | Int63land | Int63lor | Int63lxor
-  | Int63addc | Int63subc
-  | Int63addCarryC | Int63subCarryC  | Int63mulc | Int63diveucl
-  | Int63eq | Int63lt | Int63le | Int63compare -> [Kwhnf; Kwhnf]
+let arity t = List.length (types t) - 1
 
-  | Int63div21 | Int63addMulDiv -> [Kwhnf; Kwhnf; Kwhnf]
-
-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
-
-  | Int63div21 | Int63addMulDiv -> 3
+let kind t =
+  let rec aux n = if n <= 0 then [] else Kwhnf :: aux (n - 1) in
+  aux (arity t)
 
 (** Special Entries for Register **)
 
-type prim_ind =
-  | PIT_bool
-  | PIT_carry
-  | PIT_pair
-  | PIT_cmp
-
-type prim_type =
-  | PT_int63
-
 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"
   | PIT_cmp -> "cmp"
+  | PIT_f_cmp -> "f_cmp"
+  | PIT_f_class -> "f_class"
 
 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