Revision 3b2bd83d 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') > 
...  ...  
123  102  
124  103 
let new_id = ref (1) 
125  104  
105 
let rec bottom = 

106 
{ cdesc = Clink bottom; cid = 666; cscoped = false } 

107  
126  108 
let new_ck desc scoped = 
127  109 
incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped} 
128  110  
129 
let new_var scoped = 

130 
new_ck (Cvar CSet_all) scoped 

111 
let new_var scoped = new_ck Cvar scoped 

131  112  
132 
let new_univar () = 

133 
new_ck (Cunivar CSet_all) false 

113 
let new_univar () = new_ck Cunivar false 

134  114  
135  115 
let new_carrier_id = ref (1) 
136  116  
...  ...  
184  164  
185  165 
(* Removes all links in a clock. Only used for clocks 
186  166 
simplification though. *) 
187 
let rec deep_repr ck =


167 
let rec simplify ck =


188  168 
match ck.cdesc with 
189  169 
 Carrow (ck1,ck2) > 
190 
new_ck (Carrow (deep_repr ck1, deep_repr ck2)) ck.cscoped


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


191  171 
 Ctuple cl > 
192 
new_ck (Ctuple (List.map deep_repr cl)) ck.cscoped


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


193  173 
 Con (ck', c, l) > 
194 
new_ck (Con (deep_repr ck', c, l)) ck.cscoped 

195 
 Pck_up (ck',k) > 

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

197 
 Pck_down (ck',k) > 

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

199 
 Pck_phase (ck',q) > 

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

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

202 
 Clink ck' > deep_repr ck' 

203 
 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 

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


207 
 Carrow _  Clink _  Cvar  Cunivar >


234  208 
failwith "internal error clock_of_impnode_clock" 
235  209 
 Ctuple cklist > List.hd cklist 
236 
 Con (_,_,_)  Pck_up (_,_)  Pck_down (_,_)  Pck_phase (_,_) 

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

238  
239 
(** [intersect set1 set2] returns the intersection of clock subsets 

240 
[set1] and [set2]. *) 

241 
let intersect set1 set2 = 

242 
match set1,set2 with 

243 
 CSet_all,_ > set2 

244 
 _,CSet_all > set1 

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

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

247 
CSet_pck (k'',q'') 

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

250 
due to clock variables) *) 

251 
let rec can_be_pck ck = 

252 
match (repr ck).cdesc with 

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

254 
 Cvar _  Cunivar _ > 

255 
true 

256 
 Ccarrying (_,ck') > can_be_pck ck 

257 
 _ > false 

258  
259 
(** [is_concrete_pck ck] returns true if [ck] is a concrete [pck] (pck 

260 
transformations applied to a pck constant) *) 

261 
let rec is_concrete_pck ck = 

262 
match ck.cdesc with 

263 
 Carrow (_,_)  Ctuple _  Con (_,_,_) 

264 
 Cvar _  Cunivar _ > false 

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

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

267 
 Pck_const (_,_) > true 

268 
 Clink ck' > is_concrete_pck ck' 

269 
 Ccarrying (_,ck') > false 

210 
 Con (_,_,_) 

211 
 Ccarrying (_,_) > ck 

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


217 
 Cvar > false 

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

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

280 
 Cunivar _ > true 

221 
 Cunivar > true 

281  222 
 Clink ck' > is_polymorphic ck' 
282  223 
 Ccarrying (_,ck') > is_polymorphic ck' 
283  224  
...  ...  
287  228 
let rec constrained_vars_of_clock ck = 
288  229 
let rec aux vars ck = 
289  230 
match ck.cdesc with 
290 
 Pck_const (_,_) > 

291 
vars 

292 
 Cvar cset > 

293 
begin 

294 
match cset with 

295 
 CSet_all > vars 

296 
 _ > 

297 
list_union [ck] vars 

298 
end 

231 
 Cvar > vars 

299  232 
 Carrow (ck1,ck2) > 
300  233 
let l = aux vars ck1 in 
301  234 
aux l ck2 
...  ...  
304  237 
(fun acc ck' > aux acc ck') 
305  238 
vars ckl 
306  239 
 Con (ck',_,_) > aux vars ck' 
307 
 Pck_up (ck',_)  Pck_down (ck',_) > aux vars ck' 

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

309 
 Cunivar cset > 

310 
begin 

311 
match cset with 

312 
 CSet_all > vars 

313 
 _ > list_union [ck] vars 

314 
end 

240 
 Cunivar > vars 

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

321 
expression belonging to the correct clock set. *) 

322 
let rec period ck = 

323 
let rec aux ck = 

324 
match ck.cdesc with 

325 
 Carrow (_,_)  Ctuple _  Con (_,_,_) 

326 
 Cvar _  Cunivar _ > 

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

328 
 Pck_up (ck',k) > 

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

330 
 Pck_down (ck',k) > 

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

332 
 Pck_phase (ck',_) > 

333 
aux ck' 

334 
 Pck_const (n,_) > 

335 
float_of_int n 

336 
 Clink ck' > aux ck' 

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

338 
in 

339 
int_of_float (aux ck) 

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

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

343 
constant expression belonging to the correct P_k *) 

344 
let phase ck = 

345 
let rec aux ck = 

346 
match ck.cdesc with 

347 
 Carrow (_,_)  Ctuple _  Con (_,_,_) 

348 
 Cvar _  Cunivar _ > 

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

350 
 Pck_up (ck',_) > 

351 
aux ck' 

352 
 Pck_down (ck',k) > 

353 
aux ck' 

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

355 
let n = period ck' in 

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

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

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

359 
(n*a,b) 

360 
 Clink ck' > aux ck' 

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

362 
in 

363 
let (a,b) = aux ck in 

364 
simplify_rat (a,b) 

365  
366  246 
let eq_carrier cr1 cr2 = 
367  247 
match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with 
368  248 
 Carry_const id1, Carry_const id2 > id1 = id2 
...  ...  
377  257 
match ck.cdesc with 
378  258 
 Ctuple (ck'::_) 
379  259 
 Con (ck',_,_)  Clink ck'  Ccarrying (_,ck') > root ck' 
380 
 Pck_up _  Pck_down _  Pck_phase _  Pck_const _  Cvar _  Cunivar _ > ck


260 
 Cvar  Cunivar > ck


381  261 
 Carrow _  Ctuple _ > failwith "Internal error root" 
382  262  
383  263 
(* Returns the branch of clock [ck] in its clock tree *) 
...  ...  
416  296 
let disjoint ck1 ck2 = 
417  297 
eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2) 
418  298  
419 
(** [normalize pck] returns the normal form of clock [pck]. *) 

420 
let normalize pck = 

421 
let changed = ref true in 

422 
let rec aux pck = 

423 
match pck.cdesc with 

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

425 
changed:=true; 

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

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

428 
changed:=true; 

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

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

431 
changed:=true; 

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

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

434 
changed:=true; 

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

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

437 
changed:=true; 

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

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

440 
changed:=true; 

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

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

443 
 Pck_up (pck',k') > 

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

445 
 Pck_down (pck',k') > 

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

447 
 Pck_phase (pck',k') > 

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

449 
 Ccarrying (cr,ck') > 

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

451 
 _ > pck 

452 
in 

453 
let nf=ref pck in 

454 
while !changed do 

455 
changed:=false; 

456 
nf:=aux !nf 

457 
done; 

458 
!nf 

459  
460 
(** [canonize pck] reduces transformations of [pck] and removes 

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

462 
let canonize pck = 

463 
let rec remove_id_trans pck = 

464 
match pck.cdesc with 

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

466 
remove_id_trans pck' 

467 
 _ > pck 

468 
in 

469 
let pck = 

470 
match pck.cdesc with 

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

472 
let gcd = gcd k k' in 

473 
new_ck (Pck_phase 

474 
(new_ck (Pck_down 

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

476 
pck.cscoped,k'')) 

477 
pck.cscoped 

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

479 
let gcd = gcd k k' in 

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

481 
 _ > pck 

482 
in 

483 
remove_id_trans pck 

484  
485 
(** [simplify pck] applies pclocks simplifications to [pck] *) 

486 
let simplify pck = 

487 
if (is_concrete_pck pck) then 

488 
let n = period pck in 

489 
let (a,b) = phase pck in 

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

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

492 
else 

493 
let pck' = deep_repr pck in 

494 
let nf_pck = normalize pck' in 

495 
canonize nf_pck 

496 


497  299 
let print_cvar fmt cvar = 
498  300 
match cvar.cdesc with 
499 
 Cvar cset >


301 
 Cvar > 

500  302 
(* 
501  303 
if cvar.cscoped 
502  304 
then 
503 
fprintf fmt "[_%s%a]"


305 
fprintf fmt "[_%s]" 

504  306 
(name_of_type cvar.cid) 
505 
print_ckset cset 

506  307 
else 
507  308 
*) 
508 
fprintf fmt "_%s%a"


309 
fprintf fmt "_%s" 

509  310 
(name_of_type cvar.cid) 
510 
print_ckset cset 

511 
 Cunivar cset > 

311 
 Cunivar > 

512  312 
(* 
513  313 
if cvar.cscoped 
514  314 
then 
515 
fprintf fmt "['%s%a]"


315 
fprintf fmt "['%s]" 

516  316 
(name_of_type cvar.cid) 
517 
print_ckset cset 

518  317 
else 
519  318 
*) 
520 
fprintf fmt "'%s%a"


319 
fprintf fmt "'%s" 

521  320 
(name_of_type cvar.cid) 
522 
print_ckset cset 

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

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

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

540 
 Pck_down (ck,k) > 

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

542 
 Pck_phase (ck,q) > 

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

544 
 Pck_const (n,p) > 

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

546 
 Cvar cset > 

335 
 Cvar > 

547  336 
(* 
548  337 
if ck.cscoped 
549  338 
then 
...  ...  
551  340 
else 
552  341 
*) 
553  342 
fprintf fmt "_%s" (name_of_type ck.cid) 
554 
 Cunivar cset >


343 
 Cunivar > 

555  344 
(* 
556  345 
if ck.cscoped 
557  346 
then 
...  ...  
572  361  
573  362 
(* prints only the Con components of a clock, useful for printing nodes *) 
574  363 
let rec print_ck_suffix fmt ck = 
575 
let ck = simplify ck in 

576  364 
match ck.cdesc with 
577  365 
 Carrow _ 
578  366 
 Ctuple _ 
579 
 Cvar _


580 
 Cunivar _ > ()


367 
 Cvar 

368 
 Cunivar > () 

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

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

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

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

602 
reset_names (); 

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

604 
print_ck ck 

605 
print_ckset cset 

606  387 
 Cannot_be_polymorphic ck > 
607  388 
reset_names (); 
608  389 
fprintf fmt "The main node cannot have a polymorphic clock: %a@." 
...  ...  
627  408 
print_ck ck 
628  409  
629  410 
let const_of_carrier cr = 
630 
match (carrier_repr cr).carrier_desc with 

631 
 Carry_const id > id 

632 
 Carry_name 

633 
 Carry_var 

634 
 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 *)


635  416 

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