Revision 01c7d5e1 src/parserLustreSpec.mly
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