# HG changeset patch # User blanchet # Date 1342593843 -7200 # Node ID 6b65f1ad0e4b9dbdfef97c211a15a8beac062d93 # Parent 255c6e1fd5051f21ce4b4b021381a36144b942b3 systematize lazy names in relevance filter diff -r 255c6e1fd505 -r 6b65f1ad0e4b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 18 08:44:03 2012 +0200 @@ -470,7 +470,8 @@ val problem = {state = st', goal = goal, subgoal = i, subgoal_count = Sledgehammer_Util.subgoal_count st, - facts = facts |> map Sledgehammer_Provers.Untranslated_Fact} + facts = facts |> map (apfst (apfst (fn name => name ()))) + |> map Sledgehammer_Provers.Untranslated_Fact} in prover params (K (K (K ""))) problem end)) () handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut | Fail "inappropriate" => failed ATP_Proof.Inappropriate diff -r 255c6e1fd505 -r 6b65f1ad0e4b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Jul 18 08:44:03 2012 +0200 @@ -128,14 +128,14 @@ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover val facts = - Sledgehammer_Fact.nearly_all_facts ctxt ho_atp - Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t - |> filter (is_appropriate_prop o prop_of o snd) - |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params - default_prover (the_default default_max_relevant max_relevant) - (SOME relevance_fudge) Sledgehammer_Fact.no_relevance_override - chained_ths hyp_ts concl_t - |> map (fst o fst) + Sledgehammer_Fact.nearly_all_facts ctxt ho_atp + Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t + |> filter (is_appropriate_prop o prop_of o snd) + |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params + default_prover (the_default default_max_relevant max_relevant) + (SOME relevance_fudge) Sledgehammer_Fact.no_relevance_override + chained_ths hyp_ts concl_t + |> map ((fn name => name ()) o 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 255c6e1fd505 -r 6b65f1ad0e4b src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:03 2012 +0200 @@ -57,9 +57,10 @@ map_filter (find_sugg facts o of_fact_name) #> take (max_relevant_slack * the max_relevant) #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t - #> map (apfst (apfst (fn name => name ()))) - fun iter_mash_facts fs1 fs2 = + fun hybrid_facts fsp = let + val (fs1, fs2) = + fsp |> pairself (map (apfst (apfst (fn name => name ())))) val fact_eq = (op =) o pairself fst fun score_in f fs = case find_index (curry fact_eq f) fs of @@ -70,29 +71,30 @@ union fact_eq fs1 fs2 |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd |> take (the max_relevant) + |> map (apfst (apfst K)) end - fun with_index facts s = - (find_index (fn ((s', _), _) => s = s') facts + 1, s) + fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) fun index_string (j, s) = s ^ "@" ^ string_of_int j fun str_of_res label facts {outcome, run_time, used_facts, ...} = - " " ^ label ^ ": " ^ - (if is_none outcome then - "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ - (used_facts |> map (with_index facts o fst) - |> sort (int_ord o pairself fst) - |> map index_string - |> space_implode " ") ^ - (if length facts < the max_relevant then - " (of " ^ string_of_int (length facts) ^ ")" - else - "") - else - "Failure: " ^ - (facts |> map (fst o fst) - |> take (the max_relevant) - |> tag_list 1 - |> map index_string - |> space_implode " ")) + let val facts = facts |> map (fn ((name, _), _) => name ()) in + " " ^ label ^ ": " ^ + (if is_none outcome then + "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ + (used_facts |> map (with_index facts o fst) + |> sort (int_ord o pairself fst) + |> map index_string + |> space_implode " ") ^ + (if length facts < the max_relevant then + " (of " ^ string_of_int (length facts) ^ ")" + else + "") + else + "Failure: " ^ + (facts |> take (the max_relevant) + |> tag_list 1 + |> map index_string + |> space_implode " ")) + end fun prove ok heading facts goal = let val facts = facts |> take (the max_relevant) @@ -115,7 +117,7 @@ iter_facts ctxt params (max_relevant_slack * the max_relevant) goal facts val mash_facts = sugg_facts hyp_ts concl_t facts suggs - val iter_mash_facts = iter_mash_facts iter_facts mash_facts + val iter_mash_facts = hybrid_facts (iter_facts, mash_facts) val iter_s = prove iter_ok iterN iter_facts goal val mash_s = prove mash_ok mashN mash_facts goal val iter_mash_s = prove iter_mash_ok iter_mashN iter_mash_facts goal diff -r 255c6e1fd505 -r 6b65f1ad0e4b src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:03 2012 +0200 @@ -64,7 +64,7 @@ let val suggs = old_facts |> iter_facts ctxt params max_relevant goal - |> map (fact_name_of o fst o fst) + |> map (fn ((name, _), _) => fact_name_of (name ())) |> sort string_ord val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n" in File.append path s end diff -r 255c6e1fd505 -r 6b65f1ad0e4b src/HOL/TPTP/sledgehammer_tactics.ML --- a/src/HOL/TPTP/sledgehammer_tactics.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Wed Jul 18 08:44:03 2012 +0200 @@ -42,7 +42,8 @@ chained_ths hyp_ts concl_t val problem = {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - facts = map Sledgehammer_Provers.Untranslated_Fact facts} + facts = facts |> map (apfst (apfst (fn name => name ()))) + |> map Sledgehammer_Provers.Untranslated_Fact} in (case prover params (K (K (K ""))) problem of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME diff -r 255c6e1fd505 -r 6b65f1ad0e4b src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 18 08:44:03 2012 +0200 @@ -22,7 +22,7 @@ Proof.context -> params -> string -> int -> relevance_fudge option -> relevance_override -> thm list -> term list -> term -> (((unit -> string) * stature) * thm) list - -> ((string * stature) * thm) list + -> (((unit -> string) * stature) * thm) list end; structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER = @@ -537,7 +537,6 @@ relevance_filter ctxt thres0 decay max_relevant is_built_in_const fudge override facts (chained_ths |> map prop_of) hyp_ts (concl_t |> theory_constify fudge (Context.theory_name thy))) - |> map (apfst (apfst (fn f => f ()))) end end; diff -r 255c6e1fd505 -r 6b65f1ad0e4b src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:03 2012 +0200 @@ -27,9 +27,9 @@ val iter_facts : Proof.context -> params -> int -> thm -> (((unit -> string) * stature) * thm) list - -> ((string * stature) * thm) list + -> (((unit -> string) * stature) * thm) list val run_prover : - Proof.context -> params -> ((string * stature) * thm) list -> thm + Proof.context -> params -> (((unit -> string) * stature) * thm) list -> thm -> prover_result val generate_accessibility : theory -> bool -> string -> unit val generate_features : theory -> bool -> string -> unit @@ -47,7 +47,7 @@ val relevant_facts : Proof.context -> params -> string -> int -> relevance_override -> thm list -> term list -> term -> (((unit -> string) * stature) * thm) list - -> ((string * stature) * thm) list + -> (((unit -> string) * stature) * thm) list end; structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH = @@ -265,7 +265,8 @@ let val problem = {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, - facts = facts |> map Sledgehammer_Provers.Untranslated_Fact} + facts = facts |> map (apfst (apfst (fn name => name ()))) + |> map Sledgehammer_Provers.Untranslated_Fact} val prover = Sledgehammer_Minimize.get_minimizing_prover ctxt Sledgehammer_Provers.Normal (hd provers) @@ -339,10 +340,10 @@ 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 ((name, status), th) => accum @ [((name, status), th)] | NONE => accum (* shouldn't happen *) fun fix_name ((_, stature), th) = - ((th |> Thm.get_name_hint |> fact_name_of, stature), th) + ((fn () => th |> Thm.get_name_hint |> fact_name_of, stature), th) fun do_thm th = let val name = Thm.get_name_hint th @@ -391,7 +392,7 @@ (override as {add, only, ...}) chained_ths hyp_ts concl_t facts = if only then - facts |> map (apfst (apfst (fn f => f ()))) (* ###*) + facts else if max_relevant <= 0 then [] else diff -r 255c6e1fd505 -r 6b65f1ad0e4b src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:03 2012 +0200 @@ -225,6 +225,7 @@ | NONE => I) |> relevant_facts ctxt params (hd provers) max_max_relevant relevance_override chained_ths hyp_ts concl_t + |> map (apfst (apfst (fn name => name ()))) |> tap (fn facts => if debug then label ^ plural_s (length provers) ^ ": " ^