{ open Lexing open Ast open Parser let kwd_table = Hashtbl.create 10 let () = List.iter (fun (a, b) -> Hashtbl.add kwd_table a b) [ "bool", BOOL; "int", INT; "real", REAL; "const", CONST; "node", NODE; "returns", RETURNS; "var", VAR; "let", LET; "tel", TEL; "if", IF; "then", THEN; "else", ELSE; "pre", PRE; "not", NOT; "and", AND; "or", OR; "mod", MOD; "automaton", AUTOMATON; "state", STATE; "initial", INITIAL; "unless", UNLESS; "until", UNTIL; "resume", RESUME; "true", TRUE; "false", FALSE; "assume", ASSUME; "guarantee", GUARANTEE; "probe", PROBE; ] } let space = [' ' '\t' '\r']+ let newline = "\n" | "\r" | "\r\n" let digit = ['0'-'9'] let digit_ = ['0'-'9' '_'] let int_dec = digit digit_* let int_bin = ("0b" | "0B") ['0'-'1'] ['0'-'1' '_']* let int_oct = ("0o" | "0O") ['0'-'7'] ['0'-'7' '_']* let int_hex = ("0x" | "0X") ['0'-'9' 'a'-'f' 'A'-'F'] ['0'-'9' 'a'-'f' 'A'-'F' '_']* let const_int = int_bin | int_oct | int_dec | int_hex let const_real = digit_+ '.' digit* rule token = parse (* identifier (TOK_id) or reserved keyword *) | ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']* as id { try Hashtbl.find kwd_table id with Not_found -> IDENT id } (* symbols *) | "(" { LPAREN } | ")" { RPAREN } | "{" { LCURLY } | "}" { RCURLY } | "*" { STAR } | "+" { PLUS } | "-" { MINUS } | "/" { DIVIDE } | "<" { LESS } | ">" { GREATER } | "<=" { LESS_EQUAL } | ">=" { GREATER_EQUAL } | "<>" { DIFF } | "=" { EQUAL } | ";" { SEMICOLON } | ":" { COLON } | "," { COMMA } | "->" { ARROW } (* literals *) | const_int as c { INTVAL c } | const_real as c { REALVAL c } (* spaces, comments *) | "(*" { comment lexbuf; token lexbuf } | "--" [^ '\n' '\r']* { token lexbuf } | newline { new_line lexbuf; token lexbuf } | space { token lexbuf } (* end of files *) | eof { EOF } and comment = parse | "*)" { () } | [^ '\n' '\r'] { comment lexbuf } | newline { new_line lexbuf; comment lexbuf }