src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
author blanchet
Thu Nov 21 12:29:29 2013 +0100 (2013-11-21 ago)
changeset 54546 8b403a7a8c44
parent 54504 096f7d452164
child 54700 64177ce0a7bd
permissions -rw-r--r--
fixed spying so that the envirnoment variables are queried at run-time not at build-time
smolkas@51130
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
smolkas@50923
     2
    Author:     Jasmin Blanchette, TU Muenchen
smolkas@50923
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@50923
     4
smolkas@50924
     5
Preplaying of isar proofs.
smolkas@50923
     6
*)
smolkas@50923
     7
smolkas@50923
     8
signature SLEDGEHAMMER_PREPLAY =
smolkas@50923
     9
sig
smolkas@52556
    10
  type isar_proof = Sledgehammer_Proof.isar_proof
smolkas@50923
    11
  type isar_step = Sledgehammer_Proof.isar_step
smolkas@52556
    12
  type label = Sledgehammer_Proof.label
smolkas@52556
    13
smolkas@50924
    14
  eqtype preplay_time
smolkas@52626
    15
smolkas@52626
    16
  datatype preplay_result =
smolkas@52626
    17
    PplFail of exn |
smolkas@52626
    18
    PplSucc of preplay_time
smolkas@52626
    19
blanchet@53761
    20
  val trace : bool Config.T
smolkas@50924
    21
  val zero_preplay_time : preplay_time
smolkas@50924
    22
  val some_preplay_time : preplay_time
smolkas@50924
    23
  val add_preplay_time : preplay_time -> preplay_time -> preplay_time
smolkas@50924
    24
  val string_of_preplay_time : preplay_time -> string
smolkas@52556
    25
smolkas@52556
    26
  type preplay_interface =
smolkas@52626
    27
  { get_preplay_result : label -> preplay_result,
smolkas@52626
    28
    set_preplay_result : label -> preplay_result -> unit,
smolkas@52626
    29
    get_preplay_time : label -> preplay_time,
smolkas@52626
    30
    set_preplay_time : label -> preplay_time -> unit,
smolkas@52556
    31
    preplay_quietly : Time.time -> isar_step -> preplay_time,
smolkas@52626
    32
    (* the returned flag signals a preplay failure *)
smolkas@52626
    33
    overall_preplay_stats : isar_proof -> preplay_time * bool }
smolkas@52556
    34
smolkas@52556
    35
  val proof_preplay_interface :
blanchet@53761
    36
    bool -> Proof.context -> string -> string -> bool -> Time.time
smolkas@52592
    37
    -> isar_proof -> preplay_interface
blanchet@54504
    38
end;
smolkas@50923
    39
smolkas@50923
    40
structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
smolkas@50923
    41
struct
smolkas@50923
    42
smolkas@50923
    43
open Sledgehammer_Util
smolkas@50923
    44
open Sledgehammer_Proof
smolkas@50923
    45
blanchet@53761
    46
val trace =
blanchet@53761
    47
  Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
blanchet@53761
    48
smolkas@50924
    49
(* The boolean flag encodes whether the time is exact (false) or an lower bound
smolkas@51131
    50
   (true):
smolkas@51131
    51
      (t, false) = "t ms"
smolkas@51131
    52
      (t, true)  = "> t ms" *)
smolkas@50924
    53
type preplay_time = bool * Time.time
smolkas@50924
    54
smolkas@52626
    55
datatype preplay_result =
smolkas@52626
    56
  PplFail of exn |
smolkas@52626
    57
  PplSucc of preplay_time
smolkas@52626
    58
smolkas@51131
    59
val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
smolkas@51131
    60
val some_preplay_time = (true, Time.zeroTime)  (* > 0 ms *)
smolkas@50924
    61
smolkas@50924
    62
fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
smolkas@50924
    63
blanchet@52031
    64
val string_of_preplay_time = ATP_Util.string_of_ext_time
smolkas@50924
    65
smolkas@51879
    66
(* preplay tracing *)
smolkas@51879
    67
fun preplay_trace ctxt assms concl time =
smolkas@51879
    68
  let
smolkas@51879
    69
    val ctxt = ctxt |> Config.put show_markup true
smolkas@51879
    70
    val time = "[" ^ (string_of_preplay_time time) ^ "]" |> Pretty.str
smolkas@51879
    71
    val nr_of_assms = length assms
smolkas@51879
    72
    val assms = assms |> map (Display.pretty_thm ctxt)
smolkas@51879
    73
                      |> (fn [] => Pretty.str ""
smolkas@51879
    74
                           | [a] => a
wenzelm@53664
    75
                           | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms)  (* Syntax.pretty_term!? *)
smolkas@51879
    76
    val concl = concl |> Syntax.pretty_term ctxt
smolkas@51879
    77
    val trace_list = [] |> cons concl
wenzelm@53664
    78
                        |> nr_of_assms>0 ? cons (Pretty.str "\<Longrightarrow>")
smolkas@51879
    79
                        |> cons assms
smolkas@51879
    80
                        |> cons time
blanchet@53761
    81
    val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list)
smolkas@51879
    82
  in tracing (Pretty.string_of pretty_trace) end
smolkas@51879
    83
smolkas@50923
    84
(* timing *)
smolkas@50923
    85
fun take_time timeout tac arg =
smolkas@50923
    86
  let
smolkas@50923
    87
    val timing = Timing.start ()
smolkas@50923
    88
  in
smolkas@50924
    89
    (TimeLimit.timeLimit timeout tac arg;
smolkas@50924
    90
      Timing.result timing |> #cpu |> pair false)
smolkas@50924
    91
    handle TimeLimit.TimeOut => (true, timeout)
smolkas@50923
    92
  end
smolkas@50923
    93
smolkas@50923
    94
(* lookup facts in context *)
smolkas@50923
    95
fun resolve_fact_names ctxt names =
smolkas@51179
    96
  (names
blanchet@51998
    97
    |>> map string_of_label
smolkas@50923
    98
    |> op @
smolkas@51179
    99
    |> maps (thms_of_name ctxt))
smolkas@51179
   100
  handle ERROR msg => error ("preplay error: " ^ msg)
smolkas@50923
   101
smolkas@51879
   102
(* turn terms/proofs into theorems *)
smolkas@51178
   103
fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
smolkas@51879
   104
fun thm_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) =
smolkas@50923
   105
  let
smolkas@51179
   106
    val concl = (case try List.last steps of
smolkas@52454
   107
                  SOME (Prove (_, Fix [], _, t, _, _)) => t
smolkas@51876
   108
                | _ => raise Fail "preplay error: malformed subproof")
smolkas@51178
   109
    val var_idx = maxidx_of_term concl + 1
smolkas@51178
   110
    fun var_of_free (x, T) = Var((x, var_idx), T)
smolkas@51178
   111
    val substitutions =
smolkas@51178
   112
      map (`var_of_free #> swap #> apfst Free) fixed_frees
smolkas@51178
   113
  in
smolkas@51179
   114
    Logic.list_implies (assms |> map snd, concl)
smolkas@51178
   115
      |> subst_free substitutions
smolkas@51178
   116
      |> thm_of_term ctxt
smolkas@51178
   117
  end
smolkas@51178
   118
smolkas@52633
   119
(* mapping from proof methods to tactics *)
smolkas@52592
   120
fun tac_of_method method type_enc lam_trans ctxt facts =
smolkas@52592
   121
  case method of
smolkas@52592
   122
    MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
smolkas@52592
   123
  | _ =>
smolkas@52592
   124
      Method.insert_tac facts
smolkas@52592
   125
      THEN' (case method of
smolkas@52592
   126
              SimpM => Simplifier.asm_full_simp_tac
smolkas@52633
   127
            | AutoM => Clasimp.auto_tac #> K
smolkas@52592
   128
            | FastforceM => Clasimp.fast_force_tac
smolkas@52629
   129
            | ForceM => Clasimp.force_tac
smolkas@52592
   130
            | ArithM => Arith_Data.arith_tac
smolkas@52629
   131
            | BlastM => blast_tac
smolkas@52592
   132
            | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt
smolkas@52592
   133
smolkas@52556
   134
smolkas@52626
   135
(* main function for preplaying isar_steps; may throw exceptions *)
blanchet@53761
   136
fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time
blanchet@53761
   137
  | preplay_raw debug type_enc lam_trans ctxt timeout
smolkas@52592
   138
      (Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) =
smolkas@51178
   139
  let
smolkas@52453
   140
    val (prop, obtain) =
smolkas@52453
   141
      (case xs of
smolkas@52453
   142
        [] => (t, false)
smolkas@52453
   143
      | _ =>
smolkas@52453
   144
      (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
smolkas@50923
   145
           (see ~~/src/Pure/Isar/obtain.ML) *)
smolkas@50923
   146
        let
smolkas@50923
   147
          val thesis = Term.Free ("thesis", HOLogic.boolT)
smolkas@50923
   148
          val thesis_prop = thesis |> HOLogic.mk_Trueprop
smolkas@50923
   149
          val frees = map Term.Free xs
smolkas@50923
   150
smolkas@50923
   151
          (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
smolkas@50923
   152
          val inner_prop =
smolkas@50923
   153
            fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
smolkas@50923
   154
smolkas@50923
   155
          (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
smolkas@50923
   156
          val prop =
smolkas@50923
   157
            Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
smolkas@50923
   158
        in
smolkas@52453
   159
          (prop, true)
smolkas@52453
   160
        end)
smolkas@50923
   161
    val facts =
smolkas@51879
   162
      map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
smolkas@50923
   163
    val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
smolkas@52692
   164
                    |> Config.put Lin_Arith.verbose debug
smolkas@50923
   165
                    |> obtain ? Config.put Metis_Tactic.new_skolem true
smolkas@50923
   166
    val goal =
smolkas@51879
   167
      Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop
smolkas@50923
   168
    fun tac {context = ctxt, prems = _} =
smolkas@52592
   169
      HEADGOAL (tac_of_method proof_method type_enc lam_trans ctxt facts)
smolkas@51879
   170
    fun run_tac () = goal tac
smolkas@52627
   171
      handle ERROR msg => error ("Preplay error: " ^ msg)
smolkas@52556
   172
    val preplay_time = take_time timeout run_tac ()
smolkas@50923
   173
  in
smolkas@52556
   174
    (* tracing *)
blanchet@53761
   175
    (if Config.get ctxt trace then preplay_trace ctxt facts prop preplay_time
blanchet@53761
   176
     else ();
smolkas@52556
   177
     preplay_time)
smolkas@52556
   178
  end
smolkas@52556
   179
smolkas@52556
   180
smolkas@52556
   181
(*** proof preplay interface ***)
smolkas@52556
   182
smolkas@52556
   183
type preplay_interface =
smolkas@52626
   184
{ get_preplay_result : label -> preplay_result,
smolkas@52626
   185
  set_preplay_result : label -> preplay_result -> unit,
smolkas@52626
   186
  get_preplay_time : label -> preplay_time,
smolkas@52626
   187
  set_preplay_time : label -> preplay_time -> unit,
smolkas@52626
   188
  preplay_quietly : Time.time -> isar_step -> preplay_time,
smolkas@52626
   189
  (* the returned flag signals a preplay failure *)
smolkas@52626
   190
  overall_preplay_stats : isar_proof -> preplay_time * bool }
smolkas@52556
   191
smolkas@52556
   192
smolkas@52556
   193
(* enriches context with local proof facts *)
smolkas@52556
   194
fun enrich_context proof ctxt =
smolkas@52556
   195
  let
smolkas@52556
   196
    val thy = Proof_Context.theory_of ctxt
smolkas@52556
   197
smolkas@52556
   198
    fun enrich_with_fact l t =
smolkas@52556
   199
      Proof_Context.put_thms false
smolkas@52556
   200
        (string_of_label l, SOME [Skip_Proof.make_thm thy t])
smolkas@52556
   201
smolkas@52556
   202
    val enrich_with_assms = fold (uncurry enrich_with_fact)
smolkas@52556
   203
smolkas@52556
   204
    fun enrich_with_proof (Proof (_, Assume assms, isar_steps)) =
smolkas@52556
   205
      enrich_with_assms assms #> fold enrich_with_step isar_steps
smolkas@52556
   206
smolkas@52556
   207
    and enrich_with_step (Let _) = I
smolkas@52556
   208
      | enrich_with_step (Prove (_, _, l, t, subproofs, _)) =
smolkas@52556
   209
          enrich_with_fact l t #> fold enrich_with_proof subproofs
smolkas@52556
   210
  in
smolkas@52556
   211
    enrich_with_proof proof ctxt
smolkas@50923
   212
  end
smolkas@50923
   213
smolkas@52556
   214
smolkas@52626
   215
(* Given a proof, produces an imperative preplay interface with a shared table
smolkas@52626
   216
   mapping from labels to preplay results.
smolkas@52626
   217
   The preplay results are caluclated lazyly and cached to avoid repeated
smolkas@52556
   218
   calculation.
smolkas@52556
   219
blanchet@53761
   220
   PRECONDITION: the proof must be labeled canocially, see
smolkas@52556
   221
   Slegehammer_Proof.relabel_proof_canonically
smolkas@52556
   222
*)
smolkas@52626
   223
smolkas@52556
   224
fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
blanchet@53761
   225
      preplay_timeout proof : preplay_interface =
smolkas@52556
   226
  if not do_preplay then
smolkas@52556
   227
    (* the dont_preplay option pretends that everything works just fine *)
smolkas@52626
   228
    { get_preplay_result = K (PplSucc zero_preplay_time),
smolkas@52626
   229
      set_preplay_result = K (K ()),
smolkas@52626
   230
      get_preplay_time = K zero_preplay_time,
smolkas@52626
   231
      set_preplay_time = K (K ()),
smolkas@52556
   232
      preplay_quietly = K (K zero_preplay_time),
smolkas@52556
   233
      overall_preplay_stats = K (zero_preplay_time, false)}
smolkas@52556
   234
  else
smolkas@52556
   235
    let
smolkas@52556
   236
smolkas@52556
   237
      (* add local proof facts to context *)
smolkas@52556
   238
      val ctxt = enrich_context proof ctxt
smolkas@52556
   239
smolkas@52627
   240
      fun preplay quietly timeout step =
blanchet@53761
   241
        preplay_raw debug type_enc lam_trans ctxt timeout step
smolkas@52626
   242
        |> PplSucc
smolkas@52626
   243
        handle exn =>
smolkas@52627
   244
          if Exn.is_interrupt exn then
smolkas@52627
   245
            reraise exn
smolkas@52627
   246
          else if not quietly andalso debug then
smolkas@52627
   247
            (warning ("Preplay failure:\n  " ^ @{make_string} step ^ "\n  "
smolkas@52627
   248
                      ^ @{make_string} exn);
smolkas@52627
   249
             PplFail exn)
smolkas@52627
   250
          else
smolkas@52627
   251
            PplFail exn
smolkas@52556
   252
smolkas@52626
   253
      (* preplay steps treating exceptions like timeouts *)
smolkas@52556
   254
      fun preplay_quietly timeout step =
smolkas@52627
   255
        case preplay true timeout step of
smolkas@52626
   256
          PplSucc preplay_time => preplay_time
smolkas@52626
   257
        | PplFail _ => (true, timeout)
smolkas@52556
   258
smolkas@52626
   259
      val preplay_tab =
smolkas@52556
   260
        let
smolkas@52556
   261
          fun add_step_to_tab step tab =
smolkas@52556
   262
            case label_of_step step of
smolkas@52556
   263
              NONE => tab
smolkas@52556
   264
            | SOME l =>
smolkas@52556
   265
                Canonical_Lbl_Tab.update_new
smolkas@52627
   266
                  (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy)
smolkas@52556
   267
                  tab
smolkas@52592
   268
            handle Canonical_Lbl_Tab.DUP _ =>
smolkas@52575
   269
              raise Fail "Sledgehammer_Preplay: preplay time table"
smolkas@52556
   270
        in
smolkas@52556
   271
          Canonical_Lbl_Tab.empty
smolkas@52556
   272
          |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
smolkas@52556
   273
          |> Unsynchronized.ref
smolkas@52556
   274
        end
smolkas@52556
   275
smolkas@52626
   276
      fun get_preplay_result lbl =
smolkas@52626
   277
        Canonical_Lbl_Tab.lookup (!preplay_tab) lbl |> the |> Lazy.force
smolkas@52556
   278
        handle
smolkas@52556
   279
          Option.Option =>
smolkas@52556
   280
            raise Fail "Sledgehammer_Preplay: preplay time table"
smolkas@52556
   281
smolkas@52626
   282
      fun set_preplay_result lbl result =
smolkas@52626
   283
        preplay_tab :=
smolkas@52626
   284
          Canonical_Lbl_Tab.update (lbl, Lazy.value result) (!preplay_tab)
smolkas@52626
   285
smolkas@52626
   286
      fun get_preplay_time lbl =
smolkas@52626
   287
        case get_preplay_result lbl of
smolkas@52626
   288
          PplSucc preplay_time => preplay_time
smolkas@52626
   289
        | PplFail _ => some_preplay_time (* best approximation possible *)
smolkas@52626
   290
smolkas@52626
   291
      fun set_preplay_time lbl time = set_preplay_result lbl (PplSucc time)
smolkas@52556
   292
smolkas@52626
   293
      fun overall_preplay_stats (Proof(_, _, steps)) =
smolkas@52626
   294
        let
smolkas@52626
   295
          fun result_of_step step =
smolkas@52626
   296
            try (label_of_step #> the #> get_preplay_result) step
smolkas@52626
   297
            |> the_default (PplSucc zero_preplay_time)
smolkas@52626
   298
          fun do_step step =
smolkas@52626
   299
            case result_of_step step of
smolkas@52626
   300
              PplSucc preplay_time => apfst (add_preplay_time preplay_time)
smolkas@52626
   301
            | PplFail _ => apsnd (K true)
smolkas@52626
   302
        in
smolkas@52626
   303
          fold_isar_steps do_step steps (zero_preplay_time, false)
smolkas@52626
   304
        end
smolkas@52556
   305
smolkas@52556
   306
    in
smolkas@52626
   307
      { get_preplay_result = get_preplay_result,
smolkas@52626
   308
        set_preplay_result = set_preplay_result,
smolkas@52626
   309
        get_preplay_time = get_preplay_time,
smolkas@52626
   310
        set_preplay_time = set_preplay_time,
smolkas@52556
   311
        preplay_quietly = preplay_quietly,
smolkas@52556
   312
        overall_preplay_stats = overall_preplay_stats}
smolkas@52556
   313
    end
smolkas@50923
   314
blanchet@54504
   315
end;