src/Pure/type.ML
changeset 17804 4deae4b33d97
parent 17756 d4a35f82fbb4
child 18928 042608ffa2ec
     1.1 --- a/src/Pure/type.ML	Sat Oct 08 22:39:41 2005 +0200
     1.2 +++ b/src/Pure/type.ML	Sat Oct 08 22:39:42 2005 +0200
     1.3 @@ -58,6 +58,7 @@
     1.4    exception TUNIFY
     1.5    val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int
     1.6    val raw_unify: typ * typ -> tyenv -> tyenv
     1.7 +  val could_unify: typ * typ -> bool
     1.8    val eq_type: tyenv -> typ * typ -> bool
     1.9  
    1.10    (*extend and merge type signatures*)
    1.11 @@ -355,6 +356,7 @@
    1.12        | NONE => T)
    1.13    | devar tye T = T;
    1.14  
    1.15 +(*order-sorted unification*)
    1.16  fun unify (tsig as TSig {classes = (_, classes), arities, ...}) TU (tyenv, maxidx) =
    1.17    let
    1.18      val tyvar_count = ref maxidx;
    1.19 @@ -422,8 +424,17 @@
    1.20  and raw_unifys (T :: Ts, U :: Us) tye = raw_unifys (Ts, Us) (raw_unify (T, U) tye)
    1.21    | raw_unifys _ tye = tye;
    1.22  
    1.23 +(*fast unification filter*)
    1.24 +fun could_unify (Type (a, Ts), Type (b, Us)) = a = b andalso could_unifys (Ts, Us)
    1.25 +  | could_unify (TFree (a, _), TFree (b, _)) = a = b
    1.26 +  | could_unify (TVar _, _) = true
    1.27 +  | could_unify (_, TVar _) = true
    1.28 +  | could_unify _ = false
    1.29 +and could_unifys (T :: Ts, U :: Us) = could_unify (T, U) andalso could_unifys (Ts, Us)
    1.30 +  | could_unifys _ = true;
    1.31  
    1.32 -(*check whether two types are equal with respect to a type environment*)
    1.33 +
    1.34 +(*equality with respect to a type environment*)
    1.35  fun eq_type tye (T, T') =
    1.36    (case (devar tye T, devar tye T') of
    1.37       (Type (s, Ts), Type (s', Ts')) =>