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/typeops.ml | 51 ++++++++++++++++++---------------------------------
 1 file changed, 18 insertions(+), 33 deletions(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index b87384d228..a967711a83 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -243,39 +243,24 @@ let type_of_prim env t =
     | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|])
     | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.")
   in
-  let rec nary_int63_op arity ty =
-    if Int.equal arity 0 then ty
-      else Constr.mkProd(Context.nameR (Id.of_string "x"), int_ty, nary_int63_op (arity-1) ty)
-  in
-  let return_ty =
-    let open CPrimitives in
-    match t with
-    | Int63head0
-    | Int63tail0
-    | Int63add
-    | Int63sub
-    | Int63mul
-    | Int63div
-    | Int63mod
-    | Int63lsr
-    | Int63lsl
-    | Int63land
-    | Int63lor
-    | Int63lxor
-    | Int63addMulDiv -> int_ty
-    | Int63eq
-    | Int63lt
-    | Int63le -> bool_ty ()
-    | Int63mulc
-    | Int63div21
-    | Int63diveucl -> pair_ty int_ty int_ty
-    | Int63addc
-    | Int63subc
-    | Int63addCarryC
-    | Int63subCarryC -> carry_ty int_ty
-    | Int63compare -> compare_ty ()
-  in
-  nary_int63_op (CPrimitives.arity t) return_ty
+  let open CPrimitives in
+  let tr_prim_type = function
+    | PT_int63 -> int_ty in
+  let tr_ind (type t) (i : t prim_ind) (a : t) = match i, a with
+    | PIT_bool, () -> bool_ty ()
+    | PIT_carry, t -> carry_ty (tr_prim_type t)
+    | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2)
+    | PIT_cmp, () -> compare_ty () in
+  let tr_type = function
+    | PITT_ind (i, a) -> tr_ind i a
+    | PITT_type t -> tr_prim_type t in
+  let rec nary_op = function
+    | [] -> assert false
+    | [ret_ty] -> tr_type ret_ty
+    | arg_ty :: r ->
+       let arg_ty = tr_type arg_ty in
+       Constr.mkProd(Context.nameR (Id.of_string "x"), arg_ty, nary_op r) in
+  nary_op (types t)
 
 let type_of_prim_or_type env = let open CPrimitives in
   function
-- 
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/typeops.ml | 25 ++++++++++++++++++++++---
 1 file changed, 22 insertions(+), 3 deletions(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a967711a83..a9913772f2 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -215,14 +215,22 @@ let type_of_apply env func funt argsv argstv =
 (* Type of primitive constructs *)
 let type_of_prim_type _env = function
   | CPrimitives.PT_int63 -> Constr.mkSet
+  | CPrimitives.PT_float64 -> Constr.mkSet
 
 let type_of_int env =
   match env.retroknowledge.Retroknowledge.retro_int63 with
   | Some c -> mkConst c
   | None -> CErrors.user_err Pp.(str"The type int must be registered before this construction can be typechecked.")
 
+let type_of_float env =
+  match env.retroknowledge.Retroknowledge.retro_float64 with
+  | Some c -> mkConst c
+  | None -> raise
+        (Invalid_argument "Typeops.type_of_float: float64 not_defined")
+
 let type_of_prim env t =
-  let int_ty = type_of_int env in
+  let int_ty () = type_of_int env in
+  let float_ty () = type_of_float env in
   let bool_ty () =
     match env.retroknowledge.Retroknowledge.retro_bool with
     | Some ((ind,_),_) -> Constr.mkInd ind
@@ -238,6 +246,11 @@ let type_of_prim env t =
     | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|])
     | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.")
   in
+  let option_ty ty =
+    match env.retroknowledge.Retroknowledge.retro_option with
+    | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|ty|])
+    | None -> CErrors.user_err Pp.(str"The type option must be registered before this primitive.")
+  in
   let carry_ty int_ty =
     match env.retroknowledge.Retroknowledge.retro_carry with
     | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|])
@@ -245,12 +258,14 @@ let type_of_prim env t =
   in
   let open CPrimitives in
   let tr_prim_type = function
-    | PT_int63 -> int_ty in
+    | PT_int63 -> int_ty ()
+    | PT_float64 -> float_ty () in
   let tr_ind (type t) (i : t prim_ind) (a : t) = match i, a with
     | PIT_bool, () -> bool_ty ()
     | PIT_carry, t -> carry_ty (tr_prim_type t)
     | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2)
-    | PIT_cmp, () -> compare_ty () in
+    | PIT_cmp, () -> compare_ty ()
+    | PIT_option, () -> option_ty (compare_ty ()) in
   let tr_type = function
     | PITT_ind (i, a) -> tr_ind i a
     | PITT_type t -> tr_prim_type t in
@@ -270,6 +285,9 @@ let type_of_prim_or_type env = let open CPrimitives in
 let judge_of_int env i =
   make_judge (Constr.mkInt i) (type_of_int env)
 
+let judge_of_float env f =
+  make_judge (Constr.mkFloat f) (type_of_float env)
+
 (* Type of product *)
 
 let sort_of_product env domsort rangsort =
@@ -568,6 +586,7 @@ let rec execute env cstr =
 
     (* Primitive types *)
     | Int _ -> cstr, type_of_int env
+    | Float _ -> cstr, type_of_float env
 
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
-- 
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/typeops.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a9913772f2..3e79b174b8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -241,16 +241,16 @@ let type_of_prim env t =
     | Some ((ind,_),_,_) -> Constr.mkInd ind
     | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.")
   in
+  let f_compare_ty () =
+    match env.retroknowledge.Retroknowledge.retro_f_cmp with
+    | Some ((ind,_),_,_,_) -> Constr.mkInd ind
+    | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.")
+  in
   let pair_ty fst_ty snd_ty =
     match env.retroknowledge.Retroknowledge.retro_pair with
     | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|])
     | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.")
   in
-  let option_ty ty =
-    match env.retroknowledge.Retroknowledge.retro_option with
-    | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|ty|])
-    | None -> CErrors.user_err Pp.(str"The type option must be registered before this primitive.")
-  in
   let carry_ty int_ty =
     match env.retroknowledge.Retroknowledge.retro_carry with
     | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|])
@@ -265,7 +265,7 @@ let type_of_prim env t =
     | PIT_carry, t -> carry_ty (tr_prim_type t)
     | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2)
     | PIT_cmp, () -> compare_ty ()
-    | PIT_option, () -> option_ty (compare_ty ()) in
+    | PIT_f_cmp, () -> f_compare_ty () in
   let tr_type = function
     | PITT_ind (i, a) -> tr_ind i a
     | PITT_type t -> tr_prim_type t in
-- 
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/typeops.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3e79b174b8..1cc40a6707 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -246,6 +246,11 @@ let type_of_prim env t =
     | Some ((ind,_),_,_,_) -> Constr.mkInd ind
     | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.")
   in
+  let f_class_ty () =
+    match env.retroknowledge.Retroknowledge.retro_f_class with
+    | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind
+    | None -> CErrors.user_err Pp.(str"The type float_class must be registered before this primitive.")
+  in
   let pair_ty fst_ty snd_ty =
     match env.retroknowledge.Retroknowledge.retro_pair with
     | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|])
@@ -265,7 +270,8 @@ let type_of_prim env t =
     | PIT_carry, t -> carry_ty (tr_prim_type t)
     | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2)
     | PIT_cmp, () -> compare_ty ()
-    | PIT_f_cmp, () -> f_compare_ty () in
+    | PIT_f_cmp, () -> f_compare_ty ()
+    | PIT_f_class, () -> f_class_ty () in
   let tr_type = function
     | PITT_ind (i, a) -> tr_ind i a
     | PITT_type t -> tr_prim_type t in
-- 
cgit v1.2.3