src/HOL/TPTP/sledgehammer_tactics.ML
author blanchet
Fri, 27 Apr 2012 15:24:37 +0200
changeset 47790 2e1636e45770
parent 47773 src/HOL/ex/sledgehammer_tactics.ML@7292038cad2a
child 47794 4ad62c5f9f88
permissions -rw-r--r--
move file to where it belongs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47790
2e1636e45770 move file to where it belongs
blanchet
parents: 47773
diff changeset
     1
(*  Title:      HOL/TPTP/sledgehammer_tactics.ML
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
42071
04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents: 41959
diff changeset
     3
    Copyright   2010, 2011
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     4
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     5
Sledgehammer as a tactic.
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     6
*)
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     7
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     8
signature SLEDGEHAMMER_TACTICS =
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
     9
sig
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44429
diff changeset
    10
  type relevance_override = Sledgehammer_Filter.relevance_override
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44429
diff changeset
    11
44429
e5506cfe1b5a clean up Sledgehammer tactic
blanchet
parents: 44390
diff changeset
    12
  val sledgehammer_with_metis_tac :
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44429
diff changeset
    13
    Proof.context -> (string * string) list -> relevance_override -> int
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44429
diff changeset
    14
    -> tactic
44429
e5506cfe1b5a clean up Sledgehammer tactic
blanchet
parents: 44390
diff changeset
    15
  val sledgehammer_as_oracle_tac :
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44429
diff changeset
    16
    Proof.context -> (string * string) list -> relevance_override -> int
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44429
diff changeset
    17
    -> tactic
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    18
end;
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    19
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    20
structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    21
struct
42071
04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents: 41959
diff changeset
    22
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44429
diff changeset
    23
open Sledgehammer_Filter
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44429
diff changeset
    24
47773
blanchet
parents: 47766
diff changeset
    25
fun run_prover override_params relevance_override i n ctxt goal =
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    26
  let
40921
a516fbdd9931 improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents: 40635
diff changeset
    27
    val chained_ths = [] (* a tactic has no chained ths *)
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45520
diff changeset
    28
    val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
44429
e5506cfe1b5a clean up Sledgehammer tactic
blanchet
parents: 44390
diff changeset
    29
      Sledgehammer_Isar.default_params ctxt override_params
e5506cfe1b5a clean up Sledgehammer tactic
blanchet
parents: 44390
diff changeset
    30
    val name = hd provers
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43004
diff changeset
    31
    val prover =
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43004
diff changeset
    32
      Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
40921
a516fbdd9931 improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents: 40635
diff changeset
    33
    val default_max_relevant =
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45520
diff changeset
    34
      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
40921
a516fbdd9931 improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents: 40635
diff changeset
    35
    val is_built_in_const =
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40983
diff changeset
    36
      Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40983
diff changeset
    37
    val relevance_fudge =
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40983
diff changeset
    38
      Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
43088
0a97f3295642 compile
blanchet
parents: 43051
diff changeset
    39
    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
44625
4a1132815a70 more tuning
blanchet
parents: 44586
diff changeset
    40
    val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
40921
a516fbdd9931 improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents: 40635
diff changeset
    41
    val facts =
44625
4a1132815a70 more tuning
blanchet
parents: 44586
diff changeset
    42
      Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
44586
eeba1eedf32d improved handling of induction rules in Sledgehammer
nik
parents: 44462
diff changeset
    43
                                           chained_ths hyp_ts concl_t
44625
4a1132815a70 more tuning
blanchet
parents: 44586
diff changeset
    44
      |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
43351
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43212
diff changeset
    45
             (the_default default_max_relevant max_relevant) is_built_in_const
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43212
diff changeset
    46
             relevance_fudge relevance_override chained_ths hyp_ts concl_t
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    47
    val problem =
41090
b98fe4de1ecd renamings
blanchet
parents: 41087
diff changeset
    48
      {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
47532
8e1a120ed492 compile
blanchet
parents: 46365
diff changeset
    49
       facts = map Sledgehammer_Provers.Untranslated_Fact facts}
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    50
  in
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45514
diff changeset
    51
    (case prover params (K (K (K ""))) problem of
40921
a516fbdd9931 improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents: 40635
diff changeset
    52
      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
a516fbdd9931 improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents: 40635
diff changeset
    53
    | _ => NONE)
a516fbdd9931 improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents: 40635
diff changeset
    54
      handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    55
  end
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    56
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    57
fun thms_of_name ctxt name =
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    58
  let
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    59
    val lex = Keyword.get_lexicons
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42106
diff changeset
    60
    val get = maps (Proof_Context.get_fact ctxt o fst)
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    61
  in
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    62
    Source.of_string name
40635
47004929bc71 ported sledgehammer_tactic to current development version
bulwahn
parents: 40633
diff changeset
    63
    |> Symbol.source
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    64
    |> Token.source {do_recover=SOME false} lex Position.start
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    65
    |> Token.source_proper
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    66
    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    67
    |> Source.exhaust
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    68
  end
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    69
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44429
diff changeset
    70
fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    71
  let
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    72
    val override_params =
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    73
      override_params @
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    74
      [("preplay_timeout", "0")]
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    75
  in
47773
blanchet
parents: 47766
diff changeset
    76
    case run_prover override_params relevance_override i i ctxt th of
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    77
      SOME facts =>
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    78
      Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    79
          (maps (thms_of_name ctxt) facts) i th
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    80
    | NONE => Seq.empty
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    81
  end
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    82
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44429
diff changeset
    83
fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    84
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42106
diff changeset
    85
    val thy = Proof_Context.theory_of ctxt
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    86
    val override_params =
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    87
      override_params @
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    88
      [("preplay_timeout", "0"),
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47532
diff changeset
    89
       ("minimize", "false")]
47773
blanchet
parents: 47766
diff changeset
    90
    val xs = run_prover override_params relevance_override i i ctxt th
41357
ae76960d86a2 added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents: 41243
diff changeset
    91
  in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
ae76960d86a2 added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents: 41243
diff changeset
    92
40633
6cd611ceb64e adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff changeset
    93
end;