## lustrec / src / dimension.ml @ 7291cb80

History | View | Annotate | Download (11.4 KB)

1 | 22fe1c93 | ploc | (* ---------------------------------------------------------------------------- |
---|---|---|---|

2 | * SchedMCore - A MultiCore Scheduling Framework |
||

3 | * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
||

4 | * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE |
||

5 | * |
||

6 | * This file is part of Prelude |
||

7 | * |
||

8 | * Prelude is free software; you can redistribute it and/or |
||

9 | * modify it under the terms of the GNU Lesser General Public License |
||

10 | * as published by the Free Software Foundation ; either version 2 of |
||

11 | * the License, or (at your option) any later version. |
||

12 | * |
||

13 | * Prelude is distributed in the hope that it will be useful, but |
||

14 | * WITHOUT ANY WARRANTY ; without even the implied warranty of |
||

15 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
||

16 | * Lesser General Public License for more details. |
||

17 | * |
||

18 | * You should have received a copy of the GNU Lesser General Public |
||

19 | * License along with this program ; if not, write to the Free Software |
||

20 | * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
||

21 | * USA |
||

22 | *---------------------------------------------------------------------------- *) |
||

23 | |||

24 | (* This module is used for the lustre to C compiler *) |
||

25 | |||

26 | open Format |
||

27 | |||

28 | type dim_expr = |
||

29 | {mutable dim_desc: dim_desc; |
||

30 | dim_loc: Location.t; |
||

31 | dim_id: int} |
||

32 | |||

33 | and dim_desc = |
||

34 | | Dbool of bool |
||

35 | | Dint of int |
||

36 | | Dident of Utils.ident |
||

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

38 | | Dite of dim_expr * dim_expr * dim_expr |
||

39 | | Dlink of dim_expr |
||

40 | | Dvar |
||

41 | | Dunivar |
||

42 | |||

43 | exception Unify of dim_expr * dim_expr |
||

44 | exception InvalidDimension |
||

45 | |||

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

47 | |||

48 | let mkdim loc dim = |
||

49 | incr new_id; |
||

50 | { dim_loc = loc; |
||

51 | dim_id = !new_id; |
||

52 | dim_desc = dim;} |
||

53 | |||

54 | let mkdim_var () = |
||

55 | incr new_id; |
||

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

57 | dim_id = !new_id; |
||

58 | dim_desc = Dvar;} |
||

59 | |||

60 | let mkdim_ident loc id = |
||

61 | incr new_id; |
||

62 | { dim_loc = loc; |
||

63 | dim_id = !new_id; |
||

64 | dim_desc = Dident id;} |
||

65 | |||

66 | let mkdim_bool loc b = |
||

67 | incr new_id; |
||

68 | { dim_loc = loc; |
||

69 | dim_id = !new_id; |
||

70 | dim_desc = Dbool b;} |
||

71 | |||

72 | let mkdim_int loc i = |
||

73 | incr new_id; |
||

74 | { dim_loc = loc; |
||

75 | dim_id = !new_id; |
||

76 | dim_desc = Dint i;} |
||

77 | |||

78 | let mkdim_appl loc f args = |
||

79 | incr new_id; |
||

80 | { dim_loc = loc; |
||

81 | dim_id = !new_id; |
||

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

83 | |||

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

85 | incr new_id; |
||

86 | { dim_loc = loc; |
||

87 | dim_id = !new_id; |
||

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

89 | |||

90 | let rec pp_dimension fmt dim = |
||

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

92 | match dim.dim_desc with |
||

93 | | Dident id -> |
||

94 | fprintf fmt "%s" id |
||

95 | | Dint i -> |
||

96 | fprintf fmt "%d" i |
||

97 | | Dbool b -> |
||

98 | fprintf fmt "%B" b |
||

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

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

101 | pp_dimension i pp_dimension t pp_dimension e |
||

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

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

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

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

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

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

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

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

110 | |||

111 | let rec multi_dimension_product loc dim_list = |
||

112 | match dim_list with |
||

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

114 | | [d] -> d |
||

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

116 | |||

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

118 | let check_bound loc d = |
||

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

120 | |||

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

122 | let check_access loc d i = |
||

123 | mkdim_appl loc "&&" |
||

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

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

126 | |||

127 | let rec repr dim = |
||

128 | match dim.dim_desc with |
||

129 | | Dlink dim' -> repr dim' |
||

130 | | _ -> dim |
||

131 | |||

132 | let rec is_eq_dimension d1 d2 = |
||

133 | let d1 = repr d1 in |
||

134 | let d2 = repr d2 in |
||

135 | d1.dim_id = d2.dim_id || |
||

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

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

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

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

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

141 | | Dvar, _ |
||

142 | | _, Dvar |
||

143 | | Dunivar, _ |
||

144 | | _, Dunivar -> false |
||

145 | | _ -> d1 = d2 |
||

146 | |||

147 | let is_dimension_const dim = |
||

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

149 | | Dint _ |
||

150 | | Dbool _ -> true |
||

151 | | _ -> false |
||

152 | |||

153 | let size_const_dimension dim = |
||

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

155 | | Dint i -> i |
||

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

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

158 | |||

159 | let rec is_polymorphic dim = |
||

160 | match dim.dim_desc with |
||

161 | | Dident _ |
||

162 | | Dint _ |
||

163 | | Dbool _ |
||

164 | | Dvar -> false |
||

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

166 | is_polymorphic i || is_polymorphic t || is_polymorphic e |
||

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

168 | | Dlink dim' -> is_polymorphic dim' |
||

169 | | Dunivar -> true |
||

170 | |||

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

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

173 | as variables. |
||

174 | *) |
||

175 | |||

176 | let rec factors dim = |
||

177 | match dim.dim_desc with |
||

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

179 | | _ -> [dim] |
||

180 | |||

181 | let rec factors_constant fs = |
||

182 | match fs with |
||

183 | | [] -> 1 |
||

184 | | f::q -> |
||

185 | match f.dim_desc with |
||

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

187 | | _ -> factors_constant q |
||

188 | |||

189 | let norm_factors fs = |
||

190 | let k = factors_constant fs in |
||

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

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

193 | |||

194 | let rec terms dim = |
||

195 | match dim.dim_desc with |
||

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

197 | | _ -> [dim] |
||

198 | |||

199 | let rec normalize dim = |
||

200 | dim |
||

201 | 7291cb80 | xthirioux | (* |

202 | let rec unnormalize loc l = |
||

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

204 | match l with |
||

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

206 | | t::q -> |
||

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

208 | *) |
||

209 | 22fe1c93 | ploc | let copy copy_dim_vars dim = |

210 | let rec cp dim = |
||

211 | match dim.dim_desc with |
||

212 | | Dbool _ |
||

213 | | Dint _ -> dim |
||

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

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

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

217 | | Dlink dim' -> cp dim' |
||

218 | | Dunivar -> assert false |
||

219 | | Dvar -> |
||

220 | try |
||

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

222 | with Not_found -> |
||

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

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

225 | var |
||

226 | in cp dim |
||

227 | |||

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

229 | 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. |
||

230 | *) |
||

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

232 | match dim.dim_desc with |
||

233 | | Dbool _ |
||

234 | | Dint _ -> () |
||

235 | | Dident id -> |
||

236 | (match eval_const id with |
||

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

238 | | None -> raise InvalidDimension) |
||

239 | | Dite (c, t, e) -> |
||

240 | begin |
||

241 | eval eval_op eval_const c; |
||

242 | eval eval_op eval_const t; |
||

243 | eval eval_op eval_const e; |
||

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

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

246 | | _ -> () |
||

247 | end |
||

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

249 | begin |
||

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

251 | if List.for_all is_dimension_const args |
||

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

253 | end |
||

254 | | Dlink dim' -> |
||

255 | begin |
||

256 | eval eval_op eval_const dim'; |
||

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

258 | end |
||

259 | | Dvar -> () |
||

260 | | Dunivar -> assert false |
||

261 | |||

262 | 7291cb80 | xthirioux | let uneval const univar = |

263 | 22fe1c93 | ploc | let univar = repr univar in |

264 | match univar.dim_desc with |
||

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

266 | | _ -> assert false |
||

267 | |||

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

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

270 | let rec occurs dvar dim = |
||

271 | let dim = repr dim in |
||

272 | match dim.dim_desc with |
||

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

274 | | Dident _ |
||

275 | | Dint _ |
||

276 | | Dbool _ |
||

277 | | Dunivar -> false |
||

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

279 | occurs dvar i || occurs dvar t || occurs dvar e |
||

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

281 | | Dlink _ -> assert false |
||

282 | |||

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

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

285 | let rec generalize dim = |
||

286 | match dim.dim_desc with |
||

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

288 | | Dident _ |
||

289 | | Dint _ |
||

290 | | Dbool _ |
||

291 | | Dunivar -> () |
||

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

293 | generalize i; generalize t; generalize e |
||

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

295 | | Dlink dim' -> generalize dim' |
||

296 | |||

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

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

299 | *) |
||

300 | let rec instantiate inst_dim_vars dim = |
||

301 | let dim = repr dim in |
||

302 | match dim.dim_desc with |
||

303 | | Dvar _ |
||

304 | | Dident _ |
||

305 | | Dint _ |
||

306 | | Dbool _ -> dim |
||

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

308 | mkdim_ite dim.dim_loc |
||

309 | (instantiate inst_dim_vars i) |
||

310 | (instantiate inst_dim_vars t) |
||

311 | (instantiate inst_dim_vars e) |
||

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

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

314 | | Dunivar -> |
||

315 | try |
||

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

317 | with Not_found -> |
||

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

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

320 | var |
||

321 | |||

322 | let rec unify dim1 dim2 = |
||

323 | let dim1 = repr dim1 in |
||

324 | let dim2 = repr dim2 in |
||

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

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

327 | | Dunivar, _ |
||

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

329 | | Dvar , Dvar -> |
||

330 | if dim1.dim_id < dim2.dim_id |
||

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

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

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

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

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

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

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

338 | begin |
||

339 | unify i1 i2; |
||

340 | unify t1 t2; |
||

341 | unify e1 e2 |
||

342 | end |
||

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

344 | List.iter2 unify args1 args2 |
||

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

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

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

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

349 | |||

350 | 7a47b44f | xthirioux | let rec semi_unify dim1 dim2 = |

351 | let dim1 = repr dim1 in |
||

352 | let dim2 = repr dim2 in |
||

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

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

355 | | Dunivar, _ |
||

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

357 | | Dvar , Dvar -> |
||

358 | if dim1.dim_id < dim2.dim_id |
||

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

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

361 | | Dvar , _ -> raise (Unify (dim1, dim2)) |
||

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

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

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

365 | begin |
||

366 | semi_unify i1 i2; |
||

367 | semi_unify t1 t2; |
||

368 | semi_unify e1 e2 |
||

369 | end |
||

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

371 | List.iter2 semi_unify args1 args2 |
||

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

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

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

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

376 | 22fe1c93 | ploc | |

377 | e2380d4d | ploc | let rec expr_replace_var fvar e = |

378 | { e with dim_desc = expr_replace_desc fvar e.dim_desc } |
||

379 | and expr_replace_desc fvar e = |
||

380 | let re = expr_replace_var fvar in |
||

381 | match e with |
||

382 | | Dvar |
||

383 | | Dunivar |
||

384 | | Dbool _ |
||

385 | | Dint _ -> e |
||

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

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

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

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