src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML
author bulwahn
Mon Nov 22 10:41:53 2010 +0100 (2010-11-22)
changeset 40633 6cd611ceb64e
child 40635 47004929bc71
permissions -rw-r--r--
adding files to use sledgehammer as a tactic for non-interactive use
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@40633
    19
    val thy = ProofContext.theory_of ctxt
bulwahn@40633
    20
    val params as {full_types, ...} =
bulwahn@40633
    21
      ((if force_full_types then [("full_types", "true")] else [])
bulwahn@40633
    22
       @ [("timeout", Int.toString (Time.toMilliseconds timeout) ^ " ms")])
bulwahn@40633
    23
(*      @ [("overlord", "true")] *)
bulwahn@40633
    24
      |> Sledgehammer_Isar.default_params thy
bulwahn@40633
    25
    val prover = Sledgehammer.get_prover_fun thy name
bulwahn@40633
    26
    val facts = []
bulwahn@40633
    27
    (* Check for constants other than the built-in HOL constants. If none of
bulwahn@40633
    28
       them appear (as should be the case for TPTP problems, unless "auto" or
bulwahn@40633
    29
       "simp" already did its "magic"), we can skip the relevance filter. *)
bulwahn@40633
    30
    val pure_goal =
bulwahn@40633
    31
      not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
bulwahn@40633
    32
                                      not (String.isSubstring "HOL" s))
bulwahn@40633
    33
                        (prop_of goal))
bulwahn@40633
    34
    val problem =
bulwahn@40633
    35
      {state = Proof.init ctxt, goal = goal, subgoal = i, axioms = [],
bulwahn@40633
    36
       only = true}
bulwahn@40633
    37
  in
bulwahn@40633
    38
    prover params (K "") problem |> #message
bulwahn@40633
    39
    handle ERROR message => "Error: " ^ message ^ "\n"
bulwahn@40633
    40
  end
bulwahn@40633
    41
bulwahn@40633
    42
fun to_period ("." :: _) = []
bulwahn@40633
    43
  | to_period ("" :: ss) = to_period ss
bulwahn@40633
    44
  | to_period (s :: ss) = s :: to_period ss
bulwahn@40633
    45
  | to_period [] = []
bulwahn@40633
    46
bulwahn@40633
    47
val extract_metis_facts =
bulwahn@40633
    48
  space_explode " "
bulwahn@40633
    49
  #> fold (maps o space_explode) ["(", ")", Symbol.ENQ, Symbol.ACK, "\n"]
bulwahn@40633
    50
  #> Library.dropwhile (not o member (op =) ["metis", "metisFT"])
bulwahn@40633
    51
  #> (fn _ :: ss => SOME (to_period ss) | _ => NONE)
bulwahn@40633
    52
bulwahn@40633
    53
val atp = "e" (* or "vampire" *)
bulwahn@40633
    54
bulwahn@40633
    55
fun thms_of_name ctxt name =
bulwahn@40633
    56
  let
bulwahn@40633
    57
    val lex = Keyword.get_lexicons
bulwahn@40633
    58
    val get = maps (ProofContext.get_fact ctxt o fst)
bulwahn@40633
    59
  in
bulwahn@40633
    60
    Source.of_string name
bulwahn@40633
    61
    |> Symbol.source {do_recover=false}
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@40633
    70
    val thy = ProofContext.theory_of ctxt
bulwahn@40633
    71
    val timeout = Time.fromSeconds (60 * 60 * 24 * 365) (* one year *)
bulwahn@40633
    72
    val s = run_atp false timeout i i ctxt th atp
bulwahn@40633
    73
    val xs = these (extract_metis_facts s)
bulwahn@40633
    74
    val ths = maps (thms_of_name ctxt) xs
bulwahn@40633
    75
  in Metis_Tactics.metis_tac ctxt ths i th end
bulwahn@40633
    76
bulwahn@40633
    77
fun sledgehammer_as_oracle_tac ctxt i th =
bulwahn@40633
    78
  let
bulwahn@40633
    79
    val thy = ProofContext.theory_of ctxt
bulwahn@40633
    80
    val timeout = Time.fromSeconds (60 * 60 * 24 * 365) (* one year *)
bulwahn@40633
    81
    val s = run_atp true timeout i i ctxt th atp
bulwahn@40633
    82
  in
bulwahn@40633
    83
    if is_some (extract_metis_facts s) then Skip_Proof.cheat_tac thy th
bulwahn@40633
    84
    else Seq.empty
bulwahn@40633
    85
  end
bulwahn@40633
    86
bulwahn@40633
    87
end;