diff -r 5e844572939d -r c7daff0a3193 src/Pure/term.ML --- a/src/Pure/term.ML Tue Sep 12 12:12:53 2006 +0200 +++ b/src/Pure/term.ML Tue Sep 12 12:12:55 2006 +0200 @@ -76,7 +76,6 @@ val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a val add_term_names: term * string list -> string list val aconv: term * term -> bool - val aconvs: term list * term list -> bool structure Vartab: TABLE structure Typtab: TABLE structure Termtab: TABLE @@ -174,25 +173,12 @@ val eq_var: (indexname * typ) * (indexname * typ) -> bool val tvar_ord: (indexname * sort) * (indexname * sort) -> order val var_ord: (indexname * typ) * (indexname * typ) -> order - val generalize: string list * string list -> int -> term -> term - val generalizeT: string list -> int -> typ -> typ - val generalize_option: string list * string list -> int -> term -> term option - val generalizeT_option: string list -> int -> typ -> typ option - val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list - -> term -> term - val instantiateT: ((indexname * sort) * typ) list -> typ -> typ - val instantiate_option: ((indexname * sort) * typ) list * ((indexname * typ) * term) list - -> term -> term option - val instantiateT_option: ((indexname * sort) * typ) list -> typ -> typ option val maxidx_typ: typ -> int -> int val maxidx_typs: typ list -> int -> int val maxidx_term: term -> int -> int val dest_abs: string * typ * term -> string * term val declare_term_names: term -> Name.context -> Name.context val variant_frees: term -> (string * 'a) list -> (string * 'a) list - 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 dummy_pattern: typ -> term val no_dummy_patterns: term -> term @@ -490,7 +476,17 @@ (** Comparing terms, types, sorts etc. **) -(* fast syntactic comparison *) +(* alpha equivalence -- tuned for equalities *) + +fun tm1 aconv tm2 = + pointer_eq (tm1, tm2) orelse + (case (tm1, tm2) of + (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2 + | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2 + | (a1, a2) => a1 = a2); + + +(* fast syntactic ordering -- tuned for inequalities *) fun fast_indexname_ord ((x, i), (y, j)) = (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord); @@ -563,9 +559,6 @@ EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord) | ord => ord); -fun op aconv tu = (fast_term_ord tu = EQUAL); -fun aconvs ts_us = (list_ord fast_term_ord ts_us = EQUAL); - structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord); structure Typtab = TableFun(type key = typ val ord = typ_ord); structure Termtab = TableFun(type key = term val ord = fast_term_ord); @@ -955,97 +948,6 @@ in subst tm end; -(* generalization of fixed variables *) - -local exception SAME in - -fun generalizeT_same [] _ _ = raise SAME - | generalizeT_same tfrees idx ty = - let - fun gen_typ (Type (a, Ts)) = Type (a, gen_typs Ts) - | gen_typ (TFree (a, S)) = - if member (op =) tfrees a then TVar ((a, idx), S) - else raise SAME - | gen_typ _ = raise SAME - and gen_typs (T :: Ts) = - (gen_typ T :: (gen_typs Ts handle SAME => Ts) - handle SAME => T :: gen_typs Ts) - | gen_typs [] = raise SAME; - in gen_typ ty end; - -fun generalize_same ([], []) _ _ = raise SAME - | generalize_same (tfrees, frees) idx tm = - let - val genT = generalizeT_same tfrees idx; - fun gen (Free (x, T)) = - if member (op =) frees x then - Var (Name.clean_index (x, idx), genT T handle SAME => T) - else Free (x, genT T) - | gen (Var (xi, T)) = Var (xi, genT T) - | gen (Const (c, T)) = Const (c, genT T) - | gen (Bound _) = raise SAME - | gen (Abs (x, T, t)) = - (Abs (x, genT T, gen t handle SAME => t) - handle SAME => Abs (x, T, gen t)) - | gen (t $ u) = (gen t $ (gen u handle SAME => u) handle SAME => t $ gen u); - in gen tm end; - -fun generalize names i tm = generalize_same names i tm handle SAME => tm; -fun generalizeT names i ty = generalizeT_same names i ty handle SAME => ty; - -fun generalize_option names i tm = SOME (generalize_same names i tm) handle SAME => NONE; -fun generalizeT_option names i ty = SOME (generalizeT_same names i ty) handle SAME => NONE; - -end; - - -(* instantiation of schematic variables (types before terms) *) - -local exception SAME in - -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) = - (case AList.lookup eq_tvar instT v of - SOME T => T - | NONE => raise SAME) - | subst_typ _ = raise SAME - and subst_typs (T :: Ts) = - (subst_typ T :: (subst_typs Ts handle SAME => Ts) - handle SAME => T :: subst_typs Ts) - | subst_typs [] = raise SAME; - in subst_typ ty end; - -fun instantiate_same ([], []) _ = raise SAME - | instantiate_same (instT, inst) tm = - let - 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 T, false) handle SAME => (T, true) in - (case AList.lookup 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 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 end; - -fun instantiate insts tm = instantiate_same insts tm handle SAME => tm; -fun instantiateT insts ty = instantiateT_same insts ty handle SAME => ty; - -fun instantiate_option insts tm = SOME (instantiate_same insts tm) handle SAME => NONE; -fun instantiateT_option insts ty = SOME (instantiateT_same insts ty) handle SAME => NONE; - -end; - - (** Identifying first-order terms **) (*Differs from proofterm/is_fun in its treatment of TVar*) @@ -1242,25 +1144,6 @@ fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*) -(* zero var indexes *) - -fun zero_var_inst vars = - fold (fn v as ((x, i), X) => fn (inst, used) => - let - val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used; - in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end) - vars ([], Name.context) |> #1; - -fun zero_var_indexes_inst tm = - let - val instT = zero_var_inst (sort tvar_ord (add_tvars tm [])) |> map (apsnd TVar); - val inst = zero_var_inst (sort var_ord (map (apsnd (instantiateT instT)) (add_vars tm []))) - |> map (apsnd Var); - in (instT, inst) end; - -fun zero_var_indexes tm = instantiate (zero_var_indexes_inst tm) tm; - - (* dummy patterns *) val dummy_patternN = "dummy_pattern";