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/clambda.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'kernel/clambda.ml')

diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index a764cca354..8c7aa6b17a 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -28,6 +28,7 @@ type lambda =
   | Lint          of int
   | Lmakeblock    of int * lambda array
   | Luint         of Uint63.t
+  | Lfloat        of Float64.t
   | Lval          of structured_values
   | Lsort         of Sorts.t
   | Lind          of pinductive
@@ -143,6 +144,7 @@ let rec pp_lam lam =
        prlist_with_sep spc pp_lam (Array.to_list args) ++
        str")")
   | Luint i -> str (Uint63.to_string i)
+  | Lfloat f -> str (Float64.to_string f)
   | Lval _ -> str "values"
   | Lsort s -> pp_sort s
   | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i
@@ -195,7 +197,8 @@ let shift subst = subs_shft (1, subst)
 
 let map_lam_with_binders g f n lam =
   match lam with
-  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ -> lam
+  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _
+  | Lfloat _ -> lam
   | Levar (evk, args) ->
     let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Levar (evk, args')
@@ -416,7 +419,8 @@ let rec occurrence k kind lam =
     if n = k then
       if kind then false else raise Not_found
     else kind
-  | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ -> kind
+  | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _
+  | Lfloat _ -> kind
   | Levar (_, args) ->
     occurrence_args k kind args
   | Lprod(dom, codom) ->
@@ -763,6 +767,7 @@ let rec lambda_of_constr env c =
     Lproj (Projection.repr p,lc)
 
   | Int i -> Luint i
+  | Float f -> Lfloat f
 
 and lambda_of_app env f args =
   match Constr.kind f with
-- 
cgit v1.2.3