src/HOL/ex/sledgehammer_tactics.ML
author blanchet
Mon Jun 06 20:36:35 2011 +0200 (2011-06-06)
changeset 43205 23b81469499f
parent 43088 0a97f3295642
child 43212 050a03afe024
permissions -rw-r--r--
more preparations towards hijacking Metis
     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 {relevance_thresholds, max_relevant, slicing, ...} =
    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 =
    27       Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
    28     val default_max_relevant =
    29       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
    30     val is_built_in_const =
    31       Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    32     val relevance_fudge =
    33       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    34     val relevance_override = {add = [], del = [], only = false}
    35     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
    36     val facts =
    37       Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    38           (the_default default_max_relevant max_relevant) (K true)
    39           is_built_in_const relevance_fudge relevance_override chained_ths
    40           hyp_ts concl_t
    41     val problem =
    42       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    43        facts = map Sledgehammer_Provers.Untranslated_Fact facts,
    44        smt_filter = NONE}
    45   in
    46     (case prover params (K (K "")) problem of
    47       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
    48     | _ => NONE)
    49       handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
    50   end
    51 
    52 val atp = "e" (* or "vampire" or "spass" etc. *)
    53 
    54 fun thms_of_name ctxt name =
    55   let
    56     val lex = Keyword.get_lexicons
    57     val get = maps (Proof_Context.get_fact ctxt o fst)
    58   in
    59     Source.of_string name
    60     |> Symbol.source
    61     |> Token.source {do_recover=SOME false} lex Position.start
    62     |> Token.source_proper
    63     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    64     |> Source.exhaust
    65   end
    66 
    67 fun sledgehammer_with_metis_tac ctxt i th =
    68   let
    69     val timeout = Time.fromSeconds 30
    70   in
    71     case run_atp false timeout i i ctxt th atp of
    72       SOME facts =>
    73       Metis_Tactics.new_metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
    74     | NONE => Seq.empty
    75   end
    76 
    77 fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
    78   let
    79     val thy = Proof_Context.theory_of ctxt
    80     val timeout = Time.fromSeconds 30
    81     val xs = run_atp force_full_types timeout i i ctxt th atp
    82   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    83 
    84 val sledgehammer_as_unsound_oracle_tac =
    85   generic_sledgehammer_as_oracle_tac false
    86 val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
    87 
    88 end;