summaryrefslogtreecommitdiff
path: root/src/parser.mly
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser.mly')
-rw-r--r--src/parser.mly170
1 files changed, 98 insertions, 72 deletions
diff --git a/src/parser.mly b/src/parser.mly
index bd68cfdc..8e5023c8 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 Function_ If_ In IN Inc Let_ Member Nat Order
+%token Enumerate Else Exit Extern False Forall 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 Val
+%token Undefined Union With When Val Constraint
%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
@@ -150,7 +150,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
%token <string> Id TyVar TyId
%token <int> Num
-%token <string> String Bin Hex
+%token <string> String Bin Hex Real
%token <string> Amp At Carrot Div Eq Excl Gt Lt Plus Star Tilde
%token <string> AmpAmp CarrotCarrot Colon ColonColon EqEq ExclEq ExclExcl
@@ -209,6 +209,10 @@ id:
{ idl (DeIid($3)) }
| Lparen Deinfix Lt Rparen
{ idl (DeIid($3)) }
+ | Lparen Deinfix GtUnderS Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix LtUnderS Rparen
+ { idl (DeIid($3)) }
| Lparen Deinfix Minus Rparen
{ idl (DeIid("-")) }
| Lparen Deinfix MinusUnderS Rparen
@@ -226,7 +230,7 @@ id:
| Lparen Deinfix AmpAmp Rparen
{ idl (DeIid($3)) }
| Lparen Deinfix Bar Rparen
- { idl (DeIid("||")) }
+ { idl (DeIid("|")) }
| Lparen Deinfix BarBar Rparen
{ idl (DeIid("||")) }
| Lparen Deinfix CarrotCarrot Rparen
@@ -243,6 +247,8 @@ id:
{ idl (DeIid($3)) }
| Lparen Deinfix GtEq Rparen
{ idl (DeIid($3)) }
+ | Lparen Deinfix GtEqUnderS Rparen
+ { idl (DeIid($3)) }
| Lparen Deinfix GtEqPlus Rparen
{ idl (DeIid($3)) }
| Lparen Deinfix GtGt Rparen
@@ -257,6 +263,8 @@ id:
{ idl (DeIid($3)) }
| Lparen Deinfix LtEq Rparen
{ idl (DeIid($3)) }
+ | Lparen Deinfix LtEqUnderS Rparen
+ { idl (DeIid($3)) }
| Lparen Deinfix LtLt Rparen
{ idl (DeIid($3)) }
| Lparen Deinfix LtLtLt Rparen
@@ -283,6 +291,8 @@ atomic_kind:
{ bkloc BK_type }
| Nat
{ bkloc BK_nat }
+ | NatNum
+ { bkloc BK_nat }
| Order
{ bkloc BK_order }
| EFFECT
@@ -342,29 +352,7 @@ effect_typ:
| Pure
{ tloc (ATyp_set([])) }
-atomic_typ:
- | tid
- { tloc (ATyp_id $1) }
- | tyvar
- { tloc (ATyp_var $1) }
- | effect_typ
- { $1 }
- | Inc
- { tloc (ATyp_inc) }
- | Dec
- { tloc (ATyp_dec) }
- | SquareBar nexp_typ BarSquare
- { tloc (make_range_sugar $2) }
- | SquareBar nexp_typ Colon nexp_typ BarSquare
- { tloc (make_range_sugar_bounded $2 $4) }
- | SquareColon nexp_typ ColonSquare
- { tloc (make_atom_sugar $2) }
- | Lparen typ Rparen
- { $2 }
-
vec_typ:
- | atomic_typ
- { $1 }
| tid Lsquare nexp_typ Rsquare
{ tloc (make_vector_sugar false false (ATyp_aux ((ATyp_id $1), locn 1 1)) $3) }
| tid Lsquare nexp_typ Colon nexp_typ Rsquare
@@ -383,68 +371,75 @@ vec_typ:
{ tloc (make_vector_sugar_bounded true false "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
app_typs:
- | nexp_typ
+ | atomic_typ
{ [$1] }
- | nexp_typ Comma app_typs
+ | atomic_typ Comma app_typs
{ $1::$3 }
-app_typ:
+atomic_typ:
| vec_typ
{ $1 }
+ | range_typ
+ { $1 }
+ | nexp_typ
+ { $1 }
+ | Inc
+ { tloc (ATyp_inc) }
+ | Dec
+ { tloc (ATyp_dec) }
| tid Lt app_typs Gt
{ tloc (ATyp_app($1,$3)) }
| Register Lt app_typs Gt
{ tloc (ATyp_app(Id_aux(Id "register", locn 1 1),$3)) }
-app_num_typ:
- | app_typ
- { $1 }
- | Num
- { tloc (ATyp_constant $1) }
+range_typ:
+ | SquareBar nexp_typ BarSquare
+ { tloc (make_range_sugar $2) }
+ | SquareBar nexp_typ Colon nexp_typ BarSquare
+ { tloc (make_range_sugar_bounded $2 $4) }
+ | SquareColon nexp_typ ColonSquare
+ { tloc (make_atom_sugar $2) }
-star_typ:
- | app_num_typ
+nexp_typ:
+ | nexp_typ Plus nexp_typ2
+ { tloc (ATyp_sum ($1, $3)) }
+ | nexp_typ Minus nexp_typ2
+ { tloc (ATyp_minus ($1, $3)) }
+ | Minus nexp_typ2
+ { tloc (ATyp_neg $2) }
+ | nexp_typ2
{ $1 }
- | app_num_typ Star nexp_typ
- { tloc (ATyp_times ($1, $3)) }
-exp_typ:
- | star_typ
- { $1 }
- | TwoStarStar atomic_typ
- { tloc (ATyp_exp($2)) }
- | TwoStarStar Num
- { tloc (ATyp_exp (tloc (ATyp_constant $2))) }
+nexp_typ2:
+ | nexp_typ2 Star nexp_typ3
+ { tloc (ATyp_times ($1, $3)) }
+ | nexp_typ3
+ { $1 }
-nexp_typ:
- | exp_typ
+nexp_typ3:
+ | TwoStarStar nexp_typ4
+ { tloc (ATyp_exp $2) }
+ | nexp_typ4
{ $1 }
- | atomic_typ Plus nexp_typ
- { tloc (ATyp_sum($1,$3)) }
- | Lparen atomic_typ Plus nexp_typ Rparen
- { tloc (ATyp_sum($2,$4)) }
- | Num Plus nexp_typ
- { tloc (ATyp_sum((tlocl (ATyp_constant $1) 1 1),$3)) }
- | Lparen Num Plus nexp_typ Rparen
- { tloc (ATyp_sum((tlocl (ATyp_constant $2) 2 2),$4)) }
- | atomic_typ Minus nexp_typ
- { tloc (ATyp_minus($1,$3)) }
- | Lparen atomic_typ Minus nexp_typ Rparen
- { tloc (ATyp_minus($2,$4)) }
- | Num Minus nexp_typ
- { tloc (ATyp_minus((tlocl (ATyp_constant $1) 1 1),$3)) }
- | Lparen Num Minus nexp_typ Rparen
- { tloc (ATyp_minus((tlocl (ATyp_constant $2) 2 2),$4)) }
+nexp_typ4:
+ | Num
+ { tlocl (ATyp_constant $1) 1 1 }
+ | tid
+ { tloc (ATyp_id $1) }
+ | tyvar
+ { tloc (ATyp_var $1) }
+ | Lparen tup_typ Rparen
+ { $2 }
tup_typ_list:
- | app_typ Comma app_typ
+ | atomic_typ Comma atomic_typ
{ [$1;$3] }
- | app_typ Comma tup_typ_list
+ | atomic_typ Comma tup_typ_list
{ $1::$3 }
tup_typ:
- | app_typ
+ | atomic_typ
{ $1 }
| Lparen tup_typ_list Rparen
{ tloc (ATyp_tup $2) }
@@ -452,7 +447,7 @@ tup_typ:
typ:
| tup_typ
{ $1 }
- | tup_typ MinusGt typ Effect effect_typ
+ | tup_typ MinusGt tup_typ Effect effect_typ
{ tloc (ATyp_fn($1,$3,$5)) }
lit:
@@ -470,6 +465,8 @@ lit:
{ lloc (L_bin $1) }
| Hex
{ lloc (L_hex $1) }
+ | Real
+ { lloc (L_real $1) }
| Undefined
{ lloc L_undef }
| Bitzero
@@ -477,7 +474,6 @@ lit:
| Bitone
{ lloc L_one }
-
atomic_pat:
| lit
{ ploc (P_lit $1) }
@@ -485,8 +481,8 @@ atomic_pat:
{ ploc P_wild }
| Lparen pat As id Rparen
{ ploc (P_as($2,$4)) }
- | Lparen typ Rparen atomic_pat
- { ploc (P_typ($2,$4)) }
+ | Lparen tup_typ Rparen atomic_pat
+ { ploc (P_typ($2,$4)) }
| id
{ ploc (P_app($1,[])) }
| Lcurly fpats Rcurly
@@ -507,6 +503,8 @@ atomic_pat:
{ ploc (P_list([$2])) }
| SquareBarBar comma_pats BarBarSquare
{ ploc (P_list($2)) }
+ | atomic_pat ColonColon pat
+ { ploc (P_cons ($1, $3)) }
| Lparen pat Rparen
{ $2 }
@@ -569,7 +567,7 @@ atomic_exp:
{ eloc (E_lit($1)) }
| Lparen exp Rparen
{ $2 }
- | Lparen typ Rparen atomic_exp
+ | Lparen tup_typ Rparen atomic_exp
{ eloc (E_cast($2,$4)) }
| Lparen comma_exps Rparen
{ eloc (E_tuple($2)) }
@@ -597,6 +595,8 @@ atomic_exp:
{ eloc (E_case($2,$4)) }
| Sizeof atomic_typ
{ eloc (E_sizeof($2)) }
+ | Constraint Lparen nexp_constraint Rparen
+ { eloc (E_constraint $3) }
| Exit atomic_exp
{ eloc (E_exit $2) }
| Return atomic_exp
@@ -656,7 +656,7 @@ right_atomic_exp:
if $6 <> "to" && $6 <> "downto" then
raise (Parse_error_locn ((loc ()),"Missing \"to\" or \"downto\" in foreach loop"));
let step = eloc (E_lit(lloc (L_num 1))) in
- let ord =
+ let ord =
if $6 = "to"
then ATyp_aux(ATyp_inc,(locn 6 6))
else ATyp_aux(ATyp_dec,(locn 6 6)) in
@@ -970,6 +970,8 @@ case_exps:
patsexp:
| atomic_pat MinusGt exp
{ peloc (Pat_exp($1,$3)) }
+ | atomic_pat When exp MinusGt exp
+ { peloc (Pat_when ($1, $3, $5)) }
letbind:
| Let_ atomic_pat Eq exp
@@ -1023,6 +1025,10 @@ val_spec:
{ vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) }
| Val typ id
{ vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3)) }
+ | Val Cast typquant typ id
+ { vloc (VS_cast_spec (mk_typschm $3 $4 3 4,$5)) }
+ | Val Cast typ id
+ { vloc (VS_cast_spec (mk_typschm (mk_typqn ()) $3 3 3, $4)) }
| Val Extern typquant typ id
{ vloc (VS_extern_no_rename (mk_typschm $3 $4 3 4,$5)) }
| Val Extern typ id
@@ -1051,14 +1057,32 @@ nums:
{ $1::$3 }
nexp_constraint:
+ | nexp_constraint1
+ { $1 }
+ | nexp_constraint1 Bar nexp_constraint
+ { NC_aux (NC_or ($1, $3), loc ()) }
+
+nexp_constraint1:
+ | nexp_constraint2
+ { $1 }
+ | nexp_constraint2 Amp nexp_constraint1
+ { NC_aux (NC_and ($1, $3), loc ()) }
+
+nexp_constraint2:
| nexp_typ Eq nexp_typ
{ NC_aux(NC_fixed($1,$3), loc () ) }
+ | nexp_typ ExclEq nexp_typ
+ { NC_aux (NC_not_equal ($1, $3), loc ()) }
| nexp_typ GtEq nexp_typ
{ NC_aux(NC_bounded_ge($1,$3), loc () ) }
| nexp_typ LtEq nexp_typ
{ NC_aux(NC_bounded_le($1,$3), loc () ) }
+ | tyvar In Lcurly nums Rcurly
+ { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
| tyvar IN Lcurly nums Rcurly
{ NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
+ | Lparen nexp_constraint Rparen
+ { $2 }
id_constraint:
| nexp_constraint
@@ -1266,6 +1290,8 @@ def:
{ dloc (DEF_spec($1)) }
| default_typ
{ dloc (DEF_default($1)) }
+ | Overload id Lsquare enum_body Rsquare
+ { dloc (DEF_overload($2,$4)) }
| Register typ id
{ dloc (DEF_reg_dec(DEC_aux(DEC_reg($2,$3),loc ()))) }
| Register Alias id Eq exp
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 17:39:04 +0000