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