-
Notifications
You must be signed in to change notification settings - Fork 2
/
lexer.mll
99 lines (99 loc) · 2.27 KB
/
lexer.mll
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
{
open Parser
let keyword_table = Hashtbl.create 1010
let latex_table = Hashtbl.create 10101
let _ =
List.iter (fun (kwd, tok) -> Hashtbl.add keyword_table kwd tok)
[ "IMPLIES", ARROW;
"Implies", ARROW;
"implies", ARROW;
"IFF", EQUIV;
"Iff", EQUIV;
"iff", EQUIV;
"AND", AND;
"And", AND;
"and", AND;
"OR", OR;
"Or", OR;
"or", OR;
"NOT", NOT;
"Not", NOT;
"not", NOT;
"FALSE", BOT;
"False", BOT;
"false", BOT;
"TRUE", TOP;
"True", TOP;
"true", TOP;
]
let _ =
List.iter (fun (kwd, tok) -> Hashtbl.add latex_table kwd tok)
[ "to", ARROW;
"Rightarrow", ARROW;
"supset", ARROW;
"implies", ARROW;
"Leftrightarrow", EQUIV;
"equiv", EQUIV;
"leftrightarrow", EQUIV;
"iff", EQUIV;
"wedge", AND;
"land", AND;
"vee", OR;
"lor", OR;
"lnot", NOT;
"neg", NOT;
"sim", NOT;
"bot", BOT;
"top", TOP;
]
}
rule token =
parse [' ' '\t' '\n'] { token lexbuf }
| "(*" { in_comment lexbuf; token lexbuf }
| (['a'-'z' 'A'-'Z'] ['a'-'z' 'A'-'Z' '0'-'9' '_']*) as id {
try
Hashtbl.find keyword_table id
with Not_found ->
IDENT id }
| "\\" (['a'-'z' 'A'-'Z'] ['a'-'z' 'A'-'Z' '0'-'9']*) as id {
Hashtbl.find latex_table id }
| "=>" { ARROW }
| "->" { ARROW }
| "→" { ARROW }
| "⇒" { ARROW }
| "<=>" { EQUIV }
| "<->" { EQUIV }
| "=" { EQUIV }
| "⇔" { EQUIV }
| "&&" { AND }
| "&" { AND }
| "&" { AND }
| "*" { AND }
| "/\\" { AND }
| "∧" { AND }
| "||" { OR }
| "|" { OR }
| "|" { OR }
| "+" { OR }
| "\\/" { OR }
| "∨" { OR }
| "~" { NOT }
| "!" { NOT }
| "-" { NOT }
| "¬" { NOT }
| "¬" { NOT }
| "_|_" { BOT }
| "⊥" { BOT }
| "0" { BOT }
| "1" { TOP }
| "⊤" { TOP }
| "(" { LPAREN }
| "(" { LPAREN }
| ")" { RPAREN }
| ")" { RPAREN }
| _ { STRAY }
| eof { EOF }
and in_comment =
parse "(*" { in_comment lexbuf; in_comment lexbuf }
| "*)" { () }
| _ { in_comment lexbuf }