lustrec / src / parserLustreSpec.mly @ d5767b5a
History | View | Annotate | Download (7.98 KB)
1 | 22fe1c93 | ploc | %{ |
---|---|---|---|
2 | a2d97a3e | ploc | (********************************************************************) |
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 | 22fe1c93 | ploc | open Utils |
14 | open Corelang |
||
15 | open LustreSpec |
||
16 | |||
17 | 01c7d5e1 | ploc | 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 | 22fe1c93 | ploc | let mkeexpr x = mkeexpr (Location.symbol_rloc ()) x |
22 | 01c7d5e1 | ploc | (* |
23 | 22fe1c93 | ploc | let mkepredef_call x = mkepredef_call (Location.symbol_rloc ()) x |
24 | let mkepredef_unary_call x = mkepredef_unary_call (Location.symbol_rloc ()) x |
||
25 | 01c7d5e1 | ploc | *) |
26 | |||
27 | 22fe1c93 | ploc | 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 | %token INVARIANT BEHAVIOR ASSUMES |
||
56 | %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 | %type <LustreSpec.expr_annot> lustre_annot |
||
77 | |||
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 | 01c7d5e1 | ploc | | REQUIRES qexpr SCOL requires { $2::$4 } |
92 | 22fe1c93 | ploc | |
93 | ensures: |
||
94 | { [] } |
||
95 | 01c7d5e1 | ploc | | ENSURES qexpr SCOL ensures { (EnsuresExpr $2) :: $4 } |
96 | | OBSERVER IDENT LPAR tuple_qexpr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 } |
||
97 | 22fe1c93 | ploc | |
98 | behaviors: |
||
99 | { [] } |
||
100 | | BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5)::$6 } |
||
101 | |||
102 | assumes: |
||
103 | { [] } |
||
104 | 01c7d5e1 | ploc | | 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 | 22fe1c93 | ploc | |
111 | tuple_expr: |
||
112 | 01c7d5e1 | ploc | expr COMMA expr {[$3;$1]} |
113 | 22fe1c93 | ploc | | tuple_expr COMMA expr {$3::$1} |
114 | |||
115 | 01c7d5e1 | ploc | // 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 | 22fe1c93 | ploc | expr: |
125 | 01c7d5e1 | ploc | /* constants */ |
126 | INT {mkexpr (Expr_const (Const_int $1))} |
||
127 | | REAL {mkexpr (Expr_const (Const_real $1))} |
||
128 | | FLOAT {mkexpr (Expr_const (Const_float $1))} |
||
129 | /* Idents or type enum tags */ |
||
130 | | IDENT { |
||
131 | if Hashtbl.mem tag_table $1 |
||
132 | then mkexpr (Expr_const (Const_tag $1)) |
||
133 | else mkexpr (Expr_ident $1)} |
||
134 | | LPAR ANNOT expr RPAR |
||
135 | {update_expr_annot $3 $2} |
||
136 | 22fe1c93 | ploc | | LPAR expr RPAR |
137 | {$2} |
||
138 | | LPAR tuple_expr RPAR |
||
139 | 01c7d5e1 | ploc | {mkexpr (Expr_tuple (List.rev $2))} |
140 | |||
141 | /* Array expressions */ |
||
142 | | LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) } |
||
143 | | expr POWER dim { mkexpr (Expr_power ($1, $3)) } |
||
144 | | expr LBRACKET dim_list { $3 $1 } |
||
145 | |||
146 | /* Temporal operators */ |
||
147 | | PRE expr |
||
148 | {mkexpr (Expr_pre $2)} |
||
149 | 22fe1c93 | ploc | | expr ARROW expr |
150 | 01c7d5e1 | ploc | {mkexpr (Expr_arrow ($1,$3))} |
151 | 22fe1c93 | ploc | | expr FBY expr |
152 | 01c7d5e1 | ploc | {(*mkexpr (Expr_fby ($1,$3))*) |
153 | mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))} |
||
154 | 22fe1c93 | ploc | | expr WHEN IDENT |
155 | 01c7d5e1 | ploc | {mkexpr (Expr_when ($1,$3,tag_true))} |
156 | | expr WHENNOT IDENT |
||
157 | {mkexpr (Expr_when ($1,$3,tag_false))} |
||
158 | | expr WHEN IDENT LPAR IDENT RPAR |
||
159 | {mkexpr (Expr_when ($1, $5, $3))} |
||
160 | | MERGE IDENT handler_expr_list |
||
161 | {mkexpr (Expr_merge ($2,$3))} |
||
162 | |||
163 | /* Applications */ |
||
164 | 22fe1c93 | ploc | | IDENT LPAR expr RPAR |
165 | 01c7d5e1 | ploc | {mkexpr (Expr_appl ($1, $3, None))} |
166 | 22fe1c93 | ploc | | IDENT LPAR expr RPAR EVERY IDENT |
167 | 01c7d5e1 | ploc | {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))} |
168 | | IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR |
||
169 | {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) } |
||
170 | 22fe1c93 | ploc | | IDENT LPAR tuple_expr RPAR |
171 | 01c7d5e1 | ploc | {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))} |
172 | 22fe1c93 | ploc | | IDENT LPAR tuple_expr RPAR EVERY IDENT |
173 | 01c7d5e1 | ploc | {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) } |
174 | | IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR |
||
175 | {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) } |
||
176 | 22fe1c93 | ploc | |
177 | /* Boolean expr */ |
||
178 | | expr AND expr |
||
179 | 01c7d5e1 | ploc | {mkpredef_call "&&" [$1;$3]} |
180 | 22fe1c93 | ploc | | expr AMPERAMPER expr |
181 | 01c7d5e1 | ploc | {mkpredef_call "&&" [$1;$3]} |
182 | 22fe1c93 | ploc | | expr OR expr |
183 | 01c7d5e1 | ploc | {mkpredef_call "||" [$1;$3]} |
184 | 22fe1c93 | ploc | | expr BARBAR expr |
185 | 01c7d5e1 | ploc | {mkpredef_call "||" [$1;$3]} |
186 | 22fe1c93 | ploc | | expr XOR expr |
187 | 01c7d5e1 | ploc | {mkpredef_call "xor" [$1;$3]} |
188 | 22fe1c93 | ploc | | NOT expr |
189 | 01c7d5e1 | ploc | {mkpredef_unary_call "not" $2} |
190 | 22fe1c93 | ploc | | expr IMPL expr |
191 | 01c7d5e1 | ploc | {mkpredef_call "impl" [$1;$3]} |
192 | 22fe1c93 | ploc | |
193 | /* Comparison expr */ |
||
194 | | expr EQ expr |
||
195 | 01c7d5e1 | ploc | {mkpredef_call "=" [$1;$3]} |
196 | 22fe1c93 | ploc | | expr LT expr |
197 | 01c7d5e1 | ploc | {mkpredef_call "<" [$1;$3]} |
198 | 22fe1c93 | ploc | | expr LTE expr |
199 | 01c7d5e1 | ploc | {mkpredef_call "<=" [$1;$3]} |
200 | 22fe1c93 | ploc | | expr GT expr |
201 | 01c7d5e1 | ploc | {mkpredef_call ">" [$1;$3]} |
202 | 22fe1c93 | ploc | | expr GTE expr |
203 | 01c7d5e1 | ploc | {mkpredef_call ">=" [$1;$3]} |
204 | 22fe1c93 | ploc | | expr NEQ expr |
205 | 01c7d5e1 | ploc | {mkpredef_call "!=" [$1;$3]} |
206 | 22fe1c93 | ploc | |
207 | /* Arithmetic expr */ |
||
208 | | expr PLUS expr |
||
209 | 01c7d5e1 | ploc | {mkpredef_call "+" [$1;$3]} |
210 | 22fe1c93 | ploc | | expr MINUS expr |
211 | 01c7d5e1 | ploc | {mkpredef_call "-" [$1;$3]} |
212 | 22fe1c93 | ploc | | expr MULT expr |
213 | 01c7d5e1 | ploc | {mkpredef_call "*" [$1;$3]} |
214 | 22fe1c93 | ploc | | expr DIV expr |
215 | 01c7d5e1 | ploc | {mkpredef_call "/" [$1;$3]} |
216 | 22fe1c93 | ploc | | MINUS expr %prec UMINUS |
217 | 01c7d5e1 | ploc | {mkpredef_unary_call "uminus" $2} |
218 | 22fe1c93 | ploc | | expr MOD expr |
219 | 01c7d5e1 | ploc | {mkpredef_call "mod" [$1;$3]} |
220 | 22fe1c93 | ploc | |
221 | /* If */ |
||
222 | | IF expr THEN expr ELSE expr |
||
223 | 01c7d5e1 | ploc | {mkexpr (Expr_ite ($2, $4, $6))} |
224 | |||
225 | |||
226 | handler_expr_list: |
||
227 | { [] } |
||
228 | | handler_expr handler_expr_list { $1 :: $2 } |
||
229 | |||
230 | handler_expr: |
||
231 | LPAR IDENT ARROW expr RPAR { ($2, $4) } |
||
232 | 22fe1c93 | ploc | |
233 | 01c7d5e1 | ploc | qexpr: |
234 | | expr { mkeexpr [] $1 } |
||
235 | /* Quantifiers */ |
||
236 | | EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eepxr (Exists, $2) $4 } |
||
237 | | FORALL vdecl SCOL qexpr %prec prec_forall { extend_eepxr (Forall, $2) $4 } |
||
238 | 22fe1c93 | ploc | |
239 | vdecl: |
||
240 | | ident_list COL typ clock |
||
241 | {List.map mkvar_decl (List.map (fun id -> (id, $3, $4, false)) $1)} |
||
242 | | CONST ident_list COL typ clock |
||
243 | {List.map mkvar_decl (List.map (fun id -> (id, $4, $5, true)) $2)} |
||
244 | |||
245 | |||
246 | ident_list: |
||
247 | IDENT {[$1]} |
||
248 | | ident_list COMMA IDENT {$3::$1} |
||
249 | |||
250 | |||
251 | typ: |
||
252 | {mktyp Tydec_any} |
||
253 | | TINT {mktyp Tydec_int} |
||
254 | | IDENT { |
||
255 | try |
||
256 | mktyp (Hashtbl.find Corelang.type_table (Tydec_const $1)) |
||
257 | 52cfee34 | xthirioux | with Not_found -> raise (Corelang.Error (Location.symbol_rloc(), Corelang.Unbound_symbol ("type " ^ $1))) |
258 | 22fe1c93 | ploc | } |
259 | | TFLOAT {mktyp Tydec_float} |
||
260 | | TREAL {mktyp Tydec_real} |
||
261 | | TBOOL {mktyp Tydec_bool} |
||
262 | | TCLOCK {mktyp (Tydec_clock Tydec_bool) } |
||
263 | | typ POWER INT {mktyp Tydec_any (*(mktyptuple $3 $1)*)} |
||
264 | | typ POWER IDENT {mktyp Tydec_any (*(mktyptuple (try |
||
265 | match get_const $3 with Const_int i -> i with _ -> failwith "Const power error") $1)*)} |
||
266 | |||
267 | clock: |
||
268 | {mkclock Ckdec_any} |
||
269 | | when_list |
||
270 | {mkclock (Ckdec_bool (List.rev $1))} |
||
271 | |||
272 | when_cond: |
||
273 | WHEN IDENT {($2, tag_true)} |
||
274 | | WHENNOT IDENT {($2, tag_false)} |
||
275 | |||
276 | when_list: |
||
277 | when_cond {[$1]} |
||
278 | | when_list when_cond {$2::$1} |
||
279 | |||
280 | |||
281 | const: |
||
282 | 01c7d5e1 | ploc | | INT {Const_int $1} |
283 | | REAL {Const_real $1} |
||
284 | | FLOAT {Const_float $1} |
||
285 | | TRUE {Const_bool true} |
||
286 | | FALSE {Const_bool false} |
||
287 | | STRING {Const_string $1} |
||
288 | 22fe1c93 | ploc | |
289 | lustre_annot: |
||
290 | lustre_annot_list EOF { $1 } |
||
291 | |||
292 | lustre_annot_list: |
||
293 | { [] } |
||
294 | | kwd COL expr SCOL lustre_annot_list { ($1,$3)::$5 } |
||
295 | | IDENT COL expr SCOL lustre_annot_list { ([$1],$3)::$5 } |
||
296 | | INVARIANT COL expr SCOL lustre_annot_list{ (["invariant"],$3)::$5 } |
||
297 | | OBSERVER COL expr SCOL lustre_annot_list { (["observer"],$3)::$5 } |
||
298 | |||
299 | kwd: |
||
300 | DIV { [] } |
||
301 | | DIV IDENT kwd { $2::$3} |