helm/ocaml/cic_notation/cicNotationLexer.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 exception Error of int * int * string
  27
  28 exception Not_an_extended_ident
  29
  30 let regexp number = xml_digit+
  31
  32 let regexp ident_decoration = '\'' | '!' | '?' | '`'
  33 let regexp ident_cont = xml_letter | xml_digit | '_'
  34 let regexp ident = xml_letter ident_cont* ident_decoration*
  35
  36 let regexp tex_token = '\\' ident
  37
  38 let regexp keyword = '"' ident '"'
  39
  40 let regexp implicit = '?'
  41 let regexp meta = implicit number
  42
  43 let error lexbuf msg =
  44   raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg))
  45 let error_at_end lexbuf msg =
  46   raise (Error (Ulexing.lexeme_end lexbuf, Ulexing.lexeme_end lexbuf, msg))
  47
  48 let return lexbuf token =
  49   let flocation_begin =
  50     { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
  51       Lexing.pos_cnum = Ulexing.lexeme_start lexbuf }
  52   in
  53   let flocation_end =
  54     { flocation_begin with Lexing.pos_cnum = Ulexing.lexeme_end lexbuf }
  55   in
  56   (token, (flocation_begin, flocation_end))
  57
  58 let remove_quotes s = String.sub s 1 (String.length s - 2)
  59
  60 let tok_func token stream =
  61   let lexbuf = Ulexing.from_utf8_stream stream in
  62   Token.make_stream_and_flocation
  63     (fun () ->
  64       try
  65         token lexbuf
  66       with
  67       | Ulexing.Error -> error_at_end lexbuf "Unexpected character"
  68       | Ulexing.InvalidCodepoint i -> error_at_end lexbuf "Invalid code point")
  69
  70 let mk_lexer token = {
  71   Token.tok_func = token;
  72   Token.tok_using = (fun _ -> ());
  73   Token.tok_removing = (fun _ -> ());
  74   Token.tok_match = Token.default_match;
  75   Token.tok_text = Token.lexer_text;
  76   Token.tok_comm = None;
  77 }
  78
  79 let expand_macro lexbuf =
  80   let macro =
  81     Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1)
  82   in
  83   try
  84     ("SYMBOL", Utf8Macro.expand macro)
  85   with Utf8Macro.Macro_not_found _ -> "SYMBOL", Ulexing.utf8_lexeme lexbuf
  86
  87 let keyword lexbuf = "KEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf)
  88
  89 (** {2 Level 1 lexer} *)
  90
  91 let rec level1_token = lexer
  92   | xml_blank+ -> level1_token lexbuf
  93   | ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
  94   | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
  95   | keyword -> return lexbuf (keyword lexbuf)
  96   | tex_token -> return lexbuf (expand_macro lexbuf)
  97   | eof -> return lexbuf ("EOI", "")
  98   | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
  99
 100 let level1_tok_func stream = tok_func level1_token stream
 101 let level1_lexer = mk_lexer level1_tok_func
 102
 103 (** {2 Level 2 lexer} *)
 104
 105 let rec level2_token = lexer
 106   | xml_blank+ -> level1_token lexbuf
 107   | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
 108   | implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf)
 109   | ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
 110   | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
 111   | keyword -> return lexbuf (keyword lexbuf)
 112   | tex_token -> return lexbuf (expand_macro lexbuf)
 113   | eof -> return lexbuf ("EOI", "")
 114   | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
 115
 116 let level2_tok_func stream = tok_func level2_token stream
 117 let level2_lexer = mk_lexer level2_tok_func
 118