## lustrec / src / dimension.ml @ d75eb6f1

History | View | Annotate | Download (10.9 KB)

1 | b38ffff3 | ploc | (********************************************************************) |
---|---|---|---|

2 | (* *) |
||

3 | (* The LustreC compiler toolset / The LustreC Development Team *) |
||

4 | (* Copyright 2012 - -- ONERA - CNRS - INPT *) |
||

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 | (********************************************************************) |
||

11 | 0cbf0839 | ploc | |

12 | open Format |
||

13 | |||

14 | type dim_expr = |
||

15 | {mutable dim_desc: dim_desc; |
||

16 | dim_loc: Location.t; |
||

17 | dim_id: int} |
||

18 | |||

19 | and dim_desc = |
||

20 | | Dbool of bool |
||

21 | | Dint of int |
||

22 | | Dident of Utils.ident |
||

23 | | Dappl of Utils.ident * dim_expr list |
||

24 | | Dite of dim_expr * dim_expr * dim_expr |
||

25 | | Dlink of dim_expr |
||

26 | | Dvar |
||

27 | | Dunivar |
||

28 | |||

29 | exception Unify of dim_expr * dim_expr |
||

30 | exception InvalidDimension |
||

31 | |||

32 | let new_id = ref (-1) |
||

33 | |||

34 | let mkdim loc dim = |
||

35 | incr new_id; |
||

36 | { dim_loc = loc; |
||

37 | dim_id = !new_id; |
||

38 | dim_desc = dim;} |
||

39 | |||

40 | let mkdim_var () = |
||

41 | incr new_id; |
||

42 | { dim_loc = Location.dummy_loc; |
||

43 | dim_id = !new_id; |
||

44 | dim_desc = Dvar;} |
||

45 | |||

46 | let mkdim_ident loc id = |
||

47 | incr new_id; |
||

48 | { dim_loc = loc; |
||

49 | dim_id = !new_id; |
||

50 | dim_desc = Dident id;} |
||

51 | |||

52 | let mkdim_bool loc b = |
||

53 | incr new_id; |
||

54 | { dim_loc = loc; |
||

55 | dim_id = !new_id; |
||

56 | dim_desc = Dbool b;} |
||

57 | |||

58 | let mkdim_int loc i = |
||

59 | incr new_id; |
||

60 | { dim_loc = loc; |
||

61 | dim_id = !new_id; |
||

62 | dim_desc = Dint i;} |
||

63 | |||

64 | let mkdim_appl loc f args = |
||

65 | incr new_id; |
||

66 | { dim_loc = loc; |
||

67 | dim_id = !new_id; |
||

68 | dim_desc = Dappl (f, args);} |
||

69 | |||

70 | let mkdim_ite loc i t e = |
||

71 | incr new_id; |
||

72 | { dim_loc = loc; |
||

73 | dim_id = !new_id; |
||

74 | dim_desc = Dite (i, t, e);} |
||

75 | |||

76 | let rec pp_dimension fmt dim = |
||

77 | (*fprintf fmt "<%d>" (Obj.magic dim: int);*) |
||

78 | match dim.dim_desc with |
||

79 | | Dident id -> |
||

80 | fprintf fmt "%s" id |
||

81 | | Dint i -> |
||

82 | fprintf fmt "%d" i |
||

83 | | Dbool b -> |
||

84 | fprintf fmt "%B" b |
||

85 | | Dite (i, t, e) -> |
||

86 | fprintf fmt "if %a then %a else %a" |
||

87 | pp_dimension i pp_dimension t pp_dimension e |
||

88 | | Dappl (f, [arg]) -> |
||

89 | fprintf fmt "(%s%a)" f pp_dimension arg |
||

90 | | Dappl (f, [arg1; arg2]) -> |
||

91 | fprintf fmt "(%a%s%a)" pp_dimension arg1 f pp_dimension arg2 |
||

92 | | Dappl (_, _) -> assert false |
||

93 | | Dlink dim' -> fprintf fmt "%a" pp_dimension dim' |
||

94 | | Dvar -> fprintf fmt "_%s" (Utils.name_of_dimension dim.dim_id) |
||

95 | | Dunivar -> fprintf fmt "'%s" (Utils.name_of_dimension dim.dim_id) |
||

96 | |||

97 | let rec multi_dimension_product loc dim_list = |
||

98 | match dim_list with |
||

99 | | [] -> mkdim_int loc 1 |
||

100 | | [d] -> d |
||

101 | | d::q -> mkdim_appl loc "*" [d; multi_dimension_product loc q] |
||

102 | |||

103 | (* Builds a dimension expr representing 0<=d *) |
||

104 | let check_bound loc d = |
||

105 | mkdim_appl loc "<=" [mkdim_int loc 0; d] |
||

106 | |||

107 | (* Builds a dimension expr representing 0<=i<d *) |
||

108 | let check_access loc d i = |
||

109 | mkdim_appl loc "&&" |
||

110 | [mkdim_appl loc "<=" [mkdim_int loc 0; i]; |
||

111 | mkdim_appl loc "<" [i; d]] |
||

112 | |||

113 | let rec repr dim = |
||

114 | match dim.dim_desc with |
||

115 | | Dlink dim' -> repr dim' |
||

116 | | _ -> dim |
||

117 | |||

118 | let rec is_eq_dimension d1 d2 = |
||

119 | let d1 = repr d1 in |
||

120 | let d2 = repr d2 in |
||

121 | d1.dim_id = d2.dim_id || |
||

122 | match d1.dim_desc, d2.dim_desc with |
||

123 | | Dappl (f1, args1), Dappl (f2, args2) -> |
||

124 | f1 = f2 && List.length args1 = List.length args2 && List.for_all2 is_eq_dimension args1 args2 |
||

125 | | Dite (c1, t1, e1), Dite (c2, t2, e2) -> |
||

126 | is_eq_dimension c1 c2 && is_eq_dimension t1 t2 && is_eq_dimension e1 e2 |
||

127 | 6aeb3388 | xthirioux | | Dint i1 , Dint i2 -> i1 = i2 |

128 | | Dbool b1 , Dbool b2 -> b1 = b2 |
||

129 | | Dident id1, Dident id2 -> id1 = id2 |
||

130 | | _ -> false |
||

131 | 0cbf0839 | ploc | |

132 | let is_dimension_const dim = |
||

133 | match (repr dim).dim_desc with |
||

134 | | Dint _ |
||

135 | | Dbool _ -> true |
||

136 | | _ -> false |
||

137 | |||

138 | let size_const_dimension dim = |
||

139 | match (repr dim).dim_desc with |
||

140 | | Dint i -> i |
||

141 | | Dbool b -> if b then 1 else 0 |
||

142 | | _ -> (Format.eprintf "internal error: size_const_dimension %a@." pp_dimension dim; assert false) |
||

143 | |||

144 | let rec is_polymorphic dim = |
||

145 | match dim.dim_desc with |
||

146 | | Dident _ |
||

147 | | Dint _ |
||

148 | | Dbool _ |
||

149 | | Dvar -> false |
||

150 | | Dite (i, t, e) -> |
||

151 | is_polymorphic i || is_polymorphic t || is_polymorphic e |
||

152 | | Dappl (_, args) -> List.exists is_polymorphic args |
||

153 | | Dlink dim' -> is_polymorphic dim' |
||

154 | | Dunivar -> true |
||

155 | |||

156 | (* Normalizes a dimension expression, i.e. canonicalize all polynomial |
||

157 | sub-expressions, where unsupported operations (eg. '/') are treated |
||

158 | as variables. |
||

159 | *) |
||

160 | |||

161 | let rec factors dim = |
||

162 | match dim.dim_desc with |
||

163 | | Dappl (f, args) when f = "*" -> List.flatten (List.map factors args) |
||

164 | | _ -> [dim] |
||

165 | |||

166 | let rec factors_constant fs = |
||

167 | match fs with |
||

168 | | [] -> 1 |
||

169 | | f::q -> |
||

170 | match f.dim_desc with |
||

171 | | Dint i -> i * (factors_constant q) |
||

172 | | _ -> factors_constant q |
||

173 | |||

174 | let norm_factors fs = |
||

175 | let k = factors_constant fs in |
||

176 | let nk = List.filter (fun d -> not (is_dimension_const d)) fs in |
||

177 | (k, List.sort Pervasives.compare nk) |
||

178 | |||

179 | let rec terms dim = |
||

180 | match dim.dim_desc with |
||

181 | | Dappl (f, args) when f = "+" -> List.flatten (List.map terms args) |
||

182 | | _ -> [dim] |
||

183 | |||

184 | let rec normalize dim = |
||

185 | dim |
||

186 | 8b3afe43 | xthirioux | (* |

187 | let rec unnormalize loc l = |
||

188 | let l = List.sort (fun (k, l) (k', l') -> compare l l') (List.map (fun (k, l) -> (k, List.sort compare l)) l) in |
||

189 | match l with |
||

190 | | [] -> mkdim_int loc 0 |
||

191 | | t::q -> |
||

192 | List.fold_left (fun res (k, l) -> mkdim_appl loc "+" res (mkdim_appl loc "*" (mkdim_int loc k) l)) t q |
||

193 | *) |
||

194 | 0cbf0839 | ploc | let copy copy_dim_vars dim = |

195 | let rec cp dim = |
||

196 | match dim.dim_desc with |
||

197 | | Dbool _ |
||

198 | | Dint _ -> dim |
||

199 | | Dident id -> mkdim_ident dim.dim_loc id |
||

200 | | Dite (c, t, e) -> mkdim_ite dim.dim_loc (cp c) (cp t) (cp e) |
||

201 | | Dappl (id, args) -> mkdim_appl dim.dim_loc id (List.map cp args) |
||

202 | | Dlink dim' -> cp dim' |
||

203 | | Dunivar -> assert false |
||

204 | | Dvar -> |
||

205 | try |
||

206 | List.assoc dim.dim_id !copy_dim_vars |
||

207 | with Not_found -> |
||

208 | let var = mkdim dim.dim_loc Dvar in |
||

209 | copy_dim_vars := (dim.dim_id, var)::!copy_dim_vars; |
||

210 | var |
||

211 | in cp dim |
||

212 | |||

213 | (* Partially evaluates a 'simple' dimension expr [dim], i.e. an expr containing only int and bool |
||

214 | constructs, with conditionals. [eval_const] is a typing environment for static values. [eval_op] is an evaluation env for basic operators. The argument [dim] is modified in-place. |
||

215 | *) |
||

216 | let rec eval eval_op eval_const dim = |
||

217 | match dim.dim_desc with |
||

218 | | Dbool _ |
||

219 | | Dint _ -> () |
||

220 | | Dident id -> |
||

221 | (match eval_const id with |
||

222 | | Some val_dim -> dim.dim_desc <- Dlink val_dim |
||

223 | 01d48bb0 | xthirioux | | None -> (Format.eprintf "invalid %a@." pp_dimension dim; raise InvalidDimension)) |

224 | 0cbf0839 | ploc | | Dite (c, t, e) -> |

225 | begin |
||

226 | eval eval_op eval_const c; |
||

227 | eval eval_op eval_const t; |
||

228 | eval eval_op eval_const e; |
||

229 | match (repr c).dim_desc with |
||

230 | | Dbool b -> dim.dim_desc <- Dlink (if b then t else e) |
||

231 | | _ -> () |
||

232 | end |
||

233 | | Dappl (id, args) -> |
||

234 | begin |
||

235 | List.iter (eval eval_op eval_const) args; |
||

236 | if List.for_all is_dimension_const args |
||

237 | then dim.dim_desc <- Env.lookup_value eval_op id (List.map (fun d -> (repr d).dim_desc) args) |
||

238 | end |
||

239 | | Dlink dim' -> |
||

240 | begin |
||

241 | eval eval_op eval_const dim'; |
||

242 | dim.dim_desc <- Dlink (repr dim') |
||

243 | end |
||

244 | | Dvar -> () |
||

245 | | Dunivar -> assert false |
||

246 | 53206908 | xthirioux | |

247 | 8b3afe43 | xthirioux | let uneval const univar = |

248 | 0cbf0839 | ploc | let univar = repr univar in |

249 | match univar.dim_desc with |
||

250 | | Dunivar -> univar.dim_desc <- Dident const |
||

251 | | _ -> assert false |
||

252 | |||

253 | (** [occurs dvar dim] returns true if the dimension variable [dvar] occurs in |
||

254 | dimension expression [dim]. False otherwise. *) |
||

255 | let rec occurs dvar dim = |
||

256 | let dim = repr dim in |
||

257 | match dim.dim_desc with |
||

258 | | Dvar -> dim.dim_id = dvar.dim_id |
||

259 | | Dident _ |
||

260 | | Dint _ |
||

261 | | Dbool _ |
||

262 | | Dunivar -> false |
||

263 | | Dite (i, t, e) -> |
||

264 | occurs dvar i || occurs dvar t || occurs dvar e |
||

265 | | Dappl (_, args) -> List.exists (occurs dvar) args |
||

266 | | Dlink _ -> assert false |
||

267 | |||

268 | (* Promote monomorphic dimension variables to polymorphic variables. |
||

269 | Generalize by side-effects *) |
||

270 | let rec generalize dim = |
||

271 | match dim.dim_desc with |
||

272 | | Dvar -> dim.dim_desc <- Dunivar |
||

273 | | Dident _ |
||

274 | | Dint _ |
||

275 | | Dbool _ |
||

276 | | Dunivar -> () |
||

277 | | Dite (i, t, e) -> |
||

278 | generalize i; generalize t; generalize e |
||

279 | | Dappl (_, args) -> List.iter generalize args |
||

280 | | Dlink dim' -> generalize dim' |
||

281 | |||

282 | (* Instantiate polymorphic dimension variables to monomorphic variables. |
||

283 | Also duplicates the whole term structure (but the constant sub-terms). |
||

284 | *) |
||

285 | let rec instantiate inst_dim_vars dim = |
||

286 | let dim = repr dim in |
||

287 | match dim.dim_desc with |
||

288 | 7dedc5f0 | xthirioux | | Dvar |

289 | 0cbf0839 | ploc | | Dident _ |

290 | | Dint _ |
||

291 | | Dbool _ -> dim |
||

292 | | Dite (i, t, e) -> |
||

293 | mkdim_ite dim.dim_loc |
||

294 | (instantiate inst_dim_vars i) |
||

295 | (instantiate inst_dim_vars t) |
||

296 | (instantiate inst_dim_vars e) |
||

297 | | Dappl (f, args) -> mkdim_appl dim.dim_loc f (List.map (instantiate inst_dim_vars) args) |
||

298 | | Dlink dim' -> assert false (*mkdim dim.dim_loc (Dlink (instantiate inst_dim_vars dim'))*) |
||

299 | | Dunivar -> |
||

300 | try |
||

301 | List.assoc dim.dim_id !inst_dim_vars |
||

302 | with Not_found -> |
||

303 | let var = mkdim dim.dim_loc Dvar in |
||

304 | inst_dim_vars := (dim.dim_id, var)::!inst_dim_vars; |
||

305 | var |
||

306 | |||

307 | 6b4d172f | xthirioux | (** destructive unification of [dim1] and [dim2]. |

308 | Raises [Unify (t1,t2)] if the types are not unifiable. |
||

309 | if [semi] unification is required, |
||

310 | [dim1] should furthermore be an instance of [dim2] *) |
||

311 | let unify ?(semi=false) dim1 dim2 = |
||

312 | let rec unif dim1 dim2 = |
||

313 | let dim1 = repr dim1 in |
||

314 | let dim2 = repr dim2 in |
||

315 | if dim1.dim_id = dim2.dim_id then () else |
||

316 | match dim1.dim_desc, dim2.dim_desc with |
||

317 | | Dunivar, _ |
||

318 | | _ , Dunivar -> assert false |
||

319 | | Dvar , Dvar -> |
||

320 | if dim1.dim_id < dim2.dim_id |
||

321 | then dim2.dim_desc <- Dlink dim1 |
||

322 | else dim1.dim_desc <- Dlink dim2 |
||

323 | | Dvar , _ when (not semi) && not (occurs dim1 dim2) -> |
||

324 | dim1.dim_desc <- Dlink dim2 |
||

325 | | _ , Dvar when not (occurs dim2 dim1) -> |
||

326 | dim2.dim_desc <- Dlink dim1 |
||

327 | | Dite(i1, t1, e1), Dite(i2, t2, e2) -> |
||

328 | begin |
||

329 | unif i1 i2; |
||

330 | unif t1 t2; |
||

331 | unif e1 e2 |
||

332 | end |
||

333 | | Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 -> |
||

334 | List.iter2 unif args1 args2 |
||

335 | | Dbool b1, Dbool b2 when b1 = b2 -> () |
||

336 | | Dint i1 , Dint i2 when i1 = i2 -> () |
||

337 | | Dident id1, Dident id2 when id1 = id2 -> () |
||

338 | | _ -> raise (Unify (dim1, dim2)) |
||

339 | in unif dim1 dim2 |
||

340 | 0cbf0839 | ploc | |

341 | 333e3a25 | ploc | let rec rename fnode fvar e = |

342 | { e with dim_desc = expr_replace_var_desc fnode fvar e.dim_desc } |
||

343 | and expr_replace_var_desc fnode fvar e = |
||

344 | let re = rename fnode fvar in |
||

345 | c02d255e | ploc | match e with |

346 | | Dvar |
||

347 | | Dunivar |
||

348 | | Dbool _ |
||

349 | | Dint _ -> e |
||

350 | | Dident v -> Dident (fvar v) |
||

351 | 333e3a25 | ploc | | Dappl (id, el) -> Dappl (fnode id, List.map re el) |

352 | c02d255e | ploc | | Dite (g,t,e) -> Dite (re g, re t, re e) |

353 | | Dlink e -> Dlink (re e) |
||

354 | b3f91fdb | xthirioux | |

355 | let rec expr_replace_expr fvar e = |
||

356 | { e with dim_desc = expr_replace_expr_desc fvar e.dim_desc } |
||

357 | and expr_replace_expr_desc fvar e = |
||

358 | let re = expr_replace_expr fvar in |
||

359 | match e with |
||

360 | | Dvar |
||

361 | | Dunivar |
||

362 | | Dbool _ |
||

363 | | Dint _ -> e |
||

364 | | Dident v -> (fvar v).dim_desc |
||

365 | | Dappl (id, el) -> Dappl (id, List.map re el) |
||

366 | | Dite (g,t,e) -> Dite (re g, re t, re e) |
||

367 | | Dlink e -> Dlink (re e) |