summaryrefslogtreecommitdiff
path: root/parsing/tok.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/tok.ml')
-rw-r--r--parsing/tok.ml90
1 files changed, 90 insertions, 0 deletions
diff --git a/parsing/tok.ml b/parsing/tok.ml
new file mode 100644
index 00000000..bd7645c2
--- /dev/null
+++ b/parsing/tok.ml
@@ -0,0 +1,90 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** The type of token for the Coq lexer and parser *)
+
+type t =
+ | KEYWORD of string
+ | METAIDENT of string
+ | PATTERNIDENT of string
+ | IDENT of string
+ | FIELD of string
+ | INT of string
+ | STRING of string
+ | LEFTQMARK
+ | EOI
+
+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
+ | LEFTQMARK -> "?"
+ | EOI -> ""
+
+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"
+ | 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)
+
+(** For camlp5, conversion from/to [Plexing.pattern],
+ and a match function analoguous to [Plexing.default_match] *)
+
+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
+ | "STRING", s -> STRING s
+ | "LEFTQMARK", _ -> LEFTQMARK
+ | "EOI", _ -> EOI
+ | _ -> failwith "Tok.of_pattern: not a constructor"
+
+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
+ | STRING s -> "STRING", s
+ | LEFTQMARK -> "LEFTQMARK", ""
+ | EOI -> "EOI", ""
+
+let match_pattern =
+ let err () = raise Stream.Failure in
+ 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 ())
+ | "STRING", "" -> (function STRING s -> s | _ -> err ())
+ | "LEFTQMARK", "" -> (function LEFTQMARK -> "" | _ -> err ())
+ | "EOI", "" -> (function EOI -> "" | _ -> err ())
+ | pat ->
+ let tok = of_pattern pat in
+ function tok' -> if tok = tok' then snd pat else err ()