1

(********************************************************************)

2

(* *)

3

(* The LustreC compiler toolset / The LustreC Development Team *)

4

(* Copyright 2012   ONERA  CNRS  INPT  LIFL *)

5

(* *)

6

(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)

7

(* under the terms of the GNU Lesser General Public License *)

8

(* version 2.1. *)

9

(* *)

10

(* This file was originally from the Prelude compiler *)

11

(* *)

12

(********************************************************************)

13


14


15

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

16

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

17


18

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

19

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

20

identifier redefinition allowed. *)

21

open Utils

22

open Lustre_types

23

open Corelang

24

open Clocks

25


26

let loc_of_cond (_s, e) id =

27

let pos_start =

28

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

29

in

30

pos_start, e

31


32

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

33

clock [ck]. False otherwise. *)

34

let rec occurs cvar ck =

35

let ck = repr ck in

36

match ck.cdesc with

37

 Carrow (ck1, ck2) >

38

(occurs cvar ck1)  (occurs cvar ck2)

39

 Ctuple ckl >

40

List.exists (occurs cvar) ckl

41

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

42

 Cvar > ck=cvar

43

 Cunivar > false

44

 Clink ck' > occurs cvar ck'

45

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

46


47

(* Clocks generalization *)

48

let rec generalize_carrier cr =

49

match cr.carrier_desc with

50

 Carry_const _

51

 Carry_name >

52

if cr.carrier_scoped then

53

raise (Scope_carrier cr);

54

cr.carrier_desc < Carry_var

55

 Carry_var > ()

56

 Carry_link cr' > generalize_carrier cr'

57


58

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

59

(* Generalize by sideeffects *)

60

let rec generalize ck =

61

match ck.cdesc with

62

 Carrow (ck1,ck2) >

63

generalize ck1; generalize ck2

64

 Ctuple clist >

65

List.iter generalize clist

66

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

67

 Cvar >

68

if ck.cscoped then

69

raise (Scope_clock ck);

70

ck.cdesc < Cunivar

71

 Cunivar > ()

72

 Clink ck' >

73

generalize ck'

74

 Ccarrying (cr,ck') >

75

generalize_carrier cr; generalize ck'

76


77

let try_generalize ck_node loc =

78

try

79

generalize ck_node

80

with

81

 Scope_carrier cr >

82

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

83

 Scope_clock ck >

84

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

85


86

(* Clocks instanciation *)

87

let instantiate_carrier cr inst_cr_vars =

88

let cr = carrier_repr cr in

89

match cr.carrier_desc with

90

 Carry_const _

91

 Carry_name > cr

92

 Carry_link _ >

93

failwith "Internal error"

94

 Carry_var >

95

try

96

List.assoc cr.carrier_id !inst_cr_vars

97

with Not_found >

98

let cr_var = new_carrier Carry_name true in

99

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

100

cr_var

101


102

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

103

(* inst_ck_vars ensures that a polymorphic variable is instanciated with

104

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

105

type. inst_cr_vars is the same for carriers. *)

106

let rec instantiate inst_ck_vars inst_cr_vars ck =

107

match ck.cdesc with

108

 Carrow (ck1,ck2) >

109

{ck with cdesc =

110

Carrow ((instantiate inst_ck_vars inst_cr_vars ck1),

111

(instantiate inst_ck_vars inst_cr_vars ck2))}

112

 Ctuple cklist >

113

{ck with cdesc = Ctuple

114

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

115

 Con (ck',c,l) >

116

let c' = instantiate_carrier c inst_cr_vars in

117

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

118

 Cvar > ck

119

 Clink ck' >

120

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

121

 Ccarrying (cr,ck') >

122

let cr' = instantiate_carrier cr inst_cr_vars in

123

{ck with cdesc =

124

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

125

 Cunivar >

126

try

127

List.assoc ck.cid !inst_ck_vars

128

with Not_found >

129

let var = new_ck Cvar true in

130

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

131

var

132


133


134

let rec update_scope_carrier scoped cr =

135

if (not scoped) then

136

begin

137

cr.carrier_scoped < scoped;

138

match cr.carrier_desc with

139

 Carry_const _  Carry_name  Carry_var > ()

140

 Carry_link cr' > update_scope_carrier scoped cr'

141

end

142


143

let rec update_scope scoped ck =

144

if (not scoped) then

145

begin

146

ck.cscoped < scoped;

147

match ck.cdesc with

148

 Carrow (ck1,ck2) >

149

update_scope scoped ck1; update_scope scoped ck2

150

 Ctuple clist >

151

List.iter (update_scope scoped) clist

152

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

153

 Cvar  Cunivar > ()

154

 Clink ck' >

155

update_scope scoped ck'

156

 Ccarrying (cr,ck') >

157

update_scope_carrier scoped cr; update_scope scoped ck'

158

end

159


160


161

(* Unifies two clock carriers *)

162

let unify_carrier cr1 cr2 =

163

let cr1 = carrier_repr cr1 in

164

let cr2 = carrier_repr cr2 in

165

if cr1==cr2 then ()

166

else

167

match cr1.carrier_desc, cr2.carrier_desc with

168

 Carry_const id1, Carry_const id2 >

169

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

170

 Carry_const _, Carry_name >

171

begin

172

cr2.carrier_desc < Carry_link cr1;

173

update_scope_carrier cr2.carrier_scoped cr1

174

end

175

 Carry_name, Carry_const _ >

176

begin

177

cr1.carrier_desc < Carry_link cr2;

178

update_scope_carrier cr1.carrier_scoped cr2

179

end

180

 Carry_name, Carry_name >

181

if cr1.carrier_id < cr2.carrier_id then

182

begin

183

cr2.carrier_desc < Carry_link cr1;

184

update_scope_carrier cr2.carrier_scoped cr1

185

end

186

else

187

begin

188

cr1.carrier_desc < Carry_link cr2;

189

update_scope_carrier cr1.carrier_scoped cr2

190

end

191

 _,_ > assert false

192


193

(* Semiunifies two clock carriers *)

194

let semi_unify_carrier cr1 cr2 =

195

let cr1 = carrier_repr cr1 in

196

let cr2 = carrier_repr cr2 in

197

if cr1==cr2 then ()

198

else

199

match cr1.carrier_desc, cr2.carrier_desc with

200

 Carry_const id1, Carry_const id2 >

201

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

202

 Carry_const _, Carry_name >

203

begin

204

cr2.carrier_desc < Carry_link cr1;

205

update_scope_carrier cr2.carrier_scoped cr1

206

end

207

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

208

 Carry_name, Carry_name >

209

if cr1.carrier_id < cr2.carrier_id then

210

begin

211

cr2.carrier_desc < Carry_link cr1;

212

update_scope_carrier cr2.carrier_scoped cr1

213

end

214

else

215

begin

216

cr1.carrier_desc < Carry_link cr2;

217

update_scope_carrier cr1.carrier_scoped cr2

218

end

219

 _,_ > assert false

220


221

let try_unify_carrier ck1 ck2 loc =

222

try

223

unify_carrier ck1 ck2

224

with

225

 Unify (ck1',ck2') >

226

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

227

 Mismatch (cr1,cr2) >

228

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

229


230

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

231

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

232

let rec unify ck1 ck2 =

233

let ck1 = repr ck1 in

234

let ck2 = repr ck2 in

235

if ck1==ck2 then

236

()

237

else

238

match ck1.cdesc,ck2.cdesc with

239

 Cvar, Cvar >

240

if ck1.cid < ck2.cid then

241

begin

242

ck2.cdesc < Clink (simplify ck1);

243

update_scope ck2.cscoped ck1

244

end

245

else

246

begin

247

ck1.cdesc < Clink (simplify ck2);

248

update_scope ck1.cscoped ck2

249

end

250

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

251

update_scope ck1.cscoped ck2;

252

ck1.cdesc < Clink (simplify ck2)

253

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

254

update_scope ck2.cscoped ck1;

255

ck2.cdesc < Clink (simplify ck1)

256

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

257

unify_carrier cr1 cr2;

258

unify ck1' ck2'

259

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

260

raise (Unify (ck1,ck2))

261

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

262

unify c1 c1'; unify c2 c2'

263

 Ctuple ckl1, Ctuple ckl2 >

264

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

265

raise (Unify (ck1,ck2));

266

List.iter2 unify ckl1 ckl2

267

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

268

unify_carrier c1 c2;

269

unify ck' ck''

270

 Cunivar, _  _, Cunivar > ()

271

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

272


273

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

274

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

275

let rec semi_unify ck1 ck2 =

276

let ck1 = repr ck1 in

277

let ck2 = repr ck2 in

278

if ck1==ck2 then

279

()

280

else

281

match ck1.cdesc,ck2.cdesc with

282

 Cvar, Cvar >

283

if ck1.cid < ck2.cid then

284

begin

285

ck2.cdesc < Clink (simplify ck1);

286

update_scope ck2.cscoped ck1

287

end

288

else

289

begin

290

ck1.cdesc < Clink (simplify ck2);

291

update_scope ck1.cscoped ck2

292

end

293

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

294

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

295

update_scope ck2.cscoped ck1;

296

ck2.cdesc < Clink (simplify ck1)

297

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

298

semi_unify_carrier cr1 cr2;

299

semi_unify ck1' ck2'

300

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

301

raise (Unify (ck1,ck2))

302

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

303

begin

304

semi_unify c1 c1';

305

semi_unify c2 c2'

306

end

307

 Ctuple ckl1, Ctuple ckl2 >

308

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

309

raise (Unify (ck1,ck2));

310

List.iter2 semi_unify ckl1 ckl2

311

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

312

semi_unify_carrier c1 c2;

313

semi_unify ck' ck''

314

 Cunivar, _  _, Cunivar > ()

315

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

316


317

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

318

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

319

let int_factor_of_expr e =

320

match e.expr_desc with

321

 Expr_const

322

(Const_int i) > i

323

 _ > failwith "Internal error: int_factor_of_expr"

324


325

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

326

let rec clock_uncarry ck =

327

let ck = repr ck in

328

match ck.cdesc with

329

 Ccarrying (_, ck') > ck'

330

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

331

 Ctuple ckl > clock_of_clock_list (List.map clock_uncarry ckl)

332

 _ > ck

333


334

let try_unify ck1 ck2 loc =

335

try

336

unify ck1 ck2

337

with

338

 Unify (ck1',ck2') >

339

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

340

 Mismatch (cr1,cr2) >

341

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

342


343

let try_semi_unify ck1 ck2 loc =

344

try

345

semi_unify ck1 ck2

346

with

347

 Unify (ck1',ck2') >

348

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

349

 Mismatch (cr1,cr2) >

350

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

351


352

(* ck2 is a subtype of ck1 *)

353

let rec sub_unify sub ck1 ck2 =

354

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

355

 Ctuple cl1 , Ctuple cl2 >

356

if List.length cl1 <> List.length cl2

357

then raise (Unify (ck1, ck2))

358

else List.iter2 (sub_unify sub) cl1 cl2

359

 Ctuple [c1] , _ > sub_unify sub c1 ck2

360

 _ , Ctuple [c2] > sub_unify sub ck1 c2

361

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

362

begin

363

unify_carrier cr1 cr2;

364

sub_unify sub c1 c2

365

end

366

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

367

begin

368

unify_carrier cr1 cr2;

369

sub_unify sub c1 c2

370

end

371

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

372

 _ > unify ck1 ck2

373


374

let try_sub_unify sub ck1 ck2 loc =

375

try

376

sub_unify sub ck1 ck2

377

with

378

 Unify (ck1',ck2') >

379

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

380

 Mismatch (cr1,cr2) >

381

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

382


383

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

384

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

385

let unify_tuple_clock ref_ck_opt ck loc =

386

(*(match ref_ck_opt with

387

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

388

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

389

let ck_var = ref ref_ck_opt in

390

let rec aux ck =

391

match (repr ck).cdesc with

392

 Con _

393

 Cvar >

394

begin

395

match !ck_var with

396

 None >

397

ck_var:=Some ck

398

 Some v >

399

(* may fail *)

400

try_unify ck v loc

401

end

402

 Ctuple cl >

403

List.iter aux cl

404

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

405

 Ccarrying (_, ck1) >

406

aux ck1

407

 _ > ()

408

in aux ck

409


410

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

411

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

412

that is, the activation clock of the node *)

413

let unify_imported_clock ref_ck_opt ck loc =

414

let ck_var = ref ref_ck_opt in

415

let rec aux ck =

416

match (repr ck).cdesc with

417

 Cvar >

418

begin

419

match !ck_var with

420

 None >

421

ck_var := Some ck

422

 Some v >

423

(* cannot fail *)

424

try_unify ck v loc

425

end

426

 Ctuple cl >

427

List.iter aux cl

428

 Carrow (ck1,ck2) >

429

aux ck1; aux ck2

430

 Ccarrying (_, ck1) >

431

aux ck1

432

 Con (ck1, _, _) > aux ck1

433

 _ > ()

434

in

435

aux ck

436


437

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

438

which is not the same as the base clock.

439

Root clock will be used as the call clock

440

of a given node instance *)

441

let compute_root_clock ck =

442

let root = Clocks.root ck in

443

let branch = ref None in

444

let rec aux ck =

445

match (repr ck).cdesc with

446

 Ctuple cl >

447

List.iter aux cl

448

 Carrow (ck1,ck2) >

449

aux ck1; aux ck2

450

 _ >

451

begin

452

match !branch with

453

 None >

454

branch := Some (Clocks.branch ck)

455

 Some br >

456

(* cannot fail *)

457

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

458

end

459

in

460

begin

461

aux ck;

462

Clocks.clock_of_root_branch root (Utils.desome !branch)

463

end

464


465

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

466

 type each expression, remove carriers of clocks as

467

carriers may only denote variables, not arbitrary expr.

468

 try to unify these clocks altogether

469

*)

470

let rec clock_standard_args env expr_list =

471

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

472

let ck_res = new_var true in

473

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

474

ck_res

475


476

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

477

used during node application only *)

478

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

479

let loc = real_arg.expr_loc in

480

let real_clock = clock_expr env real_arg in

481

try_sub_unify sub formal_clock real_clock loc

482


483

(* computes clocks for node application *)

484

and clock_appl env f args clock_reset loc =

485

let args = expr_list_of_expr args in

486

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

487

then

488

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

489

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

490

else

491

clock_call env f args clock_reset loc

492


493

and clock_call env f args clock_reset loc =

494

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

495

let cfun = clock_ident false env f loc in

496

let cins, couts = split_arrow cfun in

497

let cins = clock_list_of_clock cins in

498

List.iter2 (clock_subtyping_arg env) args cins;

499

unify_imported_clock (Some clock_reset) cfun loc;

500

couts

501


502

and clock_ident nocarrier env id loc =

503

clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)

504


505

and clock_carrier env c loc ce =

506

let expr_c = expr_of_ident c loc in

507

let ck = clock_expr ~nocarrier:false env expr_c in

508

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

509

let ckb = new_var true in

510

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

511

try_unify ck ckcarry expr_c.expr_loc;

512

unify_tuple_clock (Some ckb) ce expr_c.expr_loc;

513

cr

514


515

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

516

environment [env] *)

517

and clock_expr ?(nocarrier=true) env expr =

518

let resulting_ck =

519

match expr.expr_desc with

520

 Expr_const _ >

521

let ck = new_var true in

522

expr.expr_clock < ck;

523

ck

524

 Expr_ident v >

525

let ckv =

526

try

527

Env.lookup_value env v

528

with Not_found >

529

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

530

in

531

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

532

expr.expr_clock < ck;

533

ck

534

 Expr_array elist >

535

let ck = clock_standard_args env elist in

536

expr.expr_clock < ck;

537

ck

538

 Expr_access (e1, _) >

539

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

540

let ck = clock_standard_args env [e1] in

541

expr.expr_clock < ck;

542

ck

543

 Expr_power (e1, _) >

544

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

545

let ck = clock_standard_args env [e1] in

546

expr.expr_clock < ck;

547

ck

548

 Expr_tuple elist >

549

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

550

expr.expr_clock < ck;

551

ck

552

 Expr_ite (c, t, e) >

553

let ck_c = clock_standard_args env [c] in

554

let ck = clock_standard_args env [t; e] in

555

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

556

unify_tuple_clock (Some ck_c) ck expr.expr_loc;

557

expr.expr_clock < ck;

558

ck

559

 Expr_appl (id, args, r) >

560

(try

561

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

562

this is also the reset clock !

563

*)

564

let cr =

565

match r with

566

 None > new_var true

567

 Some c > clock_standard_args env [c] in

568

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

569

expr.expr_clock < couts;

570

couts

571

with exn > (

572

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

573

raise exn

574

))

575

 Expr_fby (e1,e2)

576

 Expr_arrow (e1,e2) >

577

let ck = clock_standard_args env [e1; e2] in

578

unify_tuple_clock None ck expr.expr_loc;

579

expr.expr_clock < ck;

580

ck

581

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

582

let ck = clock_standard_args env [e] in

583

expr.expr_clock < ck;

584

ck

585

 Expr_when (e,c,l) >

586

let ce = clock_standard_args env [e] in

587

let c_loc = loc_of_cond expr.expr_loc c in

588

let cr = clock_carrier env c c_loc ce in

589

let ck = clock_on ce cr l in

590

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

591

let ck' = clock_on ce cr' l in

592

expr.expr_clock < ck';

593

ck

594

 Expr_merge (c,hl) >

595

let cvar = new_var true in

596

let crvar = new_carrier Carry_name true in

597

List.iter (fun (t, h) >

598

let ckh = clock_uncarry (clock_expr env h) in

599

unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;

600

let cr = clock_carrier env c expr.expr_loc cvar in

601

try_unify_carrier cr crvar expr.expr_loc;

602

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

603

expr.expr_clock < cres;

604

cres

605

in

606

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

607

Printers.pp_expr expr Clocks.print_ck resulting_ck);

608

resulting_ck

609


610

let clock_of_vlist vars =

611

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

612

clock_of_clock_list ckl

613


614

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

615

environment [env] *)

616

let clock_eq env eq =

617

let expr_lhs = expr_of_expr_list eq.eq_loc

618

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

619

let ck_rhs = clock_expr env eq.eq_rhs in

620

clock_subtyping_arg env expr_lhs ck_rhs

621


622

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

623

declaration [cck] *)

624

let clock_coreclock env cck id loc scoped =

625

match cck.ck_dec_desc with

626

 Ckdec_any > new_var scoped

627

 Ckdec_bool cl >

628

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

629

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

630

let dummy_id_expr = expr_of_ident id loc in

631

let when_expr =

632

List.fold_left

633

(fun expr (x,l) >

634

{expr_tag = new_tag ();

635

expr_desc = Expr_when (expr,x,l);

636

expr_type = Types.new_var ();

637

expr_clock = new_var scoped;

638

expr_delay = Delay.new_var ();

639

expr_loc = loc;

640

expr_annot = None})

641

dummy_id_expr cl

642

in

643

clock_expr temp_env when_expr

644


645

(* Clocks a variable declaration *)

646

let clock_var_decl scoped env vdecl =

647

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

648

let ck =

649

(* WTF ????

650

if vdecl.var_dec_const

651

then

652

(try_generalize ck vdecl.var_loc; ck)

653

else

654

*)

655

if Types.get_clock_base_type vdecl.var_type <> None

656

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

657

else ck in

658

(if vdecl.var_dec_const

659

then match vdecl.var_dec_value with

660

 None > ()

661

 Some v >

662

begin

663

let ck_static = clock_expr env v in

664

try_unify ck ck_static v.expr_loc

665

end);

666

try_unify ck vdecl.var_clock vdecl.var_loc;

667

Env.add_value env vdecl.var_id ck

668


669

(* Clocks a variable declaration list *)

670

let clock_var_decl_list env scoped l =

671

List.fold_left (clock_var_decl scoped) env l

672


673

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

674

environment [env].

675

Generalization of clocks wrt scopes follows this rule:

676

 generalize inputs (unscoped).

677

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

678

are allowed to be generalized.

679

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

680

they can be generalized.

681

*)

682

let clock_node env loc nd =

683

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

684

let new_env = clock_var_decl_list env false nd.node_inputs in

685

let new_env = clock_var_decl_list new_env true nd.node_outputs in

686

let new_env = clock_var_decl_list new_env true nd.node_locals in

687

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

688

For the moment, it is ignored *)

689

List.iter (clock_eq new_env) eqs;

690

let ck_ins = clock_of_vlist nd.node_inputs in

691

let ck_outs = clock_of_vlist nd.node_outputs in

692

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

693

unify_imported_clock None ck_node loc;

694

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

695

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

696

That's not the case for types. *)

697

try_generalize ck_node loc;

698

(*

699

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

700

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

701

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

702

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

703

(* if (is_main && is_polymorphic ck_node) then

704

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

705

*)

706

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

707

nd.node_clock < ck_node;

708

Env.add_value env nd.node_id ck_node

709


710


711

let check_imported_pclocks loc ck_node =

712

let pck = ref None in

713

let rec aux ck =

714

match ck.cdesc with

715

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

716

 Ctuple cl > List.iter aux cl

717

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

718

 Clink ck' > aux ck'

719

 Ccarrying (_,ck') > aux ck'

720

 Cvar  Cunivar >

721

match !pck with

722

 None > ()

723

 Some (_,_) >

724

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

725

in

726

aux ck_node

727


728

let clock_imported_node env loc nd =

729

let new_env = clock_var_decl_list env false nd.nodei_inputs in

730

ignore(clock_var_decl_list new_env false nd.nodei_outputs);

731

let ck_ins = clock_of_vlist nd.nodei_inputs in

732

let ck_outs = clock_of_vlist nd.nodei_outputs in

733

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

734

unify_imported_clock None ck_node loc;

735

check_imported_pclocks loc ck_node;

736

try_generalize ck_node loc;

737

nd.nodei_clock < ck_node;

738

Env.add_value env nd.nodei_id ck_node

739


740


741

let new_env = clock_var_decl_list

742


743

let clock_top_const env cdecl=

744

let ck = new_var false in

745

try_generalize ck cdecl.const_loc;

746

Env.add_value env cdecl.const_id ck

747


748

let clock_top_consts env clist =

749

List.fold_left clock_top_const env clist

750


751

let rec clock_top_decl env decl =

752

match decl.top_decl_desc with

753

 Node nd >

754

clock_node env decl.top_decl_loc nd

755

 ImportedNode nd >

756

clock_imported_node env decl.top_decl_loc nd

757

 Const c >

758

clock_top_const env c

759

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

760

 Include _  Open _ > env

761


762

let clock_prog env decls =

763

List.fold_left clock_top_decl env decls

764


765

(* Once the Lustre program is fully clocked,

766

we must get back to the original description of clocks,

767

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

768


769

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

770

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

771

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

772

*)

773

let uneval_vdecl_generics vdecl =

774

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

775

if Types.get_clock_base_type vdecl.var_type <> None

776

then

777

match get_carrier_name vdecl.var_clock with

778

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

779

 Some cr > Clocks.uneval vdecl.var_id cr

780


781

let uneval_node_generics vdecls =

782

List.iter uneval_vdecl_generics vdecls

783


784

let uneval_top_generics decl =

785

match decl.top_decl_desc with

786

 Node nd >

787

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

788

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

789

 ImportedNode nd >

790

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

791

 Const _

792

 Include _  Open _

793

 TypeDef _ > ()

794


795

let uneval_prog_generics prog =

796

List.iter uneval_top_generics prog

797


798

let check_env_compat header declared computed =

799

uneval_prog_generics header;

800

Env.iter declared (fun k decl_clock_k >

801

try

802

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

803

try_semi_unify decl_clock_k computed_c Location.dummy_loc

804

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

805

required element should have been declared

806

and is missing but typing should have catch

807

it, or it was a contract and does not

808

require this additional check. *)

809

()

810

)

811

(* Local Variables: *)

812

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

813

(* End: *)
