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 LustreSpec

13

open Corelang

14

open Clocks

15

open Causality

16


17

exception NormalizationError

18


19

module OrdVarDecl:Map.OrderedType with type t=var_decl =

20

struct type t = var_decl;; let compare = compare end

21


22

module ISet = Set.Make(OrdVarDecl)

23


24

let rec pp_val fmt v =

25

match v.value_desc with

26

 Cst c > Printers.pp_const fmt c

27

 LocalVar v > Format.pp_print_string fmt v.var_id

28

 StateVar v > Format.pp_print_string fmt v.var_id

29

 Array vl > Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl

30

 Access (t, i) > Format.fprintf fmt "%a[%a]" pp_val t pp_val i

31

 Power (v, n) > Format.fprintf fmt "(%a^%a)" pp_val v pp_val n

32

 Fun (n, vl) > Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl

33


34

let rec pp_instr fmt i =

35

match i with

36

 MLocalAssign (i,v) > Format.fprintf fmt "%s<l %a" i.var_id pp_val v

37

 MStateAssign (i,v) > Format.fprintf fmt "%s<s %a" i.var_id pp_val v

38

 MReset i > Format.fprintf fmt "reset %s" i

39

 MNoReset i > Format.fprintf fmt "noreset %s" i

40

 MStep (il, i, vl) >

41

Format.fprintf fmt "%a = %s (%a)"

42

(Utils.fprintf_list ~sep:", " (fun fmt v > Format.pp_print_string fmt v.var_id)) il

43

i

44

(Utils.fprintf_list ~sep:", " pp_val) vl

45

 MBranch (g,hl) >

46

Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"

47

pp_val g

48

(Utils.fprintf_list ~sep:"@," pp_branch) hl

49

 MComment s > Format.pp_print_string fmt s

50


51

and pp_branch fmt (t, h) =

52

Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h

53


54

and pp_instrs fmt il =

55

Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," pp_instr) il

56


57

type step_t = {

58

step_checks: (Location.t * value_t) list;

59

step_inputs: var_decl list;

60

step_outputs: var_decl list;

61

step_locals: var_decl list;

62

step_instrs: instr_t list;

63

step_asserts: value_t list;

64

}

65


66

type static_call = top_decl * (Dimension.dim_expr list)

67


68

type machine_t = {

69

mname: node_desc;

70

mmemory: var_decl list;

71

mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *)

72

minstances: (ident * static_call) list; (* submap of mcalls, from stateful instance to node *)

73

minit: instr_t list;

74

mstatic: var_decl list; (* static inputs only *)

75

mconst: instr_t list; (* assignments of node constant locals *)

76

mstep: step_t;

77

mspec: node_annot option;

78

mannot: expr_annot list;

79

}

80


81

let pp_step fmt s =

82

Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "

83

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

84

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

85

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

86

(Utils.fprintf_list ~sep:", " (fun fmt (_, c) > pp_val fmt c)) s.step_checks

87

(Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs

88

(Utils.fprintf_list ~sep:", " pp_val) s.step_asserts

89


90


91

let pp_static_call fmt (node, args) =

92

Format.fprintf fmt "%s<%a>"

93

(node_name node)

94

(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args

95


96

let pp_machine fmt m =

97

Format.fprintf fmt

98

"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ const : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ "

99

m.mname.node_id

100

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

101

(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) > Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances

102

(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit

103

(Utils.fprintf_list ~sep:"@ " pp_instr) m.mconst

104

pp_step m.mstep

105

(fun fmt > match m.mspec with  None > ()  Some spec > Printers.pp_spec fmt spec)

106

(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot

107


108

let rec is_const_value v =

109

match v.value_desc with

110

 Cst _ > true

111

 Fun (id, args) > Basic_library.is_value_internal_fun v && List.for_all is_const_value args

112

 _ > false

113


114

(* Returns the declared stateless status and the computed one. *)

115

let get_stateless_status m =

116

(m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless)

117


118

let is_input m id =

119

List.exists (fun o > o.var_id = id.var_id) m.mstep.step_inputs

120


121

let is_output m id =

122

List.exists (fun o > o.var_id = id.var_id) m.mstep.step_outputs

123


124

let is_memory m id =

125

List.exists (fun o > o.var_id = id.var_id) m.mmemory

126


127

let conditional c t e =

128

MBranch(c, [ (tag_true, t); (tag_false, e) ])

129


130

let dummy_var_decl name typ =

131

{

132

var_id = name;

133

var_orig = false;

134

var_dec_type = dummy_type_dec;

135

var_dec_clock = dummy_clock_dec;

136

var_dec_const = false;

137

var_dec_value = None;

138

var_type = typ;

139

var_clock = Clocks.new_ck Clocks.Cvar true;

140

var_loc = Location.dummy_loc

141

}

142


143

let arrow_id = "_arrow"

144


145

let arrow_typ = Types.new_ty Types.Tunivar

146


147

let arrow_desc =

148

{

149

node_id = arrow_id;

150

node_type = Type_predef.type_bin_poly_op;

151

node_clock = Clock_predef.ck_bin_univ;

152

node_inputs= [dummy_var_decl "_in1" arrow_typ; dummy_var_decl "_in2" arrow_typ];

153

node_outputs= [dummy_var_decl "_out" arrow_typ];

154

node_locals= [];

155

node_gencalls = [];

156

node_checks = [];

157

node_asserts = [];

158

node_stmts= [];

159

node_dec_stateless = false;

160

node_stateless = Some false;

161

node_spec = None;

162

node_annot = []; }

163


164

let arrow_top_decl =

165

{

166

top_decl_desc = Node arrow_desc;

167

top_decl_owner = !Options.include_dir;

168

top_decl_itf = false;

169

top_decl_loc = Location.dummy_loc

170

}

171


172

let mk_val v t = { value_desc = v;

173

value_type = t;

174

value_annot = None }

175


176

let arrow_machine =

177

let state = "_first" in

178

let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in

179

let var_input1 = List.nth arrow_desc.node_inputs 0 in

180

let var_input2 = List.nth arrow_desc.node_inputs 1 in

181

let var_output = List.nth arrow_desc.node_outputs 0 in

182

let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in

183

let t_arg = Types.new_univar () in (* TODO Xavier: c'est bien la bonne def ? *)

184

{

185

mname = arrow_desc;

186

mmemory = [var_state];

187

mcalls = [];

188

minstances = [];

189

minit = [MStateAssign(var_state, cst true)];

190

mstatic = [];

191

mconst = [];

192

mstep = {

193

step_inputs = arrow_desc.node_inputs;

194

step_outputs = arrow_desc.node_outputs;

195

step_locals = [];

196

step_checks = [];

197

step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool)

198

[MStateAssign(var_state, cst false);

199

MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)]

200

[MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)] ];

201

step_asserts = [];

202

};

203

mspec = None;

204

mannot = [];

205

}

206


207

let empty_desc =

208

{

209

node_id = arrow_id;

210

node_type = Types.bottom;

211

node_clock = Clocks.bottom;

212

node_inputs= [];

213

node_outputs= [];

214

node_locals= [];

215

node_gencalls = [];

216

node_checks = [];

217

node_asserts = [];

218

node_stmts= [];

219

node_dec_stateless = true;

220

node_stateless = Some true;

221

node_spec = None;

222

node_annot = []; }

223


224

let empty_machine =

225

{

226

mname = empty_desc;

227

mmemory = [];

228

mcalls = [];

229

minstances = [];

230

minit = [];

231

mstatic = [];

232

mconst = [];

233

mstep = {

234

step_inputs = [];

235

step_outputs = [];

236

step_locals = [];

237

step_checks = [];

238

step_instrs = [];

239

step_asserts = [];

240

};

241

mspec = None;

242

mannot = [];

243

}

244


245

let new_instance =

246

let cpt = ref (1) in

247

fun caller callee tag >

248

begin

249

let o =

250

if Stateless.check_node callee then

251

node_name callee

252

else

253

Printf.sprintf "ni_%d" (incr cpt; !cpt) in

254

let o =

255

if !Options.ansi && is_generic_node callee

256

then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e > e.expr_tag = tag) caller.node_gencalls)

257

else o in

258

o

259

end

260


261


262

(* translate_<foo> : node > context > <foo> > machine code/expression *)

263

(* the context contains m : state aka memory variables *)

264

(* si : initialization instructions *)

265

(* j : node aka machine instances *)

266

(* d : local variables *)

267

(* s : step instructions *)

268

let translate_ident node (m, si, j, d, s) id =

269

try (* id is a node var *)

270

let var_id = get_node_var id node in

271

if ISet.exists (fun v > v.var_id = id) m

272

then mk_val (StateVar var_id) var_id.var_type

273

else mk_val (LocalVar var_id) var_id.var_type

274

with Not_found >

275

try (* id is a constant *)

276

let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in

277

mk_val (LocalVar vdecl) vdecl.var_type

278

with Not_found >

279

(* id is a tag *)

280

(* DONE construire une liste des enum declarés et alors chercher dedans la liste

281

qui contient id *)

282

try

283

let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in

284

mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)

285

with Not_found > (Format.eprintf "internal error: Machine_code.translate_ident %s" id;

286

assert false)

287


288

let rec control_on_clock node ((m, si, j, d, s) as args) ck inst =

289

match (Clocks.repr ck).cdesc with

290

 Con (ck1, cr, l) >

291

let id = Clocks.const_of_carrier cr in

292

control_on_clock node args ck1 (MBranch (translate_ident node args id,

293

[l, [inst]] ))

294

 _ > inst

295


296

let rec join_branches hl1 hl2 =

297

match hl1, hl2 with

298

 [] , _ > hl2

299

 _ , [] > hl1

300

 (t1, h1)::q1, (t2, h2)::q2 >

301

if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else

302

if t1 > t2 then (t2, h2) :: join_branches hl1 q2

303

else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2

304


305

and join_guards inst1 insts2 =

306

match inst1, insts2 with

307

 _ , [] >

308

[inst1]

309

 MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 >

310

MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2))

311

:: q

312

 _ > inst1 :: insts2

313


314

let join_guards_list insts =

315

List.fold_right join_guards insts []

316


317

(* specialize predefined (polymorphic) operators

318

wrt their instances, so that the C semantics

319

is preserved *)

320

let specialize_to_c expr =

321

match expr.expr_desc with

322

 Expr_appl (id, e, r) >

323

if List.exists (fun e > Types.is_bool_type e.expr_type) (expr_list_of_expr e)

324

then let id =

325

match id with

326

 "=" > "equi"

327

 "!=" > "xor"

328

 _ > id in

329

{ expr with expr_desc = Expr_appl (id, e, r) }

330

else expr

331

 _ > expr

332


333

let specialize_op expr =

334

match !Options.output with

335

 "C" > specialize_to_c expr

336

 _ > expr

337


338

let rec translate_expr node ((m, si, j, d, s) as args) expr =

339

let expr = specialize_op expr in

340

let value_desc =

341

match expr.expr_desc with

342

 Expr_const v > Cst v

343

 Expr_ident x > (translate_ident node args x).value_desc

344

 Expr_array el > Array (List.map (translate_expr node args) el)

345

 Expr_access (t, i) > Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))

346

 Expr_power (e, n) > Power (translate_expr node args e, translate_expr node args (expr_of_dimension n))

347

 Expr_tuple _

348

 Expr_arrow _

349

 Expr_fby _

350

 Expr_pre _ > (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)

351

 Expr_when (e1, _, _) > (translate_expr node args e1).value_desc

352

 Expr_merge (x, _) > raise NormalizationError

353

 Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr >

354

let nd = node_from_name id in

355

Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))

356

(* Expr_ite (g,t,e) > (

357

(* special treatment depending on the active backend. For horn backend, ite

358

are preserved in expression. While they are removed for C or Java

359

backends. *)

360

match !Options.output with  "horn" >

361

Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])

362

 "C"  "java"  _ >

363

(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)

364

)*)

365

 _ > raise NormalizationError

366

in

367

mk_val value_desc expr.expr_type

368


369

let translate_guard node args expr =

370

match expr.expr_desc with

371

 Expr_ident x > translate_ident node args x

372

 _ > (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false)

373


374

let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =

375

match expr.expr_desc with

376

 Expr_ite (c, t, e) > let g = translate_guard node args c in

377

conditional g

378

[translate_act node args (y, t)]

379

[translate_act node args (y, e)]

380

 Expr_merge (x, hl) > MBranch (translate_ident node args x,

381

List.map (fun (t, h) > t, [translate_act node args (y, h)]) hl)

382

 _ > MLocalAssign (y, translate_expr node args expr)

383


384

let reset_instance node args i r c =

385

match r with

386

 None > []

387

 Some r > let g = translate_guard node args r in

388

[control_on_clock node args c (conditional g [MReset i] [MNoReset i])]

389


390

let translate_eq node ((m, si, j, d, s) as args) eq =

391

(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)

392

match eq.eq_lhs, eq.eq_rhs.expr_desc with

393

 [x], Expr_arrow (e1, e2) >

394

let var_x = get_node_var x node in

395

let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in

396

let c1 = translate_expr node args e1 in

397

let c2 = translate_expr node args e2 in

398

(m,

399

MReset o :: si,

400

Utils.IMap.add o (arrow_top_decl, []) j,

401

d,

402

(control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s)

403

 [x], Expr_pre e1 when ISet.mem (get_node_var x node) d >

404

let var_x = get_node_var x node in

405

(ISet.add var_x m,

406

si,

407

j,

408

d,

409

control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s)

410

 [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d >

411

let var_x = get_node_var x node in

412

(ISet.add var_x m,

413

MStateAssign (var_x, translate_expr node args e1) :: si,

414

j,

415

d,

416

control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)

417


418

 p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) >

419

let var_p = List.map (fun v > get_node_var v node) p in

420

let el = expr_list_of_expr arg in

421

let vl = List.map (translate_expr node args) el in

422

let node_f = node_from_name f in

423

let call_f =

424

node_f,

425

NodeDep.filter_static_inputs (node_inputs node_f) el in

426

let o = new_instance node node_f eq.eq_rhs.expr_tag in

427

let env_cks = List.fold_right (fun arg cks > arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in

428

let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in

429

(*Clocks.new_var true in

430

Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;

431

Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)

432

(m,

433

(if Stateless.check_node node_f then si else MReset o :: si),

434

Utils.IMap.add o call_f j,

435

d,

436

(if Stateless.check_node node_f

437

then []

438

else reset_instance node args o r call_ck) @

439

(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)

440

(*

441

(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)

442

are preserved. While they are replaced as if g then x = t else x = e in C or Java

443

backends. *)

444

 [x], Expr_ite (c, t, e)

445

when (match !Options.output with  "horn" > true  "C"  "java"  _ > false)

446

>

447

let var_x = get_node_var x node in

448

(m,

449

si,

450

j,

451

d,

452

(control_on_clock node args eq.eq_rhs.expr_clock

453

(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)

454

)

455


456

*)

457

 [x], _ > (

458

let var_x = get_node_var x node in

459

(m, si, j, d,

460

control_on_clock

461

node

462

args

463

eq.eq_rhs.expr_clock

464

(translate_act node args (var_x, eq.eq_rhs)) :: s

465

)

466

)

467

 _ >

468

begin

469

Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq;

470

assert false

471

end

472


473

let find_eq xl eqs =

474

let rec aux accu eqs =

475

match eqs with

476

 [] >

477

begin

478

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

479

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

480

Printers.pp_node_eqs eqs;

481

assert false

482

end

483

 hd::tl >

484

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

485

in

486

aux [] eqs

487


488

(* Sort the set of equations of node [nd] according

489

to the computed schedule [sch]

490

*)

491

let sort_equations_from_schedule nd sch =

492

(* Format.eprintf "%s schedule: %a@." *)

493

(* nd.node_id *)

494

(* (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch; *)

495

let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in

496

let eqs_rev, remainder =

497

List.fold_left

498

(fun (accu, node_eqs_remainder) vl >

499

if List.exists (fun eq > List.exists (fun v > List.mem v eq.eq_lhs) vl) accu

500

then

501

(accu, node_eqs_remainder)

502

else

503

let eq_v, remainder = find_eq vl node_eqs_remainder in

504

eq_v::accu, remainder

505

)

506

([], split_eqs)

507

sch

508

in

509

begin

510

if List.length remainder > 0 then (

511

Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?"

512

Printers.pp_node_eqs remainder

513

Printers.pp_node_eqs (get_node_eqs nd);

514

assert false);

515

List.rev eqs_rev

516

end

517


518

let constant_equations nd =

519

List.fold_right (fun vdecl eqs >

520

if vdecl.var_dec_const

521

then

522

{ eq_lhs = [vdecl.var_id];

523

eq_rhs = Utils.desome vdecl.var_dec_value;

524

eq_loc = vdecl.var_loc

525

} :: eqs

526

else eqs)

527

nd.node_locals []

528


529

let translate_eqs node args eqs =

530

List.fold_right (fun eq args > translate_eq node args eq) eqs args;;

531


532

let translate_decl nd sch =

533

(*Log.report ~level:1 (fun fmt > Printers.pp_node fmt nd);*)

534


535

let sorted_eqs = sort_equations_from_schedule nd sch in

536

let constant_eqs = constant_equations nd in

537


538

let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l > ISet.add l) nd.node_locals ISet.empty, [] in

539

(* memories, init instructions, node calls, local variables (including memories), step instrs *)

540

let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in

541

assert (ISet.is_empty m0);

542

assert (init0 = []);

543

assert (Utils.IMap.is_empty j0);

544

let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, []) sorted_eqs in

545

let mmap = Utils.IMap.fold (fun i n res > (i, n)::res) j [] in

546

{

547

mname = nd;

548

mmemory = ISet.elements m;

549

mcalls = mmap;

550

minstances = List.filter (fun (_, (n,_)) > not (Stateless.check_node n)) mmap;

551

minit = init;

552

mconst = s0;

553

mstatic = List.filter (fun v > v.var_dec_const) nd.node_inputs;

554

mstep = {

555

step_inputs = nd.node_inputs;

556

step_outputs = nd.node_outputs;

557

step_locals = ISet.elements (ISet.diff locals m);

558

step_checks = List.map (fun d > d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks;

559

step_instrs = (

560

(* special treatment depending on the active backend. For horn backend,

561

common branches are not merged while they are in C or Java

562

backends. *)

563

(*match !Options.output with

564

 "horn" > s

565

 "C"  "java"  _ >*) join_guards_list s

566

);

567

step_asserts =

568

let exprl = List.map (fun assert_ > assert_.assert_expr ) nd.node_asserts in

569

List.map (translate_expr nd init_args) exprl

570

;

571

};

572

mspec = nd.node_spec;

573

mannot = nd.node_annot;

574

}

575


576

(** takes the global declarations and the scheduling associated to each node *)

577

let translate_prog decls node_schs =

578

let nodes = get_nodes decls in

579

List.map

580

(fun decl >

581

let node = node_of_top decl in

582

let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in

583

translate_decl node sch

584

) nodes

585


586

let get_machine_opt name machines =

587

List.fold_left

588

(fun res m >

589

match res with

590

 Some _ > res

591

 None > if m.mname.node_id = name then Some m else None)

592

None machines

593


594

let get_const_assign m id =

595

try

596

match (List.find (fun instr > match instr with MLocalAssign (v, _) > v == id  _ > false) m.mconst) with

597

 MLocalAssign (_, e) > e

598

 _ > assert false

599

with Not_found > assert false

600


601


602

let value_of_ident loc m id =

603

(* is is a state var *)

604

try

605

let v = List.find (fun v > v.var_id = id) m.mmemory

606

in mk_val (StateVar v) v.var_type

607

with Not_found >

608

try (* id is a node var *)

609

let v = get_node_var id m.mname

610

in mk_val (LocalVar v) v.var_type

611

with Not_found >

612

try (* id is a constant *)

613

let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))

614

in mk_val (LocalVar c) c.var_type

615

with Not_found >

616

(* id is a tag *)

617

let t = Const_tag id

618

in mk_val (Cst t) (Typing.type_const loc t)

619


620

(* type of internal fun used in dimension expression *)

621

let type_of_value_appl f args =

622

if List.mem f Basic_library.arith_funs

623

then (List.hd args).value_type

624

else Type_predef.type_bool

625


626

let rec value_of_dimension m dim =

627

match dim.Dimension.dim_desc with

628

 Dimension.Dbool b >

629

mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool

630

 Dimension.Dint i >

631

mk_val (Cst (Const_int i)) Type_predef.type_int

632

 Dimension.Dident v > value_of_ident dim.Dimension.dim_loc m v

633

 Dimension.Dappl (f, args) >

634

let vargs = List.map (value_of_dimension m) args

635

in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs)

636

 Dimension.Dite (i, t, e) >

637

(match List.map (value_of_dimension m) [i; t; e] with

638

 [vi; vt; ve] > mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type

639

 _ > assert false)

640

 Dimension.Dlink dim' > value_of_dimension m dim'

641

 _ > assert false

642


643

let rec dimension_of_value value =

644

match value.value_desc with

645

 Cst (Const_tag t) when t = Corelang.tag_true > Dimension.mkdim_bool Location.dummy_loc true

646

 Cst (Const_tag t) when t = Corelang.tag_false > Dimension.mkdim_bool Location.dummy_loc false

647

 Cst (Const_int i) > Dimension.mkdim_int Location.dummy_loc i

648

 LocalVar v > Dimension.mkdim_ident Location.dummy_loc v.var_id

649

 Fun (f, args) > Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args)

650

 _ > assert false

651


652

(* Local Variables: *)

653

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

654

(* End: *)
