--- a/src/HOL/IsaMakefile Fri Apr 23 16:59:48 2010 +0200
+++ b/src/HOL/IsaMakefile Fri Apr 23 17:38:25 2010 +0200
@@ -283,7 +283,6 @@
$(SRC)/Provers/Arith/extract_common_term.ML \
$(SRC)/Tools/Metis/metis.ML \
Tools/ATP_Manager/atp_manager.ML \
- Tools/ATP_Manager/atp_minimal.ML \
Tools/ATP_Manager/atp_wrapper.ML \
Tools/Groebner_Basis/groebner.ML \
Tools/Groebner_Basis/misc.ML \
@@ -320,6 +319,7 @@
Tools/Sledgehammer/meson_tactic.ML \
Tools/Sledgehammer/metis_tactics.ML \
Tools/Sledgehammer/sledgehammer_fact_filter.ML \
+ Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \
Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \
Tools/Sledgehammer/sledgehammer_fol_clause.ML \
Tools/Sledgehammer/sledgehammer_hol_clause.ML \
--- a/src/HOL/Sledgehammer.thy Fri Apr 23 16:59:48 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Fri Apr 23 17:38:25 2010 +0200
@@ -19,7 +19,7 @@
("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
("Tools/ATP_Manager/atp_manager.ML")
("Tools/ATP_Manager/atp_wrapper.ML")
- ("Tools/ATP_Manager/atp_minimal.ML")
+ ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
("Tools/Sledgehammer/sledgehammer_isar.ML")
("Tools/Sledgehammer/meson_tactic.ML")
("Tools/Sledgehammer/metis_tactics.ML")
@@ -103,7 +103,7 @@
use "Tools/ATP_Manager/atp_manager.ML"
use "Tools/ATP_Manager/atp_wrapper.ML"
setup ATP_Wrapper.setup
-use "Tools/ATP_Manager/atp_minimal.ML"
+use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
use "Tools/Sledgehammer/sledgehammer_isar.ML"
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Apr 23 16:59:48 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-(* Title: HOL/Tools/ATP_Manager/atp_minimal.ML
- Author: Philipp Meyer, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-Minimization of theorem list for Metis using automatic theorem provers.
-*)
-
-signature ATP_MINIMAL =
-sig
- type params = ATP_Manager.params
- type prover = ATP_Manager.prover
- type prover_result = ATP_Manager.prover_result
-
- val minimize_theorems :
- params -> prover -> string -> int -> Proof.state -> (string * thm list) list
- -> (string * thm list) list option * string
-end;
-
-structure ATP_Minimal : ATP_MINIMAL =
-struct
-
-open Sledgehammer_Util
-open Sledgehammer_Fact_Preprocessor
-open Sledgehammer_Proof_Reconstruct
-open ATP_Manager
-
-(* Linear minimization algorithm *)
-
-fun linear_minimize test s =
- let
- fun aux [] p = p
- | aux (x :: xs) (needed, result) =
- case test (xs @ needed) of
- SOME result => aux xs (needed, result)
- | NONE => aux xs (x :: needed, result)
- in aux s end
-
-
-(* wrapper for calling external prover *)
-
-fun string_for_failure Unprovable = "Unprovable."
- | string_for_failure TimedOut = "Timed out."
- | string_for_failure OutOfResources = "Failed."
- | string_for_failure OldSpass = "Error."
- | string_for_failure MalformedOutput = "Error."
- | string_for_failure UnknownError = "Failed."
-fun string_for_outcome NONE = "Success."
- | string_for_outcome (SOME failure) = string_for_failure failure
-
-fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
- timeout subgoal state filtered_clauses name_thms_pairs =
- let
- val num_theorems = length name_thms_pairs
- val _ = priority ("Testing " ^ string_of_int num_theorems ^
- " theorem" ^ plural_s num_theorems ^ "...")
- val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
- val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
- val {context = ctxt, facts, goal} = Proof.goal state
- val problem =
- {subgoal = subgoal, goal = (ctxt, (facts, goal)),
- relevance_override = {add = [], del = [], only = false},
- axiom_clauses = SOME axclauses,
- filtered_clauses = SOME (the_default axclauses filtered_clauses)}
- in
- prover params (K "") timeout problem
- |> tap (priority o string_for_outcome o #outcome)
- end
-
-(* minimalization of thms *)
-
-fun minimize_theorems (params as {debug, minimize_timeout, isar_proof, modulus,
- sorts, ...})
- prover atp_name i state name_thms_pairs =
- let
- val msecs = Time.toMilliseconds minimize_timeout
- val n = length name_thms_pairs
- val _ =
- priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^
- " with a time limit of " ^ string_of_int msecs ^ " ms.")
- val test_thms_fun =
- sledgehammer_test_theorems params prover minimize_timeout i state
- fun test_thms filtered thms =
- case test_thms_fun filtered thms of
- (result as {outcome = NONE, ...}) => SOME result
- | _ => NONE
-
- val {context = ctxt, facts, goal} = Proof.goal state;
- val n = Logic.count_prems (prop_of goal)
- in
- (* try prove first to check result and get used theorems *)
- (case test_thms_fun NONE name_thms_pairs of
- result as {outcome = NONE, internal_thm_names, filtered_clauses, ...} =>
- let
- val used = internal_thm_names |> Vector.foldr (op ::) []
- |> sort_distinct string_ord
- val to_use =
- if length used < length name_thms_pairs then
- filter (fn (name1, _) => List.exists (curry (op =) name1) used)
- name_thms_pairs
- else name_thms_pairs
- val (min_thms, {proof, internal_thm_names, ...}) =
- linear_minimize (test_thms (SOME filtered_clauses)) to_use
- ([], result)
- val n = length min_thms
- val _ = priority (cat_lines
- ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
- in
- (SOME min_thms,
- proof_text isar_proof debug modulus sorts ctxt
- (K "", proof, internal_thm_names, goal, i) |> fst)
- end
- | {outcome = SOME TimedOut, ...} =>
- (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
- \option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ " s\").")
- | {outcome = SOME UnknownError, ...} =>
- (* Failure sometimes mean timeout, unfortunately. *)
- (NONE, "Failure: No proof was found with the current time limit. You \
- \can increase the time limit using the \"timeout\" \
- \option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ " s\").")
- | {message, ...} => (NONE, "ATP error: " ^ message))
- handle Sledgehammer_HOL_Clause.TRIVIAL =>
- (SOME [], metis_line i n [])
- | ERROR msg => (NONE, "Error: " ^ msg)
- end
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Apr 23 17:38:25 2010 +0200
@@ -0,0 +1,128 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
+ Author: Philipp Meyer, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+
+Minimization of theorem list for Metis using automatic theorem provers.
+*)
+
+signature SLEDGEHAMMER_FACT_MINIMIZER =
+sig
+ type params = ATP_Manager.params
+ type prover = ATP_Manager.prover
+ type prover_result = ATP_Manager.prover_result
+
+ val minimize_theorems :
+ params -> prover -> string -> int -> Proof.state -> (string * thm list) list
+ -> (string * thm list) list option * string
+end;
+
+structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Fact_Preprocessor
+open Sledgehammer_Proof_Reconstruct
+open ATP_Manager
+
+(* Linear minimization algorithm *)
+
+fun linear_minimize test s =
+ let
+ fun aux [] p = p
+ | aux (x :: xs) (needed, result) =
+ case test (xs @ needed) of
+ SOME result => aux xs (needed, result)
+ | NONE => aux xs (x :: needed, result)
+ in aux s end
+
+
+(* wrapper for calling external prover *)
+
+fun string_for_failure Unprovable = "Unprovable."
+ | string_for_failure TimedOut = "Timed out."
+ | string_for_failure OutOfResources = "Failed."
+ | string_for_failure OldSpass = "Error."
+ | string_for_failure MalformedOutput = "Error."
+ | string_for_failure UnknownError = "Failed."
+fun string_for_outcome NONE = "Success."
+ | string_for_outcome (SOME failure) = string_for_failure failure
+
+fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
+ timeout subgoal state filtered_clauses name_thms_pairs =
+ let
+ val num_theorems = length name_thms_pairs
+ val _ = priority ("Testing " ^ string_of_int num_theorems ^
+ " theorem" ^ plural_s num_theorems ^ "...")
+ val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
+ val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
+ val {context = ctxt, facts, goal} = Proof.goal state
+ val problem =
+ {subgoal = subgoal, goal = (ctxt, (facts, goal)),
+ relevance_override = {add = [], del = [], only = false},
+ axiom_clauses = SOME axclauses,
+ filtered_clauses = SOME (the_default axclauses filtered_clauses)}
+ in
+ prover params (K "") timeout problem
+ |> tap (priority o string_for_outcome o #outcome)
+ end
+
+(* minimalization of thms *)
+
+fun minimize_theorems (params as {debug, minimize_timeout, isar_proof, modulus,
+ sorts, ...})
+ prover atp_name i state name_thms_pairs =
+ let
+ val msecs = Time.toMilliseconds minimize_timeout
+ val n = length name_thms_pairs
+ val _ =
+ priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^
+ " with a time limit of " ^ string_of_int msecs ^ " ms.")
+ val test_thms_fun =
+ sledgehammer_test_theorems params prover minimize_timeout i state
+ fun test_thms filtered thms =
+ case test_thms_fun filtered thms of
+ (result as {outcome = NONE, ...}) => SOME result
+ | _ => NONE
+
+ val {context = ctxt, facts, goal} = Proof.goal state;
+ val n = Logic.count_prems (prop_of goal)
+ in
+ (* try prove first to check result and get used theorems *)
+ (case test_thms_fun NONE name_thms_pairs of
+ result as {outcome = NONE, internal_thm_names, filtered_clauses, ...} =>
+ let
+ val used = internal_thm_names |> Vector.foldr (op ::) []
+ |> sort_distinct string_ord
+ val to_use =
+ if length used < length name_thms_pairs then
+ filter (fn (name1, _) => List.exists (curry (op =) name1) used)
+ name_thms_pairs
+ else name_thms_pairs
+ val (min_thms, {proof, internal_thm_names, ...}) =
+ linear_minimize (test_thms (SOME filtered_clauses)) to_use
+ ([], result)
+ val n = length min_thms
+ val _ = priority (cat_lines
+ ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
+ in
+ (SOME min_thms,
+ proof_text isar_proof debug modulus sorts ctxt
+ (K "", proof, internal_thm_names, goal, i) |> fst)
+ end
+ | {outcome = SOME TimedOut, ...} =>
+ (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
+ \option (e.g., \"timeout = " ^
+ string_of_int (10 + msecs div 1000) ^ " s\").")
+ | {outcome = SOME UnknownError, ...} =>
+ (* Failure sometimes mean timeout, unfortunately. *)
+ (NONE, "Failure: No proof was found with the current time limit. You \
+ \can increase the time limit using the \"timeout\" \
+ \option (e.g., \"timeout = " ^
+ string_of_int (10 + msecs div 1000) ^ " s\").")
+ | {message, ...} => (NONE, "ATP error: " ^ message))
+ handle Sledgehammer_HOL_Clause.TRIVIAL =>
+ (SOME [], metis_line i n [])
+ | ERROR msg => (NONE, "Error: " ^ msg)
+ end
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Apr 23 16:59:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Apr 23 17:38:25 2010 +0200
@@ -1,5 +1,6 @@
-(* Title: HOL/Sledgehammer/sledgehammer_hol_clause.ML
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
Author: Jia Meng, NICTA
+ Author: Jasmin Blanchette, TU Muenchen
FOL clauses translated from HOL formulae.
*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 16:59:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 17:38:25 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Sledgehammer/sledgehammer_isar.ML
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar.ML
Author: Jasmin Blanchette, TU Muenchen
Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
@@ -19,8 +19,8 @@
open Sledgehammer_Util
open ATP_Manager
-open ATP_Minimal
open ATP_Wrapper
+open Sledgehammer_Fact_Minimizer
structure K = OuterKeyword and P = OuterParse