]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationLexer.ml
snapshot, notably:
[helm.git] / helm / ocaml / cic_notation / cicNotationLexer.ml
index 6ff589384a707e7db30b878c8433e2b9791d7c35..306cf45b915f88d324ebed695b90ec0caaeb367c 100644 (file)
@@ -23,9 +23,9 @@
  * 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+
 
@@ -41,40 +41,45 @@ let regexp implicit = '?'
 let regexp meta = implicit number
 
 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 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 =
@@ -97,9 +102,6 @@ let rec level1_token = lexer
   | 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
@@ -113,6 +115,8 @@ let rec level2_token = lexer
   | eof -> return lexbuf ("EOI", "")
   | _ -> 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 syntax_pattern_lexer = mk_lexer level1_token
+let ast_pattern_lexer = mk_lexer level2_token