Parsing a bit corrected...
This commit is contained in:
parent
bb9d96e79d
commit
14f3c57d6a
|
@ -88,8 +88,22 @@ open Hept_parsetree
|
||||||
%%
|
%%
|
||||||
|
|
||||||
/** Tools **/
|
/** Tools **/
|
||||||
%inline slist(S, x) : l=separated_list(S, x) {l}
|
|
||||||
%inline snlist(S, x) : l=separated_nonempty_list(S, x) {l}
|
/* Separated list */
|
||||||
|
slist(S, x) :
|
||||||
|
| {[]}
|
||||||
|
| x=x {[x]}
|
||||||
|
| x=x S r=slist(S,x) {x::r}
|
||||||
|
/*Separated Nonempty list */
|
||||||
|
snlist(S, x) :
|
||||||
|
| x=x {[x]}
|
||||||
|
| x=x S r=snlist(S,x) {x::r}
|
||||||
|
/*Option Separated Nonempty list*/
|
||||||
|
optsnlist(S,x) :
|
||||||
|
| x=x {[x]}
|
||||||
|
| x=x S {[x]}
|
||||||
|
| x=x S r=optsnlist(S,x) {x::r}
|
||||||
|
|
||||||
%inline tuple(x) : LPAREN h=x COMMA t=snlist(COMMA,x) RPAREN { h::t }
|
%inline tuple(x) : LPAREN h=x COMMA t=snlist(COMMA,x) RPAREN { h::t }
|
||||||
%inline soption(P,x):
|
%inline soption(P,x):
|
||||||
|/* empty */ { None }
|
|/* empty */ { None }
|
||||||
|
@ -220,11 +234,11 @@ node_params:
|
||||||
|
|
||||||
contract:
|
contract:
|
||||||
| /* empty */ {None}
|
| /* empty */ {None}
|
||||||
| CONTRACT b=block(LET) TEL? opt_assume opt_enforce opt_with
|
| CONTRACT b=block(LET) TEL a=opt_assume e=opt_enforce w=opt_with
|
||||||
{ Some{ c_block = b;
|
{ Some{ c_block = b;
|
||||||
c_assume = $4;
|
c_assume = a;
|
||||||
c_enforce = $5;
|
c_enforce = e;
|
||||||
c_controllables = $6 } }
|
c_controllables = w } }
|
||||||
;
|
;
|
||||||
|
|
||||||
opt_assume:
|
opt_assume:
|
||||||
|
@ -242,9 +256,9 @@ opt_with:
|
||||||
| WITH LPAREN params RPAREN { $3 }
|
| WITH LPAREN params RPAREN { $3 }
|
||||||
;
|
;
|
||||||
|
|
||||||
loc_vars:
|
loc_vars(S):
|
||||||
| /* empty */ { [] }
|
| /* empty */ { [] }
|
||||||
| VAR loc_params { $2 }
|
| VAR loc_params S { $2 }
|
||||||
;
|
;
|
||||||
|
|
||||||
loc_params:
|
loc_params:
|
||||||
|
@ -275,28 +289,25 @@ ty_ident:
|
||||||
;
|
;
|
||||||
|
|
||||||
equs:
|
equs:
|
||||||
| /* empty */ { [] }
|
| /* empty */ { [] }
|
||||||
| non_empty_equs opt_semi { List.rev $1 }
|
| eqs=optsnlist(SEMICOL,equ) { eqs }
|
||||||
;
|
;
|
||||||
|
|
||||||
non_empty_equs:
|
|
||||||
| equ { [$1] }
|
|
||||||
| non_empty_equs SEMICOL equ {$3 :: $1}
|
|
||||||
;
|
|
||||||
|
|
||||||
opt_semi:
|
|
||||||
| {}
|
|
||||||
| SEMICOL {}
|
|
||||||
;
|
|
||||||
|
|
||||||
opt_bar:
|
opt_bar:
|
||||||
| {}
|
| {}
|
||||||
| BAR {}
|
| BAR {}
|
||||||
;
|
;
|
||||||
|
|
||||||
block(S):
|
/* delimited block */
|
||||||
| l=loc_vars S eq=equs { mk_block l eq (Loc($startpos,$endpos)) }
|
block(S) :
|
||||||
| l=loc_vars { mk_block l [] (Loc($startpos,$endpos)) }
|
| VAR l=loc_params S eq=equs { mk_block l eq (Loc($startpos,$endpos)) }
|
||||||
|
| S eq=equs { mk_block [] eq (Loc($startpos,$endpos)) }
|
||||||
|
|
||||||
|
/* separated block */
|
||||||
|
sblock(S) :
|
||||||
|
| VAR l=loc_params S eq=equs { mk_block l eq (Loc($startpos,$endpos)) }
|
||||||
|
| eq=equs { mk_block [] eq (Loc($startpos,$endpos)) }
|
||||||
|
|
||||||
equ: eq=_equ { mk_equation eq (Loc($startpos,$endpos)) }
|
equ: eq=_equ { mk_equation eq (Loc($startpos,$endpos)) }
|
||||||
_equ:
|
_equ:
|
||||||
|
@ -307,15 +318,15 @@ _equ:
|
||||||
{ Eswitch($2, List.rev $4) }
|
{ Eswitch($2, List.rev $4) }
|
||||||
| PRESENT opt_bar present_handlers END
|
| PRESENT opt_bar present_handlers END
|
||||||
{ Epresent(List.rev $3, mk_block [] [] (Loc($startpos,$endpos))) }
|
{ Epresent(List.rev $3, mk_block [] [] (Loc($startpos,$endpos))) }
|
||||||
| PRESENT opt_bar present_handlers DEFAULT b=block(DO) END
|
| PRESENT opt_bar present_handlers DEFAULT DO b=sblock(IN) END
|
||||||
{ Epresent(List.rev $3, b) }
|
{ Epresent(List.rev $3, b) }
|
||||||
| IF exp THEN tb=block(DO) ELSE fb=block(DO) END
|
| IF exp THEN tb=sblock(IN) ELSE fb=sblock(IN) END
|
||||||
{ Eswitch($2,
|
{ Eswitch($2,
|
||||||
[{ w_name = ptrue; w_block = tb };
|
[{ w_name = ptrue; w_block = tb };
|
||||||
{ w_name = pfalse; w_block = fb }]) }
|
{ w_name = pfalse; w_block = fb }]) }
|
||||||
| RESET b=block(IN) EVERY e=exp
|
| RESET b=sblock(IN) EVERY e=exp
|
||||||
{ Ereset(b,e) }
|
{ Ereset(b,e) }
|
||||||
| DO b=block(IN) DONE
|
| DO b=sblock(IN) DONE
|
||||||
{ Eblock b }
|
{ Eblock b }
|
||||||
;
|
;
|
||||||
|
|
||||||
|
@ -374,8 +385,8 @@ switch_handlers:
|
||||||
;
|
;
|
||||||
|
|
||||||
present_handler:
|
present_handler:
|
||||||
| exp b=block(DO)
|
| e=exp b=block(DO)
|
||||||
{ { p_cond = $1; p_block = b } }
|
{ { p_cond = e; p_block = b } }
|
||||||
;
|
;
|
||||||
|
|
||||||
present_handlers:
|
present_handlers:
|
||||||
|
|
Loading…
Reference in a new issue