--- 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
--- 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
--- 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
--- 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, ""))
--- 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,
--- 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