# HG changeset patch # User blanchet # Date 1435614293 -7200 # Node ID 79d71bfea3105ce0925fbebf299a4f25f6dabd30 # Parent 27255d1fbe1a377e10d682c73731e8e5081bb244 removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs diff -r 27255d1fbe1a -r 79d71bfea310 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jun 29 21:56:20 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jun 29 23:44:53 2015 +0200 @@ -8,6 +8,7 @@ signature SLEDGEHAMMER = sig + type stature = ATP_Problem_Generate.stature type fact = Sledgehammer_Fact.fact type fact_override = Sledgehammer_Fact.fact_override type proof_method = Sledgehammer_Proof_Methods.proof_method @@ -20,8 +21,8 @@ val timeoutN : string val unknownN : string - val play_one_line_proof : bool -> Time.time -> (string * 'a) list -> Proof.state -> int -> - proof_method * proof_method list list -> (string * 'a) list * (proof_method * play_outcome) + val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int -> + proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome) val string_of_factss : (string * fact list) list -> string val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override -> Proof.state -> bool * (string * string list) @@ -71,48 +72,50 @@ t $ Abs (s, T, add_chained chained u) | add_chained chained t = Logic.list_implies (chained, t) -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 +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 - 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 - |> add_chained (map Thm.prop_of chained) + 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 + |> add_chained (map Thm.prop_of chained) - 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 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 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 + 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 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 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 launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout, preplay_timeout, expect, ...}) mode output_result only learn diff -r 27255d1fbe1a -r 79d71bfea310 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 29 21:56:20 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 29 23:44:53 2015 +0200 @@ -147,7 +147,7 @@ val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods val skolem_methods = Moura_Method :: systematic_methods -fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params +fun isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = let val _ = if debug then writeln "Constructing Isar proof..." else () @@ -407,20 +407,23 @@ #> relabel_isar_proof_nicely #> rationalize_obtains_in_isar_proofs ctxt) in - (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of - 1 => + (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of + (0, 1) => one_line_proof_text ctxt 0 (if play_outcome_ord (play_outcome, one_line_play) = LESS then (case isar_proof of Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) => - let val used_facts' = filter (member (op =) gfs o fst) used_facts in + let + val used_facts' = filter (fn (s, (sc, _)) => + member (op =) gfs s andalso sc <> Chained) used_facts + in ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count) end) else one_line_params) ^ (if isar_proofs = SOME true then "\n(No Isar proof available.)" else "") - | num_steps => + | (_, num_steps) => let val msg = (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @ @@ -453,7 +456,7 @@ (one_line_params as ((_, preplay), _, _, _)) = (if isar_proofs = SOME true orelse (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then - isar_proof_text ctxt debug isar_proofs smt_proofs isar_params + isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params else one_line_proof_text ctxt num_chained) one_line_params