summaryrefslogtreecommitdiff
path: root/src/lacweb.lex
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-07-01 10:55:38 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-07-01 10:55:38 -0400
commit43116f69ce9330eb09d42a25d4afc746e7c3f3ef (patch)
treee57ed0ff271cf35d5dbf88ecb90ce150a877e454 /src/lacweb.lex
parentcc2b6499cd2ea61f8882419cc5915c3428d5f5b7 (diff)
Initial disjointness prover
Diffstat (limited to 'src/lacweb.lex')
-rw-r--r--src/lacweb.lex2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 038e591f..45e2f1f2 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -120,6 +120,7 @@ realconst = [0-9]+\.[0-9]*;
str := #"\n" :: !str; continue());
<STRING> . => (str := String.sub (yytext, 0) :: !str; continue());
+<INITIAL> "()" => (Tokens.UNIT (pos yypos, pos yypos + size yytext));
<INITIAL> "(" => (Tokens.LPAREN (pos yypos, pos yypos + size yytext));
<INITIAL> ")" => (Tokens.RPAREN (pos yypos, pos yypos + size yytext));
<INITIAL> "[" => (Tokens.LBRACK (pos yypos, pos yypos + size yytext));
@@ -161,6 +162,7 @@ realconst = [0-9]+\.[0-9]*;
<INITIAL> "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext));
<INITIAL> "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext));
+<INITIAL> "Unit" => (Tokens.KUNIT (pos yypos, pos yypos + size yytext));
<INITIAL> {id} => (Tokens.SYMBOL (yytext, pos yypos, pos yypos + size yytext));
<INITIAL> {cid} => (Tokens.CSYMBOL (yytext, pos yypos, pos yypos + size yytext));