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