module Bpl

IDENTIFIER = /[a-zA-Z_.$\#'`~^\\?][\w.$\#'`~^\\?]*/

end

class BoogieLanguage macro

BLANK     \s
MLC_OPEN    \/\*
MLC_CLOSE   \*\/
SLC         \/\/
ID_INIT   [a-zA-Z_.$\#'`~^\\?]
ID_CHAR   [\w.$\#'`~^\\?]
IDENT     {ID_INIT}{ID_CHAR}*
OPERATOR  <==>|==>|\|\||&&|==|!=|<:|<=|<|>=|>|\+\+|\+|-|\*|\/|{:|:=|::|:|\|
KEYWORD   \b(assert|assume|axiom|bool|break|bv(\d+)|call|complete|const|else|ensures|exists|false|finite|forall|free|function|goto|havoc|if|implementation|int|invariant|modifies|old|procedure|requires|return|returns|then|true|type|unique|var|where|while)\b

rule

\$\$PARSE_DECL\$\$    { [:PARSE_DECL, ""] }
\$\$PARSE_PARAM\$\$   { [:PARSE_PARAM, ""] }
\$\$PARSE_SPEC\$\$    { [:PARSE_SPEC, ""] }
\$\$PARSE_BLOCKS\$\$  { [:PARSE_BLOCKS, ""] }
\$\$PARSE_STMT\$\$    { [:PARSE_STMT, ""] }
\$\$PARSE_EXPR\$\$    { [:PARSE_EXPR, ""] }
\$\$PARSE_TYPE\$\$    { [:PARSE_TYPE, ""] }

{MLC_OPEN}((?!{MLC_CLOSE})(.|\n))*{MLC_CLOSE}
{SLC}.*(?=\n)

\"[^"]*\"         { [:STRING, text[1..-2]]}

{BLANK}

{OPERATOR}        { [text, text] }

\d+bv\d+          { [:BITVECTOR, {value: text[/(\d+)bv/,1].to_i, base: text[/bv(\d+)/,1].to_i}] }
\d+               { [:NUMBER, text.to_i] }
bv\d+\b           { [:BVTYPE, text[2..-1].to_i] }

{KEYWORD}(?!{ID_CHAR}) { [text, Token.new(lineno)] }

{IDENT}           { [:IDENTIFIER, text] }
.                 { [text, text] }

end