## lustrec / src / parser_lustre.mly @ 2c083577

History | View | Annotate | Download (17 KB)

1 | ef34b4ae | xthirioux | /********************************************************************/ |
---|---|---|---|

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 | 54d032f5 | xthirioux | let mkvar_decl x = mkvar_decl (get_loc ()) ~orig:true x |

24 | ef34b4ae | xthirioux | 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 | 566dbf49 | ploc | 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 | ef34b4ae | xthirioux | %} |

47 | |||

48 | %token <int> INT |
||

49 | %token <string> REAL |
||

50 | %token <float> FLOAT |
||

51 | %token <string> STRING |
||

52 | %token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST |
||

53 | %token STATELESS ASSERT OPEN QUOTE FUNCTION |
||

54 | %token <string> IDENT |
||

55 | %token <string> UIDENT |
||

56 | %token TRUE FALSE |
||

57 | %token <LustreSpec.expr_annot> ANNOT |
||

58 | %token <LustreSpec.node_annot> NODESPEC |
||

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

60 | %token AMPERAMPER BARBAR NOT POWER |
||

61 | %token IF THEN ELSE |
||

62 | %token UCLOCK DCLOCK PHCLOCK TAIL |
||

63 | %token MERGE FBY WHEN WHENNOT EVERY |
||

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

65 | %token STRUCT ENUM |
||

66 | %token TINT TFLOAT TREAL TBOOL TCLOCK |
||

67 | %token RATE DUE |
||

68 | %token EQ LT GT LTE GTE NEQ |
||

69 | %token AND OR XOR IMPL |
||

70 | %token MULT DIV MOD |
||

71 | %token MINUS PLUS UMINUS |
||

72 | %token PRE ARROW |
||

73 | %token REQUIRES ENSURES OBSERVER |
||

74 | %token INVARIANT BEHAVIOR ASSUMES |
||

75 | %token EXISTS FORALL |
||

76 | %token PROTOTYPE LIB |
||

77 | %token EOF |
||

78 | |||

79 | %nonassoc prec_exists prec_forall |
||

80 | %nonassoc COMMA |
||

81 | ec433d69 | xthirioux | %nonassoc EVERY |

82 | ef34b4ae | xthirioux | %left MERGE IF |

83 | %nonassoc ELSE |
||

84 | %right ARROW FBY |
||

85 | %left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK |
||

86 | %right COLCOL |
||

87 | %right IMPL |
||

88 | %left OR XOR BARBAR |
||

89 | %left AND AMPERAMPER |
||

90 | %left NOT |
||

91 | %nonassoc INT |
||

92 | %nonassoc EQ LT GT LTE GTE NEQ |
||

93 | %left MINUS PLUS |
||

94 | %left MULT DIV MOD |
||

95 | %left UMINUS |
||

96 | %left POWER |
||

97 | %left PRE LAST |
||

98 | %nonassoc RBRACKET |
||

99 | %nonassoc LBRACKET |
||

100 | |||

101 | %start prog |
||

102 | %type <LustreSpec.top_decl list> prog |
||

103 | |||

104 | %start header |
||

105 | %type <LustreSpec.top_decl list> header |
||

106 | |||

107 | %start lustre_annot |
||

108 | %type <LustreSpec.expr_annot> lustre_annot |
||

109 | |||

110 | %start lustre_spec |
||

111 | %type <LustreSpec.node_annot> lustre_spec |
||

112 | |||

113 | %% |
||

114 | |||

115 | module_ident: |
||

116 | UIDENT { $1 } |
||

117 | | IDENT { $1 } |
||

118 | |||

119 | tag_ident: |
||

120 | UIDENT { $1 } |
||

121 | | TRUE { tag_true } |
||

122 | | FALSE { tag_false } |
||

123 | |||

124 | node_ident: |
||

125 | UIDENT { $1 } |
||

126 | | IDENT { $1 } |
||

127 | |||

128 | 566dbf49 | ploc | node_ident_decl: |

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

130 | |||

131 | ef34b4ae | xthirioux | vdecl_ident: |

132 | UIDENT { $1 } |
||

133 | | IDENT { $1 } |
||

134 | |||

135 | const_ident: |
||

136 | UIDENT { $1 } |
||

137 | | IDENT { $1 } |
||

138 | |||

139 | type_ident: |
||

140 | IDENT { $1 } |
||

141 | |||

142 | prog: |
||

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

144 | |||

145 | typ_def_prog: |
||

146 | typ_def_list { $1 false } |
||

147 | |||

148 | header: |
||

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

150 | |||

151 | typ_def_header: |
||

152 | typ_def_list { $1 true } |
||

153 | |||

154 | open_list: |
||

155 | { [] } |
||

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

157 | |||

158 | open_lusi: |
||

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

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

161 | |||

162 | top_decl_list: |
||

163 | {[]} |
||

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

165 | |||

166 | |||

167 | top_decl_header_list: |
||

168 | { [] } |
||

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

170 | |||

171 | state_annot: |
||

172 | FUNCTION { true } |
||

173 | | NODE { false } |
||

174 | |||

175 | top_decl_header: |
||

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

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

178 | {let nd = mktop_decl true (ImportedNode |
||

179 | {nodei_id = $3; |
||

180 | nodei_type = Types.new_var (); |
||

181 | nodei_clock = Clocks.new_var true; |
||

182 | nodei_inputs = List.rev $5; |
||

183 | nodei_outputs = List.rev $10; |
||

184 | nodei_stateless = $2; |
||

185 | nodei_spec = $1; |
||

186 | nodei_prototype = $13; |
||

187 | nodei_in_lib = $14;}) |
||

188 | in |
||

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

190 | |||

191 | prototype_opt: |
||

192 | { None } |
||

193 | | PROTOTYPE node_ident { Some $2} |
||

194 | |||

195 | in_lib_opt: |
||

196 | { None } |
||

197 | | LIB module_ident {Some $2} |
||

198 | |||

199 | top_decl: |
||

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

201 | 566dbf49 | ploc | | 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 |

202 | { |
||

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

204 | (* Declaring eqs annots *) |
||

205 | List.iter (fun ann -> |
||

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

207 | Annotations.add_node_ann $3 key |
||

208 | ) ann.annots |
||

209 | ) annots; |
||

210 | (* Building the node *) |
||

211 | let nd = mktop_decl false (Node |
||

212 | {node_id = $3; |
||

213 | node_type = Types.new_var (); |
||

214 | node_clock = Clocks.new_var true; |
||

215 | node_inputs = List.rev $5; |
||

216 | node_outputs = List.rev $10; |
||

217 | node_locals = List.rev $14; |
||

218 | node_gencalls = []; |
||

219 | node_checks = []; |
||

220 | node_asserts = asserts; |
||

221 | node_stmts = stmts; |
||

222 | node_dec_stateless = $2; |
||

223 | node_stateless = None; |
||

224 | node_spec = $1; |
||

225 | node_annot = annots}) |
||

226 | in |
||

227 | 6efbcb73 | xthirioux | pop_node (); |

228 | ef34b4ae | xthirioux | (*add_node $3 nd;*) [nd] } |

229 | 566dbf49 | ploc | |

230 | nodespec_list: |
||

231 | ef34b4ae | xthirioux | { None } |

232 | | NODESPEC nodespec_list { |
||

233 | (function |
||

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

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

236 | |||

237 | typ_def_list: |
||

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

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

240 | |||

241 | typ_def: |
||

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

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

244 | tydef_desc = $4 |
||

245 | }) |
||

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

247 | |||

248 | typ_def_rhs: |
||

249 | typeconst { $1 } |
||

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

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

252 | |||

253 | array_typ_decl: |
||

254 | { fun typ -> typ } |
||

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

256 | |||

257 | typeconst: |
||

258 | TINT array_typ_decl { $2 Tydec_int } |
||

259 | | TBOOL array_typ_decl { $2 Tydec_bool } |
||

260 | | TREAL array_typ_decl { $2 Tydec_real } |
||

261 | | TFLOAT array_typ_decl { $2 Tydec_float } |
||

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

263 | | TBOOL TCLOCK { Tydec_clock Tydec_bool } |
||

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

265 | |||

266 | tag_list: |
||

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

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

269 | |||

270 | field_list: { [] } |
||

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

272 | |||

273 | b08ffca7 | xthirioux | stmt_list: |

274 | ef34b4ae | xthirioux | { [], [], [] } |

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

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

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

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

279 | ef34b4ae | xthirioux | |

280 | automaton: |
||

281 | d5767b5a | xthirioux | AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 } |

282 | ef34b4ae | xthirioux | |

283 | handler_list: |
||

284 | { [] } |
||

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

286 | |||

287 | handler: |
||

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

289 | ef34b4ae | xthirioux | |

290 | unless_list: |
||

291 | 2822cf55 | xthirioux | { [] } |

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

293 | ef34b4ae | xthirioux | |

294 | until_list: |
||

295 | 2822cf55 | xthirioux | { [] } |

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

297 | ef34b4ae | xthirioux | |

298 | unless: |
||

299 | 2822cf55 | xthirioux | UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4) } |

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

301 | ef34b4ae | xthirioux | |

302 | until: |
||

303 | 2822cf55 | xthirioux | UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4) } |

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

305 | ef34b4ae | xthirioux | |

306 | assert_: |
||

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

308 | |||

309 | eq: |
||

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

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

312 | |||

313 | lustre_spec: |
||

314 | | contract EOF { $1 } |
||

315 | |||

316 | contract: |
||

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

318 | |||

319 | requires: |
||

320 | { [] } |
||

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

322 | |||

323 | ensures: |
||

324 | { [] } |
||

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

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

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

328 | } |
||

329 | |||

330 | behaviors: |
||

331 | { [] } |
||

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

333 | |||

334 | assumes: |
||

335 | { [] } |
||

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

337 | |||

338 | /* WARNING: UNUSED RULES */ |
||

339 | tuple_qexpr: |
||

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

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

342 | |||

343 | qexpr: |
||

344 | | expr { mkeexpr $1 } |
||

345 | /* Quantifiers */ |
||

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

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

348 | |||

349 | |||

350 | tuple_expr: |
||

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

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

353 | |||

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

355 | array_expr: |
||

356 | expr {[$1]} |
||

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

358 | |||

359 | dim_list: |
||

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

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

362 | |||

363 | expr: |
||

364 | /* constants */ |
||

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

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

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

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

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

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

371 | | LPAR ANNOT expr RPAR |
||

372 | 566dbf49 | ploc | {update_expr_annot (get_current_node ()) $3 $2} |

373 | ef34b4ae | xthirioux | | LPAR expr RPAR |

374 | {$2} |
||

375 | | LPAR tuple_expr RPAR |
||

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

377 | |||

378 | /* Array expressions */ |
||

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

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

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

382 | |||

383 | /* Temporal operators */ |
||

384 | | PRE expr |
||

385 | {mkexpr (Expr_pre $2)} |
||

386 | | expr ARROW expr |
||

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

388 | | expr FBY expr |
||

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

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

391 | | expr WHEN vdecl_ident |
||

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

393 | | expr WHENNOT vdecl_ident |
||

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

395 | | expr WHEN tag_ident LPAR vdecl_ident RPAR |
||

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

397 | | MERGE vdecl_ident handler_expr_list |
||

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

399 | |||

400 | /* Applications */ |
||

401 | | node_ident LPAR expr RPAR |
||

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

403 | 54d032f5 | xthirioux | | node_ident LPAR expr RPAR EVERY expr |

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

405 | ef34b4ae | xthirioux | | node_ident LPAR tuple_expr RPAR |

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

407 | 54d032f5 | xthirioux | | node_ident LPAR tuple_expr RPAR EVERY expr |

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

409 | ef34b4ae | xthirioux | |

410 | /* Boolean expr */ |
||

411 | | expr AND expr |
||

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

413 | | expr AMPERAMPER expr |
||

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

415 | | expr OR expr |
||

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

417 | | expr BARBAR expr |
||

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

419 | | expr XOR expr |
||

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

421 | | NOT expr |
||

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

423 | | expr IMPL expr |
||

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

425 | |||

426 | /* Comparison expr */ |
||

427 | | expr EQ expr |
||

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

429 | | expr LT expr |
||

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

431 | | expr LTE expr |
||

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

433 | | expr GT expr |
||

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

435 | | expr GTE expr |
||

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

437 | | expr NEQ expr |
||

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

439 | |||

440 | /* Arithmetic expr */ |
||

441 | | expr PLUS expr |
||

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

443 | | expr MINUS expr |
||

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

445 | | expr MULT expr |
||

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

447 | | expr DIV expr |
||

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

449 | | MINUS expr %prec UMINUS |
||

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

451 | | expr MOD expr |
||

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

453 | |||

454 | /* If */ |
||

455 | | IF expr THEN expr ELSE expr |
||

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

457 | |||

458 | handler_expr_list: |
||

459 | { [] } |
||

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

461 | |||

462 | handler_expr: |
||

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

464 | |||

465 | signed_const_array: |
||

466 | | signed_const { [$1] } |
||

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

468 | |||

469 | signed_const_struct: |
||

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

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

472 | |||

473 | signed_const: |
||

474 | INT {Const_int $1} |
||

475 | | REAL {Const_real $1} |
||

476 | | FLOAT {Const_float $1} |
||

477 | | tag_ident {Const_tag $1} |
||

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

479 | | MINUS REAL {Const_real ("-" ^ $2)} |
||

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

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

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

483 | |||

484 | dim: |
||

485 | INT { mkdim_int $1 } |
||

486 | | LPAR dim RPAR { $2 } |
||

487 | | UIDENT { mkdim_ident $1 } |
||

488 | | IDENT { mkdim_ident $1 } |
||

489 | | dim AND dim |
||

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

491 | | dim AMPERAMPER dim |
||

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

493 | | dim OR dim |
||

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

495 | | dim BARBAR dim |
||

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

497 | | dim XOR dim |
||

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

499 | | NOT dim |
||

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

501 | | dim IMPL dim |
||

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

503 | |||

504 | /* Comparison dim */ |
||

505 | | dim EQ dim |
||

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

507 | | dim LT dim |
||

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

509 | | dim LTE dim |
||

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

511 | | dim GT dim |
||

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

513 | | dim GTE dim |
||

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

515 | | dim NEQ dim |
||

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

517 | |||

518 | /* Arithmetic dim */ |
||

519 | | dim PLUS dim |
||

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

521 | | dim MINUS dim |
||

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

523 | | dim MULT dim |
||

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

525 | | dim DIV dim |
||

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

527 | | MINUS dim %prec UMINUS |
||

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

529 | | dim MOD dim |
||

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

531 | /* If */ |
||

532 | | IF dim THEN dim ELSE dim |
||

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

534 | |||

535 | locals: |
||

536 | {[]} |
||

537 | ec433d69 | xthirioux | | VAR local_vdecl_list SCOL {$2} |

538 | ef34b4ae | xthirioux | |

539 | vdecl_list: |
||

540 | ec433d69 | xthirioux | vdecl {$1} |

541 | ef34b4ae | xthirioux | | vdecl_list SCOL vdecl {$3 @ $1} |

542 | |||

543 | vdecl: |
||

544 | ec433d69 | xthirioux | ident_list COL typeconst clock |

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

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

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

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

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

550 | |||

551 | local_vdecl_list: |
||

552 | local_vdecl {$1} |
||

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

554 | ef34b4ae | xthirioux | |

555 | ec433d69 | xthirioux | local_vdecl: |

556 | /* Useless no ?*/ ident_list |
||

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

558 | ef34b4ae | xthirioux | | ident_list COL typeconst clock |

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

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

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

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

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

564 | ef34b4ae | xthirioux | |

565 | cdecl_list: |
||

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

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

568 | |||

569 | cdecl: |
||

570 | const_ident EQ signed_const { |
||

571 | (fun itf -> |
||

572 | let c = mktop_decl itf (Const { |
||

573 | const_id = $1; |
||

574 | const_loc = Location.symbol_rloc (); |
||

575 | const_type = Types.new_var (); |
||

576 | const_value = $3}) |
||

577 | in |
||

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

579 | } |
||

580 | |||

581 | clock: |
||

582 | {mkclock Ckdec_any} |
||

583 | | when_list |
||

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

585 | |||

586 | when_cond: |
||

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

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

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

590 | |||

591 | when_list: |
||

592 | when_cond {[$1]} |
||

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

594 | |||

595 | ident_list: |
||

596 | vdecl_ident {[$1]} |
||

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

598 | |||

599 | SCOL_opt: |
||

600 | SCOL {} | {} |
||

601 | |||

602 | |||

603 | lustre_annot: |
||

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

605 | |||

606 | lustre_annot_list: |
||

607 | { [] } |
||

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

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

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

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

612 | |||

613 | kwd: |
||

614 | DIV { [] } |
||

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

616 | |||

617 | %% |
||

618 | (* Local Variables: *) |
||

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

620 | (* End: *) |
||

621 | |||

622 |