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

4 files changed, 37 insertions, 3 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 217381d854..0a1371413a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -752,6 +752,30 @@ let extended_glob_local_binder_of_decl loc = function
 let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u)
 
 (**********************************************************************)
+(* mapping special floats                                             *)
+
+(* this helper function is copied from notation.ml as it's not exported *)
+let qualid_of_ref n =
+  n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+
+let q_infinity () = qualid_of_ref "num.float.infinity"
+let q_neg_infinity () = qualid_of_ref "num.float.neg_infinity"
+let q_nan () = qualid_of_ref "num.float.nan"
+
+let extern_float f scopes =
+  if Float64.is_nan f then CRef(q_nan (), None)
+  else if Float64.is_infinity f then CRef(q_infinity (), None)
+  else if Float64.is_neg_infinity f then CRef(q_neg_infinity (), None)
+  else
+    let sign = if Float64.sign f then SMinus else SPlus in
+    let s = Float64.(to_string (abs f)) in
+    match NumTok.of_string s with
+    | None -> assert false
+    | Some n ->
+       extern_prim_token_delimiter_if_required (Numeral (sign, n))
+       "float" "float_scope" scopes
+
+(**********************************************************************)
 (* mapping glob_constr to constr_expr                                    *)
 
 let extern_glob_sort = function
@@ -972,6 +996,8 @@ let rec extern inctx scopes vars r =
        (Numeral (SPlus, NumTok.int (Uint63.to_string i)))
        "int63" "int63_scope" (snd scopes)
 
+  | GFloat f -> extern_float f (snd scopes)
+
   in insert_coercion coercion (CAst.make ?loc c)
 
 and extern_typ (subentry,(_,scopes)) =
@@ -1314,6 +1340,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
   | PSort Sorts.InSet -> GSort (UNamed [GSet,0])
   | PSort Sorts.InType -> GSort (UAnonymous {rigid=true})
   | PInt i -> GInt i
+  | PFloat f -> GFloat f
 
 let extern_constr_pattern env sigma pat =
   extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 5f41c2a366..0de4eb5fa1 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -216,7 +216,7 @@ let rec is_rigid_head sigma t = match kind sigma t with
         | Fix ((fi,i),_) -> is_rigid_head sigma (args.(fi.(i)))
         | _ -> is_rigid_head sigma f)
   | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
-  | Prod _ | Meta _ | Cast _ | Int _ -> assert false
+  | Prod _ | Meta _ | Cast _ | Int _ | Float _ -> assert false
 
 let is_rigid env sigma t =
   let open Context.Rel.Declaration in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index f30a874426..7e146754b2 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -90,9 +90,11 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
   (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
 | NInt i1, NInt i2 ->
    Uint63.equal i1 i2
+| NFloat f1, NFloat f2 ->
+  Float64.equal f1 f2
 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
   | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
-  | NRec _ | NSort _ | NCast _ | NInt _), _ -> false
+  | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _), _ -> false
 
 (**********************************************************************)
 (* Re-interpret a notation as a glob_constr, taking care of binders   *)
@@ -222,6 +224,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
   | NHole (x, naming, arg)  -> GHole (x, naming, arg)
   | NRef x -> GRef (x,None)
   | NInt i -> GInt i
+  | NFloat f -> GFloat f
 
 let glob_constr_of_notation_constr ?loc x =
   let rec aux () x =
@@ -438,6 +441,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
   | GCast (c,k) -> NCast (aux c,map_cast_type aux k)
   | GSort s -> NSort s
   | GInt i -> NInt i
+  | GFloat f -> NFloat f
   | GHole (w,naming,arg) ->
      if arg != None then has_ltac := true;
      NHole (w, naming, arg)
@@ -627,6 +631,7 @@ let rec subst_notation_constr subst bound raw =
 
   | NSort _ -> raw
   | NInt _ -> raw
+  | NFloat _ -> raw
 
   | NHole (knd, naming, solve) ->
     let nknd = match knd with
@@ -1196,6 +1201,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
 
   | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma
   | GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma
+  | GFloat f1, NFloat f2 when Float64.equal f1 f2 -> sigma
   | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
   | a, NHole _ -> sigma
 
@@ -1223,7 +1229,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
 
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
      | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
-     | GCast _ | GInt _ ), _ -> raise No_match
+     | GCast _ | GInt _ | GFloat _), _ -> raise No_match
 
 and match_in u = match_ true u
 
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 908455bd05..c6ddd9ac95 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -44,6 +44,7 @@ type notation_constr =
   | NSort of glob_sort
   | NCast of notation_constr * notation_constr cast_type
   | NInt of Uint63.t
+  | NFloat of Float64.t
 
 (** Note concerning NList: first constr is iterator, second is terminator;
     first id is where each argument of the list has to be substituted