lustrec / src / corelang.ml @ 52cfee34
History  View  Annotate  Download (26.8 KB)
1 
(*  

2 
* SchedMCore  A MultiCore Scheduling Framework 
3 
* Copyright (C) 20092011, 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 021111307 
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 (nonimported) 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 
(* compilecommand:"make C .." *) 
807 
(* End: *) 