aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/cLexer.ml6
-rw-r--r--parsing/cLexer.mli2
-rw-r--r--parsing/g_constr.mlg8
-rw-r--r--parsing/g_prim.mlg27
-rw-r--r--parsing/pcoq.ml2
-rw-r--r--parsing/tok.ml16
-rw-r--r--parsing/tok.mli4
7 files changed, 34 insertions, 31 deletions
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index 6a436fbcb7..a39da96a53 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -723,7 +723,7 @@ let rec next_token ~diff_mode loc s =
let ep = Stream.count s in
IDENT id, set_loc_pos loc bp ep end
| Some ('0'..'9') ->
- let n = NumTok.parse s in
+ let n = NumTok.Unsigned.parse s in
let ep = Stream.count s in
comment_stop bp;
(NUMERAL n, set_loc_pos loc bp ep)
@@ -813,7 +813,7 @@ let token_text : type c. c Tok.p -> string = function
| PIDENT None -> "identifier"
| PIDENT (Some t) -> "'" ^ t ^ "'"
| PNUMERAL None -> "numeral"
- | PNUMERAL (Some n) -> "'" ^ NumTok.to_string n ^ "'"
+ | PNUMERAL (Some n) -> "'" ^ NumTok.Unsigned.sprint n ^ "'"
| PSTRING None -> "string"
| PSTRING (Some s) -> "STRING \"" ^ s ^ "\""
| PLEFTQMARK -> "LEFTQMARK"
@@ -888,6 +888,6 @@ let terminal s =
else PKEYWORD s
(* Precondition: the input is a numeral (c.f. [NumTok.t]) *)
-let terminal_numeral s = match NumTok.of_string s with
+let terminal_numeral s = match NumTok.Unsigned.parse_string s with
| Some n -> PNUMERAL (Some n)
| None -> failwith "numeral token expected."
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 3ce6981879..2c1284c4db 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -50,7 +50,7 @@ val check_keyword : string -> unit
val terminal : string -> string Tok.p
(** Precondition: the input is a numeral (c.f. [NumTok.t]) *)
-val terminal_numeral : string -> NumTok.t Tok.p
+val terminal_numeral : string -> NumTok.Unsigned.t Tok.p
(** The lexer of Coq: *)
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:
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 2bc1c11596..9c50109bb3 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -21,15 +21,18 @@ let _ = List.iter CLexer.add_keyword prim_kw
let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id
-let check_int loc = function
- | { NumTok.int = i; frac = ""; exp = "" } -> i
- | _ -> CErrors.user_err ~loc (Pp.str "This number is not an integer.")
-
-let my_int_of_string loc s =
+let my_int_of_string ?loc s =
try
int_of_string s
with Failure _ ->
- CErrors.user_err ~loc (Pp.str "This number is too large.")
+ CErrors.user_err ?loc (Pp.str "This number is too large.")
+
+let my_to_nat_string ?loc ispos s =
+ match NumTok.Unsigned.to_nat s with
+ | Some n -> n
+ | None ->
+ let pos = if ispos then "a natural" else "an integer" in
+ CErrors.user_err ?loc Pp.(str "This number is not " ++ str pos ++ str " number.")
let test_pipe_closedcurly =
let open Pcoq.Lookahead in
@@ -122,18 +125,18 @@ GRAMMAR EXTEND Gram
[ [ s = string -> { CAst.make ~loc s } ] ]
;
integer:
- [ [ i = bigint -> { my_int_of_string loc i } ] ]
+ [ [ i = bigint -> { my_int_of_string ~loc i } ] ]
;
natural:
- [ [ i = bignat -> { my_int_of_string loc i } ] ]
+ [ [ i = bignat -> { my_int_of_string ~loc i } ] ]
;
bigint:
- [ [ i = NUMERAL -> { check_int loc i }
- | test_minus_nat; "-"; i = NUMERAL -> { check_int loc i } ] ]
+ [ [ i = NUMERAL -> { my_to_nat_string true ~loc i }
+ | test_minus_nat; "-"; i = NUMERAL -> { "-" ^ my_to_nat_string ~loc false i } ] ]
;
bignat:
- [ [ i = NUMERAL -> { check_int loc i } ] ]
- ;
+ [ [ i = NUMERAL -> { my_to_nat_string ~loc true i } ] ]
+ ;
bar_cbrace:
[ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ]
;
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index fccd096d11..b3f997e1b3 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -166,7 +166,7 @@ struct
| _ -> None
let lk_nat tok n strm = match stream_nth n strm with
- | Tok.NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1)
+ | Tok.NUMERAL p when NumTok.Unsigned.is_nat p -> Some (n + 1)
| _ -> None
let rec lk_list lk_elem n strm =
diff --git a/parsing/tok.ml b/parsing/tok.ml
index ff4433f18c..b1ceab8822 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -17,7 +17,7 @@ type 'c p =
| PPATTERNIDENT : string option -> string p
| PIDENT : string option -> string p
| PFIELD : string option -> string p
- | PNUMERAL : NumTok.t option -> NumTok.t p
+ | PNUMERAL : NumTok.Unsigned.t option -> NumTok.Unsigned.t p
| PSTRING : string option -> string p
| PLEFTQMARK : unit p
| PBULLET : string option -> string p
@@ -31,7 +31,7 @@ let pattern_strings : type c. c p -> string * string option =
| PIDENT s -> "IDENT", s
| PFIELD s -> "FIELD", s
| PNUMERAL None -> "NUMERAL", None
- | PNUMERAL (Some n) -> "NUMERAL", Some (NumTok.to_string n)
+ | PNUMERAL (Some n) -> "NUMERAL", Some (NumTok.Unsigned.sprint n)
| PSTRING s -> "STRING", s
| PLEFTQMARK -> "LEFTQMARK", None
| PBULLET s -> "BULLET", s
@@ -43,7 +43,7 @@ type t =
| PATTERNIDENT of string
| IDENT of string
| FIELD of string
- | NUMERAL of NumTok.t
+ | NUMERAL of NumTok.Unsigned.t
| STRING of string
| LEFTQMARK
| BULLET of string
@@ -59,7 +59,7 @@ let equal_p (type a b) (t1 : a p) (t2 : b p) : (a, b) Util.eq option =
| PIDENT s1, PIDENT s2 when streq s1 s2 -> Some Util.Refl
| PFIELD s1, PFIELD s2 when streq s1 s2 -> Some Util.Refl
| PNUMERAL None, PNUMERAL None -> Some Util.Refl
- | PNUMERAL (Some n1), PNUMERAL (Some n2) when NumTok.equal n1 n2 -> Some Util.Refl
+ | PNUMERAL (Some n1), PNUMERAL (Some n2) when NumTok.Unsigned.equal n1 n2 -> Some Util.Refl
| PSTRING s1, PSTRING s2 when streq s1 s2 -> Some Util.Refl
| PLEFTQMARK, PLEFTQMARK -> Some Util.Refl
| PBULLET s1, PBULLET s2 when streq s1 s2 -> Some Util.Refl
@@ -73,7 +73,7 @@ let equal t1 t2 = match t1, t2 with
| PATTERNIDENT s1, PATTERNIDENT s2 -> string_equal s1 s2
| IDENT s1, IDENT s2 -> string_equal s1 s2
| FIELD s1, FIELD s2 -> string_equal s1 s2
-| NUMERAL n1, NUMERAL n2 -> NumTok.equal n1 n2
+| NUMERAL n1, NUMERAL n2 -> NumTok.Unsigned.equal n1 n2
| STRING s1, STRING s2 -> string_equal s1 s2
| LEFTQMARK, LEFTQMARK -> true
| BULLET s1, BULLET s2 -> string_equal s1 s2
@@ -100,7 +100,7 @@ let extract_string diff_mode = function
else s
| PATTERNIDENT s -> s
| FIELD s -> if diff_mode then "." ^ s else s
- | NUMERAL n -> NumTok.to_string n
+ | NUMERAL n -> NumTok.Unsigned.sprint n
| LEFTQMARK -> "?"
| BULLET s -> s
| QUOTATION(_,s) -> s
@@ -124,7 +124,7 @@ let match_pattern (type c) (p : c p) : t -> c =
let err () = raise Stream.Failure in
let seq = string_equal in
match p with
- | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMERAL n when seq s (NumTok.to_string n) -> s | _ -> err ())
+ | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMERAL n when seq s (NumTok.Unsigned.sprint n) -> s | _ -> err ())
| PIDENT None -> (function IDENT s' -> s' | _ -> err ())
| PIDENT (Some s) -> (function (IDENT s' | KEYWORD s') when seq s s' -> s' | _ -> err ())
| PPATTERNIDENT None -> (function PATTERNIDENT s -> s | _ -> err ())
@@ -132,7 +132,7 @@ let match_pattern (type c) (p : c p) : t -> c =
| PFIELD None -> (function FIELD s -> s | _ -> err ())
| PFIELD (Some s) -> (function FIELD s' when seq s s' -> s' | _ -> err ())
| PNUMERAL None -> (function NUMERAL s -> s | _ -> err ())
- | PNUMERAL (Some n) -> let s = NumTok.to_string n in (function NUMERAL n' when s = NumTok.to_string n' -> n' | _ -> err ())
+ | PNUMERAL (Some n) -> let s = NumTok.Unsigned.sprint n in (function NUMERAL n' when s = NumTok.Unsigned.sprint n' -> n' | _ -> err ())
| PSTRING None -> (function STRING s -> s | _ -> err ())
| PSTRING (Some s) -> (function STRING s' when seq s s' -> s' | _ -> err ())
| PLEFTQMARK -> (function LEFTQMARK -> () | _ -> err ())
diff --git a/parsing/tok.mli b/parsing/tok.mli
index 6d0691a746..b556194eb3 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -15,7 +15,7 @@ type 'c p =
| PPATTERNIDENT : string option -> string p
| PIDENT : string option -> string p
| PFIELD : string option -> string p
- | PNUMERAL : NumTok.t option -> NumTok.t p
+ | PNUMERAL : NumTok.Unsigned.t option -> NumTok.Unsigned.t p
| PSTRING : string option -> string p
| PLEFTQMARK : unit p
| PBULLET : string option -> string p
@@ -29,7 +29,7 @@ type t =
| PATTERNIDENT of string
| IDENT of string
| FIELD of string
- | NUMERAL of NumTok.t
+ | NUMERAL of NumTok.Unsigned.t
| STRING of string
| LEFTQMARK
| BULLET of string
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:03:52 +0000