(* Title: HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
Author: Jasmin Blanchette, TU Muenchen
Author: Steffen Juilf Smolka, TU Muenchen
Preplaying of isar proofs.
*)
signature SLEDGEHAMMER_PREPLAY =
sig
type isar_proof = Sledgehammer_Proof.isar_proof
type isar_step = Sledgehammer_Proof.isar_step
type label = Sledgehammer_Proof.label
eqtype preplay_time
datatype preplay_result =
PplFail of exn |
PplSucc of preplay_time
val zero_preplay_time : preplay_time
val some_preplay_time : preplay_time
val add_preplay_time : preplay_time -> preplay_time -> preplay_time
val string_of_preplay_time : preplay_time -> string
(*val preplay_raw : bool -> bool -> string -> string -> Proof.context ->
Time.time -> isar_step -> preplay_time*)
type preplay_interface =
{ get_preplay_result : label -> preplay_result,
set_preplay_result : label -> preplay_result -> unit,
get_preplay_time : label -> preplay_time,
set_preplay_time : label -> preplay_time -> unit,
preplay_quietly : Time.time -> isar_step -> preplay_time,
(* the returned flag signals a preplay failure *)
overall_preplay_stats : isar_proof -> preplay_time * bool }
val proof_preplay_interface :
bool -> Proof.context -> string -> string -> bool -> Time.time -> bool
-> isar_proof -> preplay_interface
end
structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
struct
open Sledgehammer_Util
open Sledgehammer_Proof
(* The boolean flag encodes whether the time is exact (false) or an lower bound
(true):
(t, false) = "t ms"
(t, true) = "> t ms" *)
type preplay_time = bool * Time.time
datatype preplay_result =
PplFail of exn |
PplSucc of preplay_time
val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
val some_preplay_time = (true, Time.zeroTime) (* > 0 ms *)
fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
val string_of_preplay_time = ATP_Util.string_of_ext_time
(* preplay tracing *)
fun preplay_trace ctxt assms concl time =
let
val ctxt = ctxt |> Config.put show_markup true
val time = "[" ^ (string_of_preplay_time time) ^ "]" |> Pretty.str
val nr_of_assms = length assms
val assms = assms |> map (Display.pretty_thm ctxt)
|> (fn [] => Pretty.str ""
| [a] => a
| assms => Pretty.enum ";" "⟦" "⟧" assms)
val concl = concl |> Syntax.pretty_term ctxt
val trace_list = [] |> cons concl
|> nr_of_assms>0 ? cons (Pretty.str "⟹")
|> cons assms
|> cons time
val pretty_trace = Pretty.blk(2, Pretty.breaks trace_list)
in tracing (Pretty.string_of pretty_trace) end
(* timing *)
fun take_time timeout tac arg =
let
val timing = Timing.start ()
in
(TimeLimit.timeLimit timeout tac arg;
Timing.result timing |> #cpu |> pair false)
handle TimeLimit.TimeOut => (true, timeout)
end
(* lookup facts in context *)
fun resolve_fact_names ctxt names =
(names
|>> map string_of_label
|> op @
|> maps (thms_of_name ctxt))
handle ERROR msg => error ("preplay error: " ^ msg)
(* turn terms/proofs into theorems *)
fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
fun thm_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) =
let
val concl = (case try List.last steps of
SOME (Prove (_, Fix [], _, 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 substitutions =
map (`var_of_free #> swap #> apfst Free) fixed_frees
in
Logic.list_implies (assms |> map snd, concl)
|> subst_free substitutions
|> thm_of_term ctxt
end
(* mapping from proof methods to tactics *)
fun tac_of_method method type_enc lam_trans ctxt facts =
case method of
MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
| _ =>
Method.insert_tac facts
THEN' (case method of
SimpM => Simplifier.asm_full_simp_tac
| AutoM => Clasimp.auto_tac #> K
| FastforceM => Clasimp.fast_force_tac
| ForceM => Clasimp.force_tac
| ArithM => Arith_Data.arith_tac
| BlastM => blast_tac
| _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt
(* main function for preplaying isar_steps; may throw exceptions *)
fun preplay_raw _ _ _ _ _ _ (Let _) = zero_preplay_time
| preplay_raw debug trace type_enc lam_trans ctxt timeout
(Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) =
let
val (prop, obtain) =
(case xs of
[] => (t, false)
| _ =>
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
(see ~~/src/Pure/Isar/obtain.ML) *)
let
val thesis = Term.Free ("thesis", HOLogic.boolT)
val thesis_prop = thesis |> HOLogic.mk_Trueprop
val frees = map Term.Free xs
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
val inner_prop =
fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
(* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
val prop =
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
in
(prop, true)
end)
val facts =
map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
|> Config.put Lin_Arith.verbose debug
|> obtain ? Config.put Metis_Tactic.new_skolem true
val goal =
Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop
fun tac {context = ctxt, prems = _} =
HEADGOAL (tac_of_method proof_method type_enc lam_trans ctxt facts)
fun run_tac () = goal tac
handle ERROR msg => error ("Preplay error: " ^ msg)
val preplay_time = take_time timeout run_tac ()
in
(* tracing *)
(if trace then preplay_trace ctxt facts prop preplay_time else () ;
preplay_time)
end
(*** proof preplay interface ***)
type preplay_interface =
{ get_preplay_result : label -> preplay_result,
set_preplay_result : label -> preplay_result -> unit,
get_preplay_time : label -> preplay_time,
set_preplay_time : label -> preplay_time -> unit,
preplay_quietly : Time.time -> isar_step -> preplay_time,
(* the returned flag signals a preplay failure *)
overall_preplay_stats : isar_proof -> preplay_time * bool }
(* enriches context with local proof facts *)
fun enrich_context 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 (_, Assume assms, isar_steps)) =
enrich_with_assms assms #> fold enrich_with_step isar_steps
and enrich_with_step (Let _) = I
| enrich_with_step (Prove (_, _, l, t, subproofs, _)) =
enrich_with_fact l t #> fold enrich_with_proof subproofs
in
enrich_with_proof proof ctxt
end
(* Given a proof, produces an imperative preplay interface with a shared table
mapping from labels to preplay results.
The preplay results are caluclated lazyly and cached to avoid repeated
calculation.
PRE CONDITION: the proof must be labeled canocially, see
Slegehammer_Proof.relabel_proof_canonically
*)
fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
preplay_timeout preplay_trace proof : preplay_interface =
if not do_preplay then
(* the dont_preplay option pretends that everything works just fine *)
{ get_preplay_result = K (PplSucc zero_preplay_time),
set_preplay_result = K (K ()),
get_preplay_time = K zero_preplay_time,
set_preplay_time = K (K ()),
preplay_quietly = K (K zero_preplay_time),
overall_preplay_stats = K (zero_preplay_time, false)}
else
let
(* add local proof facts to context *)
val ctxt = enrich_context proof ctxt
fun preplay quietly timeout step =
preplay_raw debug preplay_trace type_enc lam_trans ctxt timeout step
|> PplSucc
handle exn =>
if Exn.is_interrupt exn then
reraise exn
else if not quietly andalso debug then
(warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n "
^ @{make_string} exn);
PplFail exn)
else
PplFail exn
(* preplay steps treating exceptions like timeouts *)
fun preplay_quietly timeout step =
case preplay true timeout step of
PplSucc preplay_time => preplay_time
| PplFail _ => (true, timeout)
val preplay_tab =
let
fun add_step_to_tab step tab =
case label_of_step step of
NONE => tab
| SOME l =>
Canonical_Lbl_Tab.update_new
(l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy)
tab
handle Canonical_Lbl_Tab.DUP _ =>
raise Fail "Sledgehammer_Preplay: preplay time table"
in
Canonical_Lbl_Tab.empty
|> fold_isar_steps add_step_to_tab (steps_of_proof proof)
|> Unsynchronized.ref
end
fun get_preplay_result lbl =
Canonical_Lbl_Tab.lookup (!preplay_tab) lbl |> the |> Lazy.force
handle
Option.Option =>
raise Fail "Sledgehammer_Preplay: preplay time table"
fun set_preplay_result lbl result =
preplay_tab :=
Canonical_Lbl_Tab.update (lbl, Lazy.value result) (!preplay_tab)
fun get_preplay_time lbl =
case get_preplay_result lbl of
PplSucc preplay_time => preplay_time
| PplFail _ => some_preplay_time (* best approximation possible *)
fun set_preplay_time lbl time = set_preplay_result lbl (PplSucc time)
fun overall_preplay_stats (Proof(_, _, steps)) =
let
fun result_of_step step =
try (label_of_step #> the #> get_preplay_result) step
|> the_default (PplSucc zero_preplay_time)
fun do_step step =
case result_of_step step of
PplSucc preplay_time => apfst (add_preplay_time preplay_time)
| PplFail _ => apsnd (K true)
in
fold_isar_steps do_step steps (zero_preplay_time, false)
end
in
{ get_preplay_result = get_preplay_result,
set_preplay_result = set_preplay_result,
get_preplay_time = get_preplay_time,
set_preplay_time = set_preplay_time,
preplay_quietly = preplay_quietly,
overall_preplay_stats = overall_preplay_stats}
end
end