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