1

(* 

2

* SchedMCore  A MultiCore Scheduling Framework

3

* Copyright (C) 20092011, ONERA, Toulouse, FRANCE  LIFL, Lille, FRANCE

4

*

5

* This file is part of Prelude

6

*

7

* Prelude is free software; you can redistribute it and/or

8

* modify it under the terms of the GNU Lesser General Public License

9

* as published by the Free Software Foundation ; either version 2 of

10

* the License, or (at your option) any later version.

11

*

12

* Prelude is distributed in the hope that it will be useful, but

13

* WITHOUT ANY WARRANTY ; without even the implied warranty of

14

* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU

15

* Lesser General Public License for more details.

16

*

17

* You should have received a copy of the GNU Lesser General Public

18

* License along with this program ; if not, write to the Free Software

19

* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 021111307

20

* USA

21

* *)

22


23

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

24

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

25


26

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

27

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

28

identifier redefinition allowed. *)

29

open Utils

30

open LustreSpec

31

open Corelang

32

open Clocks

33

open Format

34


35

let loc_of_cond loc_containing id =

36

let pos_start =

37

{loc_containing.Location.loc_end with

38

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

39

in

40

{Location.loc_start = pos_start;

41

Location.loc_end = loc_containing.Location.loc_end}

42


43

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

44

clock [ck]. False otherwise. *)

45

let rec occurs cvar ck =

46

let ck = repr ck in

47

match ck.cdesc with

48

 Carrow (ck1, ck2) >

49

(occurs cvar ck1)  (occurs cvar ck2)

50

 Ctuple ckl >

51

List.exists (occurs cvar) ckl

52

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

53

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

54

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

55

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

56

 Cvar _ > ck=cvar

57

 Cunivar _  Pck_const (_,_) > false

58

 Clink ck' > occurs cvar ck'

59

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

60


61

(* Clocks generalization *)

62

let rec generalize_carrier cr =

63

match cr.carrier_desc with

64

 Carry_const _

65

 Carry_name >

66

if cr.carrier_scoped then

67

raise (Scope_carrier cr);

68

cr.carrier_desc < Carry_var

69

 Carry_var > ()

70

 Carry_link cr' > generalize_carrier cr'

71


72

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

73

(* Generalize by sideeffects *)

74

let rec generalize ck =

75

match ck.cdesc with

76

 Carrow (ck1,ck2) >

77

generalize ck1; generalize ck2

78

 Ctuple clist >

79

List.iter generalize clist

80

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

81

 Cvar cset >

82

if ck.cscoped then

83

raise (Scope_clock ck);

84

ck.cdesc < Cunivar cset

85

 Pck_up (ck',_) > generalize ck'

86

 Pck_down (ck',_) > generalize ck'

87

 Pck_phase (ck',_) > generalize ck'

88

 Pck_const (_,_)  Cunivar _ > ()

89

 Clink ck' >

90

generalize ck'

91

 Ccarrying (cr,ck') >

92

generalize_carrier cr; generalize ck'

93


94

let try_generalize ck_node loc =

95

try

96

generalize ck_node

97

with (Scope_carrier cr) >

98

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

99

 (Scope_clock ck) >

100

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

101


102

(* Clocks instanciation *)

103

let instantiate_carrier cr inst_cr_vars =

104

let cr = carrier_repr cr in

105

match cr.carrier_desc with

106

 Carry_const _

107

 Carry_name > cr

108

 Carry_link _ >

109

failwith "Internal error"

110

 Carry_var >

111

try

112

List.assoc cr.carrier_id !inst_cr_vars

113

with Not_found >

114

let cr_var = new_carrier Carry_name true in

115

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

116

cr_var

117


118

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

119

(* inst_ck_vars ensures that a polymorphic variable is instanciated with

120

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

121

type. inst_cr_vars is the same for carriers. *)

122

let rec instantiate inst_ck_vars inst_cr_vars ck =

123

match ck.cdesc with

124

 Carrow (ck1,ck2) >

125

{ck with cdesc =

126

Carrow ((instantiate inst_ck_vars inst_cr_vars ck1),

127

(instantiate inst_ck_vars inst_cr_vars ck2))}

128

 Ctuple cklist >

129

{ck with cdesc = Ctuple

130

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

131

 Con (ck',c,l) >

132

let c' = instantiate_carrier c inst_cr_vars in

133

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

134

 Cvar _  Pck_const (_,_) > ck

135

 Pck_up (ck',k) >

136

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

137

 Pck_down (ck',k) >

138

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

139

 Pck_phase (ck',q) >

140

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

141

 Clink ck' >

142

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

143

 Ccarrying (cr,ck') >

144

let cr' = instantiate_carrier cr inst_cr_vars in

145

{ck with cdesc =

146

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

147

 Cunivar cset >

148

try

149

List.assoc ck.cid !inst_ck_vars

150

with Not_found >

151

let var = new_ck (Cvar cset) true in

152

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

153

var

154


155

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

156

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

157

the clock variable appearing in [pck1] *)

158

let subsume pck1 cset1 =

159

let rec aux pck cset =

160

match cset with

161

 CSet_all >

162

()

163

 CSet_pck (k,(a,b)) >

164

match pck.cdesc with

165

 Cvar cset' >

166

pck.cdesc < Cvar (intersect cset' cset)

167

 Pck_up (pck',k') >

168

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

169

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

170

 Pck_down (pck',k') >

171

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

172

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

173

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

174

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

175

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

176

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

177

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

178

raise (Subsume (pck1, cset1))

179

 Clink pck' >

180

aux pck' cset

181

 Cunivar _ > ()

182

 Ccarrying (_,ck') >

183

aux ck' cset

184

 _ > raise (Subsume (pck1, cset1))

185

in

186

aux pck1 cset1

187


188

let rec update_scope_carrier scoped cr =

189

if (not scoped) then

190

begin

191

cr.carrier_scoped < scoped;

192

match cr.carrier_desc with

193

 Carry_const _  Carry_name  Carry_var > ()

194

 Carry_link cr' > update_scope_carrier scoped cr'

195

end

196


197

let rec update_scope scoped ck =

198

if (not scoped) then

199

begin

200

ck.cscoped < scoped;

201

match ck.cdesc with

202

 Carrow (ck1,ck2) >

203

update_scope scoped ck1; update_scope scoped ck2

204

 Ctuple clist >

205

List.iter (update_scope scoped) clist

206

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

207

 Cvar cset >

208

ck.cdesc < Cvar cset

209

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

210

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

211

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

212

 Pck_const (_,_)  Cunivar _ > ()

213

 Clink ck' >

214

update_scope scoped ck'

215

 Ccarrying (cr,ck') >

216

update_scope_carrier scoped cr; update_scope scoped ck'

217

end

218


219

(* Unifies two static pclocks. *)

220

let unify_static_pck ck1 ck2 =

221

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

222

raise (Unify (ck1,ck2))

223


224

(* Unifies two clock carriers *)

225

let unify_carrier cr1 cr2 =

226

let cr1 = carrier_repr cr1 in

227

let cr2 = carrier_repr cr2 in

228

if cr1=cr2 then ()

229

else

230

match cr1.carrier_desc, cr2.carrier_desc with

231

 Carry_const id1, Carry_const id2 >

232

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

233

 Carry_const _, Carry_name >

234

begin

235

cr2.carrier_desc < Carry_link cr1;

236

update_scope_carrier cr2.carrier_scoped cr1

237

end

238

 Carry_name, Carry_const _ >

239

begin

240

cr1.carrier_desc < Carry_link cr2;

241

update_scope_carrier cr1.carrier_scoped cr2

242

end

243

 Carry_name, Carry_name >

244

if cr1.carrier_id < cr2.carrier_id then

245

begin

246

cr2.carrier_desc < Carry_link cr1;

247

update_scope_carrier cr2.carrier_scoped cr1

248

end

249

else

250

begin

251

cr1.carrier_desc < Carry_link cr2;

252

update_scope_carrier cr1.carrier_scoped cr2

253

end

254

 _,_ > assert false

255


256

(* Semiunifies two clock carriers *)

257

let semi_unify_carrier cr1 cr2 =

258

let cr1 = carrier_repr cr1 in

259

let cr2 = carrier_repr cr2 in

260

if cr1=cr2 then ()

261

else

262

match cr1.carrier_desc, cr2.carrier_desc with

263

 Carry_const id1, Carry_const id2 >

264

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

265

 Carry_const _, Carry_name >

266

begin

267

cr2.carrier_desc < Carry_link cr1;

268

update_scope_carrier cr2.carrier_scoped cr1

269

end

270

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

271

 Carry_name, Carry_name >

272

if cr1.carrier_id < cr2.carrier_id then

273

begin

274

cr2.carrier_desc < Carry_link cr1;

275

update_scope_carrier cr2.carrier_scoped cr1

276

end

277

else

278

begin

279

cr1.carrier_desc < Carry_link cr2;

280

update_scope_carrier cr1.carrier_scoped cr2

281

end

282

 _,_ > assert false

283


284

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

285

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

286

let rec unify ck1 ck2 =

287

let ck1 = repr ck1 in

288

let ck2 = repr ck2 in

289

if ck1=ck2 then

290

()

291

else

292

let left_const = is_concrete_pck ck1 in

293

let right_const = is_concrete_pck ck2 in

294

if left_const && right_const then

295

unify_static_pck ck1 ck2

296

else

297

match ck1.cdesc,ck2.cdesc with

298

 Cvar cset1,Cvar cset2>

299

if ck1.cid < ck2.cid then

300

begin

301

ck2.cdesc < Clink (simplify ck1);

302

update_scope ck2.cscoped ck1;

303

subsume ck1 cset2

304

end

305

else

306

begin

307

ck1.cdesc < Clink (simplify ck2);

308

update_scope ck1.cscoped ck2;

309

subsume ck2 cset1

310

end

311

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

312

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

313

if (occurs ck1 ck2) then

314

begin

315

if (simplify ck2 = ck1) then

316

ck2.cdesc < Clink (simplify ck1)

317

else

318

raise (Unify (ck1,ck2));

319

end

320

else

321

begin

322

ck1.cdesc < Clink (simplify ck2);

323

subsume ck2 cset

324

end

325

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

326

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

327

if (occurs ck2 ck1) then

328

begin

329

if ((simplify ck1) = ck2) then

330

ck1.cdesc < Clink (simplify ck2)

331

else

332

raise (Unify (ck1,ck2));

333

end

334

else

335

begin

336

ck2.cdesc < Clink (simplify ck1);

337

subsume ck1 cset

338

end

339

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

340

subsume ck2 cset;

341

update_scope ck1.cscoped ck2;

342

ck1.cdesc < Clink (simplify ck2)

343

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

344

subsume ck1 cset;

345

update_scope ck2.cscoped ck1;

346

ck2.cdesc < Clink (simplify ck1)

347

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

348

unify_carrier cr1 cr2;

349

unify ck1' ck2'

350

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

351

raise (Unify (ck1,ck2))

352

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

353

unify c1 c1'; unify c2 c2'

354

 Ctuple ckl1, Ctuple ckl2 >

355

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

356

raise (Unify (ck1,ck2));

357

List.iter2 unify ckl1 ckl2

358

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

359

unify_carrier c1 c2;

360

unify ck' ck''

361

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

362

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

363

raise (Unify (ck1,ck2))

364

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

365

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

366

unify ck1' pck2'

367

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

368

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

369

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

370

unify ck1' pck2'

371

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

372

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

373

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

374

unify ck1' pck2'

375

 Pck_up (pck1',k),_ >

376

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

377

unify pck1' ck2'

378

 Pck_down (pck1',k),_ >

379

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

380

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

381

unify pck1' ck2'

382

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

383

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

384

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

385

unify pck1' ck2'

386

 Cunivar _, _  _, Cunivar _ > ()

387

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

388


389

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

390

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

391

let rec semi_unify ck1 ck2 =

392

let ck1 = repr ck1 in

393

let ck2 = repr ck2 in

394

if ck1=ck2 then

395

()

396

else

397

match ck1.cdesc,ck2.cdesc with

398

 Cvar cset1,Cvar cset2>

399

if ck1.cid < ck2.cid then

400

begin

401

ck2.cdesc < Clink (simplify ck1);

402

update_scope ck2.cscoped ck1

403

end

404

else

405

begin

406

ck1.cdesc < Clink (simplify ck2);

407

update_scope ck1.cscoped ck2

408

end

409

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

410

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

411

update_scope ck2.cscoped ck1;

412

ck2.cdesc < Clink (simplify ck1)

413

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

414

semi_unify_carrier cr1 cr2;

415

semi_unify ck1' ck2'

416

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

417

raise (Unify (ck1,ck2))

418

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

419

begin

420

semi_unify c1 c1';

421

semi_unify c2 c2'

422

end

423

 Ctuple ckl1, Ctuple ckl2 >

424

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

425

raise (Unify (ck1,ck2));

426

List.iter2 semi_unify ckl1 ckl2

427

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

428

semi_unify_carrier c1 c2;

429

semi_unify ck' ck''

430

 Cunivar _, _  _, Cunivar _ > ()

431

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

432


433

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

434

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

435

let int_factor_of_expr e =

436

match e.expr_desc with

437

 Expr_const

438

(Const_int i) > i

439

 _ > failwith "Internal error: int_factor_of_expr"

440


441

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

442

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

443

let unify_tuple_clock ref_ck_opt ck =

444

let ck_var = ref ref_ck_opt in

445

let rec aux ck =

446

match (repr ck).cdesc with

447

 Con _

448

 Cvar _ >

449

begin

450

match !ck_var with

451

 None >

452

ck_var:=Some ck

453

 Some v >

454

(* may fail *)

455

unify v ck

456

end

457

 Ctuple cl >

458

List.iter aux cl

459

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

460

 Ccarrying (_, ck1) >

461

aux ck1

462

 _ > ()

463

in

464

aux ck

465


466

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

467

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

468

that is, the activation clock of the node *)

469

let unify_imported_clock ref_ck_opt ck =

470

let ck_var = ref ref_ck_opt in

471

let rec aux ck =

472

match (repr ck).cdesc with

473

 Cvar _ >

474

begin

475

match !ck_var with

476

 None >

477

ck_var:=Some ck

478

 Some v >

479

(* cannot fail *)

480

unify v ck

481

end

482

 Ctuple cl >

483

List.iter aux cl

484

 Carrow (ck1,ck2) >

485

aux ck1; aux ck2

486

 Ccarrying (_, ck1) >

487

aux ck1

488

 Con (ck1, _, _) > aux ck1

489

 _ > ()

490

in

491

aux ck

492


493

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

494

let clock_uncarry ck =

495

let ck = repr ck in

496

match ck.cdesc with

497

 Ccarrying (_, ck') > ck'

498

 _ > ck

499


500

let try_unify ck1 ck2 loc =

501

try

502

unify ck1 ck2

503

with

504

 Unify (ck1',ck2') >

505

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

506

 Subsume (ck,cset) >

507

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

508

 Mismatch (cr1,cr2) >

509

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

510


511

let try_semi_unify ck1 ck2 loc =

512

try

513

semi_unify ck1 ck2

514

with

515

 Unify (ck1',ck2') >

516

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

517

 Subsume (ck,cset) >

518

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

519

 Mismatch (cr1,cr2) >

520

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

521


522

(* ck1 is a subtype of ck2 *)

523

let rec sub_unify sub ck1 ck2 =

524

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

525

 Ctuple cl1 , Ctuple cl2 >

526

if List.length cl1 <> List.length cl2

527

then raise (Unify (ck1, ck2))

528

else List.iter2 (sub_unify sub) cl1 cl2

529

 Ctuple [c1] , _ > sub_unify sub c1 ck2

530

 _ , Ctuple [c2] > sub_unify sub ck1 c2

531

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

532

begin

533

unify_carrier cr1 cr2;

534

sub_unify sub c1 c2

535

end

536

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

537

begin

538

unify_carrier cr1 cr2;

539

sub_unify sub c1 c2

540

end

541

 Ccarrying (_, c1) , _ when sub > sub_unify sub c1 ck2

542

 _ > unify ck1 ck2

543


544

let try_sub_unify sub ck1 ck2 loc =

545

try

546

sub_unify sub ck1 ck2

547

with

548

 Unify (ck1',ck2') >

549

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

550

 Subsume (ck,cset) >

551

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

552

 Mismatch (cr1,cr2) >

553

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

554


555

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

556

 type each expression, remove carriers of clocks as

557

carriers may only denote variables, not arbitrary expr.

558

 try to unify these clocks altogether

559

*)

560

let rec clock_standard_args env expr_list =

561

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

562

let ck_res = new_var true in

563

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

564

ck_res

565


566

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

567

used during node application only *)

568

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

569

let loc = real_arg.expr_loc in

570

let real_clock = clock_expr env real_arg in

571

try_sub_unify sub real_clock formal_clock loc

572


573

(* computes clocks for node application *)

574

and clock_appl env f args clock_reset loc =

575

let args = expr_list_of_expr args in

576

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

577

then

578

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

579

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

580

else

581

clock_call env f args clock_reset loc

582


583

and clock_call env f args clock_reset loc =

584

let cfun = clock_ident false env f loc in

585

let cins, couts = split_arrow cfun in

586

let cins = clock_list_of_clock cins in

587

List.iter2 (clock_subtyping_arg env) args cins;

588

unify_imported_clock (Some clock_reset) cfun;

589

couts

590


591

and clock_ident nocarrier env id loc =

592

clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)

593


594

and clock_carrier env c loc ce =

595

let expr_c = expr_of_ident c loc in

596

let ck = clock_expr ~nocarrier:false env expr_c in

597

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

598

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

599

try_unify ck ckcarry expr_c.expr_loc;

600

cr

601


602

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

603

environment [env] *)

604

and clock_expr ?(nocarrier=true) env expr =

605

let resulting_ck =

606

match expr.expr_desc with

607

 Expr_const cst >

608

let ck = new_var true in

609

expr.expr_clock < ck;

610

ck

611

 Expr_ident v >

612

let ckv =

613

try

614

Env.lookup_value env v

615

with Not_found >

616

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

617

in

618

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

619

expr.expr_clock < ck;

620

ck

621

 Expr_array elist >

622

let ck = clock_standard_args env elist in

623

expr.expr_clock < ck;

624

ck

625

 Expr_access (e1, d) >

626

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

627

let ck = clock_standard_args env [e1] in

628

expr.expr_clock < ck;

629

ck

630

 Expr_power (e1, d) >

631

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

632

let ck = clock_standard_args env [e1] in

633

expr.expr_clock < ck;

634

ck

635

 Expr_tuple elist >

636

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

637

expr.expr_clock < ck;

638

ck

639

 Expr_ite (c, t, e) >

640

let ck_c = clock_standard_args env [c] in

641

let ck = clock_standard_args env [t; e] in

642

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

643

unify_tuple_clock (Some ck_c) ck;

644

expr.expr_clock < ck;

645

ck

646

 Expr_appl (id, args, r) >

647

(try

648

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

649

this is also the reset clock !

650

*)

651

let cr =

652

match r with

653

 None > new_var true

654

 Some (x, _) > let loc_r = loc_of_cond expr.expr_loc x in

655

let expr_r = expr_of_ident x loc_r in

656

clock_expr env expr_r in

657

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

658

expr.expr_clock < couts;

659

couts

660

with exn > (

661

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

662

raise exn

663

))

664

 Expr_fby (e1,e2)

665

 Expr_arrow (e1,e2) >

666

let ck = clock_standard_args env [e1; e2] in

667

expr.expr_clock < ck;

668

ck

669

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

670

let ck = clock_standard_args env [e] in

671

expr.expr_clock < ck;

672

ck

673

 Expr_when (e,c,l) >

674

let ce = clock_standard_args env [e] in

675

let c_loc = loc_of_cond expr.expr_loc c in

676

let cr = clock_carrier env c c_loc ce in

677

let ck = new_ck (Con (ce,cr,l)) true in

678

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

679

let ck' = new_ck (Con (ce,cr',l)) true in

680

expr.expr_clock < ck';

681

ck

682

 Expr_merge (c,hl) >

683

let cvar = new_var true in

684

let cr = clock_carrier env c expr.expr_loc cvar in

685

List.iter (fun (t, h) > clock_subtyping_arg env h (new_ck (Con (cvar,cr,t)) true)) hl;

686

expr.expr_clock < cvar;

687

cvar

688

 Expr_uclock (e,k) >

689

let pck = clock_expr env e in

690

if not (can_be_pck pck) then

691

raise (Error (e.expr_loc, Not_pck));

692

if k = 0 then

693

raise (Error (expr.expr_loc, Factor_zero));

694

(try

695

subsume pck (CSet_pck (k,(0,1)))

696

with Subsume (ck,cset) >

697

raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (k,(0,1))))));

698

let ck = new_ck (Pck_up (pck,k)) true in

699

expr.expr_clock < ck;

700

ck

701

 Expr_dclock (e,k) >

702

let pck = clock_expr env e in

703

if not (can_be_pck pck) then

704

raise (Error (e.expr_loc, Not_pck));

705

if k = 0 then

706

raise (Error (expr.expr_loc, Factor_zero));

707

(try

708

subsume pck (CSet_pck (1,(0,1)))

709

with Subsume (ck,cset) >

710

raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (1,(0,1))))));

711

let ck = new_ck (Pck_down (pck,k)) true in

712

expr.expr_clock < ck;

713

ck

714

 Expr_phclock (e,(a,b)) >

715

let pck = clock_expr env e in

716

if not (can_be_pck pck) then

717

raise (Error (e.expr_loc, Not_pck));

718

let (a,b) = simplify_rat (a,b) in

719

(try

720

subsume pck (CSet_pck (b,(0,1)))

721

with Subsume (ck,cset) >

722

raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (b,(0,1))))));

723

let ck = new_ck (Pck_phase (pck,(a,b))) true in

724

expr.expr_clock < ck;

725

ck

726

in

727

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

728

resulting_ck

729


730

let clock_of_vlist vars =

731

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

732

clock_of_clock_list ckl

733


734

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

735

environment [env] *)

736

let clock_eq env eq =

737

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

738

let ck_rhs = clock_expr env eq.eq_rhs in

739

clock_subtyping_arg env expr_lhs ck_rhs

740


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) nd.node_eqs;

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;

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;

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_consts env clist =

865

List.fold_left (fun env cdecl >

866

let ck = new_var false in

867

try_generalize ck cdecl.const_loc;

868

Env.add_value env cdecl.const_id ck) env clist

869


870

let clock_top_decl env decl =

871

match decl.top_decl_desc with

872

 Node nd >

873

clock_node env decl.top_decl_loc nd

874

 ImportedNode nd >

875

clock_imported_node env decl.top_decl_loc nd

876

 Consts clist >

877

clock_top_consts env clist

878

 Open _ >

879

env

880


881

let clock_prog env decls =

882

List.fold_left (fun e decl > clock_top_decl e decl) env decls

883


884

(* Once the Lustre program is fully clocked,

885

we must get back to the original description of clocks,

886

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

887


888

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

889

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

890

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

891

*)

892

let uneval_vdecl_generics vdecl =

893

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

894

if Types.get_clock_base_type vdecl.var_type <> None

895

then

896

match get_carrier_name vdecl.var_clock with

897

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

898

 Some cr > Clocks.uneval vdecl.var_id cr

899


900

let uneval_node_generics vdecls =

901

List.iter uneval_vdecl_generics vdecls

902


903

let uneval_top_generics decl =

904

match decl.top_decl_desc with

905

 Node nd >

906

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

907

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

908

 ImportedNode nd >

909

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

910

 Consts clist > ()

911

 Open _ > ()

912


913

let uneval_prog_generics prog =

914

List.iter uneval_top_generics prog

915


916

let check_env_compat header declared computed =

917

uneval_prog_generics header;

918

Env.iter declared (fun k decl_clock_k >

919

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

920

try_semi_unify decl_clock_k computed_c Location.dummy_loc

921

)

922

(* Local Variables: *)

923

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

924

(* End: *)
