src/HOL/ex/sledgehammer_tactics.ML
author blanchet
Fri Sep 02 14:43:20 2011 +0200 (2011-09-02)
changeset 44651 5d6a11e166cf
parent 44625 4a1132815a70
child 45514 973bb7846505
permissions -rw-r--r--
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet@42071
     1
(*  Title:      HOL/ex/sledgehammer_tactics.ML
bulwahn@40633
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@42071
     3
    Copyright   2010, 2011
bulwahn@40633
     4
bulwahn@40633
     5
Sledgehammer as a tactic.
bulwahn@40633
     6
*)
bulwahn@40633
     7
bulwahn@40633
     8
signature SLEDGEHAMMER_TACTICS =
bulwahn@40633
     9
sig
blanchet@44462
    10
  type relevance_override = Sledgehammer_Filter.relevance_override
blanchet@44462
    11
blanchet@44429
    12
  val sledgehammer_with_metis_tac :
blanchet@44462
    13
    Proof.context -> (string * string) list -> relevance_override -> int
blanchet@44462
    14
    -> tactic
blanchet@44429
    15
  val sledgehammer_as_oracle_tac :
blanchet@44462
    16
    Proof.context -> (string * string) list -> relevance_override -> int
blanchet@44462
    17
    -> tactic
bulwahn@40633
    18
end;
bulwahn@40633
    19
bulwahn@40633
    20
structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
bulwahn@40633
    21
struct
blanchet@42071
    22
blanchet@44462
    23
open Sledgehammer_Filter
blanchet@44462
    24
blanchet@44462
    25
fun run_atp override_params relevance_override i n ctxt goal =
bulwahn@40633
    26
  let
bulwahn@40921
    27
    val chained_ths = [] (* a tactic has no chained ths *)
blanchet@44429
    28
    val params as {provers, relevance_thresholds, max_relevant, slicing, ...} =
blanchet@44429
    29
      Sledgehammer_Isar.default_params ctxt override_params
blanchet@44429
    30
    val name = hd provers
blanchet@43021
    31
    val prover =
blanchet@43021
    32
      Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
bulwahn@40921
    33
    val default_max_relevant =
blanchet@42443
    34
      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
bulwahn@40921
    35
    val is_built_in_const =
blanchet@41087
    36
      Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
blanchet@41087
    37
    val relevance_fudge =
blanchet@41087
    38
      Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
blanchet@43088
    39
    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
blanchet@44625
    40
    val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
bulwahn@40921
    41
    val facts =
blanchet@44625
    42
      Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
nik@44586
    43
                                           chained_ths hyp_ts concl_t
blanchet@44625
    44
      |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
blanchet@43351
    45
             (the_default default_max_relevant max_relevant) is_built_in_const
blanchet@43351
    46
             relevance_fudge relevance_override chained_ths hyp_ts concl_t
bulwahn@40633
    47
    val problem =
blanchet@41090
    48
      {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
blanchet@41243
    49
       facts = map Sledgehammer_Provers.Untranslated_Fact facts,
blanchet@41741
    50
       smt_filter = NONE}
bulwahn@40633
    51
  in
blanchet@43051
    52
    (case prover params (K (K "")) problem of
bulwahn@40921
    53
      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
bulwahn@40921
    54
    | _ => NONE)
bulwahn@40921
    55
      handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
bulwahn@40633
    56
  end
bulwahn@40633
    57
bulwahn@40633
    58
fun thms_of_name ctxt name =
bulwahn@40633
    59
  let
bulwahn@40633
    60
    val lex = Keyword.get_lexicons
wenzelm@42361
    61
    val get = maps (Proof_Context.get_fact ctxt o fst)
bulwahn@40633
    62
  in
bulwahn@40633
    63
    Source.of_string name
bulwahn@40635
    64
    |> Symbol.source
bulwahn@40633
    65
    |> Token.source {do_recover=SOME false} lex Position.start
bulwahn@40633
    66
    |> Token.source_proper
bulwahn@40633
    67
    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
bulwahn@40633
    68
    |> Source.exhaust
bulwahn@40633
    69
  end
bulwahn@40633
    70
blanchet@44462
    71
fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
blanchet@44462
    72
  case run_atp override_params relevance_override i i ctxt th of
blanchet@44429
    73
    SOME facts =>
blanchet@44651
    74
    Metis_Tactic.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
blanchet@44429
    75
  | NONE => Seq.empty
bulwahn@40633
    76
blanchet@44462
    77
fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
bulwahn@40633
    78
  let
wenzelm@42361
    79
    val thy = Proof_Context.theory_of ctxt
blanchet@44462
    80
    val xs = run_atp (override_params @ [("sound", "true")]) relevance_override
blanchet@44462
    81
                     i i ctxt th
blanchet@41357
    82
  in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
blanchet@41357
    83
bulwahn@40633
    84
end;