## lustrec / lib / dimension.ml @ 9b0432bc

History | View | Annotate | Download (10.9 KB)

1 |
(********************************************************************) |
---|---|

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

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 |
[@@deriving show] |

29 | |

30 | |

31 |
exception Unify of dim_expr * dim_expr |

32 |
exception InvalidDimension |

33 | |

34 |
let new_id = ref (-1) |

35 | |

36 |
let mkdim loc dim = |

37 |
incr new_id; |

38 |
{ dim_loc = loc; |

39 |
dim_id = !new_id; |

40 |
dim_desc = dim;} |

41 | |

42 |
let mkdim_var () = |

43 |
incr new_id; |

44 |
{ dim_loc = Location.dummy_loc; |

45 |
dim_id = !new_id; |

46 |
dim_desc = Dvar;} |

47 | |

48 |
let mkdim_ident loc id = |

49 |
incr new_id; |

50 |
{ dim_loc = loc; |

51 |
dim_id = !new_id; |

52 |
dim_desc = Dident id;} |

53 | |

54 |
let mkdim_bool loc b = |

55 |
incr new_id; |

56 |
{ dim_loc = loc; |

57 |
dim_id = !new_id; |

58 |
dim_desc = Dbool b;} |

59 | |

60 |
let mkdim_int loc i = |

61 |
incr new_id; |

62 |
{ dim_loc = loc; |

63 |
dim_id = !new_id; |

64 |
dim_desc = Dint i;} |

65 | |

66 |
let mkdim_appl loc f args = |

67 |
incr new_id; |

68 |
{ dim_loc = loc; |

69 |
dim_id = !new_id; |

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

71 | |

72 |
let mkdim_ite loc i t e = |

73 |
incr new_id; |

74 |
{ dim_loc = loc; |

75 |
dim_id = !new_id; |

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

77 | |

78 |
let rec pp_dimension fmt dim = |

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

80 |
match dim.dim_desc with |

81 |
| Dident id -> |

82 |
fprintf fmt "%s" id |

83 |
| Dint i -> |

84 |
fprintf fmt "%d" i |

85 |
| Dbool b -> |

86 |
fprintf fmt "%B" b |

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

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

89 |
pp_dimension i pp_dimension t pp_dimension e |

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

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

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

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

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

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

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

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

98 | |

99 |
let rec multi_dimension_product loc dim_list = |

100 |
match dim_list with |

101 |
| [] -> mkdim_int loc 1 |

102 |
| [d] -> d |

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

104 | |

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

106 |
let check_bound loc d = |

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

108 | |

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

110 |
let check_access loc d i = |

111 |
mkdim_appl loc "&&" |

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

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

114 | |

115 |
let rec repr dim = |

116 |
match dim.dim_desc with |

117 |
| Dlink dim' -> repr dim' |

118 |
| _ -> dim |

119 | |

120 |
let rec is_eq_dimension d1 d2 = |

121 |
let d1 = repr d1 in |

122 |
let d2 = repr d2 in |

123 |
d1.dim_id = d2.dim_id || |

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

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

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

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

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

129 |
| Dint i1 , Dint i2 -> i1 = i2 |

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

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

132 |
| _ -> false |

133 | |

134 |
let is_dimension_const dim = |

135 |
match (repr dim).dim_desc with |

136 |
| Dint _ |

137 |
| Dbool _ -> true |

138 |
| _ -> false |

139 | |

140 |
let size_const_dimension dim = |

141 |
match (repr dim).dim_desc with |

142 |
| Dint i -> i |

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

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

145 | |

146 |
let rec is_polymorphic dim = |

147 |
match dim.dim_desc with |

148 |
| Dident _ |

149 |
| Dint _ |

150 |
| Dbool _ |

151 |
| Dvar -> false |

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

153 |
is_polymorphic i || is_polymorphic t || is_polymorphic e |

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

155 |
| Dlink dim' -> is_polymorphic dim' |

156 |
| Dunivar -> true |

157 | |

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

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

160 |
as variables. |

161 |
*) |

162 | |

163 |
let rec factors dim = |

164 |
match dim.dim_desc with |

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

166 |
| _ -> [dim] |

167 | |

168 |
let rec factors_constant fs = |

169 |
match fs with |

170 |
| [] -> 1 |

171 |
| f::q -> |

172 |
match f.dim_desc with |

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

174 |
| _ -> factors_constant q |

175 | |

176 |
let norm_factors fs = |

177 |
let k = factors_constant fs in |

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

179 |
(k, List.sort compare nk) |

180 | |

181 |
let rec terms dim = |

182 |
match dim.dim_desc with |

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

184 |
| _ -> [dim] |

185 | |

186 |
let rec normalize dim = |

187 |
dim |

188 |
(* |

189 |
let rec unnormalize loc l = |

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

191 |
match l with |

192 |
| [] -> mkdim_int loc 0 |

193 |
| t::q -> |

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

195 |
*) |

196 |
let copy copy_dim_vars dim = |

197 |
let rec cp dim = |

198 |
match dim.dim_desc with |

199 |
| Dbool _ |

200 |
| Dint _ -> dim |

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

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

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

204 |
| Dlink dim' -> cp dim' |

205 |
| Dunivar -> assert false |

206 |
| Dvar -> |

207 |
try |

208 |
List.assoc dim.dim_id !copy_dim_vars |

209 |
with Not_found -> |

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

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

212 |
var |

213 |
in cp dim |

214 | |

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

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

217 |
*) |

218 |
let rec eval eval_op eval_const dim = |

219 |
match dim.dim_desc with |

220 |
| Dbool _ |

221 |
| Dint _ -> () |

222 |
| Dident id -> |

223 |
(match eval_const id with |

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

225 |
| None -> (Format.eprintf "invalid %a@." pp_dimension dim; raise InvalidDimension)) |

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

227 |
begin |

228 |
eval eval_op eval_const c; |

229 |
eval eval_op eval_const t; |

230 |
eval eval_op eval_const e; |

231 |
match (repr c).dim_desc with |

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

233 |
| _ -> () |

234 |
end |

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

236 |
begin |

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

238 |
if List.for_all is_dimension_const args |

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

240 |
end |

241 |
| Dlink dim' -> |

242 |
begin |

243 |
eval eval_op eval_const dim'; |

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

245 |
end |

246 |
| Dvar -> () |

247 |
| Dunivar -> assert false |

248 | |

249 |
let uneval const univar = |

250 |
let univar = repr univar in |

251 |
match univar.dim_desc with |

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

253 |
| _ -> assert false |

254 | |

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

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

257 |
let rec occurs dvar dim = |

258 |
let dim = repr dim in |

259 |
match dim.dim_desc with |

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

261 |
| Dident _ |

262 |
| Dint _ |

263 |
| Dbool _ |

264 |
| Dunivar -> false |

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

266 |
occurs dvar i || occurs dvar t || occurs dvar e |

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

268 |
| Dlink _ -> assert false |

269 | |

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

271 |
Generalize by side-effects *) |

272 |
let rec generalize dim = |

273 |
match dim.dim_desc with |

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

275 |
| Dident _ |

276 |
| Dint _ |

277 |
| Dbool _ |

278 |
| Dunivar -> () |

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

280 |
generalize i; generalize t; generalize e |

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

282 |
| Dlink dim' -> generalize dim' |

283 | |

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

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

286 |
*) |

287 |
let rec instantiate inst_dim_vars dim = |

288 |
let dim = repr dim in |

289 |
match dim.dim_desc with |

290 |
| Dvar |

291 |
| Dident _ |

292 |
| Dint _ |

293 |
| Dbool _ -> dim |

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

295 |
mkdim_ite dim.dim_loc |

296 |
(instantiate inst_dim_vars i) |

297 |
(instantiate inst_dim_vars t) |

298 |
(instantiate inst_dim_vars e) |

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

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

301 |
| Dunivar -> |

302 |
try |

303 |
List.assoc dim.dim_id !inst_dim_vars |

304 |
with Not_found -> |

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

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

307 |
var |

308 | |

309 |
(** destructive unification of [dim1] and [dim2]. |

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

311 |
if [semi] unification is required, |

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

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

314 |
let rec unif dim1 dim2 = |

315 |
let dim1 = repr dim1 in |

316 |
let dim2 = repr dim2 in |

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

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

319 |
| Dunivar, _ |

320 |
| _ , Dunivar -> assert false |

321 |
| Dvar , Dvar -> |

322 |
if dim1.dim_id < dim2.dim_id |

323 |
then dim2.dim_desc <- Dlink dim1 |

324 |
else dim1.dim_desc <- Dlink dim2 |

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

326 |
dim1.dim_desc <- Dlink dim2 |

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

328 |
dim2.dim_desc <- Dlink dim1 |

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

330 |
begin |

331 |
unif i1 i2; |

332 |
unif t1 t2; |

333 |
unif e1 e2 |

334 |
end |

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

336 |
List.iter2 unif args1 args2 |

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

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

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

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

341 |
in unif dim1 dim2 |

342 | |

343 |
let rec rename fnode fvar e = |

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

345 |
and expr_replace_var_desc fnode fvar e = |

346 |
let re = rename fnode fvar in |

347 |
match e with |

348 |
| Dvar |

349 |
| Dunivar |

350 |
| Dbool _ |

351 |
| Dint _ -> e |

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

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

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

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

356 | |

357 |
let rec expr_replace_expr fvar e = |

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

359 |
and expr_replace_expr_desc fvar e = |

360 |
let re = expr_replace_expr fvar in |

361 |
match e with |

362 |
| Dvar |

363 |
| Dunivar |

364 |
| Dbool _ |

365 |
| Dint _ -> e |

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

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

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

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