lustrec / src / parserLustreSpec.mly @ 3bc26d43
History  View  Annotate  Download (8.28 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 CCODE MATLAB 
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 
 TRUE {mkexpr (Expr_const (Const_bool true))} 
130 
 FALSE {mkexpr (Expr_const (Const_bool false))} 
131 
 STRING {mkexpr (Expr_const (Const_string $1))} 
132 
/* Idents or type enum tags */ 
133 
 IDENT { 
134 
if Hashtbl.mem tag_table $1 
135 
then mkexpr (Expr_const (Const_tag $1)) 
136 
else mkexpr (Expr_ident $1)} 
137 
 LPAR ANNOT expr RPAR 
138 
{update_expr_annot $3 $2} 
139 
 LPAR expr RPAR 
140 
{$2} 
141 
 LPAR tuple_expr RPAR 
142 
{mkexpr (Expr_tuple (List.rev $2))} 
143  
144 
/* Array expressions */ 
145 
 LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) } 
146 
 expr POWER dim { mkexpr (Expr_power ($1, $3)) } 
147 
 expr LBRACKET dim_list { $3 $1 } 
148  
149 
/* Temporal operators */ 
150 
 PRE expr 
151 
{mkexpr (Expr_pre $2)} 
152 
 expr ARROW expr 
153 
{mkexpr (Expr_arrow ($1,$3))} 
154 
 expr FBY expr 
155 
{(*mkexpr (Expr_fby ($1,$3))*) 
156 
mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))} 
157 
 expr WHEN IDENT 
158 
{mkexpr (Expr_when ($1,$3,tag_true))} 
159 
 expr WHENNOT IDENT 
160 
{mkexpr (Expr_when ($1,$3,tag_false))} 
161 
 expr WHEN IDENT LPAR IDENT RPAR 
162 
{mkexpr (Expr_when ($1, $5, $3))} 
163 
 MERGE IDENT handler_expr_list 
164 
{mkexpr (Expr_merge ($2,$3))} 
165  
166 
/* Applications */ 
167 
 IDENT LPAR expr RPAR 
168 
{mkexpr (Expr_appl ($1, $3, None))} 
169 
 IDENT LPAR expr RPAR EVERY IDENT 
170 
{mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))} 
171 
 IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR 
172 
{mkexpr (Expr_appl ($1, $3, Some ($8, $6))) } 
173 
 IDENT LPAR tuple_expr RPAR 
174 
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))} 
175 
 IDENT LPAR tuple_expr RPAR EVERY IDENT 
176 
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) } 
177 
 IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR 
178 
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) } 
179  
180 
/* Boolean expr */ 
181 
 expr AND expr 
182 
{mkpredef_call "&&" [$1;$3]} 
183 
 expr AMPERAMPER expr 
184 
{mkpredef_call "&&" [$1;$3]} 
185 
 expr OR expr 
186 
{mkpredef_call "" [$1;$3]} 
187 
 expr BARBAR expr 
188 
{mkpredef_call "" [$1;$3]} 
189 
 expr XOR expr 
190 
{mkpredef_call "xor" [$1;$3]} 
191 
 NOT expr 
192 
{mkpredef_unary_call "not" $2} 
193 
 expr IMPL expr 
194 
{mkpredef_call "impl" [$1;$3]} 
195  
196 
/* Comparison expr */ 
197 
 expr EQ expr 
198 
{mkpredef_call "=" [$1;$3]} 
199 
 expr LT expr 
200 
{mkpredef_call "<" [$1;$3]} 
201 
 expr LTE expr 
202 
{mkpredef_call "<=" [$1;$3]} 
203 
 expr GT expr 
204 
{mkpredef_call ">" [$1;$3]} 
205 
 expr GTE expr 
206 
{mkpredef_call ">=" [$1;$3]} 
207 
 expr NEQ expr 
208 
{mkpredef_call "!=" [$1;$3]} 
209  
210 
/* Arithmetic expr */ 
211 
 expr PLUS expr 
212 
{mkpredef_call "+" [$1;$3]} 
213 
 expr MINUS expr 
214 
{mkpredef_call "" [$1;$3]} 
215 
 expr MULT expr 
216 
{mkpredef_call "*" [$1;$3]} 
217 
 expr DIV expr 
218 
{mkpredef_call "/" [$1;$3]} 
219 
 MINUS expr %prec UMINUS 
220 
{mkpredef_unary_call "uminus" $2} 
221 
 expr MOD expr 
222 
{mkpredef_call "mod" [$1;$3]} 
223  
224 
/* If */ 
225 
 IF expr THEN expr ELSE expr 
226 
{mkexpr (Expr_ite ($2, $4, $6))} 
227  
228  
229 
handler_expr_list: 
230 
{ [] } 
231 
 handler_expr handler_expr_list { $1 :: $2 } 
232  
233 
handler_expr: 
234 
LPAR IDENT ARROW expr RPAR { ($2, $4) } 
235  
236 
qexpr: 
237 
 expr { mkeexpr [] $1 } 
238 
/* Quantifiers */ 
239 
 EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eepxr (Exists, $2) $4 } 
240 
 FORALL vdecl SCOL qexpr %prec prec_forall { extend_eepxr (Forall, $2) $4 } 
241  
242 
vdecl: 
243 
 ident_list COL typ clock 
244 
{List.map mkvar_decl (List.map (fun id > (id, $3, $4, false)) $1)} 
245 
 CONST ident_list COL typ clock 
246 
{List.map mkvar_decl (List.map (fun id > (id, $4, $5, true)) $2)} 
247  
248  
249 
ident_list: 
250 
IDENT {[$1]} 
251 
 ident_list COMMA IDENT {$3::$1} 
252  
253  
254 
typ: 
255 
{mktyp Tydec_any} 
256 
 TINT {mktyp Tydec_int} 
257 
 IDENT { 
258 
try 
259 
mktyp (Hashtbl.find Corelang.type_table (Tydec_const $1)) 
260 
with Not_found > raise (Corelang.Error (Location.symbol_rloc(), Corelang.Unbound_symbol ("type " ^ $1))) 
261 
} 
262 
 TFLOAT {mktyp Tydec_float} 
263 
 TREAL {mktyp Tydec_real} 
264 
 TBOOL {mktyp Tydec_bool} 
265 
 TCLOCK {mktyp (Tydec_clock Tydec_bool) } 
266 
 typ POWER INT {mktyp Tydec_any (*(mktyptuple $3 $1)*)} 
267 
 typ POWER IDENT {mktyp Tydec_any (*(mktyptuple (try 
268 
match get_const $3 with Const_int i > i with _ > failwith "Const power error") $1)*)} 
269  
270 
clock: 
271 
{mkclock Ckdec_any} 
272 
 when_list 
273 
{mkclock (Ckdec_bool (List.rev $1))} 
274  
275 
when_cond: 
276 
WHEN IDENT {($2, tag_true)} 
277 
 WHENNOT IDENT {($2, tag_false)} 
278  
279 
when_list: 
280 
when_cond {[$1]} 
281 
 when_list when_cond {$2::$1} 
282  
283  
284 
const: 
285 
 INT {Const_int $1} 
286 
 REAL {Const_real $1} 
287 
 FLOAT {Const_float $1} 
288 
 TRUE {Const_bool true} 
289 
 FALSE {Const_bool false} 
290 
 STRING {Const_string $1} 
291  
292 
lustre_annot: 
293 
lustre_annot_list EOF { fun node_id > $1 } 
294  
295 
lustre_annot_list: 
296 
{ [] } 
297 
 kwd COL expr SCOL lustre_annot_list { ($1,$3)::$5 } 
298 
 IDENT COL expr SCOL lustre_annot_list { ([$1],$3)::$5 } 
299 
 INVARIANT COL expr SCOL lustre_annot_list{ (["invariant"],$3)::$5 } 
300 
 OBSERVER COL expr SCOL lustre_annot_list { (["observer"],$3)::$5 } 
301 
 CCODE COL const lustre_annot_list{ (["c_code"],$3)::$5 } 
302 
 MATLAB COL const lustre_annot_list{ (["matlab"],$3)::$5 } 
303  
304 
kwd: 
305 
DIV { [] } 
306 
 DIV IDENT kwd { $2::$3} 