# HG changeset patch # User blanchet # Date 1359651245 -3600 # Node ID ce4290c33d732f4dc991f521ac99bf790bac1fac # Parent 5f2788c3812701a6ad3cebc173c06a383ec109d4 eliminated needless speed optimization -- and simplified code quite a bit diff -r 5f2788c38127 -r ce4290c33d73 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 @@ -490,8 +490,7 @@ val prover = get_prover ctxt prover_name params goal facts val problem = {state = st', goal = goal, subgoal = i, - subgoal_count = Sledgehammer_Util.subgoal_count st, - facts = facts |> map Sledgehammer_Provers.Untranslated_Fact} + subgoal_count = Sledgehammer_Util.subgoal_count st, facts = facts} in prover params (K (K (K ""))) problem end)) () handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut | Fail "inappropriate" => failed ATP_Proof.Inappropriate diff -r 5f2788c38127 -r ce4290c33d73 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,7 +45,7 @@ |> #1 val problem = {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - facts = facts |> map Untranslated_Fact} + facts = facts} in (case prover params (K (K (K ""))) problem of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME diff -r 5f2788c38127 -r ce4290c33d73 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 @@ -532,7 +532,7 @@ let val problem = {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, - facts = facts |> map Untranslated_Fact} + facts = facts} in get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K ""))) problem diff -r 5f2788c38127 -r ce4290c33d73 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 31 17:54:05 2013 +0100 @@ -68,8 +68,7 @@ else "") ^ "...") val {goal, ...} = Proof.goal state - val facts = - facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) + val facts = facts |> maps (fn (n, ths) => map (pair n) ths) val params = {debug = debug, verbose = verbose, overlord = overlord, blocking = true, provers = provers, type_enc = type_enc, strict = strict, @@ -309,10 +308,8 @@ val (used_facts, (preplay, message, _)) = if minimize then minimize_facts do_learn minimize_name params - (mode <> Normal orelse not verbose) subgoal - subgoal_count state - (filter_used_facts true used_facts - (map (apsnd single o untranslated_fact) facts)) + (mode <> Normal orelse not verbose) subgoal subgoal_count state + (filter_used_facts true used_facts (map (apsnd single) facts)) |>> Option.map (map fst) else (SOME used_facts, (preplay, message, "")) diff -r 5f2788c38127 -r ce4290c33d73 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 31 17:54:05 2013 +0100 @@ -11,6 +11,7 @@ type failure = ATP_Proof.failure type stature = ATP_Problem_Generate.stature type type_enc = ATP_Problem_Generate.type_enc + type fact = Sledgehammer_Fact.fact type reconstructor = Sledgehammer_Reconstruct.reconstructor type play = Sledgehammer_Reconstruct.play type minimize_command = Sledgehammer_Reconstruct.minimize_command @@ -62,16 +63,12 @@ threshold_divisor : real, ridiculous_threshold : real} - datatype prover_fact = - Untranslated_Fact of (string * stature) * thm | - SMT_Weighted_Fact of (string * stature) * (int option * thm) - type prover_problem = {state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, - facts : prover_fact list} + facts : fact list} type prover_result = {outcome : failure option, @@ -123,10 +120,6 @@ val weight_smt_fact : Proof.context -> int -> ((string * stature) * thm) * int -> (string * stature) * (int option * thm) - val untranslated_fact : prover_fact -> (string * stature) * thm - val smt_weighted_fact : - Proof.context -> int -> prover_fact * int - -> (string * stature) * (int option * thm) val supported_provers : Proof.context -> unit val kill_provers : unit -> unit val running_provers : unit -> unit @@ -149,6 +142,7 @@ open ATP_Proof_Reconstruct open Metis_Tactic open Sledgehammer_Util +open Sledgehammer_Fact open Sledgehammer_Reconstruct @@ -355,16 +349,12 @@ threshold_divisor : real, ridiculous_threshold : real} -datatype prover_fact = - Untranslated_Fact of (string * stature) * thm | - SMT_Weighted_Fact of (string * stature) * (int option * thm) - type prover_problem = {state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, - facts : prover_fact list} + facts : fact list} type prover_result = {outcome : failure option, @@ -430,12 +420,6 @@ (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy)) end -fun untranslated_fact (Untranslated_Fact p) = p - | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th) -fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p - | smt_weighted_fact ctxt num_facts (fact, j) = - (untranslated_fact fact, j) |> weight_smt_fact ctxt num_facts - fun overlord_file_location_for_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) @@ -773,7 +757,6 @@ cache_value else facts - |> map untranslated_fact |> not sound ? filter_out (is_dangerous_prop ctxt o prop_of o snd) |> take num_facts @@ -887,8 +870,7 @@ Lazy.lazy (fn () => let val used_pairs = - facts |> map untranslated_fact - |> filter_used_facts false used_facts + facts |> filter_used_facts false used_facts in play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal (hd reconstrs) reconstrs @@ -1079,8 +1061,9 @@ let val ctxt = Proof.context_of state val num_facts = length facts - val facts = facts ~~ (0 upto num_facts - 1) - |> map (smt_weighted_fact ctxt num_facts) + val facts = + facts ~~ (0 upto num_facts - 1) + |> map (weight_smt_fact ctxt num_facts) val {outcome, used_facts = used_pairs, run_time} = smt_filter_loop name params state goal subgoal facts val used_facts = used_pairs |> map fst @@ -1126,11 +1109,10 @@ SMT else raise Fail ("unknown reconstructor: " ^ quote name) - val used_pairs = facts |> map untranslated_fact - val used_facts = used_pairs |> map fst + val used_facts = facts |> map fst in case play_one_line_proof (if mode = Minimize then Normal else mode) debug - verbose timeout used_pairs state subgoal reconstr + verbose timeout facts state subgoal reconstr [reconstr] of play as Played (_, time) => {outcome = NONE, used_facts = used_facts, run_time = time, diff -r 5f2788c38127 -r ce4290c33d73 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 @@ -81,12 +81,11 @@ subgoal_count = subgoal_count, facts = facts |> not (Sledgehammer_Provers.is_ho_atp ctxt name) - ? filter_out (curry (op =) Induction o snd o snd o fst - o untranslated_fact) + ? filter_out (curry (op =) Induction o snd o snd o fst) |> take num_facts} fun print_used_facts used_facts = tag_list 1 facts - |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j)) + |> map (fn (j, fact) => fact |> apsnd (K j)) |> filter_used_facts false used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas @@ -196,12 +195,10 @@ val (smts, (ueq_atps, full_atps)) = provers |> List.partition (is_smt_prover ctxt) ||> List.partition (is_unit_equational_atp ctxt) - fun launch_provers state get_facts translate provers = + fun launch_provers state get_facts provers = let val facts = get_facts () val num_facts = length facts - val facts = facts ~~ (0 upto num_facts - 1) - |> map (translate num_facts) val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, facts = facts} @@ -264,18 +261,15 @@ accum) else launch_provers state (get_facts label is_appropriate_prop o K atps) - (K (Untranslated_Fact o fst)) atps + atps fun launch_smts accum = if null smts then accum else - let - val facts = get_facts "SMT solver" NONE smts - val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt - in + let val facts = get_facts "SMT solver" NONE smts in smts |> map (`(class_of_smt_solver ctxt)) |> AList.group (op =) - |> map (snd #> launch_provers state (K facts) weight #> fst) + |> map (snd #> launch_provers state (K facts) #> fst) |> max_outcome_code |> rpair state end val launch_full_atps = launch_atps "ATP" NONE full_atps