# HG changeset patch # User blanchet # Date 1277281254 -7200 # Node ID 4dca51ef0285e0f6c792232b88ffc5b3958d5f6a # Parent 6e9f48cf6adf09bd552afa2544c99a1a49976ced# Parent ff72d3ddc898f857c9e1043413949685946145c8 merged diff -r 6e9f48cf6adf -r 4dca51ef0285 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Wed Jun 23 10:05:13 2010 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Jun 23 10:20:54 2010 +0200 @@ -341,11 +341,6 @@ download page. Sledgehammer requires version 3.5 or above. See \S\ref{installation} for details. -\item[$\bullet$] \textbf{\textit{spass\_dfg}:} Same as the above, except that -Sledgehammer communicates with SPASS using the native DFG syntax rather than the -TPTP syntax. Sledgehammer requires version 3.0 or above. This ATP is provided -for compatibility reasons. - \item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/IsaMakefile Wed Jun 23 10:20:54 2010 +0200 @@ -322,6 +322,7 @@ Tools/Sledgehammer/sledgehammer_hol_clause.ML \ Tools/Sledgehammer/sledgehammer_isar.ML \ Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \ + Tools/Sledgehammer/sledgehammer_tptp_format.ML \ Tools/Sledgehammer/sledgehammer_util.ML \ Tools/SMT/cvc3_solver.ML \ Tools/SMT/smtlib_interface.ML \ diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jun 23 10:20:54 2010 +0200 @@ -299,6 +299,7 @@ fun run_sh prover hard_timeout timeout dir st = let + val _ = Sledgehammer_Fact_Filter.use_natural_form := true (* experimental *) val {context = ctxt, facts, goal} = Proof.goal st val thy = ProofContext.theory_of ctxt val change_dir = (fn SOME d => Config.put ATP_Systems.dest_dir d | _ => I) @@ -324,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 Sledgehammer_HOL_Clause.TRIVIAL () => ("trivial", SH_OK (0, 0, [])) | ERROR msg => ("error: " ^ msg, SH_ERROR) | TimeLimit.TimeOut => ("timeout", SH_ERROR) diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Nitpick_Examples/Mini_Nits.thy --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Wed Jun 23 10:20:54 2010 +0200 @@ -14,14 +14,19 @@ ML {* exception FAIL -(* int -> term -> string *) +val has_kodkodi = (getenv "KODKODI" <> "") + fun minipick n t = map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n) |> Minipick.solve_any_kodkod_problem @{theory} -(* int -> term -> bool *) -fun none n t = (minipick n t = "none" orelse raise FAIL) -fun genuine n t = (minipick n t = "genuine" orelse raise FAIL) -fun unknown n t = (minipick n t = "unknown" orelse raise FAIL) +fun minipick_expect expect n t = + if has_kodkodi then + if minipick n t = expect then () else raise FAIL + else + () +val none = minipick_expect "none" +val genuine = minipick_expect "genuine" +val unknown = minipick_expect "unknown" *} ML {* genuine 1 @{prop "x = Not"} *} diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Nitpick_Examples/ROOT.ML --- a/src/HOL/Nitpick_Examples/ROOT.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Nitpick_Examples/ROOT.ML Wed Jun 23 10:20:54 2010 +0200 @@ -5,8 +5,4 @@ Nitpick examples. *) -if getenv "KODKODI" = "" then - () -else - setmp_noncritical quick_and_dirty true use_thys - ["Nitpick_Examples"]; +setmp_noncritical quick_and_dirty true use_thys ["Nitpick_Examples"]; diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Nitpick_Examples/Tests_Nits.thy --- a/src/HOL/Nitpick_Examples/Tests_Nits.thy Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy Wed Jun 23 10:20:54 2010 +0200 @@ -11,6 +11,6 @@ imports Main begin -ML {* Nitpick_Tests.run_all_tests () *} +ML {* () |> getenv "KODKODI" <> "" ? Nitpick_Tests.run_all_tests *} end diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Wed Jun 23 10:20:54 2010 +0200 @@ -17,6 +17,7 @@ ("Tools/Sledgehammer/sledgehammer_hol_clause.ML") ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML") ("Tools/Sledgehammer/sledgehammer_fact_filter.ML") + ("Tools/Sledgehammer/sledgehammer_tptp_format.ML") ("Tools/ATP_Manager/atp_manager.ML") ("Tools/ATP_Manager/atp_systems.ML") ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML") @@ -103,12 +104,12 @@ use "Tools/Sledgehammer/sledgehammer_hol_clause.ML" use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML" use "Tools/Sledgehammer/sledgehammer_fact_filter.ML" +use "Tools/Sledgehammer/sledgehammer_tptp_format.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" -setup Sledgehammer_Isar.setup subsection {* The MESON prover *} diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Jun 23 10:20:54 2010 +0200 @@ -8,7 +8,8 @@ signature ATP_MANAGER = sig - type name_pool = Sledgehammer_HOL_Clause.name_pool + type name_pool = Sledgehammer_FOL_Clause.name_pool + type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm type relevance_override = Sledgehammer_Fact_Filter.relevance_override type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command type params = @@ -31,8 +32,8 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: (thm * (string * int)) list option, - filtered_clauses: (thm * (string * int)) list option} + axiom_clauses: cnf_thm list option, + filtered_clauses: cnf_thm list option} datatype failure = Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError @@ -46,7 +47,7 @@ proof: string, internal_thm_names: string Vector.vector, conjecture_shape: int list list, - filtered_clauses: (thm * (string * int)) list} + filtered_clauses: cnf_thm list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result @@ -66,6 +67,7 @@ open Sledgehammer_Util open Sledgehammer_Fact_Filter +open Sledgehammer_HOL_Clause open Sledgehammer_Proof_Reconstruct (** problems, results, provers, etc. **) @@ -91,8 +93,8 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: (thm * (string * int)) list option, - filtered_clauses: (thm * (string * int)) list option}; + axiom_clauses: cnf_thm list option, + filtered_clauses: cnf_thm list option} datatype failure = Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass | @@ -108,7 +110,7 @@ proof: string, internal_thm_names: string Vector.vector, conjecture_shape: int list list, - filtered_clauses: (thm * (string * int)) list}; + filtered_clauses: cnf_thm list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result @@ -354,7 +356,7 @@ filtered_clauses = NONE} val message = #message (prover params (minimize_command name) timeout problem) - handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line full_types i n [] + handle TRIVIAL () => metis_line full_types i n [] | ERROR message => "Error: " ^ message ^ "\n" val _ = unregister params message (Thread.self ()); in () end) diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jun 23 10:20:54 2010 +0200 @@ -27,6 +27,7 @@ open Sledgehammer_HOL_Clause open Sledgehammer_Fact_Filter open Sledgehammer_Proof_Reconstruct +open Sledgehammer_TPTP_Format open ATP_Manager (** generic ATP **) @@ -110,33 +111,39 @@ fun shape_of_clauses _ [] = [] | shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses - | shape_of_clauses j ((lit :: lits) :: clauses) = + | shape_of_clauses j ((_ :: lits) :: clauses) = let val shape = shape_of_clauses (j + 1) (lits :: clauses) in (j :: hd shape) :: tl shape end -fun generic_prover overlord get_facts prepare write_file home_var executable - args proof_delims known_failures name - ({debug, full_types, explicit_apply, isar_proof, isar_shrink_factor, - ...} : params) minimize_command +(* generic TPTP-based provers *) + +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) + minimize_command timeout ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} : problem) = let (* get clauses and prepare them for writing *) - val (ctxt, (chained_ths, th)) = goal; + val (ctxt, (_, th)) = goal; val thy = ProofContext.theory_of ctxt; val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal) val goal_cls = List.concat goal_clss val the_filtered_clauses = (case filtered_clauses of - NONE => get_facts relevance_override goal goal_cls + NONE => relevant_facts full_types respect_no_atp relevance_threshold + relevance_convergence defs_relevant max_axiom_clauses + (the_default prefers_theory_relevant theory_relevant) + relevance_override goal goal_cls | SOME fcls => fcls); - val the_axiom_clauses = - (case axiom_clauses of - NONE => the_filtered_clauses - | SOME axcls => axcls); + val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses val (internal_thm_names, clauses) = - prepare goal_cls chained_ths the_axiom_clauses the_filtered_clauses thy; + prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses + thy (* path to unique problem file *) val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" @@ -161,10 +168,10 @@ fun command_line probfile = (if Config.get ctxt measure_runtime then "TIMEFORMAT='%3U'; { time " ^ - space_implode " " [File.shell_path command, args, + space_implode " " [File.shell_path command, arguments timeout, File.shell_path probfile] ^ " ; } 2>&1" else - space_implode " " ["exec", File.shell_path command, args, + space_implode " " ["exec", File.shell_path command, arguments timeout, File.shell_path probfile, "2>&1"]) ^ (if overlord then " | sed 's/,/, /g' \ @@ -185,11 +192,12 @@ val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; in (output, as_time t) end; - fun split_time' s = - if Config.get ctxt measure_runtime then split_time s else (s, 0) + val split_time' = + if Config.get ctxt measure_runtime then split_time else rpair 0 fun run_on probfile = if File.exists command then - write_file full_types explicit_apply probfile clauses + write_tptp_file (debug andalso overlord) full_types explicit_apply + probfile clauses |> pair (apfst split_time' (bash_output (command_line probfile))) else if home = "" then error ("The environment variable " ^ quote home_var ^ " is not set.") @@ -233,58 +241,12 @@ proof = proof, internal_thm_names = internal_thm_names, conjecture_shape = conjecture_shape, filtered_clauses = the_filtered_clauses} - end; - - -(* generic TPTP-based provers *) - -fun generic_tptp_prover - (name, {home_var, executable, arguments, proof_delims, known_failures, - max_axiom_clauses, prefers_theory_relevant}) - (params as {debug, overlord, full_types, respect_no_atp, - relevance_threshold, relevance_convergence, theory_relevant, - defs_relevant, isar_proof, ...}) - minimize_command timeout = - generic_prover overlord - (relevant_facts full_types respect_no_atp relevance_threshold - relevance_convergence defs_relevant max_axiom_clauses - (the_default prefers_theory_relevant theory_relevant)) - (prepare_clauses false full_types) - (write_tptp_file (debug andalso overlord)) home_var - executable (arguments timeout) proof_delims known_failures name params - minimize_command + end fun tptp_prover name p = (name, generic_tptp_prover (name, p)); - -(** common provers **) - fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000 -(* Vampire *) - -(* Vampire requires an explicit time limit. *) - -val vampire_config : prover_config = - {home_var = "VAMPIRE_HOME", - executable = "vampire", - arguments = fn timeout => - "--output_syntax tptp --mode casc -t " ^ - string_of_int (to_generous_secs timeout), - proof_delims = - [("=========== Refutation ==========", - "======= End of refutation ======="), - ("% SZS output start Refutation", "% SZS output end Refutation")], - known_failures = - [(Unprovable, "UNPROVABLE"), - (IncompleteUnprovable, "CANNOT PROVE"), - (Unprovable, "Satisfiability detected"), - (OutOfResources, "Refutation not found")], - max_axiom_clauses = 60, - prefers_theory_relevant = false} -val vampire = tptp_prover "vampire" vampire_config - - (* E prover *) val tstp_proof_delims = @@ -311,33 +273,14 @@ val e = tptp_prover "e" e_config -(* SPASS *) - -fun generic_dfg_prover - (name, {home_var, executable, arguments, proof_delims, known_failures, - max_axiom_clauses, prefers_theory_relevant}) - (params as {overlord, full_types, respect_no_atp, relevance_threshold, - relevance_convergence, theory_relevant, defs_relevant, ...}) - minimize_command timeout = - generic_prover overlord - (relevant_facts full_types respect_no_atp relevance_threshold - relevance_convergence defs_relevant max_axiom_clauses - (the_default prefers_theory_relevant theory_relevant)) - (prepare_clauses true full_types) write_dfg_file home_var executable - (arguments timeout) proof_delims known_failures name params - minimize_command - -fun dfg_prover name p = (name, generic_dfg_prover (name, p)) - (* The "-VarWeight=3" option helps the higher-order problems, probably by counteracting the presence of "hAPP". *) -fun generic_spass_config dfg : prover_config = +val spass_config : prover_config = {home_var = "SPASS_HOME", executable = "SPASS", arguments = fn timeout => - "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ - \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout) - |> not dfg ? prefix "-TPTP ", + "-TPTP -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ + \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout), proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = [(IncompleteUnprovable, "SPASS beiseite: Completion found"), @@ -349,13 +292,30 @@ (OldSpass, "Unrecognized option TPTP")], max_axiom_clauses = 40, prefers_theory_relevant = true} -val spass_dfg_config = generic_spass_config true -val spass_dfg = dfg_prover "spass_dfg" spass_dfg_config - -val spass_config = generic_spass_config false val spass = tptp_prover "spass" spass_config -(* remote prover invocation via SystemOnTPTP *) +(* Vampire *) + +val vampire_config : prover_config = + {home_var = "VAMPIRE_HOME", + executable = "vampire", + arguments = fn timeout => + "--output_syntax tptp --mode casc -t " ^ + string_of_int (to_generous_secs timeout), + proof_delims = + [("=========== Refutation ==========", + "======= End of refutation ======="), + ("% SZS output start Refutation", "% SZS output end Refutation")], + known_failures = + [(Unprovable, "UNPROVABLE"), + (IncompleteUnprovable, "CANNOT PROVE"), + (Unprovable, "Satisfiability detected"), + (OutOfResources, "Refutation not found")], + max_axiom_clauses = 60, + prefers_theory_relevant = false} +val vampire = tptp_prover "vampire" vampire_config + +(* Remote prover invocation via SystemOnTPTP *) val systems = Synchronized.var "atp_systems" ([]: string list); @@ -366,7 +326,7 @@ error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer) fun refresh_systems_on_tptp () = - Synchronized.change systems (fn _ => get_systems ()); + Synchronized.change systems (fn _ => get_systems ()) fun get_system prefix = Synchronized.change_result systems (fn systems => (if null systems then get_systems () else systems) @@ -374,15 +334,14 @@ fun the_system prefix = (case get_system prefix of - NONE => error ("System " ^ quote prefix ^ - " not available at SystemOnTPTP.") + NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.") | SOME sys => sys); val remote_known_failures = [(TimedOut, "says Timeout"), (MalformedOutput, "Remote script could not extract proof")] -fun remote_prover_config atp_prefix args +fun remote_config atp_prefix args ({proof_delims, known_failures, max_axiom_clauses, prefers_theory_relevant, ...} : prover_config) : prover_config = {home_var = "ISABELLE_ATP_MANAGER", @@ -395,17 +354,12 @@ max_axiom_clauses = max_axiom_clauses, prefers_theory_relevant = prefers_theory_relevant} -val remote_vampire = - tptp_prover (remotify (fst vampire)) - (remote_prover_config "Vampire---9" "" vampire_config) +fun remote_tptp_prover prover atp_prefix args config = + tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config) -val remote_e = - tptp_prover (remotify (fst e)) - (remote_prover_config "EP---" "" e_config) - -val remote_spass = - tptp_prover (remotify (fst spass)) - (remote_prover_config "SPASS---" "-x" spass_config) +val remote_e = remote_tptp_prover e "EP---" "" e_config +val remote_spass = remote_tptp_prover spass "SPASS---" "-x" spass_config +val remote_vampire = remote_tptp_prover vampire "Vampire---9" "" vampire_config fun maybe_remote (name, _) ({home_var, ...} : prover_config) = name |> getenv home_var = "" ? remotify @@ -414,8 +368,7 @@ space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config, remotify (fst vampire)] -val provers = - [spass, spass_dfg, vampire, e, remote_vampire, remote_spass, remote_e] +val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire] val prover_setup = fold add_prover provers val setup = diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Jun 23 10:20:54 2010 +0200 @@ -943,15 +943,15 @@ fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n step subst orig_assm_ts orig_t = - let - val warning_m = if auto then K () else warning - val unknown_outcome = ("unknown", state) - in + let val warning_m = if auto then K () else warning in if getenv "KODKODI" = "" then + (* The "expect" argument is deliberately ignored if Kodkodi is missing so + that the "Nitpick_Examples" can be processed on any machine. *) (warning_m (Pretty.string_of (plazy install_kodkodi_message)); - unknown_outcome) + ("no_kodkodi", state)) else let + val unknown_outcome = ("unknown", state) val deadline = Option.map (curry Time.+ (Time.now ())) timeout val outcome as (outcome_code, _) = time_limit (if debug then NONE else timeout) diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/Sledgehammer/meson_tactic.ML --- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Wed Jun 23 10:20:54 2010 +0200 @@ -17,11 +17,11 @@ 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, _) $ u) = +fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) = String.isPrefix skolem_prefix a | is_absko _ = false; -fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ u) = (*Definition of Free, not in certain terms*) +fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ _) = (*Definition of Free, not in certain terms*) is_Free t andalso not (member (op aconv) xs t) | is_okdef _ _ = false diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Jun 23 10:20:54 2010 +0200 @@ -24,6 +24,7 @@ open Sledgehammer_HOL_Clause open Sledgehammer_Proof_Reconstruct open Sledgehammer_Fact_Filter +open Sledgehammer_TPTP_Format val trace = Unsynchronized.ref false; fun trace_msg msg = if !trace then tracing (msg ()) else (); @@ -58,7 +59,7 @@ (* Finding the relative location of an untyped term within a list of terms *) fun get_index lit = let val lit = Envir.eta_contract lit - fun get n [] = raise Empty + fun get _ [] = raise Empty | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then n else get (n+1) xs in get 1 end; @@ -238,7 +239,7 @@ | NONE => raise Fail ("fol_type_to_isa: " ^ x)); fun reveal_skolem_somes skolem_somes = - map_aterms (fn t as Const (s, T) => + map_aterms (fn t as Const (s, _) => if String.isPrefix skolem_theory_name s then AList.lookup (op =) skolem_somes s |> the |> map_types Type_Infer.paramify_vars @@ -348,8 +349,7 @@ | hol_term_from_fol _ = hol_term_from_fol_PT fun hol_terms_from_fol ctxt mode skolem_somes fol_tms = - let val thy = ProofContext.theory_of ctxt - val ts = map (hol_term_from_fol mode ctxt) fol_tms + let val ts = map (hol_term_from_fol mode ctxt) fol_tms val _ = trace_msg (fn () => " calling type inference:") val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts val ts' = ts |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt @@ -694,11 +694,10 @@ tfrees = union (op =) tfree_lits tfrees, skolem_somes = skolem_somes} end; - val lmap as {skolem_somes, ...} = - {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []} - |> fold (add_thm true) cls - |> add_tfrees - |> fold (add_thm false) ths + val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []} + |> fold (add_thm true) cls + |> add_tfrees + |> fold (add_thm false) ths val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) fun is_used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Jun 23 10:20:54 2010 +0200 @@ -5,17 +5,17 @@ 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 axiom_name = Sledgehammer_HOL_Clause.axiom_name type hol_clause = Sledgehammer_HOL_Clause.hol_clause - type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id type relevance_override = {add: Facts.ref list, del: Facts.ref list, 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 @@ -24,15 +24,12 @@ val is_quasi_fol_term : theory -> term -> bool val relevant_facts : bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override - -> Proof.context * (thm list * 'a) -> thm list - -> (thm * (string * int)) list + -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list val prepare_clauses : - bool -> bool -> thm list -> thm list - -> (thm * (axiom_name * hol_clause_id)) list - -> (thm * (axiom_name * hol_clause_id)) list -> theory - -> axiom_name vector - * (hol_clause list * hol_clause list * hol_clause list * - hol_clause list * classrel_clause list * arity_clause list) + 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 = @@ -42,6 +39,9 @@ open Sledgehammer_Fact_Preprocessor open Sledgehammer_HOL_Clause +(* Experimental feature: Filter theorems in natural form or in CNF? *) +val use_natural_form = Unsynchronized.ref false + type relevance_override = {add: Facts.ref list, del: Facts.ref list, @@ -54,36 +54,13 @@ fun strip_Trueprop (@{const Trueprop} $ t) = t | strip_Trueprop t = t; -(*A surprising number of theorems contain only a few significant constants. - These include all induction rules, and other general theorems. Filtering - theorems in clause form reveals these complexities in the form of Skolem - functions. If we were instead to filter theorems in their natural form, - some other method of measuring theorem complexity would become necessary.*) - -fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0); - -(*The default seems best in practice. A constant function of one ignores - the constant frequencies.*) -val weight_fn = log_weight2; - - -(*Including equality in this list might be expected to stop rules like subset_antisym from - being chosen, but for some reason filtering works better with them listed. The - logical signs All, Ex, &, and --> are omitted because any remaining occurrrences - must be within comprehensions.*) -val standard_consts = - [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all}, - @{const_name "=="}, @{const_name "op |"}, @{const_name Not}, - @{const_name "op ="}]; - - (*** constants with types ***) (*An abstraction of Isabelle types*) datatype const_typ = CTVar | CType of string * const_typ list (*Is the second type an instance of the first one?*) -fun match_type (CType(con1,args1)) (CType(con2,args2)) = +fun match_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso match_types args1 args2 | match_type CTVar _ = true | match_type _ CTVar = false @@ -91,63 +68,85 @@ | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2; (*Is there a unifiable constant?*) -fun uni_mem gctab (c,c_typ) = - case Symtab.lookup gctab c of - NONE => false - | SOME ctyps_list => exists (match_types c_typ) ctyps_list; - +fun uni_mem goal_const_tab (c, c_typ) = + exists (match_types c_typ) (these (Symtab.lookup goal_const_tab c)) + (*Maps a "real" type to a const_typ*) -fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) +fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) | const_typ_of (TFree _) = CTVar | const_typ_of (TVar _) = CTVar (*Pairs a constant with the list of its type instantiations (using const_typ)*) -fun const_with_typ thy (c,typ) = +fun const_with_typ thy (c,typ) = let val tvars = Sign.const_typargs thy (c,typ) in (c, map const_typ_of tvars) end - handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*) + handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*) (*Add a const/type pair to the table, but a [] entry means a standard connective, which we ignore.*) -fun add_const_typ_table ((c,ctyps), tab) = - Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list) - tab; +fun add_const_type_to_table (c, ctyps) = + Symtab.map_default (c, [ctyps]) + (fn [] => [] | ctypss => insert (op =) ctyps ctypss) + +val fresh_Ex_prefix = "Sledgehammer.Ex." -(*Free variables are included, as well as constants, to handle locales*) -fun add_term_consts_typs_rm thy (Const(c, typ), tab) = - add_const_typ_table (const_with_typ thy (c,typ), tab) - | add_term_consts_typs_rm thy (Free(c, typ), tab) = - add_const_typ_table (const_with_typ thy (c,typ), tab) - | add_term_consts_typs_rm _ (Const (@{const_name skolem_id}, _) $ _, tab) = - tab - | add_term_consts_typs_rm thy (t $ u, tab) = - add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab)) - | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab) - | add_term_consts_typs_rm _ (_, tab) = tab; - -(*The empty list here indicates that the constant is being ignored*) -fun add_standard_const (s,tab) = Symtab.update (s,[]) tab; - -val null_const_tab : const_typ list list Symtab.table = - List.foldl add_standard_const Symtab.empty standard_consts; - -fun get_goal_consts_typs thy = List.foldl (add_term_consts_typs_rm thy) null_const_tab; +fun get_goal_consts_typs thy goals = + let + val use_natural_form = !use_natural_form + (* Free variables are included, as well as constants, to handle locales. + "skolem_id" is included to increase the complexity of theorems containing + Skolem functions. In non-CNF form, "Ex" is included but each occurrence + is considered fresh, to simulate the effect of Skolemization. *) + fun aux (Const (x as (s, _))) = + (if s = @{const_name Ex} andalso use_natural_form then + (gensym fresh_Ex_prefix, []) + else + (const_with_typ thy x)) + |> add_const_type_to_table + | aux (Free x) = add_const_type_to_table (const_with_typ thy x) + | aux ((t as Const (@{const_name skolem_id}, _)) $ _) = aux t + | aux (t $ u) = aux t #> aux u + | aux (Abs (_, _, t)) = aux t + | aux _ = I + (* Including equality in this list might be expected to stop rules like + subset_antisym from being chosen, but for some reason filtering works better + with them listed. The logical signs All, Ex, &, and --> are omitted for CNF + because any remaining occurrences must be within comprehensions. *) + val standard_consts = + [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all}, + @{const_name "=="}, @{const_name "op |"}, @{const_name Not}, + @{const_name "op ="}] @ + (if use_natural_form then + [@{const_name All}, @{const_name Ex}, @{const_name "op &"}, + @{const_name "op -->"}] + else + []) + in + Symtab.empty |> fold (Symtab.update o rpair []) standard_consts + |> fold aux goals + end (*Inserts a dummy "constant" referring to the theory name, so that relevance takes the given theory into account.*) fun const_prop_of theory_relevant th = - if theory_relevant then - let val name = Context.theory_name (theory_of_thm th) - val t = Const (name ^ ". 1", HOLogic.boolT) - in t $ prop_of th end - else prop_of th; + if theory_relevant then + let + val name = Context.theory_name (theory_of_thm th) + val t = Const (name ^ ". 1", @{typ bool}) + in t $ prop_of th end + else + prop_of th + +fun appropriate_prop_of theory_relevant (cnf_thm, (_, orig_thm)) = + (if !use_natural_form then orig_thm else cnf_thm) + |> const_prop_of theory_relevant (**** Constant / Type Frequencies ****) (*A two-dimensional symbol table counts frequencies of constants. It's keyed first by constant name and second by its list of type instantiations. For the latter, we need a linear ordering on type const_typ list.*) - + local fun cons_nr CTVar = 0 @@ -165,137 +164,149 @@ structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord); -fun count_axiom_consts theory_relevant thy ((thm,_), tab) = - let fun count_const (a, T, tab) = - let val (c, cts) = const_with_typ thy (a,T) - in (*Two-dimensional table update. Constant maps to types maps to count.*) - Symtab.map_default (c, CTtab.empty) - (CTtab.map_default (cts,0) (fn n => n+1)) tab - end - fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab) - | count_term_consts (Free(a,T), tab) = count_const(a,T,tab) - | count_term_consts (t $ u, tab) = - count_term_consts (t, count_term_consts (u, tab)) - | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab) - | count_term_consts (_, tab) = tab - in count_term_consts (const_prop_of theory_relevant thm, tab) end; +fun count_axiom_consts theory_relevant thy axiom = + let + fun do_const (a, T) = + let val (c, cts) = const_with_typ thy (a,T) in + (* Two-dimensional table update. Constant maps to types maps to + count. *) + CTtab.map_default (cts, 0) (Integer.add 1) + |> Symtab.map_default (c, CTtab.empty) + end + fun do_term (Const x) = do_const x + | do_term (Free x) = do_const x + | do_term (Const (@{const_name skolem_id}, _) $ _) = I + | do_term (t $ u) = do_term t #> do_term u + | do_term (Abs (_, _, t)) = do_term t + | do_term _ = I + in axiom |> appropriate_prop_of theory_relevant |> do_term end (**** Actual Filtering Code ****) (*The frequency of a constant is the sum of those of all instances of its type.*) -fun const_frequency ctab (c, cts) = +fun const_frequency const_tab (c, cts) = CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m) - (the (Symtab.lookup ctab c)) 0 + (the (Symtab.lookup const_tab c) + handle Option.Option => raise Fail ("Const: " ^ c)) 0 -(*Add in a constant's weight, as determined by its frequency.*) -fun add_ct_weight ctab ((c,T), w) = - w + weight_fn (real (const_frequency ctab (c,T))); +(*A surprising number of theorems contain only a few significant constants. + These include all induction rules, and other general theorems. Filtering + theorems in clause form reveals these complexities in the form of Skolem + functions. If we were instead to filter theorems in their natural form, + some other method of measuring theorem complexity would become necessary.*) -(*Relevant constants are weighted according to frequency, +(* "log" seems best in practice. A constant function of one ignores the constant + frequencies. *) +fun log_weight2 (x:real) = 1.0 + 2.0 / Math.ln (x + 1.0) + +(* Computes a constant's weight, as determined by its frequency. *) +val ct_weight = log_weight2 o real oo const_frequency + +(*Relevant constants are weighted according to frequency, but irrelevant constants are simply counted. Otherwise, Skolem functions, which are rare, would harm a clause's chances of being picked.*) -fun clause_weight ctab gctyps consts_typs = +fun clause_weight const_tab gctyps consts_typs = let val rel = filter (uni_mem gctyps) consts_typs - val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel + val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0 in rel_weight / (rel_weight + real (length consts_typs - length rel)) end; - + (*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*) fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys; -fun consts_typs_of_term thy t = - let val tab = add_term_consts_typs_rm thy (t, null_const_tab) - in Symtab.fold add_expand_pairs tab [] end; +fun consts_typs_of_term thy t = + Symtab.fold add_expand_pairs (get_goal_consts_typs thy [t]) [] -fun pair_consts_typs_axiom theory_relevant thy (p as (thm, _)) = - (p, (consts_typs_of_term thy (const_prop_of theory_relevant thm))); +fun pair_consts_typs_axiom theory_relevant thy axiom = + (axiom, axiom |> appropriate_prop_of theory_relevant + |> consts_typs_of_term thy) -exception ConstFree; -fun dest_ConstFree (Const aT) = aT - | dest_ConstFree (Free aT) = aT - | dest_ConstFree _ = raise ConstFree; +exception CONST_OR_FREE of unit + +fun dest_Const_or_Free (Const x) = x + | dest_Const_or_Free (Free x) = x + | dest_Const_or_Free _ = raise CONST_OR_FREE () (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*) fun defines thy thm gctypes = let val tm = prop_of thm fun defs lhs rhs = let val (rator,args) = strip_comb lhs - val ct = const_with_typ thy (dest_ConstFree rator) + val ct = const_with_typ thy (dest_Const_or_Free rator) in forall is_Var args andalso uni_mem gctypes ct andalso subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) end - handle ConstFree => false - in + handle CONST_OR_FREE () => false + in case tm of - @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) => - defs lhs rhs + @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) => + defs lhs rhs | _ => false end; -type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list); - +type annotated_clause = 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); +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 : (annotd_cls*real) list) = +fun take_best max_new (newpairs : (annotated_clause * real) list) = let val nnew = length newpairs in if nnew <= max_new then (map #1 newpairs, []) - else + else let val cls = sort compare_pairs newpairs val accepted = List.take (cls, max_new) in - trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ + trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ ", exceeds the limit of " ^ Int.toString (max_new))); trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); trace_msg (fn () => "Actually passed: " ^ - space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted)); + space_implode ", " (map (fn (((_,((name,_), _)),_),_) => name) accepted)); (map #1 accepted, map #1 (List.drop (cls, max_new))) end end; -fun cnf_for_facts ctxt = - let val thy = ProofContext.theory_of ctxt in - maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt) - end - fun relevant_clauses ctxt relevance_convergence defs_relevant max_new - (relevance_override as {add, del, only}) ctab = + ({add, del, ...} : relevance_override) const_tab = let val thy = ProofContext.theory_of ctxt - val add_thms = cnf_for_facts ctxt add - val del_thms = cnf_for_facts ctxt del - fun iter threshold rel_consts = + val add_thms = maps (ProofContext.get_fact ctxt) add + val del_thms = maps (ProofContext.get_fact ctxt) del + fun iter threshold rel_const_tab = let fun relevant ([], _) [] = [] (* Nothing added this iteration *) | relevant (newpairs, rejects) [] = let val (newrels, more_rejects) = take_best max_new newpairs val new_consts = maps #2 newrels - val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts + val rel_const_tab = + rel_const_tab |> fold add_const_type_to_table new_consts val threshold = threshold + (1.0 - threshold) / relevance_convergence in trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels)); - map #1 newrels @ iter threshold rel_consts' + map #1 newrels @ iter threshold rel_const_tab (more_rejects @ rejects) end | relevant (newrels, rejects) - ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) = + ((ax as (clsthm as (_, ((name, n), orig_th)), + consts_typs)) :: axs) = let - val weight = if member Thm.eq_thm add_thms thm then 1.0 - else if member Thm.eq_thm del_thms thm then 0.0 - else clause_weight ctab rel_consts consts_typs + val weight = + if member Thm.eq_thm add_thms orig_th then 1.0 + else if member Thm.eq_thm del_thms orig_th then 0.0 + else clause_weight const_tab rel_const_tab consts_typs in if weight >= threshold orelse - (defs_relevant andalso defines thy (#1 clsthm) rel_consts) then - (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^ + (defs_relevant andalso + defines thy (#1 clsthm) rel_const_tab) then + (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^ " passes: " ^ Real.toString weight); relevant ((ax, weight) :: newrels, rejects) axs) else @@ -307,14 +318,14 @@ relevant ([], []) end in iter end - + fun relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override - thy axioms goals = + thy (axioms : cnf_thm list) goals = if relevance_threshold > 0.0 then let - val const_tab = List.foldl (count_axiom_consts theory_relevant thy) - Symtab.empty axioms + val const_tab = fold (count_axiom_consts theory_relevant thy) axioms + Symtab.empty val goal_const_tab = get_goal_consts_typs thy goals val _ = trace_msg (fn () => "Initial constants: " ^ @@ -398,7 +409,7 @@ fun multi_name a th (n, pairs) = (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs); -fun add_names (a, []) pairs = pairs +fun add_names (_, []) pairs = pairs | add_names (a, [th]) pairs = (a, th) :: pairs | add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs)) @@ -453,16 +464,16 @@ fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) | fold_type_consts _ _ x = x; -val add_type_consts_in_type = fold_type_consts setinsert; - (*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 add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x - | add_tcs (Abs (_, _, u)) x = add_tcs u x - | add_tcs (t $ u) x = add_tcs t (add_tcs u x) - | add_tcs _ x = x - in add_tcs end + 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); @@ -478,7 +489,7 @@ (*Ensures that no higher-order theorems "leak out"*) fun restrict_to_logic thy true cls = filter (is_quasi_fol_term thy o prop_of o fst) cls - | restrict_to_logic thy false cls = cls; + | restrict_to_logic _ false cls = cls (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****) @@ -524,16 +535,14 @@ omitted. *) fun is_dangerous_term _ @{prop True} = true | is_dangerous_term full_types t = - not full_types andalso + not full_types andalso (has_typed_var dangerous_types t orelse forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t))) -fun is_dangerous_theorem full_types add_thms thm = - not (member Thm.eq_thm add_thms thm) andalso - is_dangerous_term full_types (prop_of thm) - fun remove_dangerous_clauses full_types add_thms = - filter_out (is_dangerous_theorem full_types add_thms o fst) + filter_out (fn (cnf_th, (_, orig_th)) => + not (member Thm.eq_thm add_thms orig_th) andalso + is_dangerous_term full_types (prop_of cnf_th)) fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of @@ -555,8 +564,11 @@ |> cnf_rules_pairs thy |> not has_override ? make_unique |> not only ? restrict_to_logic thy is_FO - |> (if only then I - else remove_dangerous_clauses full_types (cnf_for_facts ctxt add)) + |> (if only then + I + else + remove_dangerous_clauses full_types + (maps (ProofContext.get_fact ctxt) add)) in relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override @@ -564,9 +576,50 @@ |> has_override ? make_unique 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 + +val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm))) +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 dfg full_types goal_cls chained_ths axcls extra_cls thy = +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 @@ -577,12 +630,12 @@ 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 dfg thy ccls - val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls) - val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls) + 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 dfg thy is_FO full_types conjectures extra_cls - val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers + 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, diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jun 23 10:20:54 2010 +0200 @@ -20,6 +20,7 @@ open Sledgehammer_Util open Sledgehammer_Fact_Preprocessor +open Sledgehammer_HOL_Clause open Sledgehammer_Proof_Reconstruct open ATP_Manager @@ -47,8 +48,8 @@ fun string_for_outcome NONE = "Success." | string_for_outcome (SOME failure) = string_for_failure failure -fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover - timeout subgoal state filtered_clauses name_thms_pairs = +fun sledgehammer_test_theorems (params : params) prover timeout subgoal state + filtered_clauses name_thms_pairs = let val num_theorems = length name_thms_pairs val _ = priority ("Testing " ^ string_of_int num_theorems ^ @@ -88,7 +89,7 @@ (result as {outcome = NONE, ...}) => SOME result | _ => NONE - val {context = ctxt, facts, goal} = Proof.goal state; + val {context = ctxt, goal, ...} = Proof.goal state; in (* try prove first to check result and get used theorems *) (case test_thms_fun NONE name_thms_pairs of @@ -125,8 +126,7 @@ \option (e.g., \"timeout = " ^ string_of_int (10 + msecs div 1000) ^ " s\").") | {message, ...} => (NONE, "ATP error: " ^ message)) - handle Sledgehammer_HOL_Clause.TRIVIAL => - (SOME [], metis_line full_types i n []) + handle TRIVIAL () => (SOME [], metis_line full_types i n []) | ERROR msg => (NONE, "Error: " ^ msg) end diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Jun 23 10:20:54 2010 +0200 @@ -7,6 +7,7 @@ signature SLEDGEHAMMER_FACT_PREPROCESSOR = sig + type cnf_thm = thm * ((string * int) * thm) val chained_prefix: string val trace: bool Unsynchronized.ref val trace_msg: (unit -> string) -> unit @@ -18,15 +19,12 @@ 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 -> (thm * (string * int)) list - val use_skolem_cache: bool Unsynchronized.ref - (* for emergency use where the Skolem cache causes problems *) - val strip_subgoal : thm -> int -> (string * typ) list * term list * term + 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 neg_clausify_tac: Proof.context -> int -> tactic val setup: theory -> theory end; @@ -35,6 +33,8 @@ open Sledgehammer_FOL_Clause +type cnf_thm = thm * ((string * int) * thm) + (* Used to label theorems chained into the goal. *) val chained_prefix = "Sledgehammer.chained_" @@ -132,14 +132,18 @@ | 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 t thx = 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) $ Envir.beta_norm t + 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 inline s th = let @@ -153,10 +157,12 @@ 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) - val rhs = list_abs_free (map dest_Free args, - HOLogic.choice_const T $ body) - |> inline ? mk_skolem_id - (*Forms a lambda-abstraction over the formal parameters*) + (* 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) + |> inline ? mk_skolem_id val def = Logic.mk_equals (c, rhs) val comb = list_comb (if inline then rhs else c, args) in dec_sko (subst_bound (comb, p)) (def :: defs) end @@ -167,7 +173,7 @@ | 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 t defs = defs (*Do nothing otherwise*) + | dec_sko _ defs = defs in dec_sko (prop_of th) [] end; @@ -409,7 +415,6 @@ val ctxt0 = Variable.global_thm_context th val (nnfth, ctxt) = to_nnf th ctxt0 val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth) - val inline = false (* FIXME: temporary *) val defs = skolem_theorems_of_assume inline s nnfth val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt in @@ -447,20 +452,20 @@ (**** Translate a set of theorems into CNF ****) -fun pair_name_cls _ (_, []) = [] - | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss) - (*The combination of rev and tail recursion preserves the original order*) fun cnf_rules_pairs thy = let - fun aux pairs [] = pairs - | aux pairs ((name, th) :: ths) = + 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 = pair_name_cls 0 (name, cnf_axiom thy th) + val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th) handle THM _ => [] | CLAUSE _ => [] - in aux (new_pairs @ pairs) ths end - in aux [] o rev end + 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 ****) @@ -520,22 +525,12 @@ end; -val use_skolem_cache = Unsynchronized.ref true - -fun clause_cache_endtheory thy = - if !use_skolem_cache then saturate_skolem_cache thy else NONE - +(* For emergency use where the Skolem cache causes problems. *) +val auto_saturate_skolem_cache = Unsynchronized.ref true -(* The cache can be kept smaller by inspecting the prop of each thm. Can ignore - all that are quasi-lambda-free, but then the individual theory caches become - much bigger. *) +fun conditionally_saturate_skolem_cache thy = + if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE -fun strip_subgoal goal i = - let - val (t, frees) = Logic.goal_params (prop_of goal) i - val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) - val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees - in (rev (map dest_Free frees), hyp_ts, concl_t) end (*** Converting a subgoal into negated conjecture clauses. ***) @@ -556,25 +551,11 @@ Subgoal.focus (Variable.set_body false ctxt) n st in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end -(*Conversion of a subgoal to conjecture clauses. Each clause has - leading !!-bound universal variables, to express generality. *) -fun neg_clausify_tac ctxt = - neg_skolemize_tac ctxt THEN' - SUBGOAL (fn (prop, i) => - let val ts = Logic.strip_assums_hyp prop in - EVERY' - [Subgoal.FOCUS - (fn {prems, ...} => - (Method.insert_tac - (map forall_intr_vars (maps neg_clausify prems)) i)) ctxt, - REPEAT_DETERM_N (length ts) o etac thin_rl] i - end); - (** setup **) val setup = - perhaps saturate_skolem_cache - #> Theory.at_end clause_cache_endtheory + perhaps conditionally_saturate_skolem_cache + #> Theory.at_end conditionally_saturate_skolem_cache end; diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed Jun 23 10:20:54 2010 +0200 @@ -10,11 +10,11 @@ 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 clause_prefix: string val const_prefix: string val tconst_prefix: string val class_prefix: string @@ -23,13 +23,12 @@ val type_const_trans_table: string Symtab.table val ascii_of: string -> string val undo_ascii_of: string -> string - val paren_pack : string list -> 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 : bool -> string -> string - val make_fixed_type_const : bool -> 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 @@ -37,56 +36,20 @@ 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 - type axiom_name = string - datatype fol_type = - TyVar of name | - TyFree of name | - TyConstr of name * fol_type list - val string_of_fol_type : - fol_type -> name_pool option -> string * name_pool option 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 - val get_tvar_strs: typ list -> string list datatype arLit = TConsLit of class * string * string list | TVarLit of class * string datatype arity_clause = ArityClause of - {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list} + {axiom_name: string, conclLit: arLit, premLits: arLit list} datatype classrel_clause = ClassrelClause of - {axiom_name: axiom_name, subclass: class, superclass: class} + {axiom_name: string, subclass: class, superclass: class} val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list - val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list - val add_type_sort_preds: typ -> int Symtab.table -> int Symtab.table - val add_classrel_clause_preds : - classrel_clause -> int Symtab.table -> int Symtab.table - val class_of_arityLit: arLit -> class - val add_arity_clause_preds: arity_clause -> int Symtab.table -> int Symtab.table - val add_fol_type_funcs: fol_type -> int Symtab.table -> int Symtab.table - val add_arity_clause_funcs: - arity_clause -> int Symtab.table -> int Symtab.table - val init_functab: int Symtab.table - val dfg_sign: bool -> string -> string - val dfg_of_type_literal: bool -> type_literal -> string - val gen_dfg_cls: int * string * kind * string list * string list * string list -> string - val string_of_preds: (string * Int.int) list -> string - val string_of_funcs: (string * int) list -> string - val string_of_symbols: string -> string -> string - val string_of_start: string -> string - val string_of_descrip : string -> string - val dfg_tfree_clause : string -> string - val dfg_classrel_clause: classrel_clause -> string - val dfg_arity_clause: arity_clause -> string - val tptp_sign: bool -> string -> string - val tptp_of_type_literal : - bool -> type_literal -> name_pool option -> string * name_pool option - val gen_tptp_cls : int * string * kind * string list * string list -> string - val tptp_tfree_clause : string -> string - val tptp_arity_clause : arity_clause -> string - val tptp_classrel_clause : classrel_clause -> string end structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE = @@ -94,15 +57,15 @@ 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 clause_prefix = "cls_"; -val arclause_prefix = "clsarity_" -val clrelclause_prefix = "clsrel_"; +val classrel_clause_prefix = "clsrel_"; val const_prefix = "c_"; val tconst_prefix = "tc_"; @@ -175,12 +138,6 @@ val undo_ascii_of = undo_ascii_aux [] o String.explode; -(* convert a list of strings into one single string; surrounded by brackets *) -fun paren_pack [] = "" (*empty argument list*) - | paren_pack strings = "(" ^ commas strings ^ ")"; - -fun tptp_clause strings = "(" ^ space_implode " | " strings ^ ")" - (*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) @@ -196,31 +153,21 @@ tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); -val max_dfg_symbol_length = 63 - -(* HACK because SPASS 3.0 truncates identifiers to 63 characters. *) -fun controlled_length dfg s = - if dfg andalso size s > max_dfg_symbol_length then - String.extract (s, 0, SOME (max_dfg_symbol_length div 2 - 1)) ^ "__" ^ - String.extract (s, size s - max_dfg_symbol_length div 2 + 1, NONE) - else - s +fun lookup_const c = + case Symtab.lookup const_trans_table c of + SOME c' => c' + | NONE => ascii_of c -fun lookup_const dfg c = - case Symtab.lookup const_trans_table c of - SOME c' => c' - | NONE => controlled_length dfg (ascii_of c); - -fun lookup_type_const dfg c = - case Symtab.lookup type_const_trans_table c of - SOME c' => c' - | NONE => controlled_length dfg (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 dfg c = const_prefix ^ lookup_const dfg c; +fun make_fixed_const @{const_name "op ="} = "equal" + | make_fixed_const c = const_prefix ^ lookup_const c -fun make_fixed_type_const dfg c = tconst_prefix ^ lookup_type_const dfg c; +fun make_fixed_type_const c = tconst_prefix ^ lookup_type_const c fun make_type_class clas = class_prefix ^ ascii_of clas; @@ -287,28 +234,12 @@ the_pool |> apsnd SOME -(**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG - format ****) +(**** Definitions and functions for FOL clauses for TPTP format output ****) datatype kind = Axiom | Conjecture; -type axiom_name = string; - (**** Isabelle FOL clauses ****) -datatype fol_type = - TyVar of name | - TyFree of name | - TyConstr of name * fol_type list - -fun string_of_fol_type (TyVar sp) pool = nice_name sp pool - | string_of_fol_type (TyFree sp) pool = nice_name sp pool - | string_of_fol_type (TyConstr (sp, tys)) pool = - let - val (s, pool) = nice_name sp pool - val (ss, pool) = pool_map string_of_fol_type tys pool - in (s ^ paren_pack ss, pool) end - (* The first component is the type class; the second is a TVar or TFree. *) datatype type_literal = TyLitVar of string * name | @@ -329,39 +260,19 @@ 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); -fun pred_of_sort (TyLitVar (s, _)) = (s, 1) - | pred_of_sort (TyLitFree (s, _)) = (s, 1) - (*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) [] -(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear. - * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a - in a lemma has the same sort as 'a in the conjecture. - * Deleting such clauses will lead to problems with locales in other use of local results - where 'a is fixed. Probably we should delete clauses unless the sorts agree. - * Currently we include a class constraint in the clause, exactly as with TVars. -*) - (** make axiom and conjecture clauses. **) -fun get_tvar_strs [] = [] - | get_tvar_strs ((TVar (indx,s))::Ts) = - insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts) - | get_tvar_strs((TFree _)::Ts) = get_tvar_strs Ts - - - (**** Isabelle arities ****) datatype arLit = TConsLit of class * string * string list | TVarLit of class * string; datatype arity_clause = - ArityClause of {axiom_name: axiom_name, - conclLit: arLit, - premLits: arLit list}; + ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list} fun gen_TVars 0 = [] @@ -372,25 +283,23 @@ | pack_sort(tvar, cls::srt) = (cls, tvar) :: pack_sort(tvar, srt); (*Arity of type constructor tcon :: (arg1,...,argN)res*) -fun make_axiom_arity_clause dfg (tcons, axiom_name, (cls,args)) = +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 dfg tcons, tvars), - premLits = map TVarLit (union_all(map pack_sort tvars_srts))} + 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: axiom_name, - subclass: class, - superclass: class}; + 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 thy [] supers = [] +fun class_pairs _ [] _ = [] | class_pairs thy subs supers = let val class_less = Sorts.class_less (Sign.classes_of thy) @@ -399,7 +308,8 @@ in fold add_supers subs [] end fun make_classrel_clause (sub,super) = - ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super, + ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^ + ascii_of super, subclass = make_type_class sub, superclass = make_type_class super}; @@ -409,20 +319,20 @@ (** Isabelle arities **) -fun arity_clause dfg _ _ (tcons, []) = [] - | arity_clause dfg seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) - arity_clause dfg seen n (tcons,ars) - | arity_clause dfg seen n (tcons, (ar as (class,_)) :: ars) = +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 dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: - arity_clause dfg seen (n+1) (tcons,ars) + 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 dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class, ar) :: - arity_clause dfg (class::seen) n (tcons,ars) + make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) :: + arity_clause (class::seen) n (tcons,ars) -fun multi_arity_clause dfg [] = [] - | multi_arity_clause dfg ((tcons, ars) :: tc_arlists) = - arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists +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.*) @@ -436,7 +346,7 @@ in map try_classes tycons end; (*Proving one (tycon, class) membership may require proving others, so iterate.*) -fun iter_type_class_pairs thy tycons [] = ([], []) +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))) @@ -444,165 +354,8 @@ val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; -fun make_arity_clauses_dfg dfg thy tycons classes = +fun make_arity_clauses thy tycons classes = let val (classes', cpairs) = iter_type_class_pairs thy tycons classes - in (classes', multi_arity_clause dfg cpairs) end; -val make_arity_clauses = make_arity_clauses_dfg false; - -(**** Find occurrences of predicates in clauses ****) - -(*FIXME: multiple-arity checking doesn't work, as update_new is the wrong - function (it flags repeated declarations of a function, even with the same arity)*) - -fun update_many keypairs = fold Symtab.update keypairs - -val add_type_sort_preds = update_many o map pred_of_sort o sorts_on_typs - -fun add_classrel_clause_preds (ClassrelClause {subclass, superclass, ...}) = - Symtab.update (subclass, 1) #> Symtab.update (superclass, 1) - -fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass - | class_of_arityLit (TVarLit (tclass, _)) = tclass; - -fun add_arity_clause_preds (ArityClause {conclLit, premLits, ...}) = - let - val classes = map (make_type_class o class_of_arityLit) - (conclLit :: premLits) - in fold (Symtab.update o rpair 1) classes end; - -(*** Find occurrences of functions in clauses ***) - -fun add_fol_type_funcs (TyVar _) = I - | add_fol_type_funcs (TyFree (s, _)) = Symtab.update (s, 0) - | add_fol_type_funcs (TyConstr ((s, _), tys)) = - Symtab.update (s, length tys) #> fold add_fol_type_funcs tys - -(*TFrees are recorded as constants*) -fun add_type_sort_funcs (TVar _, funcs) = funcs - | add_type_sort_funcs (TFree (a, _), funcs) = - Symtab.update (make_fixed_type_var a, 0) funcs - -fun add_arity_clause_funcs (ArityClause {conclLit,...}) funcs = - let val TConsLit (_, tcons, tvars) = conclLit - in Symtab.update (tcons, length tvars) funcs end; - -(*This type can be overlooked because it is built-in...*) -val init_functab = Symtab.update ("tc_itself", 1) Symtab.empty; - - -(**** String-oriented operations ****) - -fun string_of_clausename (cls_id,ax_name) = - clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id; - -fun string_of_type_clsname (cls_id,ax_name,idx) = - string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); - - -(**** Producing DFG files ****) - -(*Attach sign in DFG syntax: false means negate.*) -fun dfg_sign true s = s - | dfg_sign false s = "not(" ^ s ^ ")" - -fun dfg_of_type_literal pos (TyLitVar (s, (s', _))) = - dfg_sign pos (s ^ "(" ^ s' ^ ")") - | dfg_of_type_literal pos (TyLitFree (s, (s', _))) = - dfg_sign pos (s ^ "(" ^ s' ^ ")"); - -(*Enclose the clause body by quantifiers, if necessary*) -fun dfg_forall [] body = body - | dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")" - -fun gen_dfg_cls (cls_id, ax_name, Axiom, lits, tylits, vars) = - "clause( %(axiom)\n" ^ - dfg_forall vars ("or(" ^ commas (tylits@lits) ^ ")") ^ ",\n" ^ - string_of_clausename (cls_id,ax_name) ^ ").\n\n" - | gen_dfg_cls (cls_id, ax_name, Conjecture, lits, _, vars) = - "clause( %(negated_conjecture)\n" ^ - dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^ - string_of_clausename (cls_id,ax_name) ^ ").\n\n"; - -fun string_of_arity (name, arity) = "(" ^ name ^ ", " ^ Int.toString arity ^ ")" - -fun string_of_preds [] = "" - | string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n"; - -fun string_of_funcs [] = "" - | string_of_funcs funcs = "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ; - -fun string_of_symbols predstr funcstr = - "list_of_symbols.\n" ^ predstr ^ funcstr ^ "end_of_list.\n\n"; - -fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n"; - -fun string_of_descrip name = - "list_of_descriptions.\nname({*" ^ name ^ - "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n" - -fun dfg_tfree_clause tfree_lit = - "clause( %(negated_conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n" - -fun dfg_of_arLit (TConsLit (c,t,args)) = - dfg_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")") - | dfg_of_arLit (TVarLit (c,str)) = - dfg_sign false (make_type_class c ^ "(" ^ str ^ ")") - -fun dfg_classrelLits sub sup = "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)"; - -fun dfg_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) = - "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^ - axiom_name ^ ").\n\n"; - -fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name; - -fun dfg_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) = - let val TConsLit (_,_,tvars) = conclLit - val lits = map dfg_of_arLit (conclLit :: premLits) - in - "clause( %(axiom)\n" ^ - dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^ - string_of_ar axiom_name ^ ").\n\n" - end; - - -(**** Produce TPTP files ****) - -fun tptp_sign true s = s - | tptp_sign false s = "~ " ^ s - -fun tptp_of_type_literal pos (TyLitVar (s, name)) = - nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")")) - | tptp_of_type_literal pos (TyLitFree (s, name)) = - nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")")) - -fun tptp_cnf name kind formula = - "cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n" - -fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) = - tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom" - (tptp_clause (tylits @ lits)) - | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) = - tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture" - (tptp_clause lits) - -fun tptp_tfree_clause tfree_lit = - tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_clause [tfree_lit]) - -fun tptp_of_arLit (TConsLit (c,t,args)) = - tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")") - | tptp_of_arLit (TVarLit (c,str)) = - tptp_sign false (make_type_class c ^ "(" ^ str ^ ")") - -fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) = - tptp_cnf (string_of_ar axiom_name) "axiom" - (tptp_clause (map tptp_of_arLit (conclLit :: premLits))) - -fun tptp_classrelLits sub sup = - let val tvar = "(T)" - in tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end; - -fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) = - tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass) + in (classes', multi_arity_clause cpairs) end; end; diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Jun 23 10:20:54 2010 +0200 @@ -2,49 +2,40 @@ Author: Jia Meng, NICTA Author: Jasmin Blanchette, TU Muenchen -FOL clauses translated from HOL formulae. +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 fol_type = Sledgehammer_FOL_Clause.fol_type type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause type arity_clause = Sledgehammer_FOL_Clause.arity_clause - type axiom_name = string type polarity = bool - type hol_clause_id = int + datatype combtyp = + TyVar of name | + TyFree of name | + TyConstr of name * combtyp list datatype combterm = - CombConst of name * fol_type * fol_type list (* Const and Free *) | - CombVar of name * fol_type | + 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: hol_clause_id, axiom_name: axiom_name, th: thm, - kind: kind, literals: literal list, ctypes_sorts: typ list} + HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind, + literals: literal list, ctypes_sorts: typ list} - val type_of_combterm : combterm -> fol_type + 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 - val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list - val make_axiom_clauses : bool -> theory -> - (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list - val type_wrapper_name : string - val get_helper_clauses : - bool -> theory -> bool -> bool -> hol_clause list - -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list - val write_tptp_file : bool -> bool -> bool -> Path.T -> - hol_clause list * hol_clause list * hol_clause list * hol_clause list * - classrel_clause list * arity_clause list -> name_pool option * int - val write_dfg_file : bool -> bool -> Path.T -> - hol_clause list * hol_clause list * hol_clause list * hol_clause list * - classrel_clause list * arity_clause list -> name_pool option * int + 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 = @@ -54,39 +45,46 @@ open Sledgehammer_FOL_Clause open Sledgehammer_Fact_Preprocessor -fun min_arity_of const_min_arity c = - the_default 0 (Symtab.lookup const_min_arity c) - -(*True if the constant ever appears outside of the top-level position in literals. - If false, the constant always receives all of its arguments and is used as a predicate.*) -fun needs_hBOOL explicit_apply const_needs_hBOOL c = - explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c) - - (******************************************************) (* data types for typed combinator expressions *) (******************************************************) -type axiom_name = string; -type polarity = bool; -type hol_clause_id = int; +type polarity = bool + +datatype combtyp = + TyVar of name | + TyFree of name | + TyConstr of name * combtyp list datatype combterm = - CombConst of name * fol_type * fol_type list (* Const and Free *) | - CombVar of name * fol_type | + 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: hol_clause_id, axiom_name: axiom_name, th: thm, - kind: kind, literals: literal list, ctypes_sorts: typ list}; - + 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; @@ -98,65 +96,65 @@ fun isTaut (HOLClause {literals,...}) = exists isTrue literals; -fun type_of dfg (Type (a, Ts)) = - let val (folTypes,ts) = types_of dfg Ts in - (TyConstr (`(make_fixed_type_const dfg) a, folTypes), ts) +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, _)) = + | 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 dfg Ts = - let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts) - in (folTyps, union_all ts) end; +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 dfg (Type (a, Ts)) = - TyConstr (`(make_fixed_type_const dfg) a, map (simp_type_of dfg) 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); - +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 dfg thy (Const (c, T)) = +fun combterm_of thy (Const (c, T)) = let - val (tp, ts) = type_of dfg T + 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 dfg) - val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list) + |> map simp_type_of + val c' = CombConst (`make_fixed_const c, tp, tvar_list) in (c',ts) end - | combterm_of dfg _ (Free(v, T)) = - let val (tp,ts) = type_of dfg T + | 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 dfg _ (Var(v, T)) = - let val (tp,ts) = type_of dfg T + | 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 dfg thy (P $ Q) = - let val (P',tsP) = combterm_of dfg thy P - val (Q',tsQ) = combterm_of dfg thy Q - in (CombApp(P',Q'), union (op =) tsP tsQ) end - | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL clause", t); - -fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity) - | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity); + | 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 literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P - | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) = - literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q - | literals_of_term1 dfg thy (lits,ts) P = - let val ((pred,ts'),pol) = predicate_of dfg thy (P,true) - in - (Literal(pol,pred)::lits, union (op =) ts ts') - end; +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_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P; -val literals_of_term = literals_of_term_dfg false; +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])) ^ @@ -195,438 +193,39 @@ (skolem_somes, t) (* Trivial problem, which resolution cannot handle (empty clause) *) -exception TRIVIAL; +exception TRIVIAL of unit (* making axiom and conjecture clauses *) -fun make_clause dfg thy (clause_id, axiom_name, kind, th) skolem_somes = +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_dfg dfg thy t + val (lits, ctypes_sorts) = literals_of_term thy t in if forall isFalse lits then - raise TRIVIAL + 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 dfg thy (th, (name, id)) (skolem_somes, clss) = +fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) = let - val (skolem_somes, cls) = - make_clause dfg thy (id, name, Axiom, th) skolem_somes + 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 dfg thy clauses = - ([], []) |> fold (add_axiom_clause dfg thy) clauses |> snd +fun make_axiom_clauses thy clauses = + ([], []) |> fold (add_axiom_clause thy) clauses |> snd -fun make_conjecture_clauses dfg thy = +fun make_conjecture_clauses thy = let fun aux _ _ [] = [] | aux n skolem_somes (th :: ths) = let val (skolem_somes, cls) = - make_clause dfg thy (n, "conjecture", Conjecture, th) skolem_somes + make_clause thy (n, "conjecture", Conjecture, th) skolem_somes in cls :: aux (n + 1) skolem_somes ths end in aux 0 [] end -(**********************************************************************) -(* convert clause into ATP specific formats: *) -(* TPTP used by Vampire and E *) -(* DFG used by SPASS *) -(**********************************************************************) - -(*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; - -val type_wrapper_name = "ti" - -fun head_needs_hBOOL explicit_apply const_needs_hBOOL - (CombConst ((c, _), _, _)) = - needs_hBOOL explicit_apply const_needs_hBOOL c - | head_needs_hBOOL _ _ _ = true - -fun wrap_type full_types (s, ty) pool = - if full_types then - let val (s', pool) = string_of_fol_type ty pool in - (type_wrapper_name ^ paren_pack [s, s'], pool) - end - else - (s, pool) - -fun wrap_type_if full_types explicit_apply cnh (head, s, tp) = - if head_needs_hBOOL explicit_apply cnh head then - wrap_type full_types (s, tp) - else - pair s - -fun apply ss = "hAPP" ^ paren_pack ss; - -fun rev_apply (v, []) = v - | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg]; - -fun string_apply (v, args) = rev_apply (v, rev args); - -(* Apply an operator to the argument strings, using either the "apply" operator - or direct function application. *) -fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args) - pool = - let - val s = if s = "equal" then "c_fequal" else s - val nargs = min_arity_of cma s - val args1 = List.take (args, nargs) - handle Subscript => - raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^ - " but is applied to " ^ commas (map quote args)) - val args2 = List.drop (args, nargs) - val (targs, pool) = if full_types then ([], pool) - else pool_map string_of_fol_type tvars pool - val (s, pool) = nice_name (s, s') pool - in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end - | string_of_application _ _ (CombVar (name, _), args) pool = - nice_name name pool |>> (fn s => string_apply (s, args)) - -fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t - pool = - let - val (head, args) = strip_combterm_comb t - val (ss, pool) = pool_map (string_of_combterm params) args pool - val (s, pool) = string_of_application full_types cma (head, ss) pool - in - wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t) - pool - end - -(*Boolean-valued terms are here converted to literals.*) -fun boolify params c = - string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single - -fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t = - case t of - (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) => - (* DFG only: new TPTP prefers infix equality *) - pool_map (string_of_combterm params) [t1, t2] - #>> prefix "equal" o paren_pack - | _ => - case #1 (strip_combterm_comb t) of - CombConst ((s, _), _, _) => - (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm) - params t - | _ => boolify params t - - -(*** TPTP format ***) - -fun tptp_of_equality params pos (t1, t2) = - pool_map (string_of_combterm params) [t1, t2] - #>> space_implode (if pos then " = " else " != ") - -fun tptp_literal params - (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1), - t2))) = - tptp_of_equality params pos (t1, t2) - | tptp_literal params (Literal (pos, pred)) = - string_of_predicate params pred #>> tptp_sign pos - -(* Given a clause, returns its literals paired with a list of literals - concerning TFrees; the latter should only occur in conjecture clauses. *) -fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) - pool = - let - val (lits, pool) = pool_map (tptp_literal params) literals pool - val (tylits, pool) = pool_map (tptp_of_type_literal pos) - (type_literals_for_types ctypes_sorts) pool - in ((lits, tylits), pool) end - -fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...}) - pool = -let - val ((lits, tylits), pool) = - tptp_type_literals params (kind = Conjecture) cls pool - in - ((gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits), pool) - end - - -(*** DFG format ***) - -fun dfg_literal params (Literal (pos, pred)) = - string_of_predicate params pred #>> dfg_sign pos - -fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) = - pool_map (dfg_literal params) literals - #>> rpair (map (dfg_of_type_literal pos) - (type_literals_for_types ctypes_sorts)) - -fun get_uvars (CombConst _) vars pool = (vars, pool) - | get_uvars (CombVar (name, _)) vars pool = - nice_name name pool |>> (fn var => var :: vars) - | get_uvars (CombApp (P, Q)) vars pool = - let val (vars, pool) = get_uvars P vars pool in get_uvars Q vars pool end - -fun get_uvars_l (Literal (_, c)) = get_uvars c []; - -fun dfg_vars (HOLClause {literals, ...}) = - pool_map get_uvars_l literals #>> union_all - -fun dfg_clause params (cls as HOLClause {axiom_name, clause_id, kind, - ctypes_sorts, ...}) pool = - let - val ((lits, tylits), pool) = - dfg_type_literals params (kind = Conjecture) cls pool - val (vars, pool) = dfg_vars cls pool - val tvars = get_tvar_strs ctypes_sorts - in - ((gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars @ vars), - tylits), pool) - end - - -(** For DFG format: accumulate function and predicate declarations **) - -fun add_types tvars = fold add_fol_type_funcs tvars - -fun add_decls (full_types, explicit_apply, cma, cnh) - (CombConst ((c, _), ctp, tvars)) (funcs, preds) = - (if c = "equal" then - (add_types tvars funcs, preds) - else - let val arity = min_arity_of cma c - val ntys = if not full_types then length tvars else 0 - val addit = Symtab.update(c, arity + ntys) - in - if needs_hBOOL explicit_apply cnh c then - (add_types tvars (addit funcs), preds) - else - (add_types tvars funcs, addit preds) - end) |>> full_types ? add_fol_type_funcs ctp - | add_decls _ (CombVar (_, ctp)) (funcs, preds) = - (add_fol_type_funcs ctp funcs, preds) - | add_decls params (CombApp (P, Q)) decls = - decls |> add_decls params P |> add_decls params Q - -fun add_literal_decls params (Literal (_, c)) = add_decls params c - -fun add_clause_decls params (HOLClause {literals, ...}) decls = - fold (add_literal_decls params) literals decls - handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities") - -fun decls_of_clauses (params as (full_types, explicit_apply, _, _)) clauses - arity_clauses = - let - val functab = - init_functab - |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2), - ("tc_bool", 0)] - val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1) - val (functab, predtab) = - (functab, predtab) |> fold (add_clause_decls params) clauses - |>> fold add_arity_clause_funcs arity_clauses - in (Symtab.dest functab, Symtab.dest predtab) end - -fun add_clause_preds (HOLClause {ctypes_sorts, ...}) preds = - fold add_type_sort_preds ctypes_sorts preds - handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities") - -(*Higher-order clauses have only the predicates hBOOL and type classes.*) -fun preds_of_clauses clauses clsrel_clauses arity_clauses = - Symtab.empty - |> fold add_clause_preds clauses - |> fold add_arity_clause_preds arity_clauses - |> fold add_classrel_clause_preds clsrel_clauses - |> Symtab.dest - -(**********************************************************************) -(* write clauses to files *) -(**********************************************************************) - -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 - -val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, (name, 0))) -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 dfg thy is_FO full_types conjectures axcls = - let - val axclauses = map snd (make_axiom_clauses dfg 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 dfg thy cnfs) end - -(*Find the minimal arity of each function mentioned in the term. Also, note which uses - are not at top level, to see if hBOOL is needed.*) -fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) = - let val (head, args) = strip_combterm_comb t - val n = length args - val (const_min_arity, const_needs_hBOOL) = - (const_min_arity, const_needs_hBOOL) - |> fold (count_constants_term false) args - in - case head of - CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*) - let val a = if a="equal" andalso not toplev then "c_fequal" else a - in - (const_min_arity |> Symtab.map_default (a, n) (Integer.min n), - const_needs_hBOOL |> not toplev ? Symtab.update (a, true)) - end - | _ => (const_min_arity, const_needs_hBOOL) - end; - -(*A literal is a top-level term*) -fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) = - count_constants_term true t (const_min_arity, const_needs_hBOOL); - -fun count_constants_clause (HOLClause {literals, ...}) - (const_min_arity, const_needs_hBOOL) = - fold count_constants_lit literals (const_min_arity, const_needs_hBOOL); - -fun display_arity explicit_apply const_needs_hBOOL (c,n) = - trace_msg (fn () => "Constant: " ^ c ^ - " arity:\t" ^ Int.toString n ^ - (if needs_hBOOL explicit_apply const_needs_hBOOL c then - " needs hBOOL" - else - "")) - -fun count_constants explicit_apply - (conjectures, _, extra_clauses, helper_clauses, _, _) = - if not explicit_apply then - let val (const_min_arity, const_needs_hBOOL) = - fold count_constants_clause conjectures (Symtab.empty, Symtab.empty) - |> fold count_constants_clause extra_clauses - |> fold count_constants_clause helper_clauses - val _ = app (display_arity explicit_apply const_needs_hBOOL) - (Symtab.dest (const_min_arity)) - in (const_min_arity, const_needs_hBOOL) end - else (Symtab.empty, Symtab.empty); - -fun header () = - "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^ - "% " ^ timestamp () ^ "\n" - -(* TPTP format *) - -fun write_tptp_file readable_names full_types explicit_apply file clauses = - let - fun section _ [] = [] - | section name ss = - "\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^ - ")\n" :: ss - val pool = empty_name_pool readable_names - val (conjectures, axclauses, _, helper_clauses, - classrel_clauses, arity_clauses) = clauses - val (cma, cnh) = count_constants explicit_apply clauses - val params = (full_types, explicit_apply, cma, cnh) - val ((conjecture_clss, tfree_litss), pool) = - pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip - val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss []) - val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses - pool - val classrel_clss = map tptp_classrel_clause classrel_clauses - val arity_clss = map tptp_arity_clause arity_clauses - val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params) - helper_clauses pool - val conjecture_offset = - length ax_clss + length classrel_clss + length arity_clss - + length helper_clss - val _ = - File.write_list file - (header () :: - section "Relevant fact" ax_clss @ - section "Class relationship" classrel_clss @ - section "Arity declaration" arity_clss @ - section "Helper fact" helper_clss @ - section "Conjecture" conjecture_clss @ - section "Type variable" tfree_clss) - in (pool, conjecture_offset) end - -(* DFG format *) - -fun dfg_tfree_predicate s = (first_field "(" s |> the |> fst, 1) - -fun write_dfg_file full_types explicit_apply file clauses = - let - (* Some of the helper functions below are not name-pool-aware. However, - there's no point in adding name pool support if the DFG format is on its - way out anyway. *) - val pool = NONE - val (conjectures, axclauses, _, helper_clauses, - classrel_clauses, arity_clauses) = clauses - val (cma, cnh) = count_constants explicit_apply clauses - val params = (full_types, explicit_apply, cma, cnh) - val ((conjecture_clss, tfree_litss), pool) = - pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip - val tfree_lits = union_all tfree_litss - val problem_name = Path.implode (Path.base file) - val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool - val tfree_clss = map dfg_tfree_clause tfree_lits - val tfree_preds = map dfg_tfree_predicate tfree_lits - val (helper_clauses_strs, pool) = - pool_map (apfst fst oo dfg_clause params) helper_clauses pool - val (funcs, cl_preds) = - decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses - val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses - val preds = tfree_preds @ cl_preds @ ty_preds - val conjecture_offset = - length axclauses + length classrel_clauses + length arity_clauses - + length helper_clauses - val _ = - File.write_list file - (header () :: - string_of_start problem_name :: - string_of_descrip problem_name :: - string_of_symbols (string_of_funcs funcs) - (string_of_preds preds) :: - "list_of_clauses(axioms, cnf).\n" :: - axstrs @ - map dfg_classrel_clause classrel_clauses @ - map dfg_arity_clause arity_clauses @ - helper_clauses_strs @ - ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @ - conjecture_clss @ - tfree_clss @ - ["end_of_list.\n\n", - "end_problem.\n"]) - in (pool, conjecture_offset) end - end; diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jun 23 10:20:54 2010 +0200 @@ -12,7 +12,6 @@ val timeout: int Unsynchronized.ref val full_types: bool Unsynchronized.ref val default_params : theory -> (string * string) list -> params - val setup: theory -> theory end; structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = @@ -25,31 +24,6 @@ open ATP_Systems open Sledgehammer_Fact_Minimizer -(** Proof method used in Isar proofs **) - -val neg_clausify_setup = - Method.setup @{binding neg_clausify} - (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac) - o tap (fn _ => legacy_feature "Old 'neg_clausify' method -- \ - \rerun Sledgehammer to obtain a direct \ - \proof")) - "conversion of goal to negated conjecture clauses (legacy)" - -(** Attribute for converting a theorem into clauses **) - -val parse_clausify_attribute : attribute context_parser = - Scan.lift Parse.nat - >> (fn i => Thm.rule_attribute (fn context => fn th => - let val thy = Context.theory_of context in - Meson.make_meta_clause (nth (cnf_axiom thy th) i) - end)) - -val clausify_setup = - Attrib.setup @{binding clausify} - (parse_clausify_attribute - o tap (fn _ => legacy_feature "Old 'clausify' attribute")) - "conversion of theorem to clauses" - (** Sledgehammer commands **) fun add_to_relevance_override ns : relevance_override = @@ -58,7 +32,6 @@ {add = [], del = ns, only = false} fun only_relevance_override ns : relevance_override = {add = ns, del = [], only = true} -val no_relevance_override = add_to_relevance_override [] fun merge_relevance_override_pairwise (r1 : relevance_override) (r2 : relevance_override) = {add = #add r1 @ #add r2, del = #del r1 @ #del r2, @@ -166,7 +139,7 @@ val infinity_time_in_secs = 60 * 60 * 24 * 365 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs) -fun extract_params thy default_params override_params = +fun extract_params default_params override_params = let val override_params = map unalias_raw_param override_params val raw_params = rev override_params @ rev default_params @@ -216,7 +189,7 @@ timeout = timeout, minimize_timeout = minimize_timeout} end -fun get_params thy = extract_params thy (default_raw_params thy) +fun get_params thy = extract_params (default_raw_params thy) fun default_params thy = get_params thy o map (apsnd single) val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal @@ -264,7 +237,6 @@ val running_atpsN = "running_atps" val kill_atpsN = "kill_atps" val refresh_tptpN = "refresh_tptp" -val helpN = "help" fun minimizize_raw_param_name "timeout" = "minimize_timeout" | minimizize_raw_param_name name = name @@ -359,8 +331,4 @@ "set and display the default parameters for Sledgehammer" Keyword.thy_decl parse_sledgehammer_params_command -val setup = - neg_clausify_setup - #> clausify_setup - end; diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jun 23 10:20:54 2010 +0200 @@ -368,7 +368,7 @@ | add_type_constraint _ = I fun is_positive_literal (@{const Not} $ _) = false - | is_positive_literal t = true + | is_positive_literal _ = true fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) = Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t') @@ -551,11 +551,11 @@ (* Vampire is keen on producing these. *) fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _) $ t1 $ t2)) = (t1 aconv t2) - | is_trivial_formula t = false + | is_trivial_formula _ = false -fun add_desired_line _ _ _ _ _ (line as Definition (num, _, _)) (j, lines) = +fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) = (j, line :: map (replace_deps_in_line (num, [])) lines) - | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees + | add_desired_line isar_shrink_factor conjecture_shape thm_names frees (Inference (num, t, deps)) (j, lines) = (j + 1, if is_axiom_clause_number thm_names num orelse @@ -667,7 +667,7 @@ fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t -fun step_for_line _ _ (Definition (num, t1, t2)) = Let (t1, t2) +fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2) | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t) | step_for_line thm_names j (Inference (num, t, deps)) = Have (if j = 1 then [Show] else [], (raw_prefix, num), @@ -683,7 +683,7 @@ |> decode_lines ctxt full_types tfrees |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names) |> rpair [] |-> fold_rev add_nontrivial_line - |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor + |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor conjecture_shape thm_names frees) |> snd in @@ -722,7 +722,7 @@ else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then aux (hd proof1 :: proof_tail) (map tl proofs) else case hd proof1 of - Have ([], l, t, by) => + Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *) if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t') | _ => false) (tl proofs) andalso not (exists (member (op =) (maps new_labels_of proofs)) @@ -755,7 +755,7 @@ first_pass (proof, contra) |>> cons step | first_pass ((step as Let _) :: proof, contra) = first_pass (proof, contra) |>> cons step - | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) = + | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) = if member (op =) concl_ls l then first_pass (proof, contra ||> l = hd concl_ls ? cons step) else @@ -992,6 +992,13 @@ do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n" in do_proof end +fun strip_subgoal goal i = + let + val (t, frees) = Logic.goal_params (prop_of goal) i + val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) + val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees + in (rev (map dest_Free frees), hyp_ts, concl_t) end + fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) (other_params as (full_types, _, atp_proof, thm_names, goal, i)) = diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Wed Jun 23 10:20:54 2010 +0200 @@ -0,0 +1,255 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML + Author: Jia Meng, NICTA + Author: Jasmin Blanchette, TU Muenchen + +TPTP syntax. +*) + +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 + + val tptp_of_type_literal : + bool -> type_literal -> name_pool option -> string * name_pool option + val write_tptp_file : + bool -> bool -> bool -> Path.T + -> hol_clause list * hol_clause list * hol_clause list * hol_clause list + * classrel_clause list * arity_clause list + -> name_pool option * int +end; + +structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT = +struct + +open Sledgehammer_Util +open Sledgehammer_FOL_Clause +open Sledgehammer_HOL_Clause + +val clause_prefix = "cls_" +val arity_clause_prefix = "clsarity_" + +fun paren_pack [] = "" + | paren_pack strings = "(" ^ commas strings ^ ")" + +fun string_of_fol_type (TyVar sp) pool = nice_name sp pool + | string_of_fol_type (TyFree sp) pool = nice_name sp pool + | string_of_fol_type (TyConstr (sp, tys)) pool = + let + val (s, pool) = nice_name sp pool + val (ss, pool) = pool_map string_of_fol_type tys pool + in (s ^ paren_pack ss, pool) end + +(* True if the constant ever appears outside of the top-level position in + literals. If false, the constant always receives all of its arguments and is + used as a predicate. *) +fun needs_hBOOL explicit_apply const_needs_hBOOL c = + explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c) + +fun head_needs_hBOOL explicit_apply const_needs_hBOOL + (CombConst ((c, _), _, _)) = + needs_hBOOL explicit_apply const_needs_hBOOL c + | head_needs_hBOOL _ _ _ = true + +fun wrap_type full_types (s, ty) pool = + if full_types then + let val (s', pool) = string_of_fol_type ty pool in + (type_wrapper_name ^ paren_pack [s, s'], pool) + end + else + (s, pool) + +fun wrap_type_if full_types explicit_apply cnh (head, s, tp) = + if head_needs_hBOOL explicit_apply cnh head then + wrap_type full_types (s, tp) + else + pair s + +fun apply ss = "hAPP" ^ paren_pack ss; + +fun rev_apply (v, []) = v + | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg]; + +fun string_apply (v, args) = rev_apply (v, rev args) + +fun min_arity_of const_min_arity = the_default 0 o Symtab.lookup const_min_arity + +(* Apply an operator to the argument strings, using either the "apply" operator + or direct function application. *) +fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args) + pool = + let + val s = if s = "equal" then "c_fequal" else s + val nargs = min_arity_of cma s + val args1 = List.take (args, nargs) + handle Subscript => + raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^ + " but is applied to " ^ commas (map quote args)) + val args2 = List.drop (args, nargs) + val (targs, pool) = if full_types then ([], pool) + else pool_map string_of_fol_type tvars pool + val (s, pool) = nice_name (s, s') pool + in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end + | string_of_application _ _ (CombVar (name, _), args) pool = + nice_name name pool |>> (fn s => string_apply (s, args)) + +fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t + pool = + let + val (head, args) = strip_combterm_comb t + val (ss, pool) = pool_map (string_of_combterm params) args pool + val (s, pool) = string_of_application full_types cma (head, ss) pool + in + wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t) + pool + end + +(*Boolean-valued terms are here converted to literals.*) +fun boolify params c = + string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single + +fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t = + case #1 (strip_combterm_comb t) of + CombConst ((s, _), _, _) => + (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm) + params t + | _ => boolify params t + +fun tptp_of_equality params pos (t1, t2) = + pool_map (string_of_combterm params) [t1, t2] + #>> space_implode (if pos then " = " else " != ") + +fun tptp_sign true s = s + | tptp_sign false s = "~ " ^ s + +fun tptp_literal params + (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1), + t2))) = + tptp_of_equality params pos (t1, t2) + | tptp_literal params (Literal (pos, pred)) = + string_of_predicate params pred #>> tptp_sign pos + +fun tptp_of_type_literal pos (TyLitVar (s, name)) = + nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")")) + | tptp_of_type_literal pos (TyLitFree (s, name)) = + nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")")) + +(* Given a clause, returns its literals paired with a list of literals + concerning TFrees; the latter should only occur in conjecture clauses. *) +fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) + pool = + let + val (lits, pool) = pool_map (tptp_literal params) literals pool + val (tylits, pool) = pool_map (tptp_of_type_literal pos) + (type_literals_for_types ctypes_sorts) pool + in ((lits, tylits), pool) end + +fun tptp_cnf name kind formula = + "cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n" + +fun tptp_raw_clause strings = "(" ^ space_implode " | " strings ^ ")" + +val tptp_tfree_clause = + tptp_cnf "tfree_tcs" "negated_conjecture" o tptp_raw_clause o single + +fun tptp_classrel_literals sub sup = + let val tvar = "(T)" in + tptp_raw_clause [tptp_sign false (sub ^ tvar), tptp_sign true (sup ^ tvar)] + end + +fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...}) + pool = + let + val ((lits, tylits), pool) = + tptp_type_literals params (kind = Conjecture) cls pool + val name = clause_prefix ^ ascii_of axiom_name ^ "_" ^ + Int.toString clause_id + val cnf = + case kind of + Axiom => tptp_cnf name "axiom" (tptp_raw_clause (tylits @ lits)) + | Conjecture => tptp_cnf name "negated_conjecture" (tptp_raw_clause lits) + in ((cnf, tylits), pool) end + +fun tptp_classrel_clause (ClassrelClause {axiom_name, subclass, superclass, + ...}) = + tptp_cnf axiom_name "axiom" (tptp_classrel_literals subclass superclass) + +fun tptp_of_arity_literal (TConsLit (c, t, args)) = + tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")") + | tptp_of_arity_literal (TVarLit (c, str)) = + tptp_sign false (make_type_class c ^ "(" ^ str ^ ")") + +fun tptp_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) = + tptp_cnf (arity_clause_prefix ^ ascii_of axiom_name) "axiom" + (tptp_raw_clause (map tptp_of_arity_literal (conclLit :: premLits))) + +(*Find the minimal arity of each function mentioned in the term. Also, note which uses + are not at top level, to see if hBOOL is needed.*) +fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) = + let + val (head, args) = strip_combterm_comb t + val n = length args + val (const_min_arity, const_needs_hBOOL) = + (const_min_arity, const_needs_hBOOL) + |> fold (count_constants_term false) args + in + case head of + CombConst ((a, _), _, _) => (*predicate or function version of "equal"?*) + let val a = if a="equal" andalso not toplev then "c_fequal" else a + in + (const_min_arity |> Symtab.map_default (a, n) (Integer.min n), + const_needs_hBOOL |> not toplev ? Symtab.update (a, true)) + end + | _ => (const_min_arity, const_needs_hBOOL) + end +fun count_constants_lit (Literal (_, t)) = count_constants_term true t +fun count_constants_clause (HOLClause {literals, ...}) = + fold count_constants_lit literals +fun count_constants explicit_apply + (conjectures, _, extra_clauses, helper_clauses, _, _) = + (Symtab.empty, Symtab.empty) + |> (if explicit_apply then + I + else + fold (fold count_constants_clause) + [conjectures, extra_clauses, helper_clauses]) + +fun write_tptp_file readable_names full_types explicit_apply file clauses = + let + fun section _ [] = [] + | section name ss = + "\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^ + ")\n" :: ss + val pool = empty_name_pool readable_names + val (conjectures, axclauses, _, helper_clauses, + classrel_clauses, arity_clauses) = clauses + val (cma, cnh) = count_constants explicit_apply clauses + val params = (full_types, explicit_apply, cma, cnh) + val ((conjecture_clss, tfree_litss), pool) = + pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip + val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss []) + val (ax_clss, pool) = + pool_map (apfst fst oo tptp_clause params) axclauses pool + val classrel_clss = map tptp_classrel_clause classrel_clauses + val arity_clss = map tptp_arity_clause arity_clauses + val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params) + helper_clauses pool + val conjecture_offset = + length ax_clss + length classrel_clss + length arity_clss + + length helper_clss + val _ = + File.write_list file + ("% This file was generated by Isabelle (most likely Sledgehammer)\n\ + \% " ^ timestamp () ^ "\n" :: + section "Relevant fact" ax_clss @ + section "Class relationship" classrel_clss @ + section "Arity declaration" arity_clss @ + section "Helper fact" helper_clss @ + section "Conjecture" conjecture_clss @ + section "Type variable" tfree_clss) + in (pool, conjecture_offset) end + +end; diff -r 6e9f48cf6adf -r 4dca51ef0285 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jun 23 10:05:13 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jun 23 10:20:54 2010 +0200 @@ -6,7 +6,6 @@ signature SLEDGEHAMMER_UTIL = sig - val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c val plural_s : int -> string val serial_commas : string -> string list -> string list val replace_all : string -> string -> string -> string @@ -24,8 +23,6 @@ structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = struct -fun pairf f g x = (f x, g x) - fun plural_s n = if n = 1 then "" else "s" fun serial_commas _ [] = ["??"]