# HG changeset patch # User blanchet # Date 1287760546 -7200 # Node ID 1c75f3f192ae30b09bb9c1758484da4eb58cc11e # Parent b237f757b215158808841ab8d0a6563c617dded9# Parent 87edcef4fab04b1f9e84686f352d106944456107 merged diff -r b237f757b215 -r 1c75f3f192ae NEWS --- a/NEWS Fri Oct 22 13:59:34 2010 +0200 +++ b/NEWS Fri Oct 22 17:15:46 2010 +0200 @@ -276,18 +276,28 @@ meson_disj_FalseD2 ~> Meson.disj_FalseD2 INCOMPATIBILITY. -* Sledgehammer: Renamed lemmas: - COMBI_def ~> Meson.COMBI_def - COMBK_def ~> Meson.COMBK_def - COMBB_def ~> Meson.COMBB_def - COMBC_def ~> Meson.COMBC_def - COMBS_def ~> Meson.COMBS_def - abs_I ~> Meson.abs_I - abs_K ~> Meson.abs_K - abs_B ~> Meson.abs_B - abs_C ~> Meson.abs_C - abs_S ~> Meson.abs_S -INCOMPATIBILITY. +* Sledgehammer: + - Renamed lemmas: + COMBI_def ~> Meson.COMBI_def + COMBK_def ~> Meson.COMBK_def + COMBB_def ~> Meson.COMBB_def + COMBC_def ~> Meson.COMBC_def + COMBS_def ~> Meson.COMBS_def + abs_I ~> Meson.abs_I + abs_K ~> Meson.abs_K + abs_B ~> Meson.abs_B + abs_C ~> Meson.abs_C + abs_S ~> Meson.abs_S + INCOMPATIBILITY. + - Renamed commands: + sledgehammer atp_info ~> sledgehammer running_provers + sledgehammer atp_kill ~> sledgehammer kill_provers + sledgehammer available_atps ~> sledgehammer available_provers + INCOMPATIBILITY. + - Renamed options: + sledgehammer [atps = ...] ~> sledgehammer [provers = ...] + sledgehammer [atp = ...] ~> sledgehammer [prover = ...] + INCOMPATIBILITY. *** FOL *** diff -r b237f757b215 -r 1c75f3f192ae doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Fri Oct 22 13:59:34 2010 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Oct 22 17:15:46 2010 +0200 @@ -78,24 +78,26 @@ \label{introduction} Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs) -on the current goal. The supported ATPs are E \cite{schulz-2002}, SPASS -\cite{weidenbach-et-al-2009}, and Vampire \cite{riazanov-voronkov-2002}, which -can be run locally or remotely via the SystemOnTPTP web service -\cite{sutcliffe-2000}. +and satisfiability-modulo-theory (SMT) solvers on the current goal. The +supported ATPs are E \cite{schulz-2002}, SPASS \cite{weidenbach-et-al-2009}, +Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, and SNARK +\cite{snark}. The ATPs are run either locally or remotely via the +System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs, the +\textit{smt} proof method (which typically relies on the Z3 SMT solver +\cite{z3}) is tried as well. -The problem passed to ATPs consists of your current goal together with a -heuristic selection of hundreds of facts (theorems) from the current theory -context, filtered by relevance. Because jobs are run in the background, you can -continue to work on your proof by other means. Provers can be run in parallel. -Any reply (which may arrive minutes later) will appear in the Proof General -response buffer. +The problem passed to the automatic provers consists of your current goal +together with a heuristic selection of hundreds of facts (theorems) from the +current theory context, filtered by relevance. Because jobs are run in the +background, you can continue to work on your proof by other means. Provers can +be run in parallel. Any reply (which may arrive half a minute later) will appear +in the Proof General response buffer. -The result of a successful ATP proof search is some source text that usually -(but not always) reconstructs the proof within Isabelle, without requiring the -ATPs again. The reconstructed proof relies on the general-purpose Metis prover -\cite{metis}, which is fully integrated into Isabelle/HOL, with explicit -inferences going through the kernel. Thus its results are correct by -construction. +The result of a successful proof search is some source text that usually (but +not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed +proof relies on the general-purpose Metis prover \cite{metis}, which is fully +integrated into Isabelle/HOL, with explicit inferences going through the kernel. +Thus its results are correct by construction. In this manual, we will explicitly invoke the \textbf{sledgehammer} command. Sledgehammer also provides an automatic mode that can be enabled via the @@ -123,10 +125,10 @@ \label{installation} Sledgehammer is part of Isabelle, so you don't need to install it. However, it -relies on third-party automatic theorem provers (ATPs). Currently, E, SPASS, and -Vampire are supported. All of these are available remotely via SystemOnTPTP -\cite{sutcliffe-2000}, but if you want better performance you will need to -install at least E and SPASS locally. +relies on third-party automatic theorem provers (ATPs) and SAT solvers. +Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire, +SInE-E, and SNARK are available remotely via SystemOnTPTP \cite{sutcliffe-2000}. +If you want better performance, you should install E and SPASS locally. There are three main ways to install ATPs on your machine: @@ -199,38 +201,47 @@ \prew \slshape -Sledgehammer: ATP ``\textit{e}'' for subgoal 1: \\ +Sledgehammer: ``\textit{e}'' for subgoal 1: \\ $([a] = [b]) = (a = b)$ \\ Try this command: \textbf{by} (\textit{metis hd.simps}). \\ To minimize the number of lemmas, try this: \\ -\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount] +\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount] % -Sledgehammer: ATP ``\textit{spass}'' for subgoal 1: \\ +Sledgehammer: ``\textit{spass}'' for subgoal 1: \\ $([a] = [b]) = (a = b)$ \\ Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\ To minimize the number of lemmas, try this: \\ -\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount] +\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount] % -Sledgehammer: ATP ``\textit{remote\_vampire}'' for subgoal 1: \\ +Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\ +$([a] = [b]) = (a = b)$ \\ +Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}) \\ +To minimize the number of lemmas, try this: \\ +\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}]~(\textit{eq\_commute last\_snoc}). \\[3\smallskipamount] +% +Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\ $([a] = [b]) = (a = b)$ \\ -Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\ -\phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\ +Try this command: \textbf{by} (\textit{metis hd.simps}) \\ To minimize the number of lemmas, try this: \\ -\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{remote\_vampire}] \\ -\phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\ -\phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}). +\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount] +% +Sledgehammer: ``\textit{smt}'' for subgoal 1: \\ +$([a] = [b]) = (a = b)$ \\ +Try this command: \textbf{by} (\textit{smt hd.simps}) \\ +To minimize the number of lemmas, try this: \\ +\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{smt}]~(\textit{hd.simps}). \postw -Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E -is not installed (\S\ref{installation}), you will see references to -its remote American cousin \textit{remote\_e} instead of -\textit{e}; and if SPASS is not installed, it will not appear in the output. +Sledgehammer ran E, SPASS, Vampire, SInE-E, and the \textit{smt} proof method in +parallel. Depending on which provers are installed and how many processor cores +are available, some of the provers might be missing or present with a +\textit{remote\_} prefix. -Based on each ATP proof, Sledgehammer gives a one-liner proof that uses the -\textit{metis} method. You can click them and insert them into the theory text. -You can click the ``\textbf{sledgehammer} \textit{minimize}'' command if you -want to look for a shorter (and faster) proof. But here the proof found by E -looks perfect, so click it to finish the proof. +For each successful prover, Sledgehammer gives a one-liner proof that uses the +\textit{metis} or \textit{smt} method. You can click the proof to insert it into +the theory text. You can click the ``\textbf{sledgehammer} \textit{minimize}'' +command if you want to look for a shorter (and probably faster) proof. But here +the proof found by E looks perfect, so click it to finish the proof. You can ask Sledgehammer for an Isar text proof by passing the \textit{isar\_proof} option: @@ -241,7 +252,7 @@ When Isar proof construction is successful, it can yield proofs that are more readable and also faster than the \textit{metis} one-liners. This feature is -experimental. +experimental and is only available for ATPs. \section{Hints} \label{hints} @@ -291,14 +302,16 @@ to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a limit on the number of messages to display (5 by default). -\item[$\bullet$] \textbf{\textit{available\_atps}:} Prints the list of installed ATPs. +\item[$\bullet$] \textbf{\textit{available\_provers}:} Prints the list of installed provers. See \S\ref{installation} and \S\ref{mode-of-operation} for more information on -how to install ATPs. +how to install automatic provers. -\item[$\bullet$] \textbf{\textit{running\_atps}:} Prints information about currently -running ATPs, including elapsed runtime and remaining time until timeout. +\item[$\bullet$] \textbf{\textit{running\_provers}:} Prints information about +currently running automatic provers, including elapsed runtime and remaining +time until timeout. -\item[$\bullet$] \textbf{\textit{kill\_atps}:} Terminates all running ATPs. +\item[$\bullet$] \textbf{\textit{kill\_provers}:} Terminates all running +automatic provers. \item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}. @@ -334,12 +347,12 @@ You can instruct Sledgehammer to run automatically on newly entered theorems by enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof -General. For automatic runs, only the first ATP set using \textit{atps} +General. For automatic runs, only the first prover set using \textit{provers} (\S\ref{mode-of-operation}) is considered, \textit{verbose} (\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled, -fewer facts are passed to the ATP, and \textit{timeout} (\S\ref{timeouts}) is -superseded by the ``Auto Tools Time Limit'' in Proof General's ``Isabelle'' -menu. Sledgehammer's output is also more concise. +fewer facts are passed to the prover, and \textit{timeout} +(\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in +Proof General's ``Isabelle'' menu. Sledgehammer's output is also more concise. \section{Option Reference} \label{option-reference} @@ -382,9 +395,9 @@ \label{mode-of-operation} \begin{enum} -\opnodefault{atps}{string} -Specifies the ATPs (automated theorem provers) to use as a space-separated list -(e.g., ``\textit{e}~\textit{spass}''). The following ATPs are supported: +\opnodefault{provers}{string} +Specifies the automatic provers to use as a space-separated list (e.g., +``\textit{e}~\textit{spass}''). The following provers are supported: \begin{enum} \item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz @@ -405,6 +418,9 @@ Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire} executable. +\item[$\bullet$] \textbf{\textit{smt}:} The \textit{smt} proof method invokes an +external SMT prover (usually Z3 \cite{z3}). + \item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. @@ -418,27 +434,38 @@ \item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a prover developed by Stickel et al.\ \cite{snark}. The remote version of SNARK runs on Geoff Sutcliffe's Miami servers. + +\item[$\bullet$] \textbf{\textit{remote\_smt}:} The remote version of the +\textit{smt} proof method runs the SMT solver on servers at the TU M\"unchen (or +wherever \texttt{REMOTE\_SMT\_URL} is set to point). + \end{enum} -By default, Sledgehammer will run E, SPASS, Vampire, and SInE-E in parallel. -For at most two of E, SPASS, and Vampire, it will use any locally installed -version if available. For historical reasons, the default value of this option -can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle'' -menu in Proof General. +By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and \textit{smt} in +parallel---either locally or remotely, depending on the number of processor +cores available. For historical reasons, the default value of this option can be +overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu +in Proof General. -It is a good idea to run several ATPs in parallel, although it could slow down -your machine. Running E, SPASS, and Vampire together for 5 seconds yields about -the same success rate as running the most effective of these (Vampire) for 120 -seconds \cite{boehme-nipkow-2010}. +It is a good idea to run several provers in parallel, although it could slow +down your machine. Running E, SPASS, Vampire, and SInE-E together for 5 seconds +yields a better success rate than running the most effective of these (Vampire) +for 120 seconds \cite{boehme-nipkow-2010}. + +\opnodefault{prover}{string} +Alias for \textit{provers}. + +\opnodefault{atps}{string} +Legacy alias for \textit{provers}. \opnodefault{atp}{string} -Alias for \textit{atps}. +Legacy alias for \textit{provers}. \opdefault{timeout}{time}{$\mathbf{30}$ s} -Specifies the maximum amount of time that the ATPs should spend searching for a -proof. For historical reasons, the default value of this option can be -overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' -menu in Proof General. +Specifies the maximum amount of time that the automatic provers should spend +searching for a proof. For historical reasons, the default value of this option +can be overridden using the option ``Sledgehammer: Time Limit'' from the +``Isabelle'' menu in Proof General. \opfalse{blocking}{non\_blocking} Specifies whether the \textbf{sledgehammer} command should operate @@ -463,16 +490,17 @@ \begin{enum} \opfalse{explicit\_apply}{implicit\_apply} Specifies whether function application should be encoded as an explicit -``apply'' operator. If the option is set to \textit{false}, each function will -be directly applied to as many arguments as possible. Enabling this option can -sometimes help discover higher-order proofs that otherwise would not be found. +``apply'' operator in ATP problems. If the option is set to \textit{false}, each +function will be directly applied to as many arguments as possible. Enabling +this option can sometimes help discover higher-order proofs that otherwise would +not be found. \opfalse{full\_types}{partial\_types} -Specifies whether full-type information is exported. Enabling this option can -prevent the discovery of type-incorrect proofs, but it also tends to slow down -the ATPs significantly. For historical reasons, the default value of this option -can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle'' -menu in Proof General. +Specifies whether full-type information is encoded in ATP problems. Enabling +this option can prevent the discovery of type-incorrect proofs, but it also +tends to slow down the ATPs significantly. For historical reasons, the default +value of this option can be overridden using the option ``Sledgehammer: Full +Types'' from the ``Isabelle'' menu in Proof General. \end{enum} \subsection{Relevance Filter} @@ -490,18 +518,8 @@ \opdefault{max\_relevant}{int\_or\_smart}{\textit{smart}} Specifies the maximum number of facts that may be returned by the relevance filter. If the option is set to \textit{smart}, it is set to a value that was -empirically found to be appropriate for the ATP. A typical value would be 300. - -%\opsmartx{theory\_relevant}{theory\_irrelevant} -%Specifies whether the theory from which a fact comes should be taken into -%consideration by the relevance filter. If the option is set to \textit{smart}, -%it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs; -%empirical results suggest that these are the best settings. - -%\opfalse{defs\_relevant}{defs\_irrelevant} -%Specifies whether the definition of constants occurring in the formula to prove -%should be considered particularly relevant. Enabling this option tends to lead -%to larger problems and typically slows down the ATPs. +empirically found to be appropriate for the prover. A typical value would be +300. \end{enum} \subsection{Output Format} diff -r b237f757b215 -r 1c75f3f192ae doc-src/manual.bib --- a/doc-src/manual.bib Fri Oct 22 13:59:34 2010 +0200 +++ b/doc-src/manual.bib Fri Oct 22 17:15:46 2010 +0200 @@ -1593,6 +1593,11 @@ note = {\url{http://www.cs.kun.nl/~freek/notes/mv.ps.gz}} } +@misc{wikipedia-2009-aa-trees, + key = "Wikipedia", + title = "Wikipedia: {AA} Tree", + note = "\url{http://en.wikipedia.org/wiki/AA_tree}"} + @book{winskel93, author = {Glynn Winskel}, title = {The Formal Semantics of Programming Languages}, @@ -1611,6 +1616,11 @@ %Z +@misc{z3, + key = "Z3", + title = "Z3: An Efficient {SMT} Solver", + note = "\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}"} + % CROSS REFERENCES @@ -1855,8 +1865,3 @@ title = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison}, author = {Stefan Wehr et. al.} } - -@misc{wikipedia-2009-aa-trees, - key = "Wikipedia", - title = "Wikipedia: {AA} Tree", - note = "\url{http://en.wikipedia.org/wiki/AA_tree}"} diff -r b237f757b215 -r 1c75f3f192ae src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Oct 22 13:59:34 2010 +0200 +++ b/src/HOL/IsaMakefile Fri Oct 22 17:15:46 2010 +0200 @@ -327,8 +327,8 @@ Tools/Sledgehammer/sledgehammer_filter.ML \ Tools/Sledgehammer/sledgehammer_minimize.ML \ Tools/Sledgehammer/sledgehammer_isar.ML \ - Tools/Sledgehammer/sledgehammer_reconstruct.ML \ - Tools/Sledgehammer/sledgehammer_translate.ML \ + Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \ + Tools/Sledgehammer/sledgehammer_atp_translate.ML \ Tools/Sledgehammer/sledgehammer_util.ML \ Tools/SMT/cvc3_solver.ML \ Tools/SMT/smtlib_interface.ML \ diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 13:59:34 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 17:15:46 2010 +0200 @@ -29,8 +29,8 @@ lemmas: int, max_lems: int, time_isa: int, - time_atp: int, - time_atp_fail: int} + time_prover: int, + time_prover_fail: int} datatype me_data = MeData of { calls: int, @@ -51,10 +51,11 @@ fun make_sh_data (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, - time_atp,time_atp_fail) = + time_prover,time_prover_fail) = ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, - time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail} + time_isa=time_isa, time_prover=time_prover, + time_prover_fail=time_prover_fail} fun make_min_data (succs, ab_ratios) = MinData{succs=succs, ab_ratios=ab_ratios} @@ -71,8 +72,8 @@ fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, - time_atp, time_atp_fail}) = (calls, success, nontriv_calls, nontriv_success, - lemmas, max_lems, time_isa, time_atp, time_atp_fail) + time_prover, time_prover_fail}) = (calls, success, nontriv_calls, + nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios) @@ -127,40 +128,40 @@ fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); val inc_sh_calls = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail) - => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_success = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail) - => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_nontriv_calls = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail) - => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_nontriv_success = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail) - => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_atp, time_atp_fail)) + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) fun inc_sh_lemmas n = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_atp,time_atp_fail)) + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) fun inc_sh_max_lems n = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_atp,time_atp_fail)) + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) fun inc_sh_time_isa t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_atp,time_atp_fail)) + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) -fun inc_sh_time_atp t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp + t,time_atp_fail)) +fun inc_sh_time_prover t = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) -fun inc_sh_time_atp_fail t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail + t)) +fun inc_sh_time_prover_fail t = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) val inc_min_succs = map_min_data (fn (succs,ab_ratios) => (succs+1, ab_ratios)) @@ -214,7 +215,7 @@ if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 fun log_sh_data log - (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail) = + (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) = (log ("Total number of sledgehammer calls: " ^ str calls); log ("Number of successful sledgehammer calls: " ^ str success); log ("Number of sledgehammer lemmas: " ^ str lemmas); @@ -223,14 +224,14 @@ log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls); log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success); log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa)); - log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_atp)); - log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_atp_fail)); + log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover)); + log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail)); log ("Average time for sledgehammer calls (Isabelle): " ^ str3 (avg_time time_isa calls)); log ("Average time for successful sledgehammer calls (ATP): " ^ - str3 (avg_time time_atp success)); + str3 (avg_time time_prover success)); log ("Average time for failed sledgehammer calls (ATP): " ^ - str3 (avg_time time_atp_fail (calls - success))) + str3 (avg_time time_prover_fail (calls - success))) ) @@ -313,16 +314,17 @@ fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) -fun get_atp thy args = +fun get_prover ctxt args = let - fun default_atp_name () = - hd (#atps (Sledgehammer_Isar.default_params thy [])) + val thy = ProofContext.theory_of ctxt + fun default_prover_name () = + hd (#provers (Sledgehammer_Isar.default_params ctxt [])) handle Empty => error "No ATP available." - fun get_prover name = (name, Sledgehammer.get_prover_fun thy name) + fun get_prover name = (name, Sledgehammer.get_prover thy false name) in (case AList.lookup (op =) args proverK of SOME name => get_prover name - | NONE => get_prover (default_atp_name ())) + | NONE => get_prover (default_prover_name ())) end type locality = Sledgehammer_Filter.locality @@ -346,31 +348,35 @@ (change_dir dir #> Config.put Sledgehammer.measure_run_time true) val params as {full_types, relevance_thresholds, max_relevant, ...} = - Sledgehammer_Isar.default_params thy + Sledgehammer_Isar.default_params ctxt [("timeout", Int.toString timeout ^ " s")] + val default_max_relevant = + Sledgehammer.default_max_relevant_for_prover thy prover_name + val irrelevant_consts = + Sledgehammer.irrelevant_consts_for_prover prover_name + val relevance_fudge = Sledgehammer.relevance_fudge_for_prover prover_name val relevance_override = {add = [], del = [], only = false} - val {default_max_relevant, ...} = ATP_Systems.get_prover thy prover_name val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i val axioms = Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds - (the_default default_max_relevant max_relevant) - relevance_override chained_ths hyp_ts concl_t + (the_default default_max_relevant max_relevant) irrelevant_consts + relevance_fudge relevance_override chained_ths hyp_ts concl_t val problem = {state = st', goal = goal, subgoal = i, - axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms, - only = true} + subgoal_count = Sledgehammer_Util.subgoal_count st, + axioms = axioms |> map Sledgehammer.Unprepared, only = true} val time_limit = (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) - val ({outcome, message, used_thm_names, - atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.prover_result, + val ({outcome, message, used_axioms, run_time_in_msecs = SOME time_prover, ...} + : Sledgehammer.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (prover params (K ""))) problem in case outcome of - NONE => (message, SH_OK (time_isa, time_atp, used_thm_names)) - | SOME _ => (message, SH_FAIL (time_isa, time_atp)) + NONE => (message, SH_OK (time_isa, time_prover, used_axioms)) + | SOME _ => (message, SH_FAIL (time_isa, time_prover)) end handle ERROR msg => ("error: " ^ msg, SH_ERROR) | TimeLimit.TimeOut => ("timeout", SH_ERROR) @@ -395,7 +401,7 @@ val triv_str = if trivial then "[T] " else "" val _ = change_data id inc_sh_calls val _ = if trivial then () else change_data id inc_sh_nontriv_calls - val (prover_name, prover) = get_atp (Proof.theory_of st) args + val (prover_name, prover) = get_prover (Proof.context_of st) args val dir = AList.lookup (op =) args keepK val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK @@ -403,7 +409,7 @@ val (msg, result) = run_sh prover_name prover hard_timeout timeout dir st in case result of - SH_OK (time_isa, time_atp, names) => + SH_OK (time_isa, time_prover, names) => let fun get_thms (_, Sledgehammer_Filter.Chained) = NONE | get_thms (name, loc) = @@ -414,38 +420,36 @@ change_data id (inc_sh_lemmas (length names)); change_data id (inc_sh_max_lems (length names)); change_data id (inc_sh_time_isa time_isa); - change_data id (inc_sh_time_atp time_atp); + change_data id (inc_sh_time_prover time_prover); named_thms := SOME (map_filter get_thms names); log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ - string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg) + string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) end - | SH_FAIL (time_isa, time_atp) => + | SH_FAIL (time_isa, time_prover) => let val _ = change_data id (inc_sh_time_isa time_isa) - val _ = change_data id (inc_sh_time_atp_fail time_atp) + val _ = change_data id (inc_sh_time_prover_fail time_prover) in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg) end end - -val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal - fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = let open Metis_Translate - val thy = Proof.theory_of st + val ctxt = Proof.context_of st val n0 = length (these (!named_thms)) - val (prover_name, _) = get_atp thy args + val (prover_name, _) = get_prover ctxt args val timeout = AList.lookup (op =) args minimize_timeoutK |> Option.map (fst o read_int o explode) |> the_default 5 - val params = Sledgehammer_Isar.default_params thy - [("atps", prover_name), ("timeout", Int.toString timeout ^ " s")] + val params = Sledgehammer_Isar.default_params ctxt + [("provers", prover_name), ("timeout", Int.toString timeout ^ " s")] val minimize = - Sledgehammer_Minimize.minimize_theorems params 1 (subgoal_count st) + Sledgehammer_Minimize.minimize_facts params 1 + (Sledgehammer_Util.subgoal_count st) val _ = log separator in case minimize st (these (!named_thms)) of diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Oct 22 13:59:34 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Oct 22 17:15:46 2010 +0200 @@ -5,26 +5,37 @@ structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION = struct -structure SF = Sledgehammer_Filter +fun get args name default_value = + case AList.lookup (op =) args name of + SOME value => the (Real.fromString value) + | NONE => default_value -val relevance_filter_args = - [("worse_irrel_freq", SF.worse_irrel_freq), - ("higher_order_irrel_weight", SF.higher_order_irrel_weight), - ("abs_rel_weight", SF.abs_rel_weight), - ("abs_irrel_weight", SF.abs_irrel_weight), - ("skolem_irrel_weight", SF.skolem_irrel_weight), - ("theory_const_rel_weight", SF.theory_const_rel_weight), - ("theory_const_irrel_weight", SF.theory_const_irrel_weight), - ("intro_bonus", SF.intro_bonus), - ("elim_bonus", SF.elim_bonus), - ("simp_bonus", SF.simp_bonus), - ("local_bonus", SF.local_bonus), - ("assum_bonus", SF.assum_bonus), - ("chained_bonus", SF.chained_bonus), - ("max_imperfect", SF.max_imperfect), - ("max_imperfect_exp", SF.max_imperfect_exp), - ("threshold_divisor", SF.threshold_divisor), - ("ridiculous_threshold", SF.ridiculous_threshold)] +fun extract_relevance_fudge args + {worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight, + abs_irrel_weight, skolem_irrel_weight, theory_const_rel_weight, + theory_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus, + local_bonus, assum_bonus, chained_bonus, max_imperfect, + max_imperfect_exp, threshold_divisor, ridiculous_threshold} = + {worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq, + higher_order_irrel_weight = + get args "higher_order_irrel_weight" higher_order_irrel_weight, + abs_rel_weight = get args "abs_rel_weight" abs_rel_weight, + abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight, + skolem_irrel_weight = get args "skolem_irrel_weight" skolem_irrel_weight, + theory_const_rel_weight = + get args "theory_const_rel_weight" theory_const_rel_weight, + theory_const_irrel_weight = + get args "theory_const_irrel_weight" theory_const_irrel_weight, + intro_bonus = get args "intro_bonus" intro_bonus, + elim_bonus = get args "elim_bonus" elim_bonus, + simp_bonus = get args "simp_bonus" simp_bonus, + local_bonus = get args "local_bonus" local_bonus, + assum_bonus = get args "assum_bonus" assum_bonus, + chained_bonus = get args "chained_bonus" chained_bonus, + max_imperfect = get args "max_imperfect" max_imperfect, + max_imperfect_exp = get args "max_imperfect_exp" max_imperfect_exp, + threshold_divisor = get args "threshold_divisor" threshold_divisor, + ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold} structure Prooftab = Table(type key = int * int val ord = prod_ord int_ord int_ord); @@ -85,6 +96,7 @@ () val default_max_relevant = 300 +val prover_name = ATP_Systems.eN (* arbitrary ATP *) fun with_index (i, s) = s ^ "@" ^ string_of_int i @@ -95,23 +107,22 @@ SOME proofs => let val {context = ctxt, facts, goal} = Proof.goal pre - val thy = ProofContext.theory_of ctxt - val args = - args - |> filter (fn (key, value) => - case AList.lookup (op =) relevance_filter_args key of - SOME rf => (rf := the (Real.fromString value); false) - | NONE => true) - + val irrelevant_consts = + Sledgehammer.irrelevant_consts_for_prover prover_name + val relevance_fudge = + extract_relevance_fudge args + (Sledgehammer.relevance_fudge_for_prover prover_name) + val relevance_override = {add = [], del = [], only = false} val {relevance_thresholds, full_types, max_relevant, ...} = - Sledgehammer_Isar.default_params thy args + Sledgehammer_Isar.default_params ctxt args val subgoal = 1 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal val facts = - SF.relevant_facts ctxt full_types + Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds (the_default default_max_relevant max_relevant) - {add = [], del = [], only = false} facts hyp_ts concl_t + irrelevant_consts relevance_fudge relevance_override facts hyp_ts + concl_t |> map (fst o fst) val (found_facts, lost_facts) = List.concat proofs |> sort_distinct string_ord diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Oct 22 13:59:34 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Fri Oct 22 17:15:46 2010 +0200 @@ -10,8 +10,8 @@ imports ATP uses "Tools/Sledgehammer/sledgehammer_util.ML" "Tools/Sledgehammer/sledgehammer_filter.ML" - "Tools/Sledgehammer/sledgehammer_translate.ML" - "Tools/Sledgehammer/sledgehammer_reconstruct.ML" + "Tools/Sledgehammer/sledgehammer_atp_translate.ML" + "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML" "Tools/Sledgehammer/sledgehammer.ML" "Tools/Sledgehammer/sledgehammer_minimize.ML" "Tools/Sledgehammer/sledgehammer_isar.ML" diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 22 13:59:34 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 22 17:15:46 2010 +0200 @@ -9,7 +9,7 @@ sig type failure = ATP_Proof.failure - type prover_config = + type atp_config = {exec: string * string, required_execs: (string * string) list, arguments: bool -> Time.time -> string, @@ -20,11 +20,17 @@ explicit_forall: bool, use_conjecture_for_hypotheses: bool} - val add_prover: string * prover_config -> theory -> theory - val get_prover: theory -> string -> prover_config - val available_atps: theory -> unit + val eN : string + val spassN : string + val vampireN : string + val sine_eN : string + val snarkN : string + val remote_prefix : string + val add_atp : string * atp_config -> theory -> theory + val get_atp : theory -> string -> atp_config + val available_atps : theory -> string list + val is_atp_installed : theory -> string -> bool val refresh_systems_on_tptp : unit -> unit - val default_atps_param_value : unit -> string val setup : theory -> theory end; @@ -33,9 +39,9 @@ open ATP_Proof -(* prover configuration *) +(* ATP configuration *) -type prover_config = +type atp_config = {exec: string * string, required_execs: (string * string) list, arguments: bool -> Time.time -> string, @@ -51,33 +57,28 @@ (NoPerl, "env: perl"), (NoLibwwwPerl, "Can't locate HTTP")] -(* named provers *) +(* named ATPs *) + +val eN = "e" +val spassN = "spass" +val vampireN = "vampire" +val sine_eN = "sine_e" +val snarkN = "snark" +val remote_prefix = "remote_" structure Data = Theory_Data ( - type T = (prover_config * stamp) Symtab.table + type T = (atp_config * stamp) Symtab.table val empty = Symtab.empty val extend = I fun merge data : T = Symtab.merge (eq_snd op =) data handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") ) -fun add_prover (name, config) thy = - Data.map (Symtab.update_new (name, (config, stamp ()))) thy - handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") - -fun get_prover thy name = - the (Symtab.lookup (Data.get thy) name) |> fst - handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") - -fun available_atps thy = - priority ("Available ATPs: " ^ - commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") - fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000 -(* E prover *) +(* E *) (* Give older versions of E an extra second, because the "eproof" script wrongly subtracted an entire second to account for the overhead of the script @@ -92,7 +93,7 @@ val tstp_proof_delims = ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") -val e_config : prover_config = +val e_config : atp_config = {exec = ("E_HOME", "eproof"), required_execs = [], arguments = fn _ => fn timeout => @@ -113,14 +114,14 @@ explicit_forall = false, use_conjecture_for_hypotheses = true} -val e = ("e", e_config) +val e = (eN, e_config) (* SPASS *) (* The "-VarWeight=3" option helps the higher-order problems, probably by counteracting the presence of "hAPP". *) -val spass_config : prover_config = +val spass_config : atp_config = {exec = ("ISABELLE_ATP", "scripts/spass"), required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")], arguments = fn complete => fn timeout => @@ -142,12 +143,12 @@ explicit_forall = true, use_conjecture_for_hypotheses = true} -val spass = ("spass", spass_config) +val spass = (spassN, spass_config) (* Vampire *) -val vampire_config : prover_config = +val vampire_config : atp_config = {exec = ("VAMPIRE_HOME", "vampire"), required_execs = [], arguments = fn complete => fn timeout => @@ -172,10 +173,10 @@ explicit_forall = false, use_conjecture_for_hypotheses = true} -val vampire = ("vampire", vampire_config) +val vampire = (vampireN, vampire_config) -(* Remote prover invocation via SystemOnTPTP *) +(* Remote ATP invocation via SystemOnTPTP *) val systems = Synchronized.var "atp_systems" ([] : string list) @@ -187,9 +188,6 @@ SOME failure => string_for_failure failure | NONE => perhaps (try (unsuffix "\n")) output ^ ".") -fun refresh_systems_on_tptp () = - Synchronized.change systems (fn _ => get_systems ()) - fun find_system name [] systems = find_first (String.isPrefix name) systems | find_system name (version :: versions) systems = case find_first (String.isPrefix (name ^ "---" ^ version)) systems of @@ -208,7 +206,7 @@ fun remote_config system_name system_versions proof_delims known_failures default_max_relevant use_conjecture_for_hypotheses - : prover_config = + : atp_config = {exec = ("ISABELLE_ATP", "scripts/remote_atp"), required_execs = [], arguments = fn _ => fn timeout => @@ -225,48 +223,49 @@ fun remotify_config system_name system_versions ({proof_delims, known_failures, default_max_relevant, - use_conjecture_for_hypotheses, ...} : prover_config) : prover_config = + use_conjecture_for_hypotheses, ...} : atp_config) : atp_config = remote_config system_name system_versions proof_delims known_failures default_max_relevant use_conjecture_for_hypotheses -val remotify_name = prefix "remote_" -fun remote_prover name system_name system_versions proof_delims known_failures - default_max_relevant use_conjecture_for_hypotheses = - (remotify_name name, +fun remote_atp name system_name system_versions proof_delims known_failures + default_max_relevant use_conjecture_for_hypotheses = + (remote_prefix ^ name, remote_config system_name system_versions proof_delims known_failures default_max_relevant use_conjecture_for_hypotheses) -fun remotify_prover (name, config) system_name system_versions = - (remotify_name name, remotify_config system_name system_versions config) +fun remotify_atp (name, config) system_name system_versions = + (remote_prefix ^ name, remotify_config system_name system_versions config) -val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"] -val remote_vampire = remotify_prover vampire "Vampire" ["0.6", "9.0", "1.0"] +val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] +val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] val remote_sine_e = - remote_prover "sine_e" "SInE" [] [] [(IncompleteUnprovable, "says Unknown")] + remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")] 800 (* FUDGE *) true val remote_snark = - remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] [] - 250 (* FUDGE *) true + remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] [] + 250 (* FUDGE *) true (* Setup *) -fun is_installed ({exec, required_execs, ...} : prover_config) = - forall (curry (op <>) "" o getenv o fst) (exec :: required_execs) -fun maybe_remote (name, config) = - name |> not (is_installed config) ? remotify_name +fun add_atp (name, config) thy = + Data.map (Symtab.update_new (name, (config, stamp ()))) thy + handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") + +fun get_atp thy name = + the (Symtab.lookup (Data.get thy) name) |> fst + handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") + +val available_atps = Symtab.keys o Data.get -(* The first prover of the list is used by Auto Sledgehammer. Because of the low - timeout, it makes sense to put SPASS first. *) -fun default_atps_param_value () = - space_implode " " ((if is_installed (snd spass) then [fst spass] else []) @ - [maybe_remote e] @ - [if forall (is_installed o snd) [e, spass] then - remotify_name (fst vampire) - else - maybe_remote vampire, - fst remote_sine_e]) +fun is_atp_installed thy name = + let val {exec, required_execs, ...} = get_atp thy name in + forall (curry (op <>) "" o getenv o fst) (exec :: required_execs) + end -val provers = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e, - remote_snark] -val setup = fold add_prover provers +fun refresh_systems_on_tptp () = + Synchronized.change systems (fn _ => get_systems ()) + +val atps = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e, + remote_snark] +val setup = fold add_atp atps end; diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Oct 22 13:59:34 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Oct 22 17:15:46 2010 +0200 @@ -448,8 +448,7 @@ fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) = (trace_msg (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^ - (case sn of Minus => "concrete" | Plus => "complete") ^ - "."); + (case sn of Minus => "concrete" | Plus => "complete")); case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ()) | SOME (lits, sexps) => (lits, comps, sexps)) diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 13:59:34 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 17:15:46 2010 +0200 @@ -10,16 +10,17 @@ sig type failure = ATP_Systems.failure type locality = Sledgehammer_Filter.locality + type relevance_fudge = Sledgehammer_Filter.relevance_fudge type relevance_override = Sledgehammer_Filter.relevance_override - type fol_formula = Sledgehammer_Translate.fol_formula - type minimize_command = Sledgehammer_Reconstruct.minimize_command + type prepared_formula = Sledgehammer_ATP_Translate.prepared_formula + type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command type params = {blocking: bool, debug: bool, verbose: bool, overlord: bool, - atps: string list, + provers: string list, full_types: bool, explicit_apply: bool, relevance_thresholds: real * real, @@ -29,33 +30,40 @@ timeout: Time.time, expect: string} - type problem = + datatype axiom = + Unprepared of (string * locality) * thm | + Prepared of term * ((string * locality) * prepared_formula) option + + type prover_problem = {state: Proof.state, goal: thm, subgoal: int, - axioms: (term * ((string * locality) * fol_formula) option) list, + subgoal_count: int, + axioms: axiom list, only: bool} type prover_result = {outcome: failure option, - message: string, - pool: string Symtab.table, - used_thm_names: (string * locality) list, - atp_run_time_in_msecs: int, - output: string, - tstplike_proof: string, - axiom_names: (string * locality) list vector, - conjecture_shape: int list list} + used_axioms: (string * locality) list, + run_time_in_msecs: int option, + message: string} + + type prover = params -> minimize_command -> prover_problem -> prover_result - type prover = params -> minimize_command -> problem -> prover_result - + val smtN : string + val is_prover_available : theory -> string -> bool + val is_prover_installed : Proof.context -> string -> bool + val default_max_relevant_for_prover : theory -> string -> int + val irrelevant_consts_for_prover : string -> string list + val relevance_fudge_for_prover : string -> relevance_fudge val dest_dir : string Config.T val problem_prefix : string Config.T val measure_run_time : bool Config.T - val kill_atps: unit -> unit - val running_atps: unit -> unit - val messages: int option -> unit - val get_prover_fun : theory -> string -> prover + val available_provers : theory -> unit + val kill_provers : unit -> unit + val running_provers : unit -> unit + val messages : int option -> unit + val get_prover : theory -> bool -> string -> prover val run_sledgehammer : params -> bool -> int -> relevance_override -> (string -> minimize_command) -> Proof.state -> bool * Proof.state @@ -71,8 +79,8 @@ open Metis_Translate open Sledgehammer_Util open Sledgehammer_Filter -open Sledgehammer_Translate -open Sledgehammer_Reconstruct +open Sledgehammer_ATP_Translate +open Sledgehammer_ATP_Reconstruct (** The Sledgehammer **) @@ -81,18 +89,102 @@ "Async_Manager". *) val das_Tool = "Sledgehammer" -fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" -fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" -val messages = Async_Manager.thread_messages das_Tool "ATP" +val smtN = "smt" +val smt_prover_names = [smtN, remote_prefix ^ smtN] + +val is_smt_prover = member (op =) smt_prover_names + +fun is_prover_available thy name = + is_smt_prover name orelse member (op =) (available_atps thy) name + +fun is_prover_installed ctxt name = + let val thy = ProofContext.theory_of ctxt in + if is_smt_prover name then true (* FIXME *) + else is_atp_installed thy name + end + +val smt_default_max_relevant = 300 (* FUDGE (FIXME) *) +val auto_max_relevant_divisor = 2 (* FUDGE *) + +fun default_max_relevant_for_prover thy name = + if is_smt_prover name then smt_default_max_relevant + else #default_max_relevant (get_atp thy name) + +(* These are typically simplified away by "Meson.presimplify". Equality is + handled specially via "fequal". *) +val atp_irrelevant_consts = + [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, + @{const_name HOL.eq}] +val smt_irrelevant_consts = atp_irrelevant_consts (* FIXME *) + +fun irrelevant_consts_for_prover name = + if is_smt_prover name then smt_irrelevant_consts else atp_irrelevant_consts -(** problems, results, provers, etc. **) +(* FUDGE *) +val atp_relevance_fudge = + {worse_irrel_freq = 100.0, + higher_order_irrel_weight = 1.05, + abs_rel_weight = 0.5, + abs_irrel_weight = 2.0, + skolem_irrel_weight = 0.75, + theory_const_rel_weight = 0.5, + theory_const_irrel_weight = 0.25, + intro_bonus = 0.15, + elim_bonus = 0.15, + simp_bonus = 0.15, + local_bonus = 0.55, + assum_bonus = 1.05, + chained_bonus = 1.5, + max_imperfect = 11.5, + max_imperfect_exp = 1.0, + threshold_divisor = 2.0, + ridiculous_threshold = 0.1} + +(* FUDGE (FIXME) *) +val smt_relevance_fudge = + {worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge, + higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge, + abs_rel_weight = #abs_rel_weight atp_relevance_fudge, + abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge, + skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge, + theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge, + theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge, + intro_bonus = #intro_bonus atp_relevance_fudge, + elim_bonus = #elim_bonus atp_relevance_fudge, + simp_bonus = #simp_bonus atp_relevance_fudge, + local_bonus = #local_bonus atp_relevance_fudge, + assum_bonus = #assum_bonus atp_relevance_fudge, + chained_bonus = #chained_bonus atp_relevance_fudge, + max_imperfect = #max_imperfect atp_relevance_fudge, + max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge, + threshold_divisor = #threshold_divisor atp_relevance_fudge, + ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} + +fun relevance_fudge_for_prover name = + if is_smt_prover name then smt_relevance_fudge else atp_relevance_fudge + +fun available_provers thy = + let + val (remote_provers, local_provers) = + sort_strings (available_atps thy) @ smt_prover_names + |> List.partition (String.isPrefix remote_prefix) + in + priority ("Available provers: " ^ commas (local_provers @ remote_provers) ^ + ".") + end + +fun kill_provers () = Async_Manager.kill_threads das_Tool "provers" +fun running_provers () = Async_Manager.running_threads das_Tool "provers" +val messages = Async_Manager.thread_messages das_Tool "prover" + +(** problems, results, ATPs, etc. **) type params = {blocking: bool, debug: bool, verbose: bool, overlord: bool, - atps: string list, + provers: string list, full_types: bool, explicit_apply: bool, relevance_thresholds: real * real, @@ -102,25 +194,25 @@ timeout: Time.time, expect: string} -type problem = +datatype axiom = + Unprepared of (string * locality) * thm | + Prepared of term * ((string * locality) * prepared_formula) option + +type prover_problem = {state: Proof.state, goal: thm, subgoal: int, - axioms: (term * ((string * locality) * fol_formula) option) list, + subgoal_count: int, + axioms: axiom list, only: bool} type prover_result = {outcome: failure option, message: string, - pool: string Symtab.table, - used_thm_names: (string * locality) list, - atp_run_time_in_msecs: int, - output: string, - tstplike_proof: string, - axiom_names: (string * locality) list vector, - conjecture_shape: int list list} + used_axioms: (string * locality) list, + run_time_in_msecs: int option} -type prover = params -> minimize_command -> problem -> prover_result +type prover = params -> minimize_command -> prover_problem -> prover_result (* configuration attributes *) @@ -140,41 +232,67 @@ |> Exn.release |> tap (after path) -(* generic TPTP-based provers *) +fun prover_description ctxt ({blocking, verbose, ...} : params) name num_axioms + i n goal = + quote name ^ + (if verbose then + " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms + else + "") ^ + " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^ + (if blocking then + "" + else + "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) + +fun proof_banner auto = + if auto then "Sledgehammer found a proof" else "Try this command" + +(* generic TPTP-based ATPs *) + +fun dest_Unprepared (Unprepared p) = p + | dest_Unprepared (Prepared _) = raise Fail "dest_Unprepared" +fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p + | prepared_axiom _ (Prepared p) = p + +fun int_option_add (SOME m) (SOME n) = SOME (m + n) + | int_option_add _ _ = NONE (* Important messages are important but not so important that users want to see them each time. *) val important_message_keep_factor = 0.1 -fun prover_fun auto atp_name +fun run_atp auto atp_name {exec, required_execs, arguments, has_incomplete_mode, proof_delims, known_failures, default_max_relevant, explicit_forall, use_conjecture_for_hypotheses} ({debug, verbose, overlord, full_types, explicit_apply, max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) - minimize_command ({state, goal, subgoal, axioms, only} : problem) = + minimize_command + ({state, goal, subgoal, axioms, only, ...} : prover_problem) = let val ctxt = Proof.context_of state val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal - val axioms = axioms |> not only - ? take (the_default default_max_relevant max_relevant) - val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" - else Config.get ctxt dest_dir - val the_problem_prefix = Config.get ctxt problem_prefix + val axioms = + axioms |> not only ? take (the_default default_max_relevant max_relevant) + |> map (prepared_axiom ctxt) + val dest_dir = if overlord then getenv "ISABELLE_HOME_USER" + else Config.get ctxt dest_dir + val problem_prefix = Config.get ctxt problem_prefix val problem_file_name = Path.basic ((if overlord then "prob_" ^ atp_name - else the_problem_prefix ^ serial_string ()) + else problem_prefix ^ serial_string ()) ^ "_" ^ string_of_int subgoal) val problem_path_name = - if the_dest_dir = "" then + if dest_dir = "" then File.tmp_path problem_file_name - else if File.exists (Path.explode the_dest_dir) then - Path.append (Path.explode the_dest_dir) problem_file_name + else if File.exists (Path.explode dest_dir) then + Path.append (Path.explode dest_dir) problem_file_name else - error ("No such directory: " ^ quote the_dest_dir ^ ".") + error ("No such directory: " ^ quote dest_dir ^ ".") val measure_run_time = verbose orelse Config.get ctxt measure_run_time val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) - (* write out problem file and call prover *) + (* write out problem file and call ATP *) fun command_line complete timeout probfile = let val core = File.shell_path command ^ " " ^ arguments complete timeout ^ @@ -192,7 +310,7 @@ val digit = Scan.one Symbol.is_ascii_digit; val num3 = as_num (digit ::: digit ::: (digit >> single)); 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; + val as_time = Scan.read Symbol.stopper time o explode in (output, as_time t) end; fun run_on probfile = case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of @@ -210,17 +328,17 @@ prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I) - |>> (if measure_run_time then split_time else rpair 0) + |>> (if measure_run_time then split_time else rpair NONE) val (tstplike_proof, outcome) = extract_tstplike_proof_and_outcome complete res_code proof_delims known_failures output in (output, msecs, tstplike_proof, outcome) end val readable_names = debug andalso overlord - val (problem, pool, conjecture_offset, axiom_names) = - prepare_problem ctxt readable_names explicit_forall full_types - explicit_apply hyp_ts concl_t axioms + val (atp_problem, pool, conjecture_offset, axiom_names) = + prepare_atp_problem ctxt readable_names explicit_forall full_types + explicit_apply hyp_ts concl_t axioms val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses - problem + atp_problem val _ = File.write_list probfile ss val conjecture_shape = conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 @@ -237,7 +355,8 @@ ? (fn (_, msecs0, _, SOME _) => run true (Time.- (timeout, Timer.checkRealTimer timer)) |> (fn (output, msecs, tstplike_proof, outcome) => - (output, msecs0 + msecs, tstplike_proof, outcome)) + (output, int_option_add msecs0 msecs, + tstplike_proof, outcome)) | result => result) in ((pool, conjecture_shape, axiom_names), result) end else @@ -246,9 +365,9 @@ (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) fun cleanup probfile = - if the_dest_dir = "" then try File.rm probfile else NONE + if dest_dir = "" then try File.rm probfile else NONE fun export probfile (_, (output, _, _, _)) = - if the_dest_dir = "" then + if dest_dir = "" then () else File.write (Path.explode (Path.implode probfile ^ "_proof")) output @@ -263,19 +382,17 @@ extract_important_message output else "" - val banner = if auto then "Sledgehammer found a proof" - else "Try this command" - val (message, used_thm_names) = + val (message, used_axioms) = case outcome of NONE => proof_text isar_proof (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (banner, full_types, minimize_command, tstplike_proof, axiom_names, - goal, subgoal) + (proof_banner auto, full_types, minimize_command, tstplike_proof, + axiom_names, goal, subgoal) |>> (fn message => message ^ (if verbose then - "\nATP real CPU time: " ^ string_of_int msecs ^ - " ms." + "\nATP real CPU time: " ^ + string_of_int (the msecs) ^ " ms." else "") ^ (if important_message <> "" then @@ -285,40 +402,58 @@ "")) | SOME failure => (string_for_failure failure, []) in - {outcome = outcome, message = message, pool = pool, - used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, - output = output, tstplike_proof = tstplike_proof, - axiom_names = axiom_names, conjecture_shape = conjecture_shape} + {outcome = outcome, message = message, used_axioms = used_axioms, + run_time_in_msecs = msecs} end -fun get_prover_fun thy name = prover_fun false name (get_prover thy name) +(* FIXME: dummy *) +fun saschas_run_smt_solver remote timeout state axioms i = + (OS.Process.sleep (Time.fromMilliseconds 1500); + {outcome = NONE, used_axioms = axioms |> take 5 |> map fst, + run_time_in_msecs = NONE}) -fun run_prover (params as {blocking, debug, verbose, max_relevant, timeout, - expect, ...}) - auto i n minimize_command (problem as {state, goal, axioms, ...}) - (prover as {default_max_relevant, ...}, atp_name) = +fun run_smt_solver remote ({timeout, ...} : params) minimize_command + ({state, subgoal, subgoal_count, axioms, ...} + : prover_problem) = let + val {outcome, used_axioms, run_time_in_msecs} = + saschas_run_smt_solver remote timeout state + (map_filter (try dest_Unprepared) axioms) subgoal + val message = + if outcome = NONE then + try_command_line (proof_banner false) + (apply_on_subgoal subgoal subgoal_count ^ + command_call smtN (map fst used_axioms)) ^ + minimize_line minimize_command (map fst used_axioms) + else + "" + in + {outcome = outcome, used_axioms = used_axioms, + run_time_in_msecs = run_time_in_msecs, message = message} + end + +fun get_prover thy auto name = + if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix) + else run_atp auto name (get_atp thy name) + +fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...}) + auto minimize_command + (problem as {state, goal, subgoal, subgoal_count, axioms, ...}) + name = + let + val thy = Proof.theory_of state val ctxt = Proof.context_of state val birth_time = Time.now () val death_time = Time.+ (birth_time, timeout) - val max_relevant = the_default default_max_relevant max_relevant + val max_relevant = + the_default (default_max_relevant_for_prover thy name) max_relevant val num_axioms = Int.min (length axioms, max_relevant) val desc = - "ATP " ^ quote atp_name ^ - (if verbose then - " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms - else - "") ^ - " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^ - (if blocking then - "" - else - "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) + prover_description ctxt params name num_axioms subgoal subgoal_count goal fun go () = let fun really_go () = - prover_fun auto atp_name prover params (minimize_command atp_name) - problem + get_prover thy auto name params (minimize_command name) problem |> (fn {outcome, message, ...} => (if is_some outcome then "none" else "some", message)) val (outcome_code, message) = @@ -355,51 +490,68 @@ (false, state)) end -val auto_max_relevant_divisor = 2 - -fun run_sledgehammer (params as {blocking, atps, full_types, +fun run_sledgehammer (params as {blocking, provers, full_types, relevance_thresholds, max_relevant, ...}) auto i (relevance_override as {only, ...}) minimize_command state = - if null atps then - error "No ATP is set." + if null provers then + error "No prover is set." else case subgoal_count state of 0 => (priority "No subgoal!"; (false, state)) | n => let val _ = Proof.assert_backward state val thy = Proof.theory_of state - val _ = () |> not blocking ? kill_atps + val {context = ctxt, facts = chained_ths, goal} = Proof.goal state + val (_, hyp_ts, concl_t) = strip_subgoal goal i + val _ = () |> not blocking ? kill_provers val _ = if auto then () else priority "Sledgehammering..." - val provers = map (`(get_prover thy)) atps - fun go () = - let - val {context = ctxt, facts = chained_ths, goal} = Proof.goal state - val (_, hyp_ts, concl_t) = strip_subgoal goal i - val max_max_relevant = - case max_relevant of - SOME n => n - | NONE => - 0 |> fold (Integer.max o #default_max_relevant o fst) provers - |> auto ? (fn n => n div auto_max_relevant_divisor) - val axioms = - relevant_facts ctxt full_types relevance_thresholds - max_max_relevant relevance_override chained_ths - hyp_ts concl_t - val problem = - {state = state, goal = goal, subgoal = i, - axioms = map (prepare_axiom ctxt) axioms, only = only} - val run_prover = run_prover params auto i n minimize_command problem - in - if auto then - fold (fn prover => fn (true, state) => (true, state) - | (false, _) => run_prover prover) - provers (false, state) - else - (if blocking then Par_List.map else map) run_prover provers - |> exists fst |> rpair state - end - in if blocking then go () else Future.fork (tap go) |> K (false, state) end + val (smts, atps) = provers |> List.partition is_smt_prover + fun run_provers full_types irrelevant_consts relevance_fudge maybe_prepare + provers (res as (success, state)) = + if success orelse null provers then + res + else + let + val max_max_relevant = + case max_relevant of + SOME n => n + | NONE => + 0 |> fold (Integer.max o default_max_relevant_for_prover thy) + provers + |> auto ? (fn n => n div auto_max_relevant_divisor) + val axioms = + relevant_facts ctxt full_types relevance_thresholds + max_max_relevant irrelevant_consts relevance_fudge + relevance_override chained_ths hyp_ts concl_t + |> map maybe_prepare + val problem = + {state = state, goal = goal, subgoal = i, subgoal_count = n, + axioms = axioms, only = only} + val run_prover = run_prover params auto minimize_command + in + if auto then + fold (fn prover => fn (true, state) => (true, state) + | (false, _) => run_prover problem prover) + provers (false, state) + else + provers |> (if blocking then Par_List.map else map) + (run_prover problem) + |> exists fst |> rpair state + end + val run_atps = + run_provers full_types atp_irrelevant_consts atp_relevance_fudge + (Prepared o prepare_axiom ctxt) atps + val run_smts = + run_provers true smt_irrelevant_consts smt_relevance_fudge Unprepared + smts + fun run_atps_and_smt_solvers () = + [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ()) + in + (false, state) + |> (if blocking then run_atps #> not auto ? run_smts + else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p)) + end val setup = dest_dir_setup diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Oct 22 17:15:46 2010 +0200 @@ -0,0 +1,949 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Claire Quigley, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + +Proof reconstruction for Sledgehammer. +*) + +signature SLEDGEHAMMER_ATP_RECONSTRUCT = +sig + type locality = Sledgehammer_Filter.locality + type minimize_command = string list -> string + type metis_params = + string * bool * minimize_command * string * (string * locality) list vector + * thm * int + type isar_params = + string Symtab.table * bool * int * Proof.context * int list list + type text_result = string * (string * locality) list + + val repair_conjecture_shape_and_axiom_names : + string -> int list list -> (string * locality) list vector + -> int list list * (string * locality) list vector + val apply_on_subgoal : int -> int -> string + val command_call : string -> string list -> string + val try_command_line : string -> string -> string + val minimize_line : ('a list -> string) -> 'a list -> string + val metis_proof_text : metis_params -> text_result + val isar_proof_text : isar_params -> metis_params -> text_result + val proof_text : bool -> isar_params -> metis_params -> text_result +end; + +structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT = +struct + +open ATP_Problem +open ATP_Proof +open Metis_Translate +open Sledgehammer_Util +open Sledgehammer_Filter +open Sledgehammer_ATP_Translate + +type minimize_command = string list -> string +type metis_params = + string * bool * minimize_command * string * (string * locality) list vector + * thm * int +type isar_params = + string Symtab.table * bool * int * Proof.context * int list list +type text_result = string * (string * locality) list + +fun is_head_digit s = Char.isDigit (String.sub (s, 0)) +val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) + +fun find_first_in_list_vector vec key = + Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key + | (_, value) => value) NONE vec + + +(** SPASS's Flotter hack **) + +(* This is a hack required for keeping track of axioms after they have been + clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also + part of this hack. *) + +val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" + +fun extract_clause_sequence output = + let + val tokens_of = String.tokens (not o Char.isAlphaNum) + fun extract_num ("clause" :: (ss as _ :: _)) = + Int.fromString (List.last ss) + | extract_num _ = NONE + in output |> split_lines |> map_filter (extract_num o tokens_of) end + +val parse_clause_formula_pair = + $$ "(" |-- scan_integer --| $$ "," + -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")" + --| Scan.option ($$ ",") +val parse_clause_formula_relation = + Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" + |-- Scan.repeat parse_clause_formula_pair +val extract_clause_formula_relation = + Substring.full #> Substring.position set_ClauseFormulaRelationN + #> snd #> Substring.position "." #> fst #> Substring.string + #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation + #> fst + +fun repair_conjecture_shape_and_axiom_names output conjecture_shape + axiom_names = + if String.isSubstring set_ClauseFormulaRelationN output then + let + val j0 = hd (hd conjecture_shape) + val seq = extract_clause_sequence output + val name_map = extract_clause_formula_relation output + fun renumber_conjecture j = + conjecture_prefix ^ string_of_int (j - j0) + |> AList.find (fn (s, ss) => member (op =) ss s) name_map + |> map (fn s => find_index (curry (op =) s) seq + 1) + fun names_for_number j = + j |> AList.lookup (op =) name_map |> these + |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of + |> map (fn name => + (name, name |> find_first_in_list_vector axiom_names + |> the) + handle Option.Option => + error ("No such fact: " ^ quote name ^ ".")) + in + (conjecture_shape |> map (maps renumber_conjecture), + seq |> map names_for_number |> Vector.fromList) + end + else + (conjecture_shape, axiom_names) + + +(** Soft-core proof reconstruction: Metis one-liner **) + +fun string_for_label (s, num) = s ^ string_of_int num + +fun apply_on_subgoal _ 1 = "by " + | apply_on_subgoal 1 _ = "apply " + | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply " +fun command_call name [] = name + | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" +fun try_command_line banner command = + banner ^ ": " ^ Markup.markup Markup.sendback command ^ "." +fun using_labels [] = "" + | using_labels ls = + "using " ^ space_implode " " (map string_for_label ls) ^ " " +fun metis_name full_types = if full_types then "metisFT" else "metis" +fun metis_call full_types ss = command_call (metis_name full_types) ss +fun metis_command full_types i n (ls, ss) = + using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss +fun metis_line banner full_types i n ss = + try_command_line banner (metis_command full_types i n ([], ss)) +fun minimize_line _ [] = "" + | minimize_line minimize_command ss = + case minimize_command ss of + "" => "" + | command => + "\nTo minimize the number of lemmas, try this: " ^ + Markup.markup Markup.sendback command ^ "." + +fun resolve_axiom axiom_names ((_, SOME s)) = + (case strip_prefix_and_unascii axiom_prefix s of + SOME s' => (case find_first_in_list_vector axiom_names s' of + SOME x => [(s', x)] + | NONE => []) + | NONE => []) + | resolve_axiom axiom_names (num, NONE) = + case Int.fromString num of + SOME j => + if j > 0 andalso j <= Vector.length axiom_names then + Vector.sub (axiom_names, j - 1) + else + [] + | NONE => [] + +fun add_fact axiom_names (Inference (name, _, [])) = + append (resolve_axiom axiom_names name) + | add_fact _ _ = I + +fun used_facts_in_tstplike_proof axiom_names = + atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names) + +fun used_facts axiom_names = + used_facts_in_tstplike_proof axiom_names + #> List.partition (curry (op =) Chained o snd) + #> pairself (sort_distinct (string_ord o pairself fst)) + +fun metis_proof_text (banner, full_types, minimize_command, + tstplike_proof, axiom_names, goal, i) = + let + val (chained_lemmas, other_lemmas) = + used_facts axiom_names tstplike_proof + val n = Logic.count_prems (prop_of goal) + in + (metis_line banner full_types i n (map fst other_lemmas) ^ + minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)), + other_lemmas @ chained_lemmas) + end + + +(** Hard-core proof reconstruction: structured Isar proofs **) + +(* Simple simplifications to ensure that sort annotations don't leave a trail of + spurious "True"s. *) +fun s_not @{const False} = @{const True} + | s_not @{const True} = @{const False} + | s_not (@{const Not} $ t) = t + | s_not t = @{const Not} $ t +fun s_conj (@{const True}, t2) = t2 + | s_conj (t1, @{const True}) = t1 + | s_conj p = HOLogic.mk_conj p +fun s_disj (@{const False}, t2) = t2 + | s_disj (t1, @{const False}) = t1 + | s_disj p = HOLogic.mk_disj p +fun s_imp (@{const True}, t2) = t2 + | s_imp (t1, @{const False}) = s_not t1 + | s_imp p = HOLogic.mk_imp p +fun s_iff (@{const True}, t2) = t2 + | s_iff (t1, @{const True}) = t1 + | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2 + +fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t +fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t + +fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) = + Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t') + | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) = + Const (@{const_name All}, T) $ Abs (s, T', negate_term t') + | negate_term (@{const HOL.implies} $ t1 $ t2) = + @{const HOL.conj} $ t1 $ negate_term t2 + | negate_term (@{const HOL.conj} $ t1 $ t2) = + @{const HOL.disj} $ negate_term t1 $ negate_term t2 + | negate_term (@{const HOL.disj} $ t1 $ t2) = + @{const HOL.conj} $ negate_term t1 $ negate_term t2 + | negate_term (@{const Not} $ t) = t + | negate_term t = @{const Not} $ t + +val indent_size = 2 +val no_label = ("", ~1) + +val raw_prefix = "X" +val assum_prefix = "A" +val fact_prefix = "F" + +fun resolve_conjecture conjecture_shape (num, s_opt) = + let + val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of + SOME s => Int.fromString s |> the_default ~1 + | NONE => case Int.fromString num of + SOME j => find_index (exists (curry (op =) j)) + conjecture_shape + | NONE => ~1 + in if k >= 0 then [k] else [] end + +fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape +fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape + +fun raw_label_for_name conjecture_shape name = + case resolve_conjecture conjecture_shape name of + [j] => (conjecture_prefix, j) + | _ => case Int.fromString (fst name) of + SOME j => (raw_prefix, j) + | NONE => (raw_prefix ^ fst name, 0) + +(**** INTERPRETATION OF TSTP SYNTAX TREES ****) + +exception FO_TERM of string fo_term list +exception FORMULA of (string, string fo_term) formula list +exception SAME of unit + +(* Type variables are given the basic sort "HOL.type". Some will later be + constrained by information from type literals, or by type inference. *) +fun type_from_fo_term tfrees (u as ATerm (a, us)) = + let val Ts = map (type_from_fo_term tfrees) us in + case strip_prefix_and_unascii type_const_prefix a of + SOME b => Type (invert_const b, Ts) + | NONE => + if not (null us) then + raise FO_TERM [u] (* only "tconst"s have type arguments *) + else case strip_prefix_and_unascii tfree_prefix a of + SOME b => + let val s = "'" ^ b in + TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS) + end + | NONE => + case strip_prefix_and_unascii tvar_prefix a of + SOME b => TVar (("'" ^ b, 0), HOLogic.typeS) + | NONE => + (* Variable from the ATP, say "X1" *) + Type_Infer.param 0 (a, HOLogic.typeS) + end + +(* Type class literal applied to a type. Returns triple of polarity, class, + type. *) +fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) = + case (strip_prefix_and_unascii class_prefix a, + map (type_from_fo_term tfrees) us) of + (SOME b, [T]) => (pos, b, T) + | _ => raise FO_TERM [u] + +(** Accumulate type constraints in a formula: negative type literals **) +fun add_var (key, z) = Vartab.map_default (key, []) (cons z) +fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) + | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) + | add_type_constraint _ = I + +fun repair_atp_variable_name f s = + let + fun subscript_name s n = s ^ nat_subscript n + val s = String.map f s + in + case space_explode "_" s of + [_] => (case take_suffix Char.isDigit (String.explode s) of + (cs1 as _ :: _, cs2 as _ :: _) => + subscript_name (String.implode cs1) + (the (Int.fromString (String.implode cs2))) + | (_, _) => s) + | [s1, s2] => (case Int.fromString s2 of + SOME n => subscript_name s1 n + | NONE => s) + | _ => s + end + +(* First-order translation. No types are known for variables. "HOLogic.typeT" + should allow them to be inferred. *) +fun raw_term_from_pred thy full_types tfrees = + let + fun aux opt_T extra_us u = + case u of + ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1 + | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1 + | ATerm (a, us) => + if a = type_wrapper_name then + case us of + [typ_u, term_u] => + aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u + | _ => raise FO_TERM us + else case strip_prefix_and_unascii const_prefix a of + SOME "equal" => + let val ts = map (aux NONE []) us in + if length ts = 2 andalso hd ts aconv List.last ts then + (* Vampire is keen on producing these. *) + @{const True} + else + list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts) + end + | SOME b => + let + val c = invert_const b + val num_type_args = num_type_args thy c + val (type_us, term_us) = + chop (if full_types then 0 else num_type_args) us + (* Extra args from "hAPP" come after any arguments given directly to + the constant. *) + val term_ts = map (aux NONE []) term_us + val extra_ts = map (aux NONE []) extra_us + val t = + Const (c, if full_types then + case opt_T of + SOME T => map fastype_of term_ts ---> T + | NONE => + if num_type_args = 0 then + Sign.const_instance thy (c, []) + else + raise Fail ("no type information for " ^ quote c) + else + Sign.const_instance thy (c, + map (type_from_fo_term tfrees) type_us)) + in list_comb (t, term_ts @ extra_ts) end + | NONE => (* a free or schematic variable *) + let + val ts = map (aux NONE []) (us @ extra_us) + val T = map fastype_of ts ---> HOLogic.typeT + val t = + case strip_prefix_and_unascii fixed_var_prefix a of + SOME b => Free (b, T) + | NONE => + case strip_prefix_and_unascii schematic_var_prefix a of + SOME b => Var ((b, 0), T) + | NONE => + if is_atp_variable a then + Var ((repair_atp_variable_name Char.toLower a, 0), T) + else + (* Skolem constants? *) + Var ((repair_atp_variable_name Char.toUpper a, 0), T) + in list_comb (t, ts) end + in aux (SOME HOLogic.boolT) [] end + +fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) = + if String.isPrefix class_prefix s then + add_type_constraint (type_constraint_from_term pos tfrees u) + #> pair @{const True} + else + pair (raw_term_from_pred thy full_types tfrees u) + +val combinator_table = + [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}), + (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}), + (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}), + (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}), + (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})] + +fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2)) + | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t') + | uncombine_term (t as Const (x as (s, _))) = + (case AList.lookup (op =) combinator_table s of + SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd + | NONE => t) + | uncombine_term t = t + +(* Update schematic type variables with detected sort constraints. It's not + totally clear when this code is necessary. *) +fun repair_tvar_sorts (t, tvar_tab) = + let + fun do_type (Type (a, Ts)) = Type (a, map do_type Ts) + | do_type (TVar (xi, s)) = + TVar (xi, the_default s (Vartab.lookup tvar_tab xi)) + | do_type (TFree z) = TFree z + fun do_term (Const (a, T)) = Const (a, do_type T) + | do_term (Free (a, T)) = Free (a, do_type T) + | do_term (Var (xi, T)) = Var (xi, do_type T) + | do_term (t as Bound _) = t + | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t) + | do_term (t1 $ t2) = do_term t1 $ do_term t2 + in t |> not (Vartab.is_empty tvar_tab) ? do_term end + +fun quantify_over_var quant_of var_s t = + let + val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s) + |> map Var + in fold_rev quant_of vars t end + +(* Interpret an ATP formula as a HOL term, extracting sort constraints as they + appear in the formula. *) +fun prop_from_formula thy full_types tfrees phi = + let + fun do_formula pos phi = + case phi of + AQuant (_, [], phi) => do_formula pos phi + | AQuant (q, x :: xs, phi') => + do_formula pos (AQuant (q, xs, phi')) + #>> quantify_over_var (case q of + AForall => forall_of + | AExists => exists_of) + (repair_atp_variable_name Char.toLower x) + | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not + | AConn (c, [phi1, phi2]) => + do_formula (pos |> c = AImplies ? not) phi1 + ##>> do_formula pos phi2 + #>> (case c of + AAnd => s_conj + | AOr => s_disj + | AImplies => s_imp + | AIf => s_imp o swap + | AIff => s_iff + | ANotIff => s_not o s_iff + | _ => raise Fail "unexpected connective") + | AAtom tm => term_from_pred thy full_types tfrees pos tm + | _ => raise FORMULA [phi] + in repair_tvar_sorts (do_formula true phi Vartab.empty) end + +fun check_formula ctxt = + Type.constraint HOLogic.boolT + #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) + + +(**** Translation of TSTP files to Isar Proofs ****) + +fun unvarify_term (Var ((s, 0), T)) = Free (s, T) + | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t]) + +fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt = + let + val thy = ProofContext.theory_of ctxt + val t1 = prop_from_formula thy full_types tfrees phi1 + val vars = snd (strip_comb t1) + val frees = map unvarify_term vars + val unvarify_args = subst_atomic (vars ~~ frees) + val t2 = prop_from_formula thy full_types tfrees phi2 + val (t1, t2) = + HOLogic.eq_const HOLogic.typeT $ t1 $ t2 + |> unvarify_args |> uncombine_term |> check_formula ctxt + |> HOLogic.dest_eq + in + (Definition (name, t1, t2), + fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) + end + | decode_line full_types tfrees (Inference (name, u, deps)) ctxt = + let + val thy = ProofContext.theory_of ctxt + val t = u |> prop_from_formula thy full_types tfrees + |> uncombine_term |> check_formula ctxt + in + (Inference (name, t, deps), + fold Variable.declare_term (OldTerm.term_frees t) ctxt) + end +fun decode_lines ctxt full_types tfrees lines = + fst (fold_map (decode_line full_types tfrees) lines ctxt) + +fun is_same_inference _ (Definition _) = false + | is_same_inference t (Inference (_, t', _)) = t aconv t' + +(* No "real" literals means only type information (tfree_tcs, clsrel, or + clsarity). *) +val is_only_type_information = curry (op aconv) HOLogic.true_const + +fun replace_one_dependency (old, new) dep = + if is_same_step (dep, old) then new else [dep] +fun replace_dependencies_in_line _ (line as Definition _) = line + | replace_dependencies_in_line p (Inference (name, t, deps)) = + Inference (name, t, fold (union (op =) o replace_one_dependency p) deps []) + +(* Discard axioms; consolidate adjacent lines that prove the same formula, since + they differ only in type information.*) +fun add_line _ _ (line as Definition _) lines = line :: lines + | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines = + (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or + definitions. *) + if is_axiom axiom_names name then + (* Axioms are not proof lines. *) + if is_only_type_information t then + map (replace_dependencies_in_line (name, [])) lines + (* Is there a repetition? If so, replace later line by earlier one. *) + else case take_prefix (not o is_same_inference t) lines of + (_, []) => lines (* no repetition of proof line *) + | (pre, Inference (name', _, _) :: post) => + pre @ map (replace_dependencies_in_line (name', [name])) post + | _ => raise Fail "unexpected inference" + else if is_conjecture conjecture_shape name then + Inference (name, negate_term t, []) :: lines + else + map (replace_dependencies_in_line (name, [])) lines + | add_line _ _ (Inference (name, t, deps)) lines = + (* Type information will be deleted later; skip repetition test. *) + if is_only_type_information t then + Inference (name, t, deps) :: lines + (* Is there a repetition? If so, replace later line by earlier one. *) + else case take_prefix (not o is_same_inference t) lines of + (* FIXME: Doesn't this code risk conflating proofs involving different + types? *) + (_, []) => Inference (name, t, deps) :: lines + | (pre, Inference (name', t', _) :: post) => + Inference (name, t', deps) :: + pre @ map (replace_dependencies_in_line (name', [name])) post + | _ => raise Fail "unexpected inference" + +(* Recursively delete empty lines (type information) from the proof. *) +fun add_nontrivial_line (Inference (name, t, [])) lines = + if is_only_type_information t then delete_dependency name lines + else Inference (name, t, []) :: lines + | add_nontrivial_line line lines = line :: lines +and delete_dependency name lines = + fold_rev add_nontrivial_line + (map (replace_dependencies_in_line (name, [])) lines) [] + +(* ATPs sometimes reuse free variable names in the strangest ways. Removing + offending lines often does the trick. *) +fun is_bad_free frees (Free x) = not (member (op =) frees x) + | is_bad_free _ _ = false + +fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) = + (j, line :: map (replace_dependencies_in_line (name, [])) lines) + | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees + (Inference (name, t, deps)) (j, lines) = + (j + 1, + if is_axiom axiom_names name orelse + is_conjecture conjecture_shape name orelse + (* the last line must be kept *) + j = 0 orelse + (not (is_only_type_information t) andalso + null (Term.add_tvars t []) andalso + not (exists_subterm (is_bad_free frees) t) andalso + length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso + (* kill next to last line, which usually results in a trivial step *) + j <> 1) then + Inference (name, t, deps) :: lines (* keep line *) + else + map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) + +(** Isar proof construction and manipulation **) + +fun merge_fact_sets (ls1, ss1) (ls2, ss2) = + (union (op =) ls1 ls2, union (op =) ss1 ss2) + +type label = string * int +type facts = label list * string list + +datatype isar_qualifier = Show | Then | Moreover | Ultimately + +datatype isar_step = + Fix of (string * typ) list | + Let of term * term | + Assume of label * term | + Have of isar_qualifier list * label * term * byline +and byline = + ByMetis of facts | + CaseSplit of isar_step list list * facts + +fun smart_case_split [] facts = ByMetis facts + | smart_case_split proofs facts = CaseSplit (proofs, facts) + +fun add_fact_from_dependency conjecture_shape axiom_names name = + if is_axiom axiom_names name then + apsnd (union (op =) (map fst (resolve_axiom axiom_names name))) + else + apfst (insert (op =) (raw_label_for_name conjecture_shape name)) + +fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2) + | step_for_line conjecture_shape _ _ (Inference (name, t, [])) = + Assume (raw_label_for_name conjecture_shape name, t) + | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) = + Have (if j = 1 then [Show] else [], + raw_label_for_name conjecture_shape name, + fold_rev forall_of (map Var (Term.add_vars t [])) t, + ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names) + deps ([], []))) + +fun repair_name "$true" = "c_True" + | repair_name "$false" = "c_False" + | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *) + | repair_name "equal" = "c_equal" (* needed by SPASS? *) + | repair_name s = + if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then + "c_equal" (* seen in Vampire proofs *) + else + s + +fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor + tstplike_proof conjecture_shape axiom_names params frees = + let + val lines = + tstplike_proof + |> atp_proof_from_tstplike_string + |> nasty_atp_proof pool + |> map_term_names_in_atp_proof repair_name + |> decode_lines ctxt full_types tfrees + |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names) + |> rpair [] |-> fold_rev add_nontrivial_line + |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor + conjecture_shape axiom_names frees) + |> snd + in + (if null params then [] else [Fix params]) @ + map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1) + lines + end + +(* When redirecting proofs, we keep information about the labels seen so far in + the "backpatches" data structure. The first component indicates which facts + should be associated with forthcoming proof steps. The second component is a + pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should + become assumptions and "drop_ls" are the labels that should be dropped in a + case split. *) +type backpatches = (label * facts) list * (label list * label list) + +fun used_labels_of_step (Have (_, _, _, by)) = + (case by of + ByMetis (ls, _) => ls + | CaseSplit (proofs, (ls, _)) => + fold (union (op =) o used_labels_of) proofs ls) + | used_labels_of_step _ = [] +and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] + +fun new_labels_of_step (Fix _) = [] + | new_labels_of_step (Let _) = [] + | new_labels_of_step (Assume (l, _)) = [l] + | new_labels_of_step (Have (_, l, _, _)) = [l] +val new_labels_of = maps new_labels_of_step + +val join_proofs = + let + fun aux _ [] = NONE + | aux proof_tail (proofs as (proof1 :: _)) = + if exists null proofs then + NONE + 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, _) => (* 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)) + (used_labels_of proof_tail)) then + SOME (l, t, map rev proofs, proof_tail) + else + NONE + | _ => NONE + in aux [] o map rev end + +fun case_split_qualifiers proofs = + case length proofs of + 0 => [] + | 1 => [Then] + | _ => [Ultimately] + +fun redirect_proof hyp_ts concl_t proof = + let + (* The first pass outputs those steps that are independent of the negated + conjecture. The second pass flips the proof by contradiction to obtain a + direct proof, introducing case splits when an inference depends on + several facts that depend on the negated conjecture. *) + val concl_l = (conjecture_prefix, length hyp_ts) + fun first_pass ([], contra) = ([], contra) + | first_pass ((step as Fix _) :: proof, contra) = + 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 (_, j), _)) :: proof, contra) = + if l = concl_l then first_pass (proof, contra ||> cons step) + else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j)) + | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = + let val step = Have (qs, l, t, ByMetis (ls, ss)) in + if exists (member (op =) (fst contra)) ls then + first_pass (proof, contra |>> cons l ||> cons step) + else + first_pass (proof, contra) |>> cons step + end + | first_pass _ = raise Fail "malformed proof" + val (proof_top, (contra_ls, contra_proof)) = + first_pass (proof, ([concl_l], [])) + val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst + fun backpatch_labels patches ls = + fold merge_fact_sets (map (backpatch_label patches) ls) ([], []) + fun second_pass end_qs ([], assums, patches) = + ([Have (end_qs, no_label, concl_t, + ByMetis (backpatch_labels patches (map snd assums)))], patches) + | second_pass end_qs (Assume (l, t) :: proof, assums, patches) = + second_pass end_qs (proof, (t, l) :: assums, patches) + | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums, + patches) = + (if member (op =) (snd (snd patches)) l andalso + not (member (op =) (fst (snd patches)) l) andalso + not (AList.defined (op =) (fst patches) l) then + second_pass end_qs (proof, assums, patches ||> apsnd (append ls)) + else case List.partition (member (op =) contra_ls) ls of + ([contra_l], co_ls) => + if member (op =) qs Show then + second_pass end_qs (proof, assums, + patches |>> cons (contra_l, (co_ls, ss))) + else + second_pass end_qs + (proof, assums, + patches |>> cons (contra_l, (l :: co_ls, ss))) + |>> cons (if member (op =) (fst (snd patches)) l then + Assume (l, negate_term t) + else + Have (qs, l, negate_term t, + ByMetis (backpatch_label patches l))) + | (contra_ls as _ :: _, co_ls) => + let + val proofs = + map_filter + (fn l => + if l = concl_l then + NONE + else + let + val drop_ls = filter (curry (op <>) l) contra_ls + in + second_pass [] + (proof, assums, + patches ||> apfst (insert (op =) l) + ||> apsnd (union (op =) drop_ls)) + |> fst |> SOME + end) contra_ls + val (assumes, facts) = + if member (op =) (fst (snd patches)) l then + ([Assume (l, negate_term t)], (l :: co_ls, ss)) + else + ([], (co_ls, ss)) + in + (case join_proofs proofs of + SOME (l, t, proofs, proof_tail) => + Have (case_split_qualifiers proofs @ + (if null proof_tail then end_qs else []), l, t, + smart_case_split proofs facts) :: proof_tail + | NONE => + [Have (case_split_qualifiers proofs @ end_qs, no_label, + concl_t, smart_case_split proofs facts)], + patches) + |>> append assumes + end + | _ => raise Fail "malformed proof") + | second_pass _ _ = raise Fail "malformed proof" + val proof_bottom = + second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst + in proof_top @ proof_bottom end + +(* FIXME: Still needed? Probably not. *) +val kill_duplicate_assumptions_in_proof = + let + fun relabel_facts subst = + apfst (map (fn l => AList.lookup (op =) subst l |> the_default l)) + fun do_step (step as Assume (l, t)) (proof, subst, assums) = + (case AList.lookup (op aconv) assums t of + SOME l' => (proof, (l, l') :: subst, assums) + | NONE => (step :: proof, subst, (t, l) :: assums)) + | do_step (Have (qs, l, t, by)) (proof, subst, assums) = + (Have (qs, l, t, + case by of + ByMetis facts => ByMetis (relabel_facts subst facts) + | CaseSplit (proofs, facts) => + CaseSplit (map do_proof proofs, relabel_facts subst facts)) :: + proof, subst, assums) + | do_step step (proof, subst, assums) = (step :: proof, subst, assums) + and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev + in do_proof end + +val then_chain_proof = + let + fun aux _ [] = [] + | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof + | aux l' (Have (qs, l, t, by) :: proof) = + (case by of + ByMetis (ls, ss) => + Have (if member (op =) ls l' then + (Then :: qs, l, t, + ByMetis (filter_out (curry (op =) l') ls, ss)) + else + (qs, l, t, ByMetis (ls, ss))) + | CaseSplit (proofs, facts) => + Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) :: + aux l proof + | aux _ (step :: proof) = step :: aux no_label proof + in aux no_label end + +fun kill_useless_labels_in_proof proof = + let + val used_ls = used_labels_of proof + fun do_label l = if member (op =) used_ls l then l else no_label + fun do_step (Assume (l, t)) = Assume (do_label l, t) + | do_step (Have (qs, l, t, by)) = + Have (qs, do_label l, t, + case by of + CaseSplit (proofs, facts) => + CaseSplit (map (map do_step) proofs, facts) + | _ => by) + | do_step step = step + in map do_step proof end + +fun prefix_for_depth n = replicate_string (n + 1) + +val relabel_proof = + let + fun aux _ _ _ [] = [] + | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) = + if l = no_label then + Assume (l, t) :: aux subst depth (next_assum, next_fact) proof + else + let val l' = (prefix_for_depth depth assum_prefix, next_assum) in + Assume (l', t) :: + aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof + end + | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) = + let + val (l', subst, next_fact) = + if l = no_label then + (l, subst, next_fact) + else + let + val l' = (prefix_for_depth depth fact_prefix, next_fact) + in (l', (l, l') :: subst, next_fact + 1) end + val relabel_facts = + apfst (maps (the_list o AList.lookup (op =) subst)) + val by = + case by of + ByMetis facts => ByMetis (relabel_facts facts) + | CaseSplit (proofs, facts) => + CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs, + relabel_facts facts) + in + Have (qs, l', t, by) :: + aux subst depth (next_assum, next_fact) proof + end + | aux subst depth nextp (step :: proof) = + step :: aux subst depth nextp proof + in aux [] 0 (1, 1) end + +fun string_for_proof ctxt0 full_types i n = + let + val ctxt = ctxt0 + |> Config.put show_free_types false + |> Config.put show_types true + fun fix_print_mode f x = + Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) + (print_mode_value ())) f x + fun do_indent ind = replicate_string (ind * indent_size) " " + fun do_free (s, T) = + maybe_quote s ^ " :: " ^ + maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T) + fun do_label l = if l = no_label then "" else string_for_label l ^ ": " + fun do_have qs = + (if member (op =) qs Moreover then "moreover " else "") ^ + (if member (op =) qs Ultimately then "ultimately " else "") ^ + (if member (op =) qs Then then + if member (op =) qs Show then "thus" else "hence" + else + if member (op =) qs Show then "show" else "have") + val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) + fun do_facts (ls, ss) = + metis_command full_types 1 1 + (ls |> sort_distinct (prod_ord string_ord int_ord), + ss |> sort_distinct string_ord) + and do_step ind (Fix xs) = + do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" + | do_step ind (Let (t1, t2)) = + do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" + | do_step ind (Assume (l, t)) = + do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" + | do_step ind (Have (qs, l, t, ByMetis facts)) = + do_indent ind ^ do_have qs ^ " " ^ + do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n" + | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) = + space_implode (do_indent ind ^ "moreover\n") + (map (do_block ind) proofs) ^ + do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^ + do_facts facts ^ "\n" + and do_steps prefix suffix ind steps = + let val s = implode (map (do_step ind) steps) in + replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ + String.extract (s, ind * indent_size, + SOME (size s - ind * indent_size - 1)) ^ + suffix ^ "\n" + end + and do_block ind proof = do_steps "{ " " }" (ind + 1) proof + (* One-step proofs are pointless; better use the Metis one-liner + directly. *) + and do_proof [Have (_, _, _, ByMetis _)] = "" + | do_proof proof = + (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ + do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ + (if n <> 1 then "next" else "qed") + in do_proof end + +fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) + (other_params as (_, full_types, _, tstplike_proof, + axiom_names, goal, i)) = + let + val (params, hyp_ts, concl_t) = strip_subgoal goal i + val frees = fold Term.add_frees (concl_t :: hyp_ts) [] + val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] + val n = Logic.count_prems (prop_of goal) + val (one_line_proof, lemma_names) = metis_proof_text other_params + fun isar_proof_for () = + case isar_proof_from_tstplike_proof pool ctxt full_types tfrees + isar_shrink_factor tstplike_proof conjecture_shape axiom_names + params frees + |> redirect_proof hyp_ts concl_t + |> kill_duplicate_assumptions_in_proof + |> then_chain_proof + |> kill_useless_labels_in_proof + |> relabel_proof + |> string_for_proof ctxt full_types i n of + "" => "\nNo structured proof available." + | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof + val isar_proof = + if debug then + isar_proof_for () + else + try isar_proof_for () + |> the_default "\nWarning: The Isar proof construction failed." + in (one_line_proof ^ isar_proof, lemma_names) end + +fun proof_text isar_proof isar_params other_params = + (if isar_proof then isar_proof_text isar_params else metis_proof_text) + other_params + +end; diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri Oct 22 17:15:46 2010 +0200 @@ -0,0 +1,534 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_translate.ML + Author: Fabian Immler, TU Muenchen + Author: Makarius + Author: Jasmin Blanchette, TU Muenchen + +Translation of HOL to FOL for Sledgehammer. +*) + +signature SLEDGEHAMMER_ATP_TRANSLATE = +sig + type 'a problem = 'a ATP_Problem.problem + type prepared_formula + + val axiom_prefix : string + val conjecture_prefix : string + val prepare_axiom : + Proof.context -> (string * 'a) * thm + -> term * ((string * 'a) * prepared_formula) option + val prepare_atp_problem : + Proof.context -> bool -> bool -> bool -> bool -> term list -> term + -> (term * ((string * 'a) * prepared_formula) option) list + -> string problem * string Symtab.table * int * (string * 'a) list vector +end; + +structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE = +struct + +open ATP_Problem +open Metis_Translate +open Sledgehammer_Util + +val axiom_prefix = "ax_" +val conjecture_prefix = "conj_" +val helper_prefix = "help_" +val class_rel_clause_prefix = "clrel_"; +val arity_clause_prefix = "arity_" +val tfree_prefix = "tfree_" + +(* Freshness almost guaranteed! *) +val sledgehammer_weak_prefix = "Sledgehammer:" + +type prepared_formula = + {name: string, + kind: kind, + combformula: (name, combterm) formula, + ctypes_sorts: typ list} + +fun mk_anot phi = AConn (ANot, [phi]) +fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) +fun mk_ahorn [] phi = phi + | mk_ahorn (phi :: phis) psi = + AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) + +fun combformula_for_prop thy = + let + val do_term = combterm_from_term thy ~1 + fun do_quant bs q s T t' = + let val s = Name.variant (map fst bs) s in + do_formula ((s, T) :: bs) t' + #>> (fn phi => AQuant (q, [`make_bound_var s], phi)) + end + and do_conn bs c t1 t2 = + do_formula bs t1 ##>> do_formula bs t2 + #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) + and do_formula bs t = + case t of + @{const Not} $ t1 => + do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) + | Const (@{const_name All}, _) $ Abs (s, T, t') => + do_quant bs AForall s T t' + | Const (@{const_name Ex}, _) $ Abs (s, T, t') => + do_quant bs AExists s T t' + | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2 + | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2 + | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2 + | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => + do_conn bs AIff t1 t2 + | _ => (fn ts => do_term bs (Envir.eta_contract t) + |>> AAtom ||> union (op =) ts) + in do_formula [] end + +val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm + +fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j +fun conceal_bounds Ts t = + subst_bounds (map (Free o apfst concealed_bound_name) + (0 upto length Ts - 1 ~~ Ts), t) +fun reveal_bounds Ts = + subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) + (0 upto length Ts - 1 ~~ Ts)) + +(* Removes the lambdas from an equation of the form "t = (%x. u)". + (Cf. "extensionalize_theorem" in "Meson_Clausify".) *) +fun extensionalize_term t = + let + fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t' + | aux j (t as Const (s, Type (_, [Type (_, [_, T']), + Type (_, [_, res_T])])) + $ t2 $ Abs (var_s, var_T, t')) = + if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then + let val var_t = Var ((var_s, j), var_T) in + Const (s, T' --> T' --> res_T) + $ betapply (t2, var_t) $ subst_bound (var_t, t') + |> aux (j + 1) + end + else + t + | aux _ t = t + in aux (maxidx_of_term t + 1) t end + +fun introduce_combinators_in_term ctxt kind t = + let val thy = ProofContext.theory_of ctxt in + if Meson.is_fol_term thy t then + t + else + let + fun aux Ts t = + case t of + @{const Not} $ t1 => @{const Not} $ aux Ts t1 + | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as Const (@{const_name All}, _)) $ t1 => + aux Ts (t0 $ eta_expand Ts t1 1) + | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as Const (@{const_name Ex}, _)) $ t1 => + aux Ts (t0 $ eta_expand Ts t1 1) + | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _]))) + $ t1 $ t2 => + t0 $ aux Ts t1 $ aux Ts t2 + | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then + t + else + t |> conceal_bounds Ts + |> Envir.eta_contract + |> cterm_of thy + |> Meson_Clausify.introduce_combinators_in_cterm + |> prop_of |> Logic.dest_equals |> snd + |> reveal_bounds Ts + val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single + in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end + handle THM _ => + (* A type variable of sort "{}" will make abstraction fail. *) + if kind = Conjecture then HOLogic.false_const + else HOLogic.true_const + end + +(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the + same in Sledgehammer to prevent the discovery of unreplable proofs. *) +fun freeze_term t = + let + fun aux (t $ u) = aux t $ aux u + | aux (Abs (s, T, t)) = Abs (s, T, aux t) + | aux (Var ((s, i), T)) = + Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) + | aux t = t + in t |> exists_subterm is_Var t ? aux end + +(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example, + it leaves metaequalities over "prop"s alone. *) +val atomize_term = + let + fun aux (@{const Trueprop} $ t1) = t1 + | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) = + HOLogic.all_const T $ Abs (s, T, aux t') + | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2)) + | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) = + HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2 + | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) = + HOLogic.eq_const T $ t1 $ t2 + | aux _ = raise Fail "aux" + in perhaps (try aux) end + +(* making axiom and conjecture formulas *) +fun make_formula ctxt presimp name kind t = + let + val thy = ProofContext.theory_of ctxt + val t = t |> Envir.beta_eta_contract + |> transform_elim_term + |> atomize_term + val need_trueprop = (fastype_of t = HOLogic.boolT) + val t = t |> need_trueprop ? HOLogic.mk_Trueprop + |> extensionalize_term + |> presimp ? presimplify_term thy + |> perhaps (try (HOLogic.dest_Trueprop)) + |> introduce_combinators_in_term ctxt kind + |> kind <> Axiom ? freeze_term + val (combformula, ctypes_sorts) = combformula_for_prop thy t [] + in + {name = name, combformula = combformula, kind = kind, + ctypes_sorts = ctypes_sorts} + end + +fun make_axiom ctxt presimp ((name, loc), th) = + case make_formula ctxt presimp name Axiom (prop_of th) of + {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE + | formula => SOME ((name, loc), formula) +fun make_conjecture ctxt ts = + let val last = length ts - 1 in + map2 (fn j => make_formula ctxt true (Int.toString j) + (if j = last then Conjecture else Hypothesis)) + (0 upto last) ts + end + +(** Helper facts **) + +fun count_combterm (CombConst ((s, _), _, _)) = + Symtab.map_entry s (Integer.add 1) + | count_combterm (CombVar _) = I + | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] +fun count_combformula (AQuant (_, _, phi)) = count_combformula phi + | count_combformula (AConn (_, phis)) = fold count_combformula phis + | count_combformula (AAtom tm) = count_combterm tm +fun count_prepared_formula ({combformula, ...} : prepared_formula) = + count_combformula combformula + +val optional_helpers = + [(["c_COMBI"], @{thms Meson.COMBI_def}), + (["c_COMBK"], @{thms Meson.COMBK_def}), + (["c_COMBB"], @{thms Meson.COMBB_def}), + (["c_COMBC"], @{thms Meson.COMBC_def}), + (["c_COMBS"], @{thms Meson.COMBS_def})] +val optional_typed_helpers = + [(["c_True", "c_False", "c_If"], @{thms True_or_False}), + (["c_If"], @{thms if_True if_False})] +val mandatory_helpers = @{thms Metis.fequal_def} + +val init_counters = + [optional_helpers, optional_typed_helpers] |> maps (maps fst) + |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make + +fun get_helper_facts ctxt is_FO full_types conjectures axioms = + let + val ct = + fold (fold count_prepared_formula) [conjectures, axioms] init_counters + fun is_needed c = the (Symtab.lookup ct c) > 0 + fun baptize th = ((Thm.get_name_hint th, false), th) + in + (optional_helpers + |> full_types ? append optional_typed_helpers + |> maps (fn (ss, ths) => + if exists is_needed ss then map baptize ths else [])) @ + (if is_FO then [] else map baptize mandatory_helpers) + |> map_filter (Option.map snd o make_axiom ctxt false) + end + +fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax) + +fun prepare_formulas ctxt full_types hyp_ts concl_t axioms = + let + val thy = ProofContext.theory_of ctxt + val (axiom_ts, prepared_axioms) = ListPair.unzip axioms + (* Remove existing axioms from the conjecture, as this can dramatically + boost an ATP's performance (for some reason). *) + val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts) + val goal_t = Logic.list_implies (hyp_ts, concl_t) + val is_FO = Meson.is_fol_term thy goal_t + val subs = tfree_classes_of_terms [goal_t] + val supers = tvar_classes_of_terms axiom_ts + val tycons = type_consts_of_terms thy (goal_t :: axiom_ts) + (* TFrees in the conjecture; TVars in the axioms *) + val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t]) + val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms) + val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms + val (supers', arity_clauses) = make_arity_clauses thy tycons supers + val class_rel_clauses = make_class_rel_clauses thy subs supers' + in + (axiom_names |> map single |> Vector.fromList, + (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) + end + +fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) + +fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) + | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) + | fo_term_for_combtyp (CombType (name, tys)) = + ATerm (name, map fo_term_for_combtyp tys) + +fun fo_literal_for_type_literal (TyLitVar (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + | fo_literal_for_type_literal (TyLitFree (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + +fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot + +fun fo_term_for_combterm full_types = + let + fun aux top_level u = + let + val (head, args) = strip_combterm_comb u + val (x, ty_args) = + case head of + CombConst (name as (s, s'), _, ty_args) => + let val ty_args = if full_types then [] else ty_args in + if s = "equal" then + if top_level andalso length args = 2 then (name, []) + else (("c_fequal", @{const_name Metis.fequal}), ty_args) + else if top_level then + case s of + "c_False" => (("$false", s'), []) + | "c_True" => (("$true", s'), []) + | _ => (name, ty_args) + else + (name, ty_args) + end + | CombVar (name, _) => (name, []) + | CombApp _ => raise Fail "impossible \"CombApp\"" + val t = ATerm (x, map fo_term_for_combtyp ty_args @ + map (aux false) args) + in + if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t + end + in aux true end + +fun formula_for_combformula full_types = + let + fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) + | aux (AConn (c, phis)) = AConn (c, map aux phis) + | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm) + in aux end + +fun formula_for_axiom full_types + ({combformula, ctypes_sorts, ...} : prepared_formula) = + mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) + (type_literals_for_types ctypes_sorts)) + (formula_for_combformula full_types combformula) + +fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) = + Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula) + +fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, + superclass, ...}) = + let val ty_arg = ATerm (("T", "T"), []) in + Fof (class_rel_clause_prefix ^ ascii_of name, Axiom, + AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), + AAtom (ATerm (superclass, [ty_arg]))])) + end + +fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = + (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) + | fo_literal_for_arity_literal (TVarLit (c, sort)) = + (false, ATerm (c, [ATerm (sort, [])])) + +fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits, + ...}) = + Fof (arity_clause_prefix ^ ascii_of name, Axiom, + mk_ahorn (map (formula_for_fo_literal o apfst not + o fo_literal_for_arity_literal) premLits) + (formula_for_fo_literal + (fo_literal_for_arity_literal conclLit))) + +fun problem_line_for_conjecture full_types + ({name, kind, combformula, ...} : prepared_formula) = + Fof (conjecture_prefix ^ name, kind, + formula_for_combformula full_types combformula) + +fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : prepared_formula) = + map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) + +fun problem_line_for_free_type j lit = + Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit) +fun problem_lines_for_free_types conjectures = + let + val litss = map free_type_literals_for_conjecture conjectures + val lits = fold (union (op =)) litss [] + in map2 problem_line_for_free_type (0 upto length lits - 1) lits end + +(** "hBOOL" and "hAPP" **) + +type const_info = {min_arity: int, max_arity: int, sub_level: bool} + +fun consider_term top_level (ATerm ((s, _), ts)) = + (if is_atp_variable s then + I + else + let val n = length ts in + Symtab.map_default + (s, {min_arity = n, max_arity = 0, sub_level = false}) + (fn {min_arity, max_arity, sub_level} => + {min_arity = Int.min (n, min_arity), + max_arity = Int.max (n, max_arity), + sub_level = sub_level orelse not top_level}) + end) + #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts +fun consider_formula (AQuant (_, _, phi)) = consider_formula phi + | consider_formula (AConn (_, phis)) = fold consider_formula phis + | consider_formula (AAtom tm) = consider_term true tm + +fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi +fun consider_problem problem = fold (fold consider_problem_line o snd) problem + +fun const_table_for_problem explicit_apply problem = + if explicit_apply then NONE + else SOME (Symtab.empty |> consider_problem problem) + +fun min_arity_of thy full_types NONE s = + (if s = "equal" orelse s = type_wrapper_name orelse + String.isPrefix type_const_prefix s orelse + String.isPrefix class_prefix s then + 16383 (* large number *) + else if full_types then + 0 + else case strip_prefix_and_unascii const_prefix s of + SOME s' => num_type_args thy (invert_const s') + | NONE => 0) + | min_arity_of _ _ (SOME the_const_tab) s = + case Symtab.lookup the_const_tab s of + SOME ({min_arity, ...} : const_info) => min_arity + | NONE => 0 + +fun full_type_of (ATerm ((s, _), [ty, _])) = + if s = type_wrapper_name then ty else raise Fail "expected type wrapper" + | full_type_of _ = raise Fail "expected type wrapper" + +fun list_hAPP_rev _ t1 [] = t1 + | list_hAPP_rev NONE t1 (t2 :: ts2) = + ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) + | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = + let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, + [full_type_of t2, ty]) in + ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) + end + +fun repair_applications_in_term thy full_types const_tab = + let + fun aux opt_ty (ATerm (name as (s, _), ts)) = + if s = type_wrapper_name then + case ts of + [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) + | _ => raise Fail "malformed type wrapper" + else + let + val ts = map (aux NONE) ts + val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts + in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end + in aux NONE end + +fun boolify t = ATerm (`I "hBOOL", [t]) + +(* True if the constant ever appears outside of the top-level position in + literals, or if it appears with different arities (e.g., because of different + type instantiations). If false, the constant always receives all of its + arguments and is used as a predicate. *) +fun is_predicate NONE s = + s = "equal" orelse s = "$false" orelse s = "$true" orelse + String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s + | is_predicate (SOME the_const_tab) s = + case Symtab.lookup the_const_tab s of + SOME {min_arity, max_arity, sub_level} => + not sub_level andalso min_arity = max_arity + | NONE => false + +fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = + if s = type_wrapper_name then + case ts of + [_, t' as ATerm ((s', _), _)] => + if is_predicate const_tab s' then t' else boolify t + | _ => raise Fail "malformed type wrapper" + else + t |> not (is_predicate const_tab s) ? boolify + +fun close_universally phi = + let + fun term_vars bounds (ATerm (name as (s, _), tms)) = + (is_atp_variable s andalso not (member (op =) bounds name)) + ? insert (op =) name + #> fold (term_vars bounds) tms + fun formula_vars bounds (AQuant (_, xs, phi)) = + formula_vars (xs @ bounds) phi + | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis + | formula_vars bounds (AAtom tm) = term_vars bounds tm + in + case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) + end + +fun repair_formula thy explicit_forall full_types const_tab = + let + fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) + | aux (AConn (c, phis)) = AConn (c, map aux phis) + | aux (AAtom tm) = + AAtom (tm |> repair_applications_in_term thy full_types const_tab + |> repair_predicates_in_term const_tab) + in aux #> explicit_forall ? close_universally end + +fun repair_problem_line thy explicit_forall full_types const_tab + (Fof (ident, kind, phi)) = + Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) +fun repair_problem_with_const_table thy = + map o apsnd o map ooo repair_problem_line thy + +fun repair_problem thy explicit_forall full_types explicit_apply problem = + repair_problem_with_const_table thy explicit_forall full_types + (const_table_for_problem explicit_apply problem) problem + +fun prepare_atp_problem ctxt readable_names explicit_forall full_types + explicit_apply hyp_ts concl_t axioms = + let + val thy = ProofContext.theory_of ctxt + val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses, + arity_clauses)) = + prepare_formulas ctxt full_types hyp_ts concl_t axioms + val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms + val helper_lines = + map (problem_line_for_fact helper_prefix full_types) helper_facts + val conjecture_lines = + map (problem_line_for_conjecture full_types) conjectures + val tfree_lines = problem_lines_for_free_types conjectures + val class_rel_lines = + map problem_line_for_class_rel_clause class_rel_clauses + val arity_lines = map problem_line_for_arity_clause arity_clauses + (* Reordering these might or might not confuse the proof reconstruction + code or the SPASS Flotter hack. *) + val problem = + [("Relevant facts", axiom_lines), + ("Class relationships", class_rel_lines), + ("Arity declarations", arity_lines), + ("Helper facts", helper_lines), + ("Conjectures", conjecture_lines), + ("Type variables", tfree_lines)] + |> repair_problem thy explicit_forall full_types explicit_apply + val (problem, pool) = nice_atp_problem readable_names problem + val conjecture_offset = + length axiom_lines + length class_rel_lines + length arity_lines + + length helper_lines + in + (problem, + case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, + conjecture_offset, axiom_names) + end + +end; diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Oct 22 13:59:34 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Oct 22 17:15:46 2010 +0200 @@ -9,35 +9,38 @@ sig datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained + type relevance_fudge = + {worse_irrel_freq : real, + higher_order_irrel_weight : real, + abs_rel_weight : real, + abs_irrel_weight : real, + skolem_irrel_weight : real, + theory_const_rel_weight : real, + theory_const_irrel_weight : real, + intro_bonus : real, + elim_bonus : real, + simp_bonus : real, + local_bonus : real, + assum_bonus : real, + chained_bonus : real, + max_imperfect : real, + max_imperfect_exp : real, + threshold_divisor : real, + ridiculous_threshold : real} + type relevance_override = - {add: (Facts.ref * Attrib.src list) list, - del: (Facts.ref * Attrib.src list) list, - only: bool} + {add : (Facts.ref * Attrib.src list) list, + del : (Facts.ref * Attrib.src list) list, + only : bool} val trace : bool Unsynchronized.ref - val worse_irrel_freq : real Unsynchronized.ref - val higher_order_irrel_weight : real Unsynchronized.ref - val abs_rel_weight : real Unsynchronized.ref - val abs_irrel_weight : real Unsynchronized.ref - val skolem_irrel_weight : real Unsynchronized.ref - val theory_const_rel_weight : real Unsynchronized.ref - val theory_const_irrel_weight : real Unsynchronized.ref - val intro_bonus : real Unsynchronized.ref - val elim_bonus : real Unsynchronized.ref - val simp_bonus : real Unsynchronized.ref - val local_bonus : real Unsynchronized.ref - val assum_bonus : real Unsynchronized.ref - val chained_bonus : real Unsynchronized.ref - val max_imperfect : real Unsynchronized.ref - val max_imperfect_exp : real Unsynchronized.ref - val threshold_divisor : real Unsynchronized.ref - val ridiculous_threshold : real Unsynchronized.ref val name_thm_pairs_from_ref : Proof.context -> unit Symtab.table -> thm list -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list val relevant_facts : - Proof.context -> bool -> real * real -> int -> relevance_override - -> thm list -> term list -> term -> ((string * locality) * thm) list + Proof.context -> bool -> real * real -> int -> string list + -> relevance_fudge -> relevance_override -> thm list -> term list -> term + -> ((string * locality) * thm) list end; structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER = @@ -52,31 +55,31 @@ val term_patterns = false val respect_no_atp = true -(* FUDGE *) -val worse_irrel_freq = Unsynchronized.ref 100.0 -val higher_order_irrel_weight = Unsynchronized.ref 1.05 -val abs_rel_weight = Unsynchronized.ref 0.5 -val abs_irrel_weight = Unsynchronized.ref 2.0 -val skolem_irrel_weight = Unsynchronized.ref 0.75 -val theory_const_rel_weight = Unsynchronized.ref 0.5 -val theory_const_irrel_weight = Unsynchronized.ref 0.25 -val intro_bonus = Unsynchronized.ref 0.15 -val elim_bonus = Unsynchronized.ref 0.15 -val simp_bonus = Unsynchronized.ref 0.15 -val local_bonus = Unsynchronized.ref 0.55 -val assum_bonus = Unsynchronized.ref 1.05 -val chained_bonus = Unsynchronized.ref 1.5 -val max_imperfect = Unsynchronized.ref 11.5 -val max_imperfect_exp = Unsynchronized.ref 1.0 -val threshold_divisor = Unsynchronized.ref 2.0 -val ridiculous_threshold = Unsynchronized.ref 0.1 - datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained +type relevance_fudge = + {worse_irrel_freq : real, + higher_order_irrel_weight : real, + abs_rel_weight : real, + abs_irrel_weight : real, + skolem_irrel_weight : real, + theory_const_rel_weight : real, + theory_const_irrel_weight : real, + intro_bonus : real, + elim_bonus : real, + simp_bonus : real, + local_bonus : real, + assum_bonus : real, + chained_bonus : real, + max_imperfect : real, + max_imperfect_exp : real, + threshold_divisor : real, + ridiculous_threshold : real} + type relevance_override = - {add: (Facts.ref * Attrib.src list) list, - del: (Facts.ref * Attrib.src list) list, - only: bool} + {add : (Facts.ref * Attrib.src list) list, + del : (Facts.ref * Attrib.src list) list, + only : bool} val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator val abs_name = sledgehammer_prefix ^ "abs" @@ -172,16 +175,10 @@ fun string_for_hyper_pconst (s, ps) = s ^ "{" ^ commas (map string_for_ptype ps) ^ "}" -(* These are typically simplified away by "Meson.presimplify". Equality is - handled specially via "fequal". *) -val boring_consts = - [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, - @{const_name HOL.eq}] - (* Add a pconstant to the table, but a [] entry means a standard connective, which we ignore.*) -fun add_pconst_to_table also_skolem (c, p) = - if member (op =) boring_consts c orelse +fun add_pconst_to_table irrelevant_consts also_skolem (c, p) = + if member (op =) irrelevant_consts c orelse (not also_skolem andalso String.isPrefix skolem_prefix c) then I else @@ -189,14 +186,15 @@ fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) -fun pconsts_in_terms thy also_skolems pos ts = +fun pconsts_in_terms thy irrelevant_consts also_skolems pos ts = let val flip = Option.map not (* We include free variables, as well as constants, to handle locales. For each quantifiers that must necessarily be skolemized by the ATP, we introduce a fresh constant to simulate the effect of Skolemization. *) fun do_const const (s, T) ts = - add_pconst_to_table also_skolems (rich_pconst thy const (s, T) ts) + add_pconst_to_table irrelevant_consts also_skolems + (rich_pconst thy const (s, T) ts) #> fold do_term ts and do_term t = case strip_comb t of @@ -204,13 +202,14 @@ | (Free x, ts) => do_const false x ts | (Abs (_, T, t'), ts) => (null ts - ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, []))) + ? add_pconst_to_table irrelevant_consts true + (abs_name, PType (order_of_type T + 1, []))) #> fold do_term (t' :: ts) | (_, ts) => fold do_term ts fun do_quantifier will_surely_be_skolemized abs_T body_t = do_formula pos body_t #> (if also_skolems andalso will_surely_be_skolemized then - add_pconst_to_table true + add_pconst_to_table irrelevant_consts true (gensym skolem_prefix, PType (order_of_type abs_T, [])) else I) @@ -254,9 +253,11 @@ (*Inserts a dummy "constant" referring to the theory name, so that relevance takes the given theory into account.*) -fun theory_const_prop_of th = - if exists (curry (op <) 0.0) [!theory_const_rel_weight, - !theory_const_irrel_weight] then +fun theory_const_prop_of ({theory_const_rel_weight, + theory_const_irrel_weight, ...} : relevance_fudge) + th = + if exists (curry (op <) 0.0) [theory_const_rel_weight, + theory_const_irrel_weight] then let val name = Context.theory_name (theory_of_thm th) val t = Const (name ^ theory_const_suffix, @{typ bool}) @@ -282,7 +283,7 @@ structure PType_Tab = Table(type key = ptype val ord = ptype_ord) -fun count_axiom_consts thy = +fun count_axiom_consts thy fudge = let fun do_const const (s, T) ts = (* Two-dimensional table update. Constant maps to types maps to count. *) @@ -295,7 +296,7 @@ | (Free x, ts) => do_const false x ts | (Abs (_, _, t'), ts) => fold do_term (t' :: ts) | (_, ts) => fold do_term ts - in do_term o theory_const_prop_of o snd end + in do_term o theory_const_prop_of fudge o snd end (**** Actual Filtering Code ****) @@ -322,11 +323,12 @@ very rare constants and very common ones -- the former because they can't lead to the inclusion of too many new facts, and the latter because they are so common as to be of little interest. *) -fun irrel_weight_for order freq = - let val (k, x) = !worse_irrel_freq |> `Real.ceil in +fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...} + : relevance_fudge) order freq = + let val (k, x) = worse_irrel_freq |> `Real.ceil in (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x else rel_weight_for order freq / rel_weight_for order k) - * pow_int (!higher_order_irrel_weight) (order - 1) + * pow_int higher_order_irrel_weight (order - 1) end (* Computes a constant's weight, as determined by its frequency. *) @@ -337,22 +339,25 @@ else if String.isSuffix theory_const_suffix s then theory_const_weight else weight_for m (pconst_freq (match_ptype o f) const_tab c) -fun rel_pconst_weight const_tab = - generic_pconst_weight (!abs_rel_weight) 0.0 (!theory_const_rel_weight) +fun rel_pconst_weight ({abs_rel_weight, theory_const_rel_weight, ...} + : relevance_fudge) const_tab = + generic_pconst_weight abs_rel_weight 0.0 theory_const_rel_weight rel_weight_for I const_tab -fun irrel_pconst_weight const_tab = - generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight) - (!theory_const_irrel_weight) irrel_weight_for swap const_tab +fun irrel_pconst_weight (fudge as {abs_irrel_weight, skolem_irrel_weight, + theory_const_irrel_weight, ...}) const_tab = + generic_pconst_weight abs_irrel_weight skolem_irrel_weight + theory_const_irrel_weight (irrel_weight_for fudge) swap + const_tab -fun locality_bonus General = 0.0 - | locality_bonus Intro = !intro_bonus - | locality_bonus Elim = !elim_bonus - | locality_bonus Simp = !simp_bonus - | locality_bonus Local = !local_bonus - | locality_bonus Assum = !assum_bonus - | locality_bonus Chained = !chained_bonus +fun locality_bonus (_ : relevance_fudge) General = 0.0 + | locality_bonus {intro_bonus, ...} Intro = intro_bonus + | locality_bonus {elim_bonus, ...} Elim = elim_bonus + | locality_bonus {simp_bonus, ...} Simp = simp_bonus + | locality_bonus {local_bonus, ...} Local = local_bonus + | locality_bonus {assum_bonus, ...} Assum = assum_bonus + | locality_bonus {chained_bonus, ...} Chained = chained_bonus -fun axiom_weight loc const_tab relevant_consts axiom_consts = +fun axiom_weight fudge loc const_tab relevant_consts axiom_consts = case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts) ||> filter_out (pconst_hyper_mem swap relevant_consts) of ([], _) => 0.0 @@ -360,15 +365,15 @@ let val irrel = irrel |> filter_out (pconst_mem swap rel) val rel_weight = - 0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel + 0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel val irrel_weight = - ~ (locality_bonus loc) - |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel + ~ (locality_bonus fudge loc) + |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel val res = rel_weight / (rel_weight + irrel_weight) in if Real.isFinite res then res else 0.0 end (* FIXME: experiment -fun debug_axiom_weight loc const_tab relevant_consts axiom_consts = +fun debug_axiom_weight fudge loc const_tab relevant_consts axiom_consts = case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts) ||> filter_out (pconst_hyper_mem swap relevant_consts) of ([], _) => 0.0 @@ -378,19 +383,20 @@ val rels_weight = 0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel val irrels_weight = - ~ (locality_bonus loc) - |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel + ~ (locality_bonus fudge loc) + |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel val _ = tracing (PolyML.makestring ("REL: ", map (`(rel_pconst_weight const_tab)) rel)) -val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight const_tab)) irrel)) +val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight fudge const_tab)) irrel)) val res = rels_weight / (rels_weight + irrels_weight) in if Real.isFinite res then res else 0.0 end *) -fun pconsts_in_axiom thy t = +fun pconsts_in_axiom thy irrelevant_consts t = Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) - (pconsts_in_terms thy true (SOME true) [t]) [] -fun pair_consts_axiom thy axiom = - case axiom |> snd |> theory_const_prop_of |> pconsts_in_axiom thy of + (pconsts_in_terms thy irrelevant_consts true (SOME true) [t]) [] +fun pair_consts_axiom thy irrelevant_consts fudge axiom = + case axiom |> snd |> theory_const_prop_of fudge + |> pconsts_in_axiom thy irrelevant_consts of [] => NONE | consts => SOME ((axiom, consts), NONE) @@ -398,12 +404,13 @@ (((unit -> string) * locality) * thm) * (string * ptype) list fun take_most_relevant max_relevant remaining_max - (candidates : (annotated_thm * real) list) = + ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge) + (candidates : (annotated_thm * real) list) = let val max_imperfect = - Real.ceil (Math.pow (!max_imperfect, + Real.ceil (Math.pow (max_imperfect, Math.pow (Real.fromInt remaining_max - / Real.fromInt max_relevant, !max_imperfect_exp))) + / Real.fromInt max_relevant, max_imperfect_exp))) val (perfect, imperfect) = candidates |> sort (Real.compare o swap o pairself snd) |> take_prefix (fn (_, w) => w > 0.99999) @@ -419,22 +426,23 @@ (accepts, more_rejects @ rejects) end -fun if_empty_replace_with_locality thy axioms loc tab = +fun if_empty_replace_with_locality thy irrelevant_consts axioms loc tab = if Symtab.is_empty tab then - pconsts_in_terms thy false (SOME false) + pconsts_in_terms thy irrelevant_consts false (SOME false) (map_filter (fn ((_, loc'), th) => if loc' = loc then SOME (prop_of th) else NONE) axioms) else tab -fun relevance_filter ctxt threshold0 decay max_relevant - ({add, del, ...} : relevance_override) axioms goal_ts = +fun relevance_filter ctxt threshold0 decay max_relevant irrelevant_consts + (fudge as {threshold_divisor, ridiculous_threshold, ...}) + ({add, del, ...} : relevance_override) axioms goal_ts = let val thy = ProofContext.theory_of ctxt - val const_tab = fold (count_axiom_consts thy) axioms Symtab.empty + val const_tab = fold (count_axiom_consts thy fudge) axioms Symtab.empty val goal_const_tab = - pconsts_in_terms thy false (SOME false) goal_ts - |> fold (if_empty_replace_with_locality thy axioms) + pconsts_in_terms thy irrelevant_consts false (SOME false) goal_ts + |> fold (if_empty_replace_with_locality thy irrelevant_consts axioms) [Chained, Assum, Local] val add_ths = Attrib.eval_thms ctxt add val del_ths = Attrib.eval_thms ctxt del @@ -450,19 +458,20 @@ else NONE) rejects fun relevant [] rejects [] = (* Nothing has been added this iteration. *) - if j = 0 andalso threshold >= !ridiculous_threshold then + if j = 0 andalso threshold >= ridiculous_threshold then (* First iteration? Try again. *) - iter 0 max_relevant (threshold / !threshold_divisor) rel_const_tab + iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab hopeless hopeful else game_over (rejects @ hopeless) | relevant candidates rejects [] = let val (accepts, more_rejects) = - take_most_relevant max_relevant remaining_max candidates + take_most_relevant max_relevant remaining_max fudge candidates val rel_const_tab' = rel_const_tab - |> fold (add_pconst_to_table false) (maps (snd o fst) accepts) + |> fold (add_pconst_to_table irrelevant_consts false) + (maps (snd o fst) accepts) fun is_dirty (c, _) = Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c val (hopeful_rejects, hopeless_rejects) = @@ -499,11 +508,12 @@ val weight = case cached_weight of SOME w => w - | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts + | NONE => axiom_weight fudge loc const_tab rel_const_tab + axiom_consts (* FIXME: experiment val name = fst (fst (fst ax)) () val _ = if String.isSubstring "positive_minus" name orelse String.isSubstring "not_exp_le_zero" name then -tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight loc const_tab rel_const_tab axiom_consts)) +tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight fudge loc const_tab rel_const_tab axiom_consts)) else () *) @@ -524,7 +534,7 @@ end in axioms |> filter_out (member Thm.eq_thm del_ths o snd) - |> map_filter (pair_consts_axiom thy) + |> map_filter (pair_consts_axiom thy irrelevant_consts fudge) |> iter 0 max_relevant threshold0 goal_const_tab [] |> tap (fn res => trace_msg (fn () => "Total relevant: " ^ Int.toString (length res))) @@ -708,7 +718,9 @@ (Term.add_vars t [] |> sort_wrt (fst o fst)) |> fst -fun all_name_thms_pairs ctxt reserved full_types add_ths chained_ths = +fun all_name_thms_pairs ctxt reserved full_types + ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge) add_ths + chained_ths = let val thy = ProofContext.theory_of ctxt val global_facts = Global_Theory.facts_of thy @@ -718,7 +730,7 @@ fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms val is_chained = member Thm.eq_thm chained_ths val (intros, elims, simps) = - if exists (curry (op <) 0.0) [!intro_bonus, !elim_bonus, !simp_bonus] then + if exists (curry (op <) 0.0) [intro_bonus, elim_bonus, simp_bonus] then clasimpset_rules_of ctxt else (Termtab.empty, Termtab.empty, Termtab.empty) @@ -773,7 +785,8 @@ | NONE => "" end), let val t = prop_of th in - if is_chained th then Chained + if is_chained th then + Chained else if global then if Termtab.defined intros t then Intro else if Termtab.defined elims t then Elim @@ -801,8 +814,8 @@ (***************************************************************) fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant - (relevance_override as {add, only, ...}) chained_ths hyp_ts - concl_t = + irrelevant_consts fudge (override as {add, only, ...}) + chained_ths hyp_ts concl_t = let val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0), 1.0 / Real.fromInt (max_relevant + 1)) @@ -813,7 +826,7 @@ maps (map (fn ((name, loc), th) => ((K name, loc), (true, th))) o name_thm_pairs_from_ref ctxt reserved chained_ths) add else - all_name_thms_pairs ctxt reserved full_types add_ths chained_ths) + all_name_thms_pairs ctxt reserved full_types fudge add_ths chained_ths) |> name_thm_pairs ctxt (respect_no_atp andalso not only) |> uniquify in @@ -825,8 +838,8 @@ max_relevant = 0 then [] else - relevance_filter ctxt threshold0 decay max_relevant relevance_override - axioms (concl_t :: hyp_ts)) + relevance_filter ctxt threshold0 decay max_relevant irrelevant_consts + fudge override axioms (concl_t :: hyp_ts)) |> map (apfst (apfst (fn f => f ()))) end diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 22 13:59:34 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 22 17:15:46 2010 +0200 @@ -9,10 +9,10 @@ type params = Sledgehammer.params val auto : bool Unsynchronized.ref - val atps : string Unsynchronized.ref + val provers : string Unsynchronized.ref val timeout : int Unsynchronized.ref val full_types : bool Unsynchronized.ref - val default_params : theory -> (string * string) list -> params + val default_params : Proof.context -> (string * string) list -> params val setup : theory -> theory end; @@ -49,14 +49,14 @@ (*** parameters ***) -val atps = Unsynchronized.ref "" +val provers = Unsynchronized.ref "" val timeout = Unsynchronized.ref 30 val full_types = Unsynchronized.ref false val _ = ProofGeneralPgip.add_preference Preferences.category_proof - (Preferences.string_pref atps - "Sledgehammer: ATPs" + (Preferences.string_pref provers + "Sledgehammer: Provers" "Default automatic provers (separated by whitespace)") val _ = @@ -84,7 +84,9 @@ ("isar_shrink_factor", "1")] val alias_params = - [("atp", "atps")] + [("prover", "provers"), + ("atps", "provers"), (* FIXME: legacy *) + ("atp", "provers")] (* FIXME: legacy *) val negated_alias_params = [("non_blocking", "blocking"), ("no_debug", "debug"), @@ -98,7 +100,7 @@ ["debug", "verbose", "overlord", "full_types", "isar_proof", "isar_shrink_factor", "timeout"] -val property_dependent_params = ["atps", "full_types", "timeout"] +val property_dependent_params = ["provers", "full_types", "timeout"] fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse @@ -128,16 +130,57 @@ val extend = I fun merge p : T = AList.merge (op =) (K true) p) +(* FIXME: dummy *) +fun is_smt_solver_installed ctxt = true + +fun remotify_prover_if_available_and_not_already_remote thy name = + if String.isPrefix remote_prefix name then + SOME name + else + let val remote_name = remote_prefix ^ name in + if is_prover_available thy remote_name then SOME remote_name else NONE + end + +fun remotify_prover_if_not_installed ctxt name = + let val thy = ProofContext.theory_of ctxt in + if is_prover_available thy name andalso is_prover_installed ctxt name then + SOME name + else + remotify_prover_if_available_and_not_already_remote thy name + end + +fun avoid_too_many_local_threads _ _ [] = [] + | avoid_too_many_local_threads thy 0 provers = + map_filter (remotify_prover_if_available_and_not_already_remote thy) provers + | avoid_too_many_local_threads thy n (prover :: provers) = + let val n = if String.isPrefix remote_prefix prover then n else n - 1 in + prover :: avoid_too_many_local_threads thy n provers + end + +(* The first ATP of the list is used by Auto Sledgehammer. Because of the low + timeout, it makes sense to put SPASS first. *) +fun default_provers_param_value ctxt = + let val thy = ProofContext.theory_of ctxt in + [spassN, eN, vampireN, sine_eN (* FIXME: , smtN *)] + |> map_filter (remotify_prover_if_not_installed ctxt) + |> avoid_too_many_local_threads thy (Thread.numProcessors ()) + |> space_implode " " + end + val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param -fun default_raw_params thy = - Data.get thy - |> fold (AList.default (op =)) - [("atps", [case !atps of "" => default_atps_param_value () | s => s]), - ("full_types", [if !full_types then "true" else "false"]), - ("timeout", let val timeout = !timeout in - [if timeout <= 0 then "none" - else string_of_int timeout ^ " s"] - end)] +fun default_raw_params ctxt = + let val thy = ProofContext.theory_of ctxt in + Data.get thy + |> fold (AList.default (op =)) + [("provers", [case !provers of + "" => default_provers_param_value ctxt + | s => s]), + ("full_types", [if !full_types then "true" else "false"]), + ("timeout", let val timeout = !timeout in + [if timeout <= 0 then "none" + else string_of_int timeout ^ " s"] + end)] + end val infinity_time_in_secs = 60 * 60 * 24 * 365 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs) @@ -180,7 +223,8 @@ val debug = not auto andalso lookup_bool "debug" val verbose = debug orelse (not auto andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" - val atps = lookup_string "atps" |> space_explode " " |> auto ? single o hd + val provers = lookup_string "provers" |> space_explode " " + |> auto ? single o hd val full_types = lookup_bool "full_types" val explicit_apply = lookup_bool "explicit_apply" val relevance_thresholds = @@ -193,13 +237,14 @@ val expect = lookup_string "expect" in {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord, - atps = atps, full_types = full_types, explicit_apply = explicit_apply, + provers = provers, full_types = full_types, + explicit_apply = explicit_apply, relevance_thresholds = relevance_thresholds, max_relevant = max_relevant, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = expect} end -fun get_params auto thy = extract_params auto (default_raw_params thy) +fun get_params auto ctxt = extract_params auto (default_raw_params ctxt) fun default_params thy = get_params false thy o map (apsnd single) (* Sledgehammer the given subgoal *) @@ -210,9 +255,9 @@ val runN = "run" val minimizeN = "minimize" val messagesN = "messages" -val available_atpsN = "available_atps" -val running_atpsN = "running_atps" -val kill_atpsN = "kill_atps" +val available_proversN = "available_provers" +val running_proversN = "running_provers" +val kill_proversN = "kill_provers" val refresh_tptpN = "refresh_tptp" val is_raw_param_relevant_for_minimize = @@ -220,8 +265,8 @@ fun string_for_raw_param (key, values) = key ^ (case space_implode " " values of "" => "" | value => " = " ^ value) -fun minimize_command override_params i atp_name fact_names = - sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^ +fun minimize_command override_params i prover_name fact_names = + sledgehammerN ^ " " ^ minimizeN ^ " [prover = " ^ prover_name ^ (override_params |> filter is_raw_param_relevant_for_minimize |> implode o map (prefix ", " o string_for_raw_param)) ^ "] (" ^ space_implode " " fact_names ^ ")" ^ @@ -229,27 +274,28 @@ fun hammer_away override_params subcommand opt_i relevance_override state = let + val ctxt = Proof.context_of state val thy = Proof.theory_of state val _ = app check_raw_param override_params in if subcommand = runN then let val i = the_default 1 opt_i in - run_sledgehammer (get_params false thy override_params) false i + run_sledgehammer (get_params false ctxt override_params) false i relevance_override (minimize_command override_params i) state |> K () end else if subcommand = minimizeN then - run_minimize (get_params false thy override_params) (the_default 1 opt_i) + run_minimize (get_params false ctxt override_params) (the_default 1 opt_i) (#add relevance_override) state else if subcommand = messagesN then messages opt_i - else if subcommand = available_atpsN then - available_atps thy - else if subcommand = running_atpsN then - running_atps () - else if subcommand = kill_atpsN then - kill_atps () + else if subcommand = available_proversN then + available_provers thy + else if subcommand = running_proversN then + running_provers () + else if subcommand = kill_proversN then + kill_provers () else if subcommand = refresh_tptpN then refresh_systems_on_tptp () else @@ -266,13 +312,15 @@ Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => - writeln ("Default parameters for Sledgehammer:\n" ^ - (case rev (default_raw_params thy) of - [] => "none" - | params => - (map check_raw_param params; - params |> map string_for_raw_param - |> sort_strings |> cat_lines))))) + let val ctxt = ProofContext.init_global thy in + writeln ("Default parameters for Sledgehammer:\n" ^ + (case default_raw_params ctxt |> rev of + [] => "none" + | params => + (map check_raw_param params; + params |> map string_for_raw_param + |> sort_strings |> cat_lines))) + end)) val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " val parse_value = Scan.repeat1 Parse.xname @@ -307,8 +355,8 @@ if not (!auto) then (false, state) else - let val thy = Proof.theory_of state in - run_sledgehammer (get_params true thy []) true 1 no_relevance_override + let val ctxt = Proof.context_of state in + run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override (minimize_command [] 1) state end diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 13:59:34 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 17:15:46 2010 +0200 @@ -2,7 +2,7 @@ Author: Philipp Meyer, TU Muenchen Author: Jasmin Blanchette, TU Muenchen -Minimization of theorem list for Metis using automatic theorem provers. +Minimization of fact list for Metis using ATPs. *) signature SLEDGEHAMMER_MINIMIZE = @@ -10,7 +10,7 @@ type locality = Sledgehammer_Filter.locality type params = Sledgehammer.params - val minimize_theorems : + val minimize_facts : params -> int -> int -> Proof.state -> ((string * locality) * thm list) list -> ((string * locality) * thm list) list option * string val run_minimize : @@ -23,8 +23,6 @@ open ATP_Proof open Sledgehammer_Util open Sledgehammer_Filter -open Sledgehammer_Translate -open Sledgehammer_Reconstruct open Sledgehammer (* wrapper for calling external prover *) @@ -34,9 +32,9 @@ | string_for_failure Interrupted = "Interrupted." | string_for_failure _ = "Unknown error." -fun n_theorems names = +fun n_facts names = let val n = length names in - string_of_int n ^ " theorem" ^ plural_s n ^ + string_of_int n ^ " fact" ^ plural_s n ^ (if n > 0 then ": " ^ (names |> map fst |> sort_distinct string_ord |> space_implode " ") @@ -44,46 +42,44 @@ "") end -fun test_theorems ({debug, verbose, overlord, atps, full_types, isar_proof, - isar_shrink_factor, ...} : params) - (prover : prover) explicit_apply timeout subgoal state - axioms = +fun test_facts ({debug, verbose, overlord, provers, full_types, isar_proof, + isar_shrink_factor, ...} : params) (prover : prover) + explicit_apply timeout i n state axioms = let val _ = - priority ("Testing " ^ n_theorems (map fst axioms) ^ "...") + priority ("Testing " ^ n_facts (map fst axioms) ^ "...") val params = {blocking = true, debug = debug, verbose = verbose, overlord = overlord, - atps = atps, full_types = full_types, explicit_apply = explicit_apply, - relevance_thresholds = (1.01, 1.01), - max_relevant = SOME 65536 (* a large number *), isar_proof = isar_proof, + provers = provers, full_types = full_types, + explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), + max_relevant = NONE, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} - val axioms = maps (fn (n, ths) => map (pair n) ths) axioms - val {context = ctxt, goal, ...} = Proof.goal state + val axioms = + axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n)) + val {goal, ...} = Proof.goal state val problem = - {state = state, goal = goal, subgoal = subgoal, - axioms = map (prepare_axiom ctxt) axioms, only = true} - val result as {outcome, used_thm_names, ...} = prover params (K "") problem + {state = state, goal = goal, subgoal = i, subgoal_count = n, + axioms = axioms, only = true} + val result as {outcome, used_axioms, ...} = prover params (K "") problem in priority (case outcome of - NONE => - if length used_thm_names = length axioms then - "Found proof." - else - "Found proof with " ^ n_theorems used_thm_names ^ "." - | SOME failure => string_for_failure failure); + SOME failure => string_for_failure failure + | NONE => + if length used_axioms = length axioms then "Found proof." + else "Found proof with " ^ n_facts used_axioms ^ "."); result end (* minimalization of thms *) -fun filter_used_facts used = filter (member (op =) used o fst) +fun filter_used_axioms used = filter (member (op =) used o fst) fun sublinear_minimize _ [] p = p | sublinear_minimize test (x :: xs) (seen, result) = case test (xs @ seen) of - result as {outcome = NONE, used_thm_names, ...} : prover_result => - sublinear_minimize test (filter_used_facts used_thm_names xs) - (filter_used_facts used_thm_names seen, result) + result as {outcome = NONE, used_axioms, ...} : prover_result => + sublinear_minimize test (filter_used_axioms used_axioms xs) + (filter_used_axioms used_axioms seen, result) | _ => sublinear_minimize test xs (x :: seen, result) (* Give the ATP some slack. The ATP gets further slack because the Sledgehammer @@ -91,48 +87,40 @@ timeout. *) val fudge_msecs = 1000 -fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set." - | minimize_theorems (params as {debug, atps = atp :: _, full_types, - isar_proof, isar_shrink_factor, timeout, ...}) - i (_ : int) state axioms = +fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set." + | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n + state axioms = let val thy = Proof.theory_of state - val prover = get_prover_fun thy atp + val prover = get_prover thy false prover_name val msecs = Time.toMilliseconds timeout - val _ = priority ("Sledgehammer minimize: ATP " ^ quote atp ^ ".") - val {context = ctxt, goal, ...} = Proof.goal state + val _ = priority ("Sledgehammer minimize: " ^ quote prover_name ^ ".") + val {goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i val explicit_apply = not (forall (Meson.is_fol_term thy) (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms)) fun do_test timeout = - test_theorems params prover explicit_apply timeout i state + test_facts params prover explicit_apply timeout i n state val timer = Timer.startRealTimer () in (case do_test timeout axioms of - result as {outcome = NONE, pool, used_thm_names, - conjecture_shape, ...} => + result as {outcome = NONE, used_axioms, ...} => let val time = Timer.checkRealTimer timer val new_timeout = Int.min (msecs, Time.toMilliseconds time + fudge_msecs) |> Time.fromMilliseconds - val (min_thms, {tstplike_proof, axiom_names, ...}) = + val (min_thms, {message, ...}) = sublinear_minimize (do_test new_timeout) - (filter_used_facts used_thm_names axioms) ([], result) + (filter_used_axioms used_axioms axioms) ([], result) val n = length min_thms val _ = priority (cat_lines - ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ + ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^ (case length (filter (curry (op =) Chained o snd o fst) min_thms) of 0 => "" | n => " (including " ^ Int.toString n ^ " chained)") ^ ".") - in - (SOME min_thms, - proof_text isar_proof - (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - ("Minimized command", full_types, K "", tstplike_proof, - axiom_names, goal, i) |> fst) - end + in (SOME min_thms, message) end | {outcome = SOME TimedOut, ...} => (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ \option (e.g., \"timeout = " ^ @@ -159,7 +147,8 @@ case subgoal_count state of 0 => priority "No subgoal!" | n => - (kill_atps (); priority (#2 (minimize_theorems params i n state axioms))) + (kill_provers (); + priority (#2 (minimize_facts params i n state axioms))) end end; diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Oct 22 13:59:34 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,941 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML - Author: Lawrence C. Paulson, Cambridge University Computer Laboratory - Author: Claire Quigley, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - -Proof reconstruction for Sledgehammer. -*) - -signature SLEDGEHAMMER_RECONSTRUCT = -sig - type locality = Sledgehammer_Filter.locality - type minimize_command = string list -> string - type metis_params = - string * bool * minimize_command * string * (string * locality) list vector - * thm * int - type isar_params = - string Symtab.table * bool * int * Proof.context * int list list - type text_result = string * (string * locality) list - - val repair_conjecture_shape_and_axiom_names : - string -> int list list -> (string * locality) list vector - -> int list list * (string * locality) list vector - val metis_proof_text : metis_params -> text_result - val isar_proof_text : isar_params -> metis_params -> text_result - val proof_text : bool -> isar_params -> metis_params -> text_result -end; - -structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT = -struct - -open ATP_Problem -open ATP_Proof -open Metis_Translate -open Sledgehammer_Util -open Sledgehammer_Filter -open Sledgehammer_Translate - -type minimize_command = string list -> string -type metis_params = - string * bool * minimize_command * string * (string * locality) list vector - * thm * int -type isar_params = - string Symtab.table * bool * int * Proof.context * int list list -type text_result = string * (string * locality) list - -fun is_head_digit s = Char.isDigit (String.sub (s, 0)) -val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) - -fun find_first_in_list_vector vec key = - Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key - | (_, value) => value) NONE vec - - -(** SPASS's Flotter hack **) - -(* This is a hack required for keeping track of axioms after they have been - clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also - part of this hack. *) - -val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" - -fun extract_clause_sequence output = - let - val tokens_of = String.tokens (not o Char.isAlphaNum) - fun extract_num ("clause" :: (ss as _ :: _)) = - Int.fromString (List.last ss) - | extract_num _ = NONE - in output |> split_lines |> map_filter (extract_num o tokens_of) end - -val parse_clause_formula_pair = - $$ "(" |-- scan_integer --| $$ "," - -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")" - --| Scan.option ($$ ",") -val parse_clause_formula_relation = - Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" - |-- Scan.repeat parse_clause_formula_pair -val extract_clause_formula_relation = - Substring.full #> Substring.position set_ClauseFormulaRelationN - #> snd #> Substring.position "." #> fst #> Substring.string - #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation - #> fst - -fun repair_conjecture_shape_and_axiom_names output conjecture_shape - axiom_names = - if String.isSubstring set_ClauseFormulaRelationN output then - let - val j0 = hd (hd conjecture_shape) - val seq = extract_clause_sequence output - val name_map = extract_clause_formula_relation output - fun renumber_conjecture j = - conjecture_prefix ^ string_of_int (j - j0) - |> AList.find (fn (s, ss) => member (op =) ss s) name_map - |> map (fn s => find_index (curry (op =) s) seq + 1) - fun names_for_number j = - j |> AList.lookup (op =) name_map |> these - |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of - |> map (fn name => - (name, name |> find_first_in_list_vector axiom_names - |> the) - handle Option.Option => - error ("No such fact: " ^ quote name ^ ".")) - in - (conjecture_shape |> map (maps renumber_conjecture), - seq |> map names_for_number |> Vector.fromList) - end - else - (conjecture_shape, axiom_names) - - -(** Soft-core proof reconstruction: Metis one-liner **) - -fun string_for_label (s, num) = s ^ string_of_int num - -fun metis_using [] = "" - | metis_using ls = - "using " ^ space_implode " " (map string_for_label ls) ^ " " -fun metis_apply _ 1 = "by " - | metis_apply 1 _ = "apply " - | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply " -fun metis_name full_types = if full_types then "metisFT" else "metis" -fun metis_call full_types [] = metis_name full_types - | metis_call full_types ss = - "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")" -fun metis_command full_types i n (ls, ss) = - metis_using ls ^ metis_apply i n ^ metis_call full_types ss -fun metis_line banner full_types i n ss = - banner ^ ": " ^ - Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "." -fun minimize_line _ [] = "" - | minimize_line minimize_command ss = - case minimize_command ss of - "" => "" - | command => - "\nTo minimize the number of lemmas, try this: " ^ - Markup.markup Markup.sendback command ^ "." - -fun resolve_axiom axiom_names ((_, SOME s)) = - (case strip_prefix_and_unascii axiom_prefix s of - SOME s' => (case find_first_in_list_vector axiom_names s' of - SOME x => [(s', x)] - | NONE => []) - | NONE => []) - | resolve_axiom axiom_names (num, NONE) = - case Int.fromString num of - SOME j => - if j > 0 andalso j <= Vector.length axiom_names then - Vector.sub (axiom_names, j - 1) - else - [] - | NONE => [] - -fun add_fact axiom_names (Inference (name, _, [])) = - append (resolve_axiom axiom_names name) - | add_fact _ _ = I - -fun used_facts_in_tstplike_proof axiom_names = - atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names) - -fun used_facts axiom_names = - used_facts_in_tstplike_proof axiom_names - #> List.partition (curry (op =) Chained o snd) - #> pairself (sort_distinct (string_ord o pairself fst)) - -fun metis_proof_text (banner, full_types, minimize_command, - tstplike_proof, axiom_names, goal, i) = - let - val (chained_lemmas, other_lemmas) = - used_facts axiom_names tstplike_proof - val n = Logic.count_prems (prop_of goal) - in - (metis_line banner full_types i n (map fst other_lemmas) ^ - minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)), - other_lemmas @ chained_lemmas) - end - - -(** Hard-core proof reconstruction: structured Isar proofs **) - -(* Simple simplifications to ensure that sort annotations don't leave a trail of - spurious "True"s. *) -fun s_not @{const False} = @{const True} - | s_not @{const True} = @{const False} - | s_not (@{const Not} $ t) = t - | s_not t = @{const Not} $ t -fun s_conj (@{const True}, t2) = t2 - | s_conj (t1, @{const True}) = t1 - | s_conj p = HOLogic.mk_conj p -fun s_disj (@{const False}, t2) = t2 - | s_disj (t1, @{const False}) = t1 - | s_disj p = HOLogic.mk_disj p -fun s_imp (@{const True}, t2) = t2 - | s_imp (t1, @{const False}) = s_not t1 - | s_imp p = HOLogic.mk_imp p -fun s_iff (@{const True}, t2) = t2 - | s_iff (t1, @{const True}) = t1 - | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2 - -fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t -fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t - -fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) = - Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t') - | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) = - Const (@{const_name All}, T) $ Abs (s, T', negate_term t') - | negate_term (@{const HOL.implies} $ t1 $ t2) = - @{const HOL.conj} $ t1 $ negate_term t2 - | negate_term (@{const HOL.conj} $ t1 $ t2) = - @{const HOL.disj} $ negate_term t1 $ negate_term t2 - | negate_term (@{const HOL.disj} $ t1 $ t2) = - @{const HOL.conj} $ negate_term t1 $ negate_term t2 - | negate_term (@{const Not} $ t) = t - | negate_term t = @{const Not} $ t - -val indent_size = 2 -val no_label = ("", ~1) - -val raw_prefix = "X" -val assum_prefix = "A" -val fact_prefix = "F" - -fun resolve_conjecture conjecture_shape (num, s_opt) = - let - val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of - SOME s => Int.fromString s |> the_default ~1 - | NONE => case Int.fromString num of - SOME j => find_index (exists (curry (op =) j)) - conjecture_shape - | NONE => ~1 - in if k >= 0 then [k] else [] end - -fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape -fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape - -fun raw_label_for_name conjecture_shape name = - case resolve_conjecture conjecture_shape name of - [j] => (conjecture_prefix, j) - | _ => case Int.fromString (fst name) of - SOME j => (raw_prefix, j) - | NONE => (raw_prefix ^ fst name, 0) - -(**** INTERPRETATION OF TSTP SYNTAX TREES ****) - -exception FO_TERM of string fo_term list -exception FORMULA of (string, string fo_term) formula list -exception SAME of unit - -(* Type variables are given the basic sort "HOL.type". Some will later be - constrained by information from type literals, or by type inference. *) -fun type_from_fo_term tfrees (u as ATerm (a, us)) = - let val Ts = map (type_from_fo_term tfrees) us in - case strip_prefix_and_unascii type_const_prefix a of - SOME b => Type (invert_const b, Ts) - | NONE => - if not (null us) then - raise FO_TERM [u] (* only "tconst"s have type arguments *) - else case strip_prefix_and_unascii tfree_prefix a of - SOME b => - let val s = "'" ^ b in - TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS) - end - | NONE => - case strip_prefix_and_unascii tvar_prefix a of - SOME b => TVar (("'" ^ b, 0), HOLogic.typeS) - | NONE => - (* Variable from the ATP, say "X1" *) - Type_Infer.param 0 (a, HOLogic.typeS) - end - -(* Type class literal applied to a type. Returns triple of polarity, class, - type. *) -fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) = - case (strip_prefix_and_unascii class_prefix a, - map (type_from_fo_term tfrees) us) of - (SOME b, [T]) => (pos, b, T) - | _ => raise FO_TERM [u] - -(** Accumulate type constraints in a formula: negative type literals **) -fun add_var (key, z) = Vartab.map_default (key, []) (cons z) -fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) - | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) - | add_type_constraint _ = I - -fun repair_atp_variable_name f s = - let - fun subscript_name s n = s ^ nat_subscript n - val s = String.map f s - in - case space_explode "_" s of - [_] => (case take_suffix Char.isDigit (String.explode s) of - (cs1 as _ :: _, cs2 as _ :: _) => - subscript_name (String.implode cs1) - (the (Int.fromString (String.implode cs2))) - | (_, _) => s) - | [s1, s2] => (case Int.fromString s2 of - SOME n => subscript_name s1 n - | NONE => s) - | _ => s - end - -(* First-order translation. No types are known for variables. "HOLogic.typeT" - should allow them to be inferred. *) -fun raw_term_from_pred thy full_types tfrees = - let - fun aux opt_T extra_us u = - case u of - ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1 - | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1 - | ATerm (a, us) => - if a = type_wrapper_name then - case us of - [typ_u, term_u] => - aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u - | _ => raise FO_TERM us - else case strip_prefix_and_unascii const_prefix a of - SOME "equal" => - let val ts = map (aux NONE []) us in - if length ts = 2 andalso hd ts aconv List.last ts then - (* Vampire is keen on producing these. *) - @{const True} - else - list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts) - end - | SOME b => - let - val c = invert_const b - val num_type_args = num_type_args thy c - val (type_us, term_us) = - chop (if full_types then 0 else num_type_args) us - (* Extra args from "hAPP" come after any arguments given directly to - the constant. *) - val term_ts = map (aux NONE []) term_us - val extra_ts = map (aux NONE []) extra_us - val t = - Const (c, if full_types then - case opt_T of - SOME T => map fastype_of term_ts ---> T - | NONE => - if num_type_args = 0 then - Sign.const_instance thy (c, []) - else - raise Fail ("no type information for " ^ quote c) - else - Sign.const_instance thy (c, - map (type_from_fo_term tfrees) type_us)) - in list_comb (t, term_ts @ extra_ts) end - | NONE => (* a free or schematic variable *) - let - val ts = map (aux NONE []) (us @ extra_us) - val T = map fastype_of ts ---> HOLogic.typeT - val t = - case strip_prefix_and_unascii fixed_var_prefix a of - SOME b => Free (b, T) - | NONE => - case strip_prefix_and_unascii schematic_var_prefix a of - SOME b => Var ((b, 0), T) - | NONE => - if is_atp_variable a then - Var ((repair_atp_variable_name Char.toLower a, 0), T) - else - (* Skolem constants? *) - Var ((repair_atp_variable_name Char.toUpper a, 0), T) - in list_comb (t, ts) end - in aux (SOME HOLogic.boolT) [] end - -fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) = - if String.isPrefix class_prefix s then - add_type_constraint (type_constraint_from_term pos tfrees u) - #> pair @{const True} - else - pair (raw_term_from_pred thy full_types tfrees u) - -val combinator_table = - [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}), - (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}), - (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}), - (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}), - (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})] - -fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2)) - | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t') - | uncombine_term (t as Const (x as (s, _))) = - (case AList.lookup (op =) combinator_table s of - SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd - | NONE => t) - | uncombine_term t = t - -(* Update schematic type variables with detected sort constraints. It's not - totally clear when this code is necessary. *) -fun repair_tvar_sorts (t, tvar_tab) = - let - fun do_type (Type (a, Ts)) = Type (a, map do_type Ts) - | do_type (TVar (xi, s)) = - TVar (xi, the_default s (Vartab.lookup tvar_tab xi)) - | do_type (TFree z) = TFree z - fun do_term (Const (a, T)) = Const (a, do_type T) - | do_term (Free (a, T)) = Free (a, do_type T) - | do_term (Var (xi, T)) = Var (xi, do_type T) - | do_term (t as Bound _) = t - | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t) - | do_term (t1 $ t2) = do_term t1 $ do_term t2 - in t |> not (Vartab.is_empty tvar_tab) ? do_term end - -fun quantify_over_var quant_of var_s t = - let - val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s) - |> map Var - in fold_rev quant_of vars t end - -(* Interpret an ATP formula as a HOL term, extracting sort constraints as they - appear in the formula. *) -fun prop_from_formula thy full_types tfrees phi = - let - fun do_formula pos phi = - case phi of - AQuant (_, [], phi) => do_formula pos phi - | AQuant (q, x :: xs, phi') => - do_formula pos (AQuant (q, xs, phi')) - #>> quantify_over_var (case q of - AForall => forall_of - | AExists => exists_of) - (repair_atp_variable_name Char.toLower x) - | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not - | AConn (c, [phi1, phi2]) => - do_formula (pos |> c = AImplies ? not) phi1 - ##>> do_formula pos phi2 - #>> (case c of - AAnd => s_conj - | AOr => s_disj - | AImplies => s_imp - | AIf => s_imp o swap - | AIff => s_iff - | ANotIff => s_not o s_iff) - | AAtom tm => term_from_pred thy full_types tfrees pos tm - | _ => raise FORMULA [phi] - in repair_tvar_sorts (do_formula true phi Vartab.empty) end - -fun check_formula ctxt = - Type.constraint HOLogic.boolT - #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) - - -(**** Translation of TSTP files to Isar Proofs ****) - -fun unvarify_term (Var ((s, 0), T)) = Free (s, T) - | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t]) - -fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt = - let - val thy = ProofContext.theory_of ctxt - val t1 = prop_from_formula thy full_types tfrees phi1 - val vars = snd (strip_comb t1) - val frees = map unvarify_term vars - val unvarify_args = subst_atomic (vars ~~ frees) - val t2 = prop_from_formula thy full_types tfrees phi2 - val (t1, t2) = - HOLogic.eq_const HOLogic.typeT $ t1 $ t2 - |> unvarify_args |> uncombine_term |> check_formula ctxt - |> HOLogic.dest_eq - in - (Definition (name, t1, t2), - fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) - end - | decode_line full_types tfrees (Inference (name, u, deps)) ctxt = - let - val thy = ProofContext.theory_of ctxt - val t = u |> prop_from_formula thy full_types tfrees - |> uncombine_term |> check_formula ctxt - in - (Inference (name, t, deps), - fold Variable.declare_term (OldTerm.term_frees t) ctxt) - end -fun decode_lines ctxt full_types tfrees lines = - fst (fold_map (decode_line full_types tfrees) lines ctxt) - -fun is_same_inference _ (Definition _) = false - | is_same_inference t (Inference (_, t', _)) = t aconv t' - -(* No "real" literals means only type information (tfree_tcs, clsrel, or - clsarity). *) -val is_only_type_information = curry (op aconv) HOLogic.true_const - -fun replace_one_dependency (old, new) dep = - if is_same_step (dep, old) then new else [dep] -fun replace_dependencies_in_line _ (line as Definition _) = line - | replace_dependencies_in_line p (Inference (name, t, deps)) = - Inference (name, t, fold (union (op =) o replace_one_dependency p) deps []) - -(* Discard axioms; consolidate adjacent lines that prove the same formula, since - they differ only in type information.*) -fun add_line _ _ (line as Definition _) lines = line :: lines - | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines = - (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or - definitions. *) - if is_axiom axiom_names name then - (* Axioms are not proof lines. *) - if is_only_type_information t then - map (replace_dependencies_in_line (name, [])) lines - (* Is there a repetition? If so, replace later line by earlier one. *) - else case take_prefix (not o is_same_inference t) lines of - (_, []) => lines (* no repetition of proof line *) - | (pre, Inference (name', _, _) :: post) => - pre @ map (replace_dependencies_in_line (name', [name])) post - else if is_conjecture conjecture_shape name then - Inference (name, negate_term t, []) :: lines - else - map (replace_dependencies_in_line (name, [])) lines - | add_line _ _ (Inference (name, t, deps)) lines = - (* Type information will be deleted later; skip repetition test. *) - if is_only_type_information t then - Inference (name, t, deps) :: lines - (* Is there a repetition? If so, replace later line by earlier one. *) - else case take_prefix (not o is_same_inference t) lines of - (* FIXME: Doesn't this code risk conflating proofs involving different - types? *) - (_, []) => Inference (name, t, deps) :: lines - | (pre, Inference (name', t', _) :: post) => - Inference (name, t', deps) :: - pre @ map (replace_dependencies_in_line (name', [name])) post - -(* Recursively delete empty lines (type information) from the proof. *) -fun add_nontrivial_line (Inference (name, t, [])) lines = - if is_only_type_information t then delete_dependency name lines - else Inference (name, t, []) :: lines - | add_nontrivial_line line lines = line :: lines -and delete_dependency name lines = - fold_rev add_nontrivial_line - (map (replace_dependencies_in_line (name, [])) lines) [] - -(* ATPs sometimes reuse free variable names in the strangest ways. Removing - offending lines often does the trick. *) -fun is_bad_free frees (Free x) = not (member (op =) frees x) - | is_bad_free _ _ = false - -fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) = - (j, line :: map (replace_dependencies_in_line (name, [])) lines) - | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees - (Inference (name, t, deps)) (j, lines) = - (j + 1, - if is_axiom axiom_names name orelse - is_conjecture conjecture_shape name orelse - (* the last line must be kept *) - j = 0 orelse - (not (is_only_type_information t) andalso - null (Term.add_tvars t []) andalso - not (exists_subterm (is_bad_free frees) t) andalso - length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso - (* kill next to last line, which usually results in a trivial step *) - j <> 1) then - Inference (name, t, deps) :: lines (* keep line *) - else - map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) - -(** Isar proof construction and manipulation **) - -fun merge_fact_sets (ls1, ss1) (ls2, ss2) = - (union (op =) ls1 ls2, union (op =) ss1 ss2) - -type label = string * int -type facts = label list * string list - -datatype isar_qualifier = Show | Then | Moreover | Ultimately - -datatype isar_step = - Fix of (string * typ) list | - Let of term * term | - Assume of label * term | - Have of isar_qualifier list * label * term * byline -and byline = - ByMetis of facts | - CaseSplit of isar_step list list * facts - -fun smart_case_split [] facts = ByMetis facts - | smart_case_split proofs facts = CaseSplit (proofs, facts) - -fun add_fact_from_dependency conjecture_shape axiom_names name = - if is_axiom axiom_names name then - apsnd (union (op =) (map fst (resolve_axiom axiom_names name))) - else - apfst (insert (op =) (raw_label_for_name conjecture_shape name)) - -fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2) - | step_for_line conjecture_shape _ _ (Inference (name, t, [])) = - Assume (raw_label_for_name conjecture_shape name, t) - | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) = - Have (if j = 1 then [Show] else [], - raw_label_for_name conjecture_shape name, - fold_rev forall_of (map Var (Term.add_vars t [])) t, - ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names) - deps ([], []))) - -fun repair_name "$true" = "c_True" - | repair_name "$false" = "c_False" - | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *) - | repair_name "equal" = "c_equal" (* needed by SPASS? *) - | repair_name s = - if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then - "c_equal" (* seen in Vampire proofs *) - else - s - -fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor - tstplike_proof conjecture_shape axiom_names params frees = - let - val lines = - tstplike_proof - |> atp_proof_from_tstplike_string - |> nasty_atp_proof pool - |> map_term_names_in_atp_proof repair_name - |> decode_lines ctxt full_types tfrees - |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names) - |> rpair [] |-> fold_rev add_nontrivial_line - |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor - conjecture_shape axiom_names frees) - |> snd - in - (if null params then [] else [Fix params]) @ - map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1) - lines - end - -(* When redirecting proofs, we keep information about the labels seen so far in - the "backpatches" data structure. The first component indicates which facts - should be associated with forthcoming proof steps. The second component is a - pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should - become assumptions and "drop_ls" are the labels that should be dropped in a - case split. *) -type backpatches = (label * facts) list * (label list * label list) - -fun used_labels_of_step (Have (_, _, _, by)) = - (case by of - ByMetis (ls, _) => ls - | CaseSplit (proofs, (ls, _)) => - fold (union (op =) o used_labels_of) proofs ls) - | used_labels_of_step _ = [] -and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] - -fun new_labels_of_step (Fix _) = [] - | new_labels_of_step (Let _) = [] - | new_labels_of_step (Assume (l, _)) = [l] - | new_labels_of_step (Have (_, l, _, _)) = [l] -val new_labels_of = maps new_labels_of_step - -val join_proofs = - let - fun aux _ [] = NONE - | aux proof_tail (proofs as (proof1 :: _)) = - if exists null proofs then - NONE - 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, _) => (* 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)) - (used_labels_of proof_tail)) then - SOME (l, t, map rev proofs, proof_tail) - else - NONE - | _ => NONE - in aux [] o map rev end - -fun case_split_qualifiers proofs = - case length proofs of - 0 => [] - | 1 => [Then] - | _ => [Ultimately] - -fun redirect_proof hyp_ts concl_t proof = - let - (* The first pass outputs those steps that are independent of the negated - conjecture. The second pass flips the proof by contradiction to obtain a - direct proof, introducing case splits when an inference depends on - several facts that depend on the negated conjecture. *) - val concl_l = (conjecture_prefix, length hyp_ts) - fun first_pass ([], contra) = ([], contra) - | first_pass ((step as Fix _) :: proof, contra) = - 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 (_, j), _)) :: proof, contra) = - if l = concl_l then first_pass (proof, contra ||> cons step) - else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j)) - | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = - let val step = Have (qs, l, t, ByMetis (ls, ss)) in - if exists (member (op =) (fst contra)) ls then - first_pass (proof, contra |>> cons l ||> cons step) - else - first_pass (proof, contra) |>> cons step - end - | first_pass _ = raise Fail "malformed proof" - val (proof_top, (contra_ls, contra_proof)) = - first_pass (proof, ([concl_l], [])) - val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst - fun backpatch_labels patches ls = - fold merge_fact_sets (map (backpatch_label patches) ls) ([], []) - fun second_pass end_qs ([], assums, patches) = - ([Have (end_qs, no_label, concl_t, - ByMetis (backpatch_labels patches (map snd assums)))], patches) - | second_pass end_qs (Assume (l, t) :: proof, assums, patches) = - second_pass end_qs (proof, (t, l) :: assums, patches) - | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums, - patches) = - (if member (op =) (snd (snd patches)) l andalso - not (member (op =) (fst (snd patches)) l) andalso - not (AList.defined (op =) (fst patches) l) then - second_pass end_qs (proof, assums, patches ||> apsnd (append ls)) - else case List.partition (member (op =) contra_ls) ls of - ([contra_l], co_ls) => - if member (op =) qs Show then - second_pass end_qs (proof, assums, - patches |>> cons (contra_l, (co_ls, ss))) - else - second_pass end_qs - (proof, assums, - patches |>> cons (contra_l, (l :: co_ls, ss))) - |>> cons (if member (op =) (fst (snd patches)) l then - Assume (l, negate_term t) - else - Have (qs, l, negate_term t, - ByMetis (backpatch_label patches l))) - | (contra_ls as _ :: _, co_ls) => - let - val proofs = - map_filter - (fn l => - if l = concl_l then - NONE - else - let - val drop_ls = filter (curry (op <>) l) contra_ls - in - second_pass [] - (proof, assums, - patches ||> apfst (insert (op =) l) - ||> apsnd (union (op =) drop_ls)) - |> fst |> SOME - end) contra_ls - val (assumes, facts) = - if member (op =) (fst (snd patches)) l then - ([Assume (l, negate_term t)], (l :: co_ls, ss)) - else - ([], (co_ls, ss)) - in - (case join_proofs proofs of - SOME (l, t, proofs, proof_tail) => - Have (case_split_qualifiers proofs @ - (if null proof_tail then end_qs else []), l, t, - smart_case_split proofs facts) :: proof_tail - | NONE => - [Have (case_split_qualifiers proofs @ end_qs, no_label, - concl_t, smart_case_split proofs facts)], - patches) - |>> append assumes - end - | _ => raise Fail "malformed proof") - | second_pass _ _ = raise Fail "malformed proof" - val proof_bottom = - second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst - in proof_top @ proof_bottom end - -(* FIXME: Still needed? Probably not. *) -val kill_duplicate_assumptions_in_proof = - let - fun relabel_facts subst = - apfst (map (fn l => AList.lookup (op =) subst l |> the_default l)) - fun do_step (step as Assume (l, t)) (proof, subst, assums) = - (case AList.lookup (op aconv) assums t of - SOME l' => (proof, (l, l') :: subst, assums) - | NONE => (step :: proof, subst, (t, l) :: assums)) - | do_step (Have (qs, l, t, by)) (proof, subst, assums) = - (Have (qs, l, t, - case by of - ByMetis facts => ByMetis (relabel_facts subst facts) - | CaseSplit (proofs, facts) => - CaseSplit (map do_proof proofs, relabel_facts subst facts)) :: - proof, subst, assums) - | do_step step (proof, subst, assums) = (step :: proof, subst, assums) - and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev - in do_proof end - -val then_chain_proof = - let - fun aux _ [] = [] - | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof - | aux l' (Have (qs, l, t, by) :: proof) = - (case by of - ByMetis (ls, ss) => - Have (if member (op =) ls l' then - (Then :: qs, l, t, - ByMetis (filter_out (curry (op =) l') ls, ss)) - else - (qs, l, t, ByMetis (ls, ss))) - | CaseSplit (proofs, facts) => - Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) :: - aux l proof - | aux _ (step :: proof) = step :: aux no_label proof - in aux no_label end - -fun kill_useless_labels_in_proof proof = - let - val used_ls = used_labels_of proof - fun do_label l = if member (op =) used_ls l then l else no_label - fun do_step (Assume (l, t)) = Assume (do_label l, t) - | do_step (Have (qs, l, t, by)) = - Have (qs, do_label l, t, - case by of - CaseSplit (proofs, facts) => - CaseSplit (map (map do_step) proofs, facts) - | _ => by) - | do_step step = step - in map do_step proof end - -fun prefix_for_depth n = replicate_string (n + 1) - -val relabel_proof = - let - fun aux _ _ _ [] = [] - | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) = - if l = no_label then - Assume (l, t) :: aux subst depth (next_assum, next_fact) proof - else - let val l' = (prefix_for_depth depth assum_prefix, next_assum) in - Assume (l', t) :: - aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof - end - | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) = - let - val (l', subst, next_fact) = - if l = no_label then - (l, subst, next_fact) - else - let - val l' = (prefix_for_depth depth fact_prefix, next_fact) - in (l', (l, l') :: subst, next_fact + 1) end - val relabel_facts = - apfst (maps (the_list o AList.lookup (op =) subst)) - val by = - case by of - ByMetis facts => ByMetis (relabel_facts facts) - | CaseSplit (proofs, facts) => - CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs, - relabel_facts facts) - in - Have (qs, l', t, by) :: - aux subst depth (next_assum, next_fact) proof - end - | aux subst depth nextp (step :: proof) = - step :: aux subst depth nextp proof - in aux [] 0 (1, 1) end - -fun string_for_proof ctxt0 full_types i n = - let - val ctxt = ctxt0 - |> Config.put show_free_types false - |> Config.put show_types true - fun fix_print_mode f x = - Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) - (print_mode_value ())) f x - fun do_indent ind = replicate_string (ind * indent_size) " " - fun do_free (s, T) = - maybe_quote s ^ " :: " ^ - maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T) - fun do_label l = if l = no_label then "" else string_for_label l ^ ": " - fun do_have qs = - (if member (op =) qs Moreover then "moreover " else "") ^ - (if member (op =) qs Ultimately then "ultimately " else "") ^ - (if member (op =) qs Then then - if member (op =) qs Show then "thus" else "hence" - else - if member (op =) qs Show then "show" else "have") - val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) - fun do_facts (ls, ss) = - metis_command full_types 1 1 - (ls |> sort_distinct (prod_ord string_ord int_ord), - ss |> sort_distinct string_ord) - and do_step ind (Fix xs) = - do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" - | do_step ind (Let (t1, t2)) = - do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" - | do_step ind (Assume (l, t)) = - do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" - | do_step ind (Have (qs, l, t, ByMetis facts)) = - do_indent ind ^ do_have qs ^ " " ^ - do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n" - | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) = - space_implode (do_indent ind ^ "moreover\n") - (map (do_block ind) proofs) ^ - do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^ - do_facts facts ^ "\n" - and do_steps prefix suffix ind steps = - let val s = implode (map (do_step ind) steps) in - replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ - String.extract (s, ind * indent_size, - SOME (size s - ind * indent_size - 1)) ^ - suffix ^ "\n" - end - and do_block ind proof = do_steps "{ " " }" (ind + 1) proof - (* One-step proofs are pointless; better use the Metis one-liner - directly. *) - and do_proof [Have (_, _, _, ByMetis _)] = "" - | do_proof proof = - (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ - do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ - (if n <> 1 then "next" else "qed") - in do_proof end - -fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (other_params as (_, full_types, _, tstplike_proof, - axiom_names, goal, i)) = - let - val (params, hyp_ts, concl_t) = strip_subgoal goal i - val frees = fold Term.add_frees (concl_t :: hyp_ts) [] - val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] - val n = Logic.count_prems (prop_of goal) - val (one_line_proof, lemma_names) = metis_proof_text other_params - fun isar_proof_for () = - case isar_proof_from_tstplike_proof pool ctxt full_types tfrees - isar_shrink_factor tstplike_proof conjecture_shape axiom_names - params frees - |> redirect_proof hyp_ts concl_t - |> kill_duplicate_assumptions_in_proof - |> then_chain_proof - |> kill_useless_labels_in_proof - |> relabel_proof - |> string_for_proof ctxt full_types i n of - "" => "\nNo structured proof available." - | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof - val isar_proof = - if debug then - isar_proof_for () - else - try isar_proof_for () - |> the_default "\nWarning: The Isar proof construction failed." - in (one_line_proof ^ isar_proof, lemma_names) end - -fun proof_text isar_proof isar_params other_params = - (if isar_proof then isar_proof_text isar_params else metis_proof_text) - other_params - -end; diff -r b237f757b215 -r 1c75f3f192ae src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Oct 22 13:59:34 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,533 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_translate.ML - Author: Fabian Immler, TU Muenchen - Author: Makarius - Author: Jasmin Blanchette, TU Muenchen - -Translation of HOL to FOL for Sledgehammer. -*) - -signature SLEDGEHAMMER_TRANSLATE = -sig - type 'a problem = 'a ATP_Problem.problem - type fol_formula - - val axiom_prefix : string - val conjecture_prefix : string - val prepare_axiom : - Proof.context -> (string * 'a) * thm - -> term * ((string * 'a) * fol_formula) option - val prepare_problem : - Proof.context -> bool -> bool -> bool -> bool -> term list -> term - -> (term * ((string * 'a) * fol_formula) option) list - -> string problem * string Symtab.table * int * (string * 'a) list vector -end; - -structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE = -struct - -open ATP_Problem -open Metis_Translate -open Sledgehammer_Util - -val axiom_prefix = "ax_" -val conjecture_prefix = "conj_" -val helper_prefix = "help_" -val class_rel_clause_prefix = "clrel_"; -val arity_clause_prefix = "arity_" -val tfree_prefix = "tfree_" - -(* Freshness almost guaranteed! *) -val sledgehammer_weak_prefix = "Sledgehammer:" - -type fol_formula = - {name: string, - kind: kind, - combformula: (name, combterm) formula, - ctypes_sorts: typ list} - -fun mk_anot phi = AConn (ANot, [phi]) -fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) -fun mk_ahorn [] phi = phi - | mk_ahorn (phi :: phis) psi = - AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) - -fun combformula_for_prop thy = - let - val do_term = combterm_from_term thy ~1 - fun do_quant bs q s T t' = - let val s = Name.variant (map fst bs) s in - do_formula ((s, T) :: bs) t' - #>> (fn phi => AQuant (q, [`make_bound_var s], phi)) - end - and do_conn bs c t1 t2 = - do_formula bs t1 ##>> do_formula bs t2 - #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) - and do_formula bs t = - case t of - @{const Not} $ t1 => - do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) - | Const (@{const_name All}, _) $ Abs (s, T, t') => - do_quant bs AForall s T t' - | Const (@{const_name Ex}, _) $ Abs (s, T, t') => - do_quant bs AExists s T t' - | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2 - | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2 - | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2 - | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => - do_conn bs AIff t1 t2 - | _ => (fn ts => do_term bs (Envir.eta_contract t) - |>> AAtom ||> union (op =) ts) - in do_formula [] end - -val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm - -fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j -fun conceal_bounds Ts t = - subst_bounds (map (Free o apfst concealed_bound_name) - (0 upto length Ts - 1 ~~ Ts), t) -fun reveal_bounds Ts = - subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) - (0 upto length Ts - 1 ~~ Ts)) - -(* Removes the lambdas from an equation of the form "t = (%x. u)". - (Cf. "extensionalize_theorem" in "Meson_Clausify".) *) -fun extensionalize_term t = - let - fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t' - | aux j (t as Const (s, Type (_, [Type (_, [_, T']), - Type (_, [_, res_T])])) - $ t2 $ Abs (var_s, var_T, t')) = - if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then - let val var_t = Var ((var_s, j), var_T) in - Const (s, T' --> T' --> res_T) - $ betapply (t2, var_t) $ subst_bound (var_t, t') - |> aux (j + 1) - end - else - t - | aux _ t = t - in aux (maxidx_of_term t + 1) t end - -fun introduce_combinators_in_term ctxt kind t = - let val thy = ProofContext.theory_of ctxt in - if Meson.is_fol_term thy t then - t - else - let - fun aux Ts t = - case t of - @{const Not} $ t1 => @{const Not} $ aux Ts t1 - | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, aux (T :: Ts) t') - | (t0 as Const (@{const_name All}, _)) $ t1 => - aux Ts (t0 $ eta_expand Ts t1 1) - | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, aux (T :: Ts) t') - | (t0 as Const (@{const_name Ex}, _)) $ t1 => - aux Ts (t0 $ eta_expand Ts t1 1) - | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _]))) - $ t1 $ t2 => - t0 $ aux Ts t1 $ aux Ts t2 - | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then - t - else - t |> conceal_bounds Ts - |> Envir.eta_contract - |> cterm_of thy - |> Meson_Clausify.introduce_combinators_in_cterm - |> prop_of |> Logic.dest_equals |> snd - |> reveal_bounds Ts - val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single - in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end - handle THM _ => - (* A type variable of sort "{}" will make abstraction fail. *) - if kind = Conjecture then HOLogic.false_const - else HOLogic.true_const - end - -(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the - same in Sledgehammer to prevent the discovery of unreplable proofs. *) -fun freeze_term t = - let - fun aux (t $ u) = aux t $ aux u - | aux (Abs (s, T, t)) = Abs (s, T, aux t) - | aux (Var ((s, i), T)) = - Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) - | aux t = t - in t |> exists_subterm is_Var t ? aux end - -(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example, - it leaves metaequalities over "prop"s alone. *) -val atomize_term = - let - fun aux (@{const Trueprop} $ t1) = t1 - | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) = - HOLogic.all_const T $ Abs (s, T, aux t') - | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2)) - | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) = - HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2 - | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) = - HOLogic.eq_const T $ t1 $ t2 - | aux _ = raise Fail "aux" - in perhaps (try aux) end - -(* making axiom and conjecture formulas *) -fun make_formula ctxt presimp name kind t = - let - val thy = ProofContext.theory_of ctxt - val t = t |> Envir.beta_eta_contract - |> transform_elim_term - |> atomize_term - val need_trueprop = (fastype_of t = HOLogic.boolT) - val t = t |> need_trueprop ? HOLogic.mk_Trueprop - |> extensionalize_term - |> presimp ? presimplify_term thy - |> perhaps (try (HOLogic.dest_Trueprop)) - |> introduce_combinators_in_term ctxt kind - |> kind <> Axiom ? freeze_term - val (combformula, ctypes_sorts) = combformula_for_prop thy t [] - in - {name = name, combformula = combformula, kind = kind, - ctypes_sorts = ctypes_sorts} - end - -fun make_axiom ctxt presimp ((name, loc), th) = - case make_formula ctxt presimp name Axiom (prop_of th) of - {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE - | formula => SOME ((name, loc), formula) -fun make_conjecture ctxt ts = - let val last = length ts - 1 in - map2 (fn j => make_formula ctxt true (Int.toString j) - (if j = last then Conjecture else Hypothesis)) - (0 upto last) ts - end - -(** Helper facts **) - -fun count_combterm (CombConst ((s, _), _, _)) = - Symtab.map_entry s (Integer.add 1) - | count_combterm (CombVar _) = I - | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] -fun count_combformula (AQuant (_, _, phi)) = count_combformula phi - | count_combformula (AConn (_, phis)) = fold count_combformula phis - | count_combformula (AAtom tm) = count_combterm tm -fun count_fol_formula ({combformula, ...} : fol_formula) = - count_combformula combformula - -val optional_helpers = - [(["c_COMBI"], @{thms Meson.COMBI_def}), - (["c_COMBK"], @{thms Meson.COMBK_def}), - (["c_COMBB"], @{thms Meson.COMBB_def}), - (["c_COMBC"], @{thms Meson.COMBC_def}), - (["c_COMBS"], @{thms Meson.COMBS_def})] -val optional_typed_helpers = - [(["c_True", "c_False", "c_If"], @{thms True_or_False}), - (["c_If"], @{thms if_True if_False})] -val mandatory_helpers = @{thms Metis.fequal_def} - -val init_counters = - [optional_helpers, optional_typed_helpers] |> maps (maps fst) - |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make - -fun get_helper_facts ctxt is_FO full_types conjectures axioms = - let - val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters - fun is_needed c = the (Symtab.lookup ct c) > 0 - fun baptize th = ((Thm.get_name_hint th, false), th) - in - (optional_helpers - |> full_types ? append optional_typed_helpers - |> maps (fn (ss, ths) => - if exists is_needed ss then map baptize ths else [])) @ - (if is_FO then [] else map baptize mandatory_helpers) - |> map_filter (Option.map snd o make_axiom ctxt false) - end - -fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax) - -fun prepare_formulas ctxt full_types hyp_ts concl_t axioms = - let - val thy = ProofContext.theory_of ctxt - val (axiom_ts, prepared_axioms) = ListPair.unzip axioms - (* Remove existing axioms from the conjecture, as this can dramatically - boost an ATP's performance (for some reason). *) - val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts) - val goal_t = Logic.list_implies (hyp_ts, concl_t) - val is_FO = Meson.is_fol_term thy goal_t - val subs = tfree_classes_of_terms [goal_t] - val supers = tvar_classes_of_terms axiom_ts - val tycons = type_consts_of_terms thy (goal_t :: axiom_ts) - (* TFrees in the conjecture; TVars in the axioms *) - val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t]) - val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms) - val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms - val (supers', arity_clauses) = make_arity_clauses thy tycons supers - val class_rel_clauses = make_class_rel_clauses thy subs supers' - in - (axiom_names |> map single |> Vector.fromList, - (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) - end - -fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) - -fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) - | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) - | fo_term_for_combtyp (CombType (name, tys)) = - ATerm (name, map fo_term_for_combtyp tys) - -fun fo_literal_for_type_literal (TyLitVar (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - | fo_literal_for_type_literal (TyLitFree (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - -fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot - -fun fo_term_for_combterm full_types = - let - fun aux top_level u = - let - val (head, args) = strip_combterm_comb u - val (x, ty_args) = - case head of - CombConst (name as (s, s'), _, ty_args) => - let val ty_args = if full_types then [] else ty_args in - if s = "equal" then - if top_level andalso length args = 2 then (name, []) - else (("c_fequal", @{const_name Metis.fequal}), ty_args) - else if top_level then - case s of - "c_False" => (("$false", s'), []) - | "c_True" => (("$true", s'), []) - | _ => (name, ty_args) - else - (name, ty_args) - end - | CombVar (name, _) => (name, []) - | CombApp _ => raise Fail "impossible \"CombApp\"" - val t = ATerm (x, map fo_term_for_combtyp ty_args @ - map (aux false) args) - in - if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t - end - in aux true end - -fun formula_for_combformula full_types = - let - fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) - | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm) - in aux end - -fun formula_for_axiom full_types - ({combformula, ctypes_sorts, ...} : fol_formula) = - mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) - (type_literals_for_types ctypes_sorts)) - (formula_for_combformula full_types combformula) - -fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) = - Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula) - -fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, - superclass, ...}) = - let val ty_arg = ATerm (("T", "T"), []) in - Fof (class_rel_clause_prefix ^ ascii_of name, Axiom, - AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), - AAtom (ATerm (superclass, [ty_arg]))])) - end - -fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = - (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) - | fo_literal_for_arity_literal (TVarLit (c, sort)) = - (false, ATerm (c, [ATerm (sort, [])])) - -fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits, - ...}) = - Fof (arity_clause_prefix ^ ascii_of name, Axiom, - mk_ahorn (map (formula_for_fo_literal o apfst not - o fo_literal_for_arity_literal) premLits) - (formula_for_fo_literal - (fo_literal_for_arity_literal conclLit))) - -fun problem_line_for_conjecture full_types - ({name, kind, combformula, ...} : fol_formula) = - Fof (conjecture_prefix ^ name, kind, - formula_for_combformula full_types combformula) - -fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) = - map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) - -fun problem_line_for_free_type j lit = - Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit) -fun problem_lines_for_free_types conjectures = - let - val litss = map free_type_literals_for_conjecture conjectures - val lits = fold (union (op =)) litss [] - in map2 problem_line_for_free_type (0 upto length lits - 1) lits end - -(** "hBOOL" and "hAPP" **) - -type const_info = {min_arity: int, max_arity: int, sub_level: bool} - -fun consider_term top_level (ATerm ((s, _), ts)) = - (if is_atp_variable s then - I - else - let val n = length ts in - Symtab.map_default - (s, {min_arity = n, max_arity = 0, sub_level = false}) - (fn {min_arity, max_arity, sub_level} => - {min_arity = Int.min (n, min_arity), - max_arity = Int.max (n, max_arity), - sub_level = sub_level orelse not top_level}) - end) - #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts -fun consider_formula (AQuant (_, _, phi)) = consider_formula phi - | consider_formula (AConn (_, phis)) = fold consider_formula phis - | consider_formula (AAtom tm) = consider_term true tm - -fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi -fun consider_problem problem = fold (fold consider_problem_line o snd) problem - -fun const_table_for_problem explicit_apply problem = - if explicit_apply then NONE - else SOME (Symtab.empty |> consider_problem problem) - -fun min_arity_of thy full_types NONE s = - (if s = "equal" orelse s = type_wrapper_name orelse - String.isPrefix type_const_prefix s orelse - String.isPrefix class_prefix s then - 16383 (* large number *) - else if full_types then - 0 - else case strip_prefix_and_unascii const_prefix s of - SOME s' => num_type_args thy (invert_const s') - | NONE => 0) - | min_arity_of _ _ (SOME the_const_tab) s = - case Symtab.lookup the_const_tab s of - SOME ({min_arity, ...} : const_info) => min_arity - | NONE => 0 - -fun full_type_of (ATerm ((s, _), [ty, _])) = - if s = type_wrapper_name then ty else raise Fail "expected type wrapper" - | full_type_of _ = raise Fail "expected type wrapper" - -fun list_hAPP_rev _ t1 [] = t1 - | list_hAPP_rev NONE t1 (t2 :: ts2) = - ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) - | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = - let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, - [full_type_of t2, ty]) in - ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) - end - -fun repair_applications_in_term thy full_types const_tab = - let - fun aux opt_ty (ATerm (name as (s, _), ts)) = - if s = type_wrapper_name then - case ts of - [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) - | _ => raise Fail "malformed type wrapper" - else - let - val ts = map (aux NONE) ts - val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts - in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end - in aux NONE end - -fun boolify t = ATerm (`I "hBOOL", [t]) - -(* True if the constant ever appears outside of the top-level position in - literals, or if it appears with different arities (e.g., because of different - type instantiations). If false, the constant always receives all of its - arguments and is used as a predicate. *) -fun is_predicate NONE s = - s = "equal" orelse s = "$false" orelse s = "$true" orelse - String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s - | is_predicate (SOME the_const_tab) s = - case Symtab.lookup the_const_tab s of - SOME {min_arity, max_arity, sub_level} => - not sub_level andalso min_arity = max_arity - | NONE => false - -fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = - if s = type_wrapper_name then - case ts of - [_, t' as ATerm ((s', _), _)] => - if is_predicate const_tab s' then t' else boolify t - | _ => raise Fail "malformed type wrapper" - else - t |> not (is_predicate const_tab s) ? boolify - -fun close_universally phi = - let - fun term_vars bounds (ATerm (name as (s, _), tms)) = - (is_atp_variable s andalso not (member (op =) bounds name)) - ? insert (op =) name - #> fold (term_vars bounds) tms - fun formula_vars bounds (AQuant (_, xs, phi)) = - formula_vars (xs @ bounds) phi - | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis - | formula_vars bounds (AAtom tm) = term_vars bounds tm - in - case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) - end - -fun repair_formula thy explicit_forall full_types const_tab = - let - fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) - | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (AAtom tm) = - AAtom (tm |> repair_applications_in_term thy full_types const_tab - |> repair_predicates_in_term const_tab) - in aux #> explicit_forall ? close_universally end - -fun repair_problem_line thy explicit_forall full_types const_tab - (Fof (ident, kind, phi)) = - Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) -fun repair_problem_with_const_table thy = - map o apsnd o map ooo repair_problem_line thy - -fun repair_problem thy explicit_forall full_types explicit_apply problem = - repair_problem_with_const_table thy explicit_forall full_types - (const_table_for_problem explicit_apply problem) problem - -fun prepare_problem ctxt readable_names explicit_forall full_types - explicit_apply hyp_ts concl_t axioms = - let - val thy = ProofContext.theory_of ctxt - val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses, - arity_clauses)) = - prepare_formulas ctxt full_types hyp_ts concl_t axioms - val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms - val helper_lines = - map (problem_line_for_fact helper_prefix full_types) helper_facts - val conjecture_lines = - map (problem_line_for_conjecture full_types) conjectures - val tfree_lines = problem_lines_for_free_types conjectures - val class_rel_lines = - map problem_line_for_class_rel_clause class_rel_clauses - val arity_lines = map problem_line_for_arity_clause arity_clauses - (* Reordering these might or might not confuse the proof reconstruction - code or the SPASS Flotter hack. *) - val problem = - [("Relevant facts", axiom_lines), - ("Class relationships", class_rel_lines), - ("Arity declarations", arity_lines), - ("Helper facts", helper_lines), - ("Conjectures", conjecture_lines), - ("Type variables", tfree_lines)] - |> repair_problem thy explicit_forall full_types explicit_apply - val (problem, pool) = nice_atp_problem readable_names problem - val conjecture_offset = - length axiom_lines + length class_rel_lines + length arity_lines - + length helper_lines - in - (problem, - case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, - conjecture_offset, axiom_names) - end - -end;