Project

General

Profile

Revision 01c7d5e1 src/parserLustreSpec.mly

View differences:

src/parserLustreSpec.mly
3 3
  open Corelang
4 4
  open LustreSpec
5 5
  
6
  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

  
6 10
  let mkeexpr x = mkeexpr (Location.symbol_rloc ()) x
11
  (*
7 12
  let mkepredef_call x = mkepredef_call (Location.symbol_rloc ()) x
8 13
  let mkepredef_unary_call x = mkepredef_unary_call (Location.symbol_rloc ()) x
9
  
14
  *)
15

  
10 16
  let mktyp x = mktyp (Location.symbol_rloc ()) x
11 17
  let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x
12 18
  let mkclock x = mkclock (Location.symbol_rloc ()) x
......
71 77
 
72 78
requires:
73 79
{ [] }
74
| REQUIRES expr SCOL requires { $2::$4 }
80
| REQUIRES qexpr SCOL requires { $2::$4 }
75 81

  
76 82
ensures:
77 83
{ [] }
78
| ENSURES expr SCOL ensures { (EnsuresExpr $2) :: $4 }
79
| OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 }
84
| ENSURES qexpr SCOL ensures { (EnsuresExpr $2) :: $4 }
85
| OBSERVER IDENT LPAR tuple_qexpr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 }
80 86

  
81 87
behaviors:
82 88
{ [] }
......
84 90

  
85 91
assumes:
86 92
{ [] }
87
| ASSUMES expr SCOL assumes { $2::$4 } 
93
| ASSUMES qexpr SCOL assumes { $2::$4 } 
94

  
95
tuple_qexpr:
96
| qexpr COMMA qexpr {[$3;$1]}
97
| tuple_qexpr COMMA qexpr {$3::$1}
98

  
88 99

  
89 100
tuple_expr:
90
| expr COMMA expr {[$3;$1]}
101
    expr COMMA expr {[$3;$1]}
91 102
| tuple_expr COMMA expr {$3::$1}
92 103

  
104
// 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

  
93 113
expr:
94
| const {mkeexpr (EExpr_const $1)} 
95
| IDENT 
96
    {mkeexpr (EExpr_ident $1)}
114
/* 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}
97 125
| LPAR expr RPAR
98 126
    {$2}
99 127
| LPAR tuple_expr RPAR
100
    {mkeexpr (EExpr_tuple (List.rev $2))}
128
    {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)}
101 138
| expr ARROW expr 
102
    {mkeexpr (EExpr_arrow ($1,$3))}
139
    {mkexpr (Expr_arrow ($1,$3))}
103 140
| expr FBY expr 
104
    {mkeexpr (EExpr_fby ($1,$3))}
141
    {(*mkexpr (Expr_fby ($1,$3))*)
142
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
105 143
| 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))}
144
    {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 */
109 153
| IDENT LPAR expr RPAR
110
    {mkeexpr (EExpr_appl ($1, $3, None))}
154
    {mkexpr (Expr_appl ($1, $3, None))}
111 155
| IDENT LPAR expr RPAR EVERY IDENT
112
    {mkeexpr (EExpr_appl ($1, $3, Some $6))}
156
    {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))) }
113 159
| IDENT LPAR tuple_expr RPAR
114
    {mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), None))}
160
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
115 161
| IDENT LPAR tuple_expr RPAR EVERY IDENT
116
    {mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), Some $6)) }
162
    {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))) }
117 165

  
118 166
/* Boolean expr */
119 167
| expr AND expr 
120
    {mkepredef_call "&&" [$1;$3]}
168
    {mkpredef_call "&&" [$1;$3]}
121 169
| expr AMPERAMPER expr 
122
    {mkepredef_call "&&" [$1;$3]}
170
    {mkpredef_call "&&" [$1;$3]}
123 171
| expr OR expr 
124
    {mkepredef_call "||" [$1;$3]}
172
    {mkpredef_call "||" [$1;$3]}
125 173
| expr BARBAR expr 
126
    {mkepredef_call "||" [$1;$3]}
174
    {mkpredef_call "||" [$1;$3]}
127 175
| expr XOR expr 
128
    {mkepredef_call "xor" [$1;$3]}
176
    {mkpredef_call "xor" [$1;$3]}
129 177
| NOT expr 
130
    {mkepredef_unary_call "not" $2}
178
    {mkpredef_unary_call "not" $2}
131 179
| expr IMPL expr 
132
    {mkepredef_call "impl" [$1;$3]}
180
    {mkpredef_call "impl" [$1;$3]}
133 181

  
134 182
/* Comparison expr */
135 183
| expr EQ expr 
136
    {mkepredef_call "=" [$1;$3]}
184
    {mkpredef_call "=" [$1;$3]}
137 185
| expr LT expr 
138
    {mkepredef_call "<" [$1;$3]}
186
    {mkpredef_call "<" [$1;$3]}
139 187
| expr LTE expr 
140
    {mkepredef_call "<=" [$1;$3]}
188
    {mkpredef_call "<=" [$1;$3]}
141 189
| expr GT expr 
142
    {mkepredef_call ">" [$1;$3]}
190
    {mkpredef_call ">" [$1;$3]}
143 191
| expr GTE  expr 
144
    {mkepredef_call ">=" [$1;$3]}
192
    {mkpredef_call ">=" [$1;$3]}
145 193
| expr NEQ expr 
146
    {mkepredef_call "!=" [$1;$3]}
194
    {mkpredef_call "!=" [$1;$3]}
147 195

  
148 196
/* Arithmetic expr */
149 197
| expr PLUS expr 
150
    {mkepredef_call "+" [$1;$3]}
198
    {mkpredef_call "+" [$1;$3]}
151 199
| expr MINUS expr 
152
    {mkepredef_call "-" [$1;$3]}
200
    {mkpredef_call "-" [$1;$3]}
153 201
| expr MULT expr 
154
    {mkepredef_call "*" [$1;$3]}
202
    {mkpredef_call "*" [$1;$3]}
155 203
| expr DIV expr 
156
    {mkepredef_call "/" [$1;$3]}
204
    {mkpredef_call "/" [$1;$3]}
157 205
| MINUS expr %prec UMINUS
158
    {mkepredef_unary_call "uminus" $2}
206
  {mkpredef_unary_call "uminus" $2}
159 207
| expr MOD expr 
160
    {mkepredef_call "mod" [$1;$3]}
161

  
162
/* Temp op */
163
| PRE expr 
164
    {mkeexpr (EExpr_pre $2)}
208
    {mkpredef_call "mod" [$1;$3]}
165 209

  
166 210
/* If */
167 211
| IF expr THEN expr ELSE expr
168
    {mkepredef_call "ite" [$2;$4;$6]}
212
    {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) }
169 221

  
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))}
222
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 }
173 227

  
174 228
vdecl:
175 229
| ident_list COL typ clock 
......
214 268

  
215 269

  
216 270
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}
271
| 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}
223 277

  
224 278
lustre_annot:
225 279
lustre_annot_list EOF { $1 }

Also available in: Unified diff