From 2a31e23df8ff0ab67a09008858fa49e77e5f4332 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 31 Jan 2020 01:04:07 +0100 Subject: Adding bignat to parse positive numbers; bigint now includes negative ints. Warning: in notations, the name "bigint" actually meant "bignat". A clarification will eventually be needed. --- plugins/syntax/g_numeral.mlg | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/syntax') diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 49d29e7b63..eccefdf64a 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -29,8 +29,8 @@ let pr_numnot_option = function 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 waft } +| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract n } END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF -- cgit v1.2.3 From 08189431706298d599cffea2e41dd51290305ba3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 31 Jan 2020 13:36:34 +0100 Subject: Centralizing all kinds of numeral string management in numTok.ml. Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him. --- plugins/syntax/float_syntax.ml | 5 ++--- plugins/syntax/g_numeral.mlg | 8 ++++---- plugins/syntax/r_syntax.ml | 24 +++++------------------- 3 files changed, 11 insertions(+), 26 deletions(-) (limited to 'plugins/syntax') diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml index 23d4d63228..dadce9a9ea 100644 --- a/plugins/syntax/float_syntax.ml +++ b/plugins/syntax/float_syntax.ml @@ -22,9 +22,8 @@ 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 interp_float ?loc n = + DAst.make ?loc (GFloat (Float64.of_string (NumTok.Signed.to_string n))) (* Pretty printing is already handled in constrextern.ml *) diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index eccefdf64a..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" bignat(waft) ")" ] -> { Warning waft } -| [ "(" "abstract" "after" bignat(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..e0dc3d8989 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 *) @@ -146,9 +137,7 @@ let r_of_rawnum ?loc (sign,n) = let rawnum_of_r c = 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 +150,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.Signed.of_bigint_and_exponent i e | _ -> raise Non_closed_number end | _ -> raise Non_closed_number -- cgit v1.2.3