* http://helm.cs.unibo.it/
*)
-exception Error of int * int * string
+open Printf
-exception Not_an_extended_ident
+exception Error of int * int * string
let regexp number = xml_digit+
let regexp tex_token = '\\' ident
+let regexp delim_begin = "\\["
+let regexp delim_end = "\\]"
+
let regexp keyword = '"' ident '"'
let regexp implicit = '?'
let regexp meta = implicit number
+let regexp csymbol = '\'' ident
+
+let regexp uri =
+ ("cic:/" | "theory:/") (* schema *)
+ ident ('/' ident)* (* path *)
+ ('.' ident)+ (* ext *)
+ ("#xpointer(" number ('/' number)+ ")")? (* xpointer *)
+
let error lexbuf msg =
- raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg))
+ let begin_cnum, end_cnum = Ulexing.loc lexbuf in
+ raise (Error (begin_cnum, end_cnum, msg))
let error_at_end lexbuf msg =
- raise (Error (Ulexing.lexeme_end lexbuf, Ulexing.lexeme_end lexbuf, msg))
+ let begin_cnum, end_cnum = Ulexing.loc lexbuf in
+ raise (Error (begin_cnum, end_cnum, msg))
let return lexbuf token =
+ let begin_cnum, end_cnum = Ulexing.loc lexbuf in
+ (* TODO handle line/column numbers *)
let flocation_begin =
- { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
- Lexing.pos_cnum = Ulexing.lexeme_start lexbuf }
- in
- let flocation_end =
- { flocation_begin with Lexing.pos_cnum = Ulexing.lexeme_end lexbuf }
+ { Lexing.pos_fname = "";
+ Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
+ Lexing.pos_cnum = begin_cnum }
in
+ let flocation_end = { flocation_begin with Lexing.pos_cnum = end_cnum } in
(token, (flocation_begin, flocation_end))
+let return_lexeme lexbuf name = return lexbuf (name, Ulexing.utf8_lexeme lexbuf)
+
let remove_quotes s = String.sub s 1 (String.length s - 2)
-let tok_func token stream =
- let lexbuf = Ulexing.from_utf8_stream stream in
- Token.make_stream_and_flocation
- (fun () ->
- try
- token lexbuf
- with
- | Ulexing.Error -> error_at_end lexbuf "Unexpected character"
- | Ulexing.InvalidCodepoint i -> error_at_end lexbuf "Invalid code point")
-
-let mk_lexer token = {
- Token.tok_func = token;
- Token.tok_using = (fun _ -> ());
- Token.tok_removing = (fun _ -> ());
- Token.tok_match = Token.default_match;
- Token.tok_text = Token.lexer_text;
- Token.tok_comm = None;
-}
+let mk_lexer token =
+ let tok_func stream =
+ let lexbuf = Ulexing.from_utf8_stream stream in
+ Token.make_stream_and_flocation
+ (fun () ->
+ try
+ token lexbuf
+ with
+ | Ulexing.Error -> error_at_end lexbuf "Unexpected character"
+ | Ulexing.InvalidCodepoint p ->
+ error_at_end lexbuf (sprintf "Invalid code point: %d" p))
+ in
+ {
+ Token.tok_func = tok_func;
+ Token.tok_using = (fun _ -> ());
+ Token.tok_removing = (fun _ -> ());
+ Token.tok_match = Token.default_match;
+ Token.tok_text = Token.lexer_text;
+ Token.tok_comm = None;
+ }
let expand_macro lexbuf =
let macro =
let keyword lexbuf = "KEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf)
-(** {2 Level 1 lexer} *)
-
-let rec level1_token = lexer
- | xml_blank+ -> level1_token lexbuf
- | ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
- | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
- | keyword -> return lexbuf (keyword lexbuf)
- | tex_token -> return lexbuf (expand_macro lexbuf)
- | eof -> return lexbuf ("EOI", "")
- | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
-
-let level1_tok_func stream = tok_func level1_token stream
-let level1_lexer = mk_lexer level1_tok_func
-
-(** {2 Level 2 lexer} *)
-
-let rec level2_token = lexer
- | xml_blank+ -> level1_token lexbuf
+let rec token = lexer
+ | xml_blank+ -> token lexbuf
| meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
| implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf)
| ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
| number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
| keyword -> return lexbuf (keyword lexbuf)
+ | delim_begin -> return lexbuf ("DELIM", Ulexing.utf8_lexeme lexbuf)
+ | delim_end -> return lexbuf ("DELIM", Ulexing.utf8_lexeme lexbuf)
| tex_token -> return lexbuf (expand_macro lexbuf)
+ | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
| eof -> return lexbuf ("EOI", "")
+ | csymbol -> return lexbuf ("CSYMBOL", Ulexing.utf8_lexeme lexbuf)
| _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
-let level2_tok_func stream = tok_func level2_token stream
-let level2_lexer = mk_lexer level2_tok_func
+(* API implementation *)
+
+let notation_lexer = mk_lexer token