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