lustrec / src / parserLustreSpec.mly @ 22fe1c93
History  View  Annotate  Download (5.86 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 COLCOL expr 
106 
{mkeexpr (EExpr_concat ($1,$3))} 
107 
 TAIL LPAR expr RPAR 
108 
{mkeexpr (EExpr_tail $3)} 
109 
 expr WHEN IDENT 
110 
{mkeexpr (EExpr_when ($1,$3))} 
111 
 expr WHENNOT IDENT 
112 
{mkeexpr (EExpr_whennot ($1,$3))} 
113 
 MERGE LPAR IDENT COMMA expr COMMA expr RPAR 
114 
{mkeexpr (EExpr_merge ($3,$5,$7))} 
115 
 IDENT LPAR expr RPAR 
116 
{mkeexpr (EExpr_appl ($1, $3, None))} 
117 
 IDENT LPAR expr RPAR EVERY IDENT 
118 
{mkeexpr (EExpr_appl ($1, $3, Some $6))} 
119 
 IDENT LPAR tuple_expr RPAR 
120 
{mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), None))} 
121 
 IDENT LPAR tuple_expr RPAR EVERY IDENT 
122 
{mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), Some $6)) } 
123  
124 
/* Boolean expr */ 
125 
 expr AND expr 
126 
{mkepredef_call "&&" [$1;$3]} 
127 
 expr AMPERAMPER expr 
128 
{mkepredef_call "&&" [$1;$3]} 
129 
 expr OR expr 
130 
{mkepredef_call "" [$1;$3]} 
131 
 expr BARBAR expr 
132 
{mkepredef_call "" [$1;$3]} 
133 
 expr XOR expr 
134 
{mkepredef_call "xor" [$1;$3]} 
135 
 NOT expr 
136 
{mkepredef_unary_call "not" $2} 
137 
 expr IMPL expr 
138 
{mkepredef_call "impl" [$1;$3]} 
139  
140 
/* Comparison expr */ 
141 
 expr EQ expr 
142 
{mkepredef_call "=" [$1;$3]} 
143 
 expr LT expr 
144 
{mkepredef_call "<" [$1;$3]} 
145 
 expr LTE expr 
146 
{mkepredef_call "<=" [$1;$3]} 
147 
 expr GT expr 
148 
{mkepredef_call ">" [$1;$3]} 
149 
 expr GTE expr 
150 
{mkepredef_call ">=" [$1;$3]} 
151 
 expr NEQ expr 
152 
{mkepredef_call "!=" [$1;$3]} 
153  
154 
/* Arithmetic expr */ 
155 
 expr PLUS expr 
156 
{mkepredef_call "+" [$1;$3]} 
157 
 expr MINUS expr 
158 
{mkepredef_call "" [$1;$3]} 
159 
 expr MULT expr 
160 
{mkepredef_call "*" [$1;$3]} 
161 
 expr DIV expr 
162 
{mkepredef_call "/" [$1;$3]} 
163 
 MINUS expr %prec UMINUS 
164 
{mkepredef_unary_call "uminus" $2} 
165 
 expr MOD expr 
166 
{mkepredef_call "mod" [$1;$3]} 
167  
168 
/* Temp op */ 
169 
 PRE expr 
170 
{mkeexpr (EExpr_pre $2)} 
171  
172 
/* If */ 
173 
 IF expr THEN expr ELSE expr 
174 
{mkepredef_call "ite" [$2;$4;$6]} 
175  
176 
/* Quantifiers */ 
177 
 EXISTS vdecl SCOL expr %prec prec_exists {mkeexpr (EExpr_exists ($2, $4))} 
178 
 FORALL vdecl SCOL expr %prec prec_forall {mkeexpr (EExpr_forall ($2, $4))} 
179  
180 
vdecl: 
181 
 ident_list COL typ clock 
182 
{List.map mkvar_decl (List.map (fun id > (id, $3, $4, false)) $1)} 
183 
 CONST ident_list COL typ clock 
184 
{List.map mkvar_decl (List.map (fun id > (id, $4, $5, true)) $2)} 
185  
186  
187 
ident_list: 
188 
IDENT {[$1]} 
189 
 ident_list COMMA IDENT {$3::$1} 
190  
191  
192 
typ: 
193 
{mktyp Tydec_any} 
194 
 TINT {mktyp Tydec_int} 
195 
 IDENT { 
196 
try 
197 
mktyp (Hashtbl.find Corelang.type_table (Tydec_const $1)) 
198 
with Not_found > raise (Corelang.Unbound_type ((Tydec_const $1),Location.symbol_rloc())) 
199 
} 
200 
 TFLOAT {mktyp Tydec_float} 
201 
 TREAL {mktyp Tydec_real} 
202 
 TBOOL {mktyp Tydec_bool} 
203 
 TCLOCK {mktyp (Tydec_clock Tydec_bool) } 
204 
 typ POWER INT {mktyp Tydec_any (*(mktyptuple $3 $1)*)} 
205 
 typ POWER IDENT {mktyp Tydec_any (*(mktyptuple (try 
206 
match get_const $3 with Const_int i > i with _ > failwith "Const power error") $1)*)} 
207  
208 
clock: 
209 
{mkclock Ckdec_any} 
210 
 when_list 
211 
{mkclock (Ckdec_bool (List.rev $1))} 
212  
213 
when_cond: 
214 
WHEN IDENT {($2, tag_true)} 
215 
 WHENNOT IDENT {($2, tag_false)} 
216  
217 
when_list: 
218 
when_cond {[$1]} 
219 
 when_list when_cond {$2::$1} 
220  
221  
222 
const: 
223 
 INT {EConst_int $1} 
224 
 REAL {EConst_real $1} 
225 
 FLOAT {EConst_float $1} 
226 
 TRUE {EConst_bool true} 
227 
 FALSE {EConst_bool false} 
228 
 STRING {EConst_string $1} 
229  
230 
lustre_annot: 
231 
lustre_annot_list EOF { $1 } 
232  
233 
lustre_annot_list: 
234 
{ [] } 
235 
 kwd COL expr SCOL lustre_annot_list { ($1,$3)::$5 } 
236 
 IDENT COL expr SCOL lustre_annot_list { ([$1],$3)::$5 } 
237 
 INVARIANT COL expr SCOL lustre_annot_list{ (["invariant"],$3)::$5 } 
238 
 OBSERVER COL expr SCOL lustre_annot_list { (["observer"],$3)::$5 } 
239  
240 
kwd: 
241 
DIV { [] } 
242 
 DIV IDENT kwd { $2::$3} 