## lustrec / src / clock_calculus.ml @ b08ffca7

History | View | Annotate | Download (30.9 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 | | 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 | 7291cb80 | xthirioux | let instantiate_carrier cr inst_cr_vars = |

96 | 22fe1c93 | ploc | 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 | 7291cb80 | xthirioux | let rec instantiate inst_ck_vars inst_cr_vars ck = |

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

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

117 | {ck with cdesc = |
||

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

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

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

121 | {ck with cdesc = Ctuple |
||

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

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

124 | 7291cb80 | xthirioux | 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 | 22fe1c93 | ploc | | Cvar _ | Pck_const (_,_) -> ck |

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

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

129 | 22fe1c93 | ploc | | Pck_down (ck',k) -> |

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

131 | 22fe1c93 | ploc | | Pck_phase (ck',q) -> |

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

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

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

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

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

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

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

139 | 22fe1c93 | ploc | | 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 | 8a183477 | xthirioux | if cr1==cr2 then () |

221 | 22fe1c93 | ploc | 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 | 8f1c7e91 | xthirioux | | _,_ -> 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 | 8a183477 | xthirioux | if cr1==cr2 then () |

253 | 8f1c7e91 | xthirioux | 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 | 22fe1c93 | ploc | |

276 | 6fdfb60b | xthirioux | 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 | 22fe1c93 | ploc | (** [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 | 8a183477 | xthirioux | if ck1==ck2 then |

293 | 22fe1c93 | ploc | () |

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 | 8f1c7e91 | xthirioux | | 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 | 8a183477 | xthirioux | if ck1==ck2 then |

398 | 8f1c7e91 | xthirioux | () |

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 | 22fe1c93 | ploc | | Cunivar _, _ | _, Cunivar _ -> () |

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

435 | |||

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

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

438 | let int_factor_of_expr e = |
||

439 | match e.expr_desc with |
||

440 | | Expr_const |
||

441 | (Const_int i) -> i |
||

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

443 | |||

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

445 | let clock_uncarry ck = |
||

446 | let ck = repr ck in |
||

447 | match ck.cdesc with |
||

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

449 | | _ -> ck |
||

450 | |||

451 | let try_unify ck1 ck2 loc = |
||

452 | try |
||

453 | unify ck1 ck2 |
||

454 | with |
||

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

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

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

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

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

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

461 | |||

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

463 | try |
||

464 | semi_unify ck1 ck2 |
||

465 | with |
||

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

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

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

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

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

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

472 | |||

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

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

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

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

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

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

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

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

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

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

483 | begin |
||

484 | unify_carrier cr1 cr2; |
||

485 | sub_unify sub c1 c2 |
||

486 | end |
||

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

488 | begin |
||

489 | unify_carrier cr1 cr2; |
||

490 | sub_unify sub c1 c2 |
||

491 | end |
||

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

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

494 | |||

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

496 | try |
||

497 | sub_unify sub ck1 ck2 |
||

498 | with |
||

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

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

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

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

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

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

505 | 22fe1c93 | ploc | |

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

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

508 | let unify_tuple_clock ref_ck_opt ck loc = |
||

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

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

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

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

513 | let rec aux ck = |
||

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

515 | | Con _ |
||

516 | | Cvar _ -> |
||

517 | begin |
||

518 | match !ck_var with |
||

519 | | None -> |
||

520 | ck_var:=Some ck |
||

521 | | Some v -> |
||

522 | (* may fail *) |
||

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

524 | 45c13277 | xthirioux | end |

525 | | Ctuple cl -> |
||

526 | List.iter aux cl |
||

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

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

529 | aux ck1 |
||

530 | | _ -> () |
||

531 | 6fdfb60b | xthirioux | in aux ck |

532 | 45c13277 | xthirioux | |

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

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

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

536 | let unify_imported_clock ref_ck_opt ck loc = |
||

537 | let ck_var = ref ref_ck_opt in |
||

538 | let rec aux ck = |
||

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

540 | | Cvar _ -> |
||

541 | begin |
||

542 | match !ck_var with |
||

543 | | None -> |
||

544 | ck_var:=Some ck |
||

545 | | Some v -> |
||

546 | (* cannot fail *) |
||

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

548 | 45c13277 | xthirioux | end |

549 | | Ctuple cl -> |
||

550 | List.iter aux cl |
||

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

552 | aux ck1; aux ck2 |
||

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

554 | aux ck1 |
||

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

556 | | _ -> () |
||

557 | in |
||

558 | aux ck |
||

559 | |||

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

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

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

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

564 | *) |
||

565 | let rec clock_standard_args env expr_list = |
||

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

567 | let ck_res = new_var true in |
||

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

569 | ck_res |
||

570 | |||

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

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

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

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

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

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

577 | 22fe1c93 | ploc | |

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

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

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

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

582 | then |
||

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

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

585 | else |
||

586 | clock_call env f args clock_reset loc |
||

587 | |||

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

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

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

591 | let cins = clock_list_of_clock cins in |
||

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

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

594 | 22fe1c93 | ploc | couts |

595 | |||

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

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

598 | |||

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

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

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

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

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

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

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

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

607 | cr |
||

608 | 22fe1c93 | ploc | |

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

610 | environment [env] *) |
||

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

612 | let resulting_ck = |
||

613 | match expr.expr_desc with |
||

614 | | Expr_const cst -> |
||

615 | let ck = new_var true in |
||

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

617 | ck |
||

618 | | Expr_ident v -> |
||

619 | let ckv = |
||

620 | try |
||

621 | Env.lookup_value env v |
||

622 | with Not_found -> |
||

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

624 | in |
||

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

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

627 | ck |
||

628 | | Expr_array elist -> |
||

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

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

631 | ck |
||

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

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

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

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

636 | ck |
||

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

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

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

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

641 | ck |
||

642 | | Expr_tuple elist -> |
||

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

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

645 | ck |
||

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

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

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

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

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

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

652 | ck |
||

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

654 | (try |
||

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

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

657 | *) |
||

658 | let cr = |
||

659 | match r with |
||

660 | | None -> new_var true |
||

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

662 | let expr_r = expr_of_ident x loc_r in |
||

663 | clock_expr env expr_r in |
||

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

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

666 | couts |
||

667 | with exn -> ( |
||

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

669 | raise exn |
||

670 | )) |
||

671 | | Expr_fby (e1,e2) |
||

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

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

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

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

676 | ck |
||

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

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

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

680 | ck |
||

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

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

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

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

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

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

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

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

689 | ck |
||

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

691 | let cvar = new_var true in |
||

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

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

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

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

696 | 22fe1c93 | ploc | expr.expr_clock <- cvar; |

697 | cvar |
||

698 | in |
||

699 | 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); |

700 | 22fe1c93 | ploc | resulting_ck |

701 | |||

702 | let clock_of_vlist vars = |
||

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

704 | clock_of_clock_list ckl |
||

705 | |||

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

707 | environment [env] *) |
||

708 | let clock_eq env eq = |
||

709 | let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in |
||

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

711 | clock_subtyping_arg env expr_lhs ck_rhs |
||

712 | |||

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

714 | declaration [cck] *) |
||

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

716 | match cck.ck_dec_desc with |
||

717 | | Ckdec_any -> new_var scoped |
||

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

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

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

721 | ck |
||

722 | | Ckdec_bool cl -> |
||

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

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

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

726 | let when_expr = |
||

727 | List.fold_left |
||

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

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

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

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

732 | expr_clock = new_var scoped; |
||

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

734 | expr_loc = loc; |
||

735 | expr_annot = None}) |
||

736 | dummy_id_expr cl |
||

737 | in |
||

738 | clock_expr temp_env when_expr |
||

739 | |||

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

741 | let clock_var_decl scoped env vdecl = |
||

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

743 | 89b9e25c | xthirioux | let ck = |

744 | (* WTF ???? |
||

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

746 | then |
||

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

748 | else |
||

749 | 89b9e25c | xthirioux | *) |

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

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

752 | else ck in |
||

753 | 22fe1c93 | ploc | vdecl.var_clock <- ck; |

754 | Env.add_value env vdecl.var_id ck |
||

755 | |||

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

757 | let clock_var_decl_list env scoped l = |
||

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

759 | |||

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

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

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

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

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

765 | are allowed to be generalized. |
||

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

767 | they can be generalized. |
||

768 | *) |
||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

783 | (* |
||

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

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

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

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

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

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

790 | *) |
||

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

792 | 22fe1c93 | ploc | nd.node_clock <- ck_node; |

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

794 | |||

795 | |||

796 | let check_imported_pclocks loc ck_node = |
||

797 | let pck = ref None in |
||

798 | let rec aux ck = |
||

799 | match ck.cdesc with |
||

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

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

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

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

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

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

806 | begin |
||

807 | match !pck with |
||

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

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

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

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

812 | end |
||

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

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

815 | | Cvar _ | Cunivar _ -> |
||

816 | match !pck with |
||

817 | | None -> () |
||

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

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

820 | in |
||

821 | aux ck_node |
||

822 | |||

823 | let clock_imported_node env loc nd = |
||

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

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

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

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

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

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

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

831 | try_generalize ck_node loc; |
||

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

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

834 | |||

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

836 | let ck = new_var false in |
||

837 | try_generalize ck cdecl.const_loc; |
||

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

839 | 22fe1c93 | ploc | |

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

841 | List.fold_left clock_top_const env clist |
||

842 | |||

843 | let rec clock_top_decl env decl = |
||

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

845 | | Node nd -> |
||

846 | clock_node env decl.top_decl_loc nd |
||

847 | | ImportedNode nd -> |
||

848 | clock_imported_node env decl.top_decl_loc nd |
||

849 | ef34b4ae | xthirioux | | Const c -> |

850 | clock_top_const env c |
||

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

852 | | Open _ -> env |
||

853 | 22fe1c93 | ploc | |

854 | let clock_prog env decls = |
||

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

856 | 22fe1c93 | ploc | |

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

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

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

860 | |||

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

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

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

864 | *) |
||

865 | let uneval_vdecl_generics vdecl = |
||

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

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

868 | 8f1c7e91 | xthirioux | then |

869 | match get_carrier_name vdecl.var_clock with |
||

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

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

872 | |||

873 | let uneval_node_generics vdecls = |
||

874 | List.iter uneval_vdecl_generics vdecls |
||

875 | |||

876 | let uneval_top_generics decl = |
||

877 | match decl.top_decl_desc with |
||

878 | | Node nd -> |
||

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

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

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

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

883 | ef34b4ae | xthirioux | | Const _ |

884 | b1655a21 | xthirioux | | Open _ |

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

886 | 8f1c7e91 | xthirioux | |

887 | let uneval_prog_generics prog = |
||

888 | List.iter uneval_top_generics prog |
||

889 | |||

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

891 | 8f1c7e91 | xthirioux | uneval_prog_generics header; |

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

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

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

895 | 5c1184ad | ploc | ) |

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

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

898 | (* End: *) |