blob: c561cef5639dc41dab6abbc11c6d91f755968075 (
plain) (
blame)
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
106
107
108
109
110
111
112
113
114
115
|
open Lexing
open Util
type 'a ext = 'a * extent
type id = string
type typ =
| AST_TINT
| AST_TBOOL
| AST_TREAL
type unary_op =
| AST_UPLUS
| AST_UMINUS
type binary_op =
(* num * num -> num *)
| AST_PLUS
| AST_MINUS
| AST_MUL
| AST_DIV
| AST_MOD
type binary_rel_op =
(* 'a * 'a -> bool *)
| AST_EQ
| AST_NE
(* num * num -> bool *)
| AST_LT
| AST_LE
| AST_GT
| AST_GE
type bin_bool_op =
(* bool * bool -> bool *)
| AST_AND
| AST_OR
type expr =
| AST_identifier of id ext
| AST_idconst of id ext
(* on numerical values *)
| AST_int_const of string ext
| AST_real_const of string ext
| AST_unary of unary_op * (expr ext)
| AST_binary of binary_op * (expr ext) * (expr ext)
| AST_cast of (expr ext) * typ
(* on boolean values *)
| AST_bool_const of bool
| AST_binary_rel of binary_rel_op * (expr ext) * (expr ext)
| AST_binary_bool of bin_bool_op * (expr ext) * (expr ext)
| AST_not of expr ext
(* temporal primitives *)
| AST_pre of expr ext * id
| AST_arrow of (expr ext) * (expr ext)
(* other *)
| AST_if of (expr ext) * (expr ext) * (expr ext)
| AST_instance of (id ext) * (expr ext list) * id
| AST_tuple of expr ext list
type var_def = bool * id * typ
type automaton = id * state ext list * id list
and state = {
initial : bool;
st_name : id;
st_locals : var_def list;
body : eqn ext list;
until : transition list;
(* these two rst info are determined after parsing, in typing.ml when
the variable list is extracted *)
mutable i_rst : bool; (* resettable by S -> S transition *)
mutable o_rst : bool; (* resettable by S' -> S transition *)
}
and transition = (expr ext) * (id ext) * bool (* bool : does it reset ? *)
and activate_block = {
act_id : id;
act_locals : var_def list;
body : eqn ext list;
}
and activate_if =
| AST_activate_body of activate_block
| AST_activate_if of expr ext * activate_if * activate_if
and activate = activate_if * id list
and eqn =
| AST_assign of (id ext list) * (expr ext)
| AST_assume of (id ext) * (expr ext)
| AST_guarantee of (id ext) * (expr ext)
| AST_automaton of automaton
| AST_activate of activate
type node_decl = {
n_name : id;
args : var_def list;
ret : var_def list;
var : var_def list;
body : eqn ext list;
}
type const_decl = {
c_name : id;
typ : typ;
value : expr ext;
}
type toplevel =
| AST_node_decl of node_decl ext
| AST_const_decl of const_decl ext
type prog = toplevel list
|
