## lustrec / src / clock_calculus.ml @ a2d97a3e

History | View | Annotate | Download (30.1 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 |
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify |

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

278 |
let rec unify ck1 ck2 = |

279 |
let ck1 = repr ck1 in |

280 |
let ck2 = repr ck2 in |

281 |
if ck1==ck2 then |

282 |
() |

283 |
else |

284 |
let left_const = is_concrete_pck ck1 in |

285 |
let right_const = is_concrete_pck ck2 in |

286 |
if left_const && right_const then |

287 |
unify_static_pck ck1 ck2 |

288 |
else |

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

290 |
| Cvar cset1,Cvar cset2-> |

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

292 |
begin |

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

294 |
update_scope ck2.cscoped ck1; |

295 |
subsume ck1 cset2 |

296 |
end |

297 |
else |

298 |
begin |

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

300 |
update_scope ck1.cscoped ck2; |

301 |
subsume ck2 cset1 |

302 |
end |

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

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

305 |
if (occurs ck1 ck2) then |

306 |
begin |

307 |
if (simplify ck2 = ck1) then |

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

309 |
else |

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

311 |
end |

312 |
else |

313 |
begin |

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

315 |
subsume ck2 cset |

316 |
end |

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

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

319 |
if (occurs ck2 ck1) then |

320 |
begin |

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

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

323 |
else |

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

325 |
end |

326 |
else |

327 |
begin |

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

329 |
subsume ck1 cset |

330 |
end |

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

332 |
subsume ck2 cset; |

333 |
update_scope ck1.cscoped ck2; |

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

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

336 |
subsume ck1 cset; |

337 |
update_scope ck2.cscoped ck1; |

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

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

340 |
unify_carrier cr1 cr2; |

341 |
unify ck1' ck2' |

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

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

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

345 |
unify c1 c1'; unify c2 c2' |

346 |
| Ctuple ckl1, Ctuple ckl2 -> |

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

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

349 |
List.iter2 unify ckl1 ckl2 |

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

351 |
unify_carrier c1 c2; |

352 |
unify ck' ck'' |

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

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

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

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

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

358 |
unify ck1' pck2' |

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

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

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

362 |
unify ck1' pck2' |

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

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

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

366 |
unify ck1' pck2' |

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

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

369 |
unify pck1' ck2' |

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

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

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

373 |
unify pck1' ck2' |

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

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

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

377 |
unify pck1' ck2' |

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

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

380 | |

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

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

383 |
let rec semi_unify ck1 ck2 = |

384 |
let ck1 = repr ck1 in |

385 |
let ck2 = repr ck2 in |

386 |
if ck1==ck2 then |

387 |
() |

388 |
else |

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

390 |
| Cvar cset1,Cvar cset2-> |

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

392 |
begin |

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

394 |
update_scope ck2.cscoped ck1 |

395 |
end |

396 |
else |

397 |
begin |

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

399 |
update_scope ck1.cscoped ck2 |

400 |
end |

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

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

403 |
update_scope ck2.cscoped ck1; |

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

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

406 |
semi_unify_carrier cr1 cr2; |

407 |
semi_unify ck1' ck2' |

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

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

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

411 |
begin |

412 |
semi_unify c1 c1'; |

413 |
semi_unify c2 c2' |

414 |
end |

415 |
| Ctuple ckl1, Ctuple ckl2 -> |

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

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

418 |
List.iter2 semi_unify ckl1 ckl2 |

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

420 |
semi_unify_carrier c1 c2; |

421 |
semi_unify ck' ck'' |

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

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

424 | |

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

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

427 |
let int_factor_of_expr e = |

428 |
match e.expr_desc with |

429 |
| Expr_const |

430 |
(Const_int i) -> i |

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

432 | |

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

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

435 |
let unify_tuple_clock ref_ck_opt ck = |

436 |
let ck_var = ref ref_ck_opt in |

437 |
let rec aux ck = |

438 |
match (repr ck).cdesc with |

439 |
| Con _ |

440 |
| Cvar _ -> |

441 |
begin |

442 |
match !ck_var with |

443 |
| None -> |

444 |
ck_var:=Some ck |

445 |
| Some v -> |

446 |
(* may fail *) |

447 |
unify v ck |

448 |
end |

449 |
| Ctuple cl -> |

450 |
List.iter aux cl |

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

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

453 |
aux ck1 |

454 |
| _ -> () |

455 |
in |

456 |
aux ck |

457 | |

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

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

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

461 |
let unify_imported_clock ref_ck_opt ck = |

462 |
let ck_var = ref ref_ck_opt in |

463 |
let rec aux ck = |

464 |
match (repr ck).cdesc with |

465 |
| Cvar _ -> |

466 |
begin |

467 |
match !ck_var with |

468 |
| None -> |

469 |
ck_var:=Some ck |

470 |
| Some v -> |

471 |
(* cannot fail *) |

472 |
unify v ck |

473 |
end |

474 |
| Ctuple cl -> |

475 |
List.iter aux cl |

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

477 |
aux ck1; aux ck2 |

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

479 |
aux ck1 |

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

481 |
| _ -> () |

482 |
in |

483 |
aux ck |

484 | |

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

486 |
let clock_uncarry ck = |

487 |
let ck = repr ck in |

488 |
match ck.cdesc with |

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

490 |
| _ -> ck |

491 | |

492 |
let try_unify ck1 ck2 loc = |

493 |
try |

494 |
unify ck1 ck2 |

495 |
with |

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

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

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

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

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

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

502 | |

503 |
let try_semi_unify ck1 ck2 loc = |

504 |
try |

505 |
semi_unify ck1 ck2 |

506 |
with |

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

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

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

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

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

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

513 | |

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

515 |
let rec sub_unify sub ck1 ck2 = |

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

517 |
| Ctuple cl1 , Ctuple cl2 -> |

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

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

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

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

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

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

524 |
begin |

525 |
unify_carrier cr1 cr2; |

526 |
sub_unify sub c1 c2 |

527 |
end |

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

529 |
begin |

530 |
unify_carrier cr1 cr2; |

531 |
sub_unify sub c1 c2 |

532 |
end |

533 |
| Ccarrying (_, c1) , _ when sub -> sub_unify sub c1 ck2 |

534 |
| _ -> unify ck1 ck2 |

535 | |

536 |
let try_sub_unify sub ck1 ck2 loc = |

537 |
try |

538 |
sub_unify sub ck1 ck2 |

539 |
with |

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

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

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

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

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

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

546 | |

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

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

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

550 |
- try to unify these clocks altogether |

551 |
*) |

552 |
let rec clock_standard_args env expr_list = |

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

554 |
let ck_res = new_var true in |

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

556 |
ck_res |

557 | |

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

559 |
used during node application only *) |

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

561 |
let loc = real_arg.expr_loc in |

562 |
let real_clock = clock_expr env real_arg in |

563 |
try_sub_unify sub real_clock formal_clock loc |

564 | |

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

566 |
and clock_appl env f args clock_reset loc = |

567 |
let args = expr_list_of_expr args in |

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

569 |
then |

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

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

572 |
else |

573 |
clock_call env f args clock_reset loc |

574 | |

575 |
and clock_call env f args clock_reset loc = |

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

577 |
let cins, couts = split_arrow cfun in |

578 |
let cins = clock_list_of_clock cins in |

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

580 |
unify_imported_clock (Some clock_reset) cfun; |

581 |
couts |

582 | |

583 |
and clock_ident nocarrier env id loc = |

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

585 | |

586 |
and clock_carrier env c loc ce = |

587 |
let expr_c = expr_of_ident c loc in |

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

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

590 |
let ckcarry = new_ck (Ccarrying (cr,ce)) ck.cscoped in |

591 |
try_unify ck ckcarry expr_c.expr_loc; |

592 |
cr |

593 | |

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

595 |
environment [env] *) |

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

597 |
let resulting_ck = |

598 |
match expr.expr_desc with |

599 |
| Expr_const cst -> |

600 |
let ck = new_var true in |

601 |
expr.expr_clock <- ck; |

602 |
ck |

603 |
| Expr_ident v -> |

604 |
let ckv = |

605 |
try |

606 |
Env.lookup_value env v |

607 |
with Not_found -> |

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

609 |
in |

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

611 |
expr.expr_clock <- ck; |

612 |
ck |

613 |
| Expr_array elist -> |

614 |
let ck = clock_standard_args env elist in |

615 |
expr.expr_clock <- ck; |

616 |
ck |

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

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

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

620 |
expr.expr_clock <- ck; |

621 |
ck |

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

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

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

625 |
expr.expr_clock <- ck; |

626 |
ck |

627 |
| Expr_tuple elist -> |

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

629 |
expr.expr_clock <- ck; |

630 |
ck |

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

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

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

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

635 |
unify_tuple_clock (Some ck_c) ck; |

636 |
expr.expr_clock <- ck; |

637 |
ck |

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

639 |
(try |

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

641 |
this is also the reset clock ! |

642 |
*) |

643 |
let cr = |

644 |
match r with |

645 |
| None -> new_var true |

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

647 |
let expr_r = expr_of_ident x loc_r in |

648 |
clock_expr env expr_r in |

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

650 |
expr.expr_clock <- couts; |

651 |
couts |

652 |
with exn -> ( |

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

654 |
raise exn |

655 |
)) |

656 |
| Expr_fby (e1,e2) |

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

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

659 |
unify_tuple_clock None ck; |

660 |
expr.expr_clock <- ck; |

661 |
ck |

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

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

664 |
expr.expr_clock <- ck; |

665 |
ck |

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

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

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

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

670 |
let ck = new_ck (Con (ce,cr,l)) true in |

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

672 |
let ck' = new_ck (Con (ce,cr',l)) true in |

673 |
expr.expr_clock <- ck'; |

674 |
ck |

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

676 |
let cvar = new_var true in |

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

678 |
List.iter (fun (t, h) -> clock_subtyping_arg env h (new_ck (Con (cvar,cr,t)) true)) hl; |

679 |
expr.expr_clock <- cvar; |

680 |
cvar |

681 |
in |

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

683 |
resulting_ck |

684 | |

685 |
let clock_of_vlist vars = |

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

687 |
clock_of_clock_list ckl |

688 | |

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

690 |
environment [env] *) |

691 |
let clock_eq env eq = |

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

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

694 |
clock_subtyping_arg env expr_lhs ck_rhs |

695 | |

696 | |

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

698 |
declaration [cck] *) |

699 |
let clock_coreclock env cck id loc scoped = |

700 |
match cck.ck_dec_desc with |

701 |
| Ckdec_any -> new_var scoped |

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

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

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

705 |
ck |

706 |
| Ckdec_bool cl -> |

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

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

709 |
let dummy_id_expr = expr_of_ident id loc in |

710 |
let when_expr = |

711 |
List.fold_left |

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

713 |
{expr_tag = new_tag (); |

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

715 |
expr_type = Types.new_var (); |

716 |
expr_clock = new_var scoped; |

717 |
expr_delay = Delay.new_var (); |

718 |
expr_loc = loc; |

719 |
expr_annot = None}) |

720 |
dummy_id_expr cl |

721 |
in |

722 |
clock_expr temp_env when_expr |

723 | |

724 |
(* Clocks a variable declaration *) |

725 |
let clock_var_decl scoped env vdecl = |

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

727 |
let ck = |

728 |
(* WTF ???? |

729 |
if vdecl.var_dec_const |

730 |
then |

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

732 |
else |

733 |
*) |

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

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

736 |
else ck in |

737 |
vdecl.var_clock <- ck; |

738 |
Env.add_value env vdecl.var_id ck |

739 | |

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

741 |
let clock_var_decl_list env scoped l = |

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

743 | |

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

745 |
environment [env]. |

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

747 |
- generalize inputs (unscoped). |

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

749 |
are allowed to be generalized. |

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

751 |
they can be generalized. |

752 |
*) |

753 |
let clock_node env loc nd = |

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

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

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

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

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

759 |
let ck_ins = clock_of_vlist nd.node_inputs in |

760 |
let ck_outs = clock_of_vlist nd.node_outputs in |

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

762 |
unify_imported_clock None ck_node; |

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

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

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

766 |
try_generalize ck_node loc; |

767 |
(* |

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

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

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

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

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

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

774 |
*) |

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

776 |
nd.node_clock <- ck_node; |

777 |
Env.add_value env nd.node_id ck_node |

778 | |

779 | |

780 |
let check_imported_pclocks loc ck_node = |

781 |
let pck = ref None in |

782 |
let rec aux ck = |

783 |
match ck.cdesc with |

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

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

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

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

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

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

790 |
begin |

791 |
match !pck with |

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

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

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

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

796 |
end |

797 |
| Clink ck' -> aux ck' |

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

799 |
| Cvar _ | Cunivar _ -> |

800 |
match !pck with |

801 |
| None -> () |

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

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

804 |
in |

805 |
aux ck_node |

806 | |

807 |
let clock_imported_node env loc nd = |

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

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

810 |
let ck_ins = clock_of_vlist nd.nodei_inputs in |

811 |
let ck_outs = clock_of_vlist nd.nodei_outputs in |

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

813 |
unify_imported_clock None ck_node; |

814 |
check_imported_pclocks loc ck_node; |

815 |
try_generalize ck_node loc; |

816 |
nd.nodei_clock <- ck_node; |

817 |
Env.add_value env nd.nodei_id ck_node |

818 | |

819 |
let clock_top_consts env clist = |

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

821 |
let ck = new_var false in |

822 |
try_generalize ck cdecl.const_loc; |

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

824 | |

825 |
let clock_top_decl env decl = |

826 |
match decl.top_decl_desc with |

827 |
| Node nd -> |

828 |
clock_node env decl.top_decl_loc nd |

829 |
| ImportedNode nd -> |

830 |
clock_imported_node env decl.top_decl_loc nd |

831 |
| Consts clist -> |

832 |
clock_top_consts env clist |

833 |
| Open _ -> |

834 |
env |

835 | |

836 |
let clock_prog env decls = |

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

838 | |

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

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

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

842 | |

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

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

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

846 |
*) |

847 |
let uneval_vdecl_generics vdecl = |

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

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

850 |
then |

851 |
match get_carrier_name vdecl.var_clock with |

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

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

854 | |

855 |
let uneval_node_generics vdecls = |

856 |
List.iter uneval_vdecl_generics vdecls |

857 | |

858 |
let uneval_top_generics decl = |

859 |
match decl.top_decl_desc with |

860 |
| Node nd -> |

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

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

863 |
| ImportedNode nd -> |

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

865 |
| Consts clist -> () |

866 |
| Open _ -> () |

867 | |

868 |
let uneval_prog_generics prog = |

869 |
List.iter uneval_top_generics prog |

870 | |

871 |
let check_env_compat header declared computed = |

872 |
uneval_prog_generics header; |

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

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

875 |
try_semi_unify decl_clock_k computed_c Location.dummy_loc |

876 |
) |

877 |
(* Local Variables: *) |

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

879 |
(* End: *) |