lustrec / src / corelang.ml @ 2863281f
History | View | Annotate | Download (39.3 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 |
open Lustre_types |
14 |
open Machine_code_types |
15 |
(*open Dimension*) |
16 |
|
17 |
|
18 |
exception Error of Location.t * Error.error_kind |
19 |
|
20 |
module VDeclModule = |
21 |
struct (* Node module *) |
22 |
type t = var_decl |
23 |
let compare v1 v2 = compare v1.var_id v2.var_id |
24 |
end |
25 |
|
26 |
module VMap = Map.Make(VDeclModule) |
27 |
|
28 |
module VSet : Set.S with type elt = var_decl = Set.Make(VDeclModule) |
29 |
|
30 |
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc} |
31 |
|
32 |
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc} |
33 |
|
34 |
|
35 |
|
36 |
(************************************************************) |
37 |
(* *) |
38 |
|
39 |
let mktyp loc d = |
40 |
{ ty_dec_desc = d; ty_dec_loc = loc } |
41 |
|
42 |
let mkclock loc d = |
43 |
{ ck_dec_desc = d; ck_dec_loc = loc } |
44 |
|
45 |
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value, parentid) = |
46 |
assert (value = None || is_const); |
47 |
{ var_id = id; |
48 |
var_orig = orig; |
49 |
var_dec_type = ty_dec; |
50 |
var_dec_clock = ck_dec; |
51 |
var_dec_const = is_const; |
52 |
var_dec_value = value; |
53 |
var_parent_nodeid = parentid; |
54 |
var_type = Types.new_var (); |
55 |
var_clock = Clocks.new_var true; |
56 |
var_loc = loc } |
57 |
|
58 |
let dummy_var_decl name typ = |
59 |
{ |
60 |
var_id = name; |
61 |
var_orig = false; |
62 |
var_dec_type = dummy_type_dec; |
63 |
var_dec_clock = dummy_clock_dec; |
64 |
var_dec_const = false; |
65 |
var_dec_value = None; |
66 |
var_parent_nodeid = None; |
67 |
var_type = typ; |
68 |
var_clock = Clocks.new_ck Clocks.Cvar true; |
69 |
var_loc = Location.dummy_loc |
70 |
} |
71 |
|
72 |
let mkexpr loc d = |
73 |
{ expr_tag = Utils.new_tag (); |
74 |
expr_desc = d; |
75 |
expr_type = Types.new_var (); |
76 |
expr_clock = Clocks.new_var true; |
77 |
expr_delay = Delay.new_var (); |
78 |
expr_annot = None; |
79 |
expr_loc = loc } |
80 |
|
81 |
let var_decl_of_const ?(parentid=None) c = |
82 |
{ var_id = c.const_id; |
83 |
var_orig = true; |
84 |
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any }; |
85 |
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any }; |
86 |
var_dec_const = true; |
87 |
var_dec_value = None; |
88 |
var_parent_nodeid = parentid; |
89 |
var_type = c.const_type; |
90 |
var_clock = Clocks.new_var false; |
91 |
var_loc = c.const_loc } |
92 |
|
93 |
let mk_new_name used id = |
94 |
let rec new_name name cpt = |
95 |
if used name |
96 |
then new_name (sprintf "_%s_%i" id cpt) (cpt+1) |
97 |
else name |
98 |
in new_name id 1 |
99 |
|
100 |
let mkeq loc (lhs, rhs) = |
101 |
{ eq_lhs = lhs; |
102 |
eq_rhs = rhs; |
103 |
eq_loc = loc } |
104 |
|
105 |
let mkassert loc expr = |
106 |
{ assert_loc = loc; |
107 |
assert_expr = expr |
108 |
} |
109 |
|
110 |
let mktop_decl loc own itf d = |
111 |
{ top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf } |
112 |
|
113 |
let mkpredef_call loc funname args = |
114 |
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None)) |
115 |
|
116 |
let is_clock_dec_type cty = |
117 |
match cty with |
118 |
| Tydec_clock _ -> true |
119 |
| _ -> false |
120 |
|
121 |
let const_of_top top_decl = |
122 |
match top_decl.top_decl_desc with |
123 |
| Const c -> c |
124 |
| _ -> assert false |
125 |
|
126 |
let node_of_top top_decl = |
127 |
match top_decl.top_decl_desc with |
128 |
| Node nd -> nd |
129 |
| _ -> raise Not_found |
130 |
|
131 |
let imported_node_of_top top_decl = |
132 |
match top_decl.top_decl_desc with |
133 |
| ImportedNode ind -> ind |
134 |
| _ -> assert false |
135 |
|
136 |
let typedef_of_top top_decl = |
137 |
match top_decl.top_decl_desc with |
138 |
| TypeDef tdef -> tdef |
139 |
| _ -> assert false |
140 |
|
141 |
let dependency_of_top top_decl = |
142 |
match top_decl.top_decl_desc with |
143 |
| Open (local, dep) -> (local, dep) |
144 |
| _ -> assert false |
145 |
|
146 |
let consts_of_enum_type top_decl = |
147 |
match top_decl.top_decl_desc with |
148 |
| TypeDef tdef -> |
149 |
(match tdef.tydef_desc with |
150 |
| Tydec_enum tags -> |
151 |
List.map |
152 |
(fun tag -> |
153 |
let cdecl = { |
154 |
const_id = tag; |
155 |
const_loc = top_decl.top_decl_loc; |
156 |
const_value = Const_tag tag; |
157 |
const_type = Type_predef.type_const tdef.tydef_id |
158 |
} in |
159 |
{ top_decl with top_decl_desc = Const cdecl }) |
160 |
tags |
161 |
| _ -> []) |
162 |
| _ -> assert false |
163 |
|
164 |
(************************************************************) |
165 |
(* Eexpr functions *) |
166 |
(************************************************************) |
167 |
|
168 |
let merge_node_annot ann1 ann2 = |
169 |
{ requires = ann1.requires @ ann2.requires; |
170 |
ensures = ann1.ensures @ ann2.ensures; |
171 |
behaviors = ann1.behaviors @ ann2.behaviors; |
172 |
spec_loc = ann1.spec_loc |
173 |
} |
174 |
|
175 |
let mkeexpr loc expr = |
176 |
{ eexpr_tag = Utils.new_tag (); |
177 |
eexpr_qfexpr = expr; |
178 |
eexpr_quantifiers = []; |
179 |
eexpr_type = Types.new_var (); |
180 |
eexpr_clock = Clocks.new_var true; |
181 |
eexpr_normalized = None; |
182 |
eexpr_loc = loc } |
183 |
|
184 |
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers } |
185 |
|
186 |
(* |
187 |
let mkepredef_call loc funname args = |
188 |
mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None)) |
189 |
|
190 |
let mkepredef_unary_call loc funname arg = |
191 |
mkeexpr loc (EExpr_appl (funname, arg, None)) |
192 |
*) |
193 |
|
194 |
let merge_expr_annot ann1 ann2 = |
195 |
match ann1, ann2 with |
196 |
| None, None -> assert false |
197 |
| Some _, None -> ann1 |
198 |
| None, Some _ -> ann2 |
199 |
| Some ann1, Some ann2 -> Some { |
200 |
annots = ann1.annots @ ann2.annots; |
201 |
annot_loc = ann1.annot_loc |
202 |
} |
203 |
|
204 |
let update_expr_annot node_id e annot = |
205 |
List.iter (fun (key, _) -> |
206 |
Annotations.add_expr_ann node_id e.expr_tag key |
207 |
) annot.annots; |
208 |
e.expr_annot <- merge_expr_annot e.expr_annot (Some annot); |
209 |
e |
210 |
|
211 |
|
212 |
let mkinstr ?lustre_expr ?lustre_eq i = |
213 |
{ |
214 |
instr_desc = i; |
215 |
(* lustre_expr = lustre_expr; *) |
216 |
lustre_eq = lustre_eq; |
217 |
} |
218 |
|
219 |
let get_instr_desc i = i.instr_desc |
220 |
let update_instr_desc i id = { i with instr_desc = id } |
221 |
|
222 |
(***********************************************************) |
223 |
(* Fast access to nodes, by name *) |
224 |
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30 |
225 |
let consts_table = Hashtbl.create 30 |
226 |
|
227 |
let print_node_table fmt () = |
228 |
begin |
229 |
Format.fprintf fmt "{ /* node table */@."; |
230 |
Hashtbl.iter (fun id nd -> |
231 |
Format.fprintf fmt "%s |-> %a" |
232 |
id |
233 |
Printers.pp_short_decl nd |
234 |
) node_table; |
235 |
Format.fprintf fmt "}@." |
236 |
end |
237 |
|
238 |
let print_consts_table fmt () = |
239 |
begin |
240 |
Format.fprintf fmt "{ /* consts table */@."; |
241 |
Hashtbl.iter (fun id const -> |
242 |
Format.fprintf fmt "%s |-> %a" |
243 |
id |
244 |
Printers.pp_const_decl (const_of_top const) |
245 |
) consts_table; |
246 |
Format.fprintf fmt "}@." |
247 |
end |
248 |
|
249 |
let node_name td = |
250 |
match td.top_decl_desc with |
251 |
| Node nd -> nd.node_id |
252 |
| ImportedNode nd -> nd.nodei_id |
253 |
| _ -> assert false |
254 |
|
255 |
let is_generic_node td = |
256 |
match td.top_decl_desc with |
257 |
| Node nd -> List.exists (fun v -> v.var_dec_const) nd.node_inputs |
258 |
| ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs |
259 |
| _ -> assert false |
260 |
|
261 |
let node_inputs td = |
262 |
match td.top_decl_desc with |
263 |
| Node nd -> nd.node_inputs |
264 |
| ImportedNode nd -> nd.nodei_inputs |
265 |
| _ -> assert false |
266 |
|
267 |
let node_from_name id = |
268 |
try |
269 |
Hashtbl.find node_table id |
270 |
with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id; |
271 |
assert false) |
272 |
|
273 |
let is_imported_node td = |
274 |
match td.top_decl_desc with |
275 |
| Node nd -> false |
276 |
| ImportedNode nd -> true |
277 |
| _ -> assert false |
278 |
|
279 |
|
280 |
(* alias and type definition table *) |
281 |
|
282 |
let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false |
283 |
|
284 |
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int}) |
285 |
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool}) |
286 |
(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) *) |
287 |
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real}) |
288 |
|
289 |
let type_table = |
290 |
Utils.create_hashtable 20 [ |
291 |
Tydec_int , top_int_type; |
292 |
Tydec_bool , top_bool_type; |
293 |
(* Tydec_float, top_float_type; *) |
294 |
Tydec_real , top_real_type |
295 |
] |
296 |
|
297 |
let print_type_table fmt () = |
298 |
begin |
299 |
Format.fprintf fmt "{ /* type table */@."; |
300 |
Hashtbl.iter (fun tydec tdef -> |
301 |
Format.fprintf fmt "%a |-> %a" |
302 |
Printers.pp_var_type_dec_desc tydec |
303 |
Printers.pp_typedef (typedef_of_top tdef) |
304 |
) type_table; |
305 |
Format.fprintf fmt "}@." |
306 |
end |
307 |
|
308 |
let rec is_user_type typ = |
309 |
match typ with |
310 |
| Tydec_int | Tydec_bool | Tydec_real |
311 |
(* | Tydec_float *) | Tydec_any | Tydec_const _ -> false |
312 |
| Tydec_clock typ' -> is_user_type typ' |
313 |
| _ -> true |
314 |
|
315 |
let get_repr_type typ = |
316 |
let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in |
317 |
if is_user_type typ_def then typ else typ_def |
318 |
|
319 |
let rec coretype_equal ty1 ty2 = |
320 |
let res = |
321 |
match ty1, ty2 with |
322 |
| Tydec_any , _ |
323 |
| _ , Tydec_any -> assert false |
324 |
| Tydec_const _ , Tydec_const _ -> get_repr_type ty1 = get_repr_type ty2 |
325 |
| Tydec_const _ , _ -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc |
326 |
in (not (is_user_type ty1')) && coretype_equal ty1' ty2 |
327 |
| _ , Tydec_const _ -> coretype_equal ty2 ty1 |
328 |
| Tydec_int , Tydec_int |
329 |
| Tydec_real , Tydec_real |
330 |
(* | Tydec_float , Tydec_float *) |
331 |
| Tydec_bool , Tydec_bool -> true |
332 |
| Tydec_clock ty1 , Tydec_clock ty2 -> coretype_equal ty1 ty2 |
333 |
| Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2 |
334 |
| Tydec_enum tl1 , Tydec_enum tl2 -> List.sort compare tl1 = List.sort compare tl2 |
335 |
| Tydec_struct fl1 , Tydec_struct fl2 -> |
336 |
List.length fl1 = List.length fl2 |
337 |
&& List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2) |
338 |
(List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1) |
339 |
(List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2) |
340 |
| _ -> false |
341 |
in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res) |
342 |
|
343 |
let tag_true = "true" |
344 |
let tag_false = "false" |
345 |
let tag_default = "default" |
346 |
|
347 |
let const_is_bool c = |
348 |
match c with |
349 |
| Const_tag t -> t = tag_true || t = tag_false |
350 |
| _ -> false |
351 |
|
352 |
(* Computes the negation of a boolean constant *) |
353 |
let const_negation c = |
354 |
assert (const_is_bool c); |
355 |
match c with |
356 |
| Const_tag t when t = tag_true -> Const_tag tag_false |
357 |
| _ -> Const_tag tag_true |
358 |
|
359 |
let const_or c1 c2 = |
360 |
assert (const_is_bool c1 && const_is_bool c2); |
361 |
match c1, c2 with |
362 |
| Const_tag t1, _ when t1 = tag_true -> c1 |
363 |
| _ , Const_tag t2 when t2 = tag_true -> c2 |
364 |
| _ -> Const_tag tag_false |
365 |
|
366 |
let const_and c1 c2 = |
367 |
assert (const_is_bool c1 && const_is_bool c2); |
368 |
match c1, c2 with |
369 |
| Const_tag t1, _ when t1 = tag_false -> c1 |
370 |
| _ , Const_tag t2 when t2 = tag_false -> c2 |
371 |
| _ -> Const_tag tag_true |
372 |
|
373 |
let const_xor c1 c2 = |
374 |
assert (const_is_bool c1 && const_is_bool c2); |
375 |
match c1, c2 with |
376 |
| Const_tag t1, Const_tag t2 when t1 <> t2 -> Const_tag tag_true |
377 |
| _ -> Const_tag tag_false |
378 |
|
379 |
let const_impl c1 c2 = |
380 |
assert (const_is_bool c1 && const_is_bool c2); |
381 |
match c1, c2 with |
382 |
| Const_tag t1, _ when t1 = tag_false -> Const_tag tag_true |
383 |
| _ , Const_tag t2 when t2 = tag_true -> Const_tag tag_true |
384 |
| _ -> Const_tag tag_false |
385 |
|
386 |
(* To guarantee uniqueness of tags in enum types *) |
387 |
let tag_table = |
388 |
Utils.create_hashtable 20 [ |
389 |
tag_true, top_bool_type; |
390 |
tag_false, top_bool_type |
391 |
] |
392 |
|
393 |
(* To guarantee uniqueness of fields in struct types *) |
394 |
let field_table = |
395 |
Utils.create_hashtable 20 [ |
396 |
] |
397 |
|
398 |
let get_enum_type_tags cty = |
399 |
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*) |
400 |
match cty with |
401 |
| Tydec_bool -> [tag_true; tag_false] |
402 |
| Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with |
403 |
| Tydec_enum tl -> tl |
404 |
| _ -> assert false) |
405 |
| _ -> assert false |
406 |
|
407 |
let get_struct_type_fields cty = |
408 |
match cty with |
409 |
| Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with |
410 |
| Tydec_struct fl -> fl |
411 |
| _ -> assert false) |
412 |
| _ -> assert false |
413 |
|
414 |
let const_of_bool b = |
415 |
Const_tag (if b then tag_true else tag_false) |
416 |
|
417 |
(* let get_const c = snd (Hashtbl.find consts_table c) *) |
418 |
|
419 |
let ident_of_expr expr = |
420 |
match expr.expr_desc with |
421 |
| Expr_ident id -> id |
422 |
| _ -> assert false |
423 |
|
424 |
(* Generate a new ident expression from a declared variable *) |
425 |
let expr_of_vdecl v = |
426 |
{ expr_tag = Utils.new_tag (); |
427 |
expr_desc = Expr_ident v.var_id; |
428 |
expr_type = v.var_type; |
429 |
expr_clock = v.var_clock; |
430 |
expr_delay = Delay.new_var (); |
431 |
expr_annot = None; |
432 |
expr_loc = v.var_loc } |
433 |
|
434 |
(* Caution, returns an untyped and unclocked expression *) |
435 |
let expr_of_ident id loc = |
436 |
{expr_tag = Utils.new_tag (); |
437 |
expr_desc = Expr_ident id; |
438 |
expr_type = Types.new_var (); |
439 |
expr_clock = Clocks.new_var true; |
440 |
expr_delay = Delay.new_var (); |
441 |
expr_loc = loc; |
442 |
expr_annot = None} |
443 |
|
444 |
let is_tuple_expr expr = |
445 |
match expr.expr_desc with |
446 |
| Expr_tuple _ -> true |
447 |
| _ -> false |
448 |
|
449 |
let expr_list_of_expr expr = |
450 |
match expr.expr_desc with |
451 |
| Expr_tuple elist -> elist |
452 |
| _ -> [expr] |
453 |
|
454 |
let expr_of_expr_list loc elist = |
455 |
match elist with |
456 |
| [t] -> { t with expr_loc = loc } |
457 |
| t::_ -> |
458 |
let tlist = List.map (fun e -> e.expr_type) elist in |
459 |
let clist = List.map (fun e -> e.expr_clock) elist in |
460 |
{ t with expr_desc = Expr_tuple elist; |
461 |
expr_type = Type_predef.type_tuple tlist; |
462 |
expr_clock = Clock_predef.ck_tuple clist; |
463 |
expr_tag = Utils.new_tag (); |
464 |
expr_loc = loc } |
465 |
| _ -> assert false |
466 |
|
467 |
let call_of_expr expr = |
468 |
match expr.expr_desc with |
469 |
| Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r) |
470 |
| _ -> assert false |
471 |
|
472 |
|
473 |
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *) |
474 |
let rec expr_of_dimension dim = |
475 |
let open Dimension in |
476 |
match dim.dim_desc with |
477 |
| Dbool b -> |
478 |
mkexpr dim.dim_loc (Expr_const (const_of_bool b)) |
479 |
| Dint i -> |
480 |
mkexpr dim.dim_loc (Expr_const (Const_int i)) |
481 |
| Dident id -> |
482 |
mkexpr dim.dim_loc (Expr_ident id) |
483 |
| Dite (c, t, e) -> |
484 |
mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e)) |
485 |
| Dappl (id, args) -> |
486 |
mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None)) |
487 |
| Dlink dim' -> expr_of_dimension dim' |
488 |
| Dvar |
489 |
| Dunivar -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim; |
490 |
assert false) |
491 |
|
492 |
let dimension_of_const loc const = |
493 |
let open Dimension in |
494 |
match const with |
495 |
| Const_int i -> mkdim_int loc i |
496 |
| Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true) |
497 |
| _ -> raise InvalidDimension |
498 |
|
499 |
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments |
500 |
into dimension expressions *) |
501 |
let rec dimension_of_expr expr = |
502 |
let open Dimension in |
503 |
match expr.expr_desc with |
504 |
| Expr_const c -> dimension_of_const expr.expr_loc c |
505 |
| Expr_ident id -> mkdim_ident expr.expr_loc id |
506 |
| Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr -> |
507 |
let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in |
508 |
if k = None then raise InvalidDimension; |
509 |
mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args)) |
510 |
| Expr_ite (i, t, e) -> |
511 |
mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e) |
512 |
| _ -> raise InvalidDimension (* not a simple dimension expression *) |
513 |
|
514 |
|
515 |
let sort_handlers hl = |
516 |
List.sort (fun (t, _) (t', _) -> compare t t') hl |
517 |
|
518 |
let num_10 = Num.num_of_int 10 |
519 |
|
520 |
let rec is_eq_const c1 c2 = |
521 |
match c1, c2 with |
522 |
| Const_real (n1, i1, _), Const_real (n2, i2, _) |
523 |
-> Num.(let n1 = n1 // (num_10 **/ (num_of_int i1)) in |
524 |
let n2 = n2 // (num_10 **/ (num_of_int i2)) in |
525 |
eq_num n1 n2) |
526 |
| Const_struct lcl1, Const_struct lcl2 |
527 |
-> List.length lcl1 = List.length lcl2 |
528 |
&& List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2 |
529 |
| _ -> c1 = c2 |
530 |
|
531 |
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with |
532 |
| Expr_const c1, Expr_const c2 -> is_eq_const c1 c2 |
533 |
| Expr_ident i1, Expr_ident i2 -> i1 = i2 |
534 |
| Expr_array el1, Expr_array el2 |
535 |
| Expr_tuple el1, Expr_tuple el2 -> |
536 |
List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 |
537 |
| Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' |
538 |
| Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' |
539 |
| 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 |
540 |
(* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *) |
541 |
(* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *) |
542 |
| Expr_pre e, Expr_pre e' -> is_eq_expr e e' |
543 |
| Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e' |
544 |
| 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') |
545 |
| Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e' |
546 |
| Expr_power (e1, i1), Expr_power (e2, i2) |
547 |
| Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2) |
548 |
| _ -> false |
549 |
|
550 |
let get_node_vars nd = |
551 |
nd.node_inputs @ nd.node_locals @ nd.node_outputs |
552 |
|
553 |
let mk_new_node_name nd id = |
554 |
let used_vars = get_node_vars nd in |
555 |
let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in |
556 |
mk_new_name used id |
557 |
|
558 |
let get_var id var_list = |
559 |
List.find (fun v -> v.var_id = id) var_list |
560 |
|
561 |
let get_node_var id node = |
562 |
try |
563 |
get_var id (get_node_vars node) |
564 |
with Not_found -> begin |
565 |
(* Format.eprintf "Unable to find variable %s in node %s@.@?" id node.node_id; *) |
566 |
raise Not_found |
567 |
end |
568 |
|
569 |
|
570 |
let get_node_eqs = |
571 |
let get_eqs stmts = |
572 |
List.fold_right |
573 |
(fun stmt (res_eq, res_aut) -> |
574 |
match stmt with |
575 |
| Eq eq -> eq :: res_eq, res_aut |
576 |
| Aut aut -> res_eq, aut::res_aut) |
577 |
stmts |
578 |
([], []) in |
579 |
let table_eqs = Hashtbl.create 23 in |
580 |
(fun nd -> |
581 |
try |
582 |
let (old, res) = Hashtbl.find table_eqs nd.node_id |
583 |
in if old == nd.node_stmts then res else raise Not_found |
584 |
with Not_found -> |
585 |
let res = get_eqs nd.node_stmts in |
586 |
begin |
587 |
Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res); |
588 |
res |
589 |
end) |
590 |
|
591 |
let get_node_eq id node = |
592 |
let eqs, auts = get_node_eqs node in |
593 |
try |
594 |
List.find (fun eq -> List.mem id eq.eq_lhs) eqs |
595 |
with |
596 |
Not_found -> (* Shall be defined in automata auts *) raise Not_found |
597 |
|
598 |
let get_nodes prog = |
599 |
List.fold_left ( |
600 |
fun nodes decl -> |
601 |
match decl.top_decl_desc with |
602 |
| Node _ -> decl::nodes |
603 |
| Const _ | ImportedNode _ | Open _ | TypeDef _ -> nodes |
604 |
) [] prog |
605 |
|
606 |
let get_imported_nodes prog = |
607 |
List.fold_left ( |
608 |
fun nodes decl -> |
609 |
match decl.top_decl_desc with |
610 |
| ImportedNode _ -> decl::nodes |
611 |
| Const _ | Node _ | Open _ | TypeDef _-> nodes |
612 |
) [] prog |
613 |
|
614 |
let get_consts prog = |
615 |
List.fold_right ( |
616 |
fun decl consts -> |
617 |
match decl.top_decl_desc with |
618 |
| Const _ -> decl::consts |
619 |
| Node _ | ImportedNode _ | Open _ | TypeDef _ -> consts |
620 |
) prog [] |
621 |
|
622 |
let get_typedefs prog = |
623 |
List.fold_right ( |
624 |
fun decl types -> |
625 |
match decl.top_decl_desc with |
626 |
| TypeDef _ -> decl::types |
627 |
| Node _ | ImportedNode _ | Open _ | Const _ -> types |
628 |
) prog [] |
629 |
|
630 |
let get_dependencies prog = |
631 |
List.fold_right ( |
632 |
fun decl deps -> |
633 |
match decl.top_decl_desc with |
634 |
| Open _ -> decl::deps |
635 |
| Node _ | ImportedNode _ | TypeDef _ | Const _ -> deps |
636 |
) prog [] |
637 |
|
638 |
let get_node_interface nd = |
639 |
{nodei_id = nd.node_id; |
640 |
nodei_type = nd.node_type; |
641 |
nodei_clock = nd.node_clock; |
642 |
nodei_inputs = nd.node_inputs; |
643 |
nodei_outputs = nd.node_outputs; |
644 |
nodei_stateless = nd.node_dec_stateless; |
645 |
nodei_spec = nd.node_spec; |
646 |
(* nodei_annot = nd.node_annot; *) |
647 |
nodei_prototype = None; |
648 |
nodei_in_lib = []; |
649 |
} |
650 |
|
651 |
(************************************************************************) |
652 |
(* Renaming *) |
653 |
|
654 |
let rec rename_static rename cty = |
655 |
match cty with |
656 |
| Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty') |
657 |
| Tydec_clock cty -> Tydec_clock (rename_static rename cty) |
658 |
| Tydec_struct fl -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl) |
659 |
| _ -> cty |
660 |
|
661 |
let rec rename_carrier rename cck = |
662 |
match cck with |
663 |
| Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl) |
664 |
| _ -> cck |
665 |
|
666 |
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*) |
667 |
|
668 |
(* applies the renaming function [fvar] to all variables of expression [expr] *) |
669 |
(* let rec expr_replace_var fvar expr = *) |
670 |
(* { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *) |
671 |
|
672 |
(* and expr_desc_replace_var fvar expr_desc = *) |
673 |
(* match expr_desc with *) |
674 |
(* | Expr_const _ -> expr_desc *) |
675 |
(* | Expr_ident i -> Expr_ident (fvar i) *) |
676 |
(* | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *) |
677 |
(* | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *) |
678 |
(* | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *) |
679 |
(* | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *) |
680 |
(* | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) *) |
681 |
(* | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) *) |
682 |
(* | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) *) |
683 |
(* | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *) |
684 |
(* | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *) |
685 |
(* | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) *) |
686 |
(* | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') *) |
687 |
|
688 |
|
689 |
|
690 |
let rec rename_expr f_node f_var expr = |
691 |
{ expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc } |
692 |
and rename_expr_desc f_node f_var expr_desc = |
693 |
let re = rename_expr f_node f_var in |
694 |
match expr_desc with |
695 |
| Expr_const _ -> expr_desc |
696 |
| Expr_ident i -> Expr_ident (f_var i) |
697 |
| Expr_array el -> Expr_array (List.map re el) |
698 |
| Expr_access (e1, d) -> Expr_access (re e1, d) |
699 |
| Expr_power (e1, d) -> Expr_power (re e1, d) |
700 |
| Expr_tuple el -> Expr_tuple (List.map re el) |
701 |
| Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e) |
702 |
| Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) |
703 |
| Expr_fby (e1, e2) -> Expr_fby (re e1, re e2) |
704 |
| Expr_pre e' -> Expr_pre (re e') |
705 |
| Expr_when (e', i, l)-> Expr_when (re e', f_var i, l) |
706 |
| Expr_merge (i, hl) -> |
707 |
Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl) |
708 |
| Expr_appl (i, e', i') -> |
709 |
Expr_appl (f_node i, re e', Utils.option_map re i') |
710 |
|
711 |
let rename_dec_type f_node f_var t = assert false (* |
712 |
Types.rename_dim_type (Dimension.rename f_node f_var) t*) |
713 |
|
714 |
let rename_dec_clock f_node f_var c = assert false (* |
715 |
Clocks.rename_clock_expr f_var c*) |
716 |
|
717 |
let rename_var f_node f_var v = { |
718 |
v with |
719 |
var_id = f_var v.var_id; |
720 |
var_dec_type = rename_dec_type f_node f_var v.var_type; |
721 |
var_dec_clock = rename_dec_clock f_node f_var v.var_clock |
722 |
} |
723 |
|
724 |
let rename_vars f_node f_var = List.map (rename_var f_node f_var) |
725 |
|
726 |
let rec rename_eq f_node f_var eq = { eq with |
727 |
eq_lhs = List.map f_var eq.eq_lhs; |
728 |
eq_rhs = rename_expr f_node f_var eq.eq_rhs |
729 |
} |
730 |
and rename_handler f_node f_var h = {h with |
731 |
hand_state = f_var h.hand_state; |
732 |
hand_unless = List.map ( |
733 |
fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id |
734 |
) h.hand_unless; |
735 |
hand_until = List.map ( |
736 |
fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id |
737 |
) h.hand_until; |
738 |
hand_locals = rename_vars f_node f_var h.hand_locals; |
739 |
hand_stmts = rename_stmts f_node f_var h.hand_stmts; |
740 |
hand_annots = rename_annots f_node f_var h.hand_annots; |
741 |
|
742 |
} |
743 |
and rename_aut f_node f_var aut = { aut with |
744 |
aut_id = f_var aut.aut_id; |
745 |
aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers; |
746 |
} |
747 |
and rename_stmts f_node f_var stmts = List.map (fun stmt -> match stmt with |
748 |
| Eq eq -> Eq (rename_eq f_node f_var eq) |
749 |
| Aut at -> Aut (rename_aut f_node f_var at)) |
750 |
stmts |
751 |
and rename_annotl f_node f_var annots = |
752 |
List.map |
753 |
(fun (key, value) -> key, rename_eexpr f_node f_var value) |
754 |
annots |
755 |
and rename_annot f_node f_var annot = |
756 |
{ annot with annots = rename_annotl f_node f_var annot.annots } |
757 |
and rename_annots f_node f_var annots = |
758 |
List.map (rename_annot f_node f_var) annots |
759 |
and rename_eexpr f_node f_var ee = |
760 |
{ ee with |
761 |
eexpr_tag = Utils.new_tag (); |
762 |
eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr; |
763 |
eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_node f_var vdecls) ee.eexpr_quantifiers; |
764 |
eexpr_normalized = Utils.option_map |
765 |
(fun (vdecl, eqs, vdecls) -> |
766 |
rename_var f_node f_var vdecl, |
767 |
List.map (rename_eq f_node f_var) eqs, |
768 |
rename_vars f_node f_var vdecls |
769 |
) ee.eexpr_normalized; |
770 |
|
771 |
} |
772 |
|
773 |
|
774 |
|
775 |
|
776 |
let rename_node f_node f_var nd = |
777 |
let rename_var = rename_var f_node f_var in |
778 |
let rename_expr = rename_expr f_node f_var in |
779 |
let rename_stmts = rename_stmts f_node f_var in |
780 |
let inputs = List.map rename_var nd.node_inputs in |
781 |
let outputs = List.map rename_var nd.node_outputs in |
782 |
let locals = List.map rename_var nd.node_locals in |
783 |
let gen_calls = List.map rename_expr nd.node_gencalls in |
784 |
let node_checks = List.map (Dimension.rename f_node f_var) nd.node_checks in |
785 |
let node_asserts = List.map |
786 |
(fun a -> |
787 |
{a with assert_expr = |
788 |
let expr = a.assert_expr in |
789 |
rename_expr expr}) |
790 |
nd.node_asserts |
791 |
in |
792 |
let node_stmts = rename_stmts nd.node_stmts |
793 |
|
794 |
|
795 |
in |
796 |
let spec = |
797 |
Utils.option_map |
798 |
(fun s -> assert false; (*rename_node_annot f_node f_var s*) ) (* TODO: implement! *) |
799 |
nd.node_spec |
800 |
in |
801 |
let annot = rename_annots f_node f_var nd.node_annot in |
802 |
{ |
803 |
node_id = f_node nd.node_id; |
804 |
node_type = nd.node_type; |
805 |
node_clock = nd.node_clock; |
806 |
node_inputs = inputs; |
807 |
node_outputs = outputs; |
808 |
node_locals = locals; |
809 |
node_gencalls = gen_calls; |
810 |
node_checks = node_checks; |
811 |
node_asserts = node_asserts; |
812 |
node_stmts = node_stmts; |
813 |
node_dec_stateless = nd.node_dec_stateless; |
814 |
node_stateless = nd.node_stateless; |
815 |
node_spec = spec; |
816 |
node_annot = annot; |
817 |
} |
818 |
|
819 |
|
820 |
let rename_const f_const c = |
821 |
{ c with const_id = f_const c.const_id } |
822 |
|
823 |
let rename_typedef f_var t = |
824 |
match t.tydef_desc with |
825 |
| Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) } |
826 |
| _ -> t |
827 |
|
828 |
let rename_prog f_node f_var f_const prog = |
829 |
List.rev ( |
830 |
List.fold_left (fun accu top -> |
831 |
(match top.top_decl_desc with |
832 |
| Node nd -> |
833 |
{ top with top_decl_desc = Node (rename_node f_node f_var nd) } |
834 |
| Const c -> |
835 |
{ top with top_decl_desc = Const (rename_const f_const c) } |
836 |
| TypeDef tdef -> |
837 |
{ top with top_decl_desc = TypeDef (rename_typedef f_var tdef) } |
838 |
| ImportedNode _ |
839 |
| Open _ -> top) |
840 |
::accu |
841 |
) [] prog |
842 |
) |
843 |
|
844 |
(* Applies the renaming function [fvar] to every rhs |
845 |
only when the corresponding lhs satisfies predicate [pvar] *) |
846 |
let eq_replace_rhs_var pvar fvar eq = |
847 |
let pvar l = List.exists pvar l in |
848 |
let rec replace lhs rhs = |
849 |
{ rhs with expr_desc = |
850 |
match lhs with |
851 |
| [] -> assert false |
852 |
| [_] -> if pvar lhs then rename_expr_desc (fun x -> x) fvar rhs.expr_desc else rhs.expr_desc |
853 |
| _ -> |
854 |
(match rhs.expr_desc with |
855 |
| Expr_tuple tl -> |
856 |
Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl) |
857 |
| Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs -> |
858 |
let args = expr_list_of_expr arg in |
859 |
Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None) |
860 |
| Expr_array _ |
861 |
| Expr_access _ |
862 |
| Expr_power _ |
863 |
| Expr_const _ |
864 |
| Expr_ident _ |
865 |
| Expr_appl _ -> |
866 |
if pvar lhs |
867 |
then rename_expr_desc (fun x -> x) fvar rhs.expr_desc |
868 |
else rhs.expr_desc |
869 |
| Expr_ite (c, t, e) -> Expr_ite (replace lhs c, replace lhs t, replace lhs e) |
870 |
| Expr_arrow (e1, e2) -> Expr_arrow (replace lhs e1, replace lhs e2) |
871 |
| Expr_fby (e1, e2) -> Expr_fby (replace lhs e1, replace lhs e2) |
872 |
| Expr_pre e' -> Expr_pre (replace lhs e') |
873 |
| Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i |
874 |
in Expr_when (replace lhs e', i', l) |
875 |
| Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i |
876 |
in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl) |
877 |
) |
878 |
} |
879 |
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } |
880 |
|
881 |
|
882 |
(**********************************************************************) |
883 |
(* Pretty printers *) |
884 |
|
885 |
let pp_decl_type fmt tdecl = |
886 |
match tdecl.top_decl_desc with |
887 |
| Node nd -> |
888 |
fprintf fmt "%s: " nd.node_id; |
889 |
Utils.reset_names (); |
890 |
fprintf fmt "%a@ " Types.print_ty nd.node_type |
891 |
| ImportedNode ind -> |
892 |
fprintf fmt "%s: " ind.nodei_id; |
893 |
Utils.reset_names (); |
894 |
fprintf fmt "%a@ " Types.print_ty ind.nodei_type |
895 |
| Const _ | Open _ | TypeDef _ -> () |
896 |
|
897 |
let pp_prog_type fmt tdecl_list = |
898 |
Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list |
899 |
|
900 |
let pp_decl_clock fmt cdecl = |
901 |
match cdecl.top_decl_desc with |
902 |
| Node nd -> |
903 |
fprintf fmt "%s: " nd.node_id; |
904 |
Utils.reset_names (); |
905 |
fprintf fmt "%a@ " Clocks.print_ck nd.node_clock |
906 |
| ImportedNode ind -> |
907 |
fprintf fmt "%s: " ind.nodei_id; |
908 |
Utils.reset_names (); |
909 |
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock |
910 |
| Const _ | Open _ | TypeDef _ -> () |
911 |
|
912 |
let pp_prog_clock fmt prog = |
913 |
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog |
914 |
|
915 |
|
916 |
(* filling node table with internal functions *) |
917 |
let vdecls_of_typ_ck cpt ty = |
918 |
let loc = Location.dummy_loc in |
919 |
List.map |
920 |
(fun _ -> incr cpt; |
921 |
let name = sprintf "_var_%d" !cpt in |
922 |
mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None, None)) |
923 |
(Types.type_list_of_type ty) |
924 |
|
925 |
let mk_internal_node id = |
926 |
let spec = None in |
927 |
let ty = Env.lookup_value Basic_library.type_env id in |
928 |
let ck = Env.lookup_value Basic_library.clock_env id in |
929 |
let (tin, tout) = Types.split_arrow ty in |
930 |
(*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*) |
931 |
let cpt = ref (-1) in |
932 |
mktop |
933 |
(ImportedNode |
934 |
{nodei_id = id; |
935 |
nodei_type = ty; |
936 |
nodei_clock = ck; |
937 |
nodei_inputs = vdecls_of_typ_ck cpt tin; |
938 |
nodei_outputs = vdecls_of_typ_ck cpt tout; |
939 |
nodei_stateless = Types.get_static_value ty <> None; |
940 |
nodei_spec = spec; |
941 |
(* nodei_annot = []; *) |
942 |
nodei_prototype = None; |
943 |
nodei_in_lib = []; |
944 |
}) |
945 |
|
946 |
let add_internal_funs () = |
947 |
List.iter |
948 |
(fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd) |
949 |
Basic_library.internal_funs |
950 |
|
951 |
|
952 |
|
953 |
(* Replace any occurence of a var in vars_to_replace by its associated |
954 |
expression in defs until e does not contain any such variables *) |
955 |
let rec substitute_expr vars_to_replace defs e = |
956 |
let se = substitute_expr vars_to_replace defs in |
957 |
{ e with expr_desc = |
958 |
let ed = e.expr_desc in |
959 |
match ed with |
960 |
| Expr_const _ -> ed |
961 |
| Expr_array el -> Expr_array (List.map se el) |
962 |
| Expr_access (e1, d) -> Expr_access (se e1, d) |
963 |
| Expr_power (e1, d) -> Expr_power (se e1, d) |
964 |
| Expr_tuple el -> Expr_tuple (List.map se el) |
965 |
| Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e) |
966 |
| Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) |
967 |
| Expr_fby (e1, e2) -> Expr_fby (se e1, se e2) |
968 |
| Expr_pre e' -> Expr_pre (se e') |
969 |
| Expr_when (e', i, l)-> Expr_when (se e', i, l) |
970 |
| Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl) |
971 |
| Expr_appl (i, e', i') -> Expr_appl (i, se e', i') |
972 |
| Expr_ident i -> |
973 |
if List.exists (fun v -> v.var_id = i) vars_to_replace then ( |
974 |
let eq_i eq = eq.eq_lhs = [i] in |
975 |
if List.exists eq_i defs then |
976 |
let sub = List.find eq_i defs in |
977 |
let sub' = se sub.eq_rhs in |
978 |
sub'.expr_desc |
979 |
else |
980 |
assert false |
981 |
) |
982 |
else |
983 |
ed |
984 |
|
985 |
} |
986 |
|
987 |
let rec expr_to_eexpr expr = |
988 |
{ eexpr_tag = expr.expr_tag; |
989 |
eexpr_qfexpr = expr; |
990 |
eexpr_quantifiers = []; |
991 |
eexpr_type = expr.expr_type; |
992 |
eexpr_clock = expr.expr_clock; |
993 |
eexpr_loc = expr.expr_loc; |
994 |
eexpr_normalized = None |
995 |
} |
996 |
(* and expr_desc_to_eexpr_desc expr_desc = *) |
997 |
(* let conv = expr_to_eexpr in *) |
998 |
(* match expr_desc with *) |
999 |
(* | Expr_const c -> EExpr_const (match c with *) |
1000 |
(* | Const_int x -> EConst_int x *) |
1001 |
(* | Const_real x -> EConst_real x *) |
1002 |
(* | Const_float x -> EConst_float x *) |
1003 |
(* | Const_tag x -> EConst_tag x *) |
1004 |
(* | _ -> assert false *) |
1005 |
|
1006 |
(* ) *) |
1007 |
(* | Expr_ident i -> EExpr_ident i *) |
1008 |
(* | Expr_tuple el -> EExpr_tuple (List.map conv el) *) |
1009 |
|
1010 |
(* | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) *) |
1011 |
(* | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2) *) |
1012 |
(* | Expr_pre e' -> EExpr_pre (conv e') *) |
1013 |
(* | Expr_appl (i, e', i') -> *) |
1014 |
(* EExpr_appl *) |
1015 |
(* (i, conv e', match i' with None -> None | Some(id, _) -> Some id) *) |
1016 |
|
1017 |
(* | Expr_when _ *) |
1018 |
(* | Expr_merge _ -> assert false *) |
1019 |
(* | Expr_array _ *) |
1020 |
(* | Expr_access _ *) |
1021 |
(* | Expr_power _ -> assert false *) |
1022 |
(* | Expr_ite (c, t, e) -> assert false *) |
1023 |
(* | _ -> assert false *) |
1024 |
|
1025 |
|
1026 |
let rec get_expr_calls nodes e = |
1027 |
let get_calls = get_expr_calls nodes in |
1028 |
match e.expr_desc with |
1029 |
| Expr_const _ |
1030 |
| Expr_ident _ -> Utils.ISet.empty |
1031 |
| Expr_tuple el |
1032 |
| Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el |
1033 |
| Expr_pre e1 |
1034 |
| Expr_when (e1, _, _) |
1035 |
| Expr_access (e1, _) |
1036 |
| Expr_power (e1, _) -> get_calls e1 |
1037 |
| Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) |
1038 |
| Expr_arrow (e1, e2) |
1039 |
| Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2) |
1040 |
| Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty hl |
1041 |
| Expr_appl (i, e', i') -> |
1042 |
if Basic_library.is_expr_internal_fun e then |
1043 |
(get_calls e') |
1044 |
else |
1045 |
let calls = Utils.ISet.add i (get_calls e') in |
1046 |
let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in |
1047 |
if List.exists test nodes then |
1048 |
match (List.find test nodes).top_decl_desc with |
1049 |
| Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls |
1050 |
| _ -> assert false |
1051 |
else |
1052 |
calls |
1053 |
|
1054 |
and get_eq_calls nodes eq = |
1055 |
get_expr_calls nodes eq.eq_rhs |
1056 |
and get_aut_handler_calls nodes h = |
1057 |
List.fold_left (fun accu stmt -> match stmt with |
1058 |
| Eq eq -> Utils.ISet.union (get_eq_calls nodes eq) accu |
1059 |
| Aut aut' -> Utils.ISet.union (get_aut_calls nodes aut') accu |
1060 |
) Utils.ISet.empty h.hand_stmts |
1061 |
and get_aut_calls nodes aut = |
1062 |
List.fold_left (fun accu h -> Utils.ISet.union (get_aut_handler_calls nodes h) accu) |
1063 |
Utils.ISet.empty aut.aut_handlers |
1064 |
and get_node_calls nodes node = |
1065 |
let eqs, auts = get_node_eqs node in |
1066 |
let aut_calls = |
1067 |
List.fold_left |
1068 |
(fun accu aut -> Utils.ISet.union (get_aut_calls nodes aut) accu) |
1069 |
Utils.ISet.empty auts |
1070 |
in |
1071 |
List.fold_left |
1072 |
(fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) |
1073 |
aut_calls eqs |
1074 |
|
1075 |
let get_expr_vars e = |
1076 |
let rec get_expr_vars vars e = |
1077 |
get_expr_desc_vars vars e.expr_desc |
1078 |
and get_expr_desc_vars vars expr_desc = |
1079 |
(*Format.eprintf "get_expr_desc_vars expr=%a@." Printers.pp_expr (mkexpr Location.dummy_loc expr_desc);*) |
1080 |
match expr_desc with |
1081 |
| Expr_const _ -> vars |
1082 |
| Expr_ident x -> Utils.ISet.add x vars |
1083 |
| Expr_tuple el |
1084 |
| Expr_array el -> List.fold_left get_expr_vars vars el |
1085 |
| Expr_pre e1 -> get_expr_vars vars e1 |
1086 |
| Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 |
1087 |
| Expr_access (e1, d) |
1088 |
| Expr_power (e1, d) -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d] |
1089 |
| Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e] |
1090 |
| Expr_arrow (e1, e2) |
1091 |
| Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2] |
1092 |
| Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl |
1093 |
| Expr_appl (_, arg, None) -> get_expr_vars vars arg |
1094 |
| Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r] |
1095 |
in |
1096 |
get_expr_vars Utils.ISet.empty e |
1097 |
|
1098 |
let rec expr_has_arrows e = |
1099 |
expr_desc_has_arrows e.expr_desc |
1100 |
and expr_desc_has_arrows expr_desc = |
1101 |
match expr_desc with |
1102 |
| Expr_const _ |
1103 |
| Expr_ident _ -> false |
1104 |
| Expr_tuple el |
1105 |
| Expr_array el -> List.exists expr_has_arrows el |
1106 |
| Expr_pre e1 |
1107 |
| Expr_when (e1, _, _) |
1108 |
| Expr_access (e1, _) |
1109 |
| Expr_power (e1, _) -> expr_has_arrows e1 |
1110 |
| Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e] |
1111 |
| Expr_arrow (e1, e2) |
1112 |
| Expr_fby (e1, e2) -> true |
1113 |
| Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl |
1114 |
| Expr_appl (i, e', i') -> expr_has_arrows e' |
1115 |
|
1116 |
and eq_has_arrows eq = |
1117 |
expr_has_arrows eq.eq_rhs |
1118 |
and aut_has_arrows aut = List.exists (fun h -> List.exists (fun stmt -> match stmt with Eq eq -> eq_has_arrows eq | Aut aut' -> aut_has_arrows aut') h.hand_stmts ) aut.aut_handlers |
1119 |
and node_has_arrows node = |
1120 |
let eqs, auts = get_node_eqs node in |
1121 |
List.exists (fun eq -> eq_has_arrows eq) eqs || List.exists (fun aut -> aut_has_arrows aut) auts |
1122 |
|
1123 |
|
1124 |
|
1125 |
let copy_var_decl vdecl = |
1126 |
mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig (vdecl.var_id, vdecl.var_dec_type, vdecl.var_dec_clock, vdecl.var_dec_const, vdecl.var_dec_value, vdecl.var_parent_nodeid) |
1127 |
|
1128 |
let copy_const cdecl = |
1129 |
{ cdecl with const_type = Types.new_var () } |
1130 |
|
1131 |
let copy_node nd = |
1132 |
{ nd with |
1133 |
node_type = Types.new_var (); |
1134 |
node_clock = Clocks.new_var true; |
1135 |
node_inputs = List.map copy_var_decl nd.node_inputs; |
1136 |
node_outputs = List.map copy_var_decl nd.node_outputs; |
1137 |
node_locals = List.map copy_var_decl nd.node_locals; |
1138 |
node_gencalls = []; |
1139 |
node_checks = []; |
1140 |
node_stateless = None; |
1141 |
} |
1142 |
|
1143 |
let copy_top top = |
1144 |
match top.top_decl_desc with |
1145 |
| Node nd -> { top with top_decl_desc = Node (copy_node nd) } |
1146 |
| Const c -> { top with top_decl_desc = Const (copy_const c) } |
1147 |
| _ -> top |
1148 |
|
1149 |
let copy_prog top_list = |
1150 |
List.map copy_top top_list |
1151 |
|
1152 |
|
1153 |
let rec expr_contains_expr expr_tag expr = |
1154 |
let search = expr_contains_expr expr_tag in |
1155 |
expr.expr_tag = expr_tag || |
1156 |
( |
1157 |
match expr.expr_desc with |
1158 |
| Expr_const _ -> false |
1159 |
| Expr_array el -> List.exists search el |
1160 |
| Expr_access (e1, _) |
1161 |
| Expr_power (e1, _) -> search e1 |
1162 |
| Expr_tuple el -> List.exists search el |
1163 |
| Expr_ite (c, t, e) -> List.exists search [c;t;e] |
1164 |
| Expr_arrow (e1, e2) |
1165 |
| Expr_fby (e1, e2) -> List.exists search [e1; e2] |
1166 |
| Expr_pre e' |
1167 |
| Expr_when (e', _, _) -> search e' |
1168 |
| Expr_merge (_, hl) -> List.exists (fun (_, h) -> search h) hl |
1169 |
| Expr_appl (_, e', None) -> search e' |
1170 |
| Expr_appl (_, e', Some e'') -> List.exists search [e'; e''] |
1171 |
| Expr_ident _ -> false |
1172 |
) |
1173 |
|
1174 |
|
1175 |
|
1176 |
|
1177 |
(* Local Variables: *) |
1178 |
(* compile-command:"make -C .." *) |
1179 |
(* End: *) |