summaryrefslogtreecommitdiff
path: root/src/parser2.mly
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser2.mly')
-rw-r--r--src/parser2.mly154
1 files changed, 126 insertions, 28 deletions
diff --git a/src/parser2.mly b/src/parser2.mly
index 02a8f09c..e6c63196 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -46,11 +46,14 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *)
open Parse_ast
-let loc n m = Range (m, n)
+let loc n m = Range (n, m)
-let mk_id i n m = Id_aux (i, loc m n)
+let mk_id i n m = Id_aux (i, loc n m)
let mk_kid str n m = Kid_aux (Var str, loc n m)
+let id_of_kid = function
+ | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
+
let deinfix (Id_aux (Id v, l)) = Id_aux (DeIid v, l)
let mk_effect e n m = BE_aux (e, loc n m)
@@ -121,21 +124,19 @@ let rec desugar_rchain chain s e =
/*Terminals with no content*/
-%token And As Assert Bitzero Bitone Bits By Match Clause Const Dec Def Default Effect EFFECT End Op
-%token Enum Else Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Int Order Cast
-%token Pure Rec Register Return Scattered Sizeof Struct Then True TwoCaret Type TYPE Typedef
-%token Undefined Union With Val Constraint Throw Try Catch
+%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
+%token Enum Else False Forall Foreach Overload Function_ If_ In Inc Let_ Int Order Cast
+%token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
+%token Undefined Union With Val Constraint Throw Try Catch Exit
%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
+%token Repeat Until While Do
%nonassoc Then
%nonassoc Else
-%token Div_ Mod ModUnderS Quot Rem QuotUnderS
-
%token Bar Comma Dot Eof Minus Semi Under DotDot
%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar
-%token BarBar BarSquare BarBarSquare ColonEq ColonGt ColonSquare
-%token MinusGt LtBar LtColon SquareBar SquareBarBar
+%token MinusGt
/*Terminals with content*/
@@ -143,15 +144,17 @@ let rec desugar_rchain chain s e =
%token <int> Num
%token <string> String Bin Hex Real
-%token <string> Amp At Caret Div Eq Excl Gt Lt Plus Star EqGt Unit
+%token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit
%token <string> Colon ExclEq
-%token <string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt
-%token <string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar
+%token <string> GtEq
+%token <string> LtEq
%token <string> Op0 Op1 Op2 Op3 Op4 Op5 Op6 Op7 Op8 Op9
%token <string> Op0l Op1l Op2l Op3l Op4l Op5l Op6l Op7l Op8l Op9l
%token <string> Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r
+%token <Parse_ast.fixity_token> Fixity
+
%start file
%start typschm_eof
%type <Parse_ast.typschm> typschm_eof
@@ -198,6 +201,14 @@ id:
| Op Plus { mk_id (DeIid "+") $startpos $endpos }
| Op Minus { mk_id (DeIid "-") $startpos $endpos }
| Op Star { mk_id (DeIid "*") $startpos $endpos }
+ | Op ExclEq { mk_id (DeIid "!=") $startpos $endpos }
+ | Op Lt { mk_id (DeIid "<") $startpos $endpos }
+ | Op Gt { mk_id (DeIid ">") $startpos $endpos }
+ | Op LtEq { mk_id (DeIid "<=") $startpos $endpos }
+ | Op GtEq { mk_id (DeIid ">=") $startpos $endpos }
+ | Op Amp { mk_id (DeIid "&") $startpos $endpos }
+ | Op Bar { mk_id (DeIid "|") $startpos $endpos }
+ | Op Caret { mk_id (DeIid "^") $startpos $endpos }
op0: Op0 { mk_id (Id $1) $startpos $endpos }
op1: Op1 { mk_id (Id $1) $startpos $endpos }
@@ -266,7 +277,7 @@ atomic_nc:
| False
{ mk_nc NC_false $startpos $endpos }
| typ Eq typ
- { mk_nc (NC_fixed ($1, $3)) $startpos $endpos }
+ { mk_nc (NC_equal ($1, $3)) $startpos $endpos }
| typ ExclEq typ
{ mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
| nc_lchain
@@ -276,7 +287,7 @@ atomic_nc:
| Lparen nc Rparen
{ $2 }
| kid In Lcurly num_list Rcurly
- { mk_nc (NC_nat_set_bounded ($1, $4)) $startpos $endpos }
+ { mk_nc (NC_set ($1, $4)) $startpos $endpos }
num_list:
| Num
@@ -434,16 +445,19 @@ typ8:
| typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
| typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
| TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+ | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
| typ9 { $1 }
typ8l:
| typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
| typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
| TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+ | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
| typ9 { $1 }
typ8r:
| typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
| typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
| TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+ | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
| typ9 { $1 }
typ9:
@@ -481,7 +495,7 @@ atomic_typ:
{ let v = mk_kid "n" $startpos $endpos in
let atom_id = mk_id (Id "atom") $startpos $endpos in
let atom_of_v = mk_typ (ATyp_app (atom_id, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in
- mk_typ (ATyp_exist ([v], NC_aux (NC_nat_set_bounded (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
+ mk_typ (ATyp_exist ([v], NC_aux (NC_set (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
| Lcurly kid_list Dot typ Rcurly
{ mk_typ (ATyp_exist ($2, NC_aux (NC_true, loc $startpos $endpos), $4)) $startpos $endpos }
| Lcurly kid_list Comma nc Dot typ Rcurly
@@ -582,13 +596,25 @@ typschm_eof:
| typschm Eof
{ $1 }
-pat:
+pat1:
| atomic_pat
{ $1 }
- | atomic_pat As id
+ | atomic_pat At pat_concat
+ { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
+
+pat_concat:
+ | atomic_pat
+ { [$1] }
+ | atomic_pat At pat_concat
+ { $1 :: $3 }
+
+pat:
+ | pat1
+ { $1 }
+ | pat1 As id
{ mk_pat (P_as ($1, $3)) $startpos $endpos }
- | Lparen pat Comma pat_list Rparen
- { mk_pat (P_tup ($2 :: $4)) $startpos $endpos }
+ | pat1 As kid
+ { mk_pat (P_var ($1, $3)) $startpos $endpos }
pat_list:
| pat
@@ -604,13 +630,17 @@ atomic_pat:
| id
{ mk_pat (P_id $1) $startpos $endpos }
| kid
- { mk_pat (P_var $1) $startpos $endpos }
+ { mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos, $1)) $startpos $endpos }
| id Lparen pat_list Rparen
{ mk_pat (P_app ($1, $3)) $startpos $endpos }
- | pat Colon typ
+ | atomic_pat Colon typ
{ mk_pat (P_typ ($3, $1)) $startpos $endpos }
| Lparen pat Rparen
{ $2 }
+ | Lparen pat Comma pat_list Rparen
+ { mk_pat (P_tup ($2 :: $4)) $startpos $endpos }
+ | Lsquare pat_list Rsquare
+ { mk_pat (P_vector $2) $startpos $endpos }
lit:
| True
@@ -633,6 +663,8 @@ lit:
{ mk_lit (L_hex $1) $startpos $endpos }
| String
{ mk_lit (L_string $1) $startpos $endpos }
+ | Real
+ { mk_lit (L_real $1) $startpos $endpos }
exp:
| exp0
@@ -655,8 +687,39 @@ exp:
{ mk_exp (E_case ($2, $4)) $startpos $endpos }
| Try exp Catch Lcurly case_list Rcurly
{ mk_exp (E_try ($2, $5)) $startpos $endpos }
- | Lparen exp0 Comma exp_list Rparen
- { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos }
+ | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp In typ Rparen exp
+ { if $4 <> "from" then
+ raise (Parse_error_locn (loc $startpos $endpos,"Missing \"from\" in foreach loop"));
+ if $6 <> "to" then
+ raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" in foreach loop"));
+ mk_exp (E_for ($3, $5, $7, $9, $11, $13)) $startpos $endpos }
+ | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp Rparen exp
+ { if $4 <> "from" then
+ raise (Parse_error_locn (loc $startpos $endpos,"Missing \"from\" in foreach loop"));
+ if $6 <> "to" && $6 <> "downto" then
+ raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" or \"downto\" in foreach loop"));
+ let order =
+ if $6 = "to"
+ then ATyp_aux(ATyp_inc,loc $startpos($6) $endpos($6))
+ else ATyp_aux(ATyp_dec,loc $startpos($6) $endpos($6))
+ in
+ mk_exp (E_for ($3, $5, $7, $9, order, $11)) $startpos $endpos }
+ | Foreach Lparen id Id atomic_exp Id atomic_exp Rparen exp
+ { if $4 <> "from" then
+ raise (Parse_error_locn (loc $startpos $endpos,"Missing \"from\" in foreach loop"));
+ if $6 <> "to" && $6 <> "downto" then
+ raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" or \"downto\" in foreach loop"));
+ let step = mk_lit_exp (L_num 1) $startpos $endpos in
+ let ord =
+ if $6 = "to"
+ then ATyp_aux(ATyp_inc,loc $startpos($6) $endpos($6))
+ else ATyp_aux(ATyp_dec,loc $startpos($6) $endpos($6))
+ in
+ mk_exp (E_for ($3, $5, $7, step, ord, $9)) $startpos $endpos }
+ | Repeat exp Until exp
+ { mk_exp (E_loop (Until, $4, $2)) $startpos $endpos }
+ | While exp Do exp
+ { mk_exp (E_loop (While, $2, $4)) $startpos $endpos }
/* The following implements all nine levels of user-defined precedence for
operators in expressions, with both left, right and non-associative operators */
@@ -693,6 +756,7 @@ exp2:
| exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp2l op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp3 { $1 }
exp2l:
| exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
@@ -701,12 +765,14 @@ exp2l:
exp2r:
| exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp3 { $1 }
exp3:
| exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp3l op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp4 { $1 }
exp3l:
| exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
@@ -715,10 +781,16 @@ exp3l:
exp3r:
| exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp4 { $1 }
exp4:
| exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp5 Lt exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+ | exp5 Gt exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+ | exp5 LtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+ | exp5 GtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+ | exp5 ExclEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "!=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp5 { $1 }
@@ -785,6 +857,7 @@ exp8:
| exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp8l op8l exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp9 op8r exp8r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp9 Caret exp8r { mk_exp (E_app_infix ($1, mk_id (Id "^") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos }
| exp9 { $1 }
exp8l:
@@ -795,6 +868,7 @@ exp8l:
exp8r:
| exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp9 op8r exp8r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp9 Caret exp8r { mk_exp (E_app_infix ($1, mk_id (Id "^") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos }
| exp9 { $1 }
@@ -836,13 +910,15 @@ block:
%inline letbind:
| pat Eq exp
- { LB_aux (LB_val_implicit ($1, $3), loc $startpos $endpos) }
+ { LB_aux (LB_val ($1, $3), loc $startpos $endpos) }
atomic_exp:
| atomic_exp Colon atomic_typ
{ mk_exp (E_cast ($3, $1)) $startpos $endpos }
| lit
{ mk_exp (E_lit $1) $startpos $endpos }
+ | atomic_exp Dot id
+ { mk_exp (E_field ($1, $3)) $startpos $endpos }
| id
{ mk_exp (E_id $1) $startpos $endpos }
| kid
@@ -851,10 +927,14 @@ atomic_exp:
{ mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
| id Lparen exp_list Rparen
{ mk_exp (E_app ($1, $3)) $startpos $endpos }
+ | Exit Lparen exp Rparen
+ { mk_exp (E_exit $3) $startpos $endpos }
| Sizeof Lparen typ Rparen
{ mk_exp (E_sizeof $3) $startpos $endpos }
| Constraint Lparen nc Rparen
{ mk_exp (E_constraint $3) $startpos $endpos }
+ | Assert Lparen exp Rparen
+ { mk_exp (E_assert ($3, mk_lit_exp (L_string "") $startpos($4) $endpos($4))) $startpos $endpos }
| Assert Lparen exp Comma exp Rparen
{ mk_exp (E_assert ($3, $5)) $startpos $endpos }
| atomic_exp Lsquare exp Rsquare
@@ -869,6 +949,8 @@ atomic_exp:
{ mk_exp (E_vector_update_subrange ($2, $4, $6, $8)) $startpos $endpos }
| Lparen exp Rparen
{ $2 }
+ | Lparen exp Comma exp_list Rparen
+ { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos }
exp_list:
| exp
@@ -880,11 +962,19 @@ funcl:
| id pat Eq exp
{ mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos }
+funcls:
+ | id pat Eq exp
+ { [mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos] }
+ | id pat Eq exp And funcls
+ { mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos :: $6 }
+
type_def:
| Typedef id typquant Eq typ
{ mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm $3 $5 $startpos($3) $endpos)) $startpos $endpos }
| Typedef id Eq typ
{ mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm mk_typqn $4 $startpos($4) $endpos)) $startpos $endpos }
+ | Struct id Eq Lcurly struct_fields Rcurly
+ { mk_td (TD_record ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
| Struct id typquant Eq Lcurly struct_fields Rcurly
{ mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
| Enum id Eq enum_bar
@@ -933,8 +1023,8 @@ type_unions:
{ $1 :: $3 }
fun_def:
- | Function_ funcl
- { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, [$2])) $startpos $endpos }
+ | Function_ funcls
+ { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos }
let_def:
| Let_ letbind
@@ -942,7 +1032,13 @@ let_def:
val_spec_def:
| Val id Colon typschm
- { mk_vs (VS_val_spec ($4, $2)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($4, $2, None, false)) $startpos $endpos }
+ | Val Cast id Colon typschm
+ { mk_vs (VS_val_spec ($5, $3, None, true)) $startpos $endpos }
+ | Val id Eq String Colon typschm
+ { mk_vs (VS_val_spec ($6, $2, Some $4, false)) $startpos $endpos }
+ | Val Cast id Eq String Colon typschm
+ { mk_vs (VS_val_spec ($7, $3, Some $5, true)) $startpos $endpos }
register_def:
| Register id Colon typ
@@ -965,6 +1061,8 @@ scattered_def:
def:
| fun_def
{ DEF_fundef $1 }
+ | Fixity
+ { let (prec, n, op) = $1 in DEF_fixity (prec, n, Id_aux (Id op, loc $startpos $endpos)) }
| val_spec_def
{ DEF_spec $1 }
| type_def
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 17:46:32 +0000