Project

General

Profile

Revision a0b18d45 src/parser_lustre.mly

View differences:

src/parser_lustre.mly
84 84
%token EXISTS FORALL
85 85
%token PROTOTYPE LIB
86 86
%token EOF
87
%token END
87 88

  
88 89
%nonassoc prec_exists prec_forall
89 90
/* unused precedence rules*/
......
116 117
%nonassoc RBRACKET
117 118
%nonassoc LBRACKET
118 119

  
119
%start prog
120
%type <Lustre_types.top_decl list> prog
120
/* these XXX_main rules are used to avoid end-of-stream conflicts with
121
   menhir. See http://gallium.inria.fr/~fpottier/menhir/manual.html#sec43
122
*/
123
%start prog_main %type <Lustre_types.top_decl list>
124
prog_main
121 125

  
122
%start header
123
%type <Lustre_types.top_decl list> header
126
%start header_main
127
%type <Lustre_types.top_decl list> header_main
124 128

  
125
%start lustre_annot
126
%type <Lustre_types.expr_annot> lustre_annot
129
%start lustre_annot_main
130
%type <Lustre_types.expr_annot> lustre_annot_main
127 131

  
128
%start lustre_spec
129
%type <Lustre_types.contract_desc> lustre_spec
132
%start lustre_spec_main
133
%type <Lustre_types.contract_desc> lustre_spec_main
130 134

  
131
%start signed_const
132
%type <Lustre_types.constant> signed_const
135
%start signed_const_main
136
%type <Lustre_types.constant> signed_const_main
133 137

  
134
%start expr
135
%type <Lustre_types.expr> expr
138
%start expr_main
139
%type <Lustre_types.expr> expr_main
136 140

  
137
%start stmt_list
138
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list
141
%start stmt_list_main
142
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list_main
139 143

  
140
%start vdecl_list
141
%type <Lustre_types.var_decl list> vdecl_list
144
%start vdecl_list_main
145
%type <Lustre_types.var_decl list> vdecl_list_main
142 146
%%
143 147

  
144 148
module_ident:
......
168 172
type_ident:
169 173
  IDENT { $1 }
170 174

  
175
prog_main:
176
  | e = prog END { e }
177

  
171 178
prog:
172 179
 open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) }
173 180

  
174 181
typ_def_prog:
175 182
 typ_def_list { $1 false }
176 183

  
184
header_main:
185
  | e = header END { e }
186

  
177 187
header:
178 188
 open_list typ_def_header top_decl_header_list EOF { $1 @ $2 @ (List.rev $3) }
179 189

  
......
299 309
field_list:                           { [] }
300 310
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
301 311

  
312
stmt_list_main:
313
| e = stmt_list END { e }
314

  
302 315
stmt_list:
303 316
  { [], [], [] }
304 317
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}
......
339 352
       ident_list      EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)}
340 353
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
341 354

  
355
lustre_spec_main:
356
  | e = lustre_spec END { e }
357

  
342 358
lustre_spec:
343
| contract EOF { $1 }
359
  | contract EOF { $1 }
344 360

  
345 361
contract:
346 362
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
......
390 406
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
391 407
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
392 408

  
409
expr_main:
410
  | e = expr END { e }
411

  
393 412
expr:
394 413
/* constants */
395 414
  INT {mkexpr (Expr_const (Const_int $1))}
......
521 540
| IDENT EQ signed_const { [ ($1, $3) ] }
522 541
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
523 542

  
543
signed_const_main:
544
  | e = signed_const END { e }
545

  
524 546
signed_const:
525 547
  INT {Const_int $1}
526 548
| REAL {let c,e,s =$1 in Const_real (c,e,s)}
......
587 609
  {[]}
588 610
| VAR local_vdecl_list SCOL {$2}
589 611

  
612
vdecl_list_main:
613
  | e = vdecl_list END { e }
614

  
590 615
vdecl_list:
591 616
  vdecl {$1}
592 617
| vdecl_list SCOL vdecl {$3 @ $1}
......
650 675
SCOL_opt:
651 676
    SCOL {} | {}
652 677

  
678
lustre_annot_main:
679
  | e = lustre_annot END { e }
653 680

  
654 681
lustre_annot:
655 682
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }

Also available in: Unified diff