## lustrec / src / corelang.ml @ e135421f

History | View | Annotate | Download (25.3 KB)

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

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

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

4 | * |
||

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

6 | * |
||

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

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

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

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

11 | * |
||

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

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

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

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

16 | * |
||

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

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

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

20 | * USA |
||

21 | *---------------------------------------------------------------------------- *) |
||

22 | open Format |
||

23 | open LustreSpec |
||

24 | open Dimension |
||

25 | |||

26 | (** The core language and its ast. Every element of the ast contains its |
||

27 | location in the program text. The type and clock of an ast element |
||

28 | is mutable (and initialized to dummy values). This avoids to have to |
||

29 | duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *) |
||

30 | |||

31 | type ident = Utils.ident |
||

32 | type label = Utils.ident |
||

33 | type rat = Utils.rat |
||

34 | type tag = Utils.tag |
||

35 | |||

36 | type constant = |
||

37 | | Const_int of int |
||

38 | | Const_real of string |
||

39 | | Const_float of float |
||

40 | | Const_array of constant list |
||

41 | | Const_tag of label |
||

42 | 12af4908 | xthirioux | | Const_struct of (label * constant) list |

43 | 22fe1c93 | ploc | |

44 | type type_dec = LustreSpec.type_dec |
||

45 | |||

46 | let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc} |
||

47 | |||

48 | |||

49 | type clock_dec = LustreSpec.clock_dec |
||

50 | |||

51 | let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc} |
||

52 | |||

53 | type var_decl = LustreSpec.var_decl |
||

54 | |||

55 | (* The tag of an expression is a unique identifier used to distinguish |
||

56 | different instances of the same node *) |
||

57 | type expr = |
||

58 | {expr_tag: tag; |
||

59 | expr_desc: expr_desc; |
||

60 | mutable expr_type: Types.type_expr; |
||

61 | mutable expr_clock: Clocks.clock_expr; |
||

62 | mutable expr_delay: Delay.delay_expr; |
||

63 | mutable expr_annot: LustreSpec.expr_annot option; |
||

64 | expr_loc: Location.t} |
||

65 | |||

66 | and expr_desc = |
||

67 | | Expr_const of constant |
||

68 | | Expr_ident of ident |
||

69 | | Expr_tuple of expr list |
||

70 | | Expr_ite of expr * expr * expr |
||

71 | | Expr_arrow of expr * expr |
||

72 | | Expr_fby of expr * expr |
||

73 | | Expr_array of expr list |
||

74 | | Expr_access of expr * Dimension.dim_expr |
||

75 | | Expr_power of expr * Dimension.dim_expr |
||

76 | | Expr_pre of expr |
||

77 | | Expr_when of expr * ident * label |
||

78 | | Expr_merge of ident * (label * expr) list |
||

79 | e2380d4d | ploc | | Expr_appl of call_t |

80 | 22fe1c93 | ploc | | Expr_uclock of expr * int |

81 | | Expr_dclock of expr * int |
||

82 | | Expr_phclock of expr * rat |
||

83 | e2380d4d | ploc | and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *) |

84 | 22fe1c93 | ploc | |

85 | type eq = |
||

86 | {eq_lhs: ident list; |
||

87 | eq_rhs: expr; |
||

88 | eq_loc: Location.t} |
||

89 | |||

90 | type assert_t = |
||

91 | { |
||

92 | assert_expr: expr; |
||

93 | assert_loc: Location.t |
||

94 | } |
||

95 | |||

96 | type node_desc = |
||

97 | {node_id: ident; |
||

98 | mutable node_type: Types.type_expr; |
||

99 | mutable node_clock: Clocks.clock_expr; |
||

100 | node_inputs: var_decl list; |
||

101 | node_outputs: var_decl list; |
||

102 | node_locals: var_decl list; |
||

103 | mutable node_gencalls: expr list; |
||

104 | mutable node_checks: Dimension.dim_expr list; |
||

105 | node_asserts: assert_t list; |
||

106 | node_eqs: eq list; |
||

107 | e135421f | xthirioux | mutable node_dec_stateless: bool; |

108 | 52cfee34 | xthirioux | mutable node_stateless: bool option; |

109 | 22fe1c93 | ploc | node_spec: LustreSpec.node_annot option; |

110 | node_annot: LustreSpec.expr_annot option; |
||

111 | } |
||

112 | |||

113 | type imported_node_desc = |
||

114 | {nodei_id: ident; |
||

115 | mutable nodei_type: Types.type_expr; |
||

116 | mutable nodei_clock: Clocks.clock_expr; |
||

117 | nodei_inputs: var_decl list; |
||

118 | nodei_outputs: var_decl list; |
||

119 | nodei_stateless: bool; |
||

120 | nodei_spec: LustreSpec.node_annot option; |
||

121 | } |
||

122 | |||

123 | type const_desc = |
||

124 | {const_id: ident; |
||

125 | const_loc: Location.t; |
||

126 | const_value: constant; |
||

127 | mutable const_type: Types.type_expr; |
||

128 | } |
||

129 | |||

130 | type top_decl_desc = |
||

131 | | Node of node_desc |
||

132 | | Consts of const_desc list |
||

133 | | ImportedNode of imported_node_desc |
||

134 | 5c1184ad | ploc | | Open of string |

135 | 22fe1c93 | ploc | |

136 | type top_decl = |
||

137 | {top_decl_desc: top_decl_desc; |
||

138 | top_decl_loc: Location.t} |
||

139 | |||

140 | type program = top_decl list |
||

141 | |||

142 | type error = |
||

143 | Main_not_found |
||

144 | | Main_wrong_kind |
||

145 | | No_main_specified |
||

146 | 21485807 | xthirioux | | Unbound_symbol of ident |

147 | | Already_bound_symbol of ident |
||

148 | 22fe1c93 | ploc | |

149 | 52cfee34 | xthirioux | exception Error of Location.t * error |

150 | 22fe1c93 | ploc | |

151 | module VDeclModule = |
||

152 | struct (* Node module *) |
||

153 | type t = var_decl |
||

154 | let compare v1 v2 = compare v1 v2 |
||

155 | let hash n = Hashtbl.hash n |
||

156 | let equal n1 n2 = n1 = n2 |
||

157 | end |
||

158 | |||

159 | module VMap = Map.Make(VDeclModule) |
||

160 | |||

161 | module VSet = Set.Make(VDeclModule) |
||

162 | |||

163 | (************************************************************) |
||

164 | (* *) |
||

165 | |||

166 | let mktyp loc d = |
||

167 | { ty_dec_desc = d; ty_dec_loc = loc } |
||

168 | |||

169 | let mkclock loc d = |
||

170 | { ck_dec_desc = d; ck_dec_loc = loc } |
||

171 | |||

172 | let mkvar_decl loc (id, ty_dec, ck_dec, is_const) = |
||

173 | { var_id = id; |
||

174 | var_dec_type = ty_dec; |
||

175 | var_dec_clock = ck_dec; |
||

176 | var_dec_const = is_const; |
||

177 | var_type = Types.new_var (); |
||

178 | var_clock = Clocks.new_var true; |
||

179 | var_loc = loc } |
||

180 | |||

181 | let mkexpr loc d = |
||

182 | { expr_tag = Utils.new_tag (); |
||

183 | expr_desc = d; |
||

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

185 | expr_clock = Clocks.new_var true; |
||

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

187 | expr_annot = None; |
||

188 | expr_loc = loc } |
||

189 | |||

190 | let var_decl_of_const c = |
||

191 | { var_id = c.const_id; |
||

192 | var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any }; |
||

193 | var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any }; |
||

194 | var_dec_const = true; |
||

195 | var_type = c.const_type; |
||

196 | var_clock = Clocks.new_var false; |
||

197 | var_loc = c.const_loc } |
||

198 | |||

199 | let mk_new_name vdecl_list id = |
||

200 | let rec new_name name cpt = |
||

201 | if List.exists (fun v -> v.var_id = name) vdecl_list |
||

202 | then new_name (sprintf "_%s_%i" id cpt) (cpt+1) |
||

203 | else name |
||

204 | in new_name id 1 |
||

205 | |||

206 | let update_expr_annot e annot = |
||

207 | { e with expr_annot = LustreSpec.merge_expr_annot e.expr_annot (Some annot) } |
||

208 | |||

209 | let mkeq loc (lhs, rhs) = |
||

210 | { eq_lhs = lhs; |
||

211 | eq_rhs = rhs; |
||

212 | eq_loc = loc } |
||

213 | |||

214 | let mkassert loc expr = |
||

215 | { assert_loc = loc; |
||

216 | assert_expr = expr |
||

217 | } |
||

218 | |||

219 | let mktop_decl loc d = |
||

220 | { top_decl_desc = d; top_decl_loc = loc } |
||

221 | |||

222 | let mkpredef_call loc funname args = |
||

223 | mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None)) |
||

224 | |||

225 | let mkpredef_unary_call loc funname arg = |
||

226 | mkexpr loc (Expr_appl (funname, arg, None)) |
||

227 | |||

228 | |||

229 | (***********************************************************) |
||

230 | (* Fast access to nodes, by name *) |
||

231 | let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30 |
||

232 | let consts_table = Hashtbl.create 30 |
||

233 | |||

234 | let node_name td = |
||

235 | match td.top_decl_desc with |
||

236 | | Node nd -> nd.node_id |
||

237 | | ImportedNode nd -> nd.nodei_id |
||

238 | | _ -> assert false |
||

239 | |||

240 | let is_generic_node td = |
||

241 | match td.top_decl_desc with |
||

242 | | Node nd -> List.exists (fun v -> v.var_dec_const) nd.node_inputs |
||

243 | | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs |
||

244 | | _ -> assert false |
||

245 | |||

246 | let node_inputs td = |
||

247 | match td.top_decl_desc with |
||

248 | | Node nd -> nd.node_inputs |
||

249 | | ImportedNode nd -> nd.nodei_inputs |
||

250 | | _ -> assert false |
||

251 | |||

252 | let node_from_name id = |
||

253 | try |
||

254 | Hashtbl.find node_table id |
||

255 | with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id; |
||

256 | assert false) |
||

257 | |||

258 | let is_imported_node td = |
||

259 | match td.top_decl_desc with |
||

260 | | Node nd -> false |
||

261 | | ImportedNode nd -> true |
||

262 | | _ -> assert false |
||

263 | |||

264 | 52cfee34 | xthirioux | |

265 | 22fe1c93 | ploc | (* alias and type definition table *) |

266 | let type_table = |
||

267 | Utils.create_hashtable 20 [ |
||

268 | Tydec_int , Tydec_int; |
||

269 | Tydec_bool , Tydec_bool; |
||

270 | Tydec_float, Tydec_float; |
||

271 | Tydec_real , Tydec_real |
||

272 | ] |
||

273 | |||

274 | let rec is_user_type typ = |
||

275 | match typ with |
||

276 | | Tydec_int | Tydec_bool | Tydec_real |
||

277 | | Tydec_float | Tydec_any | Tydec_const _ -> false |
||

278 | | Tydec_clock typ' -> is_user_type typ' |
||

279 | | _ -> true |
||

280 | |||

281 | let get_repr_type typ = |
||

282 | let typ_def = Hashtbl.find type_table typ in |
||

283 | if is_user_type typ_def then typ else typ_def |
||

284 | |||

285 | let tag_true = "true" |
||

286 | let tag_false = "false" |
||

287 | |||

288 | let const_is_bool c = |
||

289 | match c with |
||

290 | | Const_tag t -> t = tag_true || t = tag_false |
||

291 | | _ -> false |
||

292 | |||

293 | (* Computes the negation of a boolean constant *) |
||

294 | let const_negation c = |
||

295 | assert (const_is_bool c); |
||

296 | match c with |
||

297 | | Const_tag t when t = tag_true -> Const_tag tag_false |
||

298 | | _ -> Const_tag tag_true |
||

299 | |||

300 | let const_or c1 c2 = |
||

301 | assert (const_is_bool c1 && const_is_bool c2); |
||

302 | match c1, c2 with |
||

303 | | Const_tag t1, _ when t1 = tag_true -> c1 |
||

304 | | _ , Const_tag t2 when t2 = tag_true -> c2 |
||

305 | | _ -> Const_tag tag_false |
||

306 | |||

307 | let const_and c1 c2 = |
||

308 | assert (const_is_bool c1 && const_is_bool c2); |
||

309 | match c1, c2 with |
||

310 | | Const_tag t1, _ when t1 = tag_false -> c1 |
||

311 | | _ , Const_tag t2 when t2 = tag_false -> c2 |
||

312 | | _ -> Const_tag tag_true |
||

313 | |||

314 | let const_xor c1 c2 = |
||

315 | assert (const_is_bool c1 && const_is_bool c2); |
||

316 | match c1, c2 with |
||

317 | | Const_tag t1, Const_tag t2 when t1 <> t2 -> Const_tag tag_true |
||

318 | | _ -> Const_tag tag_false |
||

319 | |||

320 | let const_impl c1 c2 = |
||

321 | assert (const_is_bool c1 && const_is_bool c2); |
||

322 | match c1, c2 with |
||

323 | | Const_tag t1, _ when t1 = tag_false -> Const_tag tag_true |
||

324 | | _ , Const_tag t2 when t2 = tag_true -> Const_tag tag_true |
||

325 | | _ -> Const_tag tag_false |
||

326 | |||

327 | (* To guarantee uniqueness of tags in enum types *) |
||

328 | let tag_table = |
||

329 | Utils.create_hashtable 20 [ |
||

330 | tag_true, Tydec_bool; |
||

331 | tag_false, Tydec_bool |
||

332 | ] |
||

333 | |||

334 | fa090c4e | xthirioux | (* To guarantee uniqueness of fields in struct types *) |

335 | let field_table = |
||

336 | Utils.create_hashtable 20 [ |
||

337 | ] |
||

338 | |||

339 | 22fe1c93 | ploc | let get_enum_type_tags cty = |

340 | match cty with |
||

341 | | Tydec_bool -> [tag_true; tag_false] |
||

342 | | Tydec_const _ -> (match Hashtbl.find type_table cty with |
||

343 | | Tydec_enum tl -> tl |
||

344 | | _ -> assert false) |
||

345 | | _ -> assert false |
||

346 | 6a6abd76 | xthirioux | |

347 | fa090c4e | xthirioux | let get_struct_type_fields cty = |

348 | match cty with |
||

349 | | Tydec_const _ -> (match Hashtbl.find type_table cty with |
||

350 | | Tydec_struct fl -> fl |
||

351 | | _ -> assert false) |
||

352 | | _ -> assert false |
||

353 | 6a6abd76 | xthirioux | |

354 | 22fe1c93 | ploc | let const_of_bool b = |

355 | Const_tag (if b then tag_true else tag_false) |
||

356 | |||

357 | (* let get_const c = snd (Hashtbl.find consts_table c) *) |
||

358 | |||

359 | (* Caution, returns an untyped and unclocked expression *) |
||

360 | let expr_of_ident id loc = |
||

361 | {expr_tag = Utils.new_tag (); |
||

362 | expr_desc = Expr_ident id; |
||

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

364 | expr_clock = Clocks.new_var true; |
||

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

366 | expr_loc = loc; |
||

367 | expr_annot = None} |
||

368 | |||

369 | let expr_list_of_expr expr = |
||

370 | match expr.expr_desc with |
||

371 | | Expr_tuple elist -> |
||

372 | elist |
||

373 | | _ -> [expr] |
||

374 | |||

375 | let expr_of_expr_list loc elist = |
||

376 | match elist with |
||

377 | | [t] -> { t with expr_loc = loc } |
||

378 | | t::_ -> { t with expr_desc = Expr_tuple elist; expr_loc = loc } |
||

379 | | _ -> assert false |
||

380 | |||

381 | let call_of_expr expr = |
||

382 | match expr.expr_desc with |
||

383 | | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r) |
||

384 | | _ -> assert false |
||

385 | |||

386 | (* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *) |
||

387 | let rec expr_of_dimension dim = |
||

388 | match dim.dim_desc with |
||

389 | | Dbool b -> |
||

390 | mkexpr dim.dim_loc (Expr_const (const_of_bool b)) |
||

391 | | Dint i -> |
||

392 | mkexpr dim.dim_loc (Expr_const (Const_int i)) |
||

393 | | Dident id -> |
||

394 | mkexpr dim.dim_loc (Expr_ident id) |
||

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

396 | mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e)) |
||

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

398 | mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None)) |
||

399 | | Dlink dim' -> expr_of_dimension dim' |
||

400 | | Dvar |
||

401 | | Dunivar -> (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim; |
||

402 | assert false) |
||

403 | |||

404 | let dimension_of_const loc const = |
||

405 | match const with |
||

406 | | Const_int i -> mkdim_int loc i |
||

407 | | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true) |
||

408 | | _ -> raise InvalidDimension |
||

409 | |||

410 | (* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments |
||

411 | into dimension expressions *) |
||

412 | let rec dimension_of_expr expr = |
||

413 | match expr.expr_desc with |
||

414 | | Expr_const c -> dimension_of_const expr.expr_loc c |
||

415 | | Expr_ident id -> mkdim_ident expr.expr_loc id |
||

416 | | Expr_appl (f, args, None) when Basic_library.is_internal_fun f -> |
||

417 | let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in |
||

418 | if k = None then raise InvalidDimension; |
||

419 | mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args)) |
||

420 | | Expr_ite (i, t, e) -> |
||

421 | mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e) |
||

422 | | _ -> raise InvalidDimension (* not a simple dimension expression *) |
||

423 | |||

424 | |||

425 | let sort_handlers hl = |
||

426 | List.sort (fun (t, _) (t', _) -> compare t t') hl |
||

427 | |||

428 | let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with |
||

429 | | Expr_const c1, Expr_const c2 -> c1 = c2 |
||

430 | | Expr_ident i1, Expr_ident i2 -> i1 = i2 |
||

431 | | Expr_array el1, Expr_array el2 |
||

432 | | Expr_tuple el1, Expr_tuple el2 -> |
||

433 | List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 |
||

434 | | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' |
||

435 | | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' |
||

436 | | Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2 |
||

437 | (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *) |
||

438 | (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *) |
||

439 | | Expr_pre e, Expr_pre e' -> is_eq_expr e e' |
||

440 | | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e' |
||

441 | | Expr_merge(i, hl), Expr_merge(i', hl') -> i=i' && List.for_all2 (fun (t, h) (t', h') -> t=t' && is_eq_expr h h') (sort_handlers hl) (sort_handlers hl') |
||

442 | | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e' |
||

443 | | Expr_uclock(e, i), Expr_uclock(e', i') -> i=i' && is_eq_expr e e' |
||

444 | | Expr_dclock(e, i), Expr_dclock(e', i') -> i=i' && is_eq_expr e e' |
||

445 | | Expr_phclock(e, r), Expr_phclock(e', r') -> r=r' && is_eq_expr e e' |
||

446 | | Expr_power (e1, i1), Expr_power (e2, i2) |
||

447 | | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2) |
||

448 | | _ -> false |
||

449 | |||

450 | let node_vars nd = |
||

451 | nd.node_inputs @ nd.node_locals @ nd.node_outputs |
||

452 | |||

453 | let node_var id node = |
||

454 | List.find (fun v -> v.var_id = id) (node_vars node) |
||

455 | |||

456 | let node_eq id node = |
||

457 | List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs |
||

458 | |||

459 | (* Consts unfoooolding *) |
||

460 | let is_const i consts = |
||

461 | List.exists (fun c -> c.const_id = i) consts |
||

462 | |||

463 | let get_const i consts = |
||

464 | let c = List.find (fun c -> c.const_id = i) consts in |
||

465 | c.const_value |
||

466 | |||

467 | let rec expr_unfold_consts consts e = |
||

468 | { e with expr_desc = expr_desc_unfold_consts consts e.expr_desc } |
||

469 | |||

470 | and expr_desc_unfold_consts consts e = |
||

471 | let unfold = expr_unfold_consts consts in |
||

472 | match e with |
||

473 | | Expr_const _ -> e |
||

474 | | Expr_ident i -> if is_const i consts then Expr_const (get_const i consts) else e |
||

475 | | Expr_array el -> Expr_array (List.map unfold el) |
||

476 | | Expr_access (e1, d) -> Expr_access (unfold e1, d) |
||

477 | | Expr_power (e1, d) -> Expr_power (unfold e1, d) |
||

478 | | Expr_tuple el -> Expr_tuple (List.map unfold el) |
||

479 | | Expr_ite (c, t, e) -> Expr_ite (unfold c, unfold t, unfold e) |
||

480 | | Expr_arrow (e1, e2)-> Expr_arrow (unfold e1, unfold e2) |
||

481 | | Expr_fby (e1, e2) -> Expr_fby (unfold e1, unfold e2) |
||

482 | (* | Expr_concat (e1, e2) -> Expr_concat (unfold e1, unfold e2) *) |
||

483 | (* | Expr_tail e' -> Expr_tail (unfold e') *) |
||

484 | | Expr_pre e' -> Expr_pre (unfold e') |
||

485 | | Expr_when (e', i, l)-> Expr_when (unfold e', i, l) |
||

486 | | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, unfold h)) hl) |
||

487 | | Expr_appl (i, e', i') -> Expr_appl (i, unfold e', i') |
||

488 | | Expr_uclock (e', i) -> Expr_uclock (unfold e', i) |
||

489 | | Expr_dclock (e', i) -> Expr_dclock (unfold e', i) |
||

490 | | Expr_phclock _ -> e |
||

491 | |||

492 | let eq_unfold_consts consts eq = |
||

493 | { eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs } |
||

494 | |||

495 | let node_unfold_consts consts node = |
||

496 | { node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs } |
||

497 | |||

498 | let get_consts prog = |
||

499 | List.fold_left ( |
||

500 | fun consts decl -> |
||

501 | match decl.top_decl_desc with |
||

502 | | Consts clist -> clist@consts |
||

503 | 52cfee34 | xthirioux | | Node _ | ImportedNode _ | Open _ -> consts |

504 | 22fe1c93 | ploc | ) [] prog |

505 | |||

506 | |||

507 | let get_nodes prog = |
||

508 | List.fold_left ( |
||

509 | fun nodes decl -> |
||

510 | match decl.top_decl_desc with |
||

511 | | Node nd -> nd::nodes |
||

512 | 52cfee34 | xthirioux | | Consts _ | ImportedNode _ | Open _ -> nodes |

513 | 22fe1c93 | ploc | ) [] prog |

514 | |||

515 | let prog_unfold_consts prog = |
||

516 | let consts = get_consts prog in |
||

517 | List.map ( |
||

518 | fun decl -> match decl.top_decl_desc with |
||

519 | | Node nd -> {decl with top_decl_desc = Node (node_unfold_consts consts nd)} |
||

520 | | _ -> decl |
||

521 | ) prog |
||

522 | |||

523 | e2380d4d | ploc | |

524 | |||

525 | (************************************************************************) |
||

526 | (* Renaming *) |
||

527 | |||

528 | 22fe1c93 | ploc | (* applies the renaming function [fvar] to all variables of expression [expr] *) |

529 | let rec expr_replace_var fvar expr = |
||

530 | { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } |
||

531 | |||

532 | and expr_desc_replace_var fvar expr_desc = |
||

533 | match expr_desc with |
||

534 | | Expr_const _ -> expr_desc |
||

535 | | Expr_ident i -> Expr_ident (fvar i) |
||

536 | | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) |
||

537 | | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) |
||

538 | | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) |
||

539 | | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) |
||

540 | | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) |
||

541 | | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) |
||

542 | | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) |
||

543 | | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') |
||

544 | | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) |
||

545 | | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) |
||

546 | | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) -> fvar x, l) i') |
||

547 | | _ -> assert false |
||

548 | |||

549 | (* Applies the renaming function [fvar] to every rhs |
||

550 | only when the corresponding lhs satisfies predicate [pvar] *) |
||

551 | let eq_replace_rhs_var pvar fvar eq = |
||

552 | let pvar l = List.exists pvar l in |
||

553 | let rec replace lhs rhs = |
||

554 | { rhs with expr_desc = replace_desc lhs rhs.expr_desc } |
||

555 | and replace_desc lhs rhs_desc = |
||

556 | match lhs with |
||

557 | | [] -> assert false |
||

558 | | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc |
||

559 | | _ -> |
||

560 | (match rhs_desc with |
||

561 | | Expr_tuple tl -> |
||

562 | Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl) |
||

563 | | Expr_appl (f, arg, None) when Basic_library.is_internal_fun f -> |
||

564 | let args = expr_list_of_expr arg in |
||

565 | Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None) |
||

566 | | Expr_array _ |
||

567 | | Expr_access _ |
||

568 | | Expr_power _ |
||

569 | | Expr_const _ |
||

570 | | Expr_ident _ |
||

571 | | Expr_appl _ -> |
||

572 | if pvar lhs |
||

573 | then expr_desc_replace_var fvar rhs_desc |
||

574 | else rhs_desc |
||

575 | | Expr_ite (c, t, e) -> Expr_ite (replace lhs c, replace lhs t, replace lhs e) |
||

576 | | Expr_arrow (e1, e2) -> Expr_arrow (replace lhs e1, replace lhs e2) |
||

577 | | Expr_fby (e1, e2) -> Expr_fby (replace lhs e1, replace lhs e2) |
||

578 | | Expr_pre e' -> Expr_pre (replace lhs e') |
||

579 | | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i |
||

580 | in Expr_when (replace lhs e', i', l) |
||

581 | | Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i |
||

582 | in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl) |
||

583 | | _ -> assert false) |
||

584 | in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } |
||

585 | |||

586 | e2380d4d | ploc | |

587 | let rec rename_expr f_node f_var f_const expr = |
||

588 | { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc } |
||

589 | and rename_expr_desc f_node f_var f_const expr_desc = |
||

590 | let re = rename_expr f_node f_var f_const in |
||

591 | match expr_desc with |
||

592 | | Expr_const _ -> expr_desc |
||

593 | | Expr_ident i -> Expr_ident (f_var i) |
||

594 | | Expr_array el -> Expr_array (List.map re el) |
||

595 | | Expr_access (e1, d) -> Expr_access (re e1, d) |
||

596 | | Expr_power (e1, d) -> Expr_power (re e1, d) |
||

597 | | Expr_tuple el -> Expr_tuple (List.map re el) |
||

598 | | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e) |
||

599 | | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) |
||

600 | | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2) |
||

601 | | Expr_pre e' -> Expr_pre (re e') |
||

602 | | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l) |
||

603 | | Expr_merge (i, hl) -> |
||

604 | Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl) |
||

605 | | Expr_appl (i, e', i') -> |
||

606 | Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i') |
||

607 | | _ -> assert false |
||

608 | |||

609 | let rename_node_annot f_node f_var f_const expr = |
||

610 | 592f508c | ploc | expr |

611 | (* TODO assert false *) |
||

612 | e2380d4d | ploc | |

613 | let rename_expr_annot f_node f_var f_const annot = |
||

614 | 592f508c | ploc | annot |

615 | (* TODO assert false *) |
||

616 | e2380d4d | ploc | |

617 | let rename_node f_node f_var f_const nd = |
||

618 | let rename_var v = { v with var_id = f_var v.var_id } in |
||

619 | let inputs = List.map rename_var nd.node_inputs in |
||

620 | let outputs = List.map rename_var nd.node_outputs in |
||

621 | let locals = List.map rename_var nd.node_locals in |
||

622 | let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in |
||

623 | let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in |
||

624 | let node_asserts = List.map |
||

625 | (fun a -> |
||

626 | { a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } |
||

627 | ) nd.node_asserts |
||

628 | in |
||

629 | let eqs = List.map |
||

630 | (fun eq -> { eq with |
||

631 | eq_lhs = List.map f_var eq.eq_lhs; |
||

632 | eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs |
||

633 | } ) nd.node_eqs |
||

634 | in |
||

635 | let spec = |
||

636 | Utils.option_map |
||

637 | (fun s -> rename_node_annot f_node f_var f_const s) |
||

638 | nd.node_spec |
||

639 | in |
||

640 | let annot = |
||

641 | Utils.option_map |
||

642 | (fun s -> rename_expr_annot f_node f_var f_const s) |
||

643 | nd.node_annot |
||

644 | in |
||

645 | { |
||

646 | node_id = f_node nd.node_id; |
||

647 | node_type = nd.node_type; |
||

648 | node_clock = nd.node_clock; |
||

649 | node_inputs = inputs; |
||

650 | node_outputs = outputs; |
||

651 | node_locals = locals; |
||

652 | node_gencalls = gen_calls; |
||

653 | node_checks = node_checks; |
||

654 | node_asserts = node_asserts; |
||

655 | node_eqs = eqs; |
||

656 | 52cfee34 | xthirioux | node_dec_stateless = nd.node_dec_stateless; |

657 | node_stateless = nd.node_stateless; |
||

658 | e2380d4d | ploc | node_spec = spec; |

659 | node_annot = annot; |
||

660 | } |
||

661 | |||

662 | |||

663 | let rename_const f_const c = |
||

664 | { c with const_id = f_const c.const_id } |
||

665 | |||

666 | let rename_prog f_node f_var f_const prog = |
||

667 | List.rev ( |
||

668 | List.fold_left (fun accu top -> |
||

669 | (match top.top_decl_desc with |
||

670 | | Node nd -> |
||

671 | { top with top_decl_desc = Node (rename_node f_node f_var f_const nd) } |
||

672 | | Consts c -> |
||

673 | { top with top_decl_desc = Consts (List.map (rename_const f_const) c) } |
||

674 | | ImportedNode _ |
||

675 | | Open _ -> top) |
||

676 | ::accu |
||

677 | ) [] prog |
||

678 | ) |
||

679 | |||

680 | (**********************************************************************) |
||

681 | 22fe1c93 | ploc | (* Pretty printers *) |

682 | |||

683 | let pp_decl_type fmt tdecl = |
||

684 | match tdecl.top_decl_desc with |
||

685 | | Node nd -> |
||

686 | fprintf fmt "%s: " nd.node_id; |
||

687 | Utils.reset_names (); |
||

688 | fprintf fmt "%a@ " Types.print_ty nd.node_type |
||

689 | | ImportedNode ind -> |
||

690 | fprintf fmt "%s: " ind.nodei_id; |
||

691 | Utils.reset_names (); |
||

692 | fprintf fmt "%a@ " Types.print_ty ind.nodei_type |
||

693 | 5c1184ad | ploc | | Consts _ | Open _ -> () |

694 | 22fe1c93 | ploc | |

695 | let pp_prog_type fmt tdecl_list = |
||

696 | Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list |
||

697 | |||

698 | let pp_decl_clock fmt cdecl = |
||

699 | match cdecl.top_decl_desc with |
||

700 | | Node nd -> |
||

701 | fprintf fmt "%s: " nd.node_id; |
||

702 | Utils.reset_names (); |
||

703 | fprintf fmt "%a@ " Clocks.print_ck nd.node_clock |
||

704 | | ImportedNode ind -> |
||

705 | fprintf fmt "%s: " ind.nodei_id; |
||

706 | 5c1184ad | ploc | Utils.reset_names (); |

707 | fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock |
||

708 | 52cfee34 | xthirioux | | Consts _ | Open _ -> () |

709 | 22fe1c93 | ploc | |

710 | let pp_prog_clock fmt prog = |
||

711 | Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog |
||

712 | |||

713 | let pp_error fmt = function |
||

714 | Main_not_found -> |
||

715 | fprintf fmt "Cannot compile node %s: could not find the node definition.@." |
||

716 | !Options.main_node |
||

717 | | Main_wrong_kind -> |
||

718 | fprintf fmt |
||

719 | "Name %s does not correspond to a (non-imported) node definition.@." |
||

720 | !Options.main_node |
||

721 | | No_main_specified -> |
||

722 | fprintf fmt "No main node specified@." |
||

723 | 21485807 | xthirioux | | Unbound_symbol sym -> |

724 | fprintf fmt |
||

725 | "%s is undefined.@." |
||

726 | sym |
||

727 | | Already_bound_symbol sym -> |
||

728 | fprintf fmt |
||

729 | "%s is already defined.@." |
||

730 | sym |
||

731 | 22fe1c93 | ploc | |

732 | (* filling node table with internal functions *) |
||

733 | let vdecls_of_typ_ck cpt ty = |
||

734 | let loc = Location.dummy_loc in |
||

735 | List.map |
||

736 | (fun _ -> incr cpt; |
||

737 | let name = sprintf "_var_%d" !cpt in |
||

738 | mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false)) |
||

739 | (Types.type_list_of_type ty) |
||

740 | |||

741 | let mk_internal_node id = |
||

742 | let spec = None in |
||

743 | let ty = Env.lookup_value Basic_library.type_env id in |
||

744 | let ck = Env.lookup_value Basic_library.clock_env id in |
||

745 | let (tin, tout) = Types.split_arrow ty in |
||

746 | (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*) |
||

747 | let cpt = ref (-1) in |
||

748 | mktop_decl Location.dummy_loc |
||

749 | (ImportedNode |
||

750 | {nodei_id = id; |
||

751 | nodei_type = ty; |
||

752 | nodei_clock = ck; |
||

753 | nodei_inputs = vdecls_of_typ_ck cpt tin; |
||

754 | nodei_outputs = vdecls_of_typ_ck cpt tout; |
||

755 | nodei_stateless = Types.get_static_value ty <> None; |
||

756 | nodei_spec = spec}) |
||

757 | |||

758 | let add_internal_funs () = |
||

759 | List.iter |
||

760 | (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd) |
||

761 | Basic_library.internal_funs |
||

762 | |||

763 | (* Local Variables: *) |
||

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

765 | (* End: *) |