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

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