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