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 Mismatch of carrier_expr * carrier_expr
|
70
|
exception Scope_carrier of carrier_expr
|
71
|
exception Scope_clock of clock_expr
|
72
|
exception Error of Location.t * error
|
73
|
|
74
|
let rec print_carrier fmt cr =
|
75
|
(* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
|
76
|
match cr.carrier_desc with
|
77
|
| Carry_const id -> fprintf fmt "%s" id
|
78
|
| Carry_name ->
|
79
|
fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
|
80
|
| Carry_var ->
|
81
|
fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
|
82
|
| Carry_link cr' ->
|
83
|
print_carrier fmt cr'
|
84
|
|
85
|
(* Simple pretty-printing, performs no simplifications. Linear
|
86
|
complexity. For debug mainly. *)
|
87
|
let rec print_ck_long fmt ck =
|
88
|
match ck.cdesc with
|
89
|
| Carrow (ck1,ck2) ->
|
90
|
fprintf fmt "%a -> %a" print_ck_long ck1 print_ck_long ck2
|
91
|
| Ctuple cklist ->
|
92
|
fprintf fmt "(%a)"
|
93
|
(fprintf_list ~sep:" * " print_ck_long) cklist
|
94
|
| Con (ck,c,l) ->
|
95
|
fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
|
96
|
| Cvar -> fprintf fmt "'_%i" ck.cid
|
97
|
| Cunivar -> fprintf fmt "'%i" ck.cid
|
98
|
| Clink ck' ->
|
99
|
fprintf fmt "link %a" print_ck_long ck'
|
100
|
| Ccarrying (cr,ck') ->
|
101
|
fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
|
102
|
|
103
|
let new_id = ref (-1)
|
104
|
|
105
|
let rec bottom =
|
106
|
{ cdesc = Clink bottom; cid = -666; cscoped = false }
|
107
|
|
108
|
let new_ck desc scoped =
|
109
|
incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped}
|
110
|
|
111
|
let new_var scoped = new_ck Cvar scoped
|
112
|
|
113
|
let new_univar () = new_ck Cunivar false
|
114
|
|
115
|
let new_carrier_id = ref (-1)
|
116
|
|
117
|
let new_carrier desc scoped =
|
118
|
incr new_carrier_id; {carrier_desc = desc;
|
119
|
carrier_id = !new_carrier_id;
|
120
|
carrier_scoped = scoped}
|
121
|
|
122
|
let new_carrier_name () =
|
123
|
new_carrier Carry_name true
|
124
|
|
125
|
let rec repr =
|
126
|
function
|
127
|
{cdesc=Clink ck'} ->
|
128
|
repr ck'
|
129
|
| ck -> ck
|
130
|
|
131
|
let rec carrier_repr =
|
132
|
function {carrier_desc = Carry_link cr'} -> carrier_repr cr'
|
133
|
| cr -> cr
|
134
|
|
135
|
(** Splits [ck] into the [lhs,rhs] of an arrow clock. Expects an arrow clock
|
136
|
(ensured by language syntax) *)
|
137
|
let split_arrow ck =
|
138
|
match (repr ck).cdesc with
|
139
|
| Carrow (cin,cout) -> cin,cout
|
140
|
(* Functions are not first order, I don't think the var case
|
141
|
needs to be considered here *)
|
142
|
| _ -> failwith "Internal error: not an arrow clock"
|
143
|
|
144
|
let get_carrier_name ck =
|
145
|
match (repr ck).cdesc with
|
146
|
| Ccarrying (cr, _) -> Some cr
|
147
|
| _ -> None
|
148
|
|
149
|
let rename_carrier_static rename cr =
|
150
|
match (carrier_repr cr).carrier_desc with
|
151
|
| Carry_const id -> { cr with carrier_desc = Carry_const (rename id) }
|
152
|
| _ -> (Format.eprintf "internal error: Clocks.rename_carrier_static %a@." print_carrier cr; assert false)
|
153
|
|
154
|
let rec rename_static rename ck =
|
155
|
match (repr ck).cdesc with
|
156
|
| Ccarrying (cr, ck') -> { ck with cdesc = Ccarrying (rename_carrier_static rename cr, rename_static rename ck') }
|
157
|
| Con (ck', cr, l) -> { ck with cdesc = Con (rename_static rename ck', rename_carrier_static rename cr, l) }
|
158
|
| _ -> ck
|
159
|
|
160
|
let uncarrier ck =
|
161
|
match ck.cdesc with
|
162
|
| Ccarrying (_, ck') -> ck'
|
163
|
| _ -> ck
|
164
|
|
165
|
(* Removes all links in a clock. Only used for clocks
|
166
|
simplification though. *)
|
167
|
let rec simplify ck =
|
168
|
match ck.cdesc with
|
169
|
| Carrow (ck1,ck2) ->
|
170
|
new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped
|
171
|
| Ctuple cl ->
|
172
|
new_ck (Ctuple (List.map simplify cl)) ck.cscoped
|
173
|
| Con (ck', c, l) ->
|
174
|
new_ck (Con (simplify ck', c, l)) ck.cscoped
|
175
|
| Cvar | Cunivar -> ck
|
176
|
| Clink ck' -> simplify ck'
|
177
|
| Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, simplify ck')) ck.cscoped
|
178
|
|
179
|
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock
|
180
|
(ensured by language syntax) *)
|
181
|
let split_arrow ck =
|
182
|
match (repr ck).cdesc with
|
183
|
| Carrow (cin,cout) -> cin,cout
|
184
|
| _ -> failwith "Internal error: not an arrow clock"
|
185
|
|
186
|
(** Returns the clock corresponding to a clock list. *)
|
187
|
let clock_of_clock_list ckl =
|
188
|
if (List.length ckl) > 1 then
|
189
|
new_ck (Ctuple ckl) true
|
190
|
else
|
191
|
List.hd ckl
|
192
|
|
193
|
let clock_list_of_clock ck =
|
194
|
match (repr ck).cdesc with
|
195
|
| Ctuple cl -> cl
|
196
|
| _ -> [ck]
|
197
|
|
198
|
let clock_on ck cr l =
|
199
|
clock_of_clock_list (List.map (fun ck -> new_ck (Con (ck,cr,l)) true) (clock_list_of_clock ck))
|
200
|
|
201
|
let clock_current ck =
|
202
|
clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with Con(ck',_,_) -> ck' | _ -> assert false) (clock_list_of_clock ck))
|
203
|
|
204
|
let clock_of_impnode_clock ck =
|
205
|
let ck = repr ck in
|
206
|
match ck.cdesc with
|
207
|
| Carrow _ | Clink _ | Cvar | Cunivar ->
|
208
|
failwith "internal error clock_of_impnode_clock"
|
209
|
| Ctuple cklist -> List.hd cklist
|
210
|
| Con (_,_,_)
|
211
|
| Ccarrying (_,_) -> ck
|
212
|
|
213
|
|
214
|
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *)
|
215
|
let rec is_polymorphic ck =
|
216
|
match ck.cdesc with
|
217
|
| Cvar -> false
|
218
|
| Carrow (ck1,ck2) -> (is_polymorphic ck1) || (is_polymorphic ck2)
|
219
|
| Ctuple ckl -> List.exists (fun c -> is_polymorphic c) ckl
|
220
|
| Con (ck',_,_) -> is_polymorphic ck'
|
221
|
| Cunivar -> true
|
222
|
| Clink ck' -> is_polymorphic ck'
|
223
|
| Ccarrying (_,ck') -> is_polymorphic ck'
|
224
|
|
225
|
(** [constrained_vars_of_clock ck] returns the clock variables subject
|
226
|
to sub-typing constraints appearing in clock [ck]. Removes duplicates *)
|
227
|
(* Used mainly for debug, non-linear complexity. *)
|
228
|
let rec constrained_vars_of_clock ck =
|
229
|
let rec aux vars ck =
|
230
|
match ck.cdesc with
|
231
|
| Cvar -> vars
|
232
|
| Carrow (ck1,ck2) ->
|
233
|
let l = aux vars ck1 in
|
234
|
aux l ck2
|
235
|
| Ctuple ckl ->
|
236
|
List.fold_left
|
237
|
(fun acc ck' -> aux acc ck')
|
238
|
vars ckl
|
239
|
| Con (ck',_,_) -> aux vars ck'
|
240
|
| Cunivar -> vars
|
241
|
| Clink ck' -> aux vars ck'
|
242
|
| Ccarrying (_,ck') -> aux vars ck'
|
243
|
in
|
244
|
aux [] ck
|
245
|
|
246
|
let eq_carrier cr1 cr2 =
|
247
|
match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
|
248
|
| Carry_const id1, Carry_const id2 -> id1 = id2
|
249
|
| _ -> cr1.carrier_id = cr2.carrier_id
|
250
|
|
251
|
let eq_clock ck1 ck2 =
|
252
|
(repr ck1).cid = (repr ck2).cid
|
253
|
|
254
|
(* Returns the clock root of a clock *)
|
255
|
let rec root ck =
|
256
|
let ck = repr ck in
|
257
|
match ck.cdesc with
|
258
|
| Ctuple (ck'::_)
|
259
|
| Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') -> root ck'
|
260
|
| Cvar | Cunivar -> ck
|
261
|
| Carrow _ | Ctuple _ -> failwith "Internal error root"
|
262
|
|
263
|
(* Returns the branch of clock [ck] in its clock tree *)
|
264
|
let rec branch ck =
|
265
|
let rec branch ck acc =
|
266
|
match (repr ck).cdesc with
|
267
|
| Ccarrying (_, ck) -> branch ck acc
|
268
|
| Con (ck, cr, l) -> branch ck ((cr, l) :: acc)
|
269
|
| Ctuple (ck::_) -> branch ck acc
|
270
|
| Ctuple _
|
271
|
| Carrow _ -> assert false
|
272
|
| _ -> acc
|
273
|
in branch ck [];;
|
274
|
|
275
|
let clock_of_root_branch r br =
|
276
|
List.fold_left (fun ck (cr,l) -> new_ck (Con (ck, cr, l)) true) r br
|
277
|
|
278
|
(* Computes the (longest) common prefix of two branches *)
|
279
|
let rec common_prefix br1 br2 =
|
280
|
match br1, br2 with
|
281
|
| [] , _
|
282
|
| _ , [] -> []
|
283
|
| (cr1,l1)::q1, (cr2,l2)::q2 ->
|
284
|
if eq_carrier cr1 cr2 && (l1 = l2)
|
285
|
then (cr1, l1) :: common_prefix q1 q2
|
286
|
else []
|
287
|
|
288
|
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *)
|
289
|
let rec disjoint_branches br1 br2 =
|
290
|
match br1, br2 with
|
291
|
| [] , _
|
292
|
| _ , [] -> false
|
293
|
| (cr1,l1)::q1, (cr2,l2)::q2 -> eq_carrier cr1 cr2 && ((l1 <> l2) || disjoint_branches q1 q2);;
|
294
|
|
295
|
(* Disjunction relation between variables based upon their static clocks. *)
|
296
|
let disjoint ck1 ck2 =
|
297
|
eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
|
298
|
|
299
|
let print_cvar fmt cvar =
|
300
|
match cvar.cdesc with
|
301
|
| Cvar ->
|
302
|
(*
|
303
|
if cvar.cscoped
|
304
|
then
|
305
|
fprintf fmt "[_%s]"
|
306
|
(name_of_type cvar.cid)
|
307
|
else
|
308
|
*)
|
309
|
fprintf fmt "_%s"
|
310
|
(name_of_type cvar.cid)
|
311
|
| Cunivar ->
|
312
|
(*
|
313
|
if cvar.cscoped
|
314
|
then
|
315
|
fprintf fmt "['%s]"
|
316
|
(name_of_type cvar.cid)
|
317
|
else
|
318
|
*)
|
319
|
fprintf fmt "'%s"
|
320
|
(name_of_type cvar.cid)
|
321
|
| _ -> failwith "Internal error print_cvar"
|
322
|
|
323
|
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
|
324
|
complexity. *)
|
325
|
let print_ck fmt ck =
|
326
|
let rec aux fmt ck =
|
327
|
match ck.cdesc with
|
328
|
| Carrow (ck1,ck2) ->
|
329
|
fprintf fmt "%a -> %a" aux ck1 aux ck2
|
330
|
| Ctuple cklist ->
|
331
|
fprintf fmt "(%a)"
|
332
|
(fprintf_list ~sep:" * " aux) cklist
|
333
|
| Con (ck,c,l) ->
|
334
|
fprintf fmt "%a on %s(%a)" aux ck l print_carrier c
|
335
|
| Cvar ->
|
336
|
(*
|
337
|
if ck.cscoped
|
338
|
then
|
339
|
fprintf fmt "[_%s]" (name_of_type ck.cid)
|
340
|
else
|
341
|
*)
|
342
|
fprintf fmt "_%s" (name_of_type ck.cid)
|
343
|
| Cunivar ->
|
344
|
(*
|
345
|
if ck.cscoped
|
346
|
then
|
347
|
fprintf fmt "['%s]" (name_of_type ck.cid)
|
348
|
else
|
349
|
*)
|
350
|
fprintf fmt "'%s" (name_of_type ck.cid)
|
351
|
| Clink ck' ->
|
352
|
aux fmt ck'
|
353
|
| Ccarrying (cr,ck') ->
|
354
|
fprintf fmt "(%a:%a)" print_carrier cr aux ck'
|
355
|
in
|
356
|
let cvars = constrained_vars_of_clock ck in
|
357
|
aux fmt ck;
|
358
|
if cvars <> [] then
|
359
|
fprintf fmt " (where %a)"
|
360
|
(fprintf_list ~sep:", " print_cvar) cvars
|
361
|
|
362
|
(* prints only the Con components of a clock, useful for printing nodes *)
|
363
|
let rec print_ck_suffix fmt ck =
|
364
|
match ck.cdesc with
|
365
|
| Carrow _
|
366
|
| Ctuple _
|
367
|
| Cvar
|
368
|
| Cunivar -> ()
|
369
|
| Con (ck,c,l) ->
|
370
|
fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
|
371
|
| Clink ck' ->
|
372
|
print_ck_suffix fmt ck'
|
373
|
| Ccarrying (cr,ck') ->
|
374
|
fprintf fmt "%a" print_ck_suffix ck'
|
375
|
|
376
|
|
377
|
let pp_error fmt = function
|
378
|
| Clock_clash (ck1,ck2) ->
|
379
|
reset_names ();
|
380
|
fprintf fmt "Expected clock %a, got clock %a@."
|
381
|
print_ck ck1
|
382
|
print_ck ck2
|
383
|
| Carrier_mismatch (cr1, cr2) ->
|
384
|
fprintf fmt "Name clash. Expected clock %a, got clock %a@."
|
385
|
print_carrier cr1
|
386
|
print_carrier cr2
|
387
|
| Cannot_be_polymorphic ck ->
|
388
|
reset_names ();
|
389
|
fprintf fmt "The main node cannot have a polymorphic clock: %a@."
|
390
|
print_ck ck
|
391
|
| Invalid_imported_clock ck ->
|
392
|
reset_names ();
|
393
|
fprintf fmt "Not a valid imported node clock: %a@."
|
394
|
print_ck ck
|
395
|
| Invalid_const ck ->
|
396
|
reset_names ();
|
397
|
fprintf fmt "Clock %a is not a valid periodic clock@."
|
398
|
print_ck ck;
|
399
|
| Factor_zero ->
|
400
|
fprintf fmt "Cannot apply clock transformation with factor 0@."
|
401
|
| Carrier_extrusion (ck,cr) ->
|
402
|
fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@."
|
403
|
print_ck ck
|
404
|
print_carrier cr
|
405
|
| Clock_extrusion (ck_node,ck) ->
|
406
|
fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@."
|
407
|
print_ck ck_node
|
408
|
print_ck ck
|
409
|
|
410
|
let const_of_carrier cr =
|
411
|
match (carrier_repr cr).carrier_desc with
|
412
|
| Carry_const id -> id
|
413
|
| Carry_name
|
414
|
| Carry_var
|
415
|
| Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
|
416
|
|
417
|
let uneval const cr =
|
418
|
(*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)
|
419
|
let cr = carrier_repr cr in
|
420
|
match cr.carrier_desc with
|
421
|
| Carry_var -> cr.carrier_desc <- Carry_const const
|
422
|
| Carry_name -> cr.carrier_desc <- Carry_const const
|
423
|
| _ -> assert false
|
424
|
|
425
|
(* Local Variables: *)
|
426
|
(* compile-command:"make -C .." *)
|
427
|
(* End: *)
|