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/constr.ml | 31 +++++++++++++++++++++----------
 1 file changed, 21 insertions(+), 10 deletions(-)

(limited to 'kernel/constr.ml')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 8375316003..b60b2d6d04 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -104,6 +104,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of Projection.t * 'constr
   | Int       of Uint63.t
+  | Float     of Float64.t
 (* constr is the fixpoint of the previous type. Requires option
    -rectypes of the Caml compiler to be set *)
 type t = (t, t, Sorts.t, Instance.t) kind_of_term
@@ -241,6 +242,9 @@ let mkRef (gr,u) = let open GlobRef in match gr with
 (* Constructs a primitive integer *)
 let mkInt i = Int i
 
+(* Constructs a primitive float number *)
+let mkFloat f = Float f
+
 (************************************************************************)
 (*    kind_of_term = constructions as seen by the user                 *)
 (************************************************************************)
@@ -446,7 +450,7 @@ let decompose_appvect c =
 
 let fold f acc c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> acc
+    | Construct _ | Int _ | Float _) -> acc
   | Cast (c,_,t) -> f (f acc c) t
   | Prod (_,t,c) -> f (f acc t) c
   | Lambda (_,t,c) -> f (f acc t) c
@@ -466,7 +470,7 @@ let fold f acc c = match kind c with
 
 let iter f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> ()
+    | Construct _ | Int _ | Float _) -> ()
   | Cast (c,_,t) -> f c; f t
   | Prod (_,t,c) -> f t; f c
   | Lambda (_,t,c) -> f t; f c
@@ -486,7 +490,7 @@ let iter f c = match kind c with
 
 let iter_with_binders g f n c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> ()
+    | Construct _ | Int _ | Float _) -> ()
   | Cast (c,_,t) -> f n c; f n t
   | Prod (_,t,c) -> f n t; f (g n) c
   | Lambda (_,t,c) -> f n t; f (g n) c
@@ -512,7 +516,7 @@ let iter_with_binders g f n c = match kind c with
 let fold_constr_with_binders g f n acc c =
   match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> acc
+    | Construct _ | Int _ | Float _) -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
   | Prod (_na,t,c) -> f (g  n) (f n acc t) c
   | Lambda (_na,t,c) -> f (g  n) (f n acc t) c
@@ -608,7 +612,7 @@ let map_return_predicate_with_full_binders g f l ci p =
 
 let map_gen userview f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> c
+    | Construct _ | Int _ | Float _) -> c
   | Cast (b,k,t) ->
       let b' = f b in
       let t' = f t in
@@ -673,7 +677,7 @@ let map = map_gen false
 
 let fold_map f accu c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> accu, c
+    | Construct _ | Int _ | Float _) -> accu, c
   | Cast (b,k,t) ->
       let accu, b' = f accu b in
       let accu, t' = f accu t in
@@ -733,7 +737,7 @@ let fold_map f accu c = match kind c with
 
 let map_with_binders g f l c0 = match kind c0 with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> c0
+    | Construct _ | Int _ | Float _) -> c0
   | Cast (c, k, t) ->
     let c' = f l c in
     let t' = f l t in
@@ -810,7 +814,7 @@ let lift n = liftn n 1
 let fold_with_full_binders g f n acc c =
   let open Context.Rel.Declaration in
   match kind c with
-  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _  | Int _ -> acc
+  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _  | Int _ | Float _ -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
   | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
   | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
@@ -852,6 +856,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
   | Meta m1, Meta m2 -> Int.equal m1 m2
   | Var id1, Var id2 -> Id.equal id1 id2
   | Int i1, Int i2 -> Uint63.equal i1 i2
+  | Float f1, Float f2 -> Float64.equal f1 f2
   | Sort s1, Sort s2 -> leq_sorts s1 s2
   | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2
   | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2
@@ -878,7 +883,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
     Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
   | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _
     | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _
-    | CoFix _ | Int _), _ -> false
+    | CoFix _ | Int _ | Float _), _ -> false
 
 (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
    the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
@@ -1055,6 +1060,8 @@ let constr_ord_int f t1 t2 =
     | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
     | Proj _, _ -> -1 | _, Proj _ -> 1
     | Int i1, Int i2 -> Uint63.compare i1 i2
+    | Int _, _ -> -1 | _, Int _ -> 1
+    | Float f1, Float f2 -> Float64.total_compare f1 f2
 
 let rec compare m n=
   constr_ord_int compare m n
@@ -1139,9 +1146,10 @@ let hasheq t1 t2 =
       && array_eqeq tl1 tl2
       && array_eqeq bl1 bl2
     | Int i1, Int i2 -> i1 == i2
+    | Float f1, Float f2 -> Float64.equal f1 f2
     | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _
       | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _
-      | Fix _ | CoFix _ | Int _), _ -> false
+      | Fix _ | CoFix _ | Int _ | Float _), _ -> false
 
 (** Note that the following Make has the side effect of creating
     once and for all the table we'll use for hash-consing all constr *)
@@ -1247,6 +1255,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
       | Int i ->
         let (h,l) = Uint63.to_int2 i in
         (t, combinesmall 18 (combine h l))
+      | Float f -> (t, combinesmall 19 (Float64.hash f))
 
   and sh_rec t =
     let (y, h) = hash_term t in
@@ -1311,6 +1320,7 @@ let rec hash t =
     | Proj (p,c) ->
       combinesmall 17 (combine (Projection.hash p) (hash c))
     | Int i -> combinesmall 18 (Uint63.hash i)
+    | Float f -> combinesmall 19 (Float64.hash f)
 
 and hash_term_array t =
   Array.fold_left (fun acc t -> combine (hash t) acc) 0 t
@@ -1455,3 +1465,4 @@ let rec debug_print c =
            cut() ++ str":=" ++ debug_print bd) (Array.to_list fixl)) ++
          str"}")
   | Int i -> str"Int("++str (Uint63.to_string i) ++ str")"
+  | Float i -> str"Float("++str (Float64.to_string i) ++ str")"
-- 
cgit v1.2.3