lustrec / src / corelang.ml @ 52cfee34
History | View | Annotate | Download (26.8 KB)
1 |
(* ---------------------------------------------------------------------------- |
---|---|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
3 |
* Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
4 |
* |
5 |
* This file is part of Prelude |
6 |
* |
7 |
* Prelude is free software; you can redistribute it and/or |
8 |
* modify it under the terms of the GNU Lesser General Public License |
9 |
* as published by the Free Software Foundation ; either version 2 of |
10 |
* the License, or (at your option) any later version. |
11 |
* |
12 |
* Prelude is distributed in the hope that it will be useful, but |
13 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
14 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
15 |
* Lesser General Public License for more details. |
16 |
* |
17 |
* You should have received a copy of the GNU Lesser General Public |
18 |
* License along with this program ; if not, write to the Free Software |
19 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
20 |
* USA |
21 |
*---------------------------------------------------------------------------- *) |
22 |
open Format |
23 |
open LustreSpec |
24 |
open Dimension |
25 |
|
26 |
(** The core language and its ast. Every element of the ast contains its |
27 |
location in the program text. The type and clock of an ast element |
28 |
is mutable (and initialized to dummy values). This avoids to have to |
29 |
duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *) |
30 |
|
31 |
type ident = Utils.ident |
32 |
type label = Utils.ident |
33 |
type rat = Utils.rat |
34 |
type tag = Utils.tag |
35 |
|
36 |
type constant = |
37 |
| Const_int of int |
38 |
| Const_real of string |
39 |
| Const_float of float |
40 |
| Const_array of constant list |
41 |
| Const_tag of label |
42 |
| Const_struct of (label * constant) list |
43 |
|
44 |
type type_dec = LustreSpec.type_dec |
45 |
|
46 |
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc} |
47 |
|
48 |
|
49 |
type clock_dec = LustreSpec.clock_dec |
50 |
|
51 |
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc} |
52 |
|
53 |
type var_decl = LustreSpec.var_decl |
54 |
|
55 |
(* The tag of an expression is a unique identifier used to distinguish |
56 |
different instances of the same node *) |
57 |
type expr = |
58 |
{expr_tag: tag; |
59 |
expr_desc: expr_desc; |
60 |
mutable expr_type: Types.type_expr; |
61 |
mutable expr_clock: Clocks.clock_expr; |
62 |
mutable expr_delay: Delay.delay_expr; |
63 |
mutable expr_annot: LustreSpec.expr_annot option; |
64 |
expr_loc: Location.t} |
65 |
|
66 |
and expr_desc = |
67 |
| Expr_const of constant |
68 |
| Expr_ident of ident |
69 |
| Expr_tuple of expr list |
70 |
| Expr_ite of expr * expr * expr |
71 |
| Expr_arrow of expr * expr |
72 |
| Expr_fby of expr * expr |
73 |
| Expr_array of expr list |
74 |
| Expr_access of expr * Dimension.dim_expr |
75 |
| Expr_power of expr * Dimension.dim_expr |
76 |
| Expr_pre of expr |
77 |
| Expr_when of expr * ident * label |
78 |
| Expr_merge of ident * (label * expr) list |
79 |
| Expr_appl of call_t |
80 |
| Expr_uclock of expr * int |
81 |
| Expr_dclock of expr * int |
82 |
| Expr_phclock of expr * rat |
83 |
and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *) |
84 |
|
85 |
type eq = |
86 |
{eq_lhs: ident list; |
87 |
eq_rhs: expr; |
88 |
eq_loc: Location.t} |
89 |
|
90 |
type assert_t = |
91 |
{ |
92 |
assert_expr: expr; |
93 |
assert_loc: Location.t |
94 |
} |
95 |
|
96 |
type node_desc = |
97 |
{node_id: ident; |
98 |
mutable node_type: Types.type_expr; |
99 |
mutable node_clock: Clocks.clock_expr; |
100 |
node_inputs: var_decl list; |
101 |
node_outputs: var_decl list; |
102 |
node_locals: var_decl list; |
103 |
mutable node_gencalls: expr list; |
104 |
mutable node_checks: Dimension.dim_expr list; |
105 |
node_asserts: assert_t list; |
106 |
node_eqs: eq list; |
107 |
node_dec_stateless: bool; |
108 |
mutable node_stateless: bool option; |
109 |
node_spec: LustreSpec.node_annot option; |
110 |
node_annot: LustreSpec.expr_annot option; |
111 |
} |
112 |
|
113 |
type imported_node_desc = |
114 |
{nodei_id: ident; |
115 |
mutable nodei_type: Types.type_expr; |
116 |
mutable nodei_clock: Clocks.clock_expr; |
117 |
nodei_inputs: var_decl list; |
118 |
nodei_outputs: var_decl list; |
119 |
nodei_stateless: bool; |
120 |
nodei_spec: LustreSpec.node_annot option; |
121 |
} |
122 |
|
123 |
type const_desc = |
124 |
{const_id: ident; |
125 |
const_loc: Location.t; |
126 |
const_value: constant; |
127 |
mutable const_type: Types.type_expr; |
128 |
} |
129 |
|
130 |
type top_decl_desc = |
131 |
| Node of node_desc |
132 |
| Consts of const_desc list |
133 |
| ImportedNode of imported_node_desc |
134 |
| Open of string |
135 |
|
136 |
type top_decl = |
137 |
{top_decl_desc: top_decl_desc; |
138 |
top_decl_loc: Location.t} |
139 |
|
140 |
type program = top_decl list |
141 |
|
142 |
type error = |
143 |
Main_not_found |
144 |
| Main_wrong_kind |
145 |
| No_main_specified |
146 |
| Unbound_symbol of ident |
147 |
| Already_bound_symbol of ident |
148 |
| Stateful of ident |
149 |
|
150 |
exception Error of Location.t * error |
151 |
|
152 |
module VDeclModule = |
153 |
struct (* Node module *) |
154 |
type t = var_decl |
155 |
let compare v1 v2 = compare v1 v2 |
156 |
let hash n = Hashtbl.hash n |
157 |
let equal n1 n2 = n1 = n2 |
158 |
end |
159 |
|
160 |
module VMap = Map.Make(VDeclModule) |
161 |
|
162 |
module VSet = Set.Make(VDeclModule) |
163 |
|
164 |
(************************************************************) |
165 |
(* *) |
166 |
|
167 |
let mktyp loc d = |
168 |
{ ty_dec_desc = d; ty_dec_loc = loc } |
169 |
|
170 |
let mkclock loc d = |
171 |
{ ck_dec_desc = d; ck_dec_loc = loc } |
172 |
|
173 |
let mkvar_decl loc (id, ty_dec, ck_dec, is_const) = |
174 |
{ var_id = id; |
175 |
var_dec_type = ty_dec; |
176 |
var_dec_clock = ck_dec; |
177 |
var_dec_const = is_const; |
178 |
var_type = Types.new_var (); |
179 |
var_clock = Clocks.new_var true; |
180 |
var_loc = loc } |
181 |
|
182 |
let mkexpr loc d = |
183 |
{ expr_tag = Utils.new_tag (); |
184 |
expr_desc = d; |
185 |
expr_type = Types.new_var (); |
186 |
expr_clock = Clocks.new_var true; |
187 |
expr_delay = Delay.new_var (); |
188 |
expr_annot = None; |
189 |
expr_loc = loc } |
190 |
|
191 |
let var_decl_of_const c = |
192 |
{ var_id = c.const_id; |
193 |
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any }; |
194 |
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any }; |
195 |
var_dec_const = true; |
196 |
var_type = c.const_type; |
197 |
var_clock = Clocks.new_var false; |
198 |
var_loc = c.const_loc } |
199 |
|
200 |
let mk_new_name vdecl_list id = |
201 |
let rec new_name name cpt = |
202 |
if List.exists (fun v -> v.var_id = name) vdecl_list |
203 |
then new_name (sprintf "_%s_%i" id cpt) (cpt+1) |
204 |
else name |
205 |
in new_name id 1 |
206 |
|
207 |
let update_expr_annot e annot = |
208 |
{ e with expr_annot = LustreSpec.merge_expr_annot e.expr_annot (Some annot) } |
209 |
|
210 |
let mkeq loc (lhs, rhs) = |
211 |
{ eq_lhs = lhs; |
212 |
eq_rhs = rhs; |
213 |
eq_loc = loc } |
214 |
|
215 |
let mkassert loc expr = |
216 |
{ assert_loc = loc; |
217 |
assert_expr = expr |
218 |
} |
219 |
|
220 |
let mktop_decl loc d = |
221 |
{ top_decl_desc = d; top_decl_loc = loc } |
222 |
|
223 |
let mkpredef_call loc funname args = |
224 |
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None)) |
225 |
|
226 |
let mkpredef_unary_call loc funname arg = |
227 |
mkexpr loc (Expr_appl (funname, arg, None)) |
228 |
|
229 |
|
230 |
(***********************************************************) |
231 |
(* Fast access to nodes, by name *) |
232 |
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30 |
233 |
let consts_table = Hashtbl.create 30 |
234 |
|
235 |
let node_name td = |
236 |
match td.top_decl_desc with |
237 |
| Node nd -> nd.node_id |
238 |
| ImportedNode nd -> nd.nodei_id |
239 |
| _ -> assert false |
240 |
|
241 |
let is_generic_node td = |
242 |
match td.top_decl_desc with |
243 |
| Node nd -> List.exists (fun v -> v.var_dec_const) nd.node_inputs |
244 |
| ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs |
245 |
| _ -> assert false |
246 |
|
247 |
let node_inputs td = |
248 |
match td.top_decl_desc with |
249 |
| Node nd -> nd.node_inputs |
250 |
| ImportedNode nd -> nd.nodei_inputs |
251 |
| _ -> assert false |
252 |
|
253 |
let node_from_name id = |
254 |
try |
255 |
Hashtbl.find node_table id |
256 |
with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id; |
257 |
assert false) |
258 |
|
259 |
let is_imported_node td = |
260 |
match td.top_decl_desc with |
261 |
| Node nd -> false |
262 |
| ImportedNode nd -> true |
263 |
| _ -> assert false |
264 |
|
265 |
let rec is_stateless_expr expr = |
266 |
match expr.expr_desc with |
267 |
| Expr_const _ |
268 |
| Expr_ident _ -> true |
269 |
| Expr_tuple el |
270 |
| Expr_array el -> List.for_all is_stateless_expr el |
271 |
| Expr_access (e1, _) |
272 |
| Expr_power (e1, _) -> is_stateless_expr e1 |
273 |
| Expr_ite (c, t, e) -> is_stateless_expr c && is_stateless_expr t && is_stateless_expr e |
274 |
| Expr_arrow (e1, e2) |
275 |
| Expr_fby (e1, e2) -> is_stateless_expr e1 && is_stateless_expr e2 |
276 |
| Expr_pre e' -> is_stateless_expr e' |
277 |
| Expr_when (e', i, l)-> is_stateless_expr e' |
278 |
| Expr_merge (i, hl) -> List.for_all (fun (t, h) -> is_stateless_expr h) hl |
279 |
| Expr_appl (i, e', i') -> |
280 |
is_stateless_expr e' && |
281 |
(Basic_library.is_internal_fun i || check_stateless_node (node_from_name i)) |
282 |
| Expr_uclock _ |
283 |
| Expr_dclock _ |
284 |
| Expr_phclock _ -> assert false |
285 |
and compute_stateless_node nd = |
286 |
List.for_all (fun eq -> is_stateless_expr eq.eq_rhs) nd.node_eqs |
287 |
and check_stateless_node td = |
288 |
match td.top_decl_desc with |
289 |
| Node nd -> ( |
290 |
match nd.node_stateless with |
291 |
| None -> |
292 |
begin |
293 |
let stateless = compute_stateless_node nd in |
294 |
nd.node_stateless <- Some (false && stateless); |
295 |
if nd.node_dec_stateless && (not stateless) |
296 |
then raise (Error (td.top_decl_loc, Stateful nd.node_id)) |
297 |
else stateless |
298 |
end |
299 |
| Some stl -> stl) |
300 |
| ImportedNode nd -> nd.nodei_stateless |
301 |
| _ -> true |
302 |
|
303 |
(* alias and type definition table *) |
304 |
let type_table = |
305 |
Utils.create_hashtable 20 [ |
306 |
Tydec_int , Tydec_int; |
307 |
Tydec_bool , Tydec_bool; |
308 |
Tydec_float, Tydec_float; |
309 |
Tydec_real , Tydec_real |
310 |
] |
311 |
|
312 |
let rec is_user_type typ = |
313 |
match typ with |
314 |
| Tydec_int | Tydec_bool | Tydec_real |
315 |
| Tydec_float | Tydec_any | Tydec_const _ -> false |
316 |
| Tydec_clock typ' -> is_user_type typ' |
317 |
| _ -> true |
318 |
|
319 |
let get_repr_type typ = |
320 |
let typ_def = Hashtbl.find type_table typ in |
321 |
if is_user_type typ_def then typ else typ_def |
322 |
|
323 |
let tag_true = "true" |
324 |
let tag_false = "false" |
325 |
|
326 |
let const_is_bool c = |
327 |
match c with |
328 |
| Const_tag t -> t = tag_true || t = tag_false |
329 |
| _ -> false |
330 |
|
331 |
(* Computes the negation of a boolean constant *) |
332 |
let const_negation c = |
333 |
assert (const_is_bool c); |
334 |
match c with |
335 |
| Const_tag t when t = tag_true -> Const_tag tag_false |
336 |
| _ -> Const_tag tag_true |
337 |
|
338 |
let const_or c1 c2 = |
339 |
assert (const_is_bool c1 && const_is_bool c2); |
340 |
match c1, c2 with |
341 |
| Const_tag t1, _ when t1 = tag_true -> c1 |
342 |
| _ , Const_tag t2 when t2 = tag_true -> c2 |
343 |
| _ -> Const_tag tag_false |
344 |
|
345 |
let const_and c1 c2 = |
346 |
assert (const_is_bool c1 && const_is_bool c2); |
347 |
match c1, c2 with |
348 |
| Const_tag t1, _ when t1 = tag_false -> c1 |
349 |
| _ , Const_tag t2 when t2 = tag_false -> c2 |
350 |
| _ -> Const_tag tag_true |
351 |
|
352 |
let const_xor c1 c2 = |
353 |
assert (const_is_bool c1 && const_is_bool c2); |
354 |
match c1, c2 with |
355 |
| Const_tag t1, Const_tag t2 when t1 <> t2 -> Const_tag tag_true |
356 |
| _ -> Const_tag tag_false |
357 |
|
358 |
let const_impl c1 c2 = |
359 |
assert (const_is_bool c1 && const_is_bool c2); |
360 |
match c1, c2 with |
361 |
| Const_tag t1, _ when t1 = tag_false -> Const_tag tag_true |
362 |
| _ , Const_tag t2 when t2 = tag_true -> Const_tag tag_true |
363 |
| _ -> Const_tag tag_false |
364 |
|
365 |
(* To guarantee uniqueness of tags in enum types *) |
366 |
let tag_table = |
367 |
Utils.create_hashtable 20 [ |
368 |
tag_true, Tydec_bool; |
369 |
tag_false, Tydec_bool |
370 |
] |
371 |
|
372 |
(* To guarantee uniqueness of fields in struct types *) |
373 |
let field_table = |
374 |
Utils.create_hashtable 20 [ |
375 |
] |
376 |
|
377 |
let get_enum_type_tags cty = |
378 |
match cty with |
379 |
| Tydec_bool -> [tag_true; tag_false] |
380 |
| Tydec_const _ -> (match Hashtbl.find type_table cty with |
381 |
| Tydec_enum tl -> tl |
382 |
| _ -> assert false) |
383 |
| _ -> assert false |
384 |
|
385 |
let get_struct_type_fields cty = |
386 |
match cty with |
387 |
| Tydec_const _ -> (match Hashtbl.find type_table cty with |
388 |
| Tydec_struct fl -> fl |
389 |
| _ -> assert false) |
390 |
| _ -> assert false |
391 |
|
392 |
let const_of_bool b = |
393 |
Const_tag (if b then tag_true else tag_false) |
394 |
|
395 |
(* let get_const c = snd (Hashtbl.find consts_table c) *) |
396 |
|
397 |
(* Caution, returns an untyped and unclocked expression *) |
398 |
let expr_of_ident id loc = |
399 |
{expr_tag = Utils.new_tag (); |
400 |
expr_desc = Expr_ident id; |
401 |
expr_type = Types.new_var (); |
402 |
expr_clock = Clocks.new_var true; |
403 |
expr_delay = Delay.new_var (); |
404 |
expr_loc = loc; |
405 |
expr_annot = None} |
406 |
|
407 |
let expr_list_of_expr expr = |
408 |
match expr.expr_desc with |
409 |
| Expr_tuple elist -> |
410 |
elist |
411 |
| _ -> [expr] |
412 |
|
413 |
let expr_of_expr_list loc elist = |
414 |
match elist with |
415 |
| [t] -> { t with expr_loc = loc } |
416 |
| t::_ -> { t with expr_desc = Expr_tuple elist; expr_loc = loc } |
417 |
| _ -> assert false |
418 |
|
419 |
let call_of_expr expr = |
420 |
match expr.expr_desc with |
421 |
| Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r) |
422 |
| _ -> assert false |
423 |
|
424 |
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *) |
425 |
let rec expr_of_dimension dim = |
426 |
match dim.dim_desc with |
427 |
| Dbool b -> |
428 |
mkexpr dim.dim_loc (Expr_const (const_of_bool b)) |
429 |
| Dint i -> |
430 |
mkexpr dim.dim_loc (Expr_const (Const_int i)) |
431 |
| Dident id -> |
432 |
mkexpr dim.dim_loc (Expr_ident id) |
433 |
| Dite (c, t, e) -> |
434 |
mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e)) |
435 |
| Dappl (id, args) -> |
436 |
mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None)) |
437 |
| Dlink dim' -> expr_of_dimension dim' |
438 |
| Dvar |
439 |
| Dunivar -> (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim; |
440 |
assert false) |
441 |
|
442 |
let dimension_of_const loc const = |
443 |
match const with |
444 |
| Const_int i -> mkdim_int loc i |
445 |
| Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true) |
446 |
| _ -> raise InvalidDimension |
447 |
|
448 |
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments |
449 |
into dimension expressions *) |
450 |
let rec dimension_of_expr expr = |
451 |
match expr.expr_desc with |
452 |
| Expr_const c -> dimension_of_const expr.expr_loc c |
453 |
| Expr_ident id -> mkdim_ident expr.expr_loc id |
454 |
| Expr_appl (f, args, None) when Basic_library.is_internal_fun f -> |
455 |
let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in |
456 |
if k = None then raise InvalidDimension; |
457 |
mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args)) |
458 |
| Expr_ite (i, t, e) -> |
459 |
mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e) |
460 |
| _ -> raise InvalidDimension (* not a simple dimension expression *) |
461 |
|
462 |
|
463 |
let sort_handlers hl = |
464 |
List.sort (fun (t, _) (t', _) -> compare t t') hl |
465 |
|
466 |
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with |
467 |
| Expr_const c1, Expr_const c2 -> c1 = c2 |
468 |
| Expr_ident i1, Expr_ident i2 -> i1 = i2 |
469 |
| Expr_array el1, Expr_array el2 |
470 |
| Expr_tuple el1, Expr_tuple el2 -> |
471 |
List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 |
472 |
| Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' |
473 |
| Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' |
474 |
| Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2 |
475 |
(* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *) |
476 |
(* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *) |
477 |
| Expr_pre e, Expr_pre e' -> is_eq_expr e e' |
478 |
| Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e' |
479 |
| Expr_merge(i, hl), Expr_merge(i', hl') -> i=i' && List.for_all2 (fun (t, h) (t', h') -> t=t' && is_eq_expr h h') (sort_handlers hl) (sort_handlers hl') |
480 |
| Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e' |
481 |
| Expr_uclock(e, i), Expr_uclock(e', i') -> i=i' && is_eq_expr e e' |
482 |
| Expr_dclock(e, i), Expr_dclock(e', i') -> i=i' && is_eq_expr e e' |
483 |
| Expr_phclock(e, r), Expr_phclock(e', r') -> r=r' && is_eq_expr e e' |
484 |
| Expr_power (e1, i1), Expr_power (e2, i2) |
485 |
| Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2) |
486 |
| _ -> false |
487 |
|
488 |
let node_vars nd = |
489 |
nd.node_inputs @ nd.node_locals @ nd.node_outputs |
490 |
|
491 |
let node_var id node = |
492 |
List.find (fun v -> v.var_id = id) (node_vars node) |
493 |
|
494 |
let node_eq id node = |
495 |
List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs |
496 |
|
497 |
(* Consts unfoooolding *) |
498 |
let is_const i consts = |
499 |
List.exists (fun c -> c.const_id = i) consts |
500 |
|
501 |
let get_const i consts = |
502 |
let c = List.find (fun c -> c.const_id = i) consts in |
503 |
c.const_value |
504 |
|
505 |
let rec expr_unfold_consts consts e = |
506 |
{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc } |
507 |
|
508 |
and expr_desc_unfold_consts consts e = |
509 |
let unfold = expr_unfold_consts consts in |
510 |
match e with |
511 |
| Expr_const _ -> e |
512 |
| Expr_ident i -> if is_const i consts then Expr_const (get_const i consts) else e |
513 |
| Expr_array el -> Expr_array (List.map unfold el) |
514 |
| Expr_access (e1, d) -> Expr_access (unfold e1, d) |
515 |
| Expr_power (e1, d) -> Expr_power (unfold e1, d) |
516 |
| Expr_tuple el -> Expr_tuple (List.map unfold el) |
517 |
| Expr_ite (c, t, e) -> Expr_ite (unfold c, unfold t, unfold e) |
518 |
| Expr_arrow (e1, e2)-> Expr_arrow (unfold e1, unfold e2) |
519 |
| Expr_fby (e1, e2) -> Expr_fby (unfold e1, unfold e2) |
520 |
(* | Expr_concat (e1, e2) -> Expr_concat (unfold e1, unfold e2) *) |
521 |
(* | Expr_tail e' -> Expr_tail (unfold e') *) |
522 |
| Expr_pre e' -> Expr_pre (unfold e') |
523 |
| Expr_when (e', i, l)-> Expr_when (unfold e', i, l) |
524 |
| Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, unfold h)) hl) |
525 |
| Expr_appl (i, e', i') -> Expr_appl (i, unfold e', i') |
526 |
| Expr_uclock (e', i) -> Expr_uclock (unfold e', i) |
527 |
| Expr_dclock (e', i) -> Expr_dclock (unfold e', i) |
528 |
| Expr_phclock _ -> e |
529 |
|
530 |
let eq_unfold_consts consts eq = |
531 |
{ eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs } |
532 |
|
533 |
let node_unfold_consts consts node = |
534 |
{ node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs } |
535 |
|
536 |
let get_consts prog = |
537 |
List.fold_left ( |
538 |
fun consts decl -> |
539 |
match decl.top_decl_desc with |
540 |
| Consts clist -> clist@consts |
541 |
| Node _ | ImportedNode _ | Open _ -> consts |
542 |
) [] prog |
543 |
|
544 |
|
545 |
let get_nodes prog = |
546 |
List.fold_left ( |
547 |
fun nodes decl -> |
548 |
match decl.top_decl_desc with |
549 |
| Node nd -> nd::nodes |
550 |
| Consts _ | ImportedNode _ | Open _ -> nodes |
551 |
) [] prog |
552 |
|
553 |
let prog_unfold_consts prog = |
554 |
let consts = get_consts prog in |
555 |
List.map ( |
556 |
fun decl -> match decl.top_decl_desc with |
557 |
| Node nd -> {decl with top_decl_desc = Node (node_unfold_consts consts nd)} |
558 |
| _ -> decl |
559 |
) prog |
560 |
|
561 |
|
562 |
|
563 |
(************************************************************************) |
564 |
(* Renaming *) |
565 |
|
566 |
(* applies the renaming function [fvar] to all variables of expression [expr] *) |
567 |
let rec expr_replace_var fvar expr = |
568 |
{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } |
569 |
|
570 |
and expr_desc_replace_var fvar expr_desc = |
571 |
match expr_desc with |
572 |
| Expr_const _ -> expr_desc |
573 |
| Expr_ident i -> Expr_ident (fvar i) |
574 |
| Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) |
575 |
| Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) |
576 |
| Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) |
577 |
| Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) |
578 |
| Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) |
579 |
| Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) |
580 |
| Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) |
581 |
| Expr_pre e' -> Expr_pre (expr_replace_var fvar e') |
582 |
| Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) |
583 |
| Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) |
584 |
| Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) -> fvar x, l) i') |
585 |
| _ -> assert false |
586 |
|
587 |
(* Applies the renaming function [fvar] to every rhs |
588 |
only when the corresponding lhs satisfies predicate [pvar] *) |
589 |
let eq_replace_rhs_var pvar fvar eq = |
590 |
let pvar l = List.exists pvar l in |
591 |
let rec replace lhs rhs = |
592 |
{ rhs with expr_desc = replace_desc lhs rhs.expr_desc } |
593 |
and replace_desc lhs rhs_desc = |
594 |
match lhs with |
595 |
| [] -> assert false |
596 |
| [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc |
597 |
| _ -> |
598 |
(match rhs_desc with |
599 |
| Expr_tuple tl -> |
600 |
Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl) |
601 |
| Expr_appl (f, arg, None) when Basic_library.is_internal_fun f -> |
602 |
let args = expr_list_of_expr arg in |
603 |
Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None) |
604 |
| Expr_array _ |
605 |
| Expr_access _ |
606 |
| Expr_power _ |
607 |
| Expr_const _ |
608 |
| Expr_ident _ |
609 |
| Expr_appl _ -> |
610 |
if pvar lhs |
611 |
then expr_desc_replace_var fvar rhs_desc |
612 |
else rhs_desc |
613 |
| Expr_ite (c, t, e) -> Expr_ite (replace lhs c, replace lhs t, replace lhs e) |
614 |
| Expr_arrow (e1, e2) -> Expr_arrow (replace lhs e1, replace lhs e2) |
615 |
| Expr_fby (e1, e2) -> Expr_fby (replace lhs e1, replace lhs e2) |
616 |
| Expr_pre e' -> Expr_pre (replace lhs e') |
617 |
| Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i |
618 |
in Expr_when (replace lhs e', i', l) |
619 |
| Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i |
620 |
in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl) |
621 |
| _ -> assert false) |
622 |
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } |
623 |
|
624 |
|
625 |
let rec rename_expr f_node f_var f_const expr = |
626 |
{ expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc } |
627 |
and rename_expr_desc f_node f_var f_const expr_desc = |
628 |
let re = rename_expr f_node f_var f_const in |
629 |
match expr_desc with |
630 |
| Expr_const _ -> expr_desc |
631 |
| Expr_ident i -> Expr_ident (f_var i) |
632 |
| Expr_array el -> Expr_array (List.map re el) |
633 |
| Expr_access (e1, d) -> Expr_access (re e1, d) |
634 |
| Expr_power (e1, d) -> Expr_power (re e1, d) |
635 |
| Expr_tuple el -> Expr_tuple (List.map re el) |
636 |
| Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e) |
637 |
| Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) |
638 |
| Expr_fby (e1, e2) -> Expr_fby (re e1, re e2) |
639 |
| Expr_pre e' -> Expr_pre (re e') |
640 |
| Expr_when (e', i, l)-> Expr_when (re e', f_var i, l) |
641 |
| Expr_merge (i, hl) -> |
642 |
Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl) |
643 |
| Expr_appl (i, e', i') -> |
644 |
Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i') |
645 |
| _ -> assert false |
646 |
|
647 |
let rename_node_annot f_node f_var f_const expr = |
648 |
expr |
649 |
(* TODO assert false *) |
650 |
|
651 |
let rename_expr_annot f_node f_var f_const annot = |
652 |
annot |
653 |
(* TODO assert false *) |
654 |
|
655 |
let rename_node f_node f_var f_const nd = |
656 |
let rename_var v = { v with var_id = f_var v.var_id } in |
657 |
let inputs = List.map rename_var nd.node_inputs in |
658 |
let outputs = List.map rename_var nd.node_outputs in |
659 |
let locals = List.map rename_var nd.node_locals in |
660 |
let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in |
661 |
let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in |
662 |
let node_asserts = List.map |
663 |
(fun a -> |
664 |
{ a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } |
665 |
) nd.node_asserts |
666 |
in |
667 |
let eqs = List.map |
668 |
(fun eq -> { eq with |
669 |
eq_lhs = List.map f_var eq.eq_lhs; |
670 |
eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs |
671 |
} ) nd.node_eqs |
672 |
in |
673 |
let spec = |
674 |
Utils.option_map |
675 |
(fun s -> rename_node_annot f_node f_var f_const s) |
676 |
nd.node_spec |
677 |
in |
678 |
let annot = |
679 |
Utils.option_map |
680 |
(fun s -> rename_expr_annot f_node f_var f_const s) |
681 |
nd.node_annot |
682 |
in |
683 |
{ |
684 |
node_id = f_node nd.node_id; |
685 |
node_type = nd.node_type; |
686 |
node_clock = nd.node_clock; |
687 |
node_inputs = inputs; |
688 |
node_outputs = outputs; |
689 |
node_locals = locals; |
690 |
node_gencalls = gen_calls; |
691 |
node_checks = node_checks; |
692 |
node_asserts = node_asserts; |
693 |
node_eqs = eqs; |
694 |
node_dec_stateless = nd.node_dec_stateless; |
695 |
node_stateless = nd.node_stateless; |
696 |
node_spec = spec; |
697 |
node_annot = annot; |
698 |
} |
699 |
|
700 |
|
701 |
let rename_const f_const c = |
702 |
{ c with const_id = f_const c.const_id } |
703 |
|
704 |
let rename_prog f_node f_var f_const prog = |
705 |
List.rev ( |
706 |
List.fold_left (fun accu top -> |
707 |
(match top.top_decl_desc with |
708 |
| Node nd -> |
709 |
{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) } |
710 |
| Consts c -> |
711 |
{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) } |
712 |
| ImportedNode _ |
713 |
| Open _ -> top) |
714 |
::accu |
715 |
) [] prog |
716 |
) |
717 |
|
718 |
(**********************************************************************) |
719 |
(* Pretty printers *) |
720 |
|
721 |
let pp_decl_type fmt tdecl = |
722 |
match tdecl.top_decl_desc with |
723 |
| Node nd -> |
724 |
fprintf fmt "%s: " nd.node_id; |
725 |
Utils.reset_names (); |
726 |
fprintf fmt "%a@ " Types.print_ty nd.node_type |
727 |
| ImportedNode ind -> |
728 |
fprintf fmt "%s: " ind.nodei_id; |
729 |
Utils.reset_names (); |
730 |
fprintf fmt "%a@ " Types.print_ty ind.nodei_type |
731 |
| Consts _ | Open _ -> () |
732 |
|
733 |
let pp_prog_type fmt tdecl_list = |
734 |
Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list |
735 |
|
736 |
let pp_decl_clock fmt cdecl = |
737 |
match cdecl.top_decl_desc with |
738 |
| Node nd -> |
739 |
fprintf fmt "%s: " nd.node_id; |
740 |
Utils.reset_names (); |
741 |
fprintf fmt "%a@ " Clocks.print_ck nd.node_clock |
742 |
| ImportedNode ind -> |
743 |
fprintf fmt "%s: " ind.nodei_id; |
744 |
Utils.reset_names (); |
745 |
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock |
746 |
| Consts _ | Open _ -> () |
747 |
|
748 |
let pp_prog_clock fmt prog = |
749 |
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog |
750 |
|
751 |
let pp_error fmt = function |
752 |
Main_not_found -> |
753 |
fprintf fmt "Cannot compile node %s: could not find the node definition.@." |
754 |
!Options.main_node |
755 |
| Main_wrong_kind -> |
756 |
fprintf fmt |
757 |
"Name %s does not correspond to a (non-imported) node definition.@." |
758 |
!Options.main_node |
759 |
| No_main_specified -> |
760 |
fprintf fmt "No main node specified@." |
761 |
| Unbound_symbol sym -> |
762 |
fprintf fmt |
763 |
"%s is undefined.@." |
764 |
sym |
765 |
| Already_bound_symbol sym -> |
766 |
fprintf fmt |
767 |
"%s is already defined.@." |
768 |
sym |
769 |
| Stateful nd -> |
770 |
fprintf fmt |
771 |
"node %s is declared stateless, but it is stateful.@." |
772 |
nd |
773 |
|
774 |
(* filling node table with internal functions *) |
775 |
let vdecls_of_typ_ck cpt ty = |
776 |
let loc = Location.dummy_loc in |
777 |
List.map |
778 |
(fun _ -> incr cpt; |
779 |
let name = sprintf "_var_%d" !cpt in |
780 |
mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false)) |
781 |
(Types.type_list_of_type ty) |
782 |
|
783 |
let mk_internal_node id = |
784 |
let spec = None in |
785 |
let ty = Env.lookup_value Basic_library.type_env id in |
786 |
let ck = Env.lookup_value Basic_library.clock_env id in |
787 |
let (tin, tout) = Types.split_arrow ty in |
788 |
(*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*) |
789 |
let cpt = ref (-1) in |
790 |
mktop_decl Location.dummy_loc |
791 |
(ImportedNode |
792 |
{nodei_id = id; |
793 |
nodei_type = ty; |
794 |
nodei_clock = ck; |
795 |
nodei_inputs = vdecls_of_typ_ck cpt tin; |
796 |
nodei_outputs = vdecls_of_typ_ck cpt tout; |
797 |
nodei_stateless = Types.get_static_value ty <> None; |
798 |
nodei_spec = spec}) |
799 |
|
800 |
let add_internal_funs () = |
801 |
List.iter |
802 |
(fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd) |
803 |
Basic_library.internal_funs |
804 |
|
805 |
(* Local Variables: *) |
806 |
(* compile-command:"make -C .." *) |
807 |
(* End: *) |