summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast.ml1
-rw-r--r--src/ast_util.ml5
-rw-r--r--src/ast_util.mli2
-rw-r--r--src/initial_check.ml1
-rw-r--r--src/lexer2.mll4
-rw-r--r--src/parse_ast.ml1
-rw-r--r--src/parser2.mly11
-rw-r--r--src/type_check.ml20
8 files changed, 42 insertions, 3 deletions
diff --git a/src/ast.ml b/src/ast.ml
index 45428fed..710e8067 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -260,6 +260,7 @@ type
| P_as of 'a pat * id (* named pattern *)
| P_typ of typ * 'a pat (* typed pattern *)
| P_id of id (* identifier *)
+ | P_var of kid (* bind identifier and type variable *)
| P_app of id * ('a pat) list (* union constructor pattern *)
| P_record of ('a fpat) list * bool (* struct pattern *)
| P_vector of ('a pat) list (* vector pattern *)
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 0c6461d1..ddd83429 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -112,6 +112,7 @@ and map_pat_annot_aux f = function
| P_as (pat, id) -> P_as (map_pat_annot f pat, id)
| P_typ (typ, pat) -> P_typ (typ, map_pat_annot f pat)
| P_id id -> P_id id
+ | P_var kid -> P_var kid
| P_app (id, pats) -> P_app (id, List.map (map_pat_annot f) pats)
| P_record (fpats, b) -> P_record (List.map (map_fpat_annot f) fpats, b)
| P_tup pats -> P_tup (List.map (map_pat_annot f) pats)
@@ -145,6 +146,9 @@ let string_of_id = function
| Id_aux (Id v, _) -> v
| Id_aux (DeIid v, _) -> "(deinfix " ^ v ^ ")"
+let id_of_kid = function
+ | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
+
let string_of_kid = function
| Kid_aux (Var v, _) -> v
@@ -313,6 +317,7 @@ and string_of_pat (P_aux (pat, l)) =
| P_lit lit -> string_of_lit lit
| P_wild -> "_"
| P_id v -> string_of_id v
+ | P_var kid -> string_of_kid kid
| P_typ (typ, pat) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_pat pat
| P_tup pats -> "(" ^ string_of_list ", " string_of_pat pats ^ ")"
| P_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_pat pats ^ ")"
diff --git a/src/ast_util.mli b/src/ast_util.mli
index ae340839..94f3f0cc 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -86,6 +86,8 @@ val string_of_index_range : index_range -> string
val id_of_fundef : 'a fundef -> id
+val id_of_kid : kid -> id
+
module Id : sig
type t = id
val compare : id -> id -> int
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 357ed100..e5717389 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -415,6 +415,7 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa
| Parse_ast.P_as(pat,id) -> P_as(to_ast_pat k_env def_ord pat,to_ast_id id)
| Parse_ast.P_typ(typ,pat) -> P_typ(to_ast_typ k_env def_ord typ,to_ast_pat k_env def_ord pat)
| Parse_ast.P_id(id) -> P_id(to_ast_id id)
+ | Parse_ast.P_var kid -> P_var (to_ast_var kid)
| Parse_ast.P_app(id,pats) ->
if pats = []
then P_id (to_ast_id id)
diff --git a/src/lexer2.mll b/src/lexer2.mll
index 4f4a8be2..f5350ea8 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -192,7 +192,6 @@ rule token = parse
token lexbuf }
| "&" { (Amp(r"&")) }
| "@" { (At "@") }
- | "|" { Bar }
| "2" ws "^" { TwoCaret }
| "^" { (Caret(r"^")) }
| ":" { Colon(r ":") }
@@ -207,6 +206,9 @@ rule token = parse
| ";" { Semi }
| "*" { (Star(r"*")) }
| "_" { Under }
+ | "{|" { LcurlyBar }
+ | "|}" { RcurlyBar }
+ | "|" { Bar }
| "{" { Lcurly }
| "}" { Rcurly }
| "()" { Unit(r"()") }
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 54feaf29..3951ab51 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -234,6 +234,7 @@ pat_aux = (* Pattern *)
| P_as of pat * id (* named pattern *)
| P_typ of atyp * pat (* typed pattern *)
| P_id of id (* identifier *)
+ | P_var of kid
| P_app of id * (pat) list (* union constructor pattern *)
| P_record of (fpat) list * bool (* struct pattern *)
| P_vector of (pat) list (* vector pattern *)
diff --git a/src/parser2.mly b/src/parser2.mly
index 9ce947be..bde542e0 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -133,7 +133,7 @@ let rec desugar_rchain chain s e =
%token Div_ Mod ModUnderS Quot Rem QuotUnderS
%token Bar Comma Dot Eof Minus Semi Under DotDot
-%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare
+%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar
%token BarBar BarSquare BarBarSquare ColonEq ColonGt ColonSquare
%token MinusGt LtBar LtColon SquareBar SquareBarBar
@@ -484,6 +484,11 @@ atomic_typ:
{ $2 }
| Lparen typ Comma typ_list Rparen
{ mk_typ (ATyp_tup ($2 :: $4)) $startpos $endpos }
+ | LcurlyBar num_list RcurlyBar
+ { 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 }
| 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
@@ -603,6 +608,10 @@ atomic_pat:
{ mk_pat (P_lit $1) $startpos $endpos }
| id
{ mk_pat (P_id $1) $startpos $endpos }
+ | kid
+ { mk_pat (P_var $1) $startpos $endpos }
+ | tydecl typ
+ { mk_pat (P_typ ($2, mk_pat (P_var $1) $startpos $endpos($1))) $startpos $endpos }
| id Lparen pat_list Rparen
{ mk_pat (P_app ($1, $3)) $startpos $endpos }
| pat Colon typ
diff --git a/src/type_check.ml b/src/type_check.ml
index 8a7983ce..ec0b4a58 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -811,7 +811,7 @@ end = struct
then typ_error (kid_loc kid) ("Kind identifier " ^ string_of_kid kid ^ " is already bound")
else
begin
- typ_debug ("Adding kind identifier binding " ^ string_of_kid kid ^ " :: " ^ string_of_base_kind_aux k);
+ typ_print ("Adding kind identifier " ^ string_of_kid kid ^ " :: " ^ string_of_base_kind_aux k);
{ env with typ_vars = KBindings.add kid k env.typ_vars }
end
@@ -2064,6 +2064,23 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
| Unification_error (l, m) -> typ_error l ("Unification error when pattern matching against union constructor: " ^ m)
end
end
+ | P_var kid ->
+ begin
+ let v = id_of_kid kid in
+ match Env.lookup_id v env with
+ | Local (Immutable, _) | Unbound ->
+ begin
+ match destruct_exist env typ with
+ | Some ([kid'], nc, typ) ->
+ let env = Env.add_typ_var kid BK_nat env in
+ let env = Env.add_constraint (nc_subst_nexp kid' (Nexp_var kid) nc) env in
+ let env = Env.add_local v (Immutable, typ_subst_nexp kid' (Nexp_var kid) typ) env in
+ annot_pat (P_var kid) typ, env
+ | Some _ -> typ_error l ("Cannot bind type variable pattern against multiple argument existential")
+ | None _ -> typ_error l ("Cannot bind type variable against non existential type")
+ end
+ | _ -> typ_error l ("Bad type identifer pattern: " ^ string_of_pat pat)
+ end
| P_wild -> annot_pat P_wild typ, env
| P_cons (hd_pat, tl_pat) ->
begin
@@ -2829,6 +2846,7 @@ and propagate_pat_effect_aux = function
let p_pat = propagate_pat_effect pat in
P_typ (typ, p_pat), effect_of_pat p_pat
| P_id id -> P_id id, no_effect
+ | P_var kid -> P_var kid, no_effect
| P_app (id, pats) ->
let p_pats = List.map propagate_pat_effect pats in
P_app (id, p_pats), collect_effects_pat p_pats
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 09:02:07 +0000