src/Pure/type.ML
changeset 16946 7f9a7fe413f3
parent 16885 cabcd33cde18
child 17184 3d80209e9a53
     1.1 --- a/src/Pure/type.ML	Thu Jul 28 15:20:02 2005 +0200
     1.2 +++ b/src/Pure/type.ML	Thu Jul 28 15:20:03 2005 +0200
     1.3 @@ -51,11 +51,13 @@
     1.4    exception TYPE_MATCH
     1.5    type tyenv
     1.6    val lookup: tyenv * (indexname * sort) -> typ option
     1.7 -  val typ_match: tsig -> tyenv * (typ * typ) -> tyenv
     1.8 +  val typ_match: tsig -> typ * typ -> tyenv -> tyenv
     1.9    val typ_instance: tsig -> typ * typ -> bool
    1.10 +  val raw_match: typ * typ -> tyenv -> tyenv
    1.11 +  val raw_instance: typ * typ -> bool
    1.12    exception TUNIFY
    1.13 -  val unify: tsig -> tyenv * int -> typ * typ -> tyenv * int
    1.14 -  val raw_unify: typ * typ -> bool
    1.15 +  val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int
    1.16 +  val raw_unify: typ * typ -> tyenv -> tyenv
    1.17    val eq_type: tyenv -> typ * typ -> bool
    1.18  
    1.19    (*extend and merge type signatures*)
    1.20 @@ -213,10 +215,7 @@
    1.21  (* varify, unvarify *)
    1.22  
    1.23  val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S));
    1.24 -
    1.25 -fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
    1.26 -  | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
    1.27 -  | unvarifyT T = T;
    1.28 +val unvarifyT = map_type_tvar (fn ((a, 0), S) => TFree (a, S) | v => TVar v);
    1.29  
    1.30  fun varify (t, fixed) =
    1.31    let
    1.32 @@ -224,9 +223,9 @@
    1.33      val ixns = add_term_tvar_ixns (t, []);
    1.34      val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
    1.35      fun thaw (f as (a, S)) =
    1.36 -      (case assoc (fmap, f) of
    1.37 +      (case gen_assoc (op =) (fmap, f) of
    1.38          NONE => TFree f
    1.39 -      | SOME b => TVar (b, S));
    1.40 +      | SOME xi => TVar (xi, S));
    1.41    in (map_term_types (map_type_tfree thaw) t, fmap) end;
    1.42  
    1.43  
    1.44 @@ -294,7 +293,7 @@
    1.45  
    1.46  exception TYPE_MATCH;
    1.47  
    1.48 -fun typ_match tsig (tyenv, TU) =
    1.49 +fun typ_match tsig =
    1.50    let
    1.51      fun match (TVar (v, S), T) subs =
    1.52            (case lookup (subs, (v, S)) of
    1.53 @@ -310,10 +309,27 @@
    1.54        | match _ _ = raise TYPE_MATCH
    1.55      and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs)
    1.56        | matches _ subs = subs;
    1.57 -  in match TU tyenv end;
    1.58 +  in match end;
    1.59  
    1.60  fun typ_instance tsig (T, U) =
    1.61 -  (typ_match tsig (Vartab.empty, (U, T)); true) handle TYPE_MATCH => false;
    1.62 +  (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
    1.63 +
    1.64 +(*purely structural matching*)
    1.65 +fun raw_match (TVar (v, S), T) subs =
    1.66 +      (case lookup (subs, (v, S)) of
    1.67 +        NONE => Vartab.update_new ((v, (S, T)), subs)
    1.68 +      | SOME U => if U = T then subs else raise TYPE_MATCH)
    1.69 +  | raw_match (Type (a, Ts), Type (b, Us)) subs =
    1.70 +      if a <> b then raise TYPE_MATCH
    1.71 +      else raw_matches (Ts, Us) subs
    1.72 +  | raw_match (TFree x, TFree y) subs =
    1.73 +      if x = y then subs else raise TYPE_MATCH
    1.74 +  | raw_match _ _ = raise TYPE_MATCH
    1.75 +and raw_matches (T :: Ts, U :: Us) subs = raw_matches (Ts, Us) (raw_match (T, U) subs)
    1.76 +  | raw_matches _ subs = subs;
    1.77 +
    1.78 +fun raw_instance (T, U) =
    1.79 +  (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
    1.80  
    1.81  
    1.82  (* unification *)
    1.83 @@ -339,7 +355,7 @@
    1.84        | NONE => T)
    1.85    | devar tye T = T;
    1.86  
    1.87 -fun unify (tsig as TSig {classes = (_, classes), arities, ...}) (tyenv, maxidx) TU =
    1.88 +fun unify (tsig as TSig {classes = (_, classes), arities, ...}) TU (tyenv, maxidx) =
    1.89    let
    1.90      val tyvar_count = ref maxidx;
    1.91      fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
    1.92 @@ -386,10 +402,26 @@
    1.93        | unifs _ tye = tye;
    1.94    in (unif TU tyenv, ! tyvar_count) end;
    1.95  
    1.96 -(*purely structural unification *)
    1.97 -fun raw_unify (ty1, ty2) =
    1.98 -  (unify empty_tsig (Vartab.empty, 0) (strip_sorts ty1, strip_sorts ty2); true)
    1.99 -    handle TUNIFY => false;
   1.100 +(*purely structural unification*)
   1.101 +fun raw_unify (ty1, ty2) tye =
   1.102 +  (case (devar tye ty1, devar tye ty2) of
   1.103 +    (T as TVar (v, S1), U as TVar (w, S2)) =>
   1.104 +      if eq_ix (v, w) then
   1.105 +        if S1 = S2 then tye else tvar_clash v S1 S2
   1.106 +      else Vartab.update_new ((w, (S2, T)), tye)
   1.107 +  | (TVar (v, S), T) =>
   1.108 +      if occurs v tye T then raise TUNIFY
   1.109 +      else Vartab.update_new ((v, (S, T)), tye)
   1.110 +  | (T, TVar (v, S)) =>
   1.111 +      if occurs v tye T then raise TUNIFY
   1.112 +      else Vartab.update_new ((v, (S, T)), tye)
   1.113 +  | (Type (a, Ts), Type (b, Us)) =>
   1.114 +      if a <> b then raise TUNIFY
   1.115 +      else raw_unifys (Ts, Us) tye
   1.116 +  | (T, U) => if T = U then tye else raise TUNIFY)
   1.117 +and raw_unifys (T :: Ts, U :: Us) tye = raw_unifys (Ts, Us) (raw_unify (T, U) tye)
   1.118 +  | raw_unifys _ tye = tye;
   1.119 +
   1.120  
   1.121  (*check whether two types are equal with respect to a type environment*)
   1.122  fun eq_type tye (T, T') =
   1.123 @@ -527,7 +559,7 @@
   1.124        Graph.merge_trans_acyclic (op =) (classes1, classes2)
   1.125          handle Graph.DUPS cs => err_dup_classes cs
   1.126            | Graph.CYCLES css => err_cyclic_classes pp css;
   1.127 -  in (space, classes) end;    
   1.128 +  in (space, classes) end;
   1.129  
   1.130  end;
   1.131  
   1.132 @@ -578,7 +610,7 @@
   1.133    let
   1.134      fun err msg =
   1.135        error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a);
   1.136 -    val rhs' = compress_type (strip_sorts (no_tvars (cert_typ_syntax tsig rhs)))
   1.137 +    val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs))
   1.138        handle TYPE (msg, _, _) => err msg;
   1.139    in
   1.140      (case duplicates vs of