# HG changeset patch # User blanchet # Date 1292937525 -3600 # Node ID 3cb30e525ee9320ba7860bb5c1ae1f6cd46b9350 # Parent 04ecd79827f29b4131991608946ae5b312e10758# Parent d1e4a20911cbe1483b1c63a6051961b237c35437 merged diff -r 04ecd79827f2 -r 3cb30e525ee9 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Dec 21 12:48:47 2010 +0100 +++ b/src/HOL/IsaMakefile Tue Dec 21 14:18:45 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 04ecd79827f2 -r 3cb30e525ee9 src/HOL/Mirabelle/Mirabelle.thy --- a/src/HOL/Mirabelle/Mirabelle.thy Tue Dec 21 12:48:47 2010 +0100 +++ b/src/HOL/Mirabelle/Mirabelle.thy Tue Dec 21 14:18:45 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 04ecd79827f2 -r 3cb30e525ee9 src/HOL/Mirabelle/Mirabelle_Test.thy --- a/src/HOL/Mirabelle/Mirabelle_Test.thy Tue Dec 21 12:48:47 2010 +0100 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Tue Dec 21 14:18:45 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 04ecd79827f2 -r 3cb30e525ee9 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Dec 21 12:48:47 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Dec 21 14:18:45 2010 +0100 @@ -13,6 +13,7 @@ val minimizeK = "minimize" val minimize_timeoutK = "minimize_timeout" val metis_ftK = "metis_ft" +val reconstructorK = "reconstructor" fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " @@ -331,10 +332,13 @@ type locality = Sledgehammer_Filter.locality (* hack *) -fun reconstructor_from_msg msg = - if String.isSubstring "metisFT" msg then "metisFT" - else if String.isSubstring "metis" msg then "metis" - else "smt" +fun reconstructor_from_msg args msg = + (case AList.lookup (op =) args reconstructorK of + SOME name => name + | NONE => + if String.isSubstring "metisFT" msg then "metisFT" + else if String.isSubstring "metis" msg then "metis" + else "smt") local @@ -445,7 +449,7 @@ change_data id (inc_sh_max_lems (length names)); change_data id (inc_sh_time_isa time_isa); change_data id (inc_sh_time_prover time_prover); - reconstructor := reconstructor_from_msg msg; + reconstructor := reconstructor_from_msg args msg; named_thms := SOME (map_filter get_thms names); log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) @@ -487,7 +491,7 @@ change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); if length named_thms' = n0 then log (minimize_tag id ^ "already minimal") - else (reconstructor := reconstructor_from_msg msg; + else (reconstructor := reconstructor_from_msg args msg; named_thms := SOME named_thms'; log (minimize_tag id ^ "succeeded:\n" ^ msg)) ) @@ -499,7 +503,11 @@ ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = let fun do_reconstructor thms ctxt = - (if !reconstructor = "smt" then + (if !reconstructor = "sledgehammer_tac" then + (fn ctxt => fn thms => + Method.insert_tac thms THEN' + Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt) + else if !reconstructor = "smt" then SMT_Solver.smt_tac else if full orelse !reconstructor = "metisFT" then Metis_Tactics.metisFT_tac diff -r 04ecd79827f2 -r 3cb30e525ee9 src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Tue Dec 21 12:48:47 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,98 +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_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 = "e" (* or "vampire" *) - -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 sledgehammer_as_oracle_tac ctxt i th = - let - val thy = ProofContext.theory_of ctxt - val timeout = Time.fromSeconds 30 - val xs = run_atp true timeout i i ctxt th atp - in - if is_some xs then Skip_Proof.cheat_tac thy th - else Seq.empty - end - -end; diff -r 04ecd79827f2 -r 3cb30e525ee9 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 14:18:45 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; diff -r 04ecd79827f2 -r 3cb30e525ee9 src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Tue Dec 21 12:48:47 2010 +0100 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Tue Dec 21 14:18:45 2010 +0100 @@ -82,7 +82,7 @@ print SETUP_FILE "setup {* Mirabelle_$name.invoke ["; my $sep = ""; foreach (split(/,/, $settings_str)) { - if (m/\s*(.*)\s*=\s*(.*)\s*/) { + if (m/\s*([^=]*)\s*=\s*(.*)\s*/) { print SETUP_FILE "$sep(\"$1\", \"$2\")"; $sep = ", "; } diff -r 04ecd79827f2 -r 3cb30e525ee9 src/HOL/Nitpick_Examples/Hotel_Nits.thy --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Tue Dec 21 12:48:47 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Tue Dec 21 14:18:45 2010 +0100 @@ -51,7 +51,8 @@ theorem safe: "s \ reach \ safe s r \ g \ isin s r \ owns s r = Some g" nitpick [card room = 1, card guest = 2, card "guest option" = 3, - card key = 4, card state = 6, expect = genuine] + card key = 4, card state = 6, show_consts, format = 2, + expect = genuine] (* nitpick [card room = 1, card guest = 2, expect = genuine] *) oops