src/HOL/ex/sledgehammer_tactics.ML
author blanchet
Fri Jun 10 12:01:15 2011 +0200 (2011-06-10)
changeset 43351 b19d95b4d736
parent 43212 050a03afe024
child 44390 99ef9fd7341b
permissions -rw-r--r--
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
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
bulwahn@40633
    10
  val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
blanchet@41357
    11
  val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
bulwahn@40633
    12
  val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
bulwahn@40633
    13
end;
bulwahn@40633
    14
bulwahn@40633
    15
structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
bulwahn@40633
    16
struct
blanchet@42071
    17
bulwahn@40633
    18
fun run_atp force_full_types timeout i n ctxt goal name =
bulwahn@40633
    19
  let
bulwahn@40921
    20
    val chained_ths = [] (* a tactic has no chained ths *)
blanchet@42642
    21
    val params as {relevance_thresholds, max_relevant, slicing, ...} =
bulwahn@40633
    22
      ((if force_full_types then [("full_types", "true")] else [])
wenzelm@41491
    23
       @ [("timeout", string_of_int (Time.toSeconds timeout))])
blanchet@41357
    24
       (* @ [("overlord", "true")] *)
bulwahn@40635
    25
      |> Sledgehammer_Isar.default_params ctxt
blanchet@43021
    26
    val prover =
blanchet@43021
    27
      Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
bulwahn@40921
    28
    val default_max_relevant =
blanchet@42443
    29
      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
bulwahn@40921
    30
    val is_built_in_const =
blanchet@41087
    31
      Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
blanchet@41087
    32
    val relevance_fudge =
blanchet@41087
    33
      Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
bulwahn@40921
    34
    val relevance_override = {add = [], del = [], only = false}
blanchet@43088
    35
    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
bulwahn@40921
    36
    val facts =
blanchet@43351
    37
      Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths
blanchet@43351
    38
                                           hyp_ts concl_t
blanchet@43351
    39
      |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
blanchet@43351
    40
             (the_default default_max_relevant max_relevant) is_built_in_const
blanchet@43351
    41
             relevance_fudge relevance_override chained_ths hyp_ts concl_t
bulwahn@40633
    42
    val problem =
blanchet@41090
    43
      {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
blanchet@41243
    44
       facts = map Sledgehammer_Provers.Untranslated_Fact facts,
blanchet@41741
    45
       smt_filter = NONE}
bulwahn@40633
    46
  in
blanchet@43051
    47
    (case prover params (K (K "")) problem of
bulwahn@40921
    48
      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
bulwahn@40921
    49
    | _ => NONE)
bulwahn@40921
    50
      handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
bulwahn@40633
    51
  end
bulwahn@40633
    52
blanchet@42071
    53
val atp = "e" (* or "vampire" or "spass" etc. *)
bulwahn@40633
    54
bulwahn@40633
    55
fun thms_of_name ctxt name =
bulwahn@40633
    56
  let
bulwahn@40633
    57
    val lex = Keyword.get_lexicons
wenzelm@42361
    58
    val get = maps (Proof_Context.get_fact ctxt o fst)
bulwahn@40633
    59
  in
bulwahn@40633
    60
    Source.of_string name
bulwahn@40635
    61
    |> Symbol.source
bulwahn@40633
    62
    |> Token.source {do_recover=SOME false} lex Position.start
bulwahn@40633
    63
    |> Token.source_proper
bulwahn@40633
    64
    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
bulwahn@40633
    65
    |> Source.exhaust
bulwahn@40633
    66
  end
bulwahn@40633
    67
bulwahn@40633
    68
fun sledgehammer_with_metis_tac ctxt i th =
bulwahn@40633
    69
  let
bulwahn@40921
    70
    val timeout = Time.fromSeconds 30
bulwahn@40921
    71
  in
bulwahn@40921
    72
    case run_atp false timeout i i ctxt th atp of
blanchet@41357
    73
      SOME facts =>
blanchet@43212
    74
      Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
bulwahn@40921
    75
    | NONE => Seq.empty
bulwahn@40921
    76
  end
bulwahn@40633
    77
blanchet@41357
    78
fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
bulwahn@40633
    79
  let
wenzelm@42361
    80
    val thy = Proof_Context.theory_of ctxt
bulwahn@40921
    81
    val timeout = Time.fromSeconds 30
blanchet@41357
    82
    val xs = run_atp force_full_types timeout i i ctxt th atp
blanchet@41357
    83
  in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
blanchet@41357
    84
blanchet@41357
    85
val sledgehammer_as_unsound_oracle_tac =
blanchet@41357
    86
  generic_sledgehammer_as_oracle_tac false
blanchet@41357
    87
val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
bulwahn@40633
    88
bulwahn@40633
    89
end;