lustrec / src / parserLustreSpec.mly @ 01c7d5e1
History | View | Annotate | Download (7.28 KB)
1 |
%{ |
---|---|
2 |
open Utils |
3 |
open Corelang |
4 |
open LustreSpec |
5 |
|
6 |
let mkexpr x = mkexpr (Location.symbol_rloc ()) x |
7 |
let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x |
8 |
let mkpredef_unary_call x = mkpredef_unary_call (Location.symbol_rloc ()) x |
9 |
|
10 |
let mkeexpr x = mkeexpr (Location.symbol_rloc ()) x |
11 |
(* |
12 |
let mkepredef_call x = mkepredef_call (Location.symbol_rloc ()) x |
13 |
let mkepredef_unary_call x = mkepredef_unary_call (Location.symbol_rloc ()) x |
14 |
*) |
15 |
|
16 |
let mktyp x = mktyp (Location.symbol_rloc ()) x |
17 |
let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x |
18 |
let mkclock x = mkclock (Location.symbol_rloc ()) x |
19 |
|
20 |
%} |
21 |
|
22 |
|
23 |
%token <int> INT |
24 |
%token <string> REAL |
25 |
%token <float> FLOAT |
26 |
%token <string> STRING |
27 |
%token TRUE FALSE STATELESS ASSERT INCLUDE QUOTE |
28 |
%token <string> IDENT |
29 |
%token LPAR RPAR SCOL COL COMMA COLCOL |
30 |
%token AMPERAMPER BARBAR NOT POWER |
31 |
%token IF THEN ELSE |
32 |
%token UCLOCK DCLOCK PHCLOCK TAIL |
33 |
%token MERGE FBY WHEN WHENNOT EVERY |
34 |
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST |
35 |
%token TINT TFLOAT TREAL TBOOL TCLOCK |
36 |
%token RATE DUE |
37 |
%token EQ LT GT LTE GTE NEQ |
38 |
%token AND OR XOR IMPL |
39 |
%token MULT DIV MOD |
40 |
%token MINUS PLUS UMINUS |
41 |
%token PRE ARROW |
42 |
%token EOF |
43 |
%token REQUIRES ENSURES OBSERVER |
44 |
%token INVARIANT BEHAVIOR ASSUMES |
45 |
%token EXISTS FORALL |
46 |
|
47 |
%nonassoc prec_exists prec_forall |
48 |
%nonassoc COMMA POWER |
49 |
%left MERGE IF |
50 |
%nonassoc ELSE |
51 |
%right ARROW FBY |
52 |
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK |
53 |
%right COLCOL |
54 |
%right IMPL |
55 |
%left OR XOR BARBAR |
56 |
%left AND AMPERAMPER |
57 |
%left NOT |
58 |
%nonassoc EQ LT GT LTE GTE NEQ |
59 |
%left MINUS PLUS |
60 |
%left MULT DIV MOD |
61 |
%left PRE |
62 |
%nonassoc UMINUS |
63 |
|
64 |
%start lustre_annot |
65 |
%type <LustreSpec.expr_annot> lustre_annot |
66 |
|
67 |
%start lustre_spec |
68 |
%type <LustreSpec.node_annot> lustre_spec |
69 |
|
70 |
%% |
71 |
|
72 |
lustre_spec: |
73 |
| contract EOF { $1 } |
74 |
|
75 |
contract: |
76 |
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; } } |
77 |
|
78 |
requires: |
79 |
{ [] } |
80 |
| REQUIRES qexpr SCOL requires { $2::$4 } |
81 |
|
82 |
ensures: |
83 |
{ [] } |
84 |
| ENSURES qexpr SCOL ensures { (EnsuresExpr $2) :: $4 } |
85 |
| OBSERVER IDENT LPAR tuple_qexpr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 } |
86 |
|
87 |
behaviors: |
88 |
{ [] } |
89 |
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5)::$6 } |
90 |
|
91 |
assumes: |
92 |
{ [] } |
93 |
| ASSUMES qexpr SCOL assumes { $2::$4 } |
94 |
|
95 |
tuple_qexpr: |
96 |
| qexpr COMMA qexpr {[$3;$1]} |
97 |
| tuple_qexpr COMMA qexpr {$3::$1} |
98 |
|
99 |
|
100 |
tuple_expr: |
101 |
expr COMMA expr {[$3;$1]} |
102 |
| tuple_expr COMMA expr {$3::$1} |
103 |
|
104 |
// Same as tuple expr but accepting lists with single element |
105 |
array_expr: |
106 |
expr {[$1]} |
107 |
| expr COMMA array_expr {$1::$3} |
108 |
|
109 |
dim_list: |
110 |
dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) } |
111 |
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) } |
112 |
|
113 |
expr: |
114 |
/* constants */ |
115 |
INT {mkexpr (Expr_const (Const_int $1))} |
116 |
| REAL {mkexpr (Expr_const (Const_real $1))} |
117 |
| FLOAT {mkexpr (Expr_const (Const_float $1))} |
118 |
/* Idents or type enum tags */ |
119 |
| IDENT { |
120 |
if Hashtbl.mem tag_table $1 |
121 |
then mkexpr (Expr_const (Const_tag $1)) |
122 |
else mkexpr (Expr_ident $1)} |
123 |
| LPAR ANNOT expr RPAR |
124 |
{update_expr_annot $3 $2} |
125 |
| LPAR expr RPAR |
126 |
{$2} |
127 |
| LPAR tuple_expr RPAR |
128 |
{mkexpr (Expr_tuple (List.rev $2))} |
129 |
|
130 |
/* Array expressions */ |
131 |
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) } |
132 |
| expr POWER dim { mkexpr (Expr_power ($1, $3)) } |
133 |
| expr LBRACKET dim_list { $3 $1 } |
134 |
|
135 |
/* Temporal operators */ |
136 |
| PRE expr |
137 |
{mkexpr (Expr_pre $2)} |
138 |
| expr ARROW expr |
139 |
{mkexpr (Expr_arrow ($1,$3))} |
140 |
| expr FBY expr |
141 |
{(*mkexpr (Expr_fby ($1,$3))*) |
142 |
mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))} |
143 |
| expr WHEN IDENT |
144 |
{mkexpr (Expr_when ($1,$3,tag_true))} |
145 |
| expr WHENNOT IDENT |
146 |
{mkexpr (Expr_when ($1,$3,tag_false))} |
147 |
| expr WHEN IDENT LPAR IDENT RPAR |
148 |
{mkexpr (Expr_when ($1, $5, $3))} |
149 |
| MERGE IDENT handler_expr_list |
150 |
{mkexpr (Expr_merge ($2,$3))} |
151 |
|
152 |
/* Applications */ |
153 |
| IDENT LPAR expr RPAR |
154 |
{mkexpr (Expr_appl ($1, $3, None))} |
155 |
| IDENT LPAR expr RPAR EVERY IDENT |
156 |
{mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))} |
157 |
| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR |
158 |
{mkexpr (Expr_appl ($1, $3, Some ($8, $6))) } |
159 |
| IDENT LPAR tuple_expr RPAR |
160 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))} |
161 |
| IDENT LPAR tuple_expr RPAR EVERY IDENT |
162 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) } |
163 |
| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR |
164 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) } |
165 |
|
166 |
/* Boolean expr */ |
167 |
| expr AND expr |
168 |
{mkpredef_call "&&" [$1;$3]} |
169 |
| expr AMPERAMPER expr |
170 |
{mkpredef_call "&&" [$1;$3]} |
171 |
| expr OR expr |
172 |
{mkpredef_call "||" [$1;$3]} |
173 |
| expr BARBAR expr |
174 |
{mkpredef_call "||" [$1;$3]} |
175 |
| expr XOR expr |
176 |
{mkpredef_call "xor" [$1;$3]} |
177 |
| NOT expr |
178 |
{mkpredef_unary_call "not" $2} |
179 |
| expr IMPL expr |
180 |
{mkpredef_call "impl" [$1;$3]} |
181 |
|
182 |
/* Comparison expr */ |
183 |
| expr EQ expr |
184 |
{mkpredef_call "=" [$1;$3]} |
185 |
| expr LT expr |
186 |
{mkpredef_call "<" [$1;$3]} |
187 |
| expr LTE expr |
188 |
{mkpredef_call "<=" [$1;$3]} |
189 |
| expr GT expr |
190 |
{mkpredef_call ">" [$1;$3]} |
191 |
| expr GTE expr |
192 |
{mkpredef_call ">=" [$1;$3]} |
193 |
| expr NEQ expr |
194 |
{mkpredef_call "!=" [$1;$3]} |
195 |
|
196 |
/* Arithmetic expr */ |
197 |
| expr PLUS expr |
198 |
{mkpredef_call "+" [$1;$3]} |
199 |
| expr MINUS expr |
200 |
{mkpredef_call "-" [$1;$3]} |
201 |
| expr MULT expr |
202 |
{mkpredef_call "*" [$1;$3]} |
203 |
| expr DIV expr |
204 |
{mkpredef_call "/" [$1;$3]} |
205 |
| MINUS expr %prec UMINUS |
206 |
{mkpredef_unary_call "uminus" $2} |
207 |
| expr MOD expr |
208 |
{mkpredef_call "mod" [$1;$3]} |
209 |
|
210 |
/* If */ |
211 |
| IF expr THEN expr ELSE expr |
212 |
{mkexpr (Expr_ite ($2, $4, $6))} |
213 |
|
214 |
|
215 |
handler_expr_list: |
216 |
{ [] } |
217 |
| handler_expr handler_expr_list { $1 :: $2 } |
218 |
|
219 |
handler_expr: |
220 |
LPAR IDENT ARROW expr RPAR { ($2, $4) } |
221 |
|
222 |
qexpr: |
223 |
| expr { mkeexpr [] $1 } |
224 |
/* Quantifiers */ |
225 |
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eepxr (Exists, $2) $4 } |
226 |
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eepxr (Forall, $2) $4 } |
227 |
|
228 |
vdecl: |
229 |
| ident_list COL typ clock |
230 |
{List.map mkvar_decl (List.map (fun id -> (id, $3, $4, false)) $1)} |
231 |
| CONST ident_list COL typ clock |
232 |
{List.map mkvar_decl (List.map (fun id -> (id, $4, $5, true)) $2)} |
233 |
|
234 |
|
235 |
ident_list: |
236 |
IDENT {[$1]} |
237 |
| ident_list COMMA IDENT {$3::$1} |
238 |
|
239 |
|
240 |
typ: |
241 |
{mktyp Tydec_any} |
242 |
| TINT {mktyp Tydec_int} |
243 |
| IDENT { |
244 |
try |
245 |
mktyp (Hashtbl.find Corelang.type_table (Tydec_const $1)) |
246 |
with Not_found -> raise (Corelang.Error (Location.symbol_rloc(), Corelang.Unbound_symbol ("type " ^ $1))) |
247 |
} |
248 |
| TFLOAT {mktyp Tydec_float} |
249 |
| TREAL {mktyp Tydec_real} |
250 |
| TBOOL {mktyp Tydec_bool} |
251 |
| TCLOCK {mktyp (Tydec_clock Tydec_bool) } |
252 |
| typ POWER INT {mktyp Tydec_any (*(mktyptuple $3 $1)*)} |
253 |
| typ POWER IDENT {mktyp Tydec_any (*(mktyptuple (try |
254 |
match get_const $3 with Const_int i -> i with _ -> failwith "Const power error") $1)*)} |
255 |
|
256 |
clock: |
257 |
{mkclock Ckdec_any} |
258 |
| when_list |
259 |
{mkclock (Ckdec_bool (List.rev $1))} |
260 |
|
261 |
when_cond: |
262 |
WHEN IDENT {($2, tag_true)} |
263 |
| WHENNOT IDENT {($2, tag_false)} |
264 |
|
265 |
when_list: |
266 |
when_cond {[$1]} |
267 |
| when_list when_cond {$2::$1} |
268 |
|
269 |
|
270 |
const: |
271 |
| INT {Const_int $1} |
272 |
| REAL {Const_real $1} |
273 |
| FLOAT {Const_float $1} |
274 |
| TRUE {Const_bool true} |
275 |
| FALSE {Const_bool false} |
276 |
| STRING {Const_string $1} |
277 |
|
278 |
lustre_annot: |
279 |
lustre_annot_list EOF { $1 } |
280 |
|
281 |
lustre_annot_list: |
282 |
{ [] } |
283 |
| kwd COL expr SCOL lustre_annot_list { ($1,$3)::$5 } |
284 |
| IDENT COL expr SCOL lustre_annot_list { ([$1],$3)::$5 } |
285 |
| INVARIANT COL expr SCOL lustre_annot_list{ (["invariant"],$3)::$5 } |
286 |
| OBSERVER COL expr SCOL lustre_annot_list { (["observer"],$3)::$5 } |
287 |
|
288 |
kwd: |
289 |
DIV { [] } |
290 |
| DIV IDENT kwd { $2::$3} |