proper consideration of chained facts in 'try0' minimization
authorblanchet
Tue May 17 08:40:24 2016 +0200 (2016-05-17 ago)
changeset 63097ee8edbcbb4ad
parent 63096 7910b1db2596
child 63098 af0e964aad7b
child 63099 56f03591898b
proper consideration of chained facts in 'try0' minimization
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat May 14 22:00:44 2016 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue May 17 08:40:24 2016 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4                  else
     1.5                    let
     1.6                      val (time', used_names') =
     1.7 -                      minimized_isar_step ctxt time (mk_step fact_names [meth])
     1.8 +                      minimized_isar_step ctxt chained time (mk_step fact_names [meth])
     1.9                        ||> (facts_of_isar_step #> snd)
    1.10                      val used_facts' = filter (member (op =) used_names' o fst) used_facts
    1.11                    in
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sat May 14 22:00:44 2016 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Tue May 17 08:40:24 2016 +0200
     2.3 @@ -12,7 +12,8 @@
     2.4    type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
     2.5  
     2.6    val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step
     2.7 -  val minimized_isar_step : Proof.context -> Time.time -> isar_step -> Time.time * isar_step
     2.8 +  val minimized_isar_step : Proof.context -> thm list -> Time.time -> isar_step ->
     2.9 +    Time.time * isar_step
    2.10    val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref ->
    2.11      isar_step -> isar_step
    2.12    val postprocess_isar_proof_remove_show_stuttering : isar_proof -> isar_proof
    2.13 @@ -37,7 +38,7 @@
    2.14  
    2.15  val slack = seconds 0.025
    2.16  
    2.17 -fun minimized_isar_step ctxt time
    2.18 +fun minimized_isar_step ctxt chained time
    2.19      (Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
    2.20    let
    2.21      fun mk_step_lfs_gfs lfs gfs =
    2.22 @@ -45,7 +46,7 @@
    2.23  
    2.24      fun minimize_half _ min_facts [] time = (min_facts, time)
    2.25        | minimize_half mk_step min_facts (fact :: facts) time =
    2.26 -        (case preplay_isar_step_for_method ctxt [] (time + slack) meth
    2.27 +        (case preplay_isar_step_for_method ctxt chained (time + slack) meth
    2.28              (mk_step (min_facts @ facts)) of
    2.29            Played time' => minimize_half mk_step min_facts facts time'
    2.30          | _ => minimize_half mk_step (fact :: min_facts) facts time)
    2.31 @@ -64,7 +65,7 @@
    2.32          fun old_data_for_method meth' =
    2.33            (meth', peek_at_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth'))
    2.34  
    2.35 -        val (time', step') = minimized_isar_step ctxt time step
    2.36 +        val (time', step') = minimized_isar_step ctxt [] time step
    2.37        in
    2.38          set_preplay_outcomes_of_isar_step ctxt time' preplay_data step'
    2.39            ((meth, Played time') :: (if step' = step then map old_data_for_method meths else []));