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