Revision 01c7d5e1 src/parserLustreSpec.mly
src/parserLustreSpec.mly | ||
---|---|---|
3 | 3 |
open Corelang |
4 | 4 |
open LustreSpec |
5 | 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 |
|
|
6 | 10 |
let mkeexpr x = mkeexpr (Location.symbol_rloc ()) x |
11 |
(* |
|
7 | 12 |
let mkepredef_call x = mkepredef_call (Location.symbol_rloc ()) x |
8 | 13 |
let mkepredef_unary_call x = mkepredef_unary_call (Location.symbol_rloc ()) x |
9 |
|
|
14 |
*) |
|
15 |
|
|
10 | 16 |
let mktyp x = mktyp (Location.symbol_rloc ()) x |
11 | 17 |
let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x |
12 | 18 |
let mkclock x = mkclock (Location.symbol_rloc ()) x |
... | ... | |
71 | 77 |
|
72 | 78 |
requires: |
73 | 79 |
{ [] } |
74 |
| REQUIRES expr SCOL requires { $2::$4 } |
|
80 |
| REQUIRES qexpr SCOL requires { $2::$4 }
|
|
75 | 81 |
|
76 | 82 |
ensures: |
77 | 83 |
{ [] } |
78 |
| ENSURES expr SCOL ensures { (EnsuresExpr $2) :: $4 } |
|
79 |
| OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 } |
|
84 |
| ENSURES qexpr SCOL ensures { (EnsuresExpr $2) :: $4 }
|
|
85 |
| OBSERVER IDENT LPAR tuple_qexpr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 }
|
|
80 | 86 |
|
81 | 87 |
behaviors: |
82 | 88 |
{ [] } |
... | ... | |
84 | 90 |
|
85 | 91 |
assumes: |
86 | 92 |
{ [] } |
87 |
| ASSUMES expr SCOL assumes { $2::$4 } |
|
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 |
|
|
88 | 99 |
|
89 | 100 |
tuple_expr: |
90 |
| expr COMMA expr {[$3;$1]}
|
|
101 |
expr COMMA expr {[$3;$1]}
|
|
91 | 102 |
| tuple_expr COMMA expr {$3::$1} |
92 | 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 |
|
|
93 | 113 |
expr: |
94 |
| const {mkeexpr (EExpr_const $1)} |
|
95 |
| IDENT |
|
96 |
{mkeexpr (EExpr_ident $1)} |
|
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} |
|
97 | 125 |
| LPAR expr RPAR |
98 | 126 |
{$2} |
99 | 127 |
| LPAR tuple_expr RPAR |
100 |
{mkeexpr (EExpr_tuple (List.rev $2))} |
|
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)} |
|
101 | 138 |
| expr ARROW expr |
102 |
{mkeexpr (EExpr_arrow ($1,$3))}
|
|
139 |
{mkexpr (Expr_arrow ($1,$3))}
|
|
103 | 140 |
| expr FBY expr |
104 |
{mkeexpr (EExpr_fby ($1,$3))} |
|
141 |
{(*mkexpr (Expr_fby ($1,$3))*) |
|
142 |
mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))} |
|
105 | 143 |
| expr WHEN IDENT |
106 |
{mkeexpr (EExpr_when ($1,$3))} |
|
107 |
| MERGE LPAR IDENT COMMA expr COMMA expr RPAR |
|
108 |
{mkeexpr (EExpr_merge ($3,$5,$7))} |
|
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 */ |
|
109 | 153 |
| IDENT LPAR expr RPAR |
110 |
{mkeexpr (EExpr_appl ($1, $3, None))}
|
|
154 |
{mkexpr (Expr_appl ($1, $3, None))}
|
|
111 | 155 |
| IDENT LPAR expr RPAR EVERY IDENT |
112 |
{mkeexpr (EExpr_appl ($1, $3, Some $6))} |
|
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))) } |
|
113 | 159 |
| IDENT LPAR tuple_expr RPAR |
114 |
{mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), None))}
|
|
160 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
|
|
115 | 161 |
| IDENT LPAR tuple_expr RPAR EVERY IDENT |
116 |
{mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), Some $6)) } |
|
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))) } |
|
117 | 165 |
|
118 | 166 |
/* Boolean expr */ |
119 | 167 |
| expr AND expr |
120 |
{mkepredef_call "&&" [$1;$3]}
|
|
168 |
{mkpredef_call "&&" [$1;$3]} |
|
121 | 169 |
| expr AMPERAMPER expr |
122 |
{mkepredef_call "&&" [$1;$3]}
|
|
170 |
{mkpredef_call "&&" [$1;$3]} |
|
123 | 171 |
| expr OR expr |
124 |
{mkepredef_call "||" [$1;$3]}
|
|
172 |
{mkpredef_call "||" [$1;$3]} |
|
125 | 173 |
| expr BARBAR expr |
126 |
{mkepredef_call "||" [$1;$3]}
|
|
174 |
{mkpredef_call "||" [$1;$3]} |
|
127 | 175 |
| expr XOR expr |
128 |
{mkepredef_call "xor" [$1;$3]}
|
|
176 |
{mkpredef_call "xor" [$1;$3]} |
|
129 | 177 |
| NOT expr |
130 |
{mkepredef_unary_call "not" $2}
|
|
178 |
{mkpredef_unary_call "not" $2} |
|
131 | 179 |
| expr IMPL expr |
132 |
{mkepredef_call "impl" [$1;$3]}
|
|
180 |
{mkpredef_call "impl" [$1;$3]} |
|
133 | 181 |
|
134 | 182 |
/* Comparison expr */ |
135 | 183 |
| expr EQ expr |
136 |
{mkepredef_call "=" [$1;$3]}
|
|
184 |
{mkpredef_call "=" [$1;$3]} |
|
137 | 185 |
| expr LT expr |
138 |
{mkepredef_call "<" [$1;$3]}
|
|
186 |
{mkpredef_call "<" [$1;$3]} |
|
139 | 187 |
| expr LTE expr |
140 |
{mkepredef_call "<=" [$1;$3]}
|
|
188 |
{mkpredef_call "<=" [$1;$3]} |
|
141 | 189 |
| expr GT expr |
142 |
{mkepredef_call ">" [$1;$3]}
|
|
190 |
{mkpredef_call ">" [$1;$3]} |
|
143 | 191 |
| expr GTE expr |
144 |
{mkepredef_call ">=" [$1;$3]}
|
|
192 |
{mkpredef_call ">=" [$1;$3]} |
|
145 | 193 |
| expr NEQ expr |
146 |
{mkepredef_call "!=" [$1;$3]}
|
|
194 |
{mkpredef_call "!=" [$1;$3]} |
|
147 | 195 |
|
148 | 196 |
/* Arithmetic expr */ |
149 | 197 |
| expr PLUS expr |
150 |
{mkepredef_call "+" [$1;$3]}
|
|
198 |
{mkpredef_call "+" [$1;$3]} |
|
151 | 199 |
| expr MINUS expr |
152 |
{mkepredef_call "-" [$1;$3]}
|
|
200 |
{mkpredef_call "-" [$1;$3]} |
|
153 | 201 |
| expr MULT expr |
154 |
{mkepredef_call "*" [$1;$3]}
|
|
202 |
{mkpredef_call "*" [$1;$3]} |
|
155 | 203 |
| expr DIV expr |
156 |
{mkepredef_call "/" [$1;$3]}
|
|
204 |
{mkpredef_call "/" [$1;$3]} |
|
157 | 205 |
| MINUS expr %prec UMINUS |
158 |
{mkepredef_unary_call "uminus" $2}
|
|
206 |
{mkpredef_unary_call "uminus" $2}
|
|
159 | 207 |
| expr MOD expr |
160 |
{mkepredef_call "mod" [$1;$3]} |
|
161 |
|
|
162 |
/* Temp op */ |
|
163 |
| PRE expr |
|
164 |
{mkeexpr (EExpr_pre $2)} |
|
208 |
{mkpredef_call "mod" [$1;$3]} |
|
165 | 209 |
|
166 | 210 |
/* If */ |
167 | 211 |
| IF expr THEN expr ELSE expr |
168 |
{mkepredef_call "ite" [$2;$4;$6]} |
|
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) } |
|
169 | 221 |
|
170 |
/* Quantifiers */ |
|
171 |
| EXISTS vdecl SCOL expr %prec prec_exists {mkeexpr (EExpr_exists ($2, $4))} |
|
172 |
| FORALL vdecl SCOL expr %prec prec_forall {mkeexpr (EExpr_forall ($2, $4))} |
|
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 } |
|
173 | 227 |
|
174 | 228 |
vdecl: |
175 | 229 |
| ident_list COL typ clock |
... | ... | |
214 | 268 |
|
215 | 269 |
|
216 | 270 |
const: |
217 |
| INT {EConst_int $1}
|
|
218 |
| REAL {EConst_real $1}
|
|
219 |
| FLOAT {EConst_float $1}
|
|
220 |
| TRUE {EConst_bool true}
|
|
221 |
| FALSE {EConst_bool false}
|
|
222 |
| STRING {EConst_string $1}
|
|
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} |
|
223 | 277 |
|
224 | 278 |
lustre_annot: |
225 | 279 |
lustre_annot_list EOF { $1 } |
Also available in: Unified diff