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
100
101
102
103
104
105
|
{
open Lexing
open Ast
open Parser
let kwd_table = Hashtbl.create 10
let () =
List.iter (fun (a, b) -> Hashtbl.add kwd_table a b)
[
"bool", BOOL;
"int", INT;
"real", REAL;
"const", CONST;
"node", NODE;
"returns", RETURNS;
"var", VAR;
"let", LET;
"tel", TEL;
"if", IF;
"then", THEN;
"else", ELSE;
"pre", PRE;
"not", NOT;
"and", AND;
"or", OR;
"mod", MOD;
"true", TRUE;
"false", FALSE;
"assume", ASSUME;
"guarantee",GUARANTEE;
"probe", PROBE;
]
}
(* special character classes *)
let space = [' ' '\t' '\r']+
let newline = "\n" | "\r" | "\r\n"
(* utilities *)
let digit = ['0'-'9']
let digit_ = ['0'-'9' '_']
(* integers *)
let int_dec = digit digit_*
let int_bin = ("0b" | "0B") ['0'-'1'] ['0'-'1' '_']*
let int_oct = ("0o" | "0O") ['0'-'7'] ['0'-'7' '_']*
let int_hex = ("0x" | "0X") ['0'-'9' 'a'-'f' 'A'-'F'] ['0'-'9' 'a'-'f' 'A'-'F' '_']*
let const_int = int_bin | int_oct | int_dec | int_hex
(* tokens *)
rule token = parse
(* identifier (TOK_id) or reserved keyword *)
| ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']* as id
{ try Hashtbl.find kwd_table id with Not_found -> IDENT id }
(* symbols *)
| "(" { LPAREN }
| ")" { RPAREN }
| "{" { LCURLY }
| "}" { RCURLY }
| "*" { STAR }
| "+" { PLUS }
| "-" { MINUS }
| "!" { EXCLAIM }
| "/" { DIVIDE }
| "%" { PERCENT }
| "<" { LESS }
| ">" { GREATER }
| "<=" { LESS_EQUAL }
| ">=" { GREATER_EQUAL }
| "==" { EQUAL_EQUAL }
| "<>" { DIFF }
| "&&" { AND_AND }
| "||" { BAR_BAR }
| ";" { SEMICOLON }
| ":" { COLON }
| "," { COMMA }
| "=" { EQUAL }
| "->" { ARROW }
(* literals *)
| const_int as c { INTVAL c }
(* spaces, comments *)
| "(*" { comment lexbuf; token lexbuf }
| "--" [^ '\n' '\r']* { token lexbuf }
| newline { new_line lexbuf; token lexbuf }
| space { token lexbuf }
(* end of files *)
| eof { EOF }
(* nested comments (handled recursively) *)
and comment = parse
| "*)" { () }
| [^ '\n' '\r'] { comment lexbuf }
| newline { new_line lexbuf; comment lexbuf }
|
