]> matita.cs.unibo.it Git - helm.git/blob - helm/software/lambda-delta/automath/autLexer.mll
freescale porting
[helm.git] / helm / software / lambda-delta / 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 L = Log
14    module P = AutParser
15    
16    let debug = false
17    let out s = if debug then L.warn s else ()
18
19    let unquote = ref false
20
21 (* This turns an Automath identifier into an XML nmtoken *)
22    let quote id =
23       let l = String.length id in
24       let rec aux i =
25          if i < l then begin
26             if id.[i] = '\'' || id.[i] = '`' then id.[i] <- '_';
27             aux (succ i)
28          end else
29             id
30       in
31       aux 0
32 }
33
34 let LC  = ['#' '%']
35 let OC  = "{"
36 let CC  = "}"
37 let SPC = [' ' '\t' '\n']+
38 let NL  = "\n"
39 let ID  = ['0'-'9' 'A'-'Z' 'a'-'z' '_' '\'' '`']+
40
41 rule line_comment = parse
42    | NL  { () }
43    | OC  { block_comment lexbuf; line_comment lexbuf }
44    | _   { line_comment lexbuf }
45    | eof { () } 
46 and block_comment = parse
47    | CC  { () }
48    | OC  { block_comment lexbuf; block_comment lexbuf }
49    | LC  { line_comment lexbuf; block_comment lexbuf  }
50    | _   { block_comment lexbuf }
51 and token = parse
52    | SPC      { token lexbuf } 
53    | LC       { line_comment lexbuf; token lexbuf  }
54    | OC       { block_comment lexbuf; token lexbuf }
55    | "_E"     { out "E"; P.E         }
56    | "'_E'"   { out "E"; P.E         }
57    | "---"    { out "EB"; P.EB       }
58    | "'eb'"   { out "EB"; P.EB       }
59    | "EB"     { out "EB"; P.EB       }
60    | "--"     { out "EXIT"; P.EXIT   }
61    | "PN"     { out "PN"; P.PN       }
62    | "'pn'"   { out "PN"; P.PN       }
63    | "PRIM"   { out "PN"; P.PN       }
64    | "'prim'" { out "PN"; P.PN       }
65    | "???"    { out "PN"; P.PN       }
66    | "PROP"   { out "PROP"; P.PROP   }
67    | "'prop'" { out "PROP"; P.PROP   }
68    | "TYPE"   { out "TYPE"; P.TYPE   }
69    | "'type'" { out "TYPE"; P.TYPE   }
70    | ID       { out "ID"; 
71                    let s = Lexing.lexeme lexbuf in
72                    if !unquote then P.IDENT s else P.IDENT (quote s)
73               }
74    | ":="     { out "DEF"; P.DEF     }
75    | "("      { out "OP"; P.OP       }
76    | ")"      { out "CP"; P.CP       }
77    | "["      { out "OB"; P.OB       }
78    | "]"      { out "CB"; P.CB       }
79    | "<"      { out "OA"; P.OA       }
80    | ">"      { out "CA"; P.CA       }
81    | "@"      { out "AT"; P.AT       }
82    | "~"      { out "TD"; P.TD       }
83    | "\""     { out "QT"; P.QT       }
84    | ":"      { out "CN"; P.CN       }   
85    | ","      { out "CM"; P.CM       }
86    | ";"      { out "SC"; P.SC       }
87    | "."      { out "FS"; P.FS       }   
88    | "+"      { out "PLUS"; P.PLUS   }
89    | "-"      { out "MINUS"; P.MINUS }
90    | "*"      { out "TIMES"; P.TIMES }
91    | "="      { out "DEF"; P.DEF     }
92    | eof      { out "EOF"; P.EOF     }