--- a/NEWS Fri Jul 01 17:36:25 2011 +0200
+++ b/NEWS Fri Jul 01 18:11:17 2011 +0200
@@ -81,14 +81,14 @@
INCOMPATIBILITY.
* Sledgehammer:
- - sledgehammer available_provers ~> sledgehammer supported_provers
+ - sledgehammer available_provers ~> sledgehammer supported_provers.
INCOMPATIBILITY.
- Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed
TPTP problems (TFF).
- - Added "type_sys", "sound", "max_mono_iters", and "max_new_mono_instances"
- options.
- - Removed "full_types" option and corresponding Proof General menu item.
- INCOMPATIBILITY.
+ - Added "preplay_timeout", "slicing", "type_enc", "sound", "max_mono_iters",
+ and "max_new_mono_instances" options.
+ - Removed "explicit_apply" and "full_types" options as well as "Full Types"
+ Proof General menu item. INCOMPATIBILITY.
* Metis:
- Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.
--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Jul 01 17:36:25 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Jul 01 18:11:17 2011 +0200
@@ -177,14 +177,14 @@
set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
-with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 0.6 and 1.0%
+with E 1.0 to 1.3, SPASS 3.5 and 3.7, and Vampire 0.6 and 1.0%
\footnote{Following the rewrite of Vampire, the counter for version numbers was
reset to 0; hence the (new) Vampire versions 0.6 and 1.0 are more recent than,
say, Vampire 11.5.}%
. Since the ATPs' output formats are neither documented nor stable, other
versions of the ATPs might or might not work well with Sledgehammer. Ideally,
also set \texttt{E\_VERSION}, \texttt{SPASS\_VERSION}, or
-\texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.2'').
+\texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.3'').
\end{enum}
To check whether E and SPASS are successfully installed, follow the example in
@@ -401,7 +401,7 @@
This message usually indicates that Sledgehammer found a type-incorrect proof.
This was a frequent issue with older versions of Sledgehammer, which did not
supply enough typing information to the ATPs by default. If you notice many
-unsound proofs and are not using \textit{type\_sys} (\S\ref{problem-encoding}),
+unsound proofs and are not using \textit{type\_enc} (\S\ref{problem-encoding}),
contact the author at \authoremail.
\point{How can I tell whether a generated proof is sound?}
@@ -646,13 +646,13 @@
The \textit{metis} proof method has the syntax
\prew
-\textbf{\textit{metis}}~(\qty{type\_sys})${}^?$~\qty{facts}${}^?$
+\textbf{\textit{metis}}~(\qty{type\_enc})${}^?$~\qty{facts}${}^?$
\postw
-where \qty{type\_sys} is a type system specification with the same semantics as
-Sledgehammer's \textit{type\_sys} option (\S\ref{problem-encoding}) and
+where \qty{type\_enc} is a type encoding specification with the same semantics
+as Sledgehammer's \textit{type\_enc} option (\S\ref{problem-encoding}) and
\qty{facts} is a list of arbitrary facts. In addition to the values listed in
-\S\ref{problem-encoding}, \qty{type\_sys} may also be \textit{full\_types}, in
+\S\ref{problem-encoding}, \qty{type\_enc} may also be \textit{full\_types}, in
which case an appropriate type-sound encoding is chosen, \textit{partial\_types}
(the default type-unsound encoding), or \textit{no\_types}, a synonym for
\textit{erased}.
@@ -772,36 +772,39 @@
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
\item[$\bullet$] \textbf{\textit{remote\_leo2}:} LEO-II is an automatic
-higher-order prover developed by Christoph Benzm\"uller et al. \cite{leo2}. The
-remote version of LEO-II runs on Geoff Sutcliffe's Miami servers. In the current
-setup, the problems given to LEO-II are only mildly higher-order.
+higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
+with support for the TPTP higher-order syntax (THF). The remote version of
+LEO-II runs on Geoff Sutcliffe's Miami servers. In the current setup, the
+problems given to LEO-II are only mildly higher-order.
\item[$\bullet$] \textbf{\textit{remote\_satallax}:} Satallax is an automatic
-higher-order prover developed by Chad Brown et al. \cite{satallax}. The remote
-version of Satallax runs on Geoff Sutcliffe's Miami servers. In the current
-setup, the problems given to Satallax are only mildly higher-order.
+higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
+support for the TPTP higher-order syntax (THF). The remote version of Satallax
+runs on Geoff Sutcliffe's Miami servers. In the current setup, the problems
+given to Satallax are only mildly higher-order.
\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
SInE runs on Geoff Sutcliffe's Miami servers.
\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order
-resolution prover developed by Stickel et al.\ \cite{snark}. The remote version
-of SNARK runs on Geoff Sutcliffe's Miami servers.
+resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
+TPTP many-typed first-order format (TFF). The remote version of SNARK runs on
+Geoff Sutcliffe's Miami servers.
\item[$\bullet$] \textbf{\textit{remote\_tofof\_e}:} ToFoF-E is a metaprover
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
-servers. This ATP supports a fragment of the TPTP many-typed first-order format
-(TFF). It is supported primarily for experimenting with the
-\textit{type\_sys} $=$ \textit{simple} option (\S\ref{problem-encoding}).
+servers. This ATP supports the TPTP many-typed first-order format (TFF). The
+remote version of ToFoF-E runs on Geoff Sutcliffe's Miami servers.
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
\item[$\bullet$] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
-used to prove universally quantified equations using unconditional equations.
-The remote version of Waldmeister runs on Geoff Sutcliffe's Miami servers.
+used to prove universally quantified equations using unconditional equations,
+corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister
+runs on Geoff Sutcliffe's Miami servers.
\item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
@@ -873,11 +876,11 @@
\label{problem-encoding}
\begin{enum}
-\opdefault{type\_sys}{string}{smart}
-Specifies the type system to use in ATP problems. Some of the type systems are
-unsound, meaning that they can give rise to spurious proofs (unreconstructible
-using Metis). The supported type systems are listed below, with an indication of
-their soundness in parentheses:
+\opdefault{type\_enc}{string}{smart}
+Specifies the type encoding to use in ATP problems. Some of the type encodings
+are unsound, meaning that they can give rise to spurious proofs
+(unreconstructible using Metis). The supported type encodings are listed below,
+with an indication of their soundness in parentheses:
\begin{enum}
\item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is
@@ -919,52 +922,57 @@
$\mathit{type\_info\/}(\tau, t)$ becomes a unary function
$\mathit{type\_info\_}\tau(t)$.
-\item[$\bullet$] \textbf{\textit{simple} (sound):} Use the prover's support for
-simple types if available; otherwise, fall back on \textit{mangled\_preds}. The
-problem is monomorphized.
+\item[$\bullet$] \textbf{\textit{simple} (sound):} Exploit simple first-order
+types if the prover supports the TFF or THF syntax; otherwise, fall back on
+\textit{mangled\_preds}. The problem is monomorphized.
+
+\item[$\bullet$] \textbf{\textit{simple\_higher} (sound):} Exploit simple
+higher-order types if the prover supports the THF syntax; otherwise, fall back
+on \textit{simple} or \textit{mangled\_preds\_heavy}. The problem is
+monomorphized.
\item[$\bullet$]
\textbf{%
\textit{poly\_preds}?, \textit{poly\_tags}?, \textit{mono\_preds}?, \textit{mono\_tags}?, \\
-\textit{mangled\_preds}?, \textit{mangled\_tags}?, \textit{simple}? (quasi-sound):} \\
-The type systems \textit{poly\_preds}, \textit{poly\_tags},
+\textit{mangled\_preds}?, \textit{mangled\_tags}?, \textit{simple}?, \textit{simple\_higher}? (quasi-sound):} \\
+The type encodings \textit{poly\_preds}, \textit{poly\_tags},
\textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
-\textit{mangled\_tags}, and \textit{simple} are fully typed and sound. For each
-of these, Sledgehammer also provides a lighter, virtually sound variant
-identified by a question mark (`{?}')\ that detects and erases monotonic types,
-notably infinite types. (For \textit{simple}, the types are not actually erased
-but rather replaced by a shared uniform type of individuals.) As argument to the
-\textit{metis} proof method, the question mark is replaced by a
-``\textit{\_query}'' suffix. If the \emph{sound} option is enabled, these
-encodings are fully sound.
+\textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} are fully
+typed and sound. For each of these, Sledgehammer also provides a lighter,
+virtually sound variant identified by a question mark (`{?}')\ that detects and
+erases monotonic types, notably infinite types. (For \textit{simple} and
+\textit{simple\_higher}, the types are not actually erased but rather replaced
+by a shared uniform type of individuals.) As argument to the \textit{metis}
+proof method, the question mark is replaced by a \hbox{``\textit{\_query}''}
+suffix. If the \emph{sound} option is enabled, these encodings are fully sound.
\item[$\bullet$]
\textbf{%
\textit{poly\_preds}!, \textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\
-\textit{mangled\_preds}!, \textit{mangled\_tags}!, \textit{simple}! \\
+\textit{mangled\_preds}!, \textit{mangled\_tags}!, \textit{simple}!, \textit{simple\_higher}! \\
(mildly unsound):} \\
-The type systems \textit{poly\_preds}, \textit{poly\_tags},
+The type encodings \textit{poly\_preds}, \textit{poly\_tags},
\textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
-\textit{mangled\_tags}, and \textit{simple} also admit a mildly unsound (but
-very efficient) variant identified by an exclamation mark (`{!}') that detects
-and erases erases all types except those that are clearly finite (e.g.,
-\textit{bool}). (For \textit{simple}, the types are not actually erased but
-rather replaced by a shared uniform type of individuals.) As argument to the
-\textit{metis} proof method, the exclamation mark is replaced by a
-``\textit{\_bang}'' suffix.
+\textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
+a mildly unsound (but very efficient) variant identified by an exclamation mark
+(`{!}') that detects and erases erases all types except those that are clearly
+finite (e.g., \textit{bool}). (For \textit{simple} and \textit{simple\_higher},
+the types are not actually erased but rather replaced by a shared uniform type
+of individuals.) As argument to the \textit{metis} proof method, the exclamation
+mark is replaced by a \hbox{``\textit{\_bang}''} suffix.
\item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
the ATP and should be the most efficient virtually sound encoding for that ATP.
\end{enum}
-In addition, all the \textit{preds} and \textit{tags} type systems are available
-in two variants, a lightweight and a heavyweight variant. The lightweight
-variants are generally more efficient and are the default; the heavyweight
-variants are identified by a \textit{\_heavy} suffix (e.g.,
+In addition, all the \textit{preds} and \textit{tags} type encodings are
+available in two variants, a lightweight and a heavyweight variant. The
+lightweight variants are generally more efficient and are the default; the
+heavyweight variants are identified by a \textit{\_heavy} suffix (e.g.,
\textit{mangled\_preds\_heavy}{?}).
-For SMT solvers and ToFoF-E, the type system is always \textit{simple},
-irrespective of the value of this option.
+For SMT solvers, the type encoding is always \textit{simple}, irrespective of
+the value of this option.
\nopagebreak
{\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
@@ -998,19 +1006,19 @@
Specifies the maximum number of monomorphic instances to generate beyond
\textit{max\_relevant}. The higher this limit is, the more monomorphic instances
are potentially generated. Whether monomorphization takes place depends on the
-type system used.
+type encoding used.
\nopagebreak
-{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).}
+{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
\opdefault{max\_mono\_iters}{int}{\upshape 3}
Specifies the maximum number of iterations for the monomorphization fixpoint
construction. The higher this limit is, the more monomorphic instances are
potentially generated. Whether monomorphization takes place depends on the
-type system used.
+type encoding used.
\nopagebreak
-{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).}
+{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
\end{enum}
\subsection{Output Format}
--- a/src/HOL/Metis_Examples/Proxies.thy Fri Jul 01 17:36:25 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy Fri Jul 01 18:11:17 2011 +0200
@@ -50,215 +50,215 @@
by linarith
lemma "B \<subseteq> C"
-sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
+sledgehammer [type_enc = poly_args, max_relevant = 100, expect = some]
by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
text {* Proxies for logical constants *}
lemma "id (op =) x x"
-sledgehammer [type_sys = erased, expect = none] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = none] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis (full_types) id_apply)
lemma "id True"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "\<not> id False"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "x = id True \<or> x = id False"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id x = id True \<or> id x = id False"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
-sledgehammer [type_sys = erased, expect = none] ()
-sledgehammer [type_sys = poly_args, expect = none] ()
-sledgehammer [type_sys = poly_tags?, expect = some] ()
-sledgehammer [type_sys = poly_tags, expect = some] ()
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] ()
-sledgehammer [type_sys = mangled_tags?, expect = some] ()
-sledgehammer [type_sys = mangled_tags, expect = some] ()
-sledgehammer [type_sys = mangled_preds?, expect = some] ()
-sledgehammer [type_sys = mangled_preds, expect = some] ()
+sledgehammer [type_enc = erased, expect = none] ()
+sledgehammer [type_enc = poly_args, expect = none] ()
+sledgehammer [type_enc = poly_tags?, expect = some] ()
+sledgehammer [type_enc = poly_tags, expect = some] ()
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] ()
+sledgehammer [type_enc = mangled_tags?, expect = some] ()
+sledgehammer [type_enc = mangled_tags, expect = some] ()
+sledgehammer [type_enc = mangled_preds?, expect = some] ()
+sledgehammer [type_enc = mangled_preds, expect = some] ()
by (metis (full_types))
lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id a"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id b"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id (a \<or> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id b \<Longrightarrow> id (a \<or> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
-sledgehammer [type_sys = erased, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = erased, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
by (metis_exhaust id_apply)
end
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Fri Jul 01 17:36:25 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Fri Jul 01 18:11:17 2011 +0200
@@ -24,7 +24,7 @@
ML {*
(* The commented-out type systems are too incomplete for our exhaustive
tests. *)
-val type_syss =
+val type_encs =
["erased",
"poly_preds",
"poly_preds_heavy",
@@ -43,8 +43,8 @@
"mangled_args",
"simple",
"poly_preds?",
-(* "poly_preds_heavy?", *)
-(* "poly_tags?", *)
+ "poly_preds_heavy?",
+ "poly_tags?",
(* "poly_tags_heavy?", *)
"mono_preds?",
"mono_preds_heavy?",
@@ -56,9 +56,9 @@
"mangled_tags_heavy?",
"simple?",
"poly_preds!",
-(* "poly_preds_heavy!", *)
+ "poly_preds_heavy!",
(* "poly_tags!", *)
-(* "poly_tags_heavy!", *)
+ "poly_tags_heavy!",
"mono_preds!",
"mono_preds_heavy!",
"mono_tags!",
@@ -72,18 +72,18 @@
fun metis_exhaust_tac ctxt ths =
let
fun tac [] st = all_tac st
- | tac (type_sys :: type_syss) st =
- st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *)
- |> ((if null type_syss then all_tac else rtac @{thm fork} 1)
- THEN Metis_Tactics.metis_tac [type_sys] ctxt ths 1
+ | tac (type_enc :: type_encs) st =
+ st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *)
+ |> ((if null type_encs then all_tac else rtac @{thm fork} 1)
+ THEN Metis_Tactics.metis_tac [type_enc] ctxt ths 1
THEN COND (has_fewer_prems 2) all_tac no_tac
- THEN tac type_syss)
+ THEN tac type_encs)
in tac end
*}
method_setup metis_exhaust = {*
Attrib.thms >>
- (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_syss))
+ (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_encs))
*} "exhaustively run the new Metis with all type encodings"
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 01 17:36:25 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 01 18:11:17 2011 +0200
@@ -8,7 +8,7 @@
val proverK = "prover"
val prover_timeoutK = "prover_timeout"
val keepK = "keep"
-val type_sysK = "type_sys"
+val type_encK = "type_enc"
val slicingK = "slicing"
val e_weight_methodK = "e_weight_method"
val spass_force_sosK = "spass_force_sos"
@@ -353,7 +353,7 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos
+fun run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
vampire_force_sos hard_timeout timeout dir st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
@@ -377,7 +377,7 @@
val params as {relevance_thresholds, max_relevant, slicing, ...} =
Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),
- ("type_sys", type_sys),
+ ("type_enc", type_enc),
("max_relevant", max_relevant),
("slicing", slicing),
("timeout", string_of_int timeout)]
@@ -452,7 +452,7 @@
val _ = change_data id inc_sh_calls
val _ = if trivial then () else change_data id inc_sh_nontriv_calls
val (prover_name, prover) = get_prover (Proof.context_of st) args
- val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
+ val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
val slicing = AList.lookup (op =) args slicingK |> the_default "true"
val e_weight_method = AList.lookup (op =) args e_weight_methodK
@@ -466,7 +466,7 @@
minimizer has a chance to do its magic *)
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
- run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos
+ run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
vampire_force_sos hard_timeout timeout dir st
in
case result of
@@ -503,7 +503,7 @@
val ctxt = Proof.context_of st
val n0 = length (these (!named_thms))
val (prover_name, _) = get_prover ctxt args
- val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
+ val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
val timeout =
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *)
@@ -511,7 +511,7 @@
val params = Sledgehammer_Isar.default_params ctxt
[("provers", prover_name),
("verbose", "true"),
- ("type_sys", type_sys),
+ ("type_enc", type_enc),
("timeout", string_of_int timeout)]
val minimize =
Sledgehammer_Minimize.minimize_facts prover_name params
@@ -546,9 +546,9 @@
else if !reconstructor = "smt" then
SMT_Solver.smt_tac
else if full orelse !reconstructor = "metis (full_types)" then
- Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys]
+ Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc]
else if !reconstructor = "metis (no_types)" then
- Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
+ Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
else
Metis_Tactics.metis_tac []) ctxt thms
fun apply_reconstructor thms =
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 01 17:36:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 01 18:11:17 2011 +0200
@@ -172,6 +172,7 @@
if method = e_autoN then
"-xAutoDev"
else
+ (* supplied by Stephan Schulz *)
"--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
\--destructive-er-aggressive --destructive-er --presat-simplify \
\--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
@@ -385,8 +386,8 @@
prem_kind = prem_kind,
formats = formats,
best_slices = fn ctxt =>
- let val (max_relevant, type_sys) = best_slice ctxt in
- [(1.0, (false, (max_relevant, type_sys, "")))]
+ let val (max_relevant, type_enc) = best_slice ctxt in
+ [(1.0, (false, (max_relevant, type_enc, "")))]
end}
fun remotify_config system_name system_versions best_slice
@@ -414,10 +415,10 @@
remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_preds?") (* FUDGE *))
val remote_leo2 =
remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
- (K (100, "simple") (* FUDGE *))
+ (K (100, "simple_higher") (* FUDGE *))
val remote_satallax =
remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
- (K (64, "simple") (* FUDGE *))
+ (K (64, "simple_higher") (* FUDGE *))
val remote_sine_e =
remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
Conjecture [FOF] (K (500, "mangled_preds?") (* FUDGE *))
--- a/src/HOL/Tools/ATP/atp_translate.ML Fri Jul 01 17:36:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Jul 01 18:11:17 2011 +0200
@@ -19,14 +19,15 @@
General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
Chained
+ datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
datatype type_level =
All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
No_Types
datatype type_heaviness = Heavyweight | Lightweight
- datatype type_sys =
- Simple_Types of type_level |
+ datatype type_enc =
+ Simple_Types of order * type_level |
Preds of polymorphism * type_level * type_heaviness |
Tags of polymorphism * type_level * type_heaviness
@@ -74,12 +75,12 @@
val atp_irrelevant_consts : string list
val atp_schematic_consts_of : term -> typ list Symtab.table
val is_locality_global : locality -> bool
- val type_sys_from_string : string -> type_sys
- val polymorphism_of_type_sys : type_sys -> polymorphism
- val level_of_type_sys : type_sys -> type_level
- val is_type_sys_virtually_sound : type_sys -> bool
- val is_type_sys_fairly_sound : type_sys -> bool
- val choose_format : format list -> type_sys -> format * type_sys
+ val type_enc_from_string : string -> type_enc
+ val polymorphism_of_type_enc : type_enc -> polymorphism
+ val level_of_type_enc : type_enc -> type_level
+ val is_type_enc_virtually_sound : type_enc -> bool
+ val is_type_enc_fairly_sound : type_enc -> bool
+ val choose_format : format list -> type_enc -> format * type_enc
val mk_aconns :
connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
val unmangled_const : string -> string * string fo_term list
@@ -87,7 +88,7 @@
val helper_table : ((string * bool) * thm list) list
val factsN : string
val prepare_atp_problem :
- Proof.context -> format -> formula_kind -> formula_kind -> type_sys -> bool
+ Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
-> bool -> bool -> bool -> term list -> term
-> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
@@ -269,24 +270,19 @@
SOME c' => c'
| NONE => ascii_of c
-(*Remove the initial ' character from a type variable, if it is present*)
-fun trim_type_var s =
- if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
- else raise Fail ("trim_type: Malformed type variable encountered: " ^ s)
-
-fun ascii_of_indexname (v,0) = ascii_of v
- | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i
+fun ascii_of_indexname (v, 0) = ascii_of v
+ | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
fun make_bound_var x = bound_var_prefix ^ ascii_of x
fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
-fun make_schematic_type_var (x,i) =
- tvar_prefix ^ (ascii_of_indexname (trim_type_var x, i))
-fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x))
+fun make_schematic_type_var (x, i) =
+ tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
+fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
-(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
-fun make_fixed_const @{const_name HOL.eq} = "equal"
+(* "HOL.eq" is mapped to the ATP's equality. *)
+fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal
| make_fixed_const c = const_prefix ^ lookup_const c
fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
@@ -390,8 +386,8 @@
| multi_arity_clause ((tcons, ars) :: tc_arlists) =
arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
-(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
- provided its arguments have the corresponding sorts.*)
+(* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
+ theory thy provided its arguments have the corresponding sorts. *)
fun type_class_pairs thy tycons classes =
let
val alg = Sign.classes_of thy
@@ -426,7 +422,8 @@
subclass : name,
superclass : name}
-(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
+(* Generate all pairs (sub, super) such that sub is a proper subclass of super
+ in theory "thy". *)
fun class_pairs _ [] _ = []
| class_pairs thy subs supers =
let
@@ -435,9 +432,8 @@
fun add_supers sub = fold (add_super sub) supers
in fold add_supers subs [] end
-fun make_class_rel_clause (sub,super) =
- {name = sub ^ "_" ^ super,
- subclass = `make_type_class sub,
+fun make_class_rel_clause (sub, super) =
+ {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
superclass = `make_type_class super}
fun make_class_rel_clauses thy subs supers =
@@ -506,21 +502,22 @@
| is_locality_global Chained = false
| is_locality_global _ = true
+datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
datatype type_level =
All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
No_Types
datatype type_heaviness = Heavyweight | Lightweight
-datatype type_sys =
- Simple_Types of type_level |
+datatype type_enc =
+ Simple_Types of order * type_level |
Preds of polymorphism * type_level * type_heaviness |
Tags of polymorphism * type_level * type_heaviness
fun try_unsuffixes ss s =
fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
-fun type_sys_from_string s =
+fun type_enc_from_string s =
(case try (unprefix "poly_") s of
SOME s => (SOME Polymorphic, s)
| NONE =>
@@ -531,7 +528,8 @@
SOME s => (SOME Mangled_Monomorphic, s)
| NONE => (NONE, s))
||> (fn s =>
- (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
+ (* "_query" and "_bang" are for the ASCII-challenged Metis and
+ Mirabelle. *)
case try_unsuffixes ["?", "_query"] s of
SOME s => (Noninf_Nonmono_Types, s)
| NONE =>
@@ -544,7 +542,10 @@
| NONE => (Lightweight, s))
|> (fn (poly, (level, (heaviness, core))) =>
case (core, (poly, level, heaviness)) of
- ("simple", (NONE, _, Lightweight)) => Simple_Types level
+ ("simple", (NONE, _, Lightweight)) =>
+ Simple_Types (First_Order, level)
+ | ("simple_higher", (NONE, _, Lightweight)) =>
+ Simple_Types (Higher_Order, level)
| ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
| ("tags", (SOME Polymorphic, _, _)) =>
Tags (Polymorphic, level, heaviness)
@@ -556,43 +557,46 @@
| _ => raise Same.SAME)
handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
-fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
- | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
- | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
+fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
+ | is_type_enc_higher_order _ = false
+
+fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
+ | polymorphism_of_type_enc (Preds (poly, _, _)) = poly
+ | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
-fun level_of_type_sys (Simple_Types level) = level
- | level_of_type_sys (Preds (_, level, _)) = level
- | level_of_type_sys (Tags (_, level, _)) = level
+fun level_of_type_enc (Simple_Types (_, level)) = level
+ | level_of_type_enc (Preds (_, level, _)) = level
+ | level_of_type_enc (Tags (_, level, _)) = level
-fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
- | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
- | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
+fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
+ | heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness
+ | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
fun is_type_level_virtually_sound level =
level = All_Types orelse level = Noninf_Nonmono_Types
-val is_type_sys_virtually_sound =
- is_type_level_virtually_sound o level_of_type_sys
+val is_type_enc_virtually_sound =
+ is_type_level_virtually_sound o level_of_type_enc
fun is_type_level_fairly_sound level =
is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
-val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
-
-fun is_setting_higher_order THF (Simple_Types _) = true
- | is_setting_higher_order _ _ = false
+val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
-fun choose_format formats (Simple_Types level) =
- if member (op =) formats THF then (THF, Simple_Types level)
- else if member (op =) formats TFF then (TFF, Simple_Types level)
- else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
- | choose_format formats type_sys =
+fun choose_format formats (Simple_Types (order, level)) =
+ if member (op =) formats THF then
+ (THF, Simple_Types (order, level))
+ else if member (op =) formats TFF then
+ (TFF, Simple_Types (First_Order, level))
+ else
+ choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
+ | choose_format formats type_enc =
(case hd formats of
CNF_UEQ =>
- (CNF_UEQ, case type_sys of
+ (CNF_UEQ, case type_enc of
Preds stuff =>
- (if is_type_sys_fairly_sound type_sys then Tags else Preds)
+ (if is_type_enc_fairly_sound type_enc then Tags else Preds)
stuff
- | _ => type_sys)
- | format => (format, type_sys))
+ | _ => type_enc)
+ | format => (format, type_enc))
type translated_formula =
{name : string,
@@ -624,29 +628,32 @@
fun should_drop_arg_type_args (Simple_Types _) =
false (* since TFF doesn't support overloading *)
- | should_drop_arg_type_args type_sys =
- level_of_type_sys type_sys = All_Types andalso
- heaviness_of_type_sys type_sys = Heavyweight
+ | should_drop_arg_type_args type_enc =
+ level_of_type_enc type_enc = All_Types andalso
+ heaviness_of_type_enc type_enc = Heavyweight
-fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
- | general_type_arg_policy type_sys =
- if level_of_type_sys type_sys = No_Types then
+fun type_arg_policy type_enc s =
+ if s = type_tag_name then
+ (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
+ Mangled_Type_Args
+ else
+ Explicit_Type_Args) false
+ else case type_enc of
+ Tags (_, All_Types, Heavyweight) => No_Type_Args
+ | _ =>
+ if level_of_type_enc type_enc = No_Types orelse
+ s = @{const_name HOL.eq} orelse
+ (s = app_op_name andalso
+ level_of_type_enc type_enc = Const_Arg_Types) then
No_Type_Args
- else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
- Mangled_Type_Args (should_drop_arg_type_args type_sys)
else
- Explicit_Type_Args (should_drop_arg_type_args type_sys)
+ should_drop_arg_type_args type_enc
+ |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
+ Mangled_Type_Args
+ else
+ Explicit_Type_Args)
-fun type_arg_policy type_sys s =
- if s = @{const_name HOL.eq} orelse
- (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
- No_Type_Args
- else if s = type_tag_name then
- Explicit_Type_Args false
- else
- general_type_arg_policy type_sys
-
-(*Make literals for sorted type variables*)
+(* Make literals for sorted type variables. *)
fun generic_add_sorts_on_type (_, []) = I
| generic_add_sorts_on_type ((x, i), s :: ss) =
generic_add_sorts_on_type ((x, i), ss)
@@ -662,8 +669,8 @@
fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
| add_sorts_on_tvar _ = I
-fun type_literals_for_types type_sys add_sorts_on_typ Ts =
- [] |> level_of_type_sys type_sys <> No_Types ? fold add_sorts_on_typ Ts
+fun type_literals_for_types type_enc add_sorts_on_typ Ts =
+ [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
fun mk_aconns c phis =
let val (phis', phi') = split_last phis in
@@ -698,10 +705,10 @@
val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
val homo_infinite_type = Type (homo_infinite_type_name, [])
-fun fo_term_from_typ format type_sys =
+fun fo_term_from_typ format type_enc =
let
fun term (Type (s, Ts)) =
- ATerm (case (is_setting_higher_order format type_sys, s) of
+ ATerm (case (is_type_enc_higher_order type_enc, s) of
(true, @{type_name bool}) => `I tptp_bool_type
| (true, @{type_name fun}) => `I tptp_fun_type
| _ => if s = homo_infinite_type_name andalso
@@ -715,8 +722,8 @@
ATerm ((make_schematic_type_var x, s), [])
in term end
-fun fo_term_for_type_arg format type_sys T =
- if T = dummyT then NONE else SOME (fo_term_from_typ format type_sys T)
+fun fo_term_for_type_arg format type_enc T =
+ if T = dummyT then NONE else SOME (fo_term_from_typ format type_enc T)
(* This shouldn't clash with anything else. *)
val mangled_type_sep = "\000"
@@ -735,7 +742,7 @@
else
simple_type_prefix ^ ascii_of s
-fun ho_type_from_fo_term format type_sys pred_sym ary =
+fun ho_type_from_fo_term type_enc pred_sym ary =
let
fun to_atype ty =
AType ((make_simple_type (generic_mangled_type_name fst ty),
@@ -745,15 +752,15 @@
| to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
fun to_ho (ty as ATerm ((s, _), tys)) =
if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
- in if is_setting_higher_order format type_sys then to_ho else to_fo ary end
+ in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
-fun mangled_type format type_sys pred_sym ary =
- ho_type_from_fo_term format type_sys pred_sym ary
- o fo_term_from_typ format type_sys
+fun mangled_type format type_enc pred_sym ary =
+ ho_type_from_fo_term type_enc pred_sym ary
+ o fo_term_from_typ format type_enc
-fun mangled_const_name format type_sys T_args (s, s') =
+fun mangled_const_name format type_enc T_args (s, s') =
let
- val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_sys)
+ val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_enc)
fun type_suffix f g =
fold_rev (curry (op ^) o g o prefix mangled_type_sep
o generic_mangled_type_name f) ty_args ""
@@ -782,14 +789,14 @@
(hd ss, map unmangled_type (tl ss))
end
-fun introduce_proxies format type_sys =
+fun introduce_proxies type_enc =
let
fun intro top_level (CombApp (tm1, tm2)) =
CombApp (intro top_level tm1, intro false tm2)
| intro top_level (CombConst (name as (s, _), T, T_args)) =
(case proxify_const s of
SOME proxy_base =>
- if top_level orelse is_setting_higher_order format type_sys then
+ if top_level orelse is_type_enc_higher_order type_enc then
case (top_level, s) of
(_, "c_False") => (`I tptp_false, [])
| (_, "c_True") => (`I tptp_true, [])
@@ -808,11 +815,11 @@
| intro _ tm = tm
in intro true end
-fun combformula_from_prop thy format type_sys eq_as_iff =
+fun combformula_from_prop thy type_enc eq_as_iff =
let
fun do_term bs t atomic_types =
combterm_from_term thy bs (Envir.eta_contract t)
- |>> (introduce_proxies format type_sys #> AAtom)
+ |>> (introduce_proxies type_enc #> AAtom)
||> union (op =) atomic_types
fun do_quant bs q s T t' =
let val s = singleton (Name.variant_list (map fst bs)) s in
@@ -933,27 +940,27 @@
end
(* making fact and conjecture formulas *)
-fun make_formula thy format type_sys eq_as_iff name loc kind t =
+fun make_formula thy type_enc eq_as_iff name loc kind t =
let
val (combformula, atomic_types) =
- combformula_from_prop thy format type_sys eq_as_iff t []
+ combformula_from_prop thy type_enc eq_as_iff t []
in
{name = name, locality = loc, kind = kind, combformula = combformula,
atomic_types = atomic_types}
end
-fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts
+fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
((name, loc), t) =
let val thy = Proof_Context.theory_of ctxt in
case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
- |> make_formula thy format type_sys (eq_as_iff andalso format <> CNF)
- name loc Axiom of
+ |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
+ loc Axiom of
formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
if s = tptp_true then NONE else SOME formula
| formula => SOME formula
end
-fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
+fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts =
let
val thy = Proof_Context.theory_of ctxt
val last = length ts - 1
@@ -970,8 +977,8 @@
in
t |> preproc ?
(preprocess_prop ctxt presimp_consts kind #> freeze_term)
- |> make_formula thy format type_sys (format <> CNF)
- (string_of_int j) Local kind
+ |> make_formula thy type_enc (format <> CNF) (string_of_int j)
+ Local kind
|> maybe_negate
end)
(0 upto last) ts
@@ -1224,7 +1231,7 @@
end
handle TYPE _ => T_args
-fun enforce_type_arg_policy_in_combterm ctxt format type_sys =
+fun enforce_type_arg_policy_in_combterm ctxt format type_enc =
let
val thy = Proof_Context.theory_of ctxt
fun aux arity (CombApp (tm1, tm2)) =
@@ -1238,11 +1245,11 @@
fun filtered_T_args false = T_args
| filtered_T_args true = filter_type_args thy s'' arity T_args
in
- case type_arg_policy type_sys s'' of
+ case type_arg_policy type_enc s'' of
Explicit_Type_Args drop_args =>
(name, filtered_T_args drop_args)
| Mangled_Type_Args drop_args =>
- (mangled_const_name format type_sys (filtered_T_args drop_args)
+ (mangled_const_name format type_enc (filtered_T_args drop_args)
name, [])
| No_Type_Args => (name, [])
end)
@@ -1250,14 +1257,14 @@
| aux _ tm = tm
in aux 0 end
-fun repair_combterm ctxt format type_sys sym_tab =
- not (is_setting_higher_order format type_sys)
+fun repair_combterm ctxt format type_enc sym_tab =
+ not (is_type_enc_higher_order type_enc)
? (introduce_explicit_apps_in_combterm sym_tab
#> introduce_predicators_in_combterm sym_tab)
- #> enforce_type_arg_policy_in_combterm ctxt format type_sys
-fun repair_fact ctxt format type_sys sym_tab =
+ #> enforce_type_arg_policy_in_combterm ctxt format type_enc
+fun repair_fact ctxt format type_enc sym_tab =
update_combformula (formula_map
- (repair_combterm ctxt format type_sys sym_tab))
+ (repair_combterm ctxt format type_enc sym_tab))
(** Helper facts **)
@@ -1306,32 +1313,35 @@
|> close_formula_universally, simp_info, NONE)
end
-fun should_specialize_helper type_sys t =
- case general_type_arg_policy type_sys of
- Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
- | _ => false
+fun should_specialize_helper type_enc t =
+ polymorphism_of_type_enc type_enc = Mangled_Monomorphic andalso
+ level_of_type_enc type_enc <> No_Types andalso
+ not (null (Term.hidden_polymorphism t))
-fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
+fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
case strip_prefix_and_unascii const_prefix s of
SOME mangled_s =>
let
val thy = Proof_Context.theory_of ctxt
val unmangled_s = mangled_s |> unmangled_const_name
+ fun dub needs_fairly_sound j k =
+ (unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
+ (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
+ (if needs_fairly_sound then typed_helper_suffix
+ else untyped_helper_suffix),
+ Helper)
fun dub_and_inst needs_fairly_sound (th, j) =
- ((unmangled_s ^ "_" ^ string_of_int j ^
- (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
- (if needs_fairly_sound then typed_helper_suffix
- else untyped_helper_suffix),
- Helper),
- let val t = th |> prop_of in
- t |> should_specialize_helper type_sys t
- ? (case types of
- [T] => specialize_type thy (invert_const unmangled_s, T)
- | _ => I)
- end)
+ let val t = prop_of th in
+ if should_specialize_helper type_enc t then
+ map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
+ types
+ else
+ [t]
+ end
+ |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
val make_facts =
- map_filter (make_fact ctxt format type_sys false false [])
- val fairly_sound = is_type_sys_fairly_sound type_sys
+ map_filter (make_fact ctxt format type_enc false false [])
+ val fairly_sound = is_type_enc_fairly_sound type_enc
in
helper_table
|> maps (fn ((helper_s, needs_fairly_sound), ths) =>
@@ -1340,12 +1350,12 @@
[]
else
ths ~~ (1 upto length ths)
- |> map (dub_and_inst needs_fairly_sound)
+ |> maps (dub_and_inst needs_fairly_sound)
|> make_facts)
end
| NONE => []
-fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
- Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
+fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
+ Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
[]
(***************************************************************)
@@ -1367,9 +1377,8 @@
val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
-(*fold type constructors*)
-fun fold_type_constrs f (Type (a, Ts)) x =
- fold (fold_type_constrs f) Ts (f (a,x))
+fun fold_type_constrs f (Type (s, Ts)) x =
+ fold (fold_type_constrs f) Ts (f (s, x))
| fold_type_constrs _ _ x = x
(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
@@ -1387,13 +1396,13 @@
fun type_constrs_of_terms thy ts =
Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
-fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
+fun translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
facts =
let
val thy = Proof_Context.theory_of ctxt
val fact_ts = facts |> map snd
val presimp_consts = Meson.presimplified_consts ctxt
- val make_fact = make_fact ctxt format type_sys true preproc presimp_consts
+ val make_fact = make_fact ctxt format type_enc true preproc presimp_consts
val (facts, fact_names) =
facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
|> map_filter (try (apfst the))
@@ -1410,9 +1419,9 @@
val tycons = type_constrs_of_terms thy all_ts
val conjs =
hyp_ts @ [concl_t]
- |> make_conjecture ctxt format prem_kind type_sys preproc presimp_consts
+ |> make_conjecture ctxt format prem_kind type_enc preproc presimp_consts
val (supers', arity_clauses) =
- if level_of_type_sys type_sys = No_Types then ([], [])
+ if level_of_type_enc type_enc = No_Types then ([], [])
else make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers'
in
@@ -1428,9 +1437,9 @@
val type_pred = `make_fixed_const type_pred_name
-fun type_pred_combterm ctxt format type_sys T tm =
+fun type_pred_combterm ctxt format type_enc T tm =
CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
- |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
+ |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm)
fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
| is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
@@ -1439,15 +1448,15 @@
formula_fold pos (is_var_positively_naked_in_term name) phi false
| should_predicate_on_var_in_formula _ _ _ _ = true
-fun mk_const_aterm format type_sys x T_args args =
- ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
+fun mk_const_aterm format type_enc x T_args args =
+ ATerm (x, map_filter (fo_term_for_type_arg format type_enc) T_args @ args)
-fun tag_with_type ctxt format nonmono_Ts type_sys pos T tm =
+fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
CombConst (type_tag, T --> T, [T])
- |> enforce_type_arg_policy_in_combterm ctxt format type_sys
- |> term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
+ |> enforce_type_arg_policy_in_combterm ctxt format type_enc
+ |> term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
|> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
-and term_from_combterm ctxt format nonmono_Ts type_sys =
+and term_from_combterm ctxt format nonmono_Ts type_enc =
let
fun aux site u =
let
@@ -1463,32 +1472,32 @@
(pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
| Eq_Arg pos => (pos, Elsewhere)
| Elsewhere => (NONE, Elsewhere)
- val t = mk_const_aterm format type_sys x T_args
+ val t = mk_const_aterm format type_enc x T_args
(map (aux arg_site) args)
val T = combtyp_of u
in
- t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
- tag_with_type ctxt format nonmono_Ts type_sys pos T
+ t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
+ tag_with_type ctxt format nonmono_Ts type_enc pos T
else
I)
end
in aux end
-and formula_from_combformula ctxt format nonmono_Ts type_sys
+and formula_from_combformula ctxt format nonmono_Ts type_enc
should_predicate_on_var =
let
fun do_term pos =
- term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
+ term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
val do_bound_type =
- case type_sys of
- Simple_Types level =>
+ case type_enc of
+ Simple_Types (_, level) =>
homogenized_type ctxt nonmono_Ts level 0
- #> mangled_type format type_sys false 0 #> SOME
+ #> mangled_type format type_enc false 0 #> SOME
| _ => K NONE
fun do_out_of_bound_type pos phi universal (name, T) =
- if should_predicate_on_type ctxt nonmono_Ts type_sys
+ if should_predicate_on_type ctxt nonmono_Ts type_enc
(fn () => should_predicate_on_var pos phi universal name) T then
CombVar (name, T)
- |> type_pred_combterm ctxt format type_sys T
+ |> type_pred_combterm ctxt format type_enc T
|> do_term pos |> AAtom |> SOME
else
NONE
@@ -1511,23 +1520,23 @@
| do_formula pos (AAtom tm) = AAtom (do_term pos tm)
in do_formula end
-fun bound_tvars type_sys Ts =
+fun bound_tvars type_enc Ts =
mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
- (type_literals_for_types type_sys add_sorts_on_tvar Ts))
+ (type_literals_for_types type_enc add_sorts_on_tvar Ts))
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
- type_sys (j, {name, locality, kind, combformula, atomic_types}) =
+ type_enc (j, {name, locality, kind, combformula, atomic_types}) =
(prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
kind,
combformula
|> close_combformula_universally
- |> formula_from_combformula ctxt format nonmono_Ts type_sys
+ |> formula_from_combformula ctxt format nonmono_Ts type_enc
should_predicate_on_var_in_formula
(if pos then SOME true else NONE)
- |> bound_tvars type_sys atomic_types
+ |> bound_tvars type_enc atomic_types
|> close_formula_universally,
NONE,
case locality of
@@ -1560,45 +1569,45 @@
(fo_literal_from_arity_literal concl_lits))
|> close_formula_universally, intro_info, NONE)
-fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
+fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
({name, kind, combformula, atomic_types, ...} : translated_formula) =
Formula (conjecture_prefix ^ name, kind,
- formula_from_combformula ctxt format nonmono_Ts type_sys
+ formula_from_combformula ctxt format nonmono_Ts type_enc
should_predicate_on_var_in_formula (SOME false)
(close_combformula_universally combformula)
- |> bound_tvars type_sys atomic_types
+ |> bound_tvars type_enc atomic_types
|> close_formula_universally, NONE, NONE)
-fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
- atomic_types |> type_literals_for_types type_sys add_sorts_on_tfree
+fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
+ atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
|> map fo_literal_from_type_literal
fun formula_line_for_free_type j lit =
Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
formula_from_fo_literal lit, NONE, NONE)
-fun formula_lines_for_free_types type_sys facts =
+fun formula_lines_for_free_types type_enc facts =
let
- val litss = map (free_type_literals type_sys) facts
+ val litss = map (free_type_literals type_enc) facts
val lits = fold (union (op =)) litss []
in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
(** Symbol declarations **)
-fun should_declare_sym type_sys pred_sym s =
+fun should_declare_sym type_enc pred_sym s =
is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
- (case type_sys of
+ (case type_enc of
Simple_Types _ => true
| Tags (_, _, Lightweight) => true
| _ => not pred_sym)
-fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
+fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
let
fun add_combterm in_conj tm =
let val (head, args) = strip_combterm_comb tm in
(case head of
CombConst ((s, s'), T, T_args) =>
let val pred_sym = is_pred_sym repaired_sym_tab s in
- if should_declare_sym type_sys pred_sym s then
+ if should_declare_sym type_enc pred_sym s then
Symtab.map_default (s, [])
(insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
in_conj))
@@ -1612,7 +1621,7 @@
fact_lift (formula_fold NONE (K (add_combterm in_conj)))
in
Symtab.empty
- |> is_type_sys_fairly_sound type_sys
+ |> is_type_enc_fairly_sound type_enc
? (fold (add_fact true) conjs #> fold (add_fact false) facts)
end
@@ -1635,8 +1644,8 @@
formula_fold (SOME (kind <> Conjecture))
(add_combterm_nonmonotonic_types ctxt level sound locality)
combformula
-fun nonmonotonic_types_for_facts ctxt type_sys sound facts =
- let val level = level_of_type_sys type_sys in
+fun nonmonotonic_types_for_facts ctxt type_enc sound facts =
+ let val level = level_of_type_enc type_enc in
if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
[] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
(* We must add "bool" in case the helper "True_or_False" is added
@@ -1647,21 +1656,21 @@
[]
end
-fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
+fun decl_line_for_sym ctxt format nonmono_Ts type_enc s
(s', T_args, T, pred_sym, ary, _) =
let
val (T_arg_Ts, level) =
- case type_sys of
- Simple_Types level => ([], level)
+ case type_enc of
+ Simple_Types (_, level) => ([], level)
| _ => (replicate (length T_args) homo_infinite_type, No_Types)
in
Decl (sym_decl_prefix ^ s, (s, s'),
(T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
- |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))
+ |> mangled_type format type_enc pred_sym (length T_arg_Ts + ary))
end
fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
- poly_nonmono_Ts type_sys n s j (s', T_args, T, _, ary, in_conj) =
+ poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
let
val (kind, maybe_negate) =
if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
@@ -1675,7 +1684,7 @@
val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
fun should_keep_arg_type T =
sym_needs_arg_types orelse
- not (should_predicate_on_type ctxt nonmono_Ts type_sys (K false) T)
+ not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)
val bound_Ts =
arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
in
@@ -1683,18 +1692,18 @@
(if n > 1 then "_" ^ string_of_int j else ""), kind,
CombConst ((s, s'), T, T_args)
|> fold (curry (CombApp o swap)) bounds
- |> type_pred_combterm ctxt format type_sys res_T
+ |> type_pred_combterm ctxt format type_enc res_T
|> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
- |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys
+ |> formula_from_combformula ctxt format poly_nonmono_Ts type_enc
(K (K (K (K true)))) (SOME true)
- |> n > 1 ? bound_tvars type_sys (atyps_of T)
+ |> n > 1 ? bound_tvars type_enc (atyps_of T)
|> close_formula_universally
|> maybe_negate,
intro_info, NONE)
end
fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
- poly_nonmono_Ts type_sys n s
+ poly_nonmono_Ts type_enc n s
(j, (s', T_args, T, pred_sym, ary, in_conj)) =
let
val ident_base =
@@ -1707,22 +1716,22 @@
val bound_names =
1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
val bounds = bound_names |> map (fn name => ATerm (name, []))
- val cst = mk_const_aterm format type_sys (s, s') T_args
+ val cst = mk_const_aterm format type_enc (s, s') T_args
val atomic_Ts = atyps_of T
fun eq tms =
(if pred_sym then AConn (AIff, map AAtom tms)
else AAtom (ATerm (`I tptp_equal, tms)))
- |> bound_tvars type_sys atomic_Ts
+ |> bound_tvars type_enc atomic_Ts
|> close_formula_universally
|> maybe_negate
(* See also "should_tag_with_type". *)
fun should_encode T =
should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
- (case type_sys of
+ (case type_enc of
Tags (Polymorphic, level, Lightweight) =>
level <> All_Types andalso Monomorph.typ_has_tvars T
| _ => false)
- val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_sys NONE
+ val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_enc NONE
val add_formula_for_res =
if should_encode res_T then
cons (Formula (ident_base ^ "_res", kind,
@@ -1751,10 +1760,10 @@
fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
- poly_nonmono_Ts type_sys (s, decls) =
- case type_sys of
+ poly_nonmono_Ts type_enc (s, decls) =
+ case type_enc of
Simple_Types _ =>
- decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
+ decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
| Preds _ =>
let
val decls =
@@ -1770,13 +1779,13 @@
| _ => decls
val n = length decls
val decls =
- decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_sys
+ decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_enc
(K true)
o result_type_of_decl)
in
(0 upto length decls - 1, decls)
|-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
- nonmono_Ts poly_nonmono_Ts type_sys n s)
+ nonmono_Ts poly_nonmono_Ts type_enc n s)
end
| Tags (_, _, heaviness) =>
(case heaviness of
@@ -1785,17 +1794,17 @@
let val n = length decls in
(0 upto n - 1 ~~ decls)
|> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
- conj_sym_kind poly_nonmono_Ts type_sys n s)
+ conj_sym_kind poly_nonmono_Ts type_enc n s)
end)
fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
- poly_nonmono_Ts type_sys sym_decl_tab =
+ poly_nonmono_Ts type_enc sym_decl_tab =
sym_decl_tab
|> Symtab.dest
|> sort_wrt fst
|> rpair []
|-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
- nonmono_Ts poly_nonmono_Ts type_sys)
+ nonmono_Ts poly_nonmono_Ts type_enc)
fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
poly <> Mangled_Monomorphic andalso
@@ -1819,39 +1828,39 @@
val explicit_apply = NONE (* for experimental purposes *)
-fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys sound
+fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
exporter readable_names preproc hyp_ts concl_t facts =
let
- val (format, type_sys) = choose_format [format] type_sys
+ val (format, type_enc) = choose_format [format] type_enc
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
- translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
+ translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
facts
val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
val nonmono_Ts =
- conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys sound
- val repair = repair_fact ctxt format type_sys sym_tab
+ conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound
+ val repair = repair_fact ctxt format type_enc sym_tab
val (conjs, facts) = (conjs, facts) |> pairself (map repair)
val repaired_sym_tab =
conjs @ facts |> sym_table_for_facts ctxt (SOME false)
val helpers =
- repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
+ repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
|> map repair
val poly_nonmono_Ts =
if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
- polymorphism_of_type_sys type_sys <> Polymorphic then
+ polymorphism_of_type_enc type_enc <> Polymorphic then
nonmono_Ts
else
[TVar (("'a", 0), HOLogic.typeS)]
val sym_decl_lines =
(conjs, helpers @ facts)
- |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
+ |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab
|> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
- poly_nonmono_Ts type_sys
+ poly_nonmono_Ts type_enc
val helper_lines =
0 upto length helpers - 1 ~~ helpers
|> map (formula_line_for_fact ctxt format helper_prefix I false true
- poly_nonmono_Ts type_sys)
- |> (if needs_type_tag_idempotence type_sys then
+ poly_nonmono_Ts type_enc)
+ |> (if needs_type_tag_idempotence type_enc then
cons (type_tag_idempotence_fact ())
else
I)
@@ -1862,15 +1871,15 @@
(factsN,
map (formula_line_for_fact ctxt format fact_prefix ascii_of
(not exporter) (not exporter) nonmono_Ts
- type_sys)
+ type_enc)
(0 upto length facts - 1 ~~ facts)),
(class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
(aritiesN, map formula_line_for_arity_clause arity_clauses),
(helpersN, helper_lines),
(conjsN,
- map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
+ map (formula_line_for_conjecture ctxt format nonmono_Ts type_enc)
conjs),
- (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
+ (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
val problem =
problem
|> (case format of
--- a/src/HOL/Tools/Metis/metis_tactics.ML Fri Jul 01 17:36:25 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Fri Jul 01 18:11:17 2011 +0200
@@ -13,10 +13,10 @@
val full_typesN : string
val partial_typesN : string
val no_typesN : string
- val really_full_type_sys : string
- val full_type_sys : string
- val partial_type_sys : string
- val no_type_sys : string
+ val really_full_type_enc : string
+ val full_type_enc : string
+ val partial_type_enc : string
+ val no_type_enc : string
val full_type_syss : string list
val partial_type_syss : string list
val trace : bool Config.T
@@ -39,22 +39,22 @@
val partial_typesN = "partial_types"
val no_typesN = "no_types"
-val really_full_type_sys = "poly_tags_heavy"
-val full_type_sys = "poly_preds_heavy_query"
-val partial_type_sys = "poly_args"
-val no_type_sys = "erased"
+val really_full_type_enc = "poly_tags_heavy"
+val full_type_enc = "poly_preds_heavy_query"
+val partial_type_enc = "poly_args"
+val no_type_enc = "erased"
-val full_type_syss = [full_type_sys, really_full_type_sys]
-val partial_type_syss = partial_type_sys :: full_type_syss
+val full_type_syss = [full_type_enc, really_full_type_enc]
+val partial_type_syss = partial_type_enc :: full_type_syss
-val type_sys_aliases =
+val type_enc_aliases =
[(full_typesN, full_type_syss),
(partial_typesN, partial_type_syss),
- (no_typesN, [no_type_sys])]
+ (no_typesN, [no_type_enc])]
-fun method_call_for_type_sys type_syss =
+fun method_call_for_type_enc type_syss =
metisN ^ " (" ^
- (case AList.find (op =) type_sys_aliases type_syss of
+ (case AList.find (op =) type_enc_aliases type_syss of
[alias] => alias
| _ => hd type_syss) ^ ")"
@@ -102,7 +102,7 @@
val resolution_params = {active = active_params, waiting = waiting_params}
(* Main function to start Metis proof and reconstruction *)
-fun FOL_SOLVE (type_sys :: fallback_type_syss) ctxt cls ths0 =
+fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
let val thy = Proof_Context.theory_of ctxt
val new_skolemizer =
Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
@@ -118,7 +118,7 @@
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
val (sym_tab, axioms, old_skolems) =
- prepare_metis_problem ctxt type_sys cls ths
+ prepare_metis_problem ctxt type_enc cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
| get_isa_thm _ (Isa_Raw ith) = ith
@@ -126,7 +126,7 @@
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
val thms = axioms |> map fst
val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
- val _ = trace_msg ctxt (fn () => "type_sys = " ^ type_sys)
+ val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
in
case filter (fn t => prop_of t aconv @{prop False}) cls of
@@ -186,7 +186,7 @@
| _ =>
(verbose_warning ctxt
("Falling back on " ^
- quote (method_call_for_type_sys fallback_type_syss) ^ "...");
+ quote (method_call_for_type_enc fallback_type_syss) ^ "...");
FOL_SOLVE fallback_type_syss ctxt cls ths0)
val neg_clausify =
@@ -249,7 +249,7 @@
fun setup_method (binding, type_syss) =
((Args.parens (Scan.repeat Parse.short_ident)
- >> maps (fn s => case AList.lookup (op =) type_sys_aliases s of
+ >> maps (fn s => case AList.lookup (op =) type_enc_aliases s of
SOME tss => tss
| NONE => [s]))
|> Scan.option |> Scan.lift)
--- a/src/HOL/Tools/Metis/metis_translate.ML Fri Jul 01 17:36:25 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Fri Jul 01 18:11:17 2011 +0200
@@ -165,11 +165,11 @@
| metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
(* Function to generate metis clauses, including comb and type clauses *)
-fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
+fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
let
- val type_sys = type_sys_from_string type_sys
+ val type_enc = type_enc_from_string type_enc
val (conj_clauses, fact_clauses) =
- if polymorphism_of_type_sys type_sys = Polymorphic then
+ if polymorphism_of_type_enc type_enc = Polymorphic then
(conj_clauses, fact_clauses)
else
conj_clauses @ fact_clauses
@@ -196,7 +196,7 @@
tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys true false false
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false false
false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 01 17:36:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 01 18:11:17 2011 +0200
@@ -84,7 +84,7 @@
("verbose", "false"),
("overlord", "false"),
("blocking", "false"),
- ("type_sys", "smart"),
+ ("type_enc", "smart"),
("sound", "false"),
("relevance_thresholds", "0.45 0.85"),
("max_relevant", "smart"),
@@ -107,7 +107,7 @@
("no_slicing", "slicing")]
val params_for_minimize =
- ["debug", "verbose", "overlord", "type_sys", "sound", "max_mono_iters",
+ ["debug", "verbose", "overlord", "type_enc", "sound", "max_mono_iters",
"max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
"preplay_timeout"]
@@ -124,15 +124,15 @@
ss as _ :: _ => forall (is_prover_supported ctxt) ss
| _ => false
-(* "provers =" and "type_sys =" can be left out. The latter is a secret
+(* "provers =" and "type_enc =" can be left out. The latter is a secret
feature. *)
fun check_and_repair_raw_param ctxt (name, value) =
if is_known_raw_param name then
(name, value)
else if is_prover_list ctxt name andalso null value then
("provers", [name])
- else if can type_sys_from_string name andalso null value then
- ("type_sys", [name])
+ else if can type_enc_from_string name andalso null value then
+ ("type_enc", [name])
else
error ("Unknown parameter: " ^ quote name ^ ".")
@@ -264,12 +264,12 @@
lookup_bool "blocking"
val provers = lookup_string "provers" |> space_explode " "
|> mode = Auto_Try ? single o hd
- val type_sys =
+ val type_enc =
if mode = Auto_Try then
NONE
- else case lookup_string "type_sys" of
+ else case lookup_string "type_enc" of
"smart" => NONE
- | s => SOME (type_sys_from_string s)
+ | s => SOME (type_enc_from_string s)
val sound = mode = Auto_Try orelse lookup_bool "sound"
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
val max_relevant = lookup_option lookup_int "max_relevant"
@@ -288,7 +288,7 @@
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
provers = provers, relevance_thresholds = relevance_thresholds,
max_relevant = max_relevant, max_mono_iters = max_mono_iters,
- max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
+ max_new_mono_instances = max_new_mono_instances, type_enc = type_enc,
sound = sound, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slicing = slicing,
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 01 17:36:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 01 18:11:17 2011 +0200
@@ -47,7 +47,7 @@
fun print silent f = if silent then () else Output.urgent_message (f ())
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
- max_new_mono_instances, type_sys, isar_proof,
+ max_new_mono_instances, type_enc, isar_proof,
isar_shrink_factor, preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state facts =
let
@@ -59,7 +59,7 @@
val {goal, ...} = Proof.goal state
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
- provers = provers, type_sys = type_sys, sound = true,
+ provers = provers, type_enc = type_enc, sound = true,
relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
@@ -173,7 +173,7 @@
else
sublinear_minimize (do_test new_timeout) facts ([], result)
val _ = print silent (fn () => cat_lines
- ["Minimized to " ^ n_facts used_facts] ^
+ ["Minimized to " ^ n_facts (map fst min_facts)] ^
(case length (filter (curry (op =) Chained o snd o fst) min_facts) of
0 => ""
| n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".")
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 01 17:36:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 01 18:11:17 2011 +0200
@@ -10,7 +10,7 @@
sig
type failure = ATP_Proof.failure
type locality = ATP_Translate.locality
- type type_sys = ATP_Translate.type_sys
+ type type_enc = ATP_Translate.type_enc
type reconstructor = ATP_Reconstruct.reconstructor
type play = ATP_Reconstruct.play
type minimize_command = ATP_Reconstruct.minimize_command
@@ -24,7 +24,7 @@
overlord: bool,
blocking: bool,
provers: string list,
- type_sys: type_sys option,
+ type_enc: type_enc option,
sound: bool,
relevance_thresholds: real * real,
max_relevant: int option,
@@ -289,7 +289,7 @@
overlord: bool,
blocking: bool,
provers: string list,
- type_sys: type_sys option,
+ type_enc: type_enc option,
sound: bool,
relevance_thresholds: real * real,
max_relevant: int option,
@@ -407,11 +407,11 @@
in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
fun tac_for_reconstructor Metis =
- Metis_Tactics.metis_tac [Metis_Tactics.partial_type_sys]
+ Metis_Tactics.metis_tac [Metis_Tactics.partial_type_enc]
| tac_for_reconstructor Metis_Full_Types =
Metis_Tactics.metis_tac Metis_Tactics.full_type_syss
| tac_for_reconstructor Metis_No_Types =
- Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
+ Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
| tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
fun timed_reconstructor reconstructor debug timeout ths =
@@ -504,10 +504,10 @@
them each time. *)
val atp_important_message_keep_quotient = 10
-fun choose_format_and_type_sys best_type_sys formats type_sys_opt =
- (case type_sys_opt of
+fun choose_format_and_type_enc best_type_enc formats type_enc_opt =
+ (case type_enc_opt of
SOME ts => ts
- | NONE => type_sys_from_string best_type_sys)
+ | NONE => type_enc_from_string best_type_enc)
|> choose_format formats
val metis_minimize_max_time = seconds 2.0
@@ -527,10 +527,14 @@
#> Config.put Monomorph.max_new_instances max_new_instances
#> Config.put Monomorph.keep_partial_instances false
+(* Give the ATPs some slack before interrupting them the hard way. "z3_atp" on
+ Linux appears to be the only ATP that does not honor its time limit. *)
+val atp_timeout_slack = seconds 5.0
+
fun run_atp mode name
({exec, required_execs, arguments, proof_delims, known_failures,
conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
- ({debug, verbose, overlord, type_sys, sound, max_relevant,
+ ({debug, verbose, overlord, type_enc, sound, max_relevant,
max_mono_iters, max_new_mono_instances, isar_proof,
isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
minimize_command
@@ -598,21 +602,21 @@
|> maps (fn (name, rths) => map (pair name o snd) rths)
end
fun run_slice (slice, (time_frac, (complete,
- (best_max_relevant, best_type_sys, extra))))
+ (best_max_relevant, best_type_enc, extra))))
time_left =
let
val num_facts =
length facts |> is_none max_relevant
? Integer.min best_max_relevant
- val (format, type_sys) =
- choose_format_and_type_sys best_type_sys formats type_sys
- val fairly_sound = is_type_sys_fairly_sound type_sys
+ val (format, type_enc) =
+ choose_format_and_type_enc best_type_enc formats type_enc
+ val fairly_sound = is_type_enc_fairly_sound type_enc
val facts =
facts |> map untranslated_fact
|> not fairly_sound
? filter_out (is_dangerous_prop ctxt o prop_of o snd)
|> take num_facts
- |> polymorphism_of_type_sys type_sys <> Polymorphic
+ |> polymorphism_of_type_enc type_enc <> Polymorphic
? monomorphize_facts
|> map (apsnd prop_of)
val real_ms = Real.fromInt o Time.toMilliseconds
@@ -623,6 +627,7 @@
else
I))
* 0.001) |> seconds
+ val generous_slice_timeout = slice_timeout + atp_timeout_slack
val _ =
if debug then
quote name ^ " slice #" ^ string_of_int (slice + 1) ^
@@ -635,7 +640,7 @@
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_sys sound false (Config.get ctxt atp_readable_names)
+ type_enc sound false (Config.get ctxt atp_readable_names)
true hyp_ts concl_t facts
fun weights () = atp_problem_weights atp_problem
val full_proof = debug orelse isar_proof
@@ -657,25 +662,31 @@
conjecture_offset + 1
upto conjecture_offset + length hyp_ts + 1
|> map single
- val ((output, msecs), _) =
- bash_output command
+ val ((output, msecs), (atp_proof, outcome)) =
+ TimeLimit.timeLimit generous_slice_timeout bash_output command
|>> (if overlord then
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
else
I)
- |>> (if measure_run_time then split_time else rpair NONE)
- val (atp_proof, outcome) =
- extract_tstplike_proof_and_outcome verbose complete
- proof_delims known_failures output
- |>> atp_proof_from_tstplike_proof atp_problem output
- handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)
+ |> fst
+ |> (if measure_run_time then split_time else rpair NONE)
+ |> (fn accum as (output, _) =>
+ (accum,
+ extract_tstplike_proof_and_outcome verbose complete
+ proof_delims known_failures output
+ |>> atp_proof_from_tstplike_proof atp_problem output
+ handle UNRECOGNIZED_ATP_PROOF () =>
+ ([], SOME ProofIncomplete)))
+ handle TimeLimit.TimeOut =>
+ (("", SOME (Time.toMilliseconds slice_timeout)),
+ ([], SOME TimedOut))
val outcome =
case outcome of
NONE =>
used_facts_in_unsound_atp_proof ctxt
conjecture_shape facts_offset fact_names atp_proof
|> Option.map (fn facts =>
- UnsoundProof (is_type_sys_virtually_sound type_sys,
+ UnsoundProof (is_type_enc_virtually_sound type_enc,
facts |> sort string_ord))
| _ => outcome
in
@@ -779,20 +790,15 @@
these are sorted out properly in the SMT module, we have to interpret these
ourselves. *)
val remote_smt_failures =
- [(22, CantConnect),
- (2, NoLibwwwPerl)]
-val z3_wrapper_failures =
- [(11, InternalError),
- (12, InternalError),
- (13, InternalError)]
+ [(2, NoLibwwwPerl),
+ (22, CantConnect)]
val z3_failures =
[(101, OutOfResources),
(103, MalformedInput),
(110, MalformedInput)]
val unix_failures =
[(139, Crashed)]
-val smt_failures =
- remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
+val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
if is_real_cex then Unprovable else GaveUp
--- a/src/HOL/ex/atp_export.ML Fri Jul 01 17:36:25 2011 +0200
+++ b/src/HOL/ex/atp_export.ML Fri Jul 01 18:11:17 2011 +0200
@@ -149,17 +149,17 @@
if heading = factsN then (heading, order_facts ord lines) :: problem
else (heading, lines) :: order_problem_facts ord problem
-fun generate_tptp_inference_file_for_theory ctxt thy type_sys file_name =
+fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name =
let
val format = FOF
- val type_sys = type_sys |> type_sys_from_string
+ val type_enc = type_enc |> type_enc_from_string
val path = file_name |> Path.explode
val _ = File.write path ""
val facts = facts_of thy
val (atp_problem, _, _, _, _, _, _) =
facts
|> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
- |> prepare_atp_problem ctxt format Axiom Axiom type_sys true true false
+ |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true false
true [] @{prop False}
val atp_problem =
atp_problem