avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
Author: Steffen Juilf Smolka, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Preplaying of Isar proofs.
*)
signature SLEDGEHAMMER_ISAR_PREPLAY =
sig
type play_outcome = Sledgehammer_Proof_Methods.play_outcome
type proof_method = Sledgehammer_Isar_Proof.proof_method
type isar_step = Sledgehammer_Isar_Proof.isar_step
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
type label = Sledgehammer_Isar_Proof.label
val trace : bool Config.T
type isar_preplay_data
val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
val preplay_isar_step_for_method : Proof.context -> bool -> Time.time -> proof_method ->
isar_step -> play_outcome
val preplay_isar_step : Proof.context -> bool -> Time.time -> proof_method list -> isar_step ->
(proof_method * play_outcome) list
val set_preplay_outcomes_of_isar_step : Proof.context -> bool -> Time.time ->
isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit
val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome
val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method ->
play_outcome Lazy.lazy
val fastest_method_of_isar_step : isar_preplay_data -> label -> proof_method
val preplay_outcome_of_isar_proof : isar_preplay_data -> isar_proof -> play_outcome
end;
structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
struct
open ATP_Proof_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
fun enrich_context_with_local_facts proof ctxt =
let
val thy = Proof_Context.theory_of ctxt
fun enrich_with_fact l t =
Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t])
val enrich_with_assms = fold (uncurry enrich_with_fact)
fun enrich_with_proof (Proof (_, assms, isar_steps)) =
enrich_with_assms assms #> fold enrich_with_step isar_steps
and enrich_with_step (Prove (_, _, l, t, subproofs, _, _, _)) =
enrich_with_fact l t #> fold enrich_with_proof subproofs
| enrich_with_step _ = I
in
enrich_with_proof proof ctxt
end
fun preplay_trace ctxt assmsp concl outcome =
let
val ctxt = ctxt |> Config.put show_markup true
val assms = op @ assmsp
val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]")
val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms)
val concl = Syntax.pretty_term ctxt concl
in
tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl])))
end
fun take_time timeout tac arg =
let val timing = Timing.start () in
(TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing)))
handle TimeLimit.TimeOut => Play_Timed_Out timeout
end
fun resolve_fact_names ctxt names =
(names
|>> map string_of_label
|> pairself (maps (thms_of_name ctxt)))
handle ERROR msg => error ("preplay error: " ^ msg)
fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) =
let
val thy = Proof_Context.theory_of ctxt
val concl =
(case try List.last steps of
SOME (Prove (_, [], _, t, _, _, _, _)) => t
| _ => raise Fail "preplay error: malformed subproof")
val var_idx = maxidx_of_term concl + 1
fun var_of_free (x, T) = Var ((x, var_idx), T)
val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees
in
Logic.list_implies (assms |> map snd, concl)
|> subst_free subst
|> Skip_Proof.make_thm thy
end
(* may throw exceptions *)
fun raw_preplay_step_for_method ctxt debug timeout meth
(Prove (_, xs, _, t, subproofs, facts, _, _)) =
let
val goal =
(case xs of
[] => t
| _ =>
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
(cf. "~~/src/Pure/Isar/obtain.ML") *)
let
val frees = map Free xs
val thesis =
Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT))
val thesis_prop = HOLogic.mk_Trueprop thesis
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
in
(* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
end)
val assmsp =
resolve_fact_names ctxt facts
|>> append (map (thm_of_proof ctxt) subproofs)
fun prove () =
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
HEADGOAL (tac_of_proof_method ctxt debug assmsp meth))
handle ERROR msg => error ("Preplay error: " ^ msg)
val play_outcome = take_time timeout prove ()
in
if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
play_outcome
end
fun preplay_isar_step_for_method ctxt debug timeout meth =
try (raw_preplay_step_for_method ctxt debug timeout meth) #> the_default Play_Failed
fun preplay_isar_step ctxt debug timeout hopeless step =
let
fun try_method meth =
(case preplay_isar_step_for_method ctxt debug timeout meth step of
outcome as Played _ => SOME (meth, outcome)
| _ => NONE)
val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless
in
the_list (Par_List.get_some try_method meths)
end
type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table
fun time_of_play (Played time) = time
| time_of_play (Play_Timed_Out time) = time
fun add_preplay_outcomes Play_Failed _ = Play_Failed
| add_preplay_outcomes _ Play_Failed = Play_Failed
| add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
| add_preplay_outcomes play1 play2 =
Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
fun set_preplay_outcomes_of_isar_step ctxt debug timeout preplay_data
(step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
let
fun lazy_preplay meth =
Lazy.lazy (fn () => preplay_isar_step_for_method ctxt debug timeout meth step)
val meths_outcomes = meths_outcomes0
|> map (apsnd Lazy.value)
|> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
in
preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes [])
(!preplay_data)
end
| set_preplay_outcomes_of_isar_step _ _ _ _ _ _ = ()
fun peek_at_outcome outcome = if Lazy.is_finished outcome then Lazy.force outcome else Not_Played
fun get_best_method_outcome force =
tap (List.app (K () o Lazy.future Future.default_params o snd)) (* optional parallelism *)
#> map (apsnd force)
#> sort (play_outcome_ord o pairself snd)
#> hd
fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l =
let
val meths_outcomes as (_, outcome1) :: _ = the (Canonical_Label_Tab.lookup preplay_data l)
in
if forall (not o Lazy.is_finished o snd) meths_outcomes then
(case Lazy.force outcome1 of
outcome as Played _ => outcome
| _ => snd (get_best_method_outcome Lazy.force meths_outcomes))
else
(case get_best_method_outcome peek_at_outcome meths_outcomes of
(_, Not_Played) => snd (get_best_method_outcome Lazy.force meths_outcomes)
| (_, outcome) => outcome)
end
fun preplay_outcome_of_isar_step_for_method preplay_data l =
AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
#> the_default (Lazy.value Not_Played)
fun fastest_method_of_isar_step preplay_data =
the o Canonical_Label_Tab.lookup preplay_data
#> get_best_method_outcome Lazy.force
#> fst
fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths, _)) =
Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths))
| forced_outcome_of_step _ _ = Played Time.zeroTime
fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) =
fold_isar_steps (add_preplay_outcomes o forced_outcome_of_step preplay_data) steps
(Played Time.zeroTime)
end;