diff options
Diffstat (limited to 'parsing/tok.ml')
| -rw-r--r-- | parsing/tok.ml | 27 |
1 files changed, 24 insertions, 3 deletions
diff --git a/parsing/tok.ml b/parsing/tok.ml index 5b9aed6d..efd57968 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -17,8 +17,22 @@ type t = | INT of string | STRING of string | LEFTQMARK + | BULLET of string | EOI +let equal t1 t2 = match t1, t2 with +| 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 +| LEFTQMARK, LEFTQMARK -> true +| BULLET s1, BULLET s2 -> CString.equal s1 s2 +| EOI, EOI -> true +| _ -> false + let extract_string = function | KEYWORD s -> s | IDENT s -> s @@ -28,6 +42,7 @@ let extract_string = function | FIELD s -> s | INT s -> s | LEFTQMARK -> "?" + | BULLET s -> s | EOI -> "" let to_string = function @@ -39,13 +54,16 @@ let to_string = function | INT s -> Format.sprintf "INT %s" s | STRING s -> Format.sprintf "STRING %S" s | LEFTQMARK -> "LEFTQMARK" + | BULLET s -> Format.sprintf "STRING %S" s | EOI -> "EOI" let match_keyword kwd = function | KEYWORD kwd' when kwd = kwd' -> true | _ -> false -let print ppf tok = Format.fprintf ppf "%s" (to_string tok) +(* Needed to fix Camlp4 signature. + Cannot use Pp because of silly Tox -> Compat -> Pp dependency *) +let print ppf tok = Format.pp_print_string ppf (to_string tok) (** For camlp5, conversion from/to [Plexing.pattern], and a match function analoguous to [Plexing.default_match] *) @@ -59,6 +77,7 @@ let of_pattern = function | "INT", s -> INT s | "STRING", s -> STRING s | "LEFTQMARK", _ -> LEFTQMARK + | "BULLET", s -> BULLET s | "EOI", _ -> EOI | _ -> failwith "Tok.of_pattern: not a constructor" @@ -71,6 +90,7 @@ let to_pattern = function | INT s -> "INT", s | STRING s -> "STRING", s | LEFTQMARK -> "LEFTQMARK", "" + | BULLET s -> "BULLET", s | EOI -> "EOI", "" let match_pattern = @@ -84,7 +104,8 @@ let match_pattern = | "INT", "" -> (function INT s -> s | _ -> err ()) | "STRING", "" -> (function STRING s -> s | _ -> err ()) | "LEFTQMARK", "" -> (function LEFTQMARK -> "" | _ -> err ()) + | "BULLET", "" -> (function BULLET s -> s | _ -> err ()) | "EOI", "" -> (function EOI -> "" | _ -> err ()) | pat -> let tok = of_pattern pat in - function tok' -> if tok = tok' then snd pat else err () + function tok' -> if equal tok tok' then snd pat else err () |