clean up Sledgehammer tactic
authorblanchet
Tue Aug 23 18:42:05 2011 +0200 (2011-08-23)
changeset 44429e5506cfe1b5a
parent 44428 ccb8998f70b7
child 44430 c6f0490d432f
clean up Sledgehammer tactic
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Tue Aug 23 17:44:31 2011 +0200
     1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Tue Aug 23 18:42:05 2011 +0200
     1.3 @@ -7,22 +7,21 @@
     1.4  
     1.5  signature SLEDGEHAMMER_TACTICS =
     1.6  sig
     1.7 -  val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
     1.8 -  val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
     1.9 -  val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
    1.10 +  val sledgehammer_with_metis_tac :
    1.11 +    Proof.context -> (string * string) list -> int -> tactic
    1.12 +  val sledgehammer_as_oracle_tac :
    1.13 +    Proof.context -> (string * string) list -> int -> tactic
    1.14  end;
    1.15  
    1.16  structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    1.17  struct
    1.18  
    1.19 -fun run_atp force_full_types timeout i n ctxt goal name =
    1.20 +fun run_atp override_params i n ctxt goal =
    1.21    let
    1.22      val chained_ths = [] (* a tactic has no chained ths *)
    1.23 -    val params as {relevance_thresholds, max_relevant, slicing, ...} =
    1.24 -      ((if force_full_types then [("sound", "true")] else [])
    1.25 -       @ [("timeout", string_of_int (Time.toSeconds timeout))])
    1.26 -       (* @ [("overlord", "true")] *)
    1.27 -      |> Sledgehammer_Isar.default_params ctxt
    1.28 +    val params as {provers, relevance_thresholds, max_relevant, slicing, ...} =
    1.29 +      Sledgehammer_Isar.default_params ctxt override_params
    1.30 +    val name = hd provers
    1.31      val prover =
    1.32        Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
    1.33      val default_max_relevant =
    1.34 @@ -50,8 +49,6 @@
    1.35        handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
    1.36    end
    1.37  
    1.38 -val atp = "e" (* or "vampire" or "spass" etc. *)
    1.39 -
    1.40  fun thms_of_name ctxt name =
    1.41    let
    1.42      val lex = Keyword.get_lexicons
    1.43 @@ -65,25 +62,16 @@
    1.44      |> Source.exhaust
    1.45    end
    1.46  
    1.47 -fun sledgehammer_with_metis_tac ctxt i th =
    1.48 -  let
    1.49 -    val timeout = Time.fromSeconds 30
    1.50 -  in
    1.51 -    case run_atp false timeout i i ctxt th atp of
    1.52 -      SOME facts =>
    1.53 -      Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
    1.54 -    | NONE => Seq.empty
    1.55 -  end
    1.56 +fun sledgehammer_with_metis_tac ctxt override_params i th =
    1.57 +  case run_atp override_params i i ctxt th of
    1.58 +    SOME facts =>
    1.59 +    Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
    1.60 +  | NONE => Seq.empty
    1.61  
    1.62 -fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
    1.63 +fun sledgehammer_as_oracle_tac ctxt override_params i th =
    1.64    let
    1.65      val thy = Proof_Context.theory_of ctxt
    1.66 -    val timeout = Time.fromSeconds 30
    1.67 -    val xs = run_atp force_full_types timeout i i ctxt th atp
    1.68 +    val xs = run_atp (override_params @ [("sound", "true")]) i i ctxt th
    1.69    in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    1.70  
    1.71 -val sledgehammer_as_unsound_oracle_tac =
    1.72 -  generic_sledgehammer_as_oracle_tac false
    1.73 -val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
    1.74 -
    1.75  end;