From 2dc5974592c78dd870a4c3bfc6cc9acd7f05d400 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Tue, 18 Feb 2020 14:34:45 +0200 Subject: [PATCH] Separate matching from subtyping like in F-ing modules to allow RDS --- elab.ml | 21 +++--- regression.1ml | 3 + sub.ml | 178 ++++++++++++++++++++++++++++++++++++++----------- sub.mli | 10 ++- types.mli | 1 + 5 files changed, 163 insertions(+), 50 deletions(-) diff --git a/elab.ml b/elab.ml index 72a3ba0e..74b47a90 100644 --- a/elab.ml +++ b/elab.ml @@ -266,11 +266,11 @@ Trace.debug (lazy ("[AndT] ti = " ^ string_of_norm_typ ti)); let aksi = List.filter (fun (a, k) -> VarSet.mem a vi) aks1 in Trace.debug (lazy ("[AndT] aksi = " ^ string_of_norm_extyp (ExT(aksi, StrT [])))); let aks = aks1 @ aks2 in - let ts, zs3, _ = + let su, zs3, _ = try sub_typ (add_typs aks env) t2 ti (varTs aksi) with Sub e -> error typ.at ("type refinement does not match: " ^ Sub.string_of_error e) in -Trace.debug (lazy ("[AndT] ts = " ^ String.concat ", " (List.map string_of_norm_typ ts))); - let t = merge_typs (subst_typ (subst (Lib.List.take (List.length ts) aksi) ts) t1) t2 in +Trace.debug (lazy ("[AndT] su = " ^ string_of_match su)); + let t = merge_typs (subst_typ (subst_of_match su) t1) t2 in Trace.debug (lazy ("[AndT] t = " ^ string_of_norm_typ t)); let vt = vars_typ t in let s = ExT(List.filter (fun (a, k) -> VarSet.mem a vt) aks, t) in @@ -489,16 +489,17 @@ Trace.debug (lazy ("[AppE] tf = " ^ string_of_norm_typ tf)); let t2 = lookup_var env var2 in Trace.debug (lazy ("[AppE] s1 = " ^ string_of_norm_extyp (ExT(aks1, t1)))); Trace.debug (lazy ("[AppE] t2 = " ^ string_of_norm_typ t2)); - let ts, zs3, f = + let su, zs3, f = try sub_typ env t2 t1 (varTs aks1) with Sub e -> error var2.at ("argument type does not match function: " ^ Sub.string_of_error e) in -Trace.debug (lazy ("[AppE] ts = " ^ String.concat ", " (List.map string_of_norm_typ ts))); +Trace.debug (lazy ("[AppE] su = " ^ string_of_match su)); let ExT(aks2, t2) = s in let aks2' = freshen_vars env (rename_vars (prepend_path l) aks2) in let s' = ExT(aks2', subst_typ (subst aks2 (varTs aks2')) t2) in - subst_extyp (subst aks1 ts) s', p, zs1 @ zs @ zs3, - IL.AppE(IL.instE(ex1, List.map erase_typ ts), IL.AppE(f, IL.VarE(var2.it))) + subst_extyp (subst_of_match su) s', p, zs1 @ zs @ zs3, + IL.AppE(IL.instE(ex1, List.map (fun (_, t) -> erase_typ t) su), + IL.AppE(f, IL.VarE(var2.it))) | EL.UnwrapE(var, typ) -> let aks, t, s2, zs2 = @@ -561,16 +562,16 @@ Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2)); let t2, zs2 = elab_pathexp env1 exp1 l in Trace.debug (lazy ("[RecT] s1 = " ^ string_of_norm_extyp s1)); Trace.debug (lazy ("[RecT] t2 = " ^ string_of_norm_typ t2)); - let ts, zs3, e = + let su, zs3, e = try sub_typ env1 t2 t1 (varTs aks1) with Sub e -> error typ.at ("recursive type does not match annotation: " ^ Sub.string_of_error e) in -Trace.debug (lazy ("[RecT] ts = " ^ String.concat ", " (List.map string_of_norm_typ ts))); +Trace.debug (lazy ("[RecT] su = " ^ string_of_match su)); let t3, k3 = try make_rec_typ t1 with Recursive -> error typ.at "illegal type for recursive expression" in let a = freshen_var env var.it in let tas1 = paths_typ (VarT(a, k3)) (varTs aks1) t1 in - let t3' = subst_typ (subst aks1 tas1) (subst_typ (subst aks1 ts) t3) in + let t3' = subst_typ (subst aks1 tas1) (subst_typ (subst_of_match su) t3) in let t4 = RecT((a, k3), t3') in Trace.debug (lazy ("[RecT] t4 = " ^ string_of_norm_typ t4)); let t = subst_typ (subst aks1 (List.map (subst_typ [a, t4]) tas1)) t1 in diff --git a/regression.1ml b/regression.1ml index fc997330..faf00c09 100644 --- a/regression.1ml +++ b/regression.1ml @@ -182,6 +182,9 @@ And = { type RDS = {A: {type t}, B: {type t}} & {A: {type t}, B: {v: A.t}} & {B: {type t}, A: {v: B.t}} + + do {A = {t = bool, v = 1}, B = {t = int, v = true}} :> RDS + do {A = {t = bool, v = 1}, B = {t = int, v = true}} : RDS } ;; diff --git a/sub.ml b/sub.ml index d26abcfc..22e6318f 100644 --- a/sub.ml +++ b/sub.ml @@ -165,32 +165,58 @@ let unify_typ t1 t2 = Trace.sub (lazy ("[unify_typ] t2 = " ^ string_of_norm_typ t2)); unify_typ t1 t2 -let rec psubst p t = +let rec psubst (p, t) = match p with | VarT(a, k) -> a, t - | AppT(p', ts) -> psubst p' (LamT(List.map unvarT ts, t)) + | AppT(p', ts) -> psubst (p', LamT(List.map unvarT ts, t)) | _ -> assert false +let rec var_of = function + | VarT(a, _) -> a + | AppT(p', _) -> var_of p' + | _ -> assert false + +let subst_of_match su = List.map (fun (p, t) -> var_of p, t) su + +let string_of_match su = + su + |> List.map (fun (p, t) -> + string_of_norm_typ t ^ " / " ^ string_of_norm_typ p) + |> String.concat ", " + let rec sub_typ infer_binds env t1 t2 ps = Trace.sub (lazy ("[sub_typ] t1 = " ^ string_of_norm_typ t1)); Trace.sub (lazy ("[sub_typ] t2 = " ^ string_of_norm_typ t2)); Trace.sub (lazy ("[sub_typ] ps = " ^ String.concat ", " (List.map string_of_norm_typ ps))); + let su', zs', t2, ps = + if ps <> [] then + let su, zs' = match_typ infer_binds env t1 t2 ps in + Trace.sub (lazy ("[sub_typ] su = " ^ string_of_match su)); + let t2 = subst_typ (List.map psubst su) t2 in + let ps = List.filter (fun p -> not (List.mem_assoc p su)) ps in + if ps <> [] then + Trace.sub (lazy ("[sub_typ] unmatched ps = " ^ + String.concat ", " (List.map string_of_norm_typ ps))); + su, zs', t2, ps + else + [], [], t2, ps + in let e1 = IL.VarE("x") in - let ts, zs, e = + let su, zs, e = match norm_typ t1, freshen_typ env (norm_typ t2) with | t1, FunT(aks21, t21, ExT(aks22, t22), Implicit) -> assert (aks22 = []); - let ts, zs, f = sub_typ infer_binds (add_typs aks21 env) t1 t22 ps in - List.map (fun t -> LamT(aks21, t)) ts, lift env zs, + let su, zs, f = sub_typ infer_binds (add_typs aks21 env) t1 t22 ps in + List.map (fun (p, t) -> (p, LamT(aks21, t))) su, lift env zs, IL.genE(erase_bind aks21, (IL.LamE("y", erase_typ t21, IL.AppE(f, e1)))) | FunT(aks11, t11, ExT(aks12, t12), Implicit), t2 -> assert (aks12 = []); let ts1, zs1 = guess_typs (Env.domain_typ env) aks11 in let t1' = subst_typ (subst aks11 ts1) t12 in - let ts2, zs2, f = sub_typ infer_binds env t1' t2 ps in - ts2, zs1 @ zs2, + let su, zs2, f = sub_typ infer_binds env t1' t2 ps in + su, zs1 @ zs2, IL.AppE(f, IL.AppE(IL.instE(e1, List.map erase_typ ts1), materialize_typ (subst_typ (subst aks11 ts1) t11))) @@ -199,15 +225,15 @@ let rec sub_typ infer_binds env t1 t2 ps = | ExT(aks1, t), ExT([], p1), p2::ps' when p1 = p2 -> if aks1 <> [] || not (!undecidable_flag || is_small_typ t) then raise (Sub (Mismatch (t1, t2))); - [t], [], e1 + [(p1, t)], [], e1 | _ -> let zs = try equal_extyp env s1 s2 with Sub e -> raise (Sub (Type e)) in [], zs, e1 ) | StrT(tr1), StrT(tr2) -> - let ts, zs, fs = sub_row infer_binds env tr1 tr2 ps in - ts, zs, + let su, zs, fs = sub_row infer_binds env tr1 tr2 ps in + su, zs, IL.TupE(List.map2 (fun (l, _) f -> l, f l e1) tr2 fs) | TupT(tr1), TupT(tr2) -> @@ -217,17 +243,18 @@ let rec sub_typ infer_binds env t1 t2 ps = | FunT(aks1, t11, s1, Explicit p1), FunT(aks2, t21, s2, Explicit p2) -> if p1 = Impure && p2 = Pure then raise (Sub (FunEffect(p1, p2))); let env' = add_typs aks2 env in - let ts1, zs1, f1 = + let su1, zs1, f1 = try sub_typ infer_binds env' t21 t11 (varTs aks1) with Sub e -> raise (Sub (FunParam e)) in let ps' = List.map (fun p -> AppT(p, varTs aks2)) ps in - let ts2, zs2, f2 = - try sub_extyp infer_binds env' (subst_extyp (subst aks1 ts1) s1) s2 ps' + let su2, zs2, f2 = + try sub_extyp infer_binds env' (subst_extyp (subst_of_match su1) s1) s2 ps' with Sub e -> raise (Sub (FunResult e)) in - List.map (fun t -> LamT(aks2, t)) ts2, lift env (zs1 @ zs2), + List.map (fun (p, t) -> (p, LamT(aks2, t))) su2, lift env (zs1 @ zs2), IL.genE(erase_bind aks2, (IL.LamE("y", erase_typ t21, - IL.AppE(f2, IL.AppE(IL.instE(e1, List.map erase_typ ts1), - IL.AppE(f1, IL.VarE("y"))))))) + IL.AppE(f2, + IL.AppE(IL.instE(e1, List.map (fun (_, t) -> erase_typ t) su1), + IL.AppE(f1, IL.VarE("y"))))))) | WrapT(s1), WrapT(s2) -> let _, zs, f = @@ -274,26 +301,26 @@ let rec sub_typ infer_binds env t1 t2 ps = | InferT(z) as t1, (TypT(_) as t2) -> let t11, zs1 = guess_typ (Env.domain_typ env) BaseK in let t1' = TypT(ExT([], t11)) in - let ts, zs2, f = sub_typ infer_binds env t1' t2 ps in + let su, zs2, f = sub_typ infer_binds env t1' t2 ps in if not (resolve_typ z t1') then raise (Sub (Mismatch(t1, t2))); - ts, zs1 @ zs2, IL.AppE(f, e1) + su, zs1 @ zs2, IL.AppE(f, e1) | InferT(z) as t1, (StrT(tr2) as t2) -> (* TODO: row polymorphism *) let tzsr = map_row (fun _ -> guess_typ (Env.domain_typ env) BaseK) tr2 in let t1' = StrT(map_row fst tzsr) in let zs1 = List.concat (List.map snd (List.map snd tzsr)) in - let ts, zs2, f = sub_typ infer_binds env t1' t2 ps in + let su, zs2, f = sub_typ infer_binds env t1' t2 ps in if not (resolve_typ z t1') then raise (Sub (Mismatch(t1, t2))); - ts, zs1 @ zs2, IL.AppE(f, e1) + su, zs1 @ zs2, IL.AppE(f, e1) | InferT(z) as t1, (FunT([], t21, ExT([], t22), Explicit Impure) as t2) -> let t11, zs1 = guess_typ (Env.domain_typ env) BaseK in let t12, zs2 = guess_typ (Env.domain_typ env) BaseK in let t1' = FunT([], t11, ExT([], t12), Explicit Impure) in - let ts, zs3, f = sub_typ infer_binds env t1' t2 ps in + let su, zs3, f = sub_typ infer_binds env t1' t2 ps in if not (resolve_typ z t1') then raise (Sub (Mismatch(t1, t2))); - ts, zs1 @ zs2 @ zs3, IL.AppE(f, e1) + su, zs1 @ zs2 @ zs3, IL.AppE(f, e1) | InferT(z) as t1, t2 -> if not (resolve_typ z t2) then raise (Sub (Mismatch(t1, t2))); @@ -302,26 +329,26 @@ let rec sub_typ infer_binds env t1 t2 ps = | TypT(_) as t1, (InferT(z) as t2) -> let t21, zs1 = guess_typ (Env.domain_typ env) BaseK in let t2' = TypT(ExT([], t21)) in - let ts, zs2, f = sub_typ infer_binds env t1 t2' ps in + let su, zs2, f = sub_typ infer_binds env t1 t2' ps in if not (resolve_typ z t2') then raise (Sub (Mismatch(t1, t2))); - ts, zs1 @ zs2, IL.AppE(f, e1) + su, zs1 @ zs2, IL.AppE(f, e1) | StrT(tr1) as t1, (InferT(z) as t2) -> (* TODO: row polymorphism *) let tzsr = map_row (fun _ -> guess_typ (Env.domain_typ env) BaseK) tr1 in let t2' = StrT(map_row fst tzsr) in let zs1 = List.concat (List.map snd (List.map snd tzsr)) in - let ts, zs2, f = sub_typ infer_binds env t1 t2' ps in + let su, zs2, f = sub_typ infer_binds env t1 t2' ps in if not (resolve_typ z t2') then raise (Sub (Mismatch(t1, t2))); - ts, zs1 @ zs2, IL.AppE(f, e1) + su, zs1 @ zs2, IL.AppE(f, e1) | FunT([], t11, ExT([], t12), Explicit p) as t1, (InferT(z) as t2) -> let t21, zs1 = guess_typ (Env.domain_typ env) BaseK in let t22, zs2 = guess_typ (Env.domain_typ env) BaseK in let t2' = FunT([], t21, ExT([], t22), Explicit Impure) in - let ts, zs3, f = sub_typ infer_binds env t1 t2' ps in + let su, zs3, f = sub_typ infer_binds env t1 t2' ps in if not (resolve_typ z t2') then raise (Sub (Mismatch(t1, t2))); - ts, zs1 @ zs2 @ zs3, IL.AppE(f, e1) + su, zs1 @ zs2 @ zs3, IL.AppE(f, e1) | t1, (InferT(z) as t2) -> if not (resolve_typ z t1) then raise (Sub (Mismatch(t1, t2))); @@ -332,12 +359,12 @@ let rec sub_typ infer_binds env t1 t2 ps = | _ -> raise (Sub (Mismatch(t1, t2))) in + let su = su' @ su in Trace.sub (lazy ("[sub_typ] done t1 = " ^ string_of_norm_typ t1)); Trace.sub (lazy ("[sub_typ] done t2 = " ^ string_of_norm_typ t2)); - Trace.sub (lazy ("[sub_typ] done ts = " ^ - String.concat ", " (List.map string_of_norm_typ ts))); + Trace.sub (lazy ("[sub_typ] done su = " ^ string_of_match su)); Trace.sub (lazy ("[sub_typ] done x -> " ^ IL.string_of_exp e)); - ts, zs, IL.LamE("x", erase_typ t1, e) + su, zs' @ zs, IL.LamE("x", erase_typ t1, e) and sub_extyp infer_binds env s1 s2 ps = Trace.sub (lazy ("[sub_extyp] s1 = " ^ string_of_norm_extyp s1)); @@ -348,12 +375,12 @@ and sub_extyp infer_binds env s1 s2 ps = | [], [] -> sub_typ infer_binds env t1 t2 ps | _ -> - let ts, zs, f = + let su, zs, f = sub_typ infer_binds (add_typs aks1 env) t1 t2 (varTs aks2) in [], lift env zs, IL.LamE("x", erase_extyp s1, IL.openE(IL.VarE("x"), List.map fst aks1, "y", - IL.packE(List.map erase_typ ts, + IL.packE(List.map (fun (_, t) -> erase_typ t) su, IL.AppE(f, IL.VarE("y")), erase_extyp s2))) and sub_row infer_binds env tr1 tr2 ps = @@ -363,13 +390,13 @@ and sub_row infer_binds env tr1 tr2 ps = | (l, t2)::tr2' -> Trace.sub (lazy ("[sub_row] l = " ^ l)); let t1, zs, app = extract_bind infer_binds env tr1 l t2 in - let ts1, zs1, f = + let su1, zs1, f = try sub_typ infer_binds env t1 t2 ps with | Sub e -> raise (Sub (Struct(l, e))) in - let su = List.map2 psubst (Lib.List.take (List.length ts1) ps) ts1 in - let ps' = Lib.List.drop (List.length ts1) ps in - let ts2, zs2, fs = sub_row infer_binds env tr1 (subst_row su tr2') ps' in - ts1 @ ts2, zs @ zs1 @ zs2, app f::fs + let ps = List.filter (fun p -> List.mem_assoc p su1) ps in + let su2, zs2, fs = + sub_row infer_binds env tr1 (subst_row (subst_of_match su1) tr2') ps in + su1 @ su2, zs @ zs1 @ zs2, app f::fs and equal_typ env t1 t2 = Trace.sub (lazy ("[equal_typ] t1 = " ^ string_of_norm_typ t1)); @@ -396,5 +423,80 @@ and equal_row env tr1 tr2 ps = try sub_row false env tr2 tr1 ps with Sub e -> raise (Sub (Right e)) in zs1 @ zs2 +and match_typ infer_binds env t1 t2 ps = + let t2 = norm_typ t2 in + Trace.sub (lazy ("[match_typ] t1 = " ^ string_of_norm_typ t1)); + Trace.sub (lazy ("[match_typ] t2 = " ^ string_of_typ t2)); + Trace.sub (lazy ("[match_typ] ps = " ^ + String.concat ", " (List.map string_of_norm_typ ps))); + if not (has_typs t2) then [], [] else + match norm_typ t1, freshen_typ env t2 with + | t1, FunT(aks21, t21, ExT(aks22, t22), Implicit) -> + assert (aks22 = []); + let su, zs = match_typ infer_binds (add_typs aks21 env) t1 t22 ps in + List.map (fun (p, t) -> (p, LamT(aks21, t))) su, lift env zs + + | FunT(aks11, t11, ExT(aks12, t12), Implicit), t2 -> + assert (aks12 = []); + let ts1, zs1 = guess_typs (Env.domain_typ env) aks11 in + let t1' = subst_typ (subst aks11 ts1) t12 in + let su, zs2 = match_typ infer_binds env t1' t2 ps in + su, zs1 @ zs2 + + | TypT(s1), TypT(s2) -> + (match s1, s2 with + | ExT(aks1, t), ExT([], p) when List.mem p ps -> + if aks1 <> [] || not (!undecidable_flag || is_small_typ t) then + raise (Sub (Mismatch (t1, t2))); + [(p, t)], [] + | _ -> + [], []) + + | StrT(tr1), StrT(tr2) -> + match_row infer_binds env tr1 tr2 ps + + | FunT(aks1, t11, s1, Explicit p1), FunT(aks2, t21, s2, Explicit p2) -> + if p1 = Impure && p2 = Pure then raise (Sub (FunEffect(p1, p2))); + if p1 <> Pure || p2 <> Pure then + [], [] + else + let env' = add_typs aks2 env in + let su1, zs1, f1 = + try sub_typ infer_binds env' t21 t11 (varTs aks1) with Sub e -> + raise (Sub (FunParam e)) in + let ps' = List.map (fun p -> AppT(p, varTs aks2)) ps in + let su, zs2 = + try match_extyp + infer_binds env' (subst_extyp (subst_of_match su1) s1) s2 ps' + with Sub e -> raise (Sub (FunResult e)) in + List.map (function (AppT(p, _), t) -> (p, LamT(aks2, t)) + | _ -> assert false) su, lift env (zs1 @ zs2) + + | _ -> + [], [] + +and match_extyp infer_binds env s1 s2 ps = + let ExT(aks2, t2) = freshen_extyp env s2 in + let ExT(aks1, t1) = freshen_extyp (add_typs aks2 env) s1 in + match aks1, aks2 with + | [], [] -> + match_typ infer_binds env t1 t2 ps + | _ -> + [], [] + +and match_row infer_binds env tr1 tr2 ps = + match tr2 with + | [] -> + [], [] + | (l, t2)::tr2' -> + let t1, zs, app = extract_bind infer_binds env tr1 l t2 in + let su1, zs1 = + try match_typ infer_binds env t1 t2 ps with + | Sub e -> raise (Sub (Struct(l, e))) + in + let su2, zs2 = + match_row infer_binds env tr1 (subst_row (List.map psubst su1) tr2') ps in + su1 @ su2, zs @ zs1 @ zs2 + let sub_typ = sub_typ true let sub_extyp = sub_extyp true diff --git a/sub.mli b/sub.mli index a3856abd..9660c8a2 100644 --- a/sub.mli +++ b/sub.mli @@ -24,12 +24,18 @@ val string_of_error : error -> string val sub_typ : Env.env -> Types.typ -> Types.typ -> Types.typ list -> - Types.typ list * Types.infer ref list * Fomega.exp (* raise Sub *) + (Types.typ * Types.typ) list * Types.infer ref list * Fomega.exp (* raise Sub *) val sub_extyp : Env.env -> Types.extyp -> Types.extyp -> Types.typ list -> - Types.typ list * Types.infer ref list * Fomega.exp (* raise Sub *) + (Types.typ * Types.typ) list * Types.infer ref list * Fomega.exp (* raise Sub *) val equal_typ : Env.env -> Types.typ -> Types.typ -> Types.infer ref list (* raise Sub *) val equal_extyp : Env.env -> Types.extyp -> Types.extyp -> Types.infer ref list (* raise Sub *) + +val subst_of_match: (Types.typ * Types.typ) list -> (Types.var * Types.typ) list + +(* String conversion *) + +val string_of_match: (Types.typ * Types.typ) list -> string diff --git a/types.mli b/types.mli index fd6a4dc9..a1d35f1a 100644 --- a/types.mli +++ b/types.mli @@ -97,6 +97,7 @@ val map_rowi : (lab -> 'a -> 'b) -> 'a row -> 'b row val intersect_row : 'a row -> 'a row -> 'a row val diff_row : 'a row -> 'a row -> 'a row +val has_typs : typ -> bool val intersect_typs : typ -> typ -> typ val merge_typs : typ -> typ -> typ