Revision 45f0f48d src/clocks.ml
src/clocks.ml  

15  15 
open Utils 
16  16 
open Format 
17  17  
18 
(* Clock type sets, for subtyping. *)


19 
type clock_set =


20 
CSet_all


21 
 CSet_pck of int*rat


18 
(* (\* Clock type sets, for subtyping. *\) *)


19 
(* type clock_set = *)


20 
(* CSet_all *)


21 
(*  CSet_pck of int*rat *)


22  22  
23  23 
(* Clock carriers basically correspond to the "c" in "x when c" *) 
24  24 
type carrier_desc = 
...  ...  
44  44 
 Carrow of clock_expr * clock_expr 
45  45 
 Ctuple of clock_expr list 
46  46 
 Con of clock_expr * carrier_expr * ident 
47 
 Pck_up of clock_expr * int


48 
 Pck_down of clock_expr * int


49 
 Pck_phase of clock_expr * rat


50 
 Pck_const of int * rat


51 
 Cvar of clock_set (* Monomorphic clock variable *)


52 
 Cunivar of clock_set (* Polymorphic clock variable *)


47 
(*  Pck_up of clock_expr * int *)


48 
(*  Pck_down of clock_expr * int *)


49 
(*  Pck_phase of clock_expr * rat *)


50 
(*  Pck_const of int * rat *)


51 
 Cvar (* of clock_set *) (* Monomorphic clock variable *)


52 
 Cunivar (* of clock_set *) (* Polymorphic clock variable *)


53  53 
 Clink of clock_expr (* During unification, make links instead of substitutions *) 
54  54 
 Ccarrying of carrier_expr * clock_expr 
55  55  
56  56 
type error = 
57  57 
 Clock_clash of clock_expr * clock_expr 
58 
 Not_pck


59 
 Clock_set_mismatch of clock_expr * clock_set


58 
(*  Not_pck *)


59 
(*  Clock_set_mismatch of clock_expr * clock_set *)


60  60 
 Cannot_be_polymorphic of clock_expr 
61  61 
 Invalid_imported_clock of clock_expr 
62  62 
 Invalid_const of clock_expr 
...  ...  
66  66 
 Clock_extrusion of clock_expr * clock_expr 
67  67  
68  68 
exception Unify of clock_expr * clock_expr 
69 
exception Subsume of clock_expr * clock_set 

70  69 
exception Mismatch of carrier_expr * carrier_expr 
71  70 
exception Scope_carrier of carrier_expr 
72  71 
exception Scope_clock of clock_expr 
73  72 
exception Error of Location.t * error 
74  73  
75 
let print_ckset fmt s = 

76 
match s with 

77 
 CSet_all > () 

78 
 CSet_pck (k,q) > 

79 
let (a,b) = simplify_rat q in 

80 
if k = 1 && a = 0 then 

81 
fprintf fmt "<:P" 

82 
else 

83 
fprintf fmt "<:P_(%i,%a)" k print_rat (a,b) 

84  
85  74 
let rec print_carrier fmt cr = 
86  75 
(* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt > *) 
87  76 
match cr.carrier_desc with 
...  ...  
104  93 
(fprintf_list ~sep:" * " print_ck_long) cklist 
105  94 
 Con (ck,c,l) > 
106  95 
fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c 
107 
 Pck_up (ck,k) > 

108 
fprintf fmt "%a*^%i" print_ck_long ck k 

109 
 Pck_down (ck,k) > 

110 
fprintf fmt "%a/^%i" print_ck_long ck k 

111 
 Pck_phase (ck,q) > 

112 
fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q) 

113 
 Pck_const (n,p) > 

114 
fprintf fmt "(%i,%a)" n print_rat (simplify_rat p) 

115 
 Cvar cset > 

116 
fprintf fmt "'_%i%a" ck.cid print_ckset cset 

117 
 Cunivar cset > 

118 
fprintf fmt "'%i%a" ck.cid print_ckset cset 

96 
 Cvar > fprintf fmt "'_%i" ck.cid 

97 
 Cunivar > fprintf fmt "'%i" ck.cid 

119  98 
 Clink ck' > 
120  99 
fprintf fmt "link %a" print_ck_long ck' 
121  100 
 Ccarrying (cr,ck') > 
...  ...  
129  108 
let new_ck desc scoped = 
130  109 
incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped} 
131  110  
132 
let new_var scoped = 

133 
new_ck (Cvar CSet_all) scoped 

111 
let new_var scoped = new_ck Cvar scoped 

134  112  
135 
let new_univar () = 

136 
new_ck (Cunivar CSet_all) false 

113 
let new_univar () = new_ck Cunivar false 

137  114  
138  115 
let new_carrier_id = ref (1) 
139  116  
...  ...  
187  164  
188  165 
(* Removes all links in a clock. Only used for clocks 
189  166 
simplification though. *) 
190 
let rec deep_repr ck =


167 
let rec simplify ck =


191  168 
match ck.cdesc with 
192  169 
 Carrow (ck1,ck2) > 
193 
new_ck (Carrow (deep_repr ck1, deep_repr ck2)) ck.cscoped


170 
new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped


194  171 
 Ctuple cl > 
195 
new_ck (Ctuple (List.map deep_repr cl)) ck.cscoped


172 
new_ck (Ctuple (List.map simplify cl)) ck.cscoped


196  173 
 Con (ck', c, l) > 
197 
new_ck (Con (deep_repr ck', c, l)) ck.cscoped 

198 
 Pck_up (ck',k) > 

199 
new_ck (Pck_up (deep_repr ck',k)) ck.cscoped 

200 
 Pck_down (ck',k) > 

201 
new_ck (Pck_down (deep_repr ck',k)) ck.cscoped 

202 
 Pck_phase (ck',q) > 

203 
new_ck (Pck_phase (deep_repr ck',q)) ck.cscoped 

204 
 Pck_const (_,_)  Cvar _  Cunivar _ > ck 

205 
 Clink ck' > deep_repr ck' 

206 
 Ccarrying (cr,ck') > new_ck (Ccarrying (cr, deep_repr ck')) ck.cscoped 

174 
new_ck (Con (simplify ck', c, l)) ck.cscoped 

175 
 Cvar  Cunivar > ck 

176 
 Clink ck' > simplify ck' 

177 
 Ccarrying (cr,ck') > new_ck (Ccarrying (cr, simplify ck')) ck.cscoped 

207  178  
208  179 
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock 
209  180 
(ensured by language syntax) *) 
...  ...  
233  204 
let clock_of_impnode_clock ck = 
234  205 
let ck = repr ck in 
235  206 
match ck.cdesc with 
236 
 Carrow _  Clink _  Cvar _  Cunivar _ >


207 
 Carrow _  Clink _  Cvar  Cunivar >


237  208 
failwith "internal error clock_of_impnode_clock" 
238  209 
 Ctuple cklist > List.hd cklist 
239 
 Con (_,_,_)  Pck_up (_,_)  Pck_down (_,_)  Pck_phase (_,_) 

240 
 Pck_const (_,_)  Ccarrying (_,_) > ck 

241  
242 
(** [intersect set1 set2] returns the intersection of clock subsets 

243 
[set1] and [set2]. *) 

244 
let intersect set1 set2 = 

245 
match set1,set2 with 

246 
 CSet_all,_ > set2 

247 
 _,CSet_all > set1 

248 
 CSet_pck (k,q), CSet_pck (k',q') > 

249 
let k'',q'' = lcm k k',max_rat q q' in 

250 
CSet_pck (k'',q'') 

251  
252 
(** [can_be_pck ck] returns true if [ck] "may be" a pclock (the uncertainty is 

253 
due to clock variables) *) 

254 
let rec can_be_pck ck = 

255 
match (repr ck).cdesc with 

256 
 Pck_up (_,_)  Pck_down (_,_)  Pck_phase (_,_)  Pck_const (_,_) 

257 
 Cvar _  Cunivar _ > 

258 
true 

259 
 Ccarrying (_,ck') > can_be_pck ck 

260 
 _ > false 

261  
262 
(** [is_concrete_pck ck] returns true if [ck] is a concrete [pck] (pck 

263 
transformations applied to a pck constant) *) 

264 
let rec is_concrete_pck ck = 

265 
match ck.cdesc with 

266 
 Carrow (_,_)  Ctuple _  Con (_,_,_) 

267 
 Cvar _  Cunivar _ > false 

268 
 Pck_up (ck',_)  Pck_down (ck',_) > is_concrete_pck ck' 

269 
 Pck_phase (ck',_) > is_concrete_pck ck' 

270 
 Pck_const (_,_) > true 

271 
 Clink ck' > is_concrete_pck ck' 

272 
 Ccarrying (_,ck') > false 

210 
 Con (_,_,_) 

211 
 Ccarrying (_,_) > ck 

212  
273  213  
274  214 
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *) 
275  215 
let rec is_polymorphic ck = 
276  216 
match ck.cdesc with 
277 
 Cvar _  Pck_const (_,_) > false


217 
 Cvar > false 

278  218 
 Carrow (ck1,ck2) > (is_polymorphic ck1)  (is_polymorphic ck2) 
279  219 
 Ctuple ckl > List.exists (fun c > is_polymorphic c) ckl 
280  220 
 Con (ck',_,_) > is_polymorphic ck' 
281 
 Pck_up (ck',_)  Pck_down (ck',_) > is_polymorphic ck' 

282 
 Pck_phase (ck',_) > is_polymorphic ck' 

283 
 Cunivar _ > true 

221 
 Cunivar > true 

284  222 
 Clink ck' > is_polymorphic ck' 
285  223 
 Ccarrying (_,ck') > is_polymorphic ck' 
286  224  
...  ...  
290  228 
let rec constrained_vars_of_clock ck = 
291  229 
let rec aux vars ck = 
292  230 
match ck.cdesc with 
293 
 Pck_const (_,_) > 

294 
vars 

295 
 Cvar cset > 

296 
begin 

297 
match cset with 

298 
 CSet_all > vars 

299 
 _ > 

300 
list_union [ck] vars 

301 
end 

231 
 Cvar > vars 

302  232 
 Carrow (ck1,ck2) > 
303  233 
let l = aux vars ck1 in 
304  234 
aux l ck2 
...  ...  
307  237 
(fun acc ck' > aux acc ck') 
308  238 
vars ckl 
309  239 
 Con (ck',_,_) > aux vars ck' 
310 
 Pck_up (ck',_)  Pck_down (ck',_) > aux vars ck' 

311 
 Pck_phase (ck',_) > aux vars ck' 

312 
 Cunivar cset > 

313 
begin 

314 
match cset with 

315 
 CSet_all > vars 

316 
 _ > list_union [ck] vars 

317 
end 

240 
 Cunivar > vars 

318  241 
 Clink ck' > aux vars ck' 
319  242 
 Ccarrying (_,ck') > aux vars ck' 
320  243 
in 
321  244 
aux [] ck 
322  245  
323 
(** [period ck] returns the period of [ck]. Expects a constant pclock 

324 
expression belonging to the correct clock set. *) 

325 
let rec period ck = 

326 
let rec aux ck = 

327 
match ck.cdesc with 

328 
 Carrow (_,_)  Ctuple _  Con (_,_,_) 

329 
 Cvar _  Cunivar _ > 

330 
failwith "internal error: can only compute period of const pck" 

331 
 Pck_up (ck',k) > 

332 
(aux ck')/.(float_of_int k) 

333 
 Pck_down (ck',k) > 

334 
(float_of_int k)*.(aux ck') 

335 
 Pck_phase (ck',_) > 

336 
aux ck' 

337 
 Pck_const (n,_) > 

338 
float_of_int n 

339 
 Clink ck' > aux ck' 

340 
 Ccarrying (_,ck') > aux ck' 

341 
in 

342 
int_of_float (aux ck) 

343  
344 
(** [phase ck] returns the phase of [ck]. It is not expressed as a 

345 
fraction of the period, but instead as an amount of time. Expects a 

346 
constant expression belonging to the correct P_k *) 

347 
let phase ck = 

348 
let rec aux ck = 

349 
match ck.cdesc with 

350 
 Carrow (_,_)  Ctuple _  Con (_,_,_) 

351 
 Cvar _  Cunivar _ > 

352 
failwith "internal error: can only compute phase of const pck" 

353 
 Pck_up (ck',_) > 

354 
aux ck' 

355 
 Pck_down (ck',k) > 

356 
aux ck' 

357 
 Pck_phase (ck',(a,b)) > 

358 
let n = period ck' in 

359 
let (a',b') = aux ck' in 

360 
sum_rat (a',b') (n*a,b) 

361 
 Pck_const (n,(a,b)) > 

362 
(n*a,b) 

363 
 Clink ck' > aux ck' 

364 
 Ccarrying (_,ck') > aux ck' 

365 
in 

366 
let (a,b) = aux ck in 

367 
simplify_rat (a,b) 

368  
369  246 
let eq_carrier cr1 cr2 = 
370  247 
match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with 
371  248 
 Carry_const id1, Carry_const id2 > id1 = id2 
...  ...  
380  257 
match ck.cdesc with 
381  258 
 Ctuple (ck'::_) 
382  259 
 Con (ck',_,_)  Clink ck'  Ccarrying (_,ck') > root ck' 
383 
 Pck_up _  Pck_down _  Pck_phase _  Pck_const _  Cvar _  Cunivar _ > ck


260 
 Cvar  Cunivar > ck


384  261 
 Carrow _  Ctuple _ > failwith "Internal error root" 
385  262  
386  263 
(* Returns the branch of clock [ck] in its clock tree *) 
...  ...  
419  296 
let disjoint ck1 ck2 = 
420  297 
eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2) 
421  298  
422 
(** [normalize pck] returns the normal form of clock [pck]. *) 

423 
let normalize pck = 

424 
let changed = ref true in 

425 
let rec aux pck = 

426 
match pck.cdesc with 

427 
 Pck_up ({cdesc=Pck_up (pck',k')},k) > 

428 
changed:=true; 

429 
new_ck (Pck_up (aux pck',k*k')) pck.cscoped 

430 
 Pck_up ({cdesc=Pck_down (pck',k')},k) > 

431 
changed:=true; 

432 
new_ck (Pck_down (new_ck (Pck_up (aux pck',k)) pck.cscoped,k')) pck.cscoped 

433 
 Pck_up ({cdesc=Pck_phase (pck',(a,b))},k) > 

434 
changed:=true; 

435 
new_ck (Pck_phase (new_ck (Pck_up (aux pck',k)) pck.cscoped,(a*k,b))) pck.cscoped 

436 
 Pck_down ({cdesc=Pck_down (pck',k')},k) > 

437 
changed:=true; 

438 
new_ck (Pck_down (aux pck',k*k')) pck.cscoped 

439 
 Pck_down ({cdesc=Pck_phase (pck',(a,b))},k) > 

440 
changed:=true; 

441 
new_ck (Pck_phase (new_ck (Pck_down (aux pck',k)) pck.cscoped,(a,b*k))) pck.cscoped 

442 
 Pck_phase ({cdesc=Pck_phase (pck',(a',b'))},(a,b)) > 

443 
changed:=true; 

444 
let (a'',b'') = sum_rat (a,b) (a',b') in 

445 
new_ck (Pck_phase (aux pck',(a'',b''))) pck.cscoped 

446 
 Pck_up (pck',k') > 

447 
new_ck (Pck_up (aux pck',k')) pck.cscoped 

448 
 Pck_down (pck',k') > 

449 
new_ck (Pck_down (aux pck',k')) pck.cscoped 

450 
 Pck_phase (pck',k') > 

451 
new_ck (Pck_phase (aux pck',k')) pck.cscoped 

452 
 Ccarrying (cr,ck') > 

453 
new_ck (Ccarrying (cr, aux ck')) pck.cscoped 

454 
 _ > pck 

455 
in 

456 
let nf=ref pck in 

457 
while !changed do 

458 
changed:=false; 

459 
nf:=aux !nf 

460 
done; 

461 
!nf 

462  
463 
(** [canonize pck] reduces transformations of [pck] and removes 

464 
identity transformations. Expects a normalized periodic clock ! *) 

465 
let canonize pck = 

466 
let rec remove_id_trans pck = 

467 
match pck.cdesc with 

468 
 Pck_up (pck',1)  Pck_down (pck',1)  Pck_phase (pck',(0,_)) > 

469 
remove_id_trans pck' 

470 
 _ > pck 

471 
in 

472 
let pck = 

473 
match pck.cdesc with 

474 
 Pck_phase ({cdesc=Pck_down ({cdesc=Pck_up (v,k)},k')},k'') > 

475 
let gcd = gcd k k' in 

476 
new_ck (Pck_phase 

477 
(new_ck (Pck_down 

478 
(new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd)) 

479 
pck.cscoped,k'')) 

480 
pck.cscoped 

481 
 Pck_down ({cdesc=Pck_up (v,k)},k') > 

482 
let gcd = gcd k k' in 

483 
new_ck (Pck_down (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd)) pck.cscoped 

484 
 _ > pck 

485 
in 

486 
remove_id_trans pck 

487  
488 
(** [simplify pck] applies pclocks simplifications to [pck] *) 

489 
let simplify pck = 

490 
if (is_concrete_pck pck) then 

491 
let n = period pck in 

492 
let (a,b) = phase pck in 

493 
let phase' = simplify_rat (a,b*n) in 

494 
new_ck (Pck_const (n,phase')) pck.cscoped 

495 
else 

496 
let pck' = deep_repr pck in 

497 
let nf_pck = normalize pck' in 

498 
canonize nf_pck 

499 


500  299 
let print_cvar fmt cvar = 
501  300 
match cvar.cdesc with 
502 
 Cvar cset >


301 
 Cvar > 

503  302 
(* 
504  303 
if cvar.cscoped 
505  304 
then 
506 
fprintf fmt "[_%s%a]"


305 
fprintf fmt "[_%s]" 

507  306 
(name_of_type cvar.cid) 
508 
print_ckset cset 

509  307 
else 
510  308 
*) 
511 
fprintf fmt "_%s%a"


309 
fprintf fmt "_%s" 

512  310 
(name_of_type cvar.cid) 
513 
print_ckset cset 

514 
 Cunivar cset > 

311 
 Cunivar > 

515  312 
(* 
516  313 
if cvar.cscoped 
517  314 
then 
518 
fprintf fmt "['%s%a]"


315 
fprintf fmt "['%s]" 

519  316 
(name_of_type cvar.cid) 
520 
print_ckset cset 

521  317 
else 
522  318 
*) 
523 
fprintf fmt "'%s%a"


319 
fprintf fmt "'%s" 

524  320 
(name_of_type cvar.cid) 
525 
print_ckset cset 

526  321 
 _ > failwith "Internal error print_cvar" 
527  322  
528  323 
(* Nice prettyprinting. Simplifies expressions before printing them. Nonlinear 
529  324 
complexity. *) 
530  325 
let print_ck fmt ck = 
531  326 
let rec aux fmt ck = 
532 
let ck = simplify ck in 

533  327 
match ck.cdesc with 
534  328 
 Carrow (ck1,ck2) > 
535  329 
fprintf fmt "%a > %a" aux ck1 aux ck2 
...  ...  
538  332 
(fprintf_list ~sep:" * " aux) cklist 
539  333 
 Con (ck,c,l) > 
540  334 
fprintf fmt "%a on %s(%a)" aux ck l print_carrier c 
541 
 Pck_up (ck,k) > 

542 
fprintf fmt "%a*.%i" aux ck k 

543 
 Pck_down (ck,k) > 

544 
fprintf fmt "%a/.%i" aux ck k 

545 
 Pck_phase (ck,q) > 

546 
fprintf fmt "%a>.%a" aux ck print_rat (simplify_rat q) 

547 
 Pck_const (n,p) > 

548 
fprintf fmt "(%i,%a)" n print_rat (simplify_rat p) 

549 
 Cvar cset > 

335 
 Cvar > 

550  336 
(* 
551  337 
if ck.cscoped 
552  338 
then 
...  ...  
554  340 
else 
555  341 
*) 
556  342 
fprintf fmt "_%s" (name_of_type ck.cid) 
557 
 Cunivar cset >


343 
 Cunivar > 

558  344 
(* 
559  345 
if ck.cscoped 
560  346 
then 
...  ...  
575  361  
576  362 
(* prints only the Con components of a clock, useful for printing nodes *) 
577  363 
let rec print_ck_suffix fmt ck = 
578 
let ck = simplify ck in 

579  364 
match ck.cdesc with 
580  365 
 Carrow _ 
581  366 
 Ctuple _ 
582 
 Cvar _


583 
 Cunivar _ > ()


367 
 Cvar 

368 
 Cunivar > () 

584  369 
 Con (ck,c,l) > 
585  370 
fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c 
586  371 
 Clink ck' > 
587  372 
print_ck_suffix fmt ck' 
588  373 
 Ccarrying (cr,ck') > 
589  374 
fprintf fmt "%a" print_ck_suffix ck' 
590 
 _ > assert false 

375  
591  376  
592  377 
let pp_error fmt = function 
593  378 
 Clock_clash (ck1,ck2) > 
...  ...  
595  380 
fprintf fmt "Expected clock %a, got clock %a@." 
596  381 
print_ck ck1 
597  382 
print_ck ck2 
598 
 Not_pck > 

599 
fprintf fmt "The clock of this expression must be periodic@." 

600  383 
 Carrier_mismatch (cr1, cr2) > 
601  384 
fprintf fmt "Name clash. Expected clock %a, got clock %a@." 
602  385 
print_carrier cr1 
603  386 
print_carrier cr2 
604 
 Clock_set_mismatch (ck,cset) > 

605 
reset_names (); 

606 
fprintf fmt "Clock %a is not included in clock set %a@." 

607 
print_ck ck 

608 
print_ckset cset 

609  387 
 Cannot_be_polymorphic ck > 
610  388 
reset_names (); 
611  389 
fprintf fmt "The main node cannot have a polymorphic clock: %a@." 
...  ...  
630  408 
print_ck ck 
631  409  
632  410 
let const_of_carrier cr = 
633 
match (carrier_repr cr).carrier_desc with 

634 
 Carry_const id > id 

635 
 Carry_name 

636 
 Carry_var 

637 
 Carry_link _ > (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *) 

411 
match (carrier_repr cr).carrier_desc with


412 
 Carry_const id > id


413 
 Carry_name


414 
 Carry_var


415 
 Carry_link _ > (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)


638  416 

639  417 
let uneval const cr = 
640  418 
(*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*) 
Also available in: Unified diff