## lustrec / src / clock_calculus.ml @ e7cc5186

History | View | Annotate | Download (26.6 KB)

1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|

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 | 22fe1c93 | ploc | |

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 | 45f0f48d | xthirioux | | Cvar -> ck=cvar |

46 | | Cunivar -> false |
||

47 | 22fe1c93 | ploc | | Clink ck' -> occurs cvar ck' |

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

49 | |||

50 | (* Clocks generalization *) |
||

51 | let rec generalize_carrier cr = |
||

52 | match cr.carrier_desc with |
||

53 | | Carry_const _ |
||

54 | | Carry_name -> |
||

55 | if cr.carrier_scoped then |
||

56 | raise (Scope_carrier cr); |
||

57 | cr.carrier_desc <- Carry_var |
||

58 | | Carry_var -> () |
||

59 | | Carry_link cr' -> generalize_carrier cr' |
||

60 | |||

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

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

63 | let rec generalize ck = |
||

64 | match ck.cdesc with |
||

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

66 | generalize ck1; generalize ck2 |
||

67 | | Ctuple clist -> |
||

68 | List.iter generalize clist |
||

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

70 | 45f0f48d | xthirioux | | Cvar -> |

71 | 22fe1c93 | ploc | if ck.cscoped then |

72 | raise (Scope_clock ck); |
||

73 | 45f0f48d | xthirioux | ck.cdesc <- Cunivar |

74 | | Cunivar -> () |
||

75 | 22fe1c93 | ploc | | Clink ck' -> |

76 | generalize ck' |
||

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

78 | generalize_carrier cr; generalize ck' |
||

79 | |||

80 | let try_generalize ck_node loc = |
||

81 | try |
||

82 | generalize ck_node |
||

83 | with (Scope_carrier cr) -> |
||

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

85 | | (Scope_clock ck) -> |
||

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

87 | |||

88 | (* Clocks instanciation *) |
||

89 | 7291cb80 | xthirioux | let instantiate_carrier cr inst_cr_vars = |

90 | 22fe1c93 | ploc | let cr = carrier_repr cr in |

91 | match cr.carrier_desc with |
||

92 | | Carry_const _ |
||

93 | | Carry_name -> cr |
||

94 | | Carry_link _ -> |
||

95 | failwith "Internal error" |
||

96 | | Carry_var -> |
||

97 | try |
||

98 | List.assoc cr.carrier_id !inst_cr_vars |
||

99 | with Not_found -> |
||

100 | let cr_var = new_carrier Carry_name true in |
||

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

102 | cr_var |
||

103 | |||

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

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

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

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

108 | 7291cb80 | xthirioux | let rec instantiate inst_ck_vars inst_cr_vars ck = |

109 | 22fe1c93 | ploc | match ck.cdesc with |

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

111 | {ck with cdesc = |
||

112 | 7291cb80 | xthirioux | Carrow ((instantiate inst_ck_vars inst_cr_vars ck1), |

113 | (instantiate inst_ck_vars inst_cr_vars ck2))} |
||

114 | 22fe1c93 | ploc | | Ctuple cklist -> |

115 | {ck with cdesc = Ctuple |
||

116 | 7291cb80 | xthirioux | (List.map (instantiate inst_ck_vars inst_cr_vars) cklist)} |

117 | 22fe1c93 | ploc | | Con (ck',c,l) -> |

118 | 7291cb80 | xthirioux | let c' = instantiate_carrier c inst_cr_vars in |

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

120 | 45f0f48d | xthirioux | | Cvar -> ck |

121 | 22fe1c93 | ploc | | Clink ck' -> |

122 | 7291cb80 | xthirioux | {ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')} |

123 | 22fe1c93 | ploc | | Ccarrying (cr,ck') -> |

124 | 7291cb80 | xthirioux | let cr' = instantiate_carrier cr inst_cr_vars in |

125 | 22fe1c93 | ploc | {ck with cdesc = |

126 | 7291cb80 | xthirioux | Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')} |

127 | 45f0f48d | xthirioux | | Cunivar -> |

128 | 22fe1c93 | ploc | try |

129 | List.assoc ck.cid !inst_ck_vars |
||

130 | with Not_found -> |
||

131 | 45f0f48d | xthirioux | let var = new_ck Cvar true in |

132 | 22fe1c93 | ploc | inst_ck_vars := (ck.cid, var)::!inst_ck_vars; |

133 | var |
||

134 | |||

135 | |||

136 | let rec update_scope_carrier scoped cr = |
||

137 | if (not scoped) then |
||

138 | begin |
||

139 | cr.carrier_scoped <- scoped; |
||

140 | match cr.carrier_desc with |
||

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

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

143 | end |
||

144 | |||

145 | let rec update_scope scoped ck = |
||

146 | if (not scoped) then |
||

147 | begin |
||

148 | ck.cscoped <- scoped; |
||

149 | match ck.cdesc with |
||

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

151 | update_scope scoped ck1; update_scope scoped ck2 |
||

152 | | Ctuple clist -> |
||

153 | List.iter (update_scope scoped) clist |
||

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

155 | 45f0f48d | xthirioux | | Cvar | Cunivar -> () |

156 | 22fe1c93 | ploc | | Clink ck' -> |

157 | update_scope scoped ck' |
||

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

159 | update_scope_carrier scoped cr; update_scope scoped ck' |
||

160 | end |
||

161 | |||

162 | |||

163 | (* Unifies two clock carriers *) |
||

164 | let unify_carrier cr1 cr2 = |
||

165 | let cr1 = carrier_repr cr1 in |
||

166 | let cr2 = carrier_repr cr2 in |
||

167 | 8a183477 | xthirioux | if cr1==cr2 then () |

168 | 22fe1c93 | ploc | else |

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

170 | | Carry_const id1, Carry_const id2 -> |
||

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

172 | | Carry_const _, Carry_name -> |
||

173 | begin |
||

174 | cr2.carrier_desc <- Carry_link cr1; |
||

175 | update_scope_carrier cr2.carrier_scoped cr1 |
||

176 | end |
||

177 | | Carry_name, Carry_const _ -> |
||

178 | begin |
||

179 | cr1.carrier_desc <- Carry_link cr2; |
||

180 | update_scope_carrier cr1.carrier_scoped cr2 |
||

181 | end |
||

182 | | Carry_name, Carry_name -> |
||

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

184 | begin |
||

185 | cr2.carrier_desc <- Carry_link cr1; |
||

186 | update_scope_carrier cr2.carrier_scoped cr1 |
||

187 | end |
||

188 | else |
||

189 | begin |
||

190 | cr1.carrier_desc <- Carry_link cr2; |
||

191 | update_scope_carrier cr1.carrier_scoped cr2 |
||

192 | end |
||

193 | 8f1c7e91 | xthirioux | | _,_ -> assert false |

194 | |||

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

196 | let semi_unify_carrier cr1 cr2 = |
||

197 | let cr1 = carrier_repr cr1 in |
||

198 | let cr2 = carrier_repr cr2 in |
||

199 | 8a183477 | xthirioux | if cr1==cr2 then () |

200 | 8f1c7e91 | xthirioux | else |

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

202 | | Carry_const id1, Carry_const id2 -> |
||

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

204 | | Carry_const _, Carry_name -> |
||

205 | begin |
||

206 | cr2.carrier_desc <- Carry_link cr1; |
||

207 | update_scope_carrier cr2.carrier_scoped cr1 |
||

208 | end |
||

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

210 | | Carry_name, Carry_name -> |
||

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

212 | begin |
||

213 | cr2.carrier_desc <- Carry_link cr1; |
||

214 | update_scope_carrier cr2.carrier_scoped cr1 |
||

215 | end |
||

216 | else |
||

217 | begin |
||

218 | cr1.carrier_desc <- Carry_link cr2; |
||

219 | update_scope_carrier cr1.carrier_scoped cr2 |
||

220 | end |
||

221 | | _,_ -> assert false |
||

222 | 22fe1c93 | ploc | |

223 | 6fdfb60b | xthirioux | let try_unify_carrier ck1 ck2 loc = |

224 | try |
||

225 | unify_carrier ck1 ck2 |
||

226 | with |
||

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

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

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

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

231 | |||

232 | 22fe1c93 | ploc | (** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify |

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

234 | let rec unify ck1 ck2 = |
||

235 | let ck1 = repr ck1 in |
||

236 | let ck2 = repr ck2 in |
||

237 | 8a183477 | xthirioux | if ck1==ck2 then |

238 | 22fe1c93 | ploc | () |

239 | else |
||

240 | 45f0f48d | xthirioux | match ck1.cdesc,ck2.cdesc with |

241 | | Cvar, Cvar -> |
||

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

243 | begin |
||

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

245 | update_scope ck2.cscoped ck1 |
||

246 | end |
||

247 | else |
||

248 | begin |
||

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

250 | update_scope ck1.cscoped ck2 |
||

251 | end |
||

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

253 | update_scope ck1.cscoped ck2; |
||

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

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

256 | update_scope ck2.cscoped ck1; |
||

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

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

259 | unify_carrier cr1 cr2; |
||

260 | unify ck1' ck2' |
||

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

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

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

264 | unify c1 c1'; unify c2 c2' |
||

265 | | Ctuple ckl1, Ctuple ckl2 -> |
||

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

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

268 | List.iter2 unify ckl1 ckl2 |
||

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

270 | unify_carrier c1 c2; |
||

271 | unify ck' ck'' |
||

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

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

274 | 8f1c7e91 | xthirioux | |

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

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

277 | let rec semi_unify ck1 ck2 = |
||

278 | let ck1 = repr ck1 in |
||

279 | let ck2 = repr ck2 in |
||

280 | 8a183477 | xthirioux | if ck1==ck2 then |

281 | 8f1c7e91 | xthirioux | () |

282 | else |
||

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

284 | 45f0f48d | xthirioux | | Cvar, Cvar -> |

285 | 8f1c7e91 | xthirioux | if ck1.cid < ck2.cid then |

286 | begin |
||

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

288 | update_scope ck2.cscoped ck1 |
||

289 | end |
||

290 | else |
||

291 | begin |
||

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

293 | update_scope ck1.cscoped ck2 |
||

294 | end |
||

295 | 45f0f48d | xthirioux | | (Cvar, _) -> raise (Unify (ck1,ck2)) |

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

297 | 8f1c7e91 | xthirioux | update_scope ck2.cscoped ck1; |

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

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

300 | semi_unify_carrier cr1 cr2; |
||

301 | semi_unify ck1' ck2' |
||

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

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

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

305 | begin |
||

306 | semi_unify c1 c1'; |
||

307 | semi_unify c2 c2' |
||

308 | end |
||

309 | | Ctuple ckl1, Ctuple ckl2 -> |
||

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

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

312 | List.iter2 semi_unify ckl1 ckl2 |
||

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

314 | semi_unify_carrier c1 c2; |
||

315 | semi_unify ck' ck'' |
||

316 | 45f0f48d | xthirioux | | Cunivar, _ | _, Cunivar -> () |

317 | 22fe1c93 | ploc | | _,_ -> raise (Unify (ck1,ck2)) |

318 | |||

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

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

321 | let int_factor_of_expr e = |
||

322 | match e.expr_desc with |
||

323 | | Expr_const |
||

324 | (Const_int i) -> i |
||

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

326 | |||

327 | 54d032f5 | xthirioux | (** [clock_uncarry ck] drops the possible carrier(s) name(s) from clock [ck] *) |

328 | let rec clock_uncarry ck = |
||

329 | 22fe1c93 | ploc | let ck = repr ck in |

330 | match ck.cdesc with |
||

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

332 | 54d032f5 | xthirioux | | Con(ck', cr, l) -> clock_on (clock_uncarry ck') cr l |

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

334 | 22fe1c93 | ploc | | _ -> ck |

335 | |||

336 | let try_unify ck1 ck2 loc = |
||

337 | try |
||

338 | unify ck1 ck2 |
||

339 | with |
||

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

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

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

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

344 | |||

345 | 8f1c7e91 | xthirioux | let try_semi_unify ck1 ck2 loc = |

346 | try |
||

347 | semi_unify ck1 ck2 |
||

348 | with |
||

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

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

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

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

353 | |||

354 | 6fdfb60b | xthirioux | (* ck2 is a subtype of ck1 *) |

355 | 52cfee34 | xthirioux | let rec sub_unify sub ck1 ck2 = |

356 | 22fe1c93 | ploc | match (repr ck1).cdesc, (repr ck2).cdesc with |

357 | 52cfee34 | xthirioux | | Ctuple cl1 , Ctuple cl2 -> |

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

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

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

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

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

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

364 | begin |
||

365 | unify_carrier cr1 cr2; |
||

366 | sub_unify sub c1 c2 |
||

367 | end |
||

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

369 | begin |
||

370 | unify_carrier cr1 cr2; |
||

371 | sub_unify sub c1 c2 |
||

372 | end |
||

373 | 6fdfb60b | xthirioux | | _, Ccarrying (_, c2) when sub -> sub_unify sub ck1 c2 |

374 | 52cfee34 | xthirioux | | _ -> unify ck1 ck2 |

375 | |||

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

377 | try |
||

378 | sub_unify sub ck1 ck2 |
||

379 | with |
||

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

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

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

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

384 | 22fe1c93 | ploc | |

385 | 45c13277 | xthirioux | (* Unifies all the clock variables in the clock type of a tuple |

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

387 | let unify_tuple_clock ref_ck_opt ck loc = |
||

388 | 6fdfb60b | xthirioux | (*(match ref_ck_opt with |

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

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

391 | 45c13277 | xthirioux | let ck_var = ref ref_ck_opt in |

392 | let rec aux ck = |
||

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

394 | | Con _ |
||

395 | 45f0f48d | xthirioux | | Cvar -> |

396 | 45c13277 | xthirioux | begin |

397 | match !ck_var with |
||

398 | | None -> |
||

399 | ck_var:=Some ck |
||

400 | | Some v -> |
||

401 | (* may fail *) |
||

402 | 6fdfb60b | xthirioux | try_unify ck v loc |

403 | 45c13277 | xthirioux | end |

404 | | Ctuple cl -> |
||

405 | List.iter aux cl |
||

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

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

408 | aux ck1 |
||

409 | | _ -> () |
||

410 | 6fdfb60b | xthirioux | in aux ck |

411 | 45c13277 | xthirioux | |

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

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

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

415 | let unify_imported_clock ref_ck_opt ck loc = |
||

416 | let ck_var = ref ref_ck_opt in |
||

417 | let rec aux ck = |
||

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

419 | 45f0f48d | xthirioux | | Cvar -> |

420 | 45c13277 | xthirioux | begin |

421 | match !ck_var with |
||

422 | | None -> |
||

423 | ck_var:=Some ck |
||

424 | | Some v -> |
||

425 | (* cannot fail *) |
||

426 | 6fdfb60b | xthirioux | try_unify ck v loc |

427 | 45c13277 | xthirioux | end |

428 | | Ctuple cl -> |
||

429 | List.iter aux cl |
||

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

431 | aux ck1; aux ck2 |
||

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

433 | aux ck1 |
||

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

435 | | _ -> () |
||

436 | in |
||

437 | aux ck |
||

438 | |||

439 | 54d032f5 | xthirioux | (* Computes the root clock of a tuple or a node clock, |

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

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

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

443 | let compute_root_clock ck = |
||

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

445 | let branch = ref None in |
||

446 | let rec aux ck = |
||

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

448 | | Ctuple cl -> |
||

449 | List.iter aux cl |
||

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

451 | aux ck1; aux ck2 |
||

452 | | _ -> |
||

453 | begin |
||

454 | match !branch with |
||

455 | | None -> |
||

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

457 | | Some br -> |
||

458 | (* cannot fail *) |
||

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

460 | end |
||

461 | in |
||

462 | begin |
||

463 | aux ck; |
||

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

465 | end |
||

466 | |||

467 | 22fe1c93 | ploc | (* Clocks a list of arguments of Lustre builtin operators: |

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

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

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

471 | *) |
||

472 | let rec clock_standard_args env expr_list = |
||

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

474 | let ck_res = new_var true in |
||

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

476 | ck_res |
||

477 | |||

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

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

480 | 52cfee34 | xthirioux | and clock_subtyping_arg env ?(sub=true) real_arg formal_clock = |

481 | 22fe1c93 | ploc | let loc = real_arg.expr_loc in |

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

483 | 74f1d8d3 | xthirioux | try_sub_unify sub formal_clock real_clock loc |

484 | 22fe1c93 | ploc | |

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

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

487 | b616fe7a | xthirioux | let args = expr_list_of_expr args in |

488 | 04a63d25 | xthirioux | if Basic_library.is_homomorphic_fun f && List.exists is_tuple_expr args |

489 | b616fe7a | xthirioux | then |

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

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

492 | else |
||

493 | clock_call env f args clock_reset loc |
||

494 | |||

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

496 | 22fe1c93 | ploc | let cfun = clock_ident false env f loc in |

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

498 | let cins = clock_list_of_clock cins in |
||

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

500 | 45c13277 | xthirioux | unify_imported_clock (Some clock_reset) cfun loc; |

501 | 22fe1c93 | ploc | couts |

502 | |||

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

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

505 | |||

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

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

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

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

510 | 6fdfb60b | xthirioux | let ckb = new_var true in |

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

512 | 22fe1c93 | ploc | try_unify ck ckcarry expr_c.expr_loc; |

513 | 6fdfb60b | xthirioux | unify_tuple_clock (Some ckb) ce expr_c.expr_loc; |

514 | cr |
||

515 | 22fe1c93 | ploc | |

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

517 | environment [env] *) |
||

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

519 | let resulting_ck = |
||

520 | match expr.expr_desc with |
||

521 | | Expr_const cst -> |
||

522 | let ck = new_var true in |
||

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

524 | ck |
||

525 | | Expr_ident v -> |
||

526 | let ckv = |
||

527 | try |
||

528 | Env.lookup_value env v |
||

529 | with Not_found -> |
||

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

531 | in |
||

532 | 7291cb80 | xthirioux | let ck = instantiate (ref []) (ref []) ckv in |

533 | 22fe1c93 | ploc | expr.expr_clock <- ck; |

534 | ck |
||

535 | | Expr_array elist -> |
||

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

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

538 | ck |
||

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

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

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

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

543 | ck |
||

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

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

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

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

548 | ck |
||

549 | | Expr_tuple elist -> |
||

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

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

552 | ck |
||

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

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

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

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

557 | 45c13277 | xthirioux | unify_tuple_clock (Some ck_c) ck expr.expr_loc; |

558 | 22fe1c93 | ploc | expr.expr_clock <- ck; |

559 | ck |
||

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

561 | (try |
||

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

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

564 | *) |
||

565 | let cr = |
||

566 | match r with |
||

567 | | None -> new_var true |
||

568 | 54d032f5 | xthirioux | | Some c -> clock_standard_args env [c] in |

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

570 | 22fe1c93 | ploc | expr.expr_clock <- couts; |

571 | couts |
||

572 | with exn -> ( |
||

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

574 | raise exn |
||

575 | )) |
||

576 | | Expr_fby (e1,e2) |
||

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

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

579 | 45c13277 | xthirioux | unify_tuple_clock None ck expr.expr_loc; |

580 | 22fe1c93 | ploc | expr.expr_clock <- ck; |

581 | ck |
||

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

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

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

585 | ck |
||

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

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

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

589 | 6fdfb60b | xthirioux | let cr = clock_carrier env c c_loc ce in |

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

591 | 22fe1c93 | ploc | let cr' = new_carrier (Carry_const c) ck.cscoped in |

592 | 6fdfb60b | xthirioux | let ck' = clock_on ce cr' l in |

593 | 22fe1c93 | ploc | expr.expr_clock <- ck'; |

594 | ck |
||

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

596 | let cvar = new_var true in |
||

597 | 6fdfb60b | xthirioux | let crvar = new_carrier Carry_name true in |

598 | 54d032f5 | xthirioux | 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; |

599 | 6fdfb60b | xthirioux | let cr = clock_carrier env c expr.expr_loc cvar in |

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

601 | 54d032f5 | xthirioux | let cres = clock_current ((snd (List.hd hl)).expr_clock) in |

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

603 | cres |
||

604 | 22fe1c93 | ploc | in |

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

606 | 22fe1c93 | ploc | resulting_ck |

607 | |||

608 | let clock_of_vlist vars = |
||

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

610 | clock_of_clock_list ckl |
||

611 | |||

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

613 | environment [env] *) |
||

614 | let clock_eq env eq = |
||

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

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

617 | clock_subtyping_arg env expr_lhs ck_rhs |
||

618 | |||

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

620 | declaration [cck] *) |
||

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

622 | match cck.ck_dec_desc with |
||

623 | | Ckdec_any -> new_var scoped |
||

624 | | Ckdec_bool cl -> |
||

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

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

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

628 | let when_expr = |
||

629 | List.fold_left |
||

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

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

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

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

634 | expr_clock = new_var scoped; |
||

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

636 | expr_loc = loc; |
||

637 | expr_annot = None}) |
||

638 | dummy_id_expr cl |
||

639 | in |
||

640 | clock_expr temp_env when_expr |
||

641 | |||

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

643 | let clock_var_decl scoped env vdecl = |
||

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

645 | 89b9e25c | xthirioux | let ck = |

646 | (* WTF ???? |
||

647 | 22fe1c93 | ploc | if vdecl.var_dec_const |

648 | then |
||

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

650 | else |
||

651 | 89b9e25c | xthirioux | *) |

652 | 6afa892a | xthirioux | if Types.get_clock_base_type vdecl.var_type <> None |

653 | 89b9e25c | xthirioux | then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped |

654 | else ck in |
||

655 | ec433d69 | xthirioux | (if vdecl.var_dec_const |

656 | then match vdecl.var_dec_value with |
||

657 | | None -> () |
||

658 | | Some v -> |
||

659 | begin |
||

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

661 | try_unify ck ck_static v.expr_loc |
||

662 | end); |
||

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

664 | 22fe1c93 | ploc | Env.add_value env vdecl.var_id ck |

665 | |||

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

667 | let clock_var_decl_list env scoped l = |
||

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

669 | |||

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

671 | 89b9e25c | xthirioux | environment [env]. |

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

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

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

675 | are allowed to be generalized. |
||

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

677 | they can be generalized. |
||

678 | *) |
||

679 | 22fe1c93 | ploc | let clock_node env loc nd = |

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

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

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

683 | d4807c3d | xthirioux | let new_env = clock_var_decl_list new_env true nd.node_locals in |

684 | b08ffca7 | xthirioux | List.iter (clock_eq new_env) (get_node_eqs nd); |

685 | 22fe1c93 | ploc | let ck_ins = clock_of_vlist nd.node_inputs in |

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

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

688 | 45c13277 | xthirioux | unify_imported_clock None ck_node loc; |

689 | 52cfee34 | xthirioux | Log.report ~level:3 (fun fmt -> print_ck fmt ck_node); |

690 | 89b9e25c | xthirioux | (* Local variables may contain first-order carrier variables that should be generalized. |

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

692 | 6afa892a | xthirioux | try_generalize ck_node loc; |

693 | (* |
||

694 | 89b9e25c | xthirioux | List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs; |

695 | 6afa892a | xthirioux | List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*) |

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

697 | 22fe1c93 | ploc | (* TODO : Xavier pourquoi ai je cette erreur ? *) |

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

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

700 | *) |
||

701 | 52cfee34 | xthirioux | Log.report ~level:3 (fun fmt -> print_ck fmt ck_node); |

702 | 22fe1c93 | ploc | 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 | | Clink ck' -> aux ck' |
||

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

715 | 45f0f48d | xthirioux | | Cvar | Cunivar -> |

716 | 22fe1c93 | ploc | match !pck with |

717 | | None -> () |
||

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

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

720 | in |
||

721 | aux ck_node |
||

722 | |||

723 | let clock_imported_node env loc nd = |
||

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

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

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

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

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

729 | 45c13277 | xthirioux | unify_imported_clock None ck_node loc; |

730 | 22fe1c93 | ploc | check_imported_pclocks loc ck_node; |

731 | try_generalize ck_node loc; |
||

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

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

734 | |||

735 | ef34b4ae | xthirioux | let clock_top_const env cdecl= |

736 | let ck = new_var false in |
||

737 | try_generalize ck cdecl.const_loc; |
||

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

739 | 22fe1c93 | ploc | |

740 | ef34b4ae | xthirioux | let clock_top_consts env clist = |

741 | List.fold_left clock_top_const env clist |
||

742 | |||

743 | let rec clock_top_decl env decl = |
||

744 | 22fe1c93 | ploc | match decl.top_decl_desc with |

745 | | Node nd -> |
||

746 | clock_node env decl.top_decl_loc nd |
||

747 | | ImportedNode nd -> |
||

748 | clock_imported_node env decl.top_decl_loc nd |
||

749 | ef34b4ae | xthirioux | | Const c -> |

750 | clock_top_const env c |
||

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

752 | | Open _ -> env |
||

753 | 22fe1c93 | ploc | |

754 | let clock_prog env decls = |
||

755 | ef34b4ae | xthirioux | List.fold_left clock_top_decl env decls |

756 | 22fe1c93 | ploc | |

757 | 8f1c7e91 | xthirioux | (* Once the Lustre program is fully clocked, |

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

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

760 | |||

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

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

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

764 | *) |
||

765 | let uneval_vdecl_generics vdecl = |
||

766 | 89b9e25c | xthirioux | (*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*) |

767 | 6afa892a | xthirioux | if Types.get_clock_base_type vdecl.var_type <> None |

768 | 8f1c7e91 | xthirioux | then |

769 | match get_carrier_name vdecl.var_clock with |
||

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

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

772 | |||

773 | let uneval_node_generics vdecls = |
||

774 | List.iter uneval_vdecl_generics vdecls |
||

775 | |||

776 | let uneval_top_generics decl = |
||

777 | match decl.top_decl_desc with |
||

778 | | Node nd -> |
||

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

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

781 | 8f1c7e91 | xthirioux | | ImportedNode nd -> |

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

783 | ef34b4ae | xthirioux | | Const _ |

784 | b1655a21 | xthirioux | | Open _ |

785 | ef34b4ae | xthirioux | | TypeDef _ -> () |

786 | 8f1c7e91 | xthirioux | |

787 | let uneval_prog_generics prog = |
||

788 | List.iter uneval_top_generics prog |
||

789 | |||

790 | 7291cb80 | xthirioux | let check_env_compat header declared computed = |

791 | 8f1c7e91 | xthirioux | uneval_prog_generics header; |

792 | 5c1184ad | ploc | Env.iter declared (fun k decl_clock_k -> |

793 | 7291cb80 | xthirioux | let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in |

794 | 8f1c7e91 | xthirioux | try_semi_unify decl_clock_k computed_c Location.dummy_loc |

795 | 5c1184ad | ploc | ) |

796 | 22fe1c93 | ploc | (* Local Variables: *) |

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

798 | (* End: *) |