## lustrec / src / clock_calculus.ml @ 7dedc5f0

History | View | Annotate | Download (30.8 KB)

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

2 |
(* *) |

3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |

4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *) |

5 |
(* *) |

6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |

7 |
(* under the terms of the GNU Lesser General Public License *) |

8 |
(* version 2.1. *) |

9 |
(* *) |

10 |
(* This file was originally from the Prelude compiler *) |

11 |
(* *) |

12 |
(********************************************************************) |

13 | |

14 | |

15 |
(** Main clock-calculus module. Based on type inference algorithms with |

16 |
destructive unification. Uses a bit of subtyping for periodic clocks. *) |

17 | |

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. *) |

21 |
open Utils |

22 |
open LustreSpec |

23 |
open Corelang |

24 |
open Clocks |

25 |
open Format |

26 | |

27 |
let loc_of_cond loc_containing id = |

28 |
let pos_start = |

29 |
{loc_containing.Location.loc_end with |

30 |
Lexing.pos_cnum=loc_containing.Location.loc_end.Lexing.pos_cnum-(String.length id)} |

31 |
in |

32 |
{Location.loc_start = pos_start; |

33 |
Location.loc_end = loc_containing.Location.loc_end} |

34 | |

35 |
(** [occurs cvar ck] returns true if the clock variable [cvar] occurs in |

36 |
clock [ck]. False otherwise. *) |

37 |
let rec occurs cvar ck = |

38 |
let ck = repr ck in |

39 |
match ck.cdesc with |

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

41 |
(occurs cvar ck1) || (occurs cvar ck2) |

42 |
| Ctuple ckl -> |

43 |
List.exists (occurs cvar) ckl |

44 |
| Con (ck',_,_) -> occurs cvar ck' |

45 |
| Pck_up (ck',_) -> occurs cvar ck' |

46 |
| Pck_down (ck',_) -> occurs cvar ck' |

47 |
| Pck_phase (ck',_) -> occurs cvar ck' |

48 |
| Cvar _ -> ck=cvar |

49 |
| Cunivar _ | Pck_const (_,_) -> false |

50 |
| Clink ck' -> occurs cvar ck' |

51 |
| Ccarrying (_,ck') -> occurs cvar ck' |

52 | |

53 |
(* Clocks generalization *) |

54 |
let rec generalize_carrier cr = |

55 |
match cr.carrier_desc with |

56 |
| Carry_const _ |

57 |
| Carry_name -> |

58 |
if cr.carrier_scoped then |

59 |
raise (Scope_carrier cr); |

60 |
cr.carrier_desc <- Carry_var |

61 |
| Carry_var -> () |

62 |
| Carry_link cr' -> generalize_carrier cr' |

63 | |

64 |
(** Promote monomorphic clock variables to polymorphic clock variables. *) |

65 |
(* Generalize by side-effects *) |

66 |
let rec generalize ck = |

67 |
match ck.cdesc with |

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

69 |
generalize ck1; generalize ck2 |

70 |
| Ctuple clist -> |

71 |
List.iter generalize clist |

72 |
| Con (ck',cr,_) -> generalize ck'; generalize_carrier cr |

73 |
| Cvar cset -> |

74 |
if ck.cscoped then |

75 |
raise (Scope_clock ck); |

76 |
ck.cdesc <- Cunivar cset |

77 |
| Pck_up (ck',_) -> generalize ck' |

78 |
| Pck_down (ck',_) -> generalize ck' |

79 |
| Pck_phase (ck',_) -> generalize ck' |

80 |
| Pck_const (_,_) | Cunivar _ -> () |

81 |
| Clink ck' -> |

82 |
generalize ck' |

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

84 |
generalize_carrier cr; generalize ck' |

85 | |

86 |
let try_generalize ck_node loc = |

87 |
try |

88 |
generalize ck_node |

89 |
with (Scope_carrier cr) -> |

90 |
raise (Error (loc, Carrier_extrusion (ck_node, cr))) |

91 |
| (Scope_clock ck) -> |

92 |
raise (Error (loc, Clock_extrusion (ck_node, ck))) |

93 | |

94 |
(* Clocks instanciation *) |

95 |
let instantiate_carrier cr inst_cr_vars = |

96 |
let cr = carrier_repr cr in |

97 |
match cr.carrier_desc with |

98 |
| Carry_const _ |

99 |
| Carry_name -> cr |

100 |
| Carry_link _ -> |

101 |
failwith "Internal error" |

102 |
| Carry_var -> |

103 |
try |

104 |
List.assoc cr.carrier_id !inst_cr_vars |

105 |
with Not_found -> |

106 |
let cr_var = new_carrier Carry_name true in |

107 |
inst_cr_vars := (cr.carrier_id,cr_var)::!inst_cr_vars; |

108 |
cr_var |

109 | |

110 |
(** Downgrade polymorphic clock variables to monomorphic clock variables *) |

111 |
(* inst_ck_vars ensures that a polymorphic variable is instanciated with |

112 |
the same monomorphic variable if it occurs several times in the same |

113 |
type. inst_cr_vars is the same for carriers. *) |

114 |
let rec instantiate inst_ck_vars inst_cr_vars ck = |

115 |
match ck.cdesc with |

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

117 |
{ck with cdesc = |

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

119 |
(instantiate inst_ck_vars inst_cr_vars ck2))} |

120 |
| Ctuple cklist -> |

121 |
{ck with cdesc = Ctuple |

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

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

124 |
let c' = instantiate_carrier c inst_cr_vars in |

125 |
{ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)} |

126 |
| Cvar _ | Pck_const (_,_) -> ck |

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

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

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

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

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

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

133 |
| Clink ck' -> |

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 |
{ck with cdesc = |

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

139 |
| Cunivar cset -> |

140 |
try |

141 |
List.assoc ck.cid !inst_ck_vars |

142 |
with Not_found -> |

143 |
let var = new_ck (Cvar cset) true in |

144 |
inst_ck_vars := (ck.cid, var)::!inst_ck_vars; |

145 |
var |

146 | |

147 |
(** [subsume pck1 cset1] subsumes clock [pck1] by clock subset |

148 |
[cset1]. The clock constraint is actually recursively transfered to |

149 |
the clock variable appearing in [pck1] *) |

150 |
let subsume pck1 cset1 = |

151 |
let rec aux pck cset = |

152 |
match cset with |

153 |
| CSet_all -> |

154 |
() |

155 |
| CSet_pck (k,(a,b)) -> |

156 |
match pck.cdesc with |

157 |
| Cvar cset' -> |

158 |
pck.cdesc <- Cvar (intersect cset' cset) |

159 |
| Pck_up (pck',k') -> |

160 |
let rat = if a=0 then (0,1) else (a,b*k') in |

161 |
aux pck' (CSet_pck ((k*k'),rat)) |

162 |
| Pck_down (pck',k') -> |

163 |
let k''=k/(gcd k k') in |

164 |
aux pck' (CSet_pck (k'',(a*k',b))) |

165 |
| Pck_phase (pck',(a',b')) -> |

166 |
let (a'',b'')= max_rat (sum_rat (a,b) (-a',b')) (0,1) in |

167 |
aux pck' (CSet_pck (k, (a'',b''))) |

168 |
| Pck_const (n,(a',b')) -> |

169 |
if n mod k <> 0 || (max_rat (a,b) (a',b')) <> (a',b') then |

170 |
raise (Subsume (pck1, cset1)) |

171 |
| Clink pck' -> |

172 |
aux pck' cset |

173 |
| Cunivar _ -> () |

174 |
| Ccarrying (_,ck') -> |

175 |
aux ck' cset |

176 |
| _ -> raise (Subsume (pck1, cset1)) |

177 |
in |

178 |
aux pck1 cset1 |

179 | |

180 |
let rec update_scope_carrier scoped cr = |

181 |
if (not scoped) then |

182 |
begin |

183 |
cr.carrier_scoped <- scoped; |

184 |
match cr.carrier_desc with |

185 |
| Carry_const _ | Carry_name | Carry_var -> () |

186 |
| Carry_link cr' -> update_scope_carrier scoped cr' |

187 |
end |

188 | |

189 |
let rec update_scope scoped ck = |

190 |
if (not scoped) then |

191 |
begin |

192 |
ck.cscoped <- scoped; |

193 |
match ck.cdesc with |

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

195 |
update_scope scoped ck1; update_scope scoped ck2 |

196 |
| Ctuple clist -> |

197 |
List.iter (update_scope scoped) clist |

198 |
| Con (ck',cr,_) -> update_scope scoped ck'(*; update_scope_carrier scoped cr*) |

199 |
| Cvar cset -> |

200 |
ck.cdesc <- Cvar cset |

201 |
| Pck_up (ck',_) -> update_scope scoped ck' |

202 |
| Pck_down (ck',_) -> update_scope scoped ck' |

203 |
| Pck_phase (ck',_) -> update_scope scoped ck' |

204 |
| Pck_const (_,_) | Cunivar _ -> () |

205 |
| Clink ck' -> |

206 |
update_scope scoped ck' |

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

208 |
update_scope_carrier scoped cr; update_scope scoped ck' |

209 |
end |

210 | |

211 |
(* Unifies two static pclocks. *) |

212 |
let unify_static_pck ck1 ck2 = |

213 |
if (period ck1 <> period ck2) || (phase ck1 <> phase ck2) then |

214 |
raise (Unify (ck1,ck2)) |

215 | |

216 |
(* Unifies two clock carriers *) |

217 |
let unify_carrier cr1 cr2 = |

218 |
let cr1 = carrier_repr cr1 in |

219 |
let cr2 = carrier_repr cr2 in |

220 |
if cr1==cr2 then () |

221 |
else |

222 |
match cr1.carrier_desc, cr2.carrier_desc with |

223 |
| Carry_const id1, Carry_const id2 -> |

224 |
if id1 <> id2 then raise (Mismatch (cr1, cr2)) |

225 |
| Carry_const _, Carry_name -> |

226 |
begin |

227 |
cr2.carrier_desc <- Carry_link cr1; |

228 |
update_scope_carrier cr2.carrier_scoped cr1 |

229 |
end |

230 |
| Carry_name, Carry_const _ -> |

231 |
begin |

232 |
cr1.carrier_desc <- Carry_link cr2; |

233 |
update_scope_carrier cr1.carrier_scoped cr2 |

234 |
end |

235 |
| Carry_name, Carry_name -> |

236 |
if cr1.carrier_id < cr2.carrier_id then |

237 |
begin |

238 |
cr2.carrier_desc <- Carry_link cr1; |

239 |
update_scope_carrier cr2.carrier_scoped cr1 |

240 |
end |

241 |
else |

242 |
begin |

243 |
cr1.carrier_desc <- Carry_link cr2; |

244 |
update_scope_carrier cr1.carrier_scoped cr2 |

245 |
end |

246 |
| _,_ -> assert false |

247 | |

248 |
(* Semi-unifies two clock carriers *) |

249 |
let semi_unify_carrier cr1 cr2 = |

250 |
let cr1 = carrier_repr cr1 in |

251 |
let cr2 = carrier_repr cr2 in |

252 |
if cr1==cr2 then () |

253 |
else |

254 |
match cr1.carrier_desc, cr2.carrier_desc with |

255 |
| Carry_const id1, Carry_const id2 -> |

256 |
if id1 <> id2 then raise (Mismatch (cr1, cr2)) |

257 |
| Carry_const _, Carry_name -> |

258 |
begin |

259 |
cr2.carrier_desc <- Carry_link cr1; |

260 |
update_scope_carrier cr2.carrier_scoped cr1 |

261 |
end |

262 |
| Carry_name, Carry_const _ -> raise (Mismatch (cr1, cr2)) |

263 |
| Carry_name, Carry_name -> |

264 |
if cr1.carrier_id < cr2.carrier_id then |

265 |
begin |

266 |
cr2.carrier_desc <- Carry_link cr1; |

267 |
update_scope_carrier cr2.carrier_scoped cr1 |

268 |
end |

269 |
else |

270 |
begin |

271 |
cr1.carrier_desc <- Carry_link cr2; |

272 |
update_scope_carrier cr1.carrier_scoped cr2 |

273 |
end |

274 |
| _,_ -> assert false |

275 | |

276 |
let try_unify_carrier ck1 ck2 loc = |

277 |
try |

278 |
unify_carrier ck1 ck2 |

279 |
with |

280 |
| Unify (ck1',ck2') -> |

281 |
raise (Error (loc, Clock_clash (ck1',ck2'))) |

282 |
| Subsume (ck,cset) -> |

283 |
raise (Error (loc, Clock_set_mismatch (ck,cset))) |

284 |
| Mismatch (cr1,cr2) -> |

285 |
raise (Error (loc, Carrier_mismatch (cr1,cr2))) |

286 | |

287 |
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify |

288 |
(ck1,ck2)] if the clocks are not unifiable.*) |

289 |
let rec unify ck1 ck2 = |

290 |
let ck1 = repr ck1 in |

291 |
let ck2 = repr ck2 in |

292 |
if ck1==ck2 then |

293 |
() |

294 |
else |

295 |
let left_const = is_concrete_pck ck1 in |

296 |
let right_const = is_concrete_pck ck2 in |

297 |
if left_const && right_const then |

298 |
unify_static_pck ck1 ck2 |

299 |
else |

300 |
match ck1.cdesc,ck2.cdesc with |

301 |
| Cvar cset1,Cvar cset2-> |

302 |
if ck1.cid < ck2.cid then |

303 |
begin |

304 |
ck2.cdesc <- Clink (simplify ck1); |

305 |
update_scope ck2.cscoped ck1; |

306 |
subsume ck1 cset2 |

307 |
end |

308 |
else |

309 |
begin |

310 |
ck1.cdesc <- Clink (simplify ck2); |

311 |
update_scope ck1.cscoped ck2; |

312 |
subsume ck2 cset1 |

313 |
end |

314 |
| Cvar cset, Pck_up (_,_) | Cvar cset, Pck_down (_,_) |

315 |
| Cvar cset, Pck_phase (_,_) | Cvar cset, Pck_const (_,_) -> |

316 |
if (occurs ck1 ck2) then |

317 |
begin |

318 |
if (simplify ck2 = ck1) then |

319 |
ck2.cdesc <- Clink (simplify ck1) |

320 |
else |

321 |
raise (Unify (ck1,ck2)); |

322 |
end |

323 |
else |

324 |
begin |

325 |
ck1.cdesc <- Clink (simplify ck2); |

326 |
subsume ck2 cset |

327 |
end |

328 |
| Pck_up (_,_), Cvar cset | Pck_down (_,_), Cvar cset |

329 |
| Pck_phase (_,_), Cvar cset | Pck_const (_,_), Cvar cset -> |

330 |
if (occurs ck2 ck1) then |

331 |
begin |

332 |
if ((simplify ck1) = ck2) then |

333 |
ck1.cdesc <- Clink (simplify ck2) |

334 |
else |

335 |
raise (Unify (ck1,ck2)); |

336 |
end |

337 |
else |

338 |
begin |

339 |
ck2.cdesc <- Clink (simplify ck1); |

340 |
subsume ck1 cset |

341 |
end |

342 |
| (Cvar cset,_) when (not (occurs ck1 ck2)) -> |

343 |
subsume ck2 cset; |

344 |
update_scope ck1.cscoped ck2; |

345 |
ck1.cdesc <- Clink (simplify ck2) |

346 |
| (_, (Cvar cset)) when (not (occurs ck2 ck1)) -> |

347 |
subsume ck1 cset; |

348 |
update_scope ck2.cscoped ck1; |

349 |
ck2.cdesc <- Clink (simplify ck1) |

350 |
| Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') -> |

351 |
unify_carrier cr1 cr2; |

352 |
unify ck1' ck2' |

353 |
| Ccarrying (_,_),_ | _,Ccarrying (_,_) -> |

354 |
raise (Unify (ck1,ck2)) |

355 |
| Carrow (c1,c2), Carrow (c1',c2') -> |

356 |
unify c1 c1'; unify c2 c2' |

357 |
| Ctuple ckl1, Ctuple ckl2 -> |

358 |
if (List.length ckl1) <> (List.length ckl2) then |

359 |
raise (Unify (ck1,ck2)); |

360 |
List.iter2 unify ckl1 ckl2 |

361 |
| Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 -> |

362 |
unify_carrier c1 c2; |

363 |
unify ck' ck'' |

364 |
| Pck_const (i,r), Pck_const (i',r') -> |

365 |
if i<>i' || r <> r' then |

366 |
raise (Unify (ck1,ck2)) |

367 |
| (_, Pck_up (pck2',k)) when (not right_const) -> |

368 |
let ck1' = simplify (new_ck (Pck_down (ck1,k)) true) in |

369 |
unify ck1' pck2' |

370 |
| (_,Pck_down (pck2',k)) when (not right_const) -> |

371 |
subsume ck1 (CSet_pck (k,(0,1))); |

372 |
let ck1' = simplify (new_ck (Pck_up (ck1,k)) true) in |

373 |
unify ck1' pck2' |

374 |
| (_,Pck_phase (pck2',(a,b))) when (not right_const) -> |

375 |
subsume ck1 (CSet_pck (b,(a,b))); |

376 |
let ck1' = simplify (new_ck (Pck_phase (ck1,(-a,b))) true) in |

377 |
unify ck1' pck2' |

378 |
| Pck_up (pck1',k),_ -> |

379 |
let ck2' = simplify (new_ck (Pck_down (ck2,k)) true) in |

380 |
unify pck1' ck2' |

381 |
| Pck_down (pck1',k),_ -> |

382 |
subsume ck2 (CSet_pck (k,(0,1))); |

383 |
let ck2' = simplify (new_ck (Pck_up (ck2,k)) true) in |

384 |
unify pck1' ck2' |

385 |
| Pck_phase (pck1',(a,b)),_ -> |

386 |
subsume ck2 (CSet_pck (b,(a,b))); |

387 |
let ck2' = simplify (new_ck (Pck_phase (ck2,(-a,b))) true) in |

388 |
unify pck1' ck2' |

389 |
| Cunivar _, _ | _, Cunivar _ -> () |

390 |
| _,_ -> raise (Unify (ck1,ck2)) |

391 | |

392 |
(** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify |

393 |
(ck1,ck2)] if the clocks are not semi-unifiable.*) |

394 |
let rec semi_unify ck1 ck2 = |

395 |
let ck1 = repr ck1 in |

396 |
let ck2 = repr ck2 in |

397 |
if ck1==ck2 then |

398 |
() |

399 |
else |

400 |
match ck1.cdesc,ck2.cdesc with |

401 |
| Cvar cset1,Cvar cset2-> |

402 |
if ck1.cid < ck2.cid then |

403 |
begin |

404 |
ck2.cdesc <- Clink (simplify ck1); |

405 |
update_scope ck2.cscoped ck1 |

406 |
end |

407 |
else |

408 |
begin |

409 |
ck1.cdesc <- Clink (simplify ck2); |

410 |
update_scope ck1.cscoped ck2 |

411 |
end |

412 |
| (Cvar cset,_) -> raise (Unify (ck1,ck2)) |

413 |
| (_, (Cvar cset)) when (not (occurs ck2 ck1)) -> |

414 |
update_scope ck2.cscoped ck1; |

415 |
ck2.cdesc <- Clink (simplify ck1) |

416 |
| Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') -> |

417 |
semi_unify_carrier cr1 cr2; |

418 |
semi_unify ck1' ck2' |

419 |
| Ccarrying (_,_),_ | _,Ccarrying (_,_) -> |

420 |
raise (Unify (ck1,ck2)) |

421 |
| Carrow (c1,c2), Carrow (c1',c2') -> |

422 |
begin |

423 |
semi_unify c1 c1'; |

424 |
semi_unify c2 c2' |

425 |
end |

426 |
| Ctuple ckl1, Ctuple ckl2 -> |

427 |
if (List.length ckl1) <> (List.length ckl2) then |

428 |
raise (Unify (ck1,ck2)); |

429 |
List.iter2 semi_unify ckl1 ckl2 |

430 |
| Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 -> |

431 |
semi_unify_carrier c1 c2; |

432 |
semi_unify ck' ck'' |

433 |
| Cunivar _, _ | _, Cunivar _ -> () |

434 |
| _,_ -> raise (Unify (ck1,ck2)) |

435 | |

436 |
(* Returns the value corresponding to a pclock (integer) factor |

437 |
expression. Expects a constant expression (checked by typing). *) |

438 |
let int_factor_of_expr e = |

439 |
match e.expr_desc with |

440 |
| Expr_const |

441 |
(Const_int i) -> i |

442 |
| _ -> failwith "Internal error: int_factor_of_expr" |

443 | |

444 |
(** [clock_uncarry ck] drops the possible carrier name from clock [ck] *) |

445 |
let clock_uncarry ck = |

446 |
let ck = repr ck in |

447 |
match ck.cdesc with |

448 |
| Ccarrying (_, ck') -> ck' |

449 |
| _ -> ck |

450 | |

451 |
let try_unify ck1 ck2 loc = |

452 |
try |

453 |
unify ck1 ck2 |

454 |
with |

455 |
| Unify (ck1',ck2') -> |

456 |
raise (Error (loc, Clock_clash (ck1',ck2'))) |

457 |
| Subsume (ck,cset) -> |

458 |
raise (Error (loc, Clock_set_mismatch (ck,cset))) |

459 |
| Mismatch (cr1,cr2) -> |

460 |
raise (Error (loc, Carrier_mismatch (cr1,cr2))) |

461 | |

462 |
let try_semi_unify ck1 ck2 loc = |

463 |
try |

464 |
semi_unify ck1 ck2 |

465 |
with |

466 |
| Unify (ck1',ck2') -> |

467 |
raise (Error (loc, Clock_clash (ck1',ck2'))) |

468 |
| Subsume (ck,cset) -> |

469 |
raise (Error (loc, Clock_set_mismatch (ck,cset))) |

470 |
| Mismatch (cr1,cr2) -> |

471 |
raise (Error (loc, Carrier_mismatch (cr1,cr2))) |

472 | |

473 |
(* ck2 is a subtype of ck1 *) |

474 |
let rec sub_unify sub ck1 ck2 = |

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

476 |
| Ctuple cl1 , Ctuple cl2 -> |

477 |
if List.length cl1 <> List.length cl2 |

478 |
then raise (Unify (ck1, ck2)) |

479 |
else List.iter2 (sub_unify sub) cl1 cl2 |

480 |
| Ctuple [c1] , _ -> sub_unify sub c1 ck2 |

481 |
| _ , Ctuple [c2] -> sub_unify sub ck1 c2 |

482 |
| Con (c1, cr1, t1) , Con (c2, cr2, t2) when t1=t2 -> |

483 |
begin |

484 |
unify_carrier cr1 cr2; |

485 |
sub_unify sub c1 c2 |

486 |
end |

487 |
| Ccarrying (cr1, c1), Ccarrying (cr2, c2)-> |

488 |
begin |

489 |
unify_carrier cr1 cr2; |

490 |
sub_unify sub c1 c2 |

491 |
end |

492 |
| _, Ccarrying (_, c2) when sub -> sub_unify sub ck1 c2 |

493 |
| _ -> unify ck1 ck2 |

494 | |

495 |
let try_sub_unify sub ck1 ck2 loc = |

496 |
try |

497 |
sub_unify sub ck1 ck2 |

498 |
with |

499 |
| Unify (ck1',ck2') -> |

500 |
raise (Error (loc, Clock_clash (ck1',ck2'))) |

501 |
| Subsume (ck,cset) -> |

502 |
raise (Error (loc, Clock_set_mismatch (ck,cset))) |

503 |
| Mismatch (cr1,cr2) -> |

504 |
raise (Error (loc, Carrier_mismatch (cr1,cr2))) |

505 | |

506 |
(* Unifies all the clock variables in the clock type of a tuple |

507 |
expression, so that the clock type only uses at most one clock variable *) |

508 |
let unify_tuple_clock ref_ck_opt ck loc = |

509 |
(*(match ref_ck_opt with |

510 |
| None -> Format.eprintf "unify_tuple_clock None %a@." Clocks.print_ck ck |

511 |
| Some ck' -> Format.eprintf "unify_tuple_clock (Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*) |

512 |
let ck_var = ref ref_ck_opt in |

513 |
let rec aux ck = |

514 |
match (repr ck).cdesc with |

515 |
| Con _ |

516 |
| Cvar _ -> |

517 |
begin |

518 |
match !ck_var with |

519 |
| None -> |

520 |
ck_var:=Some ck |

521 |
| Some v -> |

522 |
(* may fail *) |

523 |
try_unify ck v loc |

524 |
end |

525 |
| Ctuple cl -> |

526 |
List.iter aux cl |

527 |
| Carrow _ -> assert false (* should not occur *) |

528 |
| Ccarrying (_, ck1) -> |

529 |
aux ck1 |

530 |
| _ -> () |

531 |
in aux ck |

532 | |

533 |
(* Unifies all the clock variables in the clock type of an imported |

534 |
node, so that the clock type only uses at most one base clock variable, |

535 |
that is, the activation clock of the node *) |

536 |
let unify_imported_clock ref_ck_opt ck loc = |

537 |
let ck_var = ref ref_ck_opt in |

538 |
let rec aux ck = |

539 |
match (repr ck).cdesc with |

540 |
| Cvar _ -> |

541 |
begin |

542 |
match !ck_var with |

543 |
| None -> |

544 |
ck_var:=Some ck |

545 |
| Some v -> |

546 |
(* cannot fail *) |

547 |
try_unify ck v loc |

548 |
end |

549 |
| Ctuple cl -> |

550 |
List.iter aux cl |

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

552 |
aux ck1; aux ck2 |

553 |
| Ccarrying (_, ck1) -> |

554 |
aux ck1 |

555 |
| Con (ck1, _, _) -> aux ck1 |

556 |
| _ -> () |

557 |
in |

558 |
aux ck |

559 | |

560 |
(* Clocks a list of arguments of Lustre builtin operators: |

561 |
- type each expression, remove carriers of clocks as |

562 |
carriers may only denote variables, not arbitrary expr. |

563 |
- try to unify these clocks altogether |

564 |
*) |

565 |
let rec clock_standard_args env expr_list = |

566 |
let ck_list = List.map (fun e -> clock_uncarry (clock_expr env e)) expr_list in |

567 |
let ck_res = new_var true in |

568 |
List.iter2 (fun e ck -> try_unify ck ck_res e.expr_loc) expr_list ck_list; |

569 |
ck_res |

570 | |

571 |
(* emulates a subtyping relation between clocks c and (cr : c), |

572 |
used during node application only *) |

573 |
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock = |

574 |
let loc = real_arg.expr_loc in |

575 |
let real_clock = clock_expr env real_arg in |

576 |
try_sub_unify sub formal_clock real_clock loc |

577 | |

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

579 |
and clock_appl env f args clock_reset loc = |

580 |
let args = expr_list_of_expr args in |

581 |
if Basic_library.is_internal_fun f && List.exists is_tuple_expr args |

582 |
then |

583 |
let args = Utils.transpose_list (List.map expr_list_of_expr args) in |

584 |
Clocks.clock_of_clock_list (List.map (fun args -> clock_call env f args clock_reset loc) args) |

585 |
else |

586 |
clock_call env f args clock_reset loc |

587 | |

588 |
and clock_call env f args clock_reset loc = |

589 |
let cfun = clock_ident false env f loc in |

590 |
let cins, couts = split_arrow cfun in |

591 |
let cins = clock_list_of_clock cins in |

592 |
List.iter2 (clock_subtyping_arg env) args cins; |

593 |
unify_imported_clock (Some clock_reset) cfun loc; |

594 |
couts |

595 | |

596 |
and clock_ident nocarrier env id loc = |

597 |
clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc) |

598 | |

599 |
and clock_carrier env c loc ce = |

600 |
let expr_c = expr_of_ident c loc in |

601 |
let ck = clock_expr ~nocarrier:false env expr_c in |

602 |
let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in |

603 |
let ckb = new_var true in |

604 |
let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in |

605 |
try_unify ck ckcarry expr_c.expr_loc; |

606 |
unify_tuple_clock (Some ckb) ce expr_c.expr_loc; |

607 |
cr |

608 | |

609 |
(** [clock_expr env expr] performs the clock calculus for expression [expr] in |

610 |
environment [env] *) |

611 |
and clock_expr ?(nocarrier=true) env expr = |

612 |
let resulting_ck = |

613 |
match expr.expr_desc with |

614 |
| Expr_const cst -> |

615 |
let ck = new_var true in |

616 |
expr.expr_clock <- ck; |

617 |
ck |

618 |
| Expr_ident v -> |

619 |
let ckv = |

620 |
try |

621 |
Env.lookup_value env v |

622 |
with Not_found -> |

623 |
failwith ("Internal error, variable \""^v^"\" not found") |

624 |
in |

625 |
let ck = instantiate (ref []) (ref []) ckv in |

626 |
expr.expr_clock <- ck; |

627 |
ck |

628 |
| Expr_array elist -> |

629 |
let ck = clock_standard_args env elist in |

630 |
expr.expr_clock <- ck; |

631 |
ck |

632 |
| Expr_access (e1, d) -> |

633 |
(* dimension, being a static value, doesn't need to be clocked *) |

634 |
let ck = clock_standard_args env [e1] in |

635 |
expr.expr_clock <- ck; |

636 |
ck |

637 |
| Expr_power (e1, d) -> |

638 |
(* dimension, being a static value, doesn't need to be clocked *) |

639 |
let ck = clock_standard_args env [e1] in |

640 |
expr.expr_clock <- ck; |

641 |
ck |

642 |
| Expr_tuple elist -> |

643 |
let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in |

644 |
expr.expr_clock <- ck; |

645 |
ck |

646 |
| Expr_ite (c, t, e) -> |

647 |
let ck_c = clock_standard_args env [c] in |

648 |
let ck = clock_standard_args env [t; e] in |

649 |
(* Here, the branches may exhibit a tuple clock, not the condition *) |

650 |
unify_tuple_clock (Some ck_c) ck expr.expr_loc; |

651 |
expr.expr_clock <- ck; |

652 |
ck |

653 |
| Expr_appl (id, args, r) -> |

654 |
(try |

655 |
(* for a modular compilation scheme, all inputs/outputs must share the same clock ! |

656 |
this is also the reset clock ! |

657 |
*) |

658 |
let cr = |

659 |
match r with |

660 |
| None -> new_var true |

661 |
| Some (x, _) -> let loc_r = loc_of_cond expr.expr_loc x in |

662 |
let expr_r = expr_of_ident x loc_r in |

663 |
clock_expr env expr_r in |

664 |
let couts = clock_appl env id args cr expr.expr_loc in |

665 |
expr.expr_clock <- couts; |

666 |
couts |

667 |
with exn -> ( |

668 |
Format.eprintf "Current expr: %a@." Printers.pp_expr expr; |

669 |
raise exn |

670 |
)) |

671 |
| Expr_fby (e1,e2) |

672 |
| Expr_arrow (e1,e2) -> |

673 |
let ck = clock_standard_args env [e1; e2] in |

674 |
unify_tuple_clock None ck expr.expr_loc; |

675 |
expr.expr_clock <- ck; |

676 |
ck |

677 |
| Expr_pre e -> (* todo : deal with phases as in tail ? *) |

678 |
let ck = clock_standard_args env [e] in |

679 |
expr.expr_clock <- ck; |

680 |
ck |

681 |
| Expr_when (e,c,l) -> |

682 |
let ce = clock_standard_args env [e] in |

683 |
let c_loc = loc_of_cond expr.expr_loc c in |

684 |
let cr = clock_carrier env c c_loc ce in |

685 |
let ck = clock_on ce cr l in |

686 |
let cr' = new_carrier (Carry_const c) ck.cscoped in |

687 |
let ck' = clock_on ce cr' l in |

688 |
expr.expr_clock <- ck'; |

689 |
ck |

690 |
| Expr_merge (c,hl) -> |

691 |
let cvar = new_var true in |

692 |
let crvar = new_carrier Carry_name true in |

693 |
List.iter (fun (t, h) -> let ckh = clock_expr env h in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl; |

694 |
let cr = clock_carrier env c expr.expr_loc cvar in |

695 |
try_unify_carrier cr crvar expr.expr_loc; |

696 |
expr.expr_clock <- cvar; |

697 |
cvar |

698 |
in |

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

700 |
resulting_ck |

701 | |

702 |
let clock_of_vlist vars = |

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

704 |
clock_of_clock_list ckl |

705 | |

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

707 |
environment [env] *) |

708 |
let clock_eq env eq = |

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

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

711 |
clock_subtyping_arg env expr_lhs ck_rhs |

712 | |

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

714 |
declaration [cck] *) |

715 |
let clock_coreclock env cck id loc scoped = |

716 |
match cck.ck_dec_desc with |

717 |
| Ckdec_any -> new_var scoped |

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

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

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

721 |
ck |

722 |
| Ckdec_bool cl -> |

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

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

725 |
let dummy_id_expr = expr_of_ident id loc in |

726 |
let when_expr = |

727 |
List.fold_left |

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

729 |
{expr_tag = new_tag (); |

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

731 |
expr_type = Types.new_var (); |

732 |
expr_clock = new_var scoped; |

733 |
expr_delay = Delay.new_var (); |

734 |
expr_loc = loc; |

735 |
expr_annot = None}) |

736 |
dummy_id_expr cl |

737 |
in |

738 |
clock_expr temp_env when_expr |

739 | |

740 |
(* Clocks a variable declaration *) |

741 |
let clock_var_decl scoped env vdecl = |

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

743 |
let ck = |

744 |
(* WTF ???? |

745 |
if vdecl.var_dec_const |

746 |
then |

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

748 |
else |

749 |
*) |

750 |
if Types.get_clock_base_type vdecl.var_type <> None |

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

752 |
else ck in |

753 |
vdecl.var_clock <- ck; |

754 |
Env.add_value env vdecl.var_id ck |

755 | |

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

757 |
let clock_var_decl_list env scoped l = |

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

759 | |

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

761 |
environment [env]. |

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

763 |
- generalize inputs (unscoped). |

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

765 |
are allowed to be generalized. |

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

767 |
they can be generalized. |

768 |
*) |

769 |
let clock_node env loc nd = |

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

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

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

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

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

775 |
let ck_ins = clock_of_vlist nd.node_inputs in |

776 |
let ck_outs = clock_of_vlist nd.node_outputs in |

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

778 |
unify_imported_clock None ck_node loc; |

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

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

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

782 |
try_generalize ck_node loc; |

783 |
(* |

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

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

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

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

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

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

790 |
*) |

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

792 |
nd.node_clock <- ck_node; |

793 |
Env.add_value env nd.node_id ck_node |

794 | |

795 | |

796 |
let check_imported_pclocks loc ck_node = |

797 |
let pck = ref None in |

798 |
let rec aux ck = |

799 |
match ck.cdesc with |

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

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

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

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

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

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

806 |
begin |

807 |
match !pck with |

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

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

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

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

812 |
end |

813 |
| Clink ck' -> aux ck' |

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

815 |
| Cvar _ | Cunivar _ -> |

816 |
match !pck with |

817 |
| None -> () |

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

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

820 |
in |

821 |
aux ck_node |

822 | |

823 |
let clock_imported_node env loc nd = |

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

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

826 |
let ck_ins = clock_of_vlist nd.nodei_inputs in |

827 |
let ck_outs = clock_of_vlist nd.nodei_outputs in |

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

829 |
unify_imported_clock None ck_node loc; |

830 |
check_imported_pclocks loc ck_node; |

831 |
try_generalize ck_node loc; |

832 |
nd.nodei_clock <- ck_node; |

833 |
Env.add_value env nd.nodei_id ck_node |

834 | |

835 |
let clock_top_consts env clist = |

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

837 |
let ck = new_var false in |

838 |
try_generalize ck cdecl.const_loc; |

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

840 | |

841 |
let clock_top_decl env decl = |

842 |
match decl.top_decl_desc with |

843 |
| Node nd -> |

844 |
clock_node env decl.top_decl_loc nd |

845 |
| ImportedNode nd -> |

846 |
clock_imported_node env decl.top_decl_loc nd |

847 |
| Consts clist -> |

848 |
clock_top_consts env clist |

849 |
| Open _ |

850 |
| Type _ -> env |

851 | |

852 |
let clock_prog env decls = |

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

854 | |

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

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

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

858 | |

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

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

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

862 |
*) |

863 |
let uneval_vdecl_generics vdecl = |

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

865 |
if Types.get_clock_base_type vdecl.var_type <> None |

866 |
then |

867 |
match get_carrier_name vdecl.var_clock with |

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

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

870 | |

871 |
let uneval_node_generics vdecls = |

872 |
List.iter uneval_vdecl_generics vdecls |

873 | |

874 |
let uneval_top_generics decl = |

875 |
match decl.top_decl_desc with |

876 |
| Node nd -> |

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

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

879 |
| ImportedNode nd -> |

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

881 |
| Consts _ |

882 |
| Open _ |

883 |
| Type _ -> () |

884 | |

885 |
let uneval_prog_generics prog = |

886 |
List.iter uneval_top_generics prog |

887 | |

888 |
let check_env_compat header declared computed = |

889 |
uneval_prog_generics header; |

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

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

892 |
try_semi_unify decl_clock_k computed_c Location.dummy_loc |

893 |
) |

894 |
(* Local Variables: *) |

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

896 |
(* End: *) |