1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Aug 24 11:17:33 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Aug 24 11:17:33 2011 +0200
     1.3 @@ -569,27 +569,34 @@
     1.4  fun run_reconstructor trivial full m name reconstructor named_thms id
     1.5      ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
     1.6    let
     1.7 -    fun do_reconstructor thms ctxt =
     1.8 -      (if !reconstructor = "sledgehammer_tac" then
     1.9 -         (fn ctxt => fn thms =>
    1.10 -            Method.insert_tac thms THEN'
    1.11 -            (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
    1.12 -                 (e_override_params timeout)
    1.13 -             ORELSE'
    1.14 -             Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
    1.15 -                 (vampire_override_params timeout)))
    1.16 -       else if !reconstructor = "smt" then
    1.17 -         SMT_Solver.smt_tac
    1.18 -       else if full orelse !reconstructor = "metis (full_types)" then
    1.19 -         Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc]
    1.20 -       else if !reconstructor = "metis (no_types)" then
    1.21 -         Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
    1.22 -       else if !reconstructor = "metis" then
    1.23 -         Metis_Tactics.metis_tac []
    1.24 -       else
    1.25 -         K (K (K all_tac))) ctxt thms
    1.26 -    fun apply_reconstructor thms =
    1.27 -      Mirabelle.can_apply timeout (do_reconstructor thms) st
    1.28 +    fun do_reconstructor named_thms ctxt =
    1.29 +      let
    1.30 +        val ref_of_str =
    1.31 +          suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm
    1.32 +          #> fst
    1.33 +        val thms = named_thms |> maps snd
    1.34 +        val facts = named_thms |> map (ref_of_str o fst o fst)
    1.35 +        val relevance_override = {add = facts, del = [], only = true}
    1.36 +      in
    1.37 +        if !reconstructor = "sledgehammer_tac" then
    1.38 +          Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
    1.39 +             (e_override_params timeout) relevance_override
    1.40 +          ORELSE'
    1.41 +          Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
    1.42 +             (vampire_override_params timeout) relevance_override
    1.43 +        else if !reconstructor = "smt" then
    1.44 +          SMT_Solver.smt_tac ctxt thms
    1.45 +        else if full orelse !reconstructor = "metis (full_types)" then
    1.46 +          Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] ctxt thms
    1.47 +        else if !reconstructor = "metis (no_types)" then
    1.48 +          Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] ctxt thms
    1.49 +        else if !reconstructor = "metis" then
    1.50 +          Metis_Tactics.metis_tac [] ctxt thms
    1.51 +        else
    1.52 +          K all_tac
    1.53 +      end
    1.54 +    fun apply_reconstructor named_thms =
    1.55 +      Mirabelle.can_apply timeout (do_reconstructor named_thms) st
    1.56  
    1.57      fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
    1.58        | with_time (true, t) = (change_data id (inc_reconstructor_success m);
    1.59 @@ -601,8 +608,8 @@
    1.60            if name = "proof" then change_data id (inc_reconstructor_proofs m)
    1.61            else ();
    1.62            "succeeded (" ^ string_of_int t ^ ")")
    1.63 -    fun timed_reconstructor thms =
    1.64 -      (with_time (Mirabelle.cpu_time apply_reconstructor thms), true)
    1.65 +    fun timed_reconstructor named_thms =
    1.66 +      (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true)
    1.67        handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m);
    1.68                 ("timeout", false))
    1.69             | ERROR msg => ("error: " ^ msg, false)
    1.70 @@ -612,7 +619,7 @@
    1.71      val _ = if trivial then ()
    1.72              else change_data id (inc_reconstructor_nontriv_calls m)
    1.73    in
    1.74 -    maps snd named_thms
    1.75 +    named_thms
    1.76      |> timed_reconstructor
    1.77      |>> log o prefix (reconstructor_tag reconstructor id)
    1.78      |> snd

     2.1 --- a/src/HOL/TPTP/CASC_Setup.thy	Wed Aug 24 11:17:33 2011 +0200
     2.2 +++ b/src/HOL/TPTP/CASC_Setup.thy	Wed Aug 24 11:17:33 2011 +0200
     2.3 @@ -119,14 +119,16 @@
     2.4     SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
     2.5     ORELSE
     2.6     SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
     2.7 -       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
     2.8 +       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []
     2.9 +                      Sledgehammer_Filter.no_relevance_override))
    2.10     ORELSE
    2.11     SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
    2.12     ORELSE
    2.13     SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
    2.14     ORELSE
    2.15     SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
    2.16 -       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
    2.17 +       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []
    2.18 +                          Sledgehammer_Filter.no_relevance_override))
    2.19     ORELSE
    2.20     SOLVE_TIMEOUT (max_secs div 10) "metis"
    2.21         (ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Aug 24 11:17:33 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Aug 24 11:17:33 2011 +0200
     3.3 @@ -38,6 +38,7 @@
     3.4    val trace : bool Config.T
     3.5    val ignore_no_atp : bool Config.T
     3.6    val instantiate_inducts : bool Config.T
     3.7 +  val no_relevance_override : relevance_override
     3.8    val const_names_in_fact :
     3.9      theory -> (string * typ -> term list -> bool * term list) -> term
    3.10      -> string list
    3.11 @@ -100,6 +101,8 @@
    3.12     del : (Facts.ref * Attrib.src list) list,
    3.13     only : bool}
    3.14  
    3.15 +val no_relevance_override = {add = [], del = [], only = false}
    3.16 +
    3.17  val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
    3.18  val abs_name = sledgehammer_prefix ^ "abs"
    3.19  val skolem_prefix = sledgehammer_prefix ^ "sko"

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Aug 24 11:17:33 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Aug 24 11:17:33 2011 +0200
     4.3 @@ -22,6 +22,7 @@
     4.4  open ATP_Systems
     4.5  open ATP_Translate
     4.6  open Sledgehammer_Util
     4.7 +open Sledgehammer_Filter
     4.8  open Sledgehammer_Provers
     4.9  open Sledgehammer_Minimize
    4.10  open Sledgehammer_Run
    4.11 @@ -46,7 +47,6 @@
    4.12  
    4.13  (** Sledgehammer commands **)
    4.14  
    4.15 -val no_relevance_override = {add = [], del = [], only = false}
    4.16  fun add_relevance_override ns : relevance_override =
    4.17    {add = ns, del = [], only = false}
    4.18  fun del_relevance_override ns : relevance_override =

     5.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Wed Aug 24 11:17:33 2011 +0200
     5.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Wed Aug 24 11:17:33 2011 +0200
     5.3 @@ -7,16 +7,22 @@
     5.4  
     5.5  signature SLEDGEHAMMER_TACTICS =
     5.6  sig
     5.7 +  type relevance_override = Sledgehammer_Filter.relevance_override
     5.8 +
     5.9    val sledgehammer_with_metis_tac :
    5.10 -    Proof.context -> (string * string) list -> int -> tactic
    5.11 +    Proof.context -> (string * string) list -> relevance_override -> int
    5.12 +    -> tactic
    5.13    val sledgehammer_as_oracle_tac :
    5.14 -    Proof.context -> (string * string) list -> int -> tactic
    5.15 +    Proof.context -> (string * string) list -> relevance_override -> int
    5.16 +    -> tactic
    5.17  end;
    5.18  
    5.19  structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    5.20  struct
    5.21  
    5.22 -fun run_atp override_params i n ctxt goal =
    5.23 +open Sledgehammer_Filter
    5.24 +
    5.25 +fun run_atp override_params relevance_override i n ctxt goal =
    5.26    let
    5.27      val chained_ths = [] (* a tactic has no chained ths *)
    5.28      val params as {provers, relevance_thresholds, max_relevant, slicing, ...} =
    5.29 @@ -30,7 +36,6 @@
    5.30        Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    5.31      val relevance_fudge =
    5.32        Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    5.33 -    val relevance_override = {add = [], del = [], only = false}
    5.34      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
    5.35      val facts =
    5.36        Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths
    5.37 @@ -62,16 +67,17 @@
    5.38      |> Source.exhaust
    5.39    end
    5.40  
    5.41 -fun sledgehammer_with_metis_tac ctxt override_params i th =
    5.42 -  case run_atp override_params i i ctxt th of
    5.43 +fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
    5.44 +  case run_atp override_params relevance_override i i ctxt th of
    5.45      SOME facts =>
    5.46      Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
    5.47    | NONE => Seq.empty
    5.48  
    5.49 -fun sledgehammer_as_oracle_tac ctxt override_params i th =
    5.50 +fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
    5.51    let
    5.52      val thy = Proof_Context.theory_of ctxt
    5.53 -    val xs = run_atp (override_params @ [("sound", "true")]) i i ctxt th
    5.54 +    val xs = run_atp (override_params @ [("sound", "true")]) relevance_override
    5.55 +                     i i ctxt th
    5.56    in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    5.57  
    5.58  end;