src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
author blanchet
Thu Nov 21 12:29:29 2013 +0100 (2013-11-21 ago)
changeset 54546 8b403a7a8c44
parent 54504 096f7d452164
child 54700 64177ce0a7bd
permissions -rw-r--r--
fixed spying so that the envirnoment variables are queried at run-time not at build-time
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Steffen Juilf Smolka, TU Muenchen
     4 
     5 Preplaying of isar proofs.
     6 *)
     7 
     8 signature SLEDGEHAMMER_PREPLAY =
     9 sig
    10   type isar_proof = Sledgehammer_Proof.isar_proof
    11   type isar_step = Sledgehammer_Proof.isar_step
    12   type label = Sledgehammer_Proof.label
    13 
    14   eqtype preplay_time
    15 
    16   datatype preplay_result =
    17     PplFail of exn |
    18     PplSucc of preplay_time
    19 
    20   val trace : bool Config.T
    21   val zero_preplay_time : preplay_time
    22   val some_preplay_time : preplay_time
    23   val add_preplay_time : preplay_time -> preplay_time -> preplay_time
    24   val string_of_preplay_time : preplay_time -> string
    25 
    26   type preplay_interface =
    27   { get_preplay_result : label -> preplay_result,
    28     set_preplay_result : label -> preplay_result -> unit,
    29     get_preplay_time : label -> preplay_time,
    30     set_preplay_time : label -> preplay_time -> unit,
    31     preplay_quietly : Time.time -> isar_step -> preplay_time,
    32     (* the returned flag signals a preplay failure *)
    33     overall_preplay_stats : isar_proof -> preplay_time * bool }
    34 
    35   val proof_preplay_interface :
    36     bool -> Proof.context -> string -> string -> bool -> Time.time
    37     -> isar_proof -> preplay_interface
    38 end;
    39 
    40 structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
    41 struct
    42 
    43 open Sledgehammer_Util
    44 open Sledgehammer_Proof
    45 
    46 val trace =
    47   Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
    48 
    49 (* The boolean flag encodes whether the time is exact (false) or an lower bound
    50    (true):
    51       (t, false) = "t ms"
    52       (t, true)  = "> t ms" *)
    53 type preplay_time = bool * Time.time
    54 
    55 datatype preplay_result =
    56   PplFail of exn |
    57   PplSucc of preplay_time
    58 
    59 val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
    60 val some_preplay_time = (true, Time.zeroTime)  (* > 0 ms *)
    61 
    62 fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
    63 
    64 val string_of_preplay_time = ATP_Util.string_of_ext_time
    65 
    66 (* preplay tracing *)
    67 fun preplay_trace ctxt assms concl time =
    68   let
    69     val ctxt = ctxt |> Config.put show_markup true
    70     val time = "[" ^ (string_of_preplay_time time) ^ "]" |> Pretty.str
    71     val nr_of_assms = length assms
    72     val assms = assms |> map (Display.pretty_thm ctxt)
    73                       |> (fn [] => Pretty.str ""
    74                            | [a] => a
    75                            | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms)  (* Syntax.pretty_term!? *)
    76     val concl = concl |> Syntax.pretty_term ctxt
    77     val trace_list = [] |> cons concl
    78                         |> nr_of_assms>0 ? cons (Pretty.str "\<Longrightarrow>")
    79                         |> cons assms
    80                         |> cons time
    81     val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list)
    82   in tracing (Pretty.string_of pretty_trace) end
    83 
    84 (* timing *)
    85 fun take_time timeout tac arg =
    86   let
    87     val timing = Timing.start ()
    88   in
    89     (TimeLimit.timeLimit timeout tac arg;
    90       Timing.result timing |> #cpu |> pair false)
    91     handle TimeLimit.TimeOut => (true, timeout)
    92   end
    93 
    94 (* lookup facts in context *)
    95 fun resolve_fact_names ctxt names =
    96   (names
    97     |>> map string_of_label
    98     |> op @
    99     |> maps (thms_of_name ctxt))
   100   handle ERROR msg => error ("preplay error: " ^ msg)
   101 
   102 (* turn terms/proofs into theorems *)
   103 fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
   104 fun thm_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) =
   105   let
   106     val concl = (case try List.last steps of
   107                   SOME (Prove (_, Fix [], _, t, _, _)) => t
   108                 | _ => raise Fail "preplay error: malformed subproof")
   109     val var_idx = maxidx_of_term concl + 1
   110     fun var_of_free (x, T) = Var((x, var_idx), T)
   111     val substitutions =
   112       map (`var_of_free #> swap #> apfst Free) fixed_frees
   113   in
   114     Logic.list_implies (assms |> map snd, concl)
   115       |> subst_free substitutions
   116       |> thm_of_term ctxt
   117   end
   118 
   119 (* mapping from proof methods to tactics *)
   120 fun tac_of_method method type_enc lam_trans ctxt facts =
   121   case method of
   122     MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
   123   | _ =>
   124       Method.insert_tac facts
   125       THEN' (case method of
   126               SimpM => Simplifier.asm_full_simp_tac
   127             | AutoM => Clasimp.auto_tac #> K
   128             | FastforceM => Clasimp.fast_force_tac
   129             | ForceM => Clasimp.force_tac
   130             | ArithM => Arith_Data.arith_tac
   131             | BlastM => blast_tac
   132             | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt
   133 
   134 
   135 (* main function for preplaying isar_steps; may throw exceptions *)
   136 fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time
   137   | preplay_raw debug type_enc lam_trans ctxt timeout
   138       (Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) =
   139   let
   140     val (prop, obtain) =
   141       (case xs of
   142         [] => (t, false)
   143       | _ =>
   144       (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
   145            (see ~~/src/Pure/Isar/obtain.ML) *)
   146         let
   147           val thesis = Term.Free ("thesis", HOLogic.boolT)
   148           val thesis_prop = thesis |> HOLogic.mk_Trueprop
   149           val frees = map Term.Free xs
   150 
   151           (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
   152           val inner_prop =
   153             fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
   154 
   155           (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
   156           val prop =
   157             Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
   158         in
   159           (prop, true)
   160         end)
   161     val facts =
   162       map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
   163     val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
   164                     |> Config.put Lin_Arith.verbose debug
   165                     |> obtain ? Config.put Metis_Tactic.new_skolem true
   166     val goal =
   167       Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop
   168     fun tac {context = ctxt, prems = _} =
   169       HEADGOAL (tac_of_method proof_method type_enc lam_trans ctxt facts)
   170     fun run_tac () = goal tac
   171       handle ERROR msg => error ("Preplay error: " ^ msg)
   172     val preplay_time = take_time timeout run_tac ()
   173   in
   174     (* tracing *)
   175     (if Config.get ctxt trace then preplay_trace ctxt facts prop preplay_time
   176      else ();
   177      preplay_time)
   178   end
   179 
   180 
   181 (*** proof preplay interface ***)
   182 
   183 type preplay_interface =
   184 { get_preplay_result : label -> preplay_result,
   185   set_preplay_result : label -> preplay_result -> unit,
   186   get_preplay_time : label -> preplay_time,
   187   set_preplay_time : label -> preplay_time -> unit,
   188   preplay_quietly : Time.time -> isar_step -> preplay_time,
   189   (* the returned flag signals a preplay failure *)
   190   overall_preplay_stats : isar_proof -> preplay_time * bool }
   191 
   192 
   193 (* enriches context with local proof facts *)
   194 fun enrich_context proof ctxt =
   195   let
   196     val thy = Proof_Context.theory_of ctxt
   197 
   198     fun enrich_with_fact l t =
   199       Proof_Context.put_thms false
   200         (string_of_label l, SOME [Skip_Proof.make_thm thy t])
   201 
   202     val enrich_with_assms = fold (uncurry enrich_with_fact)
   203 
   204     fun enrich_with_proof (Proof (_, Assume assms, isar_steps)) =
   205       enrich_with_assms assms #> fold enrich_with_step isar_steps
   206 
   207     and enrich_with_step (Let _) = I
   208       | enrich_with_step (Prove (_, _, l, t, subproofs, _)) =
   209           enrich_with_fact l t #> fold enrich_with_proof subproofs
   210   in
   211     enrich_with_proof proof ctxt
   212   end
   213 
   214 
   215 (* Given a proof, produces an imperative preplay interface with a shared table
   216    mapping from labels to preplay results.
   217    The preplay results are caluclated lazyly and cached to avoid repeated
   218    calculation.
   219 
   220    PRECONDITION: the proof must be labeled canocially, see
   221    Slegehammer_Proof.relabel_proof_canonically
   222 *)
   223 
   224 fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
   225       preplay_timeout proof : preplay_interface =
   226   if not do_preplay then
   227     (* the dont_preplay option pretends that everything works just fine *)
   228     { get_preplay_result = K (PplSucc zero_preplay_time),
   229       set_preplay_result = K (K ()),
   230       get_preplay_time = K zero_preplay_time,
   231       set_preplay_time = K (K ()),
   232       preplay_quietly = K (K zero_preplay_time),
   233       overall_preplay_stats = K (zero_preplay_time, false)}
   234   else
   235     let
   236 
   237       (* add local proof facts to context *)
   238       val ctxt = enrich_context proof ctxt
   239 
   240       fun preplay quietly timeout step =
   241         preplay_raw debug type_enc lam_trans ctxt timeout step
   242         |> PplSucc
   243         handle exn =>
   244           if Exn.is_interrupt exn then
   245             reraise exn
   246           else if not quietly andalso debug then
   247             (warning ("Preplay failure:\n  " ^ @{make_string} step ^ "\n  "
   248                       ^ @{make_string} exn);
   249              PplFail exn)
   250           else
   251             PplFail exn
   252 
   253       (* preplay steps treating exceptions like timeouts *)
   254       fun preplay_quietly timeout step =
   255         case preplay true timeout step of
   256           PplSucc preplay_time => preplay_time
   257         | PplFail _ => (true, timeout)
   258 
   259       val preplay_tab =
   260         let
   261           fun add_step_to_tab step tab =
   262             case label_of_step step of
   263               NONE => tab
   264             | SOME l =>
   265                 Canonical_Lbl_Tab.update_new
   266                   (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy)
   267                   tab
   268             handle Canonical_Lbl_Tab.DUP _ =>
   269               raise Fail "Sledgehammer_Preplay: preplay time table"
   270         in
   271           Canonical_Lbl_Tab.empty
   272           |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
   273           |> Unsynchronized.ref
   274         end
   275 
   276       fun get_preplay_result lbl =
   277         Canonical_Lbl_Tab.lookup (!preplay_tab) lbl |> the |> Lazy.force
   278         handle
   279           Option.Option =>
   280             raise Fail "Sledgehammer_Preplay: preplay time table"
   281 
   282       fun set_preplay_result lbl result =
   283         preplay_tab :=
   284           Canonical_Lbl_Tab.update (lbl, Lazy.value result) (!preplay_tab)
   285 
   286       fun get_preplay_time lbl =
   287         case get_preplay_result lbl of
   288           PplSucc preplay_time => preplay_time
   289         | PplFail _ => some_preplay_time (* best approximation possible *)
   290 
   291       fun set_preplay_time lbl time = set_preplay_result lbl (PplSucc time)
   292 
   293       fun overall_preplay_stats (Proof(_, _, steps)) =
   294         let
   295           fun result_of_step step =
   296             try (label_of_step #> the #> get_preplay_result) step
   297             |> the_default (PplSucc zero_preplay_time)
   298           fun do_step step =
   299             case result_of_step step of
   300               PplSucc preplay_time => apfst (add_preplay_time preplay_time)
   301             | PplFail _ => apsnd (K true)
   302         in
   303           fold_isar_steps do_step steps (zero_preplay_time, false)
   304         end
   305 
   306     in
   307       { get_preplay_result = get_preplay_result,
   308         set_preplay_result = set_preplay_result,
   309         get_preplay_time = get_preplay_time,
   310         set_preplay_time = set_preplay_time,
   311         preplay_quietly = preplay_quietly,
   312         overall_preplay_stats = overall_preplay_stats}
   313     end
   314 
   315 end;