Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parsers / parserLustreSpec.mly @ f4cba4b8

History | View | Annotate | Download (8.41 KB)

1
%{
2
(********************************************************************)
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
  open Utils
14
  open Corelang
15
  open LustreSpec
16
  
17
  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
  let mkeexpr x = mkeexpr (Location.symbol_rloc ()) x
22
  (*
23
  let mkepredef_call x = mkepredef_call (Location.symbol_rloc ()) x
24
  let mkepredef_unary_call x = mkepredef_unary_call (Location.symbol_rloc ()) x
25
  *)
26

    
27
  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 CCODE MATLAB
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
%type <LustreSpec.ident -> LustreSpec.expr_annot> lustre_annot
77

    
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
{ [] }
88
| CONST ident EQ expr SCOL contract
89
    { Const($2, None, $4)::$3 }
90
| CONST ident COL typeconst EQ expr SCOL contract
91
    { Const($2, Some($4), $6)::$3 }
92
| ASSUME qexpr SCOL contract
93
    { Assume($2)::$4 }
94
| GUARANTEES qexpr SCOL contract	
95
    { Guarantees($2)::$4 }
96
| MODE ident LPAR mode_content RPAR SCOL contract
97
    { Mode($2,$4)::$7 }	
98
| IMPORT ident LPAR expr RPAR returns LPAR expr RPAR SCOL contract
99
    { Import($2, $4, $8)::$11 }
100
	
101

    
102
mode_content:
103
{ [] }
104
| REQUIRE qexpr COL mode_content { Require($2)::$4 }
105
| ENSURE qexpr COL mode_content { Require($2)::$4 }
106

    
107
tuple_qexpr:
108
| qexpr COMMA qexpr {[$3;$1]}
109
| tuple_qexpr COMMA qexpr {$3::$1}
110

    
111

    
112
tuple_expr:
113
    expr COMMA expr {[$3;$1]}
114
| tuple_expr COMMA expr {$3::$1}
115

    
116
// Same as tuple expr but accepting lists with single element
117
array_expr:
118
  expr {[$1]}
119
| expr COMMA array_expr {$1::$3}
120

    
121
dim_list:
122
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
123
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
124

    
125
expr:
126
/* constants */
127
| INT {mkexpr (Expr_const (Const_int $1))}
128
| REAL {mkexpr (Expr_const (Const_real $1))}
129
| FLOAT {mkexpr (Expr_const (Const_float $1))}
130
| TRUE {mkexpr (Expr_const (Const_bool true))}
131
| FALSE {mkexpr (Expr_const (Const_bool false))}
132
| STRING {mkexpr (Expr_const (Const_string $1))}
133
/* Idents or type enum tags */
134
| IDENT {
135
  if Hashtbl.mem tag_table $1
136
  then mkexpr (Expr_const (Const_tag $1))
137
  else mkexpr (Expr_ident $1)}
138
| LPAR ANNOT expr RPAR
139
    {update_expr_annot $3 $2}
140
| LPAR expr RPAR
141
    {$2}
142
| LPAR tuple_expr RPAR
143
    {mkexpr (Expr_tuple (List.rev $2))}
144

    
145
/* Array expressions */
146
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
147
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
148
| expr LBRACKET dim_list { $3 $1 }
149

    
150
/* Temporal operators */
151
| PRE expr 
152
    {mkexpr (Expr_pre $2)}
153
| expr ARROW expr 
154
    {mkexpr (Expr_arrow ($1,$3))}
155
| expr FBY expr 
156
    {(*mkexpr (Expr_fby ($1,$3))*)
157
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
158
| expr WHEN IDENT 
159
    {mkexpr (Expr_when ($1,$3,tag_true))}
160
| expr WHENNOT IDENT
161
    {mkexpr (Expr_when ($1,$3,tag_false))}
162
| expr WHEN IDENT LPAR IDENT RPAR
163
    {mkexpr (Expr_when ($1, $5, $3))}
164
| MERGE IDENT handler_expr_list
165
    {mkexpr (Expr_merge ($2,$3))}
166

    
167
/* Applications */
168
| IDENT LPAR expr RPAR
169
    {mkexpr (Expr_appl ($1, $3, None))}
170
| IDENT LPAR expr RPAR EVERY IDENT
171
    {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}
172
| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR
173
    {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }
174
| IDENT LPAR tuple_expr RPAR
175
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
176
| IDENT LPAR tuple_expr RPAR EVERY IDENT
177
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }
178
| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR
179
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }
180

    
181
/* Boolean expr */
182
| expr AND expr 
183
    {mkpredef_call "&&" [$1;$3]}
184
| expr AMPERAMPER expr 
185
    {mkpredef_call "&&" [$1;$3]}
186
| expr OR expr 
187
    {mkpredef_call "||" [$1;$3]}
188
| expr BARBAR expr 
189
    {mkpredef_call "||" [$1;$3]}
190
| expr XOR expr 
191
    {mkpredef_call "xor" [$1;$3]}
192
| NOT expr 
193
    {mkpredef_unary_call "not" $2}
194
| expr IMPL expr 
195
    {mkpredef_call "impl" [$1;$3]}
196

    
197
/* Comparison expr */
198
| expr EQ expr 
199
    {mkpredef_call "=" [$1;$3]}
200
| expr LT expr 
201
    {mkpredef_call "<" [$1;$3]}
202
| expr LTE expr 
203
    {mkpredef_call "<=" [$1;$3]}
204
| expr GT expr 
205
    {mkpredef_call ">" [$1;$3]}
206
| expr GTE  expr 
207
    {mkpredef_call ">=" [$1;$3]}
208
| expr NEQ expr 
209
    {mkpredef_call "!=" [$1;$3]}
210

    
211
/* Arithmetic expr */
212
| expr PLUS expr 
213
    {mkpredef_call "+" [$1;$3]}
214
| expr MINUS expr 
215
    {mkpredef_call "-" [$1;$3]}
216
| expr MULT expr 
217
    {mkpredef_call "*" [$1;$3]}
218
| expr DIV expr 
219
    {mkpredef_call "/" [$1;$3]}
220
| MINUS expr %prec UMINUS
221
  {mkpredef_unary_call "uminus" $2}
222
| expr MOD expr 
223
    {mkpredef_call "mod" [$1;$3]}
224

    
225
/* If */
226
| IF expr THEN expr ELSE expr
227
    {mkexpr (Expr_ite ($2, $4, $6))}
228

    
229

    
230
handler_expr_list:
231
   { [] }
232
| handler_expr handler_expr_list { $1 :: $2 }
233

    
234
handler_expr:
235
 LPAR IDENT ARROW expr RPAR { ($2, $4) }
236

    
237
qexpr:
238
| expr { mkeexpr [] $1 }
239
  /* Quantifiers */
240
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eepxr (Exists, $2) $4 } 
241
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eepxr (Forall, $2) $4 }
242

    
243
vdecl:
244
| ident_list COL typ clock 
245
    {List.map mkvar_decl (List.map (fun id -> (id, $3, $4, false)) $1)}
246
| CONST ident_list COL typ clock 
247
    {List.map mkvar_decl (List.map (fun id -> (id, $4, $5, true)) $2)}
248

    
249

    
250
ident_list:
251
  IDENT {[$1]}
252
| ident_list COMMA IDENT {$3::$1}
253

    
254

    
255
typ:
256
    {mktyp Tydec_any}
257
| TINT {mktyp Tydec_int}
258
| IDENT {
259
  try 
260
    mktyp (Hashtbl.find Corelang.type_table (Tydec_const $1))
261
  with Not_found -> raise (Corelang.Error (Location.symbol_rloc(), Corelang.Unbound_symbol ("type " ^ $1)))
262
}
263
| TFLOAT {mktyp Tydec_float}
264
| TREAL {mktyp Tydec_real}
265
| TBOOL {mktyp Tydec_bool}
266
| TCLOCK {mktyp (Tydec_clock Tydec_bool) }
267
| typ POWER INT {mktyp Tydec_any (*(mktyptuple $3 $1)*)}
268
| typ POWER IDENT {mktyp Tydec_any (*(mktyptuple (try 
269
					match get_const $3 with Const_int i -> i with _ -> failwith "Const power error") $1)*)}
270

    
271
clock:
272
    {mkclock Ckdec_any}
273
| when_list
274
    {mkclock (Ckdec_bool (List.rev $1))}
275

    
276
when_cond:
277
    WHEN IDENT {($2, tag_true)}
278
| WHENNOT IDENT {($2, tag_false)}
279

    
280
when_list:
281
    when_cond {[$1]}
282
| when_list when_cond {$2::$1}
283

    
284

    
285
const:
286
| INT {Const_int $1}
287
| REAL {Const_real $1}
288
| FLOAT {Const_float $1}
289
| TRUE {Const_bool true}
290
| FALSE {Const_bool false}
291
| STRING {Const_string $1}
292

    
293
lustre_annot:
294
lustre_annot_list EOF { fun node_id -> $1 }
295

    
296
lustre_annot_list:
297
  { [] } 
298
| kwd COL expr SCOL lustre_annot_list { ($1,$3)::$5 }
299
| IDENT COL expr SCOL lustre_annot_list { ([$1],$3)::$5 }
300
| INVARIANT COL expr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
301
| OBSERVER COL expr SCOL lustre_annot_list { (["observer"],$3)::$5 }
302
| CCODE COL const lustre_annot_list{ (["c_code"],$3)::$5 }
303
| MATLAB COL const lustre_annot_list{ (["matlab"],$3)::$5 }
304

    
305
kwd:
306
DIV { [] }
307
| DIV IDENT kwd { $2::$3}