1

(* 

2

* SchedMCore  A MultiCore Scheduling Framework

3

* Copyright (C) 20092011, 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 021111307

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

 Const_struct of (label * constant) list

43


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

 Expr_appl of call_t

80

 Expr_uclock of expr * int

81

 Expr_dclock of expr * int

82

 Expr_phclock of expr * rat

83

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

84


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

mutable node_dec_stateless: bool;

108

mutable node_stateless: bool option;

109

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

nodei_prototype: string option;

122

nodei_in_lib: string option;

123

}

124


125

type const_desc =

126

{const_id: ident;

127

const_loc: Location.t;

128

const_value: constant;

129

mutable const_type: Types.type_expr;

130

}

131


132

type top_decl_desc =

133

 Node of node_desc

134

 Consts of const_desc list

135

 ImportedNode of imported_node_desc

136

 Open of bool * string (* the boolean set to true denotes a local

137

lusi vs a lusi installed at system level *)

138


139

type top_decl =

140

{top_decl_desc: top_decl_desc;

141

top_decl_loc: Location.t}

142


143

type program = top_decl list

144


145

type error =

146

Main_not_found

147

 Main_wrong_kind

148

 No_main_specified

149

 Unbound_symbol of ident

150

 Already_bound_symbol of ident

151


152

exception Error of Location.t * error

153


154

module VDeclModule =

155

struct (* Node module *)

156

type t = var_decl

157

let compare v1 v2 = compare v1 v2

158

let hash n = Hashtbl.hash n

159

let equal n1 n2 = n1 = n2

160

end

161


162

module VMap = Map.Make(VDeclModule)

163


164

module VSet = Set.Make(VDeclModule)

165


166

(************************************************************)

167

(* *)

168


169

let mktyp loc d =

170

{ ty_dec_desc = d; ty_dec_loc = loc }

171


172

let mkclock loc d =

173

{ ck_dec_desc = d; ck_dec_loc = loc }

174


175

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

176

{ var_id = id;

177

var_dec_type = ty_dec;

178

var_dec_clock = ck_dec;

179

var_dec_const = is_const;

180

var_type = Types.new_var ();

181

var_clock = Clocks.new_var true;

182

var_loc = loc }

183


184

let mkexpr loc d =

185

{ expr_tag = Utils.new_tag ();

186

expr_desc = d;

187

expr_type = Types.new_var ();

188

expr_clock = Clocks.new_var true;

189

expr_delay = Delay.new_var ();

190

expr_annot = None;

191

expr_loc = loc }

192


193

let var_decl_of_const c =

194

{ var_id = c.const_id;

195

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

196

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

197

var_dec_const = true;

198

var_type = c.const_type;

199

var_clock = Clocks.new_var false;

200

var_loc = c.const_loc }

201


202

let mk_new_name vdecl_list id =

203

let rec new_name name cpt =

204

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

205

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

206

else name

207

in new_name id 1

208


209

let update_expr_annot e annot =

210

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

211


212

let mkeq loc (lhs, rhs) =

213

{ eq_lhs = lhs;

214

eq_rhs = rhs;

215

eq_loc = loc }

216


217

let mkassert loc expr =

218

{ assert_loc = loc;

219

assert_expr = expr

220

}

221


222

let mktop_decl loc d =

223

{ top_decl_desc = d; top_decl_loc = loc }

224


225

let mkpredef_call loc funname args =

226

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

227


228

(***********************************************************)

229

(* Fast access to nodes, by name *)

230

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

231

let consts_table = Hashtbl.create 30

232


233

let node_name td =

234

match td.top_decl_desc with

235

 Node nd > nd.node_id

236

 ImportedNode nd > nd.nodei_id

237

 _ > assert false

238


239

let is_generic_node td =

240

match td.top_decl_desc with

241

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

242

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

243

 _ > assert false

244


245

let node_inputs td =

246

match td.top_decl_desc with

247

 Node nd > nd.node_inputs

248

 ImportedNode nd > nd.nodei_inputs

249

 _ > assert false

250


251

let node_from_name id =

252

try

253

Hashtbl.find node_table id

254

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

255

assert false)

256


257

let is_imported_node td =

258

match td.top_decl_desc with

259

 Node nd > false

260

 ImportedNode nd > true

261

 _ > assert false

262


263


264

(* alias and type definition table *)

265

let type_table =

266

Utils.create_hashtable 20 [

267

Tydec_int , Tydec_int;

268

Tydec_bool , Tydec_bool;

269

Tydec_float, Tydec_float;

270

Tydec_real , Tydec_real

271

]

272


273

let rec is_user_type typ =

274

match typ with

275

 Tydec_int  Tydec_bool  Tydec_real

276

 Tydec_float  Tydec_any  Tydec_const _ > false

277

 Tydec_clock typ' > is_user_type typ'

278

 _ > true

279


280

let get_repr_type typ =

281

let typ_def = Hashtbl.find type_table typ in

282

if is_user_type typ_def then typ else typ_def

283


284

let tag_true = "true"

285

let tag_false = "false"

286


287

let const_is_bool c =

288

match c with

289

 Const_tag t > t = tag_true  t = tag_false

290

 _ > false

291


292

(* Computes the negation of a boolean constant *)

293

let const_negation c =

294

assert (const_is_bool c);

295

match c with

296

 Const_tag t when t = tag_true > Const_tag tag_false

297

 _ > Const_tag tag_true

298


299

let const_or c1 c2 =

300

assert (const_is_bool c1 && const_is_bool c2);

301

match c1, c2 with

302

 Const_tag t1, _ when t1 = tag_true > c1

303

 _ , Const_tag t2 when t2 = tag_true > c2

304

 _ > Const_tag tag_false

305


306

let const_and c1 c2 =

307

assert (const_is_bool c1 && const_is_bool c2);

308

match c1, c2 with

309

 Const_tag t1, _ when t1 = tag_false > c1

310

 _ , Const_tag t2 when t2 = tag_false > c2

311

 _ > Const_tag tag_true

312


313

let const_xor c1 c2 =

314

assert (const_is_bool c1 && const_is_bool c2);

315

match c1, c2 with

316

 Const_tag t1, Const_tag t2 when t1 <> t2 > Const_tag tag_true

317

 _ > Const_tag tag_false

318


319

let const_impl c1 c2 =

320

assert (const_is_bool c1 && const_is_bool c2);

321

match c1, c2 with

322

 Const_tag t1, _ when t1 = tag_false > Const_tag tag_true

323

 _ , Const_tag t2 when t2 = tag_true > Const_tag tag_true

324

 _ > Const_tag tag_false

325


326

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

327

let tag_table =

328

Utils.create_hashtable 20 [

329

tag_true, Tydec_bool;

330

tag_false, Tydec_bool

331

]

332


333

(* To guarantee uniqueness of fields in struct types *)

334

let field_table =

335

Utils.create_hashtable 20 [

336

]

337


338

let get_enum_type_tags cty =

339

match cty with

340

 Tydec_bool > [tag_true; tag_false]

341

 Tydec_const _ > (match Hashtbl.find type_table cty with

342

 Tydec_enum tl > tl

343

 _ > assert false)

344

 _ > assert false

345


346

let get_struct_type_fields cty =

347

match cty with

348

 Tydec_const _ > (match Hashtbl.find type_table cty with

349

 Tydec_struct fl > fl

350

 _ > assert false)

351

 _ > assert false

352


353

let const_of_bool b =

354

Const_tag (if b then tag_true else tag_false)

355


356

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

357


358

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

359

let expr_of_ident id loc =

360

{expr_tag = Utils.new_tag ();

361

expr_desc = Expr_ident id;

362

expr_type = Types.new_var ();

363

expr_clock = Clocks.new_var true;

364

expr_delay = Delay.new_var ();

365

expr_loc = loc;

366

expr_annot = None}

367


368

let is_tuple_expr expr =

369

match expr.expr_desc with

370

 Expr_tuple _ > true

371

 _ > false

372


373

let expr_list_of_expr expr =

374

match expr.expr_desc with

375

 Expr_tuple elist >

376

elist

377

 _ > [expr]

378


379

let expr_of_expr_list loc elist =

380

match elist with

381

 [t] > { t with expr_loc = loc }

382

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

383

 _ > assert false

384


385

let call_of_expr expr =

386

match expr.expr_desc with

387

 Expr_appl (f, args, r) > (f, expr_list_of_expr args, r)

388

 _ > assert false

389


390

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

391

let rec expr_of_dimension dim =

392

match dim.dim_desc with

393

 Dbool b >

394

mkexpr dim.dim_loc (Expr_const (const_of_bool b))

395

 Dint i >

396

mkexpr dim.dim_loc (Expr_const (Const_int i))

397

 Dident id >

398

mkexpr dim.dim_loc (Expr_ident id)

399

 Dite (c, t, e) >

400

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

401

 Dappl (id, args) >

402

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

403

 Dlink dim' > expr_of_dimension dim'

404

 Dvar

405

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

406

assert false)

407


408

let dimension_of_const loc const =

409

match const with

410

 Const_int i > mkdim_int loc i

411

 Const_tag t when t = tag_true  t = tag_false > mkdim_bool loc (t = tag_true)

412

 _ > raise InvalidDimension

413


414

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

415

into dimension expressions *)

416

let rec dimension_of_expr expr =

417

match expr.expr_desc with

418

 Expr_const c > dimension_of_const expr.expr_loc c

419

 Expr_ident id > mkdim_ident expr.expr_loc id

420

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

421

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

422

if k = None then raise InvalidDimension;

423

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

424

 Expr_ite (i, t, e) >

425

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

426

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

427


428


429

let sort_handlers hl =

430

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

431


432

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

433

 Expr_const c1, Expr_const c2 > c1 = c2

434

 Expr_ident i1, Expr_ident i2 > i1 = i2

435

 Expr_array el1, Expr_array el2

436

 Expr_tuple el1, Expr_tuple el2 >

437

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

438

 Expr_arrow (e1, e2), Expr_arrow (e1', e2') > is_eq_expr e1 e1' && is_eq_expr e2 e2'

439

 Expr_fby (e1,e2), Expr_fby (e1',e2') > is_eq_expr e1 e1' && is_eq_expr e2 e2'

440

 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

441

(*  Expr_concat (e1,e2), Expr_concat (e1',e2') > is_eq_expr e1 e1' && is_eq_expr e2 e2' *)

442

(*  Expr_tail e, Expr_tail e' > is_eq_expr e e' *)

443

 Expr_pre e, Expr_pre e' > is_eq_expr e e'

444

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

445

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

446

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

447

 Expr_uclock(e, i), Expr_uclock(e', i') > i=i' && is_eq_expr e e'

448

 Expr_dclock(e, i), Expr_dclock(e', i') > i=i' && is_eq_expr e e'

449

 Expr_phclock(e, r), Expr_phclock(e', r') > r=r' && is_eq_expr e e'

450

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

451

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

452

 _ > false

453


454

let node_vars nd =

455

nd.node_inputs @ nd.node_locals @ nd.node_outputs

456


457

let node_var id node =

458

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

459


460

let node_eq id node =

461

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

462


463

(* Consts unfoooolding *)

464

let is_const i consts =

465

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

466


467

let get_const i consts =

468

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

469

c.const_value

470


471

let rec expr_unfold_consts consts e =

472

{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc }

473


474

and expr_desc_unfold_consts consts e =

475

let unfold = expr_unfold_consts consts in

476

match e with

477

 Expr_const _ > e

478

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

479

 Expr_array el > Expr_array (List.map unfold el)

480

 Expr_access (e1, d) > Expr_access (unfold e1, d)

481

 Expr_power (e1, d) > Expr_power (unfold e1, d)

482

 Expr_tuple el > Expr_tuple (List.map unfold el)

483

 Expr_ite (c, t, e) > Expr_ite (unfold c, unfold t, unfold e)

484

 Expr_arrow (e1, e2)> Expr_arrow (unfold e1, unfold e2)

485

 Expr_fby (e1, e2) > Expr_fby (unfold e1, unfold e2)

486

(*  Expr_concat (e1, e2) > Expr_concat (unfold e1, unfold e2) *)

487

(*  Expr_tail e' > Expr_tail (unfold e') *)

488

 Expr_pre e' > Expr_pre (unfold e')

489

 Expr_when (e', i, l)> Expr_when (unfold e', i, l)

490

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

491

 Expr_appl (i, e', i') > Expr_appl (i, unfold e', i')

492

 Expr_uclock (e', i) > Expr_uclock (unfold e', i)

493

 Expr_dclock (e', i) > Expr_dclock (unfold e', i)

494

 Expr_phclock _ > e

495


496

let eq_unfold_consts consts eq =

497

{ eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }

498


499

let node_unfold_consts consts node =

500

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

501


502

let get_consts prog =

503

List.fold_left (

504

fun consts decl >

505

match decl.top_decl_desc with

506

 Consts clist > clist@consts

507

 Node _  ImportedNode _  Open _ > consts

508

) [] prog

509


510


511

let get_nodes prog =

512

List.fold_left (

513

fun nodes decl >

514

match decl.top_decl_desc with

515

 Node nd > nd::nodes

516

 Consts _  ImportedNode _  Open _ > nodes

517

) [] prog

518


519

let prog_unfold_consts prog =

520

let consts = get_consts prog in

521

List.map (

522

fun decl > match decl.top_decl_desc with

523

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

524

 _ > decl

525

) prog

526


527


528


529

(************************************************************************)

530

(* Renaming *)

531


532

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

533

let rec expr_replace_var fvar expr =

534

{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }

535


536

and expr_desc_replace_var fvar expr_desc =

537

match expr_desc with

538

 Expr_const _ > expr_desc

539

 Expr_ident i > Expr_ident (fvar i)

540

 Expr_array el > Expr_array (List.map (expr_replace_var fvar) el)

541

 Expr_access (e1, d) > Expr_access (expr_replace_var fvar e1, d)

542

 Expr_power (e1, d) > Expr_power (expr_replace_var fvar e1, d)

543

 Expr_tuple el > Expr_tuple (List.map (expr_replace_var fvar) el)

544

 Expr_ite (c, t, e) > Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)

545

 Expr_arrow (e1, e2)> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2)

546

 Expr_fby (e1, e2) > Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)

547

 Expr_pre e' > Expr_pre (expr_replace_var fvar e')

548

 Expr_when (e', i, l)> Expr_when (expr_replace_var fvar e', fvar i, l)

549

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

550

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

551

 _ > assert false

552


553

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

554

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

555

let eq_replace_rhs_var pvar fvar eq =

556

let pvar l = List.exists pvar l in

557

let rec replace lhs rhs =

558

{ rhs with expr_desc = replace_desc lhs rhs.expr_desc }

559

and replace_desc lhs rhs_desc =

560

match lhs with

561

 [] > assert false

562

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

563

 _ >

564

(match rhs_desc with

565

 Expr_tuple tl >

566

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

567

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

568

let args = expr_list_of_expr arg in

569

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

570

 Expr_array _

571

 Expr_access _

572

 Expr_power _

573

 Expr_const _

574

 Expr_ident _

575

 Expr_appl _ >

576

if pvar lhs

577

then expr_desc_replace_var fvar rhs_desc

578

else rhs_desc

579

 Expr_ite (c, t, e) > Expr_ite (replace lhs c, replace lhs t, replace lhs e)

580

 Expr_arrow (e1, e2) > Expr_arrow (replace lhs e1, replace lhs e2)

581

 Expr_fby (e1, e2) > Expr_fby (replace lhs e1, replace lhs e2)

582

 Expr_pre e' > Expr_pre (replace lhs e')

583

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

584

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

585

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

586

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

587

 _ > assert false)

588

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

589


590


591

let rec rename_expr f_node f_var f_const expr =

592

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

593

and rename_expr_desc f_node f_var f_const expr_desc =

594

let re = rename_expr f_node f_var f_const in

595

match expr_desc with

596

 Expr_const _ > expr_desc

597

 Expr_ident i > Expr_ident (f_var i)

598

 Expr_array el > Expr_array (List.map re el)

599

 Expr_access (e1, d) > Expr_access (re e1, d)

600

 Expr_power (e1, d) > Expr_power (re e1, d)

601

 Expr_tuple el > Expr_tuple (List.map re el)

602

 Expr_ite (c, t, e) > Expr_ite (re c, re t, re e)

603

 Expr_arrow (e1, e2)> Expr_arrow (re e1, re e2)

604

 Expr_fby (e1, e2) > Expr_fby (re e1, re e2)

605

 Expr_pre e' > Expr_pre (re e')

606

 Expr_when (e', i, l)> Expr_when (re e', f_var i, l)

607

 Expr_merge (i, hl) >

608

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

609

 Expr_appl (i, e', i') >

610

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

611

 _ > assert false

612


613

let rename_node_annot f_node f_var f_const expr =

614

expr

615

(* TODO assert false *)

616


617

let rename_expr_annot f_node f_var f_const annot =

618

annot

619

(* TODO assert false *)

620


621

let rename_node f_node f_var f_const nd =

622

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

623

let inputs = List.map rename_var nd.node_inputs in

624

let outputs = List.map rename_var nd.node_outputs in

625

let locals = List.map rename_var nd.node_locals in

626

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

627

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

628

let node_asserts = List.map

629

(fun a >

630

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

631

) nd.node_asserts

632

in

633

let eqs = List.map

634

(fun eq > { eq with

635

eq_lhs = List.map f_var eq.eq_lhs;

636

eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs

637

} ) nd.node_eqs

638

in

639

let spec =

640

Utils.option_map

641

(fun s > rename_node_annot f_node f_var f_const s)

642

nd.node_spec

643

in

644

let annot =

645

Utils.option_map

646

(fun s > rename_expr_annot f_node f_var f_const s)

647

nd.node_annot

648

in

649

{

650

node_id = f_node nd.node_id;

651

node_type = nd.node_type;

652

node_clock = nd.node_clock;

653

node_inputs = inputs;

654

node_outputs = outputs;

655

node_locals = locals;

656

node_gencalls = gen_calls;

657

node_checks = node_checks;

658

node_asserts = node_asserts;

659

node_eqs = eqs;

660

node_dec_stateless = nd.node_dec_stateless;

661

node_stateless = nd.node_stateless;

662

node_spec = spec;

663

node_annot = annot;

664

}

665


666


667

let rename_const f_const c =

668

{ c with const_id = f_const c.const_id }

669


670

let rename_prog f_node f_var f_const prog =

671

List.rev (

672

List.fold_left (fun accu top >

673

(match top.top_decl_desc with

674

 Node nd >

675

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

676

 Consts c >

677

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

678

 ImportedNode _

679

 Open _ > top)

680

::accu

681

) [] prog

682

)

683


684

(**********************************************************************)

685

(* Pretty printers *)

686


687

let pp_decl_type fmt tdecl =

688

match tdecl.top_decl_desc with

689

 Node nd >

690

fprintf fmt "%s: " nd.node_id;

691

Utils.reset_names ();

692

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

693

 ImportedNode ind >

694

fprintf fmt "%s: " ind.nodei_id;

695

Utils.reset_names ();

696

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

697

 Consts _  Open _ > ()

698


699

let pp_prog_type fmt tdecl_list =

700

Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list

701


702

let pp_decl_clock fmt cdecl =

703

match cdecl.top_decl_desc with

704

 Node nd >

705

fprintf fmt "%s: " nd.node_id;

706

Utils.reset_names ();

707

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

708

 ImportedNode ind >

709

fprintf fmt "%s: " ind.nodei_id;

710

Utils.reset_names ();

711

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

712

 Consts _  Open _ > ()

713


714

let pp_prog_clock fmt prog =

715

Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog

716


717

let pp_error fmt = function

718

Main_not_found >

719

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

720

!Options.main_node

721

 Main_wrong_kind >

722

fprintf fmt

723

"Name %s does not correspond to a (nonimported) node definition.@."

724

!Options.main_node

725

 No_main_specified >

726

fprintf fmt "No main node specified@."

727

 Unbound_symbol sym >

728

fprintf fmt

729

"%s is undefined.@."

730

sym

731

 Already_bound_symbol sym >

732

fprintf fmt

733

"%s is already defined.@."

734

sym

735


736

(* filling node table with internal functions *)

737

let vdecls_of_typ_ck cpt ty =

738

let loc = Location.dummy_loc in

739

List.map

740

(fun _ > incr cpt;

741

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

742

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

743

(Types.type_list_of_type ty)

744


745

let mk_internal_node id =

746

let spec = None in

747

let ty = Env.lookup_value Basic_library.type_env id in

748

let ck = Env.lookup_value Basic_library.clock_env id in

749

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

750

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

751

let cpt = ref (1) in

752

mktop_decl Location.dummy_loc

753

(ImportedNode

754

{nodei_id = id;

755

nodei_type = ty;

756

nodei_clock = ck;

757

nodei_inputs = vdecls_of_typ_ck cpt tin;

758

nodei_outputs = vdecls_of_typ_ck cpt tout;

759

nodei_stateless = Types.get_static_value ty <> None;

760

nodei_spec = spec;

761

nodei_prototype = None;

762

nodei_in_lib = None;

763

})

764


765

let add_internal_funs () =

766

List.iter

767

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

768

Basic_library.internal_funs

769


770

(* Local Variables: *)

771

(* compilecommand:"make C .." *)

772

(* End: *)
