Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parserLustreSpec.mly @ e9350b02

History | View | Annotate | Download (8.01 KB)

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