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 name from clock [ck] *)

445

let clock_uncarry ck =

446

let ck = repr ck in

447

match ck.cdesc with

448

 Ccarrying (_, ck') > ck'

449

 _ > ck

450


451

let try_unify ck1 ck2 loc =

452

try

453

unify ck1 ck2

454

with

455

 Unify (ck1',ck2') >

456

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

457

 Subsume (ck,cset) >

458

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

459

 Mismatch (cr1,cr2) >

460

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

461


462

let try_semi_unify ck1 ck2 loc =

463

try

464

semi_unify ck1 ck2

465

with

466

 Unify (ck1',ck2') >

467

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

468

 Subsume (ck,cset) >

469

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

470

 Mismatch (cr1,cr2) >

471

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

472


473

(* ck2 is a subtype of ck1 *)

474

let rec sub_unify sub ck1 ck2 =

475

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

476

 Ctuple cl1 , Ctuple cl2 >

477

if List.length cl1 <> List.length cl2

478

then raise (Unify (ck1, ck2))

479

else List.iter2 (sub_unify sub) cl1 cl2

480

 Ctuple [c1] , _ > sub_unify sub c1 ck2

481

 _ , Ctuple [c2] > sub_unify sub ck1 c2

482

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

483

begin

484

unify_carrier cr1 cr2;

485

sub_unify sub c1 c2

486

end

487

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

488

begin

489

unify_carrier cr1 cr2;

490

sub_unify sub c1 c2

491

end

492

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

493

 _ > unify ck1 ck2

494


495

let try_sub_unify sub ck1 ck2 loc =

496

try

497

sub_unify sub ck1 ck2

498

with

499

 Unify (ck1',ck2') >

500

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

501

 Subsume (ck,cset) >

502

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

503

 Mismatch (cr1,cr2) >

504

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

505


506

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

507

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

508

let unify_tuple_clock ref_ck_opt ck loc =

509

(*(match ref_ck_opt with

510

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

511

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

512

let ck_var = ref ref_ck_opt in

513

let rec aux ck =

514

match (repr ck).cdesc with

515

 Con _

516

 Cvar _ >

517

begin

518

match !ck_var with

519

 None >

520

ck_var:=Some ck

521

 Some v >

522

(* may fail *)

523

try_unify ck v loc

524

end

525

 Ctuple cl >

526

List.iter aux cl

527

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

528

 Ccarrying (_, ck1) >

529

aux ck1

530

 _ > ()

531

in aux ck

532


533

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

534

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

535

that is, the activation clock of the node *)

536

let unify_imported_clock ref_ck_opt ck loc =

537

let ck_var = ref ref_ck_opt in

538

let rec aux ck =

539

match (repr ck).cdesc with

540

 Cvar _ >

541

begin

542

match !ck_var with

543

 None >

544

ck_var:=Some ck

545

 Some v >

546

(* cannot fail *)

547

try_unify ck v loc

548

end

549

 Ctuple cl >

550

List.iter aux cl

551

 Carrow (ck1,ck2) >

552

aux ck1; aux ck2

553

 Ccarrying (_, ck1) >

554

aux ck1

555

 Con (ck1, _, _) > aux ck1

556

 _ > ()

557

in

558

aux ck

559


560

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

561

 type each expression, remove carriers of clocks as

562

carriers may only denote variables, not arbitrary expr.

563

 try to unify these clocks altogether

564

*)

565

let rec clock_standard_args env expr_list =

566

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

567

let ck_res = new_var true in

568

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

569

ck_res

570


571

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

572

used during node application only *)

573

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

574

let loc = real_arg.expr_loc in

575

let real_clock = clock_expr env real_arg in

576

try_sub_unify sub formal_clock real_clock loc

577


578

(* computes clocks for node application *)

579

and clock_appl env f args clock_reset loc =

580

let args = expr_list_of_expr args in

581

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

582

then

583

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

584

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

585

else

586

clock_call env f args clock_reset loc

587


588

and clock_call env f args clock_reset loc =

589

let cfun = clock_ident false env f loc in

590

let cins, couts = split_arrow cfun in

591

let cins = clock_list_of_clock cins in

592

List.iter2 (clock_subtyping_arg env) args cins;

593

unify_imported_clock (Some clock_reset) cfun loc;

594

couts

595


596

and clock_ident nocarrier env id loc =

597

clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)

598


599

and clock_carrier env c loc ce =

600

let expr_c = expr_of_ident c loc in

601

let ck = clock_expr ~nocarrier:false env expr_c in

602

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

603

let ckb = new_var true in

604

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

605

try_unify ck ckcarry expr_c.expr_loc;

606

unify_tuple_clock (Some ckb) ce expr_c.expr_loc;

607

cr

608


609

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

610

environment [env] *)

611

and clock_expr ?(nocarrier=true) env expr =

612

let resulting_ck =

613

match expr.expr_desc with

614

 Expr_const cst >

615

let ck = new_var true in

616

expr.expr_clock < ck;

617

ck

618

 Expr_ident v >

619

let ckv =

620

try

621

Env.lookup_value env v

622

with Not_found >

623

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

624

in

625

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

626

expr.expr_clock < ck;

627

ck

628

 Expr_array elist >

629

let ck = clock_standard_args env elist in

630

expr.expr_clock < ck;

631

ck

632

 Expr_access (e1, d) >

633

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

634

let ck = clock_standard_args env [e1] in

635

expr.expr_clock < ck;

636

ck

637

 Expr_power (e1, d) >

638

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

639

let ck = clock_standard_args env [e1] in

640

expr.expr_clock < ck;

641

ck

642

 Expr_tuple elist >

643

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

644

expr.expr_clock < ck;

645

ck

646

 Expr_ite (c, t, e) >

647

let ck_c = clock_standard_args env [c] in

648

let ck = clock_standard_args env [t; e] in

649

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

650

unify_tuple_clock (Some ck_c) ck expr.expr_loc;

651

expr.expr_clock < ck;

652

ck

653

 Expr_appl (id, args, r) >

654

(try

655

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

656

this is also the reset clock !

657

*)

658

let cr =

659

match r with

660

 None > new_var true

661

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

662

let expr_r = expr_of_ident x loc_r in

663

clock_expr env expr_r in

664

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

665

expr.expr_clock < couts;

666

couts

667

with exn > (

668

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

669

raise exn

670

))

671

 Expr_fby (e1,e2)

672

 Expr_arrow (e1,e2) >

673

let ck = clock_standard_args env [e1; e2] in

674

unify_tuple_clock None ck expr.expr_loc;

675

expr.expr_clock < ck;

676

ck

677

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

678

let ck = clock_standard_args env [e] in

679

expr.expr_clock < ck;

680

ck

681

 Expr_when (e,c,l) >

682

let ce = clock_standard_args env [e] in

683

let c_loc = loc_of_cond expr.expr_loc c in

684

let cr = clock_carrier env c c_loc ce in

685

let ck = clock_on ce cr l in

686

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

687

let ck' = clock_on ce cr' l in

688

expr.expr_clock < ck';

689

ck

690

 Expr_merge (c,hl) >

691

let cvar = new_var true in

692

let crvar = new_carrier Carry_name true in

693

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

694

let cr = clock_carrier env c expr.expr_loc cvar in

695

try_unify_carrier cr crvar expr.expr_loc;

696

expr.expr_clock < cvar;

697

cvar

698

in

699

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

700

resulting_ck

701


702

let clock_of_vlist vars =

703

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

704

clock_of_clock_list ckl

705


706

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

707

environment [env] *)

708

let clock_eq env eq =

709

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

710

let ck_rhs = clock_expr env eq.eq_rhs in

711

clock_subtyping_arg env expr_lhs ck_rhs

712


713

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

714

declaration [cck] *)

715

let clock_coreclock env cck id loc scoped =

716

match cck.ck_dec_desc with

717

 Ckdec_any > new_var scoped

718

 Ckdec_pclock (n,(a,b)) >

719

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

720

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

721

ck

722

 Ckdec_bool cl >

723

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

724

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

725

let dummy_id_expr = expr_of_ident id loc in

726

let when_expr =

727

List.fold_left

728

(fun expr (x,l) >

729

{expr_tag = new_tag ();

730

expr_desc = Expr_when (expr,x,l);

731

expr_type = Types.new_var ();

732

expr_clock = new_var scoped;

733

expr_delay = Delay.new_var ();

734

expr_loc = loc;

735

expr_annot = None})

736

dummy_id_expr cl

737

in

738

clock_expr temp_env when_expr

739


740

(* Clocks a variable declaration *)

741

let clock_var_decl scoped env vdecl =

742

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

743

let ck =

744

(* WTF ????

745

if vdecl.var_dec_const

746

then

747

(try_generalize ck vdecl.var_loc; ck)

748

else

749

*)

750

if Types.get_clock_base_type vdecl.var_type <> None

751

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

752

else ck in

753

vdecl.var_clock < ck;

754

Env.add_value env vdecl.var_id ck

755


756

(* Clocks a variable declaration list *)

757

let clock_var_decl_list env scoped l =

758

List.fold_left (clock_var_decl scoped) env l

759


760

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

761

environment [env].

762

Generalization of clocks wrt scopes follows this rule:

763

 generalize inputs (unscoped).

764

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

765

are allowed to be generalized.

766

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

767

they can be generalized.

768

*)

769

let clock_node env loc nd =

770

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

771

let new_env = clock_var_decl_list env false nd.node_inputs in

772

let new_env = clock_var_decl_list new_env true nd.node_outputs in

773

let new_env = clock_var_decl_list new_env true nd.node_locals in

774

List.iter (clock_eq new_env) nd.node_eqs;

775

let ck_ins = clock_of_vlist nd.node_inputs in

776

let ck_outs = clock_of_vlist nd.node_outputs in

777

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

778

unify_imported_clock None ck_node loc;

779

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

780

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

781

That's not the case for types. *)

782

try_generalize ck_node loc;

783

(*

784

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

785

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

786

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

787

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

788

(* if (is_main && is_polymorphic ck_node) then

789

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

790

*)

791

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

792

nd.node_clock < ck_node;

793

Env.add_value env nd.node_id ck_node

794


795


796

let check_imported_pclocks loc ck_node =

797

let pck = ref None in

798

let rec aux ck =

799

match ck.cdesc with

800

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

801

 Ctuple cl > List.iter aux cl

802

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

803

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

804

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

805

 Pck_const (n,p) >

806

begin

807

match !pck with

808

 None > pck := Some (n,p)

809

 Some (n',p') >

810

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

811

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

812

end

813

 Clink ck' > aux ck'

814

 Ccarrying (_,ck') > aux ck'

815

 Cvar _  Cunivar _ >

816

match !pck with

817

 None > ()

818

 Some (_,_) >

819

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

820

in

821

aux ck_node

822


823

let clock_imported_node env loc nd =

824

let new_env = clock_var_decl_list env false nd.nodei_inputs in

825

ignore(clock_var_decl_list new_env false nd.nodei_outputs);

826

let ck_ins = clock_of_vlist nd.nodei_inputs in

827

let ck_outs = clock_of_vlist nd.nodei_outputs in

828

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

829

unify_imported_clock None ck_node loc;

830

check_imported_pclocks loc ck_node;

831

try_generalize ck_node loc;

832

nd.nodei_clock < ck_node;

833

Env.add_value env nd.nodei_id ck_node

834


835

let clock_top_consts env clist =

836

List.fold_left (fun env cdecl >

837

let ck = new_var false in

838

try_generalize ck cdecl.const_loc;

839

Env.add_value env cdecl.const_id ck) env clist

840


841

let clock_top_decl env decl =

842

match decl.top_decl_desc with

843

 Node nd >

844

clock_node env decl.top_decl_loc nd

845

 ImportedNode nd >

846

clock_imported_node env decl.top_decl_loc nd

847

 Consts clist >

848

clock_top_consts env clist

849

 Open _ >

850

env

851


852

let clock_prog env decls =

853

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

854


855

(* Once the Lustre program is fully clocked,

856

we must get back to the original description of clocks,

857

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

858


859

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

860

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

861

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

862

*)

863

let uneval_vdecl_generics vdecl =

864

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

865

if Types.get_clock_base_type vdecl.var_type <> None

866

then

867

match get_carrier_name vdecl.var_clock with

868

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

869

 Some cr > Clocks.uneval vdecl.var_id cr

870


871

let uneval_node_generics vdecls =

872

List.iter uneval_vdecl_generics vdecls

873


874

let uneval_top_generics decl =

875

match decl.top_decl_desc with

876

 Node nd >

877

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

878

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

879

 ImportedNode nd >

880

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

881

 Consts clist > ()

882

 Open _ > ()

883


884

let uneval_prog_generics prog =

885

List.iter uneval_top_generics prog

886


887

let check_env_compat header declared computed =

888

uneval_prog_generics header;

889

Env.iter declared (fun k decl_clock_k >

890

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

891

try_semi_unify decl_clock_k computed_c Location.dummy_loc

892

)

893

(* Local Variables: *)

894

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

895

(* End: *)
