aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/float_syntax.ml53
-rw-r--r--plugins/syntax/g_numeral.mlg8
-rw-r--r--plugins/syntax/r_syntax.ml57
3 files changed, 91 insertions, 27 deletions
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml
index 23d4d63228..e0a9906689 100644
--- a/plugins/syntax/float_syntax.ml
+++ b/plugins/syntax/float_syntax.ml
@@ -22,9 +22,56 @@ let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
(*** Parsing for float in digital notation ***)
-let interp_float ?loc (sign,n) =
- let sign = Constrexpr.(match sign with SPlus -> "" | SMinus -> "-") in
- DAst.make ?loc (GFloat (Float64.of_string (sign ^ NumTok.to_string n)))
+let warn_inexact_float =
+ CWarnings.create ~name:"inexact-float" ~category:"parsing"
+ (fun (sn, f) ->
+ Pp.strbrk
+ (Printf.sprintf
+ "The constant %s is not a binary64 floating-point value. \
+ A closest value will be used and unambiguously printed %s."
+ sn (Float64.to_string f)))
+
+let interp_float ?loc n =
+ let sn = NumTok.Signed.to_string n in
+ let f = Float64.of_string sn in
+ (* return true when f is not exactly equal to n,
+ this is only used to decide whether or not to display a warning
+ and does not play any actual role in the parsing *)
+ let inexact () = match Float64.classify f with
+ | Float64.(PInf | NInf | NaN) -> true
+ | Float64.(PZero | NZero) -> not (NumTok.Signed.is_zero n)
+ | Float64.(PNormal | NNormal | PSubn | NSubn) ->
+ let m, e =
+ let (_, i), f, e = NumTok.Signed.to_decimal_and_exponent n in
+ let i = NumTok.UnsignedNat.to_string i in
+ let f = match f with
+ | None -> "" | Some f -> NumTok.UnsignedNat.to_string f in
+ let e = match e with
+ | None -> "0" | Some e -> NumTok.SignedNat.to_string e in
+ Bigint.of_string (i ^ f),
+ (try int_of_string e with Failure _ -> 0) - String.length f in
+ let m', e' =
+ let m', e' = Float64.frshiftexp f in
+ let m' = Float64.normfr_mantissa m' in
+ let e' = Uint63.to_int_min e' 4096 - Float64.eshift - 53 in
+ Bigint.of_string (Uint63.to_string m'),
+ e' in
+ let c2, c5 = Bigint.(of_int 2, of_int 5) in
+ (* check m*5^e <> m'*2^e' *)
+ let check m e m' e' =
+ not (Bigint.(equal (mult m (pow c5 e)) (mult m' (pow c2 e')))) in
+ (* check m*5^e*2^e' <> m' *)
+ let check' m e e' m' =
+ not (Bigint.(equal (mult (mult m (pow c5 e)) (pow c2 e')) m')) in
+ (* we now have to check m*10^e <> m'*2^e' *)
+ if e >= 0 then
+ if e <= e' then check m e m' (e' - e)
+ else check' m e (e - e') m'
+ else (* e < 0 *)
+ if e' <= e then check m' (-e) m (e - e')
+ else check' m' (-e) (e' - e) m in
+ if inexact () then warn_inexact_float ?loc (sn, f);
+ DAst.make ?loc (GFloat f)
(* Pretty printing is already handled in constrextern.ml *)
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 49d29e7b63..e66dbe17b2 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -21,16 +21,16 @@ open Pcoq.Prim
let pr_numnot_option = function
| Nop -> mt ()
- | Warning n -> str "(warning after " ++ str n ++ str ")"
- | Abstract n -> str "(abstract after " ++ str n ++ str ")"
+ | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")"
+ | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")"
}
VERNAC ARGUMENT EXTEND numnotoption
PRINTED BY { pr_numnot_option }
| [ ] -> { Nop }
-| [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft }
-| [ "(" "abstract" "after" bigint(n) ")" ] -> { Abstract n }
+| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) }
+| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) }
END
VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 7043653f7b..c4e9c8b73d 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -12,7 +12,6 @@ open Util
open Names
open Glob_term
open Bigint
-open Constrexpr
(* Poor's man DECLARE PLUGIN *)
let __coq_plugin_name = "r_syntax_plugin"
@@ -113,8 +112,8 @@ let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z")
let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos")
-let r_of_rawnum ?loc (sign,n) =
- let n, f, e = NumTok.(n.int, n.frac, n.exp) in
+let r_of_rawnum ?loc n =
+ let n,e = NumTok.Signed.to_bigint_and_exponent n in
let izr z =
DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in
let rmult r r' =
@@ -126,15 +125,7 @@ let r_of_rawnum ?loc (sign,n) =
let e = pos_of_bignat e in
DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [ten; e]) in
let n =
- let n = Bigint.of_string (n ^ f) in
- let n = match sign with SPlus -> n | SMinus -> Bigint.(neg n) in
izr (z_of_int ?loc n) in
- let e =
- let e = if e = "" then Bigint.zero else match e.[1] with
- | '+' -> Bigint.of_string (String.sub e 2 (String.length e - 2))
- | '-' -> Bigint.(neg (of_string (String.sub e 2 (String.length e - 2))))
- | _ -> Bigint.of_string (String.sub e 1 (String.length e - 1)) in
- Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' f))))) in
if Bigint.is_strictly_pos e then rmult n (izr (pow10 e))
else if Bigint.is_strictly_neg e then rdiv n (izr (pow10 (neg e)))
else n (* e = 0 *)
@@ -143,12 +134,41 @@ let r_of_rawnum ?loc (sign,n) =
(* Printing R via scopes *)
(**********************************************************************)
-let rawnum_of_r c = match DAst.get c with
+let rawnum_of_r c =
+ (* print i * 10^e, precondition: e <> 0 *)
+ let numTok_of_int_exp i e =
+ (* choose between 123e-2 and 1.23, this is purely heuristic
+ and doesn't play any soundness role *)
+ let choose_exponent =
+ if Bigint.is_strictly_pos e then
+ true (* don't print 12 * 10^2 as 1200 to distinguish them *)
+ else
+ let i = Bigint.to_string i in
+ let li = if i.[0] = '-' then String.length i - 1 else String.length i in
+ let e = Bigint.neg e in
+ let le = String.length (Bigint.to_string e) in
+ Bigint.(less_than (add (of_int li) (of_int le)) e) in
+ (* print 123 * 10^-2 as 123e-2 *)
+ let numTok_exponent () = NumTok.Signed.of_bigint_and_exponent i e in
+ (* print 123 * 10^-2 as 1.23, precondition e < 0 *)
+ let numTok_dot () =
+ let s, i =
+ if Bigint.is_pos_or_zero i then NumTok.SPlus, Bigint.to_string i
+ else NumTok.SMinus, Bigint.(to_string (neg i)) in
+ let ni = String.length i in
+ let e = - (Bigint.to_int e) in
+ assert (e > 0);
+ let i, f =
+ if e < ni then String.sub i 0 (ni - e), String.sub i (ni - e) e
+ else "0", String.make (e - ni) '0' ^ i in
+ let i = s, NumTok.UnsignedNat.of_string i in
+ let f = NumTok.UnsignedNat.of_string f in
+ NumTok.Signed.of_decimal_and_exponent i (Some f) None in
+ if choose_exponent then numTok_exponent () else numTok_dot () in
+ match DAst.get c with
| GApp (r, [a]) when is_gr r glob_IZR ->
let n = bigint_of_z a in
- let s, n =
- if is_strictly_neg n then SMinus, neg n else SPlus, n in
- s, NumTok.int (to_string n)
+ NumTok.Signed.of_bigint n
| GApp (md, [l; r]) when is_gr md glob_Rmult || is_gr md glob_Rdiv ->
begin match DAst.get l, DAst.get r with
| GApp (i, [l]), GApp (i', [r])
@@ -161,11 +181,8 @@ let rawnum_of_r c = match DAst.get c with
else
let i = bigint_of_z l in
let e = bignat_of_pos e in
- let s, i = if is_pos_or_zero i then SPlus, i else SMinus, neg i in
- let i = Bigint.to_string i in
- let se = if is_gr md glob_Rdiv then "-" else "" in
- let e = "e" ^ se ^ Bigint.to_string e in
- s, { NumTok.int = i; frac = ""; exp = e }
+ let e = if is_gr md glob_Rdiv then neg e else e in
+ numTok_of_int_exp i e
| _ -> raise Non_closed_number
end
| _ -> raise Non_closed_number
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:05:28 +0000