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