diff options
Diffstat (limited to 'src/parser.mly')
| -rw-r--r-- | src/parser.mly | 38 |
1 files changed, 31 insertions, 7 deletions
diff --git a/src/parser.mly b/src/parser.mly index 62a2c9f4..10241137 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -129,9 +129,9 @@ 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 Undefined Union With When Val Constraint Try Catch Throw %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,10 +497,12 @@ 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,[])) } + | tyvar + { ploc (P_var $1) } | Lcurly fpats Rcurly { ploc (P_record((fst $2, snd $2))) } | Lsquare comma_pats Rsquare @@ -569,7 +585,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)) } @@ -595,10 +611,14 @@ atomic_exp: { eloc (E_list($2)) } | Switch exp Lcurly case_exps Rcurly { eloc (E_case($2,$4)) } + | Try exp Catch Lcurly case_exps Rcurly + { eloc (E_try ($2, $5)) } | Sizeof atomic_typ { eloc (E_sizeof($2)) } | Constraint Lparen nexp_constraint Rparen { eloc (E_constraint $3) } + | Throw atomic_exp + { eloc (E_throw $2) } | Exit atomic_exp { eloc (E_exit $2) } | Return atomic_exp @@ -1083,6 +1103,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 } |