src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

reset timing information after changes

(*  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_Reconstructor.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 =
    {reset_preplay_outcomes: isar_step -> unit,
     set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
     preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
     preplay_quietly: Time.time -> isar_step -> play_outcome,
     overall_preplay_outcome: isar_proof -> play_outcome}

  val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time ->
    isar_proof -> isar_preplay_data
end;

structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
struct

open Sledgehammer_Util
open Sledgehammer_Reconstructor
open Sledgehammer_Isar_Proof

val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)

fun preplay_trace ctxt assmsp concl result =
  let
    val ctxt = ctxt |> Config.put show_markup true
    val assms = op @ assmsp
    val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str
    val nr_of_assms = length assms
    val assms = assms
      |> map (Display.pretty_thm ctxt)
      |> (fn [] => Pretty.str ""
           | [a] => a
           | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms)  (* Syntax.pretty_term!? *)
    val concl = concl |> Syntax.pretty_term ctxt
    val trace_list = []
      |> cons concl
      |> nr_of_assms > 0 ? cons (Pretty.str "\<Longrightarrow>")
      |> cons assms
      |> cons time
    val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list)
  in
    tracing (Pretty.string_of pretty_trace)
  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

fun tac_of_method meth type_enc lam_trans ctxt (local_facts, global_facts) =
  Method.insert_tac local_facts THEN'
  (case meth of
    Meson_Method => Meson.meson_tac ctxt global_facts
  | Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt global_facts
  | _ =>
    Method.insert_tac global_facts THEN'
    (case meth of
      Simp_Method => Simplifier.asm_full_simp_tac ctxt
    | Simp_Size_Method =>
      Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
    | Auto_Method => K (Clasimp.auto_tac ctxt)
    | Fastforce_Method => Clasimp.fast_force_tac ctxt
    | Force_Method => Clasimp.force_tac ctxt
    | Arith_Method => Arith_Data.arith_tac ctxt
    | Blast_Method => blast_tac ctxt
    | Algebra_Method => Groebner.algebra_tac [] [] ctxt
    | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))

(* main function for preplaying Isar steps; may throw exceptions *)
fun preplay_raw debug type_enc lam_trans ctxt timeout meth
      (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
    let
      val goal =
        (case xs of
          [] => t
        | _ =>
          (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
             (cf. "~~/src/Pure/Isar/obtain.ML") *)
          let
            (* FIXME: generate fresh name *)
            val thesis = Free ("thesis", HOLogic.boolT)
            val thesis_prop = thesis |> HOLogic.mk_Trueprop
            val frees = map Free xs

            (* !!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 facts =
        resolve_fact_names ctxt fact_names
        |>> append (map (thm_of_proof ctxt) subproofs)

      val ctxt' = ctxt |> silence_reconstructors debug

      fun prove () =
        Goal.prove ctxt' [] [] goal (fn {context = ctxt, ...} =>
          HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts))
        handle ERROR msg => error ("Preplay error: " ^ msg)

      val play_outcome = take_time timeout prove ()
    in
      (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else ();
       play_outcome)
    end

type isar_preplay_data =
  {reset_preplay_outcomes: isar_step -> unit,
   set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
   preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
   preplay_quietly: Time.time -> isar_step -> play_outcome,
   overall_preplay_outcome: isar_proof -> play_outcome}

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 (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

fun merge_preplay_outcomes _ Play_Failed = Play_Failed
  | merge_preplay_outcomes Play_Failed _ = Play_Failed
  | merge_preplay_outcomes (Play_Timed_Out t1) (Play_Timed_Out t2) =
    Play_Timed_Out (Time.+ (t1, t2))
  | merge_preplay_outcomes (Played t1) (Play_Timed_Out t2) = Play_Timed_Out (Time.+ (t1, t2))
  | merge_preplay_outcomes (Play_Timed_Out t1) (Played t2) = Play_Timed_Out (Time.+ (t1, t2))
  | merge_preplay_outcomes (Played t1) (Played t2) = Played (Time.+ (t1, t2))

(* 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.

   Precondition: The proof must be labeled canonically; cf.
   "Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *)
fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
  if not do_preplay then
    (* the "dont_preplay" option pretends that everything works just fine *)
    {reset_preplay_outcomes = K (),
     set_preplay_outcome = K (K (K ())),
     preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
     preplay_quietly = K (K (Played Time.zeroTime)),
     overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
  else
    let
      val ctxt = enrich_context_with_local_facts proof ctxt

      fun preplay quietly timeout meth step =
        preplay_raw debug type_enc lam_trans ctxt timeout meth step
        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)
             else
               ();
             Play_Failed)

      (* preplay steps treating exceptions like timeouts *)
      fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, (meth :: _) :: _))) =
          preplay true timeout meth step
        | preplay_quietly _ _ = Played Time.zeroTime

      val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty

      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, methss))) =
          preplay_tab := Canonical_Label_Tab.update (l, maps (map (fn meth =>
              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
            (!preplay_tab)
        | reset_preplay_outcomes _ = ()

      fun set_preplay_outcome l meth result =
        preplay_tab := Canonical_Label_Tab.map_entry l
          (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)

      fun preplay_outcome l meth =
        (case Canonical_Label_Tab.lookup (!preplay_tab) l of
          SOME meths_outcomes =>
          (case AList.lookup (op =) meths_outcomes meth of
            SOME outcome => outcome
          | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
        | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")

      val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()

      fun result_of_step (Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
          Lazy.force (preplay_outcome l meth)
        | result_of_step _ = Played Time.zeroTime

      fun overall_preplay_outcome (Proof (_, _, steps)) =
        fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
    in
      {reset_preplay_outcomes = reset_preplay_outcomes,
       set_preplay_outcome = set_preplay_outcome,
       preplay_outcome = preplay_outcome,
       preplay_quietly = preplay_quietly,
       overall_preplay_outcome = overall_preplay_outcome}
    end

end;