lustrec / src / corelang.ml @ c1adf235
History  View  Annotate  Download (23.8 KB)
1 
(*  

2 
* SchedMCore  A MultiCore Scheduling Framework 
3 
* Copyright (C) 20092011, ONERA, Toulouse, FRANCE  LIFL, Lille, FRANCE 
4 
* 
5 
* This file is part of Prelude 
6 
* 
7 
* Prelude is free software; you can redistribute it and/or 
8 
* modify it under the terms of the GNU Lesser General Public License 
9 
* as published by the Free Software Foundation ; either version 2 of 
10 
* the License, or (at your option) any later version. 
11 
* 
12 
* Prelude is distributed in the hope that it will be useful, but 
13 
* WITHOUT ANY WARRANTY ; without even the implied warranty of 
14 
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 
15 
* Lesser General Public License for more details. 
16 
* 
17 
* You should have received a copy of the GNU Lesser General Public 
18 
* License along with this program ; if not, write to the Free Software 
19 
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 021111307 
20 
* USA 
21 
* *) 
22 
open Format 
23 
open LustreSpec 
24 
open Dimension 
25  
26 
(** The core language and its ast. Every element of the ast contains its 
27 
location in the program text. The type and clock of an ast element 
28 
is mutable (and initialized to dummy values). This avoids to have to 
29 
duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *) 
30  
31 
type ident = Utils.ident 
32 
type label = Utils.ident 
33 
type rat = Utils.rat 
34 
type tag = Utils.tag 
35  
36 
type constant = 
37 
 Const_int of int 
38 
 Const_real of string 
39 
 Const_float of float 
40 
 Const_array of constant list 
41 
 Const_tag of label 
42 
 Const_struct of (label * constant) list 
43  
44 
type type_dec = LustreSpec.type_dec 
45  
46 
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc} 
47  
48  
49 
type clock_dec = LustreSpec.clock_dec 
50  
51 
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc} 
52  
53 
type var_decl = LustreSpec.var_decl 
54  
55 
(* The tag of an expression is a unique identifier used to distinguish 
56 
different instances of the same node *) 
57 
type expr = 
58 
{expr_tag: tag; 
59 
expr_desc: expr_desc; 
60 
mutable expr_type: Types.type_expr; 
61 
mutable expr_clock: Clocks.clock_expr; 
62 
mutable expr_delay: Delay.delay_expr; 
63 
mutable expr_annot: LustreSpec.expr_annot option; 
64 
expr_loc: Location.t} 
65  
66 
and expr_desc = 
67 
 Expr_const of constant 
68 
 Expr_ident of ident 
69 
 Expr_tuple of expr list 
70 
 Expr_ite of expr * expr * expr 
71 
 Expr_arrow of expr * expr 
72 
 Expr_fby of expr * expr 
73 
 Expr_array of expr list 
74 
 Expr_access of expr * Dimension.dim_expr 
75 
 Expr_power of expr * Dimension.dim_expr 
76 
 Expr_pre of expr 
77 
 Expr_when of expr * ident * label 
78 
 Expr_merge of ident * (label * expr) list 
79 
 Expr_appl of call_t 
80 
 Expr_uclock of expr * int 
81 
 Expr_dclock of expr * int 
82 
 Expr_phclock of expr * rat 
83 
and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *) 
84  
85 
type eq = 
86 
{eq_lhs: ident list; 
87 
eq_rhs: expr; 
88 
eq_loc: Location.t} 
89  
90 
type assert_t = 
91 
{ 
92 
assert_expr: expr; 
93 
assert_loc: Location.t 
94 
} 
95  
96 
type node_desc = 
97 
{node_id: ident; 
98 
mutable node_type: Types.type_expr; 
99 
mutable node_clock: Clocks.clock_expr; 
100 
node_inputs: var_decl list; 
101 
node_outputs: var_decl list; 
102 
node_locals: var_decl list; 
103 
mutable node_gencalls: expr list; 
104 
mutable node_checks: Dimension.dim_expr list; 
105 
node_asserts: assert_t list; 
106 
node_eqs: eq list; 
107 
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 
let get_nodes prog = 
464 
List.fold_left ( 
465 
fun nodes decl > 
466 
match decl.top_decl_desc with 
467 
 Node nd > nd::nodes 
468 
 Consts _  ImportedNode _  Open _ > nodes 
469 
) [] prog 
470  
471 
let get_consts prog = 
472 
List.fold_left ( 
473 
fun consts decl > 
474 
match decl.top_decl_desc with 
475 
 Consts clist > clist@consts 
476 
 Node _  ImportedNode _  Open _ > consts 
477 
) [] prog 
478  
479  
480  
481 
(************************************************************************) 
482 
(* Renaming *) 
483  
484 
(* applies the renaming function [fvar] to all variables of expression [expr] *) 
485 
let rec expr_replace_var fvar expr = 
486 
{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } 
487  
488 
and expr_desc_replace_var fvar expr_desc = 
489 
match expr_desc with 
490 
 Expr_const _ > expr_desc 
491 
 Expr_ident i > Expr_ident (fvar i) 
492 
 Expr_array el > Expr_array (List.map (expr_replace_var fvar) el) 
493 
 Expr_access (e1, d) > Expr_access (expr_replace_var fvar e1, d) 
494 
 Expr_power (e1, d) > Expr_power (expr_replace_var fvar e1, d) 
495 
 Expr_tuple el > Expr_tuple (List.map (expr_replace_var fvar) el) 
496 
 Expr_ite (c, t, e) > Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) 
497 
 Expr_arrow (e1, e2)> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 
498 
 Expr_fby (e1, e2) > Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) 
499 
 Expr_pre e' > Expr_pre (expr_replace_var fvar e') 
500 
 Expr_when (e', i, l)> Expr_when (expr_replace_var fvar e', fvar i, l) 
501 
 Expr_merge (i, hl) > Expr_merge (fvar i, List.map (fun (t, h) > (t, expr_replace_var fvar h)) hl) 
502 
 Expr_appl (i, e', i') > Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) > fvar x, l) i') 
503 
 _ > assert false 
504  
505 
(* Applies the renaming function [fvar] to every rhs 
506 
only when the corresponding lhs satisfies predicate [pvar] *) 
507 
let eq_replace_rhs_var pvar fvar eq = 
508 
let pvar l = List.exists pvar l in 
509 
let rec replace lhs rhs = 
510 
{ rhs with expr_desc = replace_desc lhs rhs.expr_desc } 
511 
and replace_desc lhs rhs_desc = 
512 
match lhs with 
513 
 [] > assert false 
514 
 [_] > if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc 
515 
 _ > 
516 
(match rhs_desc with 
517 
 Expr_tuple tl > 
518 
Expr_tuple (List.map2 (fun v e > replace [v] e) lhs tl) 
519 
 Expr_appl (f, arg, None) when Basic_library.is_internal_fun f > 
520 
let args = expr_list_of_expr arg in 
521 
Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None) 
522 
 Expr_array _ 
523 
 Expr_access _ 
524 
 Expr_power _ 
525 
 Expr_const _ 
526 
 Expr_ident _ 
527 
 Expr_appl _ > 
528 
if pvar lhs 
529 
then expr_desc_replace_var fvar rhs_desc 
530 
else rhs_desc 
531 
 Expr_ite (c, t, e) > Expr_ite (replace lhs c, replace lhs t, replace lhs e) 
532 
 Expr_arrow (e1, e2) > Expr_arrow (replace lhs e1, replace lhs e2) 
533 
 Expr_fby (e1, e2) > Expr_fby (replace lhs e1, replace lhs e2) 
534 
 Expr_pre e' > Expr_pre (replace lhs e') 
535 
 Expr_when (e', i, l) > let i' = if pvar lhs then fvar i else i 
536 
in Expr_when (replace lhs e', i', l) 
537 
 Expr_merge (i, hl) > let i' = if pvar lhs then fvar i else i 
538 
in Expr_merge (i', List.map (fun (t, h) > (t, replace lhs h)) hl) 
539 
 _ > assert false) 
540 
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } 
541  
542  
543 
let rec rename_expr f_node f_var f_const expr = 
544 
{ expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc } 
545 
and rename_expr_desc f_node f_var f_const expr_desc = 
546 
let re = rename_expr f_node f_var f_const in 
547 
match expr_desc with 
548 
 Expr_const _ > expr_desc 
549 
 Expr_ident i > Expr_ident (f_var i) 
550 
 Expr_array el > Expr_array (List.map re el) 
551 
 Expr_access (e1, d) > Expr_access (re e1, d) 
552 
 Expr_power (e1, d) > Expr_power (re e1, d) 
553 
 Expr_tuple el > Expr_tuple (List.map re el) 
554 
 Expr_ite (c, t, e) > Expr_ite (re c, re t, re e) 
555 
 Expr_arrow (e1, e2)> Expr_arrow (re e1, re e2) 
556 
 Expr_fby (e1, e2) > Expr_fby (re e1, re e2) 
557 
 Expr_pre e' > Expr_pre (re e') 
558 
 Expr_when (e', i, l)> Expr_when (re e', f_var i, l) 
559 
 Expr_merge (i, hl) > 
560 
Expr_merge (f_var i, List.map (fun (t, h) > (t, re h)) hl) 
561 
 Expr_appl (i, e', i') > 
562 
Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) > f_var x, l) i') 
563 
 _ > assert false 
564  
565 
let rename_node_annot f_node f_var f_const expr = 
566 
expr 
567 
(* TODO assert false *) 
568  
569 
let rename_expr_annot f_node f_var f_const annot = 
570 
annot 
571 
(* TODO assert false *) 
572  
573 
let rename_node f_node f_var f_const nd = 
574 
let rename_var v = { v with var_id = f_var v.var_id } in 
575 
let inputs = List.map rename_var nd.node_inputs in 
576 
let outputs = List.map rename_var nd.node_outputs in 
577 
let locals = List.map rename_var nd.node_locals in 
578 
let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in 
579 
let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in 
580 
let node_asserts = List.map 
581 
(fun a > 
582 
{ a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } 
583 
) nd.node_asserts 
584 
in 
585 
let eqs = List.map 
586 
(fun eq > { eq with 
587 
eq_lhs = List.map f_var eq.eq_lhs; 
588 
eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs 
589 
} ) nd.node_eqs 
590 
in 
591 
let spec = 
592 
Utils.option_map 
593 
(fun s > rename_node_annot f_node f_var f_const s) 
594 
nd.node_spec 
595 
in 
596 
let annot = 
597 
Utils.option_map 
598 
(fun s > rename_expr_annot f_node f_var f_const s) 
599 
nd.node_annot 
600 
in 
601 
{ 
602 
node_id = f_node nd.node_id; 
603 
node_type = nd.node_type; 
604 
node_clock = nd.node_clock; 
605 
node_inputs = inputs; 
606 
node_outputs = outputs; 
607 
node_locals = locals; 
608 
node_gencalls = gen_calls; 
609 
node_checks = node_checks; 
610 
node_asserts = node_asserts; 
611 
node_eqs = eqs; 
612 
node_dec_stateless = nd.node_dec_stateless; 
613 
node_stateless = nd.node_stateless; 
614 
node_spec = spec; 
615 
node_annot = annot; 
616 
} 
617  
618  
619 
let rename_const f_const c = 
620 
{ c with const_id = f_const c.const_id } 
621 

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