src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
author blanchet
Fri Mar 14 11:15:46 2014 +0100 (2014-03-14 ago)
changeset 56128 c106ac2ff76d
parent 56093 4eeb73a1feec
child 57054 fed0329ea8e2
permissions -rw-r--r--
undo rewrite rules (e.g. for 'fun_app') in Isar
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@55287
    10
  type play_outcome = Sledgehammer_Proof_Methods.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@55260
    18
  type isar_preplay_data
smolkas@52556
    19
blanchet@55256
    20
  val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
blanchet@55452
    21
  val preplay_isar_step_for_method : Proof.context -> bool -> Time.time -> proof_method ->
blanchet@55452
    22
    isar_step -> play_outcome
blanchet@55452
    23
  val preplay_isar_step : Proof.context -> bool -> Time.time -> proof_method list -> isar_step ->
blanchet@55278
    24
    (proof_method * play_outcome) list
blanchet@55452
    25
  val set_preplay_outcomes_of_isar_step : Proof.context -> bool -> Time.time ->
blanchet@55278
    26
    isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit
blanchet@55272
    27
  val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome
blanchet@55266
    28
  val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method ->
blanchet@55260
    29
    play_outcome Lazy.lazy
blanchet@55266
    30
  val fastest_method_of_isar_step : isar_preplay_data -> label -> proof_method
blanchet@55260
    31
  val preplay_outcome_of_isar_proof : isar_preplay_data -> isar_proof -> play_outcome
blanchet@54504
    32
end;
smolkas@50923
    33
blanchet@55202
    34
structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
smolkas@50923
    35
struct
smolkas@50923
    36
blanchet@55257
    37
open ATP_Proof_Reconstruct
smolkas@50923
    38
open Sledgehammer_Util
blanchet@55287
    39
open Sledgehammer_Proof_Methods
blanchet@55202
    40
open Sledgehammer_Isar_Proof
smolkas@50923
    41
blanchet@54763
    42
val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
smolkas@50924
    43
blanchet@55256
    44
fun enrich_context_with_local_facts proof ctxt =
blanchet@55256
    45
  let
blanchet@55256
    46
    val thy = Proof_Context.theory_of ctxt
blanchet@55256
    47
blanchet@55256
    48
    fun enrich_with_fact l t =
blanchet@55256
    49
      Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t])
blanchet@55256
    50
blanchet@55256
    51
    val enrich_with_assms = fold (uncurry enrich_with_fact)
blanchet@55256
    52
blanchet@55256
    53
    fun enrich_with_proof (Proof (_, assms, isar_steps)) =
blanchet@55256
    54
      enrich_with_assms assms #> fold enrich_with_step isar_steps
blanchet@55299
    55
    and enrich_with_step (Prove (_, _, l, t, subproofs, _, _, _)) =
blanchet@55256
    56
        enrich_with_fact l t #> fold enrich_with_proof subproofs
blanchet@55299
    57
      | enrich_with_step _ = I
blanchet@55256
    58
  in
blanchet@55256
    59
    enrich_with_proof proof ctxt
blanchet@55256
    60
  end
blanchet@55256
    61
blanchet@55260
    62
fun preplay_trace ctxt assmsp concl outcome =
smolkas@51879
    63
  let
smolkas@51879
    64
    val ctxt = ctxt |> Config.put show_markup true
blanchet@55194
    65
    val assms = op @ assmsp
blanchet@55260
    66
    val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]")
blanchet@55251
    67
    val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms)
blanchet@55251
    68
    val concl = Syntax.pretty_term ctxt concl
blanchet@54761
    69
  in
blanchet@55251
    70
    tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl])))
blanchet@54761
    71
  end
smolkas@51879
    72
smolkas@50923
    73
fun take_time timeout tac arg =
blanchet@54761
    74
  let val timing = Timing.start () in
blanchet@54828
    75
    (TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing)))
blanchet@54828
    76
    handle TimeLimit.TimeOut => Play_Timed_Out timeout
smolkas@50923
    77
  end
smolkas@50923
    78
smolkas@50923
    79
fun resolve_fact_names ctxt names =
smolkas@51179
    80
  (names
blanchet@54761
    81
   |>> map string_of_label
blanchet@55194
    82
   |> pairself (maps (thms_of_name ctxt)))
smolkas@51179
    83
  handle ERROR msg => error ("preplay error: " ^ msg)
smolkas@50923
    84
blanchet@54700
    85
fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) =
smolkas@50923
    86
  let
blanchet@54761
    87
    val thy = Proof_Context.theory_of ctxt
blanchet@54761
    88
blanchet@54700
    89
    val concl = 
blanchet@54700
    90
      (case try List.last steps of
blanchet@55299
    91
        SOME (Prove (_, [], _, t, _, _, _, _)) => t
blanchet@54700
    92
      | _ => raise Fail "preplay error: malformed subproof")
blanchet@54761
    93
smolkas@51178
    94
    val var_idx = maxidx_of_term concl + 1
blanchet@54761
    95
    fun var_of_free (x, T) = Var ((x, var_idx), T)
blanchet@54761
    96
    val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees
smolkas@51178
    97
  in
smolkas@51179
    98
    Logic.list_implies (assms |> map snd, concl)
blanchet@54761
    99
    |> subst_free subst
blanchet@54761
   100
    |> Skip_Proof.make_thm thy
smolkas@51178
   101
  end
smolkas@51178
   102
blanchet@55299
   103
(* may throw exceptions *)
blanchet@55452
   104
fun raw_preplay_step_for_method ctxt debug timeout meth
blanchet@55452
   105
    (Prove (_, xs, _, t, subproofs, facts, _, _)) =
blanchet@55258
   106
  let
blanchet@55258
   107
    val goal =
blanchet@55258
   108
      (case xs of
blanchet@55258
   109
        [] => t
blanchet@55258
   110
      | _ =>
blanchet@55258
   111
        (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
blanchet@55258
   112
           (cf. "~~/src/Pure/Isar/obtain.ML") *)
blanchet@55258
   113
        let
blanchet@55294
   114
          val frees = map Free xs
blanchet@55294
   115
          val thesis =
blanchet@55294
   116
            Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT))
blanchet@55258
   117
          val thesis_prop = HOLogic.mk_Trueprop thesis
smolkas@50923
   118
blanchet@55258
   119
          (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
blanchet@55258
   120
          val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
blanchet@55258
   121
        in
blanchet@55258
   122
          (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
blanchet@55258
   123
          Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
blanchet@55258
   124
        end)
blanchet@54761
   125
blanchet@55299
   126
    val assmsp =
blanchet@55299
   127
      resolve_fact_names ctxt facts
blanchet@55258
   128
      |>> append (map (thm_of_proof ctxt) subproofs)
blanchet@55194
   129
blanchet@55258
   130
    fun prove () =
blanchet@55258
   131
      Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
blanchet@55452
   132
        HEADGOAL (tac_of_proof_method ctxt debug assmsp meth))
blanchet@55258
   133
      handle ERROR msg => error ("Preplay error: " ^ msg)
blanchet@54761
   134
blanchet@55258
   135
    val play_outcome = take_time timeout prove ()
blanchet@55258
   136
  in
blanchet@55329
   137
    if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
blanchet@55329
   138
    play_outcome
blanchet@55258
   139
  end
blanchet@55258
   140
blanchet@55452
   141
fun preplay_isar_step_for_method ctxt debug timeout meth =
blanchet@55452
   142
  try (raw_preplay_step_for_method ctxt debug timeout meth) #> the_default Play_Failed
blanchet@55278
   143
blanchet@55452
   144
fun preplay_isar_step ctxt debug timeout hopeless step =
blanchet@55278
   145
  let
blanchet@55278
   146
    fun try_method meth =
blanchet@55452
   147
      (case preplay_isar_step_for_method ctxt debug timeout meth step of
blanchet@55278
   148
        outcome as Played _ => SOME (meth, outcome)
blanchet@55278
   149
      | _ => NONE)
blanchet@55328
   150
blanchet@55328
   151
    val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless
blanchet@55278
   152
  in
blanchet@55328
   153
    the_list (Par_List.get_some try_method meths)
blanchet@55278
   154
  end
smolkas@52556
   155
blanchet@55260
   156
type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table
smolkas@52556
   157
blanchet@55256
   158
fun time_of_play (Played time) = time
blanchet@55256
   159
  | time_of_play (Play_Timed_Out time) = time
smolkas@50923
   160
blanchet@55260
   161
fun add_preplay_outcomes Play_Failed _ = Play_Failed
blanchet@55260
   162
  | add_preplay_outcomes _ Play_Failed = Play_Failed
blanchet@55260
   163
  | add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
blanchet@55260
   164
  | add_preplay_outcomes play1 play2 =
blanchet@55256
   165
    Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
blanchet@54827
   166
blanchet@55452
   167
fun set_preplay_outcomes_of_isar_step ctxt debug timeout preplay_data
blanchet@55299
   168
      (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
blanchet@55264
   169
    let
blanchet@55278
   170
      fun lazy_preplay meth =
blanchet@55452
   171
        Lazy.lazy (fn () => preplay_isar_step_for_method ctxt debug timeout meth step)
blanchet@55278
   172
      val meths_outcomes = meths_outcomes0
blanchet@55278
   173
        |> map (apsnd Lazy.value)
blanchet@55278
   174
        |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
blanchet@55264
   175
    in
blanchet@55308
   176
      preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes [])
blanchet@55308
   177
        (!preplay_data)
blanchet@55264
   178
    end
blanchet@55452
   179
  | set_preplay_outcomes_of_isar_step _ _ _ _ _ _ = ()
smolkas@52556
   180
blanchet@56093
   181
fun peek_at_outcome outcome =
blanchet@56093
   182
  if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime
blanchet@55269
   183
blanchet@55275
   184
fun get_best_method_outcome force =
blanchet@55275
   185
  tap (List.app (K () o Lazy.future Future.default_params o snd)) (* optional parallelism *)
blanchet@55275
   186
  #> map (apsnd force)
blanchet@55275
   187
  #> sort (play_outcome_ord o pairself snd)
blanchet@55275
   188
  #> hd
blanchet@55275
   189
blanchet@55272
   190
fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l =
blanchet@55269
   191
  let
blanchet@55309
   192
    val meths_outcomes as (_, outcome1) :: _ = the (Canonical_Label_Tab.lookup preplay_data l)
blanchet@55269
   193
  in
blanchet@55275
   194
    if forall (not o Lazy.is_finished o snd) meths_outcomes then
blanchet@55275
   195
      (case Lazy.force outcome1 of
blanchet@55275
   196
        outcome as Played _ => outcome
blanchet@55275
   197
      | _ => snd (get_best_method_outcome Lazy.force meths_outcomes))
blanchet@55275
   198
    else
blanchet@56093
   199
      let val outcome = snd (get_best_method_outcome peek_at_outcome meths_outcomes) in
blanchet@56093
   200
        if outcome = Play_Timed_Out Time.zeroTime then
blanchet@56093
   201
          snd (get_best_method_outcome Lazy.force meths_outcomes)
blanchet@56093
   202
        else
blanchet@56093
   203
          outcome
blanchet@56093
   204
      end
blanchet@55269
   205
  end
blanchet@55269
   206
blanchet@55268
   207
fun preplay_outcome_of_isar_step_for_method preplay_data l =
blanchet@55329
   208
  AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
blanchet@56093
   209
  #> the_default (Lazy.value (Play_Timed_Out Time.zeroTime))
blanchet@55252
   210
blanchet@55268
   211
fun fastest_method_of_isar_step preplay_data =
blanchet@55269
   212
  the o Canonical_Label_Tab.lookup preplay_data
blanchet@55275
   213
  #> get_best_method_outcome Lazy.force
blanchet@55275
   214
  #> fst
blanchet@55266
   215
blanchet@55299
   216
fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths, _)) =
blanchet@55295
   217
    Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths))
blanchet@55260
   218
  | forced_outcome_of_step _ _ = Played Time.zeroTime
blanchet@55252
   219
blanchet@55260
   220
fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) =
blanchet@55260
   221
  fold_isar_steps (add_preplay_outcomes o forced_outcome_of_step preplay_data) steps
blanchet@55260
   222
    (Played Time.zeroTime)
smolkas@50923
   223
blanchet@54504
   224
end;