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 mkident x = x, get_loc ()

22

let mktyp x = mktyp (get_loc ()) x

23

let mkclock x = mkclock (get_loc ()) x

24

let mkvar_decl x loc = mkvar_decl loc ~orig:true x

25

let mkexpr x = mkexpr (get_loc ()) x

26

let mkeexpr x = mkeexpr (get_loc ()) x

27

let mkeq x = mkeq (get_loc ()) x

28

let mkassert x = mkassert (get_loc ()) x

29

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

30

let mkpredef_call x = mkpredef_call (get_loc ()) x

31

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

32


33

let mkdim_int i = mkdim_int (get_loc ()) i

34

let mkdim_bool b = mkdim_bool (get_loc ()) b

35

let mkdim_ident id = mkdim_ident (get_loc ()) id

36

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

37

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

38


39

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

40


41

let node_stack : ident list ref = ref []

42

let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack

43

let push_node nd = node_stack:= nd :: !node_stack

44

let pop_node () = try node_stack := List.tl !node_stack with _ > assert false

45

let get_current_node () = try List.hd !node_stack with _ > assert false

46


47

let rec fby expr n init =

48

if n<=1 then

49

mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr)))

50

else

51

mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n1) init))))

52


53

%}

54


55

%token <int> INT

56

%token <Num.num * int * string> REAL

57


58

%token <string> STRING

59

%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST

60

%token STATELESS ASSERT OPEN QUOTE FUNCTION

61

%token <string> IDENT

62

%token <string> UIDENT

63

%token TRUE FALSE

64

%token <LustreSpec.expr_annot> ANNOT

65

%token <LustreSpec.node_annot> NODESPEC

66

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

67

%token AMPERAMPER BARBAR NOT POWER

68

%token IF THEN ELSE

69

%token UCLOCK DCLOCK PHCLOCK TAIL

70

%token MERGE FBY WHEN WHENNOT EVERY

71

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

72

%token STRUCT ENUM

73

%token TINT TREAL TBOOL TCLOCK

74

%token RATE DUE

75

%token EQ LT GT LTE GTE NEQ

76

%token AND OR XOR IMPL

77

%token MULT DIV MOD

78

%token MINUS PLUS UMINUS

79

%token PRE ARROW

80

%token REQUIRES ENSURES OBSERVER

81

%token INVARIANT BEHAVIOR ASSUMES

82

%token EXISTS FORALL

83

%token PROTOTYPE LIB

84

%token EOF

85


86

%nonassoc prec_exists prec_forall

87

%nonassoc COMMA

88

%nonassoc EVERY

89

%left MERGE IF

90

%nonassoc ELSE

91

%right ARROW FBY

92

%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK

93

%right COLCOL

94

%right IMPL

95

%left OR XOR BARBAR

96

%left AND AMPERAMPER

97

%left NOT

98

%nonassoc INT

99

%nonassoc EQ LT GT LTE GTE NEQ

100

%left MINUS PLUS

101

%left MULT DIV MOD

102

%left UMINUS

103

%left POWER

104

%left PRE LAST

105

%nonassoc RBRACKET

106

%nonassoc LBRACKET

107


108

%start prog

109

%type <LustreSpec.top_decl list> prog

110


111

%start header

112

%type <LustreSpec.top_decl list> header

113


114

%start lustre_annot

115

%type <LustreSpec.expr_annot> lustre_annot

116


117

%start lustre_spec

118

%type <LustreSpec.node_annot> lustre_spec

119


120

%start signed_const

121

%type <LustreSpec.constant> signed_const

122


123

%%

124


125

module_ident:

126

UIDENT { $1 }

127

 IDENT { $1 }

128


129

tag_ident:

130

UIDENT { $1 }

131

 TRUE { tag_true }

132

 FALSE { tag_false }

133


134

node_ident:

135

UIDENT { $1 }

136

 IDENT { $1 }

137


138

node_ident_decl:

139

node_ident { push_node $1; $1 }

140


141

vdecl_ident:

142

UIDENT { mkident $1 }

143

 IDENT { mkident $1 }

144


145

const_ident:

146

UIDENT { $1 }

147

 IDENT { $1 }

148


149

type_ident:

150

IDENT { $1 }

151


152

prog:

153

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

154


155

typ_def_prog:

156

typ_def_list { $1 false }

157


158

header:

159

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

160


161

typ_def_header:

162

typ_def_list { $1 true }

163


164

open_list:

165

{ [] }

166

 open_lusi open_list { $1 :: $2 }

167


168

open_lusi:

169

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

170

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

171


172

top_decl_list:

173

{[]}

174

 top_decl_list top_decl {$2@$1}

175


176


177

top_decl_header_list:

178

{ [] }

179

 top_decl_header_list top_decl_header { $2@$1 }

180


181

state_annot:

182

FUNCTION { true }

183

 NODE { false }

184


185

top_decl_header:

186

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

187

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

188

{let nd = mktop_decl true (ImportedNode

189

{nodei_id = $3;

190

nodei_type = Types.new_var ();

191

nodei_clock = Clocks.new_var true;

192

nodei_inputs = List.rev $5;

193

nodei_outputs = List.rev $10;

194

nodei_stateless = $2;

195

nodei_spec = $1;

196

nodei_prototype = $13;

197

nodei_in_lib = $14;})

198

in

199

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

200


201

prototype_opt:

202

{ None }

203

 PROTOTYPE node_ident { Some $2}

204


205

in_lib_list:

206

{ [] }

207

 LIB module_ident in_lib_list { $2::$3 }

208


209

top_decl:

210

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

211

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

212

{

213

let stmts, asserts, annots = $16 in

214

(* Declaring eqs annots *)

215

List.iter (fun ann >

216

List.iter (fun (key, _) >

217

Annotations.add_node_ann $3 key

218

) ann.annots

219

) annots;

220

(* Building the node *)

221

let nd = mktop_decl false (Node

222

{node_id = $3;

223

node_type = Types.new_var ();

224

node_clock = Clocks.new_var true;

225

node_inputs = List.rev $5;

226

node_outputs = List.rev $10;

227

node_locals = List.rev $14;

228

node_gencalls = [];

229

node_checks = [];

230

node_asserts = asserts;

231

node_stmts = stmts;

232

node_dec_stateless = $2;

233

node_stateless = None;

234

node_spec = $1;

235

node_annot = annots})

236

in

237

pop_node ();

238

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

239


240

nodespec_list:

241

{ None }

242

 NODESPEC nodespec_list {

243

(function

244

 None > (fun s1 > Some s1)

245

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

246


247

typ_def_list:

248

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

249

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

250


251

typ_def:

252

TYPE type_ident EQ typ_def_rhs { (fun itf >

253

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

254

tydef_desc = $4

255

})

256

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

257


258

typ_def_rhs:

259

typeconst { $1 }

260

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

261

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

262


263

array_typ_decl:

264

%prec POWER { fun typ > typ }

265

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

266


267

typeconst:

268

TINT array_typ_decl { $2 Tydec_int }

269

 TBOOL array_typ_decl { $2 Tydec_bool }

270

 TREAL array_typ_decl { $2 Tydec_real }

271

/*  TFLOAT array_typ_decl { $2 Tydec_float } */

272

 type_ident array_typ_decl { $2 (Tydec_const $1) }

273

 TBOOL TCLOCK { Tydec_clock Tydec_bool }

274

 IDENT TCLOCK { Tydec_clock (Tydec_const $1) }

275


276

tag_list:

277

UIDENT { $1 :: [] }

278

 tag_list COMMA UIDENT { $3 :: $1 }

279


280

field_list: { [] }

281

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

282


283

stmt_list:

284

{ [], [], [] }

285

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

286

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

287

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

288

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

289


290

automaton:

291

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

292


293

handler_list:

294

{ [] }

295

 handler handler_list { $1::$2 }

296


297

handler:

298

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

299


300

unless_list:

301

{ [] }

302

 unless unless_list { $1::$2 }

303


304

until_list:

305

{ [] }

306

 until until_list { $1::$2 }

307


308

unless:

309

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

310

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

311


312

until:

313

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

314

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

315


316

assert_:

317

 ASSERT expr SCOL {mkassert ($2)}

318


319

eq:

320

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

321

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

322


323

lustre_spec:

324

 contract EOF { $1 }

325


326

contract:

327

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

328


329

requires:

330

{ [] }

331

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

332


333

ensures:

334

{ [] }

335

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

336

 OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures {

337

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

338

}

339


340

behaviors:

341

{ [] }

342

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

343


344

assumes:

345

{ [] }

346

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

347


348

/* WARNING: UNUSED RULES */

349

tuple_qexpr:

350

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

351

 tuple_qexpr COMMA qexpr {$3::$1}

352


353

qexpr:

354

 expr { mkeexpr $1 }

355

/* Quantifiers */

356

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

357

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

358


359


360

tuple_expr:

361

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

362

 tuple_expr COMMA expr {$3::$1}

363


364

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

365

array_expr:

366

expr {[$1]}

367

 expr COMMA array_expr {$1::$3}

368


369

dim_list:

370

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

371

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

372


373

expr:

374

/* constants */

375

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

376

 REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))}

377

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

378

/* Idents or type enum tags */

379

 IDENT { mkexpr (Expr_ident $1) }

380

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

381

 LPAR ANNOT expr RPAR

382

{update_expr_annot (get_current_node ()) $3 $2}

383

 LPAR expr RPAR

384

{$2}

385

 LPAR tuple_expr RPAR

386

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

387


388

/* Array expressions */

389

 LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }

390

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

391

 expr LBRACKET dim_list { $3 $1 }

392


393

/* Temporal operators */

394

 PRE expr

395

{mkexpr (Expr_pre $2)}

396

 expr ARROW expr

397

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

398

 expr FBY expr

399

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

400

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

401

 expr WHEN vdecl_ident

402

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

403

 expr WHENNOT vdecl_ident

404

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

405

 expr WHEN tag_ident LPAR vdecl_ident RPAR

406

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

407

 MERGE vdecl_ident handler_expr_list

408

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

409


410

/* Applications */

411

 node_ident LPAR expr RPAR

412

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

413

 node_ident LPAR expr RPAR EVERY expr

414

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

415

 node_ident LPAR tuple_expr RPAR

416

{

417

let id=$1 in

418

let args=List.rev $3 in

419

match id, args with

420

 "fbyn", [expr;n;init] >

421

let n = match n.expr_desc with

422

 Expr_const (Const_int n) > n

423

 _ > assert false

424

in

425

fby expr n init

426

 _ > mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None))

427

}

428

 node_ident LPAR tuple_expr RPAR EVERY expr

429

{

430

let id=$1 in

431

let args=List.rev $3 in

432

let clock=$6 in

433

if id="fby" then

434

assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)

435

else

436

mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock))

437

}

438


439

/* Boolean expr */

440

 expr AND expr

441

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

442

 expr AMPERAMPER expr

443

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

444

 expr OR expr

445

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

446

 expr BARBAR expr

447

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

448

 expr XOR expr

449

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

450

 NOT expr

451

{mkpredef_call "not" [$2]}

452

 expr IMPL expr

453

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

454


455

/* Comparison expr */

456

 expr EQ expr

457

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

458

 expr LT expr

459

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

460

 expr LTE expr

461

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

462

 expr GT expr

463

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

464

 expr GTE expr

465

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

466

 expr NEQ expr

467

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

468


469

/* Arithmetic expr */

470

 expr PLUS expr

471

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

472

 expr MINUS expr

473

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

474

 expr MULT expr

475

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

476

 expr DIV expr

477

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

478

 MINUS expr %prec UMINUS

479

{mkpredef_call "uminus" [$2]}

480

 expr MOD expr

481

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

482


483

/* If */

484

 IF expr THEN expr ELSE expr

485

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

486


487

handler_expr_list:

488

{ [] }

489

 handler_expr handler_expr_list { $1 :: $2 }

490


491

handler_expr:

492

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

493


494

signed_const_array:

495

 signed_const { [$1] }

496

 signed_const COMMA signed_const_array { $1 :: $3 }

497


498

signed_const_struct:

499

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

500

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

501


502

signed_const:

503

INT {Const_int $1}

504

 REAL {let c,e,s =$1 in Const_real (c,e,s)}

505

/*  FLOAT {Const_float $1} */

506

 tag_ident {Const_tag $1}

507

 MINUS INT {Const_int (1 * $2)}

508

 MINUS REAL {let c,e,s = $2 in Const_real (Num.minus_num c, e, "" ^ s)}

509

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

510

 LCUR signed_const_struct RCUR { Const_struct $2 }

511

 LBRACKET signed_const_array RBRACKET { Const_array $2 }

512


513

dim:

514

INT { mkdim_int $1 }

515

 LPAR dim RPAR { $2 }

516

 UIDENT { mkdim_ident $1 }

517

 IDENT { mkdim_ident $1 }

518

 dim AND dim

519

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

520

 dim AMPERAMPER dim

521

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

522

 dim OR dim

523

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

524

 dim BARBAR dim

525

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

526

 dim XOR dim

527

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

528

 NOT dim

529

{mkdim_appl "not" [$2]}

530

 dim IMPL dim

531

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

532


533

/* Comparison dim */

534

 dim EQ dim

535

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

536

 dim LT dim

537

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

538

 dim LTE dim

539

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

540

 dim GT dim

541

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

542

 dim GTE dim

543

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

544

 dim NEQ dim

545

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

546


547

/* Arithmetic dim */

548

 dim PLUS dim

549

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

550

 dim MINUS dim

551

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

552

 dim MULT dim

553

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

554

 dim DIV dim

555

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

556

 MINUS dim %prec UMINUS

557

{mkdim_appl "uminus" [$2]}

558

 dim MOD dim

559

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

560

/* If */

561

 IF dim THEN dim ELSE dim

562

{mkdim_ite $2 $4 $6}

563


564

locals:

565

{[]}

566

 VAR local_vdecl_list SCOL {$2}

567


568

vdecl_list:

569

vdecl {$1}

570

 vdecl_list SCOL vdecl {$3 @ $1}

571


572

vdecl:

573

ident_list COL typeconst clock

574

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

575

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

576

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

577

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

578

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

579


580

local_vdecl_list:

581

local_vdecl {$1}

582

 local_vdecl_list SCOL local_vdecl {$3 @ $1}

583


584

local_vdecl:

585

/* Useless no ?*/ ident_list

586

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

587

 ident_list COL typeconst clock

588

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

589

 CONST vdecl_ident EQ expr /* static parameters don't have clocks */

590

{ let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4) loc] }

591

 CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */

592

{ let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6) loc] }

593


594

cdecl_list:

595

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

596

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

597


598

cdecl:

599

const_ident EQ signed_const {

600

(fun itf >

601

let c = mktop_decl itf (Const {

602

const_id = $1;

603

const_loc = Location.symbol_rloc ();

604

const_type = Types.new_var ();

605

const_value = $3})

606

in

607

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

608

}

609


610

clock:

611

{mkclock Ckdec_any}

612

 when_list

613

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

614


615

when_cond:

616

WHEN IDENT {($2, tag_true)}

617

 WHENNOT IDENT {($2, tag_false)}

618

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

619


620

when_list:

621

when_cond {[$1]}

622

 when_list when_cond {$2::$1}

623


624

ident_list:

625

vdecl_ident {[$1]}

626

 ident_list COMMA vdecl_ident {$3::$1}

627


628

SCOL_opt:

629

SCOL {}  {}

630


631


632

lustre_annot:

633

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

634


635

lustre_annot_list:

636

{ [] }

637

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

638

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

639

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

640

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

641


642

kwd:

643

DIV { [] }

644

 DIV IDENT kwd { $2::$3}

645


646

%%

647

(* Local Variables: *)

648

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

649

(* End: *)

650


651

