diff options
| author | Hugo Herbelin | 2020-01-31 13:36:34 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-22 15:02:43 +0100 |
| commit | 08189431706298d599cffea2e41dd51290305ba3 (patch) | |
| tree | 919eaba259e65658dc1cda1615250222bac08e9a /dev | |
| parent | 2a31e23df8ff0ab67a09008858fa49e77e5f4332 (diff) | |
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.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.md | 2 | ||||
| -rw-r--r-- | dev/top_printers.dbg | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | dev/top_printers.mli | 2 |
4 files changed, 8 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index b82388675c..eac8d86b0a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -11,6 +11,8 @@ Notations: +- Most operators on numerals have moved to file numTok.ml. + - Types `precedence`, `parenRelation`, `tolerability` in `notgram_ops.ml` have been reworked. See `entry_level` and `entry_relative_level` in `constrexpr.ml`. diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index da224aa5ab..06db787488 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -24,6 +24,8 @@ install_printer Top_printers.ppglob_constr install_printer Top_printers.pppattern install_printer Top_printers.ppfconstr install_printer Top_printers.ppbigint +install_printer Top_printers.ppnumtokunsigned +install_printer Top_printers.ppnumtokunsignednat install_printer Top_printers.ppintset install_printer Top_printers.ppidset install_printer Top_printers.ppidmapgen diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 96dbf9142b..7002cbffac 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -86,6 +86,8 @@ let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let ppbigint n = pp (str (Bigint.to_string n));; +let ppnumtokunsigned n = pp (NumTok.Unsigned.print n) +let ppnumtokunsignednat n = pp (NumTok.UnsignedNat.print n) let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" let ppintset l = pp (prset int (Int.Set.elements l)) diff --git a/dev/top_printers.mli b/dev/top_printers.mli index c5f97f5873..c826391cac 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -54,6 +54,8 @@ val pppattern : Pattern.constr_pattern -> unit val ppfconstr : CClosure.fconstr -> unit val ppbigint : Bigint.bigint -> unit +val ppnumtokunsigned : NumTok.Unsigned.t -> unit +val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit val ppintset : Int.Set.t -> unit val ppidset : Names.Id.Set.t -> unit |