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

%{

24

open LustreSpec

25

open Corelang

26

open Dimension

27

open Utils

28


29

let mktyp x = mktyp (Location.symbol_rloc ()) x

30

let mkclock x = mkclock (Location.symbol_rloc ()) x

31

let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x

32

let mkexpr x = mkexpr (Location.symbol_rloc ()) x

33

let mkeq x = mkeq (Location.symbol_rloc ()) x

34

let mkassert x = mkassert (Location.symbol_rloc ()) x

35

let mktop_decl x = mktop_decl (Location.symbol_rloc ()) x

36

let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x

37

let mkpredef_unary_call x = mkpredef_unary_call (Location.symbol_rloc ()) x

38


39

let mkdim_int i = mkdim_int (Location.symbol_rloc ()) i

40

let mkdim_bool b = mkdim_bool (Location.symbol_rloc ()) b

41

let mkdim_ident id = mkdim_ident (Location.symbol_rloc ()) id

42

let mkdim_appl f args = mkdim_appl (Location.symbol_rloc ()) f args

43

let mkdim_ite i t e = mkdim_ite (Location.symbol_rloc ()) i t e

44


45

%}

46


47

%token <int> INT

48

%token <string> REAL

49

%token <float> FLOAT

50

%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST

51

%token STATELESS ASSERT OPEN QUOTE FUNCTION

52

%token <string> IDENT

53

%token <LustreSpec.expr_annot> ANNOT

54

%token <LustreSpec.node_annot> NODESPEC

55

%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL

56

%token AMPERAMPER BARBAR NOT POWER

57

%token IF THEN ELSE

58

%token UCLOCK DCLOCK PHCLOCK TAIL

59

%token MERGE FBY WHEN WHENNOT EVERY

60

%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST

61

%token STRUCT ENUM

62

%token TINT TFLOAT TREAL TBOOL TCLOCK

63

%token RATE DUE

64

%token EQ LT GT LTE GTE NEQ

65

%token AND OR XOR IMPL

66

%token MULT DIV MOD

67

%token MINUS PLUS UMINUS

68

%token PRE ARROW

69


70

%token EOF

71


72

%nonassoc COMMA

73

%left MERGE IF

74

%nonassoc ELSE

75

%right ARROW FBY

76

%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK

77

%right COLCOL

78

%right IMPL

79

%left OR XOR BARBAR

80

%left AND AMPERAMPER

81

%left NOT

82

%nonassoc INT

83

%nonassoc EQ LT GT LTE GTE NEQ

84

%left MINUS PLUS

85

%left MULT DIV MOD

86

%left UMINUS

87

%left POWER

88

%left PRE LAST

89

%nonassoc RBRACKET

90

%nonassoc LBRACKET

91


92

%start prog

93

%type <Corelang.top_decl list> prog

94

%start header

95

%type <Corelang.top_decl list> header

96


97

%%

98


99

prog:

100

open_list typ_def_list top_decl_list EOF { $1 @ (List.rev $3) }

101


102

header:

103

open_list typ_def_list top_decl_header_list EOF { $1 @ (List.rev $3) }

104


105

open_list:

106

{ [] }

107

 open_lusi open_list { $1 :: $2 }

108


109

open_lusi:

110

OPEN QUOTE IDENT QUOTE { mktop_decl (Open $3) }

111


112

top_decl_list:

113

top_decl {[$1]}

114

 top_decl_list top_decl {$2::$1}

115


116


117

top_decl_header_list:

118

top_decl_header {[$1]}

119

 top_decl_header_list top_decl_header {$2::$1}

120


121


122

top_decl_header:

123

 NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL

124

{let nd = mktop_decl (ImportedNode

125

{nodei_id = $2;

126

nodei_type = Types.new_var ();

127

nodei_clock = Clocks.new_var true;

128

nodei_inputs = List.rev $4;

129

nodei_outputs = List.rev $9;

130

nodei_stateless = $12;

131

nodei_spec = None})

132

in

133

Hashtbl.add node_table $2 nd; nd}

134


135

 nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL

136

{let nd = mktop_decl (ImportedNode

137

{nodei_id = $3;

138

nodei_type = Types.new_var ();

139

nodei_clock = Clocks.new_var true;

140

nodei_inputs = List.rev $5;

141

nodei_outputs = List.rev $10;

142

nodei_stateless = $13;

143

nodei_spec = Some $1})

144

in

145

Hashtbl.add node_table $3 nd; nd}

146


147

 FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL

148

{let nd = mktop_decl (ImportedNode

149

{nodei_id = $2;

150

nodei_type = Types.new_var ();

151

nodei_clock = Clocks.new_var true;

152

nodei_inputs = List.rev $4;

153

nodei_outputs = List.rev $9;

154

nodei_stateless = true;

155

nodei_spec = None})

156

in

157

Hashtbl.add node_table $2 nd; nd}

158


159

 nodespec_list FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL

160

{let nd = mktop_decl (ImportedNode

161

{nodei_id = $3;

162

nodei_type = Types.new_var ();

163

nodei_clock = Clocks.new_var true;

164

nodei_inputs = List.rev $5;

165

nodei_outputs = List.rev $10;

166

nodei_stateless = true;

167

nodei_spec = Some $1})

168

in

169

Hashtbl.add node_table $3 nd; nd}

170


171

top_decl:

172

 CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }

173


174

 NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL

175

{let eqs, asserts, annots = $15 in

176

let nd = mktop_decl (Node

177

{node_id = $2;

178

node_type = Types.new_var ();

179

node_clock = Clocks.new_var true;

180

node_inputs = List.rev $4;

181

node_outputs = List.rev $9;

182

node_locals = List.rev $13;

183

node_gencalls = [];

184

node_checks = [];

185

node_asserts = asserts;

186

node_eqs = eqs;

187

node_spec = None;

188

node_annot = match annots with [] > None  _ > Some annots})

189

in

190

Hashtbl.add node_table $2 nd; nd}

191


192

 nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL

193

{let eqs, asserts, annots = $16 in

194

let nd = mktop_decl (Node

195

{node_id = $3;

196

node_type = Types.new_var ();

197

node_clock = Clocks.new_var true;

198

node_inputs = List.rev $5;

199

node_outputs = List.rev $10;

200

node_locals = List.rev $14;

201

node_gencalls = [];

202

node_checks = [];

203

node_asserts = asserts;

204

node_eqs = eqs;

205

node_spec = Some $1;

206

node_annot = match annots with [] > None  _ > Some annots})

207

in

208

Hashtbl.add node_table $3 nd; nd}

209


210

nodespec_list:

211

NODESPEC { $1 }

212

 NODESPEC nodespec_list { LustreSpec.merge_node_annot $1 $2 }

213


214

stateless_opt:

215

{ false }

216

 STATELESS {true}

217


218

typ_def_list:

219

/* empty */ {}

220

 typ_def SCOL typ_def_list {$1;$3}

221


222

typ_def:

223

TYPE IDENT EQ typeconst {

224

try

225

Hashtbl.add type_table (Tydec_const $2) (Corelang.get_repr_type $4)

226

with Not_found> raise (Corelang.Unbound_type ($4, Location.symbol_rloc())) }

227

 TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) }

228

 TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) Tydec_any }

229


230

array_typ_decl:

231

{ fun typ > typ }

232

 POWER dim array_typ_decl { fun typ > $3 (Tydec_array ($2, typ)) }

233


234

typeconst:

235

TINT array_typ_decl { $2 Tydec_int }

236

 TBOOL array_typ_decl { $2 Tydec_bool }

237

 TREAL array_typ_decl { $2 Tydec_real }

238

 TFLOAT array_typ_decl { $2 Tydec_float }

239

 IDENT array_typ_decl { $2 (Tydec_const $1) }

240

 TBOOL TCLOCK { Tydec_clock Tydec_bool }

241

 IDENT TCLOCK { Tydec_clock (Tydec_const $1) }

242


243

tag_list:

244

IDENT

245

{ (fun t > if Hashtbl.mem tag_table $1

246

then raise (Corelang.Already_bound_label ($1, t, Location.symbol_rloc ()))

247

else (Hashtbl.add tag_table $1 t; $1 :: [])) }

248

 tag_list COMMA IDENT

249

{ (fun t > if Hashtbl.mem tag_table $3

250

then raise (Corelang.Already_bound_label ($3, t, Location.symbol_rloc ()))

251

else (Hashtbl.add tag_table $3 t; $3 :: ($1 t))) }

252


253

field_list:

254

{ [] }

255

 IDENT COL typeconst SCOL field_list { ($1, $3) :: $5 }

256


257

eq_list:

258

{ [], [], [] }

259

 eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}

260

 assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}

261

 ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1@annotl}

262

 automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}

263


264

automaton:

265

AUTOMATON IDENT handler_list { failwith "not implemented" }

266


267

handler_list:

268

{ [] }

269

 handler handler_list { $1::$2 }

270


271

handler:

272

STATE IDENT ARROW unless_list locals LET eq_list TEL until_list { () }

273


274

unless_list:

275

{ [] }

276

 unless unless_list { $1::$2 }

277


278

until_list:

279

{ [] }

280

 until until_list { $1::$2 }

281


282

unless:

283

UNLESS expr RESTART IDENT { }

284

 UNLESS expr RESUME IDENT { }

285


286

until:

287

UNTIL expr RESTART IDENT { }

288

 UNTIL expr RESUME IDENT { }

289


290

assert_:

291

 ASSERT expr SCOL {mkassert ($2)}

292


293

eq:

294

ident_list EQ expr SCOL {mkeq (List.rev $1,$3)}

295

 LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}

296


297

tuple_expr:

298

expr COMMA expr {[$3;$1]}

299

 tuple_expr COMMA expr {$3::$1}

300


301

// Same as tuple expr but accepting lists with single element

302

array_expr:

303

expr {[$1]}

304

 expr COMMA array_expr {$1::$3}

305


306

dim_list:

307

dim RBRACKET { fun base > mkexpr (Expr_access (base, $1)) }

308

 dim RBRACKET LBRACKET dim_list { fun base > $4 (mkexpr (Expr_access (base, $1))) }

309


310

expr:

311

/* constants */

312

INT {mkexpr (Expr_const (Const_int $1))}

313

 REAL {mkexpr (Expr_const (Const_real $1))}

314

 FLOAT {mkexpr (Expr_const (Const_float $1))}

315

/* Idents or type enum tags */

316

 IDENT {

317

if Hashtbl.mem tag_table $1

318

then mkexpr (Expr_const (Const_tag $1))

319

else mkexpr (Expr_ident $1)}

320

 LPAR ANNOT expr RPAR

321

{update_expr_annot $3 $2}

322

 LPAR expr RPAR

323

{$2}

324

 LPAR tuple_expr RPAR

325

{mkexpr (Expr_tuple (List.rev $2))}

326


327

/* Array expressions */

328

 LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }

329

 expr POWER dim { mkexpr (Expr_power ($1, $3)) }

330

 expr LBRACKET dim_list { $3 $1 }

331


332

/* Temporal operators */

333

 PRE expr

334

{mkexpr (Expr_pre $2)}

335

 expr ARROW expr

336

{mkexpr (Expr_arrow ($1,$3))}

337

 expr FBY expr

338

{(*mkexpr (Expr_fby ($1,$3))*)

339

mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}

340

 expr WHEN IDENT

341

{mkexpr (Expr_when ($1,$3,tag_true))}

342

 expr WHENNOT IDENT

343

{mkexpr (Expr_when ($1,$3,tag_false))}

344

 expr WHEN IDENT LPAR IDENT RPAR

345

{mkexpr (Expr_when ($1, $5, $3))}

346

 MERGE IDENT handler_expr_list

347

{mkexpr (Expr_merge ($2,$3))}

348


349

/* Applications */

350

 IDENT LPAR expr RPAR

351

{mkexpr (Expr_appl ($1, $3, None))}

352

 IDENT LPAR expr RPAR EVERY IDENT

353

{mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}

354

 IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR

355

{mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }

356

 IDENT LPAR tuple_expr RPAR

357

{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}

358

 IDENT LPAR tuple_expr RPAR EVERY IDENT

359

{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }

360

 IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR

361

{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }

362


363

/* Boolean expr */

364

 expr AND expr

365

{mkpredef_call "&&" [$1;$3]}

366

 expr AMPERAMPER expr

367

{mkpredef_call "&&" [$1;$3]}

368

 expr OR expr

369

{mkpredef_call "" [$1;$3]}

370

 expr BARBAR expr

371

{mkpredef_call "" [$1;$3]}

372

 expr XOR expr

373

{mkpredef_call "xor" [$1;$3]}

374

 NOT expr

375

{mkpredef_unary_call "not" $2}

376

 expr IMPL expr

377

{mkpredef_call "impl" [$1;$3]}

378


379

/* Comparison expr */

380

 expr EQ expr

381

{mkpredef_call "=" [$1;$3]}

382

 expr LT expr

383

{mkpredef_call "<" [$1;$3]}

384

 expr LTE expr

385

{mkpredef_call "<=" [$1;$3]}

386

 expr GT expr

387

{mkpredef_call ">" [$1;$3]}

388

 expr GTE expr

389

{mkpredef_call ">=" [$1;$3]}

390

 expr NEQ expr

391

{mkpredef_call "!=" [$1;$3]}

392


393

/* Arithmetic expr */

394

 expr PLUS expr

395

{mkpredef_call "+" [$1;$3]}

396

 expr MINUS expr

397

{mkpredef_call "" [$1;$3]}

398

 expr MULT expr

399

{mkpredef_call "*" [$1;$3]}

400

 expr DIV expr

401

{mkpredef_call "/" [$1;$3]}

402

 MINUS expr %prec UMINUS

403

{mkpredef_unary_call "uminus" $2}

404

 expr MOD expr

405

{mkpredef_call "mod" [$1;$3]}

406


407

/* If */

408

 IF expr THEN expr ELSE expr

409

{mkexpr (Expr_ite ($2, $4, $6))}

410


411

handler_expr_list:

412

{ [] }

413

 handler_expr handler_expr_list { $1 :: $2 }

414


415

handler_expr:

416

LPAR IDENT ARROW expr RPAR { ($2, $4) }

417


418

signed_const_array:

419

 signed_const { [$1] }

420

 signed_const COMMA signed_const_array { $1 :: $3 }

421


422

signed_const:

423

INT {Const_int $1}

424

 REAL {Const_real $1}

425

 FLOAT {Const_float $1}

426

 IDENT {Const_tag $1}

427

 MINUS INT {Const_int (1 * $2)}

428

 MINUS REAL {Const_real ("" ^ $2)}

429

 MINUS FLOAT {Const_float (1. *. $2)}

430

 LBRACKET signed_const_array RBRACKET { Const_array $2 }

431


432

dim:

433

INT { mkdim_int $1 }

434

 LPAR dim RPAR { $2 }

435

 IDENT { mkdim_ident $1 }

436

 dim AND dim

437

{mkdim_appl "&&" [$1;$3]}

438

 dim AMPERAMPER dim

439

{mkdim_appl "&&" [$1;$3]}

440

 dim OR dim

441

{mkdim_appl "" [$1;$3]}

442

 dim BARBAR dim

443

{mkdim_appl "" [$1;$3]}

444

 dim XOR dim

445

{mkdim_appl "xor" [$1;$3]}

446

 NOT dim

447

{mkdim_appl "not" [$2]}

448

 dim IMPL dim

449

{mkdim_appl "impl" [$1;$3]}

450


451

/* Comparison dim */

452

 dim EQ dim

453

{mkdim_appl "=" [$1;$3]}

454

 dim LT dim

455

{mkdim_appl "<" [$1;$3]}

456

 dim LTE dim

457

{mkdim_appl "<=" [$1;$3]}

458

 dim GT dim

459

{mkdim_appl ">" [$1;$3]}

460

 dim GTE dim

461

{mkdim_appl ">=" [$1;$3]}

462

 dim NEQ dim

463

{mkdim_appl "!=" [$1;$3]}

464


465

/* Arithmetic dim */

466

 dim PLUS dim

467

{mkdim_appl "+" [$1;$3]}

468

 dim MINUS dim

469

{mkdim_appl "" [$1;$3]}

470

 dim MULT dim

471

{mkdim_appl "*" [$1;$3]}

472

 dim DIV dim

473

{mkdim_appl "/" [$1;$3]}

474

 MINUS dim %prec UMINUS

475

{mkdim_appl "uminus" [$2]}

476

 dim MOD dim

477

{mkdim_appl "mod" [$1;$3]}

478

/* If */

479

 IF dim THEN dim ELSE dim

480

{mkdim_ite $2 $4 $6}

481


482

locals:

483

{[]}

484

 VAR vdecl_list SCOL {$2}

485


486

vdecl_list:

487

vdecl {$1}

488

 vdecl_list SCOL vdecl {$3 @ $1}

489


490

vdecl:

491

/* Useless no ?*/ ident_list

492

{List.map mkvar_decl

493

(List.map (fun id > (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}

494


495

 ident_list COL typeconst clock

496

{List.map mkvar_decl (List.map (fun id > (id, mktyp $3, $4, false)) $1)}

497

 CONST ident_list COL typeconst /* static parameters don't have clocks */

498

{List.map mkvar_decl (List.map (fun id > (id, mktyp $4, mkclock Ckdec_any, true)) $2)}

499


500

cdecl_list:

501

cdecl SCOL { [$1] }

502

 cdecl_list cdecl SCOL { $2::$1 }

503


504

cdecl:

505

IDENT EQ signed_const {

506

let c = {

507

const_id = $1;

508

const_loc = Location.symbol_rloc ();

509

const_type = Types.new_var ();

510

const_value = $3;

511

} in

512

Hashtbl.add consts_table $1 c; c

513

}

514


515

clock:

516

{mkclock Ckdec_any}

517

 when_list

518

{mkclock (Ckdec_bool (List.rev $1))}

519


520

when_cond:

521

WHEN IDENT {($2, tag_true)}

522

 WHENNOT IDENT {($2, tag_false)}

523

 WHEN IDENT LPAR IDENT RPAR {($4, $2)}

524


525

when_list:

526

when_cond {[$1]}

527

 when_list when_cond {$2::$1}

528


529

ident_list:

530

IDENT {[$1]}

531

 ident_list COMMA IDENT {$3::$1}

532


533

SCOL_opt:

534

SCOL {}  {}
