declare_term_names: cover types as well;
authorwenzelm
Thu Jul 27 23:28:23 2006 +0200 (2006-07-27)
changeset 20239620a3f297072
parent 20238 7e17d70a9303
child 20240 a7b027328d6e
declare_term_names: cover types as well;
removed unused zero_var_indexesT;
tuned;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Thu Jul 27 15:33:21 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Jul 27 23:28:23 2006 +0200
     1.3 @@ -188,10 +188,9 @@
     1.4    val maxidx_typ: typ -> int -> int
     1.5    val maxidx_typs: typ list -> int -> int
     1.6    val maxidx_term: term -> int -> int
     1.7 +  val dest_abs: string * typ * term -> string * term
     1.8    val declare_term_names: term -> Name.context -> Name.context
     1.9 -  val dest_abs: string * typ * term -> string * term
    1.10    val variant_frees: term -> (string * 'a) list -> (string * 'a) list
    1.11 -  val zero_var_indexesT: typ -> typ
    1.12    val zero_var_indexes: term -> term
    1.13    val zero_var_indexes_inst: term ->
    1.14      ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    1.15 @@ -1145,11 +1144,6 @@
    1.16    | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
    1.17    | add_term_names (_, bs) = bs;
    1.18  
    1.19 -val declare_term_names = fold_aterms
    1.20 -  (fn Const (a, _) => Name.declare (NameSpace.base a)     (*expensive*)
    1.21 -    | Free (a, _) => Name.declare a
    1.22 -    | _ => I);
    1.23 -
    1.24  (*Accumulates the TVars in a type, suppressing duplicates. *)
    1.25  fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
    1.26    | add_typ_tvars(TFree(_),vs) = vs
    1.27 @@ -1238,6 +1232,13 @@
    1.28  
    1.29  (* renaming variables *)
    1.30  
    1.31 +fun declare_term_names tm =
    1.32 +  fold_aterms
    1.33 +    (fn Const (a, _) => Name.declare (NameSpace.base a)
    1.34 +      | Free (a, _) => Name.declare a
    1.35 +      | _ => I) tm #>
    1.36 +  fold_types (fold_atyps (fn TFree (a, _) => Name.declare a | _ => I)) tm;
    1.37 +
    1.38  fun variant_frees t frees =
    1.39    fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
    1.40  
    1.41 @@ -1247,21 +1248,17 @@
    1.42  (* zero var indexes *)
    1.43  
    1.44  fun zero_var_inst vars =
    1.45 -  fold (fn v as ((x, i), X) => fn (used, inst) =>
    1.46 +  fold (fn v as ((x, i), X) => fn (inst, used) =>
    1.47      let
    1.48        val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used;
    1.49 -    in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end)
    1.50 -  vars (Name.context, []) |> #2;
    1.51 -
    1.52 -fun zero_var_indexesT ty =
    1.53 -  instantiateT (map (apsnd TVar) (zero_var_inst (sort tvar_ord (add_tvarsT ty [])))) ty;
    1.54 +    in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end)
    1.55 +  vars ([], Name.context) |> #1;
    1.56  
    1.57  fun zero_var_indexes_inst tm =
    1.58    let
    1.59 -    val instT = map (apsnd TVar) (zero_var_inst (sort tvar_ord (fold_types add_tvarsT tm [])));
    1.60 -    val inst =
    1.61 -      add_vars tm [] |> map (apsnd (instantiateT instT))
    1.62 -      |> sort var_ord |> zero_var_inst |> map (apsnd Var);
    1.63 +    val instT = zero_var_inst (sort tvar_ord (add_tvars tm [])) |> map (apsnd TVar);
    1.64 +    val inst = zero_var_inst (sort var_ord (map (apsnd (instantiateT instT)) (add_vars tm [])))
    1.65 +      |> map (apsnd Var);
    1.66    in (instT, inst) end;
    1.67  
    1.68  fun zero_var_indexes tm = instantiate (zero_var_indexes_inst tm) tm;