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 Lustre_types

23

open Corelang

24

open Clocks

25


26

let loc_of_cond (_s, e) id =

27

let pos_start =

28

{ e with Lexing.pos_cnum = e.Lexing.pos_cnum  (String.length id) }

29

in

30

pos_start, e

31


32

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

33

clock [ck]. False otherwise. *)

34

let rec occurs cvar ck =

35

let ck = repr ck in

36

match ck.cdesc with

37

 Carrow (ck1, ck2) >

38

(occurs cvar ck1)  (occurs cvar ck2)

39

 Ctuple ckl >

40

List.exists (occurs cvar) ckl

41

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

42

 Cvar > ck=cvar

43

 Cunivar > false

44

 Clink ck' > occurs cvar ck'

45

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

46


47

(* Clocks generalization *)

48

let rec generalize_carrier cr =

49

match cr.carrier_desc with

50

 Carry_const _

51

 Carry_name >

52

if cr.carrier_scoped then

53

raise (Scope_carrier cr);

54

cr.carrier_desc < Carry_var

55

 Carry_var > ()

56

 Carry_link cr' > generalize_carrier cr'

57


58

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

59

(* Generalize by sideeffects *)

60

let rec generalize ck =

61

match ck.cdesc with

62

 Carrow (ck1,ck2) >

63

generalize ck1; generalize ck2

64

 Ctuple clist >

65

List.iter generalize clist

66

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

67

 Cvar >

68

if ck.cscoped then

69

raise (Scope_clock ck);

70

ck.cdesc < Cunivar

71

 Cunivar > ()

72

 Clink ck' >

73

generalize ck'

74

 Ccarrying (cr,ck') >

75

generalize_carrier cr; generalize ck'

76


77

let try_generalize ck_node loc =

78

try

79

generalize ck_node

80

with

81

 Scope_carrier cr >

82

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

83

 Scope_clock ck >

84

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

85


86

(* Clocks instanciation *)

87

let instantiate_carrier cr inst_cr_vars =

88

let cr = carrier_repr cr in

89

match cr.carrier_desc with

90

 Carry_const _

91

 Carry_name > cr

92

 Carry_link _ >

93

failwith "Internal error"

94

 Carry_var >

95

try

96

List.assoc cr.carrier_id !inst_cr_vars

97

with Not_found >

98

let cr_var = new_carrier Carry_name true in

99

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

100

cr_var

101


102

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

103

(* inst_ck_vars ensures that a polymorphic variable is instanciated with

104

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

105

type. inst_cr_vars is the same for carriers. *)

106

let rec instantiate inst_ck_vars inst_cr_vars ck =

107

match ck.cdesc with

108

 Carrow (ck1,ck2) >

109

{ck with cdesc =

110

Carrow ((instantiate inst_ck_vars inst_cr_vars ck1),

111

(instantiate inst_ck_vars inst_cr_vars ck2))}

112

 Ctuple cklist >

113

{ck with cdesc = Ctuple

114

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

115

 Con (ck',c,l) >

116

let c' = instantiate_carrier c inst_cr_vars in

117

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

118

 Cvar > ck

119

 Clink ck' >

120

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

121

 Ccarrying (cr,ck') >

122

let cr' = instantiate_carrier cr inst_cr_vars in

123

{ck with cdesc =

124

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

125

 Cunivar >

126

try

127

List.assoc ck.cid !inst_ck_vars

128

with Not_found >

129

let var = new_ck Cvar true in

130

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

131

var

132


133


134

let rec update_scope_carrier scoped cr =

135

if (not scoped) then

136

begin

137

cr.carrier_scoped < scoped;

138

match cr.carrier_desc with

139

 Carry_const _  Carry_name  Carry_var > ()

140

 Carry_link cr' > update_scope_carrier scoped cr'

141

end

142


143

let rec update_scope scoped ck =

144

if (not scoped) then

145

begin

146

ck.cscoped < scoped;

147

match ck.cdesc with

148

 Carrow (ck1,ck2) >

149

update_scope scoped ck1; update_scope scoped ck2

150

 Ctuple clist >

151

List.iter (update_scope scoped) clist

152

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

153

 Cvar  Cunivar > ()

154

 Clink ck' >

155

update_scope scoped ck'

156

 Ccarrying (cr,ck') >

157

update_scope_carrier scoped cr; update_scope scoped ck'

158

end

159


160


161

(* Unifies two clock carriers *)

162

let unify_carrier cr1 cr2 =

163

let cr1 = carrier_repr cr1 in

164

let cr2 = carrier_repr cr2 in

165

if cr1==cr2 then ()

166

else

167

match cr1.carrier_desc, cr2.carrier_desc with

168

 Carry_const id1, Carry_const id2 >

169

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

170

 Carry_const _, Carry_name >

171

begin

172

cr2.carrier_desc < Carry_link cr1;

173

update_scope_carrier cr2.carrier_scoped cr1

174

end

175

 Carry_name, Carry_const _ >

176

begin

177

cr1.carrier_desc < Carry_link cr2;

178

update_scope_carrier cr1.carrier_scoped cr2

179

end

180

 Carry_name, Carry_name >

181

if cr1.carrier_id < cr2.carrier_id then

182

begin

183

cr2.carrier_desc < Carry_link cr1;

184

update_scope_carrier cr2.carrier_scoped cr1

185

end

186

else

187

begin

188

cr1.carrier_desc < Carry_link cr2;

189

update_scope_carrier cr1.carrier_scoped cr2

190

end

191

 _,_ > assert false

192


193

(* Semiunifies two clock carriers *)

194

let semi_unify_carrier cr1 cr2 =

195

let cr1 = carrier_repr cr1 in

196

let cr2 = carrier_repr cr2 in

197

if cr1==cr2 then ()

198

else

199

match cr1.carrier_desc, cr2.carrier_desc with

200

 Carry_const id1, Carry_const id2 >

201

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

202

 Carry_const _, Carry_name >

203

begin

204

cr2.carrier_desc < Carry_link cr1;

205

update_scope_carrier cr2.carrier_scoped cr1

206

end

207

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

208

 Carry_name, Carry_name >

209

if cr1.carrier_id < cr2.carrier_id then

210

begin

211

cr2.carrier_desc < Carry_link cr1;

212

update_scope_carrier cr2.carrier_scoped cr1

213

end

214

else

215

begin

216

cr1.carrier_desc < Carry_link cr2;

217

update_scope_carrier cr1.carrier_scoped cr2

218

end

219

 _,_ > assert false

220


221

let try_unify_carrier ck1 ck2 loc =

222

try

223

unify_carrier ck1 ck2

224

with

225

 Unify (ck1',ck2') >

226

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

227

 Mismatch (cr1,cr2) >

228

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

229


230

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

231

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

232

let rec unify ck1 ck2 =

233

let ck1 = repr ck1 in

234

let ck2 = repr ck2 in

235

if ck1==ck2 then

236

()

237

else

238

match ck1.cdesc,ck2.cdesc with

239

 Cvar, Cvar >

240

if ck1.cid < ck2.cid then

241

begin

242

ck2.cdesc < Clink (simplify ck1);

243

update_scope ck2.cscoped ck1

244

end

245

else

246

begin

247

ck1.cdesc < Clink (simplify ck2);

248

update_scope ck1.cscoped ck2

249

end

250

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

251

update_scope ck1.cscoped ck2;

252

ck1.cdesc < Clink (simplify ck2)

253

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

254

update_scope ck2.cscoped ck1;

255

ck2.cdesc < Clink (simplify ck1)

256

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

257

unify_carrier cr1 cr2;

258

unify ck1' ck2'

259

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

260

raise (Unify (ck1,ck2))

261

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

262

unify c1 c1'; unify c2 c2'

263

 Ctuple ckl1, Ctuple ckl2 >

264

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

265

raise (Unify (ck1,ck2));

266

List.iter2 unify ckl1 ckl2

267

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

268

unify_carrier c1 c2;

269

unify ck' ck''

270

 Cunivar, _  _, Cunivar > ()

271

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

272


273

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

274

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

275

let rec semi_unify ck1 ck2 =

276

let ck1 = repr ck1 in

277

let ck2 = repr ck2 in

278

if ck1==ck2 then

279

()

280

else

281

match ck1.cdesc,ck2.cdesc with

282

 Cvar, Cvar >

283

if ck1.cid < ck2.cid then

284

begin

285

ck2.cdesc < Clink (simplify ck1);

286

update_scope ck2.cscoped ck1

287

end

288

else

289

begin

290

ck1.cdesc < Clink (simplify ck2);

291

update_scope ck1.cscoped ck2

292

end

293

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

294

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

295

update_scope ck2.cscoped ck1;

296

ck2.cdesc < Clink (simplify ck1)

297

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

298

semi_unify_carrier cr1 cr2;

299

semi_unify ck1' ck2'

300

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

301

raise (Unify (ck1,ck2))

302

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

303

begin

304

semi_unify c1 c1';

305

semi_unify c2 c2'

306

end

307

 Ctuple ckl1, Ctuple ckl2 >

308

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

309

raise (Unify (ck1,ck2));

310

List.iter2 semi_unify ckl1 ckl2

311

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

312

semi_unify_carrier c1 c2;

313

semi_unify ck' ck''

314

 Cunivar, _  _, Cunivar > ()

315

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

316


317

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

318

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

319

let int_factor_of_expr e =

320

match e.expr_desc with

321

 Expr_const

322

(Const_int i) > i

323

 _ > failwith "Internal error: int_factor_of_expr"

324


325

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

326

let rec clock_uncarry ck =

327

let ck = repr ck in

328

match ck.cdesc with

329

 Ccarrying (_, ck') > ck'

330

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

331

 Ctuple ckl > clock_of_clock_list (List.map clock_uncarry ckl)

332

 _ > ck

333


334

let try_unify ck1 ck2 loc =

335

try

336

unify ck1 ck2

337

with

338

 Unify (ck1',ck2') >

339

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

340

 Mismatch (cr1,cr2) >

341

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

342


343

let try_semi_unify ck1 ck2 loc =

344

try

345

semi_unify ck1 ck2

346

with

347

 Unify (ck1',ck2') >

348

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

349

 Mismatch (cr1,cr2) >

350

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

351


352

(* ck2 is a subtype of ck1 *)

353

let rec sub_unify sub ck1 ck2 =

354

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

355

 Ctuple cl1 , Ctuple cl2 >

356

if List.length cl1 <> List.length cl2

357

then raise (Unify (ck1, ck2))

358

else List.iter2 (sub_unify sub) cl1 cl2

359

 Ctuple [c1] , _ > sub_unify sub c1 ck2

360

 _ , Ctuple [c2] > sub_unify sub ck1 c2

361

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

362

begin

363

unify_carrier cr1 cr2;

364

sub_unify sub c1 c2

365

end

366

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

367

begin

368

unify_carrier cr1 cr2;

369

sub_unify sub c1 c2

370

end

371

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

372

 _ > unify ck1 ck2

373


374

let try_sub_unify sub ck1 ck2 loc =

375

try

376

sub_unify sub ck1 ck2

377

with

378

 Unify (ck1',ck2') >

379

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

380

 Mismatch (cr1,cr2) >

381

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

382


383

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

384

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

385

let unify_tuple_clock ref_ck_opt ck loc =

386

(*(match ref_ck_opt with

387

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

388

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

389

let ck_var = ref ref_ck_opt in

390

let rec aux ck =

391

match (repr ck).cdesc with

392

 Con _

393

 Cvar >

394

begin

395

match !ck_var with

396

 None >

397

ck_var:=Some ck

398

 Some v >

399

(* may fail *)

400

try_unify ck v loc

401

end

402

 Ctuple cl >

403

List.iter aux cl

404

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

405

 Ccarrying (_, ck1) >

406

aux ck1

407

 _ > ()

408

in aux ck

409


410

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

411

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

412

that is, the activation clock of the node *)

413

let unify_imported_clock ref_ck_opt ck loc =

414

let ck_var = ref ref_ck_opt in

415

let rec aux ck =

416

match (repr ck).cdesc with

417

 Cvar >

418

begin

419

match !ck_var with

420

 None >

421

ck_var := Some ck

422

 Some v >

423

(* cannot fail *)

424

try_unify ck v loc

425

end

426

 Ctuple cl >

427

List.iter aux cl

428

 Carrow (ck1,ck2) >

429

aux ck1; aux ck2

430

 Ccarrying (_, ck1) >

431

aux ck1

432

 Con (ck1, _, _) > aux ck1

433

 _ > ()

434

in

435

aux ck

436


437

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

438

which is not the same as the base clock.

439

Root clock will be used as the call clock

440

of a given node instance *)

441

let compute_root_clock ck =

442

let root = Clocks.root ck in

443

let branch = ref None in

444

let rec aux ck =

445

match (repr ck).cdesc with

446

 Ctuple cl >

447

List.iter aux cl

448

 Carrow (ck1,ck2) >

449

aux ck1; aux ck2

450

 _ >

451

begin

452

match !branch with

453

 None >

454

branch := Some (Clocks.branch ck)

455

 Some br >

456

(* cannot fail *)

457

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

458

end

459

in

460

begin

461

aux ck;

462

Clocks.clock_of_root_branch root (Utils.desome !branch)

463

end

464


465

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

466

 type each expression, remove carriers of clocks as

467

carriers may only denote variables, not arbitrary expr.

468

 try to unify these clocks altogether

469

*)

470

let rec clock_standard_args env expr_list =

471

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

472

let ck_res = new_var true in

473

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

474

ck_res

475


476

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

477

used during node application only *)

478

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

479

let loc = real_arg.expr_loc in

480

let real_clock = clock_expr env real_arg in

481

try_sub_unify sub formal_clock real_clock loc

482


483

(* computes clocks for node application *)

484

and clock_appl env f args clock_reset loc =

485

let args = expr_list_of_expr args in

486

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

487

then

488

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

489

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

490

else

491

clock_call env f args clock_reset loc

492


493

and clock_call env f args clock_reset loc =

494

(* Format.eprintf "Clocking call %s@." f; *)

495

let cfun = clock_ident false env f loc in

496

let cins, couts = split_arrow cfun in

497

let cins = clock_list_of_clock cins in

498

List.iter2 (clock_subtyping_arg env) args cins;

499

unify_imported_clock (Some clock_reset) cfun loc;

500

couts

501


502

and clock_ident nocarrier env id loc =

503

clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)

504


505

and clock_carrier env c loc ce =

506

let expr_c = expr_of_ident c loc in

507

let ck = clock_expr ~nocarrier:false env expr_c in

508

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

509

let ckb = new_var true in

510

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

511

try_unify ck ckcarry expr_c.expr_loc;

512

unify_tuple_clock (Some ckb) ce expr_c.expr_loc;

513

cr

514


515

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

516

environment [env] *)

517

and clock_expr ?(nocarrier=true) env expr =

518

let resulting_ck =

519

match expr.expr_desc with

520

 Expr_const _ >

521

let ck = new_var true in

522

expr.expr_clock < ck;

523

ck

524

 Expr_ident v >

525

let ckv =

526

try

527

Env.lookup_value env v

528

with Not_found >

529

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

530

in

531

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

532

expr.expr_clock < ck;

533

ck

534

 Expr_array elist >

535

let ck = clock_standard_args env elist in

536

expr.expr_clock < ck;

537

ck

538

 Expr_access (e1, _) >

539

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

540

let ck = clock_standard_args env [e1] in

541

expr.expr_clock < ck;

542

ck

543

 Expr_power (e1, _) >

544

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

545

let ck = clock_standard_args env [e1] in

546

expr.expr_clock < ck;

547

ck

548

 Expr_tuple elist >

549

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

550

expr.expr_clock < ck;

551

ck

552

 Expr_ite (c, t, e) >

553

let ck_c = clock_standard_args env [c] in

554

let ck = clock_standard_args env [t; e] in

555

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

556

unify_tuple_clock (Some ck_c) ck expr.expr_loc;

557

expr.expr_clock < ck;

558

ck

559

 Expr_appl (id, args, r) >

560

(try

561

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

562

this is also the reset clock !

563

*)

564

let cr =

565

match r with

566

 None > new_var true

567

 Some c > clock_standard_args env [c] in

568

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

569

expr.expr_clock < couts;

570

couts

571

with exn > (

572

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

573

raise exn

574

))

575

 Expr_fby (e1,e2)

576

 Expr_arrow (e1,e2) >

577

let ck = clock_standard_args env [e1; e2] in

578

unify_tuple_clock None ck expr.expr_loc;

579

expr.expr_clock < ck;

580

ck

581

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

582

let ck = clock_standard_args env [e] in

583

expr.expr_clock < ck;

584

ck

585

 Expr_when (e,c,l) >

586

let ce = clock_standard_args env [e] in

587

let c_loc = loc_of_cond expr.expr_loc c in

588

let cr = clock_carrier env c c_loc ce in

589

let ck = clock_on ce cr l in

590

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

591

let ck' = clock_on ce cr' l in

592

expr.expr_clock < ck';

593

ck

594

 Expr_merge (c,hl) >

595

let cvar = new_var true in

596

let crvar = new_carrier Carry_name true in

597

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;

598

let cr = clock_carrier env c expr.expr_loc cvar in

599

try_unify_carrier cr crvar expr.expr_loc;

600

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

601

expr.expr_clock < cres;

602

cres

603

in

604

Log.report ~level:4 (fun fmt > Format.fprintf fmt "Clock of expr %a: %a@ "

605

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

616

(List.map (fun v > expr_of_ident v eq.eq_loc) eq.eq_lhs) in

617

let ck_rhs = clock_expr env eq.eq_rhs in

618

clock_subtyping_arg env expr_lhs ck_rhs

619


620

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

621

declaration [cck] *)

622

let clock_coreclock env cck id loc scoped =

623

match cck.ck_dec_desc with

624

 Ckdec_any > new_var scoped

625

 Ckdec_bool cl >

626

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

627

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

628

let dummy_id_expr = expr_of_ident id loc in

629

let when_expr =

630

List.fold_left

631

(fun expr (x,l) >

632

{expr_tag = new_tag ();

633

expr_desc = Expr_when (expr,x,l);

634

expr_type = Types.new_var ();

635

expr_clock = new_var scoped;

636

expr_delay = Delay.new_var ();

637

expr_loc = loc;

638

expr_annot = None})

639

dummy_id_expr cl

640

in

641

clock_expr temp_env when_expr

642


643

(* Clocks a variable declaration *)

644

let clock_var_decl scoped env vdecl =

645

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

646

let ck =

647

(* WTF ????

648

if vdecl.var_dec_const

649

then

650

(try_generalize ck vdecl.var_loc; ck)

651

else

652

*)

653

if Types.get_clock_base_type vdecl.var_type <> None

654

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

655

else ck in

656

(if vdecl.var_dec_const

657

then match vdecl.var_dec_value with

658

 None > ()

659

 Some v >

660

begin

661

let ck_static = clock_expr env v in

662

try_unify ck ck_static v.expr_loc

663

end);

664

try_unify ck vdecl.var_clock vdecl.var_loc;

665

Env.add_value env vdecl.var_id ck

666


667

(* Clocks a variable declaration list *)

668

let clock_var_decl_list env scoped l =

669

List.fold_left (clock_var_decl scoped) env l

670


671

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

672

environment [env].

673

Generalization of clocks wrt scopes follows this rule:

674

 generalize inputs (unscoped).

675

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

676

are allowed to be generalized.

677

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

678

they can be generalized.

679

*)

680

let clock_node env loc nd =

681

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

682

let new_env = clock_var_decl_list env false nd.node_inputs in

683

let new_env = clock_var_decl_list new_env true nd.node_outputs in

684

let new_env = clock_var_decl_list new_env true nd.node_locals in

685

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

686

For the moment, it is ignored *)

687

List.iter (clock_eq new_env) eqs;

688

let ck_ins = clock_of_vlist nd.node_inputs in

689

let ck_outs = clock_of_vlist nd.node_outputs in

690

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

691

unify_imported_clock None ck_node loc;

692

Log.report ~level:3 (fun fmt > Format.fprintf fmt "Clock of %s: %a@ " nd.node_id print_ck ck_node);

693

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

694

That's not the case for types. *)

695

try_generalize ck_node loc;

696

(*

697

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

698

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

699

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

700

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

701

(* if (is_main && is_polymorphic ck_node) then

702

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

703

*)

704

Log.report ~level:3 (fun fmt > Format.fprintf fmt "Generalized clock of %s: %a@ @ " nd.node_id print_ck ck_node);

705

nd.node_clock < ck_node;

706

Env.add_value env nd.node_id ck_node

707


708


709

let check_imported_pclocks loc ck_node =

710

let pck = ref None in

711

let rec aux ck =

712

match ck.cdesc with

713

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

714

 Ctuple cl > List.iter aux cl

715

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

716

 Clink ck' > aux ck'

717

 Ccarrying (_,ck') > aux ck'

718

 Cvar  Cunivar >

719

match !pck with

720

 None > ()

721

 Some (_,_) >

722

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

723

in

724

aux ck_node

725


726

let clock_imported_node env loc nd =

727

let new_env = clock_var_decl_list env false nd.nodei_inputs in

728

ignore(clock_var_decl_list new_env false nd.nodei_outputs);

729

let ck_ins = clock_of_vlist nd.nodei_inputs in

730

let ck_outs = clock_of_vlist nd.nodei_outputs in

731

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

732

unify_imported_clock None ck_node loc;

733

check_imported_pclocks loc ck_node;

734

try_generalize ck_node loc;

735

nd.nodei_clock < ck_node;

736

Env.add_value env nd.nodei_id ck_node

737


738


739

let new_env = clock_var_decl_list

740


741

let clock_top_const env cdecl=

742

let ck = new_var false in

743

try_generalize ck cdecl.const_loc;

744

Env.add_value env cdecl.const_id ck

745


746

let clock_top_consts env clist =

747

List.fold_left clock_top_const env clist

748


749

let rec clock_top_decl env decl =

750

match decl.top_decl_desc with

751

 Node nd >

752

clock_node env decl.top_decl_loc nd

753

 ImportedNode nd >

754

clock_imported_node env decl.top_decl_loc nd

755

 Const c >

756

clock_top_const env c

757

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

758

 Include _  Open _ > env

759


760

let clock_prog env decls =

761

List.fold_left clock_top_decl env decls

762


763

(* Once the Lustre program is fully clocked,

764

we must get back to the original description of clocks,

765

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

766


767

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

768

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

769

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

770

*)

771

let uneval_vdecl_generics vdecl =

772

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

773

if Types.get_clock_base_type vdecl.var_type <> None

774

then

775

match get_carrier_name vdecl.var_clock with

776

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

777

 Some cr > Clocks.uneval vdecl.var_id cr

778


779

let uneval_node_generics vdecls =

780

List.iter uneval_vdecl_generics vdecls

781


782

let uneval_top_generics decl =

783

match decl.top_decl_desc with

784

 Node nd >

785

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

786

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

787

 ImportedNode nd >

788

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

789

 Const _

790

 Include _  Open _

791

 TypeDef _ > ()

792


793

let uneval_prog_generics prog =

794

List.iter uneval_top_generics prog

795


796

let check_env_compat header declared computed =

797

uneval_prog_generics header;

798

Env.iter declared (fun k decl_clock_k >

799

try

800

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

801

try_semi_unify decl_clock_k computed_c Location.dummy_loc

802

with Not_found > (* If the lookup failed then either an actual

803

required element should have been declared

804

and is missing but typing should have catch

805

it, or it was a contract and does not

806

require this additional check. *)

807

()

808

)

809

(* Local Variables: *)

810

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

811

(* End: *)
