lustrec / src / clock_calculus.ml @ 01c7d5e1
History | View | Annotate | Download (30.2 KB)
1 | 22fe1c93 | ploc | (* ---------------------------------------------------------------------------- |
---|---|---|---|
2 | * SchedMCore - A MultiCore Scheduling Framework |
||
3 | * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
||
4 | * |
||
5 | * This file is part of Prelude |
||
6 | * |
||
7 | * Prelude is free software; you can redistribute it and/or |
||
8 | * modify it under the terms of the GNU Lesser General Public License |
||
9 | * as published by the Free Software Foundation ; either version 2 of |
||
10 | * the License, or (at your option) any later version. |
||
11 | * |
||
12 | * Prelude is distributed in the hope that it will be useful, but |
||
13 | * WITHOUT ANY WARRANTY ; without even the implied warranty of |
||
14 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
||
15 | * Lesser General Public License for more details. |
||
16 | * |
||
17 | * You should have received a copy of the GNU Lesser General Public |
||
18 | * License along with this program ; if not, write to the Free Software |
||
19 | * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
||
20 | * USA |
||
21 | *---------------------------------------------------------------------------- *) |
||
22 | |||
23 | (** Main clock-calculus module. Based on type inference algorithms with |
||
24 | destructive unification. Uses a bit of subtyping for periodic clocks. *) |
||
25 | |||
26 | (* Though it shares similarities with the typing module, no code |
||
27 | is shared. Simple environments, very limited identifier scoping, no |
||
28 | identifier redefinition allowed. *) |
||
29 | open Utils |
||
30 | open LustreSpec |
||
31 | open Corelang |
||
32 | open Clocks |
||
33 | open Format |
||
34 | |||
35 | let loc_of_cond loc_containing id = |
||
36 | let pos_start = |
||
37 | {loc_containing.Location.loc_end with |
||
38 | Lexing.pos_cnum=loc_containing.Location.loc_end.Lexing.pos_cnum-(String.length id)} |
||
39 | in |
||
40 | {Location.loc_start = pos_start; |
||
41 | Location.loc_end = loc_containing.Location.loc_end} |
||
42 | |||
43 | (** [occurs cvar ck] returns true if the clock variable [cvar] occurs in |
||
44 | clock [ck]. False otherwise. *) |
||
45 | let rec occurs cvar ck = |
||
46 | let ck = repr ck in |
||
47 | match ck.cdesc with |
||
48 | | Carrow (ck1, ck2) -> |
||
49 | (occurs cvar ck1) || (occurs cvar ck2) |
||
50 | | Ctuple ckl -> |
||
51 | List.exists (occurs cvar) ckl |
||
52 | | Con (ck',_,_) -> occurs cvar ck' |
||
53 | | Pck_up (ck',_) -> occurs cvar ck' |
||
54 | | Pck_down (ck',_) -> occurs cvar ck' |
||
55 | | Pck_phase (ck',_) -> occurs cvar ck' |
||
56 | | Cvar _ -> ck=cvar |
||
57 | | Cunivar _ | Pck_const (_,_) -> false |
||
58 | | Clink ck' -> occurs cvar ck' |
||
59 | | Ccarrying (_,ck') -> occurs cvar ck' |
||
60 | |||
61 | (* Clocks generalization *) |
||
62 | let rec generalize_carrier cr = |
||
63 | match cr.carrier_desc with |
||
64 | | Carry_const _ |
||
65 | | Carry_name -> |
||
66 | if cr.carrier_scoped then |
||
67 | raise (Scope_carrier cr); |
||
68 | cr.carrier_desc <- Carry_var |
||
69 | | Carry_var -> () |
||
70 | | Carry_link cr' -> generalize_carrier cr' |
||
71 | |||
72 | (** Promote monomorphic clock variables to polymorphic clock variables. *) |
||
73 | (* Generalize by side-effects *) |
||
74 | let rec generalize ck = |
||
75 | match ck.cdesc with |
||
76 | | Carrow (ck1,ck2) -> |
||
77 | generalize ck1; generalize ck2 |
||
78 | | Ctuple clist -> |
||
79 | List.iter generalize clist |
||
80 | | Con (ck',cr,_) -> generalize ck'; generalize_carrier cr |
||
81 | | Cvar cset -> |
||
82 | if ck.cscoped then |
||
83 | raise (Scope_clock ck); |
||
84 | ck.cdesc <- Cunivar cset |
||
85 | | Pck_up (ck',_) -> generalize ck' |
||
86 | | Pck_down (ck',_) -> generalize ck' |
||
87 | | Pck_phase (ck',_) -> generalize ck' |
||
88 | | Pck_const (_,_) | Cunivar _ -> () |
||
89 | | Clink ck' -> |
||
90 | generalize ck' |
||
91 | | Ccarrying (cr,ck') -> |
||
92 | generalize_carrier cr; generalize ck' |
||
93 | |||
94 | let try_generalize ck_node loc = |
||
95 | try |
||
96 | generalize ck_node |
||
97 | with (Scope_carrier cr) -> |
||
98 | raise (Error (loc, Carrier_extrusion (ck_node, cr))) |
||
99 | | (Scope_clock ck) -> |
||
100 | raise (Error (loc, Clock_extrusion (ck_node, ck))) |
||
101 | |||
102 | (* Clocks instanciation *) |
||
103 | 7291cb80 | xthirioux | let instantiate_carrier cr inst_cr_vars = |
104 | 22fe1c93 | ploc | let cr = carrier_repr cr in |
105 | match cr.carrier_desc with |
||
106 | | Carry_const _ |
||
107 | | Carry_name -> cr |
||
108 | | Carry_link _ -> |
||
109 | failwith "Internal error" |
||
110 | | Carry_var -> |
||
111 | try |
||
112 | List.assoc cr.carrier_id !inst_cr_vars |
||
113 | with Not_found -> |
||
114 | let cr_var = new_carrier Carry_name true in |
||
115 | inst_cr_vars := (cr.carrier_id,cr_var)::!inst_cr_vars; |
||
116 | cr_var |
||
117 | |||
118 | (** Downgrade polymorphic clock variables to monomorphic clock variables *) |
||
119 | (* inst_ck_vars ensures that a polymorphic variable is instanciated with |
||
120 | the same monomorphic variable if it occurs several times in the same |
||
121 | type. inst_cr_vars is the same for carriers. *) |
||
122 | 7291cb80 | xthirioux | let rec instantiate inst_ck_vars inst_cr_vars ck = |
123 | 22fe1c93 | ploc | match ck.cdesc with |
124 | | Carrow (ck1,ck2) -> |
||
125 | {ck with cdesc = |
||
126 | 7291cb80 | xthirioux | Carrow ((instantiate inst_ck_vars inst_cr_vars ck1), |
127 | (instantiate inst_ck_vars inst_cr_vars ck2))} |
||
128 | 22fe1c93 | ploc | | Ctuple cklist -> |
129 | {ck with cdesc = Ctuple |
||
130 | 7291cb80 | xthirioux | (List.map (instantiate inst_ck_vars inst_cr_vars) cklist)} |
131 | 22fe1c93 | ploc | | Con (ck',c,l) -> |
132 | 7291cb80 | xthirioux | let c' = instantiate_carrier c inst_cr_vars in |
133 | {ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)} |
||
134 | 22fe1c93 | ploc | | Cvar _ | Pck_const (_,_) -> ck |
135 | | Pck_up (ck',k) -> |
||
136 | 7291cb80 | xthirioux | {ck with cdesc = Pck_up ((instantiate inst_ck_vars inst_cr_vars ck'),k)} |
137 | 22fe1c93 | ploc | | Pck_down (ck',k) -> |
138 | 7291cb80 | xthirioux | {ck with cdesc = Pck_down ((instantiate inst_ck_vars inst_cr_vars ck'),k)} |
139 | 22fe1c93 | ploc | | Pck_phase (ck',q) -> |
140 | 7291cb80 | xthirioux | {ck with cdesc = Pck_phase ((instantiate inst_ck_vars inst_cr_vars ck'),q)} |
141 | 22fe1c93 | ploc | | Clink ck' -> |
142 | 7291cb80 | xthirioux | {ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')} |
143 | 22fe1c93 | ploc | | Ccarrying (cr,ck') -> |
144 | 7291cb80 | xthirioux | let cr' = instantiate_carrier cr inst_cr_vars in |
145 | 22fe1c93 | ploc | {ck with cdesc = |
146 | 7291cb80 | xthirioux | Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')} |
147 | 22fe1c93 | ploc | | Cunivar cset -> |
148 | try |
||
149 | List.assoc ck.cid !inst_ck_vars |
||
150 | with Not_found -> |
||
151 | let var = new_ck (Cvar cset) true in |
||
152 | inst_ck_vars := (ck.cid, var)::!inst_ck_vars; |
||
153 | var |
||
154 | |||
155 | (** [subsume pck1 cset1] subsumes clock [pck1] by clock subset |
||
156 | [cset1]. The clock constraint is actually recursively transfered to |
||
157 | the clock variable appearing in [pck1] *) |
||
158 | let subsume pck1 cset1 = |
||
159 | let rec aux pck cset = |
||
160 | match cset with |
||
161 | | CSet_all -> |
||
162 | () |
||
163 | | CSet_pck (k,(a,b)) -> |
||
164 | match pck.cdesc with |
||
165 | | Cvar cset' -> |
||
166 | pck.cdesc <- Cvar (intersect cset' cset) |
||
167 | | Pck_up (pck',k') -> |
||
168 | let rat = if a=0 then (0,1) else (a,b*k') in |
||
169 | aux pck' (CSet_pck ((k*k'),rat)) |
||
170 | | Pck_down (pck',k') -> |
||
171 | let k''=k/(gcd k k') in |
||
172 | aux pck' (CSet_pck (k'',(a*k',b))) |
||
173 | | Pck_phase (pck',(a',b')) -> |
||
174 | let (a'',b'')= max_rat (sum_rat (a,b) (-a',b')) (0,1) in |
||
175 | aux pck' (CSet_pck (k, (a'',b''))) |
||
176 | | Pck_const (n,(a',b')) -> |
||
177 | if n mod k <> 0 || (max_rat (a,b) (a',b')) <> (a',b') then |
||
178 | raise (Subsume (pck1, cset1)) |
||
179 | | Clink pck' -> |
||
180 | aux pck' cset |
||
181 | | Cunivar _ -> () |
||
182 | | Ccarrying (_,ck') -> |
||
183 | aux ck' cset |
||
184 | | _ -> raise (Subsume (pck1, cset1)) |
||
185 | in |
||
186 | aux pck1 cset1 |
||
187 | |||
188 | let rec update_scope_carrier scoped cr = |
||
189 | if (not scoped) then |
||
190 | begin |
||
191 | cr.carrier_scoped <- scoped; |
||
192 | match cr.carrier_desc with |
||
193 | | Carry_const _ | Carry_name | Carry_var -> () |
||
194 | | Carry_link cr' -> update_scope_carrier scoped cr' |
||
195 | end |
||
196 | |||
197 | let rec update_scope scoped ck = |
||
198 | if (not scoped) then |
||
199 | begin |
||
200 | ck.cscoped <- scoped; |
||
201 | match ck.cdesc with |
||
202 | | Carrow (ck1,ck2) -> |
||
203 | update_scope scoped ck1; update_scope scoped ck2 |
||
204 | | Ctuple clist -> |
||
205 | List.iter (update_scope scoped) clist |
||
206 | | Con (ck',cr,_) -> update_scope scoped ck'(*; update_scope_carrier scoped cr*) |
||
207 | | Cvar cset -> |
||
208 | ck.cdesc <- Cvar cset |
||
209 | | Pck_up (ck',_) -> update_scope scoped ck' |
||
210 | | Pck_down (ck',_) -> update_scope scoped ck' |
||
211 | | Pck_phase (ck',_) -> update_scope scoped ck' |
||
212 | | Pck_const (_,_) | Cunivar _ -> () |
||
213 | | Clink ck' -> |
||
214 | update_scope scoped ck' |
||
215 | | Ccarrying (cr,ck') -> |
||
216 | update_scope_carrier scoped cr; update_scope scoped ck' |
||
217 | end |
||
218 | |||
219 | (* Unifies two static pclocks. *) |
||
220 | let unify_static_pck ck1 ck2 = |
||
221 | if (period ck1 <> period ck2) || (phase ck1 <> phase ck2) then |
||
222 | raise (Unify (ck1,ck2)) |
||
223 | |||
224 | (* Unifies two clock carriers *) |
||
225 | let unify_carrier cr1 cr2 = |
||
226 | let cr1 = carrier_repr cr1 in |
||
227 | let cr2 = carrier_repr cr2 in |
||
228 | 8a183477 | xthirioux | if cr1==cr2 then () |
229 | 22fe1c93 | ploc | else |
230 | match cr1.carrier_desc, cr2.carrier_desc with |
||
231 | | Carry_const id1, Carry_const id2 -> |
||
232 | if id1 <> id2 then raise (Mismatch (cr1, cr2)) |
||
233 | | Carry_const _, Carry_name -> |
||
234 | begin |
||
235 | cr2.carrier_desc <- Carry_link cr1; |
||
236 | update_scope_carrier cr2.carrier_scoped cr1 |
||
237 | end |
||
238 | | Carry_name, Carry_const _ -> |
||
239 | begin |
||
240 | cr1.carrier_desc <- Carry_link cr2; |
||
241 | update_scope_carrier cr1.carrier_scoped cr2 |
||
242 | end |
||
243 | | Carry_name, Carry_name -> |
||
244 | if cr1.carrier_id < cr2.carrier_id then |
||
245 | begin |
||
246 | cr2.carrier_desc <- Carry_link cr1; |
||
247 | update_scope_carrier cr2.carrier_scoped cr1 |
||
248 | end |
||
249 | else |
||
250 | begin |
||
251 | cr1.carrier_desc <- Carry_link cr2; |
||
252 | update_scope_carrier cr1.carrier_scoped cr2 |
||
253 | end |
||
254 | 8f1c7e91 | xthirioux | | _,_ -> assert false |
255 | |||
256 | (* Semi-unifies two clock carriers *) |
||
257 | let semi_unify_carrier cr1 cr2 = |
||
258 | let cr1 = carrier_repr cr1 in |
||
259 | let cr2 = carrier_repr cr2 in |
||
260 | 8a183477 | xthirioux | if cr1==cr2 then () |
261 | 8f1c7e91 | xthirioux | else |
262 | match cr1.carrier_desc, cr2.carrier_desc with |
||
263 | | Carry_const id1, Carry_const id2 -> |
||
264 | if id1 <> id2 then raise (Mismatch (cr1, cr2)) |
||
265 | | Carry_const _, Carry_name -> |
||
266 | begin |
||
267 | cr2.carrier_desc <- Carry_link cr1; |
||
268 | update_scope_carrier cr2.carrier_scoped cr1 |
||
269 | end |
||
270 | | Carry_name, Carry_const _ -> raise (Mismatch (cr1, cr2)) |
||
271 | | Carry_name, Carry_name -> |
||
272 | if cr1.carrier_id < cr2.carrier_id then |
||
273 | begin |
||
274 | cr2.carrier_desc <- Carry_link cr1; |
||
275 | update_scope_carrier cr2.carrier_scoped cr1 |
||
276 | end |
||
277 | else |
||
278 | begin |
||
279 | cr1.carrier_desc <- Carry_link cr2; |
||
280 | update_scope_carrier cr1.carrier_scoped cr2 |
||
281 | end |
||
282 | | _,_ -> assert false |
||
283 | 22fe1c93 | ploc | |
284 | (** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify |
||
285 | (ck1,ck2)] if the clocks are not unifiable.*) |
||
286 | let rec unify ck1 ck2 = |
||
287 | let ck1 = repr ck1 in |
||
288 | let ck2 = repr ck2 in |
||
289 | 8a183477 | xthirioux | if ck1==ck2 then |
290 | 22fe1c93 | ploc | () |
291 | else |
||
292 | let left_const = is_concrete_pck ck1 in |
||
293 | let right_const = is_concrete_pck ck2 in |
||
294 | if left_const && right_const then |
||
295 | unify_static_pck ck1 ck2 |
||
296 | else |
||
297 | match ck1.cdesc,ck2.cdesc with |
||
298 | | Cvar cset1,Cvar cset2-> |
||
299 | if ck1.cid < ck2.cid then |
||
300 | begin |
||
301 | ck2.cdesc <- Clink (simplify ck1); |
||
302 | update_scope ck2.cscoped ck1; |
||
303 | subsume ck1 cset2 |
||
304 | end |
||
305 | else |
||
306 | begin |
||
307 | ck1.cdesc <- Clink (simplify ck2); |
||
308 | update_scope ck1.cscoped ck2; |
||
309 | subsume ck2 cset1 |
||
310 | end |
||
311 | | Cvar cset, Pck_up (_,_) | Cvar cset, Pck_down (_,_) |
||
312 | | Cvar cset, Pck_phase (_,_) | Cvar cset, Pck_const (_,_) -> |
||
313 | if (occurs ck1 ck2) then |
||
314 | begin |
||
315 | if (simplify ck2 = ck1) then |
||
316 | ck2.cdesc <- Clink (simplify ck1) |
||
317 | else |
||
318 | raise (Unify (ck1,ck2)); |
||
319 | end |
||
320 | else |
||
321 | begin |
||
322 | ck1.cdesc <- Clink (simplify ck2); |
||
323 | subsume ck2 cset |
||
324 | end |
||
325 | | Pck_up (_,_), Cvar cset | Pck_down (_,_), Cvar cset |
||
326 | | Pck_phase (_,_), Cvar cset | Pck_const (_,_), Cvar cset -> |
||
327 | if (occurs ck2 ck1) then |
||
328 | begin |
||
329 | if ((simplify ck1) = ck2) then |
||
330 | ck1.cdesc <- Clink (simplify ck2) |
||
331 | else |
||
332 | raise (Unify (ck1,ck2)); |
||
333 | end |
||
334 | else |
||
335 | begin |
||
336 | ck2.cdesc <- Clink (simplify ck1); |
||
337 | subsume ck1 cset |
||
338 | end |
||
339 | | (Cvar cset,_) when (not (occurs ck1 ck2)) -> |
||
340 | subsume ck2 cset; |
||
341 | update_scope ck1.cscoped ck2; |
||
342 | ck1.cdesc <- Clink (simplify ck2) |
||
343 | | (_, (Cvar cset)) when (not (occurs ck2 ck1)) -> |
||
344 | subsume ck1 cset; |
||
345 | update_scope ck2.cscoped ck1; |
||
346 | ck2.cdesc <- Clink (simplify ck1) |
||
347 | | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') -> |
||
348 | unify_carrier cr1 cr2; |
||
349 | unify ck1' ck2' |
||
350 | | Ccarrying (_,_),_ | _,Ccarrying (_,_) -> |
||
351 | raise (Unify (ck1,ck2)) |
||
352 | | Carrow (c1,c2), Carrow (c1',c2') -> |
||
353 | unify c1 c1'; unify c2 c2' |
||
354 | | Ctuple ckl1, Ctuple ckl2 -> |
||
355 | if (List.length ckl1) <> (List.length ckl2) then |
||
356 | raise (Unify (ck1,ck2)); |
||
357 | List.iter2 unify ckl1 ckl2 |
||
358 | | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 -> |
||
359 | unify_carrier c1 c2; |
||
360 | unify ck' ck'' |
||
361 | | Pck_const (i,r), Pck_const (i',r') -> |
||
362 | if i<>i' || r <> r' then |
||
363 | raise (Unify (ck1,ck2)) |
||
364 | | (_, Pck_up (pck2',k)) when (not right_const) -> |
||
365 | let ck1' = simplify (new_ck (Pck_down (ck1,k)) true) in |
||
366 | unify ck1' pck2' |
||
367 | | (_,Pck_down (pck2',k)) when (not right_const) -> |
||
368 | subsume ck1 (CSet_pck (k,(0,1))); |
||
369 | let ck1' = simplify (new_ck (Pck_up (ck1,k)) true) in |
||
370 | unify ck1' pck2' |
||
371 | | (_,Pck_phase (pck2',(a,b))) when (not right_const) -> |
||
372 | subsume ck1 (CSet_pck (b,(a,b))); |
||
373 | let ck1' = simplify (new_ck (Pck_phase (ck1,(-a,b))) true) in |
||
374 | unify ck1' pck2' |
||
375 | | Pck_up (pck1',k),_ -> |
||
376 | let ck2' = simplify (new_ck (Pck_down (ck2,k)) true) in |
||
377 | unify pck1' ck2' |
||
378 | | Pck_down (pck1',k),_ -> |
||
379 | subsume ck2 (CSet_pck (k,(0,1))); |
||
380 | let ck2' = simplify (new_ck (Pck_up (ck2,k)) true) in |
||
381 | unify pck1' ck2' |
||
382 | | Pck_phase (pck1',(a,b)),_ -> |
||
383 | subsume ck2 (CSet_pck (b,(a,b))); |
||
384 | let ck2' = simplify (new_ck (Pck_phase (ck2,(-a,b))) true) in |
||
385 | unify pck1' ck2' |
||
386 | 8f1c7e91 | xthirioux | | Cunivar _, _ | _, Cunivar _ -> () |
387 | | _,_ -> raise (Unify (ck1,ck2)) |
||
388 | |||
389 | (** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify |
||
390 | (ck1,ck2)] if the clocks are not semi-unifiable.*) |
||
391 | let rec semi_unify ck1 ck2 = |
||
392 | let ck1 = repr ck1 in |
||
393 | let ck2 = repr ck2 in |
||
394 | 8a183477 | xthirioux | if ck1==ck2 then |
395 | 8f1c7e91 | xthirioux | () |
396 | else |
||
397 | match ck1.cdesc,ck2.cdesc with |
||
398 | | Cvar cset1,Cvar cset2-> |
||
399 | if ck1.cid < ck2.cid then |
||
400 | begin |
||
401 | ck2.cdesc <- Clink (simplify ck1); |
||
402 | update_scope ck2.cscoped ck1 |
||
403 | end |
||
404 | else |
||
405 | begin |
||
406 | ck1.cdesc <- Clink (simplify ck2); |
||
407 | update_scope ck1.cscoped ck2 |
||
408 | end |
||
409 | | (Cvar cset,_) -> raise (Unify (ck1,ck2)) |
||
410 | | (_, (Cvar cset)) when (not (occurs ck2 ck1)) -> |
||
411 | update_scope ck2.cscoped ck1; |
||
412 | ck2.cdesc <- Clink (simplify ck1) |
||
413 | | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') -> |
||
414 | semi_unify_carrier cr1 cr2; |
||
415 | semi_unify ck1' ck2' |
||
416 | | Ccarrying (_,_),_ | _,Ccarrying (_,_) -> |
||
417 | raise (Unify (ck1,ck2)) |
||
418 | | Carrow (c1,c2), Carrow (c1',c2') -> |
||
419 | begin |
||
420 | semi_unify c1 c1'; |
||
421 | semi_unify c2 c2' |
||
422 | end |
||
423 | | Ctuple ckl1, Ctuple ckl2 -> |
||
424 | if (List.length ckl1) <> (List.length ckl2) then |
||
425 | raise (Unify (ck1,ck2)); |
||
426 | List.iter2 semi_unify ckl1 ckl2 |
||
427 | | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 -> |
||
428 | semi_unify_carrier c1 c2; |
||
429 | semi_unify ck' ck'' |
||
430 | 22fe1c93 | ploc | | Cunivar _, _ | _, Cunivar _ -> () |
431 | | _,_ -> raise (Unify (ck1,ck2)) |
||
432 | |||
433 | (* Returns the value corresponding to a pclock (integer) factor |
||
434 | expression. Expects a constant expression (checked by typing). *) |
||
435 | let int_factor_of_expr e = |
||
436 | match e.expr_desc with |
||
437 | | Expr_const |
||
438 | (Const_int i) -> i |
||
439 | | _ -> failwith "Internal error: int_factor_of_expr" |
||
440 | |||
441 | (* Unifies all the clock variables in the clock type of a tuple |
||
442 | expression, so that the clock type only uses at most one clock variable *) |
||
443 | let unify_tuple_clock ref_ck_opt ck = |
||
444 | let ck_var = ref ref_ck_opt in |
||
445 | let rec aux ck = |
||
446 | match (repr ck).cdesc with |
||
447 | | Con _ |
||
448 | | Cvar _ -> |
||
449 | begin |
||
450 | match !ck_var with |
||
451 | | None -> |
||
452 | ck_var:=Some ck |
||
453 | | Some v -> |
||
454 | (* may fail *) |
||
455 | unify v ck |
||
456 | end |
||
457 | | Ctuple cl -> |
||
458 | List.iter aux cl |
||
459 | | Carrow _ -> assert false (* should not occur *) |
||
460 | | Ccarrying (_, ck1) -> |
||
461 | aux ck1 |
||
462 | | _ -> () |
||
463 | in |
||
464 | aux ck |
||
465 | |||
466 | (* Unifies all the clock variables in the clock type of an imported |
||
467 | node, so that the clock type only uses at most one base clock variable, |
||
468 | that is, the activation clock of the node *) |
||
469 | let unify_imported_clock ref_ck_opt ck = |
||
470 | let ck_var = ref ref_ck_opt in |
||
471 | let rec aux ck = |
||
472 | match (repr ck).cdesc with |
||
473 | | Cvar _ -> |
||
474 | begin |
||
475 | match !ck_var with |
||
476 | | None -> |
||
477 | ck_var:=Some ck |
||
478 | | Some v -> |
||
479 | (* cannot fail *) |
||
480 | unify v ck |
||
481 | end |
||
482 | | Ctuple cl -> |
||
483 | List.iter aux cl |
||
484 | | Carrow (ck1,ck2) -> |
||
485 | aux ck1; aux ck2 |
||
486 | | Ccarrying (_, ck1) -> |
||
487 | aux ck1 |
||
488 | | Con (ck1, _, _) -> aux ck1 |
||
489 | | _ -> () |
||
490 | in |
||
491 | aux ck |
||
492 | |||
493 | (** [clock_uncarry ck] drops the possible carrier name from clock [ck] *) |
||
494 | let clock_uncarry ck = |
||
495 | let ck = repr ck in |
||
496 | match ck.cdesc with |
||
497 | | Ccarrying (_, ck') -> ck' |
||
498 | | _ -> ck |
||
499 | |||
500 | let try_unify ck1 ck2 loc = |
||
501 | try |
||
502 | unify ck1 ck2 |
||
503 | with |
||
504 | | Unify (ck1',ck2') -> |
||
505 | raise (Error (loc, Clock_clash (ck1',ck2'))) |
||
506 | | Subsume (ck,cset) -> |
||
507 | raise (Error (loc, Clock_set_mismatch (ck,cset))) |
||
508 | | Mismatch (cr1,cr2) -> |
||
509 | raise (Error (loc, Carrier_mismatch (cr1,cr2))) |
||
510 | |||
511 | 8f1c7e91 | xthirioux | let try_semi_unify ck1 ck2 loc = |
512 | try |
||
513 | semi_unify ck1 ck2 |
||
514 | with |
||
515 | | Unify (ck1',ck2') -> |
||
516 | raise (Error (loc, Clock_clash (ck1',ck2'))) |
||
517 | | Subsume (ck,cset) -> |
||
518 | raise (Error (loc, Clock_set_mismatch (ck,cset))) |
||
519 | | Mismatch (cr1,cr2) -> |
||
520 | raise (Error (loc, Carrier_mismatch (cr1,cr2))) |
||
521 | |||
522 | 52cfee34 | xthirioux | (* ck1 is a subtype of ck2 *) |
523 | let rec sub_unify sub ck1 ck2 = |
||
524 | 22fe1c93 | ploc | match (repr ck1).cdesc, (repr ck2).cdesc with |
525 | 52cfee34 | xthirioux | | Ctuple cl1 , Ctuple cl2 -> |
526 | if List.length cl1 <> List.length cl2 |
||
527 | then raise (Unify (ck1, ck2)) |
||
528 | else List.iter2 (sub_unify sub) cl1 cl2 |
||
529 | | Ctuple [c1] , _ -> sub_unify sub c1 ck2 |
||
530 | | _ , Ctuple [c2] -> sub_unify sub ck1 c2 |
||
531 | | Con (c1, cr1, t1) , Con (c2, cr2, t2) when t1=t2 -> |
||
532 | begin |
||
533 | unify_carrier cr1 cr2; |
||
534 | sub_unify sub c1 c2 |
||
535 | end |
||
536 | | Ccarrying (cr1, c1), Ccarrying (cr2, c2)-> |
||
537 | begin |
||
538 | unify_carrier cr1 cr2; |
||
539 | sub_unify sub c1 c2 |
||
540 | end |
||
541 | | Ccarrying (_, c1) , _ when sub -> sub_unify sub c1 ck2 |
||
542 | | _ -> unify ck1 ck2 |
||
543 | |||
544 | let try_sub_unify sub ck1 ck2 loc = |
||
545 | try |
||
546 | sub_unify sub ck1 ck2 |
||
547 | with |
||
548 | | Unify (ck1',ck2') -> |
||
549 | raise (Error (loc, Clock_clash (ck1',ck2'))) |
||
550 | | Subsume (ck,cset) -> |
||
551 | raise (Error (loc, Clock_set_mismatch (ck,cset))) |
||
552 | | Mismatch (cr1,cr2) -> |
||
553 | raise (Error (loc, Carrier_mismatch (cr1,cr2))) |
||
554 | 22fe1c93 | ploc | |
555 | (* Clocks a list of arguments of Lustre builtin operators: |
||
556 | - type each expression, remove carriers of clocks as |
||
557 | carriers may only denote variables, not arbitrary expr. |
||
558 | - try to unify these clocks altogether |
||
559 | *) |
||
560 | let rec clock_standard_args env expr_list = |
||
561 | let ck_list = List.map (fun e -> clock_uncarry (clock_expr env e)) expr_list in |
||
562 | let ck_res = new_var true in |
||
563 | List.iter2 (fun e ck -> try_unify ck ck_res e.expr_loc) expr_list ck_list; |
||
564 | ck_res |
||
565 | |||
566 | (* emulates a subtyping relation between clocks c and (cr : c), |
||
567 | used during node application only *) |
||
568 | 52cfee34 | xthirioux | and clock_subtyping_arg env ?(sub=true) real_arg formal_clock = |
569 | 22fe1c93 | ploc | let loc = real_arg.expr_loc in |
570 | let real_clock = clock_expr env real_arg in |
||
571 | 52cfee34 | xthirioux | try_sub_unify sub real_clock formal_clock loc |
572 | 22fe1c93 | ploc | |
573 | (* computes clocks for node application *) |
||
574 | and clock_appl env f args clock_reset loc = |
||
575 | b616fe7a | xthirioux | let args = expr_list_of_expr args in |
576 | if Basic_library.is_internal_fun f && List.exists is_tuple_expr args |
||
577 | then |
||
578 | let args = Utils.transpose_list (List.map expr_list_of_expr args) in |
||
579 | Clocks.clock_of_clock_list (List.map (fun args -> clock_call env f args clock_reset loc) args) |
||
580 | else |
||
581 | clock_call env f args clock_reset loc |
||
582 | |||
583 | and clock_call env f args clock_reset loc = |
||
584 | 22fe1c93 | ploc | let cfun = clock_ident false env f loc in |
585 | let cins, couts = split_arrow cfun in |
||
586 | let cins = clock_list_of_clock cins in |
||
587 | List.iter2 (clock_subtyping_arg env) args cins; |
||
588 | unify_imported_clock (Some clock_reset) cfun; |
||
589 | couts |
||
590 | |||
591 | and clock_ident nocarrier env id loc = |
||
592 | clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc) |
||
593 | |||
594 | and clock_carrier env c loc ce = |
||
595 | let expr_c = expr_of_ident c loc in |
||
596 | let ck = clock_expr ~nocarrier:false env expr_c in |
||
597 | let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in |
||
598 | let ckcarry = new_ck (Ccarrying (cr,ce)) ck.cscoped in |
||
599 | try_unify ck ckcarry expr_c.expr_loc; |
||
600 | cr |
||
601 | |||
602 | (** [clock_expr env expr] performs the clock calculus for expression [expr] in |
||
603 | environment [env] *) |
||
604 | and clock_expr ?(nocarrier=true) env expr = |
||
605 | let resulting_ck = |
||
606 | match expr.expr_desc with |
||
607 | | Expr_const cst -> |
||
608 | let ck = new_var true in |
||
609 | expr.expr_clock <- ck; |
||
610 | ck |
||
611 | | Expr_ident v -> |
||
612 | let ckv = |
||
613 | try |
||
614 | Env.lookup_value env v |
||
615 | with Not_found -> |
||
616 | failwith ("Internal error, variable \""^v^"\" not found") |
||
617 | in |
||
618 | 7291cb80 | xthirioux | let ck = instantiate (ref []) (ref []) ckv in |
619 | 22fe1c93 | ploc | expr.expr_clock <- ck; |
620 | ck |
||
621 | | Expr_array elist -> |
||
622 | let ck = clock_standard_args env elist in |
||
623 | expr.expr_clock <- ck; |
||
624 | ck |
||
625 | | Expr_access (e1, d) -> |
||
626 | (* dimension, being a static value, doesn't need to be clocked *) |
||
627 | let ck = clock_standard_args env [e1] in |
||
628 | expr.expr_clock <- ck; |
||
629 | ck |
||
630 | | Expr_power (e1, d) -> |
||
631 | (* dimension, being a static value, doesn't need to be clocked *) |
||
632 | let ck = clock_standard_args env [e1] in |
||
633 | expr.expr_clock <- ck; |
||
634 | ck |
||
635 | | Expr_tuple elist -> |
||
636 | let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in |
||
637 | expr.expr_clock <- ck; |
||
638 | ck |
||
639 | | Expr_ite (c, t, e) -> |
||
640 | let ck_c = clock_standard_args env [c] in |
||
641 | let ck = clock_standard_args env [t; e] in |
||
642 | (* Here, the branches may exhibit a tuple clock, not the condition *) |
||
643 | unify_tuple_clock (Some ck_c) ck; |
||
644 | expr.expr_clock <- ck; |
||
645 | ck |
||
646 | | Expr_appl (id, args, r) -> |
||
647 | (try |
||
648 | (* for a modular compilation scheme, all inputs/outputs must share the same clock ! |
||
649 | this is also the reset clock ! |
||
650 | *) |
||
651 | let cr = |
||
652 | match r with |
||
653 | | None -> new_var true |
||
654 | | Some (x, _) -> let loc_r = loc_of_cond expr.expr_loc x in |
||
655 | let expr_r = expr_of_ident x loc_r in |
||
656 | clock_expr env expr_r in |
||
657 | let couts = clock_appl env id args cr expr.expr_loc in |
||
658 | expr.expr_clock <- couts; |
||
659 | couts |
||
660 | with exn -> ( |
||
661 | Format.eprintf "Current expr: %a@." Printers.pp_expr expr; |
||
662 | raise exn |
||
663 | )) |
||
664 | | Expr_fby (e1,e2) |
||
665 | | Expr_arrow (e1,e2) -> |
||
666 | let ck = clock_standard_args env [e1; e2] in |
||
667 | expr.expr_clock <- ck; |
||
668 | ck |
||
669 | | Expr_pre e -> (* todo : deal with phases as in tail ? *) |
||
670 | let ck = clock_standard_args env [e] in |
||
671 | expr.expr_clock <- ck; |
||
672 | ck |
||
673 | | Expr_when (e,c,l) -> |
||
674 | let ce = clock_standard_args env [e] in |
||
675 | let c_loc = loc_of_cond expr.expr_loc c in |
||
676 | let cr = clock_carrier env c c_loc ce in |
||
677 | let ck = new_ck (Con (ce,cr,l)) true in |
||
678 | let cr' = new_carrier (Carry_const c) ck.cscoped in |
||
679 | let ck' = new_ck (Con (ce,cr',l)) true in |
||
680 | expr.expr_clock <- ck'; |
||
681 | ck |
||
682 | | Expr_merge (c,hl) -> |
||
683 | let cvar = new_var true in |
||
684 | let cr = clock_carrier env c expr.expr_loc cvar in |
||
685 | List.iter (fun (t, h) -> clock_subtyping_arg env h (new_ck (Con (cvar,cr,t)) true)) hl; |
||
686 | expr.expr_clock <- cvar; |
||
687 | cvar |
||
688 | in |
||
689 | b616fe7a | xthirioux | Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck); |
690 | 22fe1c93 | ploc | resulting_ck |
691 | |||
692 | let clock_of_vlist vars = |
||
693 | let ckl = List.map (fun v -> v.var_clock) vars in |
||
694 | clock_of_clock_list ckl |
||
695 | |||
696 | (** [clock_eq env eq] performs the clock-calculus for equation [eq] in |
||
697 | environment [env] *) |
||
698 | let clock_eq env eq = |
||
699 | let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in |
||
700 | let ck_rhs = clock_expr env eq.eq_rhs in |
||
701 | clock_subtyping_arg env expr_lhs ck_rhs |
||
702 | |||
703 | |||
704 | (* [clock_coreclock cck] returns the clock_expr corresponding to clock |
||
705 | declaration [cck] *) |
||
706 | let clock_coreclock env cck id loc scoped = |
||
707 | match cck.ck_dec_desc with |
||
708 | | Ckdec_any -> new_var scoped |
||
709 | | Ckdec_pclock (n,(a,b)) -> |
||
710 | let ck = new_ck (Pck_const (n,(a,b))) scoped in |
||
711 | if n mod b <> 0 then raise (Error (loc,Invalid_const ck)); |
||
712 | ck |
||
713 | | Ckdec_bool cl -> |
||
714 | let temp_env = Env.add_value env id (new_var true) in |
||
715 | (* We just want the id to be present in the environment *) |
||
716 | let dummy_id_expr = expr_of_ident id loc in |
||
717 | let when_expr = |
||
718 | List.fold_left |
||
719 | (fun expr (x,l) -> |
||
720 | {expr_tag = new_tag (); |
||
721 | expr_desc = Expr_when (expr,x,l); |
||
722 | expr_type = Types.new_var (); |
||
723 | expr_clock = new_var scoped; |
||
724 | expr_delay = Delay.new_var (); |
||
725 | expr_loc = loc; |
||
726 | expr_annot = None}) |
||
727 | dummy_id_expr cl |
||
728 | in |
||
729 | clock_expr temp_env when_expr |
||
730 | |||
731 | (* Clocks a variable declaration *) |
||
732 | let clock_var_decl scoped env vdecl = |
||
733 | let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in |
||
734 | 89b9e25c | xthirioux | let ck = |
735 | (* WTF ???? |
||
736 | 22fe1c93 | ploc | if vdecl.var_dec_const |
737 | then |
||
738 | (try_generalize ck vdecl.var_loc; ck) |
||
739 | else |
||
740 | 89b9e25c | xthirioux | *) |
741 | 6afa892a | xthirioux | if Types.get_clock_base_type vdecl.var_type <> None |
742 | 89b9e25c | xthirioux | then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped |
743 | else ck in |
||
744 | 22fe1c93 | ploc | vdecl.var_clock <- ck; |
745 | Env.add_value env vdecl.var_id ck |
||
746 | |||
747 | (* Clocks a variable declaration list *) |
||
748 | let clock_var_decl_list env scoped l = |
||
749 | List.fold_left (clock_var_decl scoped) env l |
||
750 | |||
751 | (** [clock_node env nd] performs the clock-calculus for node [nd] in |
||
752 | 89b9e25c | xthirioux | environment [env]. |
753 | Generalization of clocks wrt scopes follows this rule: |
||
754 | - generalize inputs (unscoped). |
||
755 | - generalize outputs. As they are scoped, only clocks coming from inputs |
||
756 | are allowed to be generalized. |
||
757 | - generalize locals. As outputs don't depend on them (checked the step before), |
||
758 | they can be generalized. |
||
759 | *) |
||
760 | 22fe1c93 | ploc | let clock_node env loc nd = |
761 | (* let is_main = nd.node_id = !Options.main_node in *) |
||
762 | let new_env = clock_var_decl_list env false nd.node_inputs in |
||
763 | let new_env = clock_var_decl_list new_env true nd.node_outputs in |
||
764 | d4807c3d | xthirioux | let new_env = clock_var_decl_list new_env true nd.node_locals in |
765 | 22fe1c93 | ploc | List.iter (clock_eq new_env) nd.node_eqs; |
766 | let ck_ins = clock_of_vlist nd.node_inputs in |
||
767 | let ck_outs = clock_of_vlist nd.node_outputs in |
||
768 | let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in |
||
769 | unify_imported_clock None ck_node; |
||
770 | 52cfee34 | xthirioux | Log.report ~level:3 (fun fmt -> print_ck fmt ck_node); |
771 | 89b9e25c | xthirioux | (* Local variables may contain first-order carrier variables that should be generalized. |
772 | That's not the case for types. *) |
||
773 | 6afa892a | xthirioux | try_generalize ck_node loc; |
774 | (* |
||
775 | 89b9e25c | xthirioux | List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs; |
776 | 6afa892a | xthirioux | List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*) |
777 | d4807c3d | xthirioux | (*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*) |
778 | 22fe1c93 | ploc | (* TODO : Xavier pourquoi ai je cette erreur ? *) |
779 | (* if (is_main && is_polymorphic ck_node) then |
||
780 | raise (Error (loc,(Cannot_be_polymorphic ck_node))); |
||
781 | *) |
||
782 | 52cfee34 | xthirioux | Log.report ~level:3 (fun fmt -> print_ck fmt ck_node); |
783 | 22fe1c93 | ploc | nd.node_clock <- ck_node; |
784 | Env.add_value env nd.node_id ck_node |
||
785 | |||
786 | |||
787 | let check_imported_pclocks loc ck_node = |
||
788 | let pck = ref None in |
||
789 | let rec aux ck = |
||
790 | match ck.cdesc with |
||
791 | | Carrow (ck1,ck2) -> aux ck1; aux ck2 |
||
792 | | Ctuple cl -> List.iter aux cl |
||
793 | | Con (ck',_,_) -> aux ck' |
||
794 | | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) -> |
||
795 | raise (Error (loc, (Invalid_imported_clock ck_node))) |
||
796 | | Pck_const (n,p) -> |
||
797 | begin |
||
798 | match !pck with |
||
799 | | None -> pck := Some (n,p) |
||
800 | | Some (n',p') -> |
||
801 | if (n,p) <> (n',p') then |
||
802 | raise (Error (loc, (Invalid_imported_clock ck_node))) |
||
803 | end |
||
804 | | Clink ck' -> aux ck' |
||
805 | | Ccarrying (_,ck') -> aux ck' |
||
806 | | Cvar _ | Cunivar _ -> |
||
807 | match !pck with |
||
808 | | None -> () |
||
809 | | Some (_,_) -> |
||
810 | raise (Error (loc, (Invalid_imported_clock ck_node))) |
||
811 | in |
||
812 | aux ck_node |
||
813 | |||
814 | let clock_imported_node env loc nd = |
||
815 | let new_env = clock_var_decl_list env false nd.nodei_inputs in |
||
816 | ignore(clock_var_decl_list new_env false nd.nodei_outputs); |
||
817 | let ck_ins = clock_of_vlist nd.nodei_inputs in |
||
818 | let ck_outs = clock_of_vlist nd.nodei_outputs in |
||
819 | let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in |
||
820 | unify_imported_clock None ck_node; |
||
821 | check_imported_pclocks loc ck_node; |
||
822 | try_generalize ck_node loc; |
||
823 | nd.nodei_clock <- ck_node; |
||
824 | Env.add_value env nd.nodei_id ck_node |
||
825 | |||
826 | let clock_top_consts env clist = |
||
827 | List.fold_left (fun env cdecl -> |
||
828 | let ck = new_var false in |
||
829 | try_generalize ck cdecl.const_loc; |
||
830 | Env.add_value env cdecl.const_id ck) env clist |
||
831 | |||
832 | let clock_top_decl env decl = |
||
833 | match decl.top_decl_desc with |
||
834 | | Node nd -> |
||
835 | clock_node env decl.top_decl_loc nd |
||
836 | | ImportedNode nd -> |
||
837 | clock_imported_node env decl.top_decl_loc nd |
||
838 | | Consts clist -> |
||
839 | clock_top_consts env clist |
||
840 | 5c1184ad | ploc | | Open _ -> |
841 | 22fe1c93 | ploc | env |
842 | |||
843 | let clock_prog env decls = |
||
844 | 5c1184ad | ploc | List.fold_left (fun e decl -> clock_top_decl e decl) env decls |
845 | 22fe1c93 | ploc | |
846 | 8f1c7e91 | xthirioux | (* Once the Lustre program is fully clocked, |
847 | we must get back to the original description of clocks, |
||
848 | with constant parameters, instead of unifiable internal variables. *) |
||
849 | |||
850 | (* The following functions aims at 'unevaluating' carriers occuring in clock expressions, |
||
851 | i.e. replacing unifiable second_order variables with the original carrier names. |
||
852 | Once restored in this formulation, clocks may be meaningfully printed. |
||
853 | *) |
||
854 | let uneval_vdecl_generics vdecl = |
||
855 | 89b9e25c | xthirioux | (*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*) |
856 | 6afa892a | xthirioux | if Types.get_clock_base_type vdecl.var_type <> None |
857 | 8f1c7e91 | xthirioux | then |
858 | match get_carrier_name vdecl.var_clock with |
||
859 | | None -> (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false) |
||
860 | | Some cr -> Clocks.uneval vdecl.var_id cr |
||
861 | |||
862 | let uneval_node_generics vdecls = |
||
863 | List.iter uneval_vdecl_generics vdecls |
||
864 | |||
865 | let uneval_top_generics decl = |
||
866 | match decl.top_decl_desc with |
||
867 | | Node nd -> |
||
868 | 89b9e25c | xthirioux | (* A node could contain first-order carrier variable in local vars. This is not the case for types. *) |
869 | uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs) |
||
870 | 8f1c7e91 | xthirioux | | ImportedNode nd -> |
871 | uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) |
||
872 | | Consts clist -> () |
||
873 | | Open _ -> () |
||
874 | |||
875 | let uneval_prog_generics prog = |
||
876 | List.iter uneval_top_generics prog |
||
877 | |||
878 | 7291cb80 | xthirioux | let check_env_compat header declared computed = |
879 | 8f1c7e91 | xthirioux | uneval_prog_generics header; |
880 | 5c1184ad | ploc | Env.iter declared (fun k decl_clock_k -> |
881 | 7291cb80 | xthirioux | let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in |
882 | 8f1c7e91 | xthirioux | try_semi_unify decl_clock_k computed_c Location.dummy_loc |
883 | 5c1184ad | ploc | ) |
884 | 22fe1c93 | ploc | (* Local Variables: *) |
885 | (* compile-command:"make -C .." *) |
||
886 | (* End: *) |