lustrec / src / clocks.ml @ d50b0dc0
History | View | Annotate | Download (20.5 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 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 |
let rec print_carrier fmt cr = |
86 |
(* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *) |
87 |
match cr.carrier_desc with |
88 |
| Carry_const id -> fprintf fmt "%s" id |
89 |
| Carry_name -> |
90 |
fprintf fmt "_%s" (name_of_carrier cr.carrier_id) |
91 |
| Carry_var -> |
92 |
fprintf fmt "'%s" (name_of_carrier cr.carrier_id) |
93 |
| Carry_link cr' -> |
94 |
print_carrier fmt cr' |
95 |
|
96 |
(* Simple pretty-printing, performs no simplifications. Linear |
97 |
complexity. For debug mainly. *) |
98 |
let rec print_ck_long fmt ck = |
99 |
match ck.cdesc with |
100 |
| Carrow (ck1,ck2) -> |
101 |
fprintf fmt "%a -> %a" print_ck_long ck1 print_ck_long ck2 |
102 |
| Ctuple cklist -> |
103 |
fprintf fmt "(%a)" |
104 |
(fprintf_list ~sep:" * " print_ck_long) cklist |
105 |
| Con (ck,c,l) -> |
106 |
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 |
119 |
| Clink ck' -> |
120 |
fprintf fmt "link %a" print_ck_long ck' |
121 |
| Ccarrying (cr,ck') -> |
122 |
fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck' |
123 |
|
124 |
let new_id = ref (-1) |
125 |
|
126 |
let new_ck desc scoped = |
127 |
incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped} |
128 |
|
129 |
let new_var scoped = |
130 |
new_ck (Cvar CSet_all) scoped |
131 |
|
132 |
let new_univar () = |
133 |
new_ck (Cunivar CSet_all) false |
134 |
|
135 |
let new_carrier_id = ref (-1) |
136 |
|
137 |
let new_carrier desc scoped = |
138 |
incr new_carrier_id; {carrier_desc = desc; |
139 |
carrier_id = !new_carrier_id; |
140 |
carrier_scoped = scoped} |
141 |
|
142 |
let new_carrier_name () = |
143 |
new_carrier Carry_name true |
144 |
|
145 |
let rec repr = |
146 |
function |
147 |
{cdesc=Clink ck'} -> |
148 |
repr ck' |
149 |
| ck -> ck |
150 |
|
151 |
let rec carrier_repr = |
152 |
function {carrier_desc = Carry_link cr'} -> carrier_repr cr' |
153 |
| cr -> cr |
154 |
|
155 |
(** Splits [ck] into the [lhs,rhs] of an arrow clock. Expects an arrow clock |
156 |
(ensured by language syntax) *) |
157 |
let split_arrow ck = |
158 |
match (repr ck).cdesc with |
159 |
| Carrow (cin,cout) -> cin,cout |
160 |
(* Functions are not first order, I don't think the var case |
161 |
needs to be considered here *) |
162 |
| _ -> failwith "Internal error: not an arrow clock" |
163 |
|
164 |
let get_carrier_name ck = |
165 |
match (repr ck).cdesc with |
166 |
| Ccarrying (cr, _) -> Some cr |
167 |
| _ -> None |
168 |
|
169 |
let rename_carrier_static rename cr = |
170 |
match (carrier_repr cr).carrier_desc with |
171 |
| Carry_const id -> { cr with carrier_desc = Carry_const (rename id) } |
172 |
| _ -> (Format.eprintf "internal error: Clocks.rename_carrier_static %a@." print_carrier cr; assert false) |
173 |
|
174 |
let rec rename_static rename ck = |
175 |
match (repr ck).cdesc with |
176 |
| Ccarrying (cr, ck') -> { ck with cdesc = Ccarrying (rename_carrier_static rename cr, rename_static rename ck') } |
177 |
| Con (ck', cr, l) -> { ck with cdesc = Con (rename_static rename ck', rename_carrier_static rename cr, l) } |
178 |
| _ -> ck |
179 |
|
180 |
let uncarrier ck = |
181 |
match ck.cdesc with |
182 |
| Ccarrying (_, ck') -> ck' |
183 |
| _ -> ck |
184 |
|
185 |
(* Removes all links in a clock. Only used for clocks |
186 |
simplification though. *) |
187 |
let rec deep_repr ck = |
188 |
match ck.cdesc with |
189 |
| Carrow (ck1,ck2) -> |
190 |
new_ck (Carrow (deep_repr ck1, deep_repr ck2)) ck.cscoped |
191 |
| Ctuple cl -> |
192 |
new_ck (Ctuple (List.map deep_repr cl)) ck.cscoped |
193 |
| 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 |
204 |
|
205 |
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock |
206 |
(ensured by language syntax) *) |
207 |
let split_arrow ck = |
208 |
match (repr ck).cdesc with |
209 |
| Carrow (cin,cout) -> cin,cout |
210 |
| _ -> failwith "Internal error: not an arrow clock" |
211 |
|
212 |
(** Returns the clock corresponding to a clock list. *) |
213 |
let clock_of_clock_list ckl = |
214 |
if (List.length ckl) > 1 then |
215 |
new_ck (Ctuple ckl) true |
216 |
else |
217 |
List.hd ckl |
218 |
|
219 |
let clock_list_of_clock ck = |
220 |
match (repr ck).cdesc with |
221 |
| Ctuple cl -> cl |
222 |
| _ -> [ck] |
223 |
|
224 |
let clock_on ck cr l = |
225 |
clock_of_clock_list (List.map (fun ck -> new_ck (Con (ck,cr,l)) true) (clock_list_of_clock ck)) |
226 |
|
227 |
let clock_current ck = |
228 |
clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with Con(ck',_,_) -> ck' | _ -> assert false) (clock_list_of_clock ck)) |
229 |
|
230 |
let clock_of_impnode_clock ck = |
231 |
let ck = repr ck in |
232 |
match ck.cdesc with |
233 |
| Carrow _ | Clink _ | Cvar _ | Cunivar _ -> |
234 |
failwith "internal error clock_of_impnode_clock" |
235 |
| 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 |
270 |
|
271 |
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *) |
272 |
let rec is_polymorphic ck = |
273 |
match ck.cdesc with |
274 |
| Cvar _ | Pck_const (_,_) -> false |
275 |
| Carrow (ck1,ck2) -> (is_polymorphic ck1) || (is_polymorphic ck2) |
276 |
| Ctuple ckl -> List.exists (fun c -> is_polymorphic c) ckl |
277 |
| 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 |
281 |
| Clink ck' -> is_polymorphic ck' |
282 |
| Ccarrying (_,ck') -> is_polymorphic ck' |
283 |
|
284 |
(** [constrained_vars_of_clock ck] returns the clock variables subject |
285 |
to sub-typing constraints appearing in clock [ck]. Removes duplicates *) |
286 |
(* Used mainly for debug, non-linear complexity. *) |
287 |
let rec constrained_vars_of_clock ck = |
288 |
let rec aux vars ck = |
289 |
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 |
299 |
| Carrow (ck1,ck2) -> |
300 |
let l = aux vars ck1 in |
301 |
aux l ck2 |
302 |
| Ctuple ckl -> |
303 |
List.fold_left |
304 |
(fun acc ck' -> aux acc ck') |
305 |
vars ckl |
306 |
| 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 |
315 |
| Clink ck' -> aux vars ck' |
316 |
| Ccarrying (_,ck') -> aux vars ck' |
317 |
in |
318 |
aux [] ck |
319 |
|
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 |
let eq_carrier cr1 cr2 = |
367 |
match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with |
368 |
| Carry_const id1, Carry_const id2 -> id1 = id2 |
369 |
| _ -> cr1.carrier_id = cr2.carrier_id |
370 |
|
371 |
let eq_clock ck1 ck2 = |
372 |
(repr ck1).cid = (repr ck2).cid |
373 |
|
374 |
(* Returns the clock root of a clock *) |
375 |
let rec root ck = |
376 |
let ck = repr ck in |
377 |
match ck.cdesc with |
378 |
| Ctuple (ck'::_) |
379 |
| Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') -> root ck' |
380 |
| Pck_up _ | Pck_down _ | Pck_phase _ | Pck_const _ | Cvar _ | Cunivar _ -> ck |
381 |
| Carrow _ | Ctuple _ -> failwith "Internal error root" |
382 |
|
383 |
(* Returns the branch of clock [ck] in its clock tree *) |
384 |
let rec branch ck = |
385 |
let rec branch ck acc = |
386 |
match (repr ck).cdesc with |
387 |
| Ccarrying (_, ck) -> branch ck acc |
388 |
| Con (ck, cr, l) -> branch ck ((cr, l) :: acc) |
389 |
| Ctuple (ck::_) -> branch ck acc |
390 |
| Ctuple _ |
391 |
| Carrow _ -> assert false |
392 |
| _ -> acc |
393 |
in branch ck [];; |
394 |
|
395 |
let clock_of_root_branch r br = |
396 |
List.fold_left (fun ck (cr,l) -> new_ck (Con (ck, cr, l)) true) r br |
397 |
|
398 |
(* Computes the (longest) common prefix of two branches *) |
399 |
let rec common_prefix br1 br2 = |
400 |
match br1, br2 with |
401 |
| [] , _ |
402 |
| _ , [] -> [] |
403 |
| (cr1,l1)::q1, (cr2,l2)::q2 -> |
404 |
if eq_carrier cr1 cr2 && (l1 = l2) |
405 |
then (cr1, l1) :: common_prefix q1 q2 |
406 |
else [] |
407 |
|
408 |
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *) |
409 |
let rec disjoint_branches br1 br2 = |
410 |
match br1, br2 with |
411 |
| [] , _ |
412 |
| _ , [] -> false |
413 |
| (cr1,l1)::q1, (cr2,l2)::q2 -> eq_carrier cr1 cr2 && ((l1 <> l2) || disjoint_branches q1 q2);; |
414 |
|
415 |
(* Disjunction relation between variables based upon their static clocks. *) |
416 |
let disjoint ck1 ck2 = |
417 |
eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2) |
418 |
|
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 |
let print_cvar fmt cvar = |
498 |
match cvar.cdesc with |
499 |
| Cvar cset -> |
500 |
(* |
501 |
if cvar.cscoped |
502 |
then |
503 |
fprintf fmt "[_%s%a]" |
504 |
(name_of_type cvar.cid) |
505 |
print_ckset cset |
506 |
else |
507 |
*) |
508 |
fprintf fmt "_%s%a" |
509 |
(name_of_type cvar.cid) |
510 |
print_ckset cset |
511 |
| Cunivar cset -> |
512 |
(* |
513 |
if cvar.cscoped |
514 |
then |
515 |
fprintf fmt "['%s%a]" |
516 |
(name_of_type cvar.cid) |
517 |
print_ckset cset |
518 |
else |
519 |
*) |
520 |
fprintf fmt "'%s%a" |
521 |
(name_of_type cvar.cid) |
522 |
print_ckset cset |
523 |
| _ -> failwith "Internal error print_cvar" |
524 |
|
525 |
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear |
526 |
complexity. *) |
527 |
let print_ck fmt ck = |
528 |
let rec aux fmt ck = |
529 |
let ck = simplify ck in |
530 |
match ck.cdesc with |
531 |
| Carrow (ck1,ck2) -> |
532 |
fprintf fmt "%a -> %a" aux ck1 aux ck2 |
533 |
| Ctuple cklist -> |
534 |
fprintf fmt "(%a)" |
535 |
(fprintf_list ~sep:" * " aux) cklist |
536 |
| Con (ck,c,l) -> |
537 |
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 -> |
547 |
(* |
548 |
if ck.cscoped |
549 |
then |
550 |
fprintf fmt "[_%s]" (name_of_type ck.cid) |
551 |
else |
552 |
*) |
553 |
fprintf fmt "_%s" (name_of_type ck.cid) |
554 |
| Cunivar cset -> |
555 |
(* |
556 |
if ck.cscoped |
557 |
then |
558 |
fprintf fmt "['%s]" (name_of_type ck.cid) |
559 |
else |
560 |
*) |
561 |
fprintf fmt "'%s" (name_of_type ck.cid) |
562 |
| Clink ck' -> |
563 |
aux fmt ck' |
564 |
| Ccarrying (cr,ck') -> |
565 |
fprintf fmt "(%a:%a)" print_carrier cr aux ck' |
566 |
in |
567 |
let cvars = constrained_vars_of_clock ck in |
568 |
aux fmt ck; |
569 |
if cvars <> [] then |
570 |
fprintf fmt " (where %a)" |
571 |
(fprintf_list ~sep:", " print_cvar) cvars |
572 |
|
573 |
(* prints only the Con components of a clock, useful for printing nodes *) |
574 |
let rec print_ck_suffix fmt ck = |
575 |
let ck = simplify ck in |
576 |
match ck.cdesc with |
577 |
| Carrow _ |
578 |
| Ctuple _ |
579 |
| Cvar _ |
580 |
| Cunivar _ -> () |
581 |
| Con (ck,c,l) -> |
582 |
fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c |
583 |
| Clink ck' -> |
584 |
print_ck_suffix fmt ck' |
585 |
| Ccarrying (cr,ck') -> |
586 |
fprintf fmt "%a" print_ck_suffix ck' |
587 |
| _ -> assert false |
588 |
|
589 |
let pp_error fmt = function |
590 |
| Clock_clash (ck1,ck2) -> |
591 |
reset_names (); |
592 |
fprintf fmt "Expected clock %a, got clock %a@." |
593 |
print_ck ck1 |
594 |
print_ck ck2 |
595 |
| Not_pck -> |
596 |
fprintf fmt "The clock of this expression must be periodic@." |
597 |
| Carrier_mismatch (cr1, cr2) -> |
598 |
fprintf fmt "Name clash. Expected clock %a, got clock %a@." |
599 |
print_carrier cr1 |
600 |
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 |
| Cannot_be_polymorphic ck -> |
607 |
reset_names (); |
608 |
fprintf fmt "The main node cannot have a polymorphic clock: %a@." |
609 |
print_ck ck |
610 |
| Invalid_imported_clock ck -> |
611 |
reset_names (); |
612 |
fprintf fmt "Not a valid imported node clock: %a@." |
613 |
print_ck ck |
614 |
| Invalid_const ck -> |
615 |
reset_names (); |
616 |
fprintf fmt "Clock %a is not a valid periodic clock@." |
617 |
print_ck ck; |
618 |
| Factor_zero -> |
619 |
fprintf fmt "Cannot apply clock transformation with factor 0@." |
620 |
| Carrier_extrusion (ck,cr) -> |
621 |
fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@." |
622 |
print_ck ck |
623 |
print_carrier cr |
624 |
| Clock_extrusion (ck_node,ck) -> |
625 |
fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@." |
626 |
print_ck ck_node |
627 |
print_ck ck |
628 |
|
629 |
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 *) |
635 |
|
636 |
let uneval const cr = |
637 |
(*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*) |
638 |
let cr = carrier_repr cr in |
639 |
match cr.carrier_desc with |
640 |
| Carry_var -> cr.carrier_desc <- Carry_const const |
641 |
| Carry_name -> cr.carrier_desc <- Carry_const const |
642 |
| _ -> assert false |
643 |
|
644 |
(* Local Variables: *) |
645 |
(* compile-command:"make -C .." *) |
646 |
(* End: *) |