diff options
Diffstat (limited to 'src/parser.mly')
| -rw-r--r-- | src/parser.mly | 30 |
1 files changed, 24 insertions, 6 deletions
diff --git a/src/parser.mly b/src/parser.mly index 62a2c9f4..d6da6e63 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -129,7 +129,7 @@ let make_vector_sugar order_set is_inc typ typ1 = /*Terminals with no content*/ %token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Def Default Deinfix Effect EFFECT End -%token Enumerate Else Exit Extern False Forall Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast +%token Enumerate Else Exit Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast %token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef %token Undefined Union With When Val Constraint %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape @@ -286,6 +286,12 @@ tyvar: | TyVar { (Kid_aux((Var($1)),loc ())) } +tyvars: + | tyvar + { [$1] } + | tyvar tyvars + { $1 :: $2 } + atomic_kind: | TYPE { bkloc BK_type } @@ -431,7 +437,7 @@ nexp_typ4: { tloc (ATyp_id $2) } | tyvar { tloc (ATyp_var $1) } - | Lparen tup_typ Rparen + | Lparen exist_typ Rparen { $2 } tup_typ_list: @@ -446,10 +452,18 @@ tup_typ: | Lparen tup_typ_list Rparen { tloc (ATyp_tup $2) } -typ: +exist_typ: + | Exist tyvars Comma nexp_constraint Dot tup_typ + { tloc (ATyp_exist ($2, $4, $6)) } + | Exist tyvars Dot tup_typ + { tloc (ATyp_exist ($2, NC_aux (NC_true, loc ()), $4)) } | tup_typ { $1 } - | tup_typ MinusGt tup_typ Effect effect_typ + +typ: + | exist_typ + { $1 } + | tup_typ MinusGt exist_typ Effect effect_typ { tloc (ATyp_fn($1,$3,$5)) } lit: @@ -483,7 +497,7 @@ atomic_pat: { ploc P_wild } | Lparen pat As id Rparen { ploc (P_as($2,$4)) } - | Lparen tup_typ Rparen atomic_pat + | Lparen exist_typ Rparen atomic_pat { ploc (P_typ($2,$4)) } | id { ploc (P_app($1,[])) } @@ -569,7 +583,7 @@ atomic_exp: { eloc (E_lit($1)) } | Lparen exp Rparen { $2 } - | Lparen tup_typ Rparen atomic_exp + | Lparen exist_typ Rparen atomic_exp { eloc (E_cast($2,$4)) } | Lparen comma_exps Rparen { eloc (E_tuple($2)) } @@ -1083,6 +1097,10 @@ nexp_constraint2: { NC_aux(NC_nat_set_bounded($1,$4), loc ()) } | tyvar IN Lcurly nums Rcurly { NC_aux(NC_nat_set_bounded($1,$4), loc ()) } + | True + { NC_aux (NC_true, loc ()) } + | False + { NC_aux (NC_false, loc ()) } | Lparen nexp_constraint Rparen { $2 } |