1

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

2

(* *)

3

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

4

(* Copyright 2012   ONERA  CNRS  INPT  LIFL *)

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

(* This file was originally from the Prelude compiler *)

11

(* *)

12

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

13


14


15

(** Main clockcalculus module. Based on type inference algorithms with

16

destructive unification. Uses a bit of subtyping for periodic clocks. *)

17


18

(* Though it shares similarities with the typing module, no code

19

is shared. Simple environments, very limited identifier scoping, no

20

identifier redefinition allowed. *)

21

open Utils

22

open LustreSpec

23

open Corelang

24

open Clocks

25

open Format

26


27

let loc_of_cond loc_containing id =

28

let pos_start =

29

{loc_containing.Location.loc_end with

30

Lexing.pos_cnum=loc_containing.Location.loc_end.Lexing.pos_cnum(String.length id)}

31

in

32

{Location.loc_start = pos_start;

33

Location.loc_end = loc_containing.Location.loc_end}

34


35

(** [occurs cvar ck] returns true if the clock variable [cvar] occurs in

36

clock [ck]. False otherwise. *)

37

let rec occurs cvar ck =

38

let ck = repr ck in

39

match ck.cdesc with

40

 Carrow (ck1, ck2) >

41

(occurs cvar ck1)  (occurs cvar ck2)

42

 Ctuple ckl >

43

List.exists (occurs cvar) ckl

44

 Con (ck',_,_) > occurs cvar ck'

45

 Cvar > ck=cvar

46

 Cunivar > false

47

 Clink ck' > occurs cvar ck'

48

 Ccarrying (_,ck') > occurs cvar ck'

49


50

(* Clocks generalization *)

51

let rec generalize_carrier cr =

52

match cr.carrier_desc with

53

 Carry_const _

54

 Carry_name >

55

if cr.carrier_scoped then

56

raise (Scope_carrier cr);

57

cr.carrier_desc < Carry_var

58

 Carry_var > ()

59

 Carry_link cr' > generalize_carrier cr'

60


61

(** Promote monomorphic clock variables to polymorphic clock variables. *)

62

(* Generalize by sideeffects *)

63

let rec generalize ck =

64

match ck.cdesc with

65

 Carrow (ck1,ck2) >

66

generalize ck1; generalize ck2

67

 Ctuple clist >

68

List.iter generalize clist

69

 Con (ck',cr,_) > generalize ck'; generalize_carrier cr

70

 Cvar >

71

if ck.cscoped then

72

raise (Scope_clock ck);

73

ck.cdesc < Cunivar

74

 Cunivar > ()

75

 Clink ck' >

76

generalize ck'

77

 Ccarrying (cr,ck') >

78

generalize_carrier cr; generalize ck'

79


80

let try_generalize ck_node loc =

81

try

82

generalize ck_node

83

with (Scope_carrier cr) >

84

raise (Error (loc, Carrier_extrusion (ck_node, cr)))

85

 (Scope_clock ck) >

86

raise (Error (loc, Clock_extrusion (ck_node, ck)))

87


88

(* Clocks instanciation *)

89

let instantiate_carrier cr inst_cr_vars =

90

let cr = carrier_repr cr in

91

match cr.carrier_desc with

92

 Carry_const _

93

 Carry_name > cr

94

 Carry_link _ >

95

failwith "Internal error"

96

 Carry_var >

97

try

98

List.assoc cr.carrier_id !inst_cr_vars

99

with Not_found >

100

let cr_var = new_carrier Carry_name true in

101

inst_cr_vars := (cr.carrier_id,cr_var)::!inst_cr_vars;

102

cr_var

103


104

(** Downgrade polymorphic clock variables to monomorphic clock variables *)

105

(* inst_ck_vars ensures that a polymorphic variable is instanciated with

106

the same monomorphic variable if it occurs several times in the same

107

type. inst_cr_vars is the same for carriers. *)

108

let rec instantiate inst_ck_vars inst_cr_vars ck =

109

match ck.cdesc with

110

 Carrow (ck1,ck2) >

111

{ck with cdesc =

112

Carrow ((instantiate inst_ck_vars inst_cr_vars ck1),

113

(instantiate inst_ck_vars inst_cr_vars ck2))}

114

 Ctuple cklist >

115

{ck with cdesc = Ctuple

116

(List.map (instantiate inst_ck_vars inst_cr_vars) cklist)}

117

 Con (ck',c,l) >

118

let c' = instantiate_carrier c inst_cr_vars in

119

{ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)}

120

 Cvar > ck

121

 Clink ck' >

122

{ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')}

123

 Ccarrying (cr,ck') >

124

let cr' = instantiate_carrier cr inst_cr_vars in

125

{ck with cdesc =

126

Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')}

127

 Cunivar >

128

try

129

List.assoc ck.cid !inst_ck_vars

130

with Not_found >

131

let var = new_ck Cvar true in

132

inst_ck_vars := (ck.cid, var)::!inst_ck_vars;

133

var

134


135


136

let rec update_scope_carrier scoped cr =

137

if (not scoped) then

138

begin

139

cr.carrier_scoped < scoped;

140

match cr.carrier_desc with

141

 Carry_const _  Carry_name  Carry_var > ()

142

 Carry_link cr' > update_scope_carrier scoped cr'

143

end

144


145

let rec update_scope scoped ck =

146

if (not scoped) then

147

begin

148

ck.cscoped < scoped;

149

match ck.cdesc with

150

 Carrow (ck1,ck2) >

151

update_scope scoped ck1; update_scope scoped ck2

152

 Ctuple clist >

153

List.iter (update_scope scoped) clist

154

 Con (ck',cr,_) > update_scope scoped ck'(*; update_scope_carrier scoped cr*)

155

 Cvar  Cunivar > ()

156

 Clink ck' >

157

update_scope scoped ck'

158

 Ccarrying (cr,ck') >

159

update_scope_carrier scoped cr; update_scope scoped ck'

160

end

161


162


163

(* Unifies two clock carriers *)

164

let unify_carrier cr1 cr2 =

165

let cr1 = carrier_repr cr1 in

166

let cr2 = carrier_repr cr2 in

167

if cr1==cr2 then ()

168

else

169

match cr1.carrier_desc, cr2.carrier_desc with

170

 Carry_const id1, Carry_const id2 >

171

if id1 <> id2 then raise (Mismatch (cr1, cr2))

172

 Carry_const _, Carry_name >

173

begin

174

cr2.carrier_desc < Carry_link cr1;

175

update_scope_carrier cr2.carrier_scoped cr1

176

end

177

 Carry_name, Carry_const _ >

178

begin

179

cr1.carrier_desc < Carry_link cr2;

180

update_scope_carrier cr1.carrier_scoped cr2

181

end

182

 Carry_name, Carry_name >

183

if cr1.carrier_id < cr2.carrier_id then

184

begin

185

cr2.carrier_desc < Carry_link cr1;

186

update_scope_carrier cr2.carrier_scoped cr1

187

end

188

else

189

begin

190

cr1.carrier_desc < Carry_link cr2;

191

update_scope_carrier cr1.carrier_scoped cr2

192

end

193

 _,_ > assert false

194


195

(* Semiunifies two clock carriers *)

196

let semi_unify_carrier cr1 cr2 =

197

let cr1 = carrier_repr cr1 in

198

let cr2 = carrier_repr cr2 in

199

if cr1==cr2 then ()

200

else

201

match cr1.carrier_desc, cr2.carrier_desc with

202

 Carry_const id1, Carry_const id2 >

203

if id1 <> id2 then raise (Mismatch (cr1, cr2))

204

 Carry_const _, Carry_name >

205

begin

206

cr2.carrier_desc < Carry_link cr1;

207

update_scope_carrier cr2.carrier_scoped cr1

208

end

209

 Carry_name, Carry_const _ > raise (Mismatch (cr1, cr2))

210

 Carry_name, Carry_name >

211

if cr1.carrier_id < cr2.carrier_id then

212

begin

213

cr2.carrier_desc < Carry_link cr1;

214

update_scope_carrier cr2.carrier_scoped cr1

215

end

216

else

217

begin

218

cr1.carrier_desc < Carry_link cr2;

219

update_scope_carrier cr1.carrier_scoped cr2

220

end

221

 _,_ > assert false

222


223

let try_unify_carrier ck1 ck2 loc =

224

try

225

unify_carrier ck1 ck2

226

with

227

 Unify (ck1',ck2') >

228

raise (Error (loc, Clock_clash (ck1',ck2')))

229

 Mismatch (cr1,cr2) >

230

raise (Error (loc, Carrier_mismatch (cr1,cr2)))

231


232

(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify

233

(ck1,ck2)] if the clocks are not unifiable.*)

234

let rec unify ck1 ck2 =

235

let ck1 = repr ck1 in

236

let ck2 = repr ck2 in

237

if ck1==ck2 then

238

()

239

else

240

match ck1.cdesc,ck2.cdesc with

241

 Cvar, Cvar >

242

if ck1.cid < ck2.cid then

243

begin

244

ck2.cdesc < Clink (simplify ck1);

245

update_scope ck2.cscoped ck1

246

end

247

else

248

begin

249

ck1.cdesc < Clink (simplify ck2);

250

update_scope ck1.cscoped ck2

251

end

252

 (Cvar, _) when (not (occurs ck1 ck2)) >

253

update_scope ck1.cscoped ck2;

254

ck1.cdesc < Clink (simplify ck2)

255

 (_, Cvar) when (not (occurs ck2 ck1)) >

256

update_scope ck2.cscoped ck1;

257

ck2.cdesc < Clink (simplify ck1)

258

 Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') >

259

unify_carrier cr1 cr2;

260

unify ck1' ck2'

261

 Ccarrying (_,_),_  _,Ccarrying (_,_) >

262

raise (Unify (ck1,ck2))

263

 Carrow (c1,c2), Carrow (c1',c2') >

264

unify c1 c1'; unify c2 c2'

265

 Ctuple ckl1, Ctuple ckl2 >

266

if (List.length ckl1) <> (List.length ckl2) then

267

raise (Unify (ck1,ck2));

268

List.iter2 unify ckl1 ckl2

269

 Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 >

270

unify_carrier c1 c2;

271

unify ck' ck''

272

 Cunivar, _  _, Cunivar > ()

273

 _,_ > raise (Unify (ck1,ck2))

274


275

(** [unify ck1 ck2] semiunifies clocks [ck1] and [ck2]. Raises [Unify

276

(ck1,ck2)] if the clocks are not semiunifiable.*)

277

let rec semi_unify ck1 ck2 =

278

let ck1 = repr ck1 in

279

let ck2 = repr ck2 in

280

if ck1==ck2 then

281

()

282

else

283

match ck1.cdesc,ck2.cdesc with

284

 Cvar, Cvar >

285

if ck1.cid < ck2.cid then

286

begin

287

ck2.cdesc < Clink (simplify ck1);

288

update_scope ck2.cscoped ck1

289

end

290

else

291

begin

292

ck1.cdesc < Clink (simplify ck2);

293

update_scope ck1.cscoped ck2

294

end

295

 (Cvar, _) > raise (Unify (ck1,ck2))

296

 (_, Cvar) when (not (occurs ck2 ck1)) >

297

update_scope ck2.cscoped ck1;

298

ck2.cdesc < Clink (simplify ck1)

299

 Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') >

300

semi_unify_carrier cr1 cr2;

301

semi_unify ck1' ck2'

302

 Ccarrying (_,_),_  _,Ccarrying (_,_) >

303

raise (Unify (ck1,ck2))

304

 Carrow (c1,c2), Carrow (c1',c2') >

305

begin

306

semi_unify c1 c1';

307

semi_unify c2 c2'

308

end

309

 Ctuple ckl1, Ctuple ckl2 >

310

if (List.length ckl1) <> (List.length ckl2) then

311

raise (Unify (ck1,ck2));

312

List.iter2 semi_unify ckl1 ckl2

313

 Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 >

314

semi_unify_carrier c1 c2;

315

semi_unify ck' ck''

316

 Cunivar, _  _, Cunivar > ()

317

 _,_ > raise (Unify (ck1,ck2))

318


319

(* Returns the value corresponding to a pclock (integer) factor

320

expression. Expects a constant expression (checked by typing). *)

321

let int_factor_of_expr e =

322

match e.expr_desc with

323

 Expr_const

324

(Const_int i) > i

325

 _ > failwith "Internal error: int_factor_of_expr"

326


327

(** [clock_uncarry ck] drops the possible carrier(s) name(s) from clock [ck] *)

328

let rec clock_uncarry ck =

329

let ck = repr ck in

330

match ck.cdesc with

331

 Ccarrying (_, ck') > ck'

332

 Con(ck', cr, l) > clock_on (clock_uncarry ck') cr l

333

 Ctuple ckl > clock_of_clock_list (List.map clock_uncarry ckl)

334

 _ > ck

335


336

let try_unify ck1 ck2 loc =

337

try

338

unify ck1 ck2

339

with

340

 Unify (ck1',ck2') >

341

raise (Error (loc, Clock_clash (ck1',ck2')))

342

 Mismatch (cr1,cr2) >

343

raise (Error (loc, Carrier_mismatch (cr1,cr2)))

344


345

let try_semi_unify ck1 ck2 loc =

346

try

347

semi_unify ck1 ck2

348

with

349

 Unify (ck1',ck2') >

350

raise (Error (loc, Clock_clash (ck1',ck2')))

351

 Mismatch (cr1,cr2) >

352

raise (Error (loc, Carrier_mismatch (cr1,cr2)))

353


354

(* ck2 is a subtype of ck1 *)

355

let rec sub_unify sub ck1 ck2 =

356

match (repr ck1).cdesc, (repr ck2).cdesc with

357

 Ctuple cl1 , Ctuple cl2 >

358

if List.length cl1 <> List.length cl2

359

then raise (Unify (ck1, ck2))

360

else List.iter2 (sub_unify sub) cl1 cl2

361

 Ctuple [c1] , _ > sub_unify sub c1 ck2

362

 _ , Ctuple [c2] > sub_unify sub ck1 c2

363

 Con (c1, cr1, t1) , Con (c2, cr2, t2) when t1=t2 >

364

begin

365

unify_carrier cr1 cr2;

366

sub_unify sub c1 c2

367

end

368

 Ccarrying (cr1, c1), Ccarrying (cr2, c2)>

369

begin

370

unify_carrier cr1 cr2;

371

sub_unify sub c1 c2

372

end

373

 _, Ccarrying (_, c2) when sub > sub_unify sub ck1 c2

374

 _ > unify ck1 ck2

375


376

let try_sub_unify sub ck1 ck2 loc =

377

try

378

sub_unify sub ck1 ck2

379

with

380

 Unify (ck1',ck2') >

381

raise (Error (loc, Clock_clash (ck1',ck2')))

382

 Mismatch (cr1,cr2) >

383

raise (Error (loc, Carrier_mismatch (cr1,cr2)))

384


385

(* Unifies all the clock variables in the clock type of a tuple

386

expression, so that the clock type only uses at most one clock variable *)

387

let unify_tuple_clock ref_ck_opt ck loc =

388

(*(match ref_ck_opt with

389

 None > Format.eprintf "unify_tuple_clock None %a@." Clocks.print_ck ck

390

 Some ck' > Format.eprintf "unify_tuple_clock (Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*)

391

let ck_var = ref ref_ck_opt in

392

let rec aux ck =

393

match (repr ck).cdesc with

394

 Con _

395

 Cvar >

396

begin

397

match !ck_var with

398

 None >

399

ck_var:=Some ck

400

 Some v >

401

(* may fail *)

402

try_unify ck v loc

403

end

404

 Ctuple cl >

405

List.iter aux cl

406

 Carrow _ > assert false (* should not occur *)

407

 Ccarrying (_, ck1) >

408

aux ck1

409

 _ > ()

410

in aux ck

411


412

(* Unifies all the clock variables in the clock type of an imported

413

node, so that the clock type only uses at most one base clock variable,

414

that is, the activation clock of the node *)

415

let unify_imported_clock ref_ck_opt ck loc =

416

let ck_var = ref ref_ck_opt in

417

let rec aux ck =

418

match (repr ck).cdesc with

419

 Cvar >

420

begin

421

match !ck_var with

422

 None >

423

ck_var:=Some ck

424

 Some v >

425

(* cannot fail *)

426

try_unify ck v loc

427

end

428

 Ctuple cl >

429

List.iter aux cl

430

 Carrow (ck1,ck2) >

431

aux ck1; aux ck2

432

 Ccarrying (_, ck1) >

433

aux ck1

434

 Con (ck1, _, _) > aux ck1

435

 _ > ()

436

in

437

aux ck

438


439

(* Computes the root clock of a tuple or a node clock,

440

which is not the same as the base clock.

441

Root clock will be used as the call clock

442

of a given node instance *)

443

let compute_root_clock ck =

444

let root = Clocks.root ck in

445

let branch = ref None in

446

let rec aux ck =

447

match (repr ck).cdesc with

448

 Ctuple cl >

449

List.iter aux cl

450

 Carrow (ck1,ck2) >

451

aux ck1; aux ck2

452

 _ >

453

begin

454

match !branch with

455

 None >

456

branch := Some (Clocks.branch ck)

457

 Some br >

458

(* cannot fail *)

459

branch := Some (Clocks.common_prefix br (Clocks.branch ck))

460

end

461

in

462

begin

463

aux ck;

464

Clocks.clock_of_root_branch root (Utils.desome !branch)

465

end

466


467

(* Clocks a list of arguments of Lustre builtin operators:

468

 type each expression, remove carriers of clocks as

469

carriers may only denote variables, not arbitrary expr.

470

 try to unify these clocks altogether

471

*)

472

let rec clock_standard_args env expr_list =

473

let ck_list = List.map (fun e > clock_uncarry (clock_expr env e)) expr_list in

474

let ck_res = new_var true in

475

List.iter2 (fun e ck > try_unify ck ck_res e.expr_loc) expr_list ck_list;

476

ck_res

477


478

(* emulates a subtyping relation between clocks c and (cr : c),

479

used during node application only *)

480

and clock_subtyping_arg env ?(sub=true) real_arg formal_clock =

481

let loc = real_arg.expr_loc in

482

let real_clock = clock_expr env real_arg in

483

try_sub_unify sub formal_clock real_clock loc

484


485

(* computes clocks for node application *)

486

and clock_appl env f args clock_reset loc =

487

let args = expr_list_of_expr args in

488

if Basic_library.is_homomorphic_fun f && List.exists is_tuple_expr args

489

then

490

let args = Utils.transpose_list (List.map expr_list_of_expr args) in

491

Clocks.clock_of_clock_list (List.map (fun args > clock_call env f args clock_reset loc) args)

492

else

493

clock_call env f args clock_reset loc

494


495

and clock_call env f args clock_reset loc =

496

let cfun = clock_ident false env f loc in

497

let cins, couts = split_arrow cfun in

498

let cins = clock_list_of_clock cins in

499

List.iter2 (clock_subtyping_arg env) args cins;

500

unify_imported_clock (Some clock_reset) cfun loc;

501

couts

502


503

and clock_ident nocarrier env id loc =

504

clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)

505


506

and clock_carrier env c loc ce =

507

let expr_c = expr_of_ident c loc in

508

let ck = clock_expr ~nocarrier:false env expr_c in

509

let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in

510

let ckb = new_var true in

511

let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in

512

try_unify ck ckcarry expr_c.expr_loc;

513

unify_tuple_clock (Some ckb) ce expr_c.expr_loc;

514

cr

515


516

(** [clock_expr env expr] performs the clock calculus for expression [expr] in

517

environment [env] *)

518

and clock_expr ?(nocarrier=true) env expr =

519

let resulting_ck =

520

match expr.expr_desc with

521

 Expr_const cst >

522

let ck = new_var true in

523

expr.expr_clock < ck;

524

ck

525

 Expr_ident v >

526

let ckv =

527

try

528

Env.lookup_value env v

529

with Not_found >

530

failwith ("Internal error, variable \""^v^"\" not found")

531

in

532

let ck = instantiate (ref []) (ref []) ckv in

533

expr.expr_clock < ck;

534

ck

535

 Expr_array elist >

536

let ck = clock_standard_args env elist in

537

expr.expr_clock < ck;

538

ck

539

 Expr_access (e1, d) >

540

(* dimension, being a static value, doesn't need to be clocked *)

541

let ck = clock_standard_args env [e1] in

542

expr.expr_clock < ck;

543

ck

544

 Expr_power (e1, d) >

545

(* dimension, being a static value, doesn't need to be clocked *)

546

let ck = clock_standard_args env [e1] in

547

expr.expr_clock < ck;

548

ck

549

 Expr_tuple elist >

550

let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in

551

expr.expr_clock < ck;

552

ck

553

 Expr_ite (c, t, e) >

554

let ck_c = clock_standard_args env [c] in

555

let ck = clock_standard_args env [t; e] in

556

(* Here, the branches may exhibit a tuple clock, not the condition *)

557

unify_tuple_clock (Some ck_c) ck expr.expr_loc;

558

expr.expr_clock < ck;

559

ck

560

 Expr_appl (id, args, r) >

561

(try

562

(* for a modular compilation scheme, all inputs/outputs must share the same clock !

563

this is also the reset clock !

564

*)

565

let cr =

566

match r with

567

 None > new_var true

568

 Some c > clock_standard_args env [c] in

569

let couts = clock_appl env id args (clock_uncarry cr) expr.expr_loc in

570

expr.expr_clock < couts;

571

couts

572

with exn > (

573

Format.eprintf "Current expr: %a@." Printers.pp_expr expr;

574

raise exn

575

))

576

 Expr_fby (e1,e2)

577

 Expr_arrow (e1,e2) >

578

let ck = clock_standard_args env [e1; e2] in

579

unify_tuple_clock None ck expr.expr_loc;

580

expr.expr_clock < ck;

581

ck

582

 Expr_pre e > (* todo : deal with phases as in tail ? *)

583

let ck = clock_standard_args env [e] in

584

expr.expr_clock < ck;

585

ck

586

 Expr_when (e,c,l) >

587

let ce = clock_standard_args env [e] in

588

let c_loc = loc_of_cond expr.expr_loc c in

589

let cr = clock_carrier env c c_loc ce in

590

let ck = clock_on ce cr l in

591

let cr' = new_carrier (Carry_const c) ck.cscoped in

592

let ck' = clock_on ce cr' l in

593

expr.expr_clock < ck';

594

ck

595

 Expr_merge (c,hl) >

596

let cvar = new_var true in

597

let crvar = new_carrier Carry_name true in

598

List.iter (fun (t, h) > let ckh = clock_uncarry (clock_expr env h) in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;

599

let cr = clock_carrier env c expr.expr_loc cvar in

600

try_unify_carrier cr crvar expr.expr_loc;

601

let cres = clock_current ((snd (List.hd hl)).expr_clock) in

602

expr.expr_clock < cres;

603

cres

604

in

605

Log.report ~level:4 (fun fmt > Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck);

606

resulting_ck

607


608

let clock_of_vlist vars =

609

let ckl = List.map (fun v > v.var_clock) vars in

610

clock_of_clock_list ckl

611


612

(** [clock_eq env eq] performs the clockcalculus for equation [eq] in

613

environment [env] *)

614

let clock_eq env eq =

615

let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v > expr_of_ident v eq.eq_loc) eq.eq_lhs) in

616

let ck_rhs = clock_expr env eq.eq_rhs in

617

clock_subtyping_arg env expr_lhs ck_rhs

618


619

(* [clock_coreclock cck] returns the clock_expr corresponding to clock

620

declaration [cck] *)

621

let clock_coreclock env cck id loc scoped =

622

match cck.ck_dec_desc with

623

 Ckdec_any > new_var scoped

624

 Ckdec_bool cl >

625

let temp_env = Env.add_value env id (new_var true) in

626

(* We just want the id to be present in the environment *)

627

let dummy_id_expr = expr_of_ident id loc in

628

let when_expr =

629

List.fold_left

630

(fun expr (x,l) >

631

{expr_tag = new_tag ();

632

expr_desc = Expr_when (expr,x,l);

633

expr_type = Types.new_var ();

634

expr_clock = new_var scoped;

635

expr_delay = Delay.new_var ();

636

expr_loc = loc;

637

expr_annot = None})

638

dummy_id_expr cl

639

in

640

clock_expr temp_env when_expr

641


642

(* Clocks a variable declaration *)

643

let clock_var_decl scoped env vdecl =

644

let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in

645

let ck =

646

(* WTF ????

647

if vdecl.var_dec_const

648

then

649

(try_generalize ck vdecl.var_loc; ck)

650

else

651

*)

652

if Types.get_clock_base_type vdecl.var_type <> None

653

then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped

654

else ck in

655

(if vdecl.var_dec_const

656

then match vdecl.var_dec_value with

657

 None > ()

658

 Some v >

659

begin

660

let ck_static = clock_expr env v in

661

try_unify ck ck_static v.expr_loc

662

end);

663

try_unify ck vdecl.var_clock vdecl.var_loc;

664

Env.add_value env vdecl.var_id ck

665


666

(* Clocks a variable declaration list *)

667

let clock_var_decl_list env scoped l =

668

List.fold_left (clock_var_decl scoped) env l

669


670

(** [clock_node env nd] performs the clockcalculus for node [nd] in

671

environment [env].

672

Generalization of clocks wrt scopes follows this rule:

673

 generalize inputs (unscoped).

674

 generalize outputs. As they are scoped, only clocks coming from inputs

675

are allowed to be generalized.

676

 generalize locals. As outputs don't depend on them (checked the step before),

677

they can be generalized.

678

*)

679

let clock_node env loc nd =

680

(* let is_main = nd.node_id = !Options.main_node in *)

681

let new_env = clock_var_decl_list env false nd.node_inputs in

682

let new_env = clock_var_decl_list new_env true nd.node_outputs in

683

let new_env = clock_var_decl_list new_env true nd.node_locals in

684

let eqs, auts = get_node_eqs nd in (* TODO XXX: perform the clocking on auts.

685

For the moment, it is ignored *)

686

List.iter (clock_eq new_env) eqs;

687

let ck_ins = clock_of_vlist nd.node_inputs in

688

let ck_outs = clock_of_vlist nd.node_outputs in

689

let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in

690

unify_imported_clock None ck_node loc;

691

Log.report ~level:3 (fun fmt > print_ck fmt ck_node);

692

(* Local variables may contain firstorder carrier variables that should be generalized.

693

That's not the case for types. *)

694

try_generalize ck_node loc;

695

(*

696

List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;

697

List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*)

698

(*List.iter (fun vdecl > try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*)

699

(* TODO : Xavier pourquoi ai je cette erreur ? *)

700

(* if (is_main && is_polymorphic ck_node) then

701

raise (Error (loc,(Cannot_be_polymorphic ck_node)));

702

*)

703

Log.report ~level:3 (fun fmt > print_ck fmt ck_node);

704

nd.node_clock < ck_node;

705

Env.add_value env nd.node_id ck_node

706


707


708

let check_imported_pclocks loc ck_node =

709

let pck = ref None in

710

let rec aux ck =

711

match ck.cdesc with

712

 Carrow (ck1,ck2) > aux ck1; aux ck2

713

 Ctuple cl > List.iter aux cl

714

 Con (ck',_,_) > aux ck'

715

 Clink ck' > aux ck'

716

 Ccarrying (_,ck') > aux ck'

717

 Cvar  Cunivar >

718

match !pck with

719

 None > ()

720

 Some (_,_) >

721

raise (Error (loc, (Invalid_imported_clock ck_node)))

722

in

723

aux ck_node

724


725

let clock_imported_node env loc nd =

726

let new_env = clock_var_decl_list env false nd.nodei_inputs in

727

ignore(clock_var_decl_list new_env false nd.nodei_outputs);

728

let ck_ins = clock_of_vlist nd.nodei_inputs in

729

let ck_outs = clock_of_vlist nd.nodei_outputs in

730

let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in

731

unify_imported_clock None ck_node loc;

732

check_imported_pclocks loc ck_node;

733

try_generalize ck_node loc;

734

nd.nodei_clock < ck_node;

735

Env.add_value env nd.nodei_id ck_node

736


737

let clock_top_const env cdecl=

738

let ck = new_var false in

739

try_generalize ck cdecl.const_loc;

740

Env.add_value env cdecl.const_id ck

741


742

let clock_top_consts env clist =

743

List.fold_left clock_top_const env clist

744


745

let rec clock_top_decl env decl =

746

match decl.top_decl_desc with

747

 Node nd >

748

clock_node env decl.top_decl_loc nd

749

 ImportedNode nd >

750

clock_imported_node env decl.top_decl_loc nd

751

 Const c >

752

clock_top_const env c

753

 TypeDef _ > List.fold_left clock_top_decl env (consts_of_enum_type decl)

754

 Open _ > env

755


756

let clock_prog env decls =

757

List.fold_left clock_top_decl env decls

758


759

(* Once the Lustre program is fully clocked,

760

we must get back to the original description of clocks,

761

with constant parameters, instead of unifiable internal variables. *)

762


763

(* The following functions aims at 'unevaluating' carriers occuring in clock expressions,

764

i.e. replacing unifiable second_order variables with the original carrier names.

765

Once restored in this formulation, clocks may be meaningfully printed.

766

*)

767

let uneval_vdecl_generics vdecl =

768

(*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*)

769

if Types.get_clock_base_type vdecl.var_type <> None

770

then

771

match get_carrier_name vdecl.var_clock with

772

 None > (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false)

773

 Some cr > Clocks.uneval vdecl.var_id cr

774


775

let uneval_node_generics vdecls =

776

List.iter uneval_vdecl_generics vdecls

777


778

let uneval_top_generics decl =

779

match decl.top_decl_desc with

780

 Node nd >

781

(* A node could contain firstorder carrier variable in local vars. This is not the case for types. *)

782

uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)

783

 ImportedNode nd >

784

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

785

 Const _

786

 Open _

787

 TypeDef _ > ()

788


789

let uneval_prog_generics prog =

790

List.iter uneval_top_generics prog

791


792

let check_env_compat header declared computed =

793

uneval_prog_generics header;

794

Env.iter declared (fun k decl_clock_k >

795

let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in

796

try_semi_unify decl_clock_k computed_c Location.dummy_loc

797

)

798

(* Local Variables: *)

799

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

800

(* End: *)
