diff options
Diffstat (limited to 'plugins/syntax')
| -rw-r--r-- | plugins/syntax/float_syntax.ml | 50 | ||||
| -rw-r--r-- | plugins/syntax/r_syntax.ml | 35 |
2 files changed, 82 insertions, 3 deletions
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml index dadce9a9ea..e0a9906689 100644 --- a/plugins/syntax/float_syntax.ml +++ b/plugins/syntax/float_syntax.ml @@ -22,8 +22,56 @@ let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) (*** Parsing for float in digital notation ***) +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 = - DAst.make ?loc (GFloat (Float64.of_string (NumTok.Signed.to_string 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/r_syntax.ml b/plugins/syntax/r_syntax.ml index e0dc3d8989..c4e9c8b73d 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -134,7 +134,38 @@ let r_of_rawnum ?loc 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 NumTok.Signed.of_bigint n @@ -151,7 +182,7 @@ let rawnum_of_r c = match DAst.get c with let i = bigint_of_z l in let e = bignat_of_pos e in let e = if is_gr md glob_Rdiv then neg e else e in - NumTok.Signed.of_bigint_and_exponent i e + numTok_of_int_exp i e | _ -> raise Non_closed_number end | _ -> raise Non_closed_number |