diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-07-03 19:53:33 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-03 20:47:29 +0200 |
commit | 2b6dd2ff132a74ba247609191c344dda991e3b84 (patch) | |
tree | cbe1a8e7c01558bb0ef0b4cdc06ab926992e953c | |
parent | 4349cd9fea36fafb857b117865a5edf8ae1e3b08 (diff) |
Remove lexing of ordinal notations.
This was implemented in anticipation of a part of PR#164 that we decided not to
merge.
-rw-r--r-- | parsing/cLexer.ml4 | 52 | ||||
-rw-r--r-- | parsing/compat.ml4 | 1 | ||||
-rw-r--r-- | parsing/g_prim.ml4 | 5 | ||||
-rw-r--r-- | parsing/pcoq.ml | 1 | ||||
-rw-r--r-- | parsing/pcoq.mli | 1 | ||||
-rw-r--r-- | parsing/tok.ml | 7 | ||||
-rw-r--r-- | parsing/tok.mli | 1 |
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 |