Merge PR #9867: Add primitive floats (binary64 floating-point numbers)

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl

5 files changed, 14 insertions, 9 deletions

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