lustrec / src / clocks.ml @ 3b2bd83d
History | View | Annotate | Download (13.4 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 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: *) |