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

let node_stack : ident list ref = ref []

41

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

42

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

43

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

44

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

45


46

let rec fby expr n init =

47

if n<=1 then

48

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

49

else

50

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

51


52

%}

53


54

%token <int> INT

55

%token <string> REAL

56

%token <float> FLOAT

57

%token <string> STRING

58

%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST

59

%token STATELESS ASSERT OPEN QUOTE FUNCTION

60

%token <string> IDENT

61

%token <string> UIDENT

62

%token TRUE FALSE

63

%token <LustreSpec.expr_annot> ANNOT

64

%token <LustreSpec.node_annot> NODESPEC

65

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

66

%token AMPERAMPER BARBAR NOT POWER

67

%token IF THEN ELSE

68

%token UCLOCK DCLOCK PHCLOCK TAIL

69

%token MERGE FBY WHEN WHENNOT EVERY

70

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

71

%token STRUCT ENUM

72

%token TINT TFLOAT TREAL TBOOL TCLOCK

73

%token RATE DUE

74

%token EQ LT GT LTE GTE NEQ

75

%token AND OR XOR IMPL

76

%token MULT DIV MOD

77

%token MINUS PLUS UMINUS

78

%token PRE ARROW

79

%token REQUIRES ENSURES OBSERVER

80

%token INVARIANT BEHAVIOR ASSUMES

81

%token EXISTS FORALL

82

%token PROTOTYPE LIB

83

%token EOF

84


85

%nonassoc prec_exists prec_forall

86

%nonassoc COMMA

87

%nonassoc EVERY

88

%left MERGE IF

89

%nonassoc ELSE

90

%right ARROW FBY

91

%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK

92

%right COLCOL

93

%right IMPL

94

%left OR XOR BARBAR

95

%left AND AMPERAMPER

96

%left NOT

97

%nonassoc INT

98

%nonassoc EQ LT GT LTE GTE NEQ

99

%left MINUS PLUS

100

%left MULT DIV MOD

101

%left UMINUS

102

%left POWER

103

%left PRE LAST

104

%nonassoc RBRACKET

105

%nonassoc LBRACKET

106


107

%start prog

108

%type <LustreSpec.top_decl list> prog

109


110

%start header

111

%type <LustreSpec.top_decl list> header

112


113

%start lustre_annot

114

%type <LustreSpec.expr_annot> lustre_annot

115


116

%start lustre_spec

117

%type <LustreSpec.node_annot> lustre_spec

118


119

%%

120


121

module_ident:

122

UIDENT { $1 }

123

 IDENT { $1 }

124


125

tag_ident:

126

UIDENT { $1 }

127

 TRUE { tag_true }

128

 FALSE { tag_false }

129


130

node_ident:

131

UIDENT { $1 }

132

 IDENT { $1 }

133


134

node_ident_decl:

135

node_ident { push_node $1; $1 }

136


137

vdecl_ident:

138

UIDENT { $1 }

139

 IDENT { $1 }

140


141

const_ident:

142

UIDENT { $1 }

143

 IDENT { $1 }

144


145

type_ident:

146

IDENT { $1 }

147


148

prog:

149

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

150


151

typ_def_prog:

152

typ_def_list { $1 false }

153


154

header:

155

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

156


157

typ_def_header:

158

typ_def_list { $1 true }

159


160

open_list:

161

{ [] }

162

 open_lusi open_list { $1 :: $2 }

163


164

open_lusi:

165

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

166

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

167


168

top_decl_list:

169

{[]}

170

 top_decl_list top_decl {$2@$1}

171


172


173

top_decl_header_list:

174

{ [] }

175

 top_decl_header_list top_decl_header { $2@$1 }

176


177

state_annot:

178

FUNCTION { true }

179

 NODE { false }

180


181

top_decl_header:

182

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

183

 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

184

{let nd = mktop_decl true (ImportedNode

185

{nodei_id = $3;

186

nodei_type = Types.new_var ();

187

nodei_clock = Clocks.new_var true;

188

nodei_inputs = List.rev $5;

189

nodei_outputs = List.rev $10;

190

nodei_stateless = $2;

191

nodei_spec = $1;

192

nodei_prototype = $13;

193

nodei_in_lib = $14;})

194

in

195

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

196


197

prototype_opt:

198

{ None }

199

 PROTOTYPE node_ident { Some $2}

200


201

in_lib_opt:

202

{ None }

203

 LIB module_ident {Some $2}

204


205

top_decl:

206

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

207

 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

208

{

209

let stmts, asserts, annots = $16 in

210

(* Declaring eqs annots *)

211

List.iter (fun ann >

212

List.iter (fun (key, _) >

213

Annotations.add_node_ann $3 key

214

) ann.annots

215

) annots;

216

(* Building the node *)

217

let nd = mktop_decl false (Node

218

{node_id = $3;

219

node_type = Types.new_var ();

220

node_clock = Clocks.new_var true;

221

node_inputs = List.rev $5;

222

node_outputs = List.rev $10;

223

node_locals = List.rev $14;

224

node_gencalls = [];

225

node_checks = [];

226

node_asserts = asserts;

227

node_stmts = stmts;

228

node_dec_stateless = $2;

229

node_stateless = None;

230

node_spec = $1;

231

node_annot = annots})

232

in

233

pop_node ();

234

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

235


236

nodespec_list:

237

{ None }

238

 NODESPEC nodespec_list {

239

(function

240

 None > (fun s1 > Some s1)

241

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

242


243

typ_def_list:

244

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

245

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

246


247

typ_def:

248

TYPE type_ident EQ typ_def_rhs { (fun itf >

249

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

250

tydef_desc = $4

251

})

252

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

253


254

typ_def_rhs:

255

typeconst { $1 }

256

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

257

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

258


259

array_typ_decl:

260

{ fun typ > typ }

261

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

262


263

typeconst:

264

TINT array_typ_decl { $2 Tydec_int }

265

 TBOOL array_typ_decl { $2 Tydec_bool }

266

 TREAL array_typ_decl { $2 Tydec_real }

267

 TFLOAT array_typ_decl { $2 Tydec_float }

268

 type_ident array_typ_decl { $2 (Tydec_const $1) }

269

 TBOOL TCLOCK { Tydec_clock Tydec_bool }

270

 IDENT TCLOCK { Tydec_clock (Tydec_const $1) }

271


272

tag_list:

273

UIDENT { $1 :: [] }

274

 tag_list COMMA UIDENT { $3 :: $1 }

275


276

field_list: { [] }

277

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

278


279

stmt_list:

280

{ [], [], [] }

281

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

282

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

283

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

284

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

285


286

automaton:

287

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

288


289

handler_list:

290

{ [] }

291

 handler handler_list { $1::$2 }

292


293

handler:

294

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

295


296

unless_list:

297

{ [] }

298

 unless unless_list { $1::$2 }

299


300

until_list:

301

{ [] }

302

 until until_list { $1::$2 }

303


304

unless:

305

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

306

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

307


308

until:

309

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

310

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

311


312

assert_:

313

 ASSERT expr SCOL {mkassert ($2)}

314


315

eq:

316

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

317

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

318


319

lustre_spec:

320

 contract EOF { $1 }

321


322

contract:

323

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

324


325

requires:

326

{ [] }

327

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

328


329

ensures:

330

{ [] }

331

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

332

 OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures {

333

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

334

}

335


336

behaviors:

337

{ [] }

338

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

339


340

assumes:

341

{ [] }

342

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

343


344

/* WARNING: UNUSED RULES */

345

tuple_qexpr:

346

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

347

 tuple_qexpr COMMA qexpr {$3::$1}

348


349

qexpr:

350

 expr { mkeexpr $1 }

351

/* Quantifiers */

352

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

353

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

354


355


356

tuple_expr:

357

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

358

 tuple_expr COMMA expr {$3::$1}

359


360

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

361

array_expr:

362

expr {[$1]}

363

 expr COMMA array_expr {$1::$3}

364


365

dim_list:

366

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

367

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

368


369

expr:

370

/* constants */

371

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

372

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

373

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

374

/* Idents or type enum tags */

375

 IDENT { mkexpr (Expr_ident $1) }

376

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

377

 LPAR ANNOT expr RPAR

378

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

379

 LPAR expr RPAR

380

{$2}

381

 LPAR tuple_expr RPAR

382

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

383


384

/* Array expressions */

385

 LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }

386

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

387

 expr LBRACKET dim_list { $3 $1 }

388


389

/* Temporal operators */

390

 PRE expr

391

{mkexpr (Expr_pre $2)}

392

 expr ARROW expr

393

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

394

 expr FBY expr

395

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

396

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

397

 expr WHEN vdecl_ident

398

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

399

 expr WHENNOT vdecl_ident

400

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

401

 expr WHEN tag_ident LPAR vdecl_ident RPAR

402

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

403

 MERGE vdecl_ident handler_expr_list

404

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

405


406

/* Applications */

407

 node_ident LPAR expr RPAR

408

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

409

 node_ident LPAR expr RPAR EVERY expr

410

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

411

 node_ident LPAR tuple_expr RPAR

412

{

413

let id=$1 in

414

let args=List.rev $3 in

415

match id, args with

416

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

417

let n = match n.expr_desc with

418

 Expr_const (Const_int n) > n

419

 _ > assert false

420

in

421

fby expr n init

422

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

423

}

424

 node_ident LPAR tuple_expr RPAR EVERY expr

425

{

426

let id=$1 in

427

let args=List.rev $3 in

428

let clock=$6 in

429

if id="fby" then

430

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

431

else

432

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

433

}

434


435

/* Boolean expr */

436

 expr AND expr

437

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

438

 expr AMPERAMPER expr

439

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

440

 expr OR expr

441

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

442

 expr BARBAR expr

443

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

444

 expr XOR expr

445

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

446

 NOT expr

447

{mkpredef_call "not" [$2]}

448

 expr IMPL expr

449

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

450


451

/* Comparison expr */

452

 expr EQ expr

453

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

454

 expr LT expr

455

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

456

 expr LTE expr

457

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

458

 expr GT expr

459

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

460

 expr GTE expr

461

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

462

 expr NEQ expr

463

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

464


465

/* Arithmetic expr */

466

 expr PLUS expr

467

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

468

 expr MINUS expr

469

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

470

 expr MULT expr

471

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

472

 expr DIV expr

473

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

474

 MINUS expr %prec UMINUS

475

{mkpredef_call "uminus" [$2]}

476

 expr MOD expr

477

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

478


479

/* If */

480

 IF expr THEN expr ELSE expr

481

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

482


483

handler_expr_list:

484

{ [] }

485

 handler_expr handler_expr_list { $1 :: $2 }

486


487

handler_expr:

488

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

489


490

signed_const_array:

491

 signed_const { [$1] }

492

 signed_const COMMA signed_const_array { $1 :: $3 }

493


494

signed_const_struct:

495

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

496

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

497


498

signed_const:

499

INT {Const_int $1}

500

 REAL {Const_real $1}

501

 FLOAT {Const_float $1}

502

 tag_ident {Const_tag $1}

503

 MINUS INT {Const_int (1 * $2)}

504

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

505

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

506

 LCUR signed_const_struct RCUR { Const_struct $2 }

507

 LBRACKET signed_const_array RBRACKET { Const_array $2 }

508


509

dim:

510

INT { mkdim_int $1 }

511

 LPAR dim RPAR { $2 }

512

 UIDENT { mkdim_ident $1 }

513

 IDENT { mkdim_ident $1 }

514

 dim AND dim

515

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

516

 dim AMPERAMPER dim

517

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

518

 dim OR dim

519

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

520

 dim BARBAR dim

521

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

522

 dim XOR dim

523

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

524

 NOT dim

525

{mkdim_appl "not" [$2]}

526

 dim IMPL dim

527

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

528


529

/* Comparison dim */

530

 dim EQ dim

531

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

532

 dim LT dim

533

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

534

 dim LTE dim

535

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

536

 dim GT dim

537

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

538

 dim GTE dim

539

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

540

 dim NEQ dim

541

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

542


543

/* Arithmetic dim */

544

 dim PLUS dim

545

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

546

 dim MINUS dim

547

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

548

 dim MULT dim

549

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

550

 dim DIV dim

551

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

552

 MINUS dim %prec UMINUS

553

{mkdim_appl "uminus" [$2]}

554

 dim MOD dim

555

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

556

/* If */

557

 IF dim THEN dim ELSE dim

558

{mkdim_ite $2 $4 $6}

559


560

locals:

561

{[]}

562

 VAR local_vdecl_list SCOL {$2}

563


564

vdecl_list:

565

vdecl {$1}

566

 vdecl_list SCOL vdecl {$3 @ $1}

567


568

vdecl:

569

ident_list COL typeconst clock

570

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

571

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

572

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

573

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

574

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

575


576

local_vdecl_list:

577

local_vdecl {$1}

578

 local_vdecl_list SCOL local_vdecl {$3 @ $1}

579


580

local_vdecl:

581

/* Useless no ?*/ ident_list

582

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

583

 ident_list COL typeconst clock

584

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

585

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

586

{ [ mkvar_decl ($2, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4) ] }

587

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

588

{ [ mkvar_decl ($2, mktyp $4, mkclock Ckdec_any, true, Some $6) ] }

589


590

cdecl_list:

591

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

592

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

593


594

cdecl:

595

const_ident EQ signed_const {

596

(fun itf >

597

let c = mktop_decl itf (Const {

598

const_id = $1;

599

const_loc = Location.symbol_rloc ();

600

const_type = Types.new_var ();

601

const_value = $3})

602

in

603

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

604

}

605


606

clock:

607

{mkclock Ckdec_any}

608

 when_list

609

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

610


611

when_cond:

612

WHEN IDENT {($2, tag_true)}

613

 WHENNOT IDENT {($2, tag_false)}

614

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

615


616

when_list:

617

when_cond {[$1]}

618

 when_list when_cond {$2::$1}

619


620

ident_list:

621

vdecl_ident {[$1]}

622

 ident_list COMMA vdecl_ident {$3::$1}

623


624

SCOL_opt:

625

SCOL {}  {}

626


627


628

lustre_annot:

629

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

630


631

lustre_annot_list:

632

{ [] }

633

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

634

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

635

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

636

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

637


638

kwd:

639

DIV { [] }

640

 DIV IDENT kwd { $2::$3}

641


642

%%

643

(* Local Variables: *)

644

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

645

(* End: *)

646


647

