refactor data structure (step 1)
authorblanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 552520dc4993b4f56
parent 55251 85f5d7da4ab6
child 55253 cfd276a7dbeb
refactor data structure (step 1)
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_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
     1.8 +    ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data) proof =
     1.9    if compress_isar <= 1.0 then
    1.10      proof
    1.11    else
    1.12 @@ -137,9 +137,10 @@
    1.13          end
    1.14  
    1.15        (* elimination of trivial, one-step subproofs *)
    1.16 -      fun elim_subproofs' time qs fix l t lfs gfs (meths as meth :: _) subs nontriv_subs =
    1.17 +      fun elim_subproofs' time qs fix l t lfs gfs (meths as meth :: meths') subs nontriv_subs =
    1.18          if null subs orelse not (compress_further ()) then
    1.19 -          (set_preplay_outcome l meth (Played time);
    1.20 +          (set_preplay_outcomes l ((meth, Lazy.value (Played time)) ::
    1.21 +             map (rpair (Lazy.value Not_Played)(*FIXME*)) meths');
    1.22             Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meths)))
    1.23          else
    1.24            (case subs of
    1.25 @@ -215,7 +216,8 @@
    1.26                val ((cand as Prove (_, _, l, _, _, ((lfs, _), meth :: _))) :: steps') = drop i steps
    1.27  
    1.28                val succs = collect_successors steps' succ_lbls
    1.29 -              val succ_meths = map (hd o snd o the o byline_of_isar_step) succs
    1.30 +              val succ_methss = map (snd o the o byline_of_isar_step) succs
    1.31 +              val succ_meths = map hd succ_methss (* FIXME *)
    1.32  
    1.33                (* only touch steps that can be preplayed successfully *)
    1.34                val Played time = Lazy.force (preplay_outcome l meth)
    1.35 @@ -244,9 +246,13 @@
    1.36                val (steps1, _ :: steps2) = chop i steps
    1.37                (* replace successors with their modified versions *)
    1.38                val steps2 = update_steps steps2 succs'
    1.39 +
    1.40 +              val succ_meths_outcomess =
    1.41 +                map2 (fn meth :: meths => fn outcome => (meth, Lazy.value outcome) ::
    1.42 +                  map (rpair (Lazy.value Not_Played)(*FIXME*)) meths) succ_methss play_outcomes
    1.43              in
    1.44                decrement_step_count (); (* candidate successfully eliminated *)
    1.45 -              map3 set_preplay_outcome succ_lbls succ_meths play_outcomes;
    1.46 +              map2 set_preplay_outcomes succ_lbls succ_meths_outcomess;
    1.47                map (replace_successor l succ_lbls) lfs;
    1.48                (* removing the step would mess up the indices; replace with dummy step instead *)
    1.49                steps1 @ dummy_isar_step :: steps2
     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,8 +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
     2.8 -      {reset_preplay_outcomes, set_preplay_outcome, preplay_outcome, preplay_quietly, ...}
     2.9 +  | minimize_isar_step_dependencies {set_preplay_outcomes, preplay_outcome, preplay_quietly, ...}
    2.10        (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
    2.11      (case Lazy.force (preplay_outcome l meth) of
    2.12        Played time =>
    2.13 @@ -43,12 +42,9 @@
    2.14  
    2.15          val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
    2.16          val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
    2.17 -
    2.18 -        val step' = mk_step_lfs_gfs min_lfs min_gfs
    2.19        in
    2.20 -        reset_preplay_outcomes step';
    2.21 -        set_preplay_outcome l meth (Played time);
    2.22 -        step'
    2.23 +        set_preplay_outcomes l [(meth, Lazy.value (Played time))];
    2.24 +        mk_step_lfs_gfs min_lfs min_gfs
    2.25        end
    2.26      | _ => step (* don't touch steps that time out or fail *))
    2.27  
     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,8 +16,7 @@
     3.4    val trace : bool Config.T
     3.5  
     3.6    type isar_preplay_data =
     3.7 -    {reset_preplay_outcomes: isar_step -> unit,
     3.8 -     set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
     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 @@ -136,8 +135,7 @@
    3.14      end
    3.15  
    3.16  type isar_preplay_data =
    3.17 -  {reset_preplay_outcomes: isar_step -> unit,
    3.18 -   set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
    3.19 +  {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit,
    3.20     preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
    3.21     preplay_quietly: Time.time -> isar_step -> play_outcome,
    3.22     overall_preplay_outcome: isar_proof -> play_outcome}
    3.23 @@ -177,8 +175,7 @@
    3.24  fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
    3.25    if not do_preplay then
    3.26      (* the "dont_preplay" option pretends that everything works just fine *)
    3.27 -    {reset_preplay_outcomes = K (),
    3.28 -     set_preplay_outcome = K (K (K ())),
    3.29 +    {set_preplay_outcomes = K (K ()),
    3.30       preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
    3.31       preplay_quietly = K (K (Played Time.zeroTime)),
    3.32       overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
    3.33 @@ -205,15 +202,9 @@
    3.34  
    3.35        val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
    3.36  
    3.37 -      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
    3.38 -          preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
    3.39 -              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
    3.40 -            (!preplay_tab)
    3.41 -        | reset_preplay_outcomes _ = ()
    3.42 -
    3.43 -      fun set_preplay_outcome l meth result =
    3.44 -        preplay_tab := Canonical_Label_Tab.map_entry l
    3.45 -          (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
    3.46 +      fun set_preplay_outcomes l meths_outcomes =
    3.47 +        preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes)
    3.48 +          (!preplay_tab)
    3.49  
    3.50        fun preplay_outcome l meth =
    3.51          (case Canonical_Label_Tab.lookup (!preplay_tab) l of
    3.52 @@ -223,17 +214,22 @@
    3.53            | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
    3.54          | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
    3.55  
    3.56 -      val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
    3.57 -
    3.58        fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) =
    3.59            Lazy.force (preplay_outcome l meth)
    3.60          | result_of_step _ = Played Time.zeroTime
    3.61  
    3.62        fun overall_preplay_outcome (Proof (_, _, steps)) =
    3.63          fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
    3.64 +
    3.65 +      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
    3.66 +          preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
    3.67 +              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
    3.68 +            (!preplay_tab)
    3.69 +        | reset_preplay_outcomes _ = ()
    3.70 +
    3.71 +      val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
    3.72      in
    3.73 -      {reset_preplay_outcomes = reset_preplay_outcomes,
    3.74 -       set_preplay_outcome = set_preplay_outcome,
    3.75 +      {set_preplay_outcomes = set_preplay_outcomes,
    3.76         preplay_outcome = preplay_outcome,
    3.77         preplay_quietly = preplay_quietly,
    3.78         overall_preplay_outcome = overall_preplay_outcome}
     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 @@ -30,7 +30,7 @@
     4.4  
     4.5  fun try0_step _ _ (step as Let _) = step
     4.6    | try0_step preplay_timeout
     4.7 -      ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
     4.8 +      ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data)
     4.9        (step as Prove (_, _, l, _, _, (_, meth :: _))) =
    4.10      let
    4.11        val timeout =
    4.12 @@ -45,8 +45,8 @@
    4.13      in
    4.14        (* FIXME: create variant after success *)
    4.15        (case Par_List.get_some try_variant (variants_of_step step) of
    4.16 -        SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), result) =>
    4.17 -        (set_preplay_outcome l meth' result; step')
    4.18 +        SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), outcome) =>
    4.19 +        (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step')
    4.20        | NONE => step)
    4.21      end
    4.22