# HG changeset patch # User wenzelm # Date 1267829492 -3600 # Node ID 768d17f541257053607b101f8776b8cec692b7fd # Parent ad7d2f9cc47dfcd4387adeda8f058960b9a8e235 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing; diff -r ad7d2f9cc47d -r 768d17f54125 src/HOL/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Mar 05 23:31:58 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Mar 05 23:51:32 2010 +0100 @@ -27,7 +27,6 @@ unit (*utility functions*) - val goal_thm_of : Proof.state -> thm val can_apply : Time.time -> (Proof.context -> int -> tactic) -> Proof.state -> bool val theorems_in_proof_term : thm -> thm list @@ -155,11 +154,9 @@ (* Mirabelle utility functions *) -val goal_thm_of = #goal o Proof.raw_goal (* FIXME ?? *) - fun can_apply time tac st = let - val {context = ctxt, facts, goal} = Proof.raw_goal st (* FIXME ?? *) + val {context = ctxt, facts, goal} = Proof.goal st val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt) in (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of @@ -201,7 +198,7 @@ NONE => [] | SOME st => if not (Toplevel.is_proof st) then [] - else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st))) + else theorems_in_proof_term (#goal (Proof.goal (Toplevel.proof_of st)))) fun get_setting settings (key, default) = the_default default (AList.lookup (op =) settings key) diff -r ad7d2f9cc47d -r 768d17f54125 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 05 23:31:58 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 05 23:51:32 2010 +0100 @@ -307,7 +307,7 @@ fun run_sh prover hard_timeout timeout dir st = let - val {context = ctxt, facts, goal} = Proof.raw_goal st (* FIXME ?? *) + val {context = ctxt, facts, goal} = Proof.goal st val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I) val ctxt' = ctxt @@ -434,39 +434,39 @@ end fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) = - let val goal = Thm.major_prem_of (#goal (Proof.raw_goal pre)) (* FIXME ?? *) in - if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal - then () else - let - val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option) - val minimize = AList.defined (op =) args minimizeK - val metis_ft = AList.defined (op =) args metis_ftK - - fun apply_metis m1 m2 = - if metis_ft - then - if not (Mirabelle.catch_result metis_tag false - (run_metis false m1 name (these (!named_thms))) id st) + let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in + if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal + then () else + let + val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option) + val minimize = AList.defined (op =) args minimizeK + val metis_ft = AList.defined (op =) args metis_ftK + + fun apply_metis m1 m2 = + if metis_ft then + if not (Mirabelle.catch_result metis_tag false + (run_metis false m1 name (these (!named_thms))) id st) + then + (Mirabelle.catch_result metis_tag false + (run_metis true m2 name (these (!named_thms))) id st; ()) + else () + else (Mirabelle.catch_result metis_tag false - (run_metis true m2 name (these (!named_thms))) id st; ()) - else () - else - (Mirabelle.catch_result metis_tag false - (run_metis false m1 name (these (!named_thms))) id st; ()) - in - change_data id (set_mini minimize); - Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st; - if is_some (!named_thms) - then - (apply_metis Unminimized UnminimizedFT; - if minimize andalso not (null (these (!named_thms))) + (run_metis false m1 name (these (!named_thms))) id st; ()) + in + change_data id (set_mini minimize); + Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st; + if is_some (!named_thms) then - (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st; - apply_metis Minimized MinimizedFT) - else ()) - else () - end + (apply_metis Unminimized UnminimizedFT; + if minimize andalso not (null (these (!named_thms))) + then + (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st; + apply_metis Minimized MinimizedFT) + else ()) + else () + end end fun invoke args = diff -r ad7d2f9cc47d -r 768d17f54125 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 05 23:31:58 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 05 23:51:32 2010 +0100 @@ -253,7 +253,7 @@ NONE => warning ("Unknown external prover: " ^ quote name) | SOME prover => let - val {context = ctxt, facts, goal} = Proof.raw_goal proof_state; (* FIXME Proof.goal *) + val {context = ctxt, facts, goal} = Proof.goal proof_state; val desc = "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); diff -r ad7d2f9cc47d -r 768d17f54125 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 05 23:31:58 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 05 23:51:32 2010 +0100 @@ -117,7 +117,7 @@ val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ") val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs val axclauses = Res_Axioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs - val {context = ctxt, facts, goal} = Proof.raw_goal state (* FIXME ?? *) + val {context = ctxt, facts, goal} = Proof.goal state val problem = {with_full_types = ! ATP_Manager.full_types, subgoal = subgoalno,