(*  Title:      HOL/ex/sledgehammer_tactics.ML

     Author:     Jasmin Blanchette, TU Muenchen

     Copyright   2010, 2011

 Sledgehammer as a tactic.

 *)

 signature SLEDGEHAMMER_TACTICS =

 sig

   type relevance_override = Sledgehammer_Filter.relevance_override

   val sledgehammer_with_metis_tac :

     Proof.context -> (string * string) list -> relevance_override -> int

     -> tactic

   val sledgehammer_as_oracle_tac :

     Proof.context -> (string * string) list -> relevance_override -> int

     -> tactic

 end;

 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =

 struct

 open Sledgehammer_Filter

 fun run_atp override_params relevance_override i n ctxt goal =

   let

     val chained_ths = [] (* a tactic has no chained ths *)

     val params as {provers, relevance_thresholds, max_relevant, slice, ...} =

       Sledgehammer_Isar.default_params ctxt override_params

     val name = hd provers

     val prover =

       Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name

     val default_max_relevant =

       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name

     val is_built_in_const =

       Sledgehammer_Provers.is_built_in_const_for_prover ctxt name

     val relevance_fudge =

       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name

     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i

     val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers

     val facts =

       Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override

                                            chained_ths hyp_ts concl_t

       |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds

              (the_default default_max_relevant max_relevant) is_built_in_const

              relevance_fudge relevance_override chained_ths hyp_ts concl_t

     val problem =

       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,

        facts = map Sledgehammer_Provers.Untranslated_Fact facts,

        smt_filter = NONE}

   in

     (case prover params (K (K (K ""))) problem of

       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME

     | _ => NONE)

       handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)

   end

 fun thms_of_name ctxt name =

   let

     val lex = Keyword.get_lexicons

     val get = maps (Proof_Context.get_fact ctxt o fst)

   in

     Source.of_string name

     |> Symbol.source

     |> Token.source {do_recover=SOME false} lex Position.start

     |> Token.source_proper

     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE

     |> Source.exhaust

   end

 fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =

   case run_atp override_params relevance_override i i ctxt th of

     SOME facts =>

     Metis_Tactic.metis_tac [] ATP_Problem_Generate.combinatorsN ctxt

         (maps (thms_of_name ctxt) facts) i th

   | NONE => Seq.empty

 fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =

   let

     val thy = Proof_Context.theory_of ctxt

     val xs = run_atp (override_params @ [("sound", "true")]) relevance_override

                      i i ctxt th

   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end

 end;