## lustrec / src / parserLustreSpec.mly @ 66359a5e

History | View | Annotate | Download (8.28 KB)

1 | e2068500 | Temesghen Kahsai | %{ |
---|---|---|---|

2 | (********************************************************************) |
||

3 | (* *) |
||

4 | (* The LustreC compiler toolset / The LustreC Development Team *) |
||

5 | (* Copyright 2012 - -- ONERA - CNRS - INPT *) |
||

6 | (* *) |
||

7 | (* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
||

8 | (* under the terms of the GNU Lesser General Public License *) |
||

9 | (* version 2.1. *) |
||

10 | (* *) |
||

11 | (********************************************************************) |
||

12 | |||

13 | open Utils |
||

14 | open Corelang |
||

15 | open LustreSpec |
||

16 | |||

17 | let mkexpr x = mkexpr (Location.symbol_rloc ()) x |
||

18 | let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x |
||

19 | let mkpredef_unary_call x = mkpredef_unary_call (Location.symbol_rloc ()) x |
||

20 | |||

21 | let mkeexpr x = mkeexpr (Location.symbol_rloc ()) x |
||

22 | (* |
||

23 | let mkepredef_call x = mkepredef_call (Location.symbol_rloc ()) x |
||

24 | let mkepredef_unary_call x = mkepredef_unary_call (Location.symbol_rloc ()) x |
||

25 | *) |
||

26 | |||

27 | let mktyp x = mktyp (Location.symbol_rloc ()) x |
||

28 | let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x |
||

29 | let mkclock x = mkclock (Location.symbol_rloc ()) x |
||

30 | |||

31 | %} |
||

32 | |||

33 | |||

34 | %token <int> INT |
||

35 | %token <string> REAL |
||

36 | %token <float> FLOAT |
||

37 | %token <string> STRING |
||

38 | %token TRUE FALSE STATELESS ASSERT INCLUDE QUOTE |
||

39 | %token <string> IDENT |
||

40 | %token LPAR RPAR SCOL COL COMMA COLCOL |
||

41 | %token AMPERAMPER BARBAR NOT POWER |
||

42 | %token IF THEN ELSE |
||

43 | %token UCLOCK DCLOCK PHCLOCK TAIL |
||

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

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

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

47 | %token RATE DUE |
||

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

49 | %token AND OR XOR IMPL |
||

50 | %token MULT DIV MOD |
||

51 | %token MINUS PLUS UMINUS |
||

52 | %token PRE ARROW |
||

53 | %token EOF |
||

54 | %token REQUIRES ENSURES OBSERVER |
||

55 | 1b57e111 | Teme | %token INVARIANT BEHAVIOR ASSUMES CCODE MATLAB |

56 | e2068500 | Temesghen Kahsai | %token EXISTS FORALL |

57 | |||

58 | %nonassoc prec_exists prec_forall |
||

59 | %nonassoc COMMA POWER |
||

60 | %left MERGE IF |
||

61 | %nonassoc ELSE |
||

62 | %right ARROW FBY |
||

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

64 | %right COLCOL |
||

65 | %right IMPL |
||

66 | %left OR XOR BARBAR |
||

67 | %left AND AMPERAMPER |
||

68 | %left NOT |
||

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

70 | %left MINUS PLUS |
||

71 | %left MULT DIV MOD |
||

72 | %left PRE |
||

73 | %nonassoc UMINUS |
||

74 | |||

75 | %start lustre_annot |
||

76 | d50b0dc0 | Temesghen Kahsai | %type <LustreSpec.ident -> LustreSpec.expr_annot> lustre_annot |

77 | e2068500 | Temesghen Kahsai | |

78 | %start lustre_spec |
||

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

80 | |||

81 | %% |
||

82 | |||

83 | lustre_spec: |
||

84 | | contract EOF { $1 } |
||

85 | |||

86 | contract: |
||

87 | requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; } } |
||

88 | |||

89 | requires: |
||

90 | { [] } |
||

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

92 | |||

93 | ensures: |
||

94 | { [] } |
||

95 | | ENSURES qexpr SCOL ensures { (EnsuresExpr $2) :: $4 } |
||

96 | | OBSERVER IDENT LPAR tuple_qexpr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 } |
||

97 | |||

98 | behaviors: |
||

99 | { [] } |
||

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

101 | |||

102 | assumes: |
||

103 | { [] } |
||

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

105 | |||

106 | tuple_qexpr: |
||

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

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

109 | |||

110 | |||

111 | tuple_expr: |
||

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

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

114 | |||

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

116 | array_expr: |
||

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

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

119 | |||

120 | dim_list: |
||

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

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

123 | |||

124 | expr: |
||

125 | /* constants */ |
||

126 | 66359a5e | ploc | | INT {mkexpr (Expr_const (Const_int $1))} |

127 | e2068500 | Temesghen Kahsai | | REAL {mkexpr (Expr_const (Const_real $1))} |

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

129 | 66359a5e | ploc | | TRUE {mkexpr (Expr_const (Const_bool true))} |

130 | | FALSE {mkexpr (Expr_const (Const_bool false))} |
||

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

132 | e2068500 | Temesghen Kahsai | /* Idents or type enum tags */ |

133 | | IDENT { |
||

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

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

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

137 | | LPAR ANNOT expr RPAR |
||

138 | {update_expr_annot $3 $2} |
||

139 | | LPAR expr RPAR |
||

140 | {$2} |
||

141 | | LPAR tuple_expr RPAR |
||

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

143 | |||

144 | /* Array expressions */ |
||

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

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

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

148 | |||

149 | /* Temporal operators */ |
||

150 | | PRE expr |
||

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

152 | | expr ARROW expr |
||

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

154 | | expr FBY expr |
||

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

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

157 | | expr WHEN IDENT |
||

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

159 | | expr WHENNOT IDENT |
||

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

161 | | expr WHEN IDENT LPAR IDENT RPAR |
||

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

163 | | MERGE IDENT handler_expr_list |
||

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

165 | |||

166 | /* Applications */ |
||

167 | | IDENT LPAR expr RPAR |
||

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

169 | | IDENT LPAR expr RPAR EVERY IDENT |
||

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

171 | | IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR |
||

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

173 | | IDENT LPAR tuple_expr RPAR |
||

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

175 | | IDENT LPAR tuple_expr RPAR EVERY IDENT |
||

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

177 | | IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR |
||

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

179 | |||

180 | /* Boolean expr */ |
||

181 | | expr AND expr |
||

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

183 | | expr AMPERAMPER expr |
||

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

185 | | expr OR expr |
||

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

187 | | expr BARBAR expr |
||

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

189 | | expr XOR expr |
||

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

191 | | NOT expr |
||

192 | {mkpredef_unary_call "not" $2} |
||

193 | | expr IMPL expr |
||

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

195 | |||

196 | /* Comparison expr */ |
||

197 | | expr EQ expr |
||

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

199 | | expr LT expr |
||

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

201 | | expr LTE expr |
||

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

203 | | expr GT expr |
||

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

205 | | expr GTE expr |
||

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

207 | | expr NEQ expr |
||

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

209 | |||

210 | /* Arithmetic expr */ |
||

211 | | expr PLUS expr |
||

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

213 | | expr MINUS expr |
||

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

215 | | expr MULT expr |
||

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

217 | | expr DIV expr |
||

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

219 | | MINUS expr %prec UMINUS |
||

220 | {mkpredef_unary_call "uminus" $2} |
||

221 | | expr MOD expr |
||

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

223 | |||

224 | /* If */ |
||

225 | | IF expr THEN expr ELSE expr |
||

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

227 | |||

228 | |||

229 | handler_expr_list: |
||

230 | { [] } |
||

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

232 | |||

233 | handler_expr: |
||

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

235 | |||

236 | qexpr: |
||

237 | | expr { mkeexpr [] $1 } |
||

238 | /* Quantifiers */ |
||

239 | | EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eepxr (Exists, $2) $4 } |
||

240 | | FORALL vdecl SCOL qexpr %prec prec_forall { extend_eepxr (Forall, $2) $4 } |
||

241 | |||

242 | vdecl: |
||

243 | | ident_list COL typ clock |
||

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

245 | | CONST ident_list COL typ clock |
||

246 | {List.map mkvar_decl (List.map (fun id -> (id, $4, $5, true)) $2)} |
||

247 | |||

248 | |||

249 | ident_list: |
||

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

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

252 | |||

253 | |||

254 | typ: |
||

255 | {mktyp Tydec_any} |
||

256 | | TINT {mktyp Tydec_int} |
||

257 | | IDENT { |
||

258 | try |
||

259 | mktyp (Hashtbl.find Corelang.type_table (Tydec_const $1)) |
||

260 | with Not_found -> raise (Corelang.Error (Location.symbol_rloc(), Corelang.Unbound_symbol ("type " ^ $1))) |
||

261 | } |
||

262 | | TFLOAT {mktyp Tydec_float} |
||

263 | | TREAL {mktyp Tydec_real} |
||

264 | | TBOOL {mktyp Tydec_bool} |
||

265 | | TCLOCK {mktyp (Tydec_clock Tydec_bool) } |
||

266 | | typ POWER INT {mktyp Tydec_any (*(mktyptuple $3 $1)*)} |
||

267 | | typ POWER IDENT {mktyp Tydec_any (*(mktyptuple (try |
||

268 | match get_const $3 with Const_int i -> i with _ -> failwith "Const power error") $1)*)} |
||

269 | |||

270 | clock: |
||

271 | {mkclock Ckdec_any} |
||

272 | | when_list |
||

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

274 | |||

275 | when_cond: |
||

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

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

278 | |||

279 | when_list: |
||

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

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

282 | |||

283 | |||

284 | const: |
||

285 | | INT {Const_int $1} |
||

286 | | REAL {Const_real $1} |
||

287 | | FLOAT {Const_float $1} |
||

288 | | TRUE {Const_bool true} |
||

289 | | FALSE {Const_bool false} |
||

290 | | STRING {Const_string $1} |
||

291 | |||

292 | lustre_annot: |
||

293 | d50b0dc0 | Temesghen Kahsai | lustre_annot_list EOF { fun node_id -> $1 } |

294 | e2068500 | Temesghen Kahsai | |

295 | lustre_annot_list: |
||

296 | { [] } |
||

297 | | kwd COL expr SCOL lustre_annot_list { ($1,$3)::$5 } |
||

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

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

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

301 | 1b57e111 | Teme | | CCODE COL const lustre_annot_list{ (["c_code"],$3)::$5 } |

302 | | MATLAB COL const lustre_annot_list{ (["matlab"],$3)::$5 } |
||

303 | e2068500 | Temesghen Kahsai | |

304 | kwd: |
||

305 | DIV { [] } |
||

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