## lustrec / src / parser_lustre.mly @ 01c7d5e1

History | View | Annotate | Download (16.6 KB)

1 | 22fe1c93 | ploc | /* ---------------------------------------------------------------------------- |
---|---|---|---|

2 | * SchedMCore - A MultiCore Scheduling Framework |
||

3 | * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
||

4 | * |
||

5 | * This file is part of Prelude |
||

6 | * |
||

7 | * Prelude is free software; you can redistribute it and/or |
||

8 | * modify it under the terms of the GNU Lesser General Public License |
||

9 | * as published by the Free Software Foundation ; either version 2 of |
||

10 | * the License, or (at your option) any later version. |
||

11 | * |
||

12 | * Prelude is distributed in the hope that it will be useful, but |
||

13 | * WITHOUT ANY WARRANTY ; without even the implied warranty of |
||

14 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
||

15 | * Lesser General Public License for more details. |
||

16 | * |
||

17 | * You should have received a copy of the GNU Lesser General Public |
||

18 | * License along with this program ; if not, write to the Free Software |
||

19 | * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
||

20 | * USA |
||

21 | *---------------------------------------------------------------------------- */ |
||

22 | |||

23 | %{ |
||

24 | open LustreSpec |
||

25 | open Corelang |
||

26 | open Dimension |
||

27 | open Utils |
||

28 | |||

29 | 01c7d5e1 | ploc | let get_loc () = Location.symbol_rloc () |

30 | let mktyp x = mktyp (get_loc ()) x |
||

31 | let mkclock x = mkclock (get_loc ()) x |
||

32 | let mkvar_decl x = mkvar_decl (get_loc ()) x |
||

33 | let mkexpr x = mkexpr (get_loc ()) x |
||

34 | let mkeexpr x = mkeexpr (get_loc ()) x |
||

35 | let mkeq x = mkeq (get_loc ()) x |
||

36 | let mkassert x = mkassert (get_loc ()) x |
||

37 | let mktop_decl x = mktop_decl (get_loc ()) x |
||

38 | let mkpredef_call x = mkpredef_call (get_loc ()) x |
||

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

40 | |||

41 | let mkdim_int i = mkdim_int (get_loc ()) i |
||

42 | let mkdim_bool b = mkdim_bool (get_loc ()) b |
||

43 | let mkdim_ident id = mkdim_ident (get_loc ()) id |
||

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

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

46 | |||

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

48 | 22fe1c93 | ploc | |

49 | 3826f8cb | ploc | let add_node loc own msg hashtbl name value = |

50 | 89b9e25c | xthirioux | try |

51 | match (Hashtbl.find hashtbl name).top_decl_desc, value.top_decl_desc with |
||

52 | 3826f8cb | ploc | | Node _ , ImportedNode _ when own -> () |

53 | | ImportedNode _, _ -> Hashtbl.add hashtbl name value |
||

54 | 01c7d5e1 | ploc | | Node _ , _ -> raise (Error (loc, Already_bound_symbol msg)) |

55 | 3826f8cb | ploc | | _ -> assert false |

56 | 89b9e25c | xthirioux | with |

57 | 3826f8cb | ploc | Not_found -> Hashtbl.add hashtbl name value |

58 | 89b9e25c | xthirioux | |

59 | 3826f8cb | ploc | |

60 | let add_symbol loc msg hashtbl name value = |
||

61 | 21485807 | xthirioux | if Hashtbl.mem hashtbl name |

62 | 01c7d5e1 | ploc | then raise (Error (loc, Already_bound_symbol msg)) |

63 | 21485807 | xthirioux | else Hashtbl.add hashtbl name value |

64 | |||

65 | 3826f8cb | ploc | let check_symbol loc msg hashtbl name = |

66 | 21485807 | xthirioux | if not (Hashtbl.mem hashtbl name) |

67 | 01c7d5e1 | ploc | then raise (Error (loc, Unbound_symbol msg)) |

68 | 21485807 | xthirioux | else () |

69 | |||

70 | 01c7d5e1 | ploc | let check_node_symbol msg name value = |

71 | if Hashtbl.mem node_table name |
||

72 | then () (* TODO: should we check the types here ? *) |
||

73 | else Hashtbl.add node_table name value |
||

74 | |||

75 | 22fe1c93 | ploc | %} |

76 | |||

77 | %token <int> INT |
||

78 | %token <string> REAL |
||

79 | %token <float> FLOAT |
||

80 | 01c7d5e1 | ploc | %token <string> STRING |

81 | 22fe1c93 | ploc | %token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST |

82 | 5c1184ad | ploc | %token STATELESS ASSERT OPEN QUOTE FUNCTION |

83 | 22fe1c93 | ploc | %token <string> IDENT |

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

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

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

87 | %token AMPERAMPER BARBAR NOT POWER |
||

88 | %token IF THEN ELSE |
||

89 | %token UCLOCK DCLOCK PHCLOCK TAIL |
||

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

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

92 | %token STRUCT ENUM |
||

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

94 | %token RATE DUE |
||

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

96 | %token AND OR XOR IMPL |
||

97 | %token MULT DIV MOD |
||

98 | %token MINUS PLUS UMINUS |
||

99 | %token PRE ARROW |
||

100 | 01c7d5e1 | ploc | %token REQUIRES ENSURES OBSERVER |

101 | %token INVARIANT BEHAVIOR ASSUMES |
||

102 | %token EXISTS FORALL |
||

103 | 3826f8cb | ploc | %token PROTOTYPE LIB |

104 | 22fe1c93 | ploc | %token EOF |

105 | |||

106 | 01c7d5e1 | ploc | %nonassoc prec_exists prec_forall |

107 | 22fe1c93 | ploc | %nonassoc COMMA |

108 | %left MERGE IF |
||

109 | %nonassoc ELSE |
||

110 | %right ARROW FBY |
||

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

112 | %right COLCOL |
||

113 | %right IMPL |
||

114 | %left OR XOR BARBAR |
||

115 | %left AND AMPERAMPER |
||

116 | %left NOT |
||

117 | %nonassoc INT |
||

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

119 | %left MINUS PLUS |
||

120 | %left MULT DIV MOD |
||

121 | %left UMINUS |
||

122 | %left POWER |
||

123 | %left PRE LAST |
||

124 | %nonassoc RBRACKET |
||

125 | %nonassoc LBRACKET |
||

126 | |||

127 | %start prog |
||

128 | 01c7d5e1 | ploc | %type <LustreSpec.top_decl list> prog |

129 | |||

130 | 5c1184ad | ploc | %start header |

131 | 01c7d5e1 | ploc | %type <bool -> LustreSpec.top_decl list> header |

132 | |||

133 | %start lustre_annot |
||

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

135 | |||

136 | %start lustre_spec |
||

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

138 | 22fe1c93 | ploc | |

139 | %% |
||

140 | |||

141 | prog: |
||

142 | 7291cb80 | xthirioux | open_list typ_def_list top_decl_list EOF { $1 @ (List.rev $3) } |

143 | 22fe1c93 | ploc | |

144 | 5c1184ad | ploc | header: |

145 | 89b9e25c | xthirioux | open_list typ_def_list top_decl_header_list EOF { (fun own -> ($1 @ (List.rev ($3 own)))) } |

146 | 7291cb80 | xthirioux | |

147 | open_list: |
||

148 | { [] } |
||

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

150 | |||

151 | open_lusi: |
||

152 | 54ae8ac7 | ploc | | OPEN QUOTE IDENT QUOTE { mktop_decl (Open (true, $3))} |

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

154 | 5c1184ad | ploc | |

155 | 22fe1c93 | ploc | top_decl_list: |

156 | top_decl {[$1]} |
||

157 | | top_decl_list top_decl {$2::$1} |
||

158 | |||

159 | |||

160 | 5c1184ad | ploc | top_decl_header_list: |

161 | 89b9e25c | xthirioux | top_decl_header {(fun own -> [$1 own]) } |

162 | | top_decl_header_list top_decl_header {(fun own -> ($2 own)::($1 own)) } |
||

163 | 22fe1c93 | ploc | |

164 | 52cfee34 | xthirioux | state_annot: |

165 | FUNCTION { true } |
||

166 | | NODE { false } |
||

167 | 22fe1c93 | ploc | |

168 | 5c1184ad | ploc | top_decl_header: |

169 | 3826f8cb | ploc | | CONST cdecl_list { let top = mktop_decl (Consts (List.rev $2)) in fun _ -> top } |

170 | 54ae8ac7 | ploc | | nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_opt SCOL |

171 | 22fe1c93 | ploc | {let nd = mktop_decl (ImportedNode |

172 | 5c1184ad | ploc | {nodei_id = $3; |

173 | 22fe1c93 | ploc | nodei_type = Types.new_var (); |

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

175 | 5c1184ad | ploc | nodei_inputs = List.rev $5; |

176 | 22fe1c93 | ploc | nodei_outputs = List.rev $10; |

177 | 52cfee34 | xthirioux | nodei_stateless = $2; |

178 | 54ae8ac7 | ploc | nodei_spec = $1; |

179 | nodei_prototype = $13; |
||

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

181 | 22fe1c93 | ploc | in |

182 | 01c7d5e1 | ploc | check_node_symbol ("node " ^ $3) $3 nd; |

183 | let loc = get_loc () in |
||

184 | (fun own -> add_node loc own ("node " ^ $3) node_table $3 nd; nd) } |
||

185 | 22fe1c93 | ploc | |

186 | 54ae8ac7 | ploc | prototype_opt: |

187 | { None } |
||

188 | | PROTOTYPE IDENT { Some $2} |
||

189 | |||

190 | in_lib_opt: |
||

191 | { None } |
||

192 | 3826f8cb | ploc | | LIB IDENT {Some $2} |

193 | 54ae8ac7 | ploc | |

194 | 5c1184ad | ploc | top_decl: |

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

196 | 52cfee34 | xthirioux | | 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 |

197 | 5c1184ad | ploc | {let eqs, asserts, annots = $16 in |

198 | let nd = mktop_decl (Node |
||

199 | {node_id = $3; |
||

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

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

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

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

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

205 | node_gencalls = []; |
||

206 | node_checks = []; |
||

207 | node_asserts = asserts; |
||

208 | node_eqs = eqs; |
||

209 | 52cfee34 | xthirioux | node_dec_stateless = $2; |

210 | node_stateless = None; |
||

211 | node_spec = $1; |
||

212 | 01c7d5e1 | ploc | node_annot = annots}) |

213 | 3826f8cb | ploc | in |

214 | let loc = Location.symbol_rloc () in |
||

215 | add_node loc true ("node " ^ $3) node_table $3 nd; nd} |
||

216 | 5c1184ad | ploc | |

217 | 22fe1c93 | ploc | nodespec_list: |

218 | 52cfee34 | xthirioux | { None } |

219 | 01c7d5e1 | ploc | | NODESPEC nodespec_list { |

220 | (function |
||

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

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

223 | 22fe1c93 | ploc | |

224 | typ_def_list: |
||

225 | /* empty */ {} |
||

226 | | typ_def SCOL typ_def_list {$1;$3} |
||

227 | |||

228 | typ_def: |
||

229 | TYPE IDENT EQ typeconst { |
||

230 | try |
||

231 | 3826f8cb | ploc | let loc = Location.symbol_rloc () in |

232 | 01c7d5e1 | ploc | add_symbol loc ("type " ^ $2) type_table (Tydec_const $2) (get_repr_type $4) |

233 | 21485807 | xthirioux | with Not_found-> assert false } |

234 | 22fe1c93 | ploc | | TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) } |

235 | 6a6abd76 | xthirioux | | TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_struct ($6 (Tydec_const $2))) } |

236 | 22fe1c93 | ploc | |

237 | array_typ_decl: |
||

238 | { fun typ -> typ } |
||

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

240 | |||

241 | typeconst: |
||

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

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

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

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

246 | 3826f8cb | ploc | | IDENT array_typ_decl { |

247 | let loc = Location.symbol_rloc () in |
||

248 | check_symbol loc ("type " ^ $1) type_table (Tydec_const $1); $2 (Tydec_const $1) } |
||

249 | 22fe1c93 | ploc | | TBOOL TCLOCK { Tydec_clock Tydec_bool } |

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

251 | |||

252 | tag_list: |
||

253 | IDENT |
||

254 | 3826f8cb | ploc | { let loc = Location.symbol_rloc () in |

255 | (fun t -> |
||

256 | add_symbol loc ("tag " ^ $1) tag_table $1 t; $1 :: []) } |
||

257 | 22fe1c93 | ploc | | tag_list COMMA IDENT |

258 | 3826f8cb | ploc | { |

259 | let loc = Location.symbol_rloc () in |
||

260 | (fun t -> add_symbol loc ("tag " ^ $3)tag_table $3 t; $3 :: ($1 t)) |
||

261 | } |
||

262 | |||

263 | 22fe1c93 | ploc | field_list: |

264 | 6a6abd76 | xthirioux | { (fun t -> []) } |

265 | | field_list IDENT COL typeconst SCOL |
||

266 | 3826f8cb | ploc | { |

267 | let loc = Location.symbol_rloc () in |
||

268 | (fun t -> add_symbol loc ("field " ^ $2) field_table $2 t; ($1 t) @ [ ($2, $4) ]) } |
||

269 | |||

270 | 22fe1c93 | ploc | eq_list: |

271 | { [], [], [] } |
||

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

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

274 | 01c7d5e1 | ploc | | ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl} |

275 | 22fe1c93 | ploc | | automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl} |

276 | |||

277 | automaton: |
||

278 | AUTOMATON IDENT handler_list { failwith "not implemented" } |
||

279 | |||

280 | handler_list: |
||

281 | { [] } |
||

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

283 | |||

284 | handler: |
||

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

286 | |||

287 | unless_list: |
||

288 | { [] } |
||

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

290 | |||

291 | until_list: |
||

292 | { [] } |
||

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

294 | |||

295 | unless: |
||

296 | UNLESS expr RESTART IDENT { } |
||

297 | | UNLESS expr RESUME IDENT { } |
||

298 | |||

299 | until: |
||

300 | UNTIL expr RESTART IDENT { } |
||

301 | | UNTIL expr RESUME IDENT { } |
||

302 | |||

303 | assert_: |
||

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

305 | |||

306 | eq: |
||

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

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

309 | |||

310 | 01c7d5e1 | ploc | lustre_spec: |

311 | | contract EOF { $1 } |
||

312 | |||

313 | contract: |
||

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

315 | |||

316 | requires: |
||

317 | { [] } |
||

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

319 | |||

320 | ensures: |
||

321 | { [] } |
||

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

323 | | OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { |
||

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

325 | } |
||

326 | |||

327 | behaviors: |
||

328 | { [] } |
||

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

330 | |||

331 | assumes: |
||

332 | { [] } |
||

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

334 | |||

335 | tuple_qexpr: |
||

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

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

338 | |||

339 | qexpr: |
||

340 | | expr { mkeexpr $1 } |
||

341 | /* Quantifiers */ |
||

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

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

344 | |||

345 | |||

346 | 22fe1c93 | ploc | tuple_expr: |

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

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

349 | |||

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

351 | array_expr: |
||

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

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

354 | |||

355 | dim_list: |
||

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

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

358 | |||

359 | expr: |
||

360 | /* constants */ |
||

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

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

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

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

365 | | IDENT { |
||

366 | if Hashtbl.mem tag_table $1 |
||

367 | then mkexpr (Expr_const (Const_tag $1)) |
||

368 | else mkexpr (Expr_ident $1)} |
||

369 | | LPAR ANNOT expr RPAR |
||

370 | {update_expr_annot $3 $2} |
||

371 | | LPAR expr RPAR |
||

372 | {$2} |
||

373 | | LPAR tuple_expr RPAR |
||

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

375 | |||

376 | /* Array expressions */ |
||

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

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

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

380 | |||

381 | /* Temporal operators */ |
||

382 | | PRE expr |
||

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

384 | | expr ARROW expr |
||

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

386 | | expr FBY expr |
||

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

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

389 | | expr WHEN IDENT |
||

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

391 | | expr WHENNOT IDENT |
||

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

393 | | expr WHEN IDENT LPAR IDENT RPAR |
||

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

395 | | MERGE IDENT handler_expr_list |
||

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

397 | |||

398 | /* Applications */ |
||

399 | | IDENT LPAR expr RPAR |
||

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

401 | | IDENT LPAR expr RPAR EVERY IDENT |
||

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

403 | | IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR |
||

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

405 | | IDENT LPAR tuple_expr RPAR |
||

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

407 | | IDENT LPAR tuple_expr RPAR EVERY IDENT |
||

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

409 | | IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR |
||

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

411 | |||

412 | /* Boolean expr */ |
||

413 | | expr AND expr |
||

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

415 | | expr AMPERAMPER expr |
||

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

417 | | expr OR expr |
||

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

419 | | expr BARBAR expr |
||

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

421 | | expr XOR expr |
||

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

423 | | NOT expr |
||

424 | b616fe7a | xthirioux | {mkpredef_call "not" [$2]} |

425 | 22fe1c93 | ploc | | expr IMPL expr |

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

427 | |||

428 | /* Comparison expr */ |
||

429 | | expr EQ expr |
||

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

431 | | expr LT expr |
||

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

433 | | expr LTE expr |
||

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

435 | | expr GT expr |
||

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

437 | | expr GTE expr |
||

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

439 | | expr NEQ expr |
||

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

441 | |||

442 | /* Arithmetic expr */ |
||

443 | | expr PLUS expr |
||

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

445 | | expr MINUS expr |
||

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

447 | | expr MULT expr |
||

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

449 | | expr DIV expr |
||

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

451 | | MINUS expr %prec UMINUS |
||

452 | b616fe7a | xthirioux | {mkpredef_call "uminus" [$2]} |

453 | 22fe1c93 | ploc | | expr MOD expr |

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

455 | |||

456 | /* If */ |
||

457 | | IF expr THEN expr ELSE expr |
||

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

459 | |||

460 | handler_expr_list: |
||

461 | { [] } |
||

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

463 | |||

464 | handler_expr: |
||

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

466 | |||

467 | signed_const_array: |
||

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

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

470 | |||

471 | 12af4908 | xthirioux | signed_const_struct: |

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

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

474 | |||

475 | 22fe1c93 | ploc | signed_const: |

476 | INT {Const_int $1} |
||

477 | | REAL {Const_real $1} |
||

478 | | FLOAT {Const_float $1} |
||

479 | | IDENT {Const_tag $1} |
||

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

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

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

483 | 12af4908 | xthirioux | | LCUR signed_const_struct RCUR { Const_struct $2 } |

484 | 22fe1c93 | ploc | | LBRACKET signed_const_array RBRACKET { Const_array $2 } |

485 | |||

486 | dim: |
||

487 | INT { mkdim_int $1 } |
||

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

489 | | IDENT { mkdim_ident $1 } |
||

490 | | dim AND dim |
||

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

492 | | dim AMPERAMPER dim |
||

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

494 | | dim OR dim |
||

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

496 | | dim BARBAR dim |
||

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

498 | | dim XOR dim |
||

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

500 | | NOT dim |
||

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

502 | | dim IMPL dim |
||

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

504 | |||

505 | /* Comparison dim */ |
||

506 | | dim EQ dim |
||

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

508 | | dim LT dim |
||

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

510 | | dim LTE dim |
||

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

512 | | dim GT dim |
||

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

514 | | dim GTE dim |
||

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

516 | | dim NEQ dim |
||

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

518 | |||

519 | /* Arithmetic dim */ |
||

520 | | dim PLUS dim |
||

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

522 | | dim MINUS dim |
||

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

524 | | dim MULT dim |
||

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

526 | | dim DIV dim |
||

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

528 | | MINUS dim %prec UMINUS |
||

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

530 | | dim MOD dim |
||

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

532 | /* If */ |
||

533 | | IF dim THEN dim ELSE dim |
||

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

535 | |||

536 | locals: |
||

537 | {[]} |
||

538 | | VAR vdecl_list SCOL {$2} |
||

539 | |||

540 | vdecl_list: |
||

541 | vdecl {$1} |
||

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

543 | |||

544 | vdecl: |
||

545 | /* Useless no ?*/ ident_list |
||

546 | {List.map mkvar_decl |
||

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

548 | |||

549 | | ident_list COL typeconst clock |
||

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

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

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

553 | |||

554 | cdecl_list: |
||

555 | cdecl SCOL { [$1] } |
||

556 | | cdecl_list cdecl SCOL { $2::$1 } |
||

557 | |||

558 | cdecl: |
||

559 | IDENT EQ signed_const { |
||

560 | let c = { |
||

561 | const_id = $1; |
||

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

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

564 | const_value = $3; |
||

565 | } in |
||

566 | Hashtbl.add consts_table $1 c; c |
||

567 | } |
||

568 | |||

569 | clock: |
||

570 | {mkclock Ckdec_any} |
||

571 | | when_list |
||

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

573 | |||

574 | when_cond: |
||

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

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

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

578 | |||

579 | when_list: |
||

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

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

582 | |||

583 | ident_list: |
||

584 | IDENT {[$1]} |
||

585 | | ident_list COMMA IDENT {$3::$1} |
||

586 | |||

587 | SCOL_opt: |
||

588 | SCOL {} | {} |
||

589 | 01c7d5e1 | ploc | |

590 | |||

591 | lustre_annot: |
||

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

593 | |||

594 | lustre_annot_list: |
||

595 | { [] } |
||

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

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

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

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

600 | |||

601 | kwd: |
||

602 | DIV { [] } |
||

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

604 | |||

605 | %% |
||

606 | (* Local Variables: *) |
||

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

608 | (* End: *) |
||

609 |