diff options
Diffstat (limited to 'parsing/tok.ml')
| -rw-r--r-- | parsing/tok.ml | 27 |
1 files changed, 11 insertions, 16 deletions
diff --git a/parsing/tok.ml b/parsing/tok.ml index c96b53de..f4b60aee 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -8,9 +8,10 @@ (** The type of token for the Coq lexer and parser *) +let string_equal (s1 : string) s2 = s1 = s2 + type t = | KEYWORD of string - | METAIDENT of string | PATTERNIDENT of string | IDENT of string | FIELD of string @@ -21,16 +22,15 @@ type t = | EOI let equal t1 t2 = match t1, t2 with -| IDENT s1, KEYWORD s2 -> CString.equal s1 s2 -| KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2 -| METAIDENT s1, METAIDENT s2 -> CString.equal s1 s2 -| PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2 -| IDENT s1, IDENT s2 -> CString.equal s1 s2 -| FIELD s1, FIELD s2 -> CString.equal s1 s2 -| INT s1, INT s2 -> CString.equal s1 s2 -| STRING s1, STRING s2 -> CString.equal s1 s2 +| IDENT s1, KEYWORD s2 -> string_equal s1 s2 +| KEYWORD s1, KEYWORD s2 -> string_equal s1 s2 +| PATTERNIDENT s1, PATTERNIDENT s2 -> string_equal s1 s2 +| IDENT s1, IDENT s2 -> string_equal s1 s2 +| FIELD s1, FIELD s2 -> string_equal s1 s2 +| INT s1, INT s2 -> string_equal s1 s2 +| STRING s1, STRING s2 -> string_equal s1 s2 | LEFTQMARK, LEFTQMARK -> true -| BULLET s1, BULLET s2 -> CString.equal s1 s2 +| BULLET s1, BULLET s2 -> string_equal s1 s2 | EOI, EOI -> true | _ -> false @@ -38,7 +38,6 @@ let extract_string = function | KEYWORD s -> s | IDENT s -> s | STRING s -> s - | METAIDENT s -> s | PATTERNIDENT s -> s | FIELD s -> s | INT s -> s @@ -49,13 +48,12 @@ let extract_string = function let to_string = function | KEYWORD s -> Format.sprintf "%S" s | IDENT s -> Format.sprintf "IDENT %S" s - | METAIDENT s -> Format.sprintf "METAIDENT %S" s | PATTERNIDENT s -> Format.sprintf "PATTERNIDENT %S" s | FIELD s -> Format.sprintf "FIELD %S" s | INT s -> Format.sprintf "INT %s" s | STRING s -> Format.sprintf "STRING %S" s | LEFTQMARK -> "LEFTQMARK" - | BULLET s -> Format.sprintf "STRING %S" s + | BULLET s -> Format.sprintf "BULLET %S" s | EOI -> "EOI" let match_keyword kwd = function @@ -72,7 +70,6 @@ let print ppf tok = Format.pp_print_string ppf (to_string tok) let of_pattern = function | "", s -> KEYWORD s | "IDENT", s -> IDENT s - | "METAIDENT", s -> METAIDENT s | "PATTERNIDENT", s -> PATTERNIDENT s | "FIELD", s -> FIELD s | "INT", s -> INT s @@ -85,7 +82,6 @@ let of_pattern = function let to_pattern = function | KEYWORD s -> "", s | IDENT s -> "IDENT", s - | METAIDENT s -> "METAIDENT", s | PATTERNIDENT s -> "PATTERNIDENT", s | FIELD s -> "FIELD", s | INT s -> "INT", s @@ -99,7 +95,6 @@ let match_pattern = function | "", "" -> (function KEYWORD s -> s | _ -> err ()) | "IDENT", "" -> (function IDENT s -> s | _ -> err ()) - | "METAIDENT", "" -> (function METAIDENT s -> s | _ -> err ()) | "PATTERNIDENT", "" -> (function PATTERNIDENT s -> s | _ -> err ()) | "FIELD", "" -> (function FIELD s -> s | _ -> err ()) | "INT", "" -> (function INT s -> s | _ -> err ()) |