src/HOL/ex/sledgehammer_tactics.ML
author blanchet
Wed Mar 23 10:06:27 2011 +0100 (2011-03-23)
changeset 42071 04577a7e0c51
parent 41959 src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML@b460124855b8
child 42106 ed1d40888b1b
permissions -rw-r--r--
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
default to "e" rather than "vampire" since E is part of the Isabelle bundle
     1 (*  Title:      HOL/ex/sledgehammer_tactics.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2010, 2011
     4 
     5 Sledgehammer as a tactic.
     6 *)
     7 
     8 signature SLEDGEHAMMER_TACTICS =
     9 sig
    10   val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
    11   val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
    12   val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
    13 end;
    14 
    15 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    16 struct
    17 
    18 fun run_atp force_full_types timeout i n ctxt goal name =
    19   let
    20     val chained_ths = [] (* a tactic has no chained ths *)
    21     val params as {type_sys, relevance_thresholds, max_relevant, ...} =
    22       ((if force_full_types then [("full_types", "true")] else [])
    23        @ [("timeout", string_of_int (Time.toSeconds timeout))])
    24        (* @ [("overlord", "true")] *)
    25       |> Sledgehammer_Isar.default_params ctxt
    26     val prover = Sledgehammer_Provers.get_prover ctxt false name
    27     val default_max_relevant =
    28       Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
    29     val is_built_in_const =
    30       Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    31     val relevance_fudge =
    32       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    33     val relevance_override = {add = [], del = [], only = false}
    34     val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
    35     val no_dangerous_types =
    36       Sledgehammer_ATP_Translate.types_dangerous_types type_sys
    37     val facts =
    38       Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
    39           relevance_thresholds
    40           (the_default default_max_relevant max_relevant) is_built_in_const
    41           relevance_fudge relevance_override chained_ths hyp_ts concl_t
    42     val problem =
    43       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    44        facts = map Sledgehammer_Provers.Untranslated_Fact facts,
    45        smt_filter = NONE}
    46   in
    47     (case prover params (K "") problem of
    48       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
    49     | _ => NONE)
    50       handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
    51   end
    52 
    53 fun to_period ("." :: _) = []
    54   | to_period ("" :: ss) = to_period ss
    55   | to_period (s :: ss) = s :: to_period ss
    56   | to_period [] = []
    57 
    58 val atp = "e" (* or "vampire" or "spass" etc. *)
    59 
    60 fun thms_of_name ctxt name =
    61   let
    62     val lex = Keyword.get_lexicons
    63     val get = maps (ProofContext.get_fact ctxt o fst)
    64   in
    65     Source.of_string name
    66     |> Symbol.source
    67     |> Token.source {do_recover=SOME false} lex Position.start
    68     |> Token.source_proper
    69     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    70     |> Source.exhaust
    71   end
    72 
    73 fun sledgehammer_with_metis_tac ctxt i th =
    74   let
    75     val timeout = Time.fromSeconds 30
    76   in
    77     case run_atp false timeout i i ctxt th atp of
    78       SOME facts =>
    79       Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
    80     | NONE => Seq.empty
    81   end
    82 
    83 fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
    84   let
    85     val thy = ProofContext.theory_of ctxt
    86     val timeout = Time.fromSeconds 30
    87     val xs = run_atp force_full_types timeout i i ctxt th atp
    88   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    89 
    90 val sledgehammer_as_unsound_oracle_tac =
    91   generic_sledgehammer_as_oracle_tac false
    92 val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
    93 
    94 end;