lustrec / src / corelang.ml @ add75bcb
History  View  Annotate  Download (23.9 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 
let ident_of_expr expr = 
359 
match expr.expr_desc with 
360 
 Expr_ident id > id 
361 
 _ > assert false 
362  
363 
(* Caution, returns an untyped and unclocked expression *) 
364 
let expr_of_ident id loc = 
365 
{expr_tag = Utils.new_tag (); 
366 
expr_desc = Expr_ident id; 
367 
expr_type = Types.new_var (); 
368 
expr_clock = Clocks.new_var true; 
369 
expr_delay = Delay.new_var (); 
370 
expr_loc = loc; 
371 
expr_annot = None} 
372  
373 
let is_tuple_expr expr = 
374 
match expr.expr_desc with 
375 
 Expr_tuple _ > true 
376 
 _ > false 
377  
378 
let expr_list_of_expr expr = 
379 
match expr.expr_desc with 
380 
 Expr_tuple elist > 
381 
elist 
382 
 _ > [expr] 
383  
384 
let expr_of_expr_list loc elist = 
385 
match elist with 
386 
 [t] > { t with expr_loc = loc } 
387 
 t::_ > { t with expr_desc = Expr_tuple elist; expr_loc = loc } 
388 
 _ > assert false 
389  
390 
let call_of_expr expr = 
391 
match expr.expr_desc with 
392 
 Expr_appl (f, args, r) > (f, expr_list_of_expr args, r) 
393 
 _ > assert false 
394  
395 
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *) 
396 
let rec expr_of_dimension dim = 
397 
match dim.dim_desc with 
398 
 Dbool b > 
399 
mkexpr dim.dim_loc (Expr_const (const_of_bool b)) 
400 
 Dint i > 
401 
mkexpr dim.dim_loc (Expr_const (Const_int i)) 
402 
 Dident id > 
403 
mkexpr dim.dim_loc (Expr_ident id) 
404 
 Dite (c, t, e) > 
405 
mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e)) 
406 
 Dappl (id, args) > 
407 
mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None)) 
408 
 Dlink dim' > expr_of_dimension dim' 
409 
 Dvar 
410 
 Dunivar > (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim; 
411 
assert false) 
412  
413 
let dimension_of_const loc const = 
414 
match const with 
415 
 Const_int i > mkdim_int loc i 
416 
 Const_tag t when t = tag_true  t = tag_false > mkdim_bool loc (t = tag_true) 
417 
 _ > raise InvalidDimension 
418  
419 
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
420 
into dimension expressions *) 
421 
let rec dimension_of_expr expr = 
422 
match expr.expr_desc with 
423 
 Expr_const c > dimension_of_const expr.expr_loc c 
424 
 Expr_ident id > mkdim_ident expr.expr_loc id 
425 
 Expr_appl (f, args, None) when Basic_library.is_internal_fun f > 
426 
let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in 
427 
if k = None then raise InvalidDimension; 
428 
mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args)) 
429 
 Expr_ite (i, t, e) > 
430 
mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e) 
431 
 _ > raise InvalidDimension (* not a simple dimension expression *) 
432  
433  
434 
let sort_handlers hl = 
435 
List.sort (fun (t, _) (t', _) > compare t t') hl 
436  
437 
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with 
438 
 Expr_const c1, Expr_const c2 > c1 = c2 
439 
 Expr_ident i1, Expr_ident i2 > i1 = i2 
440 
 Expr_array el1, Expr_array el2 
441 
 Expr_tuple el1, Expr_tuple el2 > 
442 
List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
443 
 Expr_arrow (e1, e2), Expr_arrow (e1', e2') > is_eq_expr e1 e1' && is_eq_expr e2 e2' 
444 
 Expr_fby (e1,e2), Expr_fby (e1',e2') > is_eq_expr e1 e1' && is_eq_expr e2 e2' 
445 
 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 
446 
(*  Expr_concat (e1,e2), Expr_concat (e1',e2') > is_eq_expr e1 e1' && is_eq_expr e2 e2' *) 
447 
(*  Expr_tail e, Expr_tail e' > is_eq_expr e e' *) 
448 
 Expr_pre e, Expr_pre e' > is_eq_expr e e' 
449 
 Expr_when (e, i, l), Expr_when (e', i', l') > l=l' && i=i' && is_eq_expr e e' 
450 
 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') 
451 
 Expr_appl (i, e, r), Expr_appl (i', e', r') > i=i' && r=r' && is_eq_expr e e' 
452 
 Expr_uclock(e, i), Expr_uclock(e', i') > i=i' && is_eq_expr e e' 
453 
 Expr_dclock(e, i), Expr_dclock(e', i') > i=i' && is_eq_expr e e' 
454 
 Expr_phclock(e, r), Expr_phclock(e', r') > r=r' && is_eq_expr e e' 
455 
 Expr_power (e1, i1), Expr_power (e2, i2) 
456 
 Expr_access (e1, i1), Expr_access (e2, i2) > is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2) 
457 
 _ > false 
458  
459 
let node_vars nd = 
460 
nd.node_inputs @ nd.node_locals @ nd.node_outputs 
461  
462 
let node_var id node = 
463 
List.find (fun v > v.var_id = id) (node_vars node) 
464  
465 
let node_eq id node = 
466 
List.find (fun eq > List.mem id eq.eq_lhs) node.node_eqs 
467  
468 
let get_nodes prog = 
469 
List.fold_left ( 
470 
fun nodes decl > 
471 
match decl.top_decl_desc with 
472 
 Node nd > nd::nodes 
473 
 Consts _  ImportedNode _  Open _ > nodes 
474 
) [] prog 
475  
476 
let get_consts prog = 
477 
List.fold_left ( 
478 
fun consts decl > 
479 
match decl.top_decl_desc with 
480 
 Consts clist > clist@consts 
481 
 Node _  ImportedNode _  Open _ > consts 
482 
) [] prog 
483  
484  
485  
486 
(************************************************************************) 
487 
(* Renaming *) 
488  
489 
(* applies the renaming function [fvar] to all variables of expression [expr] *) 
490 
let rec expr_replace_var fvar expr = 
491 
{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } 
492  
493 
and expr_desc_replace_var fvar expr_desc = 
494 
match expr_desc with 
495 
 Expr_const _ > expr_desc 
496 
 Expr_ident i > Expr_ident (fvar i) 
497 
 Expr_array el > Expr_array (List.map (expr_replace_var fvar) el) 
498 
 Expr_access (e1, d) > Expr_access (expr_replace_var fvar e1, d) 
499 
 Expr_power (e1, d) > Expr_power (expr_replace_var fvar e1, d) 
500 
 Expr_tuple el > Expr_tuple (List.map (expr_replace_var fvar) el) 
501 
 Expr_ite (c, t, e) > Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) 
502 
 Expr_arrow (e1, e2)> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 
503 
 Expr_fby (e1, e2) > Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) 
504 
 Expr_pre e' > Expr_pre (expr_replace_var fvar e') 
505 
 Expr_when (e', i, l)> Expr_when (expr_replace_var fvar e', fvar i, l) 
506 
 Expr_merge (i, hl) > Expr_merge (fvar i, List.map (fun (t, h) > (t, expr_replace_var fvar h)) hl) 
507 
 Expr_appl (i, e', i') > Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) > fvar x, l) i') 
508 
 _ > assert false 
509  
510 
(* Applies the renaming function [fvar] to every rhs 
511 
only when the corresponding lhs satisfies predicate [pvar] *) 
512 
let eq_replace_rhs_var pvar fvar eq = 
513 
let pvar l = List.exists pvar l in 
514 
let rec replace lhs rhs = 
515 
{ rhs with expr_desc = replace_desc lhs rhs.expr_desc } 
516 
and replace_desc lhs rhs_desc = 
517 
match lhs with 
518 
 [] > assert false 
519 
 [_] > if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc 
520 
 _ > 
521 
(match rhs_desc with 
522 
 Expr_tuple tl > 
523 
Expr_tuple (List.map2 (fun v e > replace [v] e) lhs tl) 
524 
 Expr_appl (f, arg, None) when Basic_library.is_internal_fun f > 
525 
let args = expr_list_of_expr arg in 
526 
Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None) 
527 
 Expr_array _ 
528 
 Expr_access _ 
529 
 Expr_power _ 
530 
 Expr_const _ 
531 
 Expr_ident _ 
532 
 Expr_appl _ > 
533 
if pvar lhs 
534 
then expr_desc_replace_var fvar rhs_desc 
535 
else rhs_desc 
536 
 Expr_ite (c, t, e) > Expr_ite (replace lhs c, replace lhs t, replace lhs e) 
537 
 Expr_arrow (e1, e2) > Expr_arrow (replace lhs e1, replace lhs e2) 
538 
 Expr_fby (e1, e2) > Expr_fby (replace lhs e1, replace lhs e2) 
539 
 Expr_pre e' > Expr_pre (replace lhs e') 
540 
 Expr_when (e', i, l) > let i' = if pvar lhs then fvar i else i 
541 
in Expr_when (replace lhs e', i', l) 
542 
 Expr_merge (i, hl) > let i' = if pvar lhs then fvar i else i 
543 
in Expr_merge (i', List.map (fun (t, h) > (t, replace lhs h)) hl) 
544 
 _ > assert false) 
545 
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } 
546  
547  
548 
let rec rename_expr f_node f_var f_const expr = 
549 
{ expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc } 
550 
and rename_expr_desc f_node f_var f_const expr_desc = 
551 
let re = rename_expr f_node f_var f_const in 
552 
match expr_desc with 
553 
 Expr_const _ > expr_desc 
554 
 Expr_ident i > Expr_ident (f_var i) 
555 
 Expr_array el > Expr_array (List.map re el) 
556 
 Expr_access (e1, d) > Expr_access (re e1, d) 
557 
 Expr_power (e1, d) > Expr_power (re e1, d) 
558 
 Expr_tuple el > Expr_tuple (List.map re el) 
559 
 Expr_ite (c, t, e) > Expr_ite (re c, re t, re e) 
560 
 Expr_arrow (e1, e2)> Expr_arrow (re e1, re e2) 
561 
 Expr_fby (e1, e2) > Expr_fby (re e1, re e2) 
562 
 Expr_pre e' > Expr_pre (re e') 
563 
 Expr_when (e', i, l)> Expr_when (re e', f_var i, l) 
564 
 Expr_merge (i, hl) > 
565 
Expr_merge (f_var i, List.map (fun (t, h) > (t, re h)) hl) 
566 
 Expr_appl (i, e', i') > 
567 
Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) > f_var x, l) i') 
568 
 _ > assert false 
569  
570 
let rename_node_annot f_node f_var f_const expr = 
571 
expr 
572 
(* TODO assert false *) 
573  
574 
let rename_expr_annot f_node f_var f_const annot = 
575 
annot 
576 
(* TODO assert false *) 
577  
578 
let rename_node f_node f_var f_const nd = 
579 
let rename_var v = { v with var_id = f_var v.var_id } in 
580 
let inputs = List.map rename_var nd.node_inputs in 
581 
let outputs = List.map rename_var nd.node_outputs in 
582 
let locals = List.map rename_var nd.node_locals in 
583 
let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in 
584 
let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in 
585 
let node_asserts = List.map 
586 
(fun a > 
587 
{ a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } 
588 
) nd.node_asserts 
589 
in 
590 
let eqs = List.map 
591 
(fun eq > { eq with 
592 
eq_lhs = List.map f_var eq.eq_lhs; 
593 
eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs 
594 
} ) nd.node_eqs 
595 
in 
596 
let spec = 
597 
Utils.option_map 
598 
(fun s > rename_node_annot f_node f_var f_const s) 
599 
nd.node_spec 
600 
in 
601 
let annot = 
602 
Utils.option_map 
603 
(fun s > rename_expr_annot f_node f_var f_const s) 
604 
nd.node_annot 
605 
in 
606 
{ 
607 
node_id = f_node nd.node_id; 
608 
node_type = nd.node_type; 
609 
node_clock = nd.node_clock; 
610 
node_inputs = inputs; 
611 
node_outputs = outputs; 
612 
node_locals = locals; 
613 
node_gencalls = gen_calls; 
614 
node_checks = node_checks; 
615 
node_asserts = node_asserts; 
616 
node_eqs = eqs; 
617 
node_dec_stateless = nd.node_dec_stateless; 
618 
node_stateless = nd.node_stateless; 
619 
node_spec = spec; 
620 
node_annot = annot; 
621 
} 
622  
623  
624 
let rename_const f_const c = 
625 
{ c with const_id = f_const c.const_id } 
626 

627 
let rename_prog f_node f_var f_const prog = 
628 
List.rev ( 
629 
List.fold_left (fun accu top > 
630 
(match top.top_decl_desc with 
631 
 Node nd > 
632 
{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) } 
633 
 Consts c > 
634 
{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) } 
635 
 ImportedNode _ 
636 
 Open _ > top) 
637 
::accu 
638 
) [] prog 
639 
) 
640  
641 
(**********************************************************************) 
642 
(* Pretty printers *) 
643  
644 
let pp_decl_type fmt tdecl = 
645 
match tdecl.top_decl_desc with 
646 
 Node nd > 
647 
fprintf fmt "%s: " nd.node_id; 
648 
Utils.reset_names (); 
649 
fprintf fmt "%a@ " Types.print_ty nd.node_type 
650 
 ImportedNode ind > 
651 
fprintf fmt "%s: " ind.nodei_id; 
652 
Utils.reset_names (); 
653 
fprintf fmt "%a@ " Types.print_ty ind.nodei_type 
654 
 Consts _  Open _ > () 
655  
656 
let pp_prog_type fmt tdecl_list = 
657 
Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list 
658  
659 
let pp_decl_clock fmt cdecl = 
660 
match cdecl.top_decl_desc with 
661 
 Node nd > 
662 
fprintf fmt "%s: " nd.node_id; 
663 
Utils.reset_names (); 
664 
fprintf fmt "%a@ " Clocks.print_ck nd.node_clock 
665 
 ImportedNode ind > 
666 
fprintf fmt "%s: " ind.nodei_id; 
667 
Utils.reset_names (); 
668 
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock 
669 
 Consts _  Open _ > () 
670  
671 
let pp_prog_clock fmt prog = 
672 
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog 
673  
674 
let pp_error fmt = function 
675 
Main_not_found > 
676 
fprintf fmt "Cannot compile node %s: could not find the node definition.@." 
677 
!Options.main_node 
678 
 Main_wrong_kind > 
679 
fprintf fmt 
680 
"Name %s does not correspond to a (nonimported) node definition.@." 
681 
!Options.main_node 
682 
 No_main_specified > 
683 
fprintf fmt "No main node specified@." 
684 
 Unbound_symbol sym > 
685 
fprintf fmt 
686 
"%s is undefined.@." 
687 
sym 
688 
 Already_bound_symbol sym > 
689 
fprintf fmt 
690 
"%s is already defined.@." 
691 
sym 
692  
693 
(* filling node table with internal functions *) 
694 
let vdecls_of_typ_ck cpt ty = 
695 
let loc = Location.dummy_loc in 
696 
List.map 
697 
(fun _ > incr cpt; 
698 
let name = sprintf "_var_%d" !cpt in 
699 
mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false)) 
700 
(Types.type_list_of_type ty) 
701  
702 
let mk_internal_node id = 
703 
let spec = None in 
704 
let ty = Env.lookup_value Basic_library.type_env id in 
705 
let ck = Env.lookup_value Basic_library.clock_env id in 
706 
let (tin, tout) = Types.split_arrow ty in 
707 
(*eprintf "internal fun %s: %d > %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*) 
708 
let cpt = ref (1) in 
709 
mktop_decl Location.dummy_loc 
710 
(ImportedNode 
711 
{nodei_id = id; 
712 
nodei_type = ty; 
713 
nodei_clock = ck; 
714 
nodei_inputs = vdecls_of_typ_ck cpt tin; 
715 
nodei_outputs = vdecls_of_typ_ck cpt tout; 
716 
nodei_stateless = Types.get_static_value ty <> None; 
717 
nodei_spec = spec; 
718 
nodei_prototype = None; 
719 
nodei_in_lib = None; 
720 
}) 
721  
722 
let add_internal_funs () = 
723 
List.iter 
724 
(fun id > let nd = mk_internal_node id in Hashtbl.add node_table id nd) 
725 
Basic_library.internal_funs 
726  
727 
(* Local Variables: *) 
728 
(* compilecommand:"make C .." *) 
729 
(* End: *) 