1
|
open Format
|
2
|
|
3
|
type ident = Utils.ident
|
4
|
type rat = Utils.rat
|
5
|
type tag = Utils.tag
|
6
|
type label = Utils.ident
|
7
|
|
8
|
type type_dec =
|
9
|
{ty_dec_desc: type_dec_desc;
|
10
|
ty_dec_loc: Location.t}
|
11
|
|
12
|
and type_dec_desc =
|
13
|
| Tydec_any
|
14
|
| Tydec_int
|
15
|
| Tydec_real
|
16
|
| Tydec_float
|
17
|
| Tydec_bool
|
18
|
| Tydec_clock of type_dec_desc
|
19
|
| Tydec_const of ident
|
20
|
| Tydec_enum of ident list
|
21
|
| Tydec_struct of (ident * type_dec_desc) list
|
22
|
| Tydec_array of Dimension.dim_expr * type_dec_desc
|
23
|
|
24
|
type clock_dec =
|
25
|
{ck_dec_desc: clock_dec_desc;
|
26
|
ck_dec_loc: Location.t}
|
27
|
|
28
|
and clock_dec_desc =
|
29
|
| Ckdec_any
|
30
|
| Ckdec_bool of (ident * ident) list
|
31
|
| Ckdec_pclock of int * rat
|
32
|
|
33
|
type var_decl =
|
34
|
{var_id: ident;
|
35
|
var_dec_type: type_dec;
|
36
|
var_dec_clock: clock_dec;
|
37
|
var_dec_const: bool;
|
38
|
mutable var_type: Types.type_expr;
|
39
|
mutable var_clock: Clocks.clock_expr;
|
40
|
var_loc: Location.t}
|
41
|
|
42
|
(** The core language and its ast. Every element of the ast contains its
|
43
|
location in the program text. The type and clock of an ast element
|
44
|
is mutable (and initialized to dummy values). This avoids to have to
|
45
|
duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
|
46
|
|
47
|
|
48
|
type constant =
|
49
|
| Const_int of int
|
50
|
| Const_real of string
|
51
|
| Const_float of float
|
52
|
| Const_array of constant list
|
53
|
| Const_tag of label
|
54
|
| Const_string of string (* used only for annotations *)
|
55
|
| Const_struct of (label * constant) list
|
56
|
|
57
|
type quantifier_type = Exists | Forall
|
58
|
|
59
|
|
60
|
|
61
|
(* The tag of an expression is a unique identifier used to distinguish
|
62
|
different instances of the same node *)
|
63
|
type expr =
|
64
|
{expr_tag: tag;
|
65
|
expr_desc: expr_desc;
|
66
|
mutable expr_type: Types.type_expr;
|
67
|
mutable expr_clock: Clocks.clock_expr;
|
68
|
mutable expr_delay: Delay.delay_expr;
|
69
|
mutable expr_annot: expr_annot option;
|
70
|
expr_loc: Location.t}
|
71
|
|
72
|
and expr_desc =
|
73
|
| Expr_const of constant
|
74
|
| Expr_ident of ident
|
75
|
| Expr_tuple of expr list
|
76
|
| Expr_ite of expr * expr * expr
|
77
|
| Expr_arrow of expr * expr
|
78
|
| Expr_fby of expr * expr
|
79
|
| Expr_array of expr list
|
80
|
| Expr_access of expr * Dimension.dim_expr
|
81
|
| Expr_power of expr * Dimension.dim_expr
|
82
|
| Expr_pre of expr
|
83
|
| Expr_when of expr * ident * label
|
84
|
| Expr_merge of ident * (label * expr) list
|
85
|
| Expr_appl of call_t
|
86
|
and call_t = ident * expr * (ident * label) option
|
87
|
(* The third part denotes the reseting clock label and value *)
|
88
|
and
|
89
|
(* The tag of an expression is a unique identifier used to distinguish
|
90
|
different instances of the same node *)
|
91
|
eexpr =
|
92
|
{eexpr_tag: tag;
|
93
|
eexpr_qfexpr: expr;
|
94
|
eexpr_quantifiers: (quantifier_type * var_decl list) list;
|
95
|
mutable eexpr_type: Types.type_expr;
|
96
|
mutable eexpr_clock: Clocks.clock_expr;
|
97
|
mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
|
98
|
eexpr_loc: Location.t}
|
99
|
|
100
|
and expr_annot = {
|
101
|
annots: (string list * eexpr) list;
|
102
|
annot_loc: Location.t
|
103
|
}
|
104
|
and
|
105
|
eq =
|
106
|
{eq_lhs: ident list;
|
107
|
eq_rhs: expr;
|
108
|
eq_loc: Location.t}
|
109
|
|
110
|
|
111
|
type node_annot = {
|
112
|
requires: eexpr list;
|
113
|
ensures: eexpr list;
|
114
|
behaviors: (string * eexpr list * eexpr list * Location.t) list;
|
115
|
spec_loc: Location.t;
|
116
|
}
|
117
|
type assert_t =
|
118
|
{
|
119
|
assert_expr: expr;
|
120
|
assert_loc: Location.t;
|
121
|
}
|
122
|
|
123
|
type node_desc =
|
124
|
{node_id: ident;
|
125
|
mutable node_type: Types.type_expr;
|
126
|
mutable node_clock: Clocks.clock_expr;
|
127
|
node_inputs: var_decl list;
|
128
|
node_outputs: var_decl list;
|
129
|
node_locals: var_decl list;
|
130
|
mutable node_gencalls: expr list;
|
131
|
mutable node_checks: Dimension.dim_expr list;
|
132
|
node_asserts: assert_t list;
|
133
|
node_eqs: eq list;
|
134
|
mutable node_dec_stateless: bool;
|
135
|
mutable node_stateless: bool option;
|
136
|
node_spec: node_annot option;
|
137
|
node_annot: expr_annot list;
|
138
|
}
|
139
|
|
140
|
type imported_node_desc =
|
141
|
{nodei_id: ident;
|
142
|
mutable nodei_type: Types.type_expr;
|
143
|
mutable nodei_clock: Clocks.clock_expr;
|
144
|
nodei_inputs: var_decl list;
|
145
|
nodei_outputs: var_decl list;
|
146
|
nodei_stateless: bool;
|
147
|
nodei_spec: node_annot option;
|
148
|
nodei_prototype: string option;
|
149
|
nodei_in_lib: string option;
|
150
|
}
|
151
|
|
152
|
type const_desc =
|
153
|
{const_id: ident;
|
154
|
const_loc: Location.t;
|
155
|
const_value: constant;
|
156
|
mutable const_type: Types.type_expr;
|
157
|
}
|
158
|
|
159
|
type top_decl_desc =
|
160
|
| Node of node_desc
|
161
|
| Consts of const_desc list
|
162
|
| ImportedNode of imported_node_desc
|
163
|
| Open of bool * string (* the boolean set to true denotes a local
|
164
|
lusi vs a lusi installed at system level *)
|
165
|
|
166
|
type top_decl =
|
167
|
{top_decl_desc: top_decl_desc;
|
168
|
top_decl_loc: Location.t}
|
169
|
|
170
|
type program = top_decl list
|
171
|
|
172
|
type error =
|
173
|
Main_not_found
|
174
|
| Main_wrong_kind
|
175
|
| No_main_specified
|
176
|
| Unbound_symbol of ident
|
177
|
| Already_bound_symbol of ident
|
178
|
|
179
|
|
180
|
(* Local Variables: *)
|
181
|
(* compile-command:"make -C .." *)
|
182
|
(* End: *)
|