lustrec / src / parserLustreSpec.mly @ 0038002e
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} 