removed atless (use term_ord instead);
authorwenzelm
Mon Aug 01 19:20:44 2005 +0200 (2005-08-01)
changeset 169907fceb965cf52
parent 16989 1877b00fb4d2
child 16991 39f5760f72d7
removed atless (use term_ord instead);
removed (inefficient) insert_aterm;
improved bound: nameless, avoid allocating new strings;
tuned sort_ord/typ_ord: dict_ord;
tuned abstract_over: SAME;
tuned add_term_vars/frees: OrdList.insert;
removed compress_type/compress_type (cf. compress.ML);
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Mon Aug 01 19:20:43 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Mon Aug 01 19:20:44 2005 +0200
     1.3 @@ -152,16 +152,12 @@
     1.4    val term_tvars: term -> (indexname * sort) list
     1.5    val add_typ_ixns: indexname list * typ -> indexname list
     1.6    val add_term_tvar_ixns: term * indexname list -> indexname list
     1.7 -  val atless: term * term -> bool
     1.8 -  val insert_aterm: term * term list -> term list
     1.9    val add_term_vars: term * term list -> term list
    1.10    val term_vars: term -> term list
    1.11    val add_term_frees: term * term list -> term list
    1.12    val term_frees: term -> term list
    1.13    val variant_abs: string * typ * term -> string * term
    1.14    val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
    1.15 -  val compress_type: typ -> typ
    1.16 -  val compress_term: term -> term
    1.17    val show_question_marks: bool ref
    1.18  end;
    1.19  
    1.20 @@ -200,7 +196,8 @@
    1.21    val map_typ: (string -> string) -> (string -> string) -> typ -> typ
    1.22    val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
    1.23    val dest_abs: string * typ * term -> string * term
    1.24 -  val bound: int -> string -> string
    1.25 +  val bound: int -> string
    1.26 +  val is_bound: string -> bool
    1.27    val zero_var_indexesT: typ -> typ
    1.28    val zero_var_indexes: term -> term
    1.29    val zero_var_indexes_inst: term ->
    1.30 @@ -515,7 +512,7 @@
    1.31  
    1.32  fun sort_ord SS =
    1.33    if pointer_eq SS then EQUAL
    1.34 -  else list_ord fast_string_ord SS;
    1.35 +  else dict_ord fast_string_ord SS;
    1.36  
    1.37  local
    1.38  
    1.39 @@ -530,7 +527,7 @@
    1.40    else
    1.41      (case TU of
    1.42        (Type (a, Ts), Type (b, Us)) =>
    1.43 -        (case fast_string_ord (a, b) of EQUAL => list_ord typ_ord (Ts, Us) | ord => ord)
    1.44 +        (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
    1.45      | (TFree (a, S), TFree (b, S')) =>
    1.46          (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
    1.47      | (TVar (xi, S), TVar (yj, S')) =>
    1.48 @@ -880,14 +877,15 @@
    1.49    The resulting term is ready to become the body of an Abs.*)
    1.50  fun abstract_over (v, body) =
    1.51    let
    1.52 -    fun abst (lev, u) =
    1.53 -      if v aconv u then Bound lev
    1.54 +    exception SAME;
    1.55 +    fun abs lev tm =
    1.56 +      if v aconv tm then Bound lev
    1.57        else
    1.58 -        (case u of
    1.59 -          Abs (a, T, t) => Abs (a, T, abst (lev + 1, t))
    1.60 -        | f $ rand => abst (lev, f) $ abst (lev, rand)
    1.61 -        | _ => u)
    1.62 -  in abst(0, body) end;
    1.63 +        (case tm of
    1.64 +          Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
    1.65 +        | t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u)
    1.66 +        | _ => raise SAME);
    1.67 +  in abs 0 body handle SAME => body end;
    1.68  
    1.69  fun lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
    1.70    | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
    1.71 @@ -1038,7 +1036,7 @@
    1.72      in  first_order1 []  end;
    1.73  
    1.74  
    1.75 -(* maximum index of a typs and terms *)
    1.76 +(* maximum index of typs and terms *)
    1.77  
    1.78  fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
    1.79    | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
    1.80 @@ -1200,25 +1198,9 @@
    1.81  
    1.82  (** Frees and Vars **)
    1.83  
    1.84 -(*a partial ordering (not reflexive) for atomic terms*)
    1.85 -fun atless (Const (a,_), Const (b,_))  =  a<b
    1.86 -  | atless (Free (a,_), Free (b,_)) =  a<b
    1.87 -  | atless (Var(v,_), Var(w,_))  =  xless(v,w)
    1.88 -  | atless (Bound i, Bound j)  =   i<j
    1.89 -  | atless _  =  false;
    1.90 -
    1.91 -(*insert atomic term into partially sorted list, suppressing duplicates (?)*)
    1.92 -fun insert_aterm (t,us) =
    1.93 -  let fun inserta [] = [t]
    1.94 -        | inserta (us as u::us') =
    1.95 -              if atless(t,u) then t::us
    1.96 -              else if t=u then us (*duplicate*)
    1.97 -              else u :: inserta(us')
    1.98 -  in  inserta us  end;
    1.99 -
   1.100  (*Accumulates the Vars in the term, suppressing duplicates*)
   1.101  fun add_term_vars (t, vars: term list) = case t of
   1.102 -    Var   _ => insert_aterm(t,vars)
   1.103 +    Var   _ => OrdList.insert term_ord t vars
   1.104    | Abs (_,_,body) => add_term_vars(body,vars)
   1.105    | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   1.106    | _ => vars;
   1.107 @@ -1227,7 +1209,7 @@
   1.108  
   1.109  (*Accumulates the Frees in the term, suppressing duplicates*)
   1.110  fun add_term_frees (t, frees: term list) = case t of
   1.111 -    Free   _ => insert_aterm(t,frees)
   1.112 +    Free   _ => OrdList.insert term_ord t frees
   1.113    | Abs (_,_,body) => add_term_frees(body,frees)
   1.114    | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   1.115    | _ => frees;
   1.116 @@ -1252,7 +1234,19 @@
   1.117      else (x, subst_bound (Free (x, T), body))
   1.118    end;
   1.119  
   1.120 -fun bound bounds x = "." ^ x ^ "." ^ string_of_int bounds;
   1.121 +(*names for numbered variables --
   1.122 +  preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
   1.123 +local
   1.124 +  val small_int = Vector.tabulate (1000, fn i =>
   1.125 +    let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
   1.126 +    in ":" ^ leading ^ string_of_int i end);
   1.127 +in
   1.128 +  fun bound n =
   1.129 +    if n < 1000 then Vector.sub (small_int, n)
   1.130 +    else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
   1.131 +end;
   1.132 +
   1.133 +val is_bound = String.isPrefix ":";
   1.134  
   1.135  (* renames and reverses the strings in vars away from names *)
   1.136  fun rename_aTs names vars : (string*typ)list =
   1.137 @@ -1287,39 +1281,6 @@
   1.138  fun zero_var_indexes tm = instantiate (zero_var_indexes_inst tm) tm;
   1.139  
   1.140  
   1.141 -
   1.142 -(*** Compression of terms and types by sharing common subtrees.
   1.143 -     Saves 50-75% on storage requirements.  As it is a bit slow,
   1.144 -     it should be called only for axioms, stored theorems, etc.
   1.145 -     Recorded term and type fragments are never disposed. ***)
   1.146 -
   1.147 -
   1.148 -(** Sharing of types **)
   1.149 -
   1.150 -val memo_types = ref (Typtab.empty: typ Typtab.table);
   1.151 -
   1.152 -fun compress_type T =
   1.153 -  (case Typtab.lookup (! memo_types, T) of
   1.154 -    SOME T' => T'
   1.155 -  | NONE =>
   1.156 -      let val T' = (case T of Type (a, Ts) => Type (a, map compress_type Ts) | _ => T)
   1.157 -      in memo_types := Typtab.update ((T', T'), ! memo_types); T' end);
   1.158 -
   1.159 -
   1.160 -(** Sharing of atomic terms **)
   1.161 -
   1.162 -val memo_terms = ref (Termtab.empty : term Termtab.table);
   1.163 -
   1.164 -fun share_term (t $ u) = share_term t $ share_term u
   1.165 -  | share_term (Abs (a, T, u)) = Abs (a, T, share_term u)
   1.166 -  | share_term t =
   1.167 -      (case Termtab.lookup (! memo_terms, t) of
   1.168 -        SOME t' => t'
   1.169 -      | NONE => (memo_terms := Termtab.update ((t, t), ! memo_terms); t));
   1.170 -
   1.171 -val compress_term = share_term o map_term_types compress_type;
   1.172 -
   1.173 -
   1.174  (* dummy patterns *)
   1.175  
   1.176  val dummy_patternN = "dummy_pattern";