-
Notifications
You must be signed in to change notification settings - Fork 0
/
lexer.mll
70 lines (69 loc) · 2.86 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
{
open Parser
let incr_linenum lexbuf =
let pos = lexbuf.Lexing.lex_curr_p in
lexbuf.Lexing.lex_curr_p <- { pos with
Lexing.pos_lnum = pos.Lexing.pos_lnum + 1;
Lexing.pos_bol = pos.Lexing.pos_cnum;
}
;;
}
let digit = ['0' - '9']
let digits = digit +
let lower = ['a' - 'z']
let upper = ['A' - 'Z']
let letter = lower | upper
let letters = letter ((letter | digit) * )
rule token = parse
| "0" { Zero (* :: main lexbuf *) }
| "let" { Let (* :: main lexbuf *) }
| "symbols" { Symbols (* :: main lexbuf *) }
| "private" { Private (* :: main lexbuf *) }
| "channels" { Channels (* :: main lexbuf *) }
| "evchannels" { EvChannels (* :: main lexbuf *) }
| "::" { InnerSequence (* :: main lexbuf *) }
| "||" { InnerInterleave (* :: main lexbuf *) }
| "interleave" { Interleave (* :: main lexbuf *) }
| "interleave_opt" { InterleaveOpt (* :: main lexbuf *) }
| "remove_end_tests" { RemoveEndTests (* :: main lexbuf *) }
| "print_traces" { PrintTraces (* :: main lexbuf *) }
| "sequence" { Sequence (* :: main lexbuf *) }
| "print" { Print (* :: main lexbuf *) }
| "|-" { Deduc (* :: main lexbuf *) }
| "equivalentft?" { Square (* :: main lexbuf *) }
| "fwdequivalentft?" { EvSquare (* :: main lexbuf *) }
| "var" { Var (* :: main lexbuf *) }
| "equivalentct?" { Equivalent (* :: main lexbuf *) }
| "and" { And (* :: main lexbuf *) }
| "/*" { comment 1 lexbuf }
| "//" { line_comment lexbuf (* :: main lexbuf *) }
| "/" { Slash (* :: main lexbuf *) }
| "," { Comma (* :: main lexbuf *) }
| ";" { Semicolon (* :: main lexbuf *) }
| "var" { Var (* :: main lexbuf *) }
| "rewrite" { Rewrite (* :: main lexbuf *) }
| "evrewrite" { EvRewrite (* :: main lexbuf *) }
| "->" { Arrow (* :: main lexbuf *) }
| "=" { Equals (* :: main lexbuf *) }
| "out" { Out (* :: main lexbuf *) }
| "in" { In (* :: main lexbuf *) }
| "[" { LeftB (* :: main lexbuf *) }
| "]" { RightB (* :: main lexbuf *) }
| "(" { LeftP (* :: main lexbuf *) }
| ")" { RightP (* :: main lexbuf *) }
| "." { Dot (* :: main lexbuf *) }
| digits as n { Int(int_of_string n) (* :: main lexbuf *) }
| letters as s { Identifier s (* :: main lexbuf *) }
| '\n' { incr_linenum lexbuf; token lexbuf }
| eof { EOF (* [] *) }
| _ { token lexbuf }
and comment depth = parse
| '\n' { incr_linenum lexbuf; comment depth lexbuf }
| "/*" { comment (depth + 1) lexbuf }
| "*/" { if depth = 1
then token lexbuf
else comment (depth - 1) lexbuf }
| _ { comment depth lexbuf }
and line_comment = parse
| '\n' { incr_linenum lexbuf; token lexbuf }
| _ { line_comment lexbuf }