lustrec / src / corelang.ml @ e135421f
History  View  Annotate  Download (25.3 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 
mutable 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  
149 
exception Error of Location.t * error 
150  
151 
module VDeclModule = 
152 
struct (* Node module *) 
153 
type t = var_decl 
154 
let compare v1 v2 = compare v1 v2 
155 
let hash n = Hashtbl.hash n 
156 
let equal n1 n2 = n1 = n2 
157 
end 
158  
159 
module VMap = Map.Make(VDeclModule) 
160  
161 
module VSet = Set.Make(VDeclModule) 
162  
163 
(************************************************************) 
164 
(* *) 
165  
166 
let mktyp loc d = 
167 
{ ty_dec_desc = d; ty_dec_loc = loc } 
168  
169 
let mkclock loc d = 
170 
{ ck_dec_desc = d; ck_dec_loc = loc } 
171  
172 
let mkvar_decl loc (id, ty_dec, ck_dec, is_const) = 
173 
{ var_id = id; 
174 
var_dec_type = ty_dec; 
175 
var_dec_clock = ck_dec; 
176 
var_dec_const = is_const; 
177 
var_type = Types.new_var (); 
178 
var_clock = Clocks.new_var true; 
179 
var_loc = loc } 
180  
181 
let mkexpr loc d = 
182 
{ expr_tag = Utils.new_tag (); 
183 
expr_desc = d; 
184 
expr_type = Types.new_var (); 
185 
expr_clock = Clocks.new_var true; 
186 
expr_delay = Delay.new_var (); 
187 
expr_annot = None; 
188 
expr_loc = loc } 
189  
190 
let var_decl_of_const c = 
191 
{ var_id = c.const_id; 
192 
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any }; 
193 
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any }; 
194 
var_dec_const = true; 
195 
var_type = c.const_type; 
196 
var_clock = Clocks.new_var false; 
197 
var_loc = c.const_loc } 
198  
199 
let mk_new_name vdecl_list id = 
200 
let rec new_name name cpt = 
201 
if List.exists (fun v > v.var_id = name) vdecl_list 
202 
then new_name (sprintf "_%s_%i" id cpt) (cpt+1) 
203 
else name 
204 
in new_name id 1 
205  
206 
let update_expr_annot e annot = 
207 
{ e with expr_annot = LustreSpec.merge_expr_annot e.expr_annot (Some annot) } 
208  
209 
let mkeq loc (lhs, rhs) = 
210 
{ eq_lhs = lhs; 
211 
eq_rhs = rhs; 
212 
eq_loc = loc } 
213  
214 
let mkassert loc expr = 
215 
{ assert_loc = loc; 
216 
assert_expr = expr 
217 
} 
218  
219 
let mktop_decl loc d = 
220 
{ top_decl_desc = d; top_decl_loc = loc } 
221  
222 
let mkpredef_call loc funname args = 
223 
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None)) 
224  
225 
let mkpredef_unary_call loc funname arg = 
226 
mkexpr loc (Expr_appl (funname, arg, None)) 
227  
228  
229 
(***********************************************************) 
230 
(* Fast access to nodes, by name *) 
231 
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30 
232 
let consts_table = Hashtbl.create 30 
233  
234 
let node_name td = 
235 
match td.top_decl_desc with 
236 
 Node nd > nd.node_id 
237 
 ImportedNode nd > nd.nodei_id 
238 
 _ > assert false 
239  
240 
let is_generic_node td = 
241 
match td.top_decl_desc with 
242 
 Node nd > List.exists (fun v > v.var_dec_const) nd.node_inputs 
243 
 ImportedNode nd > List.exists (fun v > v.var_dec_const) nd.nodei_inputs 
244 
 _ > assert false 
245  
246 
let node_inputs td = 
247 
match td.top_decl_desc with 
248 
 Node nd > nd.node_inputs 
249 
 ImportedNode nd > nd.nodei_inputs 
250 
 _ > assert false 
251  
252 
let node_from_name id = 
253 
try 
254 
Hashtbl.find node_table id 
255 
with Not_found > (Format.eprintf "Unable to find any node named %s@ @?" id; 
256 
assert false) 
257  
258 
let is_imported_node td = 
259 
match td.top_decl_desc with 
260 
 Node nd > false 
261 
 ImportedNode nd > true 
262 
 _ > assert false 
263  
264  
265 
(* alias and type definition table *) 
266 
let type_table = 
267 
Utils.create_hashtable 20 [ 
268 
Tydec_int , Tydec_int; 
269 
Tydec_bool , Tydec_bool; 
270 
Tydec_float, Tydec_float; 
271 
Tydec_real , Tydec_real 
272 
] 
273  
274 
let rec is_user_type typ = 
275 
match typ with 
276 
 Tydec_int  Tydec_bool  Tydec_real 
277 
 Tydec_float  Tydec_any  Tydec_const _ > false 
278 
 Tydec_clock typ' > is_user_type typ' 
279 
 _ > true 
280  
281 
let get_repr_type typ = 
282 
let typ_def = Hashtbl.find type_table typ in 
283 
if is_user_type typ_def then typ else typ_def 
284  
285 
let tag_true = "true" 
286 
let tag_false = "false" 
287  
288 
let const_is_bool c = 
289 
match c with 
290 
 Const_tag t > t = tag_true  t = tag_false 
291 
 _ > false 
292  
293 
(* Computes the negation of a boolean constant *) 
294 
let const_negation c = 
295 
assert (const_is_bool c); 
296 
match c with 
297 
 Const_tag t when t = tag_true > Const_tag tag_false 
298 
 _ > Const_tag tag_true 
299  
300 
let const_or c1 c2 = 
301 
assert (const_is_bool c1 && const_is_bool c2); 
302 
match c1, c2 with 
303 
 Const_tag t1, _ when t1 = tag_true > c1 
304 
 _ , Const_tag t2 when t2 = tag_true > c2 
305 
 _ > Const_tag tag_false 
306  
307 
let const_and c1 c2 = 
308 
assert (const_is_bool c1 && const_is_bool c2); 
309 
match c1, c2 with 
310 
 Const_tag t1, _ when t1 = tag_false > c1 
311 
 _ , Const_tag t2 when t2 = tag_false > c2 
312 
 _ > Const_tag tag_true 
313  
314 
let const_xor c1 c2 = 
315 
assert (const_is_bool c1 && const_is_bool c2); 
316 
match c1, c2 with 
317 
 Const_tag t1, Const_tag t2 when t1 <> t2 > Const_tag tag_true 
318 
 _ > Const_tag tag_false 
319  
320 
let const_impl c1 c2 = 
321 
assert (const_is_bool c1 && const_is_bool c2); 
322 
match c1, c2 with 
323 
 Const_tag t1, _ when t1 = tag_false > Const_tag tag_true 
324 
 _ , Const_tag t2 when t2 = tag_true > Const_tag tag_true 
325 
 _ > Const_tag tag_false 
326  
327 
(* To guarantee uniqueness of tags in enum types *) 
328 
let tag_table = 
329 
Utils.create_hashtable 20 [ 
330 
tag_true, Tydec_bool; 
331 
tag_false, Tydec_bool 
332 
] 
333  
334 
(* To guarantee uniqueness of fields in struct types *) 
335 
let field_table = 
336 
Utils.create_hashtable 20 [ 
337 
] 
338  
339 
let get_enum_type_tags cty = 
340 
match cty with 
341 
 Tydec_bool > [tag_true; tag_false] 
342 
 Tydec_const _ > (match Hashtbl.find type_table cty with 
343 
 Tydec_enum tl > tl 
344 
 _ > assert false) 
345 
 _ > assert false 
346  
347 
let get_struct_type_fields cty = 
348 
match cty with 
349 
 Tydec_const _ > (match Hashtbl.find type_table cty with 
350 
 Tydec_struct fl > fl 
351 
 _ > assert false) 
352 
 _ > assert false 
353  
354 
let const_of_bool b = 
355 
Const_tag (if b then tag_true else tag_false) 
356  
357 
(* let get_const c = snd (Hashtbl.find consts_table c) *) 
358  
359 
(* Caution, returns an untyped and unclocked expression *) 
360 
let expr_of_ident id loc = 
361 
{expr_tag = Utils.new_tag (); 
362 
expr_desc = Expr_ident id; 
363 
expr_type = Types.new_var (); 
364 
expr_clock = Clocks.new_var true; 
365 
expr_delay = Delay.new_var (); 
366 
expr_loc = loc; 
367 
expr_annot = None} 
368  
369 
let expr_list_of_expr expr = 
370 
match expr.expr_desc with 
371 
 Expr_tuple elist > 
372 
elist 
373 
 _ > [expr] 
374  
375 
let expr_of_expr_list loc elist = 
376 
match elist with 
377 
 [t] > { t with expr_loc = loc } 
378 
 t::_ > { t with expr_desc = Expr_tuple elist; expr_loc = loc } 
379 
 _ > assert false 
380  
381 
let call_of_expr expr = 
382 
match expr.expr_desc with 
383 
 Expr_appl (f, args, r) > (f, expr_list_of_expr args, r) 
384 
 _ > assert false 
385  
386 
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *) 
387 
let rec expr_of_dimension dim = 
388 
match dim.dim_desc with 
389 
 Dbool b > 
390 
mkexpr dim.dim_loc (Expr_const (const_of_bool b)) 
391 
 Dint i > 
392 
mkexpr dim.dim_loc (Expr_const (Const_int i)) 
393 
 Dident id > 
394 
mkexpr dim.dim_loc (Expr_ident id) 
395 
 Dite (c, t, e) > 
396 
mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e)) 
397 
 Dappl (id, args) > 
398 
mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None)) 
399 
 Dlink dim' > expr_of_dimension dim' 
400 
 Dvar 
401 
 Dunivar > (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim; 
402 
assert false) 
403  
404 
let dimension_of_const loc const = 
405 
match const with 
406 
 Const_int i > mkdim_int loc i 
407 
 Const_tag t when t = tag_true  t = tag_false > mkdim_bool loc (t = tag_true) 
408 
 _ > raise InvalidDimension 
409  
410 
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
411 
into dimension expressions *) 
412 
let rec dimension_of_expr expr = 
413 
match expr.expr_desc with 
414 
 Expr_const c > dimension_of_const expr.expr_loc c 
415 
 Expr_ident id > mkdim_ident expr.expr_loc id 
416 
 Expr_appl (f, args, None) when Basic_library.is_internal_fun f > 
417 
let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in 
418 
if k = None then raise InvalidDimension; 
419 
mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args)) 
420 
 Expr_ite (i, t, e) > 
421 
mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e) 
422 
 _ > raise InvalidDimension (* not a simple dimension expression *) 
423  
424  
425 
let sort_handlers hl = 
426 
List.sort (fun (t, _) (t', _) > compare t t') hl 
427  
428 
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with 
429 
 Expr_const c1, Expr_const c2 > c1 = c2 
430 
 Expr_ident i1, Expr_ident i2 > i1 = i2 
431 
 Expr_array el1, Expr_array el2 
432 
 Expr_tuple el1, Expr_tuple el2 > 
433 
List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
434 
 Expr_arrow (e1, e2), Expr_arrow (e1', e2') > is_eq_expr e1 e1' && is_eq_expr e2 e2' 
435 
 Expr_fby (e1,e2), Expr_fby (e1',e2') > is_eq_expr e1 e1' && is_eq_expr e2 e2' 
436 
 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 
437 
(*  Expr_concat (e1,e2), Expr_concat (e1',e2') > is_eq_expr e1 e1' && is_eq_expr e2 e2' *) 
438 
(*  Expr_tail e, Expr_tail e' > is_eq_expr e e' *) 
439 
 Expr_pre e, Expr_pre e' > is_eq_expr e e' 
440 
 Expr_when (e, i, l), Expr_when (e', i', l') > l=l' && i=i' && is_eq_expr e e' 
441 
 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') 
442 
 Expr_appl (i, e, r), Expr_appl (i', e', r') > i=i' && r=r' && is_eq_expr e e' 
443 
 Expr_uclock(e, i), Expr_uclock(e', i') > i=i' && is_eq_expr e e' 
444 
 Expr_dclock(e, i), Expr_dclock(e', i') > i=i' && is_eq_expr e e' 
445 
 Expr_phclock(e, r), Expr_phclock(e', r') > r=r' && is_eq_expr e e' 
446 
 Expr_power (e1, i1), Expr_power (e2, i2) 
447 
 Expr_access (e1, i1), Expr_access (e2, i2) > is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2) 
448 
 _ > false 
449  
450 
let node_vars nd = 
451 
nd.node_inputs @ nd.node_locals @ nd.node_outputs 
452  
453 
let node_var id node = 
454 
List.find (fun v > v.var_id = id) (node_vars node) 
455  
456 
let node_eq id node = 
457 
List.find (fun eq > List.mem id eq.eq_lhs) node.node_eqs 
458  
459 
(* Consts unfoooolding *) 
460 
let is_const i consts = 
461 
List.exists (fun c > c.const_id = i) consts 
462  
463 
let get_const i consts = 
464 
let c = List.find (fun c > c.const_id = i) consts in 
465 
c.const_value 
466  
467 
let rec expr_unfold_consts consts e = 
468 
{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc } 
469  
470 
and expr_desc_unfold_consts consts e = 
471 
let unfold = expr_unfold_consts consts in 
472 
match e with 
473 
 Expr_const _ > e 
474 
 Expr_ident i > if is_const i consts then Expr_const (get_const i consts) else e 
475 
 Expr_array el > Expr_array (List.map unfold el) 
476 
 Expr_access (e1, d) > Expr_access (unfold e1, d) 
477 
 Expr_power (e1, d) > Expr_power (unfold e1, d) 
478 
 Expr_tuple el > Expr_tuple (List.map unfold el) 
479 
 Expr_ite (c, t, e) > Expr_ite (unfold c, unfold t, unfold e) 
480 
 Expr_arrow (e1, e2)> Expr_arrow (unfold e1, unfold e2) 
481 
 Expr_fby (e1, e2) > Expr_fby (unfold e1, unfold e2) 
482 
(*  Expr_concat (e1, e2) > Expr_concat (unfold e1, unfold e2) *) 
483 
(*  Expr_tail e' > Expr_tail (unfold e') *) 
484 
 Expr_pre e' > Expr_pre (unfold e') 
485 
 Expr_when (e', i, l)> Expr_when (unfold e', i, l) 
486 
 Expr_merge (i, hl) > Expr_merge (i, List.map (fun (t, h) > (t, unfold h)) hl) 
487 
 Expr_appl (i, e', i') > Expr_appl (i, unfold e', i') 
488 
 Expr_uclock (e', i) > Expr_uclock (unfold e', i) 
489 
 Expr_dclock (e', i) > Expr_dclock (unfold e', i) 
490 
 Expr_phclock _ > e 
491  
492 
let eq_unfold_consts consts eq = 
493 
{ eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs } 
494  
495 
let node_unfold_consts consts node = 
496 
{ node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs } 
497  
498 
let get_consts prog = 
499 
List.fold_left ( 
500 
fun consts decl > 
501 
match decl.top_decl_desc with 
502 
 Consts clist > clist@consts 
503 
 Node _  ImportedNode _  Open _ > consts 
504 
) [] prog 
505  
506  
507 
let get_nodes prog = 
508 
List.fold_left ( 
509 
fun nodes decl > 
510 
match decl.top_decl_desc with 
511 
 Node nd > nd::nodes 
512 
 Consts _  ImportedNode _  Open _ > nodes 
513 
) [] prog 
514  
515 
let prog_unfold_consts prog = 
516 
let consts = get_consts prog in 
517 
List.map ( 
518 
fun decl > match decl.top_decl_desc with 
519 
 Node nd > {decl with top_decl_desc = Node (node_unfold_consts consts nd)} 
520 
 _ > decl 
521 
) prog 
522  
523  
524  
525 
(************************************************************************) 
526 
(* Renaming *) 
527  
528 
(* applies the renaming function [fvar] to all variables of expression [expr] *) 
529 
let rec expr_replace_var fvar expr = 
530 
{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } 
531  
532 
and expr_desc_replace_var fvar expr_desc = 
533 
match expr_desc with 
534 
 Expr_const _ > expr_desc 
535 
 Expr_ident i > Expr_ident (fvar i) 
536 
 Expr_array el > Expr_array (List.map (expr_replace_var fvar) el) 
537 
 Expr_access (e1, d) > Expr_access (expr_replace_var fvar e1, d) 
538 
 Expr_power (e1, d) > Expr_power (expr_replace_var fvar e1, d) 
539 
 Expr_tuple el > Expr_tuple (List.map (expr_replace_var fvar) el) 
540 
 Expr_ite (c, t, e) > Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) 
541 
 Expr_arrow (e1, e2)> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 
542 
 Expr_fby (e1, e2) > Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) 
543 
 Expr_pre e' > Expr_pre (expr_replace_var fvar e') 
544 
 Expr_when (e', i, l)> Expr_when (expr_replace_var fvar e', fvar i, l) 
545 
 Expr_merge (i, hl) > Expr_merge (fvar i, List.map (fun (t, h) > (t, expr_replace_var fvar h)) hl) 
546 
 Expr_appl (i, e', i') > Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) > fvar x, l) i') 
547 
 _ > assert false 
548  
549 
(* Applies the renaming function [fvar] to every rhs 
550 
only when the corresponding lhs satisfies predicate [pvar] *) 
551 
let eq_replace_rhs_var pvar fvar eq = 
552 
let pvar l = List.exists pvar l in 
553 
let rec replace lhs rhs = 
554 
{ rhs with expr_desc = replace_desc lhs rhs.expr_desc } 
555 
and replace_desc lhs rhs_desc = 
556 
match lhs with 
557 
 [] > assert false 
558 
 [_] > if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc 
559 
 _ > 
560 
(match rhs_desc with 
561 
 Expr_tuple tl > 
562 
Expr_tuple (List.map2 (fun v e > replace [v] e) lhs tl) 
563 
 Expr_appl (f, arg, None) when Basic_library.is_internal_fun f > 
564 
let args = expr_list_of_expr arg in 
565 
Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None) 
566 
 Expr_array _ 
567 
 Expr_access _ 
568 
 Expr_power _ 
569 
 Expr_const _ 
570 
 Expr_ident _ 
571 
 Expr_appl _ > 
572 
if pvar lhs 
573 
then expr_desc_replace_var fvar rhs_desc 
574 
else rhs_desc 
575 
 Expr_ite (c, t, e) > Expr_ite (replace lhs c, replace lhs t, replace lhs e) 
576 
 Expr_arrow (e1, e2) > Expr_arrow (replace lhs e1, replace lhs e2) 
577 
 Expr_fby (e1, e2) > Expr_fby (replace lhs e1, replace lhs e2) 
578 
 Expr_pre e' > Expr_pre (replace lhs e') 
579 
 Expr_when (e', i, l) > let i' = if pvar lhs then fvar i else i 
580 
in Expr_when (replace lhs e', i', l) 
581 
 Expr_merge (i, hl) > let i' = if pvar lhs then fvar i else i 
582 
in Expr_merge (i', List.map (fun (t, h) > (t, replace lhs h)) hl) 
583 
 _ > assert false) 
584 
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } 
585  
586  
587 
let rec rename_expr f_node f_var f_const expr = 
588 
{ expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc } 
589 
and rename_expr_desc f_node f_var f_const expr_desc = 
590 
let re = rename_expr f_node f_var f_const in 
591 
match expr_desc with 
592 
 Expr_const _ > expr_desc 
593 
 Expr_ident i > Expr_ident (f_var i) 
594 
 Expr_array el > Expr_array (List.map re el) 
595 
 Expr_access (e1, d) > Expr_access (re e1, d) 
596 
 Expr_power (e1, d) > Expr_power (re e1, d) 
597 
 Expr_tuple el > Expr_tuple (List.map re el) 
598 
 Expr_ite (c, t, e) > Expr_ite (re c, re t, re e) 
599 
 Expr_arrow (e1, e2)> Expr_arrow (re e1, re e2) 
600 
 Expr_fby (e1, e2) > Expr_fby (re e1, re e2) 
601 
 Expr_pre e' > Expr_pre (re e') 
602 
 Expr_when (e', i, l)> Expr_when (re e', f_var i, l) 
603 
 Expr_merge (i, hl) > 
604 
Expr_merge (f_var i, List.map (fun (t, h) > (t, re h)) hl) 
605 
 Expr_appl (i, e', i') > 
606 
Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) > f_var x, l) i') 
607 
 _ > assert false 
608  
609 
let rename_node_annot f_node f_var f_const expr = 
610 
expr 
611 
(* TODO assert false *) 
612  
613 
let rename_expr_annot f_node f_var f_const annot = 
614 
annot 
615 
(* TODO assert false *) 
616  
617 
let rename_node f_node f_var f_const nd = 
618 
let rename_var v = { v with var_id = f_var v.var_id } in 
619 
let inputs = List.map rename_var nd.node_inputs in 
620 
let outputs = List.map rename_var nd.node_outputs in 
621 
let locals = List.map rename_var nd.node_locals in 
622 
let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in 
623 
let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in 
624 
let node_asserts = List.map 
625 
(fun a > 
626 
{ a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } 
627 
) nd.node_asserts 
628 
in 
629 
let eqs = List.map 
630 
(fun eq > { eq with 
631 
eq_lhs = List.map f_var eq.eq_lhs; 
632 
eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs 
633 
} ) nd.node_eqs 
634 
in 
635 
let spec = 
636 
Utils.option_map 
637 
(fun s > rename_node_annot f_node f_var f_const s) 
638 
nd.node_spec 
639 
in 
640 
let annot = 
641 
Utils.option_map 
642 
(fun s > rename_expr_annot f_node f_var f_const s) 
643 
nd.node_annot 
644 
in 
645 
{ 
646 
node_id = f_node nd.node_id; 
647 
node_type = nd.node_type; 
648 
node_clock = nd.node_clock; 
649 
node_inputs = inputs; 
650 
node_outputs = outputs; 
651 
node_locals = locals; 
652 
node_gencalls = gen_calls; 
653 
node_checks = node_checks; 
654 
node_asserts = node_asserts; 
655 
node_eqs = eqs; 
656 
node_dec_stateless = nd.node_dec_stateless; 
657 
node_stateless = nd.node_stateless; 
658 
node_spec = spec; 
659 
node_annot = annot; 
660 
} 
661  
662  
663 
let rename_const f_const c = 
664 
{ c with const_id = f_const c.const_id } 
665 

666 
let rename_prog f_node f_var f_const prog = 
667 
List.rev ( 
668 
List.fold_left (fun accu top > 
669 
(match top.top_decl_desc with 
670 
 Node nd > 
671 
{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) } 
672 
 Consts c > 
673 
{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) } 
674 
 ImportedNode _ 
675 
 Open _ > top) 
676 
::accu 
677 
) [] prog 
678 
) 
679  
680 
(**********************************************************************) 
681 
(* Pretty printers *) 
682  
683 
let pp_decl_type fmt tdecl = 
684 
match tdecl.top_decl_desc with 
685 
 Node nd > 
686 
fprintf fmt "%s: " nd.node_id; 
687 
Utils.reset_names (); 
688 
fprintf fmt "%a@ " Types.print_ty nd.node_type 
689 
 ImportedNode ind > 
690 
fprintf fmt "%s: " ind.nodei_id; 
691 
Utils.reset_names (); 
692 
fprintf fmt "%a@ " Types.print_ty ind.nodei_type 
693 
 Consts _  Open _ > () 
694  
695 
let pp_prog_type fmt tdecl_list = 
696 
Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list 
697  
698 
let pp_decl_clock fmt cdecl = 
699 
match cdecl.top_decl_desc with 
700 
 Node nd > 
701 
fprintf fmt "%s: " nd.node_id; 
702 
Utils.reset_names (); 
703 
fprintf fmt "%a@ " Clocks.print_ck nd.node_clock 
704 
 ImportedNode ind > 
705 
fprintf fmt "%s: " ind.nodei_id; 
706 
Utils.reset_names (); 
707 
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock 
708 
 Consts _  Open _ > () 
709  
710 
let pp_prog_clock fmt prog = 
711 
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog 
712  
713 
let pp_error fmt = function 
714 
Main_not_found > 
715 
fprintf fmt "Cannot compile node %s: could not find the node definition.@." 
716 
!Options.main_node 
717 
 Main_wrong_kind > 
718 
fprintf fmt 
719 
"Name %s does not correspond to a (nonimported) node definition.@." 
720 
!Options.main_node 
721 
 No_main_specified > 
722 
fprintf fmt "No main node specified@." 
723 
 Unbound_symbol sym > 
724 
fprintf fmt 
725 
"%s is undefined.@." 
726 
sym 
727 
 Already_bound_symbol sym > 
728 
fprintf fmt 
729 
"%s is already defined.@." 
730 
sym 
731  
732 
(* filling node table with internal functions *) 
733 
let vdecls_of_typ_ck cpt ty = 
734 
let loc = Location.dummy_loc in 
735 
List.map 
736 
(fun _ > incr cpt; 
737 
let name = sprintf "_var_%d" !cpt in 
738 
mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false)) 
739 
(Types.type_list_of_type ty) 
740  
741 
let mk_internal_node id = 
742 
let spec = None in 
743 
let ty = Env.lookup_value Basic_library.type_env id in 
744 
let ck = Env.lookup_value Basic_library.clock_env id in 
745 
let (tin, tout) = Types.split_arrow ty in 
746 
(*eprintf "internal fun %s: %d > %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*) 
747 
let cpt = ref (1) in 
748 
mktop_decl Location.dummy_loc 
749 
(ImportedNode 
750 
{nodei_id = id; 
751 
nodei_type = ty; 
752 
nodei_clock = ck; 
753 
nodei_inputs = vdecls_of_typ_ck cpt tin; 
754 
nodei_outputs = vdecls_of_typ_ck cpt tout; 
755 
nodei_stateless = Types.get_static_value ty <> None; 
756 
nodei_spec = spec}) 
757  
758 
let add_internal_funs () = 
759 
List.iter 
760 
(fun id > let nd = mk_internal_node id in Hashtbl.add node_table id nd) 
761 
Basic_library.internal_funs 
762  
763 
(* Local Variables: *) 
764 
(* compilecommand:"make C .." *) 
765 
(* End: *) 