# HG changeset patch # User haftmann # Date 1245276052 -7200 # Node ID b6710a3b4c497b13f1b5404e63c211ebda67be11 # Parent 36c5c15597f2830109d4c5a7c75100c32b1f8d15# Parent 9fc407df200ca2d0ee04c55850edcaf64443aab0 merged diff -r 9fc407df200c -r b6710a3b4c49 Admin/isatest/settings/at-mac-poly-5.1-para --- 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" diff -r 9fc407df200c -r b6710a3b4c49 doc-src/Classes/Thy/Classes.thy --- 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 \ p\<^isub>2 = (fst p\<^isub>1 \ fst p\<^isub>2, snd p\<^isub>1 \ snd p\<^isub>2)" + mult_prod_def: "p1 \ p2 = (fst p1 \ fst p2, snd p1 \ snd p2)" instance %quote proof - fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\\semigroup \ \\semigroup" - show "p\<^isub>1 \ p\<^isub>2 \ p\<^isub>3 = p\<^isub>1 \ (p\<^isub>2 \ p\<^isub>3)" + fix p1 p2 p3 :: "\\semigroup \ \\semigroup" + show "p1 \ p2 \ p3 = p1 \ (p2 \ 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 "(\)"} 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 \ \ \ \" 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)}*} diff -r 9fc407df200c -r b6710a3b4c49 doc-src/Classes/Thy/document/Classes.tex --- 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})\\ diff -r 9fc407df200c -r b6710a3b4c49 doc-src/Classes/classes.tex --- 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. diff -r 9fc407df200c -r b6710a3b4c49 doc-src/System/Thy/Presentation.thy --- 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. diff -r 9fc407df200c -r b6710a3b4c49 doc-src/System/Thy/document/Presentation.tex --- 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. diff -r 9fc407df200c -r b6710a3b4c49 lib/Tools/usedir --- 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 .. diff -r 9fc407df200c -r b6710a3b4c49 lib/scripts/polyml-version --- 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 diff -r 9fc407df200c -r b6710a3b4c49 src/HOL/Tools/datatype_package/datatype_package.ML --- 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); diff -r 9fc407df200c -r b6710a3b4c49 src/Pure/General/output.ML --- 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; diff -r 9fc407df200c -r b6710a3b4c49 src/Pure/IsaMakefile --- 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 diff -r 9fc407df200c -r b6710a3b4c49 src/Pure/ML-Systems/mosml.ML --- 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 *) diff -r 9fc407df200c -r b6710a3b4c49 src/Pure/ML-Systems/polyml_common.ML --- 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); diff -r 9fc407df200c -r b6710a3b4c49 src/Pure/ML-Systems/smlnj.ML --- 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); diff -r 9fc407df200c -r b6710a3b4c49 src/Pure/ML-Systems/timing.ML --- /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; + diff -r 9fc407df200c -r b6710a3b4c49 src/Pure/System/session.ML --- 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 ()) diff -r 9fc407df200c -r b6710a3b4c49 src/Pure/Tools/find_consts.ML --- 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, diff -r 9fc407df200c -r b6710a3b4c49 src/Pure/Tools/find_theorems.ML --- 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 "" ::