Revision 70e1006b src/parser_lustre.mly
src/parser_lustre.mly  

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 
let mktyp x = mktyp (get_loc ()) x 

21 
let mkclock x = mkclock (get_loc ()) x 

22 
let mkvar_decl x = mkvar_decl (get_loc ()) x 

23 
let mkexpr x = mkexpr (get_loc ()) x 

24 
let mkeexpr x = mkeexpr (get_loc ()) x 

25 
let mkeq x = mkeq (get_loc ()) x 

26 
let mkassert x = mkassert (get_loc ()) x 

27 
let mktop_decl x = mktop_decl (get_loc ()) x 

28 
let mkpredef_call x = mkpredef_call (get_loc ()) x 

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

30  
31 
let mkdim_int i = mkdim_int (get_loc ()) i 

32 
let mkdim_bool b = mkdim_bool (get_loc ()) b 

33 
let mkdim_ident id = mkdim_ident (get_loc ()) id 

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

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

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

38  
39 
%} 

40  
41 
%token <int> INT 

42 
%token <string> REAL 

43 
%token <float> FLOAT 

44 
%token <string> STRING 

45 
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST 

46 
%token STATELESS ASSERT OPEN QUOTE FUNCTION 

47 
%token <string> IDENT 

48 
%token <LustreSpec.expr_annot> ANNOT 

49 
%token <LustreSpec.node_annot> NODESPEC 

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

51 
%token AMPERAMPER BARBAR NOT POWER 

52 
%token IF THEN ELSE 

53 
%token UCLOCK DCLOCK PHCLOCK TAIL 

54 
%token MERGE FBY WHEN WHENNOT EVERY 

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

56 
%token STRUCT ENUM 

57 
%token TINT TFLOAT TREAL TBOOL TCLOCK 

58 
%token RATE DUE 

59 
%token EQ LT GT LTE GTE NEQ 

60 
%token AND OR XOR IMPL 

61 
%token MULT DIV MOD 

62 
%token MINUS PLUS UMINUS 

63 
%token PRE ARROW 

64 
%token REQUIRES ENSURES OBSERVER 

65 
%token INVARIANT BEHAVIOR ASSUMES 

66 
%token EXISTS FORALL 

67 
%token PROTOTYPE LIB 

68 
%token EOF 

69  
70 
%nonassoc prec_exists prec_forall 

71 
%nonassoc COMMA 

72 
%left MERGE IF 

73 
%nonassoc ELSE 

74 
%right ARROW FBY 

75 
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK 

76 
%right COLCOL 

77 
%right IMPL 

78 
%left OR XOR BARBAR 

79 
%left AND AMPERAMPER 

80 
%left NOT 

81 
%nonassoc INT 

82 
%nonassoc EQ LT GT LTE GTE NEQ 

83 
%left MINUS PLUS 

84 
%left MULT DIV MOD 

85 
%left UMINUS 

86 
%left POWER 

87 
%left PRE LAST 

88 
%nonassoc RBRACKET 

89 
%nonassoc LBRACKET 

90  
91 
%start prog 

92 
%type <LustreSpec.top_decl list> prog 

93  
94 
%start header 

95 
%type <bool > LustreSpec.top_decl list> header 

96  
97 
%start lustre_annot 

98 
%type <LustreSpec.expr_annot> lustre_annot 

99  
100 
%start lustre_spec 

101 
%type <LustreSpec.node_annot> lustre_spec 

102  
103 
%% 

104  
105 
prog: 

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

107  
108 
typ_def_prog: 

109 
typ_def_list { $1 true } 

110  
111 
header: 

112 
open_list typ_def_list top_decl_header_list EOF { (fun own > ($1 @ let typs = $2 own in typs @ (List.rev ($3 own)))) } 

113  
114 
open_list: 

115 
{ [] } 

116 
 open_lusi open_list { $1 :: $2 } 

117  
118 
open_lusi: 

119 
 OPEN QUOTE IDENT QUOTE { mktop_decl (Open (true, $3))} 

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

121  
122 
top_decl_list: 

123 
{[]} 

124 
 top_decl_list top_decl {$2::$1} 

125  
126  
127 
top_decl_header_list: 

128 
{(fun own > []) } 

129 
 top_decl_header_list top_decl_header {(fun own > let h1 = $1 own in ($2 own)::h1) } 

130  
131 
state_annot: 

132 
FUNCTION { true } 

133 
 NODE { false } 

134  
135 
top_decl_header: 

136 
 CONST cdecl_list { let top = mktop_decl (Consts (List.rev $2)) in fun _ > top } 

137 
 nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_opt SCOL 

138 
{let nd = mktop_decl (ImportedNode 

139 
{nodei_id = $3; 

140 
nodei_type = Types.new_var (); 

141 
nodei_clock = Clocks.new_var true; 

142 
nodei_inputs = List.rev $5; 

143 
nodei_outputs = List.rev $10; 

144 
nodei_stateless = $2; 

145 
nodei_spec = $1; 

146 
nodei_prototype = $13; 

147 
nodei_in_lib = $14;}) 

148 
in 

149 
(fun own > add_node own $3 nd; nd) } 

150  
151 
prototype_opt: 

152 
{ None } 

153 
 PROTOTYPE IDENT { Some $2} 

154  
155 
in_lib_opt: 

156 
{ None } 

157 
 LIB IDENT {Some $2} 

158  
159 
top_decl: 

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

161 
 nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 

162 
{let eqs, asserts, annots = $16 in 

163 
let nd = mktop_decl (Node 

164 
{node_id = $3; 

165 
node_type = Types.new_var (); 

166 
node_clock = Clocks.new_var true; 

167 
node_inputs = List.rev $5; 

168 
node_outputs = List.rev $10; 

169 
node_locals = List.rev $14; 

170 
node_gencalls = []; 

171 
node_checks = []; 

172 
node_asserts = asserts; 

173 
node_eqs = eqs; 

174 
node_dec_stateless = $2; 

175 
node_stateless = None; 

176 
node_spec = $1; 

177 
node_annot = annots}) 

178 
in 

179 
add_node true $3 nd; nd} 

180  
181 
nodespec_list: 

182 
{ None } 

183 
 NODESPEC nodespec_list { 

184 
(function 

185 
 None > (fun s1 > Some s1) 

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

187  
188 
typ_def_list: 

189 
/* empty */ { (fun own > []) } 

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

191  
192 
typ_def: 

193 
TYPE IDENT EQ typ_def_rhs { let typ = mktop_decl (Type { ty_def_id = $2; 

194 
ty_def_desc = $4 

195 
}) 

196 
in (fun own > add_type own $2 typ; typ) } 

197  
198 
typ_def_rhs: 

199 
typeconst { $1 } 

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

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

202  
203 
array_typ_decl: 

204 
{ fun typ > typ } 

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

206  
207 
typeconst: 

208 
TINT array_typ_decl { $2 Tydec_int } 

209 
 TBOOL array_typ_decl { $2 Tydec_bool } 

210 
 TREAL array_typ_decl { $2 Tydec_real } 

211 
 TFLOAT array_typ_decl { $2 Tydec_float } 

212 
 IDENT array_typ_decl { $2 (Tydec_const $1) } 

213 
 TBOOL TCLOCK { Tydec_clock Tydec_bool } 

214 
 IDENT TCLOCK { Tydec_clock (Tydec_const $1) } 

215  
216 
tag_list: 

217 
IDENT { $1 :: [] } 

218 
 tag_list COMMA IDENT { $3 :: $1 } 

219 


220 
field_list: { [] } 

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

222 


223 
eq_list: 

224 
{ [], [], [] } 

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

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

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

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

229  
230 
automaton: 

231 
AUTOMATON IDENT handler_list { failwith "not implemented" } 

232  
233 
handler_list: 

234 
{ [] } 

235 
 handler handler_list { $1::$2 } 

236  
237 
handler: 

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

239  
240 
unless_list: 

241 
{ [] } 

242 
 unless unless_list { $1::$2 } 

243  
244 
until_list: 

245 
{ [] } 

246 
 until until_list { $1::$2 } 

247  
248 
unless: 

249 
UNLESS expr RESTART IDENT { } 

250 
 UNLESS expr RESUME IDENT { } 

251  
252 
until: 

253 
UNTIL expr RESTART IDENT { } 

254 
 UNTIL expr RESUME IDENT { } 

255  
256 
assert_: 

257 
 ASSERT expr SCOL {mkassert ($2)} 

258  
259 
eq: 

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

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

262  
263 
lustre_spec: 

264 
 contract EOF { $1 } 

265  
266 
contract: 

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

268 


269 
requires: 

270 
{ [] } 

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

272  
273 
ensures: 

274 
{ [] } 

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

276 
 OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { 

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

278 
} 

279  
280 
behaviors: 

281 
{ [] } 

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

283  
284 
assumes: 

285 
{ [] } 

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

287  
288 
/* WARNING: UNUSED RULES */ 

289 
tuple_qexpr: 

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

291 
 tuple_qexpr COMMA qexpr {$3::$1} 

292  
293 
qexpr: 

294 
 expr { mkeexpr $1 } 

295 
/* Quantifiers */ 

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

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

298  
299  
300 
tuple_expr: 

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

302 
 tuple_expr COMMA expr {$3::$1} 

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

305 
array_expr: 

306 
expr {[$1]} 

307 
 expr COMMA array_expr {$1::$3} 

308  
309 
dim_list: 

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

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

312  
313 
expr: 

314 
/* constants */ 

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

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

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

318 
/* Idents or type enum tags */ 

319 
 IDENT { 

320 
if Hashtbl.mem tag_table $1 

321 
then mkexpr (Expr_const (Const_tag $1)) 

322 
else mkexpr (Expr_ident $1)} 

323 
 LPAR ANNOT expr RPAR 

324 
{update_expr_annot $3 $2} 

325 
 LPAR expr RPAR 

326 
{$2} 

327 
 LPAR tuple_expr RPAR 

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

329  
330 
/* Array expressions */ 

331 
 LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) } 

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

333 
 expr LBRACKET dim_list { $3 $1 } 

334  
335 
/* Temporal operators */ 

336 
 PRE expr 

337 
{mkexpr (Expr_pre $2)} 

338 
 expr ARROW expr 

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

340 
 expr FBY expr 

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

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

343 
 expr WHEN IDENT 

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

345 
 expr WHENNOT IDENT 

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

347 
 expr WHEN IDENT LPAR IDENT RPAR 

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

349 
 MERGE IDENT handler_expr_list 

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

351  
352 
/* Applications */ 

353 
 IDENT LPAR expr RPAR 

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

355 
 IDENT LPAR expr RPAR EVERY IDENT 

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

357 
 IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR 

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

359 
 IDENT LPAR tuple_expr RPAR 

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

361 
 IDENT LPAR tuple_expr RPAR EVERY IDENT 

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

363 
 IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR 

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

365  
366 
/* Boolean expr */ 

367 
 expr AND expr 

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

369 
 expr AMPERAMPER expr 

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

371 
 expr OR expr 

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

373 
 expr BARBAR expr 

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

375 
 expr XOR expr 

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

377 
 NOT expr 

378 
{mkpredef_call "not" [$2]} 

379 
 expr IMPL expr 

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

381  
382 
/* Comparison expr */ 

383 
 expr EQ expr 

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

385 
 expr LT expr 

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

387 
 expr LTE expr 

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

389 
 expr GT expr 

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

391 
 expr GTE expr 

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

393 
 expr NEQ expr 

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

395  
396 
/* Arithmetic expr */ 

397 
 expr PLUS expr 

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

399 
 expr MINUS expr 

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

401 
 expr MULT expr 

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

403 
 expr DIV expr 

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

405 
 MINUS expr %prec UMINUS 

406 
{mkpredef_call "uminus" [$2]} 

407 
 expr MOD expr 

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

409  
410 
/* If */ 

411 
 IF expr THEN expr ELSE expr 

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

413  
414 
handler_expr_list: 

415 
{ [] } 

416 
 handler_expr handler_expr_list { $1 :: $2 } 

417  
418 
handler_expr: 

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

420  
421 
signed_const_array: 

422 
 signed_const { [$1] } 

423 
 signed_const COMMA signed_const_array { $1 :: $3 } 

424  
425 
signed_const_struct: 

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

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

428  
429 
signed_const: 

430 
INT {Const_int $1} 

431 
 REAL {Const_real $1} 

432 
 FLOAT {Const_float $1} 

433 
 IDENT {Const_tag $1} 

434 
 MINUS INT {Const_int (1 * $2)} 

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

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

437 
 LCUR signed_const_struct RCUR { Const_struct $2 } 

438 
 LBRACKET signed_const_array RBRACKET { Const_array $2 } 

439  
440 
dim: 

441 
INT { mkdim_int $1 } 

442 
 LPAR dim RPAR { $2 } 

443 
 IDENT { mkdim_ident $1 } 

444 
 dim AND dim 

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

446 
 dim AMPERAMPER dim 

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

448 
 dim OR dim 

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

450 
 dim BARBAR dim 

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

452 
 dim XOR dim 

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

454 
 NOT dim 

455 
{mkdim_appl "not" [$2]} 

456 
 dim IMPL dim 

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

458  
459 
/* Comparison dim */ 

460 
 dim EQ dim 

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

462 
 dim LT dim 

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

464 
 dim LTE dim 

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

466 
 dim GT dim 

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

468 
 dim GTE dim 

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

470 
 dim NEQ dim 

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

472  
473 
/* Arithmetic dim */ 

474 
 dim PLUS dim 

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

476 
 dim MINUS dim 

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

478 
 dim MULT dim 

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

480 
 dim DIV dim 

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

482 
 MINUS dim %prec UMINUS 

483 
{mkdim_appl "uminus" [$2]} 

484 
 dim MOD dim 

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

486 
/* If */ 

487 
 IF dim THEN dim ELSE dim 

488 
{mkdim_ite $2 $4 $6} 

489  
490 
locals: 

491 
{[]} 

492 
 VAR vdecl_list SCOL {$2} 

493  
494 
vdecl_list: 

495 
vdecl {$1} 

496 
 vdecl_list SCOL vdecl {$3 @ $1} 

497  
498 
vdecl: 

499 
/* Useless no ?*/ ident_list 

500 
{List.map mkvar_decl 

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

502  
503 
 ident_list COL typeconst clock 

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

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

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

507  
508 
cdecl_list: 

509 
cdecl SCOL { [$1] } 

510 
 cdecl_list cdecl SCOL { $2::$1 } 

511  
512 
cdecl: 

513 
IDENT EQ signed_const { 

514 
let c = { 

515 
const_id = $1; 

516 
const_loc = Location.symbol_rloc (); 

517 
const_type = Types.new_var (); 

518 
const_value = $3; 

519 
} in 

520 
Hashtbl.add consts_table $1 c; c 

521 
} 

522  
523 
clock: 

524 
{mkclock Ckdec_any} 

525 
 when_list 

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

527  
528 
when_cond: 

529 
WHEN IDENT {($2, tag_true)} 

530 
 WHENNOT IDENT {($2, tag_false)} 

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

532  
533 
when_list: 

534 
when_cond {[$1]} 

535 
 when_list when_cond {$2::$1} 

536  
537 
ident_list: 

538 
IDENT {[$1]} 

539 
 ident_list COMMA IDENT {$3::$1} 

540  
541 
SCOL_opt: 

542 
SCOL {}  {} 

543  
544  
545 
lustre_annot: 

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

547  
548 
lustre_annot_list: 

549 
{ [] } 

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

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

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

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

554  
555 
kwd: 

556 
DIV { [] } 

557 
 DIV IDENT kwd { $2::$3} 

558  
559 
%% 

560 
(* Local Variables: *) 

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

562 
(* End: *) 

563  
564  
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 ()) 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 eq_list TEL 

192 
{let eqs, 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_eqs = eqs; 

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 
eq_list: 

255 
{ [], [], [] } 

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

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

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

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

260  
261 
automaton: 

262 
AUTOMATON type_ident handler_list { failwith "not implemented" } 

263  
264 
handler_list: 

265 
{ [] } 

266 
 handler handler_list { $1::$2 } 

267  
268 
handler: 

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

270  
271 
unless_list: 

272 
{ Automata.init } 

273 
 unless unless_list { let (expr1, case1) = $1 in (fun case > Automata.add_branch expr1 case1 ($2 case)) } 

274  
275 
until_list: 

276 
{ Automata.init } 

277 
 until until_list { let (expr1, case1) = $1 in (fun case > Automata.add_branch expr1 case1 ($2 case)) } 

278  
279 
unless: 

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

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

282  
283 
until: 

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

285 
 UNTIL expr RESUME UIDENT { ($2, (get_loc (), 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 vdecl_ident 

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

386 
 node_ident LPAR expr RPAR EVERY tag_ident LPAR vdecl_ident RPAR 

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

388 
 node_ident LPAR tuple_expr RPAR 

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

390 
 node_ident LPAR tuple_expr RPAR EVERY vdecl_ident 

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

392 
 node_ident LPAR tuple_expr RPAR EVERY tag_ident LPAR vdecl_ident RPAR 

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

394  
395 
/* Boolean expr */ 

396 
 expr AND expr 

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

398 
 expr AMPERAMPER expr 

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

400 
 expr OR expr 

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

402 
 expr BARBAR expr 

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

404 
 expr XOR expr 

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

406 
 NOT expr 

407 
{mkpredef_call "not" [$2]} 

408 
 expr IMPL expr 

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

410  
411 
/* Comparison expr */ 

412 
 expr EQ expr 

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

414 
 expr LT expr 

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

416 
 expr LTE expr 

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

418 
 expr GT expr 

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

420 
 expr GTE expr 

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

422 
 expr NEQ expr 

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

424  
425 
/* Arithmetic expr */ 

426 
 expr PLUS expr 

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

428 
 expr MINUS expr 

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

430 
 expr MULT expr 

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

432 
 expr DIV expr 

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

434 
 MINUS expr %prec UMINUS 

435 
{mkpredef_call "uminus" [$2]} 

436 
 expr MOD expr 

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

438  
439 
/* If */ 

440 
 IF expr THEN expr ELSE expr 

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

442  
443 
handler_expr_list: 

444 
{ [] } 

445 
 handler_expr handler_expr_list { $1 :: $2 } 

446  
447 
handler_expr: 

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

449  
450 
signed_const_array: 

451 
 signed_const { [$1] } 

452 
 signed_const COMMA signed_const_array { $1 :: $3 } 

453  
454 
signed_const_struct: 

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

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

457  
458 
signed_const: 

459 
INT {Const_int $1} 

460 
 REAL {Const_real $1} 

461 
 FLOAT {Const_float $1} 

462 
 tag_ident {Const_tag $1} 

463 
 MINUS INT {Const_int (1 * $2)} 

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

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

466 
 LCUR signed_const_struct RCUR { Const_struct $2 } 

467 
 LBRACKET signed_const_array RBRACKET { Const_array $2 } 

468  
469 
dim: 

470 
INT { mkdim_int $1 } 

471 
 LPAR dim RPAR { $2 } 

472 
 UIDENT { mkdim_ident $1 } 

473 
 IDENT { mkdim_ident $1 } 

474 
 dim AND dim 

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

476 
 dim AMPERAMPER dim 

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

478 
 dim OR dim 

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

480 
 dim BARBAR dim 

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

482 
 dim XOR dim 

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

484 
 NOT dim 

485 
{mkdim_appl "not" [$2]} 

486 
 dim IMPL dim 

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

488  
489 
/* Comparison dim */ 

490 
 dim EQ dim 

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

492 
 dim LT dim 

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

494 
 dim LTE dim 

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

496 
 dim GT dim 

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

498 
 dim GTE dim 

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

500 
 dim NEQ dim 

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

502  
503 
/* Arithmetic dim */ 

504 
 dim PLUS dim 

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

506 
 dim MINUS dim 

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

508 
 dim MULT dim 

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

510 
 dim DIV dim 

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

512 
 MINUS dim %prec UMINUS 

513 
{mkdim_appl "uminus" [$2]} 

514 
 dim MOD dim 

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

516 
/* If */ 

517 
 IF dim THEN dim ELSE dim 

518 
{mkdim_ite $2 $4 $6} 

519  
520 
locals: 

521 
{[]} 

522 
 VAR vdecl_list SCOL {$2} 

523  
524 
vdecl_list: 

525 
vdecl {$1} 

526 
 vdecl_list SCOL vdecl {$3 @ $1} 

527  
528 
vdecl: 

529 
/* Useless no ?*/ ident_list 

530 
{List.map mkvar_decl 

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

532  
533 
 ident_list COL typeconst clock 

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

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

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

537  
538 
cdecl_list: 

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

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

541  
542 
cdecl: 

543 
const_ident EQ signed_const { 

544 
(fun itf > 

545 
let c = mktop_decl itf (Const { 

546 
const_id = $1; 

547 
const_loc = Location.symbol_rloc (); 

548 
const_type = Types.new_var (); 

549 
const_value = $3}) 

550 
in 

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

552 
} 

553  
554 
clock: 

555 
{mkclock Ckdec_any} 

556 
 when_list 

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

558  
559 
when_cond: 

560 
WHEN IDENT {($2, tag_true)} 

561 
 WHENNOT IDENT {($2, tag_false)} 

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

563  
564 
when_list: 

565 
when_cond {[$1]} 

566 
 when_list when_cond {$2::$1} 

567  
568 
ident_list: 

569 
vdecl_ident {[$1]} 

570 
 ident_list COMMA vdecl_ident {$3::$1} 

571  
572 
SCOL_opt: 

573 
SCOL {}  {} 

574  
575  
576 
lustre_annot: 

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

578  
579 
lustre_annot_list: 

580 
{ [] } 

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

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

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

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

585  
586 
kwd: 

587 
DIV { [] } 

588 
 DIV IDENT kwd { $2::$3} 

589  
590 
%% 

591 
(* Local Variables: *) 

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

593 
(* End: *) 

594  
595 
Also available in: Unified diff