lustrec / src / clocks.ml @ 4f26dcf5
History | View | Annotate | Download (14.2 KB)
1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|
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 | 22fe1c93 | ploc | |
14 | (** Clocks definitions and a few utility functions on clocks. *) |
||
15 | open Utils |
||
16 | open Format |
||
17 | |||
18 | 45f0f48d | xthirioux | (* (\* Clock type sets, for subtyping. *\) *) |
19 | (* type clock_set = *) |
||
20 | (* CSet_all *) |
||
21 | (* | CSet_pck of int*rat *) |
||
22 | 22fe1c93 | ploc | |
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 | 333e3a25 | ploc | |
37 | 22fe1c93 | ploc | 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 | 45f0f48d | xthirioux | (* | 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 | 22fe1c93 | ploc | | 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 | 45f0f48d | xthirioux | (* | Not_pck *) |
59 | (* | Clock_set_mismatch of clock_expr * clock_set *) |
||
60 | 22fe1c93 | ploc | | 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 | fc886259 | xthirioux | 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 | e39f5319 | xthirioux | fprintf fmt "%a -> %a" print_ck_long ck1 print_ck_long ck2 |
91 | fc886259 | xthirioux | | 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 | 45f0f48d | xthirioux | | Cvar -> fprintf fmt "'_%i" ck.cid |
97 | | Cunivar -> fprintf fmt "'%i" ck.cid |
||
98 | fc886259 | xthirioux | | 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 | 22fe1c93 | ploc | let new_id = ref (-1) |
104 | |||
105 | 04a63d25 | xthirioux | let rec bottom = |
106 | { cdesc = Clink bottom; cid = -666; cscoped = false } |
||
107 | |||
108 | 22fe1c93 | ploc | let new_ck desc scoped = |
109 | incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped} |
||
110 | |||
111 | 45f0f48d | xthirioux | let new_var scoped = new_ck Cvar scoped |
112 | 22fe1c93 | ploc | |
113 | 45f0f48d | xthirioux | let new_univar () = new_ck Cunivar false |
114 | 22fe1c93 | ploc | |
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 | 8f1c7e91 | xthirioux | let get_carrier_name ck = |
145 | match (repr ck).cdesc with |
||
146 | | Ccarrying (cr, _) -> Some cr |
||
147 | | _ -> None |
||
148 | |||
149 | fc886259 | xthirioux | 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 | 22fe1c93 | ploc | let uncarrier ck = |
161 | match ck.cdesc with |
||
162 | 8f1c7e91 | xthirioux | | Ccarrying (_, ck') -> ck' |
163 | | _ -> ck |
||
164 | 22fe1c93 | ploc | |
165 | (* Removes all links in a clock. Only used for clocks |
||
166 | simplification though. *) |
||
167 | 45f0f48d | xthirioux | let rec simplify ck = |
168 | 22fe1c93 | ploc | match ck.cdesc with |
169 | | Carrow (ck1,ck2) -> |
||
170 | 45f0f48d | xthirioux | new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped |
171 | 22fe1c93 | ploc | | Ctuple cl -> |
172 | 45f0f48d | xthirioux | new_ck (Ctuple (List.map simplify cl)) ck.cscoped |
173 | 22fe1c93 | ploc | | Con (ck', c, l) -> |
174 | 45f0f48d | xthirioux | 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 | 22fe1c93 | ploc | |
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 | 6fdfb60b | xthirioux | 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 | 54d032f5 | xthirioux | 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 | 22fe1c93 | ploc | let clock_of_impnode_clock ck = |
205 | let ck = repr ck in |
||
206 | match ck.cdesc with |
||
207 | 45f0f48d | xthirioux | | Carrow _ | Clink _ | Cvar | Cunivar -> |
208 | 22fe1c93 | ploc | failwith "internal error clock_of_impnode_clock" |
209 | | Ctuple cklist -> List.hd cklist |
||
210 | 45f0f48d | xthirioux | | Con (_,_,_) |
211 | | Ccarrying (_,_) -> ck |
||
212 | |||
213 | 22fe1c93 | ploc | |
214 | (** [is_polymorphic ck] returns true if [ck] is polymorphic. *) |
||
215 | let rec is_polymorphic ck = |
||
216 | match ck.cdesc with |
||
217 | 45f0f48d | xthirioux | | Cvar -> false |
218 | 22fe1c93 | ploc | | 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 | 45f0f48d | xthirioux | | Cunivar -> true |
222 | 22fe1c93 | ploc | | 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 | 45f0f48d | xthirioux | | Cvar -> vars |
232 | 22fe1c93 | ploc | | 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 | 45f0f48d | xthirioux | | Cunivar -> vars |
241 | 22fe1c93 | ploc | | Clink ck' -> aux vars ck' |
242 | | Ccarrying (_,ck') -> aux vars ck' |
||
243 | in |
||
244 | aux [] ck |
||
245 | |||
246 | b1a97ade | xthirioux | 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 | 919292ca | xthirioux | let eq_clock ck1 ck2 = |
252 | (repr ck1).cid = (repr ck2).cid |
||
253 | |||
254 | 8f89eba8 | xthirioux | (* Returns the clock root of a clock *) |
255 | let rec root ck = |
||
256 | 919292ca | xthirioux | let ck = repr ck in |
257 | match ck.cdesc with |
||
258 | 6fdfb60b | xthirioux | | Ctuple (ck'::_) |
259 | | Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') -> root ck' |
||
260 | 45f0f48d | xthirioux | | Cvar | Cunivar -> ck |
261 | 6fdfb60b | xthirioux | | Carrow _ | Ctuple _ -> failwith "Internal error root" |
262 | 22fe1c93 | ploc | |
263 | 8f89eba8 | xthirioux | (* 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 | 6fdfb60b | xthirioux | | Ctuple (ck::_) -> branch ck acc |
270 | 919292ca | xthirioux | | Ctuple _ |
271 | 8f89eba8 | xthirioux | | Carrow _ -> assert false |
272 | | _ -> acc |
||
273 | in branch ck [];; |
||
274 | |||
275 | 54d032f5 | xthirioux | 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 | 8f89eba8 | xthirioux | (* 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 | b1a97ade | xthirioux | | (cr1,l1)::q1, (cr2,l2)::q2 -> eq_carrier cr1 cr2 && ((l1 <> l2) || disjoint_branches q1 q2);; |
294 | 8f89eba8 | xthirioux | |
295 | (* Disjunction relation between variables based upon their static clocks. *) |
||
296 | let disjoint ck1 ck2 = |
||
297 | 919292ca | xthirioux | eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2) |
298 | 8f89eba8 | xthirioux | |
299 | 22fe1c93 | ploc | let print_cvar fmt cvar = |
300 | match cvar.cdesc with |
||
301 | 45f0f48d | xthirioux | | Cvar -> |
302 | 22fe1c93 | ploc | (* |
303 | if cvar.cscoped |
||
304 | then |
||
305 | 45f0f48d | xthirioux | fprintf fmt "[_%s]" |
306 | 22fe1c93 | ploc | (name_of_type cvar.cid) |
307 | else |
||
308 | *) |
||
309 | 45f0f48d | xthirioux | fprintf fmt "_%s" |
310 | 22fe1c93 | ploc | (name_of_type cvar.cid) |
311 | 45f0f48d | xthirioux | | Cunivar -> |
312 | 22fe1c93 | ploc | (* |
313 | if cvar.cscoped |
||
314 | then |
||
315 | 45f0f48d | xthirioux | fprintf fmt "['%s]" |
316 | 22fe1c93 | ploc | (name_of_type cvar.cid) |
317 | else |
||
318 | *) |
||
319 | 45f0f48d | xthirioux | fprintf fmt "'%s" |
320 | 22fe1c93 | ploc | (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 | e39f5319 | xthirioux | fprintf fmt "%a -> %a" aux ck1 aux ck2 |
330 | 22fe1c93 | ploc | | 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 | 45f0f48d | xthirioux | | Cvar -> |
336 | 22fe1c93 | ploc | (* |
337 | if ck.cscoped |
||
338 | then |
||
339 | 52cfee34 | xthirioux | fprintf fmt "[_%s]" (name_of_type ck.cid) |
340 | 22fe1c93 | ploc | else |
341 | *) |
||
342 | 52cfee34 | xthirioux | fprintf fmt "_%s" (name_of_type ck.cid) |
343 | 45f0f48d | xthirioux | | Cunivar -> |
344 | 22fe1c93 | ploc | (* |
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 | 8f1c7e91 | xthirioux | (* 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 | 45f0f48d | xthirioux | | Cvar |
368 | | Cunivar -> () |
||
369 | 8f1c7e91 | xthirioux | | 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 | 45f0f48d | xthirioux | |
376 | 8f1c7e91 | xthirioux | |
377 | 22fe1c93 | ploc | 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 | d4807c3d | xthirioux | let const_of_carrier cr = |
411 | 45f0f48d | xthirioux | 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 | d4807c3d | xthirioux | |
417 | 8f1c7e91 | xthirioux | let uneval const cr = |
418 | 89b9e25c | xthirioux | (*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*) |
419 | 8f1c7e91 | xthirioux | let cr = carrier_repr cr in |
420 | match cr.carrier_desc with |
||
421 | | Carry_var -> cr.carrier_desc <- Carry_const const |
||
422 | d4807c3d | xthirioux | | Carry_name -> cr.carrier_desc <- Carry_const const |
423 | 8f1c7e91 | xthirioux | | _ -> assert false |
424 | 22fe1c93 | ploc | |
425 | 333e3a25 | ploc | |
426 | (* Used in rename functions in Corelang. We have to propagate the renaming to |
||
427 | ids of variables clocking the signals *) |
||
428 | |||
429 | (* Carrier are not renamed. They corresponds to enumerated type constants *) |
||
430 | (* |
||
431 | let rec rename_carrier f c = |
||
432 | { c with carrier_desc = rename_carrier_desc fvar c.carrier_desc } |
||
433 | and rename_carrier_desc f |
||
434 | let re = rename_carrier f |
||
435 | match cd with |
||
436 | | Carry_const id -> Carry_const (f id) |
||
437 | | Carry_link ce -> Carry_link (re ce) |
||
438 | | _ -> cd |
||
439 | *) |
||
440 | |||
441 | |||
442 | let rec rename_clock_expr fvar c = |
||
443 | { c with cdesc = rename_clock_desc fvar c.cdesc } |
||
444 | and rename_clock_desc fvar cd = |
||
445 | let re = rename_clock_expr fvar in |
||
446 | match cd with |
||
447 | | Carrow (c1, c2) -> Carrow (re c1, re c2) |
||
448 | | Ctuple cl -> Ctuple (List.map re cl) |
||
449 | | Con (c1, car, id) -> Con (re c1, car, fvar id) |
||
450 | | Cvar |
||
451 | | Cunivar -> cd |
||
452 | | Clink c -> Clink (re c) |
||
453 | | Ccarrying (car, c) -> Ccarrying (car, re c) |
||
454 | |||
455 | 22fe1c93 | ploc | (* Local Variables: *) |
456 | (* compile-command:"make -C .." *) |
||
457 | (* End: *) |