# HG changeset patch # User blanchet # Date 1359651245 -3600 # Node ID 5f2788c3812701a6ad3cebc173c06a383ec109d4 # Parent 198cb05fb35b5c42effde95cbdc49e194fa7fd11 distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds diff -r 198cb05fb35b -r 5f2788c38127 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 31 17:54:05 2013 +0100 @@ -478,7 +478,6 @@ (the_default default_max_facts max_facts) Sledgehammer_Fact.no_fact_override hyp_ts concl_t |> #1 (*###*) - |> map (apfst (apfst (fn name => name ()))) |> tap (fn facts => "Line " ^ str0 (Position.line_of pos) ^ ": " ^ (if null facts then diff -r 198cb05fb35b -r 5f2788c38127 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Jan 31 17:54:05 2013 +0100 @@ -136,7 +136,7 @@ |> Sledgehammer_MePo.mepo_suggested_facts ctxt params default_prover (the_default default_max_facts max_facts) (SOME relevance_fudge) hyp_ts concl_t - |> map ((fn name => name ()) o fst o fst) + |> map (fst o fst) val (found_facts, lost_facts) = flat proofs |> sort_distinct string_ord |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) diff -r 198cb05fb35b -r 5f2788c38127 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/TPTP/mash_eval.ML Thu Jan 31 17:54:05 2013 +0100 @@ -71,7 +71,7 @@ val str_of_method = enclose " " ": " fun str_of_result method facts ({outcome, run_time, used_facts, ...} : prover_result) = - let val facts = facts |> map (fn ((name, _), _) => name ()) in + let val facts = facts |> map (fst o fst) in str_of_method method ^ (if is_none outcome then "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ @@ -111,7 +111,7 @@ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 val isar_deps = isar_dependencies_of name_tabs th val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) - val find_suggs = find_suggested_facts facts + val find_suggs = find_suggested_facts facts #> map fact_of_raw_fact fun get_facts [] compute = compute facts | get_facts suggs _ = find_suggs suggs val mepo_facts = @@ -121,7 +121,8 @@ |> weight_mepo_facts fun mash_of suggs = get_facts suggs (fn _ => - find_mash_suggestions slack_max_facts suggs facts [] [] |> fst) + find_mash_suggestions slack_max_facts suggs facts [] [] + |> fst |> map fact_of_raw_fact) |> weight_mash_facts val mash_isar_facts = mash_of mash_isar_suggs val mash_prover_facts = mash_of mash_prover_suggs @@ -160,6 +161,7 @@ |> map (get #> nickify) |> maybe_instantiate_inducts ctxt hyp_ts concl_t |> take (the max_facts) + |> map fact_of_raw_fact val ctxt = ctxt |> set_file_name method prob_dir_name val res as {outcome, ...} = run_prover_for_mash ctxt params prover facts goal diff -r 198cb05fb35b -r 5f2788c38127 src/HOL/TPTP/sledgehammer_tactics.ML --- a/src/HOL/TPTP/sledgehammer_tactics.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Thu Jan 31 17:54:05 2013 +0100 @@ -45,8 +45,7 @@ |> #1 val problem = {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - facts = facts |> map (apfst (apfst (fn name => name ()))) - |> map Untranslated_Fact} + facts = facts |> map Untranslated_Fact} in (case prover params (K (K (K ""))) problem of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME diff -r 198cb05fb35b -r 5f2788c38127 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Jan 31 17:54:05 2013 +0100 @@ -10,7 +10,8 @@ type status = ATP_Problem_Generate.status type stature = ATP_Problem_Generate.stature - type fact = ((unit -> string) * stature) * thm + type raw_fact = ((unit -> string) * stature) * thm + type fact = (string * stature) * thm type fact_override = {add : (Facts.ref * Attrib.src list) list, @@ -33,12 +34,13 @@ Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list + val fact_of_raw_fact : raw_fact -> fact val all_facts : Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list - -> status Termtab.table -> fact list + -> status Termtab.table -> raw_fact list val nearly_all_facts : Proof.context -> bool -> fact_override -> unit Symtab.table - -> status Termtab.table -> thm list -> term list -> term -> fact list + -> status Termtab.table -> thm list -> term list -> term -> raw_fact list end; structure Sledgehammer_Fact : SLEDGEHAMMER_FACT = @@ -49,7 +51,8 @@ open Metis_Tactic open Sledgehammer_Util -type fact = ((unit -> string) * stature) * thm +type raw_fact = ((unit -> string) * stature) * thm +type fact = (string * stature) * thm type fact_override = {add : (Facts.ref * Attrib.src list) list, @@ -419,6 +422,8 @@ fun maybe_filter_no_atps ctxt = not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd) +fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th) + fun all_facts ctxt generous ho_atp reserved add_ths chained css = let val thy = Proof_Context.theory_of ctxt diff -r 198cb05fb35b -r 5f2788c38127 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 31 17:54:05 2013 +0100 @@ -7,6 +7,7 @@ signature SLEDGEHAMMER_MASH = sig type stature = ATP_Problem_Generate.stature + type raw_fact = Sledgehammer_Fact.raw_fact type fact = Sledgehammer_Fact.fact type fact_override = Sledgehammer_Fact.fact_override type params = Sledgehammer_Provers.params @@ -62,7 +63,7 @@ val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list val prover_dependencies_of : - Proof.context -> params -> string -> int -> fact list + Proof.context -> params -> string -> int -> raw_fact list -> string Symtab.table * string Symtab.table -> thm -> bool * string list val weight_mepo_facts : 'a list -> ('a * real) list @@ -71,8 +72,8 @@ int -> string list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list * ('b * thm) list val mash_suggested_facts : - Proof.context -> params -> string -> int -> term list -> term -> fact list - -> fact list * fact list + Proof.context -> params -> string -> int -> term list -> term + -> raw_fact list -> fact list * fact list val mash_learn_proof : Proof.context -> params -> string -> term -> ('a * thm) list -> thm list -> unit @@ -85,7 +86,7 @@ val mash_weight : real val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list - -> term -> fact list -> fact list * fact list * fact list + -> term -> raw_fact list -> fact list * fact list * fact list val kill_learners : unit -> unit val running_learners : unit -> unit end; @@ -531,8 +532,7 @@ let val problem = {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, - facts = facts |> map (apfst (apfst (fn name => name ()))) - |> map Untranslated_Fact} + facts = facts |> map Untranslated_Fact} in get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K ""))) problem @@ -687,14 +687,13 @@ val goal = goal_of_thm thy th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) - fun nickify ((_, stature), th) = - ((fn () => nickname_of_thm th, stature), th) + fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th) fun is_dep dep (_, th) = nickname_of_thm th = dep fun add_isar_dep facts dep accum = if exists (is_dep dep) accum then accum else case find_first (is_dep dep) facts of - SOME ((name, status), th) => accum @ [((name, status), th)] + SOME ((_, status), th) => accum @ [(("", status), th)] | NONE => accum (* shouldn't happen *) val facts = facts @@ -825,7 +824,10 @@ (parents, feats, hints)) end) val unknown = facts |> filter_out (is_fact_in_graph access_G snd) - in find_mash_suggestions max_facts suggs facts chained unknown end + in + find_mash_suggestions max_facts suggs facts chained unknown + |> pairself (map fact_of_raw_fact) + end fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, graph) = let @@ -1099,7 +1101,9 @@ if not (subset (op =) (the_list fact_filter, fact_filters)) then error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".") else if only then - (facts, facts, facts) + let val facts = facts |> map fact_of_raw_fact in + (facts, facts, facts) + end else if max_facts <= 0 orelse null facts then ([], [], []) else @@ -1129,11 +1133,12 @@ else mepoN val add_ths = Attrib.eval_thms ctxt add - val in_add = member Thm.eq_thm_prop add_ths o snd + fun in_add (_, th) = member Thm.eq_thm_prop add_ths th fun add_and_take accepts = (case add_ths of [] => accepts - | _ => (facts |> filter in_add) @ (accepts |> filter_out in_add)) + | _ => (facts |> filter in_add |> map fact_of_raw_fact) @ + (accepts |> filter_out in_add)) |> take max_facts fun mepo () = mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t diff -r 198cb05fb35b -r 5f2788c38127 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Thu Jan 31 17:54:05 2013 +0100 @@ -8,6 +8,7 @@ signature SLEDGEHAMMER_MEPO = sig type stature = ATP_Problem_Generate.stature + type raw_fact = Sledgehammer_Fact.raw_fact type fact = Sledgehammer_Fact.fact type params = Sledgehammer_Provers.params type relevance_fudge = Sledgehammer_Provers.relevance_fudge @@ -20,7 +21,7 @@ -> string list val mepo_suggested_facts : Proof.context -> params -> string -> int -> relevance_fudge option - -> term list -> term -> fact list -> fact list + -> term list -> term -> raw_fact list -> fact list end; structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO = @@ -337,7 +338,7 @@ fun take_most_relevant ctxt max_facts remaining_max ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge) - (candidates : ((fact * (string * ptype) list) * real) list) = + (candidates : ((raw_fact * (string * ptype) list) * real) list) = let val max_imperfect = Real.ceil (Math.pow (max_imperfect, @@ -533,6 +534,7 @@ relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge facts hyp_ts (concl_t |> theory_constify fudge (Context.theory_name thy))) + |> map fact_of_raw_fact end end; diff -r 198cb05fb35b -r 5f2788c38127 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 31 17:54:05 2013 +0100 @@ -237,7 +237,6 @@ |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t |> #1 (*###*) - |> map (apfst (apfst (fn name => name ()))) |> tap (fn facts => if verbose then label ^ plural_s (length provers) ^ ": " ^