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