summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/initial_check.ml5
-rw-r--r--src/lexer.mll7
-rw-r--r--src/parse_ast.ml1
-rw-r--r--src/parser.mly74
4 files changed, 66 insertions, 21 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index f98b11d8..897f3ec2 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -251,6 +251,11 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp)
let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in
let exist_typ = to_ast_typ k_env def_ord atyp in
Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ)
+ | Parse_ast.ATyp_with (atyp, nc) ->
+ let exist_typ = to_ast_typ k_env def_ord atyp in
+ let kids = KidSet.elements (tyvars_of_typ exist_typ) in
+ let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in
+ Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ)
| _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None
), l)
diff --git a/src/lexer.mll b/src/lexer.mll
index 8b229772..de8eed7f 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -97,8 +97,7 @@ let operators = ref
(List.fold_left
(fun r (x, y) -> M.add x y r)
M.empty
- [ ("==", mk_operator Infix 4 "==");
- ("/", mk_operator InfixL 7 "/");
+ [ ("/", mk_operator InfixL 7 "/");
("%", mk_operator InfixL 7 "%");
])
@@ -224,9 +223,7 @@ rule token = parse
| "," { Comma }
| ".." { DotDot }
| "." { Dot }
- | "==" as op
- { try M.find op !operators
- with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) }
+ | "==" { EqEq(r"==") }
| "=" { (Eq(r"=")) }
| ">" { (Gt(r">")) }
| "-" { Minus }
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index d19e85ed..30f87bc3 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -156,6 +156,7 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders
| ATyp_tup of (atyp) list (* Tuple type *)
| ATyp_app of id * (atyp) list (* type constructor application *)
| ATyp_exist of kid list * n_constraint * atyp
+ | ATyp_with of atyp * n_constraint
and atyp =
ATyp_aux of atyp_aux * l
diff --git a/src/parser.mly b/src/parser.mly
index bd7c2f62..12286e13 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -197,6 +197,7 @@ let rec desugar_rchain chain s e =
%token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit
%token <string> Colon ColonColon (* CaretCaret *) TildeTilde ExclEq
+%token <string> EqEq
%token <string> GtEq
%token <string> LtEq
@@ -260,6 +261,7 @@ id:
| Op Plus { mk_id (DeIid "+") $startpos $endpos }
| Op Minus { mk_id (DeIid "-") $startpos $endpos }
| Op Star { mk_id (DeIid "*") $startpos $endpos }
+ | Op EqEq { 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 }
@@ -337,9 +339,12 @@ atomic_nc:
{ mk_nc NC_true $startpos $endpos }
| False
{ mk_nc NC_false $startpos $endpos }
- | typ Eq typ
+ | typ0 Eq typ0
+ { Util.warn ("Deprecated syntax, use == instead at " ^ Reporting.loc_to_string (loc $startpos($2) $endpos($2)) ^ "\n");
+ mk_nc (NC_equal ($1, $3)) $startpos $endpos }
+ | typ0 EqEq typ0
{ mk_nc (NC_equal ($1, $3)) $startpos $endpos }
- | typ ExclEq typ
+ | typ0 ExclEq typ0
{ mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
| nc_lchain
{ desugar_lchain $1 $startpos $endpos }
@@ -350,6 +355,38 @@ atomic_nc:
| kid In Lcurly num_list Rcurly
{ mk_nc (NC_set ($1, $4)) $startpos $endpos }
+new_nc:
+ | new_nc Bar new_nc_and
+ { mk_nc (NC_or ($1, $3)) $startpos $endpos }
+ | nc_and
+ { $1 }
+
+new_nc_and:
+ | new_nc_and Amp new_atomic_nc
+ { mk_nc (NC_and ($1, $3)) $startpos $endpos }
+ | new_atomic_nc
+ { $1 }
+
+new_atomic_nc:
+ | Where id Lparen typ_list Rparen
+ { mk_nc (NC_app ($2, $4)) $startpos $endpos }
+ | True
+ { mk_nc NC_true $startpos $endpos }
+ | False
+ { mk_nc NC_false $startpos $endpos }
+ | typ0 EqEq typ0
+ { mk_nc (NC_equal ($1, $3)) $startpos $endpos }
+ | typ0 ExclEq typ0
+ { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
+ | nc_lchain
+ { desugar_lchain $1 $startpos $endpos }
+ | nc_rchain
+ { desugar_rchain $1 $startpos $endpos }
+ | Lparen new_nc Rparen
+ { $2 }
+ | kid In Lcurly num_list Rcurly
+ { mk_nc (NC_set ($1, $4)) $startpos $endpos }
+
num_list:
| Num
{ [$1] }
@@ -357,28 +394,30 @@ num_list:
{ $1 :: $3 }
nc_lchain:
- | typ LtEq typ
+ | typ0 LtEq typ0
{ [LC_nexp $1; LC_lteq; LC_nexp $3] }
- | typ Lt typ
+ | typ0 Lt typ0
{ [LC_nexp $1; LC_lt; LC_nexp $3] }
- | typ LtEq nc_lchain
+ | typ0 LtEq nc_lchain
{ LC_nexp $1 :: LC_lteq :: $3 }
- | typ Lt nc_lchain
+ | typ0 Lt nc_lchain
{ LC_nexp $1 :: LC_lt :: $3 }
nc_rchain:
- | typ GtEq typ
+ | typ0 GtEq typ0
{ [RC_nexp $1; RC_gteq; RC_nexp $3] }
- | typ Gt typ
+ | typ0 Gt typ0
{ [RC_nexp $1; RC_gt; RC_nexp $3] }
- | typ GtEq nc_rchain
+ | typ0 GtEq nc_rchain
{ RC_nexp $1 :: RC_gteq :: $3 }
- | typ Gt nc_rchain
+ | typ0 Gt nc_rchain
{ RC_nexp $1 :: RC_gt :: $3 }
typ:
| typ0
{ $1 }
+ | typ0 With new_nc
+ { mk_typ (ATyp_with ($1, $3)) $startpos $endpos }
/* The following implements all nine levels of user-defined precedence for
operators in types, with both left, right and non-associative operators */
@@ -677,8 +716,8 @@ pat_string_append:
pat1:
| atomic_pat
{ $1 }
- | atomic_pat Bar pat1
- { mk_pat (P_or ($1, $3)) $startpos $endpos }
+ (* | atomic_pat Bar pat1
+ { mk_pat (P_or ($1, $3)) $startpos $endpos } *)
| atomic_pat At pat_concat
{ mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
| atomic_pat ColonColon pat1
@@ -890,6 +929,7 @@ exp4:
| 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 }
+ | exp5 EqEq 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 }
@@ -1104,12 +1144,14 @@ funcl_patexp:
funcl_patexp_typ:
| pat Eq exp
{ (mk_pexp (Pat_exp ($1, $3)) $startpos $endpos, mk_tannotn) }
- | pat MinusGt funcl_typ Eq exp
- { (mk_pexp (Pat_exp ($1, $5)) $startpos $endpos, $3) }
+ | pat MinusGt typ Eq exp
+ { (mk_pexp (Pat_exp ($1, $5)) $startpos $endpos, mk_tannot mk_typqn $3 $startpos $endpos($3)) }
+ | Forall typquant Dot pat MinusGt typ Eq exp
+ { (mk_pexp (Pat_exp ($4, $8)) $startpos $endpos, mk_tannot $2 $6 $startpos $endpos($6)) }
| Lparen pat If_ exp Rparen Eq exp
{ (mk_pexp (Pat_when ($2, $4, $7)) $startpos $endpos, mk_tannotn) }
- | Lparen pat If_ exp Rparen MinusGt funcl_typ Eq exp
- { (mk_pexp (Pat_when ($2, $4, $9)) $startpos $endpos, $7) }
+ | Forall typquant Dot Lparen pat If_ exp Rparen MinusGt typ Eq exp
+ { (mk_pexp (Pat_when ($5, $7, $12)) $startpos $endpos, mk_tannot $2 $10 $startpos $endpos($10)) }
funcl:
| id funcl_patexp
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 04:57:13 +0000