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

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