diff options
| author | Hugo Herbelin | 2020-01-31 01:04:07 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-22 15:02:43 +0100 |
| commit | 2a31e23df8ff0ab67a09008858fa49e77e5f4332 (patch) | |
| tree | 30e6e02d0740a87f7d9325cce87266d329990baa /parsing | |
| parent | 7ba059507b67b1f6ea3566a5d1dee40f6af78316 (diff) | |
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.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_prim.mlg | 13 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
3 files changed, 10 insertions, 5 deletions
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index e8e802f606..2bc1c11596 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -47,7 +47,7 @@ let test_minus_nat = GRAMMAR EXTEND Gram GLOBAL: - bigint natural integer identref name ident var preident + bignat bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath ne_lstring ne_string string lstring pattern_ident pattern_identref by_notation smart_global bar_cbrace; @@ -122,13 +122,16 @@ GRAMMAR EXTEND Gram [ [ s = string -> { CAst.make ~loc s } ] ] ; integer: - [ [ i = NUMERAL -> { my_int_of_string loc (check_int loc i) } - | test_minus_nat; "-"; i = NUMERAL -> { - my_int_of_string loc (check_int loc i) } ] ] + [ [ i = bigint -> { my_int_of_string loc i } ] ] ; natural: - [ [ i = NUMERAL -> { my_int_of_string loc (check_int loc i) } ] ] + [ [ i = bignat -> { my_int_of_string loc i } ] ] ; - bigint: (* Negative numbers are dealt with elsewhere *) + bigint: + [ [ i = NUMERAL -> { check_int loc i } + | test_minus_nat; "-"; i = NUMERAL -> { check_int loc i } ] ] + ; + bignat: [ [ i = NUMERAL -> { check_int loc i } ] ] ; bar_cbrace: diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index fe2412fcd7..fccd096d11 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -462,6 +462,7 @@ module Prim = let ident = gec_gen "ident" let natural = gec_gen "natural" let integer = gec_gen "integer" + let bignat = Entry.create "Prim.bignat" let bigint = Entry.create "Prim.bigint" let string = gec_gen "string" let lstring = Entry.create "Prim.lstring" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index cd97ea20fa..87c7f168ce 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -171,6 +171,7 @@ module Prim : val pattern_ident : Id.t Entry.t val pattern_identref : lident Entry.t val base_ident : Id.t Entry.t + val bignat : string Entry.t val natural : int Entry.t val bigint : string Entry.t val integer : int Entry.t |