Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parserLustreSpec.mly @ 01c7d5e1

History | View | Annotate | Download (7.28 KB)

1 22fe1c93 ploc
%{
2
  open Utils
3
  open Corelang
4
  open LustreSpec
5
  
6 01c7d5e1 ploc
  let mkexpr x = mkexpr (Location.symbol_rloc ()) x
7
  let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x
8
  let mkpredef_unary_call x = mkpredef_unary_call (Location.symbol_rloc ()) x
9
10 22fe1c93 ploc
  let mkeexpr x = mkeexpr (Location.symbol_rloc ()) x
11 01c7d5e1 ploc
  (*
12 22fe1c93 ploc
  let mkepredef_call x = mkepredef_call (Location.symbol_rloc ()) x
13
  let mkepredef_unary_call x = mkepredef_unary_call (Location.symbol_rloc ()) x
14 01c7d5e1 ploc
  *)
15
16 22fe1c93 ploc
  let mktyp x = mktyp (Location.symbol_rloc ()) x
17
  let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x
18
  let mkclock x = mkclock (Location.symbol_rloc ()) x
19
20
%}
21
22
23
%token <int> INT
24
%token <string> REAL
25
%token <float> FLOAT
26
%token <string> STRING
27
%token TRUE FALSE STATELESS ASSERT INCLUDE QUOTE
28
%token <string> IDENT
29
%token LPAR RPAR SCOL COL COMMA COLCOL
30
%token AMPERAMPER BARBAR NOT POWER
31
%token IF THEN ELSE
32
%token UCLOCK DCLOCK PHCLOCK TAIL
33
%token MERGE FBY WHEN WHENNOT EVERY
34
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST
35
%token TINT TFLOAT TREAL TBOOL TCLOCK
36
%token RATE DUE
37
%token EQ LT GT LTE GTE NEQ
38
%token AND OR XOR IMPL
39
%token MULT DIV MOD
40
%token MINUS PLUS UMINUS
41
%token PRE ARROW
42
%token EOF
43
%token REQUIRES ENSURES OBSERVER
44
%token INVARIANT BEHAVIOR ASSUMES
45
%token EXISTS FORALL
46
47
%nonassoc prec_exists prec_forall
48
%nonassoc COMMA POWER
49
%left MERGE IF
50
%nonassoc ELSE
51
%right ARROW FBY
52
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK
53
%right COLCOL
54
%right IMPL
55
%left OR XOR BARBAR
56
%left AND AMPERAMPER
57
%left NOT
58
%nonassoc EQ LT GT LTE GTE NEQ
59
%left MINUS PLUS
60
%left MULT DIV MOD
61
%left PRE 
62
%nonassoc UMINUS
63
64
%start lustre_annot
65
%type <LustreSpec.expr_annot> lustre_annot
66
67
%start lustre_spec
68
%type <LustreSpec.node_annot> lustre_spec
69
70
%%
71
72
lustre_spec:
73
| contract EOF { $1 }
74
75
contract:
76
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; } }
77
 
78
requires:
79
{ [] }
80 01c7d5e1 ploc
| REQUIRES qexpr SCOL requires { $2::$4 }
81 22fe1c93 ploc
82
ensures:
83
{ [] }
84 01c7d5e1 ploc
| ENSURES qexpr SCOL ensures { (EnsuresExpr $2) :: $4 }
85
| OBSERVER IDENT LPAR tuple_qexpr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 }
86 22fe1c93 ploc
87
behaviors:
88
{ [] }
89
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5)::$6 }
90
91
assumes:
92
{ [] }
93 01c7d5e1 ploc
| ASSUMES qexpr SCOL assumes { $2::$4 } 
94
95
tuple_qexpr:
96
| qexpr COMMA qexpr {[$3;$1]}
97
| tuple_qexpr COMMA qexpr {$3::$1}
98
99 22fe1c93 ploc
100
tuple_expr:
101 01c7d5e1 ploc
    expr COMMA expr {[$3;$1]}
102 22fe1c93 ploc
| tuple_expr COMMA expr {$3::$1}
103
104 01c7d5e1 ploc
// Same as tuple expr but accepting lists with single element
105
array_expr:
106
  expr {[$1]}
107
| expr COMMA array_expr {$1::$3}
108
109
dim_list:
110
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
111
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
112
113 22fe1c93 ploc
expr:
114 01c7d5e1 ploc
/* constants */
115
  INT {mkexpr (Expr_const (Const_int $1))}
116
| REAL {mkexpr (Expr_const (Const_real $1))}
117
| FLOAT {mkexpr (Expr_const (Const_float $1))}
118
/* Idents or type enum tags */
119
| IDENT {
120
  if Hashtbl.mem tag_table $1
121
  then mkexpr (Expr_const (Const_tag $1))
122
  else mkexpr (Expr_ident $1)}
123
| LPAR ANNOT expr RPAR
124
    {update_expr_annot $3 $2}
125 22fe1c93 ploc
| LPAR expr RPAR
126
    {$2}
127
| LPAR tuple_expr RPAR
128 01c7d5e1 ploc
    {mkexpr (Expr_tuple (List.rev $2))}
129
130
/* Array expressions */
131
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
132
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
133
| expr LBRACKET dim_list { $3 $1 }
134
135
/* Temporal operators */
136
| PRE expr 
137
    {mkexpr (Expr_pre $2)}
138 22fe1c93 ploc
| expr ARROW expr 
139 01c7d5e1 ploc
    {mkexpr (Expr_arrow ($1,$3))}
140 22fe1c93 ploc
| expr FBY expr 
141 01c7d5e1 ploc
    {(*mkexpr (Expr_fby ($1,$3))*)
142
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
143 22fe1c93 ploc
| expr WHEN IDENT 
144 01c7d5e1 ploc
    {mkexpr (Expr_when ($1,$3,tag_true))}
145
| expr WHENNOT IDENT
146
    {mkexpr (Expr_when ($1,$3,tag_false))}
147
| expr WHEN IDENT LPAR IDENT RPAR
148
    {mkexpr (Expr_when ($1, $5, $3))}
149
| MERGE IDENT handler_expr_list
150
    {mkexpr (Expr_merge ($2,$3))}
151
152
/* Applications */
153 22fe1c93 ploc
| IDENT LPAR expr RPAR
154 01c7d5e1 ploc
    {mkexpr (Expr_appl ($1, $3, None))}
155 22fe1c93 ploc
| IDENT LPAR expr RPAR EVERY IDENT
156 01c7d5e1 ploc
    {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}
157
| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR
158
    {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }
159 22fe1c93 ploc
| IDENT LPAR tuple_expr RPAR
160 01c7d5e1 ploc
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
161 22fe1c93 ploc
| IDENT LPAR tuple_expr RPAR EVERY IDENT
162 01c7d5e1 ploc
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }
163
| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR
164
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }
165 22fe1c93 ploc
166
/* Boolean expr */
167
| expr AND expr 
168 01c7d5e1 ploc
    {mkpredef_call "&&" [$1;$3]}
169 22fe1c93 ploc
| expr AMPERAMPER expr 
170 01c7d5e1 ploc
    {mkpredef_call "&&" [$1;$3]}
171 22fe1c93 ploc
| expr OR expr 
172 01c7d5e1 ploc
    {mkpredef_call "||" [$1;$3]}
173 22fe1c93 ploc
| expr BARBAR expr 
174 01c7d5e1 ploc
    {mkpredef_call "||" [$1;$3]}
175 22fe1c93 ploc
| expr XOR expr 
176 01c7d5e1 ploc
    {mkpredef_call "xor" [$1;$3]}
177 22fe1c93 ploc
| NOT expr 
178 01c7d5e1 ploc
    {mkpredef_unary_call "not" $2}
179 22fe1c93 ploc
| expr IMPL expr 
180 01c7d5e1 ploc
    {mkpredef_call "impl" [$1;$3]}
181 22fe1c93 ploc
182
/* Comparison expr */
183
| expr EQ expr 
184 01c7d5e1 ploc
    {mkpredef_call "=" [$1;$3]}
185 22fe1c93 ploc
| expr LT expr 
186 01c7d5e1 ploc
    {mkpredef_call "<" [$1;$3]}
187 22fe1c93 ploc
| expr LTE expr 
188 01c7d5e1 ploc
    {mkpredef_call "<=" [$1;$3]}
189 22fe1c93 ploc
| expr GT expr 
190 01c7d5e1 ploc
    {mkpredef_call ">" [$1;$3]}
191 22fe1c93 ploc
| expr GTE  expr 
192 01c7d5e1 ploc
    {mkpredef_call ">=" [$1;$3]}
193 22fe1c93 ploc
| expr NEQ expr 
194 01c7d5e1 ploc
    {mkpredef_call "!=" [$1;$3]}
195 22fe1c93 ploc
196
/* Arithmetic expr */
197
| expr PLUS expr 
198 01c7d5e1 ploc
    {mkpredef_call "+" [$1;$3]}
199 22fe1c93 ploc
| expr MINUS expr 
200 01c7d5e1 ploc
    {mkpredef_call "-" [$1;$3]}
201 22fe1c93 ploc
| expr MULT expr 
202 01c7d5e1 ploc
    {mkpredef_call "*" [$1;$3]}
203 22fe1c93 ploc
| expr DIV expr 
204 01c7d5e1 ploc
    {mkpredef_call "/" [$1;$3]}
205 22fe1c93 ploc
| MINUS expr %prec UMINUS
206 01c7d5e1 ploc
  {mkpredef_unary_call "uminus" $2}
207 22fe1c93 ploc
| expr MOD expr 
208 01c7d5e1 ploc
    {mkpredef_call "mod" [$1;$3]}
209 22fe1c93 ploc
210
/* If */
211
| IF expr THEN expr ELSE expr
212 01c7d5e1 ploc
    {mkexpr (Expr_ite ($2, $4, $6))}
213
214
215
handler_expr_list:
216
   { [] }
217
| handler_expr handler_expr_list { $1 :: $2 }
218
219
handler_expr:
220
 LPAR IDENT ARROW expr RPAR { ($2, $4) }
221 22fe1c93 ploc
222 01c7d5e1 ploc
qexpr:
223
| expr { mkeexpr [] $1 }
224
  /* Quantifiers */
225
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eepxr (Exists, $2) $4 } 
226
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eepxr (Forall, $2) $4 }
227 22fe1c93 ploc
228
vdecl:
229
| ident_list COL typ clock 
230
    {List.map mkvar_decl (List.map (fun id -> (id, $3, $4, false)) $1)}
231
| CONST ident_list COL typ clock 
232
    {List.map mkvar_decl (List.map (fun id -> (id, $4, $5, true)) $2)}
233
234
235
ident_list:
236
  IDENT {[$1]}
237
| ident_list COMMA IDENT {$3::$1}
238
239
240
typ:
241
    {mktyp Tydec_any}
242
| TINT {mktyp Tydec_int}
243
| IDENT {
244
  try 
245
    mktyp (Hashtbl.find Corelang.type_table (Tydec_const $1))
246 52cfee34 xthirioux
  with Not_found -> raise (Corelang.Error (Location.symbol_rloc(), Corelang.Unbound_symbol ("type " ^ $1)))
247 22fe1c93 ploc
}
248
| TFLOAT {mktyp Tydec_float}
249
| TREAL {mktyp Tydec_real}
250
| TBOOL {mktyp Tydec_bool}
251
| TCLOCK {mktyp (Tydec_clock Tydec_bool) }
252
| typ POWER INT {mktyp Tydec_any (*(mktyptuple $3 $1)*)}
253
| typ POWER IDENT {mktyp Tydec_any (*(mktyptuple (try 
254
					match get_const $3 with Const_int i -> i with _ -> failwith "Const power error") $1)*)}
255
256
clock:
257
    {mkclock Ckdec_any}
258
| when_list
259
    {mkclock (Ckdec_bool (List.rev $1))}
260
261
when_cond:
262
    WHEN IDENT {($2, tag_true)}
263
| WHENNOT IDENT {($2, tag_false)}
264
265
when_list:
266
    when_cond {[$1]}
267
| when_list when_cond {$2::$1}
268
269
270
const:
271 01c7d5e1 ploc
| INT {Const_int $1}
272
| REAL {Const_real $1}
273
| FLOAT {Const_float $1}
274
| TRUE {Const_bool true}
275
| FALSE {Const_bool false}
276
| STRING {Const_string $1}
277 22fe1c93 ploc
278
lustre_annot:
279
lustre_annot_list EOF { $1 }
280
281
lustre_annot_list:
282
  { [] } 
283
| kwd COL expr SCOL lustre_annot_list { ($1,$3)::$5 }
284
| IDENT COL expr SCOL lustre_annot_list { ([$1],$3)::$5 }
285
| INVARIANT COL expr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
286
| OBSERVER COL expr SCOL lustre_annot_list { (["observer"],$3)::$5 }
287
288
kwd:
289
DIV { [] }
290
| DIV IDENT kwd { $2::$3}