# HG changeset patch
# User wenzelm
# Date 1128803982 -7200
# Node ID 4deae4b33d97381fab366eab2961a448e5537a2f
# Parent  e235a57651a142496ae7af5037281954ffe91666
added could_unify;

diff -r e235a57651a1 -r 4deae4b33d97 src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Oct 08 22:39:41 2005 +0200
+++ b/src/Pure/type.ML	Sat Oct 08 22:39:42 2005 +0200
@@ -58,6 +58,7 @@
   exception TUNIFY
   val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int
   val raw_unify: typ * typ -> tyenv -> tyenv
+  val could_unify: typ * typ -> bool
   val eq_type: tyenv -> typ * typ -> bool
 
   (*extend and merge type signatures*)
@@ -355,6 +356,7 @@
       | NONE => T)
   | devar tye T = T;
 
+(*order-sorted unification*)
 fun unify (tsig as TSig {classes = (_, classes), arities, ...}) TU (tyenv, maxidx) =
   let
     val tyvar_count = ref maxidx;
@@ -422,8 +424,17 @@
 and raw_unifys (T :: Ts, U :: Us) tye = raw_unifys (Ts, Us) (raw_unify (T, U) tye)
   | raw_unifys _ tye = tye;
 
+(*fast unification filter*)
+fun could_unify (Type (a, Ts), Type (b, Us)) = a = b andalso could_unifys (Ts, Us)
+  | could_unify (TFree (a, _), TFree (b, _)) = a = b
+  | could_unify (TVar _, _) = true
+  | could_unify (_, TVar _) = true
+  | could_unify _ = false
+and could_unifys (T :: Ts, U :: Us) = could_unify (T, U) andalso could_unifys (Ts, Us)
+  | could_unifys _ = true;
 
-(*check whether two types are equal with respect to a type environment*)
+
+(*equality with respect to a type environment*)
 fun eq_type tye (T, T') =
   (case (devar tye T, devar tye T') of
      (Type (s, Ts), Type (s', Ts')) =>