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