## lustrec / src / corelang.ml @ 22fe1c93

History | View | Annotate | Download (21.9 KB)

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

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

43 |
type type_dec = LustreSpec.type_dec |

44 | |

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

46 | |

47 | |

48 |
type clock_dec = LustreSpec.clock_dec |

49 | |

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

51 | |

52 |
type var_decl = LustreSpec.var_decl |

53 | |

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

55 |
different instances of the same node *) |

56 |
type expr = |

57 |
{expr_tag: tag; |

58 |
expr_desc: expr_desc; |

59 |
mutable expr_type: Types.type_expr; |

60 |
mutable expr_clock: Clocks.clock_expr; |

61 |
mutable expr_delay: Delay.delay_expr; |

62 |
mutable expr_annot: LustreSpec.expr_annot option; |

63 |
expr_loc: Location.t} |

64 | |

65 |
and expr_desc = |

66 |
| Expr_const of constant |

67 |
| Expr_ident of ident |

68 |
| Expr_tuple of expr list |

69 |
| Expr_ite of expr * expr * expr |

70 |
| Expr_arrow of expr * expr |

71 |
| Expr_fby of expr * expr |

72 |
| Expr_array of expr list |

73 |
| Expr_access of expr * Dimension.dim_expr |

74 |
| Expr_power of expr * Dimension.dim_expr |

75 |
| Expr_pre of expr |

76 |
| Expr_when of expr * ident * label |

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

78 |
| Expr_appl of ident * expr * (ident * label) option |

79 |
| Expr_uclock of expr * int |

80 |
| Expr_dclock of expr * int |

81 |
| Expr_phclock of expr * rat |

82 | |

83 | |

84 |
type eq = |

85 |
{eq_lhs: ident list; |

86 |
eq_rhs: expr; |

87 |
eq_loc: Location.t} |

88 | |

89 |
type assert_t = |

90 |
{ |

91 |
assert_expr: expr; |

92 |
assert_loc: Location.t |

93 |
} |

94 | |

95 |
type node_desc = |

96 |
{node_id: ident; |

97 |
mutable node_type: Types.type_expr; |

98 |
mutable node_clock: Clocks.clock_expr; |

99 |
node_inputs: var_decl list; |

100 |
node_outputs: var_decl list; |

101 |
node_locals: var_decl list; |

102 |
mutable node_gencalls: expr list; |

103 |
mutable node_checks: Dimension.dim_expr list; |

104 |
node_asserts: assert_t list; |

105 |
node_eqs: eq list; |

106 |
node_spec: LustreSpec.node_annot option; |

107 |
node_annot: LustreSpec.expr_annot option; |

108 |
} |

109 | |

110 |
type imported_node_desc = |

111 |
{nodei_id: ident; |

112 |
mutable nodei_type: Types.type_expr; |

113 |
mutable nodei_clock: Clocks.clock_expr; |

114 |
nodei_inputs: var_decl list; |

115 |
nodei_outputs: var_decl list; |

116 |
nodei_stateless: bool; |

117 |
nodei_spec: LustreSpec.node_annot option; |

118 |
} |

119 | |

120 |
type imported_fun_desc = |

121 |
{fun_id: ident; |

122 |
mutable fun_type: Types.type_expr; |

123 |
fun_inputs: var_decl list; |

124 |
fun_outputs: var_decl list; |

125 |
fun_spec: LustreSpec.node_annot option;} |

126 | |

127 |
type const_desc = |

128 |
{const_id: ident; |

129 |
const_loc: Location.t; |

130 |
const_value: constant; |

131 |
mutable const_type: Types.type_expr; |

132 |
} |

133 | |

134 |
type top_decl_desc = |

135 |
| Node of node_desc |

136 |
| Consts of const_desc list |

137 |
| ImportedNode of imported_node_desc |

138 |
| ImportedFun of imported_fun_desc |

139 |
| Include of string |

140 | |

141 |
type top_decl = |

142 |
{top_decl_desc: top_decl_desc; |

143 |
top_decl_loc: Location.t} |

144 | |

145 |
type program = top_decl list |

146 | |

147 |
type error = |

148 |
Main_not_found |

149 |
| Main_wrong_kind |

150 |
| No_main_specified |

151 | |

152 | |

153 |
module VDeclModule = |

154 |
struct (* Node module *) |

155 |
type t = var_decl |

156 |
let compare v1 v2 = compare v1 v2 |

157 |
let hash n = Hashtbl.hash n |

158 |
let equal n1 n2 = n1 = n2 |

159 |
end |

160 | |

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

162 | |

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

164 | |

165 |
(************************************************************) |

166 |
(* *) |

167 | |

168 |
let mktyp loc d = |

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

170 | |

171 |
let mkclock loc d = |

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

173 | |

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

175 |
{ var_id = id; |

176 |
var_dec_type = ty_dec; |

177 |
var_dec_clock = ck_dec; |

178 |
var_dec_const = is_const; |

179 |
var_type = Types.new_var (); |

180 |
var_clock = Clocks.new_var true; |

181 |
var_loc = loc } |

182 | |

183 |
let mkexpr loc d = |

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

185 |
expr_desc = d; |

186 |
expr_type = Types.new_var (); |

187 |
expr_clock = Clocks.new_var true; |

188 |
expr_delay = Delay.new_var (); |

189 |
expr_annot = None; |

190 |
expr_loc = loc } |

191 | |

192 |
let var_decl_of_const c = |

193 |
{ var_id = c.const_id; |

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

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

196 |
var_dec_const = true; |

197 |
var_type = c.const_type; |

198 |
var_clock = Clocks.new_var false; |

199 |
var_loc = c.const_loc } |

200 | |

201 |
let mk_new_name vdecl_list id = |

202 |
let rec new_name name cpt = |

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

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

205 |
else name |

206 |
in new_name id 1 |

207 | |

208 |
let update_expr_annot e annot = |

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

210 | |

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

212 |
{ eq_lhs = lhs; |

213 |
eq_rhs = rhs; |

214 |
eq_loc = loc } |

215 | |

216 |
let mkassert loc expr = |

217 |
{ assert_loc = loc; |

218 |
assert_expr = expr |

219 |
} |

220 | |

221 |
let mktop_decl loc d = |

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

223 | |

224 |
let mkpredef_call loc funname args = |

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

226 | |

227 |
let mkpredef_unary_call loc funname arg = |

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

229 | |

230 | |

231 |
(***********************************************************) |

232 |
exception Error of error |

233 |
exception Unbound_type of type_dec_desc*Location.t |

234 |
exception Already_bound_label of label*type_dec_desc*Location.t |

235 | |

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

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

238 |
let consts_table = Hashtbl.create 30 |

239 | |

240 |
let node_name td = |

241 |
match td.top_decl_desc with |

242 |
| Node nd -> nd.node_id |

243 |
| ImportedNode nd -> nd.nodei_id |

244 |
| _ -> assert false |

245 | |

246 |
let is_generic_node td = |

247 |
match td.top_decl_desc with |

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

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

250 |
| _ -> assert false |

251 | |

252 |
let node_inputs td = |

253 |
match td.top_decl_desc with |

254 |
| Node nd -> nd.node_inputs |

255 |
| ImportedNode nd -> nd.nodei_inputs |

256 |
| _ -> assert false |

257 | |

258 |
let node_from_name id = |

259 |
try |

260 |
Hashtbl.find node_table id |

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

262 |
assert false) |

263 | |

264 |
let is_imported_node td = |

265 |
match td.top_decl_desc with |

266 |
| Node nd -> false |

267 |
| ImportedNode nd -> true |

268 |
| _ -> assert false |

269 | |

270 |
(* alias and type definition table *) |

271 |
let type_table = |

272 |
Utils.create_hashtable 20 [ |

273 |
Tydec_int , Tydec_int; |

274 |
Tydec_bool , Tydec_bool; |

275 |
Tydec_float, Tydec_float; |

276 |
Tydec_real , Tydec_real |

277 |
] |

278 | |

279 |
let rec is_user_type typ = |

280 |
match typ with |

281 |
| Tydec_int | Tydec_bool | Tydec_real |

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

283 |
| Tydec_clock typ' -> is_user_type typ' |

284 |
| _ -> true |

285 | |

286 |
let get_repr_type typ = |

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

288 |
if is_user_type typ_def then typ else typ_def |

289 | |

290 |
let tag_true = "true" |

291 |
let tag_false = "false" |

292 | |

293 |
let const_is_bool c = |

294 |
match c with |

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

296 |
| _ -> false |

297 | |

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

299 |
let const_negation c = |

300 |
assert (const_is_bool c); |

301 |
match c with |

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

303 |
| _ -> Const_tag tag_true |

304 | |

305 |
let const_or c1 c2 = |

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

307 |
match c1, c2 with |

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

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

310 |
| _ -> Const_tag tag_false |

311 | |

312 |
let const_and c1 c2 = |

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

314 |
match c1, c2 with |

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

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

317 |
| _ -> Const_tag tag_true |

318 | |

319 |
let const_xor c1 c2 = |

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

321 |
match c1, c2 with |

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

323 |
| _ -> Const_tag tag_false |

324 | |

325 |
let const_impl c1 c2 = |

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

327 |
match c1, c2 with |

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

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

330 |
| _ -> Const_tag tag_false |

331 | |

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

333 |
let tag_table = |

334 |
Utils.create_hashtable 20 [ |

335 |
tag_true, Tydec_bool; |

336 |
tag_false, Tydec_bool |

337 |
] |

338 | |

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

347 |
let const_of_bool b = |

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

349 | |

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

351 | |

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

353 |
let expr_of_ident id loc = |

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

355 |
expr_desc = Expr_ident id; |

356 |
expr_type = Types.new_var (); |

357 |
expr_clock = Clocks.new_var true; |

358 |
expr_delay = Delay.new_var (); |

359 |
expr_loc = loc; |

360 |
expr_annot = None} |

361 | |

362 |
let expr_list_of_expr expr = |

363 |
match expr.expr_desc with |

364 |
| Expr_tuple elist -> |

365 |
elist |

366 |
| _ -> [expr] |

367 | |

368 |
let expr_of_expr_list loc elist = |

369 |
match elist with |

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

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

372 |
| _ -> assert false |

373 | |

374 |
let call_of_expr expr = |

375 |
match expr.expr_desc with |

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

377 |
| _ -> assert false |

378 | |

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

380 |
let rec expr_of_dimension dim = |

381 |
match dim.dim_desc with |

382 |
| Dbool b -> |

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

384 |
| Dint i -> |

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

386 |
| Dident id -> |

387 |
mkexpr dim.dim_loc (Expr_ident id) |

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

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

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

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

392 |
| Dlink dim' -> expr_of_dimension dim' |

393 |
| Dvar |

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

395 |
assert false) |

396 | |

397 |
let dimension_of_const loc const = |

398 |
match const with |

399 |
| Const_int i -> mkdim_int loc i |

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

401 |
| _ -> raise InvalidDimension |

402 | |

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

404 |
into dimension expressions *) |

405 |
let rec dimension_of_expr expr = |

406 |
match expr.expr_desc with |

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

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

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

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

411 |
if k = None then raise InvalidDimension; |

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

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

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

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

416 | |

417 | |

418 |
let sort_handlers hl = |

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

420 | |

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

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

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

424 |
| Expr_array el1, Expr_array el2 |

425 |
| Expr_tuple el1, Expr_tuple el2 -> |

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

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

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

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

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

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

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

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

434 |
| 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') |

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

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

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

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

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

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

441 |
| _ -> false |

442 | |

443 |
let node_vars nd = |

444 |
nd.node_inputs @ nd.node_locals @ nd.node_outputs |

445 | |

446 |
let node_var id node = |

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

448 | |

449 |
let node_eq id node = |

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

451 | |

452 |
(* Consts unfoooolding *) |

453 |
let is_const i consts = |

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

455 | |

456 |
let get_const i consts = |

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

458 |
c.const_value |

459 | |

460 |
let rec expr_unfold_consts consts e = |

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

462 | |

463 |
and expr_desc_unfold_consts consts e = |

464 |
let unfold = expr_unfold_consts consts in |

465 |
match e with |

466 |
| Expr_const _ -> e |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

483 |
| Expr_phclock _ -> e |

484 | |

485 |
let eq_unfold_consts consts eq = |

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

487 | |

488 |
let node_unfold_consts consts node = |

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

490 | |

491 |
let get_consts prog = |

492 |
List.fold_left ( |

493 |
fun consts decl -> |

494 |
match decl.top_decl_desc with |

495 |
| Consts clist -> clist@consts |

496 |
| Node _ | ImportedNode _ | ImportedFun _ | Include _ -> consts |

497 |
) [] prog |

498 | |

499 | |

500 |
let get_nodes prog = |

501 |
List.fold_left ( |

502 |
fun nodes decl -> |

503 |
match decl.top_decl_desc with |

504 |
| Node nd -> nd::nodes |

505 |
| Consts _ | ImportedNode _ | ImportedFun _ | Include _ -> nodes |

506 |
) [] prog |

507 | |

508 |
let prog_unfold_consts prog = |

509 |
let consts = get_consts prog in |

510 |
List.map ( |

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

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

513 |
| _ -> decl |

514 |
) prog |

515 | |

516 |
(* applies the renaming function [fvar] to all variables of expression [expr] *) |

517 |
let rec expr_replace_var fvar expr = |

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

519 | |

520 |
and expr_desc_replace_var fvar expr_desc = |

521 |
match expr_desc with |

522 |
| Expr_const _ -> expr_desc |

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

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

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

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

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

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

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

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

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

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

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

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

535 |
| _ -> assert false |

536 | |

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

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

539 |
let eq_replace_rhs_var pvar fvar eq = |

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

541 |
let rec replace lhs rhs = |

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

543 |
and replace_desc lhs rhs_desc = |

544 |
match lhs with |

545 |
| [] -> assert false |

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

547 |
| _ -> |

548 |
(match rhs_desc with |

549 |
| Expr_tuple tl -> |

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

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

552 |
let args = expr_list_of_expr arg in |

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

554 |
| Expr_array _ |

555 |
| Expr_access _ |

556 |
| Expr_power _ |

557 |
| Expr_const _ |

558 |
| Expr_ident _ |

559 |
| Expr_appl _ -> |

560 |
if pvar lhs |

561 |
then expr_desc_replace_var fvar rhs_desc |

562 |
else rhs_desc |

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

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

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

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

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

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

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

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

571 |
| _ -> assert false) |

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

573 | |

574 |
(* Pretty printers *) |

575 | |

576 |
let pp_decl_type fmt tdecl = |

577 |
match tdecl.top_decl_desc with |

578 |
| Node nd -> |

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

580 |
Utils.reset_names (); |

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

582 |
| ImportedNode ind -> |

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

584 |
Utils.reset_names (); |

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

586 |
| ImportedFun ind -> |

587 |
fprintf fmt "%s: " ind.fun_id; |

588 |
Utils.reset_names (); |

589 |
fprintf fmt "%a@ " Types.print_ty ind.fun_type |

590 |
| Consts _ | Include _ -> () |

591 | |

592 |
let pp_prog_type fmt tdecl_list = |

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

594 | |

595 |
let pp_decl_clock fmt cdecl = |

596 |
match cdecl.top_decl_desc with |

597 |
| Node nd -> |

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

599 |
Utils.reset_names (); |

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

601 |
| ImportedNode ind -> |

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

603 |
Utils.reset_names (); |

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

605 |
| ImportedFun _ | Consts _ | Include _ -> () |

606 | |

607 |
let pp_prog_clock fmt prog = |

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

609 | |

610 |
let pp_error fmt = function |

611 |
Main_not_found -> |

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

613 |
!Options.main_node |

614 |
| Main_wrong_kind -> |

615 |
fprintf fmt |

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

617 |
!Options.main_node |

618 |
| No_main_specified -> |

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

620 | |

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

622 |
let vdecls_of_typ_ck cpt ty = |

623 |
let loc = Location.dummy_loc in |

624 |
List.map |

625 |
(fun _ -> incr cpt; |

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

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

628 |
(Types.type_list_of_type ty) |

629 | |

630 |
let mk_internal_node id = |

631 |
let spec = None in |

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

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

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

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

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

637 |
mktop_decl Location.dummy_loc |

638 |
(ImportedNode |

639 |
{nodei_id = id; |

640 |
nodei_type = ty; |

641 |
nodei_clock = ck; |

642 |
nodei_inputs = vdecls_of_typ_ck cpt tin; |

643 |
nodei_outputs = vdecls_of_typ_ck cpt tout; |

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

645 |
nodei_spec = spec}) |

646 | |

647 |
let add_internal_funs () = |

648 |
List.iter |

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

650 |
Basic_library.internal_funs |

651 | |

652 |
(* Local Variables: *) |

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

654 |
(* End: *) |