lustrec / src / parserLustreSpec.mly @ 6394042a
History | View | Annotate | Download (8.01 KB)
1 |
%{ |
---|---|
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 |
%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.ident -> 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 |
| 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 |
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 |
| LPAR expr RPAR |
137 |
{$2} |
138 |
| LPAR tuple_expr RPAR |
139 |
{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 |
| expr ARROW expr |
150 |
{mkexpr (Expr_arrow ($1,$3))} |
151 |
| expr FBY expr |
152 |
{(*mkexpr (Expr_fby ($1,$3))*) |
153 |
mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))} |
154 |
| expr WHEN IDENT |
155 |
{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 |
| IDENT LPAR expr RPAR |
165 |
{mkexpr (Expr_appl ($1, $3, None))} |
166 |
| IDENT LPAR expr RPAR EVERY IDENT |
167 |
{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 |
| IDENT LPAR tuple_expr RPAR |
171 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))} |
172 |
| IDENT LPAR tuple_expr RPAR EVERY IDENT |
173 |
{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 |
|
177 |
/* Boolean expr */ |
178 |
| expr AND expr |
179 |
{mkpredef_call "&&" [$1;$3]} |
180 |
| expr AMPERAMPER expr |
181 |
{mkpredef_call "&&" [$1;$3]} |
182 |
| expr OR expr |
183 |
{mkpredef_call "||" [$1;$3]} |
184 |
| expr BARBAR expr |
185 |
{mkpredef_call "||" [$1;$3]} |
186 |
| expr XOR expr |
187 |
{mkpredef_call "xor" [$1;$3]} |
188 |
| NOT expr |
189 |
{mkpredef_unary_call "not" $2} |
190 |
| expr IMPL expr |
191 |
{mkpredef_call "impl" [$1;$3]} |
192 |
|
193 |
/* Comparison expr */ |
194 |
| expr EQ expr |
195 |
{mkpredef_call "=" [$1;$3]} |
196 |
| expr LT expr |
197 |
{mkpredef_call "<" [$1;$3]} |
198 |
| expr LTE expr |
199 |
{mkpredef_call "<=" [$1;$3]} |
200 |
| expr GT expr |
201 |
{mkpredef_call ">" [$1;$3]} |
202 |
| expr GTE expr |
203 |
{mkpredef_call ">=" [$1;$3]} |
204 |
| expr NEQ expr |
205 |
{mkpredef_call "!=" [$1;$3]} |
206 |
|
207 |
/* Arithmetic expr */ |
208 |
| expr PLUS expr |
209 |
{mkpredef_call "+" [$1;$3]} |
210 |
| expr MINUS expr |
211 |
{mkpredef_call "-" [$1;$3]} |
212 |
| expr MULT expr |
213 |
{mkpredef_call "*" [$1;$3]} |
214 |
| expr DIV expr |
215 |
{mkpredef_call "/" [$1;$3]} |
216 |
| MINUS expr %prec UMINUS |
217 |
{mkpredef_unary_call "uminus" $2} |
218 |
| expr MOD expr |
219 |
{mkpredef_call "mod" [$1;$3]} |
220 |
|
221 |
/* If */ |
222 |
| IF expr THEN expr ELSE expr |
223 |
{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 |
|
233 |
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 |
|
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 |
with Not_found -> raise (Corelang.Error (Location.symbol_rloc(), Corelang.Unbound_symbol ("type " ^ $1))) |
258 |
} |
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 |
| 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 |
|
289 |
lustre_annot: |
290 |
lustre_annot_list EOF { fun node_id -> $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} |