removed obsolete ins_ix, mem_ix, ins_term, mem_term;
authorwenzelm
Tue Jul 11 12:17:07 2006 +0200 (2006-07-11)
changeset 20082b0f5981b9267
parent 20081 c9da24b69fda
child 20083 717b1eb434f1
removed obsolete ins_ix, mem_ix, ins_term, mem_term;
moved variant(list), invent_names, bound, dest_internal/skolem etc. to name.ML;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Tue Jul 11 12:17:06 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Tue Jul 11 12:17:07 2006 +0200
     1.3 @@ -101,10 +101,6 @@
     1.4    val betapply: term * term -> term
     1.5    val betapplys: term * term list -> term
     1.6    val eq_ix: indexname * indexname -> bool
     1.7 -  val ins_ix: indexname * indexname list -> indexname list
     1.8 -  val mem_ix: indexname * indexname list -> bool
     1.9 -  val mem_term: term * term list -> bool
    1.10 -  val ins_term: term * term list -> term list
    1.11    val could_unify: term * term -> bool
    1.12    val subst_free: (term * term) list -> term -> term
    1.13    val xless: (string * int) * indexname -> bool
    1.14 @@ -126,9 +122,6 @@
    1.15    val maxidx_of_typ: typ -> int
    1.16    val maxidx_of_typs: typ list -> int
    1.17    val maxidx_of_term: term -> int
    1.18 -  val variant: string list -> string -> string
    1.19 -  val variantlist: string list * string list -> string list
    1.20 -    (*note reversed order of args wrt. variant!*)
    1.21    val add_term_consts: term * string list -> string list
    1.22    val term_consts: term -> string list
    1.23    val exists_subtype: (typ -> bool) -> typ -> bool
    1.24 @@ -186,10 +179,6 @@
    1.25    val eq_var: (indexname * typ) * (indexname * typ) -> bool
    1.26    val tvar_ord: (indexname * sort) * (indexname * sort) -> order
    1.27    val var_ord: (indexname * typ) * (indexname * typ) -> order
    1.28 -  val internal: string -> string
    1.29 -  val dest_internal: string -> string
    1.30 -  val skolem: string -> string
    1.31 -  val dest_skolem: string -> string
    1.32    val generalize: string list * string list -> int -> term -> term
    1.33    val generalizeT: string list -> int -> typ -> typ
    1.34    val generalize_option: string list * string list -> int -> term -> term option
    1.35 @@ -203,11 +192,7 @@
    1.36    val maxidx_typ: typ -> int -> int
    1.37    val maxidx_typs: typ list -> int -> int
    1.38    val maxidx_term: term -> int -> int
    1.39 -  val variant_name: (string -> bool) -> string -> string
    1.40 -  val invent_names: string list -> string -> int -> string list
    1.41    val dest_abs: string * typ * term -> string * term
    1.42 -  val bound: int -> string
    1.43 -  val is_bound: string -> bool
    1.44    val zero_var_indexesT: typ -> typ
    1.45    val zero_var_indexes: term -> term
    1.46    val zero_var_indexes_inst: term ->
    1.47 @@ -830,18 +815,10 @@
    1.48  
    1.49  (** Specialized equality, membership, insertion etc. **)
    1.50  
    1.51 -(* indexnames *)
    1.52 +(* variables *)
    1.53  
    1.54  fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
    1.55  
    1.56 -fun mem_ix (_, []) = false
    1.57 -  | mem_ix (x, y :: ys) = eq_ix (x, y) orelse mem_ix (x, ys);
    1.58 -
    1.59 -fun ins_ix (x, xs) = if mem_ix (x, xs) then xs else x :: xs;
    1.60 -
    1.61 -
    1.62 -(* variables *)
    1.63 -
    1.64  fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
    1.65  fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
    1.66  
    1.67 @@ -849,14 +826,6 @@
    1.68  val var_ord = prod_ord indexname_ord typ_ord;
    1.69  
    1.70  
    1.71 -(* terms *)
    1.72 -
    1.73 -fun mem_term (_, []) = false
    1.74 -  | mem_term (t, t'::ts) = t aconv t' orelse mem_term (t, ts);
    1.75 -
    1.76 -fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
    1.77 -
    1.78 -
    1.79  (*A fast unification filter: true unless the two terms cannot be unified.
    1.80    Terms must be NORMAL.  Treats all Vars as distinct. *)
    1.81  fun could_unify (t,u) =
    1.82 @@ -986,15 +955,6 @@
    1.83        in subst tm end;
    1.84  
    1.85  
    1.86 -(* internal identifiers *)
    1.87 -
    1.88 -val internal = suffix "_";
    1.89 -val dest_internal = unsuffix "_";
    1.90 -
    1.91 -val skolem = suffix "__";
    1.92 -val dest_skolem = unsuffix "__";
    1.93 -
    1.94 -
    1.95  (* generalization of fixed variables *)
    1.96  
    1.97  local exception SAME in
    1.98 @@ -1016,14 +976,10 @@
    1.99  fun generalize_same ([], []) _ _ = raise SAME
   1.100    | generalize_same (tfrees, frees) idx tm =
   1.101        let
   1.102 -        fun var ((x, i), T) =
   1.103 -          (case try dest_internal x of
   1.104 -            NONE => Var ((x, i), T)
   1.105 -          | SOME x' => var ((x', i + 1), T));
   1.106 -
   1.107          val genT = generalizeT_same tfrees idx;
   1.108          fun gen (Free (x, T)) =
   1.109 -              if member (op =) frees x then var ((x, idx), genT T handle SAME => T)
   1.110 +              if member (op =) frees x then
   1.111 +                Var (Name.clean_index (x, idx), genT T handle SAME => T)
   1.112                else Free (x, genT T)
   1.113            | gen (Var (xi, T)) = Var (xi, genT T)
   1.114            | gen (Const (c, T)) = Const (c, genT T)
   1.115 @@ -1137,35 +1093,6 @@
   1.116  
   1.117  (**** Syntax-related declarations ****)
   1.118  
   1.119 -(*** Printing ***)
   1.120 -
   1.121 -(*Makes a variant of a name distinct from already used names.  First
   1.122 -  attaches the suffix and then increments this; preserves a suffix of
   1.123 -  underscores "_". *)
   1.124 -fun variant_name used name =
   1.125 -  let
   1.126 -    val (c, u) = pairself implode (Library.take_suffix (fn s => s = "_") (Symbol.explode name));
   1.127 -    fun vary2 c = if used (c ^ u) then vary2 (Symbol.bump_string c) else c;
   1.128 -    fun vary1 c = if used (c ^ u) then vary2 (Symbol.bump_init c) else c;
   1.129 -  in vary1 (if c = "" then "u" else c) ^ u end;
   1.130 -
   1.131 -fun variant used_names = variant_name (member (op =) used_names);
   1.132 -
   1.133 -(*Create variants of the list of names, with priority to the first ones*)
   1.134 -fun variantlist ([], used) = []
   1.135 -  | variantlist(b::bs, used) =
   1.136 -      let val b' = variant used b
   1.137 -      in  b' :: variantlist (bs, b'::used)  end;
   1.138 -
   1.139 -(*Invent fresh names*)
   1.140 -fun invent_names _ _ 0 = []
   1.141 -  | invent_names used a n =
   1.142 -      let val b = Symbol.bump_string a in
   1.143 -        if a mem_string used then invent_names used b n
   1.144 -        else a :: invent_names used b (n - 1)
   1.145 -      end;
   1.146 -
   1.147 -
   1.148  (* substructure *)
   1.149  
   1.150  fun exists_subtype P =
   1.151 @@ -1248,7 +1175,7 @@
   1.152  (*special code to enforce left-to-right collection of TVar-indexnames*)
   1.153  
   1.154  fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts)
   1.155 -  | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns
   1.156 +  | add_typ_ixns(ixns,TVar(ixn,_)) = if member (op =) ixns ixn then ixns
   1.157                                       else ixns@[ixn]
   1.158    | add_typ_ixns(ixns,TFree(_)) = ixns;
   1.159  
   1.160 @@ -1285,7 +1212,7 @@
   1.161  (*Given an abstraction over P, replaces the bound variable by a Free variable
   1.162    having a unique name -- SLOW!*)
   1.163  fun variant_abs (a,T,P) =
   1.164 -  let val b = variant (add_term_names(P,[])) a
   1.165 +  let val b = Name.variant (add_term_names(P,[])) a
   1.166    in  (b,  subst_bound (Free(b,T), P))  end;
   1.167  
   1.168  fun dest_abs (x, T, body) =
   1.169 @@ -1296,28 +1223,14 @@
   1.170        | name_clash _ = false;
   1.171    in
   1.172      if name_clash body then
   1.173 -      dest_abs (variant [x] x, T, body)    (*potentially slow, but rarely happens*)
   1.174 +      dest_abs (Name.variant [x] x, T, body)    (*potentially slow, but rarely happens*)
   1.175      else (x, subst_bound (Free (x, T), body))
   1.176    end;
   1.177  
   1.178 -(*names for numbered variables --
   1.179 -  preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
   1.180 -local
   1.181 -  val small_int = Vector.tabulate (1000, fn i =>
   1.182 -    let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
   1.183 -    in ":" ^ leading ^ string_of_int i end);
   1.184 -in
   1.185 -  fun bound n =
   1.186 -    if n < 1000 then Vector.sub (small_int, n)
   1.187 -    else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
   1.188 -end;
   1.189 -
   1.190 -val is_bound = String.isPrefix ":";
   1.191 -
   1.192  (* renames and reverses the strings in vars away from names *)
   1.193  fun rename_aTs names vars : (string*typ)list =
   1.194    let fun rename_aT (vars,(a,T)) =
   1.195 -                (variant (map #1 vars @ names) a, T) :: vars
   1.196 +                (Name.variant (map #1 vars @ names) a, T) :: vars
   1.197    in Library.foldl rename_aT ([],vars) end;
   1.198  
   1.199  fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
   1.200 @@ -1328,7 +1241,7 @@
   1.201  fun zero_var_inst vars =
   1.202    fold (fn v as ((x, i), X) => fn (used, inst) =>
   1.203      let
   1.204 -      val x' = variant used (if is_bound x then "u" else x);
   1.205 +      val x' = Name.variant used (if Name.is_bound x then "u" else x);
   1.206        val used' = x' :: used;
   1.207      in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end)
   1.208    vars ([], []) |> #2;