lustrec / src / clock_calculus.ml @ 53206908
History  View  Annotate  Download (32 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 
 Pck_up (ck',_) > occurs cvar ck' 
46 
 Pck_down (ck',_) > occurs cvar ck' 
47 
 Pck_phase (ck',_) > occurs cvar ck' 
48 
 Cvar _ > ck=cvar 
49 
 Cunivar _  Pck_const (_,_) > false 
50 
 Clink ck' > occurs cvar ck' 
51 
 Ccarrying (_,ck') > occurs cvar ck' 
52  
53 
(* Clocks generalization *) 
54 
let rec generalize_carrier cr = 
55 
match cr.carrier_desc with 
56 
 Carry_const _ 
57 
 Carry_name > 
58 
if cr.carrier_scoped then 
59 
raise (Scope_carrier cr); 
60 
cr.carrier_desc < Carry_var 
61 
 Carry_var > () 
62 
 Carry_link cr' > generalize_carrier cr' 
63  
64 
(** Promote monomorphic clock variables to polymorphic clock variables. *) 
65 
(* Generalize by sideeffects *) 
66 
let rec generalize ck = 
67 
match ck.cdesc with 
68 
 Carrow (ck1,ck2) > 
69 
generalize ck1; generalize ck2 
70 
 Ctuple clist > 
71 
List.iter generalize clist 
72 
 Con (ck',cr,_) > generalize ck'; generalize_carrier cr 
73 
 Cvar cset > 
74 
if ck.cscoped then 
75 
raise (Scope_clock ck); 
76 
ck.cdesc < Cunivar cset 
77 
 Pck_up (ck',_) > generalize ck' 
78 
 Pck_down (ck',_) > generalize ck' 
79 
 Pck_phase (ck',_) > generalize ck' 
80 
 Pck_const (_,_)  Cunivar _ > () 
81 
 Clink ck' > 
82 
generalize ck' 
83 
 Ccarrying (cr,ck') > 
84 
generalize_carrier cr; generalize ck' 
85  
86 
let try_generalize ck_node loc = 
87 
try 
88 
generalize ck_node 
89 
with (Scope_carrier cr) > 
90 
raise (Error (loc, Carrier_extrusion (ck_node, cr))) 
91 
 (Scope_clock ck) > 
92 
raise (Error (loc, Clock_extrusion (ck_node, ck))) 
93  
94 
(* Clocks instanciation *) 
95 
let instantiate_carrier cr inst_cr_vars = 
96 
let cr = carrier_repr cr in 
97 
match cr.carrier_desc with 
98 
 Carry_const _ 
99 
 Carry_name > cr 
100 
 Carry_link _ > 
101 
failwith "Internal error" 
102 
 Carry_var > 
103 
try 
104 
List.assoc cr.carrier_id !inst_cr_vars 
105 
with Not_found > 
106 
let cr_var = new_carrier Carry_name true in 
107 
inst_cr_vars := (cr.carrier_id,cr_var)::!inst_cr_vars; 
108 
cr_var 
109  
110 
(** Downgrade polymorphic clock variables to monomorphic clock variables *) 
111 
(* inst_ck_vars ensures that a polymorphic variable is instanciated with 
112 
the same monomorphic variable if it occurs several times in the same 
113 
type. inst_cr_vars is the same for carriers. *) 
114 
let rec instantiate inst_ck_vars inst_cr_vars ck = 
115 
match ck.cdesc with 
116 
 Carrow (ck1,ck2) > 
117 
{ck with cdesc = 
118 
Carrow ((instantiate inst_ck_vars inst_cr_vars ck1), 
119 
(instantiate inst_ck_vars inst_cr_vars ck2))} 
120 
 Ctuple cklist > 
121 
{ck with cdesc = Ctuple 
122 
(List.map (instantiate inst_ck_vars inst_cr_vars) cklist)} 
123 
 Con (ck',c,l) > 
124 
let c' = instantiate_carrier c inst_cr_vars in 
125 
{ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)} 
126 
 Cvar _  Pck_const (_,_) > ck 
127 
 Pck_up (ck',k) > 
128 
{ck with cdesc = Pck_up ((instantiate inst_ck_vars inst_cr_vars ck'),k)} 
129 
 Pck_down (ck',k) > 
130 
{ck with cdesc = Pck_down ((instantiate inst_ck_vars inst_cr_vars ck'),k)} 
131 
 Pck_phase (ck',q) > 
132 
{ck with cdesc = Pck_phase ((instantiate inst_ck_vars inst_cr_vars ck'),q)} 
133 
 Clink ck' > 
134 
{ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')} 
135 
 Ccarrying (cr,ck') > 
136 
let cr' = instantiate_carrier cr inst_cr_vars in 
137 
{ck with cdesc = 
138 
Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')} 
139 
 Cunivar cset > 
140 
try 
141 
List.assoc ck.cid !inst_ck_vars 
142 
with Not_found > 
143 
let var = new_ck (Cvar cset) true in 
144 
inst_ck_vars := (ck.cid, var)::!inst_ck_vars; 
145 
var 
146  
147 
(** [subsume pck1 cset1] subsumes clock [pck1] by clock subset 
148 
[cset1]. The clock constraint is actually recursively transfered to 
149 
the clock variable appearing in [pck1] *) 
150 
let subsume pck1 cset1 = 
151 
let rec aux pck cset = 
152 
match cset with 
153 
 CSet_all > 
154 
() 
155 
 CSet_pck (k,(a,b)) > 
156 
match pck.cdesc with 
157 
 Cvar cset' > 
158 
pck.cdesc < Cvar (intersect cset' cset) 
159 
 Pck_up (pck',k') > 
160 
let rat = if a=0 then (0,1) else (a,b*k') in 
161 
aux pck' (CSet_pck ((k*k'),rat)) 
162 
 Pck_down (pck',k') > 
163 
let k''=k/(gcd k k') in 
164 
aux pck' (CSet_pck (k'',(a*k',b))) 
165 
 Pck_phase (pck',(a',b')) > 
166 
let (a'',b'')= max_rat (sum_rat (a,b) (a',b')) (0,1) in 
167 
aux pck' (CSet_pck (k, (a'',b''))) 
168 
 Pck_const (n,(a',b')) > 
169 
if n mod k <> 0  (max_rat (a,b) (a',b')) <> (a',b') then 
170 
raise (Subsume (pck1, cset1)) 
171 
 Clink pck' > 
172 
aux pck' cset 
173 
 Cunivar _ > () 
174 
 Ccarrying (_,ck') > 
175 
aux ck' cset 
176 
 _ > raise (Subsume (pck1, cset1)) 
177 
in 
178 
aux pck1 cset1 
179  
180 
let rec update_scope_carrier scoped cr = 
181 
if (not scoped) then 
182 
begin 
183 
cr.carrier_scoped < scoped; 
184 
match cr.carrier_desc with 
185 
 Carry_const _  Carry_name  Carry_var > () 
186 
 Carry_link cr' > update_scope_carrier scoped cr' 
187 
end 
188  
189 
let rec update_scope scoped ck = 
190 
if (not scoped) then 
191 
begin 
192 
ck.cscoped < scoped; 
193 
match ck.cdesc with 
194 
 Carrow (ck1,ck2) > 
195 
update_scope scoped ck1; update_scope scoped ck2 
196 
 Ctuple clist > 
197 
List.iter (update_scope scoped) clist 
198 
 Con (ck',cr,_) > update_scope scoped ck'(*; update_scope_carrier scoped cr*) 
199 
 Cvar cset > 
200 
ck.cdesc < Cvar cset 
201 
 Pck_up (ck',_) > update_scope scoped ck' 
202 
 Pck_down (ck',_) > update_scope scoped ck' 
203 
 Pck_phase (ck',_) > update_scope scoped ck' 
204 
 Pck_const (_,_)  Cunivar _ > () 
205 
 Clink ck' > 
206 
update_scope scoped ck' 
207 
 Ccarrying (cr,ck') > 
208 
update_scope_carrier scoped cr; update_scope scoped ck' 
209 
end 
210  
211 
(* Unifies two static pclocks. *) 
212 
let unify_static_pck ck1 ck2 = 
213 
if (period ck1 <> period ck2)  (phase ck1 <> phase ck2) then 
214 
raise (Unify (ck1,ck2)) 
215  
216 
(* Unifies two clock carriers *) 
217 
let unify_carrier cr1 cr2 = 
218 
let cr1 = carrier_repr cr1 in 
219 
let cr2 = carrier_repr cr2 in 
220 
if cr1==cr2 then () 
221 
else 
222 
match cr1.carrier_desc, cr2.carrier_desc with 
223 
 Carry_const id1, Carry_const id2 > 
224 
if id1 <> id2 then raise (Mismatch (cr1, cr2)) 
225 
 Carry_const _, Carry_name > 
226 
begin 
227 
cr2.carrier_desc < Carry_link cr1; 
228 
update_scope_carrier cr2.carrier_scoped cr1 
229 
end 
230 
 Carry_name, Carry_const _ > 
231 
begin 
232 
cr1.carrier_desc < Carry_link cr2; 
233 
update_scope_carrier cr1.carrier_scoped cr2 
234 
end 
235 
 Carry_name, Carry_name > 
236 
if cr1.carrier_id < cr2.carrier_id then 
237 
begin 
238 
cr2.carrier_desc < Carry_link cr1; 
239 
update_scope_carrier cr2.carrier_scoped cr1 
240 
end 
241 
else 
242 
begin 
243 
cr1.carrier_desc < Carry_link cr2; 
244 
update_scope_carrier cr1.carrier_scoped cr2 
245 
end 
246 
 _,_ > assert false 
247  
248 
(* Semiunifies two clock carriers *) 
249 
let semi_unify_carrier cr1 cr2 = 
250 
let cr1 = carrier_repr cr1 in 
251 
let cr2 = carrier_repr cr2 in 
252 
if cr1==cr2 then () 
253 
else 
254 
match cr1.carrier_desc, cr2.carrier_desc with 
255 
 Carry_const id1, Carry_const id2 > 
256 
if id1 <> id2 then raise (Mismatch (cr1, cr2)) 
257 
 Carry_const _, Carry_name > 
258 
begin 
259 
cr2.carrier_desc < Carry_link cr1; 
260 
update_scope_carrier cr2.carrier_scoped cr1 
261 
end 
262 
 Carry_name, Carry_const _ > raise (Mismatch (cr1, cr2)) 
263 
 Carry_name, Carry_name > 
264 
if cr1.carrier_id < cr2.carrier_id then 
265 
begin 
266 
cr2.carrier_desc < Carry_link cr1; 
267 
update_scope_carrier cr2.carrier_scoped cr1 
268 
end 
269 
else 
270 
begin 
271 
cr1.carrier_desc < Carry_link cr2; 
272 
update_scope_carrier cr1.carrier_scoped cr2 
273 
end 
274 
 _,_ > assert false 
275  
276 
let try_unify_carrier ck1 ck2 loc = 
277 
try 
278 
unify_carrier ck1 ck2 
279 
with 
280 
 Unify (ck1',ck2') > 
281 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
282 
 Subsume (ck,cset) > 
283 
raise (Error (loc, Clock_set_mismatch (ck,cset))) 
284 
 Mismatch (cr1,cr2) > 
285 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
286  
287 
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify 
288 
(ck1,ck2)] if the clocks are not unifiable.*) 
289 
let rec unify ck1 ck2 = 
290 
let ck1 = repr ck1 in 
291 
let ck2 = repr ck2 in 
292 
if ck1==ck2 then 
293 
() 
294 
else 
295 
let left_const = is_concrete_pck ck1 in 
296 
let right_const = is_concrete_pck ck2 in 
297 
if left_const && right_const then 
298 
unify_static_pck ck1 ck2 
299 
else 
300 
match ck1.cdesc,ck2.cdesc with 
301 
 Cvar cset1,Cvar cset2> 
302 
if ck1.cid < ck2.cid then 
303 
begin 
304 
ck2.cdesc < Clink (simplify ck1); 
305 
update_scope ck2.cscoped ck1; 
306 
subsume ck1 cset2 
307 
end 
308 
else 
309 
begin 
310 
ck1.cdesc < Clink (simplify ck2); 
311 
update_scope ck1.cscoped ck2; 
312 
subsume ck2 cset1 
313 
end 
314 
 Cvar cset, Pck_up (_,_)  Cvar cset, Pck_down (_,_) 
315 
 Cvar cset, Pck_phase (_,_)  Cvar cset, Pck_const (_,_) > 
316 
if (occurs ck1 ck2) then 
317 
begin 
318 
if (simplify ck2 = ck1) then 
319 
ck2.cdesc < Clink (simplify ck1) 
320 
else 
321 
raise (Unify (ck1,ck2)); 
322 
end 
323 
else 
324 
begin 
325 
ck1.cdesc < Clink (simplify ck2); 
326 
subsume ck2 cset 
327 
end 
328 
 Pck_up (_,_), Cvar cset  Pck_down (_,_), Cvar cset 
329 
 Pck_phase (_,_), Cvar cset  Pck_const (_,_), Cvar cset > 
330 
if (occurs ck2 ck1) then 
331 
begin 
332 
if ((simplify ck1) = ck2) then 
333 
ck1.cdesc < Clink (simplify ck2) 
334 
else 
335 
raise (Unify (ck1,ck2)); 
336 
end 
337 
else 
338 
begin 
339 
ck2.cdesc < Clink (simplify ck1); 
340 
subsume ck1 cset 
341 
end 
342 
 (Cvar cset,_) when (not (occurs ck1 ck2)) > 
343 
subsume ck2 cset; 
344 
update_scope ck1.cscoped ck2; 
345 
ck1.cdesc < Clink (simplify ck2) 
346 
 (_, (Cvar cset)) when (not (occurs ck2 ck1)) > 
347 
subsume ck1 cset; 
348 
update_scope ck2.cscoped ck1; 
349 
ck2.cdesc < Clink (simplify ck1) 
350 
 Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') > 
351 
unify_carrier cr1 cr2; 
352 
unify ck1' ck2' 
353 
 Ccarrying (_,_),_  _,Ccarrying (_,_) > 
354 
raise (Unify (ck1,ck2)) 
355 
 Carrow (c1,c2), Carrow (c1',c2') > 
356 
unify c1 c1'; unify c2 c2' 
357 
 Ctuple ckl1, Ctuple ckl2 > 
358 
if (List.length ckl1) <> (List.length ckl2) then 
359 
raise (Unify (ck1,ck2)); 
360 
List.iter2 unify ckl1 ckl2 
361 
 Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 > 
362 
unify_carrier c1 c2; 
363 
unify ck' ck'' 
364 
 Pck_const (i,r), Pck_const (i',r') > 
365 
if i<>i'  r <> r' then 
366 
raise (Unify (ck1,ck2)) 
367 
 (_, Pck_up (pck2',k)) when (not right_const) > 
368 
let ck1' = simplify (new_ck (Pck_down (ck1,k)) true) in 
369 
unify ck1' pck2' 
370 
 (_,Pck_down (pck2',k)) when (not right_const) > 
371 
subsume ck1 (CSet_pck (k,(0,1))); 
372 
let ck1' = simplify (new_ck (Pck_up (ck1,k)) true) in 
373 
unify ck1' pck2' 
374 
 (_,Pck_phase (pck2',(a,b))) when (not right_const) > 
375 
subsume ck1 (CSet_pck (b,(a,b))); 
376 
let ck1' = simplify (new_ck (Pck_phase (ck1,(a,b))) true) in 
377 
unify ck1' pck2' 
378 
 Pck_up (pck1',k),_ > 
379 
let ck2' = simplify (new_ck (Pck_down (ck2,k)) true) in 
380 
unify pck1' ck2' 
381 
 Pck_down (pck1',k),_ > 
382 
subsume ck2 (CSet_pck (k,(0,1))); 
383 
let ck2' = simplify (new_ck (Pck_up (ck2,k)) true) in 
384 
unify pck1' ck2' 
385 
 Pck_phase (pck1',(a,b)),_ > 
386 
subsume ck2 (CSet_pck (b,(a,b))); 
387 
let ck2' = simplify (new_ck (Pck_phase (ck2,(a,b))) true) in 
388 
unify pck1' ck2' 
389 
 Cunivar _, _  _, Cunivar _ > () 
390 
 _,_ > raise (Unify (ck1,ck2)) 
391  
392 
(** [unify ck1 ck2] semiunifies clocks [ck1] and [ck2]. Raises [Unify 
393 
(ck1,ck2)] if the clocks are not semiunifiable.*) 
394 
let rec semi_unify ck1 ck2 = 
395 
let ck1 = repr ck1 in 
396 
let ck2 = repr ck2 in 
397 
if ck1==ck2 then 
398 
() 
399 
else 
400 
match ck1.cdesc,ck2.cdesc with 
401 
 Cvar cset1,Cvar cset2> 
402 
if ck1.cid < ck2.cid then 
403 
begin 
404 
ck2.cdesc < Clink (simplify ck1); 
405 
update_scope ck2.cscoped ck1 
406 
end 
407 
else 
408 
begin 
409 
ck1.cdesc < Clink (simplify ck2); 
410 
update_scope ck1.cscoped ck2 
411 
end 
412 
 (Cvar cset,_) > raise (Unify (ck1,ck2)) 
413 
 (_, (Cvar cset)) when (not (occurs ck2 ck1)) > 
414 
update_scope ck2.cscoped ck1; 
415 
ck2.cdesc < Clink (simplify ck1) 
416 
 Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') > 
417 
semi_unify_carrier cr1 cr2; 
418 
semi_unify ck1' ck2' 
419 
 Ccarrying (_,_),_  _,Ccarrying (_,_) > 
420 
raise (Unify (ck1,ck2)) 
421 
 Carrow (c1,c2), Carrow (c1',c2') > 
422 
begin 
423 
semi_unify c1 c1'; 
424 
semi_unify c2 c2' 
425 
end 
426 
 Ctuple ckl1, Ctuple ckl2 > 
427 
if (List.length ckl1) <> (List.length ckl2) then 
428 
raise (Unify (ck1,ck2)); 
429 
List.iter2 semi_unify ckl1 ckl2 
430 
 Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 > 
431 
semi_unify_carrier c1 c2; 
432 
semi_unify ck' ck'' 
433 
 Cunivar _, _  _, Cunivar _ > () 
434 
 _,_ > raise (Unify (ck1,ck2)) 
435  
436 
(* Returns the value corresponding to a pclock (integer) factor 
437 
expression. Expects a constant expression (checked by typing). *) 
438 
let int_factor_of_expr e = 
439 
match e.expr_desc with 
440 
 Expr_const 
441 
(Const_int i) > i 
442 
 _ > failwith "Internal error: int_factor_of_expr" 
443  
444 
(** [clock_uncarry ck] drops the possible carrier(s) name(s) from clock [ck] *) 
445 
let rec clock_uncarry ck = 
446 
let ck = repr ck in 
447 
match ck.cdesc with 
448 
 Ccarrying (_, ck') > ck' 
449 
 Con(ck', cr, l) > clock_on (clock_uncarry ck') cr l 
450 
 Ctuple ckl > clock_of_clock_list (List.map clock_uncarry ckl) 
451 
 _ > ck 
452  
453 
let try_unify ck1 ck2 loc = 
454 
try 
455 
unify ck1 ck2 
456 
with 
457 
 Unify (ck1',ck2') > 
458 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
459 
 Subsume (ck,cset) > 
460 
raise (Error (loc, Clock_set_mismatch (ck,cset))) 
461 
 Mismatch (cr1,cr2) > 
462 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
463  
464 
let try_semi_unify ck1 ck2 loc = 
465 
try 
466 
semi_unify ck1 ck2 
467 
with 
468 
 Unify (ck1',ck2') > 
469 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
470 
 Subsume (ck,cset) > 
471 
raise (Error (loc, Clock_set_mismatch (ck,cset))) 
472 
 Mismatch (cr1,cr2) > 
473 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
474  
475 
(* ck2 is a subtype of ck1 *) 
476 
let rec sub_unify sub ck1 ck2 = 
477 
match (repr ck1).cdesc, (repr ck2).cdesc with 
478 
 Ctuple cl1 , Ctuple cl2 > 
479 
if List.length cl1 <> List.length cl2 
480 
then raise (Unify (ck1, ck2)) 
481 
else List.iter2 (sub_unify sub) cl1 cl2 
482 
 Ctuple [c1] , _ > sub_unify sub c1 ck2 
483 
 _ , Ctuple [c2] > sub_unify sub ck1 c2 
484 
 Con (c1, cr1, t1) , Con (c2, cr2, t2) when t1=t2 > 
485 
begin 
486 
unify_carrier cr1 cr2; 
487 
sub_unify sub c1 c2 
488 
end 
489 
 Ccarrying (cr1, c1), Ccarrying (cr2, c2)> 
490 
begin 
491 
unify_carrier cr1 cr2; 
492 
sub_unify sub c1 c2 
493 
end 
494 
 _, Ccarrying (_, c2) when sub > sub_unify sub ck1 c2 
495 
 _ > unify ck1 ck2 
496  
497 
let try_sub_unify sub ck1 ck2 loc = 
498 
try 
499 
sub_unify sub ck1 ck2 
500 
with 
501 
 Unify (ck1',ck2') > 
502 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
503 
 Subsume (ck,cset) > 
504 
raise (Error (loc, Clock_set_mismatch (ck,cset))) 
505 
 Mismatch (cr1,cr2) > 
506 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
507  
508 
(* Unifies all the clock variables in the clock type of a tuple 
509 
expression, so that the clock type only uses at most one clock variable *) 
510 
let unify_tuple_clock ref_ck_opt ck loc = 
511 
(*(match ref_ck_opt with 
512 
 None > Format.eprintf "unify_tuple_clock None %a@." Clocks.print_ck ck 
513 
 Some ck' > Format.eprintf "unify_tuple_clock (Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*) 
514 
let ck_var = ref ref_ck_opt in 
515 
let rec aux ck = 
516 
match (repr ck).cdesc with 
517 
 Con _ 
518 
 Cvar _ > 
519 
begin 
520 
match !ck_var with 
521 
 None > 
522 
ck_var:=Some ck 
523 
 Some v > 
524 
(* may fail *) 
525 
try_unify ck v loc 
526 
end 
527 
 Ctuple cl > 
528 
List.iter aux cl 
529 
 Carrow _ > assert false (* should not occur *) 
530 
 Ccarrying (_, ck1) > 
531 
aux ck1 
532 
 _ > () 
533 
in aux ck 
534  
535 
(* Unifies all the clock variables in the clock type of an imported 
536 
node, so that the clock type only uses at most one base clock variable, 
537 
that is, the activation clock of the node *) 
538 
let unify_imported_clock ref_ck_opt ck loc = 
539 
let ck_var = ref ref_ck_opt in 
540 
let rec aux ck = 
541 
match (repr ck).cdesc with 
542 
 Cvar _ > 
543 
begin 
544 
match !ck_var with 
545 
 None > 
546 
ck_var:=Some ck 
547 
 Some v > 
548 
(* cannot fail *) 
549 
try_unify ck v loc 
550 
end 
551 
 Ctuple cl > 
552 
List.iter aux cl 
553 
 Carrow (ck1,ck2) > 
554 
aux ck1; aux ck2 
555 
 Ccarrying (_, ck1) > 
556 
aux ck1 
557 
 Con (ck1, _, _) > aux ck1 
558 
 _ > () 
559 
in 
560 
aux ck 
561  
562 
(* Computes the root clock of a tuple or a node clock, 
563 
which is not the same as the base clock. 
564 
Root clock will be used as the call clock 
565 
of a given node instance *) 
566 
let compute_root_clock ck = 
567 
let root = Clocks.root ck in 
568 
let branch = ref None in 
569 
let rec aux ck = 
570 
match (repr ck).cdesc with 
571 
 Ctuple cl > 
572 
List.iter aux cl 
573 
 Carrow (ck1,ck2) > 
574 
aux ck1; aux ck2 
575 
 _ > 
576 
begin 
577 
match !branch with 
578 
 None > 
579 
branch := Some (Clocks.branch ck) 
580 
 Some br > 
581 
(* cannot fail *) 
582 
branch := Some (Clocks.common_prefix br (Clocks.branch ck)) 
583 
end 
584 
in 
585 
begin 
586 
aux ck; 
587 
Clocks.clock_of_root_branch root (Utils.desome !branch) 
588 
end 
589  
590 
(* Clocks a list of arguments of Lustre builtin operators: 
591 
 type each expression, remove carriers of clocks as 
592 
carriers may only denote variables, not arbitrary expr. 
593 
 try to unify these clocks altogether 
594 
*) 
595 
let rec clock_standard_args env expr_list = 
596 
let ck_list = List.map (fun e > clock_uncarry (clock_expr env e)) expr_list in 
597 
let ck_res = new_var true in 
598 
List.iter2 (fun e ck > try_unify ck ck_res e.expr_loc) expr_list ck_list; 
599 
ck_res 
600  
601 
(* emulates a subtyping relation between clocks c and (cr : c), 
602 
used during node application only *) 
603 
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock = 
604 
let loc = real_arg.expr_loc in 
605 
let real_clock = clock_expr env real_arg in 
606 
try_sub_unify sub formal_clock real_clock loc 
607  
608 
(* computes clocks for node application *) 
609 
and clock_appl env f args clock_reset loc = 
610 
let args = expr_list_of_expr args in 
611 
if Basic_library.is_homomorphic_fun f && List.exists is_tuple_expr args 
612 
then 
613 
let args = Utils.transpose_list (List.map expr_list_of_expr args) in 
614 
Clocks.clock_of_clock_list (List.map (fun args > clock_call env f args clock_reset loc) args) 
615 
else 
616 
clock_call env f args clock_reset loc 
617  
618 
and clock_call env f args clock_reset loc = 
619 
let cfun = clock_ident false env f loc in 
620 
let cins, couts = split_arrow cfun in 
621 
let cins = clock_list_of_clock cins in 
622 
List.iter2 (clock_subtyping_arg env) args cins; 
623 
unify_imported_clock (Some clock_reset) cfun loc; 
624 
couts 
625  
626 
and clock_ident nocarrier env id loc = 
627 
clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc) 
628  
629 
and clock_carrier env c loc ce = 
630 
let expr_c = expr_of_ident c loc in 
631 
let ck = clock_expr ~nocarrier:false env expr_c in 
632 
let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in 
633 
let ckb = new_var true in 
634 
let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in 
635 
try_unify ck ckcarry expr_c.expr_loc; 
636 
unify_tuple_clock (Some ckb) ce expr_c.expr_loc; 
637 
cr 
638  
639 
(** [clock_expr env expr] performs the clock calculus for expression [expr] in 
640 
environment [env] *) 
641 
and clock_expr ?(nocarrier=true) env expr = 
642 
let resulting_ck = 
643 
match expr.expr_desc with 
644 
 Expr_const cst > 
645 
let ck = new_var true in 
646 
expr.expr_clock < ck; 
647 
ck 
648 
 Expr_ident v > 
649 
let ckv = 
650 
try 
651 
Env.lookup_value env v 
652 
with Not_found > 
653 
failwith ("Internal error, variable \""^v^"\" not found") 
654 
in 
655 
let ck = instantiate (ref []) (ref []) ckv in 
656 
expr.expr_clock < ck; 
657 
ck 
658 
 Expr_array elist > 
659 
let ck = clock_standard_args env elist in 
660 
expr.expr_clock < ck; 
661 
ck 
662 
 Expr_access (e1, d) > 
663 
(* dimension, being a static value, doesn't need to be clocked *) 
664 
let ck = clock_standard_args env [e1] in 
665 
expr.expr_clock < ck; 
666 
ck 
667 
 Expr_power (e1, d) > 
668 
(* dimension, being a static value, doesn't need to be clocked *) 
669 
let ck = clock_standard_args env [e1] in 
670 
expr.expr_clock < ck; 
671 
ck 
672 
 Expr_tuple elist > 
673 
let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in 
674 
expr.expr_clock < ck; 
675 
ck 
676 
 Expr_ite (c, t, e) > 
677 
let ck_c = clock_standard_args env [c] in 
678 
let ck = clock_standard_args env [t; e] in 
679 
(* Here, the branches may exhibit a tuple clock, not the condition *) 
680 
unify_tuple_clock (Some ck_c) ck expr.expr_loc; 
681 
expr.expr_clock < ck; 
682 
ck 
683 
 Expr_appl (id, args, r) > 
684 
(try 
685 
(* for a modular compilation scheme, all inputs/outputs must share the same clock ! 
686 
this is also the reset clock ! 
687 
*) 
688 
let cr = 
689 
match r with 
690 
 None > new_var true 
691 
 Some c > clock_standard_args env [c] in 
692 
let couts = clock_appl env id args (clock_uncarry cr) expr.expr_loc in 
693 
expr.expr_clock < couts; 
694 
couts 
695 
with exn > ( 
696 
Format.eprintf "Current expr: %a@." Printers.pp_expr expr; 
697 
raise exn 
698 
)) 
699 
 Expr_fby (e1,e2) 
700 
 Expr_arrow (e1,e2) > 
701 
let ck = clock_standard_args env [e1; e2] in 
702 
unify_tuple_clock None ck expr.expr_loc; 
703 
expr.expr_clock < ck; 
704 
ck 
705 
 Expr_pre e > (* todo : deal with phases as in tail ? *) 
706 
let ck = clock_standard_args env [e] in 
707 
expr.expr_clock < ck; 
708 
ck 
709 
 Expr_when (e,c,l) > 
710 
let ce = clock_standard_args env [e] in 
711 
let c_loc = loc_of_cond expr.expr_loc c in 
712 
let cr = clock_carrier env c c_loc ce in 
713 
let ck = clock_on ce cr l in 
714 
let cr' = new_carrier (Carry_const c) ck.cscoped in 
715 
let ck' = clock_on ce cr' l in 
716 
expr.expr_clock < ck'; 
717 
ck 
718 
 Expr_merge (c,hl) > 
719 
let cvar = new_var true in 
720 
let crvar = new_carrier Carry_name true in 
721 
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; 
722 
let cr = clock_carrier env c expr.expr_loc cvar in 
723 
try_unify_carrier cr crvar expr.expr_loc; 
724 
let cres = clock_current ((snd (List.hd hl)).expr_clock) in 
725 
expr.expr_clock < cres; 
726 
cres 
727 
in 
728 
Log.report ~level:4 (fun fmt > Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck); 
729 
resulting_ck 
730  
731 
let clock_of_vlist vars = 
732 
let ckl = List.map (fun v > v.var_clock) vars in 
733 
clock_of_clock_list ckl 
734  
735 
(** [clock_eq env eq] performs the clockcalculus for equation [eq] in 
736 
environment [env] *) 
737 
let clock_eq env eq = 
738 
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 
739 
let ck_rhs = clock_expr env eq.eq_rhs in 
740 
clock_subtyping_arg env expr_lhs ck_rhs 
741  
742 
(* [clock_coreclock cck] returns the clock_expr corresponding to clock 
743 
declaration [cck] *) 
744 
let clock_coreclock env cck id loc scoped = 
745 
match cck.ck_dec_desc with 
746 
 Ckdec_any > new_var scoped 
747 
 Ckdec_pclock (n,(a,b)) > 
748 
let ck = new_ck (Pck_const (n,(a,b))) scoped in 
749 
if n mod b <> 0 then raise (Error (loc,Invalid_const ck)); 
750 
ck 
751 
 Ckdec_bool cl > 
752 
let temp_env = Env.add_value env id (new_var true) in 
753 
(* We just want the id to be present in the environment *) 
754 
let dummy_id_expr = expr_of_ident id loc in 
755 
let when_expr = 
756 
List.fold_left 
757 
(fun expr (x,l) > 
758 
{expr_tag = new_tag (); 
759 
expr_desc = Expr_when (expr,x,l); 
760 
expr_type = Types.new_var (); 
761 
expr_clock = new_var scoped; 
762 
expr_delay = Delay.new_var (); 
763 
expr_loc = loc; 
764 
expr_annot = None}) 
765 
dummy_id_expr cl 
766 
in 
767 
clock_expr temp_env when_expr 
768  
769 
(* Clocks a variable declaration *) 
770 
let clock_var_decl scoped env vdecl = 
771 
let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in 
772 
let ck = 
773 
(* WTF ???? 
774 
if vdecl.var_dec_const 
775 
then 
776 
(try_generalize ck vdecl.var_loc; ck) 
777 
else 
778 
*) 
779 
if Types.get_clock_base_type vdecl.var_type <> None 
780 
then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped 
781 
else ck in 
782 
(if vdecl.var_dec_const 
783 
then match vdecl.var_dec_value with 
784 
 None > () 
785 
 Some v > 
786 
begin 
787 
let ck_static = clock_expr env v in 
788 
try_unify ck ck_static v.expr_loc 
789 
end); 
790 
try_unify ck vdecl.var_clock vdecl.var_loc; 
791 
Env.add_value env vdecl.var_id ck 
792  
793 
(* Clocks a variable declaration list *) 
794 
let clock_var_decl_list env scoped l = 
795 
List.fold_left (clock_var_decl scoped) env l 
796  
797 
(** [clock_node env nd] performs the clockcalculus for node [nd] in 
798 
environment [env]. 
799 
Generalization of clocks wrt scopes follows this rule: 
800 
 generalize inputs (unscoped). 
801 
 generalize outputs. As they are scoped, only clocks coming from inputs 
802 
are allowed to be generalized. 
803 
 generalize locals. As outputs don't depend on them (checked the step before), 
804 
they can be generalized. 
805 
*) 
806 
let clock_node env loc nd = 
807 
(* let is_main = nd.node_id = !Options.main_node in *) 
808 
let new_env = clock_var_decl_list env false nd.node_inputs in 
809 
let new_env = clock_var_decl_list new_env true nd.node_outputs in 
810 
let new_env = clock_var_decl_list new_env true nd.node_locals in 
811 
List.iter (clock_eq new_env) (get_node_eqs nd); 
812 
let ck_ins = clock_of_vlist nd.node_inputs in 
813 
let ck_outs = clock_of_vlist nd.node_outputs in 
814 
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in 
815 
unify_imported_clock None ck_node loc; 
816 
Log.report ~level:3 (fun fmt > print_ck fmt ck_node); 
817 
(* Local variables may contain firstorder carrier variables that should be generalized. 
818 
That's not the case for types. *) 
819 
try_generalize ck_node loc; 
820 
(* 
821 
List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs; 
822 
List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*) 
823 
(*List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*) 
824 
(* TODO : Xavier pourquoi ai je cette erreur ? *) 
825 
(* if (is_main && is_polymorphic ck_node) then 
826 
raise (Error (loc,(Cannot_be_polymorphic ck_node))); 
827 
*) 
828 
Log.report ~level:3 (fun fmt > print_ck fmt ck_node); 
829 
nd.node_clock < ck_node; 
830 
Env.add_value env nd.node_id ck_node 
831  
832  
833 
let check_imported_pclocks loc ck_node = 
834 
let pck = ref None in 
835 
let rec aux ck = 
836 
match ck.cdesc with 
837 
 Carrow (ck1,ck2) > aux ck1; aux ck2 
838 
 Ctuple cl > List.iter aux cl 
839 
 Con (ck',_,_) > aux ck' 
840 
 Pck_up (_,_)  Pck_down (_,_)  Pck_phase (_,_) > 
841 
raise (Error (loc, (Invalid_imported_clock ck_node))) 
842 
 Pck_const (n,p) > 
843 
begin 
844 
match !pck with 
845 
 None > pck := Some (n,p) 
846 
 Some (n',p') > 
847 
if (n,p) <> (n',p') then 
848 
raise (Error (loc, (Invalid_imported_clock ck_node))) 
849 
end 
850 
 Clink ck' > aux ck' 
851 
 Ccarrying (_,ck') > aux ck' 
852 
 Cvar _  Cunivar _ > 
853 
match !pck with 
854 
 None > () 
855 
 Some (_,_) > 
856 
raise (Error (loc, (Invalid_imported_clock ck_node))) 
857 
in 
858 
aux ck_node 
859  
860 
let clock_imported_node env loc nd = 
861 
let new_env = clock_var_decl_list env false nd.nodei_inputs in 
862 
ignore(clock_var_decl_list new_env false nd.nodei_outputs); 
863 
let ck_ins = clock_of_vlist nd.nodei_inputs in 
864 
let ck_outs = clock_of_vlist nd.nodei_outputs in 
865 
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in 
866 
unify_imported_clock None ck_node loc; 
867 
check_imported_pclocks loc ck_node; 
868 
try_generalize ck_node loc; 
869 
nd.nodei_clock < ck_node; 
870 
Env.add_value env nd.nodei_id ck_node 
871  
872 
let clock_top_const env cdecl= 
873 
let ck = new_var false in 
874 
try_generalize ck cdecl.const_loc; 
875 
Env.add_value env cdecl.const_id ck 
876  
877 
let clock_top_consts env clist = 
878 
List.fold_left clock_top_const env clist 
879 

880 
let rec clock_top_decl env decl = 
881 
match decl.top_decl_desc with 
882 
 Node nd > 
883 
clock_node env decl.top_decl_loc nd 
884 
 ImportedNode nd > 
885 
clock_imported_node env decl.top_decl_loc nd 
886 
 Const c > 
887 
clock_top_const env c 
888 
 TypeDef _ > List.fold_left clock_top_decl env (consts_of_enum_type decl) 
889 
 Open _ > env 
890  
891 
let clock_prog env decls = 
892 
List.fold_left clock_top_decl env decls 
893  
894 
(* Once the Lustre program is fully clocked, 
895 
we must get back to the original description of clocks, 
896 
with constant parameters, instead of unifiable internal variables. *) 
897  
898 
(* The following functions aims at 'unevaluating' carriers occuring in clock expressions, 
899 
i.e. replacing unifiable second_order variables with the original carrier names. 
900 
Once restored in this formulation, clocks may be meaningfully printed. 
901 
*) 
902 
let uneval_vdecl_generics vdecl = 
903 
(*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*) 
904 
if Types.get_clock_base_type vdecl.var_type <> None 
905 
then 
906 
match get_carrier_name vdecl.var_clock with 
907 
 None > (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false) 
908 
 Some cr > Clocks.uneval vdecl.var_id cr 
909  
910 
let uneval_node_generics vdecls = 
911 
List.iter uneval_vdecl_generics vdecls 
912  
913 
let uneval_top_generics decl = 
914 
match decl.top_decl_desc with 
915 
 Node nd > 
916 
(* A node could contain firstorder carrier variable in local vars. This is not the case for types. *) 
917 
uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs) 
918 
 ImportedNode nd > 
919 
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) 
920 
 Const _ 
921 
 Open _ 
922 
 TypeDef _ > () 
923  
924 
let uneval_prog_generics prog = 
925 
List.iter uneval_top_generics prog 
926  
927 
let check_env_compat header declared computed = 
928 
uneval_prog_generics header; 
929 
Env.iter declared (fun k decl_clock_k > 
930 
let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in 
931 
try_semi_unify decl_clock_k computed_c Location.dummy_loc 
932 
) 
933 
(* Local Variables: *) 
934 
(* compilecommand:"make C .." *) 
935 
(* End: *) 