1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
     1.3 @@ -135,10 +135,8 @@
     1.4          val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
     1.5  
     1.6          val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
     1.7 -        val (_, ctxt) =
     1.8 -          params
     1.9 -          |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
    1.10 -          |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
    1.11 +        val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
    1.12 +        val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
    1.13  
    1.14          val do_preplay = preplay_timeout <> Time.zeroTime
    1.15          val try0_isar = try0_isar andalso do_preplay
    1.16 @@ -283,19 +281,14 @@
    1.17            |> postprocess_isar_proof_remove_unreferenced_steps I
    1.18            |> relabel_isar_proof_canonically
    1.19  
    1.20 -        val preplay_ctxt = ctxt
    1.21 +        val ctxt = ctxt
    1.22            |> enrich_context_with_local_facts canonical_isar_proof
    1.23            |> silence_reconstructors debug
    1.24  
    1.25          val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
    1.26  
    1.27 -        fun init_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
    1.28 -            set_preplay_outcomes_of_isar_step preplay_data l (map (fn meth => (meth,
    1.29 -                Lazy.lazy (fn () => preplay_isar_step preplay_ctxt preplay_timeout meth step)))
    1.30 -              meths)
    1.31 -          | init_preplay_outcomes _ = ()
    1.32 -
    1.33 -        val _ = fold_isar_steps (K o init_preplay_outcomes)
    1.34 +        val _ = fold_isar_steps (fn meth =>
    1.35 +            K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
    1.36            (steps_of_isar_proof canonical_isar_proof) ()
    1.37  
    1.38          fun str_of_preplay_outcome outcome =
    1.39 @@ -316,12 +309,12 @@
    1.40          val (play_outcome, isar_proof) =
    1.41            canonical_isar_proof
    1.42            |> tap (trace_isar_proof "Original")
    1.43 -          |> compress_isar_proof preplay_ctxt compress_isar preplay_data
    1.44 +          |> compress_isar_proof ctxt compress_isar preplay_data
    1.45            |> tap (trace_isar_proof "Compressed")
    1.46 -          |> try0_isar ? try0_isar_proof preplay_ctxt preplay_timeout preplay_data
    1.47 +          |> try0_isar ? try0_isar_proof ctxt preplay_timeout preplay_data
    1.48            |> tap (trace_isar_proof "Tried0")
    1.49            |> postprocess_isar_proof_remove_unreferenced_steps
    1.50 -               (try0_isar ? minimize_isar_step_dependencies preplay_ctxt preplay_data)
    1.51 +               (try0_isar ? minimize_isar_step_dependencies ctxt preplay_data)
    1.52            |> tap (trace_isar_proof "Minimized")
    1.53            |> `(preplay_outcome_of_isar_proof (!preplay_data))
    1.54            ||> chain_isar_proof

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
     2.3 @@ -137,11 +137,16 @@
     2.4          end
     2.5  
     2.6        (* elimination of trivial, one-step subproofs *)
     2.7 -      fun elim_subproofs' time qs fix l t lfs gfs (meths as meth :: meths') subs nontriv_subs =
     2.8 +      fun elim_one_subproof time qs fix l t lfs gfs (meths as meth :: _) subs nontriv_subs =
     2.9          if null subs orelse not (compress_further ()) then
    2.10 -          (set_preplay_outcomes_of_isar_step preplay_data l ((meth, Lazy.value (Played time)) ::
    2.11 -             map (rpair (Lazy.value Not_Played)(*FIXME*)) meths');
    2.12 -           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meths)))
    2.13 +          let
    2.14 +            val subproofs = List.revAppend (nontriv_subs, subs)
    2.15 +            val step = Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meths))
    2.16 +          in
    2.17 +            set_preplay_outcomes_of_isar_step ctxt time preplay_data step
    2.18 +              [(meth, Lazy.value (Played time))];
    2.19 +            step
    2.20 +          end
    2.21          else
    2.22            (case subs of
    2.23              (sub as Proof (_, assms, sub_steps)) :: subs =>
    2.24 @@ -166,11 +171,11 @@
    2.25              in
    2.26                decrement_step_count (); (* l' successfully eliminated! *)
    2.27                map (replace_successor l' [l]) lfs';
    2.28 -              elim_subproofs' time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs
    2.29 +              elim_one_subproof time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs
    2.30              end
    2.31              handle Bind =>
    2.32 -            elim_subproofs' time qs fix l t lfs gfs meths subs (sub :: nontriv_subs))
    2.33 -          | _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
    2.34 +              elim_one_subproof time qs fix l t lfs gfs meths subs (sub :: nontriv_subs))
    2.35 +          | _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof")
    2.36  
    2.37        fun elim_subproofs (step as Let _) = step
    2.38          | elim_subproofs (step as Prove (qs, fix, l, t, subproofs,
    2.39 @@ -179,7 +184,7 @@
    2.40              step
    2.41            else
    2.42              (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of
    2.43 -              Played time => elim_subproofs' time qs fix l t lfs gfs meths subproofs []
    2.44 +              Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs []
    2.45              | _ => step)
    2.46  
    2.47        fun compress_top_level steps =
    2.48 @@ -210,25 +215,22 @@
    2.49                 |> fold_index add_cand) []
    2.50              end
    2.51  
    2.52 -          fun try_eliminate (i, l, _) succ_lbls steps =
    2.53 +          fun try_eliminate (i, l, _) labels steps =
    2.54              let
    2.55                val ((cand as Prove (_, _, l, _, _, ((lfs, _), meth :: _))) :: steps') = drop i steps
    2.56  
    2.57 -              val succs = collect_successors steps' succ_lbls
    2.58 -              val succ_methss = map (snd o the o byline_of_isar_step) succs
    2.59 -              val succ_meths = map hd succ_methss (* FIXME *)
    2.60 +              val succs = collect_successors steps' labels
    2.61 +              val succ_meths = map (hd o snd o the o byline_of_isar_step) succs
    2.62  
    2.63                (* only touch steps that can be preplayed successfully *)
    2.64                val Played time = Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth)
    2.65  
    2.66                val succs' = map (try_merge cand #> the) succs
    2.67  
    2.68 -              val succ_times =
    2.69 -                map2 ((fn Played t => t) o Lazy.force oo
    2.70 -                  preplay_outcome_of_isar_step (!preplay_data)) succ_lbls succ_meths
    2.71 -              val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
    2.72 -              val timeouts =
    2.73 -                map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
    2.74 +              val times0 = map2 ((fn Played time => time) o Lazy.force oo
    2.75 +                preplay_outcome_of_isar_step (!preplay_data)) labels succ_meths
    2.76 +              val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
    2.77 +              val timeouts = map (curry Time.+ time_slice #> time_mult merge_timeout_slack) times0
    2.78  
    2.79                (* FIXME: debugging *)
    2.80                val _ =
    2.81 @@ -241,19 +243,20 @@
    2.82                val play_outcomes = map3 (preplay_isar_step ctxt) timeouts succ_meths succs'
    2.83  
    2.84                (* ensure none of the modified successors timed out *)
    2.85 -              val true = forall (fn Played _ => true) play_outcomes
    2.86 +              val times = map (fn Played time => time) play_outcomes
    2.87  
    2.88                val (steps1, _ :: steps2) = chop i steps
    2.89                (* replace successors with their modified versions *)
    2.90                val steps2 = update_steps steps2 succs'
    2.91  
    2.92                val succ_meths_outcomess =
    2.93 -                map2 (fn meth :: meths => fn outcome => (meth, Lazy.value outcome) ::
    2.94 -                  map (rpair (Lazy.value Not_Played)(*FIXME*)) meths) succ_methss play_outcomes
    2.95 +                map2 (fn meth => fn outcome => [(meth, Lazy.value outcome)]) succ_meths
    2.96 +                  play_outcomes
    2.97              in
    2.98                decrement_step_count (); (* candidate successfully eliminated *)
    2.99 -              map2 (set_preplay_outcomes_of_isar_step preplay_data) succ_lbls succ_meths_outcomess;
   2.100 -              map (replace_successor l succ_lbls) lfs;
   2.101 +              map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times
   2.102 +                succs succ_meths_outcomess;
   2.103 +              map (replace_successor l labels) lfs;
   2.104                (* removing the step would mess up the indices; replace with dummy step instead *)
   2.105                steps1 @ dummy_isar_step :: steps2
   2.106              end

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:14:18 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:14:18 2014 +0100
     3.3 @@ -43,9 +43,12 @@
     3.4  
     3.5          val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs) time [] lfs
     3.6          val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
     3.7 +
     3.8 +        val step' = mk_step_lfs_gfs min_lfs min_gfs
     3.9        in
    3.10 -        set_preplay_outcomes_of_isar_step preplay_data l [(meth, Lazy.value (Played time))];
    3.11 -        mk_step_lfs_gfs min_lfs min_gfs
    3.12 +        set_preplay_outcomes_of_isar_step ctxt time preplay_data step'
    3.13 +          [(meth, Lazy.value (Played time))];
    3.14 +        step'
    3.15        end
    3.16      | _ => step (* don't touch steps that time out or fail *))
    3.17  

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
     4.3 @@ -19,7 +19,8 @@
     4.4  
     4.5    val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
     4.6    val preplay_isar_step : Proof.context -> Time.time -> proof_method -> isar_step -> play_outcome
     4.7 -  val set_preplay_outcomes_of_isar_step : isar_preplay_data Unsynchronized.ref -> label ->
     4.8 +  val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
     4.9 +    isar_preplay_data Unsynchronized.ref -> isar_step ->
    4.10      (proof_method * play_outcome Lazy.lazy) list -> unit
    4.11    val preplay_outcome_of_isar_step : isar_preplay_data -> label -> proof_method ->
    4.12      play_outcome Lazy.lazy
    4.13 @@ -167,9 +168,17 @@
    4.14    | add_preplay_outcomes play1 play2 =
    4.15      Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
    4.16  
    4.17 -fun set_preplay_outcomes_of_isar_step preplay_data l meths_outcomes =
    4.18 -  preplay_data := Canonical_Label_Tab.map_default (l, [])
    4.19 -    (fold (AList.update (op =)) meths_outcomes) (!preplay_data)
    4.20 +fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
    4.21 +      (step as Prove (_, _, l, _, _, (_, meths))) meths_outcomes0 =
    4.22 +    let
    4.23 +      fun preplay meth = Lazy.lazy (fn () => preplay_isar_step ctxt timeout meth step)
    4.24 +      val meths_outcomes =
    4.25 +        fold (fn meth => AList.default (op =) (meth, preplay meth)) meths meths_outcomes0
    4.26 +    in
    4.27 +      preplay_data := Canonical_Label_Tab.map_default (l, [])
    4.28 +        (fold (AList.update (op =)) meths_outcomes) (!preplay_data)
    4.29 +    end
    4.30 +  | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
    4.31  
    4.32  fun preplay_outcome_of_isar_step preplay_data l meth =
    4.33    (case Canonical_Label_Tab.lookup preplay_data l of

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Mon Feb 03 10:14:18 2014 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Mon Feb 03 10:14:18 2014 +0100
     5.3 @@ -45,8 +45,11 @@
     5.4        (* FIXME: create variant after success *)
     5.5        (case Par_List.get_some try_method meths of
     5.6          SOME (meth', outcome) =>
     5.7 -        (set_preplay_outcomes_of_isar_step preplay_data l [(meth', Lazy.value outcome)];
     5.8 -         step_with_method meth' step)
     5.9 +        let val step' = step_with_method meth' step in
    5.10 +          (set_preplay_outcomes_of_isar_step ctxt timeout preplay_data step'
    5.11 +             [(meth', Lazy.value outcome)];
    5.12 +           step')
    5.13 +        end
    5.14        | NONE => step)
    5.15      end
    5.16