aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/deLexer.ml
diff options
context:
space:
mode:
authorJacques-Henri Jourdan <jacques-henri.jourdan@inria.fr>2015-11-07 18:17:59 +0100
committerJacques-Henri Jourdan <jacques-henri.jourdan@inria.fr>2015-11-07 18:18:24 +0100
commit331501399291aff5a9cfcf1963b89ad2300a436e (patch)
treebca979d1ee54dfad060fa25147681f7ff35c42a0 /cparser/deLexer.ml
parent99761d109a799f6ca62471058463b5713f37eddc (diff)
downloadcompcert-kvx-331501399291aff5a9cfcf1963b89ad2300a436e.tar.gz
compcert-kvx-331501399291aff5a9cfcf1963b89ad2300a436e.zip
Updating deLexer to PRE_NAME tokens
Diffstat (limited to 'cparser/deLexer.ml')
-rw-r--r--cparser/deLexer.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/cparser/deLexer.ml b/cparser/deLexer.ml
index 00308e4b..3aa168da 100644
--- a/cparser/deLexer.ml
+++ b/cparser/deLexer.ml
@@ -65,6 +65,7 @@ let delex (symbol : string) : string =
| "WHILE" -> "while"
| "TYPEDEF_NAME" -> "t" (* this should be a type name *)
| "VAR_NAME" -> "x" (* this should be a variable name *)
+ | "PRE_NAME" -> ""
| "CONSTANT" -> "42"
| "STRING_LITERAL" -> "\"\""
| "ELLIPSIS" -> "..."
@@ -121,6 +122,8 @@ let delex (symbol : string) : string =
let delex sentence =
let symbols = Str.split (Str.regexp " ") sentence in
+ if List.nth symbols (List.length symbols - 1) = "PRE_NAME" then
+ failwith "token sequence terminating with PRE_NAME";
let symbols = List.map delex symbols in
List.iter (fun symbol ->
Printf.printf "%s " symbol