src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
author blanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 55243 66709d41601e
parent 55223 3c593bad6b31
child 55244 12e1a5d8ee48
permissions -rw-r--r--
reset timing information after changes
blanchet@55202
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
blanchet@54712
     2
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@50923
     3
    Author:     Jasmin Blanchette, TU Muenchen
smolkas@50923
     4
blanchet@54763
     5
Preplaying of Isar proofs.
smolkas@50923
     6
*)
smolkas@50923
     7
blanchet@55202
     8
signature SLEDGEHAMMER_ISAR_PREPLAY =
smolkas@50923
     9
sig
blanchet@54828
    10
  type play_outcome = Sledgehammer_Reconstructor.play_outcome
blanchet@55223
    11
  type proof_method = Sledgehammer_Isar_Proof.proof_method
blanchet@55212
    12
  type isar_step = Sledgehammer_Isar_Proof.isar_step
blanchet@55202
    13
  type isar_proof = Sledgehammer_Isar_Proof.isar_proof
blanchet@55202
    14
  type label = Sledgehammer_Isar_Proof.label
smolkas@52556
    15
blanchet@55212
    16
  val trace : bool Config.T
smolkas@52556
    17
blanchet@55213
    18
  type isar_preplay_data =
blanchet@55243
    19
    {reset_preplay_outcomes: isar_step -> unit,
blanchet@55223
    20
     set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
blanchet@55243
    21
     preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
blanchet@54828
    22
     preplay_quietly: Time.time -> isar_step -> play_outcome,
blanchet@54831
    23
     overall_preplay_outcome: isar_proof -> play_outcome}
smolkas@52556
    24
blanchet@55213
    25
  val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time ->
blanchet@55213
    26
    isar_proof -> isar_preplay_data
blanchet@54504
    27
end;
smolkas@50923
    28
blanchet@55202
    29
structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
smolkas@50923
    30
struct
smolkas@50923
    31
smolkas@50923
    32
open Sledgehammer_Util
blanchet@54828
    33
open Sledgehammer_Reconstructor
blanchet@55202
    34
open Sledgehammer_Isar_Proof
smolkas@50923
    35
blanchet@54763
    36
val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
smolkas@50924
    37
blanchet@55194
    38
fun preplay_trace ctxt assmsp concl result =
smolkas@51879
    39
  let
smolkas@51879
    40
    val ctxt = ctxt |> Config.put show_markup true
blanchet@55194
    41
    val assms = op @ assmsp
blanchet@54828
    42
    val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str
smolkas@51879
    43
    val nr_of_assms = length assms
blanchet@54761
    44
    val assms = assms
blanchet@54761
    45
      |> map (Display.pretty_thm ctxt)
blanchet@54761
    46
      |> (fn [] => Pretty.str ""
blanchet@54761
    47
           | [a] => a
blanchet@54761
    48
           | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms)  (* Syntax.pretty_term!? *)
smolkas@51879
    49
    val concl = concl |> Syntax.pretty_term ctxt
blanchet@54761
    50
    val trace_list = []
blanchet@54761
    51
      |> cons concl
blanchet@54761
    52
      |> nr_of_assms > 0 ? cons (Pretty.str "\<Longrightarrow>")
blanchet@54761
    53
      |> cons assms
blanchet@54761
    54
      |> cons time
blanchet@53761
    55
    val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list)
blanchet@54761
    56
  in
blanchet@54761
    57
    tracing (Pretty.string_of pretty_trace)
blanchet@54761
    58
  end
smolkas@51879
    59
smolkas@50923
    60
fun take_time timeout tac arg =
blanchet@54761
    61
  let val timing = Timing.start () in
blanchet@54828
    62
    (TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing)))
blanchet@54828
    63
    handle TimeLimit.TimeOut => Play_Timed_Out timeout
smolkas@50923
    64
  end
smolkas@50923
    65
smolkas@50923
    66
fun resolve_fact_names ctxt names =
smolkas@51179
    67
  (names
blanchet@54761
    68
   |>> map string_of_label
blanchet@55194
    69
   |> pairself (maps (thms_of_name ctxt)))
smolkas@51179
    70
  handle ERROR msg => error ("preplay error: " ^ msg)
smolkas@50923
    71
blanchet@54700
    72
fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) =
smolkas@50923
    73
  let
blanchet@54761
    74
    val thy = Proof_Context.theory_of ctxt
blanchet@54761
    75
blanchet@54700
    76
    val concl = 
blanchet@54700
    77
      (case try List.last steps of
blanchet@54700
    78
        SOME (Prove (_, [], _, t, _, _)) => t
blanchet@54700
    79
      | _ => raise Fail "preplay error: malformed subproof")
blanchet@54761
    80
smolkas@51178
    81
    val var_idx = maxidx_of_term concl + 1
blanchet@54761
    82
    fun var_of_free (x, T) = Var ((x, var_idx), T)
blanchet@54761
    83
    val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees
smolkas@51178
    84
  in
smolkas@51179
    85
    Logic.list_implies (assms |> map snd, concl)
blanchet@54761
    86
    |> subst_free subst
blanchet@54761
    87
    |> Skip_Proof.make_thm thy
smolkas@51178
    88
  end
smolkas@51178
    89
blanchet@55194
    90
fun tac_of_method meth type_enc lam_trans ctxt (local_facts, global_facts) =
blanchet@55194
    91
  Method.insert_tac local_facts THEN'
blanchet@54766
    92
  (case meth of
blanchet@55194
    93
    Meson_Method => Meson.meson_tac ctxt global_facts
blanchet@55194
    94
  | Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt global_facts
smolkas@52592
    95
  | _ =>
blanchet@55194
    96
    Method.insert_tac global_facts THEN'
blanchet@54766
    97
    (case meth of
blanchet@55194
    98
      Simp_Method => Simplifier.asm_full_simp_tac ctxt
blanchet@54838
    99
    | Simp_Size_Method =>
blanchet@54838
   100
      Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
blanchet@54765
   101
    | Auto_Method => K (Clasimp.auto_tac ctxt)
blanchet@54765
   102
    | Fastforce_Method => Clasimp.fast_force_tac ctxt
blanchet@54765
   103
    | Force_Method => Clasimp.force_tac ctxt
blanchet@54765
   104
    | Arith_Method => Arith_Data.arith_tac ctxt
blanchet@54765
   105
    | Blast_Method => blast_tac ctxt
blanchet@55219
   106
    | Algebra_Method => Groebner.algebra_tac [] [] ctxt
blanchet@55202
   107
    | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
smolkas@52592
   108
blanchet@54761
   109
(* main function for preplaying Isar steps; may throw exceptions *)
blanchet@55223
   110
fun preplay_raw debug type_enc lam_trans ctxt timeout meth
blanchet@55223
   111
      (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
blanchet@54761
   112
    let
blanchet@54763
   113
      val goal =
blanchet@54761
   114
        (case xs of
blanchet@54761
   115
          [] => t
blanchet@54761
   116
        | _ =>
blanchet@54761
   117
          (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
blanchet@54761
   118
             (cf. "~~/src/Pure/Isar/obtain.ML") *)
blanchet@54761
   119
          let
blanchet@54813
   120
            (* FIXME: generate fresh name *)
blanchet@54813
   121
            val thesis = Free ("thesis", HOLogic.boolT)
blanchet@54761
   122
            val thesis_prop = thesis |> HOLogic.mk_Trueprop
blanchet@54813
   123
            val frees = map Free xs
smolkas@50923
   124
blanchet@54761
   125
            (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
blanchet@54761
   126
            val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
blanchet@54761
   127
          in
blanchet@54761
   128
            (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
smolkas@50923
   129
            Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
blanchet@54761
   130
          end)
blanchet@54761
   131
blanchet@55194
   132
      val facts =
blanchet@55194
   133
        resolve_fact_names ctxt fact_names
blanchet@55194
   134
        |>> append (map (thm_of_proof ctxt) subproofs)
blanchet@55194
   135
blanchet@55170
   136
      val ctxt' = ctxt |> silence_reconstructors debug
blanchet@54761
   137
blanchet@54817
   138
      fun prove () =
blanchet@54817
   139
        Goal.prove ctxt' [] [] goal (fn {context = ctxt, ...} =>
blanchet@54817
   140
          HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts))
blanchet@54817
   141
        handle ERROR msg => error ("Preplay error: " ^ msg)
blanchet@54761
   142
blanchet@54828
   143
      val play_outcome = take_time timeout prove ()
blanchet@54761
   144
    in
blanchet@54828
   145
      (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else ();
blanchet@54828
   146
       play_outcome)
blanchet@54761
   147
    end
smolkas@52556
   148
blanchet@55213
   149
type isar_preplay_data =
blanchet@55243
   150
  {reset_preplay_outcomes: isar_step -> unit,
blanchet@55223
   151
   set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
blanchet@55243
   152
   preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
blanchet@54828
   153
   preplay_quietly: Time.time -> isar_step -> play_outcome,
blanchet@54831
   154
   overall_preplay_outcome: isar_proof -> play_outcome}
smolkas@52556
   155
blanchet@54761
   156
fun enrich_context_with_local_facts proof ctxt =
smolkas@52556
   157
  let
smolkas@52556
   158
    val thy = Proof_Context.theory_of ctxt
smolkas@52556
   159
smolkas@52556
   160
    fun enrich_with_fact l t =
blanchet@54761
   161
      Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t])
smolkas@52556
   162
smolkas@52556
   163
    val enrich_with_assms = fold (uncurry enrich_with_fact)
smolkas@52556
   164
blanchet@54700
   165
    fun enrich_with_proof (Proof (_, assms, isar_steps)) =
smolkas@52556
   166
      enrich_with_assms assms #> fold enrich_with_step isar_steps
smolkas@52556
   167
    and enrich_with_step (Let _) = I
smolkas@52556
   168
      | enrich_with_step (Prove (_, _, l, t, subproofs, _)) =
blanchet@54761
   169
        enrich_with_fact l t #> fold enrich_with_proof subproofs
smolkas@52556
   170
  in
smolkas@52556
   171
    enrich_with_proof proof ctxt
smolkas@50923
   172
  end
smolkas@50923
   173
blanchet@54828
   174
fun merge_preplay_outcomes _ Play_Failed = Play_Failed
blanchet@54828
   175
  | merge_preplay_outcomes Play_Failed _ = Play_Failed
blanchet@54831
   176
  | merge_preplay_outcomes (Play_Timed_Out t1) (Play_Timed_Out t2) =
blanchet@54831
   177
    Play_Timed_Out (Time.+ (t1, t2))
blanchet@54828
   178
  | merge_preplay_outcomes (Played t1) (Play_Timed_Out t2) = Play_Timed_Out (Time.+ (t1, t2))
blanchet@54828
   179
  | merge_preplay_outcomes (Play_Timed_Out t1) (Played t2) = Play_Timed_Out (Time.+ (t1, t2))
blanchet@54828
   180
  | merge_preplay_outcomes (Played t1) (Played t2) = Played (Time.+ (t1, t2))
blanchet@54827
   181
blanchet@54761
   182
(* Given a proof, produces an imperative preplay interface with a shared table mapping from labels
blanchet@54761
   183
   to preplay results. The preplay results are caluclated lazyly and cached to avoid repeated
smolkas@52556
   184
   calculation.
smolkas@52556
   185
blanchet@54763
   186
   Precondition: The proof must be labeled canonically; cf.
blanchet@55213
   187
   "Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *)
blanchet@55213
   188
fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
smolkas@52556
   189
  if not do_preplay then
blanchet@54828
   190
    (* the "dont_preplay" option pretends that everything works just fine *)
blanchet@55243
   191
    {reset_preplay_outcomes = K (),
blanchet@55223
   192
     set_preplay_outcome = K (K (K ())),
blanchet@55243
   193
     preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
blanchet@54828
   194
     preplay_quietly = K (K (Played Time.zeroTime)),
blanchet@55213
   195
     overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
smolkas@52556
   196
  else
smolkas@52556
   197
    let
blanchet@54761
   198
      val ctxt = enrich_context_with_local_facts proof ctxt
smolkas@52556
   199
blanchet@55223
   200
      fun preplay quietly timeout meth step =
blanchet@55223
   201
        preplay_raw debug type_enc lam_trans ctxt timeout meth step
smolkas@52626
   202
        handle exn =>
blanchet@55212
   203
          if Exn.is_interrupt exn then
blanchet@55212
   204
            reraise exn
blanchet@55212
   205
          else
blanchet@55212
   206
            (if not quietly andalso debug then
blanchet@55212
   207
               warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn)
blanchet@55212
   208
             else
blanchet@55212
   209
               ();
blanchet@55212
   210
             Play_Failed)
smolkas@52556
   211
smolkas@52626
   212
      (* preplay steps treating exceptions like timeouts *)
blanchet@55223
   213
      fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, (meth :: _) :: _))) =
blanchet@55223
   214
          preplay true timeout meth step
blanchet@55223
   215
        | preplay_quietly _ _ = Played Time.zeroTime
blanchet@55223
   216
blanchet@55243
   217
      val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
smolkas@52556
   218
blanchet@55243
   219
      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, methss))) =
blanchet@55243
   220
          preplay_tab := Canonical_Label_Tab.update (l, maps (map (fn meth =>
blanchet@55243
   221
              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
blanchet@55243
   222
            (!preplay_tab)
blanchet@55243
   223
        | reset_preplay_outcomes _ = ()
blanchet@55243
   224
blanchet@55243
   225
      fun set_preplay_outcome l meth result =
blanchet@55243
   226
        preplay_tab := Canonical_Label_Tab.map_entry l
blanchet@55243
   227
          (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
smolkas@52556
   228
blanchet@55223
   229
      fun preplay_outcome l meth =
blanchet@55223
   230
        (case Canonical_Label_Tab.lookup (!preplay_tab) l of
blanchet@55223
   231
          SOME meths_outcomes =>
blanchet@55223
   232
          (case AList.lookup (op =) meths_outcomes meth of
blanchet@55223
   233
            SOME outcome => outcome
blanchet@55223
   234
          | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
blanchet@55223
   235
        | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
smolkas@52556
   236
blanchet@55243
   237
      val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
smolkas@52626
   238
blanchet@55223
   239
      fun result_of_step (Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
blanchet@55223
   240
          Lazy.force (preplay_outcome l meth)
blanchet@55223
   241
        | result_of_step _ = Played Time.zeroTime
blanchet@54763
   242
blanchet@54831
   243
      fun overall_preplay_outcome (Proof (_, _, steps)) =
blanchet@54828
   244
        fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
smolkas@52556
   245
    in
blanchet@55243
   246
      {reset_preplay_outcomes = reset_preplay_outcomes,
blanchet@54828
   247
       set_preplay_outcome = set_preplay_outcome,
blanchet@55243
   248
       preplay_outcome = preplay_outcome,
blanchet@54712
   249
       preplay_quietly = preplay_quietly,
blanchet@54831
   250
       overall_preplay_outcome = overall_preplay_outcome}
smolkas@52556
   251
    end
smolkas@50923
   252
blanchet@54504
   253
end;