# HG changeset patch # User blanchet # Date 1277708146 -7200 # Node ID a209fff747920764f3ebff21d1fc24b481b50d93 # Parent 19fca77829eac43fc82782621bb1422604d6c806# Parent c2ed8112ce57fc3d999969a44d85a34ed6b01aac merged diff -r 19fca77829ea -r a209fff74792 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Sun Jun 27 08:33:01 2010 +0100 +++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 28 08:55:46 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} diff -r 19fca77829ea -r a209fff74792 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/IsaMakefile Mon Jun 28 08:55:46 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 \ diff -r 19fca77829ea -r a209fff74792 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 28 08:55:46 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)) diff -r 19fca77829ea -r a209fff74792 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/Sledgehammer.thy Mon Jun 28 08:55:46 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 \ '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 diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/ATP_Manager/async_manager.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP_Manager/async_manager.ML Mon Jun 28 08:55:46 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; diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jun 28 08:55:46 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; diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 28 08:55:46 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 diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/clausifier.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Jun 28 08:55:46 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; diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/meson_tactic.ML --- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Mon Jun 28 08:55:46 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 => diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/metis_clauses.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Jun 28 08:55:46 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; diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 28 08:55:46 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 diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jun 28 08:55:46 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; diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Jun 28 08:55:46 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 diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Jun 27 08:33:01 2010 +0100 +++ /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; diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Sun Jun 27 08:33:01 2010 +0100 +++ /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; diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Sun Jun 27 08:33:01 2010 +0100 +++ /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; diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 28 08:55:46 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 = diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jun 28 08:55:46 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 diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jun 28 08:55:46 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} diff -r 19fca77829ea -r a209fff74792 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Jun 27 08:33:01 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Jun 28 08:55:46 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 =