lustrec / src / clock_calculus.ml @ b08ffca7
History  View  Annotate  Download (30.9 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 name from clock [ck] *) 
445 
let clock_uncarry ck = 
446 
let ck = repr ck in 
447 
match ck.cdesc with 
448 
 Ccarrying (_, ck') > ck' 
449 
 _ > ck 
450  
451 
let try_unify ck1 ck2 loc = 
452 
try 
453 
unify ck1 ck2 
454 
with 
455 
 Unify (ck1',ck2') > 
456 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
457 
 Subsume (ck,cset) > 
458 
raise (Error (loc, Clock_set_mismatch (ck,cset))) 
459 
 Mismatch (cr1,cr2) > 
460 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
461  
462 
let try_semi_unify ck1 ck2 loc = 
463 
try 
464 
semi_unify ck1 ck2 
465 
with 
466 
 Unify (ck1',ck2') > 
467 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
468 
 Subsume (ck,cset) > 
469 
raise (Error (loc, Clock_set_mismatch (ck,cset))) 
470 
 Mismatch (cr1,cr2) > 
471 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
472  
473 
(* ck2 is a subtype of ck1 *) 
474 
let rec sub_unify sub ck1 ck2 = 
475 
match (repr ck1).cdesc, (repr ck2).cdesc with 
476 
 Ctuple cl1 , Ctuple cl2 > 
477 
if List.length cl1 <> List.length cl2 
478 
then raise (Unify (ck1, ck2)) 
479 
else List.iter2 (sub_unify sub) cl1 cl2 
480 
 Ctuple [c1] , _ > sub_unify sub c1 ck2 
481 
 _ , Ctuple [c2] > sub_unify sub ck1 c2 
482 
 Con (c1, cr1, t1) , Con (c2, cr2, t2) when t1=t2 > 
483 
begin 
484 
unify_carrier cr1 cr2; 
485 
sub_unify sub c1 c2 
486 
end 
487 
 Ccarrying (cr1, c1), Ccarrying (cr2, c2)> 
488 
begin 
489 
unify_carrier cr1 cr2; 
490 
sub_unify sub c1 c2 
491 
end 
492 
 _, Ccarrying (_, c2) when sub > sub_unify sub ck1 c2 
493 
 _ > unify ck1 ck2 
494  
495 
let try_sub_unify sub ck1 ck2 loc = 
496 
try 
497 
sub_unify sub ck1 ck2 
498 
with 
499 
 Unify (ck1',ck2') > 
500 
raise (Error (loc, Clock_clash (ck1',ck2'))) 
501 
 Subsume (ck,cset) > 
502 
raise (Error (loc, Clock_set_mismatch (ck,cset))) 
503 
 Mismatch (cr1,cr2) > 
504 
raise (Error (loc, Carrier_mismatch (cr1,cr2))) 
505  
506 
(* Unifies all the clock variables in the clock type of a tuple 
507 
expression, so that the clock type only uses at most one clock variable *) 
508 
let unify_tuple_clock ref_ck_opt ck loc = 
509 
(*(match ref_ck_opt with 
510 
 None > Format.eprintf "unify_tuple_clock None %a@." Clocks.print_ck ck 
511 
 Some ck' > Format.eprintf "unify_tuple_clock (Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*) 
512 
let ck_var = ref ref_ck_opt in 
513 
let rec aux ck = 
514 
match (repr ck).cdesc with 
515 
 Con _ 
516 
 Cvar _ > 
517 
begin 
518 
match !ck_var with 
519 
 None > 
520 
ck_var:=Some ck 
521 
 Some v > 
522 
(* may fail *) 
523 
try_unify ck v loc 
524 
end 
525 
 Ctuple cl > 
526 
List.iter aux cl 
527 
 Carrow _ > assert false (* should not occur *) 
528 
 Ccarrying (_, ck1) > 
529 
aux ck1 
530 
 _ > () 
531 
in aux ck 
532  
533 
(* Unifies all the clock variables in the clock type of an imported 
534 
node, so that the clock type only uses at most one base clock variable, 
535 
that is, the activation clock of the node *) 
536 
let unify_imported_clock ref_ck_opt ck loc = 
537 
let ck_var = ref ref_ck_opt in 
538 
let rec aux ck = 
539 
match (repr ck).cdesc with 
540 
 Cvar _ > 
541 
begin 
542 
match !ck_var with 
543 
 None > 
544 
ck_var:=Some ck 
545 
 Some v > 
546 
(* cannot fail *) 
547 
try_unify ck v loc 
548 
end 
549 
 Ctuple cl > 
550 
List.iter aux cl 
551 
 Carrow (ck1,ck2) > 
552 
aux ck1; aux ck2 
553 
 Ccarrying (_, ck1) > 
554 
aux ck1 
555 
 Con (ck1, _, _) > aux ck1 
556 
 _ > () 
557 
in 
558 
aux ck 
559  
560 
(* Clocks a list of arguments of Lustre builtin operators: 
561 
 type each expression, remove carriers of clocks as 
562 
carriers may only denote variables, not arbitrary expr. 
563 
 try to unify these clocks altogether 
564 
*) 
565 
let rec clock_standard_args env expr_list = 
566 
let ck_list = List.map (fun e > clock_uncarry (clock_expr env e)) expr_list in 
567 
let ck_res = new_var true in 
568 
List.iter2 (fun e ck > try_unify ck ck_res e.expr_loc) expr_list ck_list; 
569 
ck_res 
570  
571 
(* emulates a subtyping relation between clocks c and (cr : c), 
572 
used during node application only *) 
573 
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock = 
574 
let loc = real_arg.expr_loc in 
575 
let real_clock = clock_expr env real_arg in 
576 
try_sub_unify sub formal_clock real_clock loc 
577  
578 
(* computes clocks for node application *) 
579 
and clock_appl env f args clock_reset loc = 
580 
let args = expr_list_of_expr args in 
581 
if Basic_library.is_internal_fun f && List.exists is_tuple_expr args 
582 
then 
583 
let args = Utils.transpose_list (List.map expr_list_of_expr args) in 
584 
Clocks.clock_of_clock_list (List.map (fun args > clock_call env f args clock_reset loc) args) 
585 
else 
586 
clock_call env f args clock_reset loc 
587  
588 
and clock_call env f args clock_reset loc = 
589 
let cfun = clock_ident false env f loc in 
590 
let cins, couts = split_arrow cfun in 
591 
let cins = clock_list_of_clock cins in 
592 
List.iter2 (clock_subtyping_arg env) args cins; 
593 
unify_imported_clock (Some clock_reset) cfun loc; 
594 
couts 
595  
596 
and clock_ident nocarrier env id loc = 
597 
clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc) 
598  
599 
and clock_carrier env c loc ce = 
600 
let expr_c = expr_of_ident c loc in 
601 
let ck = clock_expr ~nocarrier:false env expr_c in 
602 
let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in 
603 
let ckb = new_var true in 
604 
let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in 
605 
try_unify ck ckcarry expr_c.expr_loc; 
606 
unify_tuple_clock (Some ckb) ce expr_c.expr_loc; 
607 
cr 
608  
609 
(** [clock_expr env expr] performs the clock calculus for expression [expr] in 
610 
environment [env] *) 
611 
and clock_expr ?(nocarrier=true) env expr = 
612 
let resulting_ck = 
613 
match expr.expr_desc with 
614 
 Expr_const cst > 
615 
let ck = new_var true in 
616 
expr.expr_clock < ck; 
617 
ck 
618 
 Expr_ident v > 
619 
let ckv = 
620 
try 
621 
Env.lookup_value env v 
622 
with Not_found > 
623 
failwith ("Internal error, variable \""^v^"\" not found") 
624 
in 
625 
let ck = instantiate (ref []) (ref []) ckv in 
626 
expr.expr_clock < ck; 
627 
ck 
628 
 Expr_array elist > 
629 
let ck = clock_standard_args env elist in 
630 
expr.expr_clock < ck; 
631 
ck 
632 
 Expr_access (e1, d) > 
633 
(* dimension, being a static value, doesn't need to be clocked *) 
634 
let ck = clock_standard_args env [e1] in 
635 
expr.expr_clock < ck; 
636 
ck 
637 
 Expr_power (e1, d) > 
638 
(* dimension, being a static value, doesn't need to be clocked *) 
639 
let ck = clock_standard_args env [e1] in 
640 
expr.expr_clock < ck; 
641 
ck 
642 
 Expr_tuple elist > 
643 
let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in 
644 
expr.expr_clock < ck; 
645 
ck 
646 
 Expr_ite (c, t, e) > 
647 
let ck_c = clock_standard_args env [c] in 
648 
let ck = clock_standard_args env [t; e] in 
649 
(* Here, the branches may exhibit a tuple clock, not the condition *) 
650 
unify_tuple_clock (Some ck_c) ck expr.expr_loc; 
651 
expr.expr_clock < ck; 
652 
ck 
653 
 Expr_appl (id, args, r) > 
654 
(try 
655 
(* for a modular compilation scheme, all inputs/outputs must share the same clock ! 
656 
this is also the reset clock ! 
657 
*) 
658 
let cr = 
659 
match r with 
660 
 None > new_var true 
661 
 Some (x, _) > let loc_r = loc_of_cond expr.expr_loc x in 
662 
let expr_r = expr_of_ident x loc_r in 
663 
clock_expr env expr_r in 
664 
let couts = clock_appl env id args cr expr.expr_loc in 
665 
expr.expr_clock < couts; 
666 
couts 
667 
with exn > ( 
668 
Format.eprintf "Current expr: %a@." Printers.pp_expr expr; 
669 
raise exn 
670 
)) 
671 
 Expr_fby (e1,e2) 
672 
 Expr_arrow (e1,e2) > 
673 
let ck = clock_standard_args env [e1; e2] in 
674 
unify_tuple_clock None ck expr.expr_loc; 
675 
expr.expr_clock < ck; 
676 
ck 
677 
 Expr_pre e > (* todo : deal with phases as in tail ? *) 
678 
let ck = clock_standard_args env [e] in 
679 
expr.expr_clock < ck; 
680 
ck 
681 
 Expr_when (e,c,l) > 
682 
let ce = clock_standard_args env [e] in 
683 
let c_loc = loc_of_cond expr.expr_loc c in 
684 
let cr = clock_carrier env c c_loc ce in 
685 
let ck = clock_on ce cr l in 
686 
let cr' = new_carrier (Carry_const c) ck.cscoped in 
687 
let ck' = clock_on ce cr' l in 
688 
expr.expr_clock < ck'; 
689 
ck 
690 
 Expr_merge (c,hl) > 
691 
let cvar = new_var true in 
692 
let crvar = new_carrier Carry_name true in 
693 
List.iter (fun (t, h) > let ckh = clock_expr env h in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl; 
694 
let cr = clock_carrier env c expr.expr_loc cvar in 
695 
try_unify_carrier cr crvar expr.expr_loc; 
696 
expr.expr_clock < cvar; 
697 
cvar 
698 
in 
699 
Log.report ~level:4 (fun fmt > Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck); 
700 
resulting_ck 
701  
702 
let clock_of_vlist vars = 
703 
let ckl = List.map (fun v > v.var_clock) vars in 
704 
clock_of_clock_list ckl 
705  
706 
(** [clock_eq env eq] performs the clockcalculus for equation [eq] in 
707 
environment [env] *) 
708 
let clock_eq env eq = 
709 
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 
710 
let ck_rhs = clock_expr env eq.eq_rhs in 
711 
clock_subtyping_arg env expr_lhs ck_rhs 
712  
713 
(* [clock_coreclock cck] returns the clock_expr corresponding to clock 
714 
declaration [cck] *) 
715 
let clock_coreclock env cck id loc scoped = 
716 
match cck.ck_dec_desc with 
717 
 Ckdec_any > new_var scoped 
718 
 Ckdec_pclock (n,(a,b)) > 
719 
let ck = new_ck (Pck_const (n,(a,b))) scoped in 
720 
if n mod b <> 0 then raise (Error (loc,Invalid_const ck)); 
721 
ck 
722 
 Ckdec_bool cl > 
723 
let temp_env = Env.add_value env id (new_var true) in 
724 
(* We just want the id to be present in the environment *) 
725 
let dummy_id_expr = expr_of_ident id loc in 
726 
let when_expr = 
727 
List.fold_left 
728 
(fun expr (x,l) > 
729 
{expr_tag = new_tag (); 
730 
expr_desc = Expr_when (expr,x,l); 
731 
expr_type = Types.new_var (); 
732 
expr_clock = new_var scoped; 
733 
expr_delay = Delay.new_var (); 
734 
expr_loc = loc; 
735 
expr_annot = None}) 
736 
dummy_id_expr cl 
737 
in 
738 
clock_expr temp_env when_expr 
739  
740 
(* Clocks a variable declaration *) 
741 
let clock_var_decl scoped env vdecl = 
742 
let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in 
743 
let ck = 
744 
(* WTF ???? 
745 
if vdecl.var_dec_const 
746 
then 
747 
(try_generalize ck vdecl.var_loc; ck) 
748 
else 
749 
*) 
750 
if Types.get_clock_base_type vdecl.var_type <> None 
751 
then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped 
752 
else ck in 
753 
vdecl.var_clock < ck; 
754 
Env.add_value env vdecl.var_id ck 
755  
756 
(* Clocks a variable declaration list *) 
757 
let clock_var_decl_list env scoped l = 
758 
List.fold_left (clock_var_decl scoped) env l 
759  
760 
(** [clock_node env nd] performs the clockcalculus for node [nd] in 
761 
environment [env]. 
762 
Generalization of clocks wrt scopes follows this rule: 
763 
 generalize inputs (unscoped). 
764 
 generalize outputs. As they are scoped, only clocks coming from inputs 
765 
are allowed to be generalized. 
766 
 generalize locals. As outputs don't depend on them (checked the step before), 
767 
they can be generalized. 
768 
*) 
769 
let clock_node env loc nd = 
770 
(* let is_main = nd.node_id = !Options.main_node in *) 
771 
let new_env = clock_var_decl_list env false nd.node_inputs in 
772 
let new_env = clock_var_decl_list new_env true nd.node_outputs in 
773 
let new_env = clock_var_decl_list new_env true nd.node_locals in 
774 
List.iter (clock_eq new_env) (get_node_eqs nd); 
775 
let ck_ins = clock_of_vlist nd.node_inputs in 
776 
let ck_outs = clock_of_vlist nd.node_outputs in 
777 
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in 
778 
unify_imported_clock None ck_node loc; 
779 
Log.report ~level:3 (fun fmt > print_ck fmt ck_node); 
780 
(* Local variables may contain firstorder carrier variables that should be generalized. 
781 
That's not the case for types. *) 
782 
try_generalize ck_node loc; 
783 
(* 
784 
List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs; 
785 
List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*) 
786 
(*List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*) 
787 
(* TODO : Xavier pourquoi ai je cette erreur ? *) 
788 
(* if (is_main && is_polymorphic ck_node) then 
789 
raise (Error (loc,(Cannot_be_polymorphic ck_node))); 
790 
*) 
791 
Log.report ~level:3 (fun fmt > print_ck fmt ck_node); 
792 
nd.node_clock < ck_node; 
793 
Env.add_value env nd.node_id ck_node 
794  
795  
796 
let check_imported_pclocks loc ck_node = 
797 
let pck = ref None in 
798 
let rec aux ck = 
799 
match ck.cdesc with 
800 
 Carrow (ck1,ck2) > aux ck1; aux ck2 
801 
 Ctuple cl > List.iter aux cl 
802 
 Con (ck',_,_) > aux ck' 
803 
 Pck_up (_,_)  Pck_down (_,_)  Pck_phase (_,_) > 
804 
raise (Error (loc, (Invalid_imported_clock ck_node))) 
805 
 Pck_const (n,p) > 
806 
begin 
807 
match !pck with 
808 
 None > pck := Some (n,p) 
809 
 Some (n',p') > 
810 
if (n,p) <> (n',p') then 
811 
raise (Error (loc, (Invalid_imported_clock ck_node))) 
812 
end 
813 
 Clink ck' > aux ck' 
814 
 Ccarrying (_,ck') > aux ck' 
815 
 Cvar _  Cunivar _ > 
816 
match !pck with 
817 
 None > () 
818 
 Some (_,_) > 
819 
raise (Error (loc, (Invalid_imported_clock ck_node))) 
820 
in 
821 
aux ck_node 
822  
823 
let clock_imported_node env loc nd = 
824 
let new_env = clock_var_decl_list env false nd.nodei_inputs in 
825 
ignore(clock_var_decl_list new_env false nd.nodei_outputs); 
826 
let ck_ins = clock_of_vlist nd.nodei_inputs in 
827 
let ck_outs = clock_of_vlist nd.nodei_outputs in 
828 
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in 
829 
unify_imported_clock None ck_node loc; 
830 
check_imported_pclocks loc ck_node; 
831 
try_generalize ck_node loc; 
832 
nd.nodei_clock < ck_node; 
833 
Env.add_value env nd.nodei_id ck_node 
834  
835 
let clock_top_const env cdecl= 
836 
let ck = new_var false in 
837 
try_generalize ck cdecl.const_loc; 
838 
Env.add_value env cdecl.const_id ck 
839  
840 
let clock_top_consts env clist = 
841 
List.fold_left clock_top_const env clist 
842 

843 
let rec clock_top_decl env decl = 
844 
match decl.top_decl_desc with 
845 
 Node nd > 
846 
clock_node env decl.top_decl_loc nd 
847 
 ImportedNode nd > 
848 
clock_imported_node env decl.top_decl_loc nd 
849 
 Const c > 
850 
clock_top_const env c 
851 
 TypeDef _ > List.fold_left clock_top_decl env (consts_of_enum_type decl) 
852 
 Open _ > env 
853  
854 
let clock_prog env decls = 
855 
List.fold_left clock_top_decl env decls 
856  
857 
(* Once the Lustre program is fully clocked, 
858 
we must get back to the original description of clocks, 
859 
with constant parameters, instead of unifiable internal variables. *) 
860  
861 
(* The following functions aims at 'unevaluating' carriers occuring in clock expressions, 
862 
i.e. replacing unifiable second_order variables with the original carrier names. 
863 
Once restored in this formulation, clocks may be meaningfully printed. 
864 
*) 
865 
let uneval_vdecl_generics vdecl = 
866 
(*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*) 
867 
if Types.get_clock_base_type vdecl.var_type <> None 
868 
then 
869 
match get_carrier_name vdecl.var_clock with 
870 
 None > (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false) 
871 
 Some cr > Clocks.uneval vdecl.var_id cr 
872  
873 
let uneval_node_generics vdecls = 
874 
List.iter uneval_vdecl_generics vdecls 
875  
876 
let uneval_top_generics decl = 
877 
match decl.top_decl_desc with 
878 
 Node nd > 
879 
(* A node could contain firstorder carrier variable in local vars. This is not the case for types. *) 
880 
uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs) 
881 
 ImportedNode nd > 
882 
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) 
883 
 Const _ 
884 
 Open _ 
885 
 TypeDef _ > () 
886  
887 
let uneval_prog_generics prog = 
888 
List.iter uneval_top_generics prog 
889  
890 
let check_env_compat header declared computed = 
891 
uneval_prog_generics header; 
892 
Env.iter declared (fun k decl_clock_k > 
893 
let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in 
894 
try_semi_unify decl_clock_k computed_c Location.dummy_loc 
895 
) 
896 
(* Local Variables: *) 
897 
(* compilecommand:"make C .." *) 
898 
(* End: *) 