move preplaying to own structure
authorsmolkas
Thu Jan 17 11:55:40 2013 +0100 (2013-01-17)
changeset 50923141d8f575f6f
parent 50922 b1939139f8f3
child 50924 beb95bf66b21
move preplaying to own structure
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Thu Jan 17 10:44:51 2013 +0100
     1.2 +++ b/src/HOL/Sledgehammer.thy	Thu Jan 17 11:55:40 2013 +0100
     1.3 @@ -16,6 +16,7 @@
     1.4  ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
     1.5  ML_file "Tools/Sledgehammer/sledgehammer_proof.ML"
     1.6  ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
     1.7 +ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
     1.8  ML_file "Tools/Sledgehammer/sledgehammer_shrink.ML"
     1.9  ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" 
    1.10  ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Jan 17 11:55:40 2013 +0100
     2.3 @@ -0,0 +1,94 @@
     2.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
     2.5 +    Author:     Jasmin Blanchette, TU Muenchen
     2.6 +    Author:     Steffen Juilf Smolka, TU Muenchen
     2.7 +
     2.8 +Preplaying of reconstructed isar proofs.
     2.9 +*)
    2.10 +
    2.11 +signature SLEDGEHAMMER_PREPLAY =
    2.12 +sig
    2.13 +  type isar_step = Sledgehammer_Proof.isar_step
    2.14 +  val try_metis : bool -> string -> string -> Proof.context ->
    2.15 +    Time.time -> (isar_step option * isar_step) -> unit -> Time.time option
    2.16 +  val try_metis_quietly : bool -> string -> string -> Proof.context ->
    2.17 +    Time.time -> (isar_step option * isar_step) -> unit -> Time.time option
    2.18 +end
    2.19 +
    2.20 +structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
    2.21 +struct
    2.22 +
    2.23 +open Sledgehammer_Util
    2.24 +open Sledgehammer_Proof
    2.25 +
    2.26 +(* timing *)
    2.27 +fun take_time timeout tac arg =
    2.28 +  let
    2.29 +    val timing = Timing.start ()
    2.30 +  in
    2.31 +    (TimeLimit.timeLimit timeout tac arg; Timing.result timing |> #cpu |> SOME)
    2.32 +    handle TimeLimit.TimeOut => NONE
    2.33 +  end
    2.34 +
    2.35 +(* lookup facts in context *)
    2.36 +fun resolve_fact_names ctxt names =
    2.37 +  names
    2.38 +    |>> map string_for_label
    2.39 +    |> op @
    2.40 +    |> maps (thms_of_name ctxt)
    2.41 +
    2.42 +exception ZEROTIME
    2.43 +fun try_metis debug type_enc lam_trans ctxt timeout (succedent, step) =
    2.44 +  let
    2.45 +    val (t, byline, obtain) =
    2.46 +      (case step of
    2.47 +        Prove (_, _, t, byline) => (t, byline, false)
    2.48 +      | Obtain (_, xs, _, t, byline) =>
    2.49 +        (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
    2.50 +           (see ~~/src/Pure/Isar/obtain.ML) *)
    2.51 +        let
    2.52 +          val thesis = Term.Free ("thesis", HOLogic.boolT)
    2.53 +          val thesis_prop = thesis |> HOLogic.mk_Trueprop
    2.54 +          val frees = map Term.Free xs
    2.55 +
    2.56 +          (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
    2.57 +          val inner_prop =
    2.58 +            fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
    2.59 +
    2.60 +          (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
    2.61 +          val prop =
    2.62 +            Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
    2.63 +        in
    2.64 +          (prop, byline, true)
    2.65 +        end
    2.66 +      | _ => raise ZEROTIME)
    2.67 +    val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
    2.68 +    val facts =
    2.69 +      (case byline of
    2.70 +        By_Metis fact_names => resolve_fact_names ctxt fact_names
    2.71 +      | Case_Split (cases, fact_names) =>
    2.72 +        resolve_fact_names ctxt fact_names
    2.73 +          @ (case the succedent of
    2.74 +              Assume (_, t) => make_thm t
    2.75 +            | Obtain (_, _, _, t, _) => make_thm t
    2.76 +            | Prove (_, _, t, _) => make_thm t
    2.77 +            | _ => error "Preplay error: unexpected succedent of case split")
    2.78 +          :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
    2.79 +                          | _ => error "Preplay error: malformed case split")
    2.80 +                     #> make_thm)
    2.81 +               cases)
    2.82 +    val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
    2.83 +                    |> obtain ? Config.put Metis_Tactic.new_skolem true
    2.84 +    val goal =
    2.85 +      Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
    2.86 +    fun tac {context = ctxt, prems = _} =
    2.87 +      Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
    2.88 +  in
    2.89 +    take_time timeout (fn () => goal tac)
    2.90 +  end
    2.91 +  handle ZEROTIME => K (SOME Time.zeroTime)
    2.92 +
    2.93 +(* this version does not throw exceptions but returns NONE instead *)
    2.94 +fun try_metis_quietly debug type_enc lam_trans ctxt =
    2.95 +   the_default NONE oo try oo try_metis debug type_enc lam_trans ctxt
    2.96 +
    2.97 +end
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Jan 17 10:44:51 2013 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Jan 17 11:55:40 2013 +0100
     3.3 @@ -2,7 +2,7 @@
     3.4      Author:     Jasmin Blanchette, TU Muenchen
     3.5      Author:     Steffen Juilf Smolka, TU Muenchen
     3.6  
     3.7 -Shrinking and preplaying of reconstructed isar proofs.
     3.8 +Shrinking of reconstructed isar proofs.
     3.9  *)
    3.10  
    3.11  signature SLEDGEHAMMER_SHRINK =
    3.12 @@ -18,6 +18,7 @@
    3.13  
    3.14  open Sledgehammer_Util
    3.15  open Sledgehammer_Proof
    3.16 +open Sledgehammer_Preplay
    3.17  
    3.18  (* Parameters *)
    3.19  val merge_timeout_slack = 1.2
    3.20 @@ -47,13 +48,6 @@
    3.21  (* Timing *)
    3.22  fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
    3.23  val no_time = (false, Time.zeroTime)
    3.24 -fun take_time timeout tac arg =
    3.25 -  let val timing = Timing.start () in
    3.26 -    (TimeLimit.timeLimit timeout tac arg;
    3.27 -     Timing.result timing |> #cpu |> SOME)
    3.28 -    handle TimeLimit.TimeOut => NONE
    3.29 -  end
    3.30 -
    3.31  
    3.32  (* Main function for shrinking proofs *)
    3.33  fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
    3.34 @@ -118,74 +112,18 @@
    3.35          v_fold_index (add_if_cand proof_vect) refed_by_vect []
    3.36          |> Inttab.make_list
    3.37  
    3.38 -      (* Metis Preplaying *)
    3.39 -      fun resolve_fact_names names =
    3.40 -        names
    3.41 -          |>> map string_for_label
    3.42 -          |> op @
    3.43 -          |> maps (thms_of_name ctxt)
    3.44 -
    3.45 -      (* TODO: add "Obtain" case *)
    3.46 -      exception ZEROTIME
    3.47 -      fun try_metis timeout (succedent, step) =
    3.48 -        (if not preplay then K (SOME Time.zeroTime) else
    3.49 -          let
    3.50 -            val (t, byline, obtain) =
    3.51 -              (case step of
    3.52 -                Prove (_, _, t, byline) => (t, byline, false)
    3.53 -              | Obtain (_, xs, _, t, byline) =>
    3.54 -                (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
    3.55 -                   (see ~~/src/Pure/Isar/obtain.ML) *)
    3.56 -                let
    3.57 -                  val thesis = Term.Free ("thesis", HOLogic.boolT)
    3.58 -                  val thesis_prop = thesis |> HOLogic.mk_Trueprop
    3.59 -                  val frees = map Term.Free xs
    3.60 -
    3.61 -                  (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
    3.62 -                  val inner_prop =
    3.63 -                    fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
    3.64 -
    3.65 -                  (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
    3.66 -                  val prop =
    3.67 -                    Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
    3.68 -                in
    3.69 -                  (prop, byline, true)
    3.70 -                end
    3.71 -              | _ => raise ZEROTIME)
    3.72 -            val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
    3.73 -            val facts =
    3.74 -              (case byline of
    3.75 -                By_Metis fact_names => resolve_fact_names fact_names
    3.76 -              | Case_Split (cases, fact_names) =>
    3.77 -                resolve_fact_names fact_names
    3.78 -                  @ (case the succedent of
    3.79 -                      Assume (_, t) => make_thm t
    3.80 -                    | Obtain (_, _, _, t, _) => make_thm t
    3.81 -                    | Prove (_, _, t, _) => make_thm t
    3.82 -                    | _ => error "Internal error: unexpected succedent of case split")
    3.83 -                  :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
    3.84 -                                  | _ => error "Internal error: malformed case split")
    3.85 -                             #> make_thm)
    3.86 -                       cases)
    3.87 -            val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
    3.88 -                            |> obtain ? Config.put Metis_Tactic.new_skolem true
    3.89 -            val goal =
    3.90 -              Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
    3.91 -            fun tac {context = ctxt, prems = _} =
    3.92 -              Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
    3.93 -          in
    3.94 -            take_time timeout (fn () => goal tac)
    3.95 -          end)
    3.96 -          handle ZEROTIME => K (SOME Time.zeroTime)
    3.97 -
    3.98 -      val try_metis_quietly = the_default NONE oo try oo try_metis
    3.99 -
   3.100        (* cache metis preplay times in lazy time vector *)
   3.101        val metis_time =
   3.102          v_map_index
   3.103 -          (Lazy.lazy o handle_metis_fail o try_metis preplay_timeout
   3.104 -            o apfst (fn i => try (the o get (i-1)) proof_vect) o apsnd the)
   3.105 +          (if not preplay then K (SOME Time.zeroTime) #> Lazy.value
   3.106 +           else
   3.107 +             apsnd the
   3.108 +             #> apfst (fn i => try (get (i-1) #> the) proof_vect)
   3.109 +             #> try_metis debug type_enc lam_trans ctxt preplay_timeout
   3.110 +             #> handle_metis_fail
   3.111 +             #> Lazy.lazy)
   3.112            proof_vect
   3.113 +
   3.114        fun sum_up_time lazy_time_vector =
   3.115          Vector.foldl
   3.116            ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts))
   3.117 @@ -220,7 +158,8 @@
   3.118                val s12 = merge s1 s2
   3.119                val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
   3.120              in
   3.121 -              case try_metis_quietly timeout (NONE, s12) () of
   3.122 +              case try_metis_quietly debug type_enc lam_trans ctxt timeout
   3.123 +              (NONE, s12) () of
   3.124                  NONE => (NONE, metis_time)
   3.125                | some_t12 =>
   3.126                  (SOME s12, metis_time