src/Pure/type.ML
changeset 15797 a63605582573
parent 15574 b1d1b5bfc464
child 16289 958207815931
     1.1 --- a/src/Pure/type.ML	Thu Apr 21 19:02:54 2005 +0200
     1.2 +++ b/src/Pure/type.ML	Thu Apr 21 19:12:03 2005 +0200
     1.3 @@ -41,18 +41,18 @@
     1.4    val no_tvars: typ -> typ
     1.5    val varifyT: typ -> typ
     1.6    val unvarifyT: typ -> typ
     1.7 -  val varify: term * string list -> term * (string * indexname) list
     1.8 +  val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list
     1.9    val freeze_thaw_type : typ -> typ * (typ -> typ)
    1.10    val freeze_thaw : term -> term * (term -> term)
    1.11  
    1.12    (*matching and unification*)
    1.13 -  val inst_typ_tvars: Pretty.pp -> tsig -> (indexname * typ) list -> typ -> typ
    1.14 -  val inst_term_tvars: Pretty.pp -> tsig -> (indexname * typ) list -> term -> term
    1.15    exception TYPE_MATCH
    1.16 -  val typ_match: tsig -> typ Vartab.table * (typ * typ) -> typ Vartab.table
    1.17 +  type tyenv
    1.18 +  val lookup: tyenv * (indexname * sort) -> typ option
    1.19 +  val typ_match: tsig -> tyenv * (typ * typ) -> tyenv
    1.20    val typ_instance: tsig -> typ * typ -> bool
    1.21    exception TUNIFY
    1.22 -  val unify: tsig -> typ Vartab.table * int -> typ * typ -> typ Vartab.table * int
    1.23 +  val unify: tsig -> tyenv * int -> typ * typ -> tyenv * int
    1.24    val raw_unify: typ * typ -> bool
    1.25  
    1.26    (*extend and merge type signatures*)
    1.27 @@ -219,11 +219,11 @@
    1.28  
    1.29  fun varify (t, fixed) =
    1.30    let
    1.31 -    val fs = add_term_tfree_names (t, []) \\ fixed;
    1.32 +    val fs = add_term_tfrees (t, []) \\ fixed;
    1.33      val ixns = add_term_tvar_ixns (t, []);
    1.34 -    val fmap = fs ~~ map (rpair 0) (variantlist (fs, map #1 ixns))
    1.35 +    val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
    1.36      fun thaw (f as (a, S)) =
    1.37 -      (case assoc (fmap, a) of
    1.38 +      (case assoc (fmap, f) of
    1.39          NONE => TFree f
    1.40        | SOME b => TVar (b, S));
    1.41    in (map_term_types (map_type_tfree thaw) t, fmap) end;
    1.42 @@ -273,21 +273,15 @@
    1.43  
    1.44  (** matching and unification of types **)
    1.45  
    1.46 -(* instantiation *)
    1.47 +type tyenv = (sort * typ) Vartab.table;
    1.48  
    1.49 -fun inst_typ_tvars pp tsig tye =
    1.50 -  let
    1.51 -    fun inst (var as (v, S)) =
    1.52 -      (case assoc_string_int (tye, v) of
    1.53 -        SOME U =>
    1.54 -          if of_sort tsig (U, S) then U
    1.55 -          else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [U], [])
    1.56 -      | NONE => TVar var);
    1.57 -  in map_type_tvar inst end;
    1.58 +fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
    1.59 +  quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
    1.60 +  [TVar (ixn, S), TVar (ixn, S')], []);
    1.61  
    1.62 -fun inst_term_tvars _ _ [] t = t
    1.63 -  | inst_term_tvars pp tsig tye t = map_term_types (inst_typ_tvars pp tsig tye) t;
    1.64 -
    1.65 +fun lookup (tye, (ixn, S)) = case Vartab.lookup (tye, ixn) of
    1.66 +    NONE => NONE
    1.67 +  | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S';
    1.68  
    1.69  (* matching *)
    1.70  
    1.71 @@ -296,9 +290,9 @@
    1.72  fun typ_match tsig =
    1.73    let
    1.74      fun match (subs, (TVar (v, S), T)) =
    1.75 -          (case Vartab.lookup (subs, v) of
    1.76 +          (case lookup (subs, (v, S)) of
    1.77              NONE =>
    1.78 -              if of_sort tsig (T, S) then Vartab.update ((v, T), subs)
    1.79 +              if of_sort tsig (T, S) then Vartab.update_new ((v, (S, T)), subs)
    1.80                else raise TYPE_MATCH
    1.81            | SOME U => if U = T then subs else raise TYPE_MATCH)
    1.82        | match (subs, (Type (a, Ts), Type (b, Us))) =
    1.83 @@ -322,16 +316,16 @@
    1.84    let
    1.85      fun occ (Type (_, Ts)) = exists occ Ts
    1.86        | occ (TFree _) = false
    1.87 -      | occ (TVar (w, _)) =
    1.88 +      | occ (TVar (w, S)) =
    1.89            eq_ix (v, w) orelse
    1.90 -            (case Vartab.lookup (tye, w) of
    1.91 +            (case lookup (tye, (w, S)) of
    1.92                NONE => false
    1.93              | SOME U => occ U);
    1.94    in occ end;
    1.95  
    1.96  (*chase variable assignments; if devar returns a type var then it must be unassigned*)
    1.97 -fun devar (T as TVar (v, _), tye) =
    1.98 -      (case  Vartab.lookup (tye, v) of
    1.99 +fun devar (T as TVar v, tye) =
   1.100 +      (case  lookup (tye, v) of
   1.101          SOME U => devar (U, tye)
   1.102        | NONE => T)
   1.103    | devar (T, tye) = T;
   1.104 @@ -347,8 +341,8 @@
   1.105      fun meet ((_, []), tye) = tye
   1.106        | meet ((TVar (xi, S'), S), tye) =
   1.107            if Sorts.sort_le classes (S', S) then tye
   1.108 -          else Vartab.update_new ((xi,
   1.109 -            gen_tyvar (Sorts.inter_sort classes (S', S))), tye)
   1.110 +          else Vartab.update_new ((xi, (S',
   1.111 +            gen_tyvar (Sorts.inter_sort classes (S', S)))), tye)
   1.112        | meet ((TFree (_, S'), S), tye) =
   1.113            if Sorts.sort_le classes (S', S) then tye
   1.114            else raise TUNIFY
   1.115 @@ -361,21 +355,22 @@
   1.116      fun unif ((ty1, ty2), tye) =
   1.117        (case (devar (ty1, tye), devar (ty2, tye)) of
   1.118          (T as TVar (v, S1), U as TVar (w, S2)) =>
   1.119 -          if eq_ix (v, w) then tye
   1.120 +          if eq_ix (v, w) then
   1.121 +            if S1 = S2 then tye else tvar_clash v S1 S2
   1.122            else if Sorts.sort_le classes (S1, S2) then
   1.123 -            Vartab.update_new ((w, T), tye)
   1.124 +            Vartab.update_new ((w, (S2, T)), tye)
   1.125            else if Sorts.sort_le classes (S2, S1) then
   1.126 -            Vartab.update_new ((v, U), tye)
   1.127 +            Vartab.update_new ((v, (S1, U)), tye)
   1.128            else
   1.129              let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in
   1.130 -              Vartab.update_new ((v, S), Vartab.update_new ((w, S), tye))
   1.131 +              Vartab.update_new ((v, (S1, S)), Vartab.update_new ((w, (S2, S)), tye))
   1.132              end
   1.133        | (TVar (v, S), T) =>
   1.134            if occurs v tye T then raise TUNIFY
   1.135 -          else meet ((T, S), Vartab.update_new ((v, T), tye))
   1.136 +          else meet ((T, S), Vartab.update_new ((v, (S, T)), tye))
   1.137        | (T, TVar (v, S)) =>
   1.138            if occurs v tye T then raise TUNIFY
   1.139 -          else meet ((T, S), Vartab.update_new ((v, T), tye))
   1.140 +          else meet ((T, S), Vartab.update_new ((v, (S, T)), tye))
   1.141        | (Type (a, Ts), Type (b, Us)) =>
   1.142            if a <> b then raise TUNIFY
   1.143            else foldr unif tye (Ts ~~ Us)