{
module Lexer
open System
open Parser
open Microsoft.FSharp.Text.Lexing

let lexeme lexbuf =
    LexBuffer<char>.LexemeString lexbuf
}

// These are some regular expression definitions
let digit = ['0'-'9']
let nondigit = [ 'a'-'z' 'A'-'Z' '_' ]
let idchar = (nondigit | digit)
let whitespace = [' ' '\t' ]
let newline = ('\n' | '\r' '\n')

rule tokenize = parse
| whitespace  { tokenize lexbuf }
| newline     { lexbuf.EndPos <- lexbuf.EndPos.NextLine; tokenize lexbuf }
// TODO:  | "//"[-newline]* { tokenize lexbuf }
// keywords
| "interface"    { INTERFACE }
| "datamodel"    { DATAMODEL }
| "code"         { CODE }
| "var"          { VAR }
| "constructor"  { CONSTRUCTOR }
| "method"       { METHOD }
| "frame"        { FRAME }
| "invariant"    { INVARIANT }
| "returns"      { RETURNS }
| "requires"     { REQUIRES }
| "ensures"      { ENSURES }
| "forall"       { FORALL }
// Types
| "int"          { INTTYPE }
| "bool"         { BOOLTYPE }
| "seq"          { SEQTYPE }
| "set"          { SETTYPE }
// Operators
| "..."    { DOTDOTDOT }
| ".."     { DOTDOT }
| "."      { DOT }
| "old"    { OLD }
| "+"      { PLUS }
| "-"      { MINUS }
| "*"      { STAR }
| "div"    { DIV }
| "mod"    { MOD }
| "&&"     { AND }
| "||"     { OR }
| "!"      { NOT }
| "==>"    { IMPLIES }
| "<==>"   { IFF }
| "<"      { LESS }
| "<="     { ATMOST }
| "="      { EQ }
| "!="     { NEQ }
| ">="     { ATLEAST }
| ">"      { GREATER }
| "in"     { IN }
| "!in"    { NOTIN }
// Misc
| ":="     { GETS }
| "("      { LPAREN }
| ")"      { RPAREN }
| "["      { LBRACKET }
| "]"      { RBRACKET }
| "{"      { LCURLY }
| "}"      { RCURLY }
| "|"      { VERTBAR }
| ":"      { COLON }
| "::"     { COLONCOLON }
| ","      { COMMA }
| "?"      { QMARK }
// Numberic constants
| digit+        { INTEGER (System.Convert.ToInt32(lexeme lexbuf)) }
// identifiers
| idchar+       { ID (LexBuffer<char>.LexemeString lexbuf) }
// EOF
| eof   { EOF }
| _ { printfn "Unrecognized input character: %s" (lexeme lexbuf) ; EOF }