src/HOL/TPTP/sledgehammer_tactics.ML
changeset 47790 2e1636e45770
parent 47773 7292038cad2a
child 47794 4ad62c5f9f88
equal deleted inserted replaced
47789:71a526ee569a 47790:2e1636e45770
       
     1 (*  Title:      HOL/TPTP/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   type relevance_override = Sledgehammer_Filter.relevance_override
       
    11 
       
    12   val sledgehammer_with_metis_tac :
       
    13     Proof.context -> (string * string) list -> relevance_override -> int
       
    14     -> tactic
       
    15   val sledgehammer_as_oracle_tac :
       
    16     Proof.context -> (string * string) list -> relevance_override -> int
       
    17     -> tactic
       
    18 end;
       
    19 
       
    20 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
       
    21 struct
       
    22 
       
    23 open Sledgehammer_Filter
       
    24 
       
    25 fun run_prover override_params relevance_override i n ctxt goal =
       
    26   let
       
    27     val chained_ths = [] (* a tactic has no chained ths *)
       
    28     val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
       
    29       Sledgehammer_Isar.default_params ctxt override_params
       
    30     val name = hd provers
       
    31     val prover =
       
    32       Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
       
    33     val default_max_relevant =
       
    34       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
       
    35     val is_built_in_const =
       
    36       Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
       
    37     val relevance_fudge =
       
    38       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
       
    39     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
       
    40     val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
       
    41     val facts =
       
    42       Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
       
    43                                            chained_ths hyp_ts concl_t
       
    44       |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
       
    45              (the_default default_max_relevant max_relevant) is_built_in_const
       
    46              relevance_fudge relevance_override chained_ths hyp_ts concl_t
       
    47     val problem =
       
    48       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
       
    49        facts = map Sledgehammer_Provers.Untranslated_Fact facts}
       
    50   in
       
    51     (case prover params (K (K (K ""))) problem of
       
    52       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
       
    53     | _ => NONE)
       
    54       handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
       
    55   end
       
    56 
       
    57 fun thms_of_name ctxt name =
       
    58   let
       
    59     val lex = Keyword.get_lexicons
       
    60     val get = maps (Proof_Context.get_fact ctxt o fst)
       
    61   in
       
    62     Source.of_string name
       
    63     |> Symbol.source
       
    64     |> Token.source {do_recover=SOME false} lex Position.start
       
    65     |> Token.source_proper
       
    66     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
       
    67     |> Source.exhaust
       
    68   end
       
    69 
       
    70 fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
       
    71   let
       
    72     val override_params =
       
    73       override_params @
       
    74       [("preplay_timeout", "0")]
       
    75   in
       
    76     case run_prover override_params relevance_override i i ctxt th of
       
    77       SOME facts =>
       
    78       Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
       
    79           (maps (thms_of_name ctxt) facts) i th
       
    80     | NONE => Seq.empty
       
    81   end
       
    82 
       
    83 fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
       
    84   let
       
    85     val thy = Proof_Context.theory_of ctxt
       
    86     val override_params =
       
    87       override_params @
       
    88       [("preplay_timeout", "0"),
       
    89        ("minimize", "false")]
       
    90     val xs = run_prover override_params relevance_override i i ctxt th
       
    91   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
       
    92 
       
    93 end;