src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
author blanchet
Mon Jun 02 17:34:26 2014 +0200 (2014-06-02 ago)
changeset 57158 f028d93798e6
parent 57054 fed0329ea8e2
child 57725 a297879fe5b8
permissions -rw-r--r--
simplified counterexample handling
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@57054
    21
  val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step ->
blanchet@57054
    22
    play_outcome
blanchet@57054
    23
  val preplay_isar_step : Proof.context -> Time.time -> proof_method list -> isar_step ->
blanchet@55278
    24
    (proof_method * play_outcome) list
blanchet@57054
    25
  val set_preplay_outcomes_of_isar_step : Proof.context -> 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@57054
   104
fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) =
blanchet@55258
   105
  let
blanchet@55258
   106
    val goal =
blanchet@55258
   107
      (case xs of
blanchet@55258
   108
        [] => t
blanchet@55258
   109
      | _ =>
blanchet@55258
   110
        (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
blanchet@55258
   111
           (cf. "~~/src/Pure/Isar/obtain.ML") *)
blanchet@55258
   112
        let
blanchet@55294
   113
          val frees = map Free xs
blanchet@55294
   114
          val thesis =
blanchet@55294
   115
            Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT))
blanchet@55258
   116
          val thesis_prop = HOLogic.mk_Trueprop thesis
smolkas@50923
   117
blanchet@55258
   118
          (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
blanchet@55258
   119
          val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
blanchet@55258
   120
        in
blanchet@55258
   121
          (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
blanchet@55258
   122
          Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
blanchet@55258
   123
        end)
blanchet@54761
   124
blanchet@55299
   125
    val assmsp =
blanchet@55299
   126
      resolve_fact_names ctxt facts
blanchet@55258
   127
      |>> append (map (thm_of_proof ctxt) subproofs)
blanchet@55194
   128
blanchet@55258
   129
    fun prove () =
blanchet@55258
   130
      Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
blanchet@57054
   131
        HEADGOAL (tac_of_proof_method ctxt assmsp meth))
blanchet@55258
   132
      handle ERROR msg => error ("Preplay error: " ^ msg)
blanchet@54761
   133
blanchet@55258
   134
    val play_outcome = take_time timeout prove ()
blanchet@55258
   135
  in
blanchet@55329
   136
    if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
blanchet@55329
   137
    play_outcome
blanchet@55258
   138
  end
blanchet@55258
   139
blanchet@57054
   140
fun preplay_isar_step_for_method ctxt timeout meth =
blanchet@57054
   141
  try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed
blanchet@55278
   142
blanchet@57054
   143
fun preplay_isar_step ctxt timeout hopeless step =
blanchet@55278
   144
  let
blanchet@55278
   145
    fun try_method meth =
blanchet@57054
   146
      (case preplay_isar_step_for_method ctxt timeout meth step of
blanchet@55278
   147
        outcome as Played _ => SOME (meth, outcome)
blanchet@55278
   148
      | _ => NONE)
blanchet@55328
   149
blanchet@55328
   150
    val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless
blanchet@55278
   151
  in
blanchet@55328
   152
    the_list (Par_List.get_some try_method meths)
blanchet@55278
   153
  end
smolkas@52556
   154
blanchet@55260
   155
type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table
smolkas@52556
   156
blanchet@55256
   157
fun time_of_play (Played time) = time
blanchet@55256
   158
  | time_of_play (Play_Timed_Out time) = time
smolkas@50923
   159
blanchet@55260
   160
fun add_preplay_outcomes Play_Failed _ = Play_Failed
blanchet@55260
   161
  | add_preplay_outcomes _ Play_Failed = Play_Failed
blanchet@55260
   162
  | add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
blanchet@55260
   163
  | add_preplay_outcomes play1 play2 =
blanchet@55256
   164
    Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
blanchet@54827
   165
blanchet@57054
   166
fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
blanchet@55299
   167
      (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
blanchet@55264
   168
    let
blanchet@55278
   169
      fun lazy_preplay meth =
blanchet@57054
   170
        Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
blanchet@55278
   171
      val meths_outcomes = meths_outcomes0
blanchet@55278
   172
        |> map (apsnd Lazy.value)
blanchet@55278
   173
        |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
blanchet@55264
   174
    in
blanchet@55308
   175
      preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes [])
blanchet@55308
   176
        (!preplay_data)
blanchet@55264
   177
    end
blanchet@57054
   178
  | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
smolkas@52556
   179
blanchet@56093
   180
fun peek_at_outcome outcome =
blanchet@56093
   181
  if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime
blanchet@55269
   182
blanchet@55275
   183
fun get_best_method_outcome force =
blanchet@55275
   184
  tap (List.app (K () o Lazy.future Future.default_params o snd)) (* optional parallelism *)
blanchet@55275
   185
  #> map (apsnd force)
blanchet@55275
   186
  #> sort (play_outcome_ord o pairself snd)
blanchet@55275
   187
  #> hd
blanchet@55275
   188
blanchet@55272
   189
fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l =
blanchet@55269
   190
  let
blanchet@55309
   191
    val meths_outcomes as (_, outcome1) :: _ = the (Canonical_Label_Tab.lookup preplay_data l)
blanchet@55269
   192
  in
blanchet@55275
   193
    if forall (not o Lazy.is_finished o snd) meths_outcomes then
blanchet@55275
   194
      (case Lazy.force outcome1 of
blanchet@55275
   195
        outcome as Played _ => outcome
blanchet@55275
   196
      | _ => snd (get_best_method_outcome Lazy.force meths_outcomes))
blanchet@55275
   197
    else
blanchet@56093
   198
      let val outcome = snd (get_best_method_outcome peek_at_outcome meths_outcomes) in
blanchet@56093
   199
        if outcome = Play_Timed_Out Time.zeroTime then
blanchet@56093
   200
          snd (get_best_method_outcome Lazy.force meths_outcomes)
blanchet@56093
   201
        else
blanchet@56093
   202
          outcome
blanchet@56093
   203
      end
blanchet@55269
   204
  end
blanchet@55269
   205
blanchet@55268
   206
fun preplay_outcome_of_isar_step_for_method preplay_data l =
blanchet@55329
   207
  AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
blanchet@56093
   208
  #> the_default (Lazy.value (Play_Timed_Out Time.zeroTime))
blanchet@55252
   209
blanchet@55268
   210
fun fastest_method_of_isar_step preplay_data =
blanchet@55269
   211
  the o Canonical_Label_Tab.lookup preplay_data
blanchet@55275
   212
  #> get_best_method_outcome Lazy.force
blanchet@55275
   213
  #> fst
blanchet@55266
   214
blanchet@55299
   215
fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths, _)) =
blanchet@55295
   216
    Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths))
blanchet@55260
   217
  | forced_outcome_of_step _ _ = Played Time.zeroTime
blanchet@55252
   218
blanchet@55260
   219
fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) =
blanchet@55260
   220
  fold_isar_steps (add_preplay_outcomes o forced_outcome_of_step preplay_data) steps
blanchet@55260
   221
    (Played Time.zeroTime)
smolkas@50923
   222
blanchet@54504
   223
end;