lustrec / src / lustreSpec.ml @ 2d179f5b
History | View | Annotate | Download (6.45 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
5 |
(* *) |
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 |
(* under the terms of the GNU Lesser General Public License *) |
8 |
(* version 2.1. *) |
9 |
(* *) |
10 |
(********************************************************************) |
11 |
|
12 |
open Format |
13 |
|
14 |
type ident = Utils.ident |
15 |
type rat = Utils.rat |
16 |
type tag = Utils.tag |
17 |
type label = Utils.ident |
18 |
|
19 |
type type_dec = |
20 |
{ty_dec_desc: type_dec_desc; |
21 |
ty_dec_loc: Location.t} |
22 |
|
23 |
and type_dec_desc = |
24 |
| Tydec_any |
25 |
| Tydec_int |
26 |
| Tydec_real |
27 |
| Tydec_float |
28 |
| Tydec_bool |
29 |
| Tydec_clock of type_dec_desc |
30 |
| Tydec_const of ident |
31 |
| Tydec_enum of ident list |
32 |
| Tydec_struct of (ident * type_dec_desc) list |
33 |
| Tydec_array of Dimension.dim_expr * type_dec_desc |
34 |
|
35 |
type typedec_desc = |
36 |
{tydec_id: ident} |
37 |
|
38 |
type typedef_desc = |
39 |
{tydef_id: ident; |
40 |
tydef_desc: type_dec_desc} |
41 |
|
42 |
type clock_dec = |
43 |
{ck_dec_desc: clock_dec_desc; |
44 |
ck_dec_loc: Location.t} |
45 |
|
46 |
and clock_dec_desc = |
47 |
| Ckdec_any |
48 |
| Ckdec_bool of (ident * ident) list |
49 |
| Ckdec_pclock of int * rat |
50 |
|
51 |
type constant = |
52 |
| Const_int of int |
53 |
| Const_real of string |
54 |
| Const_float of float |
55 |
| Const_array of constant list |
56 |
| Const_tag of label |
57 |
| Const_string of string (* used only for annotations *) |
58 |
| Const_struct of (label * constant) list |
59 |
|
60 |
type quantifier_type = Exists | Forall |
61 |
|
62 |
type var_decl = |
63 |
{var_id: ident; |
64 |
var_orig:bool; |
65 |
var_dec_type: type_dec; |
66 |
var_dec_clock: clock_dec; |
67 |
var_dec_const: bool; |
68 |
var_dec_value: expr option; |
69 |
mutable var_type: Types.type_expr; |
70 |
mutable var_clock: Clocks.clock_expr; |
71 |
var_loc: Location.t} |
72 |
|
73 |
(** The core language and its ast. Every element of the ast contains its |
74 |
location in the program text. The type and clock of an ast element |
75 |
is mutable (and initialized to dummy values). This avoids to have to |
76 |
duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *) |
77 |
|
78 |
|
79 |
|
80 |
(* The tag of an expression is a unique identifier used to distinguish |
81 |
different instances of the same node *) |
82 |
and expr = |
83 |
{expr_tag: tag; |
84 |
expr_desc: expr_desc; |
85 |
mutable expr_type: Types.type_expr; |
86 |
mutable expr_clock: Clocks.clock_expr; |
87 |
mutable expr_delay: Delay.delay_expr; |
88 |
mutable expr_annot: expr_annot option; |
89 |
expr_loc: Location.t} |
90 |
|
91 |
and expr_desc = |
92 |
| Expr_const of constant |
93 |
| Expr_ident of ident |
94 |
| Expr_tuple of expr list |
95 |
| Expr_ite of expr * expr * expr |
96 |
| Expr_arrow of expr * expr |
97 |
| Expr_fby of expr * expr |
98 |
| Expr_array of expr list |
99 |
| Expr_access of expr * Dimension.dim_expr |
100 |
| Expr_power of expr * Dimension.dim_expr |
101 |
| Expr_pre of expr |
102 |
| Expr_when of expr * ident * label |
103 |
| Expr_merge of ident * (label * expr) list |
104 |
| Expr_appl of call_t |
105 |
|
106 |
and call_t = ident * expr * expr option |
107 |
(* The third part denotes the boolean condition for resetting *) |
108 |
|
109 |
and eq = |
110 |
{eq_lhs: ident list; |
111 |
eq_rhs: expr; |
112 |
eq_loc: Location.t} |
113 |
|
114 |
(* The tag of an expression is a unique identifier used to distinguish |
115 |
different instances of the same node *) |
116 |
and eexpr = |
117 |
{eexpr_tag: tag; |
118 |
eexpr_qfexpr: expr; |
119 |
eexpr_quantifiers: (quantifier_type * var_decl list) list; |
120 |
mutable eexpr_type: Types.type_expr; |
121 |
mutable eexpr_clock: Clocks.clock_expr; |
122 |
mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; |
123 |
eexpr_loc: Location.t} |
124 |
|
125 |
and expr_annot = |
126 |
{annots: (string list * eexpr) list; |
127 |
annot_loc: Location.t} |
128 |
|
129 |
type node_annot = { |
130 |
requires: eexpr list; |
131 |
ensures: eexpr list; |
132 |
behaviors: (string * eexpr list * eexpr list * Location.t) list; |
133 |
spec_loc: Location.t; |
134 |
} |
135 |
|
136 |
type offset = |
137 |
| Index of Dimension.dim_expr |
138 |
| Field of label |
139 |
|
140 |
type assert_t = |
141 |
{ |
142 |
assert_expr: expr; |
143 |
assert_loc: Location.t; |
144 |
} |
145 |
|
146 |
type statement = |
147 |
| Eq of eq |
148 |
| Aut of automata_desc |
149 |
|
150 |
and automata_desc = |
151 |
{aut_id : ident; |
152 |
aut_handlers: handler_desc list; |
153 |
aut_loc: Location.t} |
154 |
|
155 |
and handler_desc = |
156 |
{hand_state: ident; |
157 |
hand_unless: (Location.t * expr * bool * ident) list; |
158 |
hand_until: (Location.t * expr * bool * ident) list; |
159 |
hand_locals: var_decl list; |
160 |
hand_stmts: statement list; |
161 |
hand_asserts: assert_t list; |
162 |
hand_annots: expr_annot list; |
163 |
hand_loc: Location.t} |
164 |
|
165 |
type node_desc = |
166 |
{node_id: ident; |
167 |
mutable node_type: Types.type_expr; |
168 |
mutable node_clock: Clocks.clock_expr; |
169 |
node_inputs: var_decl list; |
170 |
node_outputs: var_decl list; |
171 |
node_locals: var_decl list; |
172 |
mutable node_gencalls: expr list; |
173 |
mutable node_checks: Dimension.dim_expr list; |
174 |
node_asserts: assert_t list; |
175 |
node_stmts: statement list; |
176 |
mutable node_dec_stateless: bool; |
177 |
mutable node_stateless: bool option; |
178 |
node_spec: node_annot option; |
179 |
node_annot: expr_annot list; |
180 |
} |
181 |
|
182 |
type imported_node_desc = |
183 |
{nodei_id: ident; |
184 |
mutable nodei_type: Types.type_expr; |
185 |
mutable nodei_clock: Clocks.clock_expr; |
186 |
nodei_inputs: var_decl list; |
187 |
nodei_outputs: var_decl list; |
188 |
nodei_stateless: bool; |
189 |
nodei_spec: node_annot option; |
190 |
nodei_prototype: string option; |
191 |
nodei_in_lib: string option; |
192 |
} |
193 |
|
194 |
type const_desc = |
195 |
{const_id: ident; |
196 |
const_loc: Location.t; |
197 |
const_value: constant; |
198 |
mutable const_type: Types.type_expr; |
199 |
} |
200 |
|
201 |
type top_decl_desc = |
202 |
| Node of node_desc |
203 |
| Const of const_desc |
204 |
| ImportedNode of imported_node_desc |
205 |
| Open of bool * string (* the boolean set to true denotes a local |
206 |
lusi vs a lusi installed at system level *) |
207 |
| TypeDef of typedef_desc |
208 |
|
209 |
type top_decl = |
210 |
{top_decl_desc: top_decl_desc; (* description of the symbol *) |
211 |
top_decl_owner: Location.filename; (* the module where it is defined *) |
212 |
top_decl_itf: bool; (* header or source file ? *) |
213 |
top_decl_loc: Location.t} (* the location where it is defined *) |
214 |
|
215 |
type program = top_decl list |
216 |
|
217 |
type dep_t = Dep of |
218 |
bool |
219 |
* ident |
220 |
* (top_decl list) |
221 |
* bool (* is stateful *) |
222 |
|
223 |
type error = |
224 |
Main_not_found |
225 |
| Main_wrong_kind |
226 |
| No_main_specified |
227 |
| Unbound_symbol of ident |
228 |
| Already_bound_symbol of ident |
229 |
| Unknown_library of ident |
230 |
| Wrong_number of ident |
231 |
|
232 |
(* Local Variables: *) |
233 |
(* compile-command:"make -C .." *) |
234 |
(* End: *) |