--- a/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 28 10:39:39 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 28 13:36:21 2010 +0200
@@ -448,13 +448,6 @@
should be considered particularly relevant. Enabling this option tends to lead
to larger problems and typically slows down the ATPs.
-\optrue{respect\_no\_atp}{ignore\_no\_atp}
-Specifies whether Sledgehammer should honor the \textit{no\_atp} attributes. The
-\textit{no\_atp} attributes marks theorems that tend to confuse ATPs, typically
-because they can lead to unsound ATP proofs \cite{boehme-nipkow-2010}. It is
-normally a good idea to leave this option enabled, unless you are debugging
-Sledgehammer.
-
\end{enum}
\subsection{Output Format}
--- a/src/HOL/IsaMakefile Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/IsaMakefile Mon Jun 28 13:36:21 2010 +0200
@@ -267,6 +267,7 @@
$(SRC)/Provers/Arith/extract_common_term.ML \
$(SRC)/Tools/cache_io.ML \
$(SRC)/Tools/Metis/metis.ML \
+ Tools/ATP_Manager/async_manager.ML \
Tools/ATP_Manager/atp_manager.ML \
Tools/ATP_Manager/atp_systems.ML \
Tools/choice_specification.ML \
@@ -313,13 +314,12 @@
Tools/Quotient/quotient_typ.ML \
Tools/recdef.ML \
Tools/semiring_normalizer.ML \
+ Tools/Sledgehammer/clausifier.ML \
Tools/Sledgehammer/meson_tactic.ML \
+ Tools/Sledgehammer/metis_clauses.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 \
Tools/Sledgehammer/sledgehammer_isar.ML \
Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
Tools/Sledgehammer/sledgehammer_tptp_format.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 28 13:36:21 2010 +0200
@@ -325,7 +325,7 @@
NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
| SOME _ => (message, SH_FAIL (time_isa, time_atp))
end
- handle Sledgehammer_HOL_Clause.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
+ handle Metis_Clauses.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
| ERROR msg => ("error: " ^ msg, SH_ERROR)
| TimeLimit.TimeOut => ("timeout", SH_ERROR)
@@ -382,7 +382,7 @@
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
let
- open Sledgehammer_Fact_Minimizer
+ open Metis_Clauses
open Sledgehammer_Isar
val thy = Proof.theory_of st
val n0 = length (these (!named_thms))
@@ -393,7 +393,8 @@
|> the_default 5
val params = default_params thy
[("atps", prover_name), ("minimize_timeout", Int.toString timeout)]
- val minimize = minimize_theorems params 1 (subgoal_count st)
+ val minimize =
+ Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st)
val _ = log separator
in
case minimize st (these (!named_thms)) of
--- a/src/HOL/Sledgehammer.thy Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Mon Jun 28 13:36:21 2010 +0200
@@ -11,19 +11,19 @@
imports Plain Hilbert_Choice
uses
"~~/src/Tools/Metis/metis.ML"
- "Tools/Sledgehammer/sledgehammer_util.ML"
- ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
- ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
- ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
- ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
+ ("Tools/Sledgehammer/clausifier.ML")
+ ("Tools/Sledgehammer/meson_tactic.ML")
+ ("Tools/Sledgehammer/metis_clauses.ML")
+ ("Tools/Sledgehammer/metis_tactics.ML")
+ ("Tools/Sledgehammer/sledgehammer_util.ML")
("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
+ ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
+ ("Tools/ATP_Manager/async_manager.ML")
("Tools/ATP_Manager/atp_manager.ML")
("Tools/ATP_Manager/atp_systems.ML")
("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
("Tools/Sledgehammer/sledgehammer_isar.ML")
- ("Tools/Sledgehammer/meson_tactic.ML")
- ("Tools/Sledgehammer/metis_tactics.ML")
begin
definition skolem_id :: "'a \<Rightarrow> 'a" where
@@ -85,32 +85,25 @@
apply (simp add: COMBC_def)
done
-
-subsection {* Setup of external ATPs *}
+use "Tools/Sledgehammer/clausifier.ML"
+setup Clausifier.setup
-use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
-use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
-setup Sledgehammer_Fact_Preprocessor.setup
-use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
-use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
+use "Tools/Sledgehammer/meson_tactic.ML"
+setup Meson_Tactic.setup
+
+use "Tools/Sledgehammer/metis_clauses.ML"
+use "Tools/Sledgehammer/metis_tactics.ML"
+
+use "Tools/Sledgehammer/sledgehammer_util.ML"
use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
+use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
+use "Tools/ATP_Manager/async_manager.ML"
use "Tools/ATP_Manager/atp_manager.ML"
use "Tools/ATP_Manager/atp_systems.ML"
setup ATP_Systems.setup
use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
use "Tools/Sledgehammer/sledgehammer_isar.ML"
-
-
-subsection {* The MESON prover *}
-
-use "Tools/Sledgehammer/meson_tactic.ML"
-setup Meson_Tactic.setup
-
-
-subsection {* The Metis prover *}
-
-use "Tools/Sledgehammer/metis_tactics.ML"
setup Metis_Tactics.setup
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/async_manager.ML Mon Jun 28 13:36:21 2010 +0200
@@ -0,0 +1,241 @@
+(* Title: HOL/Tools/ATP_Manager/async_manager.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
+
+Central manager for asynchronous diagnosis tool threads.
+*)
+
+signature ASYNC_MANAGER =
+sig
+ val launch :
+ string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
+ -> unit
+ val kill_threads : string -> string -> unit
+ val running_threads : string -> string -> unit
+ val thread_messages : string -> string -> int option -> unit
+end;
+
+structure Async_Manager : ASYNC_MANAGER =
+struct
+
+(** preferences **)
+
+val message_store_limit = 20;
+val message_display_limit = 5;
+
+
+(** thread management **)
+
+(* data structures over threads *)
+
+structure Thread_Heap = Heap
+(
+ type elem = Time.time * Thread.thread;
+ fun ord ((a, _), (b, _)) = Time.compare (a, b);
+);
+
+fun lookup_thread xs = AList.lookup Thread.equal xs;
+fun delete_thread xs = AList.delete Thread.equal xs;
+fun update_thread xs = AList.update Thread.equal xs;
+
+
+(* state of thread manager *)
+
+type state =
+ {manager: Thread.thread option,
+ timeout_heap: Thread_Heap.T,
+ active: (Thread.thread * (string * Time.time * Time.time * string)) list,
+ canceling: (Thread.thread * (string * Time.time * string)) list,
+ messages: (string * string) list,
+ store: (string * string) list}
+
+fun make_state manager timeout_heap active canceling messages store : state =
+ {manager = manager, timeout_heap = timeout_heap, active = active,
+ canceling = canceling, messages = messages, store = store}
+
+val global_state = Synchronized.var "async_manager"
+ (make_state NONE Thread_Heap.empty [] [] [] []);
+
+
+(* unregister thread *)
+
+fun unregister verbose message thread =
+ Synchronized.change global_state
+ (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
+ (case lookup_thread active thread of
+ SOME (tool, birth_time, _, desc) =>
+ let
+ val active' = delete_thread thread active;
+ val now = Time.now ()
+ val canceling' = (thread, (tool, now, desc)) :: canceling
+ val message' =
+ desc ^ "\n" ^ message ^
+ (if verbose then
+ "Total time: " ^ Int.toString (Time.toMilliseconds
+ (Time.- (now, birth_time))) ^ " ms.\n"
+ else
+ "")
+ val messages' = (tool, message') :: messages;
+ val store' = (tool, message') ::
+ (if length store <= message_store_limit then store
+ else #1 (chop message_store_limit store));
+ in make_state manager timeout_heap active' canceling' messages' store' end
+ | NONE => state));
+
+
+(* main manager thread -- only one may exist *)
+
+val min_wait_time = Time.fromMilliseconds 300;
+val max_wait_time = Time.fromSeconds 10;
+
+fun replace_all bef aft =
+ let
+ fun aux seen "" = String.implode (rev seen)
+ | aux seen s =
+ if String.isPrefix bef s then
+ aux seen "" ^ aft ^ aux [] (unprefix bef s)
+ else
+ aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
+ in aux [] end
+
+(* This is a workaround for Proof General's off-by-a-few sendback display bug,
+ whereby "pr" in "proof" is not highlighted. *)
+val break_into_chunks =
+ maps (space_explode "\000" o replace_all "\n\n" "\000" o snd)
+
+fun print_new_messages () =
+ case Synchronized.change_result global_state
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ (messages, make_state manager timeout_heap active canceling []
+ store)) of
+ [] => ()
+ | msgs as (tool, _) :: _ =>
+ let val ss = break_into_chunks msgs in
+ List.app priority (tool ^ ": " ^ hd ss :: tl ss)
+ end
+
+fun check_thread_manager verbose = Synchronized.change global_state
+ (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
+ if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
+ else let val manager = SOME (Toplevel.thread false (fn () =>
+ let
+ fun time_limit timeout_heap =
+ (case try Thread_Heap.min timeout_heap of
+ NONE => Time.+ (Time.now (), max_wait_time)
+ | SOME (time, _) => time);
+
+ (*action: find threads whose timeout is reached, and interrupt canceling threads*)
+ fun action {manager, timeout_heap, active, canceling, messages, store} =
+ let val (timeout_threads, timeout_heap') =
+ Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
+ in
+ if null timeout_threads andalso null canceling then
+ NONE
+ else
+ let
+ val _ = List.app (Simple_Thread.interrupt o #1) canceling
+ val canceling' = filter (Thread.isActive o #1) canceling
+ val state' = make_state manager timeout_heap' active canceling' messages store;
+ in SOME (map #2 timeout_threads, state') end
+ end;
+ in
+ while Synchronized.change_result global_state
+ (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
+ if null active andalso null canceling andalso null messages
+ then (false, make_state NONE timeout_heap active canceling messages store)
+ else (true, state))
+ do
+ (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
+ |> these
+ |> List.app (unregister verbose "Timed out.\n");
+ print_new_messages ();
+ (*give threads some time to respond to interrupt*)
+ OS.Process.sleep min_wait_time)
+ end))
+ in make_state manager timeout_heap active canceling messages store end)
+
+
+(* register thread *)
+
+fun register tool verbose birth_time death_time desc thread =
+ (Synchronized.change global_state
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ let
+ val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
+ val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
+ val state' = make_state manager timeout_heap' active' canceling messages store;
+ in state' end);
+ check_thread_manager verbose);
+
+
+fun launch tool verbose birth_time death_time desc f =
+ (Toplevel.thread true
+ (fn () =>
+ let
+ val self = Thread.self ()
+ val _ = register tool verbose birth_time death_time desc self
+ val message = f ()
+ in unregister verbose message self end);
+ ())
+
+
+(** user commands **)
+
+(* kill threads *)
+
+fun kill_threads tool workers = Synchronized.change global_state
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ let
+ val killing =
+ map_filter (fn (th, (tool', _, _, desc)) =>
+ if tool' = tool then SOME (th, (tool', Time.now (), desc))
+ else NONE) active
+ val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
+ val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
+ in state' end);
+
+
+(* running threads *)
+
+fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
+
+fun running_threads tool workers =
+ let
+ val {active, canceling, ...} = Synchronized.value global_state;
+
+ val now = Time.now ();
+ fun running_info (_, (tool', birth_time, death_time, desc)) =
+ if tool' = tool then
+ SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
+ seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
+ else
+ NONE
+ fun canceling_info (_, (tool', death_time, desc)) =
+ if tool' = tool then
+ SOME ("Trying to interrupt thread since " ^
+ seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
+ else
+ NONE
+ val running =
+ case map_filter running_info active of
+ [] => ["No " ^ workers ^ " running."]
+ | ss => "Running " ^ workers ^ ":" :: ss
+ val interrupting =
+ case map_filter canceling_info canceling of
+ [] => []
+ | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
+ in priority (space_implode "\n\n" (running @ interrupting)) end
+
+fun thread_messages tool worker opt_limit =
+ let
+ val limit = the_default message_display_limit opt_limit;
+ val tool_store = Synchronized.value global_state
+ |> #store |> filter (curry (op =) tool o fst)
+ val header =
+ "Recent " ^ worker ^ " messages" ^
+ (if length tool_store <= limit then ":"
+ else " (" ^ string_of_int limit ^ " displayed):");
+ in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end
+
+end;
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jun 28 13:36:21 2010 +0200
@@ -8,8 +8,8 @@
signature ATP_MANAGER =
sig
- type name_pool = Sledgehammer_FOL_Clause.name_pool
- type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
+ type cnf_thm = Clausifier.cnf_thm
+ type name_pool = Metis_Clauses.name_pool
type relevance_override = Sledgehammer_Fact_Filter.relevance_override
type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
type params =
@@ -19,7 +19,6 @@
atps: string list,
full_types: bool,
explicit_apply: bool,
- respect_no_atp: bool,
relevance_threshold: real,
relevance_convergence: real,
theory_relevant: bool option,
@@ -57,19 +56,26 @@
val add_prover: string * prover -> theory -> theory
val get_prover: theory -> string -> prover
val available_atps: theory -> unit
- val start_prover_thread:
- params -> Time.time -> Time.time -> int -> int -> relevance_override
- -> (string -> minimize_command) -> Proof.state -> string -> unit
+ val start_prover_thread :
+ params -> int -> int -> relevance_override -> (string -> minimize_command)
+ -> Proof.state -> string -> unit
end;
structure ATP_Manager : ATP_MANAGER =
struct
-open Sledgehammer_Util
+open Metis_Clauses
open Sledgehammer_Fact_Filter
-open Sledgehammer_HOL_Clause
open Sledgehammer_Proof_Reconstruct
+(** The Sledgehammer **)
+
+val das_Tool = "Sledgehammer"
+
+fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
+fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
+val messages = Async_Manager.thread_messages das_Tool "ATP"
+
(** problems, results, provers, etc. **)
type params =
@@ -79,7 +85,6 @@
atps: string list,
full_types: bool,
explicit_apply: bool,
- respect_no_atp: bool,
relevance_threshold: real,
relevance_convergence: real,
theory_relevant: bool option,
@@ -115,221 +120,24 @@
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
-
-(** preferences **)
-
-val message_store_limit = 20;
-val message_display_limit = 5;
-
-
-(** thread management **)
-
-(* data structures over threads *)
-
-structure Thread_Heap = Heap
-(
- type elem = Time.time * Thread.thread;
- fun ord ((a, _), (b, _)) = Time.compare (a, b);
-);
-
-fun lookup_thread xs = AList.lookup Thread.equal xs;
-fun delete_thread xs = AList.delete Thread.equal xs;
-fun update_thread xs = AList.update Thread.equal xs;
-
-
-(* state of thread manager *)
-
-type state =
- {manager: Thread.thread option,
- timeout_heap: Thread_Heap.T,
- active: (Thread.thread * (Time.time * Time.time * string)) list,
- cancelling: (Thread.thread * (Time.time * string)) list,
- messages: string list,
- store: string list};
-
-fun make_state manager timeout_heap active cancelling messages store : state =
- {manager = manager, timeout_heap = timeout_heap, active = active,
- cancelling = cancelling, messages = messages, store = store};
-
-val global_state = Synchronized.var "atp_manager"
- (make_state NONE Thread_Heap.empty [] [] [] []);
-
-
-(* unregister ATP thread *)
-
-fun unregister ({verbose, ...} : params) message thread =
- Synchronized.change global_state
- (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
- (case lookup_thread active thread of
- SOME (birth_time, _, desc) =>
- let
- val active' = delete_thread thread active;
- val now = Time.now ()
- val cancelling' = (thread, (now, desc)) :: cancelling;
- val message' =
- desc ^ "\n" ^ message ^
- (if verbose then
- "Total time: " ^ Int.toString (Time.toMilliseconds
- (Time.- (now, birth_time))) ^ " ms.\n"
- else
- "")
- val messages' = message' :: messages;
- val store' = message' ::
- (if length store <= message_store_limit then store
- else #1 (chop message_store_limit store));
- in make_state manager timeout_heap active' cancelling' messages' store' end
- | NONE => state));
-
-
-(* main manager thread -- only one may exist *)
-
-val min_wait_time = Time.fromMilliseconds 300;
-val max_wait_time = Time.fromSeconds 10;
-
-(* This is a workaround for Proof General's off-by-a-few sendback display bug,
- whereby "pr" in "proof" is not highlighted. *)
-val break_into_chunks =
- map (replace_all "\n\n" "\000") #> maps (space_explode "\000")
-
-fun print_new_messages () =
- case Synchronized.change_result global_state
- (fn {manager, timeout_heap, active, cancelling, messages, store} =>
- (messages, make_state manager timeout_heap active cancelling []
- store)) of
- [] => ()
- | msgs =>
- msgs |> break_into_chunks
- |> (fn msg :: msgs => "Sledgehammer: " ^ msg :: msgs)
- |> List.app priority
-
-fun check_thread_manager params = Synchronized.change global_state
- (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
- if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
- else let val manager = SOME (Toplevel.thread false (fn () =>
- let
- fun time_limit timeout_heap =
- (case try Thread_Heap.min timeout_heap of
- NONE => Time.+ (Time.now (), max_wait_time)
- | SOME (time, _) => time);
-
- (*action: find threads whose timeout is reached, and interrupt cancelling threads*)
- fun action {manager, timeout_heap, active, cancelling, messages, store} =
- let val (timeout_threads, timeout_heap') =
- Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
- in
- if null timeout_threads andalso null cancelling
- then NONE
- else
- let
- val _ = List.app (Simple_Thread.interrupt o #1) cancelling;
- val cancelling' = filter (Thread.isActive o #1) cancelling;
- val state' = make_state manager timeout_heap' active cancelling' messages store;
- in SOME (map #2 timeout_threads, state') end
- end;
- in
- while Synchronized.change_result global_state
- (fn state as {timeout_heap, active, cancelling, messages, store, ...} =>
- if null active andalso null cancelling andalso null messages
- then (false, make_state NONE timeout_heap active cancelling messages store)
- else (true, state))
- do
- (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
- |> these
- |> List.app (unregister params "Timed out.\n");
- print_new_messages ();
- (*give threads some time to respond to interrupt*)
- OS.Process.sleep min_wait_time)
- end))
- in make_state manager timeout_heap active cancelling messages store end);
-
-
-(* register ATP thread *)
-
-fun register params birth_time death_time (thread, desc) =
- (Synchronized.change global_state
- (fn {manager, timeout_heap, active, cancelling, messages, store} =>
- let
- val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
- val active' = update_thread (thread, (birth_time, death_time, desc)) active;
- val state' = make_state manager timeout_heap' active' cancelling messages store;
- in state' end);
- check_thread_manager params);
-
-
-
-(** user commands **)
-
-(* kill ATPs *)
-
-fun kill_atps () = Synchronized.change global_state
- (fn {manager, timeout_heap, active, cancelling, messages, store} =>
- let
- val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active;
- val state' = make_state manager timeout_heap [] (killing @ cancelling) messages store;
- val _ = if null active then ()
- else priority "Killed active Sledgehammer threads."
- in state' end);
-
-
-(* running_atps *)
-
-fun seconds time = string_of_int (Time.toSeconds time) ^ "s";
-
-fun running_atps () =
- let
- val {active, cancelling, ...} = Synchronized.value global_state;
-
- val now = Time.now ();
- fun running_info (_, (birth_time, death_time, desc)) =
- "Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
- seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc;
- fun cancelling_info (_, (deadth_time, desc)) =
- "Trying to interrupt thread since " ^ seconds (Time.- (now, deadth_time)) ^ ":\n" ^ desc;
-
- val running =
- if null active then "No ATPs running."
- else space_implode "\n\n" ("Running ATPs:" :: map running_info active);
- val interrupting =
- if null cancelling then ""
- else
- space_implode "\n\n"
- ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling);
-
- in priority (running ^ "\n" ^ interrupting) end;
-
-fun messages opt_limit =
- let
- val limit = the_default message_display_limit opt_limit;
- val {store, ...} = Synchronized.value global_state;
- val header =
- "Recent ATP messages" ^
- (if length store <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
- in List.app priority (header :: break_into_chunks (#1 (chop limit store))) end
-
-
-(** The Sledgehammer **)
-
(* named provers *)
-fun err_dup_prover name = error ("Duplicate prover: " ^ quote name ^ ".");
-
structure Data = Theory_Data
(
type T = (prover * stamp) Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data : T = Symtab.merge (eq_snd op =) data
- handle Symtab.DUP name => err_dup_prover name;
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
);
fun add_prover (name, prover) thy =
Data.map (Symtab.update_new (name, (prover, stamp ()))) thy
- handle Symtab.DUP name => err_dup_prover name;
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
fun get_prover thy name =
- case Symtab.lookup (Data.get thy) name of
- SOME (prover, _) => prover
- | NONE => error ("Unknown ATP: " ^ name)
+ the (Symtab.lookup (Data.get thy) name) |> fst
+ handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
fun available_atps thy =
priority ("Available ATPs: " ^
@@ -338,28 +146,29 @@
(* start prover thread *)
-fun start_prover_thread (params as {full_types, timeout, ...}) birth_time
- death_time i n relevance_override minimize_command
- proof_state name =
+fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
+ relevance_override minimize_command proof_state name =
let
+ val birth_time = Time.now ()
+ val death_time = Time.+ (birth_time, timeout)
val prover = get_prover (Proof.theory_of proof_state) name
val {context = ctxt, facts, goal} = Proof.goal proof_state;
val desc =
"ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
- val _ = Toplevel.thread true (fn () =>
- let
- val _ = register params birth_time death_time (Thread.self (), desc)
- val problem =
- {subgoal = i, goal = (ctxt, (facts, goal)),
- relevance_override = relevance_override, axiom_clauses = NONE,
- filtered_clauses = NONE}
- val message =
- #message (prover params (minimize_command name) timeout problem)
- handle TRIVIAL () => metis_line full_types i n []
- | ERROR message => "Error: " ^ message ^ "\n"
- val _ = unregister params message (Thread.self ());
- in () end)
- in () end
+ in
+ Async_Manager.launch das_Tool verbose birth_time death_time desc
+ (fn () =>
+ let
+ val problem =
+ {subgoal = i, goal = (ctxt, (facts, goal)),
+ relevance_override = relevance_override, axiom_clauses = NONE,
+ filtered_clauses = NONE}
+ in
+ prover params (minimize_command name) timeout problem |> #message
+ handle TRIVIAL () => metis_line full_types i n []
+ | ERROR message => "Error: " ^ message ^ "\n"
+ end)
+ end
end;
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 28 13:36:21 2010 +0200
@@ -22,12 +22,12 @@
structure ATP_Systems : ATP_SYSTEMS =
struct
+open Clausifier
+open Metis_Clauses
open Sledgehammer_Util
-open Sledgehammer_Fact_Preprocessor
-open Sledgehammer_HOL_Clause
open Sledgehammer_Fact_Filter
+open Sledgehammer_TPTP_Format
open Sledgehammer_Proof_Reconstruct
-open Sledgehammer_TPTP_Format
open ATP_Manager
(** generic ATP **)
@@ -126,9 +126,9 @@
fun generic_tptp_prover
(name, {home_var, executable, arguments, proof_delims, known_failures,
max_axiom_clauses, prefers_theory_relevant})
- ({debug, overlord, full_types, explicit_apply, respect_no_atp,
- relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, isar_proof, isar_shrink_factor, ...} : params)
+ ({debug, overlord, full_types, explicit_apply, relevance_threshold,
+ relevance_convergence, theory_relevant, defs_relevant, isar_proof,
+ isar_shrink_factor, ...} : params)
minimize_command timeout
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
: problem) =
@@ -140,7 +140,7 @@
val goal_cls = List.concat goal_clss
val the_filtered_clauses =
(case filtered_clauses of
- NONE => relevant_facts full_types respect_no_atp relevance_threshold
+ NONE => relevant_facts full_types relevance_threshold
relevance_convergence defs_relevant max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant)
relevance_override goal goal_cls
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Jun 28 13:36:21 2010 +0200
@@ -0,0 +1,571 @@
+(* Title: HOL/Tools/Sledgehammer/clausifier.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
+
+Transformation of axiom rules (elim/intro/etc) into CNF forms.
+*)
+
+signature CLAUSIFIER =
+sig
+ type cnf_thm = thm * ((string * int) * thm)
+
+ val sledgehammer_prefix: string
+ val chained_prefix: string
+ val trace: bool Unsynchronized.ref
+ val trace_msg: (unit -> string) -> unit
+ val name_thms_pair_from_ref :
+ Proof.context -> thm list -> Facts.ref -> string * thm list
+ val skolem_theory_name: string
+ val skolem_prefix: string
+ val skolem_infix: string
+ val is_skolem_const_name: string -> bool
+ val num_type_args: theory -> string -> int
+ val cnf_axiom: theory -> thm -> thm list
+ val multi_base_blacklist: string list
+ val is_theorem_bad_for_atps: thm -> bool
+ val type_has_topsort: typ -> bool
+ val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
+ val saturate_cache: theory -> theory option
+ val auto_saturate_cache: bool Unsynchronized.ref
+ val neg_clausify: thm -> thm list
+ val neg_conjecture_clauses:
+ Proof.context -> thm -> int -> thm list list * (string * typ) list
+ val setup: theory -> theory
+end;
+
+structure Clausifier : CLAUSIFIER =
+struct
+
+type cnf_thm = thm * ((string * int) * thm)
+
+val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
+
+(* Used to label theorems chained into the goal. *)
+val chained_prefix = sledgehammer_prefix ^ "chained_"
+
+val trace = Unsynchronized.ref false;
+fun trace_msg msg = if !trace then tracing (msg ()) else ();
+
+fun name_thms_pair_from_ref ctxt chained_ths xref =
+ let
+ val ths = ProofContext.get_fact ctxt xref
+ val name = Facts.string_of_ref xref
+ |> forall (member Thm.eq_thm chained_ths) ths
+ ? prefix chained_prefix
+ in (name, ths) end
+
+val skolem_theory_name = sledgehammer_prefix ^ "Sko"
+val skolem_prefix = "sko_"
+val skolem_infix = "$"
+
+val type_has_topsort = Term.exists_subtype
+ (fn TFree (_, []) => true
+ | TVar (_, []) => true
+ | _ => false);
+
+
+(**** Transformation of Elimination Rules into First-Order Formulas****)
+
+val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
+val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
+
+(*Converts an elim-rule into an equivalent theorem that does not have the
+ predicate variable. Leaves other theorems unchanged. We simply instantiate the
+ conclusion variable to False.*)
+fun transform_elim th =
+ case concl_of th of (*conclusion variable*)
+ @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
+ Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
+ | v as Var(_, @{typ prop}) =>
+ Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
+ | _ => th;
+
+(*To enforce single-threading*)
+exception Clausify_failure of theory;
+
+
+(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
+
+(*Keep the full complexity of the original name*)
+fun flatten_name s = space_implode "_X" (Long_Name.explode s);
+
+fun skolem_name thm_name j var_name =
+ skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^
+ skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
+
+(* Hack: Could return false positives (e.g., a user happens to declare a
+ constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
+val is_skolem_const_name =
+ Long_Name.base_name
+ #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
+
+(* The number of type arguments of a constant, zero if it's monomorphic. For
+ (instances of) Skolem pseudoconstants, this information is encoded in the
+ constant name. *)
+fun num_type_args thy s =
+ if String.isPrefix skolem_theory_name s then
+ s |> unprefix skolem_theory_name
+ |> space_explode skolem_infix |> hd
+ |> space_explode "_" |> List.last |> Int.fromString |> the
+ else
+ (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
+
+fun rhs_extra_types lhsT rhs =
+ let val lhs_vars = Term.add_tfreesT lhsT []
+ fun add_new_TFrees (TFree v) =
+ if member (op =) lhs_vars v then I else insert (op =) (TFree v)
+ | add_new_TFrees _ = I
+ val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
+ in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
+
+fun skolem_type_and_args bound_T body =
+ let
+ val args1 = OldTerm.term_frees body
+ val Ts1 = map type_of args1
+ val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body
+ val args2 = map (fn T => Free (gensym "vsk", T)) Ts2
+ in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end
+
+(* Traverse a theorem, declaring Skolem function definitions. String "s" is the
+ suggested prefix for the Skolem constants. *)
+fun declare_skolem_funs s th thy =
+ let
+ val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
+ fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p)))
+ (axs, thy) =
+ (*Existential: declare a Skolem function, then insert into body and continue*)
+ let
+ val id = skolem_name s (Unsynchronized.inc skolem_count) s'
+ val (cT, args) = skolem_type_and_args T body
+ val rhs = list_abs_free (map dest_Free args,
+ HOLogic.choice_const T $ body)
+ (*Forms a lambda-abstraction over the formal parameters*)
+ val (c, thy) =
+ Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
+ val cdef = id ^ "_def"
+ val ((_, ax), thy) =
+ Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
+ val ax' = Drule.export_without_context ax
+ in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
+ | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
+ (*Universal quant: insert a free variable into body and continue*)
+ let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
+ in dec_sko (subst_bound (Free (fname, T), p)) thx end
+ | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
+ | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
+ | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
+ | dec_sko _ thx = thx
+ in dec_sko (prop_of th) ([], thy) end
+
+fun mk_skolem_id t =
+ let val T = fastype_of t in
+ Const (@{const_name skolem_id}, T --> T) $ t
+ end
+
+fun quasi_beta_eta_contract (Abs (s, T, t')) =
+ Abs (s, T, quasi_beta_eta_contract t')
+ | quasi_beta_eta_contract t = Envir.beta_eta_contract t
+
+(*Traverse a theorem, accumulating Skolem function definitions.*)
+fun assume_skolem_funs s th =
+ let
+ val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
+ fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs =
+ (*Existential: declare a Skolem function, then insert into body and continue*)
+ let
+ val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
+ val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*)
+ val Ts = map type_of args
+ val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
+ val id = skolem_name s (Unsynchronized.inc skolem_count) s'
+ val c = Free (id, cT) (* FIXME: needed? ### *)
+ (* Forms a lambda-abstraction over the formal parameters *)
+ val rhs =
+ list_abs_free (map dest_Free args,
+ HOLogic.choice_const T
+ $ quasi_beta_eta_contract body)
+ |> mk_skolem_id
+ val def = Logic.mk_equals (c, rhs)
+ val comb = list_comb (rhs, args)
+ in dec_sko (subst_bound (comb, p)) (def :: defs) end
+ | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
+ (*Universal quant: insert a free variable into body and continue*)
+ let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
+ in dec_sko (subst_bound (Free(fname,T), p)) defs end
+ | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
+ | dec_sko _ defs = defs
+ in dec_sko (prop_of th) [] end;
+
+
+(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
+
+(*Returns the vars of a theorem*)
+fun vars_of_thm th =
+ map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
+
+val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
+
+(* Removes the lambdas from an equation of the form t = (%x. u). *)
+fun extensionalize th =
+ case prop_of th of
+ _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
+ $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
+ | _ => th
+
+fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
+ | is_quasi_lambda_free (t1 $ t2) =
+ is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
+ | is_quasi_lambda_free (Abs _) = false
+ | is_quasi_lambda_free _ = true
+
+val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
+val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
+val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
+
+(*FIXME: requires more use of cterm constructors*)
+fun abstract ct =
+ let
+ val thy = theory_of_cterm ct
+ val Abs(x,_,body) = term_of ct
+ val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
+ val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
+ fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
+ in
+ case body of
+ Const _ => makeK()
+ | Free _ => makeK()
+ | Var _ => makeK() (*though Var isn't expected*)
+ | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
+ | rator$rand =>
+ if loose_bvar1 (rator,0) then (*C or S*)
+ if loose_bvar1 (rand,0) then (*S*)
+ let val crator = cterm_of thy (Abs(x,xT,rator))
+ val crand = cterm_of thy (Abs(x,xT,rand))
+ val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
+ in
+ Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
+ end
+ else (*C*)
+ let val crator = cterm_of thy (Abs(x,xT,rator))
+ val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
+ in
+ Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
+ end
+ else if loose_bvar1 (rand,0) then (*B or eta*)
+ if rand = Bound 0 then Thm.eta_conversion ct
+ else (*B*)
+ let val crand = cterm_of thy (Abs(x,xT,rand))
+ val crator = cterm_of thy rator
+ val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
+ in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
+ else makeK()
+ | _ => raise Fail "abstract: Bad term"
+ end;
+
+(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
+fun do_introduce_combinators ct =
+ if is_quasi_lambda_free (term_of ct) then
+ Thm.reflexive ct
+ else case term_of ct of
+ Abs _ =>
+ let
+ val (cv, cta) = Thm.dest_abs NONE ct
+ val (v, _) = dest_Free (term_of cv)
+ val u_th = do_introduce_combinators cta
+ val cu = Thm.rhs_of u_th
+ val comb_eq = abstract (Thm.cabs cv cu)
+ in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
+ | _ $ _ =>
+ let val (ct1, ct2) = Thm.dest_comb ct in
+ Thm.combination (do_introduce_combinators ct1)
+ (do_introduce_combinators ct2)
+ end
+
+fun introduce_combinators th =
+ if is_quasi_lambda_free (prop_of th) then
+ th
+ else
+ let
+ val th = Drule.eta_contraction_rule th
+ val eqth = do_introduce_combinators (cprop_of th)
+ in Thm.equal_elim eqth th end
+ handle THM (msg, _, _) =>
+ (warning ("Error in the combinator translation of " ^
+ Display.string_of_thm_without_context th ^
+ "\nException message: " ^ msg ^ ".");
+ (* A type variable of sort "{}" will make abstraction fail. *)
+ TrueI)
+
+(*cterms are used throughout for efficiency*)
+val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
+
+(*cterm version of mk_cTrueprop*)
+fun c_mkTrueprop A = Thm.capply cTrueprop A;
+
+(*Given an abstraction over n variables, replace the bound variables by free
+ ones. Return the body, along with the list of free variables.*)
+fun c_variant_abs_multi (ct0, vars) =
+ let val (cv,ct) = Thm.dest_abs NONE ct0
+ in c_variant_abs_multi (ct, cv::vars) end
+ handle CTERM _ => (ct0, rev vars);
+
+(*Given the definition of a Skolem function, return a theorem to replace
+ an existential formula by a use of that function.
+ Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
+fun skolem_theorem_of_def inline def =
+ let
+ val (c, rhs) = def |> Drule.legacy_freeze_thaw |> #1 |> cprop_of
+ |> Thm.dest_equals
+ val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
+ val (ch, frees) = c_variant_abs_multi (rhs', [])
+ val (chilbert, cabs) = ch |> Thm.dest_comb
+ val thy = Thm.theory_of_cterm chilbert
+ val t = Thm.term_of chilbert
+ val T =
+ case t of
+ Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
+ | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t])
+ val cex = Thm.cterm_of thy (HOLogic.exists_const T)
+ val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
+ and conc =
+ Drule.list_comb (if inline then rhs else c, frees)
+ |> Drule.beta_conv cabs |> c_mkTrueprop
+ fun tacf [prem] =
+ (if inline then rewrite_goals_tac @{thms skolem_id_def_raw}
+ else rewrite_goals_tac [def])
+ THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw})
+ RS @{thm someI_ex}) 1
+ in Goal.prove_internal [ex_tm] conc tacf
+ |> forall_intr_list frees
+ |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
+ |> Thm.varifyT_global
+ end;
+
+
+(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
+fun to_nnf th ctxt0 =
+ let val th1 = th |> transform_elim |> zero_var_indexes
+ val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
+ val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
+ |> extensionalize
+ |> Meson.make_nnf ctxt
+ in (th3, ctxt) end;
+
+(*Generate Skolem functions for a theorem supplied in nnf*)
+fun skolem_theorems_of_assume s th =
+ map (skolem_theorem_of_def true o Thm.assume o cterm_of (theory_of_thm th))
+ (assume_skolem_funs s th)
+
+
+(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
+
+val max_lambda_nesting = 3
+
+fun term_has_too_many_lambdas max (t1 $ t2) =
+ exists (term_has_too_many_lambdas max) [t1, t2]
+ | term_has_too_many_lambdas max (Abs (_, _, t)) =
+ max = 0 orelse term_has_too_many_lambdas (max - 1) t
+ | term_has_too_many_lambdas _ _ = false
+
+fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
+
+(* Don't count nested lambdas at the level of formulas, since they are
+ quantifiers. *)
+fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
+ formula_has_too_many_lambdas (T :: Ts) t
+ | formula_has_too_many_lambdas Ts t =
+ if is_formula_type (fastype_of1 (Ts, t)) then
+ exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
+ else
+ term_has_too_many_lambdas max_lambda_nesting t
+
+(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
+ was 11. *)
+val max_apply_depth = 15
+
+fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
+ | apply_depth (Abs (_, _, t)) = apply_depth t
+ | apply_depth _ = 0
+
+fun is_formula_too_complex t =
+ apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
+ formula_has_too_many_lambdas [] t
+
+fun is_strange_thm th =
+ case head_of (concl_of th) of
+ Const (a, _) => (a <> @{const_name Trueprop} andalso
+ a <> @{const_name "=="})
+ | _ => false;
+
+fun is_theorem_bad_for_atps thm =
+ let val t = prop_of thm in
+ is_formula_too_complex t orelse exists_type type_has_topsort t orelse
+ is_strange_thm thm
+ end
+
+(* FIXME: put other record thms here, or declare as "no_atp" *)
+val multi_base_blacklist =
+ ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
+ "split_asm", "cases", "ext_cases"];
+
+fun fake_name th =
+ if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
+ else gensym "unknown_thm_";
+
+(*Skolemize a named theorem, with Skolem functions as additional premises.*)
+fun skolemize_theorem s th =
+ if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
+ is_theorem_bad_for_atps th then
+ []
+ else
+ let
+ val ctxt0 = Variable.global_thm_context th
+ val (nnfth, ctxt) = to_nnf th ctxt0
+ val defs = skolem_theorems_of_assume s nnfth
+ val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
+ in
+ cnfs |> map introduce_combinators
+ |> Variable.export ctxt ctxt0
+ |> Meson.finish_cnf
+ end
+ handle THM _ => []
+
+(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
+ Skolem functions.*)
+structure ThmCache = Theory_Data
+(
+ type T = thm list Thmtab.table * unit Symtab.table;
+ val empty = (Thmtab.empty, Symtab.empty);
+ val extend = I;
+ fun merge ((cache1, seen1), (cache2, seen2)) : T =
+ (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
+);
+
+val lookup_cache = Thmtab.lookup o #1 o ThmCache.get;
+val already_seen = Symtab.defined o #2 o ThmCache.get;
+
+val update_cache = ThmCache.map o apfst o Thmtab.update;
+fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ())));
+
+(* Convert Isabelle theorems into axiom clauses. *)
+fun cnf_axiom thy th0 =
+ let val th = Thm.transfer thy th0 in
+ case lookup_cache thy th of
+ SOME cls => cls
+ | NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th)
+ end;
+
+
+(**** Translate a set of theorems into CNF ****)
+
+(*The combination of rev and tail recursion preserves the original order*)
+fun cnf_rules_pairs thy =
+ let
+ fun do_one _ [] = []
+ | do_one ((name, k), th) (cls :: clss) =
+ (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss
+ fun do_all pairs [] = pairs
+ | do_all pairs ((name, th) :: ths) =
+ let
+ val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
+ handle THM _ => []
+ in do_all (new_pairs @ pairs) ths end
+ in do_all [] o rev end
+
+
+(**** Convert all facts of the theory into FOL or HOL clauses ****)
+
+local
+
+fun skolem_def (name, th) thy =
+ let val ctxt0 = Variable.global_thm_context th in
+ case try (to_nnf th) ctxt0 of
+ NONE => (NONE, thy)
+ | SOME (nnfth, ctxt) =>
+ let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy
+ in (SOME (th, ctxt0, ctxt, nnfth, defs), thy') end
+ end;
+
+fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) =
+ let
+ val (cnfs, ctxt) =
+ Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt
+ val cnfs' = cnfs
+ |> map introduce_combinators
+ |> Variable.export ctxt ctxt0
+ |> Meson.finish_cnf
+ |> map Thm.close_derivation;
+ in (th, cnfs') end;
+
+in
+
+fun saturate_cache thy =
+ let
+ val facts = PureThy.facts_of thy;
+ val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) =>
+ if Facts.is_concealed facts name orelse already_seen thy name then I
+ else cons (name, ths));
+ val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
+ if member (op =) multi_base_blacklist (Long_Name.base_name name) then
+ I
+ else
+ fold_index (fn (i, th) =>
+ if is_theorem_bad_for_atps th orelse
+ is_some (lookup_cache thy th) then
+ I
+ else
+ cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
+ in
+ if null new_facts then
+ NONE
+ else
+ let
+ val (defs, thy') = thy
+ |> fold (mark_seen o #1) new_facts
+ |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
+ |>> map_filter I;
+ val cache_entries = Par_List.map skolem_cnfs defs;
+ in SOME (fold update_cache cache_entries thy') end
+ end;
+
+end;
+
+(* For emergency use where the Skolem cache causes problems. *)
+val auto_saturate_cache = Unsynchronized.ref true
+
+fun conditionally_saturate_cache thy =
+ if !auto_saturate_cache then saturate_cache thy else NONE
+
+
+(*** Converting a subgoal into negated conjecture clauses. ***)
+
+fun neg_skolemize_tac ctxt =
+ EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
+
+val neg_clausify =
+ single
+ #> Meson.make_clauses_unsorted
+ #> map introduce_combinators
+ #> Meson.finish_cnf
+
+fun neg_conjecture_clauses ctxt st0 n =
+ let
+ (* "Option" is thrown if the assumptions contain schematic variables. *)
+ val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
+ val ({params, prems, ...}, _) =
+ Subgoal.focus (Variable.set_body false ctxt) n st
+ in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
+
+
+(** setup **)
+
+val setup =
+ perhaps conditionally_saturate_cache
+ #> Theory.at_end conditionally_saturate_cache
+
+end;
--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Mon Jun 28 13:36:21 2010 +0200
@@ -14,11 +14,9 @@
structure Meson_Tactic : MESON_TACTIC =
struct
-open Sledgehammer_Fact_Preprocessor
-
(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) =
- String.isPrefix skolem_prefix a
+ String.isPrefix Clausifier.skolem_prefix a
| is_absko _ = false;
fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ _) = (*Definition of Free, not in certain terms*)
@@ -43,7 +41,10 @@
let
val thy = ProofContext.theory_of ctxt
val ctxt0 = Classical.put_claset HOL_cs ctxt
- in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
+ in
+ (Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) i
+ THEN expand_defs_tac st0) st0
+ end
val setup =
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Jun 28 13:36:21 2010 +0200
@@ -0,0 +1,685 @@
+(* Title: HOL/Tools/Sledgehammer/metis_clauses.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
+
+Storing/printing FOL clauses and arity clauses. Typed equality is
+treated differently.
+*)
+
+signature METIS_CLAUSES =
+sig
+ type cnf_thm = Clausifier.cnf_thm
+ type name = string * string
+ type name_pool = string Symtab.table * string Symtab.table
+ datatype kind = Axiom | Conjecture
+ datatype type_literal =
+ TyLitVar of string * name |
+ TyLitFree of string * name
+ datatype arLit =
+ TConsLit of class * string * string list
+ | TVarLit of class * string
+ datatype arity_clause = ArityClause of
+ {axiom_name: string, conclLit: arLit, premLits: arLit list}
+ datatype classrel_clause = ClassrelClause of
+ {axiom_name: string, subclass: class, superclass: class}
+ datatype combtyp =
+ TyVar of name |
+ TyFree of name |
+ TyConstr of name * combtyp list
+ datatype combterm =
+ CombConst of name * combtyp * combtyp list (* Const and Free *) |
+ CombVar of name * combtyp |
+ CombApp of combterm * combterm
+ datatype literal = Literal of bool * combterm
+ datatype hol_clause =
+ HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+ literals: literal list, ctypes_sorts: typ list}
+ exception TRIVIAL of unit
+
+ val type_wrapper_name : string
+ val schematic_var_prefix: string
+ val fixed_var_prefix: string
+ val tvar_prefix: string
+ val tfree_prefix: string
+ val const_prefix: string
+ val tconst_prefix: string
+ val class_prefix: string
+ val union_all: ''a list list -> ''a list
+ val invert_const: string -> string
+ val ascii_of: string -> string
+ val undo_ascii_of: string -> string
+ val strip_prefix: string -> string -> string option
+ val make_schematic_var : string * int -> string
+ val make_fixed_var : string -> string
+ val make_schematic_type_var : string * int -> string
+ val make_fixed_type_var : string -> string
+ val make_fixed_const : string -> string
+ val make_fixed_type_const : string -> string
+ val make_type_class : string -> string
+ val empty_name_pool : bool -> name_pool option
+ val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
+ val nice_name : name -> name_pool option -> string * name_pool option
+ val type_literals_for_types : typ list -> type_literal list
+ val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
+ val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
+ val type_of_combterm : combterm -> combtyp
+ val strip_combterm_comb : combterm -> combterm * combterm list
+ val literals_of_term : theory -> term -> literal list * typ list
+ val conceal_skolem_somes :
+ int -> (string * term) list -> term -> (string * term) list * term
+ val is_quasi_fol_theorem : theory -> thm -> bool
+ val make_clause_table : (thm * 'a) list -> (thm * 'a) Termtab.table
+ val tfree_classes_of_terms : term list -> string list
+ val tvar_classes_of_terms : term list -> string list
+ val type_consts_of_terms : theory -> term list -> string list
+ val prepare_clauses :
+ bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
+ -> string vector
+ * (hol_clause list * hol_clause list * hol_clause list * hol_clause list
+ * classrel_clause list * arity_clause list)
+end
+
+structure Metis_Clauses : METIS_CLAUSES =
+struct
+
+open Clausifier
+
+val type_wrapper_name = "ti"
+
+val schematic_var_prefix = "V_";
+val fixed_var_prefix = "v_";
+
+val tvar_prefix = "T_";
+val tfree_prefix = "t_";
+
+val classrel_clause_prefix = "clsrel_";
+
+val const_prefix = "c_";
+val tconst_prefix = "tc_";
+val class_prefix = "class_";
+
+fun union_all xss = fold (union (op =)) xss []
+
+(* Readable names for the more common symbolic functions. Do not mess with the
+ last nine entries of the table unless you know what you are doing. *)
+val const_trans_table =
+ Symtab.make [(@{const_name "op ="}, "equal"),
+ (@{const_name "op &"}, "and"),
+ (@{const_name "op |"}, "or"),
+ (@{const_name "op -->"}, "implies"),
+ (@{const_name "op :"}, "in"),
+ (@{const_name fequal}, "fequal"),
+ (@{const_name COMBI}, "COMBI"),
+ (@{const_name COMBK}, "COMBK"),
+ (@{const_name COMBB}, "COMBB"),
+ (@{const_name COMBC}, "COMBC"),
+ (@{const_name COMBS}, "COMBS"),
+ (@{const_name True}, "True"),
+ (@{const_name False}, "False"),
+ (@{const_name If}, "If"),
+ (@{type_name "*"}, "prod"),
+ (@{type_name "+"}, "sum")]
+
+(* Invert the table of translations between Isabelle and ATPs. *)
+val const_trans_table_inv =
+ Symtab.update ("fequal", @{const_name "op ="})
+ (Symtab.make (map swap (Symtab.dest const_trans_table)))
+
+val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
+
+(*Escaping of special characters.
+ Alphanumeric characters are left unchanged.
+ The character _ goes to __
+ Characters in the range ASCII space to / go to _A to _P, respectively.
+ Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
+val A_minus_space = Char.ord #"A" - Char.ord #" ";
+
+fun stringN_of_int 0 _ = ""
+ | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
+
+fun ascii_of_c c =
+ if Char.isAlphaNum c then String.str c
+ else if c = #"_" then "__"
+ else if #" " <= c andalso c <= #"/"
+ then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
+ else if Char.isPrint c
+ then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
+ else ""
+
+val ascii_of = String.translate ascii_of_c;
+
+(** Remove ASCII armouring from names in proof files **)
+
+(*We don't raise error exceptions because this code can run inside the watcher.
+ Also, the errors are "impossible" (hah!)*)
+fun undo_ascii_aux rcs [] = String.implode(rev rcs)
+ | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*)
+ (*Three types of _ escapes: __, _A to _P, _nnn*)
+ | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
+ | undo_ascii_aux rcs (#"_" :: c :: cs) =
+ if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
+ then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
+ else
+ let val digits = List.take (c::cs, 3) handle Subscript => []
+ in
+ case Int.fromString (String.implode digits) of
+ NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*)
+ | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
+ end
+ | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
+
+val undo_ascii_of = undo_ascii_aux [] o String.explode;
+
+(* If string s has the prefix s1, return the result of deleting it,
+ un-ASCII'd. *)
+fun strip_prefix s1 s =
+ if String.isPrefix s1 s then
+ SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
+ else
+ NONE
+
+(*Remove the initial ' character from a type variable, if it is present*)
+fun trim_type_var s =
+ if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
+ else error ("trim_type: Malformed type variable encountered: " ^ s);
+
+fun ascii_of_indexname (v,0) = ascii_of v
+ | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
+
+fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
+fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
+
+fun make_schematic_type_var (x,i) =
+ tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
+fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
+
+fun lookup_const c =
+ case Symtab.lookup const_trans_table c of
+ SOME c' => c'
+ | NONE => ascii_of c
+
+(* "op =" MUST BE "equal" because it's built into ATPs. *)
+fun make_fixed_const @{const_name "op ="} = "equal"
+ | make_fixed_const c = const_prefix ^ lookup_const c
+
+fun make_fixed_type_const c = tconst_prefix ^ lookup_const c
+
+fun make_type_class clas = class_prefix ^ ascii_of clas;
+
+
+(**** name pool ****)
+
+type name = string * string
+type name_pool = string Symtab.table * string Symtab.table
+
+fun empty_name_pool readable_names =
+ if readable_names then SOME (`I Symtab.empty) else NONE
+
+fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
+fun pool_map f xs =
+ pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
+
+fun add_nice_name full_name nice_prefix j the_pool =
+ let
+ val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j)
+ in
+ case Symtab.lookup (snd the_pool) nice_name of
+ SOME full_name' =>
+ if full_name = full_name' then (nice_name, the_pool)
+ else add_nice_name full_name nice_prefix (j + 1) the_pool
+ | NONE =>
+ (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool),
+ Symtab.update_new (nice_name, full_name) (snd the_pool)))
+ end
+
+fun translate_first_char f s =
+ String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
+
+fun readable_name full_name s =
+ let
+ val s = s |> Long_Name.base_name |> Name.desymbolize false
+ val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
+ val s' =
+ (s' |> rev
+ |> implode
+ |> String.translate
+ (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
+ else ""))
+ ^ replicate_string (String.size s - length s') "_"
+ val s' =
+ if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
+ else s'
+ (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
+ ("op &", "op |", etc.). *)
+ val s' = if s' = "equal" orelse s' = "op" then full_name else s'
+ in
+ case (Char.isLower (String.sub (full_name, 0)),
+ Char.isLower (String.sub (s', 0))) of
+ (true, false) => translate_first_char Char.toLower s'
+ | (false, true) => translate_first_char Char.toUpper s'
+ | _ => s'
+ end
+
+fun nice_name (full_name, _) NONE = (full_name, NONE)
+ | nice_name (full_name, desired_name) (SOME the_pool) =
+ case Symtab.lookup (fst the_pool) full_name of
+ SOME nice_name => (nice_name, SOME the_pool)
+ | NONE => add_nice_name full_name (readable_name full_name desired_name) 0
+ the_pool
+ |> apsnd SOME
+
+(**** Definitions and functions for FOL clauses for TPTP format output ****)
+
+datatype kind = Axiom | Conjecture
+
+(**** Isabelle FOL clauses ****)
+
+(* The first component is the type class; the second is a TVar or TFree. *)
+datatype type_literal =
+ TyLitVar of string * name |
+ TyLitFree of string * name
+
+exception CLAUSE of string * term;
+
+(*Make literals for sorted type variables*)
+fun sorts_on_typs_aux (_, []) = []
+ | sorts_on_typs_aux ((x,i), s::ss) =
+ let val sorts = sorts_on_typs_aux ((x,i), ss)
+ in
+ if s = "HOL.type" then sorts
+ else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
+ else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
+ end;
+
+fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
+ | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
+
+(*Given a list of sorted type variables, return a list of type literals.*)
+fun type_literals_for_types Ts =
+ fold (union (op =)) (map sorts_on_typs Ts) []
+
+(** make axiom and conjecture clauses. **)
+
+(**** Isabelle arities ****)
+
+datatype arLit = TConsLit of class * string * string list
+ | TVarLit of class * string;
+
+datatype arity_clause =
+ ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
+
+
+fun gen_TVars 0 = []
+ | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
+
+fun pack_sort(_,[]) = []
+ | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*)
+ | pack_sort(tvar, cls::srt) = (cls, tvar) :: pack_sort(tvar, srt);
+
+(*Arity of type constructor tcon :: (arg1,...,argN)res*)
+fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
+ let val tvars = gen_TVars (length args)
+ val tvars_srts = ListPair.zip (tvars,args)
+ in
+ ArityClause {axiom_name = axiom_name,
+ conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
+ premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
+ end;
+
+
+(**** Isabelle class relations ****)
+
+datatype classrel_clause =
+ ClassrelClause of {axiom_name: string, subclass: class, superclass: class}
+
+(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
+fun class_pairs _ [] _ = []
+ | class_pairs thy subs supers =
+ let
+ val class_less = Sorts.class_less (Sign.classes_of thy)
+ fun add_super sub super = class_less (sub, super) ? cons (sub, super)
+ fun add_supers sub = fold (add_super sub) supers
+ in fold add_supers subs [] end
+
+fun make_classrel_clause (sub,super) =
+ ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
+ ascii_of super,
+ subclass = make_type_class sub,
+ superclass = make_type_class super};
+
+fun make_classrel_clauses thy subs supers =
+ map make_classrel_clause (class_pairs thy subs supers);
+
+
+(** Isabelle arities **)
+
+fun arity_clause _ _ (_, []) = []
+ | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
+ arity_clause seen n (tcons,ars)
+ | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
+ if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
+ make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
+ arity_clause seen (n+1) (tcons,ars)
+ else
+ make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
+ arity_clause (class::seen) n (tcons,ars)
+
+fun multi_arity_clause [] = []
+ | multi_arity_clause ((tcons, ars) :: tc_arlists) =
+ arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
+
+(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
+ provided its arguments have the corresponding sorts.*)
+fun type_class_pairs thy tycons classes =
+ let val alg = Sign.classes_of thy
+ fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
+ fun add_class tycon class =
+ cons (class, domain_sorts tycon class)
+ handle Sorts.CLASS_ERROR _ => I
+ fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
+ in map try_classes tycons end;
+
+(*Proving one (tycon, class) membership may require proving others, so iterate.*)
+fun iter_type_class_pairs _ _ [] = ([], [])
+ | iter_type_class_pairs thy tycons classes =
+ let val cpairs = type_class_pairs thy tycons classes
+ val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
+ |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
+ val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
+ in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
+
+fun make_arity_clauses thy tycons classes =
+ let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
+ in (classes', multi_arity_clause cpairs) end;
+
+datatype combtyp =
+ TyVar of name |
+ TyFree of name |
+ TyConstr of name * combtyp list
+
+datatype combterm =
+ CombConst of name * combtyp * combtyp list (* Const and Free *) |
+ CombVar of name * combtyp |
+ CombApp of combterm * combterm
+
+datatype literal = Literal of bool * combterm
+
+datatype hol_clause =
+ HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+ literals: literal list, ctypes_sorts: typ list}
+
+(*********************************************************************)
+(* convert a clause with type Term.term to a clause with type clause *)
+(*********************************************************************)
+
+(*Result of a function type; no need to check that the argument type matches.*)
+fun result_type (TyConstr (_, [_, tp2])) = tp2
+ | result_type _ = raise Fail "non-function type"
+
+fun type_of_combterm (CombConst (_, tp, _)) = tp
+ | type_of_combterm (CombVar (_, tp)) = tp
+ | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
+
+(*gets the head of a combinator application, along with the list of arguments*)
+fun strip_combterm_comb u =
+ let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
+ | stripc x = x
+ in stripc(u,[]) end
+
+fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
+ (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
+ | isFalse _ = false;
+
+fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
+ (pol andalso c = "c_True") orelse
+ (not pol andalso c = "c_False")
+ | isTrue _ = false;
+
+fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
+
+fun type_of (Type (a, Ts)) =
+ let val (folTypes,ts) = types_of Ts in
+ (TyConstr (`make_fixed_type_const a, folTypes), ts)
+ end
+ | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
+ | type_of (tp as TVar (x, _)) =
+ (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
+and types_of Ts =
+ let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
+ (folTyps, union_all ts)
+ end
+
+(* same as above, but no gathering of sort information *)
+fun simp_type_of (Type (a, Ts)) =
+ TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
+ | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
+ | simp_type_of (TVar (x, _)) =
+ TyVar (make_schematic_type_var x, string_of_indexname x)
+
+(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
+fun combterm_of thy (Const (c, T)) =
+ let
+ val (tp, ts) = type_of T
+ val tvar_list =
+ (if String.isPrefix skolem_theory_name c then
+ [] |> Term.add_tvarsT T |> map TVar
+ else
+ (c, T) |> Sign.const_typargs thy)
+ |> map simp_type_of
+ val c' = CombConst (`make_fixed_const c, tp, tvar_list)
+ in (c',ts) end
+ | combterm_of _ (Free(v, T)) =
+ let val (tp,ts) = type_of T
+ val v' = CombConst (`make_fixed_var v, tp, [])
+ in (v',ts) end
+ | combterm_of _ (Var(v, T)) =
+ let val (tp,ts) = type_of T
+ val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
+ in (v',ts) end
+ | combterm_of thy (P $ Q) =
+ let val (P', tsP) = combterm_of thy P
+ val (Q', tsQ) = combterm_of thy Q
+ in (CombApp (P', Q'), union (op =) tsP tsQ) end
+ | combterm_of _ (t as Abs _) = raise Fail "HOL clause: Abs"
+
+fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
+ | predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
+
+fun literals_of_term1 args thy (@{const Trueprop} $ P) =
+ literals_of_term1 args thy P
+ | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
+ literals_of_term1 (literals_of_term1 args thy P) thy Q
+ | literals_of_term1 (lits, ts) thy P =
+ let val ((pred, ts'), pol) = predicate_of thy (P, true) in
+ (Literal (pol, pred) :: lits, union (op =) ts ts')
+ end
+val literals_of_term = literals_of_term1 ([], [])
+
+fun skolem_name i j num_T_args =
+ skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
+ skolem_infix ^ "g"
+
+fun conceal_skolem_somes i skolem_somes t =
+ if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
+ let
+ fun aux skolem_somes
+ (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
+ let
+ val (skolem_somes, s) =
+ if i = ~1 then
+ (skolem_somes, @{const_name undefined})
+ else case AList.find (op aconv) skolem_somes t of
+ s :: _ => (skolem_somes, s)
+ | [] =>
+ let
+ val s = skolem_theory_name ^ "." ^
+ skolem_name i (length skolem_somes)
+ (length (Term.add_tvarsT T []))
+ in ((s, t) :: skolem_somes, s) end
+ in (skolem_somes, Const (s, T)) end
+ | aux skolem_somes (t1 $ t2) =
+ let
+ val (skolem_somes, t1) = aux skolem_somes t1
+ val (skolem_somes, t2) = aux skolem_somes t2
+ in (skolem_somes, t1 $ t2) end
+ | aux skolem_somes (Abs (s, T, t')) =
+ let val (skolem_somes, t') = aux skolem_somes t' in
+ (skolem_somes, Abs (s, T, t'))
+ end
+ | aux skolem_somes t = (skolem_somes, t)
+ in aux skolem_somes t end
+ else
+ (skolem_somes, t)
+
+fun is_quasi_fol_theorem thy =
+ Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
+
+(* Trivial problem, which resolution cannot handle (empty clause) *)
+exception TRIVIAL of unit
+
+(* making axiom and conjecture clauses *)
+fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
+ let
+ val (skolem_somes, t) =
+ th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
+ val (lits, ctypes_sorts) = literals_of_term thy t
+ in
+ if forall isFalse lits then
+ raise TRIVIAL ()
+ else
+ (skolem_somes,
+ HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
+ kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
+ end
+
+fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
+ let
+ val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
+ in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
+
+fun make_axiom_clauses thy clauses =
+ ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
+
+fun make_conjecture_clauses thy =
+ let
+ fun aux _ _ [] = []
+ | aux n skolem_somes (th :: ths) =
+ let
+ val (skolem_somes, cls) =
+ make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
+ in cls :: aux (n + 1) skolem_somes ths end
+ in aux 0 [] end
+
+(** Helper clauses **)
+
+fun count_combterm (CombConst ((c, _), _, _)) =
+ Symtab.map_entry c (Integer.add 1)
+ | count_combterm (CombVar _) = I
+ | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
+fun count_literal (Literal (_, t)) = count_combterm t
+fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
+
+fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
+fun cnf_helper_thms thy raw =
+ map (`Thm.get_name_hint)
+ #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
+
+val optional_helpers =
+ [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
+ (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
+ (["c_COMBS"], (false, @{thms COMBS_def}))]
+val optional_typed_helpers =
+ [(["c_True", "c_False"], (true, @{thms True_or_False})),
+ (["c_If"], (true, @{thms if_True if_False True_or_False}))]
+val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
+
+val init_counters =
+ Symtab.make (maps (maps (map (rpair 0) o fst))
+ [optional_helpers, optional_typed_helpers])
+
+fun get_helper_clauses thy is_FO full_types conjectures axcls =
+ let
+ val axclauses = map snd (make_axiom_clauses thy axcls)
+ val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
+ fun is_needed c = the (Symtab.lookup ct c) > 0
+ val cnfs =
+ (optional_helpers
+ |> full_types ? append optional_typed_helpers
+ |> maps (fn (ss, (raw, ths)) =>
+ if exists is_needed ss then cnf_helper_thms thy raw ths
+ else []))
+ @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
+ in map snd (make_axiom_clauses thy cnfs) end
+
+fun make_clause_table xs =
+ fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
+
+
+(***************************************************************)
+(* Type Classes Present in the Axiom or Conjecture Clauses *)
+(***************************************************************)
+
+fun set_insert (x, s) = Symtab.update (x, ()) s
+
+fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
+
+(*Remove this trivial type class*)
+fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
+
+fun tfree_classes_of_terms ts =
+ let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
+ in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
+
+fun tvar_classes_of_terms ts =
+ let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
+ in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
+
+(*fold type constructors*)
+fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
+ | fold_type_consts _ _ x = x;
+
+(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
+fun add_type_consts_in_term thy =
+ let
+ val const_typargs = Sign.const_typargs thy
+ fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
+ | aux (Abs (_, _, u)) = aux u
+ | aux (Const (@{const_name skolem_id}, _) $ _) = I
+ | aux (t $ u) = aux t #> aux u
+ | aux _ = I
+ in aux end
+
+fun type_consts_of_terms thy ts =
+ Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
+
+(* Remove existing axiom clauses from the conjecture clauses, as this can
+ dramatically boost an ATP's performance (for some reason). *)
+fun subtract_cls ax_clauses =
+ filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
+
+(* prepare for passing to writer,
+ create additional clauses based on the information from extra_cls *)
+fun prepare_clauses full_types goal_cls axcls extra_cls thy =
+ let
+ val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
+ val ccls = subtract_cls extra_cls goal_cls
+ val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
+ val ccltms = map prop_of ccls
+ and axtms = map (prop_of o #1) extra_cls
+ val subs = tfree_classes_of_terms ccltms
+ and supers = tvar_classes_of_terms axtms
+ and tycons = type_consts_of_terms thy (ccltms @ axtms)
+ (*TFrees in conjecture clauses; TVars in axiom clauses*)
+ val conjectures = make_conjecture_clauses thy ccls
+ val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
+ val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
+ val helper_clauses =
+ get_helper_clauses thy is_FO full_types conjectures extra_cls
+ val (supers', arity_clauses) = make_arity_clauses thy tycons supers
+ val classrel_clauses = make_classrel_clauses thy subs supers'
+ in
+ (Vector.fromList clnames,
+ (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
+ end
+
+end;
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 28 13:36:21 2010 +0200
@@ -18,13 +18,8 @@
structure Metis_Tactics : METIS_TACTICS =
struct
-open Sledgehammer_Util
-open Sledgehammer_FOL_Clause
-open Sledgehammer_Fact_Preprocessor
-open Sledgehammer_HOL_Clause
-open Sledgehammer_Proof_Reconstruct
-open Sledgehammer_Fact_Filter
-open Sledgehammer_TPTP_Format
+open Clausifier
+open Metis_Clauses
exception METIS of string * string
@@ -234,7 +229,7 @@
| NONE => make_tvar v)
| fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
(case strip_prefix tconst_prefix x of
- SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
+ SOME tc => Term.Type (invert_const tc, map (fol_type_to_isa ctxt) tys)
| NONE =>
case strip_prefix tfree_prefix x of
SOME tf => mk_tfree ctxt tf
@@ -295,7 +290,7 @@
| NONE => (*Not a constant. Is it a type constructor?*)
case strip_prefix tconst_prefix a of
SOME b =>
- Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
+ Type (Term.Type (invert_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
case strip_prefix tfree_prefix a of
SOME b => Type (mk_tfree ctxt b)
@@ -724,6 +719,7 @@
fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
+
(* Main function to start Metis proof and reconstruction *)
fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
@@ -737,7 +733,8 @@
val (mode, {axioms, tfrees, skolem_somes}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (trace_msg (fn () => "TFREE CLAUSES");
- app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
+ app (fn TyLitFree (s, (s', _)) =>
+ trace_msg (fn _ => s ^ "(" ^ s' ^ ")")) tfrees)
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
val thms = map #1 axioms
val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jun 28 13:36:21 2010 +0200
@@ -5,10 +5,7 @@
signature SLEDGEHAMMER_FACT_FILTER =
sig
- type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
- type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
- type arity_clause = Sledgehammer_FOL_Clause.arity_clause
- type hol_clause = Sledgehammer_HOL_Clause.hol_clause
+ type cnf_thm = Clausifier.cnf_thm
type relevance_override =
{add: Facts.ref list,
@@ -16,29 +13,18 @@
only: bool}
val use_natural_form : bool Unsynchronized.ref
- val name_thms_pair_from_ref :
- Proof.context -> thm list -> Facts.ref -> string * thm list
- val tvar_classes_of_terms : term list -> string list
- val tfree_classes_of_terms : term list -> string list
- val type_consts_of_terms : theory -> term list -> string list
- val is_quasi_fol_theorem : theory -> thm -> bool
val relevant_facts :
- bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
+ bool -> real -> real -> bool -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
- val prepare_clauses :
- bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
- -> string vector
- * (hol_clause list * hol_clause list * hol_clause list
- * hol_clause list * classrel_clause list * arity_clause list)
end;
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
struct
-open Sledgehammer_FOL_Clause
-open Sledgehammer_Fact_Preprocessor
-open Sledgehammer_HOL_Clause
+open Clausifier
+open Metis_Clauses
+val respect_no_atp = true
(* Experimental feature: Filter theorems in natural form or in CNF? *)
val use_natural_form = Unsynchronized.ref false
@@ -280,13 +266,13 @@
| _ => false
end;
-type annotated_clause = cnf_thm * ((string * const_typ list) list)
+type annotated_cnf_thm = cnf_thm * ((string * const_typ list) list)
(*For a reverse sort, putting the largest values first.*)
fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
(*Limit the number of new clauses, to prevent runaway acceptance.*)
-fun take_best max_new (newpairs : (annotated_clause * real) list) =
+fun take_best max_new (newpairs : (annotated_cnf_thm * real) list) =
let val nnew = length newpairs
in
if nnew <= max_new then (map #1 newpairs, [])
@@ -392,10 +378,6 @@
(*** retrieve lemmas and filter them ***)
-(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
-
-fun setinsert (x,s) = Symtab.update (x,()) s;
-
(*Reject theorems with names like "List.filter.filter_list_def" or
"Accessible_Part.acc.defs", as these are definitions arising from packages.*)
fun is_package_def a =
@@ -406,21 +388,12 @@
String.isSuffix "_def" a orelse String.isSuffix "_defs" a
end;
-fun mk_clause_table xs =
- fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
-
-fun make_unique xs =
- Termtab.fold (cons o snd) (mk_clause_table xs) []
-
-(* Remove existing axiom clauses from the conjecture clauses, as this can
- dramatically boost an ATP's performance (for some reason). *)
-fun subtract_cls ax_clauses =
- filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
+fun make_unique xs = Termtab.fold (cons o snd) (make_clause_table xs) []
val exists_sledgehammer_const =
exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
-fun all_name_thms_pairs respect_no_atp ctxt chained_ths =
+fun all_name_thms_pairs ctxt chained_ths =
let
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
val local_facts = ProofContext.facts_of ctxt;
@@ -464,7 +437,7 @@
(* The single-name theorems go after the multiple-name ones, so that single
names are preferred when both are available. *)
-fun name_thm_pairs respect_no_atp ctxt name_thms_pairs =
+fun name_thm_pairs ctxt respect_no_atp name_thms_pairs =
let
val (mults, singles) = List.partition is_multi name_thms_pairs
val ps = [] |> fold add_names singles |> fold add_names mults
@@ -475,64 +448,16 @@
Display.string_of_thm_without_context th); false)
| is_named _ = true
fun checked_name_thm_pairs respect_no_atp ctxt =
- name_thm_pairs respect_no_atp ctxt
+ name_thm_pairs ctxt respect_no_atp
#> tap (fn ps => trace_msg
(fn () => ("Considering " ^ Int.toString (length ps) ^
" theorems")))
#> filter is_named
-fun name_thms_pair_from_ref ctxt chained_ths xref =
- let
- val ths = ProofContext.get_fact ctxt xref
- val name = Facts.string_of_ref xref
- |> forall (member Thm.eq_thm chained_ths) ths
- ? prefix chained_prefix
- in (name, ths) end
-
-
-(***************************************************************)
-(* Type Classes Present in the Axiom or Conjecture Clauses *)
-(***************************************************************)
-
-fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts);
-
-(*Remove this trivial type class*)
-fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
-
-fun tvar_classes_of_terms ts =
- let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
- in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
-
-fun tfree_classes_of_terms ts =
- let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
- in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
-
-(*fold type constructors*)
-fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
- | fold_type_consts _ _ x = x;
-
-(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
-fun add_type_consts_in_term thy =
- let
- val const_typargs = Sign.const_typargs thy
- fun aux (Const cT) = fold (fold_type_consts setinsert) (const_typargs cT)
- | aux (Abs (_, _, u)) = aux u
- | aux (Const (@{const_name skolem_id}, _) $ _) = I
- | aux (t $ u) = aux t #> aux u
- | aux _ = I
- in aux end
-
-fun type_consts_of_terms thy ts =
- Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
-
-
(***************************************************************)
(* ATP invocation methods setup *)
(***************************************************************)
-fun is_quasi_fol_theorem thy =
- Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
-
(**** Predicates to detect unwanted clauses (prolific or likely to cause
unsoundness) ****)
@@ -581,22 +506,19 @@
(has_typed_var dangerous_types t orelse
forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
-fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of
-
-fun relevant_facts full_types respect_no_atp relevance_threshold
- relevance_convergence defs_relevant max_new theory_relevant
+fun relevant_facts full_types relevance_threshold relevance_convergence
+ defs_relevant max_new theory_relevant
(relevance_override as {add, del, only})
(ctxt, (chained_ths, _)) goal_cls =
let
val thy = ProofContext.theory_of ctxt
val add_thms = maps (ProofContext.get_fact ctxt) add
val has_override = not (null add) orelse not (null del)
- val is_FO = is_fol_goal thy goal_cls
+ val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
val axioms =
checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
(map (name_thms_pair_from_ref ctxt chained_ths) add @
- (if only then []
- else all_name_thms_pairs respect_no_atp ctxt chained_ths))
+ (if only then [] else all_name_thms_pairs ctxt chained_ths))
|> cnf_rules_pairs thy
|> not has_override ? make_unique
|> filter (fn (cnf_thm, (_, orig_thm)) =>
@@ -611,70 +533,4 @@
|> sort (prod_ord string_ord int_ord o pairself (fst o snd))
end
-(** Helper clauses **)
-
-fun count_combterm (CombConst ((c, _), _, _)) =
- Symtab.map_entry c (Integer.add 1)
- | count_combterm (CombVar _) = I
- | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
-fun count_literal (Literal (_, t)) = count_combterm t
-fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
-
-fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
-fun cnf_helper_thms thy raw =
- map (`Thm.get_name_hint)
- #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
-
-val optional_helpers =
- [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
- (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
- (["c_COMBS"], (false, @{thms COMBS_def}))]
-val optional_typed_helpers =
- [(["c_True", "c_False"], (true, @{thms True_or_False})),
- (["c_If"], (true, @{thms if_True if_False True_or_False}))]
-val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
-
-val init_counters =
- Symtab.make (maps (maps (map (rpair 0) o fst))
- [optional_helpers, optional_typed_helpers])
-
-fun get_helper_clauses thy is_FO full_types conjectures axcls =
- let
- val axclauses = map snd (make_axiom_clauses thy axcls)
- val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
- fun is_needed c = the (Symtab.lookup ct c) > 0
- val cnfs =
- (optional_helpers
- |> full_types ? append optional_typed_helpers
- |> maps (fn (ss, (raw, ths)) =>
- if exists is_needed ss then cnf_helper_thms thy raw ths
- else []))
- @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
- in map snd (make_axiom_clauses thy cnfs) end
-
-(* prepare for passing to writer,
- create additional clauses based on the information from extra_cls *)
-fun prepare_clauses full_types goal_cls axcls extra_cls thy =
- let
- val is_FO = is_fol_goal thy goal_cls
- val ccls = subtract_cls extra_cls goal_cls
- val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
- val ccltms = map prop_of ccls
- and axtms = map (prop_of o #1) extra_cls
- val subs = tfree_classes_of_terms ccltms
- and supers = tvar_classes_of_terms axtms
- and tycons = type_consts_of_terms thy (ccltms @ axtms)
- (*TFrees in conjecture clauses; TVars in axiom clauses*)
- val conjectures = make_conjecture_clauses thy ccls
- val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
- val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
- val helper_clauses =
- get_helper_clauses thy is_FO full_types conjectures extra_cls
- val (supers', arity_clauses) = make_arity_clauses thy tycons supers
- val classrel_clauses = make_classrel_clauses thy subs supers'
- in
- (Vector.fromList clnames,
- (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
- end
-
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Jun 28 13:36:21 2010 +0200
@@ -18,9 +18,9 @@
structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
struct
+open Clausifier
+open Metis_Clauses
open Sledgehammer_Util
-open Sledgehammer_Fact_Preprocessor
-open Sledgehammer_HOL_Clause
open Sledgehammer_Proof_Reconstruct
open ATP_Manager
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Jun 28 10:39:39 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,553 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
- Author: Jia Meng, Cambridge University Computer Laboratory
- Author: Jasmin Blanchette, TU Muenchen
-
-Transformation of axiom rules (elim/intro/etc) into CNF forms.
-*)
-
-signature SLEDGEHAMMER_FACT_PREPROCESSOR =
-sig
- type cnf_thm = thm * ((string * int) * thm)
-
- val sledgehammer_prefix: string
- val chained_prefix: string
- val trace: bool Unsynchronized.ref
- val trace_msg: (unit -> string) -> unit
- val skolem_theory_name: string
- val skolem_prefix: string
- val skolem_infix: string
- val is_skolem_const_name: string -> bool
- val cnf_axiom: theory -> thm -> thm list
- val multi_base_blacklist: string list
- val is_theorem_bad_for_atps: thm -> bool
- val type_has_topsort: typ -> bool
- val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
- val saturate_skolem_cache: theory -> theory option
- val auto_saturate_skolem_cache: bool Unsynchronized.ref
- val neg_clausify: thm -> thm list
- val neg_conjecture_clauses:
- Proof.context -> thm -> int -> thm list list * (string * typ) list
- val setup: theory -> theory
-end;
-
-structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR =
-struct
-
-open Sledgehammer_FOL_Clause
-
-type cnf_thm = thm * ((string * int) * thm)
-
-val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-
-(* Used to label theorems chained into the goal. *)
-val chained_prefix = sledgehammer_prefix ^ "chained_"
-
-val trace = Unsynchronized.ref false;
-fun trace_msg msg = if !trace then tracing (msg ()) else ();
-
-val skolem_theory_name = sledgehammer_prefix ^ "Sko"
-val skolem_prefix = "sko_"
-val skolem_infix = "$"
-
-fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
-
-val type_has_topsort = Term.exists_subtype
- (fn TFree (_, []) => true
- | TVar (_, []) => true
- | _ => false);
-
-
-(**** Transformation of Elimination Rules into First-Order Formulas****)
-
-val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
-val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
-
-(*Converts an elim-rule into an equivalent theorem that does not have the
- predicate variable. Leaves other theorems unchanged. We simply instantiate the
- conclusion variable to False.*)
-fun transform_elim th =
- case concl_of th of (*conclusion variable*)
- @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
- Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
- | v as Var(_, @{typ prop}) =>
- Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
- | _ => th;
-
-(*To enforce single-threading*)
-exception Clausify_failure of theory;
-
-
-(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
-
-(*Keep the full complexity of the original name*)
-fun flatten_name s = space_implode "_X" (Long_Name.explode s);
-
-fun skolem_name thm_name j var_name =
- skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^
- skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
-
-(* Hack: Could return false positives (e.g., a user happens to declare a
- constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
-val is_skolem_const_name =
- Long_Name.base_name
- #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
-
-fun rhs_extra_types lhsT rhs =
- let val lhs_vars = Term.add_tfreesT lhsT []
- fun add_new_TFrees (TFree v) =
- if member (op =) lhs_vars v then I else insert (op =) (TFree v)
- | add_new_TFrees _ = I
- val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
- in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
-
-fun skolem_type_and_args bound_T body =
- let
- val args1 = OldTerm.term_frees body
- val Ts1 = map type_of args1
- val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body
- val args2 = map (fn T => Free (gensym "vsk", T)) Ts2
- in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end
-
-(* Traverse a theorem, declaring Skolem function definitions. String "s" is the
- suggested prefix for the Skolem constants. *)
-fun declare_skolem_funs s th thy =
- let
- val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p)))
- (axs, thy) =
- (*Existential: declare a Skolem function, then insert into body and continue*)
- let
- val id = skolem_name s (Unsynchronized.inc skolem_count) s'
- val (cT, args) = skolem_type_and_args T body
- val rhs = list_abs_free (map dest_Free args,
- HOLogic.choice_const T $ body)
- (*Forms a lambda-abstraction over the formal parameters*)
- val (c, thy) =
- Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
- val cdef = id ^ "_def"
- val ((_, ax), thy) =
- Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
- val ax' = Drule.export_without_context ax
- in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
- | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
- (*Universal quant: insert a free variable into body and continue*)
- let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
- in dec_sko (subst_bound (Free (fname, T), p)) thx end
- | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
- | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
- | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
- | dec_sko _ thx = thx
- in dec_sko (prop_of th) ([], thy) end
-
-fun mk_skolem_id t =
- let val T = fastype_of t in
- Const (@{const_name skolem_id}, T --> T) $ t
- end
-
-fun quasi_beta_eta_contract (Abs (s, T, t')) =
- Abs (s, T, quasi_beta_eta_contract t')
- | quasi_beta_eta_contract t = Envir.beta_eta_contract t
-
-(*Traverse a theorem, accumulating Skolem function definitions.*)
-fun assume_skolem_funs s th =
- let
- val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs =
- (*Existential: declare a Skolem function, then insert into body and continue*)
- let
- val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
- val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*)
- val Ts = map type_of args
- val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
- val id = skolem_name s (Unsynchronized.inc skolem_count) s'
- val c = Free (id, cT) (* FIXME: needed? ### *)
- (* Forms a lambda-abstraction over the formal parameters *)
- val rhs =
- list_abs_free (map dest_Free args,
- HOLogic.choice_const T
- $ quasi_beta_eta_contract body)
- |> mk_skolem_id
- val def = Logic.mk_equals (c, rhs)
- val comb = list_comb (rhs, args)
- in dec_sko (subst_bound (comb, p)) (def :: defs) end
- | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
- (*Universal quant: insert a free variable into body and continue*)
- let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
- in dec_sko (subst_bound (Free(fname,T), p)) defs end
- | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
- | dec_sko _ defs = defs
- in dec_sko (prop_of th) [] end;
-
-
-(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
-
-(*Returns the vars of a theorem*)
-fun vars_of_thm th =
- map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
-
-val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
-
-(* Removes the lambdas from an equation of the form t = (%x. u). *)
-fun extensionalize th =
- case prop_of th of
- _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
- $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
- | _ => th
-
-fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
- | is_quasi_lambda_free (t1 $ t2) =
- is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
- | is_quasi_lambda_free (Abs _) = false
- | is_quasi_lambda_free _ = true
-
-val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
-val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
-val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
-
-(*FIXME: requires more use of cterm constructors*)
-fun abstract ct =
- let
- val thy = theory_of_cterm ct
- val Abs(x,_,body) = term_of ct
- val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
- val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
- fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
- in
- case body of
- Const _ => makeK()
- | Free _ => makeK()
- | Var _ => makeK() (*though Var isn't expected*)
- | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
- | rator$rand =>
- if loose_bvar1 (rator,0) then (*C or S*)
- if loose_bvar1 (rand,0) then (*S*)
- let val crator = cterm_of thy (Abs(x,xT,rator))
- val crand = cterm_of thy (Abs(x,xT,rand))
- val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
- val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
- in
- Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
- end
- else (*C*)
- let val crator = cterm_of thy (Abs(x,xT,rator))
- val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
- val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
- in
- Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
- end
- else if loose_bvar1 (rand,0) then (*B or eta*)
- if rand = Bound 0 then Thm.eta_conversion ct
- else (*B*)
- let val crand = cterm_of thy (Abs(x,xT,rand))
- val crator = cterm_of thy rator
- val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
- val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
- in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
- else makeK()
- | _ => raise Fail "abstract: Bad term"
- end;
-
-(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
-fun do_introduce_combinators ct =
- if is_quasi_lambda_free (term_of ct) then
- Thm.reflexive ct
- else case term_of ct of
- Abs _ =>
- let
- val (cv, cta) = Thm.dest_abs NONE ct
- val (v, _) = dest_Free (term_of cv)
- val u_th = do_introduce_combinators cta
- val cu = Thm.rhs_of u_th
- val comb_eq = abstract (Thm.cabs cv cu)
- in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
- | _ $ _ =>
- let val (ct1, ct2) = Thm.dest_comb ct in
- Thm.combination (do_introduce_combinators ct1)
- (do_introduce_combinators ct2)
- end
-
-fun introduce_combinators th =
- if is_quasi_lambda_free (prop_of th) then
- th
- else
- let
- val th = Drule.eta_contraction_rule th
- val eqth = do_introduce_combinators (cprop_of th)
- in Thm.equal_elim eqth th end
- handle THM (msg, _, _) =>
- (warning ("Error in the combinator translation of " ^
- Display.string_of_thm_without_context th ^
- "\nException message: " ^ msg ^ ".");
- (* A type variable of sort "{}" will make abstraction fail. *)
- TrueI)
-
-(*cterms are used throughout for efficiency*)
-val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
-
-(*cterm version of mk_cTrueprop*)
-fun c_mkTrueprop A = Thm.capply cTrueprop A;
-
-(*Given an abstraction over n variables, replace the bound variables by free
- ones. Return the body, along with the list of free variables.*)
-fun c_variant_abs_multi (ct0, vars) =
- let val (cv,ct) = Thm.dest_abs NONE ct0
- in c_variant_abs_multi (ct, cv::vars) end
- handle CTERM _ => (ct0, rev vars);
-
-(*Given the definition of a Skolem function, return a theorem to replace
- an existential formula by a use of that function.
- Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
-fun skolem_theorem_of_def inline def =
- let
- val (c, rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
- val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
- val (ch, frees) = c_variant_abs_multi (rhs', [])
- val (chilbert, cabs) = ch |> Thm.dest_comb
- val thy = Thm.theory_of_cterm chilbert
- val t = Thm.term_of chilbert
- val T =
- case t of
- Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
- | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t])
- val cex = Thm.cterm_of thy (HOLogic.exists_const T)
- val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
- and conc =
- Drule.list_comb (if inline then rhs else c, frees)
- |> Drule.beta_conv cabs |> c_mkTrueprop
- fun tacf [prem] =
- (if inline then rewrite_goals_tac @{thms skolem_id_def_raw}
- else rewrite_goals_tac [def])
- THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw})
- RS @{thm someI_ex}) 1
- in Goal.prove_internal [ex_tm] conc tacf
- |> forall_intr_list frees
- |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
- |> Thm.varifyT_global
- end;
-
-
-(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
-fun to_nnf th ctxt0 =
- let val th1 = th |> transform_elim |> zero_var_indexes
- val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
- val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
- |> extensionalize
- |> Meson.make_nnf ctxt
- in (th3, ctxt) end;
-
-(*Generate Skolem functions for a theorem supplied in nnf*)
-fun skolem_theorems_of_assume s th =
- map (skolem_theorem_of_def true o Thm.assume o cterm_of (theory_of_thm th))
- (assume_skolem_funs s th)
-
-
-(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
-
-val max_lambda_nesting = 3
-
-fun term_has_too_many_lambdas max (t1 $ t2) =
- exists (term_has_too_many_lambdas max) [t1, t2]
- | term_has_too_many_lambdas max (Abs (_, _, t)) =
- max = 0 orelse term_has_too_many_lambdas (max - 1) t
- | term_has_too_many_lambdas _ _ = false
-
-fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-
-(* Don't count nested lambdas at the level of formulas, since they are
- quantifiers. *)
-fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
- formula_has_too_many_lambdas (T :: Ts) t
- | formula_has_too_many_lambdas Ts t =
- if is_formula_type (fastype_of1 (Ts, t)) then
- exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
- else
- term_has_too_many_lambdas max_lambda_nesting t
-
-(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
- was 11. *)
-val max_apply_depth = 15
-
-fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
- | apply_depth (Abs (_, _, t)) = apply_depth t
- | apply_depth _ = 0
-
-fun is_formula_too_complex t =
- apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
- formula_has_too_many_lambdas [] t
-
-fun is_strange_thm th =
- case head_of (concl_of th) of
- Const (a, _) => (a <> @{const_name Trueprop} andalso
- a <> @{const_name "=="})
- | _ => false;
-
-fun is_theorem_bad_for_atps thm =
- let val t = prop_of thm in
- is_formula_too_complex t orelse exists_type type_has_topsort t orelse
- is_strange_thm thm
- end
-
-(* FIXME: put other record thms here, or declare as "no_atp" *)
-val multi_base_blacklist =
- ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
- "split_asm", "cases", "ext_cases"];
-
-fun fake_name th =
- if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
- else gensym "unknown_thm_";
-
-(*Skolemize a named theorem, with Skolem functions as additional premises.*)
-fun skolemize_theorem s th =
- if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
- is_theorem_bad_for_atps th then
- []
- else
- let
- val ctxt0 = Variable.global_thm_context th
- val (nnfth, ctxt) = to_nnf th ctxt0
- val defs = skolem_theorems_of_assume s nnfth
- val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
- in
- cnfs |> map introduce_combinators
- |> Variable.export ctxt ctxt0
- |> Meson.finish_cnf
- end
- handle THM _ => []
-
-(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
- Skolem functions.*)
-structure ThmCache = Theory_Data
-(
- type T = thm list Thmtab.table * unit Symtab.table;
- val empty = (Thmtab.empty, Symtab.empty);
- val extend = I;
- fun merge ((cache1, seen1), (cache2, seen2)) : T =
- (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
-);
-
-val lookup_cache = Thmtab.lookup o #1 o ThmCache.get;
-val already_seen = Symtab.defined o #2 o ThmCache.get;
-
-val update_cache = ThmCache.map o apfst o Thmtab.update;
-fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ())));
-
-(* Convert Isabelle theorems into axiom clauses. *)
-fun cnf_axiom thy th0 =
- let val th = Thm.transfer thy th0 in
- case lookup_cache thy th of
- SOME cls => cls
- | NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th)
- end;
-
-
-(**** Translate a set of theorems into CNF ****)
-
-(*The combination of rev and tail recursion preserves the original order*)
-fun cnf_rules_pairs thy =
- let
- fun do_one _ [] = []
- | do_one ((name, k), th) (cls :: clss) =
- (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss
- fun do_all pairs [] = pairs
- | do_all pairs ((name, th) :: ths) =
- let
- val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
- handle THM _ => [] |
- CLAUSE _ => []
- in do_all (new_pairs @ pairs) ths end
- in do_all [] o rev end
-
-
-(**** Convert all facts of the theory into FOL or HOL clauses ****)
-
-local
-
-fun skolem_def (name, th) thy =
- let val ctxt0 = Variable.global_thm_context th in
- case try (to_nnf th) ctxt0 of
- NONE => (NONE, thy)
- | SOME (nnfth, ctxt) =>
- let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy
- in (SOME (th, ctxt0, ctxt, nnfth, defs), thy') end
- end;
-
-fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) =
- let
- val (cnfs, ctxt) =
- Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt
- val cnfs' = cnfs
- |> map introduce_combinators
- |> Variable.export ctxt ctxt0
- |> Meson.finish_cnf
- |> map Thm.close_derivation;
- in (th, cnfs') end;
-
-in
-
-fun saturate_skolem_cache thy =
- let
- val facts = PureThy.facts_of thy;
- val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) =>
- if Facts.is_concealed facts name orelse already_seen thy name then I
- else cons (name, ths));
- val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
- if member (op =) multi_base_blacklist (Long_Name.base_name name) then
- I
- else
- fold_index (fn (i, th) =>
- if is_theorem_bad_for_atps th orelse
- is_some (lookup_cache thy th) then
- I
- else
- cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
- in
- if null new_facts then
- NONE
- else
- let
- val (defs, thy') = thy
- |> fold (mark_seen o #1) new_facts
- |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
- |>> map_filter I;
- val cache_entries = Par_List.map skolem_cnfs defs;
- in SOME (fold update_cache cache_entries thy') end
- end;
-
-end;
-
-(* For emergency use where the Skolem cache causes problems. *)
-val auto_saturate_skolem_cache = Unsynchronized.ref true
-
-fun conditionally_saturate_skolem_cache thy =
- if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE
-
-
-(*** Converting a subgoal into negated conjecture clauses. ***)
-
-fun neg_skolemize_tac ctxt =
- EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
-
-val neg_clausify =
- single
- #> Meson.make_clauses_unsorted
- #> map introduce_combinators
- #> Meson.finish_cnf
-
-fun neg_conjecture_clauses ctxt st0 n =
- let
- (* "Option" is thrown if the assumptions contain schematic variables. *)
- val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
- val ({params, prems, ...}, _) =
- Subgoal.focus (Variable.set_body false ctxt) n st
- in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
-
-
-(** setup **)
-
-val setup =
- perhaps conditionally_saturate_skolem_cache
- #> Theory.at_end conditionally_saturate_skolem_cache
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Jun 28 10:39:39 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,361 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
- Author: Jia Meng, Cambridge University Computer Laboratory
- Author: Jasmin Blanchette, TU Muenchen
-
-Storing/printing FOL clauses and arity clauses. Typed equality is
-treated differently.
-
-FIXME: combine with sledgehammer_hol_clause!
-*)
-
-signature SLEDGEHAMMER_FOL_CLAUSE =
-sig
- val type_wrapper_name : string
- val schematic_var_prefix: string
- val fixed_var_prefix: string
- val tvar_prefix: string
- val tfree_prefix: string
- val const_prefix: string
- val tconst_prefix: string
- val class_prefix: string
- val union_all: ''a list list -> ''a list
- val const_trans_table: string Symtab.table
- val type_const_trans_table: string Symtab.table
- val ascii_of: string -> string
- val undo_ascii_of: string -> string
- val make_schematic_var : string * int -> string
- val make_fixed_var : string -> string
- val make_schematic_type_var : string * int -> string
- val make_fixed_type_var : string -> string
- val make_fixed_const : string -> string
- val make_fixed_type_const : string -> string
- val make_type_class : string -> string
- type name = string * string
- type name_pool = string Symtab.table * string Symtab.table
- val empty_name_pool : bool -> name_pool option
- val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
- val nice_name : name -> name_pool option -> string * name_pool option
- datatype kind = Axiom | Conjecture
- datatype type_literal =
- TyLitVar of string * name |
- TyLitFree of string * name
- exception CLAUSE of string * term
- val type_literals_for_types : typ list -> type_literal list
- datatype arLit =
- TConsLit of class * string * string list
- | TVarLit of class * string
- datatype arity_clause = ArityClause of
- {axiom_name: string, conclLit: arLit, premLits: arLit list}
- datatype classrel_clause = ClassrelClause of
- {axiom_name: string, subclass: class, superclass: class}
- val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
- val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
-end
-
-structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
-struct
-
-open Sledgehammer_Util
-
-val type_wrapper_name = "ti"
-
-val schematic_var_prefix = "V_";
-val fixed_var_prefix = "v_";
-
-val tvar_prefix = "T_";
-val tfree_prefix = "t_";
-
-val classrel_clause_prefix = "clsrel_";
-
-val const_prefix = "c_";
-val tconst_prefix = "tc_";
-val class_prefix = "class_";
-
-fun union_all xss = fold (union (op =)) xss []
-
-(* Readable names for the more common symbolic functions. Do not mess with the
- last nine entries of the table unless you know what you are doing. *)
-val const_trans_table =
- Symtab.make [(@{const_name "op ="}, "equal"),
- (@{const_name "op &"}, "and"),
- (@{const_name "op |"}, "or"),
- (@{const_name "op -->"}, "implies"),
- (@{const_name "op :"}, "in"),
- (@{const_name fequal}, "fequal"),
- (@{const_name COMBI}, "COMBI"),
- (@{const_name COMBK}, "COMBK"),
- (@{const_name COMBB}, "COMBB"),
- (@{const_name COMBC}, "COMBC"),
- (@{const_name COMBS}, "COMBS"),
- (@{const_name True}, "True"),
- (@{const_name False}, "False"),
- (@{const_name If}, "If")]
-
-val type_const_trans_table =
- Symtab.make [(@{type_name "*"}, "prod"),
- (@{type_name "+"}, "sum")]
-
-(*Escaping of special characters.
- Alphanumeric characters are left unchanged.
- The character _ goes to __
- Characters in the range ASCII space to / go to _A to _P, respectively.
- Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
-val A_minus_space = Char.ord #"A" - Char.ord #" ";
-
-fun stringN_of_int 0 _ = ""
- | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
-
-fun ascii_of_c c =
- if Char.isAlphaNum c then String.str c
- else if c = #"_" then "__"
- else if #" " <= c andalso c <= #"/"
- then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
- else if Char.isPrint c
- then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
- else ""
-
-val ascii_of = String.translate ascii_of_c;
-
-(** Remove ASCII armouring from names in proof files **)
-
-(*We don't raise error exceptions because this code can run inside the watcher.
- Also, the errors are "impossible" (hah!)*)
-fun undo_ascii_aux rcs [] = String.implode(rev rcs)
- | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*)
- (*Three types of _ escapes: __, _A to _P, _nnn*)
- | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
- | undo_ascii_aux rcs (#"_" :: c :: cs) =
- if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
- then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
- else
- let val digits = List.take (c::cs, 3) handle Subscript => []
- in
- case Int.fromString (String.implode digits) of
- NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*)
- | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
- end
- | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
-
-val undo_ascii_of = undo_ascii_aux [] o String.explode;
-
-(*Remove the initial ' character from a type variable, if it is present*)
-fun trim_type_var s =
- if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
- else error ("trim_type: Malformed type variable encountered: " ^ s);
-
-fun ascii_of_indexname (v,0) = ascii_of v
- | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
-
-fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
-fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
-
-fun make_schematic_type_var (x,i) =
- tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
-fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
-
-fun lookup_const c =
- case Symtab.lookup const_trans_table c of
- SOME c' => c'
- | NONE => ascii_of c
-
-fun lookup_type_const c =
- case Symtab.lookup type_const_trans_table c of
- SOME c' => c'
- | NONE => ascii_of c
-
-(* "op =" MUST BE "equal" because it's built into ATPs. *)
-fun make_fixed_const @{const_name "op ="} = "equal"
- | make_fixed_const c = const_prefix ^ lookup_const c
-
-fun make_fixed_type_const c = tconst_prefix ^ lookup_type_const c
-
-fun make_type_class clas = class_prefix ^ ascii_of clas;
-
-
-(**** name pool ****)
-
-type name = string * string
-type name_pool = string Symtab.table * string Symtab.table
-
-fun empty_name_pool readable_names =
- if readable_names then SOME (`I Symtab.empty) else NONE
-
-fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
-fun pool_map f xs =
- pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
-
-fun add_nice_name full_name nice_prefix j the_pool =
- let
- val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j)
- in
- case Symtab.lookup (snd the_pool) nice_name of
- SOME full_name' =>
- if full_name = full_name' then (nice_name, the_pool)
- else add_nice_name full_name nice_prefix (j + 1) the_pool
- | NONE =>
- (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool),
- Symtab.update_new (nice_name, full_name) (snd the_pool)))
- end
-
-fun translate_first_char f s =
- String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
-
-fun readable_name full_name s =
- let
- val s = s |> Long_Name.base_name
- |> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"]
- val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
- val s' =
- (s' |> rev
- |> implode
- |> String.translate
- (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
- else ""))
- ^ replicate_string (String.size s - length s') "_"
- val s' =
- if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
- else s'
- (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
- ("op &", "op |", etc.). *)
- val s' = if s' = "equal" orelse s' = "op" then full_name else s'
- in
- case (Char.isLower (String.sub (full_name, 0)),
- Char.isLower (String.sub (s', 0))) of
- (true, false) => translate_first_char Char.toLower s'
- | (false, true) => translate_first_char Char.toUpper s'
- | _ => s'
- end
-
-fun nice_name (full_name, _) NONE = (full_name, NONE)
- | nice_name (full_name, desired_name) (SOME the_pool) =
- case Symtab.lookup (fst the_pool) full_name of
- SOME nice_name => (nice_name, SOME the_pool)
- | NONE => add_nice_name full_name (readable_name full_name desired_name) 0
- the_pool
- |> apsnd SOME
-
-(**** Definitions and functions for FOL clauses for TPTP format output ****)
-
-datatype kind = Axiom | Conjecture;
-
-(**** Isabelle FOL clauses ****)
-
-(* The first component is the type class; the second is a TVar or TFree. *)
-datatype type_literal =
- TyLitVar of string * name |
- TyLitFree of string * name
-
-exception CLAUSE of string * term;
-
-(*Make literals for sorted type variables*)
-fun sorts_on_typs_aux (_, []) = []
- | sorts_on_typs_aux ((x,i), s::ss) =
- let val sorts = sorts_on_typs_aux ((x,i), ss)
- in
- if s = "HOL.type" then sorts
- else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
- else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
- end;
-
-fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
- | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
-
-(*Given a list of sorted type variables, return a list of type literals.*)
-fun type_literals_for_types Ts =
- fold (union (op =)) (map sorts_on_typs Ts) []
-
-(** make axiom and conjecture clauses. **)
-
-(**** Isabelle arities ****)
-
-datatype arLit = TConsLit of class * string * string list
- | TVarLit of class * string;
-
-datatype arity_clause =
- ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
-
-
-fun gen_TVars 0 = []
- | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
-
-fun pack_sort(_,[]) = []
- | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*)
- | pack_sort(tvar, cls::srt) = (cls, tvar) :: pack_sort(tvar, srt);
-
-(*Arity of type constructor tcon :: (arg1,...,argN)res*)
-fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
- let val tvars = gen_TVars (length args)
- val tvars_srts = ListPair.zip (tvars,args)
- in
- ArityClause {axiom_name = axiom_name,
- conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
- premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
- end;
-
-
-(**** Isabelle class relations ****)
-
-datatype classrel_clause =
- ClassrelClause of {axiom_name: string, subclass: class, superclass: class}
-
-(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
-fun class_pairs _ [] _ = []
- | class_pairs thy subs supers =
- let
- val class_less = Sorts.class_less (Sign.classes_of thy)
- fun add_super sub super = class_less (sub, super) ? cons (sub, super)
- fun add_supers sub = fold (add_super sub) supers
- in fold add_supers subs [] end
-
-fun make_classrel_clause (sub,super) =
- ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
- ascii_of super,
- subclass = make_type_class sub,
- superclass = make_type_class super};
-
-fun make_classrel_clauses thy subs supers =
- map make_classrel_clause (class_pairs thy subs supers);
-
-
-(** Isabelle arities **)
-
-fun arity_clause _ _ (_, []) = []
- | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
- arity_clause seen n (tcons,ars)
- | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
- if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
- make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
- arity_clause seen (n+1) (tcons,ars)
- else
- make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) ::
- arity_clause (class::seen) n (tcons,ars)
-
-fun multi_arity_clause [] = []
- | multi_arity_clause ((tcons, ars) :: tc_arlists) =
- arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
-
-(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
- provided its arguments have the corresponding sorts.*)
-fun type_class_pairs thy tycons classes =
- let val alg = Sign.classes_of thy
- fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
- fun add_class tycon class =
- cons (class, domain_sorts tycon class)
- handle Sorts.CLASS_ERROR _ => I
- fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
- in map try_classes tycons end;
-
-(*Proving one (tycon, class) membership may require proving others, so iterate.*)
-fun iter_type_class_pairs _ _ [] = ([], [])
- | iter_type_class_pairs thy tycons classes =
- let val cpairs = type_class_pairs thy tycons classes
- val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
- |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
- val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
- in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
-
-fun make_arity_clauses thy tycons classes =
- let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
- in (classes', multi_arity_clause cpairs) end;
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Jun 28 10:39:39 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,231 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
- Author: Jia Meng, NICTA
- Author: Jasmin Blanchette, TU Muenchen
-
-FOL clauses translated from HOL formulas.
-*)
-
-signature SLEDGEHAMMER_HOL_CLAUSE =
-sig
- type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
- type name = Sledgehammer_FOL_Clause.name
- type name_pool = Sledgehammer_FOL_Clause.name_pool
- type kind = Sledgehammer_FOL_Clause.kind
- type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
- type arity_clause = Sledgehammer_FOL_Clause.arity_clause
- type polarity = bool
-
- datatype combtyp =
- TyVar of name |
- TyFree of name |
- TyConstr of name * combtyp list
- datatype combterm =
- CombConst of name * combtyp * combtyp list (* Const and Free *) |
- CombVar of name * combtyp |
- CombApp of combterm * combterm
- datatype literal = Literal of polarity * combterm
- datatype hol_clause =
- HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
- literals: literal list, ctypes_sorts: typ list}
-
- val type_of_combterm : combterm -> combtyp
- val strip_combterm_comb : combterm -> combterm * combterm list
- val literals_of_term : theory -> term -> literal list * typ list
- val conceal_skolem_somes :
- int -> (string * term) list -> term -> (string * term) list * term
- exception TRIVIAL of unit
- val make_conjecture_clauses : theory -> thm list -> hol_clause list
- val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list
-end
-
-structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
-struct
-
-open Sledgehammer_Util
-open Sledgehammer_FOL_Clause
-open Sledgehammer_Fact_Preprocessor
-
-(******************************************************)
-(* data types for typed combinator expressions *)
-(******************************************************)
-
-type polarity = bool
-
-datatype combtyp =
- TyVar of name |
- TyFree of name |
- TyConstr of name * combtyp list
-
-datatype combterm =
- CombConst of name * combtyp * combtyp list (* Const and Free *) |
- CombVar of name * combtyp |
- CombApp of combterm * combterm
-
-datatype literal = Literal of polarity * combterm;
-
-datatype hol_clause =
- HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
- literals: literal list, ctypes_sorts: typ list}
-
-(*********************************************************************)
-(* convert a clause with type Term.term to a clause with type clause *)
-(*********************************************************************)
-
-(*Result of a function type; no need to check that the argument type matches.*)
-fun result_type (TyConstr (_, [_, tp2])) = tp2
- | result_type _ = raise Fail "non-function type"
-
-fun type_of_combterm (CombConst (_, tp, _)) = tp
- | type_of_combterm (CombVar (_, tp)) = tp
- | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
-
-(*gets the head of a combinator application, along with the list of arguments*)
-fun strip_combterm_comb u =
- let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
- | stripc x = x
- in stripc(u,[]) end
-
-fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
- (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
- | isFalse _ = false;
-
-fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
- (pol andalso c = "c_True") orelse
- (not pol andalso c = "c_False")
- | isTrue _ = false;
-
-fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
-
-fun type_of (Type (a, Ts)) =
- let val (folTypes,ts) = types_of Ts in
- (TyConstr (`make_fixed_type_const a, folTypes), ts)
- end
- | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
- | type_of (tp as TVar (x, _)) =
- (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
-and types_of Ts =
- let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
- (folTyps, union_all ts)
- end
-
-(* same as above, but no gathering of sort information *)
-fun simp_type_of (Type (a, Ts)) =
- TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
- | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
- | simp_type_of (TVar (x, _)) =
- TyVar (make_schematic_type_var x, string_of_indexname x)
-
-(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
-fun combterm_of thy (Const (c, T)) =
- let
- val (tp, ts) = type_of T
- val tvar_list =
- (if String.isPrefix skolem_theory_name c then
- [] |> Term.add_tvarsT T |> map TVar
- else
- (c, T) |> Sign.const_typargs thy)
- |> map simp_type_of
- val c' = CombConst (`make_fixed_const c, tp, tvar_list)
- in (c',ts) end
- | combterm_of _ (Free(v, T)) =
- let val (tp,ts) = type_of T
- val v' = CombConst (`make_fixed_var v, tp, [])
- in (v',ts) end
- | combterm_of _ (Var(v, T)) =
- let val (tp,ts) = type_of T
- val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
- in (v',ts) end
- | combterm_of thy (P $ Q) =
- let val (P', tsP) = combterm_of thy P
- val (Q', tsQ) = combterm_of thy Q
- in (CombApp (P', Q'), union (op =) tsP tsQ) end
- | combterm_of _ (t as Abs _) = raise CLAUSE ("HOL clause", t)
-
-fun predicate_of thy ((@{const Not} $ P), polarity) =
- predicate_of thy (P, not polarity)
- | predicate_of thy (t, polarity) =
- (combterm_of thy (Envir.eta_contract t), polarity)
-
-fun literals_of_term1 args thy (@{const Trueprop} $ P) =
- literals_of_term1 args thy P
- | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
- literals_of_term1 (literals_of_term1 args thy P) thy Q
- | literals_of_term1 (lits, ts) thy P =
- let val ((pred, ts'), pol) = predicate_of thy (P, true) in
- (Literal (pol, pred) :: lits, union (op =) ts ts')
- end
-val literals_of_term = literals_of_term1 ([], [])
-
-fun skolem_name i j num_T_args =
- skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
- skolem_infix ^ "g"
-
-fun conceal_skolem_somes i skolem_somes t =
- if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
- let
- fun aux skolem_somes
- (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
- let
- val (skolem_somes, s) =
- if i = ~1 then
- (skolem_somes, @{const_name undefined})
- else case AList.find (op aconv) skolem_somes t of
- s :: _ => (skolem_somes, s)
- | [] =>
- let
- val s = skolem_theory_name ^ "." ^
- skolem_name i (length skolem_somes)
- (length (Term.add_tvarsT T []))
- in ((s, t) :: skolem_somes, s) end
- in (skolem_somes, Const (s, T)) end
- | aux skolem_somes (t1 $ t2) =
- let
- val (skolem_somes, t1) = aux skolem_somes t1
- val (skolem_somes, t2) = aux skolem_somes t2
- in (skolem_somes, t1 $ t2) end
- | aux skolem_somes (Abs (s, T, t')) =
- let val (skolem_somes, t') = aux skolem_somes t' in
- (skolem_somes, Abs (s, T, t'))
- end
- | aux skolem_somes t = (skolem_somes, t)
- in aux skolem_somes t end
- else
- (skolem_somes, t)
-
-(* Trivial problem, which resolution cannot handle (empty clause) *)
-exception TRIVIAL of unit
-
-(* making axiom and conjecture clauses *)
-fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
- let
- val (skolem_somes, t) =
- th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
- val (lits, ctypes_sorts) = literals_of_term thy t
- in
- if forall isFalse lits then
- raise TRIVIAL ()
- else
- (skolem_somes,
- HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
- kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
- end
-
-fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
- let
- val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
- in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
-
-fun make_axiom_clauses thy clauses =
- ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
-
-fun make_conjecture_clauses thy =
- let
- fun aux _ _ [] = []
- | aux n skolem_somes (th :: ths) =
- let
- val (skolem_somes, cls) =
- make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
- in cls :: aux (n + 1) skolem_somes ths end
- in aux 0 [] end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 28 13:36:21 2010 +0200
@@ -17,9 +17,8 @@
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
struct
+open Clausifier
open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
-open Sledgehammer_Fact_Preprocessor
open ATP_Manager
open ATP_Systems
open Sledgehammer_Fact_Minimizer
@@ -69,7 +68,6 @@
("verbose", "false"),
("overlord", "false"),
("explicit_apply", "false"),
- ("respect_no_atp", "true"),
("relevance_threshold", "50"),
("relevance_convergence", "320"),
("theory_relevant", "smart"),
@@ -86,7 +84,6 @@
("no_overlord", "overlord"),
("partial_types", "full_types"),
("implicit_apply", "explicit_apply"),
- ("ignore_no_atp", "respect_no_atp"),
("theory_irrelevant", "theory_relevant"),
("defs_irrelevant", "defs_relevant"),
("no_isar_proof", "isar_proof")]
@@ -168,7 +165,6 @@
val atps = lookup_string "atps" |> space_explode " "
val full_types = lookup_bool "full_types"
val explicit_apply = lookup_bool "explicit_apply"
- val respect_no_atp = lookup_bool "respect_no_atp"
val relevance_threshold =
0.01 * Real.fromInt (lookup_int "relevance_threshold")
val relevance_convergence =
@@ -182,7 +178,7 @@
in
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
- respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
+ relevance_threshold = relevance_threshold,
relevance_convergence = relevance_convergence,
theory_relevant = theory_relevant, defs_relevant = defs_relevant,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
@@ -203,13 +199,10 @@
0 => priority "No subgoal!"
| n =>
let
- val birth_time = Time.now ()
- val death_time = Time.+ (birth_time, timeout)
val _ = kill_atps ()
val _ = priority "Sledgehammering..."
- val _ = app (start_prover_thread params birth_time death_time i n
- relevance_override minimize_command
- state) atps
+ val _ = app (start_prover_thread params i n relevance_override
+ minimize_command state) atps
in () end
fun minimize override_params i refs state =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jun 28 13:36:21 2010 +0200
@@ -8,12 +8,8 @@
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
sig
type minimize_command = string list -> string
- type name_pool = Sledgehammer_FOL_Clause.name_pool
+ type name_pool = Metis_Clauses.name_pool
- val invert_const: string -> string
- val invert_type_const: string -> string
- val num_type_args: theory -> string -> int
- val strip_prefix: string -> string -> string option
val metis_line: bool -> int -> int -> string list -> string
val metis_proof_text:
bool * minimize_command * string * string vector * thm * int
@@ -31,10 +27,9 @@
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
struct
+open Clausifier
+open Metis_Clauses
open Sledgehammer_Util
-open Sledgehammer_FOL_Clause
-open Sledgehammer_HOL_Clause
-open Sledgehammer_Fact_Preprocessor
type minimize_command = string list -> string
@@ -212,28 +207,13 @@
exception NODE of node list
-(*If string s has the prefix s1, return the result of deleting it.*)
-fun strip_prefix s1 s =
- if String.isPrefix s1 s
- then SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
- else NONE;
-
-(*Invert the table of translations between Isabelle and ATPs*)
-val type_const_trans_table_inv =
- Symtab.make (map swap (Symtab.dest type_const_trans_table));
-
-fun invert_type_const c =
- case Symtab.lookup type_const_trans_table_inv c of
- SOME c' => c'
- | NONE => c;
-
(* Type variables are given the basic sort "HOL.type". Some will later be
constrained by information from type literals, or by type inference. *)
fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
| type_from_node tfrees (u as StrNode (a, us)) =
let val Ts = map (type_from_node tfrees) us in
case strip_prefix tconst_prefix a of
- SOME b => Type (invert_type_const b, Ts)
+ SOME b => Type (invert_const b, Ts)
| NONE =>
if not (null us) then
raise NODE [u] (* only "tconst"s have type arguments *)
@@ -250,24 +230,6 @@
Type_Infer.param 0 (a, HOLogic.typeS)
end
-(*Invert the table of translations between Isabelle and ATPs*)
-val const_trans_table_inv =
- Symtab.update ("fequal", @{const_name "op ="})
- (Symtab.make (map swap (Symtab.dest const_trans_table)))
-
-fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
-
-(* The number of type arguments of a constant, zero if it's monomorphic. For
- (instances of) Skolem pseudoconstants, this information is encoded in the
- constant name. *)
-fun num_type_args thy s =
- if String.isPrefix skolem_theory_name s then
- s |> unprefix skolem_theory_name
- |> space_explode skolem_infix |> hd
- |> space_explode "_" |> List.last |> Int.fromString |> the
- else
- (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-
fun fix_atp_variable_name s =
let
fun subscript_name s n = s ^ nat_subscript n
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jun 28 13:36:21 2010 +0200
@@ -7,11 +7,11 @@
signature SLEDGEHAMMER_TPTP_FORMAT =
sig
- type name_pool = Sledgehammer_FOL_Clause.name_pool
- type type_literal = Sledgehammer_FOL_Clause.type_literal
- type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
- type arity_clause = Sledgehammer_FOL_Clause.arity_clause
- type hol_clause = Sledgehammer_HOL_Clause.hol_clause
+ type name_pool = Metis_Clauses.name_pool
+ type type_literal = Metis_Clauses.type_literal
+ type classrel_clause = Metis_Clauses.classrel_clause
+ type arity_clause = Metis_Clauses.arity_clause
+ type hol_clause = Metis_Clauses.hol_clause
val tptp_of_type_literal :
bool -> type_literal -> name_pool option -> string * name_pool option
@@ -25,9 +25,8 @@
structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
struct
+open Metis_Clauses
open Sledgehammer_Util
-open Sledgehammer_FOL_Clause
-open Sledgehammer_HOL_Clause
type const_info = {min_arity: int, max_arity: int, sub_level: bool}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Jun 28 10:39:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Jun 28 13:36:21 2010 +0200
@@ -8,8 +8,6 @@
sig
val plural_s : int -> string
val serial_commas : string -> string list -> string list
- val replace_all : string -> string -> string -> string
- val remove_all : string -> string -> string
val timestamp : unit -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
@@ -31,17 +29,6 @@
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-fun replace_all bef aft =
- let
- fun aux seen "" = String.implode (rev seen)
- | aux seen s =
- if String.isPrefix bef s then
- aux seen "" ^ aft ^ aux [] (unprefix bef s)
- else
- aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
- in aux [] end
-fun remove_all bef = replace_all bef ""
-
val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
fun parse_bool_option option name s =