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

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

46

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

47

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

48

 Cvar _ > ck=cvar

49

 Cunivar _  Pck_const (_,_) > false

50

 Clink ck' > occurs cvar ck'

51

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

52


53

(* Clocks generalization *)

54

let rec generalize_carrier cr =

55

match cr.carrier_desc with

56

 Carry_const _

57

 Carry_name >

58

if cr.carrier_scoped then

59

raise (Scope_carrier cr);

60

cr.carrier_desc < Carry_var

61

 Carry_var > ()

62

 Carry_link cr' > generalize_carrier cr'

63


64

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

65

(* Generalize by sideeffects *)

66

let rec generalize ck =

67

match ck.cdesc with

68

 Carrow (ck1,ck2) >

69

generalize ck1; generalize ck2

70

 Ctuple clist >

71

List.iter generalize clist

72

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

73

 Cvar cset >

74

if ck.cscoped then

75

raise (Scope_clock ck);

76

ck.cdesc < Cunivar cset

77

 Pck_up (ck',_) > generalize ck'

78

 Pck_down (ck',_) > generalize ck'

79

 Pck_phase (ck',_) > generalize ck'

80

 Pck_const (_,_)  Cunivar _ > ()

81

 Clink ck' >

82

generalize ck'

83

 Ccarrying (cr,ck') >

84

generalize_carrier cr; generalize ck'

85


86

let try_generalize ck_node loc =

87

try

88

generalize ck_node

89

with (Scope_carrier cr) >

90

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

91

 (Scope_clock ck) >

92

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

93


94

(* Clocks instanciation *)

95

let instantiate_carrier cr inst_cr_vars =

96

let cr = carrier_repr cr in

97

match cr.carrier_desc with

98

 Carry_const _

99

 Carry_name > cr

100

 Carry_link _ >

101

failwith "Internal error"

102

 Carry_var >

103

try

104

List.assoc cr.carrier_id !inst_cr_vars

105

with Not_found >

106

let cr_var = new_carrier Carry_name true in

107

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

108

cr_var

109


110

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

111

(* inst_ck_vars ensures that a polymorphic variable is instanciated with

112

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

113

type. inst_cr_vars is the same for carriers. *)

114

let rec instantiate inst_ck_vars inst_cr_vars ck =

115

match ck.cdesc with

116

 Carrow (ck1,ck2) >

117

{ck with cdesc =

118

Carrow ((instantiate inst_ck_vars inst_cr_vars ck1),

119

(instantiate inst_ck_vars inst_cr_vars ck2))}

120

 Ctuple cklist >

121

{ck with cdesc = Ctuple

122

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

123

 Con (ck',c,l) >

124

let c' = instantiate_carrier c inst_cr_vars in

125

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

126

 Cvar _  Pck_const (_,_) > ck

127

 Pck_up (ck',k) >

128

{ck with cdesc = Pck_up ((instantiate inst_ck_vars inst_cr_vars ck'),k)}

129

 Pck_down (ck',k) >

130

{ck with cdesc = Pck_down ((instantiate inst_ck_vars inst_cr_vars ck'),k)}

131

 Pck_phase (ck',q) >

132

{ck with cdesc = Pck_phase ((instantiate inst_ck_vars inst_cr_vars ck'),q)}

133

 Clink ck' >

134

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

135

 Ccarrying (cr,ck') >

136

let cr' = instantiate_carrier cr inst_cr_vars in

137

{ck with cdesc =

138

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

139

 Cunivar cset >

140

try

141

List.assoc ck.cid !inst_ck_vars

142

with Not_found >

143

let var = new_ck (Cvar cset) true in

144

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

145

var

146


147

(** [subsume pck1 cset1] subsumes clock [pck1] by clock subset

148

[cset1]. The clock constraint is actually recursively transfered to

149

the clock variable appearing in [pck1] *)

150

let subsume pck1 cset1 =

151

let rec aux pck cset =

152

match cset with

153

 CSet_all >

154

()

155

 CSet_pck (k,(a,b)) >

156

match pck.cdesc with

157

 Cvar cset' >

158

pck.cdesc < Cvar (intersect cset' cset)

159

 Pck_up (pck',k') >

160

let rat = if a=0 then (0,1) else (a,b*k') in

161

aux pck' (CSet_pck ((k*k'),rat))

162

 Pck_down (pck',k') >

163

let k''=k/(gcd k k') in

164

aux pck' (CSet_pck (k'',(a*k',b)))

165

 Pck_phase (pck',(a',b')) >

166

let (a'',b'')= max_rat (sum_rat (a,b) (a',b')) (0,1) in

167

aux pck' (CSet_pck (k, (a'',b'')))

168

 Pck_const (n,(a',b')) >

169

if n mod k <> 0  (max_rat (a,b) (a',b')) <> (a',b') then

170

raise (Subsume (pck1, cset1))

171

 Clink pck' >

172

aux pck' cset

173

 Cunivar _ > ()

174

 Ccarrying (_,ck') >

175

aux ck' cset

176

 _ > raise (Subsume (pck1, cset1))

177

in

178

aux pck1 cset1

179


180

let rec update_scope_carrier scoped cr =

181

if (not scoped) then

182

begin

183

cr.carrier_scoped < scoped;

184

match cr.carrier_desc with

185

 Carry_const _  Carry_name  Carry_var > ()

186

 Carry_link cr' > update_scope_carrier scoped cr'

187

end

188


189

let rec update_scope scoped ck =

190

if (not scoped) then

191

begin

192

ck.cscoped < scoped;

193

match ck.cdesc with

194

 Carrow (ck1,ck2) >

195

update_scope scoped ck1; update_scope scoped ck2

196

 Ctuple clist >

197

List.iter (update_scope scoped) clist

198

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

199

 Cvar cset >

200

ck.cdesc < Cvar cset

201

 Pck_up (ck',_) > update_scope scoped ck'

202

 Pck_down (ck',_) > update_scope scoped ck'

203

 Pck_phase (ck',_) > update_scope scoped ck'

204

 Pck_const (_,_)  Cunivar _ > ()

205

 Clink ck' >

206

update_scope scoped ck'

207

 Ccarrying (cr,ck') >

208

update_scope_carrier scoped cr; update_scope scoped ck'

209

end

210


211

(* Unifies two static pclocks. *)

212

let unify_static_pck ck1 ck2 =

213

if (period ck1 <> period ck2)  (phase ck1 <> phase ck2) then

214

raise (Unify (ck1,ck2))

215


216

(* Unifies two clock carriers *)

217

let unify_carrier cr1 cr2 =

218

let cr1 = carrier_repr cr1 in

219

let cr2 = carrier_repr cr2 in

220

if cr1==cr2 then ()

221

else

222

match cr1.carrier_desc, cr2.carrier_desc with

223

 Carry_const id1, Carry_const id2 >

224

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

225

 Carry_const _, Carry_name >

226

begin

227

cr2.carrier_desc < Carry_link cr1;

228

update_scope_carrier cr2.carrier_scoped cr1

229

end

230

 Carry_name, Carry_const _ >

231

begin

232

cr1.carrier_desc < Carry_link cr2;

233

update_scope_carrier cr1.carrier_scoped cr2

234

end

235

 Carry_name, Carry_name >

236

if cr1.carrier_id < cr2.carrier_id then

237

begin

238

cr2.carrier_desc < Carry_link cr1;

239

update_scope_carrier cr2.carrier_scoped cr1

240

end

241

else

242

begin

243

cr1.carrier_desc < Carry_link cr2;

244

update_scope_carrier cr1.carrier_scoped cr2

245

end

246

 _,_ > assert false

247


248

(* Semiunifies two clock carriers *)

249

let semi_unify_carrier cr1 cr2 =

250

let cr1 = carrier_repr cr1 in

251

let cr2 = carrier_repr cr2 in

252

if cr1==cr2 then ()

253

else

254

match cr1.carrier_desc, cr2.carrier_desc with

255

 Carry_const id1, Carry_const id2 >

256

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

257

 Carry_const _, Carry_name >

258

begin

259

cr2.carrier_desc < Carry_link cr1;

260

update_scope_carrier cr2.carrier_scoped cr1

261

end

262

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

263

 Carry_name, Carry_name >

264

if cr1.carrier_id < cr2.carrier_id then

265

begin

266

cr2.carrier_desc < Carry_link cr1;

267

update_scope_carrier cr2.carrier_scoped cr1

268

end

269

else

270

begin

271

cr1.carrier_desc < Carry_link cr2;

272

update_scope_carrier cr1.carrier_scoped cr2

273

end

274

 _,_ > assert false

275


276

let try_unify_carrier ck1 ck2 loc =

277

try

278

unify_carrier ck1 ck2

279

with

280

 Unify (ck1',ck2') >

281

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

282

 Subsume (ck,cset) >

283

raise (Error (loc, Clock_set_mismatch (ck,cset)))

284

 Mismatch (cr1,cr2) >

285

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

286


287

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

288

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

289

let rec unify ck1 ck2 =

290

let ck1 = repr ck1 in

291

let ck2 = repr ck2 in

292

if ck1==ck2 then

293

()

294

else

295

let left_const = is_concrete_pck ck1 in

296

let right_const = is_concrete_pck ck2 in

297

if left_const && right_const then

298

unify_static_pck ck1 ck2

299

else

300

match ck1.cdesc,ck2.cdesc with

301

 Cvar cset1,Cvar cset2>

302

if ck1.cid < ck2.cid then

303

begin

304

ck2.cdesc < Clink (simplify ck1);

305

update_scope ck2.cscoped ck1;

306

subsume ck1 cset2

307

end

308

else

309

begin

310

ck1.cdesc < Clink (simplify ck2);

311

update_scope ck1.cscoped ck2;

312

subsume ck2 cset1

313

end

314

 Cvar cset, Pck_up (_,_)  Cvar cset, Pck_down (_,_)

315

 Cvar cset, Pck_phase (_,_)  Cvar cset, Pck_const (_,_) >

316

if (occurs ck1 ck2) then

317

begin

318

if (simplify ck2 = ck1) then

319

ck2.cdesc < Clink (simplify ck1)

320

else

321

raise (Unify (ck1,ck2));

322

end

323

else

324

begin

325

ck1.cdesc < Clink (simplify ck2);

326

subsume ck2 cset

327

end

328

 Pck_up (_,_), Cvar cset  Pck_down (_,_), Cvar cset

329

 Pck_phase (_,_), Cvar cset  Pck_const (_,_), Cvar cset >

330

if (occurs ck2 ck1) then

331

begin

332

if ((simplify ck1) = ck2) then

333

ck1.cdesc < Clink (simplify ck2)

334

else

335

raise (Unify (ck1,ck2));

336

end

337

else

338

begin

339

ck2.cdesc < Clink (simplify ck1);

340

subsume ck1 cset

341

end

342

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

343

subsume ck2 cset;

344

update_scope ck1.cscoped ck2;

345

ck1.cdesc < Clink (simplify ck2)

346

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

347

subsume ck1 cset;

348

update_scope ck2.cscoped ck1;

349

ck2.cdesc < Clink (simplify ck1)

350

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

351

unify_carrier cr1 cr2;

352

unify ck1' ck2'

353

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

354

raise (Unify (ck1,ck2))

355

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

356

unify c1 c1'; unify c2 c2'

357

 Ctuple ckl1, Ctuple ckl2 >

358

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

359

raise (Unify (ck1,ck2));

360

List.iter2 unify ckl1 ckl2

361

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

362

unify_carrier c1 c2;

363

unify ck' ck''

364

 Pck_const (i,r), Pck_const (i',r') >

365

if i<>i'  r <> r' then

366

raise (Unify (ck1,ck2))

367

 (_, Pck_up (pck2',k)) when (not right_const) >

368

let ck1' = simplify (new_ck (Pck_down (ck1,k)) true) in

369

unify ck1' pck2'

370

 (_,Pck_down (pck2',k)) when (not right_const) >

371

subsume ck1 (CSet_pck (k,(0,1)));

372

let ck1' = simplify (new_ck (Pck_up (ck1,k)) true) in

373

unify ck1' pck2'

374

 (_,Pck_phase (pck2',(a,b))) when (not right_const) >

375

subsume ck1 (CSet_pck (b,(a,b)));

376

let ck1' = simplify (new_ck (Pck_phase (ck1,(a,b))) true) in

377

unify ck1' pck2'

378

 Pck_up (pck1',k),_ >

379

let ck2' = simplify (new_ck (Pck_down (ck2,k)) true) in

380

unify pck1' ck2'

381

 Pck_down (pck1',k),_ >

382

subsume ck2 (CSet_pck (k,(0,1)));

383

let ck2' = simplify (new_ck (Pck_up (ck2,k)) true) in

384

unify pck1' ck2'

385

 Pck_phase (pck1',(a,b)),_ >

386

subsume ck2 (CSet_pck (b,(a,b)));

387

let ck2' = simplify (new_ck (Pck_phase (ck2,(a,b))) true) in

388

unify pck1' ck2'

389

 Cunivar _, _  _, Cunivar _ > ()

390

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

391


392

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

393

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

394

let rec semi_unify ck1 ck2 =

395

let ck1 = repr ck1 in

396

let ck2 = repr ck2 in

397

if ck1==ck2 then

398

()

399

else

400

match ck1.cdesc,ck2.cdesc with

401

 Cvar cset1,Cvar cset2>

402

if ck1.cid < ck2.cid then

403

begin

404

ck2.cdesc < Clink (simplify ck1);

405

update_scope ck2.cscoped ck1

406

end

407

else

408

begin

409

ck1.cdesc < Clink (simplify ck2);

410

update_scope ck1.cscoped ck2

411

end

412

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

413

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

414

update_scope ck2.cscoped ck1;

415

ck2.cdesc < Clink (simplify ck1)

416

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

417

semi_unify_carrier cr1 cr2;

418

semi_unify ck1' ck2'

419

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

420

raise (Unify (ck1,ck2))

421

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

422

begin

423

semi_unify c1 c1';

424

semi_unify c2 c2'

425

end

426

 Ctuple ckl1, Ctuple ckl2 >

427

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

428

raise (Unify (ck1,ck2));

429

List.iter2 semi_unify ckl1 ckl2

430

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

431

semi_unify_carrier c1 c2;

432

semi_unify ck' ck''

433

 Cunivar _, _  _, Cunivar _ > ()

434

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

435


436

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

437

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

438

let int_factor_of_expr e =

439

match e.expr_desc with

440

 Expr_const

441

(Const_int i) > i

442

 _ > failwith "Internal error: int_factor_of_expr"

443


444

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

445

let rec clock_uncarry ck =

446

let ck = repr ck in

447

match ck.cdesc with

448

 Ccarrying (_, ck') > ck'

449

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

450

 Ctuple ckl > clock_of_clock_list (List.map clock_uncarry ckl)

451

 _ > ck

452


453

let try_unify ck1 ck2 loc =

454

try

455

unify ck1 ck2

456

with

457

 Unify (ck1',ck2') >

458

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

459

 Subsume (ck,cset) >

460

raise (Error (loc, Clock_set_mismatch (ck,cset)))

461

 Mismatch (cr1,cr2) >

462

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

463


464

let try_semi_unify ck1 ck2 loc =

465

try

466

semi_unify ck1 ck2

467

with

468

 Unify (ck1',ck2') >

469

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

470

 Subsume (ck,cset) >

471

raise (Error (loc, Clock_set_mismatch (ck,cset)))

472

 Mismatch (cr1,cr2) >

473

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

474


475

(* ck2 is a subtype of ck1 *)

476

let rec sub_unify sub ck1 ck2 =

477

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

478

 Ctuple cl1 , Ctuple cl2 >

479

if List.length cl1 <> List.length cl2

480

then raise (Unify (ck1, ck2))

481

else List.iter2 (sub_unify sub) cl1 cl2

482

 Ctuple [c1] , _ > sub_unify sub c1 ck2

483

 _ , Ctuple [c2] > sub_unify sub ck1 c2

484

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

485

begin

486

unify_carrier cr1 cr2;

487

sub_unify sub c1 c2

488

end

489

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

490

begin

491

unify_carrier cr1 cr2;

492

sub_unify sub c1 c2

493

end

494

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

495

 _ > unify ck1 ck2

496


497

let try_sub_unify sub ck1 ck2 loc =

498

try

499

sub_unify sub ck1 ck2

500

with

501

 Unify (ck1',ck2') >

502

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

503

 Subsume (ck,cset) >

504

raise (Error (loc, Clock_set_mismatch (ck,cset)))

505

 Mismatch (cr1,cr2) >

506

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

507


508

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

509

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

510

let unify_tuple_clock ref_ck_opt ck loc =

511

(*(match ref_ck_opt with

512

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

513

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

514

let ck_var = ref ref_ck_opt in

515

let rec aux ck =

516

match (repr ck).cdesc with

517

 Con _

518

 Cvar _ >

519

begin

520

match !ck_var with

521

 None >

522

ck_var:=Some ck

523

 Some v >

524

(* may fail *)

525

try_unify ck v loc

526

end

527

 Ctuple cl >

528

List.iter aux cl

529

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

530

 Ccarrying (_, ck1) >

531

aux ck1

532

 _ > ()

533

in aux ck

534


535

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

536

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

537

that is, the activation clock of the node *)

538

let unify_imported_clock ref_ck_opt ck loc =

539

let ck_var = ref ref_ck_opt in

540

let rec aux ck =

541

match (repr ck).cdesc with

542

 Cvar _ >

543

begin

544

match !ck_var with

545

 None >

546

ck_var:=Some ck

547

 Some v >

548

(* cannot fail *)

549

try_unify ck v loc

550

end

551

 Ctuple cl >

552

List.iter aux cl

553

 Carrow (ck1,ck2) >

554

aux ck1; aux ck2

555

 Ccarrying (_, ck1) >

556

aux ck1

557

 Con (ck1, _, _) > aux ck1

558

 _ > ()

559

in

560

aux ck

561


562

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

563

which is not the same as the base clock.

564

Root clock will be used as the call clock

565

of a given node instance *)

566

let compute_root_clock ck =

567

let root = Clocks.root ck in

568

let branch = ref None in

569

let rec aux ck =

570

match (repr ck).cdesc with

571

 Ctuple cl >

572

List.iter aux cl

573

 Carrow (ck1,ck2) >

574

aux ck1; aux ck2

575

 _ >

576

begin

577

match !branch with

578

 None >

579

branch := Some (Clocks.branch ck)

580

 Some br >

581

(* cannot fail *)

582

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

583

end

584

in

585

begin

586

aux ck;

587

Clocks.clock_of_root_branch root (Utils.desome !branch)

588

end

589


590

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

591

 type each expression, remove carriers of clocks as

592

carriers may only denote variables, not arbitrary expr.

593

 try to unify these clocks altogether

594

*)

595

let rec clock_standard_args env expr_list =

596

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

597

let ck_res = new_var true in

598

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

599

ck_res

600


601

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

602

used during node application only *)

603

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

604

let loc = real_arg.expr_loc in

605

let real_clock = clock_expr env real_arg in

606

try_sub_unify sub formal_clock real_clock loc

607


608

(* computes clocks for node application *)

609

and clock_appl env f args clock_reset loc =

610

let args = expr_list_of_expr args in

611

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

612

then

613

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

614

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

615

else

616

clock_call env f args clock_reset loc

617


618

and clock_call env f args clock_reset loc =

619

let cfun = clock_ident false env f loc in

620

let cins, couts = split_arrow cfun in

621

let cins = clock_list_of_clock cins in

622

List.iter2 (clock_subtyping_arg env) args cins;

623

unify_imported_clock (Some clock_reset) cfun loc;

624

couts

625


626

and clock_ident nocarrier env id loc =

627

clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)

628


629

and clock_carrier env c loc ce =

630

let expr_c = expr_of_ident c loc in

631

let ck = clock_expr ~nocarrier:false env expr_c in

632

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

633

let ckb = new_var true in

634

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

635

try_unify ck ckcarry expr_c.expr_loc;

636

unify_tuple_clock (Some ckb) ce expr_c.expr_loc;

637

cr

638


639

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

640

environment [env] *)

641

and clock_expr ?(nocarrier=true) env expr =

642

let resulting_ck =

643

match expr.expr_desc with

644

 Expr_const cst >

645

let ck = new_var true in

646

expr.expr_clock < ck;

647

ck

648

 Expr_ident v >

649

let ckv =

650

try

651

Env.lookup_value env v

652

with Not_found >

653

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

654

in

655

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

656

expr.expr_clock < ck;

657

ck

658

 Expr_array elist >

659

let ck = clock_standard_args env elist in

660

expr.expr_clock < ck;

661

ck

662

 Expr_access (e1, d) >

663

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

664

let ck = clock_standard_args env [e1] in

665

expr.expr_clock < ck;

666

ck

667

 Expr_power (e1, d) >

668

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

669

let ck = clock_standard_args env [e1] in

670

expr.expr_clock < ck;

671

ck

672

 Expr_tuple elist >

673

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

674

expr.expr_clock < ck;

675

ck

676

 Expr_ite (c, t, e) >

677

let ck_c = clock_standard_args env [c] in

678

let ck = clock_standard_args env [t; e] in

679

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

680

unify_tuple_clock (Some ck_c) ck expr.expr_loc;

681

expr.expr_clock < ck;

682

ck

683

 Expr_appl (id, args, r) >

684

(try

685

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

686

this is also the reset clock !

687

*)

688

let cr =

689

match r with

690

 None > new_var true

691

 Some c > clock_standard_args env [c] in

692

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

693

expr.expr_clock < couts;

694

couts

695

with exn > (

696

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

697

raise exn

698

))

699

 Expr_fby (e1,e2)

700

 Expr_arrow (e1,e2) >

701

let ck = clock_standard_args env [e1; e2] in

702

unify_tuple_clock None ck expr.expr_loc;

703

expr.expr_clock < ck;

704

ck

705

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

706

let ck = clock_standard_args env [e] in

707

expr.expr_clock < ck;

708

ck

709

 Expr_when (e,c,l) >

710

let ce = clock_standard_args env [e] in

711

let c_loc = loc_of_cond expr.expr_loc c in

712

let cr = clock_carrier env c c_loc ce in

713

let ck = clock_on ce cr l in

714

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

715

let ck' = clock_on ce cr' l in

716

expr.expr_clock < ck';

717

ck

718

 Expr_merge (c,hl) >

719

let cvar = new_var true in

720

let crvar = new_carrier Carry_name true in

721

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;

722

let cr = clock_carrier env c expr.expr_loc cvar in

723

try_unify_carrier cr crvar expr.expr_loc;

724

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

725

expr.expr_clock < cres;

726

cres

727

in

728

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

729

resulting_ck

730


731

let clock_of_vlist vars =

732

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

733

clock_of_clock_list ckl

734


735

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

736

environment [env] *)

737

let clock_eq env eq =

738

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

739

let ck_rhs = clock_expr env eq.eq_rhs in

740

clock_subtyping_arg env expr_lhs ck_rhs

741


742

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

743

declaration [cck] *)

744

let clock_coreclock env cck id loc scoped =

745

match cck.ck_dec_desc with

746

 Ckdec_any > new_var scoped

747

 Ckdec_pclock (n,(a,b)) >

748

let ck = new_ck (Pck_const (n,(a,b))) scoped in

749

if n mod b <> 0 then raise (Error (loc,Invalid_const ck));

750

ck

751

 Ckdec_bool cl >

752

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

753

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

754

let dummy_id_expr = expr_of_ident id loc in

755

let when_expr =

756

List.fold_left

757

(fun expr (x,l) >

758

{expr_tag = new_tag ();

759

expr_desc = Expr_when (expr,x,l);

760

expr_type = Types.new_var ();

761

expr_clock = new_var scoped;

762

expr_delay = Delay.new_var ();

763

expr_loc = loc;

764

expr_annot = None})

765

dummy_id_expr cl

766

in

767

clock_expr temp_env when_expr

768


769

(* Clocks a variable declaration *)

770

let clock_var_decl scoped env vdecl =

771

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

772

let ck =

773

(* WTF ????

774

if vdecl.var_dec_const

775

then

776

(try_generalize ck vdecl.var_loc; ck)

777

else

778

*)

779

if Types.get_clock_base_type vdecl.var_type <> None

780

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

781

else ck in

782

vdecl.var_clock < ck;

783

Env.add_value env vdecl.var_id ck

784


785

(* Clocks a variable declaration list *)

786

let clock_var_decl_list env scoped l =

787

List.fold_left (clock_var_decl scoped) env l

788


789

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

790

environment [env].

791

Generalization of clocks wrt scopes follows this rule:

792

 generalize inputs (unscoped).

793

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

794

are allowed to be generalized.

795

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

796

they can be generalized.

797

*)

798

let clock_node env loc nd =

799

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

800

let new_env = clock_var_decl_list env false nd.node_inputs in

801

let new_env = clock_var_decl_list new_env true nd.node_outputs in

802

let new_env = clock_var_decl_list new_env true nd.node_locals in

803

List.iter (clock_eq new_env) (get_node_eqs nd);

804

let ck_ins = clock_of_vlist nd.node_inputs in

805

let ck_outs = clock_of_vlist nd.node_outputs in

806

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

807

unify_imported_clock None ck_node loc;

808

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

809

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

810

That's not the case for types. *)

811

try_generalize ck_node loc;

812

(*

813

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

814

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

815

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

816

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

817

(* if (is_main && is_polymorphic ck_node) then

818

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

819

*)

820

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

821

nd.node_clock < ck_node;

822

Env.add_value env nd.node_id ck_node

823


824


825

let check_imported_pclocks loc ck_node =

826

let pck = ref None in

827

let rec aux ck =

828

match ck.cdesc with

829

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

830

 Ctuple cl > List.iter aux cl

831

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

832

 Pck_up (_,_)  Pck_down (_,_)  Pck_phase (_,_) >

833

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

834

 Pck_const (n,p) >

835

begin

836

match !pck with

837

 None > pck := Some (n,p)

838

 Some (n',p') >

839

if (n,p) <> (n',p') then

840

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

841

end

842

 Clink ck' > aux ck'

843

 Ccarrying (_,ck') > aux ck'

844

 Cvar _  Cunivar _ >

845

match !pck with

846

 None > ()

847

 Some (_,_) >

848

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

849

in

850

aux ck_node

851


852

let clock_imported_node env loc nd =

853

let new_env = clock_var_decl_list env false nd.nodei_inputs in

854

ignore(clock_var_decl_list new_env false nd.nodei_outputs);

855

let ck_ins = clock_of_vlist nd.nodei_inputs in

856

let ck_outs = clock_of_vlist nd.nodei_outputs in

857

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

858

unify_imported_clock None ck_node loc;

859

check_imported_pclocks loc ck_node;

860

try_generalize ck_node loc;

861

nd.nodei_clock < ck_node;

862

Env.add_value env nd.nodei_id ck_node

863


864

let clock_top_const env cdecl=

865

let ck = new_var false in

866

try_generalize ck cdecl.const_loc;

867

Env.add_value env cdecl.const_id ck

868


869

let clock_top_consts env clist =

870

List.fold_left clock_top_const env clist

871


872

let rec clock_top_decl env decl =

873

match decl.top_decl_desc with

874

 Node nd >

875

clock_node env decl.top_decl_loc nd

876

 ImportedNode nd >

877

clock_imported_node env decl.top_decl_loc nd

878

 Const c >

879

clock_top_const env c

880

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

881

 Open _ > env

882


883

let clock_prog env decls =

884

List.fold_left clock_top_decl env decls

885


886

(* Once the Lustre program is fully clocked,

887

we must get back to the original description of clocks,

888

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

889


890

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

891

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

892

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

893

*)

894

let uneval_vdecl_generics vdecl =

895

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

896

if Types.get_clock_base_type vdecl.var_type <> None

897

then

898

match get_carrier_name vdecl.var_clock with

899

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

900

 Some cr > Clocks.uneval vdecl.var_id cr

901


902

let uneval_node_generics vdecls =

903

List.iter uneval_vdecl_generics vdecls

904


905

let uneval_top_generics decl =

906

match decl.top_decl_desc with

907

 Node nd >

908

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

909

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

910

 ImportedNode nd >

911

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

912

 Const _

913

 Open _

914

 TypeDef _ > ()

915


916

let uneval_prog_generics prog =

917

List.iter uneval_top_generics prog

918


919

let check_env_compat header declared computed =

920

uneval_prog_generics header;

921

Env.iter declared (fun k decl_clock_k >

922

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

923

try_semi_unify decl_clock_k computed_c Location.dummy_loc

924

)

925

(* Local Variables: *)

926

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

927

(* End: *)
