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
|
open Utils
|
15
|
(** Clocks definitions and a few utility functions on clocks. *)
|
16
|
|
17
|
open Format
|
18
|
|
19
|
(* (\* Clock type sets, for subtyping. *\) *)
|
20
|
(* type clock_set = *)
|
21
|
(* CSet_all *)
|
22
|
(* | CSet_pck of int*rat *)
|
23
|
|
24
|
(* Clock carriers basically correspond to the "c" in "x when c" *)
|
25
|
type carrier_desc =
|
26
|
| Carry_const of ident
|
27
|
| Carry_name
|
28
|
| Carry_var
|
29
|
| Carry_link of carrier_expr
|
30
|
|
31
|
(* Carriers are scoped, to detect clock extrusion. In other words, we check the
|
32
|
scope of a clock carrier before generalizing it. *)
|
33
|
and carrier_expr = {
|
34
|
mutable carrier_desc : carrier_desc;
|
35
|
mutable carrier_scoped : bool;
|
36
|
carrier_id : int;
|
37
|
}
|
38
|
|
39
|
type clock_expr = {
|
40
|
mutable cdesc : clock_desc;
|
41
|
mutable cscoped : bool;
|
42
|
cid : int;
|
43
|
}
|
44
|
|
45
|
(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
|
46
|
and clock_desc =
|
47
|
| Carrow of clock_expr * clock_expr
|
48
|
| Ctuple of clock_expr list
|
49
|
| Con of clock_expr * carrier_expr * ident
|
50
|
(* | Pck_up of clock_expr * int *)
|
51
|
(* | Pck_down of clock_expr * int *)
|
52
|
(* | Pck_phase of clock_expr * rat *)
|
53
|
(* | Pck_const of int * rat *)
|
54
|
| Cvar (* of clock_set *)
|
55
|
(* Monomorphic clock variable *)
|
56
|
| Cunivar
|
57
|
(* of clock_set *)
|
58
|
(* Polymorphic clock variable *)
|
59
|
| Clink of clock_expr
|
60
|
(* During unification, make links instead of substitutions *)
|
61
|
| Ccarrying of carrier_expr * clock_expr
|
62
|
|
63
|
type error =
|
64
|
| Clock_clash of clock_expr * clock_expr
|
65
|
(* | Not_pck *)
|
66
|
(* | Clock_set_mismatch of clock_expr * clock_set *)
|
67
|
| Cannot_be_polymorphic of clock_expr
|
68
|
| Invalid_imported_clock of clock_expr
|
69
|
| Invalid_const of clock_expr
|
70
|
| Factor_zero
|
71
|
| Carrier_mismatch of carrier_expr * carrier_expr
|
72
|
| Carrier_extrusion of clock_expr * carrier_expr
|
73
|
| Clock_extrusion of clock_expr * clock_expr
|
74
|
|
75
|
exception Unify of clock_expr * clock_expr
|
76
|
|
77
|
exception Mismatch of carrier_expr * carrier_expr
|
78
|
|
79
|
exception Scope_carrier of carrier_expr
|
80
|
|
81
|
exception Scope_clock of clock_expr
|
82
|
|
83
|
exception Error of Location.t * error
|
84
|
|
85
|
let rec print_carrier fmt cr =
|
86
|
(* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun
|
87
|
fmt -> *)
|
88
|
match cr.carrier_desc with
|
89
|
| Carry_const id ->
|
90
|
fprintf fmt "%s" id
|
91
|
| Carry_name ->
|
92
|
fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
|
93
|
| Carry_var ->
|
94
|
fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
|
95
|
| Carry_link cr' ->
|
96
|
print_carrier fmt cr'
|
97
|
|
98
|
(* Simple pretty-printing, performs no simplifications. Linear complexity. For
|
99
|
debug mainly. *)
|
100
|
let rec print_ck_long fmt ck =
|
101
|
match ck.cdesc with
|
102
|
| Carrow (ck1, ck2) ->
|
103
|
fprintf fmt "%a -> %a" print_ck_long ck1 print_ck_long ck2
|
104
|
| Ctuple cklist ->
|
105
|
fprintf fmt "(%a)" (fprintf_list ~sep:" * " print_ck_long) cklist
|
106
|
| Con (ck, c, l) ->
|
107
|
fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
|
108
|
| Cvar ->
|
109
|
fprintf fmt "'_%i" ck.cid
|
110
|
| Cunivar ->
|
111
|
fprintf fmt "'%i" ck.cid
|
112
|
| Clink ck' ->
|
113
|
fprintf fmt "link %a" print_ck_long ck'
|
114
|
| Ccarrying (cr, ck') ->
|
115
|
fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
|
116
|
|
117
|
let new_id = ref (-1)
|
118
|
|
119
|
let rec bottom = { cdesc = Clink bottom; cid = -666; cscoped = false }
|
120
|
|
121
|
let new_ck desc scoped =
|
122
|
incr new_id;
|
123
|
{ cdesc = desc; cid = !new_id; cscoped = scoped }
|
124
|
|
125
|
let new_var scoped = new_ck Cvar scoped
|
126
|
|
127
|
let new_univar () = new_ck Cunivar false
|
128
|
|
129
|
let new_carrier_id = ref (-1)
|
130
|
|
131
|
let new_carrier desc scoped =
|
132
|
incr new_carrier_id;
|
133
|
{ carrier_desc = desc; carrier_id = !new_carrier_id; carrier_scoped = scoped }
|
134
|
|
135
|
let new_carrier_name () = new_carrier Carry_name true
|
136
|
|
137
|
let rec repr = function { cdesc = Clink ck'; _ } -> repr ck' | ck -> ck
|
138
|
|
139
|
let rec carrier_repr = function
|
140
|
| { carrier_desc = Carry_link cr'; _ } ->
|
141
|
carrier_repr cr'
|
142
|
| cr ->
|
143
|
cr
|
144
|
|
145
|
let get_carrier_name ck =
|
146
|
match (repr ck).cdesc with Ccarrying (cr, _) -> Some cr | _ -> None
|
147
|
|
148
|
let rename_carrier_static rename cr =
|
149
|
match (carrier_repr cr).carrier_desc with
|
150
|
| Carry_const id ->
|
151
|
{ cr with carrier_desc = Carry_const (rename id) }
|
152
|
| _ ->
|
153
|
Format.eprintf "internal error: Clocks.rename_carrier_static %a@."
|
154
|
print_carrier cr;
|
155
|
assert false
|
156
|
|
157
|
let rec rename_static rename ck =
|
158
|
match (repr ck).cdesc with
|
159
|
| Ccarrying (cr, ck') ->
|
160
|
{
|
161
|
ck with
|
162
|
cdesc =
|
163
|
Ccarrying (rename_carrier_static rename cr, rename_static rename ck');
|
164
|
}
|
165
|
| Con (ck', cr, l) ->
|
166
|
{
|
167
|
ck with
|
168
|
cdesc = Con (rename_static rename ck', rename_carrier_static rename cr, l);
|
169
|
}
|
170
|
| _ ->
|
171
|
ck
|
172
|
|
173
|
let uncarrier ck = match ck.cdesc with Ccarrying (_, ck') -> ck' | _ -> ck
|
174
|
|
175
|
(* Removes all links in a clock. Only used for clocks simplification though. *)
|
176
|
let rec simplify ck =
|
177
|
match ck.cdesc with
|
178
|
| Carrow (ck1, ck2) ->
|
179
|
new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped
|
180
|
| Ctuple cl ->
|
181
|
new_ck (Ctuple (List.map simplify cl)) ck.cscoped
|
182
|
| Con (ck', c, l) ->
|
183
|
new_ck (Con (simplify ck', c, l)) ck.cscoped
|
184
|
| Cvar | Cunivar ->
|
185
|
ck
|
186
|
| Clink ck' ->
|
187
|
simplify ck'
|
188
|
| Ccarrying (cr, ck') ->
|
189
|
new_ck (Ccarrying (cr, simplify ck')) ck.cscoped
|
190
|
|
191
|
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock
|
192
|
(ensured by language syntax) *)
|
193
|
let split_arrow ck =
|
194
|
match (repr ck).cdesc with
|
195
|
| Carrow (cin, cout) ->
|
196
|
cin, cout
|
197
|
| _ ->
|
198
|
failwith "Internal error: not an arrow clock"
|
199
|
|
200
|
(** Returns the clock corresponding to a clock list. *)
|
201
|
let clock_of_clock_list ckl =
|
202
|
if List.length ckl > 1 then new_ck (Ctuple ckl) true else List.hd ckl
|
203
|
|
204
|
let clock_list_of_clock ck =
|
205
|
match (repr ck).cdesc with Ctuple cl -> cl | _ -> [ ck ]
|
206
|
|
207
|
let clock_on ck cr l =
|
208
|
clock_of_clock_list
|
209
|
(List.map
|
210
|
(fun ck -> new_ck (Con (ck, cr, l)) true)
|
211
|
(clock_list_of_clock ck))
|
212
|
|
213
|
let clock_current ck =
|
214
|
clock_of_clock_list
|
215
|
(List.map
|
216
|
(fun ck ->
|
217
|
match (repr ck).cdesc with
|
218
|
| Con (ck', _, _) ->
|
219
|
ck'
|
220
|
| _ ->
|
221
|
Format.eprintf "internal error: Clocks.clock_current %a@."
|
222
|
print_ck_long (repr ck);
|
223
|
assert false)
|
224
|
(clock_list_of_clock ck))
|
225
|
|
226
|
let clock_of_impnode_clock ck =
|
227
|
let ck = repr ck in
|
228
|
match ck.cdesc with
|
229
|
| Carrow _ | Clink _ | Cvar | Cunivar ->
|
230
|
failwith "internal error clock_of_impnode_clock"
|
231
|
| Ctuple cklist ->
|
232
|
List.hd cklist
|
233
|
| Con (_, _, _) | Ccarrying (_, _) ->
|
234
|
ck
|
235
|
|
236
|
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *)
|
237
|
let rec is_polymorphic ck =
|
238
|
match ck.cdesc with
|
239
|
| Cvar ->
|
240
|
false
|
241
|
| Carrow (ck1, ck2) ->
|
242
|
is_polymorphic ck1 || is_polymorphic ck2
|
243
|
| Ctuple ckl ->
|
244
|
List.exists (fun c -> is_polymorphic c) ckl
|
245
|
| Con (ck', _, _) ->
|
246
|
is_polymorphic ck'
|
247
|
| Cunivar ->
|
248
|
true
|
249
|
| Clink ck' ->
|
250
|
is_polymorphic ck'
|
251
|
| Ccarrying (_, ck') ->
|
252
|
is_polymorphic ck'
|
253
|
|
254
|
(* Used mainly for debug, non-linear complexity. *)
|
255
|
|
256
|
(** [constrained_vars_of_clock ck] returns the clock variables subject to
|
257
|
sub-typing constraints appearing in clock [ck]. Removes duplicates *)
|
258
|
let constrained_vars_of_clock ck =
|
259
|
let rec aux vars ck =
|
260
|
match ck.cdesc with
|
261
|
| Cvar ->
|
262
|
vars
|
263
|
| Carrow (ck1, ck2) ->
|
264
|
let l = aux vars ck1 in
|
265
|
aux l ck2
|
266
|
| Ctuple ckl ->
|
267
|
List.fold_left (fun acc ck' -> aux acc ck') vars ckl
|
268
|
| Con (ck', _, _) ->
|
269
|
aux vars ck'
|
270
|
| Cunivar ->
|
271
|
vars
|
272
|
| Clink ck' ->
|
273
|
aux vars ck'
|
274
|
| Ccarrying (_, ck') ->
|
275
|
aux vars ck'
|
276
|
in
|
277
|
aux [] ck
|
278
|
|
279
|
let eq_carrier cr1 cr2 =
|
280
|
match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
|
281
|
| Carry_const id1, Carry_const id2 ->
|
282
|
id1 = id2
|
283
|
| _ ->
|
284
|
cr1.carrier_id = cr2.carrier_id
|
285
|
|
286
|
let eq_clock ck1 ck2 = (repr ck1).cid = (repr ck2).cid
|
287
|
|
288
|
(* Returns the clock root of a clock *)
|
289
|
let rec root ck =
|
290
|
let ck = repr ck in
|
291
|
match ck.cdesc with
|
292
|
| Ctuple (ck' :: _) | Con (ck', _, _) | Clink ck' | Ccarrying (_, ck') ->
|
293
|
root ck'
|
294
|
| Cvar | Cunivar ->
|
295
|
ck
|
296
|
| Carrow _ | Ctuple _ ->
|
297
|
failwith "Internal error root"
|
298
|
|
299
|
(* Returns the branch of clock [ck] in its clock tree *)
|
300
|
let branch ck =
|
301
|
let rec branch ck acc =
|
302
|
match (repr ck).cdesc with
|
303
|
| Ccarrying (_, ck) ->
|
304
|
branch ck acc
|
305
|
| Con (ck, cr, l) ->
|
306
|
branch ck ((cr, l) :: acc)
|
307
|
| Ctuple (ck :: _) ->
|
308
|
branch ck acc
|
309
|
| Ctuple _ | Carrow _ ->
|
310
|
assert false
|
311
|
| _ ->
|
312
|
acc
|
313
|
in
|
314
|
branch ck []
|
315
|
|
316
|
let clock_of_root_branch r br =
|
317
|
List.fold_left (fun ck (cr, l) -> new_ck (Con (ck, cr, l)) true) r br
|
318
|
|
319
|
(* Computes the (longest) common prefix of two branches *)
|
320
|
let rec common_prefix br1 br2 =
|
321
|
match br1, br2 with
|
322
|
| [], _ | _, [] ->
|
323
|
[]
|
324
|
| (cr1, l1) :: q1, (cr2, l2) :: q2 ->
|
325
|
if eq_carrier cr1 cr2 && l1 = l2 then (cr1, l1) :: common_prefix q1 q2
|
326
|
else []
|
327
|
|
328
|
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *)
|
329
|
let rec disjoint_branches br1 br2 =
|
330
|
match br1, br2 with
|
331
|
| [], _ | _, [] ->
|
332
|
false
|
333
|
| (cr1, l1) :: q1, (cr2, l2) :: q2 ->
|
334
|
eq_carrier cr1 cr2 && (l1 <> l2 || disjoint_branches q1 q2)
|
335
|
|
336
|
(* Disjunction relation between variables based upon their static clocks. *)
|
337
|
let disjoint ck1 ck2 =
|
338
|
eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
|
339
|
|
340
|
let print_cvar fmt cvar =
|
341
|
match cvar.cdesc with
|
342
|
| Cvar ->
|
343
|
(* if cvar.cscoped then fprintf fmt "[_%s]" (name_of_type cvar.cid) else *)
|
344
|
fprintf fmt "_%s" (name_of_type cvar.cid)
|
345
|
| Cunivar ->
|
346
|
(* if cvar.cscoped then fprintf fmt "['%s]" (name_of_type cvar.cid) else *)
|
347
|
fprintf fmt "'%s" (name_of_type cvar.cid)
|
348
|
| _ ->
|
349
|
failwith "Internal error print_cvar"
|
350
|
|
351
|
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
|
352
|
complexity. *)
|
353
|
let print_ck fmt ck =
|
354
|
let rec aux fmt ck =
|
355
|
match ck.cdesc with
|
356
|
| Carrow (ck1, ck2) ->
|
357
|
fprintf fmt "%a -> %a" aux ck1 aux ck2
|
358
|
| Ctuple cklist ->
|
359
|
fprintf fmt "(%a)" (fprintf_list ~sep:" * " aux) cklist
|
360
|
| Con (ck, c, l) ->
|
361
|
fprintf fmt "%a on %s(%a)" aux ck l print_carrier c
|
362
|
| Cvar ->
|
363
|
(* if ck.cscoped then fprintf fmt "[_%s]" (name_of_type ck.cid) else *)
|
364
|
fprintf fmt "_%s" (name_of_type ck.cid)
|
365
|
| Cunivar ->
|
366
|
(* if ck.cscoped then fprintf fmt "['%s]" (name_of_type ck.cid) else *)
|
367
|
fprintf fmt "'%s" (name_of_type ck.cid)
|
368
|
| Clink ck' ->
|
369
|
aux fmt ck'
|
370
|
| Ccarrying (cr, ck') ->
|
371
|
fprintf fmt "(%a:%a)" print_carrier cr aux ck'
|
372
|
in
|
373
|
let cvars = constrained_vars_of_clock ck in
|
374
|
aux fmt ck;
|
375
|
if cvars <> [] then
|
376
|
fprintf fmt " (where %a)" (fprintf_list ~sep:", " print_cvar) cvars
|
377
|
|
378
|
(* prints only the Con components of a clock, useful for printing nodes *)
|
379
|
let rec print_ck_suffix fmt ck =
|
380
|
match ck.cdesc with
|
381
|
| Carrow _ | Ctuple _ | Cvar | Cunivar ->
|
382
|
()
|
383
|
| Con (ck, c, l) ->
|
384
|
if !Options.kind2_print then print_ck_suffix fmt ck
|
385
|
else fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
|
386
|
| Clink ck' ->
|
387
|
print_ck_suffix fmt ck'
|
388
|
| Ccarrying (_, ck') ->
|
389
|
fprintf fmt "%a" print_ck_suffix ck'
|
390
|
|
391
|
let pp_error fmt = function
|
392
|
| Clock_clash (ck1, ck2) ->
|
393
|
reset_names ();
|
394
|
fprintf fmt "Expected clock %a, got clock %a@." print_ck ck1 print_ck ck2
|
395
|
| Carrier_mismatch (cr1, cr2) ->
|
396
|
fprintf fmt "Name clash. Expected clock %a, got clock %a@." print_carrier
|
397
|
cr1 print_carrier cr2
|
398
|
| Cannot_be_polymorphic ck ->
|
399
|
reset_names ();
|
400
|
fprintf fmt "The main node cannot have a polymorphic clock: %a@." print_ck
|
401
|
ck
|
402
|
| Invalid_imported_clock ck ->
|
403
|
reset_names ();
|
404
|
fprintf fmt "Not a valid imported node clock: %a@." print_ck ck
|
405
|
| Invalid_const ck ->
|
406
|
reset_names ();
|
407
|
fprintf fmt "Clock %a is not a valid periodic clock@." print_ck ck
|
408
|
| Factor_zero ->
|
409
|
fprintf fmt "Cannot apply clock transformation with factor 0@."
|
410
|
| Carrier_extrusion (ck, cr) ->
|
411
|
fprintf fmt
|
412
|
"This node has clock@.%a@.It is invalid as the carrier %a escapes its \
|
413
|
scope@."
|
414
|
print_ck ck print_carrier cr
|
415
|
| Clock_extrusion (ck_node, ck) ->
|
416
|
fprintf fmt
|
417
|
"This node has clock@.%a@.It is invalid as the clock %a escapes its \
|
418
|
scope@."
|
419
|
print_ck ck_node print_ck ck
|
420
|
|
421
|
let const_of_carrier cr =
|
422
|
match (carrier_repr cr).carrier_desc with
|
423
|
| Carry_const id ->
|
424
|
id
|
425
|
| Carry_name | Carry_var | Carry_link _ ->
|
426
|
Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr;
|
427
|
assert false
|
428
|
(* TODO check this Xavier *)
|
429
|
|
430
|
let uneval const cr =
|
431
|
(*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)
|
432
|
let cr = carrier_repr cr in
|
433
|
match cr.carrier_desc with
|
434
|
| Carry_var ->
|
435
|
cr.carrier_desc <- Carry_const const
|
436
|
| Carry_name ->
|
437
|
cr.carrier_desc <- Carry_const const
|
438
|
| _ ->
|
439
|
assert false
|
440
|
|
441
|
(* Used in rename functions in Corelang. We have to propagate the renaming to
|
442
|
ids of variables clocking the signals *)
|
443
|
|
444
|
(* Carrier are not renamed. They corresponds to enumerated type constants *)
|
445
|
(* let rec rename_carrier f c = { c with carrier_desc = rename_carrier_desc fvar
|
446
|
c.carrier_desc } and rename_carrier_desc f let re = rename_carrier f match cd
|
447
|
with | Carry_const id -> Carry_const (f id) | Carry_link ce -> Carry_link (re
|
448
|
ce) | _ -> cd *)
|
449
|
|
450
|
let rec rename_clock_expr fvar c =
|
451
|
{ c with cdesc = rename_clock_desc fvar c.cdesc }
|
452
|
|
453
|
and rename_clock_desc fvar cd =
|
454
|
let re = rename_clock_expr fvar in
|
455
|
match cd with
|
456
|
| Carrow (c1, c2) ->
|
457
|
Carrow (re c1, re c2)
|
458
|
| Ctuple cl ->
|
459
|
Ctuple (List.map re cl)
|
460
|
| Con (c1, car, id) ->
|
461
|
Con (re c1, car, fvar id)
|
462
|
| Cvar | Cunivar ->
|
463
|
cd
|
464
|
| Clink c ->
|
465
|
Clink (re c)
|
466
|
| Ccarrying (car, c) ->
|
467
|
Ccarrying (car, re c)
|
468
|
|
469
|
(* Local Variables: *)
|
470
|
(* compile-command:"make -C .." *)
|
471
|
(* End: *)
|