diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 20:08:44 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-28 00:39:25 +0200 |
| commit | faaa2848c37444f8f37ac432c25f9f813e1df39b (patch) | |
| tree | 2672d165fd13b5262005406d1496bc6a14e8b521 /src/verit/veritLexer.mll | |
| parent | 7940ef63c654be26b41ce20162207f3c67d0b10a (diff) | |
| download | smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip | |
Adding support for lemmas in the command verit
Diffstat (limited to 'src/verit/veritLexer.mll')
| -rw-r--r-- | src/verit/veritLexer.mll | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/verit/veritLexer.mll b/src/verit/veritLexer.mll index 2a51a02..80fcc39 100644 --- a/src/verit/veritLexer.mll +++ b/src/verit/veritLexer.mll @@ -55,6 +55,7 @@ "dl_disequality", DLDE; "la_disequality", LADE; "forall_inst", FINS; + "forall", FORALL; "exists_inst", EINS; "skolem_ex_ax", SKEA; "skolem_all_ax", SKAA; @@ -105,6 +106,7 @@ let alpha = [ 'a'-'z' 'A' - 'Z' ] let blank = [' ' '\t'] let newline = ['\n' '\r'] let var = alpha (alpha|digit|'_')* +let atvar = '@' var let bindvar = '?' var+ let int = '-'? digit+ @@ -136,7 +138,9 @@ rule token = parse | "distinct" { DIST } | "Formula is Satisfiable" { SAT } - + | "Tindex_" (int as i) { TINDEX (int_of_string i) } + | "Int" { TINT } + | "Bool" { TBOOL } | int { try INT (int_of_string (Lexing.lexeme lexbuf)) with _ -> BIGINT @@ -147,4 +151,6 @@ rule token = parse | Not_found -> VAR v } | bindvar { BINDVAR (Lexing.lexeme lexbuf) } + | atvar { ATVAR (Lexing.lexeme lexbuf) } + | eof { raise Eof } |