# HG changeset patch # User blanchet # Date 1305206958 -7200 # Node ID 626e292d22a7288a8accc2c5882d6515a963cf46 # Parent fe8ee8099b474849bb6fbdeebcf124831652e1f6 renamed type systems for more consistency diff -r fe8ee8099b47 -r 626e292d22a7 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Thu May 12 11:03:48 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Thu May 12 15:29:18 2011 +0200 @@ -460,7 +460,7 @@ 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}). +\textit{type\_sys} $=$ \textit{simple\_types} option (\S\ref{problem-encoding}). \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 @@ -571,85 +571,81 @@ following values: \begin{enum} -\item[$\bullet$] \textbf{\textit{simple}:} Use the prover's support for -many-typed first-order logic if available; otherwise, fall back on -\textit{mangled\_preds}. The problem is monomorphized, meaning that the -problem's type variables are instantiated with heuristically chosen ground -types. Monomorphization can simplify reasoning but also leads to larger fact -bases, which can slow down the ATPs. +%\item[$\bullet$] \textbf{\textit{poly\_types}:} Use the prover's support for +%polymorphic first-order logic if available; otherwise, fall back on +%\textit{poly\_preds}. -\item[$\bullet$] \textbf{\textit{preds}:} Types are encoded using a binary predicate +\item[$\bullet$] \textbf{\textit{poly\_preds}:} Types are encoded using a predicate $\mathit{has\_type\/}(\tau, t)$ that restricts the range of bound variables. Constants are annotated with their types, supplied as extra arguments, to resolve overloading. -\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with +\item[$\bullet$] \textbf{\textit{poly\_tags}:} Each term and subterm is tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$. -\item[$\bullet$] \textbf{\textit{mono\_preds}:} Similar to \textit{preds}, but -the problem is additionally monomorphized. +\item[$\bullet$] \textbf{\textit{poly\_args}:} +Like for the other sound encodings, constants are annotated with their types to +resolve overloading, but otherwise no type information is encoded. -\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but -the problem is additionally monomorphized. +\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to +the ATP. Types are simply erased. -\item[$\bullet$] \textbf{\textit{mangled\_preds}:} Similar to -\textit{mono\_preds}, but types are mangled in constant names instead of being -supplied as ground term arguments. The binary predicate -$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate -$\mathit{has\_type\_}\tau(t)$. +\item[$\bullet$] +\textbf{% +\textit{mono\_preds}, +\textit{mono\_tags}, +\textit{mono\_args}:} \\ +Similar to \textit{poly\_preds}, \textit{poly\_tags}, and \textit{poly\_args}, +respectively, but the problem is additionally monomorphized, meaning that type +variables are instantiated with heuristically chosen ground types. +Monomorphization can simplify reasoning but also leads to larger fact bases, +which can slow down the ATPs. -\item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to -\textit{mono\_tags}, but types are mangled in constant names instead of being -supplied as ground term arguments. The binary function +\item[$\bullet$] \textbf{\textit{simple\_types}:} Use the prover's support for +simply typed first-order logic if available; otherwise, fall back on +\textit{mangled\_preds}. The problem is monomorphized. + +\item[$\bullet$] +\textbf{% +\textit{mangled\_preds}, +\textit{mangled\_tags}, +\textit{mangled\_args}:} \\ +Similar to +\textit{mono\_preds}, \textit{mono\_tags}, and \textit{mono\_args}, +respectively but types are mangled in constant names instead of being supplied +as ground term arguments. The binary predicate $\mathit{has\_type\/}(\tau, t)$ +becomes a unary predicate $\mathit{has\_type\_}\tau(t)$, and the binary function $\mathit{type\_info\/}(\tau, t)$ becomes a unary function $\mathit{type\_info\_}\tau(t)$. \item[$\bullet$] \textbf{% -\textit{simple}?, -\textit{preds}?, -\textit{mono\_preds}?, -\textit{mangled\_preds}?, \\ -\textit{tags}?, -\textit{mono\_tags}?, -\textit{mangled\_tags}?:} \\ -The type systems \textit{simple}, \textit{preds}, \textit{mono\_preds}, -\textit{mangled\_preds}, \textit{tags}, \textit{mono\_tags}, and -\textit{mangled\_tags} are fully typed and virtually sound---i.e., except for -pathological cases, all found proofs are type-correct. For each of these, -Sledgehammer also provides a just-as-sound partially typed 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 ``top'' type.) +\textit{simple\_types}?, +\{\textit{poly},\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}?:} \\ +The type systems \textit{poly\_preds}, \textit{poly\_tags}, +\textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types}, +\textit{mangled\_preds}, and \textit{mangled\_tags} are fully typed and +virtually sound---except for pathological cases, all found proofs are +type-correct. For each of these, Sledgehammer also provides a just-as-sound +partially typed variant identified by a question mark (`{?}')\ that detects and +erases monotonic types, notably infinite types. (For \textit{simple\_types}, the +types are not actually erased but rather replaced by a shared uniform type.) \item[$\bullet$] \textbf{% -\textit{simple}!, -\textit{preds}!, -\textit{mono\_preds}!, -\textit{mangled\_preds}!, \\ -\textit{tags}!, -\textit{mono\_tags}!, -\textit{mangled\_tags}!:} \\ +\textit{simple\_types}!, +\{\textit{poly},\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}!:} \\ If the question mark (`{?}')\ is replaced by an exclamation mark (`{!}'),\ the translation erases all types except those that are clearly finite (e.g., \textit{bool}). This encoding is unsound. -\item[$\bullet$] \textbf{\textit{args}:} -Like for the other sound encodings, constants are annotated with their types to -resolve overloading, but otherwise no type information is encoded. This encoding -is hence less sound than the exclamation mark (`{!}')\ variants described above. - -\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to -the ATP. Types are simply erased. - \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled, uses a fully typed, virtually sound encoding; otherwise, uses any encoding. The actual encoding used depends on the ATP and should be the most efficient for that ATP. \end{enum} -For SMT solvers and ToFoF-E, the type system is always \textit{simple}. +For SMT solvers and ToFoF-E, the type system is always \textit{simple\_types}. \opdefault{monomorphize\_limit}{int}{\upshape 4} Specifies the maximum number of iterations for the monomorphization fixpoint diff -r fe8ee8099b47 -r 626e292d22a7 src/HOL/Metis_Examples/HO_Reas.thy --- a/src/HOL/Metis_Examples/HO_Reas.thy Thu May 12 11:03:48 2011 +0200 +++ b/src/HOL/Metis_Examples/HO_Reas.thy Thu May 12 15:29:18 2011 +0200 @@ -14,12 +14,12 @@ lemma "id True" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -27,12 +27,12 @@ lemma "\ id False" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -40,12 +40,12 @@ lemma "x = id True \ x = id False" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, 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_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 = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -53,12 +53,12 @@ lemma "id x = id True \ id x = id False" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -66,13 +66,13 @@ lemma "P True \ P False \ P x" sledgehammer [type_sys = erased, expect = none] () -sledgehammer [type_sys = args, expect = none] () -sledgehammer [type_sys = tags!, expect = some] () -sledgehammer [type_sys = tags?, expect = some] () -sledgehammer [type_sys = tags, expect = some] () -sledgehammer [type_sys = preds!, expect = some] () -sledgehammer [type_sys = preds?, expect = some] () -sledgehammer [type_sys = preds, expect = some] () +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_tags, expect = some] () +sledgehammer [type_sys = poly_preds!, expect = some] () +sledgehammer [type_sys = poly_preds?, expect = some] () +sledgehammer [type_sys = poly_preds, expect = some] () sledgehammer [type_sys = mangled_preds!, expect = some] () sledgehammer [type_sys = mangled_preds?, expect = some] () sledgehammer [type_sys = mangled_preds, expect = some] () @@ -80,12 +80,12 @@ lemma "id (\ a) \ \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -93,12 +93,12 @@ lemma "id (\ \ a) \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -106,12 +106,12 @@ lemma "id (\ (id (\ a))) \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -119,12 +119,12 @@ lemma "id (a \ b) \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -132,12 +132,12 @@ lemma "id (a \ b) \ id b" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -145,12 +145,12 @@ lemma "id a \ id b \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -158,12 +158,12 @@ lemma "id a \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -171,12 +171,12 @@ lemma "id b \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -184,12 +184,12 @@ lemma "id (\ a) \ id (\ b) \ id (\ (a \ b))" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -197,12 +197,12 @@ lemma "id (\ a) \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, 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_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 = poly_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) @@ -210,12 +210,12 @@ lemma "id (a \ b) \ id (\ a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) -sledgehammer [type_sys = tags!, expect = some] (id_apply) -sledgehammer [type_sys = tags?, expect = some] (id_apply) -sledgehammer [type_sys = tags, expect = some] (id_apply) -sledgehammer [type_sys = preds!, expect = some] (id_apply) -sledgehammer [type_sys = preds?, expect = some] (id_apply) -sledgehammer [type_sys = preds, 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_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 = poly_preds, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds!, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) diff -r fe8ee8099b47 -r 626e292d22a7 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu May 12 11:03:48 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu May 12 15:29:18 2011 +0200 @@ -23,6 +23,12 @@ * string fo_term option * string fo_term option type 'a problem = (string * 'a problem_line list) list +(* official TPTP syntax *) + val tptp_tff_type_of_types : string + val tptp_tff_bool_type : string + val tptp_tff_individual_type : string + val tptp_false : string + val tptp_true : string val timestamp : unit -> string val hashw : word * word -> word val hashw_string : string * word -> word @@ -55,6 +61,13 @@ * string fo_term option * string fo_term option type 'a problem = (string * 'a problem_line list) list +(* official TPTP syntax *) +val tptp_tff_type_of_types = "$tType" +val tptp_tff_bool_type = "$o" +val tptp_tff_individual_type = "$i" +val tptp_false = "$false" +val tptp_true = "$true" + val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now (* This hash function is recommended in Compilers: Principles, Techniques, and @@ -87,20 +100,21 @@ | string_for_connective AIf = "<=" | string_for_connective AIff = "<=>" | string_for_connective ANotIff = "<~>" -fun string_for_bound_var (s, NONE) = s - | string_for_bound_var (s, SOME ty) = s ^ " : " ^ ty -fun string_for_formula (AQuant (q, xs, phi)) = +fun string_for_bound_var Fof (s, _) = s + | string_for_bound_var Tff (s, ty) = + s ^ " : " ^ (ty |> the_default tptp_tff_individual_type) +fun string_for_formula format (AQuant (q, xs, phi)) = "(" ^ string_for_quantifier q ^ - "[" ^ commas (map string_for_bound_var xs) ^ "] : " ^ - string_for_formula phi ^ ")" - | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) = + "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^ + string_for_formula format phi ^ ")" + | string_for_formula _ (AConn (ANot, [AAtom (ATerm ("equal", ts))])) = space_implode " != " (map string_for_term ts) - | string_for_formula (AConn (c, [phi])) = - "(" ^ string_for_connective c ^ " " ^ string_for_formula phi ^ ")" - | string_for_formula (AConn (c, phis)) = + | string_for_formula format (AConn (c, [phi])) = + "(" ^ string_for_connective c ^ " " ^ string_for_formula format phi ^ ")" + | string_for_formula format (AConn (c, phis)) = "(" ^ space_implode (" " ^ string_for_connective c ^ " ") - (map string_for_formula phis) ^ ")" - | string_for_formula (AAtom tm) = string_for_term tm + (map (string_for_formula format) phis) ^ ")" + | string_for_formula _ (AAtom tm) = string_for_term tm fun string_for_symbol_type [] res_ty = res_ty | string_for_symbol_type [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty @@ -117,7 +131,7 @@ (Formula (ident, kind, phi, source, useful_info)) = (case format of Fof => "fof" | Tff => "tff") ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^ - string_for_formula phi ^ ")" ^ + string_for_formula format phi ^ ")" ^ (case (source, useful_info) of (NONE, NONE) => "" | (SOME tm, NONE) => ", " ^ string_for_term tm diff -r fe8ee8099b47 -r 626e292d22a7 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 11:03:48 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:18 2011 +0200 @@ -18,7 +18,7 @@ All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types datatype type_system = - Simple of type_level | + Simple_Types of type_level | Preds of polymorphism * type_level | Tags of polymorphism * type_level @@ -84,12 +84,6 @@ fun make_tff_type s = tff_type_prefix ^ ascii_of s -(* official TPTP syntax *) -val tptp_tff_type_of_types = "$tType" -val tptp_tff_bool_type = "$o" -val tptp_false = "$false" -val tptp_true = "$true" - (* Freshness almost guaranteed! *) val sledgehammer_weak_prefix = "Sledgehammer:" @@ -98,7 +92,7 @@ All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types datatype type_system = - Simple of type_level | + Simple_Types of type_level | Preds of polymorphism * type_level | Tags of polymorphism * type_level @@ -106,12 +100,15 @@ fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE fun type_sys_from_string s = - (case try (unprefix "mangled_") s of - SOME s => (Mangled_Monomorphic, s) + (case try (unprefix "poly_") s of + SOME s => (SOME Polymorphic, s) | NONE => case try (unprefix "mono_") s of - SOME s => (Monomorphic, s) - | NONE => (Polymorphic, s)) + SOME s => (SOME Monomorphic, s) + | NONE => + case try (unprefix "mangled_") s of + SOME s => (SOME Mangled_Monomorphic, s) + | NONE => (NONE, s)) ||> (fn s => (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *) case try_unsuffixes ["?", "_query"] s of @@ -120,22 +117,22 @@ case try_unsuffixes ["!", "_bang"] s of SOME s => (Finite_Types, s) | NONE => (All_Types, s)) - |> (fn (polymorphism, (level, core)) => - case (core, (polymorphism, level)) of - ("simple", (Polymorphic (* naja *), level)) => Simple level - | ("preds", extra) => Preds extra - | ("tags", extra) => Tags extra - | ("args", (_, All_Types (* naja *))) => - Preds (polymorphism, Const_Arg_Types) - | ("erased", (Polymorphic, All_Types (* naja *))) => - Preds (polymorphism, No_Types) + |> (fn (poly, (level, core)) => + case (core, (poly, level)) of + ("simple_types", (NONE, level)) => Simple_Types level + | ("preds", (SOME poly, level)) => Preds (poly, level) + | ("tags", (SOME poly, level)) => Tags (poly, level) + | ("args", (SOME poly, All_Types (* naja *))) => + Preds (poly, Const_Arg_Types) + | ("erased", (NONE, All_Types (* naja *))) => + Preds (Polymorphic, No_Types) | _ => error ("Unknown type system: " ^ quote s ^ ".")) -fun polymorphism_of_type_sys (Simple _) = Mangled_Monomorphic +fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic | polymorphism_of_type_sys (Preds (poly, _)) = poly | polymorphism_of_type_sys (Tags (poly, _)) = poly -fun level_of_type_sys (Simple level) = level +fun level_of_type_sys (Simple_Types level) = level | level_of_type_sys (Preds (_, level)) = level | level_of_type_sys (Tags (_, level)) = level @@ -830,7 +827,7 @@ end val do_bound_type = case type_sys of - Simple level => + Simple_Types level => SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level | _ => K NONE fun do_out_of_bound_type (s, T) = @@ -933,7 +930,7 @@ fun should_declare_sym type_sys pred_sym s = not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso not (String.isPrefix "$" s) andalso - ((case type_sys of Simple _ => true | _ => false) orelse not pred_sym) + ((case type_sys of Simple_Types _ => true | _ => false) orelse not pred_sym) fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) = let @@ -1029,7 +1026,7 @@ fun problem_lines_for_sym_decls ctxt conj_sym_kind nonmono_Ts type_sys (s, decls) = case type_sys of - Simple _ => map (decl_line_for_sym s) decls + Simple_Types _ => map (decl_line_for_sym s) decls | _ => let val decls = @@ -1129,7 +1126,7 @@ val problem = problem |> (case type_sys of - Simple _ => + Simple_Types _ => cons (type_declsN, map decl_line_for_tff_type (tff_types_in_problem problem)) | _ => I) diff -r fe8ee8099b47 -r 626e292d22a7 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 11:03:48 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 15:29:18 2011 +0200 @@ -346,14 +346,12 @@ val atp_important_message_keep_quotient = 10 val fallback_best_type_systems = - [Preds (Polymorphic, Const_Arg_Types), Simple All_Types] + [Preds (Polymorphic, Const_Arg_Types), Simple_Types All_Types] -fun adjust_dumb_type_sys formats (Simple level) = - if member (op =) formats Tff then (Tff, Simple level) +fun adjust_dumb_type_sys formats (Simple_Types level) = + if member (op =) formats Tff then (Tff, Simple_Types level) else (Fof, Preds (Mangled_Monomorphic, level)) - | adjust_dumb_type_sys formats type_sys = - if member (op =) formats Fof then (Fof, type_sys) - else (Tff, Simple (level_of_type_sys type_sys)) + | adjust_dumb_type_sys formats type_sys = (hd formats, type_sys) fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = adjust_dumb_type_sys formats type_sys | determine_format_and_type_sys best_type_systems formats