- Eliminated nodup_vars check.
authorberghofe
Thu Apr 21 19:12:03 2005 +0200 (2005-04-21)
changeset 15797a63605582573
parent 15796 348ce23d2fc2
child 15798 016f3be5a5ec
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
src/Pure/drule.ML
src/Pure/envir.ML
src/Pure/pattern.ML
src/Pure/proofterm.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/Pure/tactic.ML
src/Pure/term.ML
src/Pure/thm.ML
src/Pure/type.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/drule.ML	Thu Apr 21 19:02:54 2005 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu Apr 21 19:12:03 2005 +0200
     1.3 @@ -17,11 +17,13 @@
     1.4    val strip_imp_prems   : cterm -> cterm list
     1.5    val strip_imp_concl   : cterm -> cterm
     1.6    val cprems_of         : thm -> cterm list
     1.7 +  val cterm_fun         : (term -> term) -> (cterm -> cterm)
     1.8 +  val ctyp_fun          : (typ -> typ) -> (ctyp -> ctyp)
     1.9    val read_insts        :
    1.10            Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    1.11                    -> (indexname -> typ option) * (indexname -> sort option)
    1.12                    -> string list -> (indexname * string) list
    1.13 -                  -> (indexname*ctyp)list * (cterm*cterm)list
    1.14 +                  -> (ctyp * ctyp) list * (cterm * cterm) list
    1.15    val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
    1.16    val strip_shyps_warning : thm -> thm
    1.17    val forall_intr_list  : cterm list -> thm -> thm
    1.18 @@ -36,7 +38,7 @@
    1.19    val implies_elim_list : thm -> thm list -> thm
    1.20    val implies_intr_list : cterm list -> thm -> thm
    1.21    val instantiate       :
    1.22 -    (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
    1.23 +    (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    1.24    val zero_var_indexes  : thm -> thm
    1.25    val standard          : thm -> thm
    1.26    val standard'         : thm -> thm
    1.27 @@ -131,7 +133,7 @@
    1.28    val rename_bvars': string option list -> thm -> thm
    1.29    val unvarifyT: thm -> thm
    1.30    val unvarify: thm -> thm
    1.31 -  val tvars_intr_list: string list -> thm -> thm * (string * indexname) list
    1.32 +  val tvars_intr_list: string list -> thm -> thm * (string * (indexname * sort)) list
    1.33    val remdups_rl: thm
    1.34    val conj_intr: thm -> thm -> thm
    1.35    val conj_intr_list: thm list -> thm
    1.36 @@ -140,6 +142,8 @@
    1.37    val conj_elim_precise: int -> thm -> thm list
    1.38    val conj_intr_thm: thm
    1.39    val abs_def: thm -> thm
    1.40 +  val read_instantiate_sg': Sign.sg -> (indexname * string) list -> thm -> thm
    1.41 +  val read_instantiate': (indexname * string) list -> thm -> thm
    1.42  end;
    1.43  
    1.44  structure Drule: DRULE =
    1.45 @@ -181,6 +185,14 @@
    1.46  (*The premises of a theorem, as a cterm list*)
    1.47  val cprems_of = strip_imp_prems o cprop_of;
    1.48  
    1.49 +fun cterm_fun f ct =
    1.50 +  let val {t, sign, ...} = Thm.rep_cterm ct
    1.51 +  in Thm.cterm_of sign (f t) end;
    1.52 +
    1.53 +fun ctyp_fun f cT =
    1.54 +  let val {T, sign, ...} = Thm.rep_ctyp cT
    1.55 +  in Thm.ctyp_of sign (f T) end;
    1.56 +
    1.57  val proto_sign = Theory.sign_of ProtoPure.thy;
    1.58  
    1.59  val implies = cterm_of proto_sign Term.implies;
    1.60 @@ -223,8 +235,9 @@
    1.61      fun is_tv ((a, _), _) =
    1.62        (case Symbol.explode a of "'" :: _ => true | _ => false);
    1.63      val (tvs, vs) = List.partition is_tv insts;
    1.64 +    fun sort_of ixn = case rsorts ixn of SOME S => S | NONE => absent ixn;
    1.65      fun readT (ixn, st) =
    1.66 -        let val S = case rsorts ixn of SOME S => S | NONE => absent ixn;
    1.67 +        let val S = sort_of ixn;
    1.68              val T = Sign.read_typ (sign,sorts) st;
    1.69          in if Sign.typ_instance sign (T, TVar(ixn,S)) then (ixn,T)
    1.70             else inst_failure ixn
    1.71 @@ -241,7 +254,8 @@
    1.72          let val U = typ_subst_TVars tye2 T
    1.73          in cterm_of sign (Var(ixn,U)) end
    1.74      val ixnTs = ListPair.zip(ixns, map snd sTs)
    1.75 -in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) (tye2 @ tye),
    1.76 +in (map (fn (ixn, T) => (ctyp_of sign (TVar (ixn, sort_of ixn)),
    1.77 +      ctyp_of sign T)) (tye2 @ tye),
    1.78      ListPair.zip(map mkcVar ixnTs,cts))
    1.79  end;
    1.80  
    1.81 @@ -380,12 +394,12 @@
    1.82              foldr add_term_tvars 
    1.83                    (foldr add_term_tvars (term_tvars prop) tpair_l) tpair_r;
    1.84          val nms' = rev(Library.foldl add_new_id ([], map (#1 o #1) inrs));
    1.85 -        val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs)))
    1.86 +        val tye = ListPair.map (fn ((v, rs), a) => (TVar (v, rs), TVar ((a, 0), rs)))
    1.87                       (inrs, nms')
    1.88 -        val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye;
    1.89 +        val ctye = map (pairself (ctyp_of sign)) tye;
    1.90          fun varpairs([],[]) = []
    1.91            | varpairs((var as Var(v,T)) :: vars, b::bs) =
    1.92 -                let val T' = typ_subst_TVars tye T
    1.93 +                let val T' = typ_subst_atomic tye T
    1.94                  in (cterm_of sign (Var(v,T')),
    1.95                      cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
    1.96                  end
    1.97 @@ -820,16 +834,21 @@
    1.98  (*Version that normalizes the result: Thm.instantiate no longer does that*)
    1.99  fun instantiate instpair th = Thm.instantiate instpair th  COMP   asm_rl;
   1.100  
   1.101 -fun read_instantiate_sg sg sinsts th =
   1.102 +fun read_instantiate_sg' sg sinsts th =
   1.103      let val ts = types_sorts th;
   1.104          val used = add_used th [];
   1.105 -        val sinsts' = map (apfst Syntax.indexname) sinsts
   1.106 -    in  instantiate (read_insts sg ts ts used sinsts') th  end;
   1.107 +    in  instantiate (read_insts sg ts ts used sinsts) th  end;
   1.108 +
   1.109 +fun read_instantiate_sg sg sinsts th =
   1.110 +  read_instantiate_sg' sg (map (apfst Syntax.indexname) sinsts) th;
   1.111  
   1.112  (*Instantiate theorem th, reading instantiations under theory of th*)
   1.113  fun read_instantiate sinsts th =
   1.114      read_instantiate_sg (Thm.sign_of_thm th) sinsts th;
   1.115  
   1.116 +fun read_instantiate' sinsts th =
   1.117 +    read_instantiate_sg' (Thm.sign_of_thm th) sinsts th;
   1.118 +
   1.119  
   1.120  (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
   1.121    Instantiates distinct Vars by terms, inferring type instantiations. *)
   1.122 @@ -846,9 +865,9 @@
   1.123  fun cterm_instantiate ctpairs0 th =
   1.124    let val (sign,tye,_) = foldr add_types (Thm.sign_of_thm th, Vartab.empty, 0) ctpairs0
   1.125        fun instT(ct,cu) = 
   1.126 -        let val inst = cterm_of sign o subst_TVars_Vartab tye o term_of
   1.127 +        let val inst = cterm_of sign o Envir.subst_TVars tye o term_of
   1.128          in (inst ct, inst cu) end
   1.129 -      fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
   1.130 +      fun ctyp2 (ixn, (S, T)) = (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)
   1.131    in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   1.132    handle TERM _ =>
   1.133             raise THM("cterm_instantiate: incompatible signatures",0,[th])
   1.134 @@ -925,6 +944,10 @@
   1.135        (Thm.cterm_of (#sign (Thm.rep_cterm ct)) (Var v), ct)
   1.136          handle TYPE (msg, _, _) => err msg;
   1.137  
   1.138 +    fun tyinst_of (v, cT) =
   1.139 +      (Thm.ctyp_of (#sign (Thm.rep_ctyp cT)) (TVar v), cT)
   1.140 +        handle TYPE (msg, _, _) => err msg;
   1.141 +
   1.142      fun zip_vars _ [] = []
   1.143        | zip_vars (_ :: vs) (NONE :: opt_ts) = zip_vars vs opt_ts
   1.144        | zip_vars (v :: vs) (SOME t :: opt_ts) = (v, t) :: zip_vars vs opt_ts
   1.145 @@ -933,7 +956,7 @@
   1.146      (*instantiate types first!*)
   1.147      val thm' =
   1.148        if forall is_none cTs then thm
   1.149 -      else Thm.instantiate (zip_vars (map fst (tvars_of thm)) cTs, []) thm;
   1.150 +      else Thm.instantiate (map tyinst_of (zip_vars (tvars_of thm) cTs), []) thm;
   1.151      in
   1.152        if forall is_none cts then thm'
   1.153        else Thm.instantiate ([], map inst_of (zip_vars (vars_of thm') cts)) thm'
   1.154 @@ -1000,10 +1023,11 @@
   1.155  
   1.156  fun tfrees_of thm =
   1.157    let val {hyps, prop, ...} = Thm.rep_thm thm
   1.158 -  in foldr Term.add_term_tfree_names [] (prop :: hyps) end;
   1.159 +  in foldr Term.add_term_tfrees [] (prop :: hyps) end;
   1.160  
   1.161  fun tvars_intr_list tfrees thm =
   1.162 -  Thm.varifyT' (tfrees_of thm \\ tfrees) thm;
   1.163 +  apsnd (map (fn ((s, S), ixn) => (s, (ixn, S)))) (Thm.varifyT'
   1.164 +    (gen_rems (op = o apfst fst) (tfrees_of thm, tfrees)) thm);
   1.165  
   1.166  
   1.167  (* increment var indexes *)
     2.1 --- a/src/Pure/envir.ML	Thu Apr 21 19:02:54 2005 +0200
     2.2 +++ b/src/Pure/envir.ML	Thu Apr 21 19:12:03 2005 +0200
     2.3 @@ -3,33 +3,39 @@
     2.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.5      Copyright   1988  University of Cambridge
     2.6  
     2.7 -Environments.  They don't take account that typ is part of variable
     2.8 -name.  Therefore we check elsewhere that two variables with same names
     2.9 -and different types cannot occur.
    2.10 +Environments.  The type of a term variable / sort of a type variable is
    2.11 +part of its name. The lookup function must apply type substitutions,
    2.12 +since they may change the identity of a variable.
    2.13  *)
    2.14  
    2.15  signature ENVIR =
    2.16  sig
    2.17 -  datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
    2.18 -  val type_env: env -> typ Vartab.table
    2.19 +  type tenv
    2.20 +  datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int}
    2.21 +  val type_env: env -> Type.tyenv
    2.22    exception SAME
    2.23    val genvars: string -> env * typ list -> env * term list
    2.24    val genvar: string -> env * typ -> env * term
    2.25 -  val lookup: env * indexname -> term option
    2.26 -  val update: (indexname * term) * env -> env
    2.27 +  val lookup: env * (indexname * typ) -> term option
    2.28 +  val lookup': (Type.tyenv * tenv) * (indexname * typ) -> term option
    2.29 +  val update: ((indexname * typ) * term) * env -> env
    2.30    val empty: int -> env
    2.31    val is_empty: env -> bool
    2.32    val above: int * env -> bool
    2.33 -  val vupdate: (indexname * term) * env -> env
    2.34 -  val alist_of: env -> (indexname * term) list
    2.35 +  val vupdate: ((indexname * typ) * term) * env -> env
    2.36 +  val alist_of: env -> (indexname * (typ * term)) list
    2.37    val norm_term: env -> term -> term
    2.38    val norm_term_same: env -> term -> term
    2.39 -  val norm_type: typ Vartab.table -> typ -> typ
    2.40 -  val norm_type_same: typ Vartab.table -> typ -> typ
    2.41 -  val norm_types_same: typ Vartab.table -> typ list -> typ list
    2.42 +  val norm_type: Type.tyenv -> typ -> typ
    2.43 +  val norm_type_same: Type.tyenv -> typ -> typ
    2.44 +  val norm_types_same: Type.tyenv -> typ list -> typ list
    2.45    val beta_norm: term -> term
    2.46    val head_norm: env -> term -> term
    2.47    val fastype: env -> typ list -> term -> typ
    2.48 +  val typ_subst_TVars: Type.tyenv -> typ -> typ
    2.49 +  val subst_TVars: Type.tyenv -> term -> term
    2.50 +  val subst_Vars: tenv -> term -> term
    2.51 +  val subst_vars: Type.tyenv * tenv -> term -> term
    2.52  end;
    2.53  
    2.54  structure Envir : ENVIR =
    2.55 @@ -38,10 +44,12 @@
    2.56  (*updating can destroy environment in 2 ways!!
    2.57     (1) variables out of range   (2) circular assignments
    2.58  *)
    2.59 +type tenv = (typ * term) Vartab.table
    2.60 +
    2.61  datatype env = Envir of
    2.62 -    {maxidx: int,               (*maximum index of vars*)
    2.63 -     asol: term Vartab.table,   (*table of assignments to Vars*)
    2.64 -     iTs: typ Vartab.table}     (*table of assignments to TVars*)
    2.65 +    {maxidx: int,      (*maximum index of vars*)
    2.66 +     asol: tenv,       (*table of assignments to Vars*)
    2.67 +     iTs: Type.tyenv}  (*table of assignments to TVars*)
    2.68  
    2.69  fun type_env (Envir {iTs, ...}) = iTs;
    2.70  
    2.71 @@ -60,10 +68,46 @@
    2.72    let val (env',[v]) = genvars name (env,[T])
    2.73    in  (env',v)  end;
    2.74  
    2.75 -fun lookup (Envir{asol,...}, xname) : term option = Vartab.lookup (asol, xname);
    2.76 +(* de-reference TVars. When dealing with environments produced by *)
    2.77 +(* matching instead of unification, there is no need to chase     *)
    2.78 +(* assigned TVars. In this case, set b to false.                  *)
    2.79 +fun devar b iTs (T as TVar vT) = (case Type.lookup (iTs, vT) of
    2.80 +      NONE => T
    2.81 +    | SOME T' => if b then devar true iTs T' else T')
    2.82 +  | devar b iTs T = T;
    2.83 +
    2.84 +fun eq_type b iTs (T, T') =
    2.85 +  (case (devar b iTs T, devar b iTs T') of
    2.86 +     (Type (s, Ts), Type (s', Ts')) =>
    2.87 +       s = s' andalso ListPair.all (eq_type b iTs) (Ts, Ts')
    2.88 +   | (U, U') => U = U');
    2.89 +
    2.90 +fun var_clash ixn T T' = raise TYPE ("Variable " ^
    2.91 +  quote (Syntax.string_of_vname ixn) ^ " has two distinct types",
    2.92 +  [T', T], []);
    2.93  
    2.94 -fun update ((xname, t), Envir{maxidx, asol, iTs}) =
    2.95 -  Envir{maxidx=maxidx, asol=Vartab.update_new ((xname,t), asol), iTs=iTs};
    2.96 +fun gen_lookup f asol (xname, T) =
    2.97 +  (case Vartab.lookup (asol, xname) of
    2.98 +     NONE => NONE
    2.99 +   | SOME (U, t) => if f (T, U) then SOME t
   2.100 +       else var_clash xname T U);
   2.101 +
   2.102 +(* version ignoring type substitutions *)
   2.103 +fun lookup1 asol = gen_lookup op = asol;
   2.104 +
   2.105 +fun gen_lookup2 b (iTs, asol) =
   2.106 +  if Vartab.is_empty iTs then lookup1 asol
   2.107 +  else gen_lookup (eq_type b iTs) asol;
   2.108 +
   2.109 +fun lookup2 env = gen_lookup2 true env;
   2.110 +
   2.111 +fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
   2.112 +
   2.113 +(* version for matching algorithms, does not chase TVars *)
   2.114 +fun lookup' (env, p) = gen_lookup2 false env p;
   2.115 +
   2.116 +fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
   2.117 +  Envir{maxidx=maxidx, asol=Vartab.update_new ((xname, (T, t)), asol), iTs=iTs};
   2.118  
   2.119  (*The empty environment.  New variables will start with the given index+1.*)
   2.120  fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
   2.121 @@ -80,15 +124,15 @@
   2.122     | (SOME (_, i), SOME (_, i')) => i > lim andalso i' > lim);
   2.123  
   2.124  (*Update, checking Var-Var assignments: try to suppress higher indexes*)
   2.125 -fun vupdate((a,t), env) = case t of
   2.126 -      Var(name',T) =>
   2.127 -        if a=name' then env     (*cycle!*)
   2.128 +fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
   2.129 +      Var (nT as (name', T)) =>
   2.130 +        if a = name' then env     (*cycle!*)
   2.131          else if xless(a, name')  then
   2.132 -           (case lookup(env,name') of  (*if already assigned, chase*)
   2.133 -                NONE => update((name', Var(a,T)), env)
   2.134 -              | SOME u => vupdate((a,u), env))
   2.135 -        else update((a,t), env)
   2.136 -    | _ => update((a,t), env);
   2.137 +           (case lookup (env, nT) of  (*if already assigned, chase*)
   2.138 +                NONE => update ((nT, Var (a, T)), env)
   2.139 +              | SOME u => vupdate ((aU, u), env))
   2.140 +        else update ((aU, t), env)
   2.141 +    | _ => update ((aU, t), env);
   2.142  
   2.143  
   2.144  (*Convert environment to alist*)
   2.145 @@ -103,8 +147,8 @@
   2.146  exception SAME;
   2.147  
   2.148  fun norm_term1 same (asol,t) : term =
   2.149 -  let fun norm (Var (w,T)) =
   2.150 -            (case Vartab.lookup (asol, w) of
   2.151 +  let fun norm (Var wT) =
   2.152 +            (case lookup1 asol wT of
   2.153                  SOME u => (norm u handle SAME => u)
   2.154                | NONE   => raise SAME)
   2.155          | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
   2.156 @@ -120,7 +164,7 @@
   2.157  
   2.158  fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
   2.159    | normT iTs (TFree _) = raise SAME
   2.160 -  | normT iTs (TVar(v, _)) = (case Vartab.lookup (iTs, v) of
   2.161 +  | normT iTs (TVar vS) = (case Type.lookup (iTs, vS) of
   2.162            SOME U => normTh iTs U
   2.163          | NONE => raise SAME)
   2.164  and normTh iTs T = ((normT iTs T) handle SAME => T)
   2.165 @@ -133,7 +177,7 @@
   2.166    let fun norm (Const (a, T)) = Const(a, normT iTs T)
   2.167          | norm (Free (a, T)) = Free(a, normT iTs T)
   2.168          | norm (Var (w, T)) =
   2.169 -            (case Vartab.lookup (asol, w) of
   2.170 +            (case lookup2 (iTs, asol) (w, T) of
   2.171                  SOME u => normh u
   2.172                | NONE   => Var(w, normT iTs T))
   2.173          | norm (Abs (a, T, body)) =
   2.174 @@ -169,7 +213,7 @@
   2.175  
   2.176  fun head_norm env t =
   2.177    let
   2.178 -    fun hnorm (Var (v, T)) = (case lookup (env, v) of
   2.179 +    fun hnorm (Var vT) = (case lookup (env, vT) of
   2.180            SOME u => head_norm env u
   2.181          | NONE => raise SAME)
   2.182        | hnorm (Abs (a, T, body)) =  Abs (a, T, hnorm body)
   2.183 @@ -189,8 +233,8 @@
   2.184      fun fast Ts (f $ u) =
   2.185  	(case fast Ts f of
   2.186  	   Type ("fun", [_, T]) => T
   2.187 -	 | TVar(ixn, _) =>
   2.188 -		(case Vartab.lookup (iTs, ixn) of
   2.189 +	 | TVar ixnS =>
   2.190 +		(case Type.lookup (iTs, ixnS) of
   2.191  		   SOME (Type ("fun", [_, T])) => T
   2.192  		 | _ => raise TERM (funerr, [f $ u]))
   2.193  	 | _ => raise TERM (funerr, [f $ u]))
   2.194 @@ -203,4 +247,37 @@
   2.195        | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
   2.196  in fast end;
   2.197  
   2.198 +
   2.199 +(*Substitute for type Vars in a type*)
   2.200 +fun typ_subst_TVars iTs T = if Vartab.is_empty iTs then T else
   2.201 +  let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
   2.202 +        | subst(T as TFree _) = T
   2.203 +        | subst(T as TVar ixnS) =
   2.204 +            (case Type.lookup (iTs, ixnS) of NONE => T | SOME(U) => U)
   2.205 +  in subst T end;
   2.206 +
   2.207 +(*Substitute for type Vars in a term*)
   2.208 +val subst_TVars = map_term_types o typ_subst_TVars;
   2.209 +
   2.210 +(*Substitute for Vars in a term *)
   2.211 +fun subst_Vars itms t = if Vartab.is_empty itms then t else
   2.212 +  let fun subst (v as Var ixnT) = getOpt (lookup1 itms ixnT, v)
   2.213 +        | subst (Abs (a, T, t)) = Abs (a, T, subst t)
   2.214 +        | subst (f $ t) = subst f $ subst t
   2.215 +        | subst t = t
   2.216 +  in subst t end;
   2.217 +
   2.218 +(*Substitute for type/term Vars in a term *)
   2.219 +fun subst_vars (env as (iTs, itms)) =
   2.220 +  if Vartab.is_empty iTs then subst_Vars itms else
   2.221 +  let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T)
   2.222 +        | subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T)
   2.223 +        | subst (Var (ixn, T)) = (case lookup' (env, (ixn, T)) of
   2.224 +            NONE   => Var (ixn, typ_subst_TVars iTs T)
   2.225 +          | SOME t => t)
   2.226 +        | subst (b as Bound _) = b
   2.227 +        | subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t)
   2.228 +        | subst (f $ t) = subst f $ subst t
   2.229 +  in subst end;
   2.230 +
   2.231  end;
     3.1 --- a/src/Pure/pattern.ML	Thu Apr 21 19:02:54 2005 +0200
     3.2 +++ b/src/Pure/pattern.ML	Thu Apr 21 19:12:03 2005 +0200
     3.3 @@ -22,9 +22,9 @@
     3.4    val beta_eta_contract : term -> term
     3.5    val eta_contract_atom : term -> term
     3.6    val match             : Type.tsig -> term * term
     3.7 -                          -> (indexname*typ)list * (indexname*term)list
     3.8 +                          -> Type.tyenv * Envir.tenv
     3.9    val first_order_match : Type.tsig -> term * term
    3.10 -                          -> (indexname*typ)list * (indexname*term)list
    3.11 +                          -> Type.tyenv * Envir.tenv
    3.12    val matches           : Type.tsig -> term * term -> bool
    3.13    val matches_subterm   : Type.tsig -> term * term -> bool
    3.14    val unify             : Sign.sg * Envir.env * (term * term)list -> Envir.env
    3.15 @@ -72,7 +72,7 @@
    3.16    if !trace_unify_fail then clash (boundVar binders i) s
    3.17    else ()
    3.18  
    3.19 -fun proj_fail sg (env,binders,F,is,t) =
    3.20 +fun proj_fail sg (env,binders,F,_,is,t) =
    3.21    if !trace_unify_fail
    3.22    then let val f = Syntax.string_of_vname F
    3.23             val xs = bnames binders is
    3.24 @@ -94,7 +94,7 @@
    3.25    else ()
    3.26  
    3.27  fun occurs(F,t,env) =
    3.28 -    let fun occ(Var(G,_))   = (case Envir.lookup(env,G) of
    3.29 +    let fun occ(Var (G, T))   = (case Envir.lookup (env, (G, T)) of
    3.30                                   SOME(t) => occ t
    3.31                                 | NONE    => F=G)
    3.32            | occ(t1$t2)      = occ t1 orelse occ t2
    3.33 @@ -153,7 +153,7 @@
    3.34  
    3.35  fun mknewhnf(env,binders,is,F as (a,_),T,js) =
    3.36    let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js))
    3.37 -  in Envir.update((F,mkhnf(binders,is,G,js)),env') end;
    3.38 +  in Envir.update (((F, T), mkhnf (binders, is, G, js)), env') end;
    3.39  
    3.40  
    3.41  (* mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ] *)
    3.42 @@ -186,7 +186,7 @@
    3.43                            val Hty = type_of_G env (Fty,length js,ks)
    3.44                            val (env',H) = Envir.genvar a (env,Hty)
    3.45                            val env'' =
    3.46 -                                Envir.update((F,mkhnf(binders,js,H,ks)),env')
    3.47 +                            Envir.update (((F, Fty), mkhnf (binders, js, H, ks)), env')
    3.48                        in (app(H,ls),env'') end
    3.49                   | _  => raise Pattern))
    3.50          and prs(s::ss,env,d,binders) =
    3.51 @@ -216,12 +216,12 @@
    3.52    let fun ff(F,Fty,is,G as (a,_),Gty,js) =
    3.53              if js subset_int is
    3.54              then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
    3.55 -                 in Envir.update((F,t),env) end
    3.56 +                 in Envir.update (((F, Fty), t), env) end
    3.57              else let val ks = is inter_int js
    3.58                       val Hty = type_of_G env (Fty,length is,map (idx is) ks)
    3.59                       val (env',H) = Envir.genvar a (env,Hty)
    3.60                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
    3.61 -                 in Envir.update((G,lam js), Envir.update((F,lam is),env'))
    3.62 +                 in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
    3.63                   end;
    3.64    in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
    3.65  
    3.66 @@ -243,8 +243,8 @@
    3.67         ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
    3.68           if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
    3.69                    else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
    3.70 -      | ((Var(F,_),ss),_)             => flexrigid sg (env,binders,F,ints_of' env ss,t)
    3.71 -      | (_,(Var(F,_),ts))             => flexrigid sg (env,binders,F,ints_of' env ts,s)
    3.72 +      | ((Var(F,Fty),ss),_)           => flexrigid sg (env,binders,F,Fty,ints_of' env ss,t)
    3.73 +      | (_,(Var(F,Fty),ts))           => flexrigid sg (env,binders,F,Fty,ints_of' env ts,s)
    3.74        | ((Const c,ss),(Const d,ts))   => rigidrigid sg (env,binders,c,d,ss,ts)
    3.75        | ((Free(f),ss),(Free(g),ts))   => rigidrigid sg (env,binders,f,g,ss,ts)
    3.76        | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB sg (env,binders,i,j,ss,ts)
    3.77 @@ -266,10 +266,10 @@
    3.78       if i <> j then (clashBB binders i j; raise Unif)
    3.79       else Library.foldl (unif sg binders) (env ,ss~~ts)
    3.80  
    3.81 -and flexrigid sg (params as (env,binders,F,is,t)) =
    3.82 +and flexrigid sg (params as (env,binders,F,Fty,is,t)) =
    3.83        if occurs(F,t,env) then (ocheck_fail sg (F,t,binders,env); raise Unif)
    3.84        else (let val (u,env') = proj(t,env,binders,is)
    3.85 -            in Envir.update((F,mkabs(binders,is,u)),env') end
    3.86 +            in Envir.update (((F, Fty), mkabs (binders, is, u)), env') end
    3.87              handle Unif => (proj_fail sg params; raise Unif));
    3.88  
    3.89  fun unify(sg,env,tus) = Library.foldl (unif sg []) (env,tus);
    3.90 @@ -358,9 +358,9 @@
    3.91      fun mtch (instsp as (tyinsts,insts)) = fn
    3.92          (Var(ixn,T), t)  =>
    3.93            if loose_bvar(t,0) then raise MATCH
    3.94 -          else (case assoc_string_int(insts,ixn) of
    3.95 +          else (case Envir.lookup' (instsp, (ixn, T)) of
    3.96                    NONE => (typ_match tsig (tyinsts, (T, fastype_of t)),
    3.97 -                           (ixn,t)::insts)
    3.98 +                           Vartab.update_new ((ixn, (T, t)), insts))
    3.99                  | SOME u => if t aeconv u then instsp else raise MATCH)
   3.100        | (Free (a,T), Free (b,U)) =>
   3.101            if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
   3.102 @@ -374,18 +374,18 @@
   3.103        | _ => raise MATCH
   3.104    in mtch end;
   3.105  
   3.106 -fun first_order_match tsig = apfst Vartab.dest o fomatch tsig (Vartab.empty, []);
   3.107 +fun first_order_match tsig = fomatch tsig (Vartab.empty, Vartab.empty);
   3.108  
   3.109  (* Matching of higher-order patterns *)
   3.110  
   3.111 -fun match_bind(itms,binders,ixn,is,t) =
   3.112 +fun match_bind(itms,binders,ixn,T,is,t) =
   3.113    let val js = loose_bnos t
   3.114    in if null is
   3.115 -     then if null js then (ixn,t)::itms else raise MATCH
   3.116 +     then if null js then Vartab.update_new ((ixn, (T, t)), itms) else raise MATCH
   3.117       else if js subset_int is
   3.118            then let val t' = if downto0(is,length binders - 1) then t
   3.119                              else mapbnd (idx is) t
   3.120 -               in (ixn, mkabs(binders,is,t')) :: itms end
   3.121 +               in Vartab.update_new ((ixn, (T, mkabs (binders, is, t'))), itms) end
   3.122            else raise MATCH
   3.123    end;
   3.124  
   3.125 @@ -397,7 +397,7 @@
   3.126        Abs(ns,Ts,ts) =>
   3.127          (case obj of
   3.128             Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt))
   3.129 -         | _ => let val Tt = typ_subst_TVars_Vartab iTs Ts
   3.130 +         | _ => let val Tt = Envir.typ_subst_TVars iTs Ts
   3.131                  in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end)
   3.132      | _ => (case obj of
   3.133                Abs(nt,Tt,tt) =>
   3.134 @@ -412,10 +412,10 @@
   3.135                if a<> b then raise MATCH
   3.136                else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs)
   3.137      in case ph of
   3.138 -         Var(ixn,_) =>
   3.139 +         Var(ixn,T) =>
   3.140             let val is = ints_of pargs
   3.141 -           in case assoc_string_int(itms,ixn) of
   3.142 -                NONE => (iTs,match_bind(itms,binders,ixn,is,obj))
   3.143 +           in case Envir.lookup' (env, (ixn, T)) of
   3.144 +                NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
   3.145                | SOME u => if obj aeconv (red u is []) then env
   3.146                            else raise MATCH
   3.147             end
   3.148 @@ -435,10 +435,10 @@
   3.149    val pT = fastype_of pat
   3.150    and oT = fastype_of obj
   3.151    val iTs = typ_match tsg (Vartab.empty, (pT,oT))
   3.152 -  val insts2 = (iTs,[])
   3.153 +  val insts2 = (iTs, Vartab.empty)
   3.154  
   3.155 -in apfst Vartab.dest (mtch [] (insts2, po)
   3.156 -   handle Pattern => fomatch tsg insts2 po)
   3.157 +in mtch [] (insts2, po)
   3.158 +   handle Pattern => fomatch tsg insts2 po
   3.159  end;
   3.160  
   3.161  (*Predicate: does the pattern match the object?*)
   3.162 @@ -486,7 +486,7 @@
   3.163  
   3.164      fun match_rew tm (tm1, tm2) =
   3.165        let val rtm = getOpt (Term.rename_abs tm1 tm tm2, tm2)
   3.166 -      in SOME (subst_vars (match tsig (tm1, tm)) rtm, rtm)
   3.167 +      in SOME (Envir.subst_vars (match tsig (tm1, tm)) rtm, rtm)
   3.168          handle MATCH => NONE
   3.169        end;
   3.170  
     4.1 --- a/src/Pure/proofterm.ML	Thu Apr 21 19:02:54 2005 +0200
     4.2 +++ b/src/Pure/proofterm.ML	Thu Apr 21 19:12:03 2005 +0200
     4.3 @@ -69,11 +69,11 @@
     4.4    (** proof terms for specific inference rules **)
     4.5    val implies_intr_proof : term -> proof -> proof
     4.6    val forall_intr_proof : term -> string -> proof -> proof
     4.7 -  val varify_proof : term -> string list -> proof -> proof
     4.8 +  val varify_proof : term -> (string * sort) list -> proof -> proof
     4.9    val freezeT : term -> proof -> proof
    4.10    val rotate_proof : term list -> term -> int -> proof -> proof
    4.11    val permute_prems_prf : term list -> int -> int -> proof -> proof
    4.12 -  val instantiate : (indexname * typ) list -> (term * term) list -> proof -> proof
    4.13 +  val instantiate : (typ * typ) list -> (term * term) list -> proof -> proof
    4.14    val lift_proof : term -> int -> term -> proof -> proof
    4.15    val assumption_proof : term list -> term -> int -> proof -> proof
    4.16    val bicompose_proof : term list -> term list -> term list -> term option ->
    4.17 @@ -401,7 +401,8 @@
    4.18    | remove_types t = t;
    4.19  
    4.20  fun remove_types_env (Envir.Envir {iTs, asol, maxidx}) =
    4.21 -  Envir.Envir {iTs = iTs, asol = Vartab.map remove_types asol, maxidx = maxidx};
    4.22 +  Envir.Envir {iTs = iTs, asol = Vartab.map (apsnd remove_types) asol,
    4.23 +    maxidx = maxidx};
    4.24  
    4.25  fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
    4.26  
    4.27 @@ -530,11 +531,11 @@
    4.28  
    4.29  fun varify_proof t fixed prf =
    4.30    let
    4.31 -    val fs = add_term_tfree_names (t, []) \\ fixed;
    4.32 +    val fs = add_term_tfrees (t, []) \\ fixed;
    4.33      val ixns = add_term_tvar_ixns (t, []);
    4.34 -    val fmap = fs ~~ variantlist (fs, map #1 ixns)
    4.35 +    val fmap = fs ~~ variantlist (map fst fs, map #1 ixns)
    4.36      fun thaw (f as (a, S)) =
    4.37 -      (case assoc (fmap, a) of
    4.38 +      (case assoc (fmap, f) of
    4.39          NONE => TFree f
    4.40        | SOME b => TVar ((b, 0), S));
    4.41    in map_proof_terms (map_term_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
    4.42 @@ -598,7 +599,7 @@
    4.43  
    4.44  fun instantiate vTs tpairs prf =
    4.45    map_proof_terms (subst_atomic (map (apsnd remove_types) tpairs) o
    4.46 -    subst_TVars vTs) (typ_subst_TVars vTs) prf;
    4.47 +    map_term_types (typ_subst_atomic vTs)) (typ_subst_atomic vTs) prf;
    4.48  
    4.49  
    4.50  (***** lifting *****)
    4.51 @@ -955,7 +956,7 @@
    4.52  
    4.53  fun prf_subst (pinst, (tyinsts, insts)) =
    4.54    let
    4.55 -    val substT = typ_subst_TVars_Vartab tyinsts;
    4.56 +    val substT = Envir.typ_subst_TVars tyinsts;
    4.57  
    4.58      fun subst' lev (t as Var (ixn, _)) = (case assoc (insts, ixn) of
    4.59            NONE => t
     5.1 --- a/src/Pure/pure_thy.ML	Thu Apr 21 19:02:54 2005 +0200
     5.2 +++ b/src/Pure/pure_thy.ML	Thu Apr 21 19:12:03 2005 +0200
     5.3 @@ -273,7 +273,8 @@
     5.4        fun substsize prop =
     5.5              let val pat = extract_term prop
     5.6                  val (_,subst) = Pattern.match tsig (pat,obj)
     5.7 -            in Library.foldl op+ (0, map (size_of_term o snd) subst) end
     5.8 +            in Vartab.foldl (op + o apsnd (size_of_term o snd o snd)) (0, subst)
     5.9 +            end
    5.10  
    5.11        fun thm_ord ((p0,s0,_),(p1,s1,_)) =
    5.12              prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) int_ord ((p0,s0),(p1,s1));
     6.1 --- a/src/Pure/sign.ML	Thu Apr 21 19:02:54 2005 +0200
     6.2 +++ b/src/Pure/sign.ML	Thu Apr 21 19:12:03 2005 +0200
     6.3 @@ -47,7 +47,6 @@
     6.4    val classes: sg -> class list
     6.5    val defaultS: sg -> sort
     6.6    val subsort: sg -> sort * sort -> bool
     6.7 -  val nodup_vars: term -> term
     6.8    val of_sort: sg -> typ * sort -> bool
     6.9    val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list
    6.10    val universal_witness: sg -> (typ * sort) option
    6.11 @@ -103,8 +102,6 @@
    6.12    val read_typ_raw': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
    6.13    val read_tyname: sg -> string -> typ
    6.14    val read_const: sg -> string -> term
    6.15 -  val inst_typ_tvars: sg -> (indexname * typ) list -> typ -> typ
    6.16 -  val inst_term_tvars: sg -> (indexname * typ) list -> term -> term
    6.17    val infer_types: Pretty.pp -> sg -> (indexname -> typ option) ->
    6.18      (indexname -> sort option) -> string list -> bool
    6.19      -> xterm list * typ -> term * (indexname * typ) list
    6.20 @@ -740,53 +737,8 @@
    6.21  
    6.22    in typ_of ([], tm) end;
    6.23  
    6.24 -(*check for duplicate occurrences of TFree/TVar with distinct sorts*)
    6.25 -fun nodup_tvars (env, Type (_, Ts)) = nodup_tvars_list (env, Ts)
    6.26 -  | nodup_tvars (env as (tfrees, tvars), T as TFree (v as (a, S))) =
    6.27 -      (case assoc_string (tfrees, a) of
    6.28 -        SOME S' =>
    6.29 -          if S = S' then env
    6.30 -          else raise TYPE ("Type variable " ^ quote a ^
    6.31 -            " has two distinct sorts", [TFree (a, S'), T], [])
    6.32 -      | NONE => (v :: tfrees, tvars))
    6.33 -  | nodup_tvars (env as (tfrees, tvars), T as TVar (v as (a, S))) =
    6.34 -      (case assoc_string_int (tvars, a) of
    6.35 -        SOME S' =>
    6.36 -          if S = S' then env
    6.37 -          else raise TYPE ("Type variable " ^ quote (Syntax.string_of_vname a) ^
    6.38 -            " has two distinct sorts", [TVar (a, S'), T], [])
    6.39 -      | NONE => (tfrees, v :: tvars))
    6.40 -(*equivalent to foldl nodup_tvars_list, but 3X faster under Poly/ML*)
    6.41 -and nodup_tvars_list (env, []) = env
    6.42 -  | nodup_tvars_list (env, T :: Ts) = nodup_tvars_list (nodup_tvars (env, T), Ts);
    6.43 -
    6.44  in
    6.45  
    6.46 -(*check for duplicate occurrences of Free/Var with distinct types*)
    6.47 -fun nodup_vars tm =
    6.48 -  let
    6.49 -    fun nodups (envs as (env as (frees, vars), envT)) tm =
    6.50 -      (case tm of
    6.51 -        Const (c, T) => (env, nodup_tvars (envT, T))
    6.52 -      | Free (v as (a, T)) =>
    6.53 -          (case assoc_string (frees, a) of
    6.54 -            SOME T' =>
    6.55 -              if T = T' then (env, nodup_tvars (envT, T))
    6.56 -              else raise TYPE ("Variable " ^ quote a ^
    6.57 -                " has two distinct types", [T', T], [])
    6.58 -          | NONE => ((v :: frees, vars), nodup_tvars (envT, T)))
    6.59 -      | Var (v as (ixn, T)) =>
    6.60 -          (case assoc_string_int (vars, ixn) of
    6.61 -            SOME T' =>
    6.62 -              if T = T' then (env, nodup_tvars (envT, T))
    6.63 -              else raise TYPE ("Variable " ^ quote (Syntax.string_of_vname ixn) ^
    6.64 -                " has two distinct types", [T', T], [])
    6.65 -          | NONE => ((frees, v :: vars), nodup_tvars (envT, T)))
    6.66 -      | Bound _ => envs
    6.67 -      | Abs (_, T, t) => nodups (env, nodup_tvars (envT, T)) t
    6.68 -      | s $ t => nodups (nodups envs s) t)
    6.69 -  in nodups (([], []), ([], [])) tm; tm end;
    6.70 -
    6.71  fun certify_term pp sg tm =
    6.72    let
    6.73      val _ = check_stale sg;
    6.74 @@ -811,7 +763,6 @@
    6.75        | check_atoms _ = ();
    6.76    in
    6.77      check_atoms tm';
    6.78 -    nodup_vars tm';
    6.79      (tm', type_check pp sg tm', maxidx_of_term tm')
    6.80    end;
    6.81  
    6.82 @@ -835,13 +786,6 @@
    6.83  
    6.84  
    6.85  
    6.86 -(** instantiation **)
    6.87 -
    6.88 -fun inst_typ_tvars sg = Type.inst_typ_tvars (pp sg) (tsig_of sg);
    6.89 -fun inst_term_tvars sg = Type.inst_term_tvars (pp sg) (tsig_of sg);
    6.90 -
    6.91 -
    6.92 -
    6.93  (** infer_types **)         (*exception ERROR*)
    6.94  
    6.95  (*
     7.1 --- a/src/Pure/tactic.ML	Thu Apr 21 19:02:54 2005 +0200
     7.2 +++ b/src/Pure/tactic.ML	Thu Apr 21 19:12:03 2005 +0200
     7.3 @@ -94,7 +94,7 @@
     7.4    val subgoals_tac      : string list -> int -> tactic
     7.5    val subgoals_of_brl   : bool * thm -> int
     7.6    val term_lift_inst_rule       :
     7.7 -      thm * int * (indexname*typ)list * ((indexname*typ)*term)list  * thm
     7.8 +      thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm
     7.9        -> thm
    7.10    val instantiate_tac   : (string * string) list -> tactic
    7.11    val thin_tac          : string -> int -> tactic
    7.12 @@ -117,6 +117,7 @@
    7.13    val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
    7.14    val eres_inst_tac'    : (indexname * string) list -> thm -> int -> tactic
    7.15    val res_inst_tac'     : (indexname * string) list -> thm -> int -> tactic
    7.16 +  val instantiate_tac'  : (indexname * string) list -> tactic
    7.17  end;
    7.18  
    7.19  structure Tactic: TACTIC =
    7.20 @@ -246,9 +247,7 @@
    7.21                                      Logic.incr_indexes(paramTs,inc) t)
    7.22      (*Lifts instantiation pair over params*)
    7.23      fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
    7.24 -    fun lifttvar((a,i),ctyp) =
    7.25 -        let val {T,sign} = rep_ctyp ctyp
    7.26 -        in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
    7.27 +    val lifttvar = pairself (ctyp_fun (incr_tvar inc))
    7.28  in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
    7.29                       (lift_rule (st,i) rule)
    7.30  end;
    7.31 @@ -278,7 +277,9 @@
    7.32      fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T)
    7.33      (*lift only Var, not term, which must be lifted already*)
    7.34      fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t)
    7.35 -    fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T))
    7.36 +    fun liftTpair (((a, i), S), T) =
    7.37 +      (ctyp_of sign (TVar ((a, i + inc), S)),
    7.38 +       ctyp_of sign (incr_tvar inc T))
    7.39  in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
    7.40                       (lift_rule (st,i) rule)
    7.41  end;
    7.42 @@ -344,6 +345,8 @@
    7.43  (*instantiate variables in the whole state*)
    7.44  val instantiate_tac = PRIMITIVE o read_instantiate;
    7.45  
    7.46 +val instantiate_tac' = PRIMITIVE o Drule.read_instantiate';
    7.47 +
    7.48  (*Deletion of an assumption*)
    7.49  fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
    7.50  
    7.51 @@ -647,7 +650,7 @@
    7.52      val statement = Logic.list_implies (asms, prop);
    7.53      val frees = map Term.dest_Free (Term.term_frees statement);
    7.54      val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
    7.55 -    val fixed_tfrees = foldr Term.add_typ_tfree_names [] (map #2 fixed_frees);
    7.56 +    val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees);
    7.57      val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs;
    7.58  
    7.59      fun err msg = raise ERROR_MESSAGE
     8.1 --- a/src/Pure/term.ML	Thu Apr 21 19:02:54 2005 +0200
     8.2 +++ b/src/Pure/term.ML	Thu Apr 21 19:12:03 2005 +0200
     8.3 @@ -97,7 +97,6 @@
     8.4    val subst_bounds: term list * term -> term
     8.5    val subst_bound: term * term -> term
     8.6    val subst_TVars: (indexname * typ) list -> term -> term
     8.7 -  val subst_TVars_Vartab: typ Vartab.table -> term -> term
     8.8    val betapply: term * term -> term
     8.9    val eq_ix: indexname * indexname -> bool
    8.10    val ins_ix: indexname * indexname list -> indexname list
    8.11 @@ -113,9 +112,9 @@
    8.12    val could_unify: term * term -> bool
    8.13    val subst_free: (term * term) list -> term -> term
    8.14    val subst_atomic: (term * term) list -> term -> term
    8.15 +  val typ_subst_atomic: (typ * typ) list -> typ -> typ
    8.16    val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
    8.17    val typ_subst_TVars: (indexname * typ) list -> typ -> typ
    8.18 -  val typ_subst_TVars_Vartab : typ Vartab.table -> typ -> typ
    8.19    val subst_Vars: (indexname * term) list -> term -> term
    8.20    val incr_tvar: int -> typ -> typ
    8.21    val xless: (string * int) * indexname -> bool
    8.22 @@ -656,6 +655,12 @@
    8.23              | subst t = getOpt (assoc(instl,t),t)
    8.24        in  subst t  end;
    8.25  
    8.26 +(*Replace the ATOMIC type Ti by Ui;    instl = [(T1,U1), ..., (Tn,Un)].*)
    8.27 +fun typ_subst_atomic [] T = T
    8.28 +  | typ_subst_atomic instl (Type (s, Ts)) =
    8.29 +      Type (s, map (typ_subst_atomic instl) Ts)
    8.30 +  | typ_subst_atomic instl T = getOpt (assoc (instl, T), T);
    8.31 +
    8.32  (*Substitute for type Vars in a type*)
    8.33  fun typ_subst_TVars iTs T = if null iTs then T else
    8.34    let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
    8.35 @@ -1034,17 +1039,6 @@
    8.36  structure Typtab = TableFun(type key = typ val ord = typ_ord);
    8.37  structure Termtab = TableFun(type key = term val ord = term_ord);
    8.38  
    8.39 -(*Substitute for type Vars in a type, version using Vartab*)
    8.40 -fun typ_subst_TVars_Vartab iTs T = if Vartab.is_empty iTs then T else
    8.41 -  let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
    8.42 -        | subst(T as TFree _) = T
    8.43 -        | subst(T as TVar(ixn, _)) =
    8.44 -            (case Vartab.lookup (iTs, ixn) of NONE => T | SOME(U) => U)
    8.45 -  in subst T end;
    8.46 -
    8.47 -(*Substitute for type Vars in a term, version using Vartab*)
    8.48 -val subst_TVars_Vartab = map_term_types o typ_subst_TVars_Vartab;
    8.49 -
    8.50  
    8.51  (*** Compression of terms and types by sharing common subtrees.
    8.52       Saves 50-75% on storage requirements.  As it is a bit slow,
     9.1 --- a/src/Pure/thm.ML	Thu Apr 21 19:02:54 2005 +0200
     9.2 +++ b/src/Pure/thm.ML	Thu Apr 21 19:12:03 2005 +0200
     9.3 @@ -26,7 +26,6 @@
     9.4    val cterm_of          : Sign.sg -> term -> cterm
     9.5    val ctyp_of_term      : cterm -> ctyp
     9.6    val read_cterm        : Sign.sg -> string * typ -> cterm
     9.7 -  val cterm_fun         : (term -> term) -> (cterm -> cterm)
     9.8    val adjust_maxidx     : cterm -> cterm
     9.9    val read_def_cterm    :
    9.10      Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    9.11 @@ -86,11 +85,11 @@
    9.12    val implies_intr_hyps : thm -> thm
    9.13    val flexflex_rule     : thm -> thm Seq.seq
    9.14    val instantiate       :
    9.15 -    (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
    9.16 +    (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    9.17    val trivial           : cterm -> thm
    9.18    val class_triv        : Sign.sg -> class -> thm
    9.19    val varifyT           : thm -> thm
    9.20 -  val varifyT'          : string list -> thm -> thm * (string * indexname) list
    9.21 +  val varifyT'          : (string * sort) list -> thm -> thm * ((string * sort) * indexname) list
    9.22    val freezeT           : thm -> thm
    9.23    val dest_state        : thm * int ->
    9.24      (term * term) list * term list * term * term
    9.25 @@ -129,9 +128,9 @@
    9.26    val name_thm		: string * thm -> thm
    9.27    val rename_boundvars  : term -> term -> thm -> thm
    9.28    val cterm_match       : cterm * cterm ->
    9.29 -    (indexname * ctyp) list * (cterm * cterm) list
    9.30 +    (ctyp * ctyp) list * (cterm * cterm) list
    9.31    val cterm_first_order_match : cterm * cterm ->
    9.32 -    (indexname * ctyp) list * (cterm * cterm) list
    9.33 +    (ctyp * ctyp) list * (cterm * cterm) list
    9.34    val cterm_incr_indexes : int -> cterm -> cterm
    9.35    val terms_of_tpairs   : (term * term) list -> term list
    9.36  end;
    9.37 @@ -187,8 +186,6 @@
    9.38    in  Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx}
    9.39    end;
    9.40  
    9.41 -fun cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t);
    9.42 -
    9.43  
    9.44  exception CTERM of string;
    9.45  
    9.46 @@ -221,8 +218,7 @@
    9.47  fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
    9.48             (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
    9.49        if T = dty then
    9.50 -        Cterm{t = if maxidx1 >= 0 andalso maxidx2 >= 0 then Sign.nodup_vars (f $ x)
    9.51 -            else f $ x,  (*no new Vars: no expensive check!*)
    9.52 +        Cterm{t = f $ x,
    9.53            sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
    9.54            maxidx=Int.max(maxidx1, maxidx2)}
    9.55        else raise CTERM "capply: types don't agree"
    9.56 @@ -230,7 +226,7 @@
    9.57  
    9.58  fun cabs (Cterm {t=t1, sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
    9.59           (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) =
    9.60 -      Cterm {t=Sign.nodup_vars (lambda t1 t2), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2),
    9.61 +      Cterm {t = lambda t1 t2, sign_ref = Sign.merge_refs (sign_ref1,sign_ref2),
    9.62               T = T1 --> T2, maxidx=Int.max(maxidx1, maxidx2)}
    9.63        handle TERM _ => raise CTERM "cabs: first arg is not a variable";
    9.64  
    9.65 @@ -243,15 +239,18 @@
    9.66      val tsig = Sign.tsig_of (Sign.deref sign_ref);
    9.67      val (Tinsts, tinsts) = mtch tsig (t1, t2);
    9.68      val maxidx = Int.max (maxidx1, maxidx2);
    9.69 -    val vars = map dest_Var (term_vars t1);
    9.70 -    fun mk_cTinsts (ixn, T) = (ixn, Ctyp {sign_ref = sign_ref, T = T});
    9.71 -    fun mk_ctinsts (ixn, t) =
    9.72 -      let val T = typ_subst_TVars Tinsts (valOf (assoc (vars, ixn)))
    9.73 +    fun mk_cTinsts (ixn, (S, T)) =
    9.74 +      (Ctyp {sign_ref = sign_ref, T = TVar (ixn, S)},
    9.75 +       Ctyp {sign_ref = sign_ref, T = T});
    9.76 +    fun mk_ctinsts (ixn, (T, t)) =
    9.77 +      let val T = Envir.typ_subst_TVars Tinsts T
    9.78        in
    9.79          (Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = Var (ixn, T)},
    9.80           Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = t})
    9.81        end;
    9.82 -  in (map mk_cTinsts Tinsts, map mk_ctinsts tinsts) end;
    9.83 +  in (map mk_cTinsts (Vartab.dest Tinsts),
    9.84 +    map mk_ctinsts (Vartab.dest tinsts))
    9.85 +  end;
    9.86  
    9.87  val cterm_match = gen_cterm_match Pattern.match;
    9.88  val cterm_first_order_match = gen_cterm_match Pattern.first_order_match;
    9.89 @@ -417,11 +416,11 @@
    9.90  fun add_terms_sorts ([], Ss) = Ss
    9.91    | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss));
    9.92  
    9.93 -fun env_codT (Envir.Envir {iTs, ...}) = map snd (Vartab.dest iTs);
    9.94 +fun env_codT (Envir.Envir {iTs, ...}) = map (snd o snd) (Vartab.dest iTs);
    9.95  
    9.96  fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) =
    9.97 -  Vartab.foldl (add_term_sorts o swap o apsnd snd)
    9.98 -    (Vartab.foldl (add_typ_sorts o swap o apsnd snd) (Ss, iTs), asol);
    9.99 +  Vartab.foldl (add_term_sorts o swap o apsnd (snd o snd))
   9.100 +    (Vartab.foldl (add_typ_sorts o swap o apsnd (snd o snd)) (Ss, iTs), asol);
   9.101  
   9.102  fun add_insts_sorts ((iTs, is), Ss) =
   9.103    add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss));
   9.104 @@ -546,23 +545,6 @@
   9.105  
   9.106  (*** Meta rules ***)
   9.107  
   9.108 -(*Check that term does not contain same var with different typing/sorting.
   9.109 -  If this check must be made, recalculate maxidx in hope of preventing its
   9.110 -  recurrence.*)
   9.111 -fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) s =
   9.112 -  let
   9.113 -    val prop' = attach_tpairs tpairs prop;
   9.114 -    val _ = Sign.nodup_vars prop'
   9.115 -  in Thm {sign_ref = sign_ref,
   9.116 -          der = der,
   9.117 -          maxidx = maxidx_of_term prop',
   9.118 -          shyps = shyps,
   9.119 -          hyps = hyps,
   9.120 -          tpairs = tpairs,
   9.121 -          prop = prop}
   9.122 -  end handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts);
   9.123 -
   9.124 -
   9.125  (** 'primitive' rules **)
   9.126  
   9.127  (*discharge all assumptions t from ts*)
   9.128 @@ -669,7 +651,7 @@
   9.129          Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   9.130            if T<>qary then
   9.131                raise THM("forall_elim: type mismatch", 0, [th])
   9.132 -          else let val thm = fix_shyps [th] []
   9.133 +          else fix_shyps [th] []
   9.134                      (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft),
   9.135                           der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der,
   9.136                           maxidx = Int.max(maxidx, maxt),
   9.137 @@ -677,10 +659,6 @@
   9.138                           hyps = hyps,  
   9.139                           tpairs = tpairs,
   9.140                           prop = betapply(A,t)})
   9.141 -               in if maxt >= 0 andalso maxidx >= 0
   9.142 -                  then nodup_vars thm "forall_elim" 
   9.143 -                  else thm (*no new Vars: no expensive check!*)
   9.144 -               end
   9.145        | _ => raise THM("forall_elim: not quantified", 0, [th])
   9.146    end
   9.147    handle TERM _ =>
   9.148 @@ -731,7 +709,7 @@
   9.149    in case (prop1,prop2) of
   9.150         ((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) =>
   9.151            if not (u aconv u') then err"middle term"
   9.152 -          else let val thm =      
   9.153 +          else
   9.154                   Thm{sign_ref= merge_thm_sgs(th1,th2), 
   9.155                       der = Pt.infer_derivs (Pt.transitive u T) der1 der2,
   9.156                       maxidx = Int.max(max1,max2), 
   9.157 @@ -739,10 +717,6 @@
   9.158                       hyps = union_term(hyps1,hyps2),
   9.159                       tpairs = tpairs1 @ tpairs2,
   9.160                       prop = eq$t1$t2}
   9.161 -                 in if max1 >= 0 andalso max2 >= 0
   9.162 -                    then nodup_vars thm "transitive" 
   9.163 -                    else thm (*no new Vars: no expensive check!*)
   9.164 -                 end
   9.165       | _ =>  err"premises"
   9.166    end;
   9.167  
   9.168 @@ -827,8 +801,8 @@
   9.169    in case (prop1,prop2)  of
   9.170         (Const ("==", Type ("fun", [fT, _])) $ f $ g,
   9.171          Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
   9.172 -          let val _   = chktypes fT tT
   9.173 -              val thm = (*no fix_shyps*)
   9.174 +          (chktypes fT tT;
   9.175 +                        (*no fix_shyps*)
   9.176                          Thm{sign_ref = merge_thm_sgs(th1,th2), 
   9.177                              der = Pt.infer_derivs
   9.178                                (Pt.combination f g t u fT) der1 der2,
   9.179 @@ -836,11 +810,7 @@
   9.180                              shyps = Sorts.union_sort(shyps1,shyps2),
   9.181                              hyps = union_term(hyps1,hyps2),
   9.182                              tpairs = tpairs1 @ tpairs2,
   9.183 -                            prop = Logic.mk_equals(f$t, g$u)}
   9.184 -          in if max1 >= 0 andalso max2 >= 0
   9.185 -             then nodup_vars thm "combination" 
   9.186 -             else thm (*no new Vars: no expensive check!*)  
   9.187 -          end
   9.188 +                            prop = Logic.mk_equals(f$t, g$u)})
   9.189       | _ =>  raise THM("combination: premises", 0, [th1,th2])
   9.190    end;
   9.191  
   9.192 @@ -955,6 +925,8 @@
   9.193      Pretty.block [Sign.pretty_term sg t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ sg T]
   9.194    end;
   9.195  
   9.196 +fun prt_type sg_ref T = Sign.pretty_typ (Sign.deref sg_ref) T;
   9.197 +
   9.198  (*For instantiate: process pair of cterms, merge theories*)
   9.199  fun add_ctpair ((ct,cu), (sign_ref,tpairs)) =
   9.200    let
   9.201 @@ -968,9 +940,22 @@
   9.202        Pretty.fbrk, prt_typing sign_ref_merged u U]), [T,U], [t,u])
   9.203    end;
   9.204  
   9.205 -fun add_ctyp ((v,ctyp), (sign_ref',vTs)) =
   9.206 -  let val Ctyp {T,sign_ref} = ctyp
   9.207 -  in (Sign.merge_refs(sign_ref,sign_ref'), (v,T)::vTs) end;
   9.208 +fun add_ctyp ((Ctyp {T = T as TVar (_, S), sign_ref = sign_refT},
   9.209 +      Ctyp {T = U, sign_ref = sign_refU}), (sign_ref, vTs)) =
   9.210 +      let
   9.211 +        val sign_ref_merged = Sign.merge_refs
   9.212 +          (sign_ref, Sign.merge_refs (sign_refT, sign_refU));
   9.213 +        val sign = Sign.deref sign_ref_merged
   9.214 +      in
   9.215 +        if Type.of_sort (Sign.tsig_of sign) (U, S) then
   9.216 +          (sign_ref_merged, (T, U) :: vTs)
   9.217 +        else raise TYPE ("Type not of sort " ^
   9.218 +          Sign.string_of_sort sign S, [U], [])
   9.219 +      end
   9.220 +  | add_ctyp ((Ctyp {T, sign_ref}, _), _) =
   9.221 +      raise TYPE (Pretty.string_of (Pretty.block
   9.222 +        [Pretty.str "instantiate: not a type variable",
   9.223 +         Pretty.fbrk, prt_type sign_ref T]), [T], []);
   9.224  
   9.225  in
   9.226  
   9.227 @@ -982,7 +967,7 @@
   9.228    let val (newsign_ref,tpairs) = foldr add_ctpair (sign_ref,[]) ctpairs;
   9.229        val (newsign_ref,vTs) = foldr add_ctyp (newsign_ref,[]) vcTs;
   9.230        fun subst t =
   9.231 -        subst_atomic tpairs (Sign.inst_term_tvars (Sign.deref newsign_ref) vTs t);
   9.232 +        subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t);
   9.233        val newprop = subst prop;
   9.234        val newdpairs = map (pairself subst) dpairs;
   9.235        val newth =
   9.236 @@ -998,7 +983,7 @@
   9.237        then raise THM("instantiate: variables not distinct", 0, [th])
   9.238        else if not(null(findrep(map #1 vTs)))
   9.239        then raise THM("instantiate: type variables not distinct", 0, [th])
   9.240 -      else nodup_vars newth "instantiate"
   9.241 +      else newth
   9.242    end
   9.243    handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th])
   9.244         | TYPE (msg, _, _) => raise THM (msg, 0, [th]);
   9.245 @@ -1043,21 +1028,18 @@
   9.246  (* Replace all TFrees not fixed or in the hyps by new TVars *)
   9.247  fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
   9.248    let
   9.249 -    val tfrees = foldr add_term_tfree_names fixed hyps;
   9.250 +    val tfrees = foldr add_term_tfrees fixed hyps;
   9.251      val prop1 = attach_tpairs tpairs prop;
   9.252      val (prop2, al) = Type.varify (prop1, tfrees);
   9.253      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2)
   9.254 -  in let val thm = (*no fix_shyps*)
   9.255 -    Thm{sign_ref = sign_ref, 
   9.256 +  in (*no fix_shyps*)
   9.257 +   (Thm{sign_ref = sign_ref, 
   9.258          der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der,
   9.259          maxidx = Int.max(0,maxidx), 
   9.260          shyps = shyps, 
   9.261          hyps = hyps,
   9.262          tpairs = rev (map Logic.dest_equals ts),
   9.263 -        prop = prop3}
   9.264 -     in (nodup_vars thm "varifyT", al) end
   9.265 -(* this nodup_vars check can be removed if thms are guaranteed not to contain
   9.266 -duplicate TVars with different sorts *)
   9.267 +        prop = prop3}, al)
   9.268    end;
   9.269  
   9.270  val varifyT = #1 o varifyT' [];
   9.271 @@ -1324,7 +1306,7 @@
   9.272  fun norm_term_skip env 0 t = Envir.norm_term env t
   9.273    | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) =
   9.274          let val Envir.Envir{iTs, ...} = env
   9.275 -            val T' = typ_subst_TVars_Vartab iTs T
   9.276 +            val T' = Envir.typ_subst_TVars iTs T
   9.277              (*Must instantiate types of parameters because they are flattened;
   9.278                this could be a NEW parameter*)
   9.279          in  all T' $ Abs(a, T', norm_term_skip env n t)  end
    10.1 --- a/src/Pure/type.ML	Thu Apr 21 19:02:54 2005 +0200
    10.2 +++ b/src/Pure/type.ML	Thu Apr 21 19:12:03 2005 +0200
    10.3 @@ -41,18 +41,18 @@
    10.4    val no_tvars: typ -> typ
    10.5    val varifyT: typ -> typ
    10.6    val unvarifyT: typ -> typ
    10.7 -  val varify: term * string list -> term * (string * indexname) list
    10.8 +  val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list
    10.9    val freeze_thaw_type : typ -> typ * (typ -> typ)
   10.10    val freeze_thaw : term -> term * (term -> term)
   10.11  
   10.12    (*matching and unification*)
   10.13 -  val inst_typ_tvars: Pretty.pp -> tsig -> (indexname * typ) list -> typ -> typ
   10.14 -  val inst_term_tvars: Pretty.pp -> tsig -> (indexname * typ) list -> term -> term
   10.15    exception TYPE_MATCH
   10.16 -  val typ_match: tsig -> typ Vartab.table * (typ * typ) -> typ Vartab.table
   10.17 +  type tyenv
   10.18 +  val lookup: tyenv * (indexname * sort) -> typ option
   10.19 +  val typ_match: tsig -> tyenv * (typ * typ) -> tyenv
   10.20    val typ_instance: tsig -> typ * typ -> bool
   10.21    exception TUNIFY
   10.22 -  val unify: tsig -> typ Vartab.table * int -> typ * typ -> typ Vartab.table * int
   10.23 +  val unify: tsig -> tyenv * int -> typ * typ -> tyenv * int
   10.24    val raw_unify: typ * typ -> bool
   10.25  
   10.26    (*extend and merge type signatures*)
   10.27 @@ -219,11 +219,11 @@
   10.28  
   10.29  fun varify (t, fixed) =
   10.30    let
   10.31 -    val fs = add_term_tfree_names (t, []) \\ fixed;
   10.32 +    val fs = add_term_tfrees (t, []) \\ fixed;
   10.33      val ixns = add_term_tvar_ixns (t, []);
   10.34 -    val fmap = fs ~~ map (rpair 0) (variantlist (fs, map #1 ixns))
   10.35 +    val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
   10.36      fun thaw (f as (a, S)) =
   10.37 -      (case assoc (fmap, a) of
   10.38 +      (case assoc (fmap, f) of
   10.39          NONE => TFree f
   10.40        | SOME b => TVar (b, S));
   10.41    in (map_term_types (map_type_tfree thaw) t, fmap) end;
   10.42 @@ -273,21 +273,15 @@
   10.43  
   10.44  (** matching and unification of types **)
   10.45  
   10.46 -(* instantiation *)
   10.47 +type tyenv = (sort * typ) Vartab.table;
   10.48  
   10.49 -fun inst_typ_tvars pp tsig tye =
   10.50 -  let
   10.51 -    fun inst (var as (v, S)) =
   10.52 -      (case assoc_string_int (tye, v) of
   10.53 -        SOME U =>
   10.54 -          if of_sort tsig (U, S) then U
   10.55 -          else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [U], [])
   10.56 -      | NONE => TVar var);
   10.57 -  in map_type_tvar inst end;
   10.58 +fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
   10.59 +  quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
   10.60 +  [TVar (ixn, S), TVar (ixn, S')], []);
   10.61  
   10.62 -fun inst_term_tvars _ _ [] t = t
   10.63 -  | inst_term_tvars pp tsig tye t = map_term_types (inst_typ_tvars pp tsig tye) t;
   10.64 -
   10.65 +fun lookup (tye, (ixn, S)) = case Vartab.lookup (tye, ixn) of
   10.66 +    NONE => NONE
   10.67 +  | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S';
   10.68  
   10.69  (* matching *)
   10.70  
   10.71 @@ -296,9 +290,9 @@
   10.72  fun typ_match tsig =
   10.73    let
   10.74      fun match (subs, (TVar (v, S), T)) =
   10.75 -          (case Vartab.lookup (subs, v) of
   10.76 +          (case lookup (subs, (v, S)) of
   10.77              NONE =>
   10.78 -              if of_sort tsig (T, S) then Vartab.update ((v, T), subs)
   10.79 +              if of_sort tsig (T, S) then Vartab.update_new ((v, (S, T)), subs)
   10.80                else raise TYPE_MATCH
   10.81            | SOME U => if U = T then subs else raise TYPE_MATCH)
   10.82        | match (subs, (Type (a, Ts), Type (b, Us))) =
   10.83 @@ -322,16 +316,16 @@
   10.84    let
   10.85      fun occ (Type (_, Ts)) = exists occ Ts
   10.86        | occ (TFree _) = false
   10.87 -      | occ (TVar (w, _)) =
   10.88 +      | occ (TVar (w, S)) =
   10.89            eq_ix (v, w) orelse
   10.90 -            (case Vartab.lookup (tye, w) of
   10.91 +            (case lookup (tye, (w, S)) of
   10.92                NONE => false
   10.93              | SOME U => occ U);
   10.94    in occ end;
   10.95  
   10.96  (*chase variable assignments; if devar returns a type var then it must be unassigned*)
   10.97 -fun devar (T as TVar (v, _), tye) =
   10.98 -      (case  Vartab.lookup (tye, v) of
   10.99 +fun devar (T as TVar v, tye) =
  10.100 +      (case  lookup (tye, v) of
  10.101          SOME U => devar (U, tye)
  10.102        | NONE => T)
  10.103    | devar (T, tye) = T;
  10.104 @@ -347,8 +341,8 @@
  10.105      fun meet ((_, []), tye) = tye
  10.106        | meet ((TVar (xi, S'), S), tye) =
  10.107            if Sorts.sort_le classes (S', S) then tye
  10.108 -          else Vartab.update_new ((xi,
  10.109 -            gen_tyvar (Sorts.inter_sort classes (S', S))), tye)
  10.110 +          else Vartab.update_new ((xi, (S',
  10.111 +            gen_tyvar (Sorts.inter_sort classes (S', S)))), tye)
  10.112        | meet ((TFree (_, S'), S), tye) =
  10.113            if Sorts.sort_le classes (S', S) then tye
  10.114            else raise TUNIFY
  10.115 @@ -361,21 +355,22 @@
  10.116      fun unif ((ty1, ty2), tye) =
  10.117        (case (devar (ty1, tye), devar (ty2, tye)) of
  10.118          (T as TVar (v, S1), U as TVar (w, S2)) =>
  10.119 -          if eq_ix (v, w) then tye
  10.120 +          if eq_ix (v, w) then
  10.121 +            if S1 = S2 then tye else tvar_clash v S1 S2
  10.122            else if Sorts.sort_le classes (S1, S2) then
  10.123 -            Vartab.update_new ((w, T), tye)
  10.124 +            Vartab.update_new ((w, (S2, T)), tye)
  10.125            else if Sorts.sort_le classes (S2, S1) then
  10.126 -            Vartab.update_new ((v, U), tye)
  10.127 +            Vartab.update_new ((v, (S1, U)), tye)
  10.128            else
  10.129              let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in
  10.130 -              Vartab.update_new ((v, S), Vartab.update_new ((w, S), tye))
  10.131 +              Vartab.update_new ((v, (S1, S)), Vartab.update_new ((w, (S2, S)), tye))
  10.132              end
  10.133        | (TVar (v, S), T) =>
  10.134            if occurs v tye T then raise TUNIFY
  10.135 -          else meet ((T, S), Vartab.update_new ((v, T), tye))
  10.136 +          else meet ((T, S), Vartab.update_new ((v, (S, T)), tye))
  10.137        | (T, TVar (v, S)) =>
  10.138            if occurs v tye T then raise TUNIFY
  10.139 -          else meet ((T, S), Vartab.update_new ((v, T), tye))
  10.140 +          else meet ((T, S), Vartab.update_new ((v, (S, T)), tye))
  10.141        | (Type (a, Ts), Type (b, Us)) =>
  10.142            if a <> b then raise TUNIFY
  10.143            else foldr unif tye (Ts ~~ Us)
    11.1 --- a/src/Pure/unify.ML	Thu Apr 21 19:02:54 2005 +0200
    11.2 +++ b/src/Pure/unify.ML	Thu Apr 21 19:12:03 2005 +0200
    11.3 @@ -1,13 +1,10 @@
    11.4 -(*  Title: 	unify
    11.5 +(*  Title:      Pure/unify.ML
    11.6      ID:         $Id$
    11.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    11.8      Copyright   Cambridge University 1992
    11.9  
   11.10  Higher-Order Unification
   11.11  
   11.12 -Potential problem: type of Vars is often ignored, so two Vars with same
   11.13 -indexname but different types can cause errors!
   11.14 -
   11.15  Types as well as terms are unified.  The outermost functions assume the
   11.16  terms to be unified already have the same type.  In resolution, this is
   11.17  assured because both have type "prop".
   11.18 @@ -49,14 +46,14 @@
   11.19  
   11.20  fun body_type(Envir.Envir{iTs,...}) = 
   11.21  let fun bT(Type("fun",[_,T])) = bT T
   11.22 -      | bT(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
   11.23 +      | bT(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
   11.24  		NONE => T | SOME(T') => bT T')
   11.25        | bT T = T
   11.26  in bT end;
   11.27  
   11.28  fun binder_types(Envir.Envir{iTs,...}) = 
   11.29  let fun bTs(Type("fun",[T,U])) = T :: bTs U
   11.30 -      | bTs(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
   11.31 +      | bTs(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
   11.32  		NONE => [] | SOME(T') => bTs T')
   11.33        | bTs _ = []
   11.34  in bTs end;
   11.35 @@ -70,8 +67,8 @@
   11.36  fun eta_norm(env as Envir.Envir{iTs,...}) =
   11.37    let fun etif (Type("fun",[T,U]), t) =
   11.38  	    Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
   11.39 -	| etif (TVar(ixn,_),t) = 
   11.40 -	    (case Vartab.lookup (iTs,ixn) of
   11.41 +	| etif (TVar ixnS, t) = 
   11.42 +	    (case Type.lookup (iTs, ixnS) of
   11.43  		  NONE => t | SOME(T) => etif(T,t))
   11.44  	| etif (_,t) = t;
   11.45        fun eta_nm (rbinder, Abs(a,T,body)) =
   11.46 @@ -84,7 +81,11 @@
   11.47    Does the uvar occur in the term t?  
   11.48    two forms of search, for whether there is a rigid path to the current term.
   11.49    "seen" is list of variables passed thru, is a memo variable for sharing.
   11.50 -  This version searches for nonrigid occurrence, returns true if found. *)
   11.51 +  This version searches for nonrigid occurrence, returns true if found.
   11.52 +  Since terms may contain variables with same name and different types,
   11.53 +  the occurs check must ignore the types of variables. This avoids
   11.54 +  that ?x::?'a is unified with f(?x::T), which may lead to a cyclic
   11.55 +  substitution when ?'a is instantiated with T later. *)
   11.56  fun occurs_terms (seen: (indexname list) ref,
   11.57   		  env: Envir.env, v: indexname, ts: term list): bool =
   11.58    let fun occurs [] = false
   11.59 @@ -92,12 +93,12 @@
   11.60        and occur (Const _)  = false
   11.61  	| occur (Bound _)  = false
   11.62  	| occur (Free _)  = false
   11.63 -	| occur (Var (w,_))  = 
   11.64 +	| occur (Var (w, T))  = 
   11.65  	    if mem_ix (w, !seen) then false
   11.66  	    else if eq_ix(v,w) then true
   11.67  	      (*no need to lookup: v has no assignment*)
   11.68  	    else (seen := w:: !seen;  
   11.69 -	          case  Envir.lookup(env,w)  of
   11.70 +	          case Envir.lookup (env, (w, T)) of
   11.71  		      NONE    => false
   11.72  		    | SOME t => occur t)
   11.73  	| occur (Abs(_,_,body)) = occur body
   11.74 @@ -109,7 +110,7 @@
   11.75  (* f(a1,...,an)  ---->   (f,  [a1,...,an])  using the assignments*)
   11.76  fun head_of_in (env,t) : term = case t of
   11.77      f$_ => head_of_in(env,f)
   11.78 -  | Var (v,_) => (case  Envir.lookup(env,v)  of  
   11.79 +  | Var vT => (case Envir.lookup (env, vT) of  
   11.80  			SOME u => head_of_in(env,u)  |  NONE   => t)
   11.81    | _ => t;
   11.82  
   11.83 @@ -155,11 +156,11 @@
   11.84        and occur (Const _)  = NoOcc
   11.85  	| occur (Bound _)  = NoOcc
   11.86  	| occur (Free _)  = NoOcc
   11.87 -	| occur (Var (w,_))  = 
   11.88 +	| occur (Var (w, T))  = 
   11.89  	    if mem_ix (w, !seen) then NoOcc
   11.90  	    else if eq_ix(v,w) then Rigid
   11.91  	    else (seen := w:: !seen;  
   11.92 -	          case  Envir.lookup(env,w)  of
   11.93 +	          case Envir.lookup (env, (w, T)) of
   11.94  		      NONE    => NoOcc
   11.95  		    | SOME t => occur t)
   11.96  	| occur (Abs(_,_,body)) = occur body
   11.97 @@ -210,11 +211,11 @@
   11.98    If v occurs rigidly then nonunifiable.
   11.99    If v occurs nonrigidly then must use full algorithm. *)
  11.100  fun assignment (env, rbinder, t, u) =
  11.101 -    let val (v,T) = get_eta_var(rbinder,0,t)
  11.102 -    in  case rigid_occurs_term (ref[], env, v, u) of
  11.103 +    let val vT as (v,T) = get_eta_var (rbinder, 0, t)
  11.104 +    in  case rigid_occurs_term (ref [], env, v, u) of
  11.105  	      NoOcc => let val env = unify_types(body_type env T,
  11.106  						 fastype env (rbinder,u),env)
  11.107 -		in Envir.update ((v, rlist_abs(rbinder,u)), env) end
  11.108 +		in Envir.update ((vT, rlist_abs (rbinder, u)), env) end
  11.109  	    | Nonrigid =>  raise ASSIGN
  11.110  	    | Rigid =>  raise CANTUNIFY
  11.111      end;
  11.112 @@ -282,7 +283,7 @@
  11.113  
  11.114  (* changed(env,t) checks whether the head of t is a variable assigned in env*)
  11.115  fun changed (env, f$_) = changed (env,f)
  11.116 -  | changed (env, Var (v,_)) =
  11.117 +  | changed (env, Var v) =
  11.118        (case Envir.lookup(env,v) of NONE=>false  |  _ => true)
  11.119    | changed _ = false;
  11.120  
  11.121 @@ -395,12 +396,12 @@
  11.122  (*Call matchcopy to produce assignments to the variable in the dpair*)
  11.123  fun MATCH (env, (rbinder,t,u), dpairs)
  11.124  	: (Envir.env * dpair list)Seq.seq = 
  11.125 -  let val (Var(v,T), targs) = strip_comb t;
  11.126 +  let val (Var (vT as (v, T)), targs) = strip_comb t;
  11.127        val Ts = binder_types env T;
  11.128        fun new_dset (u', (env',dpairs')) =
  11.129  	  (*if v was updated to s, must unify s with u' *)
  11.130 -	  case Envir.lookup(env',v) of
  11.131 -	      NONE => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
  11.132 +	  case Envir.lookup (env', vT) of
  11.133 +	      NONE => (Envir.update ((vT, types_abs(Ts, u')), env'),  dpairs')
  11.134  	    | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs')
  11.135    in Seq.map new_dset
  11.136           (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
  11.137 @@ -413,12 +414,12 @@
  11.138  (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) 
  11.139    Attempts to update t with u, raising ASSIGN if impossible*)
  11.140  fun ff_assign(env, rbinder, t, u) : Envir.env = 
  11.141 -let val (v,T) = get_eta_var(rbinder,0,t)
  11.142 -in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
  11.143 +let val vT as (v,T) = get_eta_var(rbinder,0,t)
  11.144 +in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN
  11.145     else let val env = unify_types(body_type env T,
  11.146  				  fastype env (rbinder,u),
  11.147  				  env)
  11.148 -	in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
  11.149 +	in Envir.vupdate ((vT, rlist_abs (rbinder, u)), env) end
  11.150  end;
  11.151  
  11.152  
  11.153 @@ -494,7 +495,7 @@
  11.154      if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
  11.155      else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
  11.156  	     val body = list_comb(v', map (Bound o #j) args)
  11.157 -	     val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
  11.158 +	     val env2 = Envir.vupdate ((((v, T), types_abs(Ts, body)),   env'))
  11.159  	     (*the vupdate affects ts' if they contain v*)
  11.160  	 in  
  11.161  	     (env2, Envir.norm_term env2 (list_comb(v',ts')))
  11.162 @@ -615,12 +616,12 @@
  11.163      requires more work yet gives a less general unifier (fewer variables).
  11.164    Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
  11.165  fun smash_flexflex1 ((t,u), env) : Envir.env =
  11.166 -  let val (v,T) = var_head_of (env,t)
  11.167 -      and (w,U) = var_head_of (env,u);
  11.168 +  let val vT as (v,T) = var_head_of (env,t)
  11.169 +      and wU as (w,U) = var_head_of (env,u);
  11.170        val (env', var) = Envir.genvar (#1v) (env, body_type env T)
  11.171 -      val env'' = Envir.vupdate((w, type_abs(env',U,var)),  env')
  11.172 -  in  if (v,T)=(w,U) then env''  (*the other update would be identical*)
  11.173 -      else Envir.vupdate((v, type_abs(env',T,var)), env'')
  11.174 +      val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env')
  11.175 +  in  if vT = wU then env''  (*the other update would be identical*)
  11.176 +      else Envir.vupdate ((vT, type_abs (env', T, var)), env'')
  11.177    end;
  11.178  
  11.179