refactoring of data structure (step 2)
authorblanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 55255eceebcea3e00
parent 55254 2bc951e6761a
child 55256 6c317e374614
refactoring of data structure (step 2)
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	Sun Feb 02 20:53:51 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
     1.3 @@ -98,7 +98,7 @@
     1.4  (* Precondition: The proof must be labeled canonically
     1.5     (cf. "Slegehammer_Isar_Proof.relabel_isar_proof_canonically"). *)
     1.6  fun compress_isar_proof compress_isar
     1.7 -    ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data) proof =
     1.8 +    ({preplay_step, preplay_outcome, set_preplay_outcomes, ...} : isar_preplay_data) proof =
     1.9    if compress_isar <= 1.0 then
    1.10      proof
    1.11    else
    1.12 @@ -161,8 +161,8 @@
    1.13                val step'' = Prove (qs, fix, l, t, subs'', by)
    1.14  
    1.15                (* check if the modified step can be preplayed fast enough *)
    1.16 -              val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
    1.17 -              val Played time'' = preplay_quietly timeout step''
    1.18 +              val timeout = time_mult merge_timeout_slack (Time.+ (time, time'))
    1.19 +              val Played time'' = preplay_step timeout (hd meths)(*FIXME*) step''
    1.20              in
    1.21                decrement_step_count (); (* l' successfully eliminated! *)
    1.22                map (replace_successor l' [l]) lfs';
    1.23 @@ -238,7 +238,7 @@
    1.24                    ()
    1.25  
    1.26                (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
    1.27 -              val play_outcomes = map2 preplay_quietly timeouts succs'
    1.28 +              val play_outcomes = map3 preplay_step timeouts succ_meths succs'
    1.29  
    1.30                (* ensure none of the modified successors timed out *)
    1.31                val true = forall (fn Played _ => true) play_outcomes
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sun Feb 02 20:53:51 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sun Feb 02 20:53:51 2014 +0100
     2.3 @@ -26,7 +26,7 @@
     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 {set_preplay_outcomes, preplay_outcome, preplay_quietly, ...}
     2.8 +  | minimize_isar_step_dependencies {preplay_step, set_preplay_outcomes, preplay_outcome, ...}
     2.9        (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
    2.10      (case Lazy.force (preplay_outcome l meth) of
    2.11        Played time =>
    2.12 @@ -36,7 +36,7 @@
    2.13  
    2.14          fun minimize_facts _ time min_facts [] = (time, min_facts)
    2.15            | minimize_facts mk_step time min_facts (f :: facts) =
    2.16 -            (case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of
    2.17 +            (case preplay_step (Time.+ (time, slack)) meth (mk_step (min_facts @ facts)) of
    2.18                Played time => minimize_facts mk_step time min_facts facts
    2.19              | _ => minimize_facts mk_step time (f :: min_facts) facts)
    2.20  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
     3.3 @@ -16,9 +16,9 @@
     3.4    val trace : bool Config.T
     3.5  
     3.6    type isar_preplay_data =
     3.7 -    {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit,
     3.8 +    {preplay_step: Time.time -> proof_method -> isar_step -> play_outcome,
     3.9 +     set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit,
    3.10       preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
    3.11 -     preplay_quietly: Time.time -> isar_step -> play_outcome,
    3.12       overall_preplay_outcome: isar_proof -> play_outcome}
    3.13  
    3.14    val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> Time.time ->
    3.15 @@ -95,7 +95,7 @@
    3.16      | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
    3.17  
    3.18  (* main function for preplaying Isar steps; may throw exceptions *)
    3.19 -fun preplay_raw debug type_enc lam_trans ctxt timeout meth
    3.20 +fun raw_preplay_step debug type_enc lam_trans ctxt timeout meth
    3.21        (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
    3.22      let
    3.23        val goal =
    3.24 @@ -137,7 +137,7 @@
    3.25  type isar_preplay_data =
    3.26    {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit,
    3.27     preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
    3.28 -   preplay_quietly: Time.time -> isar_step -> play_outcome,
    3.29 +   preplay_step: Time.time -> proof_method -> isar_step -> play_outcome,
    3.30     overall_preplay_outcome: isar_proof -> play_outcome}
    3.31  
    3.32  fun enrich_context_with_local_facts proof ctxt =
    3.33 @@ -176,22 +176,9 @@
    3.34    let
    3.35      val ctxt = enrich_context_with_local_facts proof ctxt
    3.36  
    3.37 -    fun preplay quietly timeout meth step =
    3.38 -      preplay_raw debug type_enc lam_trans ctxt timeout meth step
    3.39 -      handle exn =>
    3.40 -        if Exn.is_interrupt exn then
    3.41 -          reraise exn
    3.42 -        else
    3.43 -          (if not quietly andalso debug then
    3.44 -             warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn)
    3.45 -           else
    3.46 -             ();
    3.47 -           Play_Failed)
    3.48 -
    3.49 -    (* preplay steps treating exceptions like timeouts *)
    3.50 -    fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) =
    3.51 -        preplay true timeout meth step
    3.52 -      | preplay_quietly _ _ = Played Time.zeroTime
    3.53 +    fun preplay_step timeout meth =
    3.54 +      try (raw_preplay_step debug type_enc lam_trans ctxt timeout meth)
    3.55 +      #> the_default Play_Failed
    3.56  
    3.57      val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
    3.58  
    3.59 @@ -216,15 +203,15 @@
    3.60  
    3.61      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
    3.62          preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
    3.63 -            (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
    3.64 +            (meth, Lazy.lazy (fn () => preplay_step preplay_timeout meth step))) meths)
    3.65            (!preplay_tab)
    3.66        | reset_preplay_outcomes _ = ()
    3.67  
    3.68      val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
    3.69    in
    3.70 -    {set_preplay_outcomes = set_preplay_outcomes,
    3.71 +    {preplay_step = preplay_step,
    3.72 +     set_preplay_outcomes = set_preplay_outcomes,
    3.73       preplay_outcome = preplay_outcome,
    3.74 -     preplay_quietly = preplay_quietly,
    3.75       overall_preplay_outcome = overall_preplay_outcome}
    3.76    end
    3.77  
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Sun Feb 02 20:53:51 2014 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Sun Feb 02 20:53:51 2014 +0100
     4.3 @@ -22,31 +22,30 @@
     4.4  open Sledgehammer_Isar_Proof
     4.5  open Sledgehammer_Isar_Preplay
     4.6  
     4.7 -fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meths))) =
     4.8 -    map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [meth]))) (tl meths)
     4.9 -  | variants_of_step _ = raise Fail "Sledgehammer_Isar_Try0: variants_of_step"
    4.10 +fun step_with_method meth (Prove (qs, xs, l, t, subproofs, (facts, _))) =
    4.11 +  Prove (qs, xs, l, t, subproofs, (facts, [meth]))
    4.12  
    4.13  val slack = seconds 0.05
    4.14  
    4.15  fun try0_step _ _ (step as Let _) = step
    4.16    | try0_step preplay_timeout
    4.17 -      ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data)
    4.18 -      (step as Prove (_, _, l, _, _, (_, meth :: _))) =
    4.19 +      ({preplay_step, set_preplay_outcomes, preplay_outcome, ...} : isar_preplay_data)
    4.20 +      (step as Prove (_, _, l, _, _, (_, meths as meth :: _))) =
    4.21      let
    4.22        val timeout =
    4.23          (case Lazy.force (preplay_outcome l meth) of
    4.24            Played time => Time.+ (time, slack)
    4.25          | _ => preplay_timeout)
    4.26  
    4.27 -      fun try_variant variant =
    4.28 -        (case preplay_quietly timeout variant of
    4.29 -          result as Played _ => SOME (variant, result)
    4.30 +      fun try_method meth =
    4.31 +        (case preplay_step timeout meth step of
    4.32 +          outcome as Played _ => SOME (meth, outcome)
    4.33          | _ => NONE)
    4.34      in
    4.35        (* FIXME: create variant after success *)
    4.36 -      (case Par_List.get_some try_variant (variants_of_step step) of
    4.37 -        SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), outcome) =>
    4.38 -        (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step')
    4.39 +      (case Par_List.get_some try_method meths of
    4.40 +        SOME (meth', outcome) =>
    4.41 +        (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step_with_method meth' step)
    4.42        | NONE => step)
    4.43      end
    4.44