--- a/Admin/mira.py Sat Mar 26 12:01:40 2011 +0100
+++ b/Admin/mira.py Sat Mar 26 15:55:22 2011 +0100
@@ -13,7 +13,7 @@
# build and evaluation tools
-def prepare_isabelle_repository(loc_isabelle, loc_contrib, loc_dependency_heaps, parallelism = True):
+def prepare_isabelle_repository(loc_isabelle, loc_contrib, loc_dependency_heaps, parallelism = True, more_settings=''):
loc_contrib = path.expanduser(loc_contrib)
if not path.exists(loc_contrib):
@@ -49,7 +49,9 @@
ISABELLE_PATH="%s"
ISABELLE_USEDIR_OPTIONS="$ISABELLE_USEDIR_OPTIONS %s -t true -v true -d pdf -g true -i true"
-''' % (isabelle_path, parallelism_options)
+Z3_NON_COMMERCIAL="yes"
+%s
+''' % (isabelle_path, parallelism_options, more_settings)
writer = open(path.join(loc_isabelle, 'etc', 'settings'), 'a')
writer.write(extra_settings)
@@ -95,8 +97,8 @@
def isabelle_dependency_only(env, case, paths, dep_paths, playground):
- p = paths[0]
- result = path.join(p, 'heaps')
+ isabelle_home = paths[0]
+ result = path.join(isabelle_home, 'heaps')
os.makedirs(result)
for dep_path in dep_paths:
subprocess.check_call(['cp', '-R'] + glob(dep_path + '/*') + [result])
@@ -104,28 +106,41 @@
return (True, 'ok', {}, {}, result)
-def build_isabelle_image(subdir, base, img, env, case, paths, dep_paths, playground):
+def build_isabelle_image(subdir, base, img, env, case, paths, dep_paths, playground, more_settings=''):
- p = paths[0]
+ isabelle_home = paths[0]
dep_path = dep_paths[0]
- prepare_isabelle_repository(p, env.settings.contrib, dep_path)
- os.chdir(path.join(p, 'src', subdir))
+ prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, more_settings=more_settings)
+ os.chdir(path.join(isabelle_home, 'src', subdir))
- (return_code, log) = isabelle_usedir(env, p, '-b', base, img)
+ (return_code, log) = isabelle_usedir(env, isabelle_home, '-b', base, img)
- result = path.join(p, 'heaps')
+ result = path.join(isabelle_home, 'heaps')
return (return_code == 0, extract_isabelle_run_summary(log),
{'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
-def isabelle_makeall(env, case, paths, dep_paths, playground):
+def isabelle_make(subdir, env, case, paths, dep_paths, playground, more_settings='', target='all'):
+
+ isabelle_home = paths[0]
+ dep_path = dep_paths[0] if dep_paths else None
+ prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, more_settings=more_settings)
+ os.chdir(path.join(isabelle_home, subdir))
+
+ (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', '-k', target)
- p = paths[0]
- dep_path = dep_paths[0]
- prepare_isabelle_repository(p, env.settings.contrib, dep_path)
- os.chdir(p)
+ return (return_code == 0, extract_isabelle_run_summary(log),
+ {'timing': extract_isabelle_run_timing(log)}, {'log': log}, None)
+
+
+def isabelle_makeall(env, case, paths, dep_paths, playground, more_settings='', target='all', make_options=()):
- (return_code, log) = env.run_process('%s/bin/isabelle' % p, 'makeall', '-k', 'all')
+ isabelle_home = paths[0]
+ dep_path = dep_paths[0] if dep_paths else None
+ prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, more_settings=more_settings)
+ os.chdir(isabelle_home)
+
+ (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'makeall', '-k', *(make_options + (target,)))
return (return_code == 0, extract_isabelle_run_summary(log),
{'timing': extract_isabelle_run_timing(log)}, {'log': log}, None)
@@ -137,13 +152,13 @@
def Pure(env, case, paths, dep_paths, playground):
"""Pure image"""
- p = paths[0]
- prepare_isabelle_repository(p, env.settings.contrib, '')
- os.chdir(path.join(p, 'src', 'Pure'))
+ isabelle_home = paths[0]
+ prepare_isabelle_repository(isabelle_home, env.settings.contrib, '')
+ os.chdir(path.join(isabelle_home, 'src', 'Pure'))
- (return_code, log) = env.run_process('%s/bin/isabelle' % p, 'make', 'Pure')
+ (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', 'Pure')
- result = path.join(p, 'heaps')
+ result = path.join(isabelle_home, 'heaps')
return (return_code == 0, extract_isabelle_run_summary(log),
{'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
@@ -251,7 +266,7 @@
# Judgement Day configurations
-judgement_day_provers = ('e', 'spass', 'vampire')
+judgement_day_provers = ('e', 'spass', 'vampire', 'z3', 'cvc3', 'yices')
def judgement_day(base_path, theory, opts, env, case, paths, dep_paths, playground):
"""Judgement Day regression suite"""
@@ -314,3 +329,22 @@
"""Judgement Day regression suite SN"""
return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
+
+# SML/NJ
+
+smlnj_settings = '''
+ML_SYSTEM=smlnj
+ML_HOME="/home/smlnj/110.72/bin"
+ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
+ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
+'''
+
+@configuration(repos = [Isabelle], deps = [])
+def SML_HOL(*args):
+ """HOL image built with SML/NJ"""
+ return isabelle_make('src/HOL', *args, more_settings=smlnj_settings, target='HOL')
+
+@configuration(repos = [Isabelle], deps = [])
+def SML_makeall(*args):
+ """Makeall built with SML/NJ"""
+ return isabelle_makeall(*args, more_settings=smlnj_settings, make_options=('-j', '3'))
--- a/doc-src/Codegen/Thy/Further.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/doc-src/Codegen/Thy/Further.thy Sat Mar 26 15:55:22 2011 +0100
@@ -4,6 +4,107 @@
section {* Further issues \label{sec:further} *}
+subsection {* Specialities of the @{text Scala} target language \label{sec:scala} *}
+
+text {*
+ @{text Scala} deviates from languages of the ML family in a couple
+ of aspects; those which affect code generation mainly have to do with
+ @{text Scala}'s type system:
+
+ \begin{itemize}
+
+ \item @{text Scala} prefers tupled syntax over curried syntax.
+
+ \item @{text Scala} sacrifices Hindely-Milner type inference for a
+ much more rich type system with subtyping etc. For this reason
+ type arguments sometimes have to be given explicitly in square
+ brackets (mimicing System F syntax).
+
+ \item In contrast to @{text Haskell} where most specialities of
+ the type system are implemented using \emph{type classes},
+ @{text Scala} provides a sophisticated system of \emph{implicit
+ arguments}.
+
+ \end{itemize}
+
+ \noindent Concerning currying, the @{text Scala} serializer counts
+ arguments in code equations to determine how many arguments
+ shall be tupled; remaining arguments and abstractions in terms
+ rather than function definitions are always curried.
+
+ The second aspect affects user-defined adaptations with @{command
+ code_const}. For regular terms, the @{text Scala} serializer prints
+ all type arguments explicitly. For user-defined term adaptations
+ this is only possible for adaptations which take no arguments: here
+ the type arguments are just appended. Otherwise they are ignored;
+ hence user-defined adaptations for polymorphic constants have to be
+ designed very carefully to avoid ambiguity.
+
+ Isabelle's type classes are mapped onto @{text Scala} implicits; in
+ cases with diamonds in the subclass hierarchy this can lead to
+ ambiguities in the generated code:
+*}
+
+class %quote class1 =
+ fixes foo :: "'a \<Rightarrow> 'a"
+
+class %quote class2 = class1
+
+class %quote class3 = class1
+
+text {*
+ \noindent Here both @{class class2} and @{class class3} inherit from @{class class1},
+ forming the upper part of a diamond.
+*}
+
+definition %quote bar :: "'a :: {class2, class3} \<Rightarrow> 'a" where
+ "bar = foo"
+
+text {*
+ \noindent This yields the following code:
+*}
+
+text %quotetypewriter {*
+ @{code_stmts bar (Scala)}
+*}
+
+text {*
+ \noindent This code is rejected by the @{text Scala} compiler: in
+ the definition of @{text bar}, it is not clear from where to derive
+ the implicit argument for @{text foo}.
+
+ The solution to the problem is to close the diamond by a further
+ class with inherits from both @{class class2} and @{class class3}:
+*}
+
+class %quote class4 = class2 + class3
+
+text {*
+ \noindent Then the offending code equation can be restricted to
+ @{class class4}:
+*}
+
+lemma %quote [code]:
+ "(bar :: 'a::class4 \<Rightarrow> 'a) = foo"
+ by (simp only: bar_def)
+
+text {*
+ \noindent with the following code:
+*}
+
+text %quotetypewriter {*
+ @{code_stmts bar (Scala)}
+*}
+
+text {*
+ \noindent which exposes no ambiguity.
+
+ Since the preprocessor (cf.~\secref{sec:preproc}) propagates sort
+ constraints through a system of code equations, it is usually not
+ very difficult to identify the set of code equations which actually
+ needs more restricted sort constraints.
+*}
+
subsection {* Modules namespace *}
text {*
--- a/doc-src/Codegen/Thy/Introduction.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/doc-src/Codegen/Thy/Introduction.thy Sat Mar 26 15:55:22 2011 +0100
@@ -221,6 +221,9 @@
\item You may want to skim over the more technical sections
\secref{sec:adaptation} and \secref{sec:further}.
+ \item The target language Scala \cite{scala-overview-tech-report}
+ comes with some specialities discussed in \secref{sec:scala}.
+
\item For exhaustive syntax diagrams etc. you should visit the
Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}.
--- a/doc-src/Codegen/Thy/document/Further.tex Sat Mar 26 12:01:40 2011 +0100
+++ b/doc-src/Codegen/Thy/document/Further.tex Sat Mar 26 15:55:22 2011 +0100
@@ -22,6 +22,227 @@
}
\isamarkuptrue%
%
+\isamarkupsubsection{Specialities of the \isa{Scala} target language \label{sec:scala}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\isa{Scala} deviates from languages of the ML family in a couple
+ of aspects; those which affect code generation mainly have to do with
+ \isa{Scala}'s type system:
+
+ \begin{itemize}
+
+ \item \isa{Scala} prefers tupled syntax over curried syntax.
+
+ \item \isa{Scala} sacrifices Hindely-Milner type inference for a
+ much more rich type system with subtyping etc. For this reason
+ type arguments sometimes have to be given explicitly in square
+ brackets (mimicing System F syntax).
+
+ \item In contrast to \isa{Haskell} where most specialities of
+ the type system are implemented using \emph{type classes},
+ \isa{Scala} provides a sophisticated system of \emph{implicit
+ arguments}.
+
+ \end{itemize}
+
+ \noindent Concerning currying, the \isa{Scala} serializer counts
+ arguments in code equations to determine how many arguments
+ shall be tupled; remaining arguments and abstractions in terms
+ rather than function definitions are always curried.
+
+ The second aspect affects user-defined adaptations with \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}. For regular terms, the \isa{Scala} serializer prints
+ all type arguments explicitly. For user-defined term adaptations
+ this is only possible for adaptations which take no arguments: here
+ the type arguments are just appended. Otherwise they are ignored;
+ hence user-defined adaptations for polymorphic constants have to be
+ designed very carefully to avoid ambiguity.
+
+ Isabelle's type classes are mapped onto \isa{Scala} implicits; in
+ cases with diamonds in the subclass hierarchy this can lead to
+ ambiguities in the generated code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{class}\isamarkupfalse%
+\ class{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \isakeyword{fixes}\ foo\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isanewline
+\isacommand{class}\isamarkupfalse%
+\ class{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ class{\isadigit{1}}\isanewline
+\isanewline
+\isacommand{class}\isamarkupfalse%
+\ class{\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ class{\isadigit{1}}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Here both \isa{class{\isadigit{2}}} and \isa{class{\isadigit{3}}} inherit from \isa{class{\isadigit{1}}},
+ forming the upper part of a diamond.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ bar\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{7B}{\isacharbraceleft}}class{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ class{\isadigit{3}}{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}bar\ {\isaliteral{3D}{\isacharequal}}\ foo{\isaliteral{22}{\isachardoublequoteclose}}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This yields the following code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquotetypewriter
+%
+\endisadelimquotetypewriter
+%
+\isatagquotetypewriter
+%
+\begin{isamarkuptext}%
+object\ Example\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\isanewline
+trait\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}foo{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
+def\ foo{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}foo{\isaliteral{60}{\isacharbackquote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
+\isanewline
+trait\ class{\isadigit{2}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
+\isanewline
+trait\ class{\isadigit{3}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
+\isanewline
+def\ bar{\isaliteral{5B}{\isacharbrackleft}}A\ {\isaliteral{3A}{\isacharcolon}}\ class{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}\ class{\isadigit{3}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ foo{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
+\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{2A}{\isacharasterisk}}\ object\ Example\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\isanewline%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
+%
+\isadelimquotetypewriter
+%
+\endisadelimquotetypewriter
+%
+\begin{isamarkuptext}%
+\noindent This code is rejected by the \isa{Scala} compiler: in
+ the definition of \isa{bar}, it is not clear from where to derive
+ the implicit argument for \isa{foo}.
+
+ The solution to the problem is to close the diamond by a further
+ class with inherits from both \isa{class{\isadigit{2}}} and \isa{class{\isadigit{3}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{class}\isamarkupfalse%
+\ class{\isadigit{4}}\ {\isaliteral{3D}{\isacharequal}}\ class{\isadigit{2}}\ {\isaliteral{2B}{\isacharplus}}\ class{\isadigit{3}}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Then the offending code equation can be restricted to
+ \isa{class{\isadigit{4}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}bar\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}class{\isadigit{4}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ foo{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ only{\isaliteral{3A}{\isacharcolon}}\ bar{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent with the following code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquotetypewriter
+%
+\endisadelimquotetypewriter
+%
+\isatagquotetypewriter
+%
+\begin{isamarkuptext}%
+object\ Example\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\isanewline
+trait\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}foo{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
+def\ foo{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}foo{\isaliteral{60}{\isacharbackquote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
+\isanewline
+trait\ class{\isadigit{2}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
+\isanewline
+trait\ class{\isadigit{3}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
+\isanewline
+trait\ class{\isadigit{4}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ class{\isadigit{2}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ with\ class{\isadigit{3}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
+\isanewline
+def\ bar{\isaliteral{5B}{\isacharbrackleft}}A\ {\isaliteral{3A}{\isacharcolon}}\ class{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ foo{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
+\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{2A}{\isacharasterisk}}\ object\ Example\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\isanewline%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
+%
+\isadelimquotetypewriter
+%
+\endisadelimquotetypewriter
+%
+\begin{isamarkuptext}%
+\noindent which exposes no ambiguity.
+
+ Since the preprocessor (cf.~\secref{sec:preproc}) propagates sort
+ constraints through a system of code equations, it is usually not
+ very difficult to identify the set of code equations which actually
+ needs more restricted sort constraints.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Modules namespace%
}
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Sat Mar 26 12:01:40 2011 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Sat Mar 26 15:55:22 2011 +0100
@@ -546,6 +546,9 @@
\item You may want to skim over the more technical sections
\secref{sec:adaptation} and \secref{sec:further}.
+ \item The target language Scala \cite{scala-overview-tech-report}
+ comes with some specialities discussed in \secref{sec:scala}.
+
\item For exhaustive syntax diagrams etc. you should visit the
Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}.
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 26 15:55:22 2011 +0100
@@ -982,6 +982,9 @@
\item[@{text size}] specifies the maximum size of the search space
for assignment values.
+ \item[@{text eval}] takes a term or a list of terms and evaluates
+ these terms under the variable assignment found by quickcheck.
+
\item[@{text iterations}] sets how many sets of assignments are
generated for each particular size.
--- a/etc/components Sat Mar 26 12:01:40 2011 +0100
+++ b/etc/components Sat Mar 26 15:55:22 2011 +0100
@@ -17,4 +17,5 @@
src/HOL/Library/Sum_of_Squares
src/HOL/Tools/SMT
src/HOL/Tools/Predicate_Compile
+src/HOL/Tools/Nitpick
src/HOL/Mutabelle
--- a/src/HOL/Metis_Examples/Abstraction.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy Sat Mar 26 15:55:22 2011 +0100
@@ -9,6 +9,8 @@
imports Main "~~/src/HOL/Library/FuncSet"
begin
+declare [[metis_new_skolemizer]]
+
(*For Christoph Benzmueller*)
lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))";
by (metis One_nat_def less_Suc0 not_less0 not_less_eq numeral_2_eq_2)
--- a/src/HOL/Metis_Examples/BT.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Metis_Examples/BT.thy Sat Mar 26 15:55:22 2011 +0100
@@ -11,6 +11,8 @@
imports Main
begin
+declare [[metis_new_skolemizer]]
+
datatype 'a bt =
Lf
| Br 'a "'a bt" "'a bt"
--- a/src/HOL/Metis_Examples/BigO.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Metis_Examples/BigO.thy Sat Mar 26 15:55:22 2011 +0100
@@ -15,6 +15,8 @@
"~~/src/HOL/Library/Set_Algebras"
begin
+declare [[metis_new_skolemizer]]
+
subsection {* Definitions *}
definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where
--- a/src/HOL/Metis_Examples/HO_Reas.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Metis_Examples/HO_Reas.thy Sat Mar 26 15:55:22 2011 +0100
@@ -8,6 +8,8 @@
imports Main
begin
+declare [[metis_new_skolemizer]]
+
sledgehammer_params [prover = e, blocking, isar_proof, timeout = 10]
lemma "id True"
--- a/src/HOL/Metis_Examples/Message.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Sat Mar 26 15:55:22 2011 +0100
@@ -9,6 +9,8 @@
imports Main
begin
+declare [[metis_new_skolemizer]]
+
lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
by (metis Un_commute Un_left_absorb)
--- a/src/HOL/Metis_Examples/Tarski.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy Sat Mar 26 15:55:22 2011 +0100
@@ -11,6 +11,8 @@
imports Main "~~/src/HOL/Library/FuncSet"
begin
+declare [[metis_new_skolemizer]]
+
(*Many of these higher-order problems appear to be impossible using the
current linkup. They often seem to need either higher-order unification
or explicit reasoning about connectives such as conjunction. The numerous
--- a/src/HOL/Metis_Examples/TransClosure.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Metis_Examples/TransClosure.thy Sat Mar 26 15:55:22 2011 +0100
@@ -9,13 +9,15 @@
imports Main
begin
-types addr = nat
+declare [[metis_new_skolemizer]]
+
+type_synonym addr = nat
datatype val
= Unit -- "dummy result value of void expressions"
| Null -- "null reference"
| Bool bool -- "Boolean value"
- | Intg int -- "integer value"
+ | Intg int -- "integer value"
| Addr addr -- "addresses of objects in the heap"
consts R :: "(addr \<times> addr) set"
@@ -32,7 +34,7 @@
assume A4: "(b, c) \<in> R\<^sup>*"
have F1: "f c \<noteq> f b" using A2 A1 by metis
have F2: "\<forall>u. (b, u) \<in> R \<longrightarrow> (a, u) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
- have F3: "\<exists>x. (b, x R b c) \<in> R \<or> c = b" using A4 by (metis converse_rtranclE)
+ have F3: "\<exists>x. (b, x b c R) \<in> R \<or> c = b" using A4 by (metis converse_rtranclE)
have "c \<noteq> b" using F1 by metis
hence "\<exists>u. (b, u) \<in> R" using F3 by metis
thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis
@@ -53,7 +55,7 @@
thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 by (metis transitive_closure_trans(6))
qed
-lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk>
+lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk>
\<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
apply (erule_tac x = b in converse_rtranclE)
apply metis
--- a/src/HOL/Metis_Examples/set.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Metis_Examples/set.thy Sat Mar 26 15:55:22 2011 +0100
@@ -9,6 +9,8 @@
imports Main
begin
+declare [[metis_new_skolemizer]]
+
lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
(S(x,y) | ~S(y,z) | Q(Z,Z)) &
(Q(X,y) | ~Q(y,Z) | S(X,X))"
--- a/src/HOL/Mutabelle/etc/settings Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Mutabelle/etc/settings Sat Mar 26 15:55:22 2011 +0100
@@ -4,6 +4,5 @@
MUTABELLE_LOGIC=HOL
MUTABELLE_IMPORT_THEORY=Complex_Main
-MUTABELLE_OUTPUT_PATH=/tmp/mutabelle
ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools"
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Sat Mar 26 15:55:22 2011 +0100
@@ -8,6 +8,7 @@
PRG="$(basename "$0")"
function usage() {
+ [ -n "$MUTABELLE_OUTPUT_PATH" ] || MUTABELLE_OUTPUT_PATH="None"
echo
echo "Usage: isabelle $PRG [OPTIONS] THEORY"
echo
@@ -58,6 +59,11 @@
MUTABELLE_TEST_THEORY="$1"
+if [ -z "$MUTABELLE_OUTPUT_PATH" ]; then
+ MUTABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mutabelle$$"
+ PURGE_OUTPUT="true"
+fi
+
export MUTABELLE_OUTPUT_PATH
@@ -121,3 +127,9 @@
echo "nitpick : C: $(count "nitpick" "GenuineCex") N: $(count "nitpick" "NoCex") \
T: $(count "nitpick" "Timeout") E: $(count "nitpick" "Error")"
+
+## cleanup
+
+if [ -n "$PURGE_OUTPUT" ]; then
+ rm -rf "$MUTABELLE_OUTPUT_PATH"
+fi
--- a/src/HOL/Mutabelle/mutabelle.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Sat Mar 26 15:55:22 2011 +0100
@@ -507,11 +507,11 @@
fun qc_recursive usedthy [] insts sz qciter acc = rev acc
| qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter
(Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs));
- ((x, pretty (the_default [] (Option.map fst (fst (Quickcheck.test_term
+ ((x, pretty (the_default [] (Quickcheck.counterexample_of (Quickcheck.test_term
((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter
#> Config.put Quickcheck.tester (!testgen_name))
(ProofContext.init_global usedthy))
- (true, false) (preprocess usedthy insts x, [])))))) :: acc))
+ (true, false) (preprocess usedthy insts x, []))))) :: acc))
handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat Mar 26 15:55:22 2011 +0100
@@ -10,11 +10,11 @@
val take_random : int -> 'a list -> 'a list
datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
-type timing = (string * int) list
+type timings = (string * int) list
-type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
+type mtd = string * (theory -> term -> outcome * timings)
-type mutant_subentry = term * (string * (outcome * (timing * Quickcheck.report option))) list
+type mutant_subentry = term * (string * (outcome * timings)) list
type detailed_entry = string * bool * term * mutant_subentry list
type subentry = string * int * int * int * int * int * int
@@ -103,11 +103,11 @@
| string_of_outcome Solved = "Solved"
| string_of_outcome Unsolved = "Unsolved"
-type timing = (string * int) list
+type timings = (string * int) list
-type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
+type mtd = string * (theory -> term -> outcome * timings)
-type mutant_subentry = term * (string * (outcome * (timing * Quickcheck.report option))) list
+type mutant_subentry = term * (string * (outcome * timings)) list
type detailed_entry = string * bool * term * mutant_subentry list
type subentry = string * int * int * int * int * int * int
@@ -121,12 +121,16 @@
fun invoke_quickcheck change_options quickcheck_generator thy t =
TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit))
(fn _ =>
- case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
- (false, false) [] [(t, [])] of
- (NONE, _) => (NoCex, ([], NONE))
- | (SOME _, _) => (GenuineCex, ([], NONE))) ()
+ let
+ val [result] = Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
+ (false, false) [] [(t, [])]
+ in
+ case Quickcheck.counterexample_of result of
+ NONE => (NoCex, Quickcheck.timings_of result)
+ | SOME _ => (GenuineCex, Quickcheck.timings_of result)
+ end) ()
handle TimeLimit.TimeOut =>
- (Timeout, ([("timelimit", Real.floor (!Auto_Tools.time_limit))], NONE))
+ (Timeout, [("timelimit", Real.floor (!Auto_Tools.time_limit))])
fun quickcheck_mtd change_options quickcheck_generator =
("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
@@ -138,8 +142,8 @@
val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
in
case Solve_Direct.solve_direct false state of
- (true, _) => (Solved, ([], NONE))
- | (false, _) => (Unsolved, ([], NONE))
+ (true, _) => (Solved, [])
+ | (false, _) => (Unsolved, [])
end
val solve_direct_mtd = ("solve_direct", invoke_solve_direct)
@@ -151,8 +155,8 @@
val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
in
case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of
- true => (Solved, ([], NONE))
- | false => (Unsolved, ([], NONE))
+ true => (Solved, [])
+ | false => (Unsolved, [])
end
val try_mtd = ("try", invoke_try)
@@ -198,7 +202,7 @@
(Nitpick_Isar.default_params thy []) false 1 1 1 [] [] t
val _ = Output.urgent_message ("Nitpick: " ^ res)
in
- rpair ([], NONE) (case res of
+ (rpair []) (case res of
"genuine" => GenuineCex
| "likely_genuine" => GenuineCex
| "potential" => PotentialCex
@@ -347,13 +351,13 @@
fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
let
val _ = Output.urgent_message ("Invoking " ^ mtd_name)
- val (res, (timing, reports)) = (*cpu_time "total time"
+ val (res, timing) = (*cpu_time "total time"
(fn () => *)case try (invoke_mtd thy) t of
- SOME (res, (timing, reports)) => (res, (timing, reports))
+ SOME (res, timing) => (res, timing)
| NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
- (Error, ([], NONE)))
+ (Error, []))
val _ = Output.urgent_message (" Done")
- in (res, (timing, reports)) end
+ in (res, timing) end
(* theory -> term list -> mtd -> subentry *)
@@ -431,14 +435,14 @@
fun string_of_mutant_subentry' thy thm_name (t, results) =
let
- fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
+ (* fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
satisfied_assms = s, positive_concl_tests = p}) =
"errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p
fun string_of_reports NONE = ""
| string_of_reports (SOME reports) =
cat_lines (map (fn (size, [report]) =>
- "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))
- fun string_of_mtd_result (mtd_name, (outcome, (timing, reports))) =
+ "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))*)
+ fun string_of_mtd_result (mtd_name, (outcome, timing)) =
mtd_name ^ ": " ^ string_of_outcome outcome
(*" with time " ^ " (" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"*)
(*^ "\n" ^ string_of_reports reports*)
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy Sat Mar 26 15:55:22 2011 +0100
@@ -291,6 +291,12 @@
thm big_step.equation
+definition list :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a list" where
+ "list s n = map s [0 ..< n]"
+
+values [expected "{[42, (43 :: nat)]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
+
+
subsection {* CCS *}
text{* This example formalizes finite CCS processes without communication or
--- a/src/HOL/Quickcheck_Exhaustive.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Sat Mar 26 15:55:22 2011 +0100
@@ -91,19 +91,17 @@
fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
where
- "exhaustive_fun' f i d = (if i > 1 then
- exhaustive (%(a, at). exhaustive (%(b, bt).
- exhaustive_fun' (%(g, gt). f (g(a := b),
- (%_. let T1 = (Typerep.typerep (TYPE('a)));
- T2 = (Typerep.typerep (TYPE('b)))
- in
- Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
- (Code_Evaluation.Const (STR ''Fun.fun_upd'')
- (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
- Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
- (gt ())) (at ())) (bt ())))) (i - 1) d) d) d
- else (if i > 0 then
- exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
+ "exhaustive_fun' f i d = (exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
+ orelse (if i > 1 then
+ exhaustive_fun' (%(g, gt). exhaustive (%(a, at). exhaustive (%(b, bt).
+ f (g(a := b),
+ (%_. let A = (Typerep.typerep (TYPE('a)));
+ B = (Typerep.typerep (TYPE('b)));
+ fun = (%T U. Typerep.Typerep (STR ''fun'') [T, U])
+ in
+ Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
+ (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
+ (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
where
--- a/src/HOL/RealDef.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/RealDef.thy Sat Mar 26 15:55:22 2011 +0100
@@ -1115,7 +1115,7 @@
declare [[coercion "int"]]
declare [[coercion_map map]]
-declare [[coercion_map "% f g h . g o h o f"]]
+declare [[coercion_map "% f g h x. g (h (f x))"]]
declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
lemma real_eq_of_nat: "real = of_nat"
--- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Mar 26 15:55:22 2011 +0100
@@ -8,6 +8,8 @@
signature MESON_CLAUSIFY =
sig
val new_skolem_var_prefix : string
+ val new_nonskolem_var_prefix : string
+ val is_zapped_var_name : string -> bool
val extensionalize_theorem : thm -> thm
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
@@ -26,6 +28,10 @@
val new_skolem_var_prefix = "MesonSK"
val new_nonskolem_var_prefix = "MesonV"
+fun is_zapped_var_name s =
+ exists (fn prefix => String.isPrefix prefix s)
+ [new_skolem_var_prefix, new_nonskolem_var_prefix]
+
(**** Transformation of Elimination Rules into First-Order Formulas****)
val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
@@ -327,13 +333,20 @@
val no_choice = null choice_ths
val discharger_th =
th |> (if no_choice then pull_out else skolemize choice_ths)
- val fully_skolemized_t =
+ val zapped_th =
discharger_th |> prop_of |> rename_bound_vars_to_be_zapped ax_no
|> (if no_choice then
Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> cprop_of
else
cterm_of thy)
- |> zap true |> Drule.export_without_context
+ |> zap true
+ val fixes =
+ Term.add_free_names (prop_of zapped_th) []
+ |> filter is_zapped_var_name
+ val ctxt' = ctxt |> Variable.add_fixes_direct fixes (*###*)
+ val fully_skolemized_t =
+ zapped_th
+ |> singleton (Variable.export ctxt' ctxt)
|> cprop_of |> Thm.dest_equals |> snd |> term_of
in
if exists_subterm (fn Var ((s, _), _) =>
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Mar 26 15:55:22 2011 +0100
@@ -46,7 +46,7 @@
fun types_of [] = []
| types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
- if String.isPrefix "_" a then
+ if String.isPrefix metis_generated_var_prefix a then
(*Variable generated by Metis, which might have been a type variable.*)
TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
else types_of tts
@@ -585,50 +585,6 @@
fun term_instantiate thy = cterm_instantiate o map (pairself (cterm_of thy))
-(* In principle, it should be sufficient to apply "assume_tac" to unify the
- conclusion with one of the premises. However, in practice, this is unreliable
- because of the mildly higher-order nature of the unification problems.
- Typical constraints are of the form
- "?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x",
- where the nonvariables are goal parameters. *)
-(* FIXME: ### try Pattern.match instead *)
-fun unify_first_prem_with_concl thy i th =
- let
- val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
- val prem = goal |> Logic.strip_assums_hyp |> hd
- val concl = goal |> Logic.strip_assums_concl
- fun pair_untyped_aconv (t1, t2) (u1, u2) =
- untyped_aconv t1 u1 andalso untyped_aconv t2 u2
- fun add_terms tp inst =
- if exists (pair_untyped_aconv tp) inst then inst
- else tp :: map (apsnd (subst_atomic [tp])) inst
- fun is_flex t =
- case strip_comb t of
- (Var _, args) => forall is_Bound args
- | _ => false
- fun unify_flex flex rigid =
- case strip_comb flex of
- (Var (z as (_, T)), args) =>
- add_terms (Var z,
- fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
- | _ => raise TERM ("unify_flex: expected flex", [flex])
- fun unify_potential_flex comb atom =
- if is_flex comb then unify_flex comb atom
- else if is_Var atom then add_terms (atom, comb)
- else raise TERM ("unify_terms", [comb, atom])
- fun unify_terms (t, u) =
- case (t, u) of
- (t1 $ t2, u1 $ u2) =>
- if is_flex t then unify_flex t u
- else if is_flex u then unify_flex u t
- else fold unify_terms [(t1, u1), (t2, u2)]
- | (_ $ _, _) => unify_potential_flex t u
- | (_, _ $ _) => unify_potential_flex u t
- | (Var _, _) => add_terms (t, u)
- | (_, Var _) => add_terms (u, t)
- | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
- in th |> term_instantiate thy (unify_terms (prem, concl) []) end
-
val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
fun copy_prems_tac [] ns i =
@@ -656,9 +612,10 @@
| repair t = t
val t' = t |> repair |> fold (curry absdummy) (map snd params)
fun do_instantiate th =
- let val var = Term.add_vars (prop_of th) [] |> the_single in
- th |> term_instantiate thy [(Var var, t')]
- end
+ let
+ val var = Term.add_vars (prop_of th) []
+ |> the_single
+ in th |> term_instantiate thy [(Var var, t')] end
in
(etac @{thm allE} i
THEN rotate_tac ~1 i
@@ -729,22 +686,13 @@
else
let
val thy = ProofContext.theory_of ctxt
- (* distinguish variables with same name but different types *)
- (* ### FIXME: needed? *)
- val prems_imp_false' =
- prems_imp_false |> try (forall_intr_vars #> gen_all)
- |> the_default prems_imp_false
- val prems_imp_false =
- if prop_of prems_imp_false aconv prop_of prems_imp_false' then
- prems_imp_false
- else
- prems_imp_false'
fun match_term p =
let
val (tyenv, tenv) =
Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
val tsubst =
tenv |> Vartab.dest
+ |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
|> sort (cluster_ord
o pairself (Meson_Clausify.cluster_of_zapped_var_name
o fst o fst))
@@ -762,15 +710,13 @@
| _ => raise TERM ("discharge_skolem_premises: Malformed premise",
[prem])
fun cluster_of_var_name skolem s =
- let
- val ((ax_no, (cluster_no, _)), skolem') =
- Meson_Clausify.cluster_of_zapped_var_name s
- in
+ case try Meson_Clausify.cluster_of_zapped_var_name s of
+ NONE => NONE
+ | SOME ((ax_no, (cluster_no, _)), skolem') =>
if skolem' = skolem andalso cluster_no > 0 then
SOME (ax_no, cluster_no)
else
NONE
- end
fun clusters_in_term skolem t =
Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
fun deps_for_term_subst (var, t) =
@@ -796,6 +742,7 @@
\\"Hilbert_Choice\"."
val outer_param_names =
[] |> fold (Term.add_var_names o snd) (map_filter I axioms)
+ |> filter (Meson_Clausify.is_zapped_var_name o fst)
|> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
|> filter (fn (((_, (cluster_no, _)), skolem), _) =>
cluster_no = 0 andalso skolem)
@@ -831,7 +778,6 @@
THEN ALLGOALS (fn i =>
rtac @{thm Meson.skolem_COMBK_I} i
THEN rotate_tac (rotation_for_subgoal i) i
-(* THEN PRIMITIVE (unify_first_prem_with_concl thy i) ### FIXME: needed? *)
THEN assume_tac i)))
handle ERROR _ =>
error ("Cannot replay Metis proof in Isabelle:\n\
--- a/src/HOL/Tools/Metis/metis_translate.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML Sat Mar 26 15:55:22 2011 +0100
@@ -36,6 +36,7 @@
tfrees: type_literal list,
old_skolems: (string * term) list}
+ val metis_generated_var_prefix : string
val type_tag_name : string
val bound_var_prefix : string
val schematic_var_prefix: string
@@ -83,6 +84,8 @@
structure Metis_Translate : METIS_TRANSLATE =
struct
+val metis_generated_var_prefix = "_"
+
val type_tag_name = "ti"
val bound_var_prefix = "B_"
@@ -802,7 +805,7 @@
val helper_ths =
metis_helpers
|> filter (is_used o fst)
- |> maps (fn (c, (needs_full_types, thms)) =>
+ |> maps (fn (_, (needs_full_types, thms)) =>
if needs_full_types andalso mode <> FT then []
else map prepare_helper thms)
in lmap |> fold (add_thm false) helper_ths end
--- a/src/HOL/Tools/Nitpick/lib/Tools/nitrox Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Tools/Nitpick/lib/Tools/nitrox Sat Mar 26 15:55:22 2011 +0100
@@ -16,6 +16,8 @@
exit 1
}
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
for FILE in "$@"
do
(echo "theory Nitrox_Run imports Main begin" &&
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Mar 26 15:55:22 2011 +0100
@@ -39,7 +39,7 @@
val write_program : logic_program -> string
val run : (Time.time * prolog_system) -> logic_program -> (string * prol_term list) -> string list -> int option -> prol_term list list
- val quickcheck : Proof.context -> term -> int -> term list option * Quickcheck.report option
+ val quickcheck : Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
val trace : bool Unsynchronized.ref
@@ -1009,12 +1009,13 @@
(* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *)
-fun quickcheck ctxt t size =
+fun quickcheck ctxt (t, []) size =
let
+ val t' = list_abs_free (Term.add_frees t [], t)
val options = code_options_of (ProofContext.theory_of ctxt)
val thy = Theory.copy (ProofContext.theory_of ctxt)
val ((((full_constname, constT), vs'), intro), thy1) =
- Predicate_Compile_Aux.define_quickcheck_predicate t thy
+ Predicate_Compile_Aux.define_quickcheck_predicate t' thy
val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
val thy3 = Predicate_Compile.preprocess preprocess_options (Const (full_constname, constT)) thy2
val ctxt' = ProofContext.init_global thy3
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Mar 26 15:55:22 2011 +0100
@@ -130,12 +130,12 @@
fun preprocess options t thy =
let
val _ = print_step options "Fetching definitions from theory..."
- val gr = cond_timeit (!Quickcheck.timing) "preprocess-obtain graph"
+ val gr = cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-obtain graph"
(fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
|> (fn gr => Term_Graph.subgraph (member (op =) (Term_Graph.all_succs gr [t])) gr))
val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
in
- cond_timeit (!Quickcheck.timing) "preprocess-process"
+ cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-process"
(fn () => (fold_rev (preprocess_strong_conn_constnames options gr)
(Term_Graph.strong_conn gr) thy))
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Mar 26 15:55:22 2011 +0100
@@ -51,6 +51,7 @@
val is_predT : typ -> bool
val is_constrt : theory -> term -> bool
val is_constr : Proof.context -> string -> bool
+ val strip_ex : term -> (string * typ) list * term
val focus_ex : term -> Name.context -> ((string * typ) list * term) * Name.context
val strip_all : term -> (string * typ) list * term
val strip_intro_concl : thm -> term * term list
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Mar 26 15:55:22 2011 +0100
@@ -1363,7 +1363,7 @@
val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt,
modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt)
val ((moded_clauses, needs_random), errors) =
- cond_timeit (!Quickcheck.timing) "Infering modes"
+ cond_timeit (Config.get ctxt Quickcheck.timing) "Infering modes"
(fn _ => infer_modes mode_analysis_options
options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy
@@ -1373,19 +1373,19 @@
val _ = print_modes options modes
val _ = print_step options "Defining executable functions..."
val thy'' =
- cond_timeit (!Quickcheck.timing) "Defining executable functions..."
+ cond_timeit (Config.get ctxt Quickcheck.timing) "Defining executable functions..."
(fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'
|> Theory.checkpoint)
val ctxt'' = ProofContext.init_global thy''
val _ = print_step options "Compiling equations..."
val compiled_terms =
- cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
+ cond_timeit (Config.get ctxt Quickcheck.timing) "Compiling equations...." (fn _ =>
compile_preds options
(#comp_modifiers (dest_steps steps)) ctxt'' all_vs param_vs preds moded_clauses)
val _ = print_compiled_terms options ctxt'' compiled_terms
val _ = print_step options "Proving equations..."
val result_thms =
- cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
+ cond_timeit (Config.get ctxt Quickcheck.timing) "Proving equations...." (fn _ =>
#prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
(maps_modes result_thms)
@@ -1393,7 +1393,7 @@
val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
(fn thm => Context.mapping (Code.add_eqn thm) I))))
val thy''' =
- cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
+ cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." (fn _ =>
fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
[((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
[attrib thy ])] thy))
@@ -1683,21 +1683,47 @@
);
val put_lseq_random_stats_result = Lseq_Random_Stats_Result.put;
+fun dest_special_compr t =
+ let
+ val (inner_t, T_compr) = case t of (Const (@{const_name Collect}, _) $ Abs (x, T, t)) => (t, T)
+ | _ => raise TERM ("dest_special_compr", [t])
+ val (Ts, conj) = apfst (map snd) (Predicate_Compile_Aux.strip_ex inner_t)
+ val [eq, body] = HOLogic.dest_conj conj
+ val rhs = case HOLogic.dest_eq eq of
+ (Bound i, rhs) => if i = length Ts then rhs else raise TERM ("dest_special_compr", [t])
+ | _ => raise TERM ("dest_special_compr", [t])
+ val output_names = Name.variant_list (fold Term.add_free_names [rhs, body] [])
+ (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
+ val output_frees = map2 (curry Free) output_names (rev Ts)
+ val body = subst_bounds (output_frees, body)
+ val output = subst_bounds (output_frees, rhs)
+ in
+ (((body, output), T_compr), output_names)
+ end
+
+fun dest_general_compr ctxt t_compr =
+ let
+ val inner_t = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
+ | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
+ val (body, Ts, fp) = HOLogic.strip_psplits inner_t;
+ val output_names = Name.variant_list (Term.add_free_names body [])
+ (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
+ val output_frees = map2 (curry Free) output_names (rev Ts)
+ val body = subst_bounds (output_frees, body)
+ val T_compr = HOLogic.mk_ptupleT fp Ts
+ val output = HOLogic.mk_ptuple fp T_compr (rev output_frees)
+ in
+ (((body, output), T_compr), output_names)
+ end
+
(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
fun analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes
(compilation, arguments) t_compr =
let
val compfuns = Comp_Mod.compfuns comp_modifiers
val all_modes_of = all_modes_of compilation
- val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
- | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
- val (body, Ts, fp) = HOLogic.strip_psplits split;
- val output_names = Name.variant_list (Term.add_free_names body [])
- (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
- val output_frees = map2 (curry Free) output_names (rev Ts)
- val body = subst_bounds (output_frees, body)
- val T_compr = HOLogic.mk_ptupleT fp Ts
- val output_tuple = HOLogic.mk_ptuple fp T_compr (rev output_frees)
+ val (((body, output), T_compr), output_names) =
+ case try dest_special_compr t_compr of SOME r => r | NONE => dest_general_compr ctxt t_compr
val (pred as Const (name, T), all_args) =
case strip_comb body of
(Const (name, T), all_args) => (Const (name, T), all_args)
@@ -1752,7 +1778,7 @@
val t_pred = compile_expr comp_modifiers ctxt
(body, deriv) [] additional_arguments;
val T_pred = dest_predT compfuns (fastype_of t_pred)
- val arrange = HOLogic.tupled_lambda (HOLogic.mk_tuple outargs) output_tuple
+ val arrange = HOLogic.tupled_lambda (HOLogic.mk_tuple outargs) output
in
if null outargs then t_pred else mk_map compfuns T_pred T_compr arrange t_pred
end
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Sat Mar 26 15:55:22 2011 +0100
@@ -101,10 +101,10 @@
depthCheck :: Testable a => Int -> a -> IO ();
depthCheck d p =
- (refute $ run (const p) 0 d) >>= (\n -> putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d);
+ (refute $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
smallCheck :: Testable a => Int -> a -> IO ();
-smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE");
+smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
}
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Mar 26 15:55:22 2011 +0100
@@ -136,7 +136,7 @@
val main = "module Main where {\n\n" ^
"import Narrowing_Engine;\n" ^
"import Code;\n\n" ^
- "main = Narrowing_Engine.smallCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
+ "main = Narrowing_Engine.depthCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
"}\n"
val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
(unprefix "module Code where {" code)
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Mar 26 15:55:22 2011 +0100
@@ -98,7 +98,7 @@
fun map_Abs f t =
case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t])
fun process_args t = case strip_comb t of
- (c as Const (_, _), ts) => list_comb (c, map post_process_term ts)
+ (c as Const (_, _), ts) => list_comb (c, map post_process_term ts)
in
case fastype_of t of
Type (@{type_name fun}, [T1, T2]) =>
@@ -108,15 +108,15 @@
|> (case T2 of
@{typ bool} =>
(case t of
- Abs(_, _, @{const True}) => fst #> rev #> make_set T1
- | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1
+ Abs(_, _, @{const False}) => fst #> rev #> make_set T1
+ | Abs(_, _, @{const True}) => fst #> rev #> make_coset T1
| Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
| _ => raise TERM ("post_process_term", [t]))
| Type (@{type_name option}, _) =>
(case t of
- Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2
+ Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2
| Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
- | _ => make_fun_upds T1 T2)
+ | _ => make_fun_upds T1 T2)
| _ => make_fun_upds T1 T2)
| NONE => process_args t)
| _ => process_args t
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Mar 26 15:55:22 2011 +0100
@@ -495,7 +495,9 @@
val smt_failures =
remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
-fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
+
+fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
+ if is_real_cex then Unprovable else IncompleteUnprovable
| failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
| failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
(case AList.lookup (op =) smt_failures code of
--- a/src/HOL/ex/Quickcheck_Examples.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Sat Mar 26 15:55:22 2011 +0100
@@ -36,6 +36,7 @@
theorem "rev (xs @ ys) = rev ys @ rev xs"
quickcheck[random, expect = no_counterexample]
quickcheck[exhaustive, expect = no_counterexample]
+ quickcheck[exhaustive, size = 1000, timeout = 0.1]
oops
theorem "rev (xs @ ys) = rev xs @ rev ys"
--- a/src/HOL/ex/TPTP.thy Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/ex/TPTP.thy Sat Mar 26 15:55:22 2011 +0100
@@ -14,6 +14,10 @@
declare [[smt_oracle]]
+refute_params [maxtime = 10000, no_assms, expect = genuine]
+nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms,
+ expect = genuine]
+
ML {* Proofterm.proofs := 0 *}
ML {*
--- a/src/HOL/ex/sledgehammer_tactics.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/HOL/ex/sledgehammer_tactics.ML Sat Mar 26 15:55:22 2011 +0100
@@ -50,11 +50,6 @@
handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
end
-fun to_period ("." :: _) = []
- | to_period ("" :: ss) = to_period ss
- | to_period (s :: ss) = s :: to_period ss
- | to_period [] = []
-
val atp = "e" (* or "vampire" or "spass" etc. *)
fun thms_of_name ctxt name =
--- a/src/Tools/Metis/Makefile Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/Makefile Sat Mar 26 15:55:22 2011 +0100
@@ -179,6 +179,12 @@
POLYML_OPTS =
+ifeq ($(shell uname), Darwin)
+ POLYML_LINK_OPTS = -lpolymain -lpolyml -segprot POLY rwx rwx
+else
+ POLYML_LINK_OPTS = -lpolymain -lpolyml
+endif
+
POLYML_SRC = \
src/Random.sig src/Random.sml \
src/Portable.sig src/PortablePolyml.sml \
@@ -205,7 +211,7 @@
@echo '*****************************'
@echo
@echo $@
- cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) -lpolymain -lpolyml
+ cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) $(POLYML_LINK_OPTS)
@echo
.PHONY: polyml-info
--- a/src/Tools/Metis/metis.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/metis.ML Sat Mar 26 15:55:22 2011 +0100
@@ -555,7 +555,20 @@
(* Tracing. *)
(* ------------------------------------------------------------------------- *)
-val tracePrint = Unsynchronized.ref TextIO.print;
+local
+ val traceOut = TextIO.stdOut;
+
+ fun tracePrintFn mesg =
+ let
+ val () = TextIO.output (traceOut,mesg)
+
+ val () = TextIO.flushOut traceOut
+ in
+ ()
+ end;
+in
+ val tracePrint = Unsynchronized.ref tracePrintFn;
+end;
fun trace mesg = !tracePrint mesg;
@@ -759,7 +772,7 @@
case l of
[] =>
let
- val acc = if null row then acc else rev row :: acc
+ val acc = if List.null row then acc else rev row :: acc
in
rev acc
end
@@ -788,9 +801,9 @@
local
fun fstEq ((x,_),(y,_)) = x = y;
- fun collapse l = (fst (hd l), map snd l);
-in
- fun groupsByFst l = map collapse (groupsBy fstEq l);
+ fun collapse l = (fst (hd l), List.map snd l);
+in
+ fun groupsByFst l = List.map collapse (groupsBy fstEq l);
end;
fun groupsOf n =
@@ -935,10 +948,10 @@
| sortMap f cmp xs =
let
fun ncmp ((m,_),(n,_)) = cmp (m,n)
- val nxs = map (fn x => (f x, x)) xs
+ val nxs = List.map (fn x => (f x, x)) xs
val nys = sort ncmp nxs
in
- map snd nys
+ List.map snd nys
end;
(* ------------------------------------------------------------------------- *)
@@ -1146,7 +1159,7 @@
fun alignColumn {leftAlign,padChar} column =
let
- val (n,_) = maximum Int.compare (map size column)
+ val (n,_) = maximum Int.compare (List.map size column)
fun pad entry row =
let
@@ -1162,13 +1175,18 @@
local
fun alignTab aligns rows =
case aligns of
- [] => map (K "") rows
- | [{leftAlign = true, padChar = #" "}] => map hd rows
+ [] => List.map (K "") rows
+ | [{leftAlign = true, padChar = #" "}] => List.map hd rows
| align :: aligns =>
- alignColumn align (map hd rows) (alignTab aligns (map tl rows));
+ let
+ val col = List.map hd rows
+ and cols = alignTab aligns (List.map tl rows)
+ in
+ alignColumn align col cols
+ end;
in
fun alignTable aligns rows =
- if null rows then [] else alignTab aligns rows;
+ if List.null rows then [] else alignTab aligns rows;
end;
(* ------------------------------------------------------------------------- *)
@@ -6599,6 +6617,8 @@
val ppPpstream : ppstream pp
+val ppException : exn pp
+
(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators. *)
(* ------------------------------------------------------------------------- *)
@@ -6689,7 +6709,7 @@
fun escapeString {escape} =
let
- val escapeMap = map (fn c => (c, "\\" ^ str c)) escape
+ val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape
fun escapeChar c =
case c of
@@ -6858,7 +6878,7 @@
let
val Block {indent = _, style = _, size, chunks} = block
- val empty = null chunks
+ val empty = List.null chunks
(*BasicDebug
val _ = not empty orelse size = 0 orelse
@@ -7430,7 +7450,7 @@
lines
end
in
- if null lines then Metis_Stream.Nil else Metis_Stream.singleton lines
+ if List.null lines then Metis_Stream.Nil else Metis_Stream.singleton lines
end;
in
fun execute {lineLength} =
@@ -7503,7 +7523,7 @@
fun ppOpA a = sequence (ppOp' s) (ppA a)
in
fn [] => skip
- | h :: t => blockProgram Inconsistent 0 (ppA h :: map ppOpA t)
+ | h :: t => blockProgram Inconsistent 0 (ppA h :: List.map ppOpA t)
end;
fun ppOpStream' s ppA =
@@ -7655,6 +7675,8 @@
val ppPpstream = ppStream ppStep;
+fun ppException e = ppString (exnMessage e);
+
(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators. *)
(* ------------------------------------------------------------------------- *)
@@ -8258,9 +8280,9 @@
val newNames : int -> name list
-val variantPrime : (name -> bool) -> name -> name
-
-val variantNum : (name -> bool) -> name -> name
+val variantPrime : {avoid : name -> bool} -> name -> name
+
+val variantNum : {avoid : name -> bool} -> name -> name
(* ------------------------------------------------------------------------- *)
(* Parsing and pretty printing. *)
@@ -8311,22 +8333,21 @@
in
fun newName () = numName (newInt ());
- fun newNames n = map numName (newInts n);
-end;
-
-fun variantPrime acceptable =
- let
- fun variant n = if acceptable n then n else variant (n ^ "'")
+ fun newNames n = List.map numName (newInts n);
+end;
+
+fun variantPrime {avoid} =
+ let
+ fun variant n = if avoid n then variant (n ^ "'") else n
in
variant
end;
local
- fun isDigitOrPrime #"'" = true
- | isDigitOrPrime c = Char.isDigit c;
-in
- fun variantNum acceptable n =
- if acceptable n then n
+ fun isDigitOrPrime c = c = #"'" orelse Char.isDigit c;
+in
+ fun variantNum {avoid} n =
+ if not (avoid n) then n
else
let
val n = stripSuffix isDigitOrPrime n
@@ -8335,7 +8356,7 @@
let
val n_i = n ^ Int.toString i
in
- if acceptable n_i then n_i else variant (i + 1)
+ if avoid n_i then variant (i + 1) else n_i
end
in
variant 0
@@ -8878,7 +8899,7 @@
in
case tm of
Var _ => subtms rest acc
- | Fn (_,args) => subtms (map f (enumerate args) @ rest) acc
+ | Fn (_,args) => subtms (List.map f (enumerate args) @ rest) acc
end;
in
fun subterms tm = subtms [([],tm)] [];
@@ -8909,7 +8930,7 @@
Var _ => search rest
| Fn (_,a) =>
let
- val subtms = map (fn (i,t) => (i :: path, t)) (enumerate a)
+ val subtms = List.map (fn (i,t) => (i :: path, t)) (enumerate a)
in
search (subtms @ rest)
end
@@ -8949,14 +8970,14 @@
fun newVar () = Var (Metis_Name.newName ());
-fun newVars n = map Var (Metis_Name.newNames n);
-
-local
- fun avoidAcceptable avoid n = not (Metis_NameSet.member n avoid);
-in
- fun variantPrime avoid = Metis_Name.variantPrime (avoidAcceptable avoid);
-
- fun variantNum avoid = Metis_Name.variantNum (avoidAcceptable avoid);
+fun newVars n = List.map Var (Metis_Name.newNames n);
+
+local
+ fun avoid av n = Metis_NameSet.member n av;
+in
+ fun variantPrime av = Metis_Name.variantPrime {avoid = avoid av};
+
+ fun variantNum av = Metis_Name.variantNum {avoid = avoid av};
end;
(* ------------------------------------------------------------------------- *)
@@ -9028,7 +9049,7 @@
val acc = (rev path, tm) :: acc
- val rest = map f (enumerate args) @ rest
+ val rest = List.map f (enumerate args) @ rest
in
subtms rest acc
end;
@@ -9237,7 +9258,7 @@
and basic bv (Var v) = varName bv v
| basic bv (Fn (f,args)) =
Metis_Print.blockProgram Metis_Print.Inconsistent 2
- (functionName bv f :: map (functionArgument bv) args)
+ (functionName bv f :: List.map (functionArgument bv) args)
and customBracket bv tm =
case destBrack tm of
@@ -9249,13 +9270,13 @@
NONE => term bv tm
| SOME (q,v,vs,tm) =>
let
- val bv = Metis_StringSet.addList bv (map Metis_Name.toString (v :: vs))
+ val bv = Metis_StringSet.addList bv (List.map Metis_Name.toString (v :: vs))
in
Metis_Print.program
[Metis_Print.ppString q,
varName bv v,
Metis_Print.program
- (map (Metis_Print.sequence (Metis_Print.addBreak 1) o varName bv) vs),
+ (List.map (Metis_Print.sequence (Metis_Print.addBreak 1) o varName bv) vs),
Metis_Print.ppString ".",
Metis_Print.addBreak 1,
innerQuant bv tm]
@@ -9342,9 +9363,9 @@
and neg = !negation
and bracks = ("(",")") :: !brackets
- val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
-
- val bTokens = map #2 bracks @ map #3 bracks
+ val bracks = List.map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
+
+ val bTokens = List.map #2 bracks @ List.map #3 bracks
fun possibleVarName "" = false
| possibleVarName s = isAlphaNum (String.sub (s,0))
@@ -9399,8 +9420,8 @@
in
var ||
const ||
- first (map bracket bracks) ||
- first (map quantifier quants)
+ first (List.map bracket bracks) ||
+ first (List.map quantifier quants)
end tokens
and molecule bv tokens =
@@ -10057,7 +10078,7 @@
fun subterms ((_,tms) : atom) =
let
- fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Metis_Term.subterms tm) @ l
+ fun f ((n,tm),l) = List.map (fn (p,s) => (n :: p, s)) (Metis_Term.subterms tm) @ l
in
List.foldl f [] (enumerate tms)
end;
@@ -10941,9 +10962,9 @@
fun promote (Metis_Term.Var v) = Metis_Atom (v,[])
| promote (Metis_Term.Fn (f,tms)) =
- if Metis_Name.equal f truthName andalso null tms then
+ if Metis_Name.equal f truthName andalso List.null tms then
True
- else if Metis_Name.equal f falsityName andalso null tms then
+ else if Metis_Name.equal f falsityName andalso List.null tms then
False
else if Metis_Name.toString f = !Metis_Term.negation andalso length tms = 1 then
Not (promote (hd tms))
@@ -10973,7 +10994,7 @@
local
fun add_asms asms goal =
- if null asms then goal else Imp (listMkConj (rev asms), goal);
+ if List.null asms then goal else Imp (listMkConj (rev asms), goal);
fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
@@ -10987,7 +11008,7 @@
| (true, Imp (f1,f2)) => split (f1 :: asms) true f2
| (true, Iff (f1,f2)) =>
split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
- | (true, Forall (v,f)) => map (add_var_asms asms v) (split [] true f)
+ | (true, Forall (v,f)) => List.map (add_var_asms asms v) (split [] true f)
(* Negative splittables *)
| (false,False) => []
| (false, Not f) => split asms true f
@@ -10997,7 +11018,7 @@
| (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2
| (false, Iff (f1,f2)) =>
split (f1 :: asms) false f2 @ split (f2 :: asms) false f1
- | (false, Exists (v,f)) => map (add_var_asms asms v) (split [] false f)
+ | (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f)
(* Unsplittables *)
| _ => [add_asms asms (if pol then fm else Not fm)];
in
@@ -11750,7 +11771,7 @@
local
fun toFormula th =
Metis_Formula.listMkDisj
- (map Metis_Literal.toFormula (Metis_LiteralSet.toList (clause th)));
+ (List.map Metis_Literal.toFormula (Metis_LiteralSet.toList (clause th)));
in
fun pp th =
Metis_Print.blockProgram Metis_Print.Inconsistent 3
@@ -12057,7 +12078,7 @@
Metis_Print.blockProgram Metis_Print.Consistent 0
[Metis_Print.ppString "START OF PROOF",
Metis_Print.addNewline,
- Metis_Print.program (map ppStep prf),
+ Metis_Print.program (List.map ppStep prf),
Metis_Print.ppString "END OF PROOF"]
end
(*MetisDebug
@@ -12737,6 +12758,7 @@
else
let
val sub = Metis_Subst.fromList [(xVarName,x),(yVarName,y)]
+
val symTh = Metis_Thm.subst sub symmetry
in
Metis_Thm.resolve lit th symTh
@@ -12750,9 +12772,9 @@
type equation = (Metis_Term.term * Metis_Term.term) * Metis_Thm.thm;
-fun ppEquation (_,th) = Metis_Thm.pp th;
-
-fun equationToString x = Metis_Print.toString ppEquation x;
+fun ppEquation ((_,th) : equation) = Metis_Thm.pp th;
+
+val equationToString = Metis_Print.toString ppEquation;
fun equationLiteral (t_u,th) =
let
@@ -12866,7 +12888,7 @@
fun rewrConv (eqn as ((x,y), eqTh)) path tm =
if Metis_Term.equal x y then allConv tm
- else if null path then (y,eqTh)
+ else if List.null path then (y,eqTh)
else
let
val reflTh = Metis_Thm.refl tm
@@ -12905,7 +12927,7 @@
fun subtermsConv _ (tm as Metis_Term.Var _) = allConv tm
| subtermsConv conv (tm as Metis_Term.Fn (_,a)) =
- everyConv (map (subtermConv conv) (interval 0 (length a))) tm;
+ everyConv (List.map (subtermConv conv) (interval 0 (length a))) tm;
(* ------------------------------------------------------------------------- *)
(* Applying a conversion to every subterm, with some traversal strategy. *)
@@ -13019,7 +13041,7 @@
fun allArgumentsLiterule conv lit =
everyLiterule
- (map (argumentLiterule conv) (interval 0 (Metis_Literal.arity lit))) lit;
+ (List.map (argumentLiterule conv) (interval 0 (Metis_Literal.arity lit))) lit;
(* ------------------------------------------------------------------------- *)
(* A rule takes one theorem and either deduces another or raises an Error *)
@@ -13435,7 +13457,7 @@
let
fun fact sub = removeSym (Metis_Thm.subst sub th)
in
- map fact (factor' (Metis_Thm.clause th))
+ List.map fact (factor' (Metis_Thm.clause th))
end;
end
@@ -14453,11 +14475,11 @@
val deps = List.filter (isUnproved proved) pars
in
- if null deps then
+ if List.null deps then
let
val (fm,inf) = destThm th
- val fms = map (lookupProved proved) pars
+ val fms = List.map (lookupProved proved) pars
val acc = (fm,inf,fms) :: acc
@@ -14884,7 +14906,7 @@
let
val cls = proveCnf [mkAxiom fm]
in
- map fst cls
+ List.map fst cls
end;
end
@@ -15441,7 +15463,7 @@
local
fun mkEntry tag (na,n) = (tag,na,n);
- fun mkList tag m = map (mkEntry tag) (Metis_NameArityMap.toList m);
+ fun mkList tag m = List.map (mkEntry tag) (Metis_NameArityMap.toList m);
fun ppEntry (tag,source_arity,target) =
Metis_Print.blockProgram Metis_Print.Inconsistent 2
@@ -15461,7 +15483,7 @@
| entry :: entries =>
Metis_Print.blockProgram Metis_Print.Consistent 0
(ppEntry entry ::
- map (Metis_Print.sequence Metis_Print.addNewline o ppEntry) entries)
+ List.map (Metis_Print.sequence Metis_Print.addNewline o ppEntry) entries)
end;
end;
@@ -15507,7 +15529,7 @@
end;
val projectionFixed =
- unionListFixed (map arityProjectionFixed projectionList);
+ unionListFixed (List.map arityProjectionFixed projectionList);
(* Arithmetic *)
@@ -15610,7 +15632,7 @@
let
val fns =
Metis_NameArityMap.fromList
- (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
+ (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
numeralList @
[((addName,2), fixed2 addFn),
((divName,2), fixed2 divFn),
@@ -15710,7 +15732,7 @@
let
val fns =
Metis_NameArityMap.fromList
- (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
+ (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
numeralList @
[((addName,2), fixed2 addFn),
((divName,2), fixed2 divFn),
@@ -16202,13 +16224,13 @@
fun interpret tm =
case destTerm tm of
Metis_Term.Var v => getValuation V v
- | Metis_Term.Fn (f,tms) => interpretFunction M (f, map interpret tms)
+ | Metis_Term.Fn (f,tms) => interpretFunction M (f, List.map interpret tms)
in
interpret
end;
fun interpretAtom M V (r,tms) =
- interpretRelation M (r, map (interpretTerm M V) tms);
+ interpretRelation M (r, List.map (interpretTerm M V) tms);
fun interpretFormula M =
let
@@ -16325,7 +16347,7 @@
Metis_Term.Var v => (ModelVar, getValuation V v)
| Metis_Term.Fn (f,tms) =>
let
- val (tms,xs) = unzip (map modelTm tms)
+ val (tms,xs) = unzip (List.map modelTm tms)
in
(ModelFn (f,tms,xs), interpretFunction M (f,xs))
end
@@ -16408,7 +16430,7 @@
let
fun onTarget ys = interpretRelation M (rel,ys) = target
- val (tms,xs) = unzip (map (modelTerm M V) tms)
+ val (tms,xs) = unzip (List.map (modelTerm M V) tms)
val rel_xs = (rel,xs)
@@ -16424,7 +16446,7 @@
fun pertClause M V cl acc = Metis_LiteralSet.foldl (pertLiteral M V) acc cl;
fun pickPerturb M perts =
- if null perts then ()
+ if List.null perts then ()
else perturb M (List.nth (perts, Metis_Portable.randomInt (length perts)));
in
fun perturbTerm M V (tm,target) =
@@ -16564,16 +16586,16 @@
Metis_Formula.listMkDisj (Metis_LiteralSet.transform Metis_Literal.toFormula cl);
in
fun toFormula prob =
- Metis_Formula.listMkConj (map clauseToFormula (toClauses prob));
+ Metis_Formula.listMkConj (List.map clauseToFormula (toClauses prob));
fun toGoal {axioms,conjecture} =
let
val clToFm = Metis_Formula.generalize o clauseToFormula
- val clsToFm = Metis_Formula.listMkConj o map clToFm
+ val clsToFm = Metis_Formula.listMkConj o List.map clToFm
val fm = Metis_Formula.False
val fm =
- if null conjecture then fm
+ if List.null conjecture then fm
else Metis_Formula.Imp (clsToFm conjecture, fm)
val fm = Metis_Formula.Imp (clsToFm axioms, fm)
in
@@ -16641,7 +16663,7 @@
val horn =
if List.exists Metis_LiteralSet.null cls then Trivial
else if List.all (fn cl => Metis_LiteralSet.size cl = 1) cls then Unit
- else
+ else
let
fun pos cl = Metis_LiteralSet.count Metis_Literal.positive cl <= 1
fun neg cl = Metis_LiteralSet.count Metis_Literal.negative cl <= 1
@@ -16786,7 +16808,7 @@
fun equalFnQterm f1 f2 = compareFnQterm (f1,f2) = EQUAL;
fun termToQterm (Metis_Term.Var _) = Var
- | termToQterm (Metis_Term.Fn (f,l)) = Fn ((f, length l), map termToQterm l);
+ | termToQterm (Metis_Term.Fn (f,l)) = Fn ((f, length l), List.map termToQterm l);
local
fun qm [] = true
@@ -16852,7 +16874,7 @@
local
fun qtermToTerm Var = anonymousVar
- | qtermToTerm (Fn ((f,_),l)) = Metis_Term.Fn (f, map qtermToTerm l);
+ | qtermToTerm (Fn ((f,_),l)) = Metis_Term.Fn (f, List.map qtermToTerm l);
in
val ppQterm = Metis_Print.ppMap qtermToTerm Metis_Term.pp;
end;
@@ -17075,7 +17097,7 @@
fun fifoize ({fifo, ...} : parameters) l = if fifo then sort idwise l else l;
in
- fun finally parm l = map snd (fifoize parm l);
+ fun finally parm l = List.map snd (fifoize parm l);
end;
local
@@ -17966,7 +17988,7 @@
fun ppWeight (Weight (m,c)) =
let
val l = Metis_NameMap.toList m
- val l = map (fn (v,n) => (SOME v, n)) l
+ val l = List.map (fn (v,n) => (SOME v, n)) l
val l = if c = 0 then l else l @ [(NONE,c)]
in
ppWeightList l
@@ -18243,7 +18265,7 @@
fun ppField f ppA a =
Metis_Print.blockProgram Metis_Print.Inconsistent 2
- [Metis_Print.addString (f ^ " ="),
+ [Metis_Print.ppString (f ^ " ="),
Metis_Print.addBreak 1,
ppA a];
@@ -18269,24 +18291,24 @@
in
fun pp (Metis_Rewrite {known,redexes,subterms,waiting,...}) =
Metis_Print.blockProgram Metis_Print.Inconsistent 2
- [Metis_Print.addString "Metis_Rewrite",
+ [Metis_Print.ppString "Metis_Rewrite",
Metis_Print.addBreak 1,
Metis_Print.blockProgram Metis_Print.Inconsistent 1
- [Metis_Print.addString "{",
+ [Metis_Print.ppString "{",
ppKnown known,
(*MetisTrace5
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
ppRedexes redexes,
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
ppSubterms subterms,
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
ppWaiting waiting,
*)
Metis_Print.skip],
- Metis_Print.addString "}"]
+ Metis_Print.ppString "}"]
end;
*)
@@ -18349,10 +18371,15 @@
else
let
val Metis_Rewrite {order,redexes,subterms,waiting, ...} = rw
+
val ort = orderToOrient (order (fst eqn))
+
val known = Metis_IntMap.insert known (id,(eqn,ort))
+
val redexes = addRedexes id (eqn,ort) redexes
+
val waiting = Metis_IntSet.add waiting id
+
val rw =
Metis_Rewrite
{order = order, known = known, redexes = redexes,
@@ -18364,7 +18391,11 @@
rw
end;
-fun addList x = List.foldl (fn (eqn,rw) => add rw eqn) x;
+local
+ fun uncurriedAdd (eqn,rw) = add rw eqn;
+in
+ fun addList rw = List.foldl uncurriedAdd rw;
+end;
(* ------------------------------------------------------------------------- *)
(* Rewriting (the order must be a refinement of the rewrite order). *)
@@ -18797,7 +18828,7 @@
val ppResult = Metis_Print.ppPair pp (Metis_Print.ppList Metis_Print.ppInt)
val () = Metis_Print.trace ppResult "Metis_Rewrite.reduce': result" result
*)
- val ths = map (fn (id,((_,th),_)) => (id,th)) (Metis_IntMap.toList known')
+ val ths = List.map (fn (id,((_,th),_)) => (id,th)) (Metis_IntMap.toList known')
val _ =
not (List.exists (uncurry (thmReducible order known')) ths) orelse
raise Bug "Metis_Rewrite.reduce': not fully reduced"
@@ -18824,7 +18855,11 @@
end;
end;
-fun rewrite x = orderedRewrite (K (SOME GREATER)) x;
+local
+ val order : reductionOrder = K (SOME GREATER);
+in
+ val rewrite = orderedRewrite order;
+end;
end
@@ -19172,7 +19207,7 @@
val default : parameters =
{ordering = Metis_KnuthBendixOrder.default,
- orderLiterals = UnsignedLiteralOrder,
+ orderLiterals = PositiveLiteralOrder,
orderTerms = true};
fun mk info = Metis_Clause info
@@ -19364,7 +19399,7 @@
fun apply sub = new parameters (Metis_Thm.subst sub thm)
in
- map apply (Metis_Rule.factor' lits)
+ List.map apply (Metis_Rule.factor' lits)
end;
(*MetisTrace5
@@ -20409,8 +20444,8 @@
Metis_Clause.mk {parameters = clause, id = Metis_Clause.newId (), thm = th}
val active = empty parameters
- val (active,axioms) = factor active (map mk_clause axioms)
- val (active,conjecture) = factor active (map mk_clause conjecture)
+ val (active,axioms) = factor active (List.map mk_clause axioms)
+ val (active,conjecture) = factor active (List.map mk_clause conjecture)
in
(active, {axioms = axioms, conjecture = conjecture})
end;
@@ -20591,7 +20626,7 @@
val pp =
Metis_Print.ppMap
(fn Metis_Waiting {clauses,...} =>
- map (fn (w,(_,cl)) => (w, Metis_Clause.id cl, cl)) (Metis_Heap.toList clauses))
+ List.map (fn (w,(_,cl)) => (w, Metis_Clause.id cl, cl)) (Metis_Heap.toList clauses))
(Metis_Print.ppList (Metis_Print.ppTriple Metis_Print.ppReal Metis_Print.ppInt Metis_Clause.pp));
*)
@@ -20609,10 +20644,10 @@
(fvs,lits)
end;
-val mkModelClauses = map mkModelClause;
+val mkModelClauses = List.map mkModelClause;
fun perturbModel M cls =
- if null cls then K ()
+ if List.null cls then K ()
else
let
val N = {size = Metis_Model.size M}
@@ -20723,6 +20758,14 @@
val Metis_Waiting {parameters,clauses,models} = waiting
val {models = modelParameters, ...} = parameters
+(*MetisDebug
+ val _ = not (List.null cls) orelse
+ raise Bug "Metis_Waiting.add': null"
+
+ val _ = length mcls = length cls orelse
+ raise Bug "Metis_Waiting.add': different lengths"
+*)
+
val dist = dist + Math.ln (Real.fromInt (length cls))
fun addCl ((mcl,cl),acc) =
@@ -20739,22 +20782,23 @@
Metis_Waiting {parameters = parameters, clauses = clauses, models = models}
end;
-fun add waiting (_,[]) = waiting
- | add waiting (dist,cls) =
- let
+fun add waiting (dist,cls) =
+ if List.null cls then waiting
+ else
+ let
(*MetisTrace3
- val () = Metis_Print.trace pp "Metis_Waiting.add: waiting" waiting
- val () = Metis_Print.trace (Metis_Print.ppList Metis_Clause.pp) "Metis_Waiting.add: cls" cls
-*)
-
- val waiting = add' waiting dist (mkModelClauses cls) cls
+ val () = Metis_Print.trace pp "Metis_Waiting.add: waiting" waiting
+ val () = Metis_Print.trace (Metis_Print.ppList Metis_Clause.pp) "Metis_Waiting.add: cls" cls
+*)
+
+ val waiting = add' waiting dist (mkModelClauses cls) cls
(*MetisTrace3
- val () = Metis_Print.trace pp "Metis_Waiting.add: waiting" waiting
-*)
- in
- waiting
- end;
+ val () = Metis_Print.trace pp "Metis_Waiting.add: waiting" waiting
+*)
+ in
+ waiting
+ end;
local
fun cmp ((w1,_),(w2,_)) = Real.compare (w1,w2);
@@ -20763,7 +20807,7 @@
let
val {models = modelParameters, ...} = parameters
val clauses = Metis_Heap.new cmp
- and models = map (initialModel axioms conjecture) modelParameters
+ and models = List.map (initialModel axioms conjecture) modelParameters
in
Metis_Waiting {parameters = parameters, clauses = clauses, models = models}
end;
@@ -20775,8 +20819,17 @@
val waiting = empty parameters mAxioms mConjecture
in
- add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture)
- end;
+ if List.null axioms andalso List.null conjecture then waiting
+ else add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture)
+ end
+(*MetisDebug
+ handle e =>
+ let
+ val () = Metis_Print.trace Metis_Print.ppException "Metis_Waiting.new: exception" e
+ in
+ raise e
+ end;
+*)
end;
(* ------------------------------------------------------------------------- *)
@@ -20788,9 +20841,12 @@
else
let
val ((_,dcl),clauses) = Metis_Heap.remove clauses
+
val waiting =
Metis_Waiting
- {parameters = parameters, clauses = clauses, models = models}
+ {parameters = parameters,
+ clauses = clauses,
+ models = models}
in
SOME (dcl,waiting)
end;
@@ -20888,11 +20944,21 @@
fun new parameters ths =
let
val {active = activeParm, waiting = waitingParm} = parameters
+
val (active,cls) = Metis_Active.new activeParm ths (* cls = factored ths *)
+
val waiting = Metis_Waiting.new waitingParm cls
in
Metis_Resolution {parameters = parameters, active = active, waiting = waiting}
- end;
+ end
+(*MetisDebug
+ handle e =>
+ let
+ val () = Metis_Print.trace Metis_Print.ppException "Metis_Resolution.new: exception" e
+ in
+ raise e
+ end;
+*)
fun active (Metis_Resolution {active = a, ...}) = a;
@@ -20917,9 +20983,10 @@
Decided of decision
| Undecided of resolution;
-fun iterate resolution =
- let
- val Metis_Resolution {parameters,active,waiting} = resolution
+fun iterate res =
+ let
+ val Metis_Resolution {parameters,active,waiting} = res
+
(*MetisTrace2
val () = Metis_Print.trace Metis_Active.pp "Metis_Resolution.iterate: active" active
val () = Metis_Print.trace Metis_Waiting.pp "Metis_Resolution.iterate: waiting" waiting
@@ -20927,7 +20994,11 @@
in
case Metis_Waiting.remove waiting of
NONE =>
- Decided (Satisfiable (map Metis_Clause.thm (Metis_Active.saturation active)))
+ let
+ val sat = Satisfiable (List.map Metis_Clause.thm (Metis_Active.saturation active))
+ in
+ Decided sat
+ end
| SOME ((d,cl),waiting) =>
if Metis_Clause.isContradiction cl then
Decided (Contradiction (Metis_Clause.thm cl))
@@ -20937,18 +21008,23 @@
val () = Metis_Print.trace Metis_Clause.pp "Metis_Resolution.iterate: cl" cl
*)
val (active,cls) = Metis_Active.add active cl
+
val waiting = Metis_Waiting.add waiting (d,cls)
- in
- Undecided
- (Metis_Resolution
- {parameters = parameters, active = active, waiting = waiting})
- end
- end;
-
-fun loop resolution =
- case iterate resolution of
- Decided decision => decision
- | Undecided resolution => loop resolution;
+
+ val res =
+ Metis_Resolution
+ {parameters = parameters,
+ active = active,
+ waiting = waiting}
+ in
+ Undecided res
+ end
+ end;
+
+fun loop res =
+ case iterate res of
+ Decided dec => dec
+ | Undecided res => loop res;
end
;
--- a/src/Tools/Metis/src/Active.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Active.sml Sat Mar 26 15:55:22 2011 +0100
@@ -876,8 +876,8 @@
Clause.mk {parameters = clause, id = Clause.newId (), thm = th}
val active = empty parameters
- val (active,axioms) = factor active (map mk_clause axioms)
- val (active,conjecture) = factor active (map mk_clause conjecture)
+ val (active,axioms) = factor active (List.map mk_clause axioms)
+ val (active,conjecture) = factor active (List.map mk_clause conjecture)
in
(active, {axioms = axioms, conjecture = conjecture})
end;
--- a/src/Tools/Metis/src/Atom.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Atom.sml Sat Mar 26 15:55:22 2011 +0100
@@ -84,7 +84,7 @@
fun subterms ((_,tms) : atom) =
let
- fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Term.subterms tm) @ l
+ fun f ((n,tm),l) = List.map (fn (p,s) => (n :: p, s)) (Term.subterms tm) @ l
in
List.foldl f [] (enumerate tms)
end;
--- a/src/Tools/Metis/src/Clause.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Clause.sml Sat Mar 26 15:55:22 2011 +0100
@@ -69,7 +69,7 @@
val default : parameters =
{ordering = KnuthBendixOrder.default,
- orderLiterals = UnsignedLiteralOrder,
+ orderLiterals = PositiveLiteralOrder,
orderTerms = true};
fun mk info = Clause info
@@ -261,7 +261,7 @@
fun apply sub = new parameters (Thm.subst sub thm)
in
- map apply (Rule.factor' lits)
+ List.map apply (Rule.factor' lits)
end;
(*MetisTrace5
--- a/src/Tools/Metis/src/Formula.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Formula.sml Sat Mar 26 15:55:22 2011 +0100
@@ -517,9 +517,9 @@
fun promote (Term.Var v) = Atom (v,[])
| promote (Term.Fn (f,tms)) =
- if Name.equal f truthName andalso null tms then
+ if Name.equal f truthName andalso List.null tms then
True
- else if Name.equal f falsityName andalso null tms then
+ else if Name.equal f falsityName andalso List.null tms then
False
else if Name.toString f = !Term.negation andalso length tms = 1 then
Not (promote (hd tms))
@@ -549,7 +549,7 @@
local
fun add_asms asms goal =
- if null asms then goal else Imp (listMkConj (rev asms), goal);
+ if List.null asms then goal else Imp (listMkConj (rev asms), goal);
fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
@@ -563,7 +563,7 @@
| (true, Imp (f1,f2)) => split (f1 :: asms) true f2
| (true, Iff (f1,f2)) =>
split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
- | (true, Forall (v,f)) => map (add_var_asms asms v) (split [] true f)
+ | (true, Forall (v,f)) => List.map (add_var_asms asms v) (split [] true f)
(* Negative splittables *)
| (false,False) => []
| (false, Not f) => split asms true f
@@ -573,7 +573,7 @@
| (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2
| (false, Iff (f1,f2)) =>
split (f1 :: asms) false f2 @ split (f2 :: asms) false f1
- | (false, Exists (v,f)) => map (add_var_asms asms v) (split [] false f)
+ | (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f)
(* Unsplittables *)
| _ => [add_asms asms (if pol then fm else Not fm)];
in
--- a/src/Tools/Metis/src/KnuthBendixOrder.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sml Sat Mar 26 15:55:22 2011 +0100
@@ -113,7 +113,7 @@
fun ppWeight (Weight (m,c)) =
let
val l = NameMap.toList m
- val l = map (fn (v,n) => (SOME v, n)) l
+ val l = List.map (fn (v,n) => (SOME v, n)) l
val l = if c = 0 then l else l @ [(NONE,c)]
in
ppWeightList l
--- a/src/Tools/Metis/src/Model.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Model.sml Sat Mar 26 15:55:22 2011 +0100
@@ -268,7 +268,7 @@
local
fun mkEntry tag (na,n) = (tag,na,n);
- fun mkList tag m = map (mkEntry tag) (NameArityMap.toList m);
+ fun mkList tag m = List.map (mkEntry tag) (NameArityMap.toList m);
fun ppEntry (tag,source_arity,target) =
Print.blockProgram Print.Inconsistent 2
@@ -288,7 +288,7 @@
| entry :: entries =>
Print.blockProgram Print.Consistent 0
(ppEntry entry ::
- map (Print.sequence Print.addNewline o ppEntry) entries)
+ List.map (Print.sequence Print.addNewline o ppEntry) entries)
end;
end;
@@ -334,7 +334,7 @@
end;
val projectionFixed =
- unionListFixed (map arityProjectionFixed projectionList);
+ unionListFixed (List.map arityProjectionFixed projectionList);
(* Arithmetic *)
@@ -437,7 +437,7 @@
let
val fns =
NameArityMap.fromList
- (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
+ (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
numeralList @
[((addName,2), fixed2 addFn),
((divName,2), fixed2 divFn),
@@ -537,7 +537,7 @@
let
val fns =
NameArityMap.fromList
- (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
+ (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
numeralList @
[((addName,2), fixed2 addFn),
((divName,2), fixed2 divFn),
@@ -1029,13 +1029,13 @@
fun interpret tm =
case destTerm tm of
Term.Var v => getValuation V v
- | Term.Fn (f,tms) => interpretFunction M (f, map interpret tms)
+ | Term.Fn (f,tms) => interpretFunction M (f, List.map interpret tms)
in
interpret
end;
fun interpretAtom M V (r,tms) =
- interpretRelation M (r, map (interpretTerm M V) tms);
+ interpretRelation M (r, List.map (interpretTerm M V) tms);
fun interpretFormula M =
let
@@ -1152,7 +1152,7 @@
Term.Var v => (ModelVar, getValuation V v)
| Term.Fn (f,tms) =>
let
- val (tms,xs) = unzip (map modelTm tms)
+ val (tms,xs) = unzip (List.map modelTm tms)
in
(ModelFn (f,tms,xs), interpretFunction M (f,xs))
end
@@ -1235,7 +1235,7 @@
let
fun onTarget ys = interpretRelation M (rel,ys) = target
- val (tms,xs) = unzip (map (modelTerm M V) tms)
+ val (tms,xs) = unzip (List.map (modelTerm M V) tms)
val rel_xs = (rel,xs)
@@ -1251,7 +1251,7 @@
fun pertClause M V cl acc = LiteralSet.foldl (pertLiteral M V) acc cl;
fun pickPerturb M perts =
- if null perts then ()
+ if List.null perts then ()
else perturb M (List.nth (perts, Portable.randomInt (length perts)));
in
fun perturbTerm M V (tm,target) =
--- a/src/Tools/Metis/src/Name.sig Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Name.sig Sat Mar 26 15:55:22 2011 +0100
@@ -28,9 +28,9 @@
val newNames : int -> name list
-val variantPrime : (name -> bool) -> name -> name
+val variantPrime : {avoid : name -> bool} -> name -> name
-val variantNum : (name -> bool) -> name -> name
+val variantNum : {avoid : name -> bool} -> name -> name
(* ------------------------------------------------------------------------- *)
(* Parsing and pretty printing. *)
--- a/src/Tools/Metis/src/Name.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Name.sml Sat Mar 26 15:55:22 2011 +0100
@@ -33,22 +33,21 @@
in
fun newName () = numName (newInt ());
- fun newNames n = map numName (newInts n);
+ fun newNames n = List.map numName (newInts n);
end;
-fun variantPrime acceptable =
+fun variantPrime {avoid} =
let
- fun variant n = if acceptable n then n else variant (n ^ "'")
+ fun variant n = if avoid n then variant (n ^ "'") else n
in
variant
end;
local
- fun isDigitOrPrime #"'" = true
- | isDigitOrPrime c = Char.isDigit c;
+ fun isDigitOrPrime c = c = #"'" orelse Char.isDigit c;
in
- fun variantNum acceptable n =
- if acceptable n then n
+ fun variantNum {avoid} n =
+ if not (avoid n) then n
else
let
val n = stripSuffix isDigitOrPrime n
@@ -57,7 +56,7 @@
let
val n_i = n ^ Int.toString i
in
- if acceptable n_i then n_i else variant (i + 1)
+ if avoid n_i then variant (i + 1) else n_i
end
in
variant 0
--- a/src/Tools/Metis/src/Normalize.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Normalize.sml Sat Mar 26 15:55:22 2011 +0100
@@ -951,11 +951,11 @@
val deps = List.filter (isUnproved proved) pars
in
- if null deps then
+ if List.null deps then
let
val (fm,inf) = destThm th
- val fms = map (lookupProved proved) pars
+ val fms = List.map (lookupProved proved) pars
val acc = (fm,inf,fms) :: acc
@@ -1382,7 +1382,7 @@
let
val cls = proveCnf [mkAxiom fm]
in
- map fst cls
+ List.map fst cls
end;
end
--- a/src/Tools/Metis/src/Options.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Options.sml Sat Mar 26 15:55:22 2011 +0100
@@ -155,7 +155,7 @@
[{leftAlign = true, padChar = #"."},
{leftAlign = true, padChar = #" "}]
- val table = alignTable alignment (map listOpts options)
+ val table = alignTable alignment (List.map listOpts options)
in
header ^ join "\n" table ^ "\n" ^ footer
end;
--- a/src/Tools/Metis/src/PortableMosml.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/PortableMosml.sml Sat Mar 26 15:55:22 2011 +0100
@@ -67,7 +67,7 @@
val _ = catch_interrupt true;
(* ------------------------------------------------------------------------- *)
-(* Forcing fully qualified names of some key functions. *)
+(* Forcing fully qualified names of functions with generic names. *)
(* ------------------------------------------------------------------------- *)
(*BasicDebug
@@ -75,6 +75,8 @@
and foldl = ()
and foldr = ()
and implode = ()
+and map = ()
+and null = ()
and print = ();
*)
@@ -112,10 +114,18 @@
fun OS_Process_isSuccess s = s = OS.Process.success;
-fun String_concatWith s l =
- case l of
- [] => ""
- | h :: t => List.foldl (fn (x,y) => y ^ s ^ x) h t;
+fun String_concatWith s =
+ let
+ fun add (x,l) = s :: x :: l
+ in
+ fn [] => ""
+ | x :: xs =>
+ let
+ val xs = List.foldl add [] (rev xs)
+ in
+ String.concat (x :: xs)
+ end
+ end;
fun String_isSubstring p s =
let
--- a/src/Tools/Metis/src/Print.sig Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Print.sig Sat Mar 26 15:55:22 2011 +0100
@@ -131,6 +131,8 @@
val ppPpstream : ppstream pp
+val ppException : exn pp
+
(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Print.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Print.sml Sat Mar 26 15:55:22 2011 +0100
@@ -46,7 +46,7 @@
fun escapeString {escape} =
let
- val escapeMap = map (fn c => (c, "\\" ^ str c)) escape
+ val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape
fun escapeChar c =
case c of
@@ -215,7 +215,7 @@
let
val Block {indent = _, style = _, size, chunks} = block
- val empty = null chunks
+ val empty = List.null chunks
(*BasicDebug
val _ = not empty orelse size = 0 orelse
@@ -787,7 +787,7 @@
lines
end
in
- if null lines then Stream.Nil else Stream.singleton lines
+ if List.null lines then Stream.Nil else Stream.singleton lines
end;
in
fun execute {lineLength} =
@@ -860,7 +860,7 @@
fun ppOpA a = sequence (ppOp' s) (ppA a)
in
fn [] => skip
- | h :: t => blockProgram Inconsistent 0 (ppA h :: map ppOpA t)
+ | h :: t => blockProgram Inconsistent 0 (ppA h :: List.map ppOpA t)
end;
fun ppOpStream' s ppA =
@@ -1012,6 +1012,8 @@
val ppPpstream = ppStream ppStep;
+fun ppException e = ppString (exnMessage e);
+
(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Problem.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Problem.sml Sat Mar 26 15:55:22 2011 +0100
@@ -44,16 +44,16 @@
Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl);
in
fun toFormula prob =
- Formula.listMkConj (map clauseToFormula (toClauses prob));
+ Formula.listMkConj (List.map clauseToFormula (toClauses prob));
fun toGoal {axioms,conjecture} =
let
val clToFm = Formula.generalize o clauseToFormula
- val clsToFm = Formula.listMkConj o map clToFm
+ val clsToFm = Formula.listMkConj o List.map clToFm
val fm = Formula.False
val fm =
- if null conjecture then fm
+ if List.null conjecture then fm
else Formula.Imp (clsToFm conjecture, fm)
val fm = Formula.Imp (clsToFm axioms, fm)
in
@@ -121,7 +121,7 @@
val horn =
if List.exists LiteralSet.null cls then Trivial
else if List.all (fn cl => LiteralSet.size cl = 1) cls then Unit
- else
+ else
let
fun pos cl = LiteralSet.count Literal.positive cl <= 1
fun neg cl = LiteralSet.count Literal.negative cl <= 1
--- a/src/Tools/Metis/src/Proof.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Proof.sml Sat Mar 26 15:55:22 2011 +0100
@@ -133,7 +133,7 @@
Print.blockProgram Print.Consistent 0
[Print.ppString "START OF PROOF",
Print.addNewline,
- Print.program (map ppStep prf),
+ Print.program (List.map ppStep prf),
Print.ppString "END OF PROOF"]
end
(*MetisDebug
--- a/src/Tools/Metis/src/Resolution.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Resolution.sml Sat Mar 26 15:55:22 2011 +0100
@@ -33,11 +33,21 @@
fun new parameters ths =
let
val {active = activeParm, waiting = waitingParm} = parameters
+
val (active,cls) = Active.new activeParm ths (* cls = factored ths *)
+
val waiting = Waiting.new waitingParm cls
in
Resolution {parameters = parameters, active = active, waiting = waiting}
- end;
+ end
+(*MetisDebug
+ handle e =>
+ let
+ val () = Print.trace Print.ppException "Resolution.new: exception" e
+ in
+ raise e
+ end;
+*)
fun active (Resolution {active = a, ...}) = a;
@@ -62,9 +72,10 @@
Decided of decision
| Undecided of resolution;
-fun iterate resolution =
+fun iterate res =
let
- val Resolution {parameters,active,waiting} = resolution
+ val Resolution {parameters,active,waiting} = res
+
(*MetisTrace2
val () = Print.trace Active.pp "Resolution.iterate: active" active
val () = Print.trace Waiting.pp "Resolution.iterate: waiting" waiting
@@ -72,7 +83,11 @@
in
case Waiting.remove waiting of
NONE =>
- Decided (Satisfiable (map Clause.thm (Active.saturation active)))
+ let
+ val sat = Satisfiable (List.map Clause.thm (Active.saturation active))
+ in
+ Decided sat
+ end
| SOME ((d,cl),waiting) =>
if Clause.isContradiction cl then
Decided (Contradiction (Clause.thm cl))
@@ -82,17 +97,22 @@
val () = Print.trace Clause.pp "Resolution.iterate: cl" cl
*)
val (active,cls) = Active.add active cl
+
val waiting = Waiting.add waiting (d,cls)
+
+ val res =
+ Resolution
+ {parameters = parameters,
+ active = active,
+ waiting = waiting}
in
- Undecided
- (Resolution
- {parameters = parameters, active = active, waiting = waiting})
+ Undecided res
end
end;
-fun loop resolution =
- case iterate resolution of
- Decided decision => decision
- | Undecided resolution => loop resolution;
+fun loop res =
+ case iterate res of
+ Decided dec => dec
+ | Undecided res => loop res;
end
--- a/src/Tools/Metis/src/Rewrite.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Rewrite.sml Sat Mar 26 15:55:22 2011 +0100
@@ -86,7 +86,7 @@
fun ppField f ppA a =
Print.blockProgram Print.Inconsistent 2
- [Print.addString (f ^ " ="),
+ [Print.ppString (f ^ " ="),
Print.addBreak 1,
ppA a];
@@ -112,24 +112,24 @@
in
fun pp (Rewrite {known,redexes,subterms,waiting,...}) =
Print.blockProgram Print.Inconsistent 2
- [Print.addString "Rewrite",
+ [Print.ppString "Rewrite",
Print.addBreak 1,
Print.blockProgram Print.Inconsistent 1
- [Print.addString "{",
+ [Print.ppString "{",
ppKnown known,
(*MetisTrace5
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
ppRedexes redexes,
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
ppSubterms subterms,
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
ppWaiting waiting,
*)
Print.skip],
- Print.addString "}"]
+ Print.ppString "}"]
end;
*)
@@ -192,10 +192,15 @@
else
let
val Rewrite {order,redexes,subterms,waiting, ...} = rw
+
val ort = orderToOrient (order (fst eqn))
+
val known = IntMap.insert known (id,(eqn,ort))
+
val redexes = addRedexes id (eqn,ort) redexes
+
val waiting = IntSet.add waiting id
+
val rw =
Rewrite
{order = order, known = known, redexes = redexes,
@@ -207,7 +212,11 @@
rw
end;
-fun addList x = List.foldl (fn (eqn,rw) => add rw eqn) x;
+local
+ fun uncurriedAdd (eqn,rw) = add rw eqn;
+in
+ fun addList rw = List.foldl uncurriedAdd rw;
+end;
(* ------------------------------------------------------------------------- *)
(* Rewriting (the order must be a refinement of the rewrite order). *)
@@ -640,7 +649,7 @@
val ppResult = Print.ppPair pp (Print.ppList Print.ppInt)
val () = Print.trace ppResult "Rewrite.reduce': result" result
*)
- val ths = map (fn (id,((_,th),_)) => (id,th)) (IntMap.toList known')
+ val ths = List.map (fn (id,((_,th),_)) => (id,th)) (IntMap.toList known')
val _ =
not (List.exists (uncurry (thmReducible order known')) ths) orelse
raise Bug "Rewrite.reduce': not fully reduced"
@@ -667,6 +676,10 @@
end;
end;
-fun rewrite x = orderedRewrite (K (SOME GREATER)) x;
+local
+ val order : reductionOrder = K (SOME GREATER);
+in
+ val rewrite = orderedRewrite order;
+end;
end
--- a/src/Tools/Metis/src/Rule.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Rule.sml Sat Mar 26 15:55:22 2011 +0100
@@ -81,6 +81,7 @@
else
let
val sub = Subst.fromList [(xVarName,x),(yVarName,y)]
+
val symTh = Thm.subst sub symmetry
in
Thm.resolve lit th symTh
@@ -94,9 +95,9 @@
type equation = (Term.term * Term.term) * Thm.thm;
-fun ppEquation (_,th) = Thm.pp th;
+fun ppEquation ((_,th) : equation) = Thm.pp th;
-fun equationToString x = Print.toString ppEquation x;
+val equationToString = Print.toString ppEquation;
fun equationLiteral (t_u,th) =
let
@@ -210,7 +211,7 @@
fun rewrConv (eqn as ((x,y), eqTh)) path tm =
if Term.equal x y then allConv tm
- else if null path then (y,eqTh)
+ else if List.null path then (y,eqTh)
else
let
val reflTh = Thm.refl tm
@@ -249,7 +250,7 @@
fun subtermsConv _ (tm as Term.Var _) = allConv tm
| subtermsConv conv (tm as Term.Fn (_,a)) =
- everyConv (map (subtermConv conv) (interval 0 (length a))) tm;
+ everyConv (List.map (subtermConv conv) (interval 0 (length a))) tm;
(* ------------------------------------------------------------------------- *)
(* Applying a conversion to every subterm, with some traversal strategy. *)
@@ -363,7 +364,7 @@
fun allArgumentsLiterule conv lit =
everyLiterule
- (map (argumentLiterule conv) (interval 0 (Literal.arity lit))) lit;
+ (List.map (argumentLiterule conv) (interval 0 (Literal.arity lit))) lit;
(* ------------------------------------------------------------------------- *)
(* A rule takes one theorem and either deduces another or raises an Error *)
@@ -779,7 +780,7 @@
let
fun fact sub = removeSym (Thm.subst sub th)
in
- map fact (factor' (Thm.clause th))
+ List.map fact (factor' (Thm.clause th))
end;
end
--- a/src/Tools/Metis/src/Term.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Term.sml Sat Mar 26 15:55:22 2011 +0100
@@ -164,7 +164,7 @@
in
case tm of
Var _ => subtms rest acc
- | Fn (_,args) => subtms (map f (enumerate args) @ rest) acc
+ | Fn (_,args) => subtms (List.map f (enumerate args) @ rest) acc
end;
in
fun subterms tm = subtms [([],tm)] [];
@@ -195,7 +195,7 @@
Var _ => search rest
| Fn (_,a) =>
let
- val subtms = map (fn (i,t) => (i :: path, t)) (enumerate a)
+ val subtms = List.map (fn (i,t) => (i :: path, t)) (enumerate a)
in
search (subtms @ rest)
end
@@ -235,14 +235,14 @@
fun newVar () = Var (Name.newName ());
-fun newVars n = map Var (Name.newNames n);
+fun newVars n = List.map Var (Name.newNames n);
local
- fun avoidAcceptable avoid n = not (NameSet.member n avoid);
+ fun avoid av n = NameSet.member n av;
in
- fun variantPrime avoid = Name.variantPrime (avoidAcceptable avoid);
+ fun variantPrime av = Name.variantPrime {avoid = avoid av};
- fun variantNum avoid = Name.variantNum (avoidAcceptable avoid);
+ fun variantNum av = Name.variantNum {avoid = avoid av};
end;
(* ------------------------------------------------------------------------- *)
@@ -314,7 +314,7 @@
val acc = (rev path, tm) :: acc
- val rest = map f (enumerate args) @ rest
+ val rest = List.map f (enumerate args) @ rest
in
subtms rest acc
end;
@@ -523,7 +523,7 @@
and basic bv (Var v) = varName bv v
| basic bv (Fn (f,args)) =
Print.blockProgram Print.Inconsistent 2
- (functionName bv f :: map (functionArgument bv) args)
+ (functionName bv f :: List.map (functionArgument bv) args)
and customBracket bv tm =
case destBrack tm of
@@ -535,13 +535,13 @@
NONE => term bv tm
| SOME (q,v,vs,tm) =>
let
- val bv = StringSet.addList bv (map Name.toString (v :: vs))
+ val bv = StringSet.addList bv (List.map Name.toString (v :: vs))
in
Print.program
[Print.ppString q,
varName bv v,
Print.program
- (map (Print.sequence (Print.addBreak 1) o varName bv) vs),
+ (List.map (Print.sequence (Print.addBreak 1) o varName bv) vs),
Print.ppString ".",
Print.addBreak 1,
innerQuant bv tm]
@@ -628,9 +628,9 @@
and neg = !negation
and bracks = ("(",")") :: !brackets
- val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
+ val bracks = List.map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
- val bTokens = map #2 bracks @ map #3 bracks
+ val bTokens = List.map #2 bracks @ List.map #3 bracks
fun possibleVarName "" = false
| possibleVarName s = isAlphaNum (String.sub (s,0))
@@ -685,8 +685,8 @@
in
var ||
const ||
- first (map bracket bracks) ||
- first (map quantifier quants)
+ first (List.map bracket bracks) ||
+ first (List.map quantifier quants)
end tokens
and molecule bv tokens =
--- a/src/Tools/Metis/src/TermNet.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/TermNet.sml Sat Mar 26 15:55:22 2011 +0100
@@ -50,7 +50,7 @@
fun equalFnQterm f1 f2 = compareFnQterm (f1,f2) = EQUAL;
fun termToQterm (Term.Var _) = Var
- | termToQterm (Term.Fn (f,l)) = Fn ((f, length l), map termToQterm l);
+ | termToQterm (Term.Fn (f,l)) = Fn ((f, length l), List.map termToQterm l);
local
fun qm [] = true
@@ -116,7 +116,7 @@
local
fun qtermToTerm Var = anonymousVar
- | qtermToTerm (Fn ((f,_),l)) = Term.Fn (f, map qtermToTerm l);
+ | qtermToTerm (Fn ((f,_),l)) = Term.Fn (f, List.map qtermToTerm l);
in
val ppQterm = Print.ppMap qtermToTerm Term.pp;
end;
@@ -339,7 +339,7 @@
fun fifoize ({fifo, ...} : parameters) l = if fifo then sort idwise l else l;
in
- fun finally parm l = map snd (fifoize parm l);
+ fun finally parm l = List.map snd (fifoize parm l);
end;
local
--- a/src/Tools/Metis/src/Thm.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Thm.sml Sat Mar 26 15:55:22 2011 +0100
@@ -107,7 +107,7 @@
local
fun toFormula th =
Formula.listMkDisj
- (map Literal.toFormula (LiteralSet.toList (clause th)));
+ (List.map Literal.toFormula (LiteralSet.toList (clause th)));
in
fun pp th =
Print.blockProgram Print.Inconsistent 3
--- a/src/Tools/Metis/src/Tptp.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Tptp.sml Sat Mar 26 15:55:22 2011 +0100
@@ -430,8 +430,8 @@
fun lift {name,arity,tptp} =
{name = Name.fromString name, arity = arity, tptp = tptp}
- val functionMapping = map lift defaultFunctionMapping
- and relationMapping = map lift defaultRelationMapping
+ val functionMapping = List.map lift defaultFunctionMapping
+ and relationMapping = List.map lift defaultRelationMapping
val mapping =
{functionMapping = functionMapping,
@@ -448,7 +448,7 @@
let
fun mkEntry {name,arity,model} = ((Name.fromString name, arity), model)
- fun mkMap l = NameArityMap.fromList (map mkEntry l)
+ fun mkMap l = NameArityMap.fromList (List.map mkEntry l)
in
{functionMap = mkMap funcModel,
relationMap = mkMap relModel}
@@ -766,8 +766,12 @@
val lexToken = alphaNumToken || punctToken || quoteToken;
val space = many (some Char.isSpace) >> K ();
+
+ val space1 = atLeastOne (some Char.isSpace) >> K ();
in
- val lexer = (space ++ lexToken ++ space) >> (fn ((),(tok,())) => tok);
+ val lexer =
+ (space ++ lexToken) >> (fn ((),tok) => [tok]) ||
+ space1 >> K [];
end;
(* ------------------------------------------------------------------------- *)
@@ -800,11 +804,11 @@
List.foldl fvs NameSet.empty
end;
-fun clauseSubst sub lits = map (literalSubst sub) lits;
-
-fun clauseToFormula lits = Formula.listMkDisj (map literalToFormula lits);
-
-fun clauseFromFormula fm = map literalFromFormula (Formula.stripDisj fm);
+fun clauseSubst sub lits = List.map (literalSubst sub) lits;
+
+fun clauseToFormula lits = Formula.listMkDisj (List.map literalToFormula lits);
+
+fun clauseFromFormula fm = List.map literalFromFormula (Formula.stripDisj fm);
fun clauseFromLiteralSet cl =
clauseFromFormula
@@ -1105,7 +1109,7 @@
end
| ProofFormulaSource {inference,parents} =>
let
- val isTaut = null parents
+ val isTaut = List.null parents
val gen = if isTaut then GEN_INTRODUCED else GEN_INFERENCE
@@ -1118,7 +1122,7 @@
Proof.Subst (s,_) => s
| _ => Subst.empty
in
- map (fn parent => (parent,sub)) parents
+ List.map (fn parent => (parent,sub)) parents
end
in
Print.blockProgram Print.Inconsistent (size gen + 1)
@@ -1300,7 +1304,7 @@
| f [x] = x
| f (h :: t) = (h ++ f t) >> K ();
in
- fun symbolParser s = f (map punctParser (String.explode s));
+ fun symbolParser s = f (List.map punctParser (String.explode s));
end;
val definedParser =
@@ -1568,7 +1572,7 @@
and quantifiedFormulaParser mapping input =
let
- fun mk (q,(vs,((),f))) = q (map (mkVarName mapping) vs, f)
+ fun mk (q,(vs,((),f))) = q (List.map (mkVarName mapping) vs, f)
in
(quantifierParser ++ varListParser ++ punctParser #":" ++
unitaryFormulaParser mapping) >> mk
@@ -1699,7 +1703,7 @@
fun parseChars parser chars =
let
- val tokens = Parse.everything (lexer >> singleton) chars
+ val tokens = Parse.everything lexer chars
in
Parse.everything (parser >> singleton) tokens
end;
@@ -1904,7 +1908,7 @@
val {problem,sources} : normalization = acc
val {axioms,conjecture} = problem
- val cls = map fst clauses
+ val cls = List.map fst clauses
val (axioms,conjecture) =
if isCnfConjectureRole role then (axioms, cls @ conjecture)
else (cls @ axioms, conjecture)
@@ -1939,7 +1943,7 @@
fun sourcify (cl,inf) = (cl, FofClauseSource inf)
val (clauses,cnf) = Normalize.addCnf th cnf
- val clauses = map sourcify clauses
+ val clauses = List.map sourcify clauses
val norm = addClauses role clauses norm
in
(norm,cnf)
@@ -1978,26 +1982,26 @@
let
val subgoals = Formula.splitGoal goal
val subgoals =
- if null subgoals then [Formula.True] else subgoals
+ if List.null subgoals then [Formula.True] else subgoals
val parents = [name]
in
- map (mk parents) subgoals
+ List.map (mk parents) subgoals
end
in
- fn goals => List.concat (map split goals)
+ fn goals => List.concat (List.map split goals)
end;
fun clausesToGoal cls =
let
- val cls = map (Formula.generalize o clauseToFormula o snd) cls
+ val cls = List.map (Formula.generalize o clauseToFormula o snd) cls
in
Formula.listMkConj cls
end;
fun formulasToGoal fms =
let
- val fms = map (Formula.generalize o snd) fms
+ val fms = List.map (Formula.generalize o snd) fms
in
Formula.listMkConj fms
end;
@@ -2013,11 +2017,11 @@
| FofGoal goals => formulasToGoal goals
val fm =
- if null fofAxioms then fm
+ if List.null fofAxioms then fm
else Formula.Imp (formulasToGoal fofAxioms, fm)
val fm =
- if null cnfAxioms then fm
+ if List.null cnfAxioms then fm
else Formula.Imp (clausesToGoal cnfAxioms, fm)
in
fm
@@ -2137,8 +2141,8 @@
let
val Problem {comments,includes,formulas} = problem
- val includesTop = null comments
- val formulasTop = includesTop andalso null includes
+ val includesTop = List.null comments
+ val formulasTop = includesTop andalso List.null includes
in
Stream.toTextFile
{filename = filename}
@@ -2153,8 +2157,8 @@
local
fun refute {axioms,conjecture} =
let
- val axioms = map Thm.axiom axioms
- and conjecture = map Thm.axiom conjecture
+ val axioms = List.map Thm.axiom axioms
+ and conjecture = List.map Thm.axiom conjecture
val problem = {axioms = axioms, conjecture = conjecture}
val resolution = Resolution.new Resolution.default problem
in
@@ -2166,7 +2170,7 @@
fun prove filename =
let
val problem = read filename
- val problems = map #problem (normalize problem)
+ val problems = List.map #problem (normalize problem)
in
List.all refute problems
end;
@@ -2334,7 +2338,7 @@
val number = i - 1
val (subgoal,formulas) =
- if null pars then (NONE,formulas)
+ if List.null pars then (NONE,formulas)
else
let
val role = PlainRole
@@ -2374,7 +2378,7 @@
| Normalize.Definition (_,fm) => fm :: fms
| _ => fms
- val parents = map (lookupFormulaName fmNames) fms
+ val parents = List.map (lookupFormulaName fmNames) fms
in
NormalizeFormulaSource
{inference = inference,
@@ -2388,9 +2392,9 @@
Proof.Axiom cl => [lookupClauseSourceName sources fmNames cl]
| _ =>
let
- val cls = map Thm.clause (Proof.parents inference)
+ val cls = List.map Thm.clause (Proof.parents inference)
in
- map (lookupClauseName clNames) cls
+ List.map (lookupClauseName clNames) cls
end
in
ProofFormulaSource
--- a/src/Tools/Metis/src/Useful.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Useful.sml Sat Mar 26 15:55:22 2011 +0100
@@ -50,7 +50,20 @@
(* Tracing. *)
(* ------------------------------------------------------------------------- *)
-val tracePrint = ref TextIO.print;
+local
+ val traceOut = TextIO.stdOut;
+
+ fun tracePrintFn mesg =
+ let
+ val () = TextIO.output (traceOut,mesg)
+
+ val () = TextIO.flushOut traceOut
+ in
+ ()
+ end;
+in
+ val tracePrint = ref tracePrintFn;
+end;
fun trace mesg = !tracePrint mesg;
@@ -254,7 +267,7 @@
case l of
[] =>
let
- val acc = if null row then acc else rev row :: acc
+ val acc = if List.null row then acc else rev row :: acc
in
rev acc
end
@@ -283,9 +296,9 @@
local
fun fstEq ((x,_),(y,_)) = x = y;
- fun collapse l = (fst (hd l), map snd l);
+ fun collapse l = (fst (hd l), List.map snd l);
in
- fun groupsByFst l = map collapse (groupsBy fstEq l);
+ fun groupsByFst l = List.map collapse (groupsBy fstEq l);
end;
fun groupsOf n =
@@ -430,10 +443,10 @@
| sortMap f cmp xs =
let
fun ncmp ((m,_),(n,_)) = cmp (m,n)
- val nxs = map (fn x => (f x, x)) xs
+ val nxs = List.map (fn x => (f x, x)) xs
val nys = sort ncmp nxs
in
- map snd nys
+ List.map snd nys
end;
(* ------------------------------------------------------------------------- *)
@@ -641,7 +654,7 @@
fun alignColumn {leftAlign,padChar} column =
let
- val (n,_) = maximum Int.compare (map size column)
+ val (n,_) = maximum Int.compare (List.map size column)
fun pad entry row =
let
@@ -657,13 +670,18 @@
local
fun alignTab aligns rows =
case aligns of
- [] => map (K "") rows
- | [{leftAlign = true, padChar = #" "}] => map hd rows
+ [] => List.map (K "") rows
+ | [{leftAlign = true, padChar = #" "}] => List.map hd rows
| align :: aligns =>
- alignColumn align (map hd rows) (alignTab aligns (map tl rows));
+ let
+ val col = List.map hd rows
+ and cols = alignTab aligns (List.map tl rows)
+ in
+ alignColumn align col cols
+ end;
in
fun alignTable aligns rows =
- if null rows then [] else alignTab aligns rows;
+ if List.null rows then [] else alignTab aligns rows;
end;
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Waiting.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/Waiting.sml Sat Mar 26 15:55:22 2011 +0100
@@ -63,7 +63,7 @@
val pp =
Print.ppMap
(fn Waiting {clauses,...} =>
- map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses))
+ List.map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses))
(Print.ppList (Print.ppTriple Print.ppReal Print.ppInt Clause.pp));
*)
@@ -81,10 +81,10 @@
(fvs,lits)
end;
-val mkModelClauses = map mkModelClause;
+val mkModelClauses = List.map mkModelClause;
fun perturbModel M cls =
- if null cls then K ()
+ if List.null cls then K ()
else
let
val N = {size = Model.size M}
@@ -195,6 +195,14 @@
val Waiting {parameters,clauses,models} = waiting
val {models = modelParameters, ...} = parameters
+(*MetisDebug
+ val _ = not (List.null cls) orelse
+ raise Bug "Waiting.add': null"
+
+ val _ = length mcls = length cls orelse
+ raise Bug "Waiting.add': different lengths"
+*)
+
val dist = dist + Math.ln (Real.fromInt (length cls))
fun addCl ((mcl,cl),acc) =
@@ -211,22 +219,23 @@
Waiting {parameters = parameters, clauses = clauses, models = models}
end;
-fun add waiting (_,[]) = waiting
- | add waiting (dist,cls) =
- let
+fun add waiting (dist,cls) =
+ if List.null cls then waiting
+ else
+ let
(*MetisTrace3
- val () = Print.trace pp "Waiting.add: waiting" waiting
- val () = Print.trace (Print.ppList Clause.pp) "Waiting.add: cls" cls
+ val () = Print.trace pp "Waiting.add: waiting" waiting
+ val () = Print.trace (Print.ppList Clause.pp) "Waiting.add: cls" cls
*)
- val waiting = add' waiting dist (mkModelClauses cls) cls
+ val waiting = add' waiting dist (mkModelClauses cls) cls
(*MetisTrace3
- val () = Print.trace pp "Waiting.add: waiting" waiting
+ val () = Print.trace pp "Waiting.add: waiting" waiting
*)
- in
- waiting
- end;
+ in
+ waiting
+ end;
local
fun cmp ((w1,_),(w2,_)) = Real.compare (w1,w2);
@@ -235,7 +244,7 @@
let
val {models = modelParameters, ...} = parameters
val clauses = Heap.new cmp
- and models = map (initialModel axioms conjecture) modelParameters
+ and models = List.map (initialModel axioms conjecture) modelParameters
in
Waiting {parameters = parameters, clauses = clauses, models = models}
end;
@@ -247,8 +256,17 @@
val waiting = empty parameters mAxioms mConjecture
in
- add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture)
- end;
+ if List.null axioms andalso List.null conjecture then waiting
+ else add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture)
+ end
+(*MetisDebug
+ handle e =>
+ let
+ val () = Print.trace Print.ppException "Waiting.new: exception" e
+ in
+ raise e
+ end;
+*)
end;
(* ------------------------------------------------------------------------- *)
@@ -260,9 +278,12 @@
else
let
val ((_,dcl),clauses) = Heap.remove clauses
+
val waiting =
Waiting
- {parameters = parameters, clauses = clauses, models = models}
+ {parameters = parameters,
+ clauses = clauses,
+ models = models}
in
SOME (dcl,waiting)
end;
--- a/src/Tools/Metis/src/metis.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/metis.sml Sat Mar 26 15:55:22 2011 +0100
@@ -13,23 +13,25 @@
val VERSION = "2.3";
-val versionString = PROGRAM^" "^VERSION^" (release 20100916)"^"\n";
+val versionString = PROGRAM^" "^VERSION^" (release 20101229)"^"\n";
(* ------------------------------------------------------------------------- *)
(* Program options. *)
(* ------------------------------------------------------------------------- *)
+val ITEMS = ["name","goal","clauses","size","category","proof","saturation"];
+
+val TIMEOUT : int option ref = ref NONE;
+
+val TPTP : string option ref = ref NONE;
+
val QUIET = ref false;
val TEST = ref false;
-val TPTP : string option ref = ref NONE;
-
-val ITEMS = ["name","goal","clauses","size","category","proof","saturation"];
-
val extended_items = "all" :: ITEMS;
-val show_items = map (fn s => (s, ref false)) ITEMS;
+val show_items = List.map (fn s => (s, ref false)) ITEMS;
fun show_ref s =
case List.find (equal s o fst) show_items of
@@ -68,6 +70,11 @@
description = "hide ITEM (see below for list)",
processor =
beginOpt (enumOpt extended_items endOpt) (fn _ => fn s => hide s)},
+ {switches = ["--time-limit"], arguments = ["N"],
+ description = "give up after N seconds",
+ processor =
+ beginOpt (optionOpt ("-", intOpt (SOME 0, NONE)) endOpt)
+ (fn _ => fn n => TIMEOUT := n)},
{switches = ["--tptp"], arguments = ["DIR"],
description = "specify the TPTP installation directory",
processor =
@@ -113,6 +120,25 @@
(* The core application. *)
(* ------------------------------------------------------------------------- *)
+fun newLimit () =
+ case !TIMEOUT of
+ NONE => K true
+ | SOME lim =>
+ let
+ val timer = Timer.startRealTimer ()
+
+ val lim = Time.fromReal (Real.fromInt lim)
+
+ fun check () =
+ let
+ val time = Timer.checkRealTimer timer
+ in
+ Time.<= (time,lim)
+ end
+ in
+ check
+ end;
+
(*MetisDebug
val next_cnf =
let
@@ -237,7 +263,7 @@
names = Tptp.noClauseNames,
roles = Tptp.noClauseRoles,
problem = {axioms = [],
- conjecture = map Thm.clause ths}}
+ conjecture = List.map Thm.clause ths}}
val mapping =
Tptp.addVarSetMapping Tptp.defaultMapping
@@ -294,21 +320,25 @@
end
*)
val () = display_clauses cls
+
val () = display_size cls
+
val () = display_category cls
in
()
end;
fun mkTptpFilename filename =
- case !TPTP of
- NONE => filename
- | SOME tptp =>
- let
- val tptp = stripSuffix (equal #"/") tptp
- in
- tptp ^ "/" ^ filename
- end;
+ if isPrefix "/" filename then filename
+ else
+ case !TPTP of
+ NONE => filename
+ | SOME tptp =>
+ let
+ val tptp = stripSuffix (equal #"/") tptp
+ in
+ tptp ^ "/" ^ filename
+ end;
fun readIncludes mapping seen formulas includes =
case includes of
@@ -338,7 +368,7 @@
val Tptp.Problem {comments,includes,formulas} = problem
in
- if null includes then problem
+ if List.null includes then problem
else
let
val seen = StringSet.empty
@@ -356,8 +386,7 @@
val resolutionParameters =
let
- val {active,
- waiting} = Resolution.default
+ val {active,waiting} = Resolution.default
val waiting =
let
@@ -394,17 +423,25 @@
waiting = waiting}
end;
- fun refute {axioms,conjecture} =
+ fun resolutionLoop limit res =
+ case Resolution.iterate res of
+ Resolution.Decided dec => SOME dec
+ | Resolution.Undecided res =>
+ if limit () then resolutionLoop limit res else NONE;
+
+ fun refute limit {axioms,conjecture} =
let
- val axioms = map Thm.axiom axioms
- and conjecture = map Thm.axiom conjecture
+ val axioms = List.map Thm.axiom axioms
+ and conjecture = List.map Thm.axiom conjecture
+
val problem = {axioms = axioms, conjecture = conjecture}
- val resolution = Resolution.new resolutionParameters problem
+
+ val res = Resolution.new resolutionParameters problem
in
- Resolution.loop resolution
+ resolutionLoop limit res
end;
- fun refuteAll filename tptp probs acc =
+ fun refuteAll limit filename tptp probs acc =
case probs of
[] =>
let
@@ -427,10 +464,10 @@
val () = display_problem filename problem
in
- if !TEST then refuteAll filename tptp probs acc
+ if !TEST then refuteAll limit filename tptp probs acc
else
- case refute problem of
- Resolution.Contradiction th =>
+ case refute limit problem of
+ SOME (Resolution.Contradiction th) =>
let
val subgoalProof =
{subgoal = subgoal,
@@ -439,9 +476,9 @@
val acc = subgoalProof :: acc
in
- refuteAll filename tptp probs acc
+ refuteAll limit filename tptp probs acc
end
- | Resolution.Satisfiable ths =>
+ | SOME (Resolution.Satisfiable ths) =>
let
val status =
if Tptp.hasFofConjecture tptp then
@@ -450,29 +487,42 @@
Tptp.SatisfiableStatus
val () = display_status filename status
+
val () = display_saturation filename ths
in
false
end
+ | NONE =>
+ let
+ val status = Tptp.UnknownStatus
+
+ val () = display_status filename status
+ in
+ false
+ end
end;
in
- fun prove mapping filename =
+ fun prove limit mapping filename =
let
val () = display_sep ()
+
val () = display_name filename
+
val tptp = read mapping filename
+
val () = display_goal tptp
+
val problems = Tptp.normalize tptp
in
- refuteAll filename tptp problems []
+ refuteAll limit filename tptp problems []
end;
+end;
- fun proveAll mapping filenames =
- List.all
- (if !QUIET then prove mapping
- else fn filename => prove mapping filename orelse true)
- filenames;
-end;
+fun proveAll limit mapping filenames =
+ List.all
+ (if !QUIET then prove limit mapping
+ else fn filename => prove limit mapping filename orelse true)
+ filenames;
(* ------------------------------------------------------------------------- *)
(* Top level. *)
@@ -482,11 +532,13 @@
let
val work = processOptions ()
- val () = if null work then usage "no input problem files" else ()
+ val () = if List.null work then usage "no input problem files" else ()
+
+ val limit = newLimit ()
val mapping = Tptp.defaultMapping
- val success = proveAll mapping work
+ val success = proveAll limit mapping work
in
exit {message = NONE, usage = false, success = success}
end
--- a/src/Tools/Metis/src/problems.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/problems.sml Sat Mar 26 15:55:22 2011 +0100
@@ -22,7 +22,7 @@
fun mkProblem collection description (problem : problem) : problem =
let
val {name,comments,goal} = problem
- val comments = if null comments then [] else "" :: comments
+ val comments = if List.null comments then [] else "" :: comments
val comments = "Description: " ^ description :: comments
val comments = mkCollection collection :: comments
in
@@ -33,7 +33,7 @@
Useful.mem (mkCollection collection) comments;
fun mkProblems collection description problems =
- map (mkProblem collection description) problems;
+ List.map (mkProblem collection description) problems;
end;
(* ========================================================================= *)
--- a/src/Tools/Metis/src/problems2tptp.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/problems2tptp.sml Sat Mar 26 15:55:22 2011 +0100
@@ -34,7 +34,7 @@
if x <> x' then dups xs
else raise Error ("duplicate problem name: " ^ x)
- val names = sort String.compare (map #name problems)
+ val names = sort String.compare (List.map #name problems)
in
dups names
end;
@@ -56,8 +56,8 @@
val comments =
[comment_bar] @
["Name: " ^ name] @
- (if null comments then [] else "" :: comments) @
- (if null comment_footer then [] else "" :: comment_footer) @
+ (if List.null comments then [] else "" :: comments) @
+ (if List.null comment_footer then [] else "" :: comment_footer) @
[comment_bar]
val includes = []
@@ -145,7 +145,7 @@
val (opts,work) =
Options.processOptions programOptions (CommandLine.arguments ());
-val () = if null work then () else usage "too many arguments";
+val () = if List.null work then () else usage "too many arguments";
(* ------------------------------------------------------------------------- *)
(* Top level. *)
--- a/src/Tools/Metis/src/selftest.sml Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/Metis/src/selftest.sml Sat Mar 26 15:55:22 2011 +0100
@@ -84,7 +84,7 @@
and L = Literal.parse
and F = Formula.parse
and S = Subst.fromList;
-val LS = LiteralSet.fromList o map L;
+val LS = LiteralSet.fromList o List.map L;
val AX = Thm.axiom o LS;
val CL = mkCl Clause.default o AX;
val Q = (fn th => (Thm.destUnitEq th, th)) o AX o singleton
@@ -116,7 +116,7 @@
val () = SAY "The parser and pretty-printer";
(* ------------------------------------------------------------------------- *)
-fun prep l = (chop_newline o String.concat o map unquote) l;
+fun prep l = (chop_newline o String.concat o List.map unquote) l;
fun mini_print n fm = withRef (Print.lineLength,n) Formula.toString fm;
@@ -509,7 +509,7 @@
fun clauseToFormula cl =
Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl);
in
- fun clausesToFormula cls = Formula.listMkConj (map clauseToFormula cls);
+ fun clausesToFormula cls = Formula.listMkConj (List.map clauseToFormula cls);
end;
val cnf' = pvFm o clausesToFormula o Normalize.cnf o F;
@@ -565,7 +565,7 @@
in
fun checkModel M cls =
let
- val table = map (checkModelClause M) cls
+ val table = List.map (checkModelClause M) cls
val rows = alignTable format table
@@ -587,7 +587,7 @@
else Model.perturbClause M V cl
end
- val cls = map (fn cl => (LiteralSet.freeVars cl, cl)) cls
+ val cls = List.map (fn cl => (LiteralSet.freeVars cl, cl)) cls
fun perturbClauses () = app perturbClause cls
@@ -1085,7 +1085,7 @@
val quot_clauses =
Formula.listMkConj o sort Formula.compare o
- map (quot o snd o Formula.stripForall) o Formula.stripConj;
+ List.map (quot o snd o Formula.stripForall) o Formula.stripConj;
fun quotient (Formula.Imp (a, Formula.Imp (b, Formula.False))) =
Formula.Imp (quot_clauses a, Formula.Imp (quot_clauses b, Formula.False))
@@ -1142,6 +1142,8 @@
end;
val _ = tptp "PUZ001-1";
+val _ = tptp "NO_FORMULAS";
+val _ = tptp "SEPARATED_COMMENTS";
val _ = tptp "NUMBERED_FORMULAS";
val _ = tptp "DEFINED_TERMS";
val _ = tptp "SYSTEM_TERMS";
--- a/src/Tools/quickcheck.ML Sat Mar 26 12:01:40 2011 +0100
+++ b/src/Tools/quickcheck.ML Sat Mar 26 15:55:22 2011 +0100
@@ -9,36 +9,45 @@
val setup: theory -> theory
(* configuration *)
val auto: bool Unsynchronized.ref
- val timing : bool Unsynchronized.ref
val tester : string Config.T
val size : int Config.T
val iterations : int Config.T
val no_assms : bool Config.T
val report : bool Config.T
+ val timing : bool Config.T
val quiet : bool Config.T
val timeout : real Config.T
val finite_types : bool Config.T
val finite_type_size : int Config.T
- datatype report = Report of
- { iterations : int, raised_match_errors : int,
- satisfied_assms : int list, positive_concl_tests : int }
datatype expectation = No_Expectation | No_Counterexample | Counterexample;
datatype test_params = Test_Params of {default_type: typ list, expect : expectation};
val test_params_of : Proof.context -> test_params
val map_test_params : (typ list * expectation -> typ list * expectation)
-> Context.generic -> Context.generic
+ datatype report = Report of
+ { iterations : int, raised_match_errors : int,
+ satisfied_assms : int list, positive_concl_tests : int }
+ (* registering generators *)
val add_generator:
string * (Proof.context -> term * term list -> int -> term list option * report option)
-> Context.generic -> Context.generic
val add_batch_generator:
string * (Proof.context -> term list -> (int -> term list option) list)
-> Context.generic -> Context.generic
+ (* quickcheck's result *)
+ datatype result =
+ Result of
+ {counterexample : (string * term) list option,
+ evaluation_terms : (term * term) list option,
+ timings : (string * int) list,
+ reports : (int * report) list}
+ val counterexample_of : result -> (string * term) list option
+ val timings_of : result -> (string * int) list
(* testing terms and proof states *)
- val test_term: Proof.context -> bool * bool -> term * term list ->
- ((string * term) list * (term * term) list) option * ((string * int) list * ((int * report) list) option)
+ val test_term: Proof.context -> bool * bool -> term * term list -> result
val test_goal_terms:
Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list
- -> ((string * term) list * (term * term) list) option * ((string * int) list * ((int * report) list) option) list
+ -> result list
val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
(* testing a batch of terms *)
val test_terms: Proof.context -> term list -> (string * term) list option list option
@@ -51,8 +60,6 @@
val auto = Unsynchronized.ref false;
-val timing = Unsynchronized.ref false;
-
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
(Unsynchronized.setmp auto true (fn () =>
@@ -66,6 +73,50 @@
{ iterations : int, raised_match_errors : int,
satisfied_assms : int list, positive_concl_tests : int }
+(* Quickcheck Result *)
+
+datatype result = Result of
+ { counterexample : (string * term) list option, evaluation_terms : (term * term) list option,
+ timings : (string * int) list, reports : (int * report) list}
+
+val empty_result =
+ Result {counterexample = NONE, evaluation_terms = NONE, timings = [], reports = []}
+
+fun counterexample_of (Result r) = #counterexample r
+
+fun found_counterexample (Result r) = is_some (#counterexample r)
+
+fun response_of (Result r) = case (#counterexample r, #evaluation_terms r) of
+ (SOME ts, SOME evals) => SOME (ts, evals)
+ | (NONE, NONE) => NONE
+
+fun timings_of (Result r) = #timings r
+
+fun set_reponse names eval_terms (SOME ts) (Result r) =
+ let
+ val (ts1, ts2) = chop (length names) ts
+ in
+ Result {counterexample = SOME (names ~~ ts1), evaluation_terms = SOME (eval_terms ~~ ts2),
+ timings = #timings r, reports = #reports r}
+ end
+ | set_reponse _ _ NONE result = result
+
+fun cons_timing timing (Result r) =
+ Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
+ timings = cons timing (#timings r), reports = #reports r}
+
+fun cons_report size (SOME report) (Result r) =
+ Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
+ timings = #timings r, reports = cons (size, report) (#reports r)}
+ | cons_report _ NONE result = result
+
+fun add_timing timing result_ref = (result_ref := cons_timing timing (!result_ref))
+
+fun add_report size report result_ref = (result_ref := cons_report size report (!result_ref))
+
+fun add_response names eval_terms response result_ref =
+ (result_ref := set_reponse names eval_terms response (!result_ref))
+
(* expectation *)
datatype expectation = No_Expectation | No_Counterexample | Counterexample;
@@ -79,6 +130,7 @@
val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100)
val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false)
val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true)
+val (timing, setup_timing) = Attrib.config_bool "quickcheck_timing" (K false)
val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
val (finite_types, setup_finite_types) = Attrib.config_bool "quickcheck_finite_types" (K true)
@@ -86,8 +138,8 @@
Attrib.config_int "quickcheck_finite_type_size" (K 3)
val setup_config =
- setup_tester #> setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet
- #> setup_timeout #> setup_finite_types #> setup_finite_type_size
+ setup_tester #> setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_timing
+ #> setup_quiet #> setup_timeout #> setup_finite_types #> setup_finite_type_size
datatype test_params = Test_Params of
{default_type: typ list, expect : expectation};
@@ -178,48 +230,44 @@
else
f ()
-fun mk_result names eval_terms ts =
- let
- val (ts1, ts2) = chop (length names) ts
- in
- (names ~~ ts1, eval_terms ~~ ts2)
- end
-
fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
let
+ fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
val _ = check_test_term t
val names = Term.add_free_names t []
val current_size = Unsynchronized.ref 0
- fun excipit s =
- "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
+ val current_result = Unsynchronized.ref empty_result
+ fun excipit () =
+ "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
val (test_fun, comp_time) = cpu_time "quickcheck compilation"
(fn () => mk_tester ctxt (t, eval_terms));
- fun with_size test_fun k reports =
+ val _ = add_timing comp_time current_result
+ fun with_size test_fun k =
if k > Config.get ctxt size then
- (NONE, reports)
+ NONE
else
let
- val _ = if Config.get ctxt quiet then () else Output.urgent_message
- ("Test data size: " ^ string_of_int k)
+ val _ = message ("Test data size: " ^ string_of_int k)
val _ = current_size := k
- val ((result, new_report), timing) =
+ val ((result, report), timing) =
cpu_time ("size " ^ string_of_int k) (fn () => test_fun (k - 1))
- val reports = case new_report of NONE => reports | SOME rep => (k, rep) :: reports
+ val _ = add_timing timing current_result
+ val _ = add_report k report current_result
in
- case result of NONE => with_size test_fun (k + 1) reports | SOME q => (SOME q, reports)
+ case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q
end;
in
- case test_fun of NONE => (NONE, ([comp_time], NONE))
+ case test_fun of NONE => !current_result
| SOME test_fun =>
limit ctxt (limit_time, is_interactive) (fn () =>
let
- val ((result, reports), exec_time) =
- cpu_time "quickcheck execution" (fn () => with_size test_fun 1 [])
+ val (response, exec_time) =
+ cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
+ val _ = add_response names eval_terms response current_result
+ val _ = add_timing exec_time current_result
in
- (Option.map (mk_result names eval_terms) result,
- ([exec_time, comp_time],
- if Config.get ctxt report andalso not (null reports) then SOME reports else NONE))
- end) (fn () => error (excipit "ran out of time")) ()
+ !current_result
+ end) (fn () => (message (excipit ()); !current_result)) ()
end;
fun test_terms ctxt ts =
@@ -244,17 +292,24 @@
fun test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) ts =
let
val thy = ProofContext.theory_of ctxt
+ fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
val (ts, eval_terms) = split_list ts
val _ = map check_test_term ts
val names = Term.add_free_names (hd ts) []
val Ts = map snd (Term.add_frees (hd ts) [])
+ val current_result = Unsynchronized.ref empty_result
val (test_funs, comp_time) = cpu_time "quickcheck compilation"
(fn () => map (mk_tester ctxt) (ts ~~ eval_terms))
+ val _ = add_timing comp_time current_result
fun test_card_size (card, size) =
(* FIXME: why decrement size by one? *)
- case fst (the (nth test_funs (card - 1)) (size - 1)) of
- SOME ts => SOME (mk_result names (nth eval_terms (card - 1)) ts)
- | NONE => NONE
+ let
+ val (ts, timing) = cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
+ (fn () => fst (the (nth test_funs (card - 1)) (size - 1)))
+ val _ = add_timing timing current_result
+ in
+ Option.map (pair card) ts
+ end
val enumeration_card_size =
if forall (fn T => Sign.of_sort thy (T, ["Enum.enum"])) Ts then
(* size does not matter *)
@@ -264,12 +319,15 @@
map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size))
|> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
in
- if (forall is_none test_funs) then
- (NONE, ([comp_time], NONE))
+ if (forall is_none test_funs) then !current_result
else if (forall is_some test_funs) then
limit ctxt (limit_time, is_interactive) (fn () =>
- (get_first test_card_size enumeration_card_size, ([comp_time], NONE)))
- (fn () => error "Quickcheck ran out of time") ()
+ let
+ val _ = case get_first test_card_size enumeration_card_size of
+ SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
+ | NONE => ()
+ in !current_result end)
+ (fn () => (message "Quickcheck ran out of time"; !current_result)) ()
else
error "Unexpectedly, testers of some cardinalities are executable but others are not"
end
@@ -325,20 +383,25 @@
[[]] => error error_msg
| xs => xs
val _ = if Config.get lthy quiet then () else warning error_msg
- fun collect_results f reports [] = (NONE, rev reports)
- | collect_results f reports (t :: ts) =
- case f t of
- (SOME res, report) => (SOME res, rev (report :: reports))
- | (NONE, report) => collect_results f (report :: reports) ts
+ fun collect_results f [] results = results
+ | collect_results f (t :: ts) results =
+ let
+ val result = f t
+ in
+ if found_counterexample result then
+ (result :: results)
+ else
+ collect_results f ts (result :: results)
+ end
fun test_term' goal =
case goal of
[(NONE, t)] => test_term lthy (limit_time, is_interactive) t
| ts => test_term_with_increasing_cardinality lthy (limit_time, is_interactive) (map snd ts)
in
if Config.get lthy finite_types then
- collect_results test_term' [] correct_inst_goals
+ collect_results test_term' correct_inst_goals []
else
- collect_results (test_term lthy (limit_time, is_interactive)) [] (maps (map snd) correct_inst_goals)
+ collect_results (test_term lthy (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
end;
fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
@@ -400,9 +463,15 @@
(rev reports))
| pretty_reports ctxt NONE = Pretty.str ""
-fun pretty_counterex_and_reports ctxt auto (cex, timing_and_reports) =
- Pretty.chunks (pretty_counterex ctxt auto cex ::
- map (pretty_reports ctxt) (map snd timing_and_reports))
+fun pretty_timings timings =
+ Pretty.chunks (Pretty.fbrk :: Pretty.str "timings:" ::
+ maps (fn (label, time) =>
+ Pretty.str (label ^ ": " ^ string_of_int time ^ " ms") :: Pretty.brk 1 :: []) (rev timings))
+
+fun pretty_counterex_and_reports ctxt auto (result :: _) =
+ Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
+ (* map (pretty_reports ctxt) (reports_of result) :: *)
+ (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
(* automatic testing *)
@@ -416,9 +485,11 @@
in
case res of
NONE => (false, state)
- | SOME (NONE, report) => (false, state)
- | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
- Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state)
+ | SOME (result :: _) => if found_counterexample result then
+ (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
+ Pretty.mark Markup.hilite (pretty_counterex ctxt true (response_of result))])) state)
+ else
+ (false, state)
end
val setup = Auto_Tools.register_tool (auto, auto_quickcheck)
@@ -482,16 +553,23 @@
fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
+fun check_expectation state results =
+ (if found_counterexample (hd results) andalso expect (Proof.context_of state) = No_Counterexample
+ then
+ error ("quickcheck expected to find no counterexample but found one")
+ else
+ (if not (found_counterexample (hd results)) andalso expect (Proof.context_of state) = Counterexample
+ then
+ error ("quickcheck expected to find a counterexample but did not find one")
+ else ()))
+
fun gen_quickcheck args i state =
state
|> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args (([], []), ctxt))
|> (fn ((insts, eval_terms), state') => test_goal (true, true) (insts, eval_terms) i state'
- |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
- error ("quickcheck expected to find no counterexample but found one") else ()
- | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
- error ("quickcheck expected to find a counterexample but did not find one") else ()))
+ |> tap (check_expectation state'))
-fun quickcheck args i state = Option.map fst (fst (gen_quickcheck args i state));
+fun quickcheck args i state = counterexample_of (hd (gen_quickcheck args i state))
fun quickcheck_cmd args i state =
gen_quickcheck args i (Toplevel.proof_of state)