tuning
authorblanchet
Fri Jan 31 18:43:16 2014 +0100 (2014-01-31)
changeset 55221ee90eebb8b73
parent 55220 9d833fe96c51
child 55222 a4ef6eb1fc20
tuning
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 18:43:16 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 18:43:16 2014 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4  (* Precondition: The proof must be labeled canonically
     1.5     (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
     1.6  fun compress_isar_proof compress_isar
     1.7 -    ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
     1.8 +    ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
     1.9    if compress_isar <= 1.0 then
    1.10      proof
    1.11    else
    1.12 @@ -148,7 +148,7 @@
    1.13                val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
    1.14  
    1.15                (* only touch proofs that can be preplayed sucessfully *)
    1.16 -              val Played time' = get_preplay_outcome l'
    1.17 +              val Played time' = preplay_outcome l'
    1.18  
    1.19                (* merge steps *)
    1.20                val subs'' = subs @ nontriv_subs
    1.21 @@ -177,7 +177,7 @@
    1.22            if subproofs = [] then
    1.23              step
    1.24            else
    1.25 -            (case get_preplay_outcome l of
    1.26 +            (case preplay_outcome l of
    1.27                Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
    1.28              | _ => step)
    1.29  
    1.30 @@ -214,10 +214,9 @@
    1.31            fun try_eliminate (i, l, _) succ_lbls steps =
    1.32              let
    1.33                (* only touch steps that can be preplayed successfully *)
    1.34 -              val Played time = get_preplay_outcome l
    1.35 +              val Played time = preplay_outcome l
    1.36  
    1.37 -              val succ_times =
    1.38 -                map (get_preplay_outcome #> (fn Played t => t)) succ_lbls
    1.39 +              val succ_times = map (preplay_outcome #> (fn Played t => t)) succ_lbls
    1.40                val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
    1.41                val timeouts =
    1.42                  map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 18:43:16 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 18:43:16 2014 +0100
     2.3 @@ -26,9 +26,9 @@
     2.4  val slack = seconds 0.1
     2.5  
     2.6  fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
     2.7 -  | minimize_isar_step_dependencies {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
     2.8 +  | minimize_isar_step_dependencies {preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
     2.9        (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
    2.10 -    (case get_preplay_outcome l of
    2.11 +    (case preplay_outcome l of
    2.12        Played time =>
    2.13        let
    2.14          fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 18:43:16 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 18:43:16 2014 +0100
     3.3 @@ -15,8 +15,9 @@
     3.4    val trace : bool Config.T
     3.5  
     3.6    type isar_preplay_data =
     3.7 -    {get_preplay_outcome: label -> play_outcome,
     3.8 +    {preplay_outcome: label -> play_outcome,
     3.9       set_preplay_outcome: label -> play_outcome -> unit,
    3.10 +     string_of_preplay_outcome: label -> string,
    3.11       preplay_quietly: Time.time -> isar_step -> play_outcome,
    3.12       overall_preplay_outcome: isar_proof -> play_outcome}
    3.13  
    3.14 @@ -145,12 +146,10 @@
    3.15         play_outcome)
    3.16      end
    3.17  
    3.18 -
    3.19 -(*** proof preplay interface ***)
    3.20 -
    3.21  type isar_preplay_data =
    3.22 -  {get_preplay_outcome: label -> play_outcome,
    3.23 +  {preplay_outcome: label -> play_outcome,
    3.24     set_preplay_outcome: label -> play_outcome -> unit,
    3.25 +   string_of_preplay_outcome: label -> string,
    3.26     preplay_quietly: Time.time -> isar_step -> play_outcome,
    3.27     overall_preplay_outcome: isar_proof -> play_outcome}
    3.28  
    3.29 @@ -189,8 +188,9 @@
    3.30  fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
    3.31    if not do_preplay then
    3.32      (* the "dont_preplay" option pretends that everything works just fine *)
    3.33 -    {get_preplay_outcome = K (Played Time.zeroTime),
    3.34 +    {preplay_outcome = K (Played Time.zeroTime),
    3.35       set_preplay_outcome = K (K ()),
    3.36 +     string_of_preplay_outcome = K "",
    3.37       preplay_quietly = K (K (Played Time.zeroTime)),
    3.38       overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
    3.39    else
    3.40 @@ -228,22 +228,25 @@
    3.41            |> Unsynchronized.ref
    3.42          end
    3.43  
    3.44 -      fun get_preplay_outcome l =
    3.45 +      fun preplay_outcome l =
    3.46          Canonical_Label_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
    3.47          handle Option.Option => raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
    3.48  
    3.49        fun set_preplay_outcome l result =
    3.50          preplay_tab := Canonical_Label_Tab.update (l, Lazy.value result) (!preplay_tab)
    3.51  
    3.52 +      fun string_of_preplay_outcome l = @{make_string} (preplay_outcome l)
    3.53 +
    3.54        val result_of_step =
    3.55 -        try (label_of_step #> the #> get_preplay_outcome)
    3.56 +        try (label_of_step #> the #> preplay_outcome)
    3.57          #> the_default (Played Time.zeroTime)
    3.58  
    3.59        fun overall_preplay_outcome (Proof (_, _, steps)) =
    3.60          fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
    3.61      in
    3.62 -      {get_preplay_outcome = get_preplay_outcome,
    3.63 +      {preplay_outcome = preplay_outcome,
    3.64         set_preplay_outcome = set_preplay_outcome,
    3.65 +       string_of_preplay_outcome = string_of_preplay_outcome,
    3.66         preplay_quietly = preplay_quietly,
    3.67         overall_preplay_outcome = overall_preplay_outcome}
    3.68      end
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 18:43:16 2014 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 18:43:16 2014 +0100
     4.3 @@ -30,11 +30,11 @@
     4.4  
     4.5  fun try0_step _ _ (step as Let _) = step
     4.6    | try0_step preplay_timeout
     4.7 -      ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
     4.8 +      ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
     4.9        (step as Prove (_, _, l, _, _, _)) =
    4.10      let
    4.11        val timeout =
    4.12 -        (case get_preplay_outcome l of
    4.13 +        (case preplay_outcome l of
    4.14            Played time => Time.+ (time, slack)
    4.15          | _ => preplay_timeout)
    4.16