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