LEFT JOIN

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