## lustrec / src / clock_calculus.ml @ b616fe7a

History | View | Annotate | Download (31.5 KB)

1 |
(* ---------------------------------------------------------------------------- |
---|---|

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 |
let instantiate_carrier cr inst_cr_vars = |

104 |
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 |
let rec instantiate inst_ck_vars inst_cr_vars ck = |

123 |
match ck.cdesc with |

124 |
| Carrow (ck1,ck2) -> |

125 |
{ck with cdesc = |

126 |
Carrow ((instantiate inst_ck_vars inst_cr_vars ck1), |

127 |
(instantiate inst_ck_vars inst_cr_vars ck2))} |

128 |
| Ctuple cklist -> |

129 |
{ck with cdesc = Ctuple |

130 |
(List.map (instantiate inst_ck_vars inst_cr_vars) cklist)} |

131 |
| Con (ck',c,l) -> |

132 |
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 |
| Cvar _ | Pck_const (_,_) -> ck |

135 |
| Pck_up (ck',k) -> |

136 |
{ck with cdesc = Pck_up ((instantiate inst_ck_vars inst_cr_vars ck'),k)} |

137 |
| Pck_down (ck',k) -> |

138 |
{ck with cdesc = Pck_down ((instantiate inst_ck_vars inst_cr_vars ck'),k)} |

139 |
| Pck_phase (ck',q) -> |

140 |
{ck with cdesc = Pck_phase ((instantiate inst_ck_vars inst_cr_vars ck'),q)} |

141 |
| Clink ck' -> |

142 |
{ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')} |

143 |
| Ccarrying (cr,ck') -> |

144 |
let cr' = instantiate_carrier cr inst_cr_vars in |

145 |
{ck with cdesc = |

146 |
Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')} |

147 |
| 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 |
if cr1=cr2 then () |

229 |
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 |
| _,_ -> 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 |
if cr1=cr2 then () |

261 |
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 | |

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 |
if ck1=ck2 then |

290 |
() |

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 |
| 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 |
if ck1=ck2 then |

395 |
() |

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 |
| 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 |
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 |
(* ck1 is a subtype of ck2 *) |

523 |
let rec sub_unify sub ck1 ck2 = |

524 |
match (repr ck1).cdesc, (repr ck2).cdesc with |

525 |
| 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 | |

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 |
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock = |

569 |
let loc = real_arg.expr_loc in |

570 |
let real_clock = clock_expr env real_arg in |

571 |
try_sub_unify sub real_clock formal_clock loc |

572 | |

573 |
(* computes clocks for node application *) |

574 |
and clock_appl env f args clock_reset loc = |

575 |
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 |
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 |
let ck = instantiate (ref []) (ref []) ckv in |

619 |
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 |
| Expr_uclock (e,k) -> |

689 |
let pck = clock_expr env e in |

690 |
if not (can_be_pck pck) then |

691 |
raise (Error (e.expr_loc, Not_pck)); |

692 |
if k = 0 then |

693 |
raise (Error (expr.expr_loc, Factor_zero)); |

694 |
(try |

695 |
subsume pck (CSet_pck (k,(0,1))) |

696 |
with Subsume (ck,cset) -> |

697 |
raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (k,(0,1)))))); |

698 |
let ck = new_ck (Pck_up (pck,k)) true in |

699 |
expr.expr_clock <- ck; |

700 |
ck |

701 |
| Expr_dclock (e,k) -> |

702 |
let pck = clock_expr env e in |

703 |
if not (can_be_pck pck) then |

704 |
raise (Error (e.expr_loc, Not_pck)); |

705 |
if k = 0 then |

706 |
raise (Error (expr.expr_loc, Factor_zero)); |

707 |
(try |

708 |
subsume pck (CSet_pck (1,(0,1))) |

709 |
with Subsume (ck,cset) -> |

710 |
raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (1,(0,1)))))); |

711 |
let ck = new_ck (Pck_down (pck,k)) true in |

712 |
expr.expr_clock <- ck; |

713 |
ck |

714 |
| Expr_phclock (e,(a,b)) -> |

715 |
let pck = clock_expr env e in |

716 |
if not (can_be_pck pck) then |

717 |
raise (Error (e.expr_loc, Not_pck)); |

718 |
let (a,b) = simplify_rat (a,b) in |

719 |
(try |

720 |
subsume pck (CSet_pck (b,(0,1))) |

721 |
with Subsume (ck,cset) -> |

722 |
raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (b,(0,1)))))); |

723 |
let ck = new_ck (Pck_phase (pck,(a,b))) true in |

724 |
expr.expr_clock <- ck; |

725 |
ck |

726 |
in |

727 |
Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck); |

728 |
resulting_ck |

729 | |

730 |
let clock_of_vlist vars = |

731 |
let ckl = List.map (fun v -> v.var_clock) vars in |

732 |
clock_of_clock_list ckl |

733 | |

734 |
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in |

735 |
environment [env] *) |

736 |
let clock_eq env eq = |

737 |
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 |

738 |
let ck_rhs = clock_expr env eq.eq_rhs in |

739 |
clock_subtyping_arg env expr_lhs ck_rhs |

740 | |

741 | |

742 |
(* [clock_coreclock cck] returns the clock_expr corresponding to clock |

743 |
declaration [cck] *) |

744 |
let clock_coreclock env cck id loc scoped = |

745 |
match cck.ck_dec_desc with |

746 |
| Ckdec_any -> new_var scoped |

747 |
| Ckdec_pclock (n,(a,b)) -> |

748 |
let ck = new_ck (Pck_const (n,(a,b))) scoped in |

749 |
if n mod b <> 0 then raise (Error (loc,Invalid_const ck)); |

750 |
ck |

751 |
| Ckdec_bool cl -> |

752 |
let temp_env = Env.add_value env id (new_var true) in |

753 |
(* We just want the id to be present in the environment *) |

754 |
let dummy_id_expr = expr_of_ident id loc in |

755 |
let when_expr = |

756 |
List.fold_left |

757 |
(fun expr (x,l) -> |

758 |
{expr_tag = new_tag (); |

759 |
expr_desc = Expr_when (expr,x,l); |

760 |
expr_type = Types.new_var (); |

761 |
expr_clock = new_var scoped; |

762 |
expr_delay = Delay.new_var (); |

763 |
expr_loc = loc; |

764 |
expr_annot = None}) |

765 |
dummy_id_expr cl |

766 |
in |

767 |
clock_expr temp_env when_expr |

768 | |

769 |
(* Clocks a variable declaration *) |

770 |
let clock_var_decl scoped env vdecl = |

771 |
let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in |

772 |
let ck = |

773 |
(* WTF ???? |

774 |
if vdecl.var_dec_const |

775 |
then |

776 |
(try_generalize ck vdecl.var_loc; ck) |

777 |
else |

778 |
*) |

779 |
if Types.is_clock_type vdecl.var_type |

780 |
then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped |

781 |
else ck in |

782 |
vdecl.var_clock <- ck; |

783 |
Env.add_value env vdecl.var_id ck |

784 | |

785 |
(* Clocks a variable declaration list *) |

786 |
let clock_var_decl_list env scoped l = |

787 |
List.fold_left (clock_var_decl scoped) env l |

788 | |

789 |
(** [clock_node env nd] performs the clock-calculus for node [nd] in |

790 |
environment [env]. |

791 |
Generalization of clocks wrt scopes follows this rule: |

792 |
- generalize inputs (unscoped). |

793 |
- generalize outputs. As they are scoped, only clocks coming from inputs |

794 |
are allowed to be generalized. |

795 |
- generalize locals. As outputs don't depend on them (checked the step before), |

796 |
they can be generalized. |

797 |
*) |

798 |
let clock_node env loc nd = |

799 |
(* let is_main = nd.node_id = !Options.main_node in *) |

800 |
let new_env = clock_var_decl_list env false nd.node_inputs in |

801 |
let new_env = clock_var_decl_list new_env true nd.node_outputs in |

802 |
let new_env = clock_var_decl_list new_env true nd.node_locals in |

803 |
List.iter (clock_eq new_env) nd.node_eqs; |

804 |
let ck_ins = clock_of_vlist nd.node_inputs in |

805 |
let ck_outs = clock_of_vlist nd.node_outputs in |

806 |
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in |

807 |
unify_imported_clock None ck_node; |

808 |
Log.report ~level:3 (fun fmt -> print_ck fmt ck_node); |

809 |
(* Local variables may contain first-order carrier variables that should be generalized. |

810 |
That's not the case for types. *) |

811 |
List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs; |

812 |
List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs; |

813 |
(*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*) |

814 |
(* TODO : Xavier pourquoi ai je cette erreur ? *) |

815 |
(* if (is_main && is_polymorphic ck_node) then |

816 |
raise (Error (loc,(Cannot_be_polymorphic ck_node))); |

817 |
*) |

818 |
Log.report ~level:3 (fun fmt -> print_ck fmt ck_node); |

819 |
nd.node_clock <- ck_node; |

820 |
Env.add_value env nd.node_id ck_node |

821 | |

822 | |

823 |
let check_imported_pclocks loc ck_node = |

824 |
let pck = ref None in |

825 |
let rec aux ck = |

826 |
match ck.cdesc with |

827 |
| Carrow (ck1,ck2) -> aux ck1; aux ck2 |

828 |
| Ctuple cl -> List.iter aux cl |

829 |
| Con (ck',_,_) -> aux ck' |

830 |
| Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) -> |

831 |
raise (Error (loc, (Invalid_imported_clock ck_node))) |

832 |
| Pck_const (n,p) -> |

833 |
begin |

834 |
match !pck with |

835 |
| None -> pck := Some (n,p) |

836 |
| Some (n',p') -> |

837 |
if (n,p) <> (n',p') then |

838 |
raise (Error (loc, (Invalid_imported_clock ck_node))) |

839 |
end |

840 |
| Clink ck' -> aux ck' |

841 |
| Ccarrying (_,ck') -> aux ck' |

842 |
| Cvar _ | Cunivar _ -> |

843 |
match !pck with |

844 |
| None -> () |

845 |
| Some (_,_) -> |

846 |
raise (Error (loc, (Invalid_imported_clock ck_node))) |

847 |
in |

848 |
aux ck_node |

849 | |

850 |
let clock_imported_node env loc nd = |

851 |
let new_env = clock_var_decl_list env false nd.nodei_inputs in |

852 |
ignore(clock_var_decl_list new_env false nd.nodei_outputs); |

853 |
let ck_ins = clock_of_vlist nd.nodei_inputs in |

854 |
let ck_outs = clock_of_vlist nd.nodei_outputs in |

855 |
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in |

856 |
unify_imported_clock None ck_node; |

857 |
check_imported_pclocks loc ck_node; |

858 |
try_generalize ck_node loc; |

859 |
nd.nodei_clock <- ck_node; |

860 |
Env.add_value env nd.nodei_id ck_node |

861 | |

862 |
let clock_top_consts env clist = |

863 |
List.fold_left (fun env cdecl -> |

864 |
let ck = new_var false in |

865 |
try_generalize ck cdecl.const_loc; |

866 |
Env.add_value env cdecl.const_id ck) env clist |

867 | |

868 |
let clock_top_decl env decl = |

869 |
match decl.top_decl_desc with |

870 |
| Node nd -> |

871 |
clock_node env decl.top_decl_loc nd |

872 |
| ImportedNode nd -> |

873 |
clock_imported_node env decl.top_decl_loc nd |

874 |
| Consts clist -> |

875 |
clock_top_consts env clist |

876 |
| Open _ -> |

877 |
env |

878 | |

879 |
let clock_prog env decls = |

880 |
List.fold_left (fun e decl -> clock_top_decl e decl) env decls |

881 | |

882 |
(* Once the Lustre program is fully clocked, |

883 |
we must get back to the original description of clocks, |

884 |
with constant parameters, instead of unifiable internal variables. *) |

885 | |

886 |
(* The following functions aims at 'unevaluating' carriers occuring in clock expressions, |

887 |
i.e. replacing unifiable second_order variables with the original carrier names. |

888 |
Once restored in this formulation, clocks may be meaningfully printed. |

889 |
*) |

890 |
let uneval_vdecl_generics vdecl = |

891 |
(*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*) |

892 |
if Types.is_clock_type vdecl.var_type |

893 |
then |

894 |
match get_carrier_name vdecl.var_clock with |

895 |
| None -> (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false) |

896 |
| Some cr -> Clocks.uneval vdecl.var_id cr |

897 | |

898 |
let uneval_node_generics vdecls = |

899 |
List.iter uneval_vdecl_generics vdecls |

900 | |

901 |
let uneval_top_generics decl = |

902 |
match decl.top_decl_desc with |

903 |
| Node nd -> |

904 |
(* A node could contain first-order carrier variable in local vars. This is not the case for types. *) |

905 |
uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs) |

906 |
| ImportedNode nd -> |

907 |
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) |

908 |
| Consts clist -> () |

909 |
| Open _ -> () |

910 | |

911 |
let uneval_prog_generics prog = |

912 |
List.iter uneval_top_generics prog |

913 | |

914 |
let check_env_compat header declared computed = |

915 |
uneval_prog_generics header; |

916 |
Env.iter declared (fun k decl_clock_k -> |

917 |
let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in |

918 |
try_semi_unify decl_clock_k computed_c Location.dummy_loc |

919 |
) |

920 |
(* Local Variables: *) |

921 |
(* compile-command:"make -C .." *) |

922 |
(* End: *) |