--- a/NEWS Fri Aug 27 14:24:26 2010 +0200
+++ b/NEWS Fri Aug 27 14:25:07 2010 +0200
@@ -40,6 +40,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/Codegen/Thy/Introduction.thy Fri Aug 27 14:24:26 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Fri Aug 27 14:25:07 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/IsarRef/Thy/HOL_Specific.thy Fri Aug 27 14:24:26 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Aug 27 14:25:07 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/manual.bib Fri Aug 27 14:24:26 2010 +0200
+++ b/doc-src/manual.bib Fri Aug 27 14:25:07 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},