## lustrec / src / parser_lustre.mly @ 1ac315e3

History | View | Annotate | Download (18.4 KB)

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 Lustre_types |

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 (n-1) 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 |

60 |
%token ASSERT OPEN QUOTE FUNCTION |

61 |
%token <string> IDENT |

62 |
%token <string> UIDENT |

63 |
%token TRUE FALSE |

64 |
%token <Lustre_types.expr_annot> ANNOT |

65 |
%token <Lustre_types.contract_desc> NODESPEC |

66 |
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA |

67 |
/* unused token? */ |

68 |
%token COLCOL |

69 |
%token AMPERAMPER BARBAR NOT POWER |

70 |
%token IF THEN ELSE |

71 |
%token MERGE FBY WHEN WHENNOT EVERY |

72 |
%token NODE LET TEL RETURNS VAR TYPE CONST |

73 |
/* unused token? */ |

74 |
%token IMPORTED |

75 |
%token STRUCT ENUM |

76 |
%token TINT TREAL TBOOL TCLOCK |

77 |
%token EQ LT GT LTE GTE NEQ |

78 |
%token AND OR XOR IMPL |

79 |
%token MULT DIV MOD |

80 |
%token MINUS PLUS UMINUS |

81 |
%token PRE ARROW |

82 |
%token REQUIRES ENSURES OBSERVER |

83 |
%token INVARIANT BEHAVIOR ASSUMES CCODE MATLAB |

84 |
%token EXISTS FORALL |

85 |
%token PROTOTYPE LIB |

86 |
%token EOF |

87 | |

88 |
%nonassoc prec_exists prec_forall |

89 |
/* unused precedence rules*/ |

90 |
/* |

91 |
%nonassoc COMMA |

92 |
*/ |

93 |
%nonassoc EVERY |

94 |
/* unused precedence rules |

95 |
%left MERGE IF |

96 |
*/ |

97 |
%nonassoc ELSE |

98 |
%right ARROW FBY |

99 |
%left WHEN WHENNOT |

100 |
/* unused token |

101 |
%right COLCOL |

102 |
*/ |

103 |
%right IMPL |

104 |
%left OR XOR BARBAR |

105 |
%left AND AMPERAMPER |

106 |
%left NOT |

107 |
/* unused precedence rule |

108 |
%nonassoc INT |

109 |
*/ |

110 |
%nonassoc EQ LT GT LTE GTE NEQ |

111 |
%left MINUS PLUS |

112 |
%left MULT DIV MOD |

113 |
%left UMINUS |

114 |
%left POWER |

115 |
%left PRE |

116 |
%nonassoc RBRACKET |

117 |
%nonassoc LBRACKET |

118 | |

119 |
%start prog |

120 |
%type <Lustre_types.top_decl list> prog |

121 | |

122 |
%start header |

123 |
%type <Lustre_types.top_decl list> header |

124 | |

125 |
%start lustre_annot |

126 |
%type <Lustre_types.expr_annot> lustre_annot |

127 | |

128 |
%start lustre_spec |

129 |
%type <Lustre_types.contract_desc> lustre_spec |

130 | |

131 |
%start signed_const |

132 |
%type <Lustre_types.constant> signed_const |

133 | |

134 |
%start expr |

135 |
%type <Lustre_types.expr> expr |

136 | |

137 |
%start stmt_list |

138 |
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list |

139 | |

140 |
%start vdecl_list |

141 |
%type <Lustre_types.var_decl list> vdecl_list |

142 |
%% |

143 | |

144 |
module_ident: |

145 |
UIDENT { $1 } |

146 |
| IDENT { $1 } |

147 | |

148 |
tag_ident: |

149 |
UIDENT { $1 } |

150 |
| TRUE { tag_true } |

151 |
| FALSE { tag_false } |

152 | |

153 |
node_ident: |

154 |
UIDENT { $1 } |

155 |
| IDENT { $1 } |

156 | |

157 |
node_ident_decl: |

158 |
node_ident { push_node $1; $1 } |

159 | |

160 |
vdecl_ident: |

161 |
UIDENT { mkident $1 } |

162 |
| IDENT { mkident $1 } |

163 | |

164 |
const_ident: |

165 |
UIDENT { $1 } |

166 |
| IDENT { $1 } |

167 | |

168 |
type_ident: |

169 |
IDENT { $1 } |

170 | |

171 |
prog: |

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

173 | |

174 |
typ_def_prog: |

175 |
typ_def_list { $1 false } |

176 | |

177 |
header: |

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

179 | |

180 |
typ_def_header: |

181 |
typ_def_list { $1 true } |

182 | |

183 |
open_list: |

184 |
{ [] } |

185 |
| open_lusi open_list { $1 :: $2 } |

186 | |

187 |
open_lusi: |

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

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

190 | |

191 |
top_decl_list: |

192 |
{[]} |

193 |
| top_decl_list top_decl {$2@$1} |

194 | |

195 | |

196 |
top_decl_header_list: |

197 |
{ [] } |

198 |
| top_decl_header_list top_decl_header { $2@$1 } |

199 | |

200 |
state_annot: |

201 |
FUNCTION { true } |

202 |
| NODE { false } |

203 | |

204 |
top_decl_header: |

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

206 |
| 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 |

207 |
{let nd = mktop_decl true (ImportedNode |

208 |
{nodei_id = $3; |

209 |
nodei_type = Types.new_var (); |

210 |
nodei_clock = Clocks.new_var true; |

211 |
nodei_inputs = List.rev $5; |

212 |
nodei_outputs = List.rev $10; |

213 |
nodei_stateless = $2; |

214 |
nodei_spec = $1; |

215 |
nodei_prototype = $13; |

216 |
nodei_in_lib = $14;}) |

217 |
in |

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

219 | |

220 |
prototype_opt: |

221 |
{ None } |

222 |
| PROTOTYPE node_ident { Some $2} |

223 | |

224 |
in_lib_list: |

225 |
{ [] } |

226 |
| LIB module_ident in_lib_list { $2::$3 } |

227 | |

228 |
top_decl: |

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

230 |
| 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 |

231 |
{ |

232 |
let stmts, asserts, annots = $16 in |

233 |
(* Declaring eqs annots *) |

234 |
List.iter (fun ann -> |

235 |
List.iter (fun (key, _) -> |

236 |
Annotations.add_node_ann $3 key |

237 |
) ann.annots |

238 |
) annots; |

239 |
(* Building the node *) |

240 |
let nd = mktop_decl false (Node |

241 |
{node_id = $3; |

242 |
node_type = Types.new_var (); |

243 |
node_clock = Clocks.new_var true; |

244 |
node_inputs = List.rev $5; |

245 |
node_outputs = List.rev $10; |

246 |
node_locals = List.rev $14; |

247 |
node_gencalls = []; |

248 |
node_checks = []; |

249 |
node_asserts = asserts; |

250 |
node_stmts = stmts; |

251 |
node_dec_stateless = $2; |

252 |
node_stateless = None; |

253 |
node_spec = $1; |

254 |
node_annot = annots}) |

255 |
in |

256 |
pop_node (); |

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

258 | |

259 |
nodespec_list: |

260 |
{ None } |

261 |
| NODESPEC nodespec_list { |

262 |
(function |

263 |
| None -> (fun s1 -> Some s1) |

264 |
| Some s2 -> (fun s1 -> Some (merge_contracts s1 s2))) $2 $1 } |

265 | |

266 |
typ_def_list: |

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

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

269 | |

270 |
typ_def: |

271 |
TYPE type_ident EQ typ_def_rhs { (fun itf -> |

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

273 |
tydef_desc = $4 |

274 |
}) |

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

276 | |

277 |
typ_def_rhs: |

278 |
typeconst { $1 } |

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

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

281 | |

282 |
array_typ_decl: |

283 |
%prec POWER { fun typ -> typ } |

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

285 | |

286 |
typeconst: |

287 |
TINT array_typ_decl { $2 Tydec_int } |

288 |
| TBOOL array_typ_decl { $2 Tydec_bool } |

289 |
| TREAL array_typ_decl { $2 Tydec_real } |

290 |
/* | TFLOAT array_typ_decl { $2 Tydec_float } */ |

291 |
| type_ident array_typ_decl { $2 (Tydec_const $1) } |

292 |
| TBOOL TCLOCK { Tydec_clock Tydec_bool } |

293 |
| IDENT TCLOCK { Tydec_clock (Tydec_const $1) } |

294 | |

295 |
tag_list: |

296 |
UIDENT { $1 :: [] } |

297 |
| tag_list COMMA UIDENT { $3 :: $1 } |

298 | |

299 |
field_list: { [] } |

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

301 | |

302 |
stmt_list: |

303 |
{ [], [], [] } |

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

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

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

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

308 | |

309 |
automaton: |

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

311 | |

312 |
handler_list: |

313 |
{ [] } |

314 |
| handler handler_list { $1::$2 } |

315 | |

316 |
handler: |

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

318 | |

319 |
unless_list: |

320 |
{ [] } |

321 |
| unless unless_list { $1::$2 } |

322 | |

323 |
until_list: |

324 |
{ [] } |

325 |
| until until_list { $1::$2 } |

326 | |

327 |
unless: |

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

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

330 | |

331 |
until: |

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

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

334 | |

335 |
assert_: |

336 |
| ASSERT expr SCOL {mkassert ($2)} |

337 | |

338 |
eq: |

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

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

341 | |

342 |
lustre_spec: |

343 |
| contract EOF { $1 } |

344 | |

345 |
contract: |

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

347 | |

348 |
requires: |

349 |
{ [] } |

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

351 | |

352 |
ensures: |

353 |
{ [] } |

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

355 |
| OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures { |

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

357 |
} |

358 | |

359 |
behaviors: |

360 |
{ [] } |

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

362 | |

363 |
assumes: |

364 |
{ [] } |

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

366 | |

367 |
/* WARNING: UNREACHABLE RULE */ |

368 |
/* |

369 |
tuple_qexpr: |

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

371 |
| tuple_qexpr COMMA qexpr {$3::$1} |

372 |
*/ |

373 |
/* END OF UNREACHABLE RULE */ |

374 | |

375 |
qexpr: |

376 |
| expr { mkeexpr $1 } |

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

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

379 | |

380 |
tuple_expr: |

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

382 |
| tuple_expr COMMA expr {$3::$1} |

383 | |

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

385 |
array_expr: |

386 |
expr {[$1]} |

387 |
| expr COMMA array_expr {$1::$3} |

388 | |

389 |
dim_list: |

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

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

392 | |

393 |
expr: |

394 |
/* constants */ |

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

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

397 |
| STRING {mkexpr (Expr_const (Const_string $1))} |

398 | |

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

400 |
/* Idents or type enum tags */ |

401 |
| IDENT { mkexpr (Expr_ident $1) } |

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

403 |
| LPAR ANNOT expr RPAR |

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

405 |
| LPAR expr RPAR |

406 |
{$2} |

407 |
| LPAR tuple_expr RPAR |

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

409 | |

410 |
/* Array expressions */ |

411 |
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) } |

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

413 |
| expr LBRACKET dim_list { $3 $1 } |

414 | |

415 |
/* Temporal operators */ |

416 |
| PRE expr |

417 |
{mkexpr (Expr_pre $2)} |

418 |
| expr ARROW expr |

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

420 |
| expr FBY expr |

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

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

423 |
| expr WHEN vdecl_ident |

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

425 |
| expr WHENNOT vdecl_ident |

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

427 |
| expr WHEN tag_ident LPAR vdecl_ident RPAR |

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

429 |
| MERGE vdecl_ident handler_expr_list |

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

431 | |

432 |
/* Applications */ |

433 |
| node_ident LPAR expr RPAR |

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

435 |
| node_ident LPAR expr RPAR EVERY expr |

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

437 |
| node_ident LPAR tuple_expr RPAR |

438 |
{ |

439 |
let id=$1 in |

440 |
let args=List.rev $3 in |

441 |
match id, args with |

442 |
| "fbyn", [expr;n;init] -> |

443 |
let n = match n.expr_desc with |

444 |
| Expr_const (Const_int n) -> n |

445 |
| _ -> assert false |

446 |
in |

447 |
fby expr n init |

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

449 |
} |

450 |
| node_ident LPAR tuple_expr RPAR EVERY expr |

451 |
{ |

452 |
let id=$1 in |

453 |
let args=List.rev $3 in |

454 |
let clock=$6 in |

455 |
if id="fby" then |

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

457 |
else |

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

459 |
} |

460 | |

461 |
/* Boolean expr */ |

462 |
| expr AND expr |

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

464 |
| expr AMPERAMPER expr |

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

466 |
| expr OR expr |

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

468 |
| expr BARBAR expr |

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

470 |
| expr XOR expr |

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

472 |
| NOT expr |

473 |
{mkpredef_call "not" [$2]} |

474 |
| expr IMPL expr |

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

476 | |

477 |
/* Comparison expr */ |

478 |
| expr EQ expr |

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

480 |
| expr LT expr |

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

482 |
| expr LTE expr |

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

484 |
| expr GT expr |

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

486 |
| expr GTE expr |

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

488 |
| expr NEQ expr |

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

490 | |

491 |
/* Arithmetic expr */ |

492 |
| expr PLUS expr |

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

494 |
| expr MINUS expr |

495 |
{mkpredef_call "-" [$1;$3]} |

496 |
| expr MULT expr |

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

498 |
| expr DIV expr |

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

500 |
| MINUS expr %prec UMINUS |

501 |
{mkpredef_call "uminus" [$2]} |

502 |
| expr MOD expr |

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

504 | |

505 |
/* If */ |

506 |
| IF expr THEN expr ELSE expr |

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

508 | |

509 |
handler_expr_list: |

510 |
{ [] } |

511 |
| handler_expr handler_expr_list { $1 :: $2 } |

512 | |

513 |
handler_expr: |

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

515 | |

516 |
signed_const_array: |

517 |
| signed_const { [$1] } |

518 |
| signed_const COMMA signed_const_array { $1 :: $3 } |

519 | |

520 |
signed_const_struct: |

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

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

523 | |

524 |
signed_const: |

525 |
INT {Const_int $1} |

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

527 |
/* | FLOAT {Const_float $1} */ |

528 |
| tag_ident {Const_tag $1} |

529 |
| MINUS INT {Const_int (-1 * $2)} |

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

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

532 |
| LCUR signed_const_struct RCUR { Const_struct $2 } |

533 |
| LBRACKET signed_const_array RBRACKET { Const_array $2 } |

534 | |

535 |
dim: |

536 |
INT { mkdim_int $1 } |

537 |
| LPAR dim RPAR { $2 } |

538 |
| UIDENT { mkdim_ident $1 } |

539 |
| IDENT { mkdim_ident $1 } |

540 |
| dim AND dim |

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

542 |
| dim AMPERAMPER dim |

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

544 |
| dim OR dim |

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

546 |
| dim BARBAR dim |

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

548 |
| dim XOR dim |

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

550 |
| NOT dim |

551 |
{mkdim_appl "not" [$2]} |

552 |
| dim IMPL dim |

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

554 | |

555 |
/* Comparison dim */ |

556 |
| dim EQ dim |

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

558 |
| dim LT dim |

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

560 |
| dim LTE dim |

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

562 |
| dim GT dim |

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

564 |
| dim GTE dim |

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

566 |
| dim NEQ dim |

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

568 | |

569 |
/* Arithmetic dim */ |

570 |
| dim PLUS dim |

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

572 |
| dim MINUS dim |

573 |
{mkdim_appl "-" [$1;$3]} |

574 |
| dim MULT dim |

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

576 |
| dim DIV dim |

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

578 |
| MINUS dim %prec UMINUS |

579 |
{mkdim_appl "uminus" [$2]} |

580 |
| dim MOD dim |

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

582 |
/* If */ |

583 |
| IF dim THEN dim ELSE dim |

584 |
{mkdim_ite $2 $4 $6} |

585 | |

586 |
locals: |

587 |
{[]} |

588 |
| VAR local_vdecl_list SCOL {$2} |

589 | |

590 |
vdecl_list: |

591 |
vdecl {$1} |

592 |
| vdecl_list SCOL vdecl {$3 @ $1} |

593 | |

594 |
vdecl: |

595 |
ident_list COL typeconst clock |

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

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

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

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

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

601 | |

602 |
local_vdecl_list: |

603 |
local_vdecl {$1} |

604 |
| local_vdecl_list SCOL local_vdecl {$3 @ $1} |

605 | |

606 |
local_vdecl: |

607 |
/* Useless no ?*/ ident_list |

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

609 |
| ident_list COL typeconst clock |

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

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

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

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

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

615 | |

616 |
cdecl_list: |

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

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

619 | |

620 |
cdecl: |

621 |
const_ident EQ signed_const { |

622 |
(fun itf -> |

623 |
let c = mktop_decl itf (Const { |

624 |
const_id = $1; |

625 |
const_loc = Location.symbol_rloc (); |

626 |
const_type = Types.new_var (); |

627 |
const_value = $3}) |

628 |
in |

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

630 |
} |

631 | |

632 |
clock: |

633 |
{mkclock Ckdec_any} |

634 |
| when_list |

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

636 | |

637 |
when_cond: |

638 |
WHEN IDENT {($2, tag_true)} |

639 |
| WHENNOT IDENT {($2, tag_false)} |

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

641 | |

642 |
when_list: |

643 |
when_cond {[$1]} |

644 |
| when_list when_cond {$2::$1} |

645 | |

646 |
ident_list: |

647 |
vdecl_ident {[$1]} |

648 |
| ident_list COMMA vdecl_ident {$3::$1} |

649 | |

650 |
SCOL_opt: |

651 |
SCOL {} | {} |

652 | |

653 | |

654 |
lustre_annot: |

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

656 | |

657 |
lustre_annot_list: |

658 |
{ [] } |

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

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

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

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

663 |
| CCODE COL qexpr SCOL lustre_annot_list{ (["c_code"],$3)::$5 } |

664 |
| MATLAB COL qexpr SCOL lustre_annot_list{ (["matlab"],$3)::$5 } |

665 | |

666 | |

667 |
kwd: |

668 |
DIV { [] } |

669 |
| DIV IDENT kwd { $2::$3} |

670 | |

671 |
%% |

672 |
(* Local Variables: *) |

673 |
(* compile-command:"make -C .." *) |

674 |
(* End: *) |