# HG changeset patch # User wenzelm # Date 1630920738 -7200 # Node ID eb265f54e3ce32356dd1e555bba3364448e8e0b9 # Parent 36774e8af3db272b9e0fead3633a632e1cfd9a10 more efficient operations: traverse hyps only when required; diff -r 36774e8af3db -r eb265f54e3ce src/HOL/Eisbach/eisbach_rule_insts.ML --- a/src/HOL/Eisbach/eisbach_rule_insts.ML Sun Sep 05 23:21:32 2021 +0200 +++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Mon Sep 06 11:32:18 2021 +0200 @@ -26,10 +26,10 @@ fun add_thm_insts ctxt thm = let - val tyvars = Thm.fold_terms Term.add_tvars thm []; + val tyvars = Thm.fold_terms {hyps = false} Term.add_tvars thm []; val tyvars' = tyvars |> map (mk_term_type_internal o TVar); - val tvars = Thm.fold_terms Term.add_vars thm []; + val tvars = Thm.fold_terms {hyps = false} Term.add_vars thm []; val tvars' = tvars |> map (Logic.mk_term o Var); val conj = @@ -56,8 +56,8 @@ fun instantiate_xis ctxt insts thm = let - val tyvars = Thm.fold_terms Term.add_tvars thm []; - val tvars = Thm.fold_terms Term.add_vars thm []; + val tyvars = Thm.fold_terms {hyps = false} Term.add_tvars thm []; + val tvars = Thm.fold_terms {hyps = false} Term.add_vars thm []; fun add_inst (xi, t) (Ts, ts) = (case AList.lookup (op =) tyvars xi of diff -r 36774e8af3db -r eb265f54e3ce src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Sun Sep 05 23:21:32 2021 +0200 +++ b/src/HOL/Tools/datatype_realizer.ML Mon Sep 06 11:32:18 2021 +0200 @@ -131,7 +131,7 @@ ||> Sign.restore_naming thy; val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []); - val rvs = rev (Thm.fold_terms Term.add_vars thm' []); + val rvs = rev (Thm.fold_terms {hyps = false} Term.add_vars thm' []); val ivs1 = map Var (filter_out (fn (_, T) => \<^type_name>\bool\ = tname_of (body_type T)) ivs); val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs; diff -r 36774e8af3db -r eb265f54e3ce src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Sun Sep 05 23:21:32 2021 +0200 +++ b/src/Pure/Isar/generic_target.ML Mon Sep 06 11:32:18 2021 +0200 @@ -307,8 +307,8 @@ val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms; (*export fixes*) - val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); - val frees = map Free (Thm.fold_terms Term.add_frees th' []); + val tfrees = map TFree (Thm.fold_terms {hyps = true} Term.add_tfrees th' []); + val frees = map Free (Thm.fold_terms {hyps = true} Term.add_frees th' []); val (th'' :: vs) = (th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees)) |> Variable.export ctxt thy_ctxt diff -r 36774e8af3db -r eb265f54e3ce src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Sun Sep 05 23:21:32 2021 +0200 +++ b/src/Pure/Tools/rule_insts.ML Mon Sep 06 11:32:18 2021 +0200 @@ -115,8 +115,8 @@ val (type_insts, term_insts) = List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) raw_insts; - val tvars = Term_Subst.TVars.build (Thm.fold_terms Term_Subst.add_tvars thm); - val vars = Term_Subst.Vars.build (Thm.fold_terms Term_Subst.add_vars thm); + val tvars = Term_Subst.TVars.build (Thm.fold_terms {hyps = false} Term_Subst.add_tvars thm); + val vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.add_vars thm); (*eigen-context*) val (_, ctxt1) = ctxt diff -r 36774e8af3db -r eb265f54e3ce src/Pure/drule.ML --- a/src/Pure/drule.ML Sun Sep 05 23:21:32 2021 +0200 +++ b/src/Pure/drule.ML Mon Sep 06 11:32:18 2021 +0200 @@ -184,7 +184,7 @@ |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T)); val Ts = map Term.fastype_of ps; val inst = - Term_Subst.Vars.build (th |> (Thm.fold_terms o Term.fold_aterms) + Term_Subst.Vars.build (th |> (Thm.fold_terms {hyps = false} o Term.fold_aterms) (fn t => fn inst => (case t of Var (xi, T) => diff -r 36774e8af3db -r eb265f54e3ce src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sun Sep 05 23:21:32 2021 +0200 +++ b/src/Pure/more_thm.ML Mon Sep 06 11:32:18 2021 +0200 @@ -138,12 +138,15 @@ val eq_ctyp = op = o apply2 Thm.typ_of; val op aconvc = op aconv o apply2 Thm.term_of; -val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a); -val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a); -val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a); +val add_tvars = + Thm.fold_atomic_ctyps {hyps = false} (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a); +val add_vars = + Thm.fold_atomic_cterms {hyps = false} (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a); +val add_frees = + Thm.fold_atomic_cterms {hyps = true} (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a); fun frees_of th = - (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms + (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} (fn a => fn (set, list) => (case Thm.term_of a of Free v => @@ -390,7 +393,7 @@ fun forall_elim_vars_list vars i th = let val used = - (Thm.fold_terms o Term.fold_aterms) + (Thm.fold_terms {hyps = false} o Term.fold_aterms) (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th []; val vars' = (Name.variant_list used (map #1 vars), vars) |> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T)); @@ -449,11 +452,10 @@ zip_options xs ys handle ListPair.UnequalLengths => err "more instantiations than variables in thm"; - val thm' = - Thm.instantiate ((zip_vars (build_rev (Thm.fold_terms Term.add_tvars thm)) cTs), []) thm; - val thm'' = - Thm.instantiate ([], zip_vars (build_rev (Thm.fold_terms Term.add_vars thm')) cts) thm'; - in thm'' end; + val instT = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_tvars thm)) cTs; + val thm' = Thm.instantiate (instT, []) thm; + val inst = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_vars thm')) cts; + in Thm.instantiate ([], inst) thm' end; (* forall_intr_frees: generalization over all suitable Free variables *) @@ -465,7 +467,7 @@ (fold Term_Subst.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #> fold Term_Subst.add_frees (Thm.hyps_of th)); val (_, frees) = - (th, (fixed0, [])) |-> Thm.fold_atomic_cterms (fn a => fn (fixed, frees) => + (th, (fixed0, [])) |-> Thm.fold_atomic_cterms {hyps = false} (fn a => fn (fixed, frees) => (case Thm.term_of a of Free v => if not (Term_Subst.Frees.defined fixed v) diff -r 36774e8af3db -r eb265f54e3ce src/Pure/thm.ML --- a/src/Pure/thm.ML Sun Sep 05 23:21:32 2021 +0200 +++ b/src/Pure/thm.ML Mon Sep 06 11:32:18 2021 +0200 @@ -59,9 +59,9 @@ val first_order_match: cterm * cterm -> ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list (*theorems*) - val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a - val fold_atomic_ctyps: (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a - val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a + val fold_terms: {hyps: bool} -> (term -> 'a -> 'a) -> thm -> 'a -> 'a + val fold_atomic_ctyps: {hyps: bool} -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a + val fold_atomic_cterms: {hyps: bool} -> (cterm -> 'a -> 'a) -> thm -> 'a -> 'a val terms_of_tpairs: (term * term) list -> term list val full_prop_of: thm -> term val theory_id: thm -> Context.theory_id @@ -434,16 +434,16 @@ fun rep_thm (Thm (_, args)) = args; -fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) = - fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps; +fun fold_terms h f (Thm (_, {tpairs, prop, hyps, ...})) = + fold (fn (t, u) => f t #> f u) tpairs #> f prop #> #hyps h ? fold f hyps; -fun fold_atomic_ctyps f (th as Thm (_, {cert, maxidx, shyps, ...})) = +fun fold_atomic_ctyps h f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps} - in (fold_terms o fold_types o fold_atyps) (f o ctyp) th end; + in (fold_terms h o fold_types o fold_atyps) (f o ctyp) th end; -fun fold_atomic_cterms f (th as Thm (_, {cert, maxidx, shyps, ...})) = +fun fold_atomic_cterms h f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps} in - (fold_terms o fold_aterms) + (fold_terms h o fold_aterms) (fn t as Const (_, T) => f (cterm t T) | t as Free (_, T) => f (cterm t T) | t as Var (_, T) => f (cterm t T) @@ -985,7 +985,7 @@ (*Dangling sort constraints of a thm*) fun extra_shyps (th as Thm (_, {shyps, ...})) = - Sorts.subtract (fold_terms Sorts.insert_term th []) shyps; + Sorts.subtract (fold_terms {hyps = true} Sorts.insert_term th []) shyps; (*Remove extra sorts that are witnessed by type signature information*) fun strip_shyps thm = @@ -1001,7 +1001,8 @@ fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1)); fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)]; - val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm []; + val present = + (fold_terms {hyps = true} o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm []; val extra = fold (Sorts.remove_sort o #2) present shyps; val witnessed = Sign.witness_sorts thy present extra; val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize); diff -r 36774e8af3db -r eb265f54e3ce src/Pure/variable.ML --- a/src/Pure/variable.ML Sun Sep 05 23:21:32 2021 +0200 +++ b/src/Pure/variable.ML Mon Sep 06 11:32:18 2021 +0200 @@ -267,7 +267,7 @@ val declare_prf = Proofterm.fold_proof_terms_types declare_internal (declare_internal o Logic.mk_type); -val declare_thm = Thm.fold_terms declare_internal; +val declare_thm = Thm.fold_terms {hyps = true} declare_internal; (* renaming term/type frees *) @@ -689,7 +689,9 @@ in ((xs ~~ ps', goal'), ctxt') end; fun focus_subgoal bindings i st = - let val all_vars = Term_Subst.Vars.build (Thm.fold_terms Term_Subst.add_vars st) in + let + val all_vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.add_vars st); + in Term_Subst.Vars.fold (unbind_term o #1 o #1) all_vars #> Term_Subst.Vars.fold (declare_constraints o Var o #1) all_vars #> focus_cterm bindings (Thm.cprem_of st i) diff -r 36774e8af3db -r eb265f54e3ce src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Sun Sep 05 23:21:32 2021 +0200 +++ b/src/Tools/misc_legacy.ML Mon Sep 06 11:32:18 2021 +0200 @@ -235,7 +235,7 @@ fun freeze_thaw_robust ctxt th = let val fth = Thm.legacy_freezeT th in - case Thm.fold_terms Term.add_vars fth [] of + case Thm.fold_terms {hyps = false} Term.add_vars fth [] of [] => (fth, fn _ => fn x => x) (*No vars: nothing to do!*) | vars => let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))