lustrec / src / parserLustreSpec.mly @ d3e4c22f
History  View  Annotate  Download (5.71 KB)
1 
%{ 

2 
open Utils 
3 
open Corelang 
4 
open LustreSpec 
5 

6 
let mkeexpr x = mkeexpr (Location.symbol_rloc ()) x 
7 
let mkepredef_call x = mkepredef_call (Location.symbol_rloc ()) x 
8 
let mkepredef_unary_call x = mkepredef_unary_call (Location.symbol_rloc ()) x 
9 

10 
let mktyp x = mktyp (Location.symbol_rloc ()) x 
11 
let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x 
12 
let mkclock x = mkclock (Location.symbol_rloc ()) x 
13  
14 
%} 
15  
16  
17 
%token <int> INT 
18 
%token <string> REAL 
19 
%token <float> FLOAT 
20 
%token <string> STRING 
21 
%token TRUE FALSE STATELESS ASSERT INCLUDE QUOTE 
22 
%token <string> IDENT 
23 
%token LPAR RPAR SCOL COL COMMA COLCOL 
24 
%token AMPERAMPER BARBAR NOT POWER 
25 
%token IF THEN ELSE 
26 
%token UCLOCK DCLOCK PHCLOCK TAIL 
27 
%token MERGE FBY WHEN WHENNOT EVERY 
28 
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST 
29 
%token TINT TFLOAT TREAL TBOOL TCLOCK 
30 
%token RATE DUE 
31 
%token EQ LT GT LTE GTE NEQ 
32 
%token AND OR XOR IMPL 
33 
%token MULT DIV MOD 
34 
%token MINUS PLUS UMINUS 
35 
%token PRE ARROW 
36 
%token EOF 
37 
%token REQUIRES ENSURES OBSERVER 
38 
%token INVARIANT BEHAVIOR ASSUMES 
39 
%token EXISTS FORALL 
40  
41 
%nonassoc prec_exists prec_forall 
42 
%nonassoc COMMA POWER 
43 
%left MERGE IF 
44 
%nonassoc ELSE 
45 
%right ARROW FBY 
46 
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK 
47 
%right COLCOL 
48 
%right IMPL 
49 
%left OR XOR BARBAR 
50 
%left AND AMPERAMPER 
51 
%left NOT 
52 
%nonassoc EQ LT GT LTE GTE NEQ 
53 
%left MINUS PLUS 
54 
%left MULT DIV MOD 
55 
%left PRE 
56 
%nonassoc UMINUS 
57  
58 
%start lustre_annot 
59 
%type <LustreSpec.expr_annot> lustre_annot 
60  
61 
%start lustre_spec 
62 
%type <LustreSpec.node_annot> lustre_spec 
63  
64 
%% 
65  
66 
lustre_spec: 
67 
 contract EOF { $1 } 
68  
69 
contract: 
70 
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; } } 
71 

72 
requires: 
73 
{ [] } 
74 
 REQUIRES expr SCOL requires { $2::$4 } 
75  
76 
ensures: 
77 
{ [] } 
78 
 ENSURES expr SCOL ensures { (EnsuresExpr $2) :: $4 } 
79 
 OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 } 
80  
81 
behaviors: 
82 
{ [] } 
83 
 BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5)::$6 } 
84  
85 
assumes: 
86 
{ [] } 
87 
 ASSUMES expr SCOL assumes { $2::$4 } 
88  
89 
tuple_expr: 
90 
 expr COMMA expr {[$3;$1]} 
91 
 tuple_expr COMMA expr {$3::$1} 
92  
93 
expr: 
94 
 const {mkeexpr (EExpr_const $1)} 
95 
 IDENT 
96 
{mkeexpr (EExpr_ident $1)} 
97 
 LPAR expr RPAR 
98 
{$2} 
99 
 LPAR tuple_expr RPAR 
100 
{mkeexpr (EExpr_tuple (List.rev $2))} 
101 
 expr ARROW expr 
102 
{mkeexpr (EExpr_arrow ($1,$3))} 
103 
 expr FBY expr 
104 
{mkeexpr (EExpr_fby ($1,$3))} 
105 
 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))} 
109 
 IDENT LPAR expr RPAR 
110 
{mkeexpr (EExpr_appl ($1, $3, None))} 
111 
 IDENT LPAR expr RPAR EVERY IDENT 
112 
{mkeexpr (EExpr_appl ($1, $3, Some $6))} 
113 
 IDENT LPAR tuple_expr RPAR 
114 
{mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), None))} 
115 
 IDENT LPAR tuple_expr RPAR EVERY IDENT 
116 
{mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), Some $6)) } 
117  
118 
/* Boolean expr */ 
119 
 expr AND expr 
120 
{mkepredef_call "&&" [$1;$3]} 
121 
 expr AMPERAMPER expr 
122 
{mkepredef_call "&&" [$1;$3]} 
123 
 expr OR expr 
124 
{mkepredef_call "" [$1;$3]} 
125 
 expr BARBAR expr 
126 
{mkepredef_call "" [$1;$3]} 
127 
 expr XOR expr 
128 
{mkepredef_call "xor" [$1;$3]} 
129 
 NOT expr 
130 
{mkepredef_unary_call "not" $2} 
131 
 expr IMPL expr 
132 
{mkepredef_call "impl" [$1;$3]} 
133  
134 
/* Comparison expr */ 
135 
 expr EQ expr 
136 
{mkepredef_call "=" [$1;$3]} 
137 
 expr LT expr 
138 
{mkepredef_call "<" [$1;$3]} 
139 
 expr LTE expr 
140 
{mkepredef_call "<=" [$1;$3]} 
141 
 expr GT expr 
142 
{mkepredef_call ">" [$1;$3]} 
143 
 expr GTE expr 
144 
{mkepredef_call ">=" [$1;$3]} 
145 
 expr NEQ expr 
146 
{mkepredef_call "!=" [$1;$3]} 
147  
148 
/* Arithmetic expr */ 
149 
 expr PLUS expr 
150 
{mkepredef_call "+" [$1;$3]} 
151 
 expr MINUS expr 
152 
{mkepredef_call "" [$1;$3]} 
153 
 expr MULT expr 
154 
{mkepredef_call "*" [$1;$3]} 
155 
 expr DIV expr 
156 
{mkepredef_call "/" [$1;$3]} 
157 
 MINUS expr %prec UMINUS 
158 
{mkepredef_unary_call "uminus" $2} 
159 
 expr MOD expr 
160 
{mkepredef_call "mod" [$1;$3]} 
161  
162 
/* Temp op */ 
163 
 PRE expr 
164 
{mkeexpr (EExpr_pre $2)} 
165  
166 
/* If */ 
167 
 IF expr THEN expr ELSE expr 
168 
{mkepredef_call "ite" [$2;$4;$6]} 
169  
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))} 
173  
174 
vdecl: 
175 
 ident_list COL typ clock 
176 
{List.map mkvar_decl (List.map (fun id > (id, $3, $4, false)) $1)} 
177 
 CONST ident_list COL typ clock 
178 
{List.map mkvar_decl (List.map (fun id > (id, $4, $5, true)) $2)} 
179  
180  
181 
ident_list: 
182 
IDENT {[$1]} 
183 
 ident_list COMMA IDENT {$3::$1} 
184  
185  
186 
typ: 
187 
{mktyp Tydec_any} 
188 
 TINT {mktyp Tydec_int} 
189 
 IDENT { 
190 
try 
191 
mktyp (Hashtbl.find Corelang.type_table (Tydec_const $1)) 
192 
with Not_found > raise (Corelang.Error (Location.symbol_rloc(), Corelang.Unbound_symbol ("type " ^ $1))) 
193 
} 
194 
 TFLOAT {mktyp Tydec_float} 
195 
 TREAL {mktyp Tydec_real} 
196 
 TBOOL {mktyp Tydec_bool} 
197 
 TCLOCK {mktyp (Tydec_clock Tydec_bool) } 
198 
 typ POWER INT {mktyp Tydec_any (*(mktyptuple $3 $1)*)} 
199 
 typ POWER IDENT {mktyp Tydec_any (*(mktyptuple (try 
200 
match get_const $3 with Const_int i > i with _ > failwith "Const power error") $1)*)} 
201  
202 
clock: 
203 
{mkclock Ckdec_any} 
204 
 when_list 
205 
{mkclock (Ckdec_bool (List.rev $1))} 
206  
207 
when_cond: 
208 
WHEN IDENT {($2, tag_true)} 
209 
 WHENNOT IDENT {($2, tag_false)} 
210  
211 
when_list: 
212 
when_cond {[$1]} 
213 
 when_list when_cond {$2::$1} 
214  
215  
216 
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} 
223  
224 
lustre_annot: 
225 
lustre_annot_list EOF { $1 } 
226  
227 
lustre_annot_list: 
228 
{ [] } 
229 
 kwd COL expr SCOL lustre_annot_list { ($1,$3)::$5 } 
230 
 IDENT COL expr SCOL lustre_annot_list { ([$1],$3)::$5 } 
231 
 INVARIANT COL expr SCOL lustre_annot_list{ (["invariant"],$3)::$5 } 
232 
 OBSERVER COL expr SCOL lustre_annot_list { (["observer"],$3)::$5 } 
233  
234 
kwd: 
235 
DIV { [] } 
236 
 DIV IDENT kwd { $2::$3} 