Skip to content

Commit

Permalink
Separate matching from subtyping like in F-ing modules to allow RDS
Browse files Browse the repository at this point in the history
  • Loading branch information
@polytypic
polytypic committed Jul 4, 2020
1 parent afcf81e commit 6ffef69
Show file tree
Hide file tree
Showing 5 changed files with 163 additions and 50 deletions.
21 changes: 11 additions & 10 deletions elab.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions regression.1ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
}

;;
Expand Down
178 changes: 140 additions & 38 deletions sub.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)))

Expand All @@ -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) ->
Expand All @@ -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 =
Expand Down Expand Up @@ -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)));
Expand All @@ -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)));
Expand All @@ -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));
Expand All @@ -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 =
Expand All @@ -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));
Expand All @@ -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
10 changes: 8 additions & 2 deletions sub.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading

0 comments on commit 6ffef69

Please sign in to comment.