--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Jun 17 12:37:43 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Jun 17 12:40:18 2016 +0200
@@ -63,49 +63,51 @@
fun is_metis_method (Metis_Method _) = true
| is_metis_method _ = false
-fun play_one_line_proof minimize timeout used_facts0 state i (preferred_meth, methss) =
- let val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts0 in
- if timeout = Time.zeroTime then
- (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
- else
- let
- val ctxt = Proof.context_of state
+fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) =
+ (if timeout = Time.zeroTime then
+ (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
+ else
+ let
+ val ctxt = Proof.context_of state
- val fact_names = map fst used_facts
- val {facts = chained, goal, ...} = Proof.goal state
- val goal_t = Logic.get_goal (Thm.prop_of goal) i
+ val fact_names = map fst used_facts
+ val {facts = chained, goal, ...} = Proof.goal state
+ val goal_t = Logic.get_goal (Thm.prop_of goal) i
- fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
- | try_methss ress [] =
- (used_facts,
- (case AList.lookup (op =) ress preferred_meth of
- SOME play => (preferred_meth, play)
- | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress))))
- | try_methss ress (meths :: methss) =
- let
- fun mk_step fact_names meths =
- Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
- in
- (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of
- (res as (meth, Played time)) :: _ =>
- (* if a fact is needed by an ATP, it will be needed by "metis" *)
- if not minimize orelse is_metis_method meth then
- (used_facts, res)
- else
- let
- val (time', used_names') =
- minimized_isar_step ctxt chained time (mk_step fact_names [meth])
- ||> (facts_of_isar_step #> snd)
- val used_facts' = filter (member (op =) used_names' o fst) used_facts
- in
- (used_facts', (meth, Played time'))
- end
- | ress' => try_methss (ress' @ ress) methss)
- end
- in
- try_methss [] methss
- end
- end
+ fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
+ | try_methss ress [] =
+ (used_facts,
+ (case AList.lookup (op =) ress preferred_meth of
+ SOME play => (preferred_meth, play)
+ | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress))))
+ | try_methss ress (meths :: methss) =
+ let
+ fun mk_step fact_names meths =
+ Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
+ in
+ (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of
+ (res as (meth, Played time)) :: _ =>
+ (* if a fact is needed by an ATP, it will be needed by "metis" *)
+ if not minimize orelse is_metis_method meth then
+ (used_facts, res)
+ else
+ let
+ val (time', used_names') =
+ minimized_isar_step ctxt chained time (mk_step fact_names [meth])
+ ||> (facts_of_isar_step #> snd)
+ val used_facts' = filter (member (op =) used_names' o fst) used_facts
+ in
+ (used_facts', (meth, Played time'))
+ end
+ | ress' => try_methss (ress' @ ress) methss)
+ end
+ in
+ try_methss [] methss
+ end)
+ |> (fn (used_facts, (meth, play)) =>
+ (used_facts |> not (proof_method_distinguishes_chained_and_direct meth)
+ ? filter_out (fn (_, (sc, _)) => sc = Chained),
+ (meth, play)))
fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout,
expect, ...}) mode writeln_result only learn