# HG changeset patch
# User wenzelm
# Date 1122556800 -7200
# Node ID ba05effdec42be9067a12b803d39a1f64cd19816
# Parent  c01816b32c045e1c5fe0011422a0501eff6181c0
added add_tfreesT, add_tfrees;
added bound;
added zero_var_indexesT, zero_var_indexes, zero_var_indexes_subst;
removed add_term_constsT;
tuned;

diff -r c01816b32c04 -r ba05effdec42 src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Jul 28 15:19:59 2005 +0200
+++ b/src/Pure/term.ML	Thu Jul 28 15:20:00 2005 +0200
@@ -68,6 +68,13 @@
   val map_type_tfree: (string * sort -> typ) -> typ -> typ
   val map_term_types: (typ -> typ) -> term -> term
   val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
+  val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
+  val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
+  val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
+  val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
+  val add_term_names: term * string list -> string list
+  val add_term_varnames: term -> indexname list -> indexname list
+  val term_varnames: term -> indexname list
   val aconv: term * term -> bool
   val aconvs: term list * term list -> bool
   structure Vartab: TABLE
@@ -127,12 +134,9 @@
   val add_term_classes: term * class list -> class list
   val add_term_tycons: term * string list -> string list
   val add_term_consts: term * string list -> string list
-  val add_term_constsT: term * (string * typ) list -> (string * typ) list
   val term_consts: term -> string list
-  val term_constsT: term -> (string * typ) list
+  val exists_subterm: (term -> bool) -> term -> bool
   val exists_Const: (string * typ -> bool) -> term -> bool
-  val exists_subterm: (term -> bool) -> term -> bool
-  val add_new_id: string list * string -> string list
   val add_term_free_names: term * string list -> string list
   val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   val add_typ_tfree_names: typ * string list -> string list
@@ -156,13 +160,6 @@
   val term_frees: term -> term list
   val variant_abs: string * typ * term -> string * term
   val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
-  val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
-  val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
-  val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
-  val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
-  val add_term_names: term * string list -> string list
-  val add_term_varnames: term -> indexname list -> indexname list
-  val term_varnames: term -> indexname list
   val compress_type: typ -> typ
   val compress_term: term -> term
   val show_question_marks: bool ref
@@ -172,6 +169,12 @@
 sig
   include BASIC_TERM
   val argument_type_of: term -> typ
+  val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
+  val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
+  val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
+  val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
+  val add_tfrees: term -> (string * sort) list -> (string * sort) list
+  val add_frees: term -> (string * typ) list -> (string * typ) list
   val fast_indexname_ord: indexname * indexname -> order
   val indexname_ord: indexname * indexname -> order
   val sort_ord: sort * sort -> order
@@ -183,8 +186,10 @@
   val term_lpo: (string -> int) -> term * term -> order
   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   val rename_abs: term -> term -> term -> term option
+  val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   val eq_var: (indexname * typ) * (indexname * typ) -> bool
-  val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
+  val tvar_ord: (indexname * sort) * (indexname * sort) -> order
+  val var_ord: (indexname * typ) * (indexname * typ) -> order
   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
     -> term -> term
   val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
@@ -195,10 +200,11 @@
   val map_typ: (string -> string) -> (string -> string) -> typ -> typ
   val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
   val dest_abs: string * typ * term -> string * term
-  val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
-  val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
-  val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
-  val add_frees: term -> (string * typ) list -> (string * typ) list
+  val bound: int -> string -> string
+  val zero_var_indexesT: typ -> typ
+  val zero_var_indexes: term -> term
+  val zero_var_indexes_inst: term ->
+    ((indexname * sort) * typ) list * ((indexname * typ) * term) list
   val dummy_patternN: string
   val no_dummy_patterns: term -> term
   val replace_dummy_patterns: int * term -> int * term
@@ -466,6 +472,40 @@
 in iter end
 
 
+(* fold types and terms *)
+
+(*fold atoms of type*)
+fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
+  | fold_atyps f T = f T;
+
+(*fold atoms of term*)
+fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
+  | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
+  | fold_aterms f a = f a;
+
+(*fold types of term*)
+fun fold_term_types f (t as Const (_, T)) = f t T
+  | fold_term_types f (t as Free (_, T)) = f t T
+  | fold_term_types f (t as Var (_, T)) = f t T
+  | fold_term_types f (Bound _) = I
+  | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
+  | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
+
+fun fold_types f = fold_term_types (K f);
+
+(*collect variables*)
+val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
+val add_tvars = fold_types add_tvarsT;
+val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
+val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
+val add_tfrees = fold_types add_tfreesT;
+val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
+
+(*collect variable names*)
+val add_term_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
+fun term_varnames t = add_term_varnames t [];
+
+
 (** Comparing terms, types, sorts etc. **)
 
 (* fast syntactic comparison *)
@@ -584,14 +624,8 @@
     | (t, u) =>
         (case int_ord (size_of_term t, size_of_term u) of
           EQUAL =>
-            let
-              val (f, m) = hd_depth (t, 0)
-              and (g, n) = hd_depth (u, 0);
-            in
-              (case hd_ord (f, g) of EQUAL =>
-                (case int_ord (m, n) of EQUAL => args_ord (t, u) | ord => ord)
-              | ord => ord)
-            end
+            (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
+              EQUAL => args_ord (t, u) | ord => ord)
         | ord => ord))
 and hd_ord (f, g) =
   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
@@ -781,8 +815,11 @@
 
 (* variables *)
 
-fun eq_var ((xi, T: typ), (yj, U)) = eq_ix (xi, yj) andalso T = U;
-fun eq_tvar ((xi, S: sort), (yj, S')) = eq_ix (xi, yj) andalso S = S';
+fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
+fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
+
+val tvar_ord = prod_ord indexname_ord sort_ord;
+val var_ord = prod_ord indexname_ord typ_ord;
 
 
 (* terms *)
@@ -933,12 +970,12 @@
       in subst tm end;
 
 
-(* efficient substitution of schematic variables *)
+(* instantiation of schematic variables (types before terms) *)
 
 local exception SAME in
 
-fun substT [] _ = raise SAME
-  | substT instT ty =
+fun instantiateT_same [] _ = raise SAME
+  | instantiateT_same instT ty =
       let
         fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
           | subst_typ (TVar v) =
@@ -955,23 +992,24 @@
 fun instantiate ([], []) tm = tm
   | instantiate (instT, inst) tm =
       let
-        fun subst (Const (c, T)) = Const (c, substT instT T)
-          | subst (Free (x, T)) = Free (x, substT instT T)
+        val substT = instantiateT_same instT;
+        fun subst (Const (c, T)) = Const (c, substT T)
+          | subst (Free (x, T)) = Free (x, substT T)
           | subst (Var (xi, T)) =
-              let val (T', same) = (substT instT T, false) handle SAME => (T, true) in
+              let val (T', same) = (substT T, false) handle SAME => (T, true) in
                 (case gen_assoc eq_var (inst, (xi, T')) of
                    SOME t => t
                  | NONE => if same then raise SAME else Var (xi, T'))
               end
           | subst (Bound _) = raise SAME
           | subst (Abs (x, T, t)) =
-              (Abs (x, substT instT T, subst t handle SAME => t)
+              (Abs (x, substT T, subst t handle SAME => t)
                 handle SAME => Abs (x, T, subst t))
           | subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u);
       in subst tm handle SAME => tm end;
 
 fun instantiateT instT ty =
-  substT instT ty handle SAME => ty;
+  instantiateT_same instT ty handle SAME => ty;
 
 end;
 
@@ -1025,14 +1063,14 @@
 
 (*** Printing ***)
 
-(*Makes a variant of a name distinct from the names in bs.
+(*Makes a variant of a name distinct from the names in 'used'.
   First attaches the suffix and then increments this;
   preserves a suffix of underscores "_". *)
-fun variant bs name =
+fun variant used name =
   let
     val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
-    fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c;
-    fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_init c) else c;
+    fun vary2 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_string c) else c;
+    fun vary1 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_init c) else c;
   in vary1 (if c = "" then "u" else c) ^ u end;
 
 (*Create variants of the list of names, with priority to the first ones*)
@@ -1067,29 +1105,18 @@
   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
   | add_term_consts (_, cs) = cs;
 
-fun add_term_constsT (Const c, cs) = c::cs
-  | add_term_constsT (t $ u, cs) = add_term_constsT (t, add_term_constsT (u, cs))
-  | add_term_constsT (Abs (_, _, t), cs) = add_term_constsT (t, cs)
-  | add_term_constsT (_, cs) = cs;
-
 fun term_consts t = add_term_consts(t,[]);
 
-fun term_constsT t = add_term_constsT(t,[]);
+fun exists_subterm P =
+  let
+    fun ex tm = P tm orelse
+      (case tm of
+        t $ u => ex t orelse ex u
+      | Abs (_, _, t) => ex t
+      | _ => false);
+  in ex end;
 
-fun exists_Const P t = let
-        fun ex (Const c      ) = P c
-        |   ex (t $ u        ) = ex t orelse ex u
-        |   ex (Abs (_, _, t)) = ex t
-        |   ex _               = false
-    in ex t end;
-
-fun exists_subterm P =
-  let fun ex t = P t orelse
-                 (case t of
-                    u $ v        => ex u orelse ex v
-                  | Abs(_, _, u) => ex u
-                  | _            => false)
-  in ex end;
+fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
 
 (*map classes, tycons*)
 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
@@ -1107,9 +1134,6 @@
 
 (** TFrees and TVars **)
 
-(*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)
-fun add_new_id (bs, c) : string list =  variant bs c  ::  bs;
-
 (*Accumulates the names of Frees in the term, suppressing duplicates.*)
 fun add_term_free_names (Free(a,_), bs) = a ins_string bs
   | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
@@ -1228,6 +1252,8 @@
     else (x, subst_bound (Free (x, T), body))
   end;
 
+fun bound bounds x = "." ^ x ^ "." ^ string_of_int bounds;
+
 (* renames and reverses the strings in vars away from names *)
 fun rename_aTs names vars : (string*typ)list =
   let fun rename_aT (vars,(a,T)) =
@@ -1237,36 +1263,28 @@
 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
 
 
-(* left-ro-right traversal *)
+(* zero var indexes *)
 
-(*fold atoms of type*)
-fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
-  | fold_atyps f T = f T;
-
-(*fold atoms of term*)
-fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
-  | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
-  | fold_aterms f a = f a;
+fun zero_var_inst vars =
+  fold (fn v as ((x, i), X) => fn (used, inst) =>
+    let
+      val x' = variant used x;
+      val used' = x' :: used;
+    in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end)
+  vars ([], []) |> #2;
 
-(*fold types of term*)
-fun fold_term_types f (t as Const (_, T)) = f t T
-  | fold_term_types f (t as Free (_, T)) = f t T
-  | fold_term_types f (t as Var (_, T)) = f t T
-  | fold_term_types f (Bound _) = I
-  | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
-  | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
-
-fun fold_types f = fold_term_types (K f);
+fun zero_var_indexesT ty =
+  instantiateT (map (apsnd TVar) (zero_var_inst (sort tvar_ord (add_tvarsT ty [])))) ty;
 
-(*collect variables*)
-val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
-val add_tvars = fold_types add_tvarsT;
-val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
-val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
+fun zero_var_indexes_inst tm =
+  let
+    val instT = map (apsnd TVar) (zero_var_inst (sort tvar_ord (fold_types add_tvarsT tm [])));
+    val inst =
+      add_vars tm [] |> map (apsnd (instantiateT instT))
+      |> sort var_ord |> zero_var_inst |> map (apsnd Var);
+  in (instT, inst) end;
 
-(*collect variable names*)
-val add_term_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
-fun term_varnames t = add_term_varnames t [];
+fun zero_var_indexes tm = instantiate (zero_var_indexes_inst tm) tm;