]> matita.cs.unibo.it Git - helm.git/blob - components/content_pres/cicNotationLexer.ml
some patches. still does not compile properly
[helm.git] / components / content_pres / 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 (* $Id$ *)
27
28 open Printf
29
30 exception Error of int * int * string
31
32 let regexp number = xml_digit+
33
34   (* ZACK: breaks unicode's binder followed by an ascii letter without blank *)
35 (* let regexp ident_letter = xml_letter *)
36
37 let regexp ident_letter = [ 'a' - 'z' 'A' - 'Z' ]
38
39   (* must be in sync with "is_ligature_char" below *)
40 let regexp ligature_char = [ "'`~!?@*()[]<>-+=|:;.,/\"" ]
41 let regexp ligature = ligature_char ligature_char+
42
43 let is_ligature_char =
44   (* must be in sync with "regexp ligature_char" above *)
45   let chars = "'`~!?@*()[]<>-+=|:;.,/\"" in
46   (fun char ->
47     (try
48       ignore (String.index chars char);
49       true
50     with Not_found -> false))
51
52 let regexp ident_decoration = '\'' | '?' | '`'
53 let regexp ident_cont = ident_letter | xml_digit | '_'
54 let regexp ident = ident_letter ident_cont* ident_decoration*
55
56 let regexp tex_token = '\\' ident
57
58 let regexp delim_begin = "\\["
59 let regexp delim_end = "\\]"
60
61 let regexp qkeyword = "'" ident "'"
62
63 let regexp implicit = '?'
64 let regexp placeholder = '%'
65 let regexp meta = implicit number
66
67 let regexp csymbol = '\'' ident
68
69 let regexp begin_group = "@{" | "${"
70 let regexp end_group = '}'
71 let regexp wildcard = "$_"
72 let regexp ast_ident = "@" ident
73 let regexp ast_csymbol = "@" csymbol
74 let regexp meta_ident = "$" ident
75 let regexp meta_anonymous = "$_"
76 let regexp qstring = '"' [^ '"']* '"'
77
78 let regexp begincomment = "(**" xml_blank
79 let regexp beginnote = "(*"
80 let regexp endcomment = "*)"
81 (* let regexp comment_char = [^'*'] | '*'[^')']
82 let regexp note = "|+" ([^'*'] | "**") comment_char* "+|" *)
83
84 let level1_layouts = 
85   [ "sub"; "sup";
86     "below"; "above";
87     "over"; "atop"; "frac";
88     "sqrt"; "root"
89   ]
90
91 let level1_keywords =
92   [ "hbox"; "hvbox"; "hovbox"; "vbox";
93     "break";
94     "list0"; "list1"; "sep";
95     "opt";
96     "term"; "ident"; "number"
97   ] @ level1_layouts
98
99 let level2_meta_keywords =
100   [ "if"; "then"; "else";
101     "fold"; "left"; "right"; "rec";
102     "fail";
103     "default";
104     "anonymous"; "ident"; "number"; "term"; "fresh"
105   ]
106
107   (* (string, unit) Hashtbl.t, to exploit multiple bindings *)
108 let level2_ast_keywords = Hashtbl.create 23
109 let _ =
110   List.iter (fun k -> Hashtbl.add level2_ast_keywords k ())
111   [ "CProp"; "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "match";
112     "with"; "in"; "and"; "to"; "as"; "on"; "return" ]
113
114 let add_level2_ast_keyword k = Hashtbl.add level2_ast_keywords k ()
115 let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k
116
117   (* (string, int) Hashtbl.t, with multiple bindings.
118    * int is the unicode codepoint *)
119 let ligatures = Hashtbl.create 23
120 let _ =
121   List.iter
122     (fun (ligature, symbol) -> Hashtbl.add ligatures ligature symbol)
123     [ ("->", <:unicode<to>>);   ("=>", <:unicode<Rightarrow>>);
124       ("<=", <:unicode<leq>>);  (">=", <:unicode<geq>>);
125       ("<>", <:unicode<neq>>);  (":=", <:unicode<def>>);
126       ("==", <:unicode<equiv>>);
127     ]
128
129 let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+
130
131 let regexp uri =
132   ("cic:/" | "theory:/")              (* schema *)
133 (*   ident ('/' ident)*                  |+ path +| *)
134   uri_step ('/' uri_step)*            (* path *)
135   ('.' ident)+                        (* ext *)
136   ("#xpointer(" number ('/' number)+ ")")?  (* xpointer *)
137
138 let error lexbuf msg =
139   let begin_cnum, end_cnum = Ulexing.loc lexbuf in
140   raise (Error (begin_cnum, end_cnum, msg))
141 let error_at_end lexbuf msg =
142   let begin_cnum, end_cnum = Ulexing.loc lexbuf in
143   raise (Error (begin_cnum, end_cnum, msg))
144
145 let return_with_loc token begin_cnum end_cnum =
146   (* TODO handle line/column numbers *)
147   let flocation_begin =
148     { Lexing.pos_fname = "";
149       Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
150       Lexing.pos_cnum = begin_cnum }
151   in
152   let flocation_end = { flocation_begin with Lexing.pos_cnum = end_cnum } in
153   (token, (flocation_begin, flocation_end))
154
155 let return lexbuf token =
156   let begin_cnum, end_cnum = Ulexing.loc lexbuf in
157     return_with_loc token begin_cnum end_cnum
158
159 let return_lexeme lexbuf name = return lexbuf (name, Ulexing.utf8_lexeme lexbuf)
160
161 let return_symbol lexbuf s = return lexbuf ("SYMBOL", s)
162 let return_eoi lexbuf = return lexbuf ("EOI", "")
163
164 let remove_quotes s = String.sub s 1 (String.length s - 2)
165
166 let mk_lexer token =
167   let tok_func stream =
168 (*     let lexbuf = Ulexing.from_utf8_stream stream in *)
169 (** XXX Obj.magic rationale.
170  * The problem.
171  *  camlp4 constraints the tok_func field of Token.glexer to have type:
172  *    Stream.t char -> (Stream.t 'te * flocation_function)
173  *  In order to use ulex we have (in theory) to instantiate a new lexbuf each
174  *  time a char Stream.t is passed, destroying the previous lexbuf which may
175  *  have consumed a character from the old stream which is lost forever :-(
176  * The "solution".
177  *  Instead of passing to camlp4 a char Stream.t we pass a lexbuf, casting it to
178  *  char Stream.t with Obj.magic where needed.
179  *)
180     let lexbuf = Obj.magic stream in
181     Token.make_stream_and_flocation
182       (fun () ->
183         try
184           token lexbuf
185         with
186         | Ulexing.Error -> error_at_end lexbuf "Unexpected character"
187         | Ulexing.InvalidCodepoint p ->
188             error_at_end lexbuf (sprintf "Invalid code point: %d" p))
189   in
190   {
191     Token.tok_func = tok_func;
192     Token.tok_using = (fun _ -> ());
193     Token.tok_removing = (fun _ -> ()); 
194     Token.tok_match = Token.default_match;
195     Token.tok_text = Token.lexer_text;
196     Token.tok_comm = None;
197   }
198
199 let expand_macro lexbuf =
200   let macro =
201     Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1)
202   in
203   try
204     ("SYMBOL", Utf8Macro.expand macro)
205   with Utf8Macro.Macro_not_found _ -> "SYMBOL", Ulexing.utf8_lexeme lexbuf
206
207 let remove_quotes s = String.sub s 1 (String.length s - 2)
208 let remove_left_quote s = String.sub s 1 (String.length s - 1)
209
210 let rec level2_pattern_token_group counter buffer =
211   lexer
212   | end_group -> 
213       if (counter > 0) then
214         Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ;
215       snd (Ulexing.loc lexbuf)
216   | begin_group -> 
217       Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ;
218       ignore (level2_pattern_token_group (counter + 1) buffer lexbuf) ;
219       level2_pattern_token_group counter buffer lexbuf
220   | _ -> 
221       Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ;
222       level2_pattern_token_group counter buffer lexbuf
223
224 let read_unparsed_group token_name lexbuf =
225   let buffer = Buffer.create 16 in
226   let begin_cnum, _ = Ulexing.loc lexbuf in
227   let end_cnum = level2_pattern_token_group 0 buffer lexbuf in
228     return_with_loc (token_name, Buffer.contents buffer) begin_cnum end_cnum
229
230 let rec level2_meta_token =
231   lexer
232   | xml_blank+ -> level2_meta_token lexbuf
233   | ident ->
234       let s = Ulexing.utf8_lexeme lexbuf in
235         begin
236           if List.mem s level2_meta_keywords then
237             return lexbuf ("", s)
238           else
239             return lexbuf ("IDENT", s)
240         end
241   | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf
242   | ast_ident ->
243       return lexbuf ("UNPARSED_AST",
244         remove_left_quote (Ulexing.utf8_lexeme lexbuf))
245   | ast_csymbol ->
246       return lexbuf ("UNPARSED_AST",
247         remove_left_quote (Ulexing.utf8_lexeme lexbuf))
248   | eof -> return_eoi lexbuf
249
250 let rec comment_token acc depth =
251   lexer
252   | beginnote ->
253       let acc = acc ^ Ulexing.utf8_lexeme lexbuf in
254       comment_token acc (depth + 1) lexbuf
255   | endcomment ->
256       let acc = acc ^ Ulexing.utf8_lexeme lexbuf in
257       if depth = 0
258       then acc
259       else comment_token acc (depth - 1) lexbuf
260   | _ ->
261       let acc = acc ^ Ulexing.utf8_lexeme lexbuf in
262       comment_token acc depth lexbuf
263
264   (** @param k continuation to be invoked when no ligature has been found *)
265 let rec ligatures_token k =
266   lexer
267   | ligature ->
268       let lexeme = Ulexing.utf8_lexeme lexbuf in
269       (match List.rev (Hashtbl.find_all ligatures lexeme) with
270       | [] -> (* ligature not found, rollback and try default lexer *)
271           Ulexing.rollback lexbuf;
272           k lexbuf
273       | default_lig :: _ -> (* ligatures found, use the default one *)
274           return_symbol lexbuf default_lig)
275   | eof -> return_eoi lexbuf
276   | _ ->  (* not a ligature, rollback and try default lexer *)
277       Ulexing.rollback lexbuf;
278       k lexbuf
279
280 and level2_ast_token =
281   lexer
282   | xml_blank+ -> ligatures_token level2_ast_token lexbuf
283   | meta ->
284      let s = Ulexing.utf8_lexeme lexbuf in
285       return lexbuf ("META", String.sub s 1 (String.length s - 1))
286   | implicit -> return lexbuf ("IMPLICIT", "")
287   | placeholder -> return lexbuf ("PLACEHOLDER", "")
288   | ident ->
289       let lexeme = Ulexing.utf8_lexeme lexbuf in
290       if Hashtbl.mem level2_ast_keywords lexeme then
291         return lexbuf ("", lexeme)
292       else
293         return lexbuf ("IDENT", lexeme)
294   | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
295   | tex_token -> return lexbuf (expand_macro lexbuf)
296   | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
297   | qstring ->
298       return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf))
299   | csymbol ->
300       return lexbuf ("CSYMBOL", remove_left_quote (Ulexing.utf8_lexeme lexbuf))
301   | "${" -> read_unparsed_group "UNPARSED_META" lexbuf
302   | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf
303   | '(' -> return lexbuf ("LPAREN", "")
304   | ')' -> return lexbuf ("RPAREN", "")
305   | meta_ident ->
306       return lexbuf ("UNPARSED_META",
307         remove_left_quote (Ulexing.utf8_lexeme lexbuf))
308   | meta_anonymous -> return lexbuf ("UNPARSED_META", "anonymous")
309   | beginnote -> 
310       let _comment = comment_token (Ulexing.utf8_lexeme lexbuf) 0 lexbuf in
311 (*       let comment =
312         Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 4)
313       in
314       return lexbuf ("NOTE", comment) *)
315       ligatures_token level2_ast_token lexbuf
316   | begincomment -> return lexbuf ("BEGINCOMMENT","")
317   | endcomment -> return lexbuf ("ENDCOMMENT","")
318   | eof -> return_eoi lexbuf
319   | _ -> return_symbol lexbuf (Ulexing.utf8_lexeme lexbuf)
320
321 and level1_pattern_token =
322   lexer
323   | xml_blank+ -> ligatures_token level1_pattern_token lexbuf
324   | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
325   | ident ->
326       let s = Ulexing.utf8_lexeme lexbuf in
327         begin
328           if List.mem s level1_keywords then
329             return lexbuf ("", s)
330           else
331             return lexbuf ("IDENT", s)
332         end
333   | tex_token -> return lexbuf (expand_macro lexbuf)
334   | qkeyword ->
335       return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf))
336   | '(' -> return lexbuf ("LPAREN", "")
337   | ')' -> return lexbuf ("RPAREN", "")
338   | eof -> return_eoi lexbuf
339   | _ -> return_symbol lexbuf (Ulexing.utf8_lexeme lexbuf)
340
341 let level1_pattern_token = ligatures_token level1_pattern_token
342 let level2_ast_token = ligatures_token level2_ast_token
343
344 (* API implementation *)
345
346 let level1_pattern_lexer = mk_lexer level1_pattern_token
347 let level2_ast_lexer = mk_lexer level2_ast_token
348 let level2_meta_lexer = mk_lexer level2_meta_token
349
350 let lookup_ligatures lexeme =
351   try
352     if lexeme.[0] = '\\'
353     then [ Utf8Macro.expand (String.sub lexeme 1 (String.length lexeme - 1)) ]
354     else List.rev (Hashtbl.find_all ligatures lexeme)
355   with Invalid_argument _ | Utf8Macro.Macro_not_found _ -> []
356