path: root/frontend/lexer.mll

{
  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 }