{
  open Parser
  exception Unexpected_char of string
  exception End_of_file_looking_for_double_quotes

  let chars_read = ref ""
  let add_char c = chars_read := Printf.sprintf "%s%c" !chars_read c

  let flush () = chars_read := ""
}

let id = [ 'a'-'z' '_' '0'-'9' ] ['a'-'z' 'A'-'Z' '_' '0'-'9']*

rule token = parse
    | [ ' ' '\t' ] { token lexbuf }
    | '\n' { Lexing.new_line lexbuf; token lexbuf }
    (* The several meanings of "." are disambiguated at lexing *)
    | '.' (id as s) ' '* "<=" { UPDATE (s) }
    | '.' (id as s) ' '* ":=" { FUPD(s) }
    | '.' (id as s) { SELECT (s) }
    | '[' { LBRACK }
    | ']' { RBRACK }
    | ':' { COLUMN }
    | ';' { SEMICOLUMN }
    | '(' { LPAR }
    | ')' { RPAR }
    | "ς" { SIGMA }
    | '=' { EQUAL }
    | "::=" { DEF }
    | '.' { DOT }
    | "->" { ARR }
    | "λ" { LAMBDA }
    | "Bool" { BOOL }
    | "true" { TRUE }
    | "false" { FALSE }
    | "if" { IF }
    | "then" { THEN }
    | "else" { ELSE }
    | "type" { TYPE (Parsing.rhs_start_pos 1) }
    | "let" { VAR (Parsing.rhs_start_pos 1) }
    | "check" { CHECK (Parsing.rhs_start_pos 1) }
    | "norm" { NORM (Parsing.rhs_start_pos 1) }
    | "print" { PRINT (Parsing.rhs_start_pos 1) }
    | id as s { ID (s) }
    | [ 'A'-'Z' ] ['a'-'z' 'A'-'Z' '_' '0'-'9']* as s { CID (s) }
    | '"' { flush (); string lexbuf }
    | _ as c { raise (Unexpected_char (Printf.sprintf"'%c'" c)) }
    | eof { raise End_of_file }

and string = parse
    | "\\n" { add_char '\n'; string lexbuf }
    | '\\' (_ as c) { add_char '\\'; add_char c; string lexbuf }
    | '\n' { Lexing.new_line lexbuf ; add_char '\n'; string lexbuf }
    | '"'  { STRING (!chars_read) }
    | _ as c { add_char c; string lexbuf }
    | eof { raise End_of_file_looking_for_double_quotes }