src/Pure/term.ML
changeset 20511 c7daff0a3193
parent 20331 ccdd1592f5ff
child 20531 7de9caf4fd78
     1.1 --- a/src/Pure/term.ML	Tue Sep 12 12:12:53 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Tue Sep 12 12:12:55 2006 +0200
     1.3 @@ -76,7 +76,6 @@
     1.4    val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
     1.5    val add_term_names: term * string list -> string list
     1.6    val aconv: term * term -> bool
     1.7 -  val aconvs: term list * term list -> bool
     1.8    structure Vartab: TABLE
     1.9    structure Typtab: TABLE
    1.10    structure Termtab: TABLE
    1.11 @@ -174,25 +173,12 @@
    1.12    val eq_var: (indexname * typ) * (indexname * typ) -> bool
    1.13    val tvar_ord: (indexname * sort) * (indexname * sort) -> order
    1.14    val var_ord: (indexname * typ) * (indexname * typ) -> order
    1.15 -  val generalize: string list * string list -> int -> term -> term
    1.16 -  val generalizeT: string list -> int -> typ -> typ
    1.17 -  val generalize_option: string list * string list -> int -> term -> term option
    1.18 -  val generalizeT_option: string list -> int -> typ -> typ option
    1.19 -  val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    1.20 -    -> term -> term
    1.21 -  val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
    1.22 -  val instantiate_option: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    1.23 -    -> term -> term option
    1.24 -  val instantiateT_option: ((indexname * sort) * typ) list -> typ -> typ option
    1.25    val maxidx_typ: typ -> int -> int
    1.26    val maxidx_typs: typ list -> int -> int
    1.27    val maxidx_term: term -> int -> int
    1.28    val dest_abs: string * typ * term -> string * term
    1.29    val declare_term_names: term -> Name.context -> Name.context
    1.30    val variant_frees: term -> (string * 'a) list -> (string * 'a) list
    1.31 -  val zero_var_indexes: term -> term
    1.32 -  val zero_var_indexes_inst: term ->
    1.33 -    ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    1.34    val dummy_patternN: string
    1.35    val dummy_pattern: typ -> term
    1.36    val no_dummy_patterns: term -> term
    1.37 @@ -490,7 +476,17 @@
    1.38  
    1.39  (** Comparing terms, types, sorts etc. **)
    1.40  
    1.41 -(* fast syntactic comparison *)
    1.42 +(* alpha equivalence -- tuned for equalities *)
    1.43 +
    1.44 +fun tm1 aconv tm2 =
    1.45 +  pointer_eq (tm1, tm2) orelse
    1.46 +    (case (tm1, tm2) of
    1.47 +      (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2
    1.48 +    | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
    1.49 +    | (a1, a2) => a1 = a2);
    1.50 +
    1.51 +
    1.52 +(* fast syntactic ordering -- tuned for inequalities *)
    1.53  
    1.54  fun fast_indexname_ord ((x, i), (y, j)) =
    1.55    (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
    1.56 @@ -563,9 +559,6 @@
    1.57        EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
    1.58      | ord => ord);
    1.59  
    1.60 -fun op aconv tu = (fast_term_ord tu = EQUAL);
    1.61 -fun aconvs ts_us = (list_ord fast_term_ord ts_us = EQUAL);
    1.62 -
    1.63  structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord);
    1.64  structure Typtab = TableFun(type key = typ val ord = typ_ord);
    1.65  structure Termtab = TableFun(type key = term val ord = fast_term_ord);
    1.66 @@ -955,97 +948,6 @@
    1.67        in subst tm end;
    1.68  
    1.69  
    1.70 -(* generalization of fixed variables *)
    1.71 -
    1.72 -local exception SAME in
    1.73 -
    1.74 -fun generalizeT_same [] _ _ = raise SAME
    1.75 -  | generalizeT_same tfrees idx ty =
    1.76 -      let
    1.77 -        fun gen_typ (Type (a, Ts)) = Type (a, gen_typs Ts)
    1.78 -          | gen_typ (TFree (a, S)) =
    1.79 -              if member (op =) tfrees a then TVar ((a, idx), S)
    1.80 -              else raise SAME
    1.81 -          | gen_typ _ = raise SAME
    1.82 -        and gen_typs (T :: Ts) =
    1.83 -            (gen_typ T :: (gen_typs Ts handle SAME => Ts)
    1.84 -              handle SAME => T :: gen_typs Ts)
    1.85 -          | gen_typs [] = raise SAME;
    1.86 -      in gen_typ ty end;
    1.87 -
    1.88 -fun generalize_same ([], []) _ _ = raise SAME
    1.89 -  | generalize_same (tfrees, frees) idx tm =
    1.90 -      let
    1.91 -        val genT = generalizeT_same tfrees idx;
    1.92 -        fun gen (Free (x, T)) =
    1.93 -              if member (op =) frees x then
    1.94 -                Var (Name.clean_index (x, idx), genT T handle SAME => T)
    1.95 -              else Free (x, genT T)
    1.96 -          | gen (Var (xi, T)) = Var (xi, genT T)
    1.97 -          | gen (Const (c, T)) = Const (c, genT T)
    1.98 -          | gen (Bound _) = raise SAME
    1.99 -          | gen (Abs (x, T, t)) =
   1.100 -              (Abs (x, genT T, gen t handle SAME => t)
   1.101 -                handle SAME => Abs (x, T, gen t))
   1.102 -          | gen (t $ u) = (gen t $ (gen u handle SAME => u) handle SAME => t $ gen u);
   1.103 -      in gen tm end;
   1.104 -
   1.105 -fun generalize names i tm = generalize_same names i tm handle SAME => tm;
   1.106 -fun generalizeT names i ty = generalizeT_same names i ty handle SAME => ty;
   1.107 -
   1.108 -fun generalize_option names i tm = SOME (generalize_same names i tm) handle SAME => NONE;
   1.109 -fun generalizeT_option names i ty = SOME (generalizeT_same names i ty) handle SAME => NONE;
   1.110 -
   1.111 -end;
   1.112 -
   1.113 -
   1.114 -(* instantiation of schematic variables (types before terms) *)
   1.115 -
   1.116 -local exception SAME in
   1.117 -
   1.118 -fun instantiateT_same [] _ = raise SAME
   1.119 -  | instantiateT_same instT ty =
   1.120 -      let
   1.121 -        fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
   1.122 -          | subst_typ (TVar v) =
   1.123 -              (case AList.lookup eq_tvar instT v of
   1.124 -                SOME T => T
   1.125 -              | NONE => raise SAME)
   1.126 -          | subst_typ _ = raise SAME
   1.127 -        and subst_typs (T :: Ts) =
   1.128 -            (subst_typ T :: (subst_typs Ts handle SAME => Ts)
   1.129 -              handle SAME => T :: subst_typs Ts)
   1.130 -          | subst_typs [] = raise SAME;
   1.131 -      in subst_typ ty end;
   1.132 -
   1.133 -fun instantiate_same ([], []) _ = raise SAME
   1.134 -  | instantiate_same (instT, inst) tm =
   1.135 -      let
   1.136 -        val substT = instantiateT_same instT;
   1.137 -        fun subst (Const (c, T)) = Const (c, substT T)
   1.138 -          | subst (Free (x, T)) = Free (x, substT T)
   1.139 -          | subst (Var (xi, T)) =
   1.140 -              let val (T', same) = (substT T, false) handle SAME => (T, true) in
   1.141 -                (case AList.lookup eq_var inst (xi, T') of
   1.142 -                   SOME t => t
   1.143 -                 | NONE => if same then raise SAME else Var (xi, T'))
   1.144 -              end
   1.145 -          | subst (Bound _) = raise SAME
   1.146 -          | subst (Abs (x, T, t)) =
   1.147 -              (Abs (x, substT T, subst t handle SAME => t)
   1.148 -                handle SAME => Abs (x, T, subst t))
   1.149 -          | subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u);
   1.150 -      in subst tm end;
   1.151 -
   1.152 -fun instantiate insts tm = instantiate_same insts tm handle SAME => tm;
   1.153 -fun instantiateT insts ty = instantiateT_same insts ty handle SAME => ty;
   1.154 -
   1.155 -fun instantiate_option insts tm = SOME (instantiate_same insts tm) handle SAME => NONE;
   1.156 -fun instantiateT_option insts ty = SOME (instantiateT_same insts ty) handle SAME => NONE;
   1.157 -
   1.158 -end;
   1.159 -
   1.160 -
   1.161  (** Identifying first-order terms **)
   1.162  
   1.163  (*Differs from proofterm/is_fun in its treatment of TVar*)
   1.164 @@ -1242,25 +1144,6 @@
   1.165  fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
   1.166  
   1.167  
   1.168 -(* zero var indexes *)
   1.169 -
   1.170 -fun zero_var_inst vars =
   1.171 -  fold (fn v as ((x, i), X) => fn (inst, used) =>
   1.172 -    let
   1.173 -      val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used;
   1.174 -    in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end)
   1.175 -  vars ([], Name.context) |> #1;
   1.176 -
   1.177 -fun zero_var_indexes_inst tm =
   1.178 -  let
   1.179 -    val instT = zero_var_inst (sort tvar_ord (add_tvars tm [])) |> map (apsnd TVar);
   1.180 -    val inst = zero_var_inst (sort var_ord (map (apsnd (instantiateT instT)) (add_vars tm [])))
   1.181 -      |> map (apsnd Var);
   1.182 -  in (instT, inst) end;
   1.183 -
   1.184 -fun zero_var_indexes tm = instantiate (zero_var_indexes_inst tm) tm;
   1.185 -
   1.186 -
   1.187  (* dummy patterns *)
   1.188  
   1.189  val dummy_patternN = "dummy_pattern";