--- a/src/Pure/type.ML Mon Mar 10 23:03:51 2014 +0100
+++ b/src/Pure/type.ML Tue Mar 11 10:14:45 2014 +0100
@@ -76,6 +76,8 @@
val typ_instance: tsig -> typ * typ -> bool
val raw_match: typ * typ -> tyenv -> tyenv
val raw_matches: typ list * typ list -> tyenv -> tyenv
+ val could_match: typ * typ -> bool
+ val could_matches: typ list * typ list -> bool
val raw_instance: typ * typ -> bool
exception TUNIFY
val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int
@@ -461,8 +463,19 @@
| raw_matches ([], []) subs = subs
| raw_matches _ _ = raise TYPE_MATCH;
+(*fast matching filter*)
+fun could_match (Type (a, Ts), Type (b, Us)) = a = b andalso could_matches (Ts, Us)
+ | could_match (TFree (a, _), TFree (b, _)) = a = b
+ | could_match (TVar _, _) = true
+ | could_match _ = false
+and could_matches (T :: Ts, U :: Us) = could_match (T, U) andalso could_matches (Ts, Us)
+ | could_matches ([], []) = true
+ | could_matches _ = false;
+
fun raw_instance (T, U) =
- (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
+ if could_match (U, T) then
+ (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false
+ else false;
(* unification *)