# HG changeset patch # User blanchet # Date 1282670368 -7200 # Node ID 27378b4a776beebd7ef598c0cbeb9cd904a2cfa9 # Parent d19c3a7ce38b7253374a4a5c87c4465ee80122a0 compute names lazily; there's no point to compute the names of 10000 facts when only 500 are used diff -r d19c3a7ce38b -r 27378b4a776b src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 18:03:43 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 19:19:28 2010 +0200 @@ -13,7 +13,7 @@ val trace : bool Unsynchronized.ref val name_thms_pair_from_ref : Proof.context -> unit Symtab.table -> thm list -> Facts.ref - -> (string * bool) * thm list + -> (unit -> string * bool) * thm list val relevant_facts : bool -> real -> real -> bool -> int -> bool -> relevance_override -> Proof.context * (thm list * 'a) -> term list -> term @@ -38,13 +38,13 @@ val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator fun name_thms_pair_from_ref ctxt reserved chained_ths xref = - let - val ths = ProofContext.get_fact ctxt xref - val name = Facts.string_of_ref xref - val name = name |> Symtab.defined reserved name ? quote - val chained = forall (member Thm.eq_thm chained_ths) ths - in ((name, chained), ths) end - + let val ths = ProofContext.get_fact ctxt xref in + (fn () => let + val name = Facts.string_of_ref xref + val name = name |> Symtab.defined reserved name ? quote + val chained = forall (member Thm.eq_thm chained_ths) ths + in (name, chained) end, ths) + end (***************************************************************) (* Relevance Filtering *) @@ -278,7 +278,8 @@ | _ => false end; -type annotated_thm = ((string * bool) * thm) * (string * const_typ list) list +type annotated_thm = + ((unit -> string * bool) * thm) * (string * const_typ list) list (*For a reverse sort, putting the largest values first.*) fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1) @@ -297,7 +298,7 @@ ", exceeds the limit of " ^ Int.toString max_new)); trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); trace_msg (fn () => "Actually passed: " ^ - space_implode ", " (map (fst o fst o fst o fst) accepted)); + space_implode ", " (map (fst o (fn f => f ()) o fst o fst o fst) accepted)); (map #1 accepted, List.drop (new_pairs, max_new)) end end; @@ -339,7 +340,7 @@ if null add_thms then [] else - map_filter (fn ((p as ((name, _), th), _), _) => + map_filter (fn ((p as (_, th), _), _) => if member Thm.eq_thm add_thms th then SOME p else NONE) rejects | relevant (new_pairs, rejects) [] = @@ -363,8 +364,8 @@ map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects end | relevant (new_rels, rejects) - (((ax as (((name, chained), th), axiom_consts)), - cached_weight) :: rest) = + (((ax as ((name, th), axiom_consts)), cached_weight) + :: rest) = let val weight = case cached_weight of @@ -374,7 +375,7 @@ if weight >= threshold orelse (defs_relevant andalso defines thy th rel_const_tab) then (trace_msg (fn () => - name ^ " passes: " ^ Real.toString weight + fst (name ()) ^ " passes: " ^ Real.toString weight ^ " consts: " ^ commas (map fst axiom_consts)); relevant ((ax, weight) :: new_rels, rejects) rest) else @@ -548,57 +549,64 @@ val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts); fun add_valid_facts foldx facts = - foldx (fn (name, ths0) => - if name <> "" andalso - forall (not o member Thm.eq_thm add_thms) ths0 andalso - (Facts.is_concealed facts name orelse - (respect_no_atp andalso is_package_def name) orelse - exists (fn s => String.isSuffix s name) multi_base_blacklist orelse - String.isSuffix "_def_raw" (* FIXME: crude hack *) name) then + foldx (fn (name0, ths) => + if name0 <> "" andalso + forall (not o member Thm.eq_thm add_thms) ths andalso + (Facts.is_concealed facts name0 orelse + (respect_no_atp andalso is_package_def name0) orelse + exists (fn s => String.isSuffix s name0) multi_base_blacklist orelse + String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then I else let - fun check_thms a = - (case try (ProofContext.get_thms ctxt) a of - NONE => false - | SOME ths1 => Thm.eq_thms (ths0, ths1)) - val name1 = Facts.extern facts name; - val name2 = Name_Space.extern full_space name; - val ths = - ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf - member Thm.eq_thm add_thms) + val multi = length ths > 1 fun backquotify th = "`" ^ Print_Mode.setmp [Print_Mode.input] (Syntax.string_of_term ctxt) (prop_of th) ^ "`" - val name' = - case find_first check_thms [name1, name2, name] of - SOME name' => name' |> Symtab.defined reserved name' ? quote - | NONE => ths |> map_filter (try backquotify) |> space_implode " " + fun check_thms a = + case try (ProofContext.get_thms ctxt) a of + NONE => false + | SOME ths' => Thm.eq_thms (ths, ths') in - if name' = "" then I - else cons ((name', forall is_chained ths0), ths) + pair 1 + #> fold (fn th => fn (j, rest) => + (j + 1, + if is_theorem_bad_for_atps full_types th andalso + not (member Thm.eq_thm add_thms th) then + rest + else + (fn () => + (if name0 = "" then + th |> backquotify + else + let + val name1 = Facts.extern facts name0 + val name2 = Name_Space.extern full_space name0 + in + case find_first check_thms [name1, name2, name0] of + SOME name => + let + val name = + name |> Symtab.defined reserved name ? quote + in + if multi then name ^ "(" ^ Int.toString j ^ ")" + else name + end + | NONE => "" + end, is_chained th), (multi, th)) :: rest)) ths + #> snd end) in [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals) |> add_valid_facts Facts.fold_static global_facts global_facts end -fun multi_name (name, chained) th (n, pairs) = - (n + 1, ((name ^ "(" ^ Int.toString n ^ ")", chained), th) :: pairs) -fun add_names (_, []) pairs = pairs - | add_names (p, [th]) pairs = (p, th) :: pairs - | add_names (p, ths) pairs = #2 (fold (multi_name p) ths (1, pairs)) - -fun is_multi ((name, _), ths) = - length ths > 1 orelse String.isSuffix ".axioms" name - (* The single-name theorems go after the multiple-name ones, so that single names are preferred when both are available. *) -fun name_thm_pairs ctxt respect_no_atp name_thms_pairs = - let - val (mults, singles) = List.partition is_multi name_thms_pairs - val ps = [] |> fold add_names singles |> fold add_names mults - in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end; +fun name_thm_pairs ctxt respect_no_atp = + List.partition (fst o snd) #> op @ + #> map (apsnd snd) + #> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) (***************************************************************) (* ATP invocation methods setup *) @@ -612,8 +620,11 @@ val add_thms = maps (ProofContext.get_fact ctxt) add val reserved = reserved_isar_keyword_table () val axioms = - (if only then map (name_thms_pair_from_ref ctxt reserved chained_ths) add - else all_name_thms_pairs ctxt reserved full_types add_thms chained_ths) + (if only then + maps ((fn (n, ths) => map (pair n o pair false) ths) + o name_thms_pair_from_ref ctxt reserved chained_ths) add + else + all_name_thms_pairs ctxt reserved full_types add_thms chained_ths) |> name_thm_pairs ctxt (respect_no_atp andalso not only) |> make_unique in @@ -622,6 +633,7 @@ relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override axioms (concl_t :: hyp_ts) + |> map (apfst (fn f => f ())) |> sort_wrt (fst o fst) end diff -r d19c3a7ce38b -r 27378b4a776b src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 24 18:03:43 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 24 19:19:28 2010 +0200 @@ -155,7 +155,8 @@ val reserved = reserved_isar_keyword_table () val chained_ths = #facts (Proof.goal state) val name_thms_pairs = - map (name_thms_pair_from_ref ctxt reserved chained_ths) refs + map (apfst (fn f => f ()) + o name_thms_pair_from_ref ctxt reserved chained_ths) refs in case subgoal_count state of 0 => priority "No subgoal!"