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 /parsing/g_constr.mlg | |
| 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 'parsing/g_constr.mlg')
| -rw-r--r-- | parsing/g_constr.mlg | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 3fd756e748..963f029766 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -174,7 +174,7 @@ GRAMMAR EXTEND Gram { (* Preserve parentheses around numerals so that constrintern does not collapse -(3) into the numeral -3. *) (match c.CAst.v with - | CPrim (Numeral (SPlus,n)) -> + | CPrim (Numeral (NumTok.SPlus,n)) -> CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"( _ )"),([c],[],[],[])) | _ -> c) } | "{|"; c = record_declaration; bar_cbrace -> { c } @@ -248,7 +248,7 @@ GRAMMAR EXTEND Gram atomic_constr: [ [ g = global; i = univ_instance -> { CAst.make ~loc @@ CRef (g,i) } | s = sort -> { CAst.make ~loc @@ CSort s } - | n = NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (SPlus,n)) } + | n = NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPrim (String s) } | "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } | "?"; "["; id = ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id, None) } @@ -355,12 +355,12 @@ GRAMMAR EXTEND Gram { (* Preserve parentheses around numerals so that constrintern does not collapse -(3) into the numeral -3. *) match p.CAst.v with - | CPatPrim (Numeral (SPlus,n)) -> + | CPatPrim (Numeral (NumTok.SPlus,n)) -> CAst.make ~loc @@ CPatNotation(None,(InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) | _ -> p } | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" -> { CAst.make ~loc @@ CPatOr (p::pl) } - | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) } + | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (NumTok.SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ] ; fixannot: |