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


23

module ISet = Set.Make(OrdVarDecl)

24


25


26

let rec pp_val fmt v =

27

match v.value_desc with

28

 Cst c > Printers.pp_const fmt c

29

 LocalVar v > Format.pp_print_string fmt v.var_id

30

 StateVar v > Format.pp_print_string fmt v.var_id

31

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

32

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

33

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

34

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

35


36

let rec pp_instr fmt i =

37

match i with

38

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

39

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

40

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

41

 MNoReset i > ()

42

 MStep (il, i, vl) >

43

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

44

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

45

i

46

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

47

 MBranch (g,hl) >

48

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

49

pp_val g

50

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

51

 MComment s > Format.pp_print_string fmt s

52


53

and pp_branch fmt (t, h) =

54

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

55


56

and pp_instrs fmt il =

57

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

58


59

type step_t = {

60

step_checks: (Location.t * value_t) list;

61

step_inputs: var_decl list;

62

step_outputs: var_decl list;

63

step_locals: var_decl list;

64

step_instrs: instr_t list;

65

step_asserts: value_t list;

66

}

67


68

type static_call = top_decl * (Dimension.dim_expr list)

69


70

type machine_t = {

71

mname: node_desc;

72

mmemory: var_decl list;

73

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

74

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

75

minit: instr_t list;

76

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

77

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

78

mstep: step_t;

79

mspec: node_annot option;

80

mannot: expr_annot list;

81

}

82


83

let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory

84


85

let pp_step fmt s =

86

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

87

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

88

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

89

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

90

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

91

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

92

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

93


94


95

let pp_static_call fmt (node, args) =

96

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

97

(node_name node)

98

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

99


100

let pp_machine fmt m =

101

Format.fprintf fmt

102

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

103

m.mname.node_id

104

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

105

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

106

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

107

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

108

pp_step m.mstep

109

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

110

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

111


112

let rec is_const_value v =

113

match v.value_desc with

114

 Cst _ > true

115

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

116

 _ > false

117


118

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

119

let get_stateless_status m =

120

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

121


122

let is_input m id =

123

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

124


125

let is_output m id =

126

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

127


128

let is_memory m id =

129

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

130


131

let conditional c t e =

132

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

133


134

let dummy_var_decl name typ =

135

{

136

var_id = name;

137

var_orig = false;

138

var_dec_type = dummy_type_dec;

139

var_dec_clock = dummy_clock_dec;

140

var_dec_const = false;

141

var_dec_value = None;

142

var_type = typ;

143

var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true;

144

var_loc = Location.dummy_loc

145

}

146


147

let arrow_id = "_arrow"

148


149

let arrow_typ = Types.new_ty Types.Tunivar

150


151

let arrow_desc =

152

{

153

node_id = arrow_id;

154

node_type = Type_predef.type_bin_poly_op;

155

node_clock = Clock_predef.ck_bin_univ;

156

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

157

node_outputs= [dummy_var_decl "_out" arrow_typ];

158

node_locals= [];

159

node_gencalls = [];

160

node_checks = [];

161

node_asserts = [];

162

node_stmts= [];

163

node_dec_stateless = false;

164

node_stateless = Some false;

165

node_spec = None;

166

node_annot = []; }

167


168

let arrow_top_decl =

169

{

170

top_decl_desc = Node arrow_desc;

171

top_decl_owner = Version.include_path;

172

top_decl_itf = false;

173

top_decl_loc = Location.dummy_loc

174

}

175


176

let mk_val v t = { value_desc = v;

177

value_type = t;

178

value_annot = None }

179


180

let arrow_machine =

181

let state = "_first" in

182

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

183

let var_input1 = List.nth arrow_desc.node_inputs 0 in

184

let var_input2 = List.nth arrow_desc.node_inputs 1 in

185

let var_output = List.nth arrow_desc.node_outputs 0 in

186

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

187

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

188

{

189

mname = arrow_desc;

190

mmemory = [var_state];

191

mcalls = [];

192

minstances = [];

193

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

194

mconst = [];

195

mstatic = [];

196

mstep = {

197

step_inputs = arrow_desc.node_inputs;

198

step_outputs = arrow_desc.node_outputs;

199

step_locals = [];

200

step_checks = [];

201

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

202

[MStateAssign(var_state, cst false);

203

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

204

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

205

step_asserts = [];

206

};

207

mspec = None;

208

mannot = [];

209

}

210


211

let new_instance =

212

let cpt = ref (1) in

213

fun caller callee tag >

214

begin

215

let o =

216

if Stateless.check_node callee then

217

node_name callee

218

else

219

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

220

let o =

221

if !Options.ansi && is_generic_node callee

222

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

223

else o in

224

o

225

end

226


227

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

228

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

229

(* si : initialization instructions *)

230

(* j : node aka machine instances *)

231

(* d : local variables *)

232

(* s : step instructions *)

233

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

234

try (* id is a node var *)

235

let var_id = get_node_var id node in

236

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

237

then mk_val (StateVar var_id) var_id.var_type

238

else mk_val (LocalVar var_id) var_id.var_type

239

with Not_found >

240

try (* id is a constant *)

241

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

242

mk_val (LocalVar vdecl) vdecl.var_type

243

with Not_found >

244

(* id is a tag *)

245

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

246

qui contient id *)

247

let cst = Const_tag id in

248

mk_val (Cst cst) (Typing.type_const Location.dummy_loc cst)

249


250

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

251

match (Clocks.repr ck).cdesc with

252

 Con (ck1, cr, l) >

253

let id = Clocks.const_of_carrier cr in

254

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

255

[l, [inst]] ))

256

 _ > inst

257


258

let rec join_branches hl1 hl2 =

259

match hl1, hl2 with

260

 [] , _ > hl2

261

 _ , [] > hl1

262

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

263

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

264

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

265

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

266


267

and join_guards inst1 insts2 =

268

match inst1, insts2 with

269

 _ , [] >

270

[inst1]

271

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

272

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

273

:: q

274

 _ > inst1 :: insts2

275


276

let join_guards_list insts =

277

List.fold_right join_guards insts []

278


279

(* specialize predefined (polymorphic) operators

280

wrt their instances, so that the C semantics

281

is preserved *)

282

let specialize_to_c expr =

283

match expr.expr_desc with

284

 Expr_appl (id, e, r) >

285

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

286

then let id =

287

match id with

288

 "=" > "equi"

289

 "!=" > "xor"

290

 _ > id in

291

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

292

else expr

293

 _ > expr

294


295

let specialize_op expr =

296

match !Options.output with

297

 "C" > specialize_to_c expr

298

 _ > expr

299


300

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

301

let expr = specialize_op expr in

302

let value_desc =

303

match expr.expr_desc with

304

 Expr_const v > Cst v

305

 Expr_ident x > (translate_ident node args x).value_desc

306

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

307

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

308

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

309

 Expr_tuple _

310

 Expr_arrow _

311

 Expr_fby _

312

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

313

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

314

 Expr_merge (x, _) > raise NormalizationError

315

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

316

let nd = node_from_name id in

317

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

318

 Expr_ite (g,t,e) > (

319

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

320

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

321

backends. *)

322

match !Options.output with

323

 "horn" >

324

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

325

 "C"  "java"  _ >

326

(Format.eprintf "Normalization error for backend %s: %a@."

327

!Options.output

328

Printers.pp_expr expr;

329

raise NormalizationError)

330

)

331

 _ > raise NormalizationError

332

in

333

mk_val value_desc expr.expr_type

334


335

let translate_guard node args expr =

336

match expr.expr_desc with

337

 Expr_ident x > translate_ident node args x

338

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

339


340

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

341

match expr.expr_desc with

342

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

343

conditional g [translate_act node args (y, t)]

344

[translate_act node args (y, e)]

345

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

346

 _ > MLocalAssign (y, translate_expr node args expr)

347


348

let reset_instance node args i r c =

349

match r with

350

 None > []

351

 Some r > let g = translate_guard node args r in

352

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

353


354

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

355

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

356

match eq.eq_lhs, eq.eq_rhs.expr_desc with

357

 [x], Expr_arrow (e1, e2) >

358

let var_x = get_node_var x node in

359

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

360

let c1 = translate_expr node args e1 in

361

let c2 = translate_expr node args e2 in

362

(m,

363

MReset o :: si,

364

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

365

d,

366

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

367

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

368

let var_x = get_node_var x node in

369

(ISet.add var_x m,

370

si,

371

j,

372

d,

373

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

374

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

375

let var_x = get_node_var x node in

376

(ISet.add var_x m,

377

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

378

j,

379

d,

380

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

381


382

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

383

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

384

let el = expr_list_of_expr arg in

385

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

386

let node_f = node_from_name f in

387

let call_f =

388

node_f,

389

NodeDep.filter_static_inputs (node_inputs node_f) el in

390

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

391

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

392

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

393

(*Clocks.new_var true in

394

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

395

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;*)

396

(m,

397

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

398

Utils.IMap.add o call_f j,

399

d,

400

(if Stateless.check_node node_f

401

then []

402

else reset_instance node args o r call_ck) @

403

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

404


405

 [x], _ > (

406

let var_x = get_node_var x node in

407

(m, si, j, d,

408

control_on_clock

409

node

410

args

411

eq.eq_rhs.expr_clock

412

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

413

)

414

)

415

 _ >

416

begin

417

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

418

assert false

419

end

420


421

let find_eq xl eqs =

422

let rec aux accu eqs =

423

match eqs with

424

 [] >

425

begin

426

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

427

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

428

Printers.pp_node_eqs eqs;

429

assert false

430

end

431

 hd::tl >

432

if List.exists (fun x > List.mem x hd.eq_lhs) xl then

433

hd, accu@tl

434

else

435

aux (hd::accu) tl

436

in

437

aux [] eqs

438


439

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

440

to the computed schedule [sch]

441

*)

442

let sort_equations_from_schedule nd sch =

443

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

444

(* nd.node_id *)

445

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

446

let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in

447

let eqs_rev, remainder =

448

List.fold_left

449

(fun (accu, node_eqs_remainder) vl >

450

if List.exists

451

(fun eq > (* This could be also evaluated with a forall.

452

But, by construction, each vl should be

453

associated to a single equation *)

454

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

455

accu

456

then

457

(accu, node_eqs_remainder)

458

else

459

let eq_v, remainder = find_eq vl node_eqs_remainder in

460

eq_v::accu, remainder

461

)

462

([], split_eqs)

463

sch

464

in

465

begin

466

if List.length remainder > 0 then (

467

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

468

Printers.pp_node_eqs remainder

469

Printers.pp_node_eqs (get_node_eqs nd);

470

assert false);

471

let res = List.rev eqs_rev in

472

(* (\* Debug code, to be removed *\) *)

473

(* List.iteri (fun cpt eq > Format.eprintf "Eq %i: %a@." cpt (Utils.fprintf_list ~sep:", " Format.pp_print_string) eq.eq_lhs) res; *)

474

res

475

end

476


477

let constant_equations nd =

478

List.fold_right (fun vdecl eqs >

479

if vdecl.var_dec_const

480

then

481

{ eq_lhs = [vdecl.var_id];

482

eq_rhs = Utils.desome vdecl.var_dec_value;

483

eq_loc = vdecl.var_loc

484

} :: eqs

485

else eqs)

486

nd.node_locals []

487


488

let translate_eqs node args eqs =

489

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

490


491

let translate_decl nd sch =

492

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

493


494

let sorted_eqs = sort_equations_from_schedule nd sch in

495

let constant_eqs = constant_equations nd in

496


497

(* In case of non functional backend (eg. C), additional local variables have

498

to be declared for each assert *)

499

let new_locals, assert_instrs, nd_node_asserts =

500

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

501

if Corelang.functional_backend () then

502

[], [], exprl

503

else (* Each assert(e) is associated to a fresh variable v and declared as

504

v=e; assert (v); *)

505

let _, vars, eql, assertl =

506

List.fold_left (fun (i, vars, eqlist, assertlist) expr >

507

let loc = expr.expr_loc in

508

let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in

509

let assert_var =

510

mkvar_decl

511

loc

512

~orig:false (* fresh var *)

513

(var_id,

514

mktyp loc Tydec_bool,

515

mkclock loc Ckdec_any,

516

false, (* not a constant *)

517

None (* no default value *)

518

)

519

in

520

assert_var.var_type < Types.new_ty (Types.Tbool);

521

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

522

(i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist)

523

) (1, [], [], []) exprl

524

in

525

vars, eql, assertl

526

in

527

let locals_list = nd.node_locals @ new_locals in

528


529

let nd = { nd with node_locals = locals_list } in

530

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

531

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

532

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

533

assert (ISet.is_empty m0);

534

assert (init0 = []);

535

assert (Utils.IMap.is_empty j0);

536

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

537

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

538

{

539

mname = nd;

540

mmemory = ISet.elements m;

541

mcalls = mmap;

542

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

543

minit = init;

544

mconst = s0;

545

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

546

mstep = {

547

step_inputs = nd.node_inputs;

548

step_outputs = nd.node_outputs;

549

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

550

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

551

step_instrs = (

552

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

553

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

554

backends. *)

555

match !Options.output with

556

(*  "horn" > s TODO 16/12 *)

557

 "C"  "java"  _ > join_guards_list s

558

);

559

step_asserts = List.map (translate_expr nd init_args) nd_node_asserts;

560

};

561

mspec = nd.node_spec;

562

mannot = nd.node_annot;

563

}

564


565

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

566

let translate_prog decls node_schs =

567

let nodes = get_nodes decls in

568

List.map

569

(fun decl >

570

let node = node_of_top decl in

571

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

572

translate_decl node sch

573

) nodes

574


575

let get_machine_opt name machines =

576

List.fold_left

577

(fun res m >

578

match res with

579

 Some _ > res

580

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

581

None machines

582


583

let get_const_assign m id =

584

try

585

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

586

 MLocalAssign (_, e) > e

587

 _ > assert false

588

with Not_found > assert false

589


590


591

let value_of_ident m id =

592

(* is is a state var *)

593

try

594

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

595

mk_val (StateVar mem) mem.var_type

596

with Not_found >

597

try (* id is a node var *)

598

let var = get_node_var id m.mname in

599

mk_val (LocalVar var) var.var_type

600

with Not_found >

601

try (* id is a constant *)

602

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

603

mk_val (LocalVar cst) cst.var_type

604

with Not_found >

605

(* id is a tag *)

606

let tag = Const_tag id in

607

mk_val (Cst tag) (Typing.type_const Location.dummy_loc tag)

608


609

let rec value_of_dimension m dim =

610

match dim.Dimension.dim_desc with

611

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

612

 Dimension.Dint i > mk_val (Cst (Const_int i)) Type_predef.type_int

613

 Dimension.Dident v > value_of_ident m v

614

 Dimension.Dappl (f, args) > let typ = if Basic_library.is_numeric_operator f then Type_predef.type_int else Type_predef.type_bool

615

in mk_val (Fun (f, List.map (value_of_dimension m) args)) typ

616

 Dimension.Dite (i, t, e) > (

617

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

618

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

619

 _ > assert false (* could not happen *)

620

)

621

 Dimension.Dlink dim' > value_of_dimension m dim'

622

 _ > assert false

623


624

let rec dimension_of_value value =

625

match value.value_desc with

626

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

627

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

628

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

629

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

630

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

631

 _ > assert false

632


633

(* Local Variables: *)

634

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

635

(* End: *)
