src/Pure/type.ML
changeset 16885 cabcd33cde18
parent 16650 bd4f7149ba1e
child 16946 7f9a7fe413f3
     1.1 --- a/src/Pure/type.ML	Tue Jul 19 17:21:56 2005 +0200
     1.2 +++ b/src/Pure/type.ML	Tue Jul 19 17:21:57 2005 +0200
     1.3 @@ -304,10 +304,12 @@
     1.4            | SOME U => if U = T then subs else raise TYPE_MATCH)
     1.5        | match (Type (a, Ts), Type (b, Us)) subs =
     1.6            if a <> b then raise TYPE_MATCH
     1.7 -          else fold match (Ts ~~ Us) subs
     1.8 +          else matches (Ts, Us) subs
     1.9        | match (TFree x, TFree y) subs =
    1.10            if x = y then subs else raise TYPE_MATCH
    1.11 -      | match _ _ = raise TYPE_MATCH;
    1.12 +      | match _ _ = raise TYPE_MATCH
    1.13 +    and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs)
    1.14 +      | matches _ subs = subs;
    1.15    in match TU tyenv end;
    1.16  
    1.17  fun typ_instance tsig (T, U) =
    1.18 @@ -331,11 +333,11 @@
    1.19    in occ end;
    1.20  
    1.21  (*chase variable assignments; if devar returns a type var then it must be unassigned*)
    1.22 -fun devar (T as TVar v, tye) =
    1.23 -      (case  lookup (tye, v) of
    1.24 -        SOME U => devar (U, tye)
    1.25 +fun devar tye (T as TVar v) =
    1.26 +      (case lookup (tye, v) of
    1.27 +        SOME U => devar tye U
    1.28        | NONE => T)
    1.29 -  | devar (T, tye) = T;
    1.30 +  | devar tye T = T;
    1.31  
    1.32  fun unify (tsig as TSig {classes = (_, classes), arities, ...}) (tyenv, maxidx) TU =
    1.33    let
    1.34 @@ -345,22 +347,20 @@
    1.35      fun mg_domain a S =
    1.36        Sorts.mg_domain (classes, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY;
    1.37  
    1.38 -    fun meet ((_, []), tye) = tye
    1.39 -      | meet ((TVar (xi, S'), S), tye) =
    1.40 +    fun meet (_, []) tye = tye
    1.41 +      | meet (TVar (xi, S'), S) tye =
    1.42            if Sorts.sort_le classes (S', S) then tye
    1.43            else Vartab.update_new ((xi, (S',
    1.44              gen_tyvar (Sorts.inter_sort classes (S', S)))), tye)
    1.45 -      | meet ((TFree (_, S'), S), tye) =
    1.46 +      | meet (TFree (_, S'), S) tye =
    1.47            if Sorts.sort_le classes (S', S) then tye
    1.48            else raise TUNIFY
    1.49 -      | meet ((Type (a, Ts), S), tye) = meets ((Ts, mg_domain a S), tye)
    1.50 -    and meets (([], []), tye) = tye
    1.51 -      | meets ((T :: Ts, S :: Ss), tye) =
    1.52 -          meets ((Ts, Ss), meet ((devar (T, tye), S), tye))
    1.53 -      | meets _ = sys_error "meets";
    1.54 +      | meet (Type (a, Ts), S) tye = meets (Ts, mg_domain a S) tye
    1.55 +    and meets (T :: Ts, S :: Ss) tye = meets (Ts, Ss) (meet (devar tye T, S) tye)
    1.56 +      | meets _ tye = tye;
    1.57  
    1.58 -    fun unif ((ty1, ty2), tye) =
    1.59 -      (case (devar (ty1, tye), devar (ty2, tye)) of
    1.60 +    fun unif (ty1, ty2) tye =
    1.61 +      (case (devar tye ty1, devar tye ty2) of
    1.62          (T as TVar (v, S1), U as TVar (w, S2)) =>
    1.63            if eq_ix (v, w) then
    1.64              if S1 = S2 then tye else tvar_clash v S1 S2
    1.65 @@ -374,15 +374,17 @@
    1.66              end
    1.67        | (TVar (v, S), T) =>
    1.68            if occurs v tye T then raise TUNIFY
    1.69 -          else meet ((T, S), Vartab.update_new ((v, (S, T)), tye))
    1.70 +          else meet (T, S) (Vartab.update_new ((v, (S, T)), tye))
    1.71        | (T, TVar (v, S)) =>
    1.72            if occurs v tye T then raise TUNIFY
    1.73 -          else meet ((T, S), Vartab.update_new ((v, (S, T)), tye))
    1.74 +          else meet (T, S) (Vartab.update_new ((v, (S, T)), tye))
    1.75        | (Type (a, Ts), Type (b, Us)) =>
    1.76            if a <> b then raise TUNIFY
    1.77 -          else foldr unif tye (Ts ~~ Us)
    1.78 -      | (T, U) => if T = U then tye else raise TUNIFY);
    1.79 -  in (unif (TU, tyenv), ! tyvar_count) end;
    1.80 +          else unifs (Ts, Us) tye
    1.81 +      | (T, U) => if T = U then tye else raise TUNIFY)
    1.82 +    and unifs (T :: Ts, U :: Us) tye = unifs (Ts, Us) (unif (T, U) tye)
    1.83 +      | unifs _ tye = tye;
    1.84 +  in (unif TU tyenv, ! tyvar_count) end;
    1.85  
    1.86  (*purely structural unification *)
    1.87  fun raw_unify (ty1, ty2) =
    1.88 @@ -391,7 +393,7 @@
    1.89  
    1.90  (*check whether two types are equal with respect to a type environment*)
    1.91  fun eq_type tye (T, T') =
    1.92 -  (case (devar (T, tye), devar (T', tye)) of
    1.93 +  (case (devar tye T, devar tye T') of
    1.94       (Type (s, Ts), Type (s', Ts')) =>
    1.95         s = s' andalso ListPair.all (eq_type tye) (Ts, Ts')
    1.96     | (U, U') => U = U');