1

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

2

(* *)

3

(* The LustreC compiler toolset / The LustreC Development Team *)

4

(* Copyright 2012   ONERA  CNRS  INPT *)

5

(* *)

6

(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)

7

(* under the terms of the GNU Lesser General Public License *)

8

(* version 2.1. *)

9

(* *)

10

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

11


12

open Format

13

open Lustre_types

14

open Machine_code_types

15

(*open Dimension*)

16


17

module VDeclModule = struct

18

(* Node module *)

19

type t = var_decl

20


21

let compare v1 v2 = compare v1.var_id v2.var_id

22

end

23


24

module VMap = Map.Make (VDeclModule)

25


26

module VSet : sig

27

include Set.S

28


29

val pp : Format.formatter > t > unit

30


31

val get : ident > t > elt

32

end

33

with type elt = var_decl = struct

34

include Set.Make (VDeclModule)

35


36

let pp fmt s =

37

Format.fprintf fmt "{@[%a}@]"

38

(Utils.fprintf_list ~sep:",@ " Printers.pp_var)

39

(elements s)

40


41

(* Strangley the find_first function of Set.Make is incorrect (at the current

42

time of writting this comment. Had to switch to lists *)

43

let get id s = List.find (fun v > v.var_id = id) (elements s)

44

end

45


46

let dummy_type_dec =

47

{ ty_dec_desc = Tydec_any; ty_dec_loc = Location.dummy_loc }

48


49

let dummy_clock_dec =

50

{ ck_dec_desc = Ckdec_any; ck_dec_loc = Location.dummy_loc }

51


52

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

53

(* *)

54


55

let mktyp loc d = { ty_dec_desc = d; ty_dec_loc = loc }

56


57

let mkclock loc d = { ck_dec_desc = d; ck_dec_loc = loc }

58


59

let mkvar_decl loc ?(orig = false)

60

(id, ty_dec, ck_dec, is_const, value, parentid) =

61

assert (value = None  is_const);

62

{

63

var_id = id;

64

var_orig = orig;

65

var_dec_type = ty_dec;

66

var_dec_clock = ck_dec;

67

var_dec_const = is_const;

68

var_dec_value = value;

69

var_parent_nodeid = parentid;

70

var_type = Types.new_var ();

71

var_clock = Clocks.new_var true;

72

var_loc = loc;

73

}

74


75

let dummy_var_decl name typ =

76

{

77

var_id = name;

78

var_orig = false;

79

var_dec_type = dummy_type_dec;

80

var_dec_clock = dummy_clock_dec;

81

var_dec_const = false;

82

var_dec_value = None;

83

var_parent_nodeid = None;

84

var_type = typ;

85

var_clock = Clocks.new_ck Clocks.Cvar true;

86

var_loc = Location.dummy_loc;

87

}

88


89

let mkexpr loc d =

90

{

91

expr_tag = Utils.new_tag ();

92

expr_desc = d;

93

expr_type = Types.new_var ();

94

expr_clock = Clocks.new_var true;

95

expr_delay = Delay.new_var ();

96

expr_annot = None;

97

expr_loc = loc;

98

}

99


100

let var_decl_of_const ?(parentid = None) c =

101

{

102

var_id = c.const_id;

103

var_orig = true;

104

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

105

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

106

var_dec_const = true;

107

var_dec_value = None;

108

var_parent_nodeid = parentid;

109

var_type = c.const_type;

110

var_clock = Clocks.new_var false;

111

var_loc = c.const_loc;

112

}

113


114

let mk_new_name used id =

115

let rec new_name name cpt =

116

if used name then new_name (sprintf "_%s_%i" id cpt) (cpt + 1) else name

117

in

118

new_name id 1

119


120

let mkeq loc (lhs, rhs) = { eq_lhs = lhs; eq_rhs = rhs; eq_loc = loc }

121


122

let mkassert loc expr = { assert_loc = loc; assert_expr = expr }

123


124

let mktop_decl loc own itf d =

125

{

126

top_decl_desc = d;

127

top_decl_loc = loc;

128

top_decl_owner = own;

129

top_decl_itf = itf;

130

}

131


132

let mkpredef_call loc funname args =

133

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

134


135

let is_clock_dec_type cty = match cty with Tydec_clock _ > true  _ > false

136


137

let const_of_top top_decl =

138

match top_decl.top_decl_desc with Const c > c  _ > assert false

139


140

let node_of_top top_decl =

141

match top_decl.top_decl_desc with Node nd > nd  _ > raise Not_found

142


143

let imported_node_of_top top_decl =

144

match top_decl.top_decl_desc with

145

 ImportedNode ind >

146

ind

147

 _ >

148

assert false

149


150

let typedef_of_top top_decl =

151

match top_decl.top_decl_desc with TypeDef tdef > tdef  _ > assert false

152


153

let dependency_of_top top_decl =

154

match top_decl.top_decl_desc with

155

 Open (local, dep) >

156

local, dep

157

 _ >

158

assert false

159


160

let consts_of_enum_type top_decl =

161

match top_decl.top_decl_desc with

162

 TypeDef tdef > (

163

match tdef.tydef_desc with

164

 Tydec_enum tags >

165

List.map

166

(fun tag >

167

let cdecl =

168

{

169

const_id = tag;

170

const_loc = top_decl.top_decl_loc;

171

const_value = Const_tag tag;

172

const_type = Type_predef.type_const tdef.tydef_id;

173

}

174

in

175

{ top_decl with top_decl_desc = Const cdecl })

176

tags

177

 _ >

178

[])

179

 _ >

180

assert false

181


182

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

183

(* Eexpr functions *)

184

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

185


186

let empty_contract =

187

{

188

consts = [];

189

locals = [];

190

stmts = [];

191

assume = [];

192

guarantees = [];

193

modes = [];

194

imports = [];

195

spec_loc = Location.dummy_loc;

196

}

197


198

(* For const declaration we do as for regular lustre node. But for local flows

199

we registered the variable and the lustre flow definition *)

200

let mk_contract_var id is_const type_opt expr loc =

201

let typ = match type_opt with None > mktyp loc Tydec_any  Some t > t in

202

if is_const then

203

let v =

204

mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None)

205

in

206

{ empty_contract with consts = [ v ]; spec_loc = loc }

207

else

208

let v =

209

mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None)

210

in

211

let eq = mkeq loc ([ id ], expr) in

212

{ empty_contract with locals = [ v ]; stmts = [ Eq eq ]; spec_loc = loc }

213


214

let eexpr_add_name eexpr eexpr_name = { eexpr with eexpr_name }

215


216

let mk_contract_guarantees name eexpr =

217

{

218

empty_contract with

219

guarantees = [ eexpr_add_name eexpr name ];

220

spec_loc = eexpr.eexpr_loc;

221

}

222


223

let mk_contract_assume name eexpr =

224

{

225

empty_contract with

226

assume = [ eexpr_add_name eexpr name ];

227

spec_loc = eexpr.eexpr_loc;

228

}

229


230

let mk_contract_mode id rl el loc =

231

{

232

empty_contract with

233

modes = [ { mode_id = id; require = rl; ensure = el; mode_loc = loc } ];

234

spec_loc = loc;

235

}

236


237

let mk_contract_import id ins outs loc =

238

{

239

empty_contract with

240

imports =

241

[ { import_nodeid = id; inputs = ins; outputs = outs; import_loc = loc } ];

242

spec_loc = loc;

243

}

244


245

let merge_contracts ann1 ann2 =

246

(* keeping the first item loc *)

247

{

248

consts = ann1.consts @ ann2.consts;

249

locals = ann1.locals @ ann2.locals;

250

stmts = ann1.stmts @ ann2.stmts;

251

assume = ann1.assume @ ann2.assume;

252

guarantees = ann1.guarantees @ ann2.guarantees;

253

modes = ann1.modes @ ann2.modes;

254

imports = ann1.imports @ ann2.imports;

255

spec_loc = ann1.spec_loc;

256

}

257


258

let mkeexpr loc expr =

259

{

260

eexpr_tag = Utils.new_tag ();

261

eexpr_qfexpr = expr;

262

eexpr_quantifiers = [];

263

eexpr_name = None;

264

eexpr_type = Types.new_var ();

265

eexpr_clock = Clocks.new_var true;

266

eexpr_loc = loc;

267

}

268


269

let extend_eexpr q e = { e with eexpr_quantifiers = q @ e.eexpr_quantifiers }

270


271

(* let mkepredef_call loc funname args = mkeexpr loc (EExpr_appl (funname,

272

mkeexpr loc (EExpr_tuple args), None))

273


274

let mkepredef_unary_call loc funname arg = mkeexpr loc (EExpr_appl (funname,

275

arg, None)) *)

276


277

let merge_expr_annot ann1 ann2 =

278

match ann1, ann2 with

279

 None, None >

280

assert false

281

 Some _, None >

282

ann1

283

 None, Some _ >

284

ann2

285

 Some ann1, Some ann2 >

286

Some { annots = ann1.annots @ ann2.annots; annot_loc = ann1.annot_loc }

287


288

let update_expr_annot node_id e annot =

289

List.iter

290

(fun (key, _) > Annotations.add_expr_ann node_id e.expr_tag key)

291

annot.annots;

292

e.expr_annot < merge_expr_annot e.expr_annot (Some annot);

293

e

294


295

let mkinstr ?lustre_eq ?(instr_spec = []) instr_desc =

296

{ instr_desc; (* lustre_expr = lustre_expr; *)

297

instr_spec; lustre_eq }

298


299

let get_instr_desc i = i.instr_desc

300


301

let update_instr_desc i id = { i with instr_desc = id }

302


303

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

304

(* Fast access to nodes, by name *)

305

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

306


307

let consts_table = Hashtbl.create 30

308


309

let print_node_table fmt () =

310

Format.fprintf fmt "{ /* node table */@.";

311

Hashtbl.iter

312

(fun id nd > Format.fprintf fmt "%s > %a" id Printers.pp_short_decl nd)

313

node_table;

314

Format.fprintf fmt "}@."

315


316

let print_consts_table fmt () =

317

Format.fprintf fmt "{ /* consts table */@.";

318

Hashtbl.iter

319

(fun id const >

320

Format.fprintf fmt "%s > %a" id Printers.pp_const_decl

321

(const_of_top const))

322

consts_table;

323

Format.fprintf fmt "}@."

324


325

let node_name td =

326

match td.top_decl_desc with

327

 Node nd >

328

nd.node_id

329

 ImportedNode nd >

330

nd.nodei_id

331

 _ >

332

assert false

333


334

let is_generic_node td =

335

match td.top_decl_desc with

336

 Node nd >

337

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

338

 ImportedNode nd >

339

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

340

 _ >

341

assert false

342


343

let node_inputs td =

344

match td.top_decl_desc with

345

 Node nd >

346

nd.node_inputs

347

 ImportedNode nd >

348

nd.nodei_inputs

349

 _ >

350

assert false

351


352

let node_from_name id = Hashtbl.find node_table id

353


354

let update_node id top = Hashtbl.replace node_table id top

355


356

let is_imported_node td =

357

match td.top_decl_desc with

358

 Node _ >

359

false

360

 ImportedNode _ >

361

true

362

 _ >

363

assert false

364


365

let is_node_contract nd =

366

match nd.node_spec with Some (Contract _) > true  _ > false

367


368

let get_node_contract nd =

369

match nd.node_spec with Some (Contract c) > c  _ > assert false

370


371

let is_contract td =

372

match td.top_decl_desc with Node nd > is_node_contract nd  _ > false

373


374

(* alias and type definition table *)

375


376

let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false

377


378

let top_int_type = mktop (TypeDef { tydef_id = "int"; tydef_desc = Tydec_int })

379


380

let top_bool_type =

381

mktop (TypeDef { tydef_id = "bool"; tydef_desc = Tydec_bool })

382


383

(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc =

384

Tydec_float}) *)

385

let top_real_type =

386

mktop (TypeDef { tydef_id = "real"; tydef_desc = Tydec_real })

387


388

let type_table =

389

Utils.create_hashtable 20

390

[

391

Tydec_int, top_int_type;

392

Tydec_bool, top_bool_type;

393

(* Tydec_float, top_float_type; *)

394

Tydec_real, top_real_type;

395

]

396


397

let print_type_table fmt () =

398

Format.fprintf fmt "{ /* type table */@.";

399

Hashtbl.iter

400

(fun tydec tdef >

401

Format.fprintf fmt "%a > %a" Printers.pp_var_type_dec_desc tydec

402

Printers.pp_typedef (typedef_of_top tdef))

403

type_table;

404

Format.fprintf fmt "}@."

405


406

let rec is_user_type typ =

407

match typ with

408

 Tydec_int

409

 Tydec_bool

410

 Tydec_real (*  Tydec_float *)

411

 Tydec_any

412

 Tydec_const _ >

413

false

414

 Tydec_clock typ' >

415

is_user_type typ'

416

 _ >

417

true

418


419

let get_repr_type typ =

420

let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in

421

if is_user_type typ_def then typ else typ_def

422


423

let rec coretype_equal ty1 ty2 =

424

let res =

425

match ty1, ty2 with

426

 Tydec_any, _  _, Tydec_any >

427

assert false

428

 Tydec_const _, Tydec_const _ >

429

get_repr_type ty1 = get_repr_type ty2

430

 Tydec_const _, _ >

431

let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc in

432

(not (is_user_type ty1')) && coretype_equal ty1' ty2

433

 _, Tydec_const _ >

434

coretype_equal ty2 ty1

435

 Tydec_int, Tydec_int

436

 Tydec_real, Tydec_real

437

(*  Tydec_float , Tydec_float *)

438

 Tydec_bool, Tydec_bool >

439

true

440

 Tydec_clock ty1, Tydec_clock ty2 >

441

coretype_equal ty1 ty2

442

 Tydec_array (d1, ty1), Tydec_array (d2, ty2) >

443

Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2

444

 Tydec_enum tl1, Tydec_enum tl2 >

445

List.sort compare tl1 = List.sort compare tl2

446

 Tydec_struct fl1, Tydec_struct fl2 >

447

List.length fl1 = List.length fl2

448

&& List.for_all2

449

(fun (f1, t1) (f2, t2) > f1 = f2 && coretype_equal t1 t2)

450

(List.sort (fun (f1, _) (f2, _) > compare f1 f2) fl1)

451

(List.sort (fun (f1, _) (f2, _) > compare f1 f2) fl2)

452

 _ >

453

false

454

in

455

(*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc

456

ty1 Printers.pp_var_type_dec_desc ty2 res;*)

457

res

458


459

let tag_default = "default"

460


461

let const_is_bool c =

462

match c with Const_tag t > t = tag_true  t = tag_false  _ > false

463


464

(* Computes the negation of a boolean constant *)

465

let const_negation c =

466

assert (const_is_bool c);

467

match c with

468

 Const_tag t when t = tag_true >

469

Const_tag tag_false

470

 _ >

471

Const_tag tag_true

472


473

let const_or c1 c2 =

474

assert (const_is_bool c1 && const_is_bool c2);

475

match c1, c2 with

476

 Const_tag t1, _ when t1 = tag_true >

477

c1

478

 _, Const_tag t2 when t2 = tag_true >

479

c2

480

 _ >

481

Const_tag tag_false

482


483

let const_and c1 c2 =

484

assert (const_is_bool c1 && const_is_bool c2);

485

match c1, c2 with

486

 Const_tag t1, _ when t1 = tag_false >

487

c1

488

 _, Const_tag t2 when t2 = tag_false >

489

c2

490

 _ >

491

Const_tag tag_true

492


493

let const_xor c1 c2 =

494

assert (const_is_bool c1 && const_is_bool c2);

495

match c1, c2 with

496

 Const_tag t1, Const_tag t2 when t1 <> t2 >

497

Const_tag tag_true

498

 _ >

499

Const_tag tag_false

500


501

let const_impl c1 c2 =

502

assert (const_is_bool c1 && const_is_bool c2);

503

match c1, c2 with

504

 Const_tag t1, _ when t1 = tag_false >

505

Const_tag tag_true

506

 _, Const_tag t2 when t2 = tag_true >

507

Const_tag tag_true

508

 _ >

509

Const_tag tag_false

510


511

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

512

let tag_table =

513

Utils.create_hashtable 20

514

[ tag_true, top_bool_type; tag_false, top_bool_type ]

515


516

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

517

let field_table = Utils.create_hashtable 20 []

518


519

let get_enum_type_tags cty =

520

(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)

521

match cty with

522

 Tydec_bool >

523

[ tag_true; tag_false ]

524

 Tydec_const _ > (

525

match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with

526

 Tydec_enum tl >

527

tl

528

 _ >

529

assert false)

530

 _ >

531

assert false

532


533

let get_struct_type_fields cty =

534

match cty with

535

 Tydec_const _ > (

536

match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with

537

 Tydec_struct fl >

538

fl

539

 _ >

540

assert false)

541

 _ >

542

assert false

543


544

let const_of_bool b = Const_tag (if b then tag_true else tag_false)

545


546

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

547


548

let ident_of_expr expr =

549

match expr.expr_desc with Expr_ident id > id  _ > assert false

550


551

(* Generate a new ident expression from a declared variable *)

552

let expr_of_vdecl v =

553

{

554

expr_tag = Utils.new_tag ();

555

expr_desc = Expr_ident v.var_id;

556

expr_type = v.var_type;

557

expr_clock = v.var_clock;

558

expr_delay = Delay.new_var ();

559

expr_annot = None;

560

expr_loc = v.var_loc;

561

}

562


563

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

564

let expr_of_ident id loc =

565

{

566

expr_tag = Utils.new_tag ();

567

expr_desc = Expr_ident id;

568

expr_type = Types.new_var ();

569

expr_clock = Clocks.new_var true;

570

expr_delay = Delay.new_var ();

571

expr_loc = loc;

572

expr_annot = None;

573

}

574


575

let is_tuple_expr expr =

576

match expr.expr_desc with Expr_tuple _ > true  _ > false

577


578

let expr_list_of_expr expr =

579

match expr.expr_desc with Expr_tuple elist > elist  _ > [ expr ]

580


581

let expr_of_expr_list loc elist =

582

match elist with

583

 [ t ] >

584

{ t with expr_loc = loc }

585

 t :: _ >

586

let tlist = List.map (fun e > e.expr_type) elist in

587

let clist = List.map (fun e > e.expr_clock) elist in

588

{

589

t with

590

expr_desc = Expr_tuple elist;

591

expr_type = Type_predef.type_tuple tlist;

592

expr_clock = Clock_predef.ck_tuple clist;

593

expr_tag = Utils.new_tag ();

594

expr_loc = loc;

595

}

596

 _ >

597

assert false

598


599

let call_of_expr expr =

600

match expr.expr_desc with

601

 Expr_appl (f, args, r) >

602

f, expr_list_of_expr args, r

603

 _ >

604

assert false

605


606

(* Conversion from dimension expr to standard expr, for the purpose of printing,

607

typing, etc... *)

608

let rec expr_of_dimension dim =

609

let open Dimension in

610

let expr =

611

match dim.dim_desc with

612

 Dbool b >

613

mkexpr dim.dim_loc (Expr_const (const_of_bool b))

614

 Dint i >

615

mkexpr dim.dim_loc (Expr_const (Const_int i))

616

 Dident id >

617

mkexpr dim.dim_loc (Expr_ident id)

618

 Dite (c, t, e) >

619

mkexpr dim.dim_loc

620

(Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))

621

 Dappl (id, args) >

622

mkexpr dim.dim_loc

623

(Expr_appl

624

( id,

625

expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args),

626

None ))

627

 Dlink dim' >

628

expr_of_dimension dim'

629

 Dvar  Dunivar >

630

Format.eprintf "internal error: Corelang.expr_of_dimension %a@."

631

Dimension.pp_dimension dim;

632

assert false

633

in

634

{ expr with expr_type = Types.new_ty Types.type_int }

635


636

let dimension_of_const loc const =

637

let open Dimension in

638

match const with

639

 Const_int i >

640

mkdim_int loc i

641

 Const_tag t when t = tag_true  t = tag_false >

642

mkdim_bool loc (t = tag_true)

643

 _ >

644

raise InvalidDimension

645


646

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

647

static call arguments into dimension expressions *)

648

let rec dimension_of_expr expr =

649

let open Dimension in

650

match expr.expr_desc with

651

 Expr_const c >

652

dimension_of_const expr.expr_loc c

653

 Expr_ident id >

654

mkdim_ident expr.expr_loc id

655

 Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr >

656

let k =

657

Types.get_static_value (Env.lookup_value Basic_library.type_env f)

658

in

659

if k = None then raise InvalidDimension;

660

mkdim_appl expr.expr_loc f

661

(List.map dimension_of_expr (expr_list_of_expr args))

662

 Expr_ite (i, t, e) >

663

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

664

(dimension_of_expr e)

665

 _ >

666

raise InvalidDimension

667

(* not a simple dimension expression *)

668


669

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

670


671

let rec is_eq_const c1 c2 =

672

match c1, c2 with

673

 Const_real r1, Const_real _ >

674

Real.eq r1 r1

675

 Const_struct lcl1, Const_struct lcl2 >

676

List.length lcl1 = List.length lcl2

677

&& List.for_all2

678

(fun (l1, c1) (l2, c2) > l1 = l2 && is_eq_const c1 c2)

679

lcl1 lcl2

680

 _ >

681

c1 = c2

682


683

let rec is_eq_expr e1 e2 =

684

match e1.expr_desc, e2.expr_desc with

685

 Expr_const c1, Expr_const c2 >

686

is_eq_const c1 c2

687

 Expr_ident i1, Expr_ident i2 >

688

i1 = i2

689

 Expr_array el1, Expr_array el2  Expr_tuple el1, Expr_tuple el2 >

690

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

691

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

692

is_eq_expr e1 e1' && is_eq_expr e2 e2'

693

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

694

is_eq_expr e1 e1' && is_eq_expr e2 e2'

695

 Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) >

696

is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2

697

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

698

is_eq_expr e2 e2' *)

699

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

700

 Expr_pre e, Expr_pre e' >

701

is_eq_expr e e'

702

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

703

l = l' && i = i' && is_eq_expr e e'

704

 Expr_merge (i, hl), Expr_merge (i', hl') >

705

i = i'

706

&& List.for_all2

707

(fun (t, h) (t', h') > t = t' && is_eq_expr h h')

708

(sort_handlers hl) (sort_handlers hl')

709

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

710

i = i' && r = r' && is_eq_expr e e'

711

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

712

 Expr_access (e1, i1), Expr_access (e2, i2) >

713

is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)

714

 _ >

715

false

716


717

let get_node_vars nd = nd.node_inputs @ nd.node_locals @ nd.node_outputs

718


719

let mk_new_node_name nd id =

720

let used_vars = get_node_vars nd in

721

let used v = List.exists (fun vdecl > vdecl.var_id = v) used_vars in

722

mk_new_name used id

723


724

let get_var id var_list = List.find (fun v > v.var_id = id) var_list

725


726

let get_node_var id node =

727

try get_var id (get_node_vars node)

728

with Not_found >

729

(* Format.eprintf "Unable to find variable %s in node %s@.@?" id

730

node.node_id; *)

731

raise Not_found

732


733

let get_node_eqs =

734

let get_eqs stmts =

735

List.fold_right

736

(fun stmt (res_eq, res_aut) >

737

match stmt with

738

 Eq eq >

739

eq :: res_eq, res_aut

740

 Aut aut >

741

res_eq, aut :: res_aut)

742

stmts ([], [])

743

in

744

let table_eqs = Hashtbl.create 23 in

745

fun nd >

746

try

747

let old, res = Hashtbl.find table_eqs nd.node_id in

748

if old == nd.node_stmts then res else raise Not_found

749

with Not_found >

750

let res = get_eqs nd.node_stmts in

751

Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);

752

res

753


754

let get_node_eq id node =

755

let eqs, _ = get_node_eqs node in

756

try List.find (fun eq > List.mem id eq.eq_lhs) eqs

757

with Not_found > (* Shall be defined in automata auts *)

758

raise Not_found

759


760

let get_nodes prog =

761

List.fold_left

762

(fun nodes decl >

763

match decl.top_decl_desc with

764

 Node _ >

765

decl :: nodes

766

 Const _  ImportedNode _  Include _  Open _  TypeDef _ >

767

nodes)

768

[] prog

769

> List.rev

770


771

let get_imported_nodes prog =

772

List.fold_left

773

(fun nodes decl >

774

match decl.top_decl_desc with

775

 ImportedNode _ >

776

decl :: nodes

777

 Const _  Node _  Include _  Open _  TypeDef _ >

778

nodes)

779

[] prog

780


781

let get_consts prog =

782

List.fold_right

783

(fun decl consts >

784

match decl.top_decl_desc with

785

 Const _ >

786

decl :: consts

787

 Node _  ImportedNode _  Include _  Open _  TypeDef _ >

788

consts)

789

prog []

790


791

let get_typedefs prog =

792

List.fold_right

793

(fun decl types >

794

match decl.top_decl_desc with

795

 TypeDef _ >

796

decl :: types

797

 Node _  ImportedNode _  Include _  Open _  Const _ >

798

types)

799

prog []

800


801

let get_dependencies prog =

802

List.fold_right

803

(fun decl deps >

804

match decl.top_decl_desc with

805

 Open _ >

806

decl :: deps

807

 Node _  ImportedNode _  TypeDef _  Include _  Const _ >

808

deps)

809

prog []

810


811

let get_node_interface nd =

812

{

813

nodei_id = nd.node_id;

814

nodei_type = nd.node_type;

815

nodei_clock = nd.node_clock;

816

nodei_inputs = nd.node_inputs;

817

nodei_outputs = nd.node_outputs;

818

nodei_stateless = nd.node_dec_stateless;

819

nodei_spec = nd.node_spec;

820

(* nodei_annot = nd.node_annot; *)

821

nodei_prototype = None;

822

nodei_in_lib = [];

823

}

824


825

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

826

(* Renaming / Copying *)

827


828

let copy_var_decl vdecl =

829

mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig

830

( vdecl.var_id,

831

vdecl.var_dec_type,

832

vdecl.var_dec_clock,

833

vdecl.var_dec_const,

834

vdecl.var_dec_value,

835

vdecl.var_parent_nodeid )

836


837

let copy_const cdecl = { cdecl with const_type = Types.new_var () }

838


839

let copy_node nd =

840

{

841

nd with

842

node_type = Types.new_var ();

843

node_clock = Clocks.new_var true;

844

node_inputs = List.map copy_var_decl nd.node_inputs;

845

node_outputs = List.map copy_var_decl nd.node_outputs;

846

node_locals = List.map copy_var_decl nd.node_locals;

847

node_gencalls = [];

848

node_checks = [];

849

node_stateless = None;

850

}

851


852

let copy_top top =

853

match top.top_decl_desc with

854

 Node nd >

855

{ top with top_decl_desc = Node (copy_node nd) }

856

 Const c >

857

{ top with top_decl_desc = Const (copy_const c) }

858

 _ >

859

top

860


861

let copy_prog top_list = List.map copy_top top_list

862


863

let rec rename_static rename cty =

864

match cty with

865

 Tydec_array (d, cty') >

866

Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')

867

 Tydec_clock cty >

868

Tydec_clock (rename_static rename cty)

869

 Tydec_struct fl >

870

Tydec_struct (List.map (fun (f, cty) > f, rename_static rename cty) fl)

871

 _ >

872

cty

873


874

let rename_carrier rename cck =

875

match cck with

876

 Ckdec_bool cl >

877

Ckdec_bool (List.map (fun (c, l) > rename c, l) cl)

878

 _ >

879

cck

880


881

(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)

882


883

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

884

(* let rec expr_replace_var fvar expr = *)

885

(* { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *)

886


887

(* and expr_desc_replace_var fvar expr_desc = *)

888

(* match expr_desc with *)

889

(*  Expr_const _ > expr_desc *)

890

(*  Expr_ident i > Expr_ident (fvar i) *)

891

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

892

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

893

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

894

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

895

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

896

fvar t, expr_replace_var fvar e) *)

897

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

898

expr_replace_var fvar e2) *)

899

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

900

fvar e2) *)

901

(*  Expr_pre e' > Expr_pre (expr_replace_var fvar e') *)

902

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

903

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

904

expr_replace_var fvar h)) hl) *)

905

(*  Expr_appl (i, e', i') > Expr_appl (i, expr_replace_var fvar e',

906

Utils.option_map (expr_replace_var fvar) i') *)

907


908

let rec rename_expr f_node f_var expr =

909

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

910


911

and rename_expr_desc f_node f_var expr_desc =

912

let re = rename_expr f_node f_var in

913

match expr_desc with

914

 Expr_const _ >

915

expr_desc

916

 Expr_ident i >

917

Expr_ident (f_var i)

918

 Expr_array el >

919

Expr_array (List.map re el)

920

 Expr_access (e1, d) >

921

Expr_access (re e1, d)

922

 Expr_power (e1, d) >

923

Expr_power (re e1, d)

924

 Expr_tuple el >

925

Expr_tuple (List.map re el)

926

 Expr_ite (c, t, e) >

927

Expr_ite (re c, re t, re e)

928

 Expr_arrow (e1, e2) >

929

Expr_arrow (re e1, re e2)

930

 Expr_fby (e1, e2) >

931

Expr_fby (re e1, re e2)

932

 Expr_pre e' >

933

Expr_pre (re e')

934

 Expr_when (e', i, l) >

935

Expr_when (re e', f_var i, l)

936

 Expr_merge (i, hl) >

937

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

938

 Expr_appl (i, e', i') >

939

Expr_appl (f_node i, re e', Utils.option_map re i')

940


941

let rename_var f_var v =

942

{

943

(copy_var_decl v) with

944

var_id = f_var v.var_id;

945

var_type = v.var_type;

946

var_clock = v.var_clock;

947

}

948


949

let rename_vars f_var = List.map (rename_var f_var)

950


951

let rec rename_eq f_node f_var eq =

952

{

953

eq with

954

eq_lhs = List.map f_var eq.eq_lhs;

955

eq_rhs = rename_expr f_node f_var eq.eq_rhs;

956

}

957


958

and rename_handler f_node f_var h =

959

{

960

h with

961

hand_state = f_var h.hand_state;

962

hand_unless =

963

List.map

964

(fun (l, e, b, id) > l, rename_expr f_node f_var e, b, f_var id)

965

h.hand_unless;

966

hand_until =

967

List.map

968

(fun (l, e, b, id) > l, rename_expr f_node f_var e, b, f_var id)

969

h.hand_until;

970

hand_locals = rename_vars f_var h.hand_locals;

971

hand_stmts = rename_stmts f_node f_var h.hand_stmts;

972

hand_annots = rename_annots f_node f_var h.hand_annots;

973

}

974


975

and rename_aut f_node f_var aut =

976

{

977

aut with

978

aut_id = f_var aut.aut_id;

979

aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers;

980

}

981


982

and rename_stmts f_node f_var stmts =

983

List.map

984

(fun stmt >

985

match stmt with

986

 Eq eq >

987

Eq (rename_eq f_node f_var eq)

988

 Aut at >

989

Aut (rename_aut f_node f_var at))

990

stmts

991


992

and rename_annotl f_node f_var annots =

993

List.map (fun (key, value) > key, rename_eexpr f_node f_var value) annots

994


995

and rename_annot f_node f_var annot =

996

{ annot with annots = rename_annotl f_node f_var annot.annots }

997


998

and rename_annots f_node f_var annots =

999

List.map (rename_annot f_node f_var) annots

1000


1001

and rename_eexpr f_node f_var ee =

1002

{

1003

ee with

1004

eexpr_tag = Utils.new_tag ();

1005

eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;

1006

eexpr_quantifiers =

1007

List.map

1008

(fun (typ, vdecls) > typ, rename_vars f_var vdecls)

1009

ee.eexpr_quantifiers;

1010

}

1011


1012

and rename_mode f_node f_var m =

1013

let rename_ee = rename_eexpr f_node f_var in

1014

{

1015

m with

1016

require = List.map rename_ee m.require;

1017

ensure = List.map rename_ee m.ensure;

1018

}

1019


1020

let rename_import f_node f_var imp =

1021

let rename_expr = rename_expr f_node f_var in

1022

{

1023

imp with

1024

import_nodeid = f_node imp.import_nodeid;

1025

inputs = rename_expr imp.inputs;

1026

outputs = rename_expr imp.outputs;

1027

}

1028


1029

let rename_node f_node f_var nd =

1030

let f_var x =

1031

(* checking that this is actually a local variable *)

1032

if List.exists (fun v > v.var_id = x) (get_node_vars nd) then f_var x

1033

else x

1034

in

1035

let rename_var = rename_var f_var in

1036

let rename_vars = List.map rename_var in

1037

let rename_expr = rename_expr f_node f_var in

1038

let rename_eexpr = rename_eexpr f_node f_var in

1039

let rename_stmts = rename_stmts f_node f_var in

1040

let inputs = rename_vars nd.node_inputs in

1041

let outputs = rename_vars nd.node_outputs in

1042

let locals = rename_vars nd.node_locals in

1043

let gen_calls = List.map rename_expr nd.node_gencalls in

1044

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

1045

let node_asserts =

1046

List.map

1047

(fun a >

1048

{

1049

a with

1050

assert_expr =

1051

(let expr = a.assert_expr in

1052

rename_expr expr);

1053

})

1054

nd.node_asserts

1055

in

1056

let node_stmts = rename_stmts nd.node_stmts in

1057


1058

let spec =

1059

Utils.option_map

1060

(fun s >

1061

match s with

1062

 NodeSpec id >

1063

NodeSpec (f_node id)

1064

 Contract c >

1065

Contract

1066

{

1067

c with

1068

consts = rename_vars c.consts;

1069

locals = rename_vars c.locals;

1070

stmts = rename_stmts c.stmts;

1071

assume = List.map rename_eexpr c.assume;

1072

guarantees = List.map rename_eexpr c.guarantees;

1073

modes = List.map (rename_mode f_node f_var) c.modes;

1074

imports = List.map (rename_import f_node f_var) c.imports;

1075

})

1076

nd.node_spec

1077

in

1078

let annot = rename_annots f_node f_var nd.node_annot in

1079

{

1080

node_id = f_node nd.node_id;

1081

node_type = nd.node_type;

1082

node_clock = nd.node_clock;

1083

node_inputs = inputs;

1084

node_outputs = outputs;

1085

node_locals = locals;

1086

node_gencalls = gen_calls;

1087

node_checks;

1088

node_asserts;

1089

node_stmts;

1090

node_dec_stateless = nd.node_dec_stateless;

1091

node_stateless = nd.node_stateless;

1092

node_spec = spec;

1093

node_annot = annot;

1094

node_iscontract = nd.node_iscontract;

1095

}

1096


1097

let rename_const f_const c = { c with const_id = f_const c.const_id }

1098


1099

let rename_typedef f_var t =

1100

match t.tydef_desc with

1101

 Tydec_enum tags >

1102

{ t with tydef_desc = Tydec_enum (List.map f_var tags) }

1103

 _ >

1104

t

1105


1106

let rename_prog f_node f_var f_const prog =

1107

List.rev

1108

(List.fold_left

1109

(fun accu top >

1110

(match top.top_decl_desc with

1111

 Node nd >

1112

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

1113

 Const c >

1114

{ top with top_decl_desc = Const (rename_const f_const c) }

1115

 TypeDef tdef >

1116

{ top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }

1117

 ImportedNode _  Include _  Open _ >

1118

top)

1119

:: accu)

1120

[] prog)

1121


1122

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

1123

lhs satisfies predicate [pvar] *)

1124

let eq_replace_rhs_var pvar fvar eq =

1125

let pvar l = List.exists pvar l in

1126

let rec replace lhs rhs =

1127

{

1128

rhs with

1129

expr_desc =

1130

(match lhs with

1131

 [] >

1132

assert false

1133

 [ _ ] >

1134

if pvar lhs then rename_expr_desc (fun x > x) fvar rhs.expr_desc

1135

else rhs.expr_desc

1136

 _ > (

1137

match rhs.expr_desc with

1138

 Expr_tuple tl >

1139

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

1140

 Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs

1141

>

1142

let args = expr_list_of_expr arg in

1143

Expr_appl

1144

( f,

1145

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

1146

None )

1147

 Expr_array _

1148

 Expr_access _

1149

 Expr_power _

1150

 Expr_const _

1151

 Expr_ident _

1152

 Expr_appl _ >

1153

if pvar lhs then rename_expr_desc (fun x > x) fvar rhs.expr_desc

1154

else rhs.expr_desc

1155

 Expr_ite (c, t, e) >

1156

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

1157

 Expr_arrow (e1, e2) >

1158

Expr_arrow (replace lhs e1, replace lhs e2)

1159

 Expr_fby (e1, e2) >

1160

Expr_fby (replace lhs e1, replace lhs e2)

1161

 Expr_pre e' >

1162

Expr_pre (replace lhs e')

1163

 Expr_when (e', i, l) >

1164

let i' = if pvar lhs then fvar i else i in

1165

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

1166

 Expr_merge (i, hl) >

1167

let i' = if pvar lhs then fvar i else i in

1168

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

1169

}

1170

in

1171

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

1172


1173

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

1174

(* Pretty printers *)

1175


1176

let pp_decl_type fmt tdecl =

1177

match tdecl.top_decl_desc with

1178

 Node nd >

1179

fprintf fmt "%s: " nd.node_id;

1180

Utils.reset_names ();

1181

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

1182

 ImportedNode ind >

1183

fprintf fmt "%s: " ind.nodei_id;

1184

Utils.reset_names ();

1185

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

1186

 Const _  Include _  Open _  TypeDef _ >

1187

()

1188


1189

let pp_prog_type fmt tdecl_list =

1190

Utils.Format.(

1191

pp_print_list ~pp_open_box:pp_open_vbox0 pp_decl_type fmt tdecl_list)

1192


1193

let pp_decl_clock fmt cdecl =

1194

match cdecl.top_decl_desc with

1195

 Node nd >

1196

fprintf fmt "%s: " nd.node_id;

1197

Utils.reset_names ();

1198

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

1199

 ImportedNode ind >

1200

fprintf fmt "%s: " ind.nodei_id;

1201

Utils.reset_names ();

1202

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

1203

 Const _  Include _  Open _  TypeDef _ >

1204

()

1205


1206

let pp_prog_clock fmt prog = Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog

1207


1208

(* filling node table with internal functions *)

1209

let vdecls_of_typ_ck cpt ty =

1210

let loc = Location.dummy_loc in

1211

List.map

1212

(fun _ >

1213

incr cpt;

1214

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

1215

mkvar_decl loc

1216

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

1217

(Types.type_list_of_type ty)

1218


1219

let mk_internal_node id =

1220

let spec = None in

1221

let ty = Env.lookup_value Basic_library.type_env id in

1222

let ck = Env.lookup_value Basic_library.clock_env id in

1223

let tin, tout = Types.split_arrow ty in

1224

(*eprintf "internal fun %s: %d > %d@." id (List.length

1225

(Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)

1226

let cpt = ref (1) in

1227

mktop

1228

(ImportedNode

1229

{

1230

nodei_id = id;

1231

nodei_type = ty;

1232

nodei_clock = ck;

1233

nodei_inputs = vdecls_of_typ_ck cpt tin;

1234

nodei_outputs = vdecls_of_typ_ck cpt tout;

1235

nodei_stateless = Types.get_static_value ty <> None;

1236

nodei_spec = spec;

1237

(* nodei_annot = []; *)

1238

nodei_prototype = None;

1239

nodei_in_lib = [];

1240

})

1241


1242

let add_internal_funs () =

1243

List.iter

1244

(fun id >

1245

let nd = mk_internal_node id in

1246

Hashtbl.add node_table id nd)

1247

Basic_library.internal_funs

1248


1249

(* Replace any occurence of a var in vars_to_replace by its associated

1250

expression in defs until e does not contain any such variables *)

1251

let rec substitute_expr vars_to_replace defs e =

1252

let se = substitute_expr vars_to_replace defs in

1253

{

1254

e with

1255

expr_desc =

1256

(let ed = e.expr_desc in

1257

match ed with

1258

 Expr_const _ >

1259

ed

1260

 Expr_array el >

1261

Expr_array (List.map se el)

1262

 Expr_access (e1, d) >

1263

Expr_access (se e1, d)

1264

 Expr_power (e1, d) >

1265

Expr_power (se e1, d)

1266

 Expr_tuple el >

1267

Expr_tuple (List.map se el)

1268

 Expr_ite (c, t, e) >

1269

Expr_ite (se c, se t, se e)

1270

 Expr_arrow (e1, e2) >

1271

Expr_arrow (se e1, se e2)

1272

 Expr_fby (e1, e2) >

1273

Expr_fby (se e1, se e2)

1274

 Expr_pre e' >

1275

Expr_pre (se e')

1276

 Expr_when (e', i, l) >

1277

Expr_when (se e', i, l)

1278

 Expr_merge (i, hl) >

1279

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

1280

 Expr_appl (i, e', i') >

1281

Expr_appl (i, se e', i')

1282

 Expr_ident i >

1283

if List.exists (fun v > v.var_id = i) vars_to_replace then

1284

let eq_i eq = eq.eq_lhs = [ i ] in

1285

if List.exists eq_i defs then

1286

let sub = List.find eq_i defs in

1287

let sub' = se sub.eq_rhs in

1288

sub'.expr_desc

1289

else assert false

1290

else ed);

1291

}

1292


1293

let expr_to_eexpr expr =

1294

{

1295

eexpr_tag = expr.expr_tag;

1296

eexpr_qfexpr = expr;

1297

eexpr_quantifiers = [];

1298

eexpr_name = None;

1299

eexpr_type = expr.expr_type;

1300

eexpr_clock = expr.expr_clock;

1301

eexpr_loc = expr.expr_loc (*eexpr_normalized = None*);

1302

}

1303


1304

(* and expr_desc_to_eexpr_desc expr_desc = *)

1305

(* let conv = expr_to_eexpr in *)

1306

(* match expr_desc with *)

1307

(*  Expr_const c > EExpr_const (match c with *)

1308

(*  Const_int x > EConst_int x *)

1309

(*  Const_real x > EConst_real x *)

1310

(*  Const_float x > EConst_float x *)

1311

(*  Const_tag x > EConst_tag x *)

1312

(*  _ > assert false *)

1313


1314

(* ) *)

1315

(*  Expr_ident i > EExpr_ident i *)

1316

(*  Expr_tuple el > EExpr_tuple (List.map conv el) *)

1317


1318

(*  Expr_arrow (e1, e2)> EExpr_arrow (conv e1, conv e2) *)

1319

(*  Expr_fby (e1, e2) > EExpr_fby (conv e1, conv e2) *)

1320

(*  Expr_pre e' > EExpr_pre (conv e') *)

1321

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

1322

(* EExpr_appl *)

1323

(* (i, conv e', match i' with None > None  Some(id, _) > Some id) *)

1324


1325

(*  Expr_when _ *)

1326

(*  Expr_merge _ > assert false *)

1327

(*  Expr_array _ *)

1328

(*  Expr_access _ *)

1329

(*  Expr_power _ > assert false *)

1330

(*  Expr_ite (c, t, e) > assert false *)

1331

(*  _ > assert false *)

1332


1333

let rec get_expr_calls nodes e =

1334

let get_calls = get_expr_calls nodes in

1335

match e.expr_desc with

1336

 Expr_const _  Expr_ident _ >

1337

Utils.ISet.empty

1338

 Expr_tuple el  Expr_array el >

1339

List.fold_left

1340

(fun accu e > Utils.ISet.union accu (get_calls e))

1341

Utils.ISet.empty el

1342

 Expr_pre e1  Expr_when (e1, _, _)  Expr_access (e1, _)  Expr_power (e1, _)

1343

>

1344

get_calls e1

1345

 Expr_ite (c, t, e) >

1346

Utils.ISet.union

1347

(Utils.ISet.union (get_calls c) (get_calls t))

1348

(get_calls e)

1349

 Expr_arrow (e1, e2)  Expr_fby (e1, e2) >

1350

Utils.ISet.union (get_calls e1) (get_calls e2)

1351

 Expr_merge (_, hl) >

1352

List.fold_left

1353

(fun accu (_, h) > Utils.ISet.union accu (get_calls h))

1354

Utils.ISet.empty hl

1355

 Expr_appl (i, e', _) >

1356

if Basic_library.is_expr_internal_fun e then get_calls e'

1357

else

1358

let calls = Utils.ISet.add i (get_calls e') in

1359

let test n =

1360

match n.top_decl_desc with Node nd > nd.node_id = i  _ > false

1361

in

1362

if List.exists test nodes then

1363

match (List.find test nodes).top_decl_desc with

1364

 Node nd >

1365

Utils.ISet.union (get_node_calls nodes nd) calls

1366

 _ >

1367

assert false

1368

else calls

1369


1370

and get_eq_calls nodes eq = get_expr_calls nodes eq.eq_rhs

1371


1372

and get_aut_handler_calls nodes h =

1373

List.fold_left

1374

(fun accu stmt >

1375

match stmt with

1376

 Eq eq >

1377

Utils.ISet.union (get_eq_calls nodes eq) accu

1378

 Aut aut' >

1379

Utils.ISet.union (get_aut_calls nodes aut') accu)

1380

Utils.ISet.empty h.hand_stmts

1381


1382

and get_aut_calls nodes aut =

1383

List.fold_left

1384

(fun accu h > Utils.ISet.union (get_aut_handler_calls nodes h) accu)

1385

Utils.ISet.empty aut.aut_handlers

1386


1387

and get_node_calls nodes node =

1388

let eqs, auts = get_node_eqs node in

1389

let aut_calls =

1390

List.fold_left

1391

(fun accu aut > Utils.ISet.union (get_aut_calls nodes aut) accu)

1392

Utils.ISet.empty auts

1393

in

1394

List.fold_left

1395

(fun accu eq > Utils.ISet.union (get_eq_calls nodes eq) accu)

1396

aut_calls eqs

1397


1398

let get_expr_vars e =

1399

let rec get_expr_vars vars e = get_expr_desc_vars vars e.expr_desc

1400

and get_expr_desc_vars vars expr_desc =

1401

(*Format.eprintf "get_expr_desc_vars expr=%a@." Printers.pp_expr (mkexpr

1402

Location.dummy_loc expr_desc);*)

1403

match expr_desc with

1404

 Expr_const _ >

1405

vars

1406

 Expr_ident x >

1407

Utils.ISet.add x vars

1408

 Expr_tuple el  Expr_array el >

1409

List.fold_left get_expr_vars vars el

1410

 Expr_pre e1 >

1411

get_expr_vars vars e1

1412

 Expr_when (e1, c, _) >

1413

get_expr_vars (Utils.ISet.add c vars) e1

1414

 Expr_access (e1, d)  Expr_power (e1, d) >

1415

List.fold_left get_expr_vars vars [ e1; expr_of_dimension d ]

1416

 Expr_ite (c, t, e) >

1417

List.fold_left get_expr_vars vars [ c; t; e ]

1418

 Expr_arrow (e1, e2)  Expr_fby (e1, e2) >

1419

List.fold_left get_expr_vars vars [ e1; e2 ]

1420

 Expr_merge (c, hl) >

1421

List.fold_left

1422

(fun vars (_, h) > get_expr_vars vars h)

1423

(Utils.ISet.add c vars) hl

1424

 Expr_appl (_, arg, None) >

1425

get_expr_vars vars arg

1426

 Expr_appl (_, arg, Some r) >

1427

List.fold_left get_expr_vars vars [ arg; r ]

1428

in

1429

get_expr_vars Utils.ISet.empty e

1430


1431

(* let rec expr_has_arrows e =

1432

* expr_desc_has_arrows e.expr_desc

1433

* and expr_desc_has_arrows expr_desc =

1434

* match expr_desc with

1435

*  Expr_const _

1436

*  Expr_ident _ > false

1437

*  Expr_tuple el

1438

*  Expr_array el > List.exists expr_has_arrows el

1439

*  Expr_pre e1

1440

*  Expr_when (e1, _, _)

1441

*  Expr_access (e1, _)

1442

*  Expr_power (e1, _) > expr_has_arrows e1

1443

*  Expr_ite (c, t, e) > List.exists expr_has_arrows [c; t; e]

1444

*  Expr_arrow _

1445

*  Expr_fby _ > true

1446

*  Expr_merge (_, hl) > List.exists (fun (_, h) > expr_has_arrows h) hl

1447

*  Expr_appl (_, e', _) > expr_has_arrows e'

1448

*

1449

* and eq_has_arrows eq =

1450

* expr_has_arrows eq.eq_rhs

1451

* and aut_has_arrows aut = List.exists (fun h > List.exists (fun stmt > match stmt with Eq eq > eq_has_arrows eq  Aut aut' > aut_has_arrows aut') h.hand_stmts ) aut.aut_handlers

1452

* and node_has_arrows node =

1453

* let eqs, auts = get_node_eqs node in

1454

* List.exists (fun eq > eq_has_arrows eq) eqs  List.exists (fun aut > aut_has_arrows aut) auts *)

1455


1456

let rec expr_contains_expr expr_tag expr =

1457

let search = expr_contains_expr expr_tag in

1458

expr.expr_tag = expr_tag

1459



1460

match expr.expr_desc with

1461

 Expr_const _ >

1462

false

1463

 Expr_array el >

1464

List.exists search el

1465

 Expr_access (e1, _)  Expr_power (e1, _) >

1466

search e1

1467

 Expr_tuple el >

1468

List.exists search el

1469

 Expr_ite (c, t, e) >

1470

List.exists search [ c; t; e ]

1471

 Expr_arrow (e1, e2)  Expr_fby (e1, e2) >

1472

List.exists search [ e1; e2 ]

1473

 Expr_pre e'  Expr_when (e', _, _) >

1474

search e'

1475

 Expr_merge (_, hl) >

1476

List.exists (fun (_, h) > search h) hl

1477

 Expr_appl (_, e', None) >

1478

search e'

1479

 Expr_appl (_, e', Some e'') >

1480

List.exists search [ e'; e'' ]

1481

 Expr_ident _ >

1482

false

1483


1484

(* Generate a new local [node] variable *)

1485

let cpt_fresh = ref 0

1486


1487

let reset_cpt_fresh () = cpt_fresh := 0

1488


1489

let mk_fresh_var (parentid, ctx_env) loc ty ck =

1490

let rec aux () =

1491

incr cpt_fresh;

1492

let s = Printf.sprintf "__%s_%d" parentid !cpt_fresh in

1493

if List.exists (fun v > v.var_id = s) ctx_env then aux ()

1494

else

1495

{

1496

var_id = s;

1497

var_orig = false;

1498

var_dec_type = dummy_type_dec;

1499

var_dec_clock = dummy_clock_dec;

1500

var_dec_const = false;

1501

var_dec_value = None;

1502

var_parent_nodeid = Some parentid;

1503

var_type = ty;

1504

var_clock = ck;

1505

var_loc = loc;

1506

}

1507

in

1508

aux ()

1509


1510

let find_eq xl eqs =

1511

let rec aux accu eqs =

1512

match eqs with

1513

 [] >

1514

Format.eprintf "Looking for variables %a in the following equations@.%a@."

1515

(Utils.fprintf_list ~sep:" , " (fun fmt v > Format.fprintf fmt "%s" v))

1516

xl Printers.pp_node_eqs eqs;

1517

assert false

1518

 hd :: tl >

1519

if List.exists (fun x > List.mem x hd.eq_lhs) xl then hd, accu @ tl

1520

else aux (hd :: accu) tl

1521

in

1522

aux [] eqs

1523


1524

let get_node name prog =

1525

let node_opt =

1526

List.fold_left

1527

(fun res top >

1528

match res, top.top_decl_desc with

1529

 Some _, _ >

1530

res

1531

 None, Node nd >

1532

(* Format.eprintf "Checking node %s = %s: %b@." nd.node_id name

1533

(nd.node_id = name); *)

1534

if nd.node_id = name then Some nd else res

1535

 _ >

1536

None)

1537

None prog

1538

in

1539

try Utils.desome node_opt with Utils.DeSome > raise Not_found

1540


1541

(* Pushing negations in expression. Subtitute operators whenever possible *)

1542

let rec push_negations ?(neg = false) e =

1543

let res =

1544

let pn = push_negations in

1545

let map desc =

1546

(* Keeping clock and type info *)

1547

let new_e = mkexpr e.expr_loc desc in

1548

{ new_e with expr_type = e.expr_type; expr_clock = e.expr_clock }

1549

in

1550

match e.expr_desc with

1551

 Expr_ite (g, t, e) >

1552

if neg then map (Expr_ite (pn g, pn e, pn t))

1553

else map (Expr_ite (pn g, pn t, pn e))

1554

 Expr_tuple t >

1555

map (Expr_tuple (List.map (pn ~neg) t))

1556

 Expr_arrow (e1, e2) >

1557

map (Expr_arrow (pn ~neg e1, pn ~neg e2))

1558

 Expr_fby (e1, e2) >

1559

map (Expr_fby (pn ~neg e1, pn ~neg e2))

1560

 Expr_pre e >

1561

map (Expr_pre (pn ~neg e))

1562

 Expr_appl (op, e', None) when op = "not" >

1563

if neg then push_negations ~neg:false e' else push_negations ~neg:true e'

1564

 Expr_appl (op, e', None)

1565

when List.mem op (Basic_library.bool_funs @ Basic_library.rel_funs) > (

1566

match op with

1567

 "&&" >

1568

map (Expr_appl ((if neg then "" else op), pn ~neg e', None))

1569

 "" >

1570

map (Expr_appl ((if neg then "&&" else op), pn ~neg e', None))

1571

(* TODO xor/equi/impl *)

1572

 "<" >

1573

map (Expr_appl ((if neg then ">=" else op), pn e', None))

1574

 ">" >

1575

map (Expr_appl ((if neg then "<=" else op), pn e', None))

1576

 "<=" >

1577

map (Expr_appl ((if neg then ">" else op), pn e', None))

1578

 ">=" >

1579

map (Expr_appl ((if neg then "<" else op), pn e', None))

1580

 "!=" >

1581

map (Expr_appl ((if neg then "=" else op), pn e', None))

1582

 "=" >

1583

map (Expr_appl ((if neg then "!=" else op), pn e', None))

1584

 _ >

1585

assert false)

1586

 Expr_const c >

1587

if neg then map (Expr_const (const_negation c)) else e

1588

 Expr_ident _ >

1589

if neg then mkpredef_call e.expr_loc "not" [ e ] else e

1590

 Expr_appl _ >

1591

if neg then mkpredef_call e.expr_loc "not" [ e ] else e

1592

 _ >

1593

assert false

1594

(* no array, array access, power or merge/when *)

1595

in

1596

res

1597


1598

let rec add_pre_expr vars e =

1599

let ap = add_pre_expr vars in

1600

let desc =

1601

match e.expr_desc with

1602

 Expr_ite (g, t, e) >

1603

Expr_ite (ap g, ap t, ap e)

1604

 Expr_tuple t >

1605

Expr_tuple (List.map ap t)

1606

 Expr_arrow (e1, e2) >

1607

Expr_arrow (ap e1, ap e2)

1608

 Expr_fby (e1, e2) >

1609

Expr_fby (ap e1, ap e2)

1610

 Expr_pre e >

1611

Expr_pre (ap e)

1612

 Expr_appl (op, e, opt) >

1613

Expr_appl (op, ap e, opt)

1614

 Expr_const _ >

1615

e.expr_desc

1616

 Expr_ident id >

1617

if List.mem id vars then Expr_pre e else e.expr_desc

1618

 _ >

1619

assert false

1620

(* no array, array access, power or merge/when yet *)

1621

in

1622

let new_e = mkexpr e.expr_loc desc in

1623

{ new_e with expr_type = e.expr_type; expr_clock = e.expr_clock }

1624


1625

let mk_eq l e1 e2 = mkpredef_call l "=" [ e1; e2 ]

1626


1627

let rec partial_eval e =

1628

let pa = partial_eval in

1629

let edesc =

1630

match e.expr_desc with

1631

 Expr_const _ >

1632

e.expr_desc

1633

 Expr_ident _ >

1634

e.expr_desc

1635

 Expr_ite (g, t, e) > (

1636

let g, t, e = pa g, pa t, pa e in

1637

match g.expr_desc with

1638

 Expr_const (Const_tag tag) when tag = tag_true >

1639

t.expr_desc

1640

 Expr_const (Const_tag tag) when tag = tag_false >

1641

e.expr_desc

1642

 _ >

1643

Expr_ite (g, t, e))

1644

 Expr_tuple t >

1645

Expr_tuple (List.map pa t)

1646

 Expr_arrow (e1, e2) >

1647

Expr_arrow (pa e1, pa e2)

1648

 Expr_fby (e1, e2) >

1649

Expr_fby (pa e1, pa e2)

1650

 Expr_pre e >

1651

Expr_pre (pa e)

1652

 Expr_appl (op, args, opt) >

1653

let args = pa args in

1654

if Basic_library.is_expr_internal_fun e then

1655

Basic_library.partial_eval op args opt

1656

else Expr_appl (op, args, opt)

1657

 Expr_array el >

1658

Expr_array (List.map pa el)

1659

 Expr_access (e, d) >

1660

Expr_access (pa e, d)

1661

 Expr_power (e, d) >

1662

Expr_power (pa e, d)

1663

 Expr_when (e, id, l) >

1664

Expr_when (pa e, id, l)

1665

 Expr_merge (id, gl) >

1666

Expr_merge (id, List.map (fun (l, e) > l, pa e) gl)

1667

in

1668

{ e with expr_desc = edesc }

1669


1670

(* Local Variables: *)

1671

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

1672

(* End: *)
