## lustrec / src / clock_calculus.ml @ f22632aa

History | View | Annotate | Download (26.7 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 instanciate_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 instanciate inst_ck_vars inst_cr_vars ck = |

123 |
match ck.cdesc with |

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

125 |
{ck with cdesc = |

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

127 |
(instanciate inst_ck_vars inst_cr_vars ck2))} |

128 |
| Ctuple cklist -> |

129 |
{ck with cdesc = Ctuple |

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

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

132 |
let c' = instanciate_carrier c inst_cr_vars in |

133 |
{ck with cdesc = Con ((instanciate 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 ((instanciate inst_ck_vars inst_cr_vars ck'),k)} |

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

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

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

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

141 |
| Clink ck' -> |

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

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

144 |
let cr' = instanciate_carrier cr inst_cr_vars in |

145 |
{ck with cdesc = |

146 |
Ccarrying (cr',instanciate 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 |
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify |

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

258 |
let rec unify ck1 ck2 = |

259 |
let ck1 = repr ck1 in |

260 |
let ck2 = repr ck2 in |

261 |
if ck1=ck2 then |

262 |
() |

263 |
else |

264 |
let left_const = is_concrete_pck ck1 in |

265 |
let right_const = is_concrete_pck ck2 in |

266 |
if left_const && right_const then |

267 |
unify_static_pck ck1 ck2 |

268 |
else |

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

270 |
| Cvar cset1,Cvar cset2-> |

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

272 |
begin |

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

274 |
update_scope ck2.cscoped ck1; |

275 |
subsume ck1 cset2 |

276 |
end |

277 |
else |

278 |
begin |

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

280 |
update_scope ck1.cscoped ck2; |

281 |
subsume ck2 cset1 |

282 |
end |

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

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

285 |
if (occurs ck1 ck2) then |

286 |
begin |

287 |
if (simplify ck2 = ck1) then |

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

289 |
else |

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

291 |
end |

292 |
else |

293 |
begin |

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

295 |
subsume ck2 cset |

296 |
end |

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

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

299 |
if (occurs ck2 ck1) then |

300 |
begin |

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

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

303 |
else |

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

305 |
end |

306 |
else |

307 |
begin |

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

309 |
subsume ck1 cset |

310 |
end |

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

312 |
subsume ck2 cset; |

313 |
update_scope ck1.cscoped ck2; |

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

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

316 |
subsume ck1 cset; |

317 |
update_scope ck2.cscoped ck1; |

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

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

320 |
unify_carrier cr1 cr2; |

321 |
unify ck1' ck2' |

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

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

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

325 |
unify c1 c1'; unify c2 c2' |

326 |
| Ctuple ckl1, Ctuple ckl2 -> |

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

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

329 |
List.iter2 unify ckl1 ckl2 |

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

331 |
unify_carrier c1 c2; |

332 |
unify ck' ck'' |

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

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

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

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

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

338 |
unify ck1' pck2' |

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

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

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

342 |
unify ck1' pck2' |

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

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

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

346 |
unify ck1' pck2' |

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

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

349 |
unify pck1' ck2' |

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

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

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

353 |
unify pck1' ck2' |

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

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

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

357 |
unify pck1' ck2' |

358 |
(* Corner case for some functions like ite, need to unify guard clock |

359 |
with output clocks *) |

360 |
(* |

361 |
| Ctuple ckl, (Cvar _) -> List.iter (unify ck2) ckl |

362 |
| (Cvar _), Ctuple ckl -> List.iter (unify ck1) ckl |

363 |
*) |

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

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

366 | |

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

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

369 |
let int_factor_of_expr e = |

370 |
match e.expr_desc with |

371 |
| Expr_const |

372 |
(Const_int i) -> i |

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

374 | |

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

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

377 |
let unify_tuple_clock ref_ck_opt ck = |

378 |
let ck_var = ref ref_ck_opt in |

379 |
let rec aux ck = |

380 |
match (repr ck).cdesc with |

381 |
| Con _ |

382 |
| Cvar _ -> |

383 |
begin |

384 |
match !ck_var with |

385 |
| None -> |

386 |
ck_var:=Some ck |

387 |
| Some v -> |

388 |
(* may fail *) |

389 |
unify v ck |

390 |
end |

391 |
| Ctuple cl -> |

392 |
List.iter aux cl |

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

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

395 |
aux ck1 |

396 |
| _ -> () |

397 |
in |

398 |
aux ck |

399 | |

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

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

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

403 |
let unify_imported_clock ref_ck_opt ck = |

404 |
let ck_var = ref ref_ck_opt in |

405 |
let rec aux ck = |

406 |
match (repr ck).cdesc with |

407 |
| Cvar _ -> |

408 |
begin |

409 |
match !ck_var with |

410 |
| None -> |

411 |
ck_var:=Some ck |

412 |
| Some v -> |

413 |
(* cannot fail *) |

414 |
unify v ck |

415 |
end |

416 |
| Ctuple cl -> |

417 |
List.iter aux cl |

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

419 |
aux ck1; aux ck2 |

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

421 |
aux ck1 |

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

423 |
| _ -> () |

424 |
in |

425 |
aux ck |

426 | |

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

428 |
let clock_uncarry ck = |

429 |
let ck = repr ck in |

430 |
match ck.cdesc with |

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

432 |
| _ -> ck |

433 | |

434 |
let try_unify ck1 ck2 loc = |

435 |
try |

436 |
unify ck1 ck2 |

437 |
with |

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

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

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

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

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

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

444 | |

445 |
(* Checks whether ck1 is a subtype of ck2 *) |

446 |
let rec clock_subtyping ck1 ck2 = |

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

448 |
| Ccarrying _ , Ccarrying _ -> unify ck1 ck2 |

449 |
| Ccarrying (cr', ck'), _ -> unify ck' ck2 |

450 |
| _ -> unify ck1 ck2 |

451 | |

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

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

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

455 |
- try to unify these clocks altogether |

456 |
*) |

457 |
let rec clock_standard_args env expr_list = |

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

459 |
let ck_res = new_var true in |

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

461 |
ck_res |

462 | |

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

464 |
used during node application only *) |

465 |
and clock_subtyping_arg env real_arg formal_clock = |

466 |
let loc = real_arg.expr_loc in |

467 |
let real_clock = clock_expr env real_arg in |

468 |
try |

469 |
clock_subtyping real_clock formal_clock |

470 |
with |

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

472 |
raise (Error (loc, Clock_clash (real_clock, formal_clock))) |

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

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

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

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

477 | |

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

479 |
and clock_appl env f args clock_reset loc = |

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

481 |
let cins, couts = split_arrow cfun in |

482 |
let cins = clock_list_of_clock cins in |

483 |
let args = expr_list_of_expr args in |

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

485 |
unify_imported_clock (Some clock_reset) cfun; |

486 |
couts |

487 | |

488 |
and clock_ident nocarrier env id loc = |

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

490 | |

491 |
and clock_carrier env c loc ce = |

492 |
let expr_c = expr_of_ident c loc in |

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

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

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

496 |
try_unify ck ckcarry expr_c.expr_loc; |

497 |
cr |

498 | |

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

500 |
environment [env] *) |

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

502 |
let resulting_ck = |

503 |
match expr.expr_desc with |

504 |
| Expr_const cst -> |

505 |
let ck = new_var true in |

506 |
expr.expr_clock <- ck; |

507 |
ck |

508 |
| Expr_ident v -> |

509 |
let ckv = |

510 |
try |

511 |
Env.lookup_value env v |

512 |
with Not_found -> |

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

514 |
in |

515 |
let ck = instanciate (ref []) (ref []) ckv in |

516 |
expr.expr_clock <- ck; |

517 |
ck |

518 |
| Expr_array elist -> |

519 |
let ck = clock_standard_args env elist in |

520 |
expr.expr_clock <- ck; |

521 |
ck |

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

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

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

525 |
expr.expr_clock <- ck; |

526 |
ck |

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

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

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

530 |
expr.expr_clock <- ck; |

531 |
ck |

532 |
| Expr_tuple elist -> |

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

534 |
expr.expr_clock <- ck; |

535 |
ck |

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

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

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

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

540 |
unify_tuple_clock (Some ck_c) ck; |

541 |
expr.expr_clock <- ck; |

542 |
ck |

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

544 |
(try |

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

546 |
this is also the reset clock ! |

547 |
*) |

548 |
let cr = |

549 |
match r with |

550 |
| None -> new_var true |

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

552 |
let expr_r = expr_of_ident x loc_r in |

553 |
clock_expr env expr_r in |

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

555 |
expr.expr_clock <- couts; |

556 |
couts |

557 |
with exn -> ( |

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

559 |
raise exn |

560 |
)) |

561 |
| Expr_fby (e1,e2) |

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

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

564 |
expr.expr_clock <- ck; |

565 |
ck |

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

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

568 |
expr.expr_clock <- ck; |

569 |
ck |

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

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

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

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

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

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

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

577 |
expr.expr_clock <- ck'; |

578 |
ck |

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

580 |
let cvar = new_var true in |

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

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

583 |
expr.expr_clock <- cvar; |

584 |
cvar |

585 |
| Expr_uclock (e,k) -> |

586 |
let pck = clock_expr env e in |

587 |
if not (can_be_pck pck) then |

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

589 |
if k = 0 then |

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

591 |
(try |

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

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

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

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

596 |
expr.expr_clock <- ck; |

597 |
ck |

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

599 |
let pck = clock_expr env e in |

600 |
if not (can_be_pck pck) then |

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

602 |
if k = 0 then |

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

604 |
(try |

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

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

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

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

609 |
expr.expr_clock <- ck; |

610 |
ck |

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

612 |
let pck = clock_expr env e in |

613 |
if not (can_be_pck pck) then |

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

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

616 |
(try |

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

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

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

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

621 |
expr.expr_clock <- ck; |

622 |
ck |

623 |
in |

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

625 |
resulting_ck |

626 | |

627 |
let clock_of_vlist vars = |

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

629 |
clock_of_clock_list ckl |

630 | |

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

632 |
environment [env] *) |

633 |
let clock_eq env eq = |

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

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

636 |
clock_subtyping_arg env expr_lhs ck_rhs |

637 | |

638 | |

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

640 |
declaration [cck] *) |

641 |
let clock_coreclock env cck id loc scoped = |

642 |
match cck.ck_dec_desc with |

643 |
| Ckdec_any -> new_var scoped |

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

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

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

647 |
ck |

648 |
| Ckdec_bool cl -> |

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

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

651 |
let dummy_id_expr = expr_of_ident id loc in |

652 |
let when_expr = |

653 |
List.fold_left |

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

655 |
{expr_tag = new_tag (); |

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

657 |
expr_type = Types.new_var (); |

658 |
expr_clock = new_var scoped; |

659 |
expr_delay = Delay.new_var (); |

660 |
expr_loc = loc; |

661 |
expr_annot = None}) |

662 |
dummy_id_expr cl |

663 |
in |

664 |
clock_expr temp_env when_expr |

665 | |

666 |
(* Clocks a variable declaration *) |

667 |
let clock_var_decl scoped env vdecl = |

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

669 |
let ck = |

670 |
if vdecl.var_dec_const |

671 |
then |

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

673 |
else |

674 |
match vdecl.var_type.Types.tdesc with |

675 |
| Types.Tclock _ -> new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped |

676 |
| _ -> ck in |

677 |
vdecl.var_clock <- ck; |

678 |
Env.add_value env vdecl.var_id ck |

679 | |

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

681 |
let clock_var_decl_list env scoped l = |

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

683 | |

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

685 |
environment [env]. *) |

686 |
let clock_node env loc nd = |

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

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

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

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

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

692 |
let ck_ins = clock_of_vlist nd.node_inputs in |

693 |
let ck_outs = clock_of_vlist nd.node_outputs in |

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

695 |
unify_imported_clock None ck_node; |

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

697 |
try_generalize ck_node loc; |

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

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

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

701 |
*) |

702 |
nd.node_clock <- ck_node; |

703 |
Env.add_value env nd.node_id ck_node |

704 | |

705 | |

706 |
let check_imported_pclocks loc ck_node = |

707 |
let pck = ref None in |

708 |
let rec aux ck = |

709 |
match ck.cdesc with |

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

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

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

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

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

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

716 |
begin |

717 |
match !pck with |

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

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

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

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

722 |
end |

723 |
| Clink ck' -> aux ck' |

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

725 |
| Cvar _ | Cunivar _ -> |

726 |
match !pck with |

727 |
| None -> () |

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

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

730 |
in |

731 |
aux ck_node |

732 | |

733 |
let clock_imported_node env loc nd = |

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

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

736 |
let ck_ins = clock_of_vlist nd.nodei_inputs in |

737 |
let ck_outs = clock_of_vlist nd.nodei_outputs in |

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

739 |
unify_imported_clock None ck_node; |

740 |
check_imported_pclocks loc ck_node; |

741 |
try_generalize ck_node loc; |

742 |
nd.nodei_clock <- ck_node; |

743 |
Env.add_value env nd.nodei_id ck_node |

744 | |

745 |
let clock_function env loc fcn = |

746 |
let new_env = clock_var_decl_list env false fcn.fun_inputs in |

747 |
ignore(clock_var_decl_list new_env false fcn.fun_outputs); |

748 |
let ck_ins = clock_of_vlist fcn.fun_inputs in |

749 |
let ck_outs = clock_of_vlist fcn.fun_outputs in |

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

751 |
unify_imported_clock None ck_node; |

752 |
check_imported_pclocks loc ck_node; |

753 |
try_generalize ck_node loc; |

754 |
Env.add_value env fcn.fun_id ck_node |

755 | |

756 |
let clock_top_consts env clist = |

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

758 |
let ck = new_var false in |

759 |
try_generalize ck cdecl.const_loc; |

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

761 | |

762 |
let clock_top_decl env decl = |

763 |
match decl.top_decl_desc with |

764 |
| Node nd -> |

765 |
clock_node env decl.top_decl_loc nd |

766 |
| ImportedNode nd -> |

767 |
clock_imported_node env decl.top_decl_loc nd |

768 |
| ImportedFun fcn -> |

769 |
clock_function env decl.top_decl_loc fcn |

770 |
| Consts clist -> |

771 |
clock_top_consts env clist |

772 |
| Open _ -> |

773 |
env |

774 | |

775 |
let clock_prog env decls = |

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

777 | |

778 |
let check_env_compat declared computed = |

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

780 |
let computed_c = Env.lookup_value computed k in |

781 |
try_unify decl_clock_k computed_c Location.dummy_loc |

782 |
) |

783 |
(* Local Variables: *) |

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

785 |
(* End: *) |