diff options
author | 2009-04-28 11:05:28 -0400 | |
---|---|---|
committer | 2009-04-28 11:05:28 -0400 | |
commit | 008b594412606bbf78fff76daff219a102ce2daa (patch) | |
tree | 3fd436b0d0eff217ce878cae73dd070a73f12835 /src/elab_env.sml | |
parent | 04dd6b3727c7786a4824897e78b0b2982ecd6f5b (diff) |
LEFT JOIN
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r-- | src/elab_env.sml | 87 |
1 files changed, 82 insertions, 5 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index 62a310f2..7b20a700 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -507,6 +507,8 @@ fun unifyCons rs = (CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2) | (_, CUnif (_, _, _, ref (SOME c2))) => unify d (c1, c2) + | (CUnif _, _) => () + | (c1', CRel n2) => if n2 < d then case c1' of @@ -587,7 +589,56 @@ fun unifySubst (rs : con list) = | (d, _) => d} 0 -fun resolveClass (env : env) = +fun postUnify x = + let + fun unify (c1, c2) = + case (#1 c1, #1 c2) of + (CUnif (_, _, _, ref (SOME c1)), _) => unify (c1, c2) + | (_, CUnif (_, _, _, ref (SOME c2))) => unify (c1, c2) + + | (CUnif (_, _, _, r), _) => r := SOME c2 + + | (TFun (d1, r1), TFun (d2, r2)) => (unify (d1, d2); unify (r1, r2)) + | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (r1, r2)) + | (TRecord c1, TRecord c2) => unify (c1, c2) + | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) => + (unify (a1, a2); unify (b1, b2); unify (c1, c2)) + + | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify + | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify + | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) => + if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify + | (CApp (f1, x1), CApp (f2, x2)) => (unify (f1, f2); unify (x1, x2)) + | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); unify (b1, b2)) + + | (CKAbs (_, b1), CKAbs (_, b2)) => unify (b1, b2) + | (CKApp (c1, k1), CKApp (c2, k2)) => (unify (c1, c2); unifyKinds (k1, k2)) + | (TKFun (_, c1), TKFun (_, c2)) => unify (c1, c2) + + | (CName s1, CName s2) => if s1 = s2 then () else raise Unify + + | (CRecord (k1, xcs1), CRecord (k2, xcs2)) => + (unifyKinds (k1, k2); + ListPair.appEq (fn ((x1, c1), (x2, c2)) => (unify (x1, x2); unify (c1, c2))) (xcs1, xcs2) + handle ListPair.UnequalLengths => raise Unify) + | (CConcat (f1, x1), CConcat (f2, x2)) => (unify (f1, f2); unify (x1, x2)) + | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2)) + + | (CUnit, CUnit) => () + + | (CTuple cs1, CTuple cs2) => (ListPair.appEq unify (cs1, cs2) + handle ListPair.UnequalLengths => raise Unify) + | (CProj (c1, n1), CProj (c2, n2)) => (unify (c1, c2); + if n1 = n2 then () else raise Unify) + + | _ => raise Unify + in + unify x + end + +fun postUnifies x = (postUnify x; true) handle Unify => false + +fun resolveClass (hnorm : con -> con) (env : env) = let fun resolve c = let @@ -608,7 +659,8 @@ fun resolveClass (env : env) = let val eos = map (resolve o unifySubst rs) cs in - if List.exists (not o Option.isSome) eos then + if List.exists (not o Option.isSome) eos + orelse not (postUnifies (c, unifySubst rs c')) then tryRules rules' else let @@ -634,9 +686,34 @@ fun resolveClass (env : env) = tryGrounds (#ground class) end in - case class_head_in c of - SOME f => doHead f - | _ => NONE + case #1 c of + TRecord c => + (case #1 (hnorm c) of + CRecord (_, xts) => + let + fun resolver (xts, acc) = + case xts of + [] => SOME (ERecord acc, #2 c) + | (x, t) :: xts => + let + val t = hnorm t + + val t = case t of + (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc) + | _ => t + in + case resolve t of + NONE => NONE + | SOME e => resolver (xts, (x, e, t) :: acc) + end + in + resolver (xts, []) + end + | _ => NONE) + | _ => + case class_head_in c of + SOME f => doHead f + | _ => NONE end in resolve |