Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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}