honor 'dont_minimize' option when preplaying one-liner proof
authorblanchet
Mon Aug 04 11:43:19 2014 +0200 (2014-08-04)
changeset 57774d2ad1320c770
parent 57773 2719eb9d40fe
child 57775 40eea08c0cc5
honor 'dont_minimize' option when preplaying one-liner proof
src/HOL/Tools/Sledgehammer/sledgehammer.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Jun 22 06:16:57 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 04 11:43:19 2014 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    val timeoutN : string
     1.5    val unknownN : string
     1.6  
     1.7 -  val play_one_line_proof : Time.time -> (string * 'a) list -> Proof.state -> int ->
     1.8 +  val play_one_line_proof : bool -> Time.time -> (string * 'a) list -> Proof.state -> int ->
     1.9      proof_method * proof_method list list -> (string * 'a) list * (proof_method * play_outcome)
    1.10    val string_of_factss : (string * fact list) list -> string
    1.11    val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
    1.12 @@ -63,7 +63,11 @@
    1.13    (quote name,
    1.14     if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "")
    1.15  
    1.16 -fun play_one_line_proof timeout used_facts state i (preferred, methss as (meth :: _) :: _) =
    1.17 +fun is_metis_method (Metis_Method _) = true
    1.18 +  | is_metis_method _ = false
    1.19 +
    1.20 +fun play_one_line_proof minimize timeout used_facts state i
    1.21 +    (preferred, methss as (meth :: _) :: _) =
    1.22    let
    1.23      fun dont_know () =
    1.24        (used_facts,
    1.25 @@ -87,17 +91,19 @@
    1.26                  Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
    1.27              in
    1.28                (case preplay_isar_step ctxt timeout [] (mk_step fact_names meths) of
    1.29 -                (res as (Metis_Method _, Played _)) :: _ =>
    1.30 -                (used_facts, res) (* if a fact is needed by an ATP, it will be needed by "metis" *)
    1.31 -              | (meth, Played time) :: _ =>
    1.32 -                let
    1.33 -                  val (time', used_names') =
    1.34 -                    minimized_isar_step ctxt time (mk_step fact_names [meth])
    1.35 -                    ||> (facts_of_isar_step #> snd)
    1.36 -                  val used_facts' = filter (member (op =) used_names' o fst) used_facts
    1.37 -                in
    1.38 -                  (used_facts', (meth, Played time'))
    1.39 -                end
    1.40 +                (res as (meth, Played time)) :: _ =>
    1.41 +                (* if a fact is needed by an ATP, it will be needed by "metis" *)
    1.42 +                if not minimize orelse is_metis_method meth then
    1.43 +                  (used_facts, res)
    1.44 +                else
    1.45 +                  let
    1.46 +                    val (time', used_names') =
    1.47 +                      minimized_isar_step ctxt time (mk_step fact_names [meth])
    1.48 +                      ||> (facts_of_isar_step #> snd)
    1.49 +                    val used_facts' = filter (member (op =) used_names' o fst) used_facts
    1.50 +                  in
    1.51 +                    (used_facts', (meth, Played time'))
    1.52 +                  end
    1.53                | _ => try_methss methss)
    1.54              end
    1.55        in
    1.56 @@ -105,8 +111,8 @@
    1.57        end
    1.58    end
    1.59  
    1.60 -fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, preplay_timeout,
    1.61 -      expect, ...}) mode output_result only learn
    1.62 +fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout,
    1.63 +      preplay_timeout, expect, ...}) mode output_result only learn
    1.64      {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
    1.65    let
    1.66      val ctxt = Proof.context_of state
    1.67 @@ -179,8 +185,8 @@
    1.68          (if outcome = SOME ATP_Proof.TimedOut then timeoutN
    1.69           else if is_some outcome then noneN
    1.70           else someN,
    1.71 -         fn () => message (fn () => play_one_line_proof preplay_timeout used_facts state subgoal
    1.72 -           preferred_methss)))
    1.73 +         fn () => message (fn () => play_one_line_proof minimize preplay_timeout used_facts state
    1.74 +           subgoal preferred_methss)))
    1.75  
    1.76      fun go () =
    1.77        let