--- a/NEWS Fri Aug 27 12:57:55 2010 +0200
+++ b/NEWS Fri Aug 27 14:25:29 2010 +0200
@@ -56,6 +56,9 @@
*** HOL ***
+* Scala (2.8 or higher) has been added to the target languages of
+the code generator.
+
* Dropped type classes mult_mono and mult_mono1. INCOMPATIBILITY.
* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
--- a/doc-src/Classes/Thy/Classes.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy Fri Aug 27 14:25:29 2010 +0200
@@ -8,14 +8,14 @@
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}.
- As a canonical example, a polymorphic equality function
- @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different
- types for @{text "\<alpha>"}, which is achieved by splitting introduction
- of the @{text eq} function from its overloaded definitions by means
- of @{text class} and @{text instance} declarations:
- \footnote{syntax here is a kind of isabellized Haskell}
+ to classical Haskell 1.0 type classes, not considering later
+ additions in expressiveness}. As a canonical example, a polymorphic
+ equality function @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on
+ different types for @{text "\<alpha>"}, which is achieved by splitting
+ introduction of the @{text eq} function from its overloaded
+ definitions by means of @{text class} and @{text instance}
+ declarations: \footnote{syntax here is a kind of isabellized
+ Haskell}
\begin{quote}
@@ -41,14 +41,14 @@
these annotations are assertions that a particular polymorphic type
provides definitions for overloaded functions.
- Indeed, type classes not only allow for simple overloading
- but form a generic calculus, an instance of order-sorted
- algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
+ Indeed, type classes not only allow for simple overloading but form
+ a generic calculus, an instance of order-sorted algebra
+ \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
- 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
+ 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
implementations must obey. For example, the @{text "class eq"}
above could be given the following specification, demanding that
@{text "class eq"} is an equivalence relation obeying reflexivity,
@@ -65,11 +65,10 @@
\end{quote}
- \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
- all those aspects together:
+ \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 all those aspects together:
\begin{enumerate}
\item specifying abstract parameters together with
@@ -81,15 +80,15 @@
locales \cite{kammueller-locales}.
\end{enumerate}
- \noindent Isar type classes also directly support code generation
- in a Haskell like fashion. Internally, they are mapped to more primitive
- Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
+ \noindent Isar type classes also directly support code generation 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.
+ 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.
*}
section {* A simple algebra example \label{sec:example} *}
@@ -107,25 +106,24 @@
assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
text {*
- \noindent This @{command class} specification consists of two
- parts: the \qn{operational} part names the class parameter
- (@{element "fixes"}), the \qn{logical} part specifies properties on them
- (@{element "assumes"}). The local @{element "fixes"} and
- @{element "assumes"} are lifted to the theory toplevel,
- yielding the global
+ \noindent This @{command class} specification consists of two parts:
+ the \qn{operational} part names the class parameter (@{element
+ "fixes"}), the \qn{logical} part specifies properties on them
+ (@{element "assumes"}). The local @{element "fixes"} and @{element
+ "assumes"} are lifted to the theory toplevel, yielding the global
parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
- global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y
- z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
+ global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y z \<Colon>
+ \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
*}
subsection {* Class instantiation \label{sec:class_inst} *}
text {*
- The concrete type @{typ int} is made a @{class semigroup}
- instance by providing a suitable definition for the class parameter
- @{text "(\<otimes>)"} and a proof for the specification of @{fact assoc}.
- This is accomplished by the @{command instantiation} target:
+ The concrete type @{typ int} is made a @{class semigroup} instance
+ by providing a suitable definition for the class parameter @{text
+ "(\<otimes>)"} and a proof for the specification of @{fact assoc}. This is
+ accomplished by the @{command instantiation} target:
*}
instantiation %quote int :: semigroup
@@ -143,22 +141,22 @@
end %quote
text {*
- \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 reduces an instance judgement to the relevant primitive
- proof goals; typically it is the first method applied
- in an instantiation proof.
+ \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 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.
+ 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} yields the natural numbers:
+ \medskip Another instance of @{class semigroup} yields the natural
+ numbers:
*}
instantiation %quote nat :: semigroup
@@ -177,21 +175,20 @@
end %quote
text {*
- \noindent Note the occurence of the name @{text mult_nat}
- in the primrec declaration; by default, the local name of
- a class operation @{text f} to be instantiated on type constructor
- @{text \<kappa>} is mangled as @{text f_\<kappa>}. In case of uncertainty,
- these names may be inspected using the @{command "print_context"} command
- or the corresponding ProofGeneral button.
+ \noindent Note the occurence of the name @{text mult_nat} in the
+ primrec declaration; by default, the local name of a class operation
+ @{text f} to be instantiated on type constructor @{text \<kappa>} is
+ mangled as @{text f_\<kappa>}. In case of uncertainty, these names may be
+ inspected using the @{command "print_context"} command or the
+ corresponding ProofGeneral button.
*}
subsection {* Lifting and parametric types *}
text {*
- 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:
+ 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:
*}
instantiation %quote prod :: (semigroup, semigroup) semigroup
@@ -211,21 +208,19 @@
text {*
\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 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.
+ associativity of the type components; these hypotheses 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.
*}
subsection {* Subclassing *}
text {*
- 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 characteristic property:
+ 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 characteristic property:
*}
class %quote monoidl = semigroup +
@@ -233,10 +228,10 @@
assumes neutl: "\<one> \<otimes> x = x"
text {*
- \noindent Again, we prove some instances, by
- providing suitable parameter definitions and proofs for the
- additional specifications. Observe that instantiations
- for types with the same arity may be simultaneous:
+ \noindent Again, we prove some instances, by providing suitable
+ parameter definitions and proofs for the additional specifications.
+ Observe that instantiations for types with the same arity may be
+ simultaneous:
*}
instantiation %quote nat and int :: monoidl
@@ -309,8 +304,8 @@
end %quote
text {*
- \noindent To finish our small algebra example, we add a @{text group} class
- with a corresponding instance:
+ \noindent To finish our small algebra example, we add a @{text
+ group} class with a corresponding instance:
*}
class %quote group = monoidl +
@@ -338,9 +333,9 @@
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
+ 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 other than a locale:
*}
@@ -402,13 +397,14 @@
qed
text {*
- \noindent Here the \qt{@{keyword "in"} @{class group}} target specification
- indicates that the result is recorded within that context for later
- use. This local theorem is also lifted to the global one @{fact
- "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
- z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been made an instance of
- @{text "group"} before, we may refer to that fact as well: @{prop
- [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
+ \noindent Here the \qt{@{keyword "in"} @{class group}} target
+ specification indicates that the result is recorded within that
+ context for later use. This local theorem is also lifted to the
+ global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon>
+ \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been
+ made an instance of @{text "group"} before, we may refer to that
+ fact as well: @{prop [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y =
+ z"}.
*}
@@ -424,15 +420,14 @@
text {*
\noindent If the locale @{text group} is also a class, this local
- definition is propagated onto a global definition of
- @{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"}
- with corresponding theorems
+ definition is propagated onto a global definition of @{term [source]
+ "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} with corresponding theorems
@{thm pow_nat.simps [no_vars]}.
- \noindent As you can see from this example, for local
- definitions you may use any specification tool
- which works together with locales, such as Krauss's recursive function package
+ \noindent As you can see from this example, for local definitions
+ you may use any specification tool which works together with
+ locales, such as Krauss's recursive function package
\cite{krauss2006}.
*}
@@ -440,19 +435,17 @@
subsection {* A functor analogy *}
text {*
- 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 that have
- a canonical interpretation as type classes.
- 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 can simply make a particular interpretation
- of monoids for lists:
+ 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 that have a canonical interpretation as type classes.
+ 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 can simply make a particular interpretation of monoids
+ for lists:
*}
interpretation %quote list_monoid: monoid append "[]"
@@ -510,12 +503,10 @@
qed
text {*
- The logical proof is carried out on the locale level.
- Afterwards it is propagated
- to the type system, making @{text group} an instance of
- @{text monoid} by adding an additional edge
- to the graph of subclass relations
- (\figref{fig:subclass}).
+ The logical proof is carried out on the locale level. Afterwards it
+ is propagated to the type system, making @{text group} an instance
+ of @{text monoid} by adding an additional edge to the graph of
+ subclass relations (\figref{fig:subclass}).
\begin{figure}[htbp]
\begin{center}
@@ -547,8 +538,8 @@
\end{center}
\end{figure}
- For illustration, a derived definition
- in @{text group} using @{text pow_nat}
+ For illustration, a derived definition in @{text group} using @{text
+ pow_nat}
*}
definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
@@ -557,17 +548,17 @@
else (pow_nat (nat (- k)) x)\<div>)"
text {*
- \noindent yields the global definition of
- @{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
- with the corresponding theorem @{thm pow_int_def [no_vars]}.
+ \noindent yields the global definition of @{term [source] "pow_int \<Colon>
+ int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} with the corresponding theorem @{thm
+ pow_int_def [no_vars]}.
*}
subsection {* A note on syntax *}
text {*
- As a convenience, class context syntax allows references
- to local class operations and their global counterparts
- uniformly; type inference resolves ambiguities. For example:
+ As a convenience, class context syntax allows references to local
+ class operations and their global counterparts uniformly; type
+ inference resolves ambiguities. For example:
*}
context %quote semigroup
@@ -581,11 +572,11 @@
term %quote "x \<otimes> y" -- {* example 3 *}
text {*
- \noindent Here in example 1, the term refers to the local class operation
- @{text "mult [\<alpha>]"}, whereas in example 2 the type constraint
- enforces the global class operation @{text "mult [nat]"}.
- In the global context in example 3, the reference is
- to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
+ \noindent Here in example 1, the term refers to the local class
+ operation @{text "mult [\<alpha>]"}, whereas in example 2 the type
+ constraint enforces the global class operation @{text "mult [nat]"}.
+ In the global context in example 3, the reference is to the
+ polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
*}
section {* Further issues *}
@@ -593,16 +584,14 @@
subsection {* Type classes and code generation *}
text {*
- Turning back to the first motivation for type classes,
- namely overloading, it is obvious that overloading
- stemming from @{command class} statements and
- @{command instantiation}
- targets naturally maps to Haskell type classes.
- The code generator framework \cite{isabelle-codegen}
- 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:
+ Turning back to the first motivation for type classes, namely
+ overloading, it is obvious that overloading stemming from @{command
+ class} statements and @{command instantiation} targets naturally
+ maps to Haskell type classes. The code generator framework
+ \cite{isabelle-codegen} 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:
*}
definition %quote example :: int where
@@ -619,11 +608,18 @@
*}
text %quote {*@{code_stmts example (SML)}*}
+text {*
+ \noindent In Scala, implicts are used as dictionaries:
+*}
+(*<*)code_include %invisible Scala "Natural" -(*>*)
+text %quote {*@{code_stmts example (Scala)}*}
+
+
subsection {* Inspecting the type class universe *}
text {*
- To facilitate orientation in complex subclass structures,
- two diagnostics commands are provided:
+ To facilitate orientation in complex subclass structures, two
+ diagnostics commands are provided:
\begin{description}
--- a/doc-src/Classes/Thy/document/Classes.tex Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Fri Aug 27 14:25:29 2010 +0200
@@ -26,14 +26,14 @@
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}.
- As a canonical example, a polymorphic equality function
- \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different
- types for \isa{{\isasymalpha}}, which is achieved by splitting introduction
- of the \isa{eq} function from its overloaded definitions by means
- of \isa{class} and \isa{instance} declarations:
- \footnote{syntax here is a kind of isabellized Haskell}
+ to classical Haskell 1.0 type classes, not considering later
+ additions in expressiveness}. As a canonical example, a polymorphic
+ equality function \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on
+ different types for \isa{{\isasymalpha}}, which is achieved by splitting
+ introduction of the \isa{eq} function from its overloaded
+ definitions by means of \isa{class} and \isa{instance}
+ declarations: \footnote{syntax here is a kind of isabellized
+ Haskell}
\begin{quote}
@@ -59,14 +59,14 @@
these annotations are assertions that a particular polymorphic type
provides definitions for overloaded functions.
- Indeed, type classes not only allow for simple overloading
- but form a generic calculus, an instance of order-sorted
- algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
+ Indeed, type classes not only allow for simple overloading but form
+ a generic calculus, an instance of order-sorted algebra
+ \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
- 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
+ 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
implementations must obey. For example, the \isa{class\ eq}
above could be given the following specification, demanding that
\isa{class\ eq} is an equivalence relation obeying reflexivity,
@@ -83,11 +83,10 @@
\end{quote}
- \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
- all those aspects together:
+ \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 all those aspects together:
\begin{enumerate}
\item specifying abstract parameters together with
@@ -99,15 +98,15 @@
locales \cite{kammueller-locales}.
\end{enumerate}
- \noindent Isar type classes also directly support code generation
- in a Haskell like fashion. Internally, they are mapped to more primitive
- Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
+ \noindent Isar type classes also directly support code generation 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.%
+ 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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -142,12 +141,9 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two
- parts: the \qn{operational} part names the class parameter
- (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
- (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}). The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and
- \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel,
- yielding the global
+\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two parts:
+ the \qn{operational} part names the class parameter (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
+ (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}). The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel, yielding the global
parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isachardot}assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
\end{isamarkuptext}%
@@ -158,10 +154,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The concrete type \isa{int} is made a \isa{semigroup}
- instance by providing a suitable definition for the class parameter
- \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}.
- This is accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
+The concrete type \isa{int} is made a \isa{semigroup} instance
+ by providing a suitable definition for the class parameter \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}. This is
+ accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -204,22 +199,19 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\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 reduces an instance judgement to the relevant primitive
- proof goals; typically it is the first method applied
- in an instantiation proof.
+\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 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.
+ 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} yields the natural numbers:%
+ \medskip Another instance of \isa{semigroup} yields the natural
+ numbers:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -259,12 +251,12 @@
\endisadelimquote
%
\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 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.%
+\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 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}%
\isamarkuptrue%
%
@@ -273,10 +265,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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:%
+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:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -318,11 +309,10 @@
\begin{isamarkuptext}%
\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 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.%
+ associativity of the type components; these hypotheses 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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -331,10 +321,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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 characteristic property:%
+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 characteristic property:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -355,10 +344,10 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Again, we prove some instances, by
- providing suitable parameter definitions and proofs for the
- additional specifications. Observe that instantiations
- for types with the same arity may be simultaneous:%
+\noindent Again, we prove some instances, by providing suitable
+ parameter definitions and proofs for the additional specifications.
+ Observe that instantiations for types with the same arity may be
+ simultaneous:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -505,8 +494,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent To finish our small algebra example, we add a \isa{group} class
- with a corresponding instance:%
+\noindent To finish our small algebra example, we add a \isa{group} class with a corresponding instance:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -563,9 +551,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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
+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 other than a locale:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -780,10 +768,12 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification
- indicates that the result is recorded within that context for later
- use. This local theorem is also lifted to the global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been made an instance of
- \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
+\noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target
+ specification indicates that the result is recorded within that
+ context for later use. This local theorem is also lifted to the
+ global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been
+ made an instance of \isa{group} before, we may refer to that
+ fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -814,16 +804,14 @@
%
\begin{isamarkuptext}%
\noindent If the locale \isa{group} is also a class, this local
- definition is propagated onto a global definition of
- \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
- with corresponding theorems
+ definition is propagated onto a global definition of \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}} with corresponding theorems
\isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
- \noindent As you can see from this example, for local
- definitions you may use any specification tool
- which works together with locales, such as Krauss's recursive function package
+ \noindent As you can see from this example, for local definitions
+ you may use any specification tool which works together with
+ locales, such as Krauss's recursive function package
\cite{krauss2006}.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -833,19 +821,17 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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 that have
- a canonical interpretation as type classes.
- 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 can simply make a particular interpretation
- of monoids for lists:%
+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 that have a canonical interpretation as type classes.
+ 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 can simply make a particular interpretation of monoids
+ for lists:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -969,12 +955,10 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-The logical proof is carried out on the locale level.
- Afterwards it is propagated
- to the type system, making \isa{group} an instance of
- \isa{monoid} by adding an additional edge
- to the graph of subclass relations
- (\figref{fig:subclass}).
+The logical proof is carried out on the locale level. Afterwards it
+ is propagated to the type system, making \isa{group} an instance
+ of \isa{monoid} by adding an additional edge to the graph of
+ subclass relations (\figref{fig:subclass}).
\begin{figure}[htbp]
\begin{center}
@@ -1006,8 +990,7 @@
\end{center}
\end{figure}
- For illustration, a derived definition
- in \isa{group} using \isa{pow{\isacharunderscore}nat}%
+ For illustration, a derived definition in \isa{group} using \isa{pow{\isacharunderscore}nat}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1029,9 +1012,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent yields the global definition of
- \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
- with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
+\noindent yields the global definition of \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}} with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1040,9 +1021,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-As a convenience, class context syntax allows references
- to local class operations and their global counterparts
- uniformly; type inference resolves ambiguities. For example:%
+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}%
\isamarkuptrue%
%
@@ -1082,11 +1063,11 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Here in example 1, the term refers to the local class operation
- \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
- enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
- In the global context in example 3, the reference is
- to the polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
+\noindent Here in example 1, the term refers to the local class
+ operation \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type
+ constraint enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
+ In the global context in example 3, the reference is to the
+ polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1099,16 +1080,13 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Turning back to the first motivation for type classes,
- namely overloading, it is obvious that overloading
- stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and
- \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. 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:%
+Turning back to the first motivation for type classes, namely
+ overloading, it is obvious that overloading stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and \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. 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%
%
@@ -1328,13 +1306,121 @@
%
\endisadelimquote
%
+\begin{isamarkuptext}%
+\noindent In Scala, implicts are used as dictionaries:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}object Example {\char123}\\
+\hspace*{0pt}\\
+\hspace*{0pt}import /*implicits*/ Example.semigroup{\char95}int,~Example.monoidl{\char95}int,\\
+\hspace*{0pt} ~Example.monoid{\char95}int,~Example.group{\char95}int\\
+\hspace*{0pt}\\
+\hspace*{0pt}abstract sealed class nat\\
+\hspace*{0pt}final case object Zero{\char95}nat extends nat\\
+\hspace*{0pt}final case class Suc(a:~nat) extends nat\\
+\hspace*{0pt}\\
+\hspace*{0pt}def nat{\char95}aux(i:~BigInt,~n:~nat):~nat =\\
+\hspace*{0pt} ~(if (i <= BigInt(0)) n else nat{\char95}aux(i - BigInt(1),~Suc(n)))\\
+\hspace*{0pt}\\
+\hspace*{0pt}def nat(i:~BigInt):~nat = nat{\char95}aux(i,~Zero{\char95}nat)\\
+\hspace*{0pt}\\
+\hspace*{0pt}trait semigroup[A] {\char123}\\
+\hspace*{0pt} ~val `Example+mult`:~(A,~A) => A\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}def mult[A](a:~A,~b:~A)(implicit A:~semigroup[A]):~A =\\
+\hspace*{0pt} ~A.`Example+mult`(a,~b)\\
+\hspace*{0pt}\\
+\hspace*{0pt}trait monoidl[A] extends semigroup[A] {\char123}\\
+\hspace*{0pt} ~val `Example+neutral`:~A\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}def neutral[A](implicit A:~monoidl[A]):~A = A.`Example+neutral`\\
+\hspace*{0pt}\\
+\hspace*{0pt}trait monoid[A] extends monoidl[A] {\char123}\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}\\
+\hspace*{0pt}trait group[A] extends monoid[A] {\char123}\\
+\hspace*{0pt} ~val `Example+inverse`:~A => A\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}def inverse[A](a:~A)(implicit A:~group[A]):~A = A.`Example+inverse`(a)\\
+\hspace*{0pt}\\
+\hspace*{0pt}def pow{\char95}nat[A:~monoid](xa0:~nat,~x:~A):~A = (xa0,~x) match {\char123}\\
+\hspace*{0pt} ~case (Zero{\char95}nat,~x) => neutral[A]\\
+\hspace*{0pt} ~case (Suc(n),~x) => mult[A](x,~pow{\char95}nat[A](n,~x))\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}\\
+\hspace*{0pt}def pow{\char95}int[A:~group](k:~BigInt,~x:~A):~A =\\
+\hspace*{0pt} ~(if (BigInt(0) <= k) pow{\char95}nat[A](nat(k),~x)\\
+\hspace*{0pt} ~~~else inverse[A](pow{\char95}nat[A](nat((- k)),~x)))\\
+\hspace*{0pt}\\
+\hspace*{0pt}def mult{\char95}int(i:~BigInt,~j:~BigInt):~BigInt = i + j\\
+\hspace*{0pt}\\
+\hspace*{0pt}implicit def semigroup{\char95}int:~semigroup[BigInt] = new semigroup[BigInt] {\char123}\\
+\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}\\
+\hspace*{0pt}def neutral{\char95}int:~BigInt = BigInt(0)\\
+\hspace*{0pt}\\
+\hspace*{0pt}implicit def monoidl{\char95}int:~monoidl[BigInt] = new monoidl[BigInt] {\char123}\\
+\hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\
+\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}\\
+\hspace*{0pt}implicit def monoid{\char95}int:~monoid[BigInt] = new monoid[BigInt] {\char123}\\
+\hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\
+\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}\\
+\hspace*{0pt}def inverse{\char95}int(i:~BigInt):~BigInt = (- i)\\
+\hspace*{0pt}\\
+\hspace*{0pt}implicit def group{\char95}int:~group[BigInt] = new group[BigInt] {\char123}\\
+\hspace*{0pt} ~val `Example+inverse` = (a:~BigInt) => inverse{\char95}int(a)\\
+\hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\
+\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\
+\hspace*{0pt}{\char125}\\
+\hspace*{0pt}\\
+\hspace*{0pt}def example:~BigInt = pow{\char95}int[BigInt](BigInt(10),~BigInt(- 2))\\
+\hspace*{0pt}\\
+\hspace*{0pt}{\char125}~/* object Example */%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
\isamarkupsubsection{Inspecting the type class universe%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-To facilitate orientation in complex subclass structures,
- two diagnostics commands are provided:
+To facilitate orientation in complex subclass structures, two
+ diagnostics commands are provided:
\begin{description}
--- a/doc-src/Codegen/Thy/Inductive_Predicate.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Fri Aug 27 14:25:29 2010 +0200
@@ -7,7 +7,7 @@
inductive %invisible append where
"append [] ys ys"
-| "append xs ys zs ==> append (x # xs) ys (x # zs)"
+| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
lemma %invisible append: "append xs ys zs = (xs @ ys = zs)"
by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
@@ -95,9 +95,9 @@
"append_i_i_o"}). You can specify your own names as follows:
*}
-code_pred %quote (modes: i => i => o => bool as concat,
- o => o => i => bool as split,
- i => o => i => bool as suffix) append .
+code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat,
+ o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split,
+ i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append .
subsection {* Alternative introduction rules *}
@@ -220,8 +220,8 @@
"values"} and the number of elements.
*}
-values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
-values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
+values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 20 "{n. tranclp succ 10 n}"
+values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 10 "{n. tranclp succ n 10}"
subsection {* Embedding into functional code within Isabelle/HOL *}
--- a/doc-src/Codegen/Thy/Introduction.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Fri Aug 27 14:25:29 2010 +0200
@@ -8,8 +8,9 @@
This tutorial introduces the code generator facilities of @{text
"Isabelle/HOL"}. It allows to turn (a certain class of) HOL
specifications into corresponding executable code in the programming
- languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml} and
- @{text Haskell} \cite{haskell-revised-report}.
+ languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml},
+ @{text Haskell} \cite{haskell-revised-report} and @{text Scala}
+ \cite{scala-overview-tech-report}.
To profit from this tutorial, some familiarity and experience with
@{theory HOL} \cite{isa-tutorial} and its basic theories is assumed.
@@ -78,8 +79,8 @@
target language identifier and a freely chosen module name. A file
name denotes the destination to store the generated code. Note that
the semantics of the destination depends on the target language: for
- @{text SML} and @{text OCaml} it denotes a \emph{file}, for @{text
- Haskell} it denotes a \emph{directory} where a file named as the
+ @{text SML}, @{text OCaml} and @{text Scala} it denotes a \emph{file},
+ for @{text Haskell} it denotes a \emph{directory} where a file named as the
module name (with extension @{text ".hs"}) is written:
*}
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Fri Aug 27 14:25:29 2010 +0200
@@ -240,7 +240,7 @@
\hspace*{0pt}structure Example :~sig\\
\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
\hspace*{0pt} ~datatype boola = True | False\\
-\hspace*{0pt} ~val anda :~boola -> boola -> boola\\
+\hspace*{0pt} ~val conj :~boola -> boola -> boola\\
\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> boola\\
\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> boola\\
\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> boola\\
@@ -250,17 +250,17 @@
\hspace*{0pt}\\
\hspace*{0pt}datatype boola = True | False;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun anda p True = p\\
-\hspace*{0pt} ~| anda p False = False\\
-\hspace*{0pt} ~| anda True p = p\\
-\hspace*{0pt} ~| anda False p = False;\\
+\hspace*{0pt}fun conj p True = p\\
+\hspace*{0pt} ~| conj p False = False\\
+\hspace*{0pt} ~| conj True p = p\\
+\hspace*{0pt} ~| conj False p = False;\\
\hspace*{0pt}\\
\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
+\hspace*{0pt}fun in{\char95}interval (k,~l) n = conj (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Fri Aug 27 14:25:29 2010 +0200
@@ -212,9 +212,9 @@
%
\isatagquote
\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
-\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool\ as\ concat{\isacharcomma}\isanewline
-\ \ o\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ split{\isacharcomma}\isanewline
-\ \ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool\ as\ concat{\isacharcomma}\isanewline
+\ \ o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool\ as\ split{\isacharcomma}\isanewline
+\ \ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
@@ -422,9 +422,9 @@
%
\isatagquote
\isacommand{values}\isamarkupfalse%
-\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isacommand{values}\isamarkupfalse%
-\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}%
+\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Fri Aug 27 14:25:29 2010 +0200
@@ -25,8 +25,9 @@
\begin{isamarkuptext}%
This tutorial introduces the code generator facilities of \isa{Isabelle{\isacharslash}HOL}. It allows to turn (a certain class of) HOL
specifications into corresponding executable code in the programming
- languages \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml} and
- \isa{Haskell} \cite{haskell-revised-report}.
+ languages \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml},
+ \isa{Haskell} \cite{haskell-revised-report} and \isa{Scala}
+ \cite{scala-overview-tech-report}.
To profit from this tutorial, some familiarity and experience with
\hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \cite{isa-tutorial} and its basic theories is assumed.%
@@ -191,7 +192,8 @@
target language identifier and a freely chosen module name. A file
name denotes the destination to store the generated code. Note that
the semantics of the destination depends on the target language: for
- \isa{SML} and \isa{OCaml} it denotes a \emph{file}, for \isa{Haskell} it denotes a \emph{directory} where a file named as the
+ \isa{SML}, \isa{OCaml} and \isa{Scala} it denotes a \emph{file},
+ for \isa{Haskell} it denotes a \emph{directory} where a file named as the
module name (with extension \isa{{\isachardot}hs}) is written:%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/pictures/architecture.tex Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/pictures/architecture.tex Fri Aug 27 14:25:29 2010 +0200
@@ -30,8 +30,8 @@
\node (seri) at (1.5, 0) [process, positive] {serialisation};
\node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
\node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
- \node (further) at (2.5, 1) [entity, positive] {(\ldots)};
- \node (Haskell) at (2.5, 0) [entity, positive] {\sys{Haskell}};
+ \node (Haskell) at (2.5, 1) [entity, positive] {\sys{Haskell}};
+ \node (Scala) at (2.5, 0) [entity, positive] {\sys{Scala}};
\draw [semithick] (spec) -- (spec_user_join);
\draw [semithick] (user) -- (spec_user_join);
\draw [-diamond, semithick] (spec_user_join) -- (raw);
@@ -41,8 +41,8 @@
\draw [arrow] (iml) -- (seri);
\draw [arrow] (seri) -- (SML);
\draw [arrow] (seri) -- (OCaml);
- \draw [arrow, dashed] (seri) -- (further);
\draw [arrow] (seri) -- (Haskell);
+ \draw [arrow] (seri) -- (Scala);
\end{tikzpicture}
}
--- a/doc-src/Codegen/codegen.tex Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/codegen.tex Fri Aug 27 14:25:29 2010 +0200
@@ -22,7 +22,7 @@
\begin{abstract}
\noindent This tutorial introduces the code generator facilities of Isabelle/HOL.
They empower the user to turn HOL specifications into corresponding executable
- programs in the languages SML, OCaml and Haskell.
+ programs in the languages SML, OCaml, Haskell and Scala.
\end{abstract}
\thispagestyle{empty}\clearpage
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Aug 27 14:25:29 2010 +0200
@@ -968,7 +968,8 @@
\medskip One framework generates code from functional programs
(including overloading using type classes) to SML \cite{SML}, OCaml
- \cite{OCaml} and Haskell \cite{haskell-revised-report}.
+ \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
+ \cite{scala-overview-tech-report}.
Conceptually, code generation is split up in three steps:
\emph{selection} of code theorems, \emph{translation} into an
abstract executable view and \emph{serialization} to a specific
@@ -1015,7 +1016,7 @@
class: nameref
;
- target: 'OCaml' | 'SML' | 'Haskell'
+ target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
;
'code' ( 'del' | 'abstype' | 'abstract' ) ?
@@ -1088,7 +1089,7 @@
after the @{keyword "module_name"} keyword; then \emph{all} code is
placed in this module.
- For \emph{SML} and \emph{OCaml}, the file specification refers to a
+ For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
single file; for \emph{Haskell}, it refers to a whole directory,
where code is generated in multiple files reflecting the module
hierarchy. Omitting the file specification denotes standard
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Aug 27 14:25:29 2010 +0200
@@ -984,7 +984,8 @@
\medskip One framework generates code from functional programs
(including overloading using type classes) to SML \cite{SML}, OCaml
- \cite{OCaml} and Haskell \cite{haskell-revised-report}.
+ \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
+ \cite{scala-overview-tech-report}.
Conceptually, code generation is split up in three steps:
\emph{selection} of code theorems, \emph{translation} into an
abstract executable view and \emph{serialization} to a specific
@@ -1031,7 +1032,7 @@
class: nameref
;
- target: 'OCaml' | 'SML' | 'Haskell'
+ target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
;
'code' ( 'del' | 'abstype' | 'abstract' ) ?
@@ -1103,7 +1104,7 @@
after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
placed in this module.
- For \emph{SML} and \emph{OCaml}, the file specification refers to a
+ For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
single file; for \emph{Haskell}, it refers to a whole directory,
where code is generated in multiple files reflecting the module
hierarchy. Omitting the file specification denotes standard
--- a/doc-src/manual.bib Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/manual.bib Fri Aug 27 14:25:29 2010 +0200
@@ -984,6 +984,14 @@
%O
+@TechReport{scala-overview-tech-report,
+ author = {Martin Odersky and al.},
+ title = {An Overview of the Scala Programming Language},
+ institution = {EPFL Lausanne, Switzerland},
+ year = 2004,
+ number = {IC/2004/64}
+}
+
@Manual{pvs-language,
title = {The {PVS} specification language},
author = {S. Owre and N. Shankar and J. M. Rushby},
--- a/src/HOL/Library/Code_Natural.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy Fri Aug 27 14:25:29 2010 +0200
@@ -9,7 +9,9 @@
section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
code_include Haskell "Natural"
-{*newtype Natural = Natural Integer deriving (Eq, Show, Read);
+{*import Data.Array.ST;
+
+newtype Natural = Natural Integer deriving (Eq, Show, Read);
instance Num Natural where {
fromInteger k = Natural (if k >= 0 then k else 0);
@@ -50,6 +52,7 @@
| otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
};*}
+
code_reserved Haskell Natural
code_include Scala "Natural"
--- a/src/Tools/Code/code_scala.ML Fri Aug 27 12:57:55 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Fri Aug 27 14:25:29 2010 +0200
@@ -27,7 +27,6 @@
fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
args_num is_singleton_constr (deresolve, deresolve_full) =
let
- val deresolve_base = Long_Name.base_name o deresolve;
fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
@@ -135,7 +134,7 @@
fun print_context tyvars vs name = applify "[" "]"
(fn (v, sort) => (Pretty.block o map str)
(lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
- NOBR ((str o deresolve_base) name) vs;
+ NOBR ((str o deresolve) name) vs;
fun print_defhead tyvars vars name vs params tys ty =
Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
@@ -202,22 +201,22 @@
let
val tyvars = intro_tyvars vs reserved;
fun print_co ((co, _), []) =
- concat [str "final", str "case", str "object", (str o deresolve_base) co,
- str "extends", applify "[" "]" I NOBR ((str o deresolve_base) name)
+ concat [str "final", str "case", str "object", (str o deresolve) co,
+ str "extends", applify "[" "]" I NOBR ((str o deresolve) name)
(replicate (length vs) (str "Nothing"))]
| print_co ((co, vs_args), tys) =
concat [applify "(" ")"
(fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
(applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
- ["final", "case", "class", deresolve_base co]) vs_args)
+ ["final", "case", "class", deresolve co]) vs_args)
(Name.names (snd reserved) "a" tys),
str "extends",
applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
- ((str o deresolve_base) name) vs
+ ((str o deresolve) name) vs
];
in
Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
- NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_base name]) vs
+ NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
:: map print_co cos)
end
| print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
@@ -241,7 +240,7 @@
in
concat [str "def", constraint (Pretty.block [applify "(" ")"
(fn (aux, ty) => constraint ((str o lookup_var vars) aux)
- (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_base classparam))
+ (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
(auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
applify "(" ")" (str o lookup_var vars) NOBR
@@ -250,7 +249,7 @@
in
Pretty.chunks (
(Pretty.block_enclose
- (concat ([str "trait", (add_typarg o deresolve_base) name]
+ (concat ([str "trait", (add_typarg o deresolve) name]
@ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
(map print_classparam_val classparams))
:: map print_classparam_def classparams
@@ -289,7 +288,7 @@
datatype node =
Dummy
| Stmt of Code_Thingol.stmt
- | Module of ((Name.context * Name.context) * Name.context) * (string list * (string * node) Graph.T);
+ | Module of (string list * (string * node) Graph.T);
in
@@ -307,29 +306,53 @@
val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
(* building empty module hierarchy *)
- val empty_module = (((reserved, reserved), reserved), ([], Graph.empty));
+ val empty_module = ([], Graph.empty);
fun map_module f (Module content) = Module (f content);
- fun declare_module name_fragement ((nsp_class, nsp_object), nsp_common) =
- let
- val declare = Name.declare name_fragement;
- in ((declare nsp_class, declare nsp_object), declare nsp_common) end;
- fun ensure_module name_fragement (nsps, (implicits, nodes)) =
- if can (Graph.get_node nodes) name_fragement then (nsps, (implicits, nodes))
- else
- (nsps |> declare_module name_fragement, (implicits,
- nodes |> Graph.new_node (name_fragement, (name_fragement, Module empty_module))));
+ fun change_module [] = I
+ | change_module (name_fragment :: name_fragments) =
+ apsnd o Graph.map_node name_fragment o apsnd o map_module
+ o change_module name_fragments;
+ fun ensure_module name_fragment (implicits, nodes) =
+ if can (Graph.get_node nodes) name_fragment then (implicits, nodes)
+ else (implicits,
+ nodes |> Graph.new_node (name_fragment, (name_fragment, Module empty_module)));
fun allocate_module [] = I
| allocate_module (name_fragment :: name_fragments) =
ensure_module name_fragment
- #> (apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
+ #> (apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
fragments_tab empty_module;
- fun change_module [] = I
- | change_module (name_fragment :: name_fragments) =
- apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module
- o change_module name_fragments;
- (* statement declaration *)
+ (* distribute statements over hierarchy *)
+ fun add_stmt name stmt =
+ let
+ val (name_fragments, base) = dest_name name;
+ fun is_classinst stmt = case stmt
+ of Code_Thingol.Classinst _ => true
+ | _ => false;
+ val implicit_deps = filter (is_classinst o Graph.get_node program)
+ (Graph.imm_succs program name);
+ in
+ change_module name_fragments (fn (implicits, nodes) =>
+ (union (op =) implicit_deps implicits, Graph.new_node (name, (base, Stmt stmt)) nodes))
+ end;
+ fun add_dependency name name' =
+ let
+ val (name_fragments, base) = dest_name name;
+ val (name_fragments', base') = dest_name name';
+ val (name_fragments_common, (diff, diff')) =
+ chop_prefix (op =) (name_fragments, name_fragments');
+ val dep = if null diff then (name, name') else (hd diff, hd diff')
+ in (change_module name_fragments_common o apsnd) (Graph.add_edge dep) end;
+ val proto_program = empty_program
+ |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
+ |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
+
+ (* name declarations *)
+ fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
+ let
+ val declare = Name.declare name_fragment;
+ in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
fun namify_class base ((nsp_class, nsp_object), nsp_common) =
let
val (base', nsp_class') = yield_singleton Name.variants base nsp_class
@@ -346,70 +369,58 @@
(base',
((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
end;
- fun declare_stmt name stmt =
+ fun namify_stmt (Code_Thingol.Fun _) = namify_object
+ | namify_stmt (Code_Thingol.Datatype _) = namify_class
+ | namify_stmt (Code_Thingol.Datatypecons _) = namify_common true
+ | namify_stmt (Code_Thingol.Class _) = namify_class
+ | namify_stmt (Code_Thingol.Classrel _) = namify_object
+ | namify_stmt (Code_Thingol.Classparam _) = namify_object
+ | namify_stmt (Code_Thingol.Classinst _) = namify_common false;
+ fun make_declarations nsps (implicits, nodes) =
let
- val (name_fragments, base) = dest_name name;
- val namify = case stmt
- of Code_Thingol.Fun _ => namify_object
- | Code_Thingol.Datatype _ => namify_class
- | Code_Thingol.Datatypecons _ => namify_common true
- | Code_Thingol.Class _ => namify_class
- | Code_Thingol.Classrel _ => namify_object
- | Code_Thingol.Classparam _ => namify_object
- | Code_Thingol.Classinst _ => namify_common false;
- val stmt' = case stmt
- of Code_Thingol.Datatypecons _ => Dummy
- | Code_Thingol.Classrel _ => Dummy
- | Code_Thingol.Classparam _ => Dummy
- | _ => Stmt stmt;
- fun is_classinst stmt = case stmt
- of Code_Thingol.Classinst _ => true
- | _ => false;
- val implicit_deps = filter (is_classinst o Graph.get_node program)
- (Graph.imm_succs program name);
- fun declaration (nsps, (implicits, nodes)) =
+ val (module_fragments, stmt_names) = List.partition
+ (fn name_fragment => case Graph.get_node nodes name_fragment
+ of (_, Module _) => true | _ => false) (Graph.keys nodes);
+ fun modify_stmt (Stmt (Code_Thingol.Datatypecons _)) = Dummy
+ | modify_stmt (Stmt (Code_Thingol.Classrel _)) = Dummy
+ | modify_stmt (Stmt (Code_Thingol.Classparam _)) = Dummy
+ | modify_stmt stmt = stmt;
+ fun declare namify modify name (nsps, nodes) =
let
- val (base', nsps') = namify base nsps;
- val implicits' = union (op =) implicit_deps implicits;
- val nodes' = Graph.new_node (name, (base', stmt')) nodes;
- in (nsps', (implicits', nodes')) end;
- in change_module name_fragments declaration end;
-
- (* dependencies *)
- fun add_dependency name name' =
- let
- val (name_fragments, base) = dest_name name;
- val (name_fragments', base') = dest_name name';
- val (name_fragments_common, (diff, diff')) =
- chop_prefix (op =) (name_fragments, name_fragments');
- val dep = if null diff then (name, name') else (hd diff, hd diff')
- in (change_module name_fragments_common o apsnd o apsnd) (Graph.add_edge dep) end;
-
- (* producing program *)
- val (_, (_, sca_program)) = empty_program
- |> Graph.fold (fn (name, (stmt, _)) => declare_stmt name stmt) program
- |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
+ val (base, node) = Graph.get_node nodes name;
+ val (base', nsps') = namify node base nsps;
+ val nodes' = Graph.map_node name (K (base', modify node)) nodes;
+ in (nsps', nodes') end;
+ val (nsps', nodes') = (nsps, nodes)
+ |> fold (declare (K namify_module) I) module_fragments
+ |> fold (declare (namify_stmt o (fn Stmt stmt => stmt)) modify_stmt) stmt_names;
+ val nodes'' = nodes'
+ |> fold (fn name_fragment => (Graph.map_node name_fragment
+ o apsnd o map_module) (make_declarations nsps')) module_fragments;
+ in (implicits, nodes'') end;
+ val (_, sca_program) = make_declarations ((reserved, reserved), reserved) proto_program;
(* deresolving *)
- fun deresolve name =
+ fun deresolver prefix_fragments name =
let
val (name_fragments, _) = dest_name name;
- val nodes = fold (fn name_fragement => fn nodes => case Graph.get_node nodes name_fragement
- of (_, Module (_, (_, nodes))) => nodes) name_fragments sca_program;
+ val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
+ val nodes = fold (fn name_fragment => fn nodes => case Graph.get_node nodes name_fragment
+ of (_, Module (_, nodes)) => nodes) name_fragments sca_program;
val (base', _) = Graph.get_node nodes name;
- in Long_Name.implode (name_fragments @ [base']) end
+ in Long_Name.implode (remainder @ [base']) end
handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
- in (deresolve, sca_program) end;
+ in (deresolver, sca_program) end;
fun serialize_scala labelled_name raw_reserved includes module_alias
_ syntax_tyco syntax_const (code_of_pretty, code_writeln)
program (stmt_names, presentation_stmt_names) destination =
let
- (* preprocess program *)
+ (* build program *)
val reserved = fold (insert (op =) o fst) includes raw_reserved;
- val (deresolve, sca_program) = scala_program_of_program labelled_name
+ val (deresolver, sca_program) = scala_program_of_program labelled_name
(Name.make_context reserved) module_alias program;
(* print statements *)
@@ -430,41 +441,44 @@
of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
| _ => false;
val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
- (make_vars reserved) args_num is_singleton_constr
- (deresolve, Long_Name.implode o fst o split_last o Long_Name.explode (*FIXME full*));
+ (make_vars reserved) args_num is_singleton_constr;
(* print nodes *)
- fun print_implicit implicit =
+ fun print_implicit prefix_fragments implicit =
let
- val s = deresolve implicit;
+ val s = deresolver prefix_fragments implicit;
in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
- fun print_implicits implicits = case map_filter print_implicit implicits
- of [] => NONE
- | ps => (SOME o Pretty.block)
- (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
- fun print_module base implicits p = Pretty.chunks2
- ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
+ fun print_implicits prefix_fragments implicits =
+ case map_filter (print_implicit prefix_fragments) implicits
+ of [] => NONE
+ | ps => (SOME o Pretty.block)
+ (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
+ fun print_module prefix_fragments base implicits p = Pretty.chunks2
+ ([str ("object " ^ base ^ " {")] @ the_list (print_implicits prefix_fragments implicits)
@ [p, str ("} /* object " ^ base ^ " */")]);
- fun print_node (_, Dummy) = NONE
- | print_node (name, Stmt stmt) = if null presentation_stmt_names
+ fun print_node _ (_, Dummy) = NONE
+ | print_node prefix_fragments (name, Stmt stmt) =
+ if null presentation_stmt_names
orelse member (op =) presentation_stmt_names name
- then SOME (print_stmt (name, stmt))
+ then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
else NONE
- | print_node (name, Module (_, (implicits, nodes))) = if null presentation_stmt_names
- then case print_nodes nodes
+ | print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
+ if null presentation_stmt_names
+ then case print_nodes (prefix_fragments @ [name_fragment]) nodes
of NONE => NONE
- | SOME p => SOME (print_module (Long_Name.base_name name) implicits p)
- else print_nodes nodes
- and print_nodes nodes = let
- val ps = map_filter (fn name => print_node (name,
+ | SOME p => SOME (print_module prefix_fragments
+ (Long_Name.base_name name_fragment) implicits p)
+ else print_nodes [] nodes
+ and print_nodes prefix_fragments nodes = let
+ val ps = map_filter (fn name => print_node prefix_fragments (name,
snd (Graph.get_node nodes name)))
((rev o flat o Graph.strong_conn) nodes);
in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
(* serialization *)
val p_includes = if null presentation_stmt_names
- then map (fn (base, p) => print_module base [] p) includes else [];
- val p = Pretty.chunks2 (p_includes @ the_list (print_nodes sca_program));
+ then map (fn (base, p) => print_module [] base [] p) includes else [];
+ val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
in
Code_Target.mk_serialization target
(fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)