(* 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
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 : bool -> bool -> string -> string -> Proof.context ->
Time.time -> isar_step -> preplay_time
type preplay_interface =
{ get_time : label -> preplay_time,
set_time : label -> preplay_time -> unit,
preplay_quietly : Time.time -> isar_step -> preplay_time,
preplay_fail : unit -> bool,
set_preplay_fail : bool -> unit,
overall_preplay_stats : unit -> 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
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 of 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 => (fn ctxt => K (Clasimp.auto_tac ctxt))
| FastforceM => Clasimp.fast_force_tac
| ArithM => Arith_Data.arith_tac
| _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt
(* main function for preplaying isar_steps *)
fun preplay _ _ _ _ _ _ (Let _) = zero_preplay_time
| preplay 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
|> 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_time : label -> preplay_time,
set_time : label -> preplay_time -> unit,
preplay_quietly : Time.time -> isar_step -> preplay_time,
preplay_fail : unit -> bool,
set_preplay_fail : bool -> unit,
overall_preplay_stats : unit -> 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 state.
The preplay times 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_time = K zero_preplay_time,
set_time = K (K ()),
preplay_quietly = K (K zero_preplay_time),
preplay_fail = K false,
set_preplay_fail = K (),
overall_preplay_stats = K (zero_preplay_time, false)}
else
let
(* add local proof facts to context *)
val ctxt = enrich_context proof ctxt
val fail = Unsynchronized.ref false
fun preplay_fail () = !fail
fun set_preplay_fail b = fail := b
val preplay = preplay debug preplay_trace type_enc lam_trans ctxt
(* preplay steps without registering preplay_fails, treating exceptions
like timeouts *)
fun preplay_quietly timeout step =
try (preplay timeout) step
|> the_default (true, timeout)
val preplay_time_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 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 register_preplay_fail lazy_time = Lazy.force lazy_time
handle exn =>
if Exn.is_interrupt exn orelse debug then reraise exn
else (fail := true; some_preplay_time)
fun get_time lbl =
register_preplay_fail
(Canonical_Lbl_Tab.lookup (!preplay_time_tab) lbl |> the)
handle
Option.Option =>
raise Fail "Sledgehammer_Preplay: preplay time table"
fun set_time lbl time =
preplay_time_tab :=
Canonical_Lbl_Tab.update (lbl, Lazy.value time) (!preplay_time_tab)
fun total_preplay_time () =
Canonical_Lbl_Tab.fold
(snd #> register_preplay_fail #> add_preplay_time)
(!preplay_time_tab) zero_preplay_time
fun overall_preplay_stats () = (total_preplay_time (), preplay_fail ())
in
{ get_time = get_time,
set_time = set_time,
preplay_quietly = preplay_quietly,
preplay_fail = preplay_fail,
set_preplay_fail = set_preplay_fail,
overall_preplay_stats = overall_preplay_stats}
end
end