helm/ocaml/cic_disambiguation/lexer.ml

   1
   2 exception Error of int * int * string
   3
   4 let regexp alpha = [ 'a' - 'z' 'A' - 'Z' ]
   5 let regexp digit = [ '0' - '9' ]
   6 let regexp blank = [ ' ' '\t' '\n' ]
   7
   8 let regexp blanks = blank+
   9 let regexp num = digit+
  10 let regexp ident = alpha (alpha | num)*
  11 let regexp symbol = [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' ]
  12 let regexp tex_token = '\\' alpha+
  13 let regexp lparen = [ '(' '[' '{' ]
  14 let regexp rparen = [ ')' ']' '}' ]
  15 let regexp meta = '?' (alpha | num)+
  16
  17 let keywords = Hashtbl.create 17
  18 let _ =
  19   List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword))
  20     [ "Prop"; "Type"; "Set"; "let"; "rec"; "using"; "match"; "with" ]
  21
  22 let error lexbuf msg =
  23   raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg))
  24 let error_at_end lexbuf msg =
  25   raise (Error (Ulexing.lexeme_end lexbuf, Ulexing.lexeme_end lexbuf, msg))
  26
  27 let return lexbuf token = (token, Ulexing.loc lexbuf)
  28
  29 let rec token = lexer
  30 | blanks -> token lexbuf
  31 | ident ->
  32     let lexeme = Ulexing.utf8_lexeme lexbuf in
  33     (try
  34       return lexbuf (Hashtbl.find keywords lexeme)
  35     with Not_found ->
  36       return lexbuf ("IDENT", lexeme))
  37 | num -> return lexbuf ("INT", Ulexing.utf8_lexeme lexbuf)
  38 | lparen -> return lexbuf ("LPAREN", Ulexing.utf8_lexeme lexbuf)
  39 | rparen -> return lexbuf ("RPAREN", Ulexing.utf8_lexeme lexbuf)
  40 | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
  41 | symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
  42 | tex_token ->
  43     let macro =
  44       Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1)
  45     in
  46     (try
  47       return lexbuf ("SYMBOL", Macro.expand macro)
  48     with Macro.Macro_not_found _ ->
  49       return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf))
  50 | eof -> return lexbuf ("EOI", "")
  51 | _ -> error lexbuf "Invalid character"
  52
  53 let tok_func stream =
  54   let lexbuf = Ulexing.from_utf8_stream stream in
  55   Token.make_stream_and_location
  56     (fun () ->
  57       try
  58         token lexbuf
  59       with
  60       | Ulexing.Error -> error_at_end lexbuf "Unexpected character"
  61       | Ulexing.InvalidCodepoint i -> error_at_end lexbuf "Invalid code point")
  62
  63 let lex =
  64   {
  65     Token.tok_func = tok_func;
  66     Token.tok_using = (fun _ -> ());
  67     Token.tok_removing = (fun _ -> ());
  68     Token.tok_match = Token.default_match;
  69     Token.tok_text = Token.lexer_text;
  70     Token.tok_comm = None;
  71   }