--- a/Admin/isatest/settings/at-mac-poly-5.1-para Wed Jun 17 17:42:46 2009 +0200
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Thu Jun 18 00:00:52 2009 +0200
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-svn"
- ML_SYSTEM="polyml-experimental"
+ POLYML_HOME="/home/polyml/polyml-5.2.1"
+ ML_SYSTEM="polyml-5.2.1"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="--mutable 800 --immutable 2000"
--- a/doc-src/Classes/Thy/Classes.thy Wed Jun 17 17:42:46 2009 +0200
+++ b/doc-src/Classes/Thy/Classes.thy Thu Jun 18 00:00:52 2009 +0200
@@ -5,8 +5,8 @@
section {* Introduction *}
text {*
- Type classes were introduces by Wadler and Blott \cite{wadler89how}
- into the Haskell language, to allow for a reasonable implementation
+ Type classes were introduced by Wadler and Blott \cite{wadler89how}
+ into the Haskell language to allow for a reasonable implementation
of overloading\footnote{throughout this tutorial, we are referring
to classical Haskell 1.0 type classes, not considering
later additions in expressiveness}.
@@ -43,9 +43,9 @@
Indeed, type classes not only allow for simple overloading
but form a generic calculus, an instance of order-sorted
- algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
+ algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
- From a software engeneering point of view, type classes
+ From a software engineering point of view, type classes
roughly correspond to interfaces in object-oriented languages like Java;
so, it is naturally desirable that type classes do not only
provide functions (class parameters) but also state specifications
@@ -65,7 +65,7 @@
\end{quote}
- \noindent From a theoretic point of view, type classes are lightweight
+ \noindent From a theoretical point of view, type classes are lightweight
modules; Haskell type classes may be emulated by
SML functors \cite{classes_modules}.
Isabelle/Isar offers a discipline of type classes which brings
@@ -77,22 +77,19 @@
\item instantiating those abstract parameters by a particular
type
\item in connection with a ``less ad-hoc'' approach to overloading,
- \item with a direct link to the Isabelle module system
- (aka locales \cite{kammueller-locales}).
+ \item with a direct link to the Isabelle module system:
+ locales \cite{kammueller-locales}.
\end{enumerate}
\noindent Isar type classes also directly support code generation
- in a Haskell like fashion.
+ in a Haskell like fashion. Internally, they are mapped to more primitive
+ Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
This tutorial demonstrates common elements of structured specifications
and abstract reasoning with type classes by the algebraic hierarchy of
semigroups, monoids and groups. Our background theory is that of
Isabelle/HOL \cite{isa-tutorial}, for which some
familiarity is assumed.
-
- Here we merely present the look-and-feel for end users.
- Internally, those are mapped to more primitive Isabelle concepts.
- See \cite{Haftmann-Wenzel:2006:classes} for more detail.
*}
section {* A simple algebra example \label{sec:example} *}
@@ -146,22 +143,22 @@
end %quote
text {*
- \noindent @{command instantiation} allows to define class parameters
+ \noindent @{command instantiation} defines class parameters
at a particular instance using common specification tools (here,
@{command definition}). The concluding @{command instance}
opens a proof that the given parameters actually conform
to the class specification. Note that the first proof step
is the @{method default} method,
which for such instance proofs maps to the @{method intro_classes} method.
- This boils down an instance judgement to the relevant primitive
- proof goals and should conveniently always be the first method applied
+ This reduces an instance judgement to the relevant primitive
+ proof goals; typically it is the first method applied
in an instantiation proof.
From now on, the type-checker will consider @{typ int}
as a @{class semigroup} automatically, i.e.\ any general results
are immediately available on concrete instances.
- \medskip Another instance of @{class semigroup} are the natural numbers:
+ \medskip Another instance of @{class semigroup} yields the natural numbers:
*}
instantiation %quote nat :: semigroup
@@ -191,7 +188,7 @@
subsection {* Lifting and parametric types *}
text {*
- Overloaded definitions given on class instantiation
+ Overloaded definitions given at a class instantiation
may include recursion over the syntactic structure of types.
As a canonical example, we model product semigroups
using our simple algebra:
@@ -201,11 +198,11 @@
begin
definition %quote
- mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
+ mult_prod_def: "p1 \<otimes> p2 = (fst p1 \<otimes> fst p2, snd p1 \<otimes> snd p2)"
instance %quote proof
- fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
- show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
+ fix p1 p2 p3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
+ show "p1 \<otimes> p2 \<otimes> p3 = p1 \<otimes> (p2 \<otimes> p3)"
unfolding mult_prod_def by (simp add: assoc)
qed
@@ -215,7 +212,7 @@
\noindent Associativity of product semigroups is established using
the definition of @{text "(\<otimes>)"} on products and the hypothetical
associativity of the type components; these hypotheses
- are facts due to the @{class semigroup} constraints imposed
+ are legitimate due to the @{class semigroup} constraints imposed
on the type components by the @{command instance} proposition.
Indeed, this pattern often occurs with parametric types
and type classes.
@@ -228,7 +225,7 @@
We define a subclass @{text monoidl} (a semigroup with a left-hand neutral)
by extending @{class semigroup}
with one additional parameter @{text neutral} together
- with its property:
+ with its characteristic property:
*}
class %quote monoidl = semigroup +
@@ -278,7 +275,7 @@
end %quote
text {*
- \noindent Fully-fledged monoids are modelled by another subclass
+ \noindent Fully-fledged monoids are modelled by another subclass,
which does not add new parameters but tightens the specification:
*}
@@ -338,13 +335,13 @@
section {* Type classes as locales *}
-subsection {* A look behind the scene *}
+subsection {* A look behind the scenes *}
text {*
The example above gives an impression how Isar type classes work
in practice. As stated in the introduction, classes also provide
a link to Isar's locale system. Indeed, the logical core of a class
- is nothing else than a locale:
+ is nothing other than a locale:
*}
class %quote idem =
@@ -378,7 +375,7 @@
proof qed (rule idem)
text {*
- \noindent This gives you at hand the full power of the Isabelle module system;
+ \noindent This gives you the full power of the Isabelle module system;
conclusions in locale @{text idem} are implicitly propagated
to class @{text idem}.
*} (*<*)setup %invisible {* Sign.parent_path *}
@@ -435,25 +432,26 @@
\noindent As you can see from this example, for local
definitions you may use any specification tool
- which works together with locales (e.g. \cite{krauss2006}).
+ which works together with locales, such as Krauss's recursive function package
+ \cite{krauss2006}.
*}
subsection {* A functor analogy *}
text {*
- We introduced Isar classes by analogy to type classes
+ We introduced Isar classes by analogy to type classes in
functional programming; if we reconsider this in the
context of what has been said about type classes and locales,
we can drive this analogy further by stating that type
- classes essentially correspond to functors which have
+ classes essentially correspond to functors that have
a canonical interpretation as type classes.
- Anyway, there is also the possibility of other interpretations.
- For example, also @{text list}s form a monoid with
+ There is also the possibility of other interpretations.
+ For example, @{text list}s also form a monoid with
@{text append} and @{term "[]"} as operations, but it
seems inappropriate to apply to lists
the same operations as for genuinely algebraic types.
- In such a case, we simply can do a particular interpretation
+ In such a case, we can simply make a particular interpretation
of monoids for lists:
*}
@@ -517,7 +515,7 @@
to the type system, making @{text group} an instance of
@{text monoid} by adding an additional edge
to the graph of subclass relations
- (cf.\ \figref{fig:subclass}).
+ (\figref{fig:subclass}).
\begin{figure}[htbp]
\begin{center}
@@ -550,7 +548,7 @@
\end{figure}
For illustration, a derived definition
- in @{text group} which uses @{text pow_nat}:
+ in @{text group} using @{text pow_nat}
*}
definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
@@ -567,7 +565,7 @@
subsection {* A note on syntax *}
text {*
- As a convenience, class context syntax allows to refer
+ As a convenience, class context syntax allows references
to local class operations and their global counterparts
uniformly; type inference resolves ambiguities. For example:
*}
@@ -601,9 +599,9 @@
@{command instantiation}
targets naturally maps to Haskell type classes.
The code generator framework \cite{isabelle-codegen}
- takes this into account. Concerning target languages
- lacking type classes (e.g.~SML), type classes
- are implemented by explicit dictionary construction.
+ takes this into account. If the target language (e.g.~SML)
+ lacks type classes, then they
+ are implemented by an explicit dictionary construction.
As example, let's go back to the power function:
*}
@@ -611,13 +609,13 @@
"example = pow_int 10 (-2)"
text {*
- \noindent This maps to Haskell as:
+ \noindent This maps to Haskell as follows:
*}
text %quote {*@{code_stmts example (Haskell)}*}
text {*
- \noindent The whole code in SML with explicit dictionary passing:
+ \noindent The code in SML has explicit dictionary passing:
*}
text %quote {*@{code_stmts example (SML)}*}
--- a/doc-src/Classes/Thy/document/Classes.tex Wed Jun 17 17:42:46 2009 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Thu Jun 18 00:00:52 2009 +0200
@@ -23,8 +23,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Type classes were introduces by Wadler and Blott \cite{wadler89how}
- into the Haskell language, to allow for a reasonable implementation
+Type classes were introduced by Wadler and Blott \cite{wadler89how}
+ into the Haskell language to allow for a reasonable implementation
of overloading\footnote{throughout this tutorial, we are referring
to classical Haskell 1.0 type classes, not considering
later additions in expressiveness}.
@@ -61,9 +61,9 @@
Indeed, type classes not only allow for simple overloading
but form a generic calculus, an instance of order-sorted
- algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
+ algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
- From a software engeneering point of view, type classes
+ From a software engineering point of view, type classes
roughly correspond to interfaces in object-oriented languages like Java;
so, it is naturally desirable that type classes do not only
provide functions (class parameters) but also state specifications
@@ -83,7 +83,7 @@
\end{quote}
- \noindent From a theoretic point of view, type classes are lightweight
+ \noindent From a theoretical point of view, type classes are lightweight
modules; Haskell type classes may be emulated by
SML functors \cite{classes_modules}.
Isabelle/Isar offers a discipline of type classes which brings
@@ -95,22 +95,19 @@
\item instantiating those abstract parameters by a particular
type
\item in connection with a ``less ad-hoc'' approach to overloading,
- \item with a direct link to the Isabelle module system
- (aka locales \cite{kammueller-locales}).
+ \item with a direct link to the Isabelle module system:
+ locales \cite{kammueller-locales}.
\end{enumerate}
\noindent Isar type classes also directly support code generation
- in a Haskell like fashion.
+ in a Haskell like fashion. Internally, they are mapped to more primitive
+ Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
This tutorial demonstrates common elements of structured specifications
and abstract reasoning with type classes by the algebraic hierarchy of
semigroups, monoids and groups. Our background theory is that of
Isabelle/HOL \cite{isa-tutorial}, for which some
- familiarity is assumed.
-
- Here we merely present the look-and-feel for end users.
- Internally, those are mapped to more primitive Isabelle concepts.
- See \cite{Haftmann-Wenzel:2006:classes} for more detail.%
+ familiarity is assumed.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -207,22 +204,22 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} allows to define class parameters
+\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} defines class parameters
at a particular instance using common specification tools (here,
\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}). The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
opens a proof that the given parameters actually conform
to the class specification. Note that the first proof step
is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
- This boils down an instance judgement to the relevant primitive
- proof goals and should conveniently always be the first method applied
+ This reduces an instance judgement to the relevant primitive
+ proof goals; typically it is the first method applied
in an instantiation proof.
From now on, the type-checker will consider \isa{int}
as a \isa{semigroup} automatically, i.e.\ any general results
are immediately available on concrete instances.
- \medskip Another instance of \isa{semigroup} are the natural numbers:%
+ \medskip Another instance of \isa{semigroup} yields the natural numbers:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -264,8 +261,8 @@
\begin{isamarkuptext}%
\noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
in the primrec declaration; by default, the local name of
- a class operation \isa{f} to instantiate on type constructor
- \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty,
+ a class operation \isa{f} to be instantiated on type constructor
+ \isa{{\isasymkappa}} is mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty,
these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
or the corresponding ProofGeneral button.%
\end{isamarkuptext}%
@@ -276,7 +273,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Overloaded definitions giving on class instantiation
+Overloaded definitions given at a class instantiation
may include recursion over the syntactic structure of types.
As a canonical example, we model product semigroups
using our simple algebra:%
@@ -294,15 +291,15 @@
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p{\isadigit{1}}\ {\isasymotimes}\ fst\ p{\isadigit{2}}{\isacharcomma}\ snd\ p{\isadigit{1}}\ {\isasymotimes}\ snd\ p{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
+\ p{\isadigit{1}}\ p{\isadigit{2}}\ p{\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}\ {\isacharequal}\ p{\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
@@ -319,11 +316,10 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Associativity from product semigroups is
- established using
+\noindent Associativity of product semigroups is established using
the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
associativity of the type components; these hypotheses
- are facts due to the \isa{semigroup} constraints imposed
+ are legitimate due to the \isa{semigroup} constraints imposed
on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
Indeed, this pattern often occurs with parametric types
and type classes.%
@@ -338,7 +334,7 @@
We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
by extending \isa{semigroup}
with one additional parameter \isa{neutral} together
- with its property:%
+ with its characteristic property:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -439,7 +435,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Fully-fledged monoids are modelled by another subclass
+\noindent Fully-fledged monoids are modelled by another subclass,
which does not add new parameters but tightens the specification:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -562,7 +558,7 @@
}
\isamarkuptrue%
%
-\isamarkupsubsection{A look behind the scene%
+\isamarkupsubsection{A look behind the scenes%
}
\isamarkuptrue%
%
@@ -570,7 +566,7 @@
The example above gives an impression how Isar type classes work
in practice. As stated in the introduction, classes also provide
a link to Isar's locale system. Indeed, the logical core of a class
- is nothing else than a locale:%
+ is nothing other than a locale:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -714,7 +710,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent This gives you at hand the full power of the Isabelle module system;
+\noindent This gives you the full power of the Isabelle module system;
conclusions in locale \isa{idem} are implicitly propagated
to class \isa{idem}.%
\end{isamarkuptext}%
@@ -832,7 +828,8 @@
\noindent As you can see from this example, for local
definitions you may use any specification tool
- which works together with locales (e.g. \cite{krauss2006}).%
+ which works together with locales, such as Krauss's recursive function package
+ \cite{krauss2006}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -841,18 +838,18 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-We introduced Isar classes by analogy to type classes
+We introduced Isar classes by analogy to type classes in
functional programming; if we reconsider this in the
context of what has been said about type classes and locales,
we can drive this analogy further by stating that type
- classes essentially correspond to functors which have
+ classes essentially correspond to functors that have
a canonical interpretation as type classes.
- Anyway, there is also the possibility of other interpretations.
- For example, also \isa{list}s form a monoid with
+ There is also the possibility of other interpretations.
+ For example, \isa{list}s also form a monoid with
\isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
seems inappropriate to apply to lists
the same operations as for genuinely algebraic types.
- In such a case, we simply can do a particular interpretation
+ In such a case, we can simply make a particular interpretation
of monoids for lists:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -982,7 +979,7 @@
to the type system, making \isa{group} an instance of
\isa{monoid} by adding an additional edge
to the graph of subclass relations
- (cf.\ \figref{fig:subclass}).
+ (\figref{fig:subclass}).
\begin{figure}[htbp]
\begin{center}
@@ -1015,7 +1012,7 @@
\end{figure}
For illustration, a derived definition
- in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
+ in \isa{group} using \isa{pow{\isacharunderscore}nat}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1048,7 +1045,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-As a convenience, class context syntax allows to refer
+As a convenience, class context syntax allows references
to local class operations and their global counterparts
uniformly; type inference resolves ambiguities. For example:%
\end{isamarkuptext}%
@@ -1113,9 +1110,9 @@
\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
targets naturally maps to Haskell type classes.
The code generator framework \cite{isabelle-codegen}
- takes this into account. Concerning target languages
- lacking type classes (e.g.~SML), type classes
- are implemented by explicit dictionary construction.
+ takes this into account. If the target language (e.g.~SML)
+ lacks type classes, then they
+ are implemented by an explicit dictionary construction.
As example, let's go back to the power function:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1136,7 +1133,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent This maps to Haskell as:%
+\noindent This maps to Haskell as follows:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1223,7 +1220,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The whole code in SML with explicit dictionary passing:%
+\noindent The code in SML has explicit dictionary passing:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1250,16 +1247,15 @@
\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoidl =\\
-\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}Classes{\char95}{\char95}semigroup{\char95}monoidl A{\char95};\\
+\hspace*{0pt}type 'a monoidl = {\char123}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
+\hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}semigroup{\char95}monoidl A{\char95};\\
\hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid :~'a monoidl{\char125};\\
-\hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}Classes{\char95}{\char95}monoidl{\char95}monoid A{\char95};\\
+\hspace*{0pt}type 'a monoid = {\char123}monoidl{\char95}monoid :~'a monoidl{\char125};\\
+\hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}monoidl{\char95}monoid A{\char95};\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a group = {\char123}Classes{\char95}{\char95}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
-\hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}Classes{\char95}{\char95}monoid{\char95}group A{\char95};\\
+\hspace*{0pt}type 'a group = {\char123}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
+\hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}monoid{\char95}group A{\char95};\\
\hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\
\hspace*{0pt}\\
\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
@@ -1271,14 +1267,12 @@
\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
\hspace*{0pt}\\
\hspace*{0pt}val monoidl{\char95}int =\\
-\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
+\hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
\hspace*{0pt} ~IntInf.int monoidl;\\
\hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}int = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:\\
-\hspace*{0pt} ~IntInf.int monoid;\\
+\hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\
\hspace*{0pt}\\
-\hspace*{0pt}val group{\char95}int =\\
-\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
+\hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
\hspace*{0pt} ~IntInf.int group;\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
--- a/doc-src/Classes/classes.tex Wed Jun 17 17:42:46 2009 +0200
+++ b/doc-src/Classes/classes.tex Thu Jun 18 00:00:52 2009 +0200
@@ -21,8 +21,7 @@
\maketitle
\begin{abstract}
- \noindent This tutorial introduces the look-and-feel of
- Isar type classes to the end-user. Isar type classes
+ \noindent This tutorial introduces Isar type classes, which
are a convenient mechanism for organizing specifications.
Essentially, they combine an operational aspect (in the
manner of Haskell) with a logical aspect, both managed uniformly.
--- a/doc-src/System/Thy/Presentation.thy Wed Jun 17 17:42:46 2009 +0200
+++ b/doc-src/System/Thy/Presentation.thy Thu Jun 18 00:00:52 2009 +0200
@@ -299,8 +299,8 @@
\begin{center}\small
\begin{tabular}{rcl}
- @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\
- @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"}
+ @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
+ @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
\end{tabular}
\end{center}
@@ -454,6 +454,7 @@
-p LEVEL set level of detail for proof objects
-r reset session path
-s NAME override session NAME
+ -t BOOL internal session timing (default false)
-v BOOL be verbose (default false)
Build object-logic or run examples. Also creates browsing
@@ -563,6 +564,9 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \medskip The @{verbatim "-t"} option produces a more detailed
+ internal timing report of the session.
+
\medskip The @{verbatim "-v"} option causes additional information
to be printed while running the session, notably the location of
prepared documents.
--- a/doc-src/System/Thy/document/Presentation.tex Wed Jun 17 17:42:46 2009 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex Thu Jun 18 00:00:52 2009 +0200
@@ -323,8 +323,8 @@
\begin{center}\small
\begin{tabular}{rcl}
- \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}\isactrlsup {\isacharplus}{\isachardoublequote}} \\
- \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}\isactrlsup {\isacharasterisk}{\isachardoublequote}}
+ \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}{\isacharplus}{\isachardoublequote}} \\
+ \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}{\isacharasterisk}{\isachardoublequote}}
\end{tabular}
\end{center}
@@ -480,6 +480,7 @@
-p LEVEL set level of detail for proof objects
-r reset session path
-s NAME override session NAME
+ -t BOOL internal session timing (default false)
-v BOOL be verbose (default false)
Build object-logic or run examples. Also creates browsing
@@ -580,6 +581,9 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \medskip The \verb|-t| option produces a more detailed
+ internal timing report of the session.
+
\medskip The \verb|-v| option causes additional information
to be printed while running the session, notably the location of
prepared documents.
--- a/lib/Tools/usedir Wed Jun 17 17:42:46 2009 +0200
+++ b/lib/Tools/usedir Thu Jun 18 00:00:52 2009 +0200
@@ -31,6 +31,7 @@
echo " -p LEVEL set level of detail for proof objects"
echo " -r reset session path"
echo " -s NAME override session NAME"
+ echo " -t BOOL internal session timing (default false)"
echo " -v BOOL be verbose (default false)"
echo
echo " Build object-logic or run examples. Also creates browsing"
@@ -84,12 +85,13 @@
RESET=false
SESSION=""
PROOFS=0
+TIMING=false
VERBOSE=false
function getoptions()
{
OPTIND=1
- while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:v:" OPT
+ while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:t:v:" OPT
do
case "$OPT" in
C)
@@ -158,6 +160,10 @@
s)
SESSION="$OPTARG"
;;
+ t)
+ check_bool "$OPTARG"
+ TIMING="$OPTARG"
+ ;;
v)
check_bool "$OPTARG"
VERBOSE="$OPTARG"
@@ -229,7 +235,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
+ -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
-q -w $LOGIC $NAME > "$LOG"
RC="$?"
else
@@ -238,7 +244,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
+ -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
-r -q "$LOGIC" > "$LOG"
RC="$?"
cd ..
--- a/lib/scripts/polyml-version Wed Jun 17 17:42:46 2009 +0200
+++ b/lib/scripts/polyml-version Thu Jun 18 00:00:52 2009 +0200
@@ -5,13 +5,8 @@
echo -n polyml
if [ -x "$ML_HOME/poly" ]; then
- if [ -x "$ML_HOME/polyimport" ]; then
- env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
- DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
- "$ML_HOME/poly" -v | \
- sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p'
- else
- "$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \
- sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p'
- fi
+ env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
+ DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
+ "$ML_HOME/poly" -v -H 10 | \
+ sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p'
fi
--- a/src/HOL/Tools/datatype_package/datatype_package.ML Wed Jun 17 17:42:46 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_package.ML Thu Jun 18 00:00:52 2009 +0200
@@ -351,7 +351,7 @@
simps : thm list}
structure DatatypeInterpretation = InterpretationFun
- (type T = datatype_config * string list val eq = eq_snd op =);
+ (type T = datatype_config * string list val eq: T * T -> bool = eq_snd op =);
fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
--- a/src/Pure/General/output.ML Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/General/output.ML Thu Jun 18 00:00:52 2009 +0200
@@ -18,7 +18,6 @@
val timeap: ('a -> 'b) -> 'a -> 'b
val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
val timing: bool ref
- val time_accumulator: string -> ('a -> 'b) -> 'a -> 'b
end;
signature OUTPUT =
@@ -47,7 +46,6 @@
val debugging: bool ref
val no_warnings: ('a -> 'b) -> 'a -> 'b
val debug: (unit -> string) -> unit
- val accumulated_time: unit -> unit
end;
structure Output: OUTPUT =
@@ -141,79 +139,9 @@
fun timeap f x = timeit (fn () => f x);
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
-
(*global timing mode*)
val timing = ref false;
-
-(* accumulated timing *)
-
-local
-
-datatype time_info = TI of
- {name: string,
- timer: Timer.cpu_timer,
- sys: Time.time,
- usr: Time.time,
- gc: Time.time,
- count: int};
-
-fun time_init name = ref (TI
- {name = name,
- timer = Timer.startCPUTimer (),
- sys = Time.zeroTime,
- usr = Time.zeroTime,
- gc = Time.zeroTime,
- count = 0});
-
-fun time_reset (r as ref (TI {name, ...})) = r := ! (time_init name);
-
-fun time_check (ref (TI r)) = r;
-
-fun time_add ti f x =
- let
- fun add_diff time time1 time2 =
- Time.+ (time, Time.- (time2, time1) handle Time.Time => Time.zeroTime);
- val {name, timer, sys, usr, gc, count} = time_check ti;
- val (sys1, usr1, gc1) = check_timer timer;
- val result = Exn.capture f x;
- val (sys2, usr2, gc2) = check_timer timer;
- in
- ti := TI
- {name = name,
- timer = timer,
- sys = add_diff sys sys1 sys2,
- usr = add_diff usr usr1 usr2,
- gc = add_diff gc gc1 gc2,
- count = count + 1};
- Exn.release result
- end;
-
-fun time_finish ti =
- let
- fun secs prfx time = prfx ^ Time.toString time;
- val {name, timer, sys, usr, gc, count} = time_check ti;
- in
- warning ("Total of " ^ quote name ^ ": " ^
- secs "User " usr ^ secs " GC " gc ^ secs " All " (Time.+ (sys, Time.+ (usr, gc))) ^
- " secs in " ^ string_of_int count ^ " calls");
- time_reset ti
- end;
-
-val time_finish_hooks = ref ([]: (unit -> unit) list);
-
-in
-
-fun time_accumulator name =
- let val ti = time_init name in
- CRITICAL (fn () => change time_finish_hooks (cons (fn () => time_finish ti)));
- time_add ti
- end;
-
-fun accumulated_time () = List.app (fn f => f ()) (! time_finish_hooks);
-
-end;
-
end;
structure BasicOutput: BASIC_OUTPUT = Output;
--- a/src/Pure/IsaMakefile Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/IsaMakefile Thu Jun 18 00:00:52 2009 +0200
@@ -29,7 +29,8 @@
ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
- ML-Systems/time_limit.ML ML-Systems/universal.ML
+ ML-Systems/timing.ML ML-Systems/time_limit.ML \
+ ML-Systems/universal.ML
RAW: $(OUT)/RAW
--- a/src/Pure/ML-Systems/mosml.ML Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/ML-Systems/mosml.ML Thu Jun 18 00:00:52 2009 +0200
@@ -154,10 +154,6 @@
val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => "";
in {message = message, user = user, all = all} end;
-fun check_timer timer =
- let val {sys, usr, gc} = Timer.checkCPUTimer timer
- in (sys, usr, gc) end;
-
(* SML basis library fixes *)
--- a/src/Pure/ML-Systems/polyml_common.ML Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML Thu Jun 18 00:00:52 2009 +0200
@@ -8,6 +8,7 @@
use "ML-Systems/exn.ML";
use "ML-Systems/multithreading.ML";
use "ML-Systems/time_limit.ML";
+use "ML-Systems/timing.ML";
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_pretty.ML";
use "ML-Systems/use_context.ML";
@@ -41,30 +42,6 @@
val implode = SML90.implode;
-(* compiler-independent timing functions *)
-
-fun start_timing () =
- let
- val timer = Timer.startCPUTimer ();
- val time = Timer.checkCPUTimer timer;
- in (timer, time) end;
-
-fun end_timing (timer, {sys, usr}) =
- let
- open Time; (*...for Time.toString, Time.+ and Time.- *)
- val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
- val user = usr2 - usr;
- val all = user + sys2 - sys;
- val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => "";
- in {message = message, user = user, all = all} end;
-
-fun check_timer timer =
- let
- val {sys, usr} = Timer.checkCPUTimer timer;
- val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *)
- in (sys, usr, gc) end;
-
-
(* prompts *)
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
--- a/src/Pure/ML-Systems/smlnj.ML Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Thu Jun 18 00:00:52 2009 +0200
@@ -12,6 +12,7 @@
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/multithreading.ML";
+use "ML-Systems/timing.ML";
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/ml_pretty.ML";
@@ -59,30 +60,6 @@
end;
-(* compiler-independent timing functions *)
-
-fun start_timing () =
- let
- val timer = Timer.startCPUTimer ();
- val time = Timer.checkCPUTimer timer;
- in (timer, time) end;
-
-fun end_timing (timer, {sys, usr}) =
- let
- open Time; (*...for Time.toString, Time.+ and Time.- *)
- val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
- val user = usr2 - usr;
- val all = user + sys2 - sys;
- val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => "";
- in {message = message, user = user, all = all} end;
-
-fun check_timer timer =
- let
- val {sys, usr} = Timer.checkCPUTimer timer;
- val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *)
- in (sys, usr, gc) end;
-
-
(*prompts*)
fun ml_prompts p1 p2 =
(Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/timing.ML Thu Jun 18 00:00:52 2009 +0200
@@ -0,0 +1,32 @@
+(* Title: Pure/ML-Systems/timing.ML
+ Author: Makarius
+
+Compiler-independent timing functions.
+*)
+
+fun start_timing () =
+ let
+ val real_timer = Timer.startRealTimer ();
+ val real_time = Timer.checkRealTimer real_timer;
+ val cpu_timer = Timer.startCPUTimer ();
+ val cpu_times = Timer.checkCPUTimes cpu_timer;
+ in (real_timer, real_time, cpu_timer, cpu_times) end;
+
+fun end_timing (real_timer, real_time, cpu_timer, cpu_times) =
+ let
+ val real_time2 = Timer.checkRealTimer real_timer;
+ val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
+ val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
+ Timer.checkCPUTimes cpu_timer;
+
+ open Time;
+ val elapsed = real_time2 - real_time;
+ val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
+ val cpu = usr2 - usr + sys2 - sys + gc;
+ val gc_percent = Real.fmt (StringCvt.FIX (SOME 1)) (100.0 * toReal gc / toReal cpu);
+ val factor = Real.fmt (StringCvt.FIX (SOME 2)) (toReal cpu / toReal elapsed);
+ val message =
+ (toString elapsed ^ "s elapsed time, " ^ toString cpu ^ "s cpu time, " ^
+ gc_percent ^ "% GC time, factor " ^ factor) handle Time => "";
+ in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
+
--- a/src/Pure/System/session.ML Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/System/session.ML Thu Jun 18 00:00:52 2009 +0200
@@ -9,8 +9,9 @@
val id: unit -> string list
val name: unit -> string
val welcome: unit -> string
- val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
- string -> string -> bool * string -> string -> int -> bool -> int -> int -> bool -> unit
+ val use_dir: string -> string -> bool -> string list -> bool -> bool ->
+ string -> bool -> string list -> string -> string -> bool * string ->
+ string -> int -> bool -> bool -> int -> int -> bool -> unit
val finish: unit -> unit
end;
@@ -72,8 +73,7 @@
(* finish *)
fun finish () =
- (Output.accumulated_time ();
- ThyInfo.finish ();
+ (ThyInfo.finish ();
Present.finish ();
Future.shutdown ();
session_finished := true);
@@ -92,13 +92,20 @@
fun dumping (_, "") = NONE
| dumping (cp, path) = SOME (cp, Path.explode path);
-fun use_dir root build modes reset info doc doc_graph doc_versions
- parent name dump rpath level verbose max_threads trace_threads parallel_proofs =
+fun use_dir item root build modes reset info doc doc_graph doc_versions parent
+ name dump rpath level timing verbose max_threads trace_threads parallel_proofs =
((fn () =>
(init reset parent name;
Present.init build info doc doc_graph doc_versions (path ()) name
(dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
- use root;
+ if timing then
+ let
+ val start = start_timing ();
+ val _ = use root;
+ val stop = end_timing start;
+ val _ = Output.std_error ("Timing " ^ item ^ " (" ^ #message stop ^ ")\n");
+ in () end
+ else use root;
finish ()))
|> setmp_noncritical Proofterm.proofs level
|> setmp_noncritical print_mode (modes @ print_mode_value ())
--- a/src/Pure/Tools/find_consts.ML Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/Tools/find_consts.ML Thu Jun 18 00:00:52 2009 +0200
@@ -25,10 +25,9 @@
| Loose of string
| Name of string;
+
(* matching types/consts *)
-fun add_tye (_, (_, t)) n = Term.size_of_typ t + n;
-
fun matches_subtype thy typat =
let
val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
@@ -51,7 +50,9 @@
fun filter_const _ NONE = NONE
| filter_const f (SOME (c, r)) =
- Option.map (pair c o (curry Int.min r)) (f c);
+ (case f c of
+ NONE => NONE
+ | SOME i => SOME (c, Int.min (r, i)));
(* pretty results *)
@@ -76,6 +77,7 @@
Pretty.quote (Syntax.pretty_typ ctxt ty')]
end;
+
(* find_consts *)
fun find_consts ctxt raw_criteria =
@@ -85,16 +87,17 @@
val thy = ProofContext.theory_of ctxt;
val low_ranking = 10000;
- fun not_internal consts (nm, _) =
+ fun not_internal consts (nm, _) =
if member (op =) (Consts.the_tags consts nm) Markup.property_internal
then NONE else SOME low_ranking;
fun make_pattern crit =
let
val raw_T = Syntax.parse_typ ctxt crit;
- val t = Syntax.check_term
- (ProofContext.set_mode ProofContext.mode_pattern ctxt)
- (Term.dummy_pattern raw_T);
+ val t =
+ Syntax.check_term
+ (ProofContext.set_mode ProofContext.mode_pattern ctxt)
+ (Term.dummy_pattern raw_T);
in Term.type_of t end;
fun make_match (Strict arg) =
@@ -102,34 +105,34 @@
fn (_, (ty, _)) =>
let
val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
- val sub_size = Vartab.fold add_tye tye 0;
+ val sub_size =
+ Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
in SOME sub_size end handle MATCH => NONE
end
-
| make_match (Loose arg) =
check_const (matches_subtype thy (make_pattern arg) o snd)
-
| make_match (Name arg) = check_const (match_string arg o fst);
fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
val criteria = map make_criterion raw_criteria;
val consts = Sign.consts_of thy;
- val (_, consts_tab) = (#constants o Consts.dest) consts;
- fun eval_entry c = fold filter_const (not_internal consts::criteria)
- (SOME (c, low_ranking));
+ val (_, consts_tab) = #constants (Consts.dest consts);
+ fun eval_entry c =
+ fold filter_const (not_internal consts :: criteria)
+ (SOME (c, low_ranking));
val matches =
Symtab.fold (cons o eval_entry) consts_tab []
|> map_filter I
|> sort (rev_order o int_ord o pairself snd)
- |> map ((apsnd fst) o fst);
+ |> map (apsnd fst o fst);
- val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
+ val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
in
Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
:: Pretty.str ""
- :: (Pretty.str o concat)
+ :: (Pretty.str o implode)
(if null matches
then ["nothing found", end_msg]
else ["found ", (string_of_int o length) matches,
--- a/src/Pure/Tools/find_theorems.ML Wed Jun 17 17:42:46 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML Thu Jun 18 00:00:52 2009 +0200
@@ -282,7 +282,7 @@
in app (opt_add r r', consts', fs) end;
in app end;
-
+
in
fun filter_criterion ctxt opt_goal (b, c) =
@@ -417,7 +417,7 @@
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria;
val returned = length thms;
-
+
val tally_msg =
(case foundo of
NONE => "displaying " ^ string_of_int returned ^ " theorems"
@@ -427,7 +427,7 @@
then " (" ^ string_of_int returned ^ " displayed)"
else ""));
- val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
+ val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
in
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
:: Pretty.str "" ::