module Language.Boogie.Tokens where
import Language.Boogie.AST
import Data.Maybe
keywords :: [String]
keywords = ["assert", "assume", "axiom", "bool", "break", "call", "complete", "const",
"else", "div", "ensures", "exists", "extends", "false", "forall", "free", "function",
"goto", "havoc", "if", "implementation", "int", "invariant", "lambda", "mod", "modifies",
"old", "procedure", "requires", "return", "returns", "then", "true", "type", "unique",
"var", "where", "while"]
opName op table = fromJust (lookup op table)
unOpTokens :: [(UnOp, String)]
unOpTokens = [(Neg, "-"),
(Not, "!")]
binOpTokens :: [(BinOp, String)]
binOpTokens = [(Plus, "+"),
(Minus, "-"),
(Times, "*"),
(Div, "div"),
(Mod, "mod"),
(And, "&&"),
(Or, "||"),
(Implies, "==>"),
(Explies, "<=="),
(Equiv, "<==>"),
(Eq, "=="),
(Neq, "!="),
(Lc, "<:"),
(Ls, "<"),
(Leq, "<="),
(Gt, ">"),
(Geq, ">=")]
qOpTokens :: [(QOp, String)]
qOpTokens = [ (Forall, "forall"),
(Exists, "exists"),
(Lambda, "lambda") ]
otherOps :: [String]
otherOps = [":", ";", "::", ":=", "="]
identifierChars = "_.$#\'`~^\\?"
commentStart = "/*"
commentEnd = "*/"
commentLine = "//"
nonIdChar = '*'