1

/********************************************************************/

2

/* */

3

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

4

/* Copyright 2012   ONERA  CNRS  INPT */

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

/********************************************************************/

11


12

%{

13

open Utils

14

open LustreSpec

15

open Corelang

16

open Dimension

17

open Parse

18


19

let get_loc () = Location.symbol_rloc ()

20


21

let mktyp x = mktyp (get_loc ()) x

22

let mkclock x = mkclock (get_loc ()) x

23

let mkvar_decl x = mkvar_decl (get_loc ()) ~orig:true x

24

let mkexpr x = mkexpr (get_loc ()) x

25

let mkeexpr x = mkeexpr (get_loc ()) x

26

let mkeq x = mkeq (get_loc ()) x

27

let mkassert x = mkassert (get_loc ()) x

28

let mktop_decl itf x = mktop_decl (get_loc ()) (Location.get_module ()) itf x

29

let mkpredef_call x = mkpredef_call (get_loc ()) x

30

(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)

31


32

let mkdim_int i = mkdim_int (get_loc ()) i

33

let mkdim_bool b = mkdim_bool (get_loc ()) b

34

let mkdim_ident id = mkdim_ident (get_loc ()) id

35

let mkdim_appl f args = mkdim_appl (get_loc ()) f args

36

let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e

37


38

let mkannots annots = { annots = annots; annot_loc = get_loc () }

39


40

%}

41


42

%token <int> INT

43

%token <string> REAL

44

%token <float> FLOAT

45

%token <string> STRING

46

%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST

47

%token STATELESS ASSERT OPEN QUOTE FUNCTION

48

%token <string> IDENT

49

%token <string> UIDENT

50

%token TRUE FALSE

51

%token <LustreSpec.expr_annot> ANNOT

52

%token <LustreSpec.node_annot> NODESPEC

53

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

54

%token AMPERAMPER BARBAR NOT POWER

55

%token IF THEN ELSE

56

%token UCLOCK DCLOCK PHCLOCK TAIL

57

%token MERGE FBY WHEN WHENNOT EVERY

58

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

59

%token STRUCT ENUM

60

%token TINT TFLOAT TREAL TBOOL TCLOCK

61

%token RATE DUE

62

%token EQ LT GT LTE GTE NEQ

63

%token AND OR XOR IMPL

64

%token MULT DIV MOD

65

%token MINUS PLUS UMINUS

66

%token PRE ARROW

67

%token REQUIRES ENSURES OBSERVER

68

%token INVARIANT BEHAVIOR ASSUMES

69

%token EXISTS FORALL

70

%token PROTOTYPE LIB

71

%token EOF

72


73

%nonassoc prec_exists prec_forall

74

%nonassoc COMMA

75

%left MERGE IF

76

%nonassoc ELSE

77

%right ARROW FBY

78

%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK

79

%right COLCOL

80

%right IMPL

81

%left OR XOR BARBAR

82

%left AND AMPERAMPER

83

%left NOT

84

%nonassoc INT

85

%nonassoc EQ LT GT LTE GTE NEQ

86

%left MINUS PLUS

87

%left MULT DIV MOD

88

%left UMINUS

89

%left POWER

90

%left PRE LAST

91

%nonassoc RBRACKET

92

%nonassoc LBRACKET

93


94

%start prog

95

%type <LustreSpec.top_decl list> prog

96


97

%start header

98

%type <LustreSpec.top_decl list> header

99


100

%start lustre_annot

101

%type <LustreSpec.expr_annot> lustre_annot

102


103

%start lustre_spec

104

%type <LustreSpec.node_annot> lustre_spec

105


106

%%

107


108

module_ident:

109

UIDENT { $1 }

110

 IDENT { $1 }

111


112

tag_ident:

113

UIDENT { $1 }

114

 TRUE { tag_true }

115

 FALSE { tag_false }

116


117

node_ident:

118

UIDENT { $1 }

119

 IDENT { $1 }

120


121

vdecl_ident:

122

UIDENT { $1 }

123

 IDENT { $1 }

124


125

const_ident:

126

UIDENT { $1 }

127

 IDENT { $1 }

128


129

type_ident:

130

IDENT { $1 }

131


132

prog:

133

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

134


135

typ_def_prog:

136

typ_def_list { $1 false }

137


138

header:

139

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

140


141

typ_def_header:

142

typ_def_list { $1 true }

143


144

open_list:

145

{ [] }

146

 open_lusi open_list { $1 :: $2 }

147


148

open_lusi:

149

 OPEN QUOTE module_ident QUOTE { mktop_decl false (Open (true, $3))}

150

 OPEN LT module_ident GT { mktop_decl false (Open (false, $3)) }

151


152

top_decl_list:

153

{[]}

154

 top_decl_list top_decl {$2@$1}

155


156


157

top_decl_header_list:

158

{ [] }

159

 top_decl_header_list top_decl_header { $2@$1 }

160


161

state_annot:

162

FUNCTION { true }

163

 NODE { false }

164


165

top_decl_header:

166

 CONST cdecl_list { List.rev ($2 true) }

167

 nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_opt SCOL

168

{let nd = mktop_decl true (ImportedNode

169

{nodei_id = $3;

170

nodei_type = Types.new_var ();

171

nodei_clock = Clocks.new_var true;

172

nodei_inputs = List.rev $5;

173

nodei_outputs = List.rev $10;

174

nodei_stateless = $2;

175

nodei_spec = $1;

176

nodei_prototype = $13;

177

nodei_in_lib = $14;})

178

in

179

(*add_imported_node $3 nd;*) [nd] }

180


181

prototype_opt:

182

{ None }

183

 PROTOTYPE node_ident { Some $2}

184


185

in_lib_opt:

186

{ None }

187

 LIB module_ident {Some $2}

188


189

top_decl:

190

 CONST cdecl_list { List.rev ($2 false) }

191

 nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL

192

{let stmts, asserts, annots = $16 in

193

let nd = mktop_decl false (Node

194

{node_id = $3;

195

node_type = Types.new_var ();

196

node_clock = Clocks.new_var true;

197

node_inputs = List.rev $5;

198

node_outputs = List.rev $10;

199

node_locals = List.rev $14;

200

node_gencalls = [];

201

node_checks = [];

202

node_asserts = asserts;

203

node_stmts = stmts;

204

node_dec_stateless = $2;

205

node_stateless = None;

206

node_spec = $1;

207

node_annot = annots})

208

in

209

(*add_node $3 nd;*) [nd] }

210


211

nodespec_list:

212

{ None }

213

 NODESPEC nodespec_list {

214

(function

215

 None > (fun s1 > Some s1)

216

 Some s2 > (fun s1 > Some (merge_node_annot s1 s2))) $2 $1 }

217


218

typ_def_list:

219

/* empty */ { (fun itf > []) }

220

 typ_def SCOL typ_def_list { (fun itf > let ty1 = ($1 itf) in ty1 :: ($3 itf)) }

221


222

typ_def:

223

TYPE type_ident EQ typ_def_rhs { (fun itf >

224

let typ = mktop_decl itf (TypeDef { tydef_id = $2;

225

tydef_desc = $4

226

})

227

in (*add_type itf $2 typ;*) typ) }

228


229

typ_def_rhs:

230

typeconst { $1 }

231

 ENUM LCUR tag_list RCUR { Tydec_enum (List.rev $3) }

232

 STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }

233


234

array_typ_decl:

235

{ fun typ > typ }

236

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

237


238

typeconst:

239

TINT array_typ_decl { $2 Tydec_int }

240

 TBOOL array_typ_decl { $2 Tydec_bool }

241

 TREAL array_typ_decl { $2 Tydec_real }

242

 TFLOAT array_typ_decl { $2 Tydec_float }

243

 type_ident array_typ_decl { $2 (Tydec_const $1) }

244

 TBOOL TCLOCK { Tydec_clock Tydec_bool }

245

 IDENT TCLOCK { Tydec_clock (Tydec_const $1) }

246


247

tag_list:

248

UIDENT { $1 :: [] }

249

 tag_list COMMA UIDENT { $3 :: $1 }

250


251

field_list: { [] }

252

 field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }

253


254

stmt_list:

255

{ [], [], [] }

256

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

257

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

258

 ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}

259

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

260


261

automaton:

262

AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 }

263


264

handler_list:

265

{ [] }

266

 handler handler_list { $1::$2 }

267


268

handler:

269

STATE UIDENT COL unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }

270


271

unless_list:

272

{ [] }

273

 unless unless_list { $1::$2 }

274


275

until_list:

276

{ [] }

277

 until until_list { $1::$2 }

278


279

unless:

280

UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4) }

281

 UNLESS expr RESUME UIDENT { (get_loc (), $2, false, $4) }

282


283

until:

284

UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4) }

285

 UNTIL expr RESUME UIDENT { (get_loc (), $2, false, $4) }

286


287

assert_:

288

 ASSERT expr SCOL {mkassert ($2)}

289


290

eq:

291

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

292

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

293


294

lustre_spec:

295

 contract EOF { $1 }

296


297

contract:

298

requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }

299


300

requires:

301

{ [] }

302

 REQUIRES qexpr SCOL requires { $2::$4 }

303


304

ensures:

305

{ [] }

306

 ENSURES qexpr SCOL ensures { $2 :: $4 }

307

 OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures {

308

mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7

309

}

310


311

behaviors:

312

{ [] }

313

 BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 }

314


315

assumes:

316

{ [] }

317

 ASSUMES qexpr SCOL assumes { $2::$4 }

318


319

/* WARNING: UNUSED RULES */

320

tuple_qexpr:

321

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

322

 tuple_qexpr COMMA qexpr {$3::$1}

323


324

qexpr:

325

 expr { mkeexpr $1 }

326

/* Quantifiers */

327

 EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 }

328

 FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }

329


330


331

tuple_expr:

332

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

333

 tuple_expr COMMA expr {$3::$1}

334


335

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

336

array_expr:

337

expr {[$1]}

338

 expr COMMA array_expr {$1::$3}

339


340

dim_list:

341

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

342

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

343


344

expr:

345

/* constants */

346

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

347

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

348

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

349

/* Idents or type enum tags */

350

 IDENT { mkexpr (Expr_ident $1) }

351

 tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) }

352

 LPAR ANNOT expr RPAR

353

{update_expr_annot $3 $2}

354

 LPAR expr RPAR

355

{$2}

356

 LPAR tuple_expr RPAR

357

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

358


359

/* Array expressions */

360

 LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }

361

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

362

 expr LBRACKET dim_list { $3 $1 }

363


364

/* Temporal operators */

365

 PRE expr

366

{mkexpr (Expr_pre $2)}

367

 expr ARROW expr

368

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

369

 expr FBY expr

370

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

371

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

372

 expr WHEN vdecl_ident

373

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

374

 expr WHENNOT vdecl_ident

375

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

376

 expr WHEN tag_ident LPAR vdecl_ident RPAR

377

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

378

 MERGE vdecl_ident handler_expr_list

379

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

380


381

/* Applications */

382

 node_ident LPAR expr RPAR

383

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

384

 node_ident LPAR expr RPAR EVERY expr

385

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

386

 node_ident LPAR tuple_expr RPAR

387

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

388

 node_ident LPAR tuple_expr RPAR EVERY expr

389

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

390


391

/* Boolean expr */

392

 expr AND expr

393

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

394

 expr AMPERAMPER expr

395

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

396

 expr OR expr

397

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

398

 expr BARBAR expr

399

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

400

 expr XOR expr

401

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

402

 NOT expr

403

{mkpredef_call "not" [$2]}

404

 expr IMPL expr

405

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

406


407

/* Comparison expr */

408

 expr EQ expr

409

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

410

 expr LT expr

411

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

412

 expr LTE expr

413

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

414

 expr GT expr

415

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

416

 expr GTE expr

417

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

418

 expr NEQ expr

419

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

420


421

/* Arithmetic expr */

422

 expr PLUS expr

423

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

424

 expr MINUS expr

425

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

426

 expr MULT expr

427

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

428

 expr DIV expr

429

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

430

 MINUS expr %prec UMINUS

431

{mkpredef_call "uminus" [$2]}

432

 expr MOD expr

433

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

434


435

/* If */

436

 IF expr THEN expr ELSE expr

437

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

438


439

handler_expr_list:

440

{ [] }

441

 handler_expr handler_expr_list { $1 :: $2 }

442


443

handler_expr:

444

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

445


446

signed_const_array:

447

 signed_const { [$1] }

448

 signed_const COMMA signed_const_array { $1 :: $3 }

449


450

signed_const_struct:

451

 IDENT EQ signed_const { [ ($1, $3) ] }

452

 IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }

453


454

signed_const:

455

INT {Const_int $1}

456

 REAL {Const_real $1}

457

 FLOAT {Const_float $1}

458

 tag_ident {Const_tag $1}

459

 MINUS INT {Const_int (1 * $2)}

460

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

461

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

462

 LCUR signed_const_struct RCUR { Const_struct $2 }

463

 LBRACKET signed_const_array RBRACKET { Const_array $2 }

464


465

dim:

466

INT { mkdim_int $1 }

467

 LPAR dim RPAR { $2 }

468

 UIDENT { mkdim_ident $1 }

469

 IDENT { mkdim_ident $1 }

470

 dim AND dim

471

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

472

 dim AMPERAMPER dim

473

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

474

 dim OR dim

475

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

476

 dim BARBAR dim

477

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

478

 dim XOR dim

479

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

480

 NOT dim

481

{mkdim_appl "not" [$2]}

482

 dim IMPL dim

483

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

484


485

/* Comparison dim */

486

 dim EQ dim

487

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

488

 dim LT dim

489

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

490

 dim LTE dim

491

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

492

 dim GT dim

493

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

494

 dim GTE dim

495

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

496

 dim NEQ dim

497

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

498


499

/* Arithmetic dim */

500

 dim PLUS dim

501

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

502

 dim MINUS dim

503

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

504

 dim MULT dim

505

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

506

 dim DIV dim

507

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

508

 MINUS dim %prec UMINUS

509

{mkdim_appl "uminus" [$2]}

510

 dim MOD dim

511

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

512

/* If */

513

 IF dim THEN dim ELSE dim

514

{mkdim_ite $2 $4 $6}

515


516

locals:

517

{[]}

518

 VAR vdecl_list SCOL {$2}

519


520

vdecl_list:

521

vdecl {$1}

522

 vdecl_list SCOL vdecl {$3 @ $1}

523


524

vdecl:

525

/* Useless no ?*/ ident_list

526

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

527


528

 ident_list COL typeconst clock

529

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

530

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

531

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

532


533

cdecl_list:

534

cdecl SCOL { (fun itf > [$1 itf]) }

535

 cdecl cdecl_list SCOL { (fun itf > let c1 = ($1 itf) in c1::($2 itf)) }

536


537

cdecl:

538

const_ident EQ signed_const {

539

(fun itf >

540

let c = mktop_decl itf (Const {

541

const_id = $1;

542

const_loc = Location.symbol_rloc ();

543

const_type = Types.new_var ();

544

const_value = $3})

545

in

546

(*add_const itf $1 c;*) c)

547

}

548


549

clock:

550

{mkclock Ckdec_any}

551

 when_list

552

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

553


554

when_cond:

555

WHEN IDENT {($2, tag_true)}

556

 WHENNOT IDENT {($2, tag_false)}

557

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

558


559

when_list:

560

when_cond {[$1]}

561

 when_list when_cond {$2::$1}

562


563

ident_list:

564

vdecl_ident {[$1]}

565

 ident_list COMMA vdecl_ident {$3::$1}

566


567

SCOL_opt:

568

SCOL {}  {}

569


570


571

lustre_annot:

572

lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }

573


574

lustre_annot_list:

575

{ [] }

576

 kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }

577

 IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }

578

 INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }

579

 OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }

580


581

kwd:

582

DIV { [] }

583

 DIV IDENT kwd { $2::$3}

584


585

%%

586

(* Local Variables: *)

587

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

588

(* End: *)

589


590

