diff options
Diffstat (limited to 'plugins/syntax/r_syntax.ml')
| -rw-r--r-- | plugins/syntax/r_syntax.ml | 57 |
1 files changed, 37 insertions, 20 deletions
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 |