aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/cLexer.ml452
-rw-r--r--parsing/compat.ml41
-rw-r--r--parsing/g_prim.ml45
-rw-r--r--parsing/pcoq.ml1
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--parsing/tok.ml7
-rw-r--r--parsing/tok.mli1
7 files changed, 7 insertions, 61 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 711d2240b..2acccfdf5 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -81,7 +81,6 @@ module Error = struct
| Undefined_token
| Bad_token of string
| UnsupportedUnicode of int
- | IncorrectIndex of char list
exception E of t
@@ -94,16 +93,7 @@ module Error = struct
| Undefined_token -> "Undefined token"
| Bad_token tok -> Format.sprintf "Bad token %S" tok
| UnsupportedUnicode x ->
- Printf.sprintf "Unsupported Unicode character (0x%x)" x
- | IncorrectIndex l ->
- let l = List.map (fun c -> Char.code c - 48) l in
- let s = match l with
- | c::d::l ->
- let l = List.map string_of_int (List.rev l) in
- String.concat "" l ^ CString.ordinal (10 * d + c)
- | [c] -> CString.ordinal c
- | [] -> assert false in
- Printf.sprintf "%s expected" s)
+ Printf.sprintf "Unsupported Unicode character (0x%x)" x)
(* Require to fix the Camlp4 signature *)
let print ppf x = Pp.pp_with ppf (Pp.str (to_string x))
@@ -286,39 +276,9 @@ let rec ident_tail loc len = parser
ident_tail loc (nstore n len s) s
| _ -> len
-let check_no_char s =
- match Stream.npeek 3 s with
- | [_;_;('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_')] -> false
- | [_;_;_] -> true
- | [_;_] -> true
- | _ -> assert false
-
-let is_teen = function
- | _::'1'::l -> true
- | _ -> false
-
-let is_gt3 = function
- | c::_ when c == '1' || c == '2' || c == '3' -> false
- | _ -> true
-
-let check_gt3 loc l len =
- if not (l == ['0']) && (is_teen l || is_gt3 l) then (false, len)
- else err loc (IncorrectIndex l)
-
-let check_n loc n l len =
- if List.hd l == n && not (is_teen l) then (false, len)
- else err loc (IncorrectIndex l)
-
-let rec number_or_index loc bp l len = parser
- | [< ' ('0'..'9' as c); s >] -> number_or_index loc bp (c::l) (store len c) s
- | [< s >] ep ->
- let loc = set_loc_pos loc bp ep in
- match Stream.npeek 2 s with
- | ['s';'t'] when check_no_char s -> njunk 2 s; check_n loc '1' l len
- | ['n';'d'] when check_no_char s -> njunk 2 s; check_n loc '2' l len
- | ['r';'d'] when check_no_char s -> njunk 2 s; check_n loc '3' l len
- | ['t';'h'] when check_no_char s -> njunk 2 s; check_gt3 loc l len
- | _ -> true, len
+let rec number len = parser
+ | [< ' ('0'..'9' as c); s >] -> number (store len c) s
+ | [< >] -> len
let warn_comment_terminator_in_string =
CWarnings.create ~name:"comment-terminator-in-string" ~category:"parsing"
@@ -603,9 +563,9 @@ let rec next_token loc = parser bp
let id = get_buff len in
comment_stop bp;
(try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
- | [< ' ('0'..'9' as c); (b,len) = number_or_index loc bp [c] (store 0 c) >] ep ->
+ | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
comment_stop bp;
- (if b then INT (get_buff len) else INDEX (get_buff len)), set_loc_pos loc bp ep
+ (INT (get_buff len), set_loc_pos loc bp ep)
| [< ''\"'; (loc,len) = string loc None bp 0 >] ep ->
comment_stop bp;
(STRING (get_buff len), set_loc_pos loc bp ep)
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index ef651f810..18bc8d664 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -257,7 +257,6 @@ IFDEF CAMLP5 THEN
| Tok.PATTERNIDENT s -> "PATTERNIDENT", s
| Tok.FIELD s -> "FIELD", s
| Tok.INT s -> "INT", s
- | Tok.INDEX s -> "INDEX", s
| Tok.STRING s -> "STRING", s
| Tok.LEFTQMARK -> "LEFTQMARK", ""
| Tok.BULLET s -> "BULLET", s
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 85eb5f5cd..b90e06cd3 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -32,7 +32,7 @@ let my_int_of_string loc s =
GEXTEND Gram
GLOBAL:
- bigint natural index integer identref name ident var preident
+ bigint natural integer identref name ident var preident
fullyqualid qualid reference dirpath ne_lstring
ne_string string pattern_ident pattern_identref by_notation smart_global;
preident:
@@ -113,9 +113,6 @@ GEXTEND Gram
natural:
[ [ i = INT -> my_int_of_string (!@loc) i ] ]
;
- index:
- [ [ i = INDEX -> my_int_of_string (!@loc) i ] ]
- ;
bigint: (* Negative numbers are dealt with specially *)
[ [ i = INT -> (Bigint.of_string i) ] ]
;
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index ab55b3d78..0e74e6f0c 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -264,7 +264,6 @@ module Prim =
let preident = gec_gen "preident"
let ident = gec_gen "ident"
let natural = gec_gen "natural"
- let index = gec_gen "index"
let integer = gec_gen "integer"
let bigint = Gram.entry_create "Prim.bigint"
let string = gec_gen "string"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 008374e09..635b0170a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -134,7 +134,6 @@ module Prim :
val pattern_identref : Id.t located Gram.entry
val base_ident : Id.t Gram.entry
val natural : int Gram.entry
- val index : int Gram.entry
val bigint : Bigint.bigint Gram.entry
val integer : int Gram.entry
val string : string Gram.entry
diff --git a/parsing/tok.ml b/parsing/tok.ml
index df7e7c2a6..8ae106512 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -16,7 +16,6 @@ type t =
| IDENT of string
| FIELD of string
| INT of string
- | INDEX of string
| STRING of string
| LEFTQMARK
| BULLET of string
@@ -29,7 +28,6 @@ let equal t1 t2 = match t1, t2 with
| IDENT s1, IDENT s2 -> string_equal s1 s2
| FIELD s1, FIELD s2 -> string_equal s1 s2
| INT s1, INT s2 -> string_equal s1 s2
-| INDEX s1, INDEX s2 -> string_equal s1 s2
| STRING s1, STRING s2 -> string_equal s1 s2
| LEFTQMARK, LEFTQMARK -> true
| BULLET s1, BULLET s2 -> string_equal s1 s2
@@ -43,7 +41,6 @@ let extract_string = function
| PATTERNIDENT s -> s
| FIELD s -> s
| INT s -> s
- | INDEX s -> s
| LEFTQMARK -> "?"
| BULLET s -> s
| EOI -> ""
@@ -54,7 +51,6 @@ let to_string = function
| PATTERNIDENT s -> Format.sprintf "PATTERNIDENT %S" s
| FIELD s -> Format.sprintf "FIELD %S" s
| INT s -> Format.sprintf "INT %s" s
- | INDEX s -> Format.sprintf "INDEX %s" s
| STRING s -> Format.sprintf "STRING %S" s
| LEFTQMARK -> "LEFTQMARK"
| BULLET s -> Format.sprintf "STRING %S" s
@@ -77,7 +73,6 @@ let of_pattern = function
| "PATTERNIDENT", s -> PATTERNIDENT s
| "FIELD", s -> FIELD s
| "INT", s -> INT s
- | "INDEX", s -> INDEX s
| "STRING", s -> STRING s
| "LEFTQMARK", _ -> LEFTQMARK
| "BULLET", s -> BULLET s
@@ -90,7 +85,6 @@ let to_pattern = function
| PATTERNIDENT s -> "PATTERNIDENT", s
| FIELD s -> "FIELD", s
| INT s -> "INT", s
- | INDEX s -> "INDEX", s
| STRING s -> "STRING", s
| LEFTQMARK -> "LEFTQMARK", ""
| BULLET s -> "BULLET", s
@@ -104,7 +98,6 @@ let match_pattern =
| "PATTERNIDENT", "" -> (function PATTERNIDENT s -> s | _ -> err ())
| "FIELD", "" -> (function FIELD s -> s | _ -> err ())
| "INT", "" -> (function INT s -> s | _ -> err ())
- | "INDEX", "" -> (function INDEX s -> s | _ -> err ())
| "STRING", "" -> (function STRING s -> s | _ -> err ())
| "LEFTQMARK", "" -> (function LEFTQMARK -> "" | _ -> err ())
| "BULLET", "" -> (function BULLET s -> s | _ -> err ())
diff --git a/parsing/tok.mli b/parsing/tok.mli
index 54b747952..b9286c53e 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -14,7 +14,6 @@ type t =
| IDENT of string
| FIELD of string
| INT of string
- | INDEX of string
| STRING of string
| LEFTQMARK
| BULLET of string
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 14:14:41 +0000