src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML
author blanchet
Fri Dec 17 16:20:02 2010 +0100 (2010-12-17)
changeset 41243 15ba335d0ba2
parent 41138 eb80538166b6
child 41357 ae76960d86a2
permissions -rw-r--r--
compile
bulwahn@40633
     1
(*  Title:      sledgehammer_tactics.ML
bulwahn@40633
     2
    Author:     Jasmin Blanchette, TU Muenchen
bulwahn@40633
     3
    Copyright   2010
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
bulwahn@40633
    11
  val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
bulwahn@40633
    12
end;
bulwahn@40633
    13
bulwahn@40633
    14
structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
bulwahn@40633
    15
struct
bulwahn@40633
    16
  
bulwahn@40633
    17
fun run_atp force_full_types timeout i n ctxt goal name =
bulwahn@40633
    18
  let
bulwahn@40921
    19
    val chained_ths = [] (* a tactic has no chained ths *)
blanchet@41138
    20
    val params as {type_sys, relevance_thresholds, max_relevant, ...} =
bulwahn@40633
    21
      ((if force_full_types then [("full_types", "true")] else [])
bulwahn@40921
    22
       @ [("timeout", Int.toString (Time.toSeconds timeout))])
bulwahn@40921
    23
       @ [("overlord", "true")]
bulwahn@40635
    24
      |> Sledgehammer_Isar.default_params ctxt
blanchet@41087
    25
    val prover = Sledgehammer_Provers.get_prover ctxt false name
bulwahn@40921
    26
    val default_max_relevant =
blanchet@41087
    27
      Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
bulwahn@40921
    28
    val is_built_in_const =
blanchet@41087
    29
      Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
blanchet@41087
    30
    val relevance_fudge =
blanchet@41087
    31
      Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
bulwahn@40921
    32
    val relevance_override = {add = [], del = [], only = false}
bulwahn@40921
    33
    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
blanchet@41138
    34
    val no_dangerous_types =
blanchet@41138
    35
      Sledgehammer_ATP_Translate.types_dangerous_types type_sys
bulwahn@40921
    36
    val facts =
blanchet@41138
    37
      Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
blanchet@41138
    38
          relevance_thresholds
bulwahn@40921
    39
          (the_default default_max_relevant max_relevant) is_built_in_const
bulwahn@40921
    40
          relevance_fudge relevance_override chained_ths hyp_ts concl_t
bulwahn@40633
    41
    (* Check for constants other than the built-in HOL constants. If none of
bulwahn@40633
    42
       them appear (as should be the case for TPTP problems, unless "auto" or
bulwahn@40633
    43
       "simp" already did its "magic"), we can skip the relevance filter. *)
bulwahn@40633
    44
    val pure_goal =
bulwahn@40633
    45
      not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
bulwahn@40633
    46
                                      not (String.isSubstring "HOL" s))
bulwahn@40633
    47
                        (prop_of goal))
bulwahn@40633
    48
    val problem =
blanchet@41090
    49
      {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
blanchet@41243
    50
       facts = map Sledgehammer_Provers.Untranslated_Fact facts,
blanchet@41243
    51
       smt_head = NONE}
bulwahn@40633
    52
  in
bulwahn@40921
    53
    (case prover params (K "") problem of
bulwahn@40921
    54
      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
bulwahn@40921
    55
    | _ => NONE)
bulwahn@40921
    56
      handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
bulwahn@40633
    57
  end
bulwahn@40633
    58
bulwahn@40633
    59
fun to_period ("." :: _) = []
bulwahn@40633
    60
  | to_period ("" :: ss) = to_period ss
bulwahn@40633
    61
  | to_period (s :: ss) = s :: to_period ss
bulwahn@40633
    62
  | to_period [] = []
bulwahn@40633
    63
bulwahn@40633
    64
val atp = "e" (* or "vampire" *)
bulwahn@40633
    65
bulwahn@40633
    66
fun thms_of_name ctxt name =
bulwahn@40633
    67
  let
bulwahn@40633
    68
    val lex = Keyword.get_lexicons
bulwahn@40633
    69
    val get = maps (ProofContext.get_fact ctxt o fst)
bulwahn@40633
    70
  in
bulwahn@40633
    71
    Source.of_string name
bulwahn@40635
    72
    |> Symbol.source
bulwahn@40633
    73
    |> Token.source {do_recover=SOME false} lex Position.start
bulwahn@40633
    74
    |> Token.source_proper
bulwahn@40633
    75
    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
bulwahn@40633
    76
    |> Source.exhaust
bulwahn@40633
    77
  end
bulwahn@40633
    78
bulwahn@40633
    79
fun sledgehammer_with_metis_tac ctxt i th =
bulwahn@40633
    80
  let
bulwahn@40921
    81
    val timeout = Time.fromSeconds 30
bulwahn@40921
    82
  in
bulwahn@40921
    83
    case run_atp false timeout i i ctxt th atp of
bulwahn@40921
    84
      SOME facts => Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
bulwahn@40921
    85
    | NONE => Seq.empty
bulwahn@40921
    86
  end
bulwahn@40633
    87
bulwahn@40633
    88
fun sledgehammer_as_oracle_tac ctxt i th =
bulwahn@40633
    89
  let
bulwahn@40633
    90
    val thy = ProofContext.theory_of ctxt
bulwahn@40921
    91
    val timeout = Time.fromSeconds 30
bulwahn@40921
    92
    val xs = run_atp true timeout i i ctxt th atp
bulwahn@40633
    93
  in
bulwahn@40921
    94
    if is_some xs then Skip_Proof.cheat_tac thy th
bulwahn@40633
    95
    else Seq.empty
bulwahn@40633
    96
  end
bulwahn@40633
    97
bulwahn@40633
    98
end;