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


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 call_t

79

 Expr_uclock of expr * int

80

 Expr_dclock of expr * int

81

 Expr_phclock of expr * rat

82

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

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

 Open 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

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

340

let field_table =

341

Utils.create_hashtable 20 [

342

]

343


344

let get_enum_type_tags cty =

345

match cty with

346

 Tydec_bool > [tag_true; tag_false]

347

 Tydec_const _ > (match Hashtbl.find type_table cty with

348

 Tydec_enum tl > tl

349

 _ > assert false)

350

 _ > assert false

351

(*

352

let get_struct_type_fields cty =

353

match cty with

354

 Tydec_const _ > (match Hashtbl.find type_table cty with

355

 Tydec_struct fl > fl

356

 _ > assert false)

357

 _ > assert false

358

*)

359

let const_of_bool b =

360

Const_tag (if b then tag_true else tag_false)

361


362

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

363


364

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

365

let expr_of_ident id loc =

366

{expr_tag = Utils.new_tag ();

367

expr_desc = Expr_ident id;

368

expr_type = Types.new_var ();

369

expr_clock = Clocks.new_var true;

370

expr_delay = Delay.new_var ();

371

expr_loc = loc;

372

expr_annot = None}

373


374

let expr_list_of_expr expr =

375

match expr.expr_desc with

376

 Expr_tuple elist >

377

elist

378

 _ > [expr]

379


380

let expr_of_expr_list loc elist =

381

match elist with

382

 [t] > { t with expr_loc = loc }

383

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

384

 _ > assert false

385


386

let call_of_expr expr =

387

match expr.expr_desc with

388

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

389

 _ > assert false

390


391

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

392

let rec expr_of_dimension dim =

393

match dim.dim_desc with

394

 Dbool b >

395

mkexpr dim.dim_loc (Expr_const (const_of_bool b))

396

 Dint i >

397

mkexpr dim.dim_loc (Expr_const (Const_int i))

398

 Dident id >

399

mkexpr dim.dim_loc (Expr_ident id)

400

 Dite (c, t, e) >

401

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

402

 Dappl (id, args) >

403

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

404

 Dlink dim' > expr_of_dimension dim'

405

 Dvar

406

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

407

assert false)

408


409

let dimension_of_const loc const =

410

match const with

411

 Const_int i > mkdim_int loc i

412

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

413

 _ > raise InvalidDimension

414


415

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

416

into dimension expressions *)

417

let rec dimension_of_expr expr =

418

match expr.expr_desc with

419

 Expr_const c > dimension_of_const expr.expr_loc c

420

 Expr_ident id > mkdim_ident expr.expr_loc id

421

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

422

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

423

if k = None then raise InvalidDimension;

424

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

425

 Expr_ite (i, t, e) >

426

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

427

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

428


429


430

let sort_handlers hl =

431

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

432


433

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

434

 Expr_const c1, Expr_const c2 > c1 = c2

435

 Expr_ident i1, Expr_ident i2 > i1 = i2

436

 Expr_array el1, Expr_array el2

437

 Expr_tuple el1, Expr_tuple el2 >

438

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

439

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

440

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

441

 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

442

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

443

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

444

 Expr_pre e, Expr_pre e' > is_eq_expr e e'

445

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

446

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

447

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

448

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

449

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

450

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

451

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

452

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

453

 _ > false

454


455

let node_vars nd =

456

nd.node_inputs @ nd.node_locals @ nd.node_outputs

457


458

let node_var id node =

459

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

460


461

let node_eq id node =

462

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

463


464

(* Consts unfoooolding *)

465

let is_const i consts =

466

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

467


468

let get_const i consts =

469

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

470

c.const_value

471


472

let rec expr_unfold_consts consts e =

473

{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc }

474


475

and expr_desc_unfold_consts consts e =

476

let unfold = expr_unfold_consts consts in

477

match e with

478

 Expr_const _ > e

479

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

480

 Expr_array el > Expr_array (List.map unfold el)

481

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

482

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

483

 Expr_tuple el > Expr_tuple (List.map unfold el)

484

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

485

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

486

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

487

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

488

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

489

 Expr_pre e' > Expr_pre (unfold e')

490

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

491

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

492

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

493

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

494

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

495

 Expr_phclock _ > e

496


497

let eq_unfold_consts consts eq =

498

{ eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }

499


500

let node_unfold_consts consts node =

501

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

502


503

let get_consts prog =

504

List.fold_left (

505

fun consts decl >

506

match decl.top_decl_desc with

507

 Consts clist > clist@consts

508

 Node _  ImportedNode _  ImportedFun _  Open _ > consts

509

) [] prog

510


511


512

let get_nodes prog =

513

List.fold_left (

514

fun nodes decl >

515

match decl.top_decl_desc with

516

 Node nd > nd::nodes

517

 Consts _  ImportedNode _  ImportedFun _  Open _ > nodes

518

) [] prog

519


520

let prog_unfold_consts prog =

521

let consts = get_consts prog in

522

List.map (

523

fun decl > match decl.top_decl_desc with

524

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

525

 _ > decl

526

) prog

527


528


529


530

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

531

(* Renaming *)

532


533

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

534

let rec expr_replace_var fvar expr =

535

{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }

536


537

and expr_desc_replace_var fvar expr_desc =

538

match expr_desc with

539

 Expr_const _ > expr_desc

540

 Expr_ident i > Expr_ident (fvar i)

541

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

542

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

543

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

544

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

545

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

546

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

547

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

548

 Expr_pre e' > Expr_pre (expr_replace_var fvar e')

549

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

550

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

551

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

552

 _ > assert false

553


554

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

555

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

556

let eq_replace_rhs_var pvar fvar eq =

557

let pvar l = List.exists pvar l in

558

let rec replace lhs rhs =

559

{ rhs with expr_desc = replace_desc lhs rhs.expr_desc }

560

and replace_desc lhs rhs_desc =

561

match lhs with

562

 [] > assert false

563

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

564

 _ >

565

(match rhs_desc with

566

 Expr_tuple tl >

567

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

568

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

569

let args = expr_list_of_expr arg in

570

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

571

 Expr_array _

572

 Expr_access _

573

 Expr_power _

574

 Expr_const _

575

 Expr_ident _

576

 Expr_appl _ >

577

if pvar lhs

578

then expr_desc_replace_var fvar rhs_desc

579

else rhs_desc

580

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

581

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

582

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

583

 Expr_pre e' > Expr_pre (replace lhs e')

584

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

585

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

586

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

587

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

588

 _ > assert false)

589

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

590


591


592

let rec rename_expr f_node f_var f_const expr =

593

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

594

and rename_expr_desc f_node f_var f_const expr_desc =

595

let re = rename_expr f_node f_var f_const in

596

match expr_desc with

597

 Expr_const _ > expr_desc

598

 Expr_ident i > Expr_ident (f_var i)

599

 Expr_array el > Expr_array (List.map re el)

600

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

601

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

602

 Expr_tuple el > Expr_tuple (List.map re el)

603

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

604

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

605

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

606

 Expr_pre e' > Expr_pre (re e')

607

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

608

 Expr_merge (i, hl) >

609

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

610

 Expr_appl (i, e', i') >

611

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

612

 _ > assert false

613


614

let rename_node_annot f_node f_var f_const expr =

615

expr

616

(* TODO assert false *)

617


618

let rename_expr_annot f_node f_var f_const annot =

619

annot

620

(* TODO assert false *)

621


622

let rename_node f_node f_var f_const nd =

623

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

624

let inputs = List.map rename_var nd.node_inputs in

625

let outputs = List.map rename_var nd.node_outputs in

626

let locals = List.map rename_var nd.node_locals in

627

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

628

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

629

let node_asserts = List.map

630

(fun a >

631

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

632

) nd.node_asserts

633

in

634

let eqs = List.map

635

(fun eq > { eq with

636

eq_lhs = List.map f_var eq.eq_lhs;

637

eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs

638

} ) nd.node_eqs

639

in

640

let spec =

641

Utils.option_map

642

(fun s > rename_node_annot f_node f_var f_const s)

643

nd.node_spec

644

in

645

let annot =

646

Utils.option_map

647

(fun s > rename_expr_annot f_node f_var f_const s)

648

nd.node_annot

649

in

650

{

651

node_id = f_node nd.node_id;

652

node_type = nd.node_type;

653

node_clock = nd.node_clock;

654

node_inputs = inputs;

655

node_outputs = outputs;

656

node_locals = locals;

657

node_gencalls = gen_calls;

658

node_checks = node_checks;

659

node_asserts = node_asserts;

660

node_eqs = eqs;

661

node_spec = spec;

662

node_annot = annot;

663

}

664


665


666

let rename_const f_const c =

667

{ c with const_id = f_const c.const_id }

668


669

let rename_prog f_node f_var f_const prog =

670

List.rev (

671

List.fold_left (fun accu top >

672

(match top.top_decl_desc with

673

 Node nd >

674

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

675

 Consts c >

676

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

677

 ImportedNode _

678

 ImportedFun _

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

 ImportedFun ind >

698

fprintf fmt "%s: " ind.fun_id;

699

Utils.reset_names ();

700

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

701

 Consts _  Open _ > ()

702


703

let pp_prog_type fmt tdecl_list =

704

Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list

705


706

let pp_decl_clock fmt cdecl =

707

match cdecl.top_decl_desc with

708

 Node nd >

709

fprintf fmt "%s: " nd.node_id;

710

Utils.reset_names ();

711

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

712

 ImportedNode ind >

713

fprintf fmt "%s: " ind.nodei_id;

714

Utils.reset_names ();

715

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

716

 ImportedFun _  Consts _  Open _ > ()

717


718

let pp_prog_clock fmt prog =

719

Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog

720


721

let pp_error fmt = function

722

Main_not_found >

723

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

724

!Options.main_node

725

 Main_wrong_kind >

726

fprintf fmt

727

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

728

!Options.main_node

729

 No_main_specified >

730

fprintf fmt "No main node specified@."

731


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

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

765

(* End: *)
