lustrec / src / clock_calculus.ml @ 3b2bd83d
History  View  Annotate  Download (26.6 KB)
1 
(********************************************************************) 

2 
(* *) 
3 
(* The LustreC compiler toolset / The LustreC Development Team *) 
4 
(* Copyright 2012   ONERA  CNRS  INPT  LIFL *) 
5 
(* *) 
6 
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) 
7 
(* under the terms of the GNU Lesser General Public License *) 
8 
(* version 2.1. *) 
9 
(* *) 
10 
(* This file was originally from the Prelude compiler *) 
11 
(* *) 
12 
(********************************************************************) 
13  
14  
15 
(** Main clockcalculus module. Based on type inference algorithms with 
16 
destructive unification. Uses a bit of subtyping for periodic clocks. *) 
17  
18 
(* Though it shares similarities with the typing module, no code 
19 
is shared. Simple environments, very limited identifier scoping, no 
20 
identifier redefinition allowed. *) 
21 
open Utils 
22 
open LustreSpec 
23 
open Corelang 
24 
open Clocks 
25 
open Format 
26  
27 
let loc_of_cond loc_containing id = 
28 
let pos_start = 
29 
{loc_containing.Location.loc_end with 
30 
Lexing.pos_cnum=loc_containing.Location.loc_end.Lexing.pos_cnum(String.length id)} 
31 
in 
32 
{Location.loc_start = pos_start; 
33 
Location.loc_end = loc_containing.Location.loc_end} 
34  
35 
(** [occurs cvar ck] returns true if the clock variable [cvar] occurs in 
36 
clock [ck]. False otherwise. *) 
37 
let rec occurs cvar ck = 
38 
let ck = repr ck in 
39 
match ck.cdesc with 
40 
 Carrow (ck1, ck2) > 
41 
(occurs cvar ck1)  (occurs cvar ck2) 
42 
 Ctuple ckl > 
43 
List.exists (occurs cvar) ckl 
44 
 Con (ck',_,_) > occurs cvar ck' 
45 
 Cvar > ck=cvar 
46 
 Cunivar > false 
47 
 Clink ck' > occurs cvar ck' 
48 
 Ccarrying (_,ck') > occurs cvar ck' 
49  
50 
(* Clocks generalization *) 
51 
let rec generalize_carrier cr = 
52 
match cr.carrier_desc with 
53 
 Carry_const _ 
54 
 Carry_name > 
55 
if cr.carrier_scoped then 
56 
raise (Scope_carrier cr); 
57 
cr.carrier_desc < Carry_var 
58 
 Carry_var > () 
59 
 Carry_link cr' > generalize_carrier cr' 
60  
61 
(** Promote monomorphic clock variables to polymorphic clock variables. *) 
62 
(* Generalize by sideeffects *) 
63 
let rec generalize ck = 
64 
match ck.cdesc with 
65 
 Carrow (ck1,ck2) > 
66 
generalize ck1; generalize ck2 
67 
 Ctuple clist > 
68 
List.iter generalize clist 
69 
 Con (ck',cr,_) > generalize ck'; generalize_carrier cr 
70 
 Cvar > 
71 
if ck.cscoped then 
72 
raise (Scope_clock ck); 
73 
ck.cdesc < Cunivar 
74 
 Cunivar > () 
75 
 Clink ck' > 
76 
generalize ck' 
77 
 Ccarrying (cr,ck') > 
78 
generalize_carrier cr; generalize ck' 
79  
80 
let try_generalize ck_node loc = 
81 
try 
82 
generalize ck_node 
83 
with (Scope_carrier cr) > 
84 
raise (Error (loc, Carrier_extrusion (ck_node, cr))) 
85 
 (Scope_clock ck) > 
86 
raise (Error (loc, Clock_extrusion (ck_node, ck))) 
87  
88 
(* Clocks instanciation *) 
89 
let instantiate_carrier cr inst_cr_vars = 
90 
let cr = carrier_repr cr in 
91 
match cr.carrier_desc with 
92 
 Carry_const _ 
93 
 Carry_name > cr 
94 
 Carry_link _ > 
95 
failwith "Internal error" 
96 
 Carry_var > 
97 
try 
98 
List.assoc cr.carrier_id !inst_cr_vars 
99 
with Not_found > 
100 
let cr_var = new_carrier Carry_name true in 
101 
inst_cr_vars := (cr.carrier_id,cr_var)::!inst_cr_vars; 
102 
cr_var 
103  
104 
(** Downgrade polymorphic clock variables to monomorphic clock variables *) 
105 
(* inst_ck_vars ensures that a polymorphic variable is instanciated with 
106 
the same monomorphic variable if it occurs several times in the same 
107 
type. inst_cr_vars is the same for carriers. *) 
108 
let rec instantiate inst_ck_vars inst_cr_vars ck = 
109 
match ck.cdesc with 
110 
 Carrow (ck1,ck2) > 
111 
{ck with cdesc = 
112 
Carrow ((instantiate inst_ck_vars inst_cr_vars ck1), 
113 
(instantiate inst_ck_vars inst_cr_vars ck2))} 
114 
 Ctuple cklist > 
115 
{ck with cdesc = Ctuple 
116 
(List.map (instantiate inst_ck_vars inst_cr_vars) cklist)} 
117 
 Con (ck',c,l) > 
118 
let c' = instantiate_carrier c inst_cr_vars in 
119 
{ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)} 
120 
 Cvar > ck 
121 
 Clink ck' > 
122 
{ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')} 
123 
 Ccarrying (cr,ck') > 
124 
let cr' = instantiate_carrier cr inst_cr_vars in 
125 
{ck with cdesc = 
126 
Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')} 
127 
 Cunivar > 
128 
try 
129 
List.assoc ck.cid !inst_ck_vars 
130 
with Not_found > 
131 
let var = new_ck Cvar true in 
132 
inst_ck_vars := (ck.cid, var)::!inst_ck_vars; 
133 
var 
134  
135  
136 
let rec update_scope_carrier scoped cr = 
137 
if (not scoped) then 
138 
begin 
139 
cr.carrier_scoped < scoped; 
140 
match cr.carrier_desc with 
141 
 Carry_const _  Carry_name  Carry_var > () 
142 
 Carry_link cr' > update_scope_carrier scoped cr' 
143 
end 
144  
145 
let rec update_scope scoped ck = 
146 
if (not scoped) then 
147 
begin 
148 
ck.cscoped < scoped; 
149 
match ck.cdesc with 
150 
 Carrow (ck1,ck2) > 
151 
update_scope scoped ck1; update_scope scoped ck2 
152 
 Ctuple clist > 
153 
List.iter (update_scope scoped) clist 
154 
 Con (ck',cr,_) > update_scope scoped ck'(*; update_scope_carrier scoped cr*) 
155 
 Cvar  Cunivar > () 
156 
 Clink ck' > 
157 
update_scope scoped ck' 
158 
 Ccarrying (cr,ck') > 
159 
update_scope_carrier scoped cr; update_scope scoped ck' 
160 
end 
161  
162  
163 
(* Unifies two clock carriers *) 
164 
let unify_carrier cr1 cr2 = 
165 
let cr1 = carrier_repr cr1 in 
166 
let cr2 = carrier_repr cr2 in 
167 
if cr1==cr2 then () 
168 
else 
169 
match cr1.carrier_desc, cr2.carrier_desc with 
170 
 Carry_const id1, Carry_const id2 > 
171 
if id1 <> id2 then raise (Mismatch (cr1, cr2)) 
172 
 Carry_const _, Carry_name > 
173 
begin 
174 
cr2.carrier_desc < Carry_link cr1; 
175 
update_scope_carrier cr2.carrier_scoped cr1 
176 
end 
177 
 Carry_name, Carry_const _ > 
178 
begin 
179 
cr1.carrier_desc < Carry_link cr2; 
180 
update_scope_carrier cr1.carrier_scoped cr2 
181 
end 
182 
 Carry_name, Carry_name > 
183 
if cr1.carrier_id < cr2.carrier_id then 
184 
begin 
185 
cr2.carrier_desc < Carry_link cr1; 
186 
update_scope_carrier cr2.carrier_scoped cr1 
187 
end 
188 
else 
189 
begin 
190 
cr1.carrier_desc < Carry_link cr2; 
191 
update_scope_carrier cr1.carrier_scoped cr2 
192 
end 
193 
 _,_ > assert false 
194  
195 
(* Semiunifies two clock carriers *) 
196 
let semi_unify_carrier cr1 cr2 = 
197 
let cr1 = carrier_repr cr1 in 
198 
let cr2 = carrier_repr cr2 in 
199 
if cr1==cr2 then () 
200 
else 
201 
match cr1.carrier_desc, cr2.carrier_desc with 
202 
 Carry_const id1, Carry_const id2 > 
203 
if id1 <> id2 then raise (Mismatch (cr1, cr2)) 
204 
 Carry_const _, Carry_name > 
205 
begin 
206 
cr2.carrier_desc < Carry_link cr1; 
207 
update_scope_carrier cr2.carrier_scoped cr1 
208 
end 
209 
 Carry_name, Carry_const _ > raise (Mismatch (cr1, cr2)) 
210 
 Carry_name, Carry_name > 
211 
if cr1.carrier_id < cr2.carrier_id then 
212 
begin 
213 
cr2.carrier_desc < Carry_link cr1; 
214 
update_scope_carrier cr2.carrier_scoped cr1 
215 
end 
216 
else 
217 
begin 
218 
cr1.carrier_desc < Carry_link cr2; 
219 
update_scope_carrier cr1.carrier_scoped cr2 
220 
end 
221 
 _,_ > assert false 
222  
223 
let try_unify_carrier ck1 ck2 loc = 
224 
try 
225 
unify_carrier ck1 ck2 
226 
with 
227 
 Unify (ck1',ck2') > 
228 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
229 
 Mismatch (cr1,cr2) > 
230 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
231  
232 
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify 
233 
(ck1,ck2)] if the clocks are not unifiable.*) 
234 
let rec unify ck1 ck2 = 
235 
let ck1 = repr ck1 in 
236 
let ck2 = repr ck2 in 
237 
if ck1==ck2 then 
238 
() 
239 
else 
240 
match ck1.cdesc,ck2.cdesc with 
241 
 Cvar, Cvar > 
242 
if ck1.cid < ck2.cid then 
243 
begin 
244 
ck2.cdesc < Clink (simplify ck1); 
245 
update_scope ck2.cscoped ck1 
246 
end 
247 
else 
248 
begin 
249 
ck1.cdesc < Clink (simplify ck2); 
250 
update_scope ck1.cscoped ck2 
251 
end 
252 
 (Cvar, _) when (not (occurs ck1 ck2)) > 
253 
update_scope ck1.cscoped ck2; 
254 
ck1.cdesc < Clink (simplify ck2) 
255 
 (_, Cvar) when (not (occurs ck2 ck1)) > 
256 
update_scope ck2.cscoped ck1; 
257 
ck2.cdesc < Clink (simplify ck1) 
258 
 Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') > 
259 
unify_carrier cr1 cr2; 
260 
unify ck1' ck2' 
261 
 Ccarrying (_,_),_  _,Ccarrying (_,_) > 
262 
raise (Unify (ck1,ck2)) 
263 
 Carrow (c1,c2), Carrow (c1',c2') > 
264 
unify c1 c1'; unify c2 c2' 
265 
 Ctuple ckl1, Ctuple ckl2 > 
266 
if (List.length ckl1) <> (List.length ckl2) then 
267 
raise (Unify (ck1,ck2)); 
268 
List.iter2 unify ckl1 ckl2 
269 
 Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 > 
270 
unify_carrier c1 c2; 
271 
unify ck' ck'' 
272 
 Cunivar, _  _, Cunivar > () 
273 
 _,_ > raise (Unify (ck1,ck2)) 
274  
275 
(** [unify ck1 ck2] semiunifies clocks [ck1] and [ck2]. Raises [Unify 
276 
(ck1,ck2)] if the clocks are not semiunifiable.*) 
277 
let rec semi_unify ck1 ck2 = 
278 
let ck1 = repr ck1 in 
279 
let ck2 = repr ck2 in 
280 
if ck1==ck2 then 
281 
() 
282 
else 
283 
match ck1.cdesc,ck2.cdesc with 
284 
 Cvar, Cvar > 
285 
if ck1.cid < ck2.cid then 
286 
begin 
287 
ck2.cdesc < Clink (simplify ck1); 
288 
update_scope ck2.cscoped ck1 
289 
end 
290 
else 
291 
begin 
292 
ck1.cdesc < Clink (simplify ck2); 
293 
update_scope ck1.cscoped ck2 
294 
end 
295 
 (Cvar, _) > raise (Unify (ck1,ck2)) 
296 
 (_, Cvar) when (not (occurs ck2 ck1)) > 
297 
update_scope ck2.cscoped ck1; 
298 
ck2.cdesc < Clink (simplify ck1) 
299 
 Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') > 
300 
semi_unify_carrier cr1 cr2; 
301 
semi_unify ck1' ck2' 
302 
 Ccarrying (_,_),_  _,Ccarrying (_,_) > 
303 
raise (Unify (ck1,ck2)) 
304 
 Carrow (c1,c2), Carrow (c1',c2') > 
305 
begin 
306 
semi_unify c1 c1'; 
307 
semi_unify c2 c2' 
308 
end 
309 
 Ctuple ckl1, Ctuple ckl2 > 
310 
if (List.length ckl1) <> (List.length ckl2) then 
311 
raise (Unify (ck1,ck2)); 
312 
List.iter2 semi_unify ckl1 ckl2 
313 
 Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 > 
314 
semi_unify_carrier c1 c2; 
315 
semi_unify ck' ck'' 
316 
 Cunivar, _  _, Cunivar > () 
317 
 _,_ > raise (Unify (ck1,ck2)) 
318  
319 
(* Returns the value corresponding to a pclock (integer) factor 
320 
expression. Expects a constant expression (checked by typing). *) 
321 
let int_factor_of_expr e = 
322 
match e.expr_desc with 
323 
 Expr_const 
324 
(Const_int i) > i 
325 
 _ > failwith "Internal error: int_factor_of_expr" 
326  
327 
(** [clock_uncarry ck] drops the possible carrier(s) name(s) from clock [ck] *) 
328 
let rec clock_uncarry ck = 
329 
let ck = repr ck in 
330 
match ck.cdesc with 
331 
 Ccarrying (_, ck') > ck' 
332 
 Con(ck', cr, l) > clock_on (clock_uncarry ck') cr l 
333 
 Ctuple ckl > clock_of_clock_list (List.map clock_uncarry ckl) 
334 
 _ > ck 
335  
336 
let try_unify ck1 ck2 loc = 
337 
try 
338 
unify ck1 ck2 
339 
with 
340 
 Unify (ck1',ck2') > 
341 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
342 
 Mismatch (cr1,cr2) > 
343 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
344  
345 
let try_semi_unify ck1 ck2 loc = 
346 
try 
347 
semi_unify ck1 ck2 
348 
with 
349 
 Unify (ck1',ck2') > 
350 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
351 
 Mismatch (cr1,cr2) > 
352 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
353  
354 
(* ck2 is a subtype of ck1 *) 
355 
let rec sub_unify sub ck1 ck2 = 
356 
match (repr ck1).cdesc, (repr ck2).cdesc with 
357 
 Ctuple cl1 , Ctuple cl2 > 
358 
if List.length cl1 <> List.length cl2 
359 
then raise (Unify (ck1, ck2)) 
360 
else List.iter2 (sub_unify sub) cl1 cl2 
361 
 Ctuple [c1] , _ > sub_unify sub c1 ck2 
362 
 _ , Ctuple [c2] > sub_unify sub ck1 c2 
363 
 Con (c1, cr1, t1) , Con (c2, cr2, t2) when t1=t2 > 
364 
begin 
365 
unify_carrier cr1 cr2; 
366 
sub_unify sub c1 c2 
367 
end 
368 
 Ccarrying (cr1, c1), Ccarrying (cr2, c2)> 
369 
begin 
370 
unify_carrier cr1 cr2; 
371 
sub_unify sub c1 c2 
372 
end 
373 
 _, Ccarrying (_, c2) when sub > sub_unify sub ck1 c2 
374 
 _ > unify ck1 ck2 
375  
376 
let try_sub_unify sub ck1 ck2 loc = 
377 
try 
378 
sub_unify sub ck1 ck2 
379 
with 
380 
 Unify (ck1',ck2') > 
381 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
382 
 Mismatch (cr1,cr2) > 
383 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
384  
385 
(* Unifies all the clock variables in the clock type of a tuple 
386 
expression, so that the clock type only uses at most one clock variable *) 
387 
let unify_tuple_clock ref_ck_opt ck loc = 
388 
(*(match ref_ck_opt with 
389 
 None > Format.eprintf "unify_tuple_clock None %a@." Clocks.print_ck ck 
390 
 Some ck' > Format.eprintf "unify_tuple_clock (Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*) 
391 
let ck_var = ref ref_ck_opt in 
392 
let rec aux ck = 
393 
match (repr ck).cdesc with 
394 
 Con _ 
395 
 Cvar > 
396 
begin 
397 
match !ck_var with 
398 
 None > 
399 
ck_var:=Some ck 
400 
 Some v > 
401 
(* may fail *) 
402 
try_unify ck v loc 
403 
end 
404 
 Ctuple cl > 
405 
List.iter aux cl 
406 
 Carrow _ > assert false (* should not occur *) 
407 
 Ccarrying (_, ck1) > 
408 
aux ck1 
409 
 _ > () 
410 
in aux ck 
411  
412 
(* Unifies all the clock variables in the clock type of an imported 
413 
node, so that the clock type only uses at most one base clock variable, 
414 
that is, the activation clock of the node *) 
415 
let unify_imported_clock ref_ck_opt ck loc = 
416 
let ck_var = ref ref_ck_opt in 
417 
let rec aux ck = 
418 
match (repr ck).cdesc with 
419 
 Cvar > 
420 
begin 
421 
match !ck_var with 
422 
 None > 
423 
ck_var:=Some ck 
424 
 Some v > 
425 
(* cannot fail *) 
426 
try_unify ck v loc 
427 
end 
428 
 Ctuple cl > 
429 
List.iter aux cl 
430 
 Carrow (ck1,ck2) > 
431 
aux ck1; aux ck2 
432 
 Ccarrying (_, ck1) > 
433 
aux ck1 
434 
 Con (ck1, _, _) > aux ck1 
435 
 _ > () 
436 
in 
437 
aux ck 
438  
439 
(* Computes the root clock of a tuple or a node clock, 
440 
which is not the same as the base clock. 
441 
Root clock will be used as the call clock 
442 
of a given node instance *) 
443 
let compute_root_clock ck = 
444 
let root = Clocks.root ck in 
445 
let branch = ref None in 
446 
let rec aux ck = 
447 
match (repr ck).cdesc with 
448 
 Ctuple cl > 
449 
List.iter aux cl 
450 
 Carrow (ck1,ck2) > 
451 
aux ck1; aux ck2 
452 
 _ > 
453 
begin 
454 
match !branch with 
455 
 None > 
456 
branch := Some (Clocks.branch ck) 
457 
 Some br > 
458 
(* cannot fail *) 
459 
branch := Some (Clocks.common_prefix br (Clocks.branch ck)) 
460 
end 
461 
in 
462 
begin 
463 
aux ck; 
464 
Clocks.clock_of_root_branch root (Utils.desome !branch) 
465 
end 
466  
467 
(* Clocks a list of arguments of Lustre builtin operators: 
468 
 type each expression, remove carriers of clocks as 
469 
carriers may only denote variables, not arbitrary expr. 
470 
 try to unify these clocks altogether 
471 
*) 
472 
let rec clock_standard_args env expr_list = 
473 
let ck_list = List.map (fun e > clock_uncarry (clock_expr env e)) expr_list in 
474 
let ck_res = new_var true in 
475 
List.iter2 (fun e ck > try_unify ck ck_res e.expr_loc) expr_list ck_list; 
476 
ck_res 
477  
478 
(* emulates a subtyping relation between clocks c and (cr : c), 
479 
used during node application only *) 
480 
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock = 
481 
let loc = real_arg.expr_loc in 
482 
let real_clock = clock_expr env real_arg in 
483 
try_sub_unify sub formal_clock real_clock loc 
484  
485 
(* computes clocks for node application *) 
486 
and clock_appl env f args clock_reset loc = 
487 
let args = expr_list_of_expr args in 
488 
if Basic_library.is_homomorphic_fun f && List.exists is_tuple_expr args 
489 
then 
490 
let args = Utils.transpose_list (List.map expr_list_of_expr args) in 
491 
Clocks.clock_of_clock_list (List.map (fun args > clock_call env f args clock_reset loc) args) 
492 
else 
493 
clock_call env f args clock_reset loc 
494  
495 
and clock_call env f args clock_reset loc = 
496 
let cfun = clock_ident false env f loc in 
497 
let cins, couts = split_arrow cfun in 
498 
let cins = clock_list_of_clock cins in 
499 
List.iter2 (clock_subtyping_arg env) args cins; 
500 
unify_imported_clock (Some clock_reset) cfun loc; 
501 
couts 
502  
503 
and clock_ident nocarrier env id loc = 
504 
clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc) 
505  
506 
and clock_carrier env c loc ce = 
507 
let expr_c = expr_of_ident c loc in 
508 
let ck = clock_expr ~nocarrier:false env expr_c in 
509 
let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in 
510 
let ckb = new_var true in 
511 
let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in 
512 
try_unify ck ckcarry expr_c.expr_loc; 
513 
unify_tuple_clock (Some ckb) ce expr_c.expr_loc; 
514 
cr 
515  
516 
(** [clock_expr env expr] performs the clock calculus for expression [expr] in 
517 
environment [env] *) 
518 
and clock_expr ?(nocarrier=true) env expr = 
519 
let resulting_ck = 
520 
match expr.expr_desc with 
521 
 Expr_const cst > 
522 
let ck = new_var true in 
523 
expr.expr_clock < ck; 
524 
ck 
525 
 Expr_ident v > 
526 
let ckv = 
527 
try 
528 
Env.lookup_value env v 
529 
with Not_found > 
530 
failwith ("Internal error, variable \""^v^"\" not found") 
531 
in 
532 
let ck = instantiate (ref []) (ref []) ckv in 
533 
expr.expr_clock < ck; 
534 
ck 
535 
 Expr_array elist > 
536 
let ck = clock_standard_args env elist in 
537 
expr.expr_clock < ck; 
538 
ck 
539 
 Expr_access (e1, d) > 
540 
(* dimension, being a static value, doesn't need to be clocked *) 
541 
let ck = clock_standard_args env [e1] in 
542 
expr.expr_clock < ck; 
543 
ck 
544 
 Expr_power (e1, d) > 
545 
(* dimension, being a static value, doesn't need to be clocked *) 
546 
let ck = clock_standard_args env [e1] in 
547 
expr.expr_clock < ck; 
548 
ck 
549 
 Expr_tuple elist > 
550 
let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in 
551 
expr.expr_clock < ck; 
552 
ck 
553 
 Expr_ite (c, t, e) > 
554 
let ck_c = clock_standard_args env [c] in 
555 
let ck = clock_standard_args env [t; e] in 
556 
(* Here, the branches may exhibit a tuple clock, not the condition *) 
557 
unify_tuple_clock (Some ck_c) ck expr.expr_loc; 
558 
expr.expr_clock < ck; 
559 
ck 
560 
 Expr_appl (id, args, r) > 
561 
(try 
562 
(* for a modular compilation scheme, all inputs/outputs must share the same clock ! 
563 
this is also the reset clock ! 
564 
*) 
565 
let cr = 
566 
match r with 
567 
 None > new_var true 
568 
 Some c > clock_standard_args env [c] in 
569 
let couts = clock_appl env id args (clock_uncarry cr) expr.expr_loc in 
570 
expr.expr_clock < couts; 
571 
couts 
572 
with exn > ( 
573 
Format.eprintf "Current expr: %a@." Printers.pp_expr expr; 
574 
raise exn 
575 
)) 
576 
 Expr_fby (e1,e2) 
577 
 Expr_arrow (e1,e2) > 
578 
let ck = clock_standard_args env [e1; e2] in 
579 
unify_tuple_clock None ck expr.expr_loc; 
580 
expr.expr_clock < ck; 
581 
ck 
582 
 Expr_pre e > (* todo : deal with phases as in tail ? *) 
583 
let ck = clock_standard_args env [e] in 
584 
expr.expr_clock < ck; 
585 
ck 
586 
 Expr_when (e,c,l) > 
587 
let ce = clock_standard_args env [e] in 
588 
let c_loc = loc_of_cond expr.expr_loc c in 
589 
let cr = clock_carrier env c c_loc ce in 
590 
let ck = clock_on ce cr l in 
591 
let cr' = new_carrier (Carry_const c) ck.cscoped in 
592 
let ck' = clock_on ce cr' l in 
593 
expr.expr_clock < ck'; 
594 
ck 
595 
 Expr_merge (c,hl) > 
596 
let cvar = new_var true in 
597 
let crvar = new_carrier Carry_name true in 
598 
List.iter (fun (t, h) > let ckh = clock_uncarry (clock_expr env h) in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl; 
599 
let cr = clock_carrier env c expr.expr_loc cvar in 
600 
try_unify_carrier cr crvar expr.expr_loc; 
601 
let cres = clock_current ((snd (List.hd hl)).expr_clock) in 
602 
expr.expr_clock < cres; 
603 
cres 
604 
in 
605 
Log.report ~level:4 (fun fmt > Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck); 
606 
resulting_ck 
607  
608 
let clock_of_vlist vars = 
609 
let ckl = List.map (fun v > v.var_clock) vars in 
610 
clock_of_clock_list ckl 
611  
612 
(** [clock_eq env eq] performs the clockcalculus for equation [eq] in 
613 
environment [env] *) 
614 
let clock_eq env eq = 
615 
let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v > expr_of_ident v eq.eq_loc) eq.eq_lhs) in 
616 
let ck_rhs = clock_expr env eq.eq_rhs in 
617 
clock_subtyping_arg env expr_lhs ck_rhs 
618  
619 
(* [clock_coreclock cck] returns the clock_expr corresponding to clock 
620 
declaration [cck] *) 
621 
let clock_coreclock env cck id loc scoped = 
622 
match cck.ck_dec_desc with 
623 
 Ckdec_any > new_var scoped 
624 
 Ckdec_bool cl > 
625 
let temp_env = Env.add_value env id (new_var true) in 
626 
(* We just want the id to be present in the environment *) 
627 
let dummy_id_expr = expr_of_ident id loc in 
628 
let when_expr = 
629 
List.fold_left 
630 
(fun expr (x,l) > 
631 
{expr_tag = new_tag (); 
632 
expr_desc = Expr_when (expr,x,l); 
633 
expr_type = Types.new_var (); 
634 
expr_clock = new_var scoped; 
635 
expr_delay = Delay.new_var (); 
636 
expr_loc = loc; 
637 
expr_annot = None}) 
638 
dummy_id_expr cl 
639 
in 
640 
clock_expr temp_env when_expr 
641  
642 
(* Clocks a variable declaration *) 
643 
let clock_var_decl scoped env vdecl = 
644 
let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in 
645 
let ck = 
646 
(* WTF ???? 
647 
if vdecl.var_dec_const 
648 
then 
649 
(try_generalize ck vdecl.var_loc; ck) 
650 
else 
651 
*) 
652 
if Types.get_clock_base_type vdecl.var_type <> None 
653 
then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped 
654 
else ck in 
655 
(if vdecl.var_dec_const 
656 
then match vdecl.var_dec_value with 
657 
 None > () 
658 
 Some v > 
659 
begin 
660 
let ck_static = clock_expr env v in 
661 
try_unify ck ck_static v.expr_loc 
662 
end); 
663 
try_unify ck vdecl.var_clock vdecl.var_loc; 
664 
Env.add_value env vdecl.var_id ck 
665  
666 
(* Clocks a variable declaration list *) 
667 
let clock_var_decl_list env scoped l = 
668 
List.fold_left (clock_var_decl scoped) env l 
669  
670 
(** [clock_node env nd] performs the clockcalculus for node [nd] in 
671 
environment [env]. 
672 
Generalization of clocks wrt scopes follows this rule: 
673 
 generalize inputs (unscoped). 
674 
 generalize outputs. As they are scoped, only clocks coming from inputs 
675 
are allowed to be generalized. 
676 
 generalize locals. As outputs don't depend on them (checked the step before), 
677 
they can be generalized. 
678 
*) 
679 
let clock_node env loc nd = 
680 
(* let is_main = nd.node_id = !Options.main_node in *) 
681 
let new_env = clock_var_decl_list env false nd.node_inputs in 
682 
let new_env = clock_var_decl_list new_env true nd.node_outputs in 
683 
let new_env = clock_var_decl_list new_env true nd.node_locals in 
684 
List.iter (clock_eq new_env) (get_node_eqs nd); 
685 
let ck_ins = clock_of_vlist nd.node_inputs in 
686 
let ck_outs = clock_of_vlist nd.node_outputs in 
687 
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in 
688 
unify_imported_clock None ck_node loc; 
689 
Log.report ~level:3 (fun fmt > print_ck fmt ck_node); 
690 
(* Local variables may contain firstorder carrier variables that should be generalized. 
691 
That's not the case for types. *) 
692 
try_generalize ck_node loc; 
693 
(* 
694 
List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs; 
695 
List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*) 
696 
(*List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*) 
697 
(* TODO : Xavier pourquoi ai je cette erreur ? *) 
698 
(* if (is_main && is_polymorphic ck_node) then 
699 
raise (Error (loc,(Cannot_be_polymorphic ck_node))); 
700 
*) 
701 
Log.report ~level:3 (fun fmt > print_ck fmt ck_node); 
702 
nd.node_clock < ck_node; 
703 
Env.add_value env nd.node_id ck_node 
704  
705  
706 
let check_imported_pclocks loc ck_node = 
707 
let pck = ref None in 
708 
let rec aux ck = 
709 
match ck.cdesc with 
710 
 Carrow (ck1,ck2) > aux ck1; aux ck2 
711 
 Ctuple cl > List.iter aux cl 
712 
 Con (ck',_,_) > aux ck' 
713 
 Clink ck' > aux ck' 
714 
 Ccarrying (_,ck') > aux ck' 
715 
 Cvar  Cunivar > 
716 
match !pck with 
717 
 None > () 
718 
 Some (_,_) > 
719 
raise (Error (loc, (Invalid_imported_clock ck_node))) 
720 
in 
721 
aux ck_node 
722  
723 
let clock_imported_node env loc nd = 
724 
let new_env = clock_var_decl_list env false nd.nodei_inputs in 
725 
ignore(clock_var_decl_list new_env false nd.nodei_outputs); 
726 
let ck_ins = clock_of_vlist nd.nodei_inputs in 
727 
let ck_outs = clock_of_vlist nd.nodei_outputs in 
728 
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in 
729 
unify_imported_clock None ck_node loc; 
730 
check_imported_pclocks loc ck_node; 
731 
try_generalize ck_node loc; 
732 
nd.nodei_clock < ck_node; 
733 
Env.add_value env nd.nodei_id ck_node 
734  
735 
let clock_top_const env cdecl= 
736 
let ck = new_var false in 
737 
try_generalize ck cdecl.const_loc; 
738 
Env.add_value env cdecl.const_id ck 
739  
740 
let clock_top_consts env clist = 
741 
List.fold_left clock_top_const env clist 
742 

743 
let rec clock_top_decl env decl = 
744 
match decl.top_decl_desc with 
745 
 Node nd > 
746 
clock_node env decl.top_decl_loc nd 
747 
 ImportedNode nd > 
748 
clock_imported_node env decl.top_decl_loc nd 
749 
 Const c > 
750 
clock_top_const env c 
751 
 TypeDef _ > List.fold_left clock_top_decl env (consts_of_enum_type decl) 
752 
 Open _ > env 
753  
754 
let clock_prog env decls = 
755 
List.fold_left clock_top_decl env decls 
756  
757 
(* Once the Lustre program is fully clocked, 
758 
we must get back to the original description of clocks, 
759 
with constant parameters, instead of unifiable internal variables. *) 
760  
761 
(* The following functions aims at 'unevaluating' carriers occuring in clock expressions, 
762 
i.e. replacing unifiable second_order variables with the original carrier names. 
763 
Once restored in this formulation, clocks may be meaningfully printed. 
764 
*) 
765 
let uneval_vdecl_generics vdecl = 
766 
(*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*) 
767 
if Types.get_clock_base_type vdecl.var_type <> None 
768 
then 
769 
match get_carrier_name vdecl.var_clock with 
770 
 None > (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false) 
771 
 Some cr > Clocks.uneval vdecl.var_id cr 
772  
773 
let uneval_node_generics vdecls = 
774 
List.iter uneval_vdecl_generics vdecls 
775  
776 
let uneval_top_generics decl = 
777 
match decl.top_decl_desc with 
778 
 Node nd > 
779 
(* A node could contain firstorder carrier variable in local vars. This is not the case for types. *) 
780 
uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs) 
781 
 ImportedNode nd > 
782 
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) 
783 
 Const _ 
784 
 Open _ 
785 
 TypeDef _ > () 
786  
787 
let uneval_prog_generics prog = 
788 
List.iter uneval_top_generics prog 
789  
790 
let check_env_compat header declared computed = 
791 
uneval_prog_generics header; 
792 
Env.iter declared (fun k decl_clock_k > 
793 
let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in 
794 
try_semi_unify decl_clock_k computed_c Location.dummy_loc 
795 
) 
796 
(* Local Variables: *) 
797 
(* compilecommand:"make C .." *) 
798 
(* End: *) 