Revision 3b2bd83d
Added by Teme Kahsai about 8 years ago
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 pretty-printing. Simplifies expressions before printing them. Non-linear |
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
updating to onera version 30f766a:2016-12-04