]> matita.cs.unibo.it Git - helm.git/blob - helm/software/helena/src/automath/autLexer.mll
update in basic_2
[helm.git] / helm / software / helena / src / automath / autLexer.mll
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.              
9      \ /   This software is distributed as is, NO WARRANTY.              
10       V_______________________________________________________________ *)
11
12
13    module KT = String
14
15    module L  = Log
16    module G  = Options
17    module AP = AutParser
18
19    let level = 0
20
21 IFDEF LEXER THEN   
22    let out s = if !G.debug_lexer then L.warn level s else ()
23 END
24
25 IFDEF QUOTE THEN
26 (* This turns an Automath identifier into an XML nmtoken *)
27    let quote id =
28       let map = function
29          | '\''
30          | '`' -> '_';
31          | c   -> c
32       in
33       KT.map map id
34
35 END
36 }
37
38 let LC  = ['#' '%']
39 let OC  = "{"
40 let CC  = "}"
41 let SPC = [' ' '\t' '\n']+
42 let NL  = "\n"
43 let ID  = ['0'-'9' 'A'-'Z' 'a'-'z' '_' '\'' '`']+
44
45 rule line_comment = parse
46    | NL  { () }
47    | OC  { block_comment lexbuf; line_comment lexbuf }
48    | _   { line_comment lexbuf }
49    | eof { () } 
50 and block_comment = parse
51    | CC  { () }
52    | OC  { block_comment lexbuf; block_comment lexbuf }
53    | LC  { line_comment lexbuf; block_comment lexbuf  }
54    | _   { block_comment lexbuf }
55 and token = parse
56    | SPC      { token lexbuf } 
57    | LC       { line_comment lexbuf; token lexbuf  }
58    | OC       { block_comment lexbuf; token lexbuf }
59    | "_E"     { IFDEF LEXER THEN out "E" ELSE () END; AP.E         }
60    | "'_E'"   { IFDEF LEXER THEN out "E" ELSE () END; AP.E         }
61    | "---"    { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB       }
62    | "'eb'"   { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB       }
63    | "EB"     { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB       }
64    | "--"     { IFDEF LEXER THEN out "EXIT" ELSE () END; AP.EXIT   }
65    | "PN"     { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
66    | "'pn'"   { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
67    | "PRIM"   { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
68    | "'prim'" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
69    | "???"    { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
70    | "PROP"   { IFDEF LEXER THEN out "PROP" ELSE () END; AP.PROP   }
71    | "'prop'" { IFDEF LEXER THEN out "PROP" ELSE () END; AP.PROP   }
72    | "TYPE"   { IFDEF LEXER THEN out "TYPE" ELSE () END; AP.TYPE   }
73    | "'type'" { IFDEF LEXER THEN out "TYPE" ELSE () END; AP.TYPE   }
74    | ID       { IFDEF LEXER THEN out "ID" ELSE () END; 
75                    let s = Lexing.lexeme lexbuf in
76 IFDEF QUOTE THEN
77                    if !G.quote then AP.IDENT (quote s) else AP.IDENT s
78 ELSE
79                    AP.IDENT s
80 END
81               }
82    | ":="     { IFDEF LEXER THEN out "DEF" ELSE () END; AP.DEF     }
83    | "("      { IFDEF LEXER THEN out "OP" ELSE () END; AP.OP       }
84    | ")"      { IFDEF LEXER THEN out "CP" ELSE () END; AP.CP       }
85    | "["      { IFDEF LEXER THEN out "OB" ELSE () END; AP.OB       }
86    | "]"      { IFDEF LEXER THEN out "CB" ELSE () END; AP.CB       }
87    | "<"      { IFDEF LEXER THEN out "OA" ELSE () END; AP.OA       }
88    | ">"      { IFDEF LEXER THEN out "CA" ELSE () END; AP.CA       }
89    | "@"      { IFDEF LEXER THEN out "AT" ELSE () END; AP.AT       }
90    | "~"      { IFDEF LEXER THEN out "TD" ELSE () END; AP.TD       }
91    | "\""     { IFDEF LEXER THEN out "QT" ELSE () END; AP.QT       }
92    | ":"      { IFDEF LEXER THEN out "CN" ELSE () END; AP.CN       }   
93    | ","      { IFDEF LEXER THEN out "CM" ELSE () END; AP.CM       }
94    | ";"      { IFDEF LEXER THEN out "SC" ELSE () END; AP.SC       }
95    | "."      { IFDEF LEXER THEN out "FS" ELSE () END; AP.FS       }   
96    | "+"      { IFDEF LEXER THEN out "PLUS" ELSE () END; AP.PLUS   }
97    | "-"      { IFDEF LEXER THEN out "MINUS" ELSE () END; AP.MINUS }
98    | "*"      { IFDEF LEXER THEN out "TIMES" ELSE () END; AP.TIMES }
99    | "="      { IFDEF LEXER THEN out "DEF" ELSE () END; AP.DEF     }
100    | eof      { IFDEF LEXER THEN out "EOF" ELSE () END; AP.EOF     }