Implement Robinson's algorithm for type unification. Closes #227.

1 files changed, 70 insertions, 75 deletions

diff --git a/src/comp/middle/ty.rs b/src/comp/middle/ty.rs
index e8f5b046..a9a4e936 100644
--- a/src/comp/middle/ty.rs
+++ b/src/comp/middle/ty.rs
@@ -570,24 +570,6 @@ fn count_ty_params(@t ty) -> uint {
     ret _vec.len[ast.def_id](*param_ids);
 }
 
-fn type_contains_ty_vars(@t ty) -> bool {
-    state obj checker(@mutable bool has_vars) {
-        fn fold_simple_ty(@t ty) -> @t {
-            alt (ty.struct) {
-                case (ty_var(_)) {
-                    *has_vars = true;
-                }
-                case (_) {}
-            }
-            ret ty;
-        }
-    }
-
-    let @mutable bool b = @mutable false;
-    fold_ty(checker(b), ty);
-    ret *b;
-}
-
 // Type accessors for substructures of types
 
 fn ty_fn_args(@t fty) -> vec[arg] {
@@ -802,7 +784,10 @@ fn is_lval(@ast.expr expr) -> bool {
     }
 }
 
-// Type unification
+// Type unification via Robinson's algorithm (Robinson 1965). Implemented as
+// described in Hoder and Voronkov:
+//
+//     http://www.cs.man.ac.uk/~hoderk/ubench/unification_full.pdf
 
 fn unify(@ty.t expected, @ty.t actual, &unify_handler handler)
         -> unify_result {
@@ -822,7 +807,7 @@ fn unify(@ty.t expected, @ty.t actual, &unify_handler handler)
         ret ures_err(terr_mismatch, expected, actual);
     }
 
-    fn unify_fn(&hashmap[int,@ty.t] bindings,
+    fn unify_fn(@hashmap[int,@ty.t] bindings,
                 @ty.t expected,
                 @ty.t actual,
                 &unify_handler handler,
@@ -891,7 +876,7 @@ fn unify(@ty.t expected, @ty.t actual, &unify_handler handler)
 
     }
 
-    fn unify_obj(&hashmap[int,@ty.t] bindings,
+    fn unify_obj(@hashmap[int,@ty.t] bindings,
                 @ty.t expected,
                 @ty.t actual,
                 &unify_handler handler,
@@ -952,27 +937,44 @@ fn unify(@ty.t expected, @ty.t actual, &unify_handler handler)
       ret ures_ok(t);
     }
 
-    fn unify_step(&hashmap[int,@ty.t] bindings, @ty.t expected, @ty.t actual,
-                  &unify_handler handler) -> unify_result {
+    fn resolve(@hashmap[int,@t] bindings, @t typ) -> @t {
+        alt (typ.struct) {
+            case (ty_var(?id)) {
+                alt (bindings.find(id)) {
+                    case (some[@t](?typ2)) {
+                        ret resolve(bindings, typ2);
+                    }
+                    case (none[@t]) {
+                        // fall through
+                    }
+                }
+            }
+            case (_) {
+                // fall through
+            }
+        }
+        ret typ;
+    }
+
+    fn unify_step(@hashmap[int,@ty.t] bindings, @ty.t in_expected,
+                  @ty.t in_actual, &unify_handler handler) -> unify_result {
+
+        // Resolve any bindings.
+        auto expected = resolve(bindings, in_expected);
+        auto actual = resolve(bindings, in_actual);
+
         // TODO: rewrite this using tuple pattern matching when available, to
         // avoid all this rightward drift and spikiness.
 
+        // TODO: occurs check, to make sure we don't loop forever when
+        // unifying e.g. 'a and option['a]
+
         alt (actual.struct) {
             // If the RHS is a variable type, then just do the appropriate
             // binding.
             case (ty.ty_var(?actual_id)) {
-                alt (bindings.find(actual_id)) {
-                    case (some[@ty.t](?actual_ty)) {
-                        // FIXME: change the binding here?
-                        // FIXME: "be"
-                        ret unify_step(bindings, expected, actual_ty,
-                                       handler);
-                    }
-                    case (none[@ty.t]) {
-                        bindings.insert(actual_id, expected);
-                        ret ures_ok(expected);
-                    }
-                }
+                bindings.insert(actual_id, expected);
+                ret ures_ok(expected);
             }
             case (ty.ty_local(?actual_id)) {
                 auto actual_ty = handler.resolve_local(actual_id);
@@ -1077,8 +1079,6 @@ fn unify(@ty.t expected, @ty.t actual, &unify_handler handler)
                         }
                     }
 
-                    // TODO: ty_var
-
                     case (_) {
                         ret ures_err(terr_mismatch, expected, actual);
                     }
@@ -1102,8 +1102,6 @@ fn unify(@ty.t expected, @ty.t actual, &unify_handler handler)
                         }
                     }
 
-                    // TODO: ty_var
-
                     case (_) {
                         ret ures_err(terr_mismatch, expected, actual);
                    }
@@ -1152,8 +1150,6 @@ fn unify(@ty.t expected, @ty.t actual, &unify_handler handler)
                         ret ures_ok(plain_ty(ty.ty_tup(result_elems)));
                     }
 
-                    // TODO: ty_var
-
                     case (_) {
                         ret ures_err(terr_mismatch, expected, actual);
                     }
@@ -1213,8 +1209,6 @@ fn unify(@ty.t expected, @ty.t actual, &unify_handler handler)
                         ret ures_ok(plain_ty(ty.ty_rec(result_fields)));
                     }
 
-                    // TODO: ty_var
-
                     case (_) {
                         ret ures_err(terr_mismatch, expected, actual);
                     }
@@ -1248,20 +1242,9 @@ fn unify(@ty.t expected, @ty.t actual, &unify_handler handler)
             }
 
             case (ty.ty_var(?expected_id)) {
-                alt (bindings.find(expected_id)) {
-                    case (some[@ty.t](?expected_ty)) {
-                        // FIXME: change the binding here?
-                        // FIXME: "be"
-                        ret unify_step(bindings,
-                                       expected_ty,
-                                       actual,
-                                       handler);
-                    }
-                    case (none[@ty.t]) {
-                        bindings.insert(expected_id, actual);
-                        ret ures_ok(actual);
-                    }
-                }
+                // Add a binding.
+                bindings.insert(expected_id, actual);
+                ret ures_ok(actual);
             }
 
             case (ty.ty_local(?expected_id)) {
@@ -1289,31 +1272,43 @@ fn unify(@ty.t expected, @ty.t actual, &unify_handler handler)
         fail;
     }
 
+    // Performs type binding substitution.
+    fn substitute(@hashmap[int,@t] bindings, @t typ) -> @t {
+        state obj folder(@hashmap[int,@t] bindings) {
+            fn fold_simple_ty(@t typ) -> @t {
+                alt (typ.struct) {
+                    case (ty_var(?id)) {
+                        alt (bindings.find(id)) {
+                            case (some[@t](?typ2)) {
+                                ret substitute(bindings, typ2);
+                            }
+                            case (none[@t]) {
+                                ret typ;
+                            }
+                        }
+                    }
+                    case (_) {
+                        ret typ;
+                    }
+                }
+            }
+        }
+
+        ret ty.fold_ty(folder(bindings), typ);
+    }
+
     fn hash_int(&int x) -> uint { ret x as uint; }
     fn eq_int(&int a, &int b) -> bool { ret a == b; }
     auto hasher = hash_int;
     auto eqer = eq_int;
-    auto bindings = map.mk_hashmap[int,@ty.t](hasher, eqer);
-
-    // FIXME: this is a slow way of driving types into residual vars that
-    // occur up in the leaves of result type; it can likely be done better
-    // when unification is actually ... down in the leaves.
+    auto bindings = @map.mk_hashmap[int,@ty.t](hasher, eqer);
 
     auto ures = unify_step(bindings, expected, actual, handler);
-    while (true) {
-        alt (ures) {
-            case (ures_ok(?t)) {
-                if (!type_contains_ty_vars(t)) {
-                    ret ures;
-                }
-                ures = unify_step(bindings, t, actual, handler);
-            }
-            case (_) {
-                ret ures;
-            }
-        }
+    alt (ures) {
+        case (ures_ok(?t))  { ret ures_ok(substitute(bindings, t)); }
+        case (_)            { ret ures;                             }
     }
-    fail;
+    fail;   // not reached
 }
 
 fn type_err_to_str(&ty.type_err err) -> str {