## lustrec / src / clock_calculus.ml @ d50b0dc0

History | View | Annotate | Download (32 KB)

1 | e2068500 | Temesghen Kahsai | (********************************************************************) |
---|---|---|---|

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(s) name(s) from clock [ck] *) |
||

445 | let rec clock_uncarry ck = |
||

446 | let ck = repr ck in |
||

447 | match ck.cdesc with |
||

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

449 | | Con(ck', cr, l) -> clock_on (clock_uncarry ck') cr l |
||

450 | | Ctuple ckl -> clock_of_clock_list (List.map clock_uncarry ckl) |
||

451 | | _ -> ck |
||

452 | |||

453 | let try_unify ck1 ck2 loc = |
||

454 | try |
||

455 | unify ck1 ck2 |
||

456 | with |
||

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

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

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

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

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

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

463 | |||

464 | let try_semi_unify ck1 ck2 loc = |
||

465 | try |
||

466 | semi_unify ck1 ck2 |
||

467 | with |
||

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

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

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

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

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

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

474 | |||

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

476 | let rec sub_unify sub ck1 ck2 = |
||

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

478 | | Ctuple cl1 , Ctuple cl2 -> |
||

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

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

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

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

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

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

485 | begin |
||

486 | unify_carrier cr1 cr2; |
||

487 | sub_unify sub c1 c2 |
||

488 | end |
||

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

490 | begin |
||

491 | unify_carrier cr1 cr2; |
||

492 | sub_unify sub c1 c2 |
||

493 | end |
||

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

495 | | _ -> unify ck1 ck2 |
||

496 | |||

497 | let try_sub_unify sub ck1 ck2 loc = |
||

498 | try |
||

499 | sub_unify sub ck1 ck2 |
||

500 | with |
||

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

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

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

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

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

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

507 | |||

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

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

510 | let unify_tuple_clock ref_ck_opt ck loc = |
||

511 | (*(match ref_ck_opt with |
||

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

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

514 | let ck_var = ref ref_ck_opt in |
||

515 | let rec aux ck = |
||

516 | match (repr ck).cdesc with |
||

517 | | Con _ |
||

518 | | Cvar _ -> |
||

519 | begin |
||

520 | match !ck_var with |
||

521 | | None -> |
||

522 | ck_var:=Some ck |
||

523 | | Some v -> |
||

524 | (* may fail *) |
||

525 | try_unify ck v loc |
||

526 | end |
||

527 | | Ctuple cl -> |
||

528 | List.iter aux cl |
||

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

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

531 | aux ck1 |
||

532 | | _ -> () |
||

533 | in aux ck |
||

534 | |||

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

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

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

538 | let unify_imported_clock ref_ck_opt ck loc = |
||

539 | let ck_var = ref ref_ck_opt in |
||

540 | let rec aux ck = |
||

541 | match (repr ck).cdesc with |
||

542 | | Cvar _ -> |
||

543 | begin |
||

544 | match !ck_var with |
||

545 | | None -> |
||

546 | ck_var:=Some ck |
||

547 | | Some v -> |
||

548 | (* cannot fail *) |
||

549 | try_unify ck v loc |
||

550 | end |
||

551 | | Ctuple cl -> |
||

552 | List.iter aux cl |
||

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

554 | aux ck1; aux ck2 |
||

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

556 | aux ck1 |
||

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

558 | | _ -> () |
||

559 | in |
||

560 | aux ck |
||

561 | |||

562 | (* Computes the root clock of a tuple or a node clock, |
||

563 | which is not the same as the base clock. |
||

564 | Root clock will be used as the call clock |
||

565 | of a given node instance *) |
||

566 | let compute_root_clock ck = |
||

567 | let root = Clocks.root ck in |
||

568 | let branch = ref None in |
||

569 | let rec aux ck = |
||

570 | match (repr ck).cdesc with |
||

571 | | Ctuple cl -> |
||

572 | List.iter aux cl |
||

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

574 | aux ck1; aux ck2 |
||

575 | | _ -> |
||

576 | begin |
||

577 | match !branch with |
||

578 | | None -> |
||

579 | branch := Some (Clocks.branch ck) |
||

580 | | Some br -> |
||

581 | (* cannot fail *) |
||

582 | branch := Some (Clocks.common_prefix br (Clocks.branch ck)) |
||

583 | end |
||

584 | in |
||

585 | begin |
||

586 | aux ck; |
||

587 | Clocks.clock_of_root_branch root (Utils.desome !branch) |
||

588 | end |
||

589 | |||

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

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

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

593 | - try to unify these clocks altogether |
||

594 | *) |
||

595 | let rec clock_standard_args env expr_list = |
||

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

597 | let ck_res = new_var true in |
||

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

599 | ck_res |
||

600 | |||

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

602 | used during node application only *) |
||

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

604 | let loc = real_arg.expr_loc in |
||

605 | let real_clock = clock_expr env real_arg in |
||

606 | try_sub_unify sub formal_clock real_clock loc |
||

607 | |||

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

609 | and clock_appl env f args clock_reset loc = |
||

610 | let args = expr_list_of_expr args in |
||

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

612 | then |
||

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

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

615 | else |
||

616 | clock_call env f args clock_reset loc |
||

617 | |||

618 | and clock_call env f args clock_reset loc = |
||

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

620 | let cins, couts = split_arrow cfun in |
||

621 | let cins = clock_list_of_clock cins in |
||

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

623 | unify_imported_clock (Some clock_reset) cfun loc; |
||

624 | couts |
||

625 | |||

626 | and clock_ident nocarrier env id loc = |
||

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

628 | |||

629 | and clock_carrier env c loc ce = |
||

630 | let expr_c = expr_of_ident c loc in |
||

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

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

633 | let ckb = new_var true in |
||

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

635 | try_unify ck ckcarry expr_c.expr_loc; |
||

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

637 | cr |
||

638 | |||

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

640 | environment [env] *) |
||

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

642 | let resulting_ck = |
||

643 | match expr.expr_desc with |
||

644 | | Expr_const cst -> |
||

645 | let ck = new_var true in |
||

646 | expr.expr_clock <- ck; |
||

647 | ck |
||

648 | | Expr_ident v -> |
||

649 | let ckv = |
||

650 | try |
||

651 | Env.lookup_value env v |
||

652 | with Not_found -> |
||

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

654 | in |
||

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

656 | expr.expr_clock <- ck; |
||

657 | ck |
||

658 | | Expr_array elist -> |
||

659 | let ck = clock_standard_args env elist in |
||

660 | expr.expr_clock <- ck; |
||

661 | ck |
||

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

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

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

665 | expr.expr_clock <- ck; |
||

666 | ck |
||

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

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

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

670 | expr.expr_clock <- ck; |
||

671 | ck |
||

672 | | Expr_tuple elist -> |
||

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

674 | expr.expr_clock <- ck; |
||

675 | ck |
||

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

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

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

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

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

681 | expr.expr_clock <- ck; |
||

682 | ck |
||

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

684 | (try |
||

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

686 | this is also the reset clock ! |
||

687 | *) |
||

688 | let cr = |
||

689 | match r with |
||

690 | | None -> new_var true |
||

691 | | Some c -> clock_standard_args env [c] in |
||

692 | let couts = clock_appl env id args (clock_uncarry cr) expr.expr_loc in |
||

693 | expr.expr_clock <- couts; |
||

694 | couts |
||

695 | with exn -> ( |
||

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

697 | raise exn |
||

698 | )) |
||

699 | | Expr_fby (e1,e2) |
||

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

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

702 | unify_tuple_clock None ck expr.expr_loc; |
||

703 | expr.expr_clock <- ck; |
||

704 | ck |
||

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

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

707 | expr.expr_clock <- ck; |
||

708 | ck |
||

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

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

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

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

713 | let ck = clock_on ce cr l in |
||

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

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

716 | expr.expr_clock <- ck'; |
||

717 | ck |
||

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

719 | let cvar = new_var true in |
||

720 | let crvar = new_carrier Carry_name true in |
||

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

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

723 | try_unify_carrier cr crvar expr.expr_loc; |
||

724 | let cres = clock_current ((snd (List.hd hl)).expr_clock) in |
||

725 | expr.expr_clock <- cres; |
||

726 | cres |
||

727 | in |
||

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

729 | resulting_ck |
||

730 | |||

731 | let clock_of_vlist vars = |
||

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

733 | clock_of_clock_list ckl |
||

734 | |||

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

736 | environment [env] *) |
||

737 | let clock_eq env eq = |
||

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

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

740 | clock_subtyping_arg env expr_lhs ck_rhs |
||

741 | |||

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

743 | declaration [cck] *) |
||

744 | let clock_coreclock env cck id loc scoped = |
||

745 | match cck.ck_dec_desc with |
||

746 | | Ckdec_any -> new_var scoped |
||

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

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

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

750 | ck |
||

751 | | Ckdec_bool cl -> |
||

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

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

754 | let dummy_id_expr = expr_of_ident id loc in |
||

755 | let when_expr = |
||

756 | List.fold_left |
||

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

758 | {expr_tag = new_tag (); |
||

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

760 | expr_type = Types.new_var (); |
||

761 | expr_clock = new_var scoped; |
||

762 | expr_delay = Delay.new_var (); |
||

763 | expr_loc = loc; |
||

764 | expr_annot = None}) |
||

765 | dummy_id_expr cl |
||

766 | in |
||

767 | clock_expr temp_env when_expr |
||

768 | |||

769 | (* Clocks a variable declaration *) |
||

770 | let clock_var_decl scoped env vdecl = |
||

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

772 | let ck = |
||

773 | (* WTF ???? |
||

774 | if vdecl.var_dec_const |
||

775 | then |
||

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

777 | else |
||

778 | *) |
||

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

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

781 | else ck in |
||

782 | d50b0dc0 | Temesghen Kahsai | (if vdecl.var_dec_const |

783 | then match vdecl.var_dec_value with |
||

784 | | None -> () |
||

785 | | Some v -> |
||

786 | begin |
||

787 | let ck_static = clock_expr env v in |
||

788 | try_unify ck ck_static v.expr_loc |
||

789 | end); |
||

790 | try_unify ck vdecl.var_clock vdecl.var_loc; |
||

791 | e2068500 | Temesghen Kahsai | Env.add_value env vdecl.var_id ck |

792 | |||

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

794 | let clock_var_decl_list env scoped l = |
||

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

796 | |||

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

798 | environment [env]. |
||

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

800 | - generalize inputs (unscoped). |
||

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

802 | are allowed to be generalized. |
||

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

804 | they can be generalized. |
||

805 | *) |
||

806 | let clock_node env loc nd = |
||

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

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

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

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

811 | List.iter (clock_eq new_env) (get_node_eqs nd); |
||

812 | let ck_ins = clock_of_vlist nd.node_inputs in |
||

813 | let ck_outs = clock_of_vlist nd.node_outputs in |
||

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

815 | unify_imported_clock None ck_node loc; |
||

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

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

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

819 | try_generalize ck_node loc; |
||

820 | (* |
||

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

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

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

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

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

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

827 | *) |
||

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

829 | nd.node_clock <- ck_node; |
||

830 | Env.add_value env nd.node_id ck_node |
||

831 | |||

832 | |||

833 | let check_imported_pclocks loc ck_node = |
||

834 | let pck = ref None in |
||

835 | let rec aux ck = |
||

836 | match ck.cdesc with |
||

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

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

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

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

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

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

843 | begin |
||

844 | match !pck with |
||

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

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

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

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

849 | end |
||

850 | | Clink ck' -> aux ck' |
||

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

852 | | Cvar _ | Cunivar _ -> |
||

853 | match !pck with |
||

854 | | None -> () |
||

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

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

857 | in |
||

858 | aux ck_node |
||

859 | |||

860 | let clock_imported_node env loc nd = |
||

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

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

863 | let ck_ins = clock_of_vlist nd.nodei_inputs in |
||

864 | let ck_outs = clock_of_vlist nd.nodei_outputs in |
||

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

866 | unify_imported_clock None ck_node loc; |
||

867 | check_imported_pclocks loc ck_node; |
||

868 | try_generalize ck_node loc; |
||

869 | nd.nodei_clock <- ck_node; |
||

870 | Env.add_value env nd.nodei_id ck_node |
||

871 | |||

872 | let clock_top_const env cdecl= |
||

873 | let ck = new_var false in |
||

874 | try_generalize ck cdecl.const_loc; |
||

875 | Env.add_value env cdecl.const_id ck |
||

876 | |||

877 | let clock_top_consts env clist = |
||

878 | List.fold_left clock_top_const env clist |
||

879 | |||

880 | let rec clock_top_decl env decl = |
||

881 | match decl.top_decl_desc with |
||

882 | | Node nd -> |
||

883 | clock_node env decl.top_decl_loc nd |
||

884 | | ImportedNode nd -> |
||

885 | clock_imported_node env decl.top_decl_loc nd |
||

886 | | Const c -> |
||

887 | clock_top_const env c |
||

888 | | TypeDef _ -> List.fold_left clock_top_decl env (consts_of_enum_type decl) |
||

889 | | Open _ -> env |
||

890 | |||

891 | let clock_prog env decls = |
||

892 | List.fold_left clock_top_decl env decls |
||

893 | |||

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

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

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

897 | |||

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

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

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

901 | *) |
||

902 | let uneval_vdecl_generics vdecl = |
||

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

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

905 | then |
||

906 | match get_carrier_name vdecl.var_clock with |
||

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

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

909 | |||

910 | let uneval_node_generics vdecls = |
||

911 | List.iter uneval_vdecl_generics vdecls |
||

912 | |||

913 | let uneval_top_generics decl = |
||

914 | match decl.top_decl_desc with |
||

915 | | Node nd -> |
||

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

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

918 | | ImportedNode nd -> |
||

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

920 | | Const _ |
||

921 | | Open _ |
||

922 | | TypeDef _ -> () |
||

923 | |||

924 | let uneval_prog_generics prog = |
||

925 | List.iter uneval_top_generics prog |
||

926 | |||

927 | let check_env_compat header declared computed = |
||

928 | uneval_prog_generics header; |
||

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

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

931 | try_semi_unify decl_clock_k computed_c Location.dummy_loc |
||

932 | ) |
||

933 | (* Local Variables: *) |
||

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

935 | (* End: *) |