]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll
596a909c8d472f9bc199585205ec8f63480c919b
[helm.git] / matita / matita / contribs / lambdadelta / bin / recomm / recommLexer.mll
1 {
2   module EP = RecommParser
3
4   let debug = ref false
5
6   let keys = [|
7     "Note";
8     "NOTE";
9   |]
10
11   let heads = [|
12     "Advanced";
13     "Alternative";
14     "Basic";
15     "Constructions";
16     "Forward";
17     "Destructions";
18     "Eliminations";
19     "Eliminators";
20     "Equalities";
21     "Helper";
22     "Inversion";
23     "Inversions";
24     "Iterators";
25     "Main";
26     "Properties";
27   |]
28
29   let str c = String.make 1 c
30
31   let nl lexbuf = Lexing.new_line lexbuf
32
33   let is_uppercase_ascii s =
34     let rec aux i =
35        if i < 0 then true else
36        if 'a' <= s.[i] && s.[i] <= 'z' then false else
37        aux (pred i)  
38     in
39     aux (String.length s - 1)
40
41   let disambiguate_word s =
42     if Array.mem s keys then EP.KW s else
43     if Array.mem s heads then EP.HW s else
44     if is_uppercase_ascii s then EP.CW s else
45     EP.SW s
46
47   let log s =
48     if !debug then Printf.eprintf "lezer: %s\n" s
49
50   let log_s s =
51     if !debug then Printf.eprintf "lexer: %S\n" s
52
53   let log_c c =
54     if !debug then Printf.eprintf "lexer: %C\n" c
55 }
56
57 let CR = "\r"
58 let SP = " "
59 let NL = "\n"
60 let SR = "*"
61 let OP = "(*"
62 let CP = SR* "*)"  
63 let PP = CP SP* OP
64 let WF = ['A'-'Z' 'a'-'z']
65 let WB = ['A'-'Z' 'a'-'z' '_' '-']*
66 let WD = WF WB
67
68 rule src_token = parse
69   | CR       { src_token lexbuf                   } 
70   | NL  as c { log "NL"; nl lexbuf; EP.NL (str c) }
71   | SP+ as s { log "SP"; EP.SP s                  }
72   | PP  as s { log "PP"; EP.PP s                  }
73   | OP  as s { log "OP"; EP.OP s                  }
74   | CP  as s { log "CP"; EP.CP s                  }
75   | SR  as c { log "SR"; EP.SR (str c)            }
76   | WD  as s { log_s s ; disambiguate_word s      }
77   | _   as c { log_c c ; EP.OT (str c)            }
78   | eof      { log "EF"; EP.EF                    }