renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name);
authorblanchet
Tue Dec 21 10:24:56 2010 +0100 (2010-12-21)
changeset 41358d5e91925916e
parent 41357 ae76960d86a2
child 41359 1eefe189434a
renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name);
use it in "Mirabelle.thy"
src/HOL/IsaMakefile
src/HOL/Mirabelle/Mirabelle.thy
src/HOL/Mirabelle/Mirabelle_Test.thy
src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML
src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Dec 21 10:18:56 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Dec 21 10:24:56 2010 +0100
     1.3 @@ -1314,7 +1314,7 @@
     1.4    Mirabelle/Tools/mirabelle_quickcheck.ML				\
     1.5    Mirabelle/Tools/mirabelle_refute.ML					\
     1.6    Mirabelle/Tools/mirabelle_sledgehammer.ML 				\
     1.7 -  Mirabelle/Tools/sledgehammer_tactic.ML
     1.8 +  Mirabelle/Tools/sledgehammer_tactics.ML
     1.9  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
    1.10  
    1.11  
     2.1 --- a/src/HOL/Mirabelle/Mirabelle.thy	Tue Dec 21 10:18:56 2010 +0100
     2.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy	Tue Dec 21 10:24:56 2010 +0100
     2.3 @@ -3,8 +3,9 @@
     2.4  *)
     2.5  
     2.6  theory Mirabelle
     2.7 -imports Pure
     2.8 +imports Sledgehammer
     2.9  uses "Tools/mirabelle.ML"
    2.10 +     "Tools/sledgehammer_tactics.ML"
    2.11  begin
    2.12  
    2.13  (* no multithreading, no parallel proofs *)  (* FIXME *)
     3.1 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Tue Dec 21 10:18:56 2010 +0100
     3.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Tue Dec 21 10:24:56 2010 +0100
     3.3 @@ -13,7 +13,6 @@
     3.4    "Tools/mirabelle_refute.ML"
     3.5    "Tools/mirabelle_sledgehammer.ML"
     3.6    "Tools/mirabelle_sledgehammer_filter.ML"
     3.7 -  "Tools/sledgehammer_tactic.ML"
     3.8  begin
     3.9  
    3.10  text {*
     4.1 --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Tue Dec 21 10:18:56 2010 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,101 +0,0 @@
     4.4 -(*  Title:      sledgehammer_tactics.ML
     4.5 -    Author:     Jasmin Blanchette, TU Muenchen
     4.6 -    Copyright   2010
     4.7 -
     4.8 -Sledgehammer as a tactic.
     4.9 -*)
    4.10 -
    4.11 -signature SLEDGEHAMMER_TACTICS =
    4.12 -sig
    4.13 -  val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
    4.14 -  val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
    4.15 -  val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
    4.16 -end;
    4.17 -
    4.18 -structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    4.19 -struct
    4.20 -  
    4.21 -fun run_atp force_full_types timeout i n ctxt goal name =
    4.22 -  let
    4.23 -    val chained_ths = [] (* a tactic has no chained ths *)
    4.24 -    val params as {type_sys, relevance_thresholds, max_relevant, ...} =
    4.25 -      ((if force_full_types then [("full_types", "true")] else [])
    4.26 -       @ [("timeout", Int.toString (Time.toSeconds timeout))])
    4.27 -       (* @ [("overlord", "true")] *)
    4.28 -      |> Sledgehammer_Isar.default_params ctxt
    4.29 -    val prover = Sledgehammer_Provers.get_prover ctxt false name
    4.30 -    val default_max_relevant =
    4.31 -      Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
    4.32 -    val is_built_in_const =
    4.33 -      Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    4.34 -    val relevance_fudge =
    4.35 -      Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    4.36 -    val relevance_override = {add = [], del = [], only = false}
    4.37 -    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
    4.38 -    val no_dangerous_types =
    4.39 -      Sledgehammer_ATP_Translate.types_dangerous_types type_sys
    4.40 -    val facts =
    4.41 -      Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
    4.42 -          relevance_thresholds
    4.43 -          (the_default default_max_relevant max_relevant) is_built_in_const
    4.44 -          relevance_fudge relevance_override chained_ths hyp_ts concl_t
    4.45 -    (* Check for constants other than the built-in HOL constants. If none of
    4.46 -       them appear (as should be the case for TPTP problems, unless "auto" or
    4.47 -       "simp" already did its "magic"), we can skip the relevance filter. *)
    4.48 -    val pure_goal =
    4.49 -      not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
    4.50 -                                      not (String.isSubstring "HOL" s))
    4.51 -                        (prop_of goal))
    4.52 -    val problem =
    4.53 -      {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    4.54 -       facts = map Sledgehammer_Provers.Untranslated_Fact facts,
    4.55 -       smt_head = NONE}
    4.56 -  in
    4.57 -    (case prover params (K "") problem of
    4.58 -      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
    4.59 -    | _ => NONE)
    4.60 -      handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
    4.61 -  end
    4.62 -
    4.63 -fun to_period ("." :: _) = []
    4.64 -  | to_period ("" :: ss) = to_period ss
    4.65 -  | to_period (s :: ss) = s :: to_period ss
    4.66 -  | to_period [] = []
    4.67 -
    4.68 -val atp = "vampire" (* or "e" or "spass" etc. *)
    4.69 -
    4.70 -fun thms_of_name ctxt name =
    4.71 -  let
    4.72 -    val lex = Keyword.get_lexicons
    4.73 -    val get = maps (ProofContext.get_fact ctxt o fst)
    4.74 -  in
    4.75 -    Source.of_string name
    4.76 -    |> Symbol.source
    4.77 -    |> Token.source {do_recover=SOME false} lex Position.start
    4.78 -    |> Token.source_proper
    4.79 -    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    4.80 -    |> Source.exhaust
    4.81 -  end
    4.82 -
    4.83 -fun sledgehammer_with_metis_tac ctxt i th =
    4.84 -  let
    4.85 -    val timeout = Time.fromSeconds 30
    4.86 -  in
    4.87 -    case run_atp false timeout i i ctxt th atp of
    4.88 -      SOME facts =>
    4.89 -      Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
    4.90 -    | NONE => Seq.empty
    4.91 -  end
    4.92 -
    4.93 -fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
    4.94 -  let
    4.95 -    val thy = ProofContext.theory_of ctxt
    4.96 -    val timeout = Time.fromSeconds 30
    4.97 -    val xs = run_atp force_full_types timeout i i ctxt th atp
    4.98 -  in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    4.99 -
   4.100 -val sledgehammer_as_unsound_oracle_tac =
   4.101 -  generic_sledgehammer_as_oracle_tac false
   4.102 -val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
   4.103 -
   4.104 -end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML	Tue Dec 21 10:24:56 2010 +0100
     5.3 @@ -0,0 +1,101 @@
     5.4 +(*  Title:      sledgehammer_tactics.ML
     5.5 +    Author:     Jasmin Blanchette, TU Muenchen
     5.6 +    Copyright   2010
     5.7 +
     5.8 +Sledgehammer as a tactic.
     5.9 +*)
    5.10 +
    5.11 +signature SLEDGEHAMMER_TACTICS =
    5.12 +sig
    5.13 +  val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
    5.14 +  val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
    5.15 +  val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
    5.16 +end;
    5.17 +
    5.18 +structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    5.19 +struct
    5.20 +  
    5.21 +fun run_atp force_full_types timeout i n ctxt goal name =
    5.22 +  let
    5.23 +    val chained_ths = [] (* a tactic has no chained ths *)
    5.24 +    val params as {type_sys, relevance_thresholds, max_relevant, ...} =
    5.25 +      ((if force_full_types then [("full_types", "true")] else [])
    5.26 +       @ [("timeout", Int.toString (Time.toSeconds timeout))])
    5.27 +       (* @ [("overlord", "true")] *)
    5.28 +      |> Sledgehammer_Isar.default_params ctxt
    5.29 +    val prover = Sledgehammer_Provers.get_prover ctxt false name
    5.30 +    val default_max_relevant =
    5.31 +      Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
    5.32 +    val is_built_in_const =
    5.33 +      Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    5.34 +    val relevance_fudge =
    5.35 +      Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    5.36 +    val relevance_override = {add = [], del = [], only = false}
    5.37 +    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
    5.38 +    val no_dangerous_types =
    5.39 +      Sledgehammer_ATP_Translate.types_dangerous_types type_sys
    5.40 +    val facts =
    5.41 +      Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
    5.42 +          relevance_thresholds
    5.43 +          (the_default default_max_relevant max_relevant) is_built_in_const
    5.44 +          relevance_fudge relevance_override chained_ths hyp_ts concl_t
    5.45 +    (* Check for constants other than the built-in HOL constants. If none of
    5.46 +       them appear (as should be the case for TPTP problems, unless "auto" or
    5.47 +       "simp" already did its "magic"), we can skip the relevance filter. *)
    5.48 +    val pure_goal =
    5.49 +      not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
    5.50 +                                      not (String.isSubstring "HOL" s))
    5.51 +                        (prop_of goal))
    5.52 +    val problem =
    5.53 +      {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    5.54 +       facts = map Sledgehammer_Provers.Untranslated_Fact facts,
    5.55 +       smt_head = NONE}
    5.56 +  in
    5.57 +    (case prover params (K "") problem of
    5.58 +      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
    5.59 +    | _ => NONE)
    5.60 +      handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
    5.61 +  end
    5.62 +
    5.63 +fun to_period ("." :: _) = []
    5.64 +  | to_period ("" :: ss) = to_period ss
    5.65 +  | to_period (s :: ss) = s :: to_period ss
    5.66 +  | to_period [] = []
    5.67 +
    5.68 +val atp = "vampire" (* or "e" or "spass" etc. *)
    5.69 +
    5.70 +fun thms_of_name ctxt name =
    5.71 +  let
    5.72 +    val lex = Keyword.get_lexicons
    5.73 +    val get = maps (ProofContext.get_fact ctxt o fst)
    5.74 +  in
    5.75 +    Source.of_string name
    5.76 +    |> Symbol.source
    5.77 +    |> Token.source {do_recover=SOME false} lex Position.start
    5.78 +    |> Token.source_proper
    5.79 +    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    5.80 +    |> Source.exhaust
    5.81 +  end
    5.82 +
    5.83 +fun sledgehammer_with_metis_tac ctxt i th =
    5.84 +  let
    5.85 +    val timeout = Time.fromSeconds 30
    5.86 +  in
    5.87 +    case run_atp false timeout i i ctxt th atp of
    5.88 +      SOME facts =>
    5.89 +      Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
    5.90 +    | NONE => Seq.empty
    5.91 +  end
    5.92 +
    5.93 +fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
    5.94 +  let
    5.95 +    val thy = ProofContext.theory_of ctxt
    5.96 +    val timeout = Time.fromSeconds 30
    5.97 +    val xs = run_atp force_full_types timeout i i ctxt th atp
    5.98 +  in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    5.99 +
   5.100 +val sledgehammer_as_unsound_oracle_tac =
   5.101 +  generic_sledgehammer_as_oracle_tac false
   5.102 +val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
   5.103 +
   5.104 +end;