Revision 3b2bd83d
Added by Teme Kahsai about 8 years ago
src/clock_calculus.ml | ||
---|---|---|
42 | 42 |
| Ctuple ckl -> |
43 | 43 |
List.exists (occurs cvar) ckl |
44 | 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 |
|
45 |
| Cvar -> ck=cvar |
|
46 |
| Cunivar -> false |
|
50 | 47 |
| Clink ck' -> occurs cvar ck' |
51 | 48 |
| Ccarrying (_,ck') -> occurs cvar ck' |
52 | 49 |
|
... | ... | |
70 | 67 |
| Ctuple clist -> |
71 | 68 |
List.iter generalize clist |
72 | 69 |
| Con (ck',cr,_) -> generalize ck'; generalize_carrier cr |
73 |
| Cvar cset ->
|
|
70 |
| Cvar -> |
|
74 | 71 |
if ck.cscoped then |
75 | 72 |
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 _ -> () |
|
73 |
ck.cdesc <- Cunivar |
|
74 |
| Cunivar -> () |
|
81 | 75 |
| Clink ck' -> |
82 | 76 |
generalize ck' |
83 | 77 |
| Ccarrying (cr,ck') -> |
... | ... | |
123 | 117 |
| Con (ck',c,l) -> |
124 | 118 |
let c' = instantiate_carrier c inst_cr_vars in |
125 | 119 |
{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)} |
|
120 |
| Cvar -> ck |
|
133 | 121 |
| Clink ck' -> |
134 | 122 |
{ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')} |
135 | 123 |
| Ccarrying (cr,ck') -> |
136 | 124 |
let cr' = instantiate_carrier cr inst_cr_vars in |
137 | 125 |
{ck with cdesc = |
138 | 126 |
Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')} |
139 |
| Cunivar cset ->
|
|
127 |
| Cunivar -> |
|
140 | 128 |
try |
141 | 129 |
List.assoc ck.cid !inst_ck_vars |
142 | 130 |
with Not_found -> |
143 |
let var = new_ck (Cvar cset) true in
|
|
131 |
let var = new_ck Cvar true in
|
|
144 | 132 |
inst_ck_vars := (ck.cid, var)::!inst_ck_vars; |
145 | 133 |
var |
146 | 134 |
|
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 | 135 |
|
180 | 136 |
let rec update_scope_carrier scoped cr = |
181 | 137 |
if (not scoped) then |
... | ... | |
196 | 152 |
| Ctuple clist -> |
197 | 153 |
List.iter (update_scope scoped) clist |
198 | 154 |
| 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 _ -> () |
|
155 |
| Cvar | Cunivar -> () |
|
205 | 156 |
| Clink ck' -> |
206 | 157 |
update_scope scoped ck' |
207 | 158 |
| Ccarrying (cr,ck') -> |
208 | 159 |
update_scope_carrier scoped cr; update_scope scoped ck' |
209 | 160 |
end |
210 | 161 |
|
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 | 162 |
|
216 | 163 |
(* Unifies two clock carriers *) |
217 | 164 |
let unify_carrier cr1 cr2 = |
... | ... | |
279 | 226 |
with |
280 | 227 |
| Unify (ck1',ck2') -> |
281 | 228 |
raise (Error (loc, Clock_clash (ck1',ck2'))) |
282 |
| Subsume (ck,cset) -> |
|
283 |
raise (Error (loc, Clock_set_mismatch (ck,cset))) |
|
284 | 229 |
| Mismatch (cr1,cr2) -> |
285 | 230 |
raise (Error (loc, Carrier_mismatch (cr1,cr2))) |
286 | 231 |
|
... | ... | |
292 | 237 |
if ck1==ck2 then |
293 | 238 |
() |
294 | 239 |
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)) |
|
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)) |
|
391 | 274 |
|
392 | 275 |
(** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify |
393 | 276 |
(ck1,ck2)] if the clocks are not semi-unifiable.*) |
... | ... | |
398 | 281 |
() |
399 | 282 |
else |
400 | 283 |
match ck1.cdesc,ck2.cdesc with |
401 |
| Cvar cset1,Cvar cset2->
|
|
284 |
| Cvar, Cvar ->
|
|
402 | 285 |
if ck1.cid < ck2.cid then |
403 | 286 |
begin |
404 | 287 |
ck2.cdesc <- Clink (simplify ck1); |
... | ... | |
409 | 292 |
ck1.cdesc <- Clink (simplify ck2); |
410 | 293 |
update_scope ck1.cscoped ck2 |
411 | 294 |
end |
412 |
| (Cvar cset,_) -> raise (Unify (ck1,ck2))
|
|
413 |
| (_, (Cvar cset)) when (not (occurs ck2 ck1)) ->
|
|
295 |
| (Cvar, _) -> raise (Unify (ck1,ck2))
|
|
296 |
| (_, Cvar) when (not (occurs ck2 ck1)) ->
|
|
414 | 297 |
update_scope ck2.cscoped ck1; |
415 | 298 |
ck2.cdesc <- Clink (simplify ck1) |
416 | 299 |
| Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') -> |
... | ... | |
430 | 313 |
| Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 -> |
431 | 314 |
semi_unify_carrier c1 c2; |
432 | 315 |
semi_unify ck' ck'' |
433 |
| Cunivar _, _ | _, Cunivar _ -> ()
|
|
316 |
| Cunivar, _ | _, Cunivar -> ()
|
|
434 | 317 |
| _,_ -> raise (Unify (ck1,ck2)) |
435 | 318 |
|
436 | 319 |
(* Returns the value corresponding to a pclock (integer) factor |
... | ... | |
456 | 339 |
with |
457 | 340 |
| Unify (ck1',ck2') -> |
458 | 341 |
raise (Error (loc, Clock_clash (ck1',ck2'))) |
459 |
| Subsume (ck,cset) -> |
|
460 |
raise (Error (loc, Clock_set_mismatch (ck,cset))) |
|
461 | 342 |
| Mismatch (cr1,cr2) -> |
462 | 343 |
raise (Error (loc, Carrier_mismatch (cr1,cr2))) |
463 | 344 |
|
... | ... | |
467 | 348 |
with |
468 | 349 |
| Unify (ck1',ck2') -> |
469 | 350 |
raise (Error (loc, Clock_clash (ck1',ck2'))) |
470 |
| Subsume (ck,cset) -> |
|
471 |
raise (Error (loc, Clock_set_mismatch (ck,cset))) |
|
472 | 351 |
| Mismatch (cr1,cr2) -> |
473 | 352 |
raise (Error (loc, Carrier_mismatch (cr1,cr2))) |
474 | 353 |
|
... | ... | |
500 | 379 |
with |
501 | 380 |
| Unify (ck1',ck2') -> |
502 | 381 |
raise (Error (loc, Clock_clash (ck1',ck2'))) |
503 |
| Subsume (ck,cset) -> |
|
504 |
raise (Error (loc, Clock_set_mismatch (ck,cset))) |
|
505 | 382 |
| Mismatch (cr1,cr2) -> |
506 | 383 |
raise (Error (loc, Carrier_mismatch (cr1,cr2))) |
507 | 384 |
|
... | ... | |
515 | 392 |
let rec aux ck = |
516 | 393 |
match (repr ck).cdesc with |
517 | 394 |
| Con _ |
518 |
| Cvar _ ->
|
|
395 |
| Cvar -> |
|
519 | 396 |
begin |
520 | 397 |
match !ck_var with |
521 | 398 |
| None -> |
... | ... | |
539 | 416 |
let ck_var = ref ref_ck_opt in |
540 | 417 |
let rec aux ck = |
541 | 418 |
match (repr ck).cdesc with |
542 |
| Cvar _ ->
|
|
419 |
| Cvar -> |
|
543 | 420 |
begin |
544 | 421 |
match !ck_var with |
545 | 422 |
| None -> |
... | ... | |
608 | 485 |
(* computes clocks for node application *) |
609 | 486 |
and clock_appl env f args clock_reset loc = |
610 | 487 |
let args = expr_list_of_expr args in |
611 |
if Basic_library.is_internal_fun f && List.exists is_tuple_expr args
|
|
488 |
if Basic_library.is_homomorphic_fun f && List.exists is_tuple_expr args
|
|
612 | 489 |
then |
613 | 490 |
let args = Utils.transpose_list (List.map expr_list_of_expr args) in |
614 | 491 |
Clocks.clock_of_clock_list (List.map (fun args -> clock_call env f args clock_reset loc) args) |
... | ... | |
744 | 621 |
let clock_coreclock env cck id loc scoped = |
745 | 622 |
match cck.ck_dec_desc with |
746 | 623 |
| 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 | 624 |
| Ckdec_bool cl -> |
752 | 625 |
let temp_env = Env.add_value env id (new_var true) in |
753 | 626 |
(* We just want the id to be present in the environment *) |
... | ... | |
837 | 710 |
| Carrow (ck1,ck2) -> aux ck1; aux ck2 |
838 | 711 |
| Ctuple cl -> List.iter aux cl |
839 | 712 |
| 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 | 713 |
| Clink ck' -> aux ck' |
851 | 714 |
| Ccarrying (_,ck') -> aux ck' |
852 |
| Cvar _ | Cunivar _ ->
|
|
715 |
| Cvar | Cunivar ->
|
|
853 | 716 |
match !pck with |
854 | 717 |
| None -> () |
855 | 718 |
| Some (_,_) -> |
Also available in: Unified diff
updating to onera version 30f766a:2016-12-04