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

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

257

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

258

let rec unify ck1 ck2 =

259

let ck1 = repr ck1 in

260

let ck2 = repr ck2 in

261

if ck1=ck2 then

262

()

263

else

264

let left_const = is_concrete_pck ck1 in

265

let right_const = is_concrete_pck ck2 in

266

if left_const && right_const then

267

unify_static_pck ck1 ck2

268

else

269

match ck1.cdesc,ck2.cdesc with

270

 Cvar cset1,Cvar cset2>

271

if ck1.cid < ck2.cid then

272

begin

273

ck2.cdesc < Clink (simplify ck1);

274

update_scope ck2.cscoped ck1;

275

subsume ck1 cset2

276

end

277

else

278

begin

279

ck1.cdesc < Clink (simplify ck2);

280

update_scope ck1.cscoped ck2;

281

subsume ck2 cset1

282

end

283

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

284

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

285

if (occurs ck1 ck2) then

286

begin

287

if (simplify ck2 = ck1) then

288

ck2.cdesc < Clink (simplify ck1)

289

else

290

raise (Unify (ck1,ck2));

291

end

292

else

293

begin

294

ck1.cdesc < Clink (simplify ck2);

295

subsume ck2 cset

296

end

297

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

298

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

299

if (occurs ck2 ck1) then

300

begin

301

if ((simplify ck1) = ck2) then

302

ck1.cdesc < Clink (simplify ck2)

303

else

304

raise (Unify (ck1,ck2));

305

end

306

else

307

begin

308

ck2.cdesc < Clink (simplify ck1);

309

subsume ck1 cset

310

end

311

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

312

subsume ck2 cset;

313

update_scope ck1.cscoped ck2;

314

ck1.cdesc < Clink (simplify ck2)

315

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

316

subsume ck1 cset;

317

update_scope ck2.cscoped ck1;

318

ck2.cdesc < Clink (simplify ck1)

319

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

320

unify_carrier cr1 cr2;

321

unify ck1' ck2'

322

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

323

raise (Unify (ck1,ck2))

324

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

325

unify c1 c1'; unify c2 c2'

326

 Ctuple ckl1, Ctuple ckl2 >

327

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

328

raise (Unify (ck1,ck2));

329

List.iter2 unify ckl1 ckl2

330

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

331

unify_carrier c1 c2;

332

unify ck' ck''

333

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

334

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

335

raise (Unify (ck1,ck2))

336

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

337

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

338

unify ck1' pck2'

339

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

340

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

341

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

342

unify ck1' pck2'

343

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

344

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

345

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

346

unify ck1' pck2'

347

 Pck_up (pck1',k),_ >

348

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

349

unify pck1' ck2'

350

 Pck_down (pck1',k),_ >

351

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

352

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

353

unify pck1' ck2'

354

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

355

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

356

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

357

unify pck1' ck2'

358

(* Corner case for some functions like ite, need to unify guard clock

359

with output clocks *)

360

(*

361

 Ctuple ckl, (Cvar _) > List.iter (unify ck2) ckl

362

 (Cvar _), Ctuple ckl > List.iter (unify ck1) ckl

363

*)

364

 Cunivar _, _  _, Cunivar _ > ()

365

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

366


367

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

368

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

369

let int_factor_of_expr e =

370

match e.expr_desc with

371

 Expr_const

372

(Const_int i) > i

373

 _ > failwith "Internal error: int_factor_of_expr"

374


375

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

376

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

377

let unify_tuple_clock ref_ck_opt ck =

378

let ck_var = ref ref_ck_opt in

379

let rec aux ck =

380

match (repr ck).cdesc with

381

 Con _

382

 Cvar _ >

383

begin

384

match !ck_var with

385

 None >

386

ck_var:=Some ck

387

 Some v >

388

(* may fail *)

389

unify v ck

390

end

391

 Ctuple cl >

392

List.iter aux cl

393

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

394

 Ccarrying (_, ck1) >

395

aux ck1

396

 _ > ()

397

in

398

aux ck

399


400

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

401

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

402

that is, the activation clock of the node *)

403

let unify_imported_clock ref_ck_opt ck =

404

let ck_var = ref ref_ck_opt in

405

let rec aux ck =

406

match (repr ck).cdesc with

407

 Cvar _ >

408

begin

409

match !ck_var with

410

 None >

411

ck_var:=Some ck

412

 Some v >

413

(* cannot fail *)

414

unify v ck

415

end

416

 Ctuple cl >

417

List.iter aux cl

418

 Carrow (ck1,ck2) >

419

aux ck1; aux ck2

420

 Ccarrying (_, ck1) >

421

aux ck1

422

 Con (ck1, _, _) > aux ck1

423

 _ > ()

424

in

425

aux ck

426


427

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

428

let clock_uncarry ck =

429

let ck = repr ck in

430

match ck.cdesc with

431

 Ccarrying (_, ck') > ck'

432

 _ > ck

433


434

let try_unify ck1 ck2 loc =

435

try

436

unify ck1 ck2

437

with

438

 Unify (ck1',ck2') >

439

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

440

 Subsume (ck,cset) >

441

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

442

 Mismatch (cr1,cr2) >

443

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

444


445

(* Checks whether ck1 is a subtype of ck2 *)

446

let rec clock_subtyping ck1 ck2 =

447

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

448

 Ccarrying _ , Ccarrying _ > unify ck1 ck2

449

 Ccarrying (cr', ck'), _ > unify ck' ck2

450

 _ > unify ck1 ck2

451


452

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

453

 type each expression, remove carriers of clocks as

454

carriers may only denote variables, not arbitrary expr.

455

 try to unify these clocks altogether

456

*)

457

let rec clock_standard_args env expr_list =

458

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

459

let ck_res = new_var true in

460

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

461

ck_res

462


463

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

464

used during node application only *)

465

and clock_subtyping_arg env real_arg formal_clock =

466

let loc = real_arg.expr_loc in

467

let real_clock = clock_expr env real_arg in

468

try

469

clock_subtyping real_clock formal_clock

470

with

471

 Unify (ck1',ck2') >

472

raise (Error (loc, Clock_clash (real_clock, formal_clock)))

473

 Subsume (ck,cset) >

474

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

475

 Mismatch (cr1,cr2) >

476

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

477


478

(* computes clocks for node application *)

479

and clock_appl env f args clock_reset loc =

480

let cfun = clock_ident false env f loc in

481

let cins, couts = split_arrow cfun in

482

let cins = clock_list_of_clock cins in

483

let args = expr_list_of_expr args in

484

List.iter2 (clock_subtyping_arg env) args cins;

485

unify_imported_clock (Some clock_reset) cfun;

486

couts

487


488

and clock_ident nocarrier env id loc =

489

clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)

490


491

and clock_carrier env c loc ce =

492

let expr_c = expr_of_ident c loc in

493

let ck = clock_expr ~nocarrier:false env expr_c in

494

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

495

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

496

try_unify ck ckcarry expr_c.expr_loc;

497

cr

498


499

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

500

environment [env] *)

501

and clock_expr ?(nocarrier=true) env expr =

502

let resulting_ck =

503

match expr.expr_desc with

504

 Expr_const cst >

505

let ck = new_var true in

506

expr.expr_clock < ck;

507

ck

508

 Expr_ident v >

509

let ckv =

510

try

511

Env.lookup_value env v

512

with Not_found >

513

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

514

in

515

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

516

expr.expr_clock < ck;

517

ck

518

 Expr_array elist >

519

let ck = clock_standard_args env elist in

520

expr.expr_clock < ck;

521

ck

522

 Expr_access (e1, d) >

523

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

524

let ck = clock_standard_args env [e1] in

525

expr.expr_clock < ck;

526

ck

527

 Expr_power (e1, d) >

528

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

529

let ck = clock_standard_args env [e1] in

530

expr.expr_clock < ck;

531

ck

532

 Expr_tuple elist >

533

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

534

expr.expr_clock < ck;

535

ck

536

 Expr_ite (c, t, e) >

537

let ck_c = clock_standard_args env [c] in

538

let ck = clock_standard_args env [t; e] in

539

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

540

unify_tuple_clock (Some ck_c) ck;

541

expr.expr_clock < ck;

542

ck

543

 Expr_appl (id, args, r) >

544

(try

545

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

546

this is also the reset clock !

547

*)

548

let cr =

549

match r with

550

 None > new_var true

551

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

552

let expr_r = expr_of_ident x loc_r in

553

clock_expr env expr_r in

554

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

555

expr.expr_clock < couts;

556

couts

557

with exn > (

558

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

559

raise exn

560

))

561

 Expr_fby (e1,e2)

562

 Expr_arrow (e1,e2) >

563

let ck = clock_standard_args env [e1; e2] in

564

expr.expr_clock < ck;

565

ck

566

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

567

let ck = clock_standard_args env [e] in

568

expr.expr_clock < ck;

569

ck

570

 Expr_when (e,c,l) >

571

let ce = clock_standard_args env [e] in

572

let c_loc = loc_of_cond expr.expr_loc c in

573

let cr = clock_carrier env c c_loc ce in

574

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

575

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

576

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

577

expr.expr_clock < ck';

578

ck

579

 Expr_merge (c,hl) >

580

let cvar = new_var true in

581

let cr = clock_carrier env c expr.expr_loc cvar in

582

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

583

expr.expr_clock < cvar;

584

cvar

585

 Expr_uclock (e,k) >

586

let pck = clock_expr env e in

587

if not (can_be_pck pck) then

588

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

589

if k = 0 then

590

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

591

(try

592

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

593

with Subsume (ck,cset) >

594

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

595

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

596

expr.expr_clock < ck;

597

ck

598

 Expr_dclock (e,k) >

599

let pck = clock_expr env e in

600

if not (can_be_pck pck) then

601

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

602

if k = 0 then

603

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

604

(try

605

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

606

with Subsume (ck,cset) >

607

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

608

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

609

expr.expr_clock < ck;

610

ck

611

 Expr_phclock (e,(a,b)) >

612

let pck = clock_expr env e in

613

if not (can_be_pck pck) then

614

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

615

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

616

(try

617

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

618

with Subsume (ck,cset) >

619

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

620

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

621

expr.expr_clock < ck;

622

ck

623

in

624

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

625

resulting_ck

626


627

let clock_of_vlist vars =

628

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

629

clock_of_clock_list ckl

630


631

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

632

environment [env] *)

633

let clock_eq env eq =

634

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

635

let ck_rhs = clock_expr env eq.eq_rhs in

636

clock_subtyping_arg env expr_lhs ck_rhs

637


638


639

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

640

declaration [cck] *)

641

let clock_coreclock env cck id loc scoped =

642

match cck.ck_dec_desc with

643

 Ckdec_any > new_var scoped

644

 Ckdec_pclock (n,(a,b)) >

645

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

646

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

647

ck

648

 Ckdec_bool cl >

649

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

650

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

651

let dummy_id_expr = expr_of_ident id loc in

652

let when_expr =

653

List.fold_left

654

(fun expr (x,l) >

655

{expr_tag = new_tag ();

656

expr_desc = Expr_when (expr,x,l);

657

expr_type = Types.new_var ();

658

expr_clock = new_var scoped;

659

expr_delay = Delay.new_var ();

660

expr_loc = loc;

661

expr_annot = None})

662

dummy_id_expr cl

663

in

664

clock_expr temp_env when_expr

665


666

(* Clocks a variable declaration *)

667

let clock_var_decl scoped env vdecl =

668

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

669

let ck =

670

if vdecl.var_dec_const

671

then

672

(try_generalize ck vdecl.var_loc; ck)

673

else

674

match vdecl.var_type.Types.tdesc with

675

 Types.Tclock _ > new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped

676

 _ > ck in

677

vdecl.var_clock < ck;

678

Env.add_value env vdecl.var_id ck

679


680

(* Clocks a variable declaration list *)

681

let clock_var_decl_list env scoped l =

682

List.fold_left (clock_var_decl scoped) env l

683


684

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

685

environment [env]. *)

686

let clock_node env loc nd =

687

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

688

let new_env = clock_var_decl_list env false nd.node_inputs in

689

let new_env = clock_var_decl_list new_env true nd.node_outputs in

690

let new_env = clock_var_decl_list new_env true nd.node_locals in

691

List.iter (clock_eq new_env) nd.node_eqs;

692

let ck_ins = clock_of_vlist nd.node_inputs in

693

let ck_outs = clock_of_vlist nd.node_outputs in

694

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

695

unify_imported_clock None ck_node;

696

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

697

try_generalize ck_node loc;

698

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

699

(* if (is_main && is_polymorphic ck_node) then

700

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

701

*)

702

nd.node_clock < ck_node;

703

Env.add_value env nd.node_id ck_node

704


705


706

let check_imported_pclocks loc ck_node =

707

let pck = ref None in

708

let rec aux ck =

709

match ck.cdesc with

710

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

711

 Ctuple cl > List.iter aux cl

712

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

713

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

714

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

715

 Pck_const (n,p) >

716

begin

717

match !pck with

718

 None > pck := Some (n,p)

719

 Some (n',p') >

720

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

721

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

722

end

723

 Clink ck' > aux ck'

724

 Ccarrying (_,ck') > aux ck'

725

 Cvar _  Cunivar _ >

726

match !pck with

727

 None > ()

728

 Some (_,_) >

729

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

730

in

731

aux ck_node

732


733

let clock_imported_node env loc nd =

734

let new_env = clock_var_decl_list env false nd.nodei_inputs in

735

ignore(clock_var_decl_list new_env false nd.nodei_outputs);

736

let ck_ins = clock_of_vlist nd.nodei_inputs in

737

let ck_outs = clock_of_vlist nd.nodei_outputs in

738

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

739

unify_imported_clock None ck_node;

740

check_imported_pclocks loc ck_node;

741

try_generalize ck_node loc;

742

nd.nodei_clock < ck_node;

743

Env.add_value env nd.nodei_id ck_node

744


745

let clock_function env loc fcn =

746

let new_env = clock_var_decl_list env false fcn.fun_inputs in

747

ignore(clock_var_decl_list new_env false fcn.fun_outputs);

748

let ck_ins = clock_of_vlist fcn.fun_inputs in

749

let ck_outs = clock_of_vlist fcn.fun_outputs in

750

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

751

unify_imported_clock None ck_node;

752

check_imported_pclocks loc ck_node;

753

try_generalize ck_node loc;

754

Env.add_value env fcn.fun_id ck_node

755


756

let clock_top_consts env clist =

757

List.fold_left (fun env cdecl >

758

let ck = new_var false in

759

try_generalize ck cdecl.const_loc;

760

Env.add_value env cdecl.const_id ck) env clist

761


762

let clock_top_decl env decl =

763

match decl.top_decl_desc with

764

 Node nd >

765

clock_node env decl.top_decl_loc nd

766

 ImportedNode nd >

767

clock_imported_node env decl.top_decl_loc nd

768

 ImportedFun fcn >

769

clock_function env decl.top_decl_loc fcn

770

 Consts clist >

771

clock_top_consts env clist

772

 Open _ >

773

env

774


775

let clock_prog env decls =

776

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

777


778

let check_env_compat header declared computed =

779

Env.iter declared (fun k decl_clock_k >

780

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

781

try_unify decl_clock_k computed_c Location.dummy_loc

782

)

783

(* Local Variables: *)

784

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

785

(* End: *)
