# HG changeset patch # User blanchet # Date 1292923496 -3600 # Node ID d5e91925916e0199ca1f13179203c3fd7437c1db # Parent ae76960d86a2d772b15f744c037f9928b7dd0fad renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name); use it in "Mirabelle.thy" diff -r ae76960d86a2 -r d5e91925916e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Dec 21 10:18:56 2010 +0100 +++ b/src/HOL/IsaMakefile Tue Dec 21 10:24:56 2010 +0100 @@ -1314,7 +1314,7 @@ Mirabelle/Tools/mirabelle_quickcheck.ML \ Mirabelle/Tools/mirabelle_refute.ML \ Mirabelle/Tools/mirabelle_sledgehammer.ML \ - Mirabelle/Tools/sledgehammer_tactic.ML + Mirabelle/Tools/sledgehammer_tactics.ML @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle diff -r ae76960d86a2 -r d5e91925916e src/HOL/Mirabelle/Mirabelle.thy --- a/src/HOL/Mirabelle/Mirabelle.thy Tue Dec 21 10:18:56 2010 +0100 +++ b/src/HOL/Mirabelle/Mirabelle.thy Tue Dec 21 10:24:56 2010 +0100 @@ -3,8 +3,9 @@ *) theory Mirabelle -imports Pure +imports Sledgehammer uses "Tools/mirabelle.ML" + "Tools/sledgehammer_tactics.ML" begin (* no multithreading, no parallel proofs *) (* FIXME *) diff -r ae76960d86a2 -r d5e91925916e src/HOL/Mirabelle/Mirabelle_Test.thy --- a/src/HOL/Mirabelle/Mirabelle_Test.thy Tue Dec 21 10:18:56 2010 +0100 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Tue Dec 21 10:24:56 2010 +0100 @@ -13,7 +13,6 @@ "Tools/mirabelle_refute.ML" "Tools/mirabelle_sledgehammer.ML" "Tools/mirabelle_sledgehammer_filter.ML" - "Tools/sledgehammer_tactic.ML" begin text {* diff -r ae76960d86a2 -r d5e91925916e src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Tue Dec 21 10:18:56 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,101 +0,0 @@ -(* Title: sledgehammer_tactics.ML - Author: Jasmin Blanchette, TU Muenchen - Copyright 2010 - -Sledgehammer as a tactic. -*) - -signature SLEDGEHAMMER_TACTICS = -sig - val sledgehammer_with_metis_tac : Proof.context -> int -> tactic - val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic - val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic -end; - -structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = -struct - -fun run_atp force_full_types timeout i n ctxt goal name = - let - val chained_ths = [] (* a tactic has no chained ths *) - val params as {type_sys, relevance_thresholds, max_relevant, ...} = - ((if force_full_types then [("full_types", "true")] else []) - @ [("timeout", Int.toString (Time.toSeconds timeout))]) - (* @ [("overlord", "true")] *) - |> Sledgehammer_Isar.default_params ctxt - val prover = Sledgehammer_Provers.get_prover ctxt false name - val default_max_relevant = - Sledgehammer_Provers.default_max_relevant_for_prover ctxt name - val is_built_in_const = - Sledgehammer_Provers.is_built_in_const_for_prover ctxt name - val relevance_fudge = - Sledgehammer_Provers.relevance_fudge_for_prover ctxt name - val relevance_override = {add = [], del = [], only = false} - val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i - val no_dangerous_types = - Sledgehammer_ATP_Translate.types_dangerous_types type_sys - val facts = - Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types - relevance_thresholds - (the_default default_max_relevant max_relevant) is_built_in_const - relevance_fudge relevance_override chained_ths hyp_ts concl_t - (* Check for constants other than the built-in HOL constants. If none of - them appear (as should be the case for TPTP problems, unless "auto" or - "simp" already did its "magic"), we can skip the relevance filter. *) - val pure_goal = - not (exists_Const (fn (s, _) => String.isSubstring "." s andalso - not (String.isSubstring "HOL" s)) - (prop_of goal)) - val problem = - {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - facts = map Sledgehammer_Provers.Untranslated_Fact facts, - smt_head = NONE} - in - (case prover params (K "") problem of - {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME - | _ => NONE) - handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) - end - -fun to_period ("." :: _) = [] - | to_period ("" :: ss) = to_period ss - | to_period (s :: ss) = s :: to_period ss - | to_period [] = [] - -val atp = "vampire" (* or "e" or "spass" etc. *) - -fun thms_of_name ctxt name = - let - val lex = Keyword.get_lexicons - val get = maps (ProofContext.get_fact ctxt o fst) - in - Source.of_string name - |> Symbol.source - |> Token.source {do_recover=SOME false} lex Position.start - |> Token.source_proper - |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE - |> Source.exhaust - end - -fun sledgehammer_with_metis_tac ctxt i th = - let - val timeout = Time.fromSeconds 30 - in - case run_atp false timeout i i ctxt th atp of - SOME facts => - Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th - | NONE => Seq.empty - end - -fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th = - let - val thy = ProofContext.theory_of ctxt - val timeout = Time.fromSeconds 30 - val xs = run_atp force_full_types timeout i i ctxt th atp - in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end - -val sledgehammer_as_unsound_oracle_tac = - generic_sledgehammer_as_oracle_tac false -val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true - -end; diff -r ae76960d86a2 -r d5e91925916e src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML Tue Dec 21 10:24:56 2010 +0100 @@ -0,0 +1,101 @@ +(* Title: sledgehammer_tactics.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2010 + +Sledgehammer as a tactic. +*) + +signature SLEDGEHAMMER_TACTICS = +sig + val sledgehammer_with_metis_tac : Proof.context -> int -> tactic + val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic + val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic +end; + +structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = +struct + +fun run_atp force_full_types timeout i n ctxt goal name = + let + val chained_ths = [] (* a tactic has no chained ths *) + val params as {type_sys, relevance_thresholds, max_relevant, ...} = + ((if force_full_types then [("full_types", "true")] else []) + @ [("timeout", Int.toString (Time.toSeconds timeout))]) + (* @ [("overlord", "true")] *) + |> Sledgehammer_Isar.default_params ctxt + val prover = Sledgehammer_Provers.get_prover ctxt false name + val default_max_relevant = + Sledgehammer_Provers.default_max_relevant_for_prover ctxt name + val is_built_in_const = + Sledgehammer_Provers.is_built_in_const_for_prover ctxt name + val relevance_fudge = + Sledgehammer_Provers.relevance_fudge_for_prover ctxt name + val relevance_override = {add = [], del = [], only = false} + val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i + val no_dangerous_types = + Sledgehammer_ATP_Translate.types_dangerous_types type_sys + val facts = + Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types + relevance_thresholds + (the_default default_max_relevant max_relevant) is_built_in_const + relevance_fudge relevance_override chained_ths hyp_ts concl_t + (* Check for constants other than the built-in HOL constants. If none of + them appear (as should be the case for TPTP problems, unless "auto" or + "simp" already did its "magic"), we can skip the relevance filter. *) + val pure_goal = + not (exists_Const (fn (s, _) => String.isSubstring "." s andalso + not (String.isSubstring "HOL" s)) + (prop_of goal)) + val problem = + {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, + facts = map Sledgehammer_Provers.Untranslated_Fact facts, + smt_head = NONE} + in + (case prover params (K "") problem of + {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME + | _ => NONE) + handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) + end + +fun to_period ("." :: _) = [] + | to_period ("" :: ss) = to_period ss + | to_period (s :: ss) = s :: to_period ss + | to_period [] = [] + +val atp = "vampire" (* or "e" or "spass" etc. *) + +fun thms_of_name ctxt name = + let + val lex = Keyword.get_lexicons + val get = maps (ProofContext.get_fact ctxt o fst) + in + Source.of_string name + |> Symbol.source + |> Token.source {do_recover=SOME false} lex Position.start + |> Token.source_proper + |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE + |> Source.exhaust + end + +fun sledgehammer_with_metis_tac ctxt i th = + let + val timeout = Time.fromSeconds 30 + in + case run_atp false timeout i i ctxt th atp of + SOME facts => + Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th + | NONE => Seq.empty + end + +fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th = + let + val thy = ProofContext.theory_of ctxt + val timeout = Time.fromSeconds 30 + val xs = run_atp force_full_types timeout i i ctxt th atp + in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end + +val sledgehammer_as_unsound_oracle_tac = + generic_sledgehammer_as_oracle_tac false +val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true + +end;