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.

1 files changed, 14 insertions, 7 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index ccc3b6e83c..0c4312dc77 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -62,9 +62,12 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
    Projection.equal p1 p2 && constr_pattern_eq t1 t2
 | PInt i1, PInt i2 ->
    Uint63.equal i1 i2
+| PFloat f1, PFloat f2 ->
+   Float64.equal f1 f2
 | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _
    | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _
-   | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _ | PInt _), _ -> false
+   | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _ | PInt _
+   | PFloat _), _ -> false
 (** FIXME: fixpoint and cofixpoint should be relativized to pattern *)
 
 and pattern_eq (i1, j1, p1) (i2, j2, p2) =
@@ -92,7 +95,7 @@ let rec occur_meta_pattern = function
       (List.exists (fun (_,_,p) -> occur_meta_pattern p) br)
   | PMeta _ | PSoApp _ -> true
   | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _
-    | PInt _ -> false
+    | PInt _ | PFloat _ -> false
 
 let rec occurn_pattern n = function
   | PRel p -> Int.equal n p
@@ -113,7 +116,7 @@ let rec occurn_pattern n = function
       (List.exists (fun (_,_,p) -> occurn_pattern n p) br)
   | PMeta _ | PSoApp _ -> true
   | PEvar (_,args) -> Array.exists (occurn_pattern n) args
-  | PVar _ | PRef _ | PSort _ | PInt _ -> false
+  | PVar _ | PRef _ | PSort _ | PInt _ | PFloat _ -> false
   | PFix (_,(_,tl,bl)) ->
      Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
   | PCoFix (_,(_,tl,bl)) ->
@@ -136,7 +139,7 @@ let rec head_pattern_bound t =
 	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
     | PLambda _ -> raise BoundPattern
-    | PCoFix _ | PInt _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")
+    | PCoFix _ | PInt _ | PFloat _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")
 
 let head_of_constr_reference sigma c = match EConstr.kind sigma c with
   | Const (sp,_) -> GlobRef.ConstRef sp
@@ -213,7 +216,8 @@ let pattern_of_constr env sigma t =
        let env' = Array.fold_left2 push env lna tl in
        PCoFix (ln,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl,
                   Array.map (pattern_of_constr env') bl))
-    | Int i -> PInt i in
+    | Int i -> PInt i
+    | Float f -> PFloat f in
   pattern_of_constr env t
 
 (* To process patterns, we need a translation without typing at all. *)
@@ -235,7 +239,8 @@ let map_pattern_with_binders g f l = function
      let l' = Array.fold_left (fun l na -> g na l) l lna in
      PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
   (* Non recursive *)
-  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ | PInt _ as x) -> x
+  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ | PInt _
+     | PFloat _ as x) -> x
 
 let error_instantiate_pattern id l =
   let is = match l with
@@ -290,7 +295,8 @@ let rec subst_pattern env sigma subst pat =
   | PVar _
   | PEvar _
   | PRel _
-  | PInt _ -> pat
+  | PInt _
+  | PFloat _ -> pat
   | PProj (p,c) -> 
       let p' = Projection.map (subst_mind subst) p in
       let c' = subst_pattern env sigma subst c in
@@ -495,6 +501,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       PCoFix (n, (names, tl, cl))
 
   | GInt i -> PInt i
+  | GFloat f -> PFloat f
   | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ ->
       err ?loc (Pp.str "Non supported pattern."))