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