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.

7 files changed, 17 insertions, 11 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index cca212f332..872f30135f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -351,7 +351,7 @@ let rec extract_type env sg db j c args =
             | (Info, TypeScheme) ->
               extract_type_app env sg db (r, type_sign env sg ty) args
             | (Info, Default) -> Tunknown))
-    | Cast _ | LetIn _ | Construct _ | Int _ -> assert false
+    | Cast _ | LetIn _ | Construct _ | Int _ | Float _ -> assert false
 
 (*s Auxiliary function dealing with type application.
   Precondition: [r] is a type scheme represented by the signature [s],
@@ -690,6 +690,7 @@ let rec extract_term env sg mle mlt c args =
        let extract_var mlt = put_magic (mlt,vty) (MLglob (GlobRef.VarRef v)) in
        extract_app env sg mle mlt extract_var args
     | Int i -> assert (args = []); MLuint i
+    | Float _ -> assert false (* TODO: Implement primitive float for extraction *)
     | Ind _ | Prod _ | Sort _ -> assert false
 
 (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 7be049269c..6db0a1119b 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -692,13 +692,14 @@ let build_proof
               end
           | Cast(t,_,_) ->
               build_proof do_finalize {dyn_infos with info = t} g
-          | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
+          | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ | Float _ ->
               do_finalize dyn_infos g
           | App(_,_) ->
               let f,args = decompose_app sigma dyn_infos.info in
               begin
                 match EConstr.kind sigma f with
-      | Int _ -> user_err Pp.(str "integer cannot be applied")
+                  | Int _ -> user_err Pp.(str "integer cannot be applied")
+                  | Float _ -> user_err Pp.(str "float cannot be applied")
                   | App _ -> assert false (* we have collected all the app in decompose_app *)
                   | Proj _ -> assert false (*FIXME*)
                   | Var _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ | Sort _ | Prod _ ->
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 0452665585..6add56dd5b 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -68,7 +68,7 @@ let is_rec names =
   let check_id id names =  Id.Set.mem id names in
   let rec lookup names gt = match DAst.get gt with
     | GVar(id) -> check_id id names
-    | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ | GInt _ -> false
+    | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ | GInt _ | GFloat _ -> false
     | GCast(b,_) -> lookup names b
     | GRec _ -> CErrors.user_err (Pp.str "GRec not handled")
     | GIf(b,_,lhs,rhs) ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7c17ecdba0..895b6a37ee 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -478,7 +478,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
   observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
   let open CAst in
   match DAst.get rt with
-    | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _  | GHole _ | GInt _ ->
+    | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _  | GHole _ | GInt _ | GFloat _ ->
 	(* do nothing (except changing type of course) *)
 	mk_result [] rt avoid
     | GApp(_,_) ->
@@ -590,6 +590,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
 	    | GRec _ -> user_err Pp.(str "Not handled GRec")
 	    | GProd _ -> user_err Pp.(str "Cannot apply a type")
             | GInt _ -> user_err Pp.(str "Cannot apply an integer")
+      | GFloat _ -> user_err Pp.(str "Cannot apply a float")
 	end (* end of the application treatement *)
 
     | GLambda(n,_,t,b) ->
@@ -1231,7 +1232,7 @@ let rebuild_cons env nb_args relname args crossed_types rt =
    TODO: Find a valid way to deal with implicit arguments here!
 *)
 let rec compute_cst_params relnames params gt = DAst.with_val (function
-  | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ -> params
+  | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ | GFloat _ -> params
   | GApp(f,args) ->
     begin match DAst.get f with
     | GVar relname' when Id.Set.mem relname' relnames ->
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 8abccabae6..5f54bad598 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -115,6 +115,7 @@ let change_vars =
       | GSort _ as x -> x
       | GHole _ as x -> x
       | GInt _ as x -> x
+      | GFloat _ as x -> x
       | GCast(b,c) ->
 	  GCast(change_vars mapping b,
                 Glob_ops.map_cast_type (change_vars mapping) c)
@@ -295,6 +296,7 @@ let rec alpha_rt excluded rt =
     | GRec _ -> user_err Pp.(str "Not handled GRec")
     | GSort _
     | GInt _
+    | GFloat _
     | GHole _ as rt -> rt
     | GCast (b,c) ->
 	GCast(alpha_rt excluded b,
@@ -354,7 +356,7 @@ let is_free_in id =
     | GHole _ -> false
     | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
     | GCast (b,CastCoerce) -> is_free_in b
-    | GInt _ -> false
+    | GInt _ | GFloat _ -> false
     ) x
   and is_free_in_br {CAst.v=(ids,_,rt)} =
     (not (Id.List.mem id ids)) && is_free_in rt
@@ -447,6 +449,7 @@ let replace_var_by_term x_id term =
       | GSort _
       | GHole _ as rt -> rt
       | GInt _ as rt -> rt
+      | GFloat _ as rt -> rt
       | GCast(b,c) ->
 	  GCast(replace_var_by_pattern b,
                 Glob_ops.map_cast_type replace_var_by_pattern c)
@@ -529,7 +532,7 @@ let expand_as =
       | PatCstr(_,patl,_) -> List.fold_left add_as map patl
   in
   let rec expand_as map = DAst.map (function
-      | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ as rt -> rt
+      | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ as rt -> rt
       | GVar id as rt ->
 	  begin
 	    try
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 29356df81d..66ed1961ba 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -270,7 +270,7 @@ let check_not_nested env sigma forbidden e =
   let rec check_not_nested e =
     match EConstr.kind sigma e with
       | Rel _ -> ()
-      | Int _ -> ()
+      | Int _ | Float _ -> ()
       | Var x ->
         if Id.List.mem x forbidden
         then user_err ~hdr:"Recdef.check_not_nested"
@@ -452,7 +452,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
           | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env env sigma expr_info.info ++ Pp.str ".")
       end
     | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
-    | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
+    | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ | Float _ ->
       let new_continuation_tac =
         jinfo.otherS () expr_info continuation_tac in
       new_continuation_tac expr_info g
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 4d7a04f5ee..9682487a22 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -319,7 +319,7 @@ let iter_constr_LR f c = match kind c with
     for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
   | Proj(_,a) -> f a
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _
-     | Int _) -> ()
+     | Int _ | Float _) -> ()
 
 (* The comparison used to determine which subterms matches is KEYED        *)
 (* CONVERSION. This looks for convertible terms that either have the same  *)