diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 6 | ||||
| -rw-r--r-- | src/ast_util.mli | 1 | ||||
| -rw-r--r-- | src/initial_check.ml | 17 | ||||
| -rw-r--r-- | src/parse_ast.ml | 4 | ||||
| -rw-r--r-- | src/parser.mly | 9 | ||||
| -rw-r--r-- | src/type_check.ml | 86 |
6 files changed, 85 insertions, 38 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 546faf14..2fb90b02 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -669,16 +669,16 @@ and string_of_pexp (Pat_aux (pexp, _)) = match pexp with | Pat_exp (pat, exp) -> string_of_pat pat ^ " -> " ^ string_of_exp exp | Pat_when (pat, guard, exp) -> string_of_pat pat ^ " when " ^ string_of_exp guard ^ " -> " ^ string_of_exp exp -and string_of_tpat = function +and string_of_typ_pat = function | TP_wild -> "_" | TP_var kid -> string_of_kid kid - | TP_app (f, tpats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_tpat tpats ^ ")" + | TP_app (f, tpats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_typ_pat tpats ^ ")" and string_of_pat (P_aux (pat, l)) = match pat with | P_lit lit -> string_of_lit lit | P_wild -> "_" | P_id v -> string_of_id v - | P_var (pat, tpat) -> string_of_pat pat ^ " as " ^ string_of_tpat tpat + | P_var (pat, tpat) -> string_of_pat pat ^ " as " ^ string_of_typ_pat tpat | 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 5ceb29f8..5d2b01b8 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -194,6 +194,7 @@ val string_of_order : order -> string val string_of_nexp : nexp -> string val string_of_typ : typ -> string val string_of_typ_arg : typ_arg -> string +val string_of_typ_pat : typ_pat -> string val string_of_annot : ('a * typ * effect) option -> string val string_of_n_constraint : n_constraint -> string val string_of_quant_item : quant_item -> string diff --git a/src/initial_check.ml b/src/initial_check.ml index 812bfaad..9516f53e 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -430,17 +430,26 @@ let to_ast_lit (Parse_ast.L_aux(lit,l)) : lit = | Parse_ast.L_bin(b) -> L_bin(b) | Parse_ast.L_real r -> L_real r | Parse_ast.L_string(s) -> L_string(s)) - ,l) - + ,l) + +let rec to_ast_typ_pat (Parse_ast.ATyp_aux (typ_aux, l)) = + match typ_aux with + | Parse_ast.ATyp_wild -> TP_wild + | Parse_ast.ATyp_var kid -> TP_var (to_ast_var kid) + | Parse_ast.ATyp_app (f, typs) -> + TP_app (to_ast_id f, List.map to_ast_typ_pat typs) + | _ -> typ_error l "Unexpected type in type pattern" None None None + let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pat,l) : Parse_ast.pat) : unit pat = P_aux( (match pat with | Parse_ast.P_lit(lit) -> P_lit(to_ast_lit lit) | Parse_ast.P_wild -> P_wild - | Parse_ast.P_as(pat,id) -> P_as(to_ast_pat k_env def_ord pat,to_ast_id id) + | Parse_ast.P_var (pat, Parse_ast.ATyp_aux (Parse_ast.ATyp_id 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 (pat,kid) -> P_var (to_ast_pat k_env def_ord pat, TP_var (to_ast_var kid)) + | Parse_ast.P_var (pat, typ) -> P_var (to_ast_pat k_env def_ord pat, to_ast_typ_pat typ) | Parse_ast.P_app(id,pats) -> if pats = [] then P_id (to_ast_id id) diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 5eb8038a..ba948040 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -150,6 +150,7 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_default_ord (* default order for increasing or decreasing signficant bits *) | ATyp_set of (base_effect) list (* effect set *) | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) + | ATyp_wild | ATyp_tup of (atyp) list (* Tuple type *) | ATyp_app of id * (atyp) list (* type constructor application *) | ATyp_exist of kid list * n_constraint * atyp @@ -239,10 +240,9 @@ type pat_aux = (* Pattern *) P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) - | P_as of pat * id (* named pattern *) | P_typ of atyp * pat (* typed pattern *) | P_id of id (* identifier *) - | P_var of pat * kid (* bind pat to type variable *) + | P_var of pat * atyp (* bind pat to type variable *) | 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/parser.mly b/src/parser.mly index 32ee3368..b781ea1f 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -512,6 +512,8 @@ typ9r: atomic_typ: | id { mk_typ (ATyp_id $1) $startpos $endpos } + | Under + { mk_typ ATyp_wild $startpos $endpos } | kid { mk_typ (ATyp_var $1) $startpos $endpos } | Num @@ -654,9 +656,7 @@ pat_concat: pat: | pat1 { $1 } - | pat1 As id - { mk_pat (P_as ($1, $3)) $startpos $endpos } - | pat1 As kid + | pat1 As typ { mk_pat (P_var ($1, $3)) $startpos $endpos } pat_list: @@ -673,7 +673,8 @@ atomic_pat: | id { mk_pat (P_id $1) $startpos $endpos } | kid - { mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos, $1)) $startpos $endpos } + { mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos, + mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos } | id Lparen pat_list Rparen { mk_pat (P_app ($1, $3)) $startpos $endpos } | atomic_pat Colon typ diff --git a/src/type_check.ml b/src/type_check.ml index 2fcfb309..4d599125 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1261,6 +1261,21 @@ let order_frees (Ord_aux (ord_aux, l)) = | Ord_var kid -> KidSet.singleton kid | _ -> KidSet.empty +let rec typ_nexps (Typ_aux (typ_aux, l)) = + match typ_aux with + | Typ_id v -> [] + | Typ_var kid -> [] + | Typ_tup typs -> List.concat (List.map typ_nexps typs) + | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args) + | Typ_exist (kids, nc, typ) -> typ_nexps typ + | Typ_fn (typ1, typ2, _) -> + typ_nexps typ1 @ typ_nexps typ2 +and typ_arg_nexps (Typ_arg_aux (typ_arg_aux, l)) = + match typ_arg_aux with + | Typ_arg_nexp n -> [n] + | Typ_arg_typ typ -> typ_nexps typ + | Typ_arg_order ord -> [] + let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) = match typ_aux with | Typ_id v -> KidSet.empty @@ -2372,40 +2387,36 @@ 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 (pat, TP_var kid) -> + | P_var (pat, typ_pat) -> let typ = Env.expand_synonyms env typ in - begin - match destruct_exist env typ, typ with - | Some ([kid'], nc, ex_typ), _ -> - let env = Env.add_typ_var kid BK_nat env in - let ex_typ = typ_subst_nexp kid' (Nexp_var kid) ex_typ in - let env = Env.add_constraint (nc_subst_nexp kid' (Nexp_var kid) nc) env in - let typed_pat, env, guards = bind_pat env pat ex_typ in - annot_pat (P_var (typed_pat, TP_var kid)) typ, env, guards - | Some _, _ -> typ_error l ("Cannot bind type variable pattern against multiple argument existential") - | None, Typ_aux (Typ_id id, _) when Id.compare id (mk_id "int") == 0 -> - let env = Env.add_typ_var kid BK_nat env in - let typed_pat, env, guards = bind_pat env pat (atom_typ (nvar kid)) in - annot_pat (P_var (typed_pat, TP_var kid)) typ, env, guards - | None, Typ_aux (Typ_id id, _) when Id.compare id (mk_id "nat") == 0 -> + let kid = Env.fresh_kid env in + let env, ex_typ = match destruct_exist env typ, typ with + | Some (kids, nc, ex_typ), _ -> + let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in + let env = Env.add_constraint nc env in + env, ex_typ + | None, Typ_aux (Typ_id id, _) when string_of_id id = "int" -> + Env.add_typ_var kid BK_nat env, atom_typ (nvar kid) + | None, Typ_aux (Typ_id id, _) when string_of_id id = "nat" -> let env = Env.add_typ_var kid BK_nat env in let env = Env.add_constraint (nc_gt (nvar kid) (nint 0)) env in - let typed_pat, env, guards = bind_pat env pat (atom_typ (nvar kid)) in - annot_pat (P_var (typed_pat, TP_var kid)) typ, env, guards + env, atom_typ (nvar kid) | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _) - when Id.compare id (mk_id "range") == 0 -> + when string_of_id id = "range" -> let env = Env.add_typ_var kid BK_nat env in - let env = Env.add_constraint (nc_and (nc_lteq lo (nvar kid)) (nc_lteq (nvar kid) hi)) env in - let typed_pat, env, guards = bind_pat env pat (atom_typ (nvar kid)) in - annot_pat (P_var (typed_pat, TP_var kid)) typ, env, guards + let env = Env.add_constraint (nc_lteq lo (nvar kid)) env in + let env = Env.add_constraint (nc_lteq (nvar kid) hi) env in + env, atom_typ (nvar kid) | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _)]), _) - when Id.compare id (mk_id "atom") == 0 -> + when string_of_id id = "atom" -> let env = Env.add_typ_var kid BK_nat env in let env = Env.add_constraint (nc_eq (nvar kid) n) env in - let typed_pat, env, guards = bind_pat env pat (atom_typ (nvar kid)) in - annot_pat (P_var (typed_pat, TP_var kid)) typ, env, guards + env, atom_typ (nvar kid) | None, _ -> typ_error l ("Cannot bind type variable against non existential or numeric type") - end + in + let env = bind_typ_pat l env typ_pat ex_typ in + let typed_pat, env, guards = bind_pat env pat ex_typ in + annot_pat (P_var (typed_pat, typ_pat)) typ, env, guards | P_wild -> annot_pat P_wild typ, env, [] | P_cons (hd_pat, tl_pat) -> begin @@ -2548,6 +2559,31 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = guards | _ -> typ_error l ("Couldn't infer type of pattern " ^ string_of_pat pat) +and bind_typ_pat l env typ_pat (Typ_aux (typ_aux, _) as typ) = + match typ_pat, typ_aux with + | TP_wild, _ -> env + | TP_var kid, _ -> + begin + match typ_nexps typ with + | [nexp] -> + Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var kid BK_nat env) + | [] -> + typ_error l ("No numeric expressions in " ^ string_of_typ typ ^ " to bind " ^ string_of_kid kid ^ " to") + | nexps -> + typ_error l ("Type " ^ string_of_typ typ ^ " has multiple numeric expressions. Cannot bind " ^ string_of_kid kid) + end + | TP_app (f1, tpats), Typ_app (f2, typs) when Id.compare f1 f2 = 0-> + List.fold_left2 (bind_typ_pat_arg l) env tpats typs + | _, _ -> typ_error l ("Couldn't bind type " ^ string_of_typ typ ^ " with " ^ string_of_typ_pat typ_pat) +and bind_typ_pat_arg l env typ_pat (Typ_arg_aux (typ_arg_aux, _) as typ_arg) = + match typ_pat, typ_arg_aux with + | TP_wild, _ -> env + | TP_var kid, Typ_arg_nexp nexp -> + Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var kid BK_nat env) + | _, Typ_arg_typ typ -> bind_typ_pat l env typ_pat typ + | _, Typ_arg_order _ -> typ_error l "Cannot bind type pattern against order" + | _, _ -> typ_error l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat) + and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as exp) = let annot_assign lexp exp = E_aux (E_assign (lexp, exp), (l, Some (env, mk_typ (Typ_id (mk_id "unit")), no_effect))) in let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in |