lustrec / src / clocks.ml @ 22fe1c93
History | View | Annotate | Download (17.3 KB)
1 |
(* ---------------------------------------------------------------------------- |
---|---|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
3 |
* Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
4 |
* |
5 |
* This file is part of Prelude |
6 |
* |
7 |
* Prelude is free software; you can redistribute it and/or |
8 |
* modify it under the terms of the GNU Lesser General Public License |
9 |
* as published by the Free Software Foundation ; either version 2 of |
10 |
* the License, or (at your option) any later version. |
11 |
* |
12 |
* Prelude is distributed in the hope that it will be useful, but |
13 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
14 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
15 |
* Lesser General Public License for more details. |
16 |
* |
17 |
* You should have received a copy of the GNU Lesser General Public |
18 |
* License along with this program ; if not, write to the Free Software |
19 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
20 |
* USA |
21 |
*---------------------------------------------------------------------------- *) |
22 |
|
23 |
(** Clocks definitions and a few utility functions on clocks. *) |
24 |
open Utils |
25 |
open Format |
26 |
|
27 |
(* Clock type sets, for subtyping. *) |
28 |
type clock_set = |
29 |
CSet_all |
30 |
| CSet_pck of int*rat |
31 |
|
32 |
(* Clock carriers basically correspond to the "c" in "x when c" *) |
33 |
type carrier_desc = |
34 |
| Carry_const of ident |
35 |
| Carry_name |
36 |
| Carry_var |
37 |
| Carry_link of carrier_expr |
38 |
|
39 |
(* Carriers are scoped, to detect clock extrusion. In other words, we |
40 |
check the scope of a clock carrier before generalizing it. *) |
41 |
and carrier_expr = |
42 |
{mutable carrier_desc: carrier_desc; |
43 |
mutable carrier_scoped: bool; |
44 |
carrier_id: int} |
45 |
|
46 |
type clock_expr = |
47 |
{mutable cdesc: clock_desc; |
48 |
mutable cscoped: bool; |
49 |
cid: int} |
50 |
|
51 |
(* pck stands for periodic clock. Easier not to separate pck from other clocks *) |
52 |
and clock_desc = |
53 |
| Carrow of clock_expr * clock_expr |
54 |
| Ctuple of clock_expr list |
55 |
| Con of clock_expr * carrier_expr * ident |
56 |
| Pck_up of clock_expr * int |
57 |
| Pck_down of clock_expr * int |
58 |
| Pck_phase of clock_expr * rat |
59 |
| Pck_const of int * rat |
60 |
| Cvar of clock_set (* Monomorphic clock variable *) |
61 |
| Cunivar of clock_set (* Polymorphic clock variable *) |
62 |
| Clink of clock_expr (* During unification, make links instead of substitutions *) |
63 |
| Ccarrying of carrier_expr * clock_expr |
64 |
|
65 |
type error = |
66 |
| Clock_clash of clock_expr * clock_expr |
67 |
| Not_pck |
68 |
| Clock_set_mismatch of clock_expr * clock_set |
69 |
| Cannot_be_polymorphic of clock_expr |
70 |
| Invalid_imported_clock of clock_expr |
71 |
| Invalid_const of clock_expr |
72 |
| Factor_zero |
73 |
| Carrier_mismatch of carrier_expr * carrier_expr |
74 |
| Carrier_extrusion of clock_expr * carrier_expr |
75 |
| Clock_extrusion of clock_expr * clock_expr |
76 |
|
77 |
exception Unify of clock_expr * clock_expr |
78 |
exception Subsume of clock_expr * clock_set |
79 |
exception Mismatch of carrier_expr * carrier_expr |
80 |
exception Scope_carrier of carrier_expr |
81 |
exception Scope_clock of clock_expr |
82 |
exception Error of Location.t * error |
83 |
|
84 |
let new_id = ref (-1) |
85 |
|
86 |
let new_ck desc scoped = |
87 |
incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped} |
88 |
|
89 |
let new_var scoped = |
90 |
new_ck (Cvar CSet_all) scoped |
91 |
|
92 |
let new_univar () = |
93 |
new_ck (Cunivar CSet_all) false |
94 |
|
95 |
let new_carrier_id = ref (-1) |
96 |
|
97 |
let new_carrier desc scoped = |
98 |
incr new_carrier_id; {carrier_desc = desc; |
99 |
carrier_id = !new_carrier_id; |
100 |
carrier_scoped = scoped} |
101 |
|
102 |
let new_carrier_name () = |
103 |
new_carrier Carry_name true |
104 |
|
105 |
let rec repr = |
106 |
function |
107 |
{cdesc=Clink ck'} -> |
108 |
repr ck' |
109 |
| ck -> ck |
110 |
|
111 |
let rec carrier_repr = |
112 |
function {carrier_desc = Carry_link cr'} -> carrier_repr cr' |
113 |
| cr -> cr |
114 |
|
115 |
(** Splits [ck] into the [lhs,rhs] of an arrow clock. Expects an arrow clock |
116 |
(ensured by language syntax) *) |
117 |
let split_arrow ck = |
118 |
match (repr ck).cdesc with |
119 |
| Carrow (cin,cout) -> cin,cout |
120 |
(* Functions are not first order, I don't think the var case |
121 |
needs to be considered here *) |
122 |
| _ -> failwith "Internal error: not an arrow clock" |
123 |
|
124 |
let uncarrier ck = |
125 |
match ck.cdesc with |
126 |
| Ccarrying (cr, ck') -> ck' |
127 |
| _ -> ck |
128 |
|
129 |
(* Removes all links in a clock. Only used for clocks |
130 |
simplification though. *) |
131 |
let rec deep_repr ck = |
132 |
match ck.cdesc with |
133 |
| Carrow (ck1,ck2) -> |
134 |
new_ck (Carrow (deep_repr ck1, deep_repr ck2)) ck.cscoped |
135 |
| Ctuple cl -> |
136 |
new_ck (Ctuple (List.map deep_repr cl)) ck.cscoped |
137 |
| Con (ck', c, l) -> |
138 |
new_ck (Con (deep_repr ck', c, l)) ck.cscoped |
139 |
| Pck_up (ck',k) -> |
140 |
new_ck (Pck_up (deep_repr ck',k)) ck.cscoped |
141 |
| Pck_down (ck',k) -> |
142 |
new_ck (Pck_down (deep_repr ck',k)) ck.cscoped |
143 |
| Pck_phase (ck',q) -> |
144 |
new_ck (Pck_phase (deep_repr ck',q)) ck.cscoped |
145 |
| Pck_const (_,_) | Cvar _ | Cunivar _ -> ck |
146 |
| Clink ck' -> deep_repr ck' |
147 |
| Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, deep_repr ck')) ck.cscoped |
148 |
|
149 |
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock |
150 |
(ensured by language syntax) *) |
151 |
let split_arrow ck = |
152 |
match (repr ck).cdesc with |
153 |
| Carrow (cin,cout) -> cin,cout |
154 |
| _ -> failwith "Internal error: not an arrow clock" |
155 |
|
156 |
(** Returns the clock corresponding to a clock list. *) |
157 |
let clock_of_clock_list ckl = |
158 |
if (List.length ckl) > 1 then |
159 |
new_ck (Ctuple ckl) true |
160 |
else |
161 |
List.hd ckl |
162 |
|
163 |
let clock_list_of_clock ck = |
164 |
match (repr ck).cdesc with |
165 |
| Ctuple cl -> cl |
166 |
| _ -> [ck] |
167 |
|
168 |
let clock_of_impnode_clock ck = |
169 |
let ck = repr ck in |
170 |
match ck.cdesc with |
171 |
| Carrow _ | Clink _ | Cvar _ | Cunivar _ -> |
172 |
failwith "internal error clock_of_impnode_clock" |
173 |
| Ctuple cklist -> List.hd cklist |
174 |
| Con (_,_,_) | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) |
175 |
| Pck_const (_,_) | Ccarrying (_,_) -> ck |
176 |
|
177 |
(** [intersect set1 set2] returns the intersection of clock subsets |
178 |
[set1] and [set2]. *) |
179 |
let intersect set1 set2 = |
180 |
match set1,set2 with |
181 |
| CSet_all,_ -> set2 |
182 |
| _,CSet_all -> set1 |
183 |
| CSet_pck (k,q), CSet_pck (k',q') -> |
184 |
let k'',q'' = lcm k k',max_rat q q' in |
185 |
CSet_pck (k'',q'') |
186 |
|
187 |
(** [can_be_pck ck] returns true if [ck] "may be" a pclock (the uncertainty is |
188 |
due to clock variables) *) |
189 |
let rec can_be_pck ck = |
190 |
match (repr ck).cdesc with |
191 |
| Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) | Pck_const (_,_) |
192 |
| Cvar _ | Cunivar _ -> |
193 |
true |
194 |
| Ccarrying (_,ck') -> can_be_pck ck |
195 |
| _ -> false |
196 |
|
197 |
(** [is_concrete_pck ck] returns true if [ck] is a concrete [pck] (pck |
198 |
transformations applied to a pck constant) *) |
199 |
let rec is_concrete_pck ck = |
200 |
match ck.cdesc with |
201 |
| Carrow (_,_) | Ctuple _ | Con (_,_,_) |
202 |
| Cvar _ | Cunivar _ -> false |
203 |
| Pck_up (ck',_) | Pck_down (ck',_) -> is_concrete_pck ck' |
204 |
| Pck_phase (ck',_) -> is_concrete_pck ck' |
205 |
| Pck_const (_,_) -> true |
206 |
| Clink ck' -> is_concrete_pck ck' |
207 |
| Ccarrying (_,ck') -> false |
208 |
|
209 |
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *) |
210 |
let rec is_polymorphic ck = |
211 |
match ck.cdesc with |
212 |
| Cvar _ | Pck_const (_,_) -> false |
213 |
| Carrow (ck1,ck2) -> (is_polymorphic ck1) || (is_polymorphic ck2) |
214 |
| Ctuple ckl -> List.exists (fun c -> is_polymorphic c) ckl |
215 |
| Con (ck',_,_) -> is_polymorphic ck' |
216 |
| Pck_up (ck',_) | Pck_down (ck',_) -> is_polymorphic ck' |
217 |
| Pck_phase (ck',_) -> is_polymorphic ck' |
218 |
| Cunivar _ -> true |
219 |
| Clink ck' -> is_polymorphic ck' |
220 |
| Ccarrying (_,ck') -> is_polymorphic ck' |
221 |
|
222 |
(** [constrained_vars_of_clock ck] returns the clock variables subject |
223 |
to sub-typing constraints appearing in clock [ck]. Removes duplicates *) |
224 |
(* Used mainly for debug, non-linear complexity. *) |
225 |
let rec constrained_vars_of_clock ck = |
226 |
let rec aux vars ck = |
227 |
match ck.cdesc with |
228 |
| Pck_const (_,_) -> |
229 |
vars |
230 |
| Cvar cset -> |
231 |
begin |
232 |
match cset with |
233 |
| CSet_all -> vars |
234 |
| _ -> |
235 |
list_union [ck] vars |
236 |
end |
237 |
| Carrow (ck1,ck2) -> |
238 |
let l = aux vars ck1 in |
239 |
aux l ck2 |
240 |
| Ctuple ckl -> |
241 |
List.fold_left |
242 |
(fun acc ck' -> aux acc ck') |
243 |
vars ckl |
244 |
| Con (ck',_,_) -> aux vars ck' |
245 |
| Pck_up (ck',_) | Pck_down (ck',_) -> aux vars ck' |
246 |
| Pck_phase (ck',_) -> aux vars ck' |
247 |
| Cunivar cset -> |
248 |
begin |
249 |
match cset with |
250 |
| CSet_all -> vars |
251 |
| _ -> list_union [ck] vars |
252 |
end |
253 |
| Clink ck' -> aux vars ck' |
254 |
| Ccarrying (_,ck') -> aux vars ck' |
255 |
in |
256 |
aux [] ck |
257 |
|
258 |
let print_ckset fmt s = |
259 |
match s with |
260 |
| CSet_all -> () |
261 |
| CSet_pck (k,q) -> |
262 |
let (a,b) = simplify_rat q in |
263 |
if k = 1 && a = 0 then |
264 |
fprintf fmt "<:P" |
265 |
else |
266 |
fprintf fmt "<:P_(%i,%a)" k print_rat (a,b) |
267 |
|
268 |
let rec print_carrier fmt cr = |
269 |
(* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *) |
270 |
match cr.carrier_desc with |
271 |
| Carry_const id -> fprintf fmt "'%s'" id |
272 |
| Carry_name -> |
273 |
fprintf fmt "?%s" (name_of_carrier cr.carrier_id) |
274 |
| Carry_var -> |
275 |
fprintf fmt "_%s" (name_of_carrier cr.carrier_id) |
276 |
| Carry_link cr' -> |
277 |
print_carrier fmt cr' |
278 |
|
279 |
(* Simple pretty-printing, performs no simplifications. Linear |
280 |
complexity. For debug mainly. *) |
281 |
let rec print_ck_long fmt ck = |
282 |
match ck.cdesc with |
283 |
| Carrow (ck1,ck2) -> |
284 |
fprintf fmt "%a->%a" print_ck_long ck1 print_ck_long ck2 |
285 |
| Ctuple cklist -> |
286 |
fprintf fmt "(%a)" |
287 |
(fprintf_list ~sep:" * " print_ck_long) cklist |
288 |
| Con (ck,c,l) -> |
289 |
fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c |
290 |
| Pck_up (ck,k) -> |
291 |
fprintf fmt "%a*^%i" print_ck_long ck k |
292 |
| Pck_down (ck,k) -> |
293 |
fprintf fmt "%a/^%i" print_ck_long ck k |
294 |
| Pck_phase (ck,q) -> |
295 |
fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q) |
296 |
| Pck_const (n,p) -> |
297 |
fprintf fmt "(%i,%a)" n print_rat (simplify_rat p) |
298 |
| Cvar cset -> |
299 |
fprintf fmt "'_%i%a" ck.cid print_ckset cset |
300 |
| Cunivar cset -> |
301 |
fprintf fmt "'%i%a" ck.cid print_ckset cset |
302 |
| Clink ck' -> |
303 |
fprintf fmt "link %a" print_ck_long ck' |
304 |
| Ccarrying (cr,ck') -> |
305 |
fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck' |
306 |
|
307 |
(** [period ck] returns the period of [ck]. Expects a constant pclock |
308 |
expression belonging to the correct clock set. *) |
309 |
let rec period ck = |
310 |
let rec aux ck = |
311 |
match ck.cdesc with |
312 |
| Carrow (_,_) | Ctuple _ | Con (_,_,_) |
313 |
| Cvar _ | Cunivar _ -> |
314 |
failwith "internal error: can only compute period of const pck" |
315 |
| Pck_up (ck',k) -> |
316 |
(aux ck')/.(float_of_int k) |
317 |
| Pck_down (ck',k) -> |
318 |
(float_of_int k)*.(aux ck') |
319 |
| Pck_phase (ck',_) -> |
320 |
aux ck' |
321 |
| Pck_const (n,_) -> |
322 |
float_of_int n |
323 |
| Clink ck' -> aux ck' |
324 |
| Ccarrying (_,ck') -> aux ck' |
325 |
in |
326 |
int_of_float (aux ck) |
327 |
|
328 |
(** [phase ck] returns the phase of [ck]. It is not expressed as a |
329 |
fraction of the period, but instead as an amount of time. Expects a |
330 |
constant expression belonging to the correct P_k *) |
331 |
let phase ck = |
332 |
let rec aux ck = |
333 |
match ck.cdesc with |
334 |
| Carrow (_,_) | Ctuple _ | Con (_,_,_) |
335 |
| Cvar _ | Cunivar _ -> |
336 |
failwith "internal error: can only compute phase of const pck" |
337 |
| Pck_up (ck',_) -> |
338 |
aux ck' |
339 |
| Pck_down (ck',k) -> |
340 |
aux ck' |
341 |
| Pck_phase (ck',(a,b)) -> |
342 |
let n = period ck' in |
343 |
let (a',b') = aux ck' in |
344 |
sum_rat (a',b') (n*a,b) |
345 |
| Pck_const (n,(a,b)) -> |
346 |
(n*a,b) |
347 |
| Clink ck' -> aux ck' |
348 |
| Ccarrying (_,ck') -> aux ck' |
349 |
in |
350 |
let (a,b) = aux ck in |
351 |
simplify_rat (a,b) |
352 |
|
353 |
(* Returns the pck clock parent of a clock *) |
354 |
let rec pclock_parent ck = |
355 |
match (repr ck).cdesc with |
356 |
| Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') -> |
357 |
pclock_parent ck' |
358 |
| Pck_up _ | Pck_down _ | Pck_phase _ | Pck_const _ | Cvar _ | Cunivar _ -> ck |
359 |
| Carrow _ | Ctuple _ -> failwith "Internal error pclock_parent" |
360 |
|
361 |
(** [normalize pck] returns the normal form of clock [pck]. *) |
362 |
let normalize pck = |
363 |
let changed = ref true in |
364 |
let rec aux pck = |
365 |
match pck.cdesc with |
366 |
| Pck_up ({cdesc=Pck_up (pck',k')},k) -> |
367 |
changed:=true; |
368 |
new_ck (Pck_up (aux pck',k*k')) pck.cscoped |
369 |
| Pck_up ({cdesc=Pck_down (pck',k')},k) -> |
370 |
changed:=true; |
371 |
new_ck (Pck_down (new_ck (Pck_up (aux pck',k)) pck.cscoped,k')) pck.cscoped |
372 |
| Pck_up ({cdesc=Pck_phase (pck',(a,b))},k) -> |
373 |
changed:=true; |
374 |
new_ck (Pck_phase (new_ck (Pck_up (aux pck',k)) pck.cscoped,(a*k,b))) pck.cscoped |
375 |
| Pck_down ({cdesc=Pck_down (pck',k')},k) -> |
376 |
changed:=true; |
377 |
new_ck (Pck_down (aux pck',k*k')) pck.cscoped |
378 |
| Pck_down ({cdesc=Pck_phase (pck',(a,b))},k) -> |
379 |
changed:=true; |
380 |
new_ck (Pck_phase (new_ck (Pck_down (aux pck',k)) pck.cscoped,(a,b*k))) pck.cscoped |
381 |
| Pck_phase ({cdesc=Pck_phase (pck',(a',b'))},(a,b)) -> |
382 |
changed:=true; |
383 |
let (a'',b'') = sum_rat (a,b) (a',b') in |
384 |
new_ck (Pck_phase (aux pck',(a'',b''))) pck.cscoped |
385 |
| Pck_up (pck',k') -> |
386 |
new_ck (Pck_up (aux pck',k')) pck.cscoped |
387 |
| Pck_down (pck',k') -> |
388 |
new_ck (Pck_down (aux pck',k')) pck.cscoped |
389 |
| Pck_phase (pck',k') -> |
390 |
new_ck (Pck_phase (aux pck',k')) pck.cscoped |
391 |
| Ccarrying (cr,ck') -> |
392 |
new_ck (Ccarrying (cr, aux ck')) pck.cscoped |
393 |
| _ -> pck |
394 |
in |
395 |
let nf=ref pck in |
396 |
while !changed do |
397 |
changed:=false; |
398 |
nf:=aux !nf |
399 |
done; |
400 |
!nf |
401 |
|
402 |
(** [canonize pck] reduces transformations of [pck] and removes |
403 |
identity transformations. Expects a normalized periodic clock ! *) |
404 |
let canonize pck = |
405 |
let rec remove_id_trans pck = |
406 |
match pck.cdesc with |
407 |
| Pck_up (pck',1) | Pck_down (pck',1) | Pck_phase (pck',(0,_)) -> |
408 |
remove_id_trans pck' |
409 |
| _ -> pck |
410 |
in |
411 |
let pck = |
412 |
match pck.cdesc with |
413 |
| Pck_phase ({cdesc=Pck_down ({cdesc=Pck_up (v,k)},k')},k'') -> |
414 |
let gcd = gcd k k' in |
415 |
new_ck (Pck_phase |
416 |
(new_ck (Pck_down |
417 |
(new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd)) |
418 |
pck.cscoped,k'')) |
419 |
pck.cscoped |
420 |
| Pck_down ({cdesc=Pck_up (v,k)},k') -> |
421 |
let gcd = gcd k k' in |
422 |
new_ck (Pck_down (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd)) pck.cscoped |
423 |
| _ -> pck |
424 |
in |
425 |
remove_id_trans pck |
426 |
|
427 |
(** [simplify pck] applies pclocks simplifications to [pck] *) |
428 |
let simplify pck = |
429 |
if (is_concrete_pck pck) then |
430 |
let n = period pck in |
431 |
let (a,b) = phase pck in |
432 |
let phase' = simplify_rat (a,b*n) in |
433 |
new_ck (Pck_const (n,phase')) pck.cscoped |
434 |
else |
435 |
let pck' = deep_repr pck in |
436 |
let nf_pck = normalize pck' in |
437 |
canonize nf_pck |
438 |
|
439 |
let print_cvar fmt cvar = |
440 |
match cvar.cdesc with |
441 |
| Cvar cset -> |
442 |
(* |
443 |
if cvar.cscoped |
444 |
then |
445 |
fprintf fmt "['_%s%a]" |
446 |
(name_of_type cvar.cid) |
447 |
print_ckset cset |
448 |
else |
449 |
*) |
450 |
fprintf fmt "'_%s%a" |
451 |
(name_of_type cvar.cid) |
452 |
print_ckset cset |
453 |
| Cunivar cset -> |
454 |
(* |
455 |
if cvar.cscoped |
456 |
then |
457 |
fprintf fmt "['%s%a]" |
458 |
(name_of_type cvar.cid) |
459 |
print_ckset cset |
460 |
else |
461 |
*) |
462 |
fprintf fmt "'%s%a" |
463 |
(name_of_type cvar.cid) |
464 |
print_ckset cset |
465 |
| _ -> failwith "Internal error print_cvar" |
466 |
|
467 |
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear |
468 |
complexity. *) |
469 |
let print_ck fmt ck = |
470 |
let rec aux fmt ck = |
471 |
let ck = simplify ck in |
472 |
match ck.cdesc with |
473 |
| Carrow (ck1,ck2) -> |
474 |
fprintf fmt "%a->%a" aux ck1 aux ck2 |
475 |
| Ctuple cklist -> |
476 |
fprintf fmt "(%a)" |
477 |
(fprintf_list ~sep:" * " aux) cklist |
478 |
| Con (ck,c,l) -> |
479 |
fprintf fmt "%a on %s(%a)" aux ck l print_carrier c |
480 |
| Pck_up (ck,k) -> |
481 |
fprintf fmt "%a*.%i" aux ck k |
482 |
| Pck_down (ck,k) -> |
483 |
fprintf fmt "%a/.%i" aux ck k |
484 |
| Pck_phase (ck,q) -> |
485 |
fprintf fmt "%a->.%a" aux ck print_rat (simplify_rat q) |
486 |
| Pck_const (n,p) -> |
487 |
fprintf fmt "(%i,%a)" n print_rat (simplify_rat p) |
488 |
| Cvar cset -> |
489 |
(* |
490 |
if ck.cscoped |
491 |
then |
492 |
fprintf fmt "['_%s]" (name_of_type ck.cid) |
493 |
else |
494 |
*) |
495 |
fprintf fmt "'_%s" (name_of_type ck.cid) |
496 |
| Cunivar cset -> |
497 |
(* |
498 |
if ck.cscoped |
499 |
then |
500 |
fprintf fmt "['%s]" (name_of_type ck.cid) |
501 |
else |
502 |
*) |
503 |
fprintf fmt "'%s" (name_of_type ck.cid) |
504 |
| Clink ck' -> |
505 |
aux fmt ck' |
506 |
| Ccarrying (cr,ck') -> |
507 |
fprintf fmt "(%a:%a)" print_carrier cr aux ck' |
508 |
in |
509 |
let cvars = constrained_vars_of_clock ck in |
510 |
aux fmt ck; |
511 |
if cvars <> [] then |
512 |
fprintf fmt " (where %a)" |
513 |
(fprintf_list ~sep:", " print_cvar) cvars |
514 |
|
515 |
let pp_error fmt = function |
516 |
| Clock_clash (ck1,ck2) -> |
517 |
reset_names (); |
518 |
fprintf fmt "Expected clock %a, got clock %a@." |
519 |
print_ck ck1 |
520 |
print_ck ck2 |
521 |
| Not_pck -> |
522 |
fprintf fmt "The clock of this expression must be periodic@." |
523 |
| Carrier_mismatch (cr1, cr2) -> |
524 |
fprintf fmt "Name clash. Expected clock %a, got clock %a@." |
525 |
print_carrier cr1 |
526 |
print_carrier cr2 |
527 |
| Clock_set_mismatch (ck,cset) -> |
528 |
reset_names (); |
529 |
fprintf fmt "Clock %a is not included in clock set %a@." |
530 |
print_ck ck |
531 |
print_ckset cset |
532 |
| Cannot_be_polymorphic ck -> |
533 |
reset_names (); |
534 |
fprintf fmt "The main node cannot have a polymorphic clock: %a@." |
535 |
print_ck ck |
536 |
| Invalid_imported_clock ck -> |
537 |
reset_names (); |
538 |
fprintf fmt "Not a valid imported node clock: %a@." |
539 |
print_ck ck |
540 |
| Invalid_const ck -> |
541 |
reset_names (); |
542 |
fprintf fmt "Clock %a is not a valid periodic clock@." |
543 |
print_ck ck; |
544 |
| Factor_zero -> |
545 |
fprintf fmt "Cannot apply clock transformation with factor 0@." |
546 |
| Carrier_extrusion (ck,cr) -> |
547 |
fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@." |
548 |
print_ck ck |
549 |
print_carrier cr |
550 |
| Clock_extrusion (ck_node,ck) -> |
551 |
fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@." |
552 |
print_ck ck_node |
553 |
print_ck ck |
554 |
|
555 |
|
556 |
(* Local Variables: *) |
557 |
(* compile-command:"make -C .." *) |
558 |
(* End: *) |