official support for Scala
authorhaftmann
Fri Aug 27 14:25:07 2010 +0200 (2010-08-27)
changeset 388144d575fbfc920
parent 38813 f50f0802ba99
child 38815 d0196406ee32
official support for Scala
NEWS
doc-src/Codegen/Thy/Introduction.thy
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/manual.bib
     1.1 --- a/NEWS	Fri Aug 27 14:24:26 2010 +0200
     1.2 +++ b/NEWS	Fri Aug 27 14:25:07 2010 +0200
     1.3 @@ -40,6 +40,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Scala (2.8 or higher) has been added to the target languages of
     1.8 +the code generator.
     1.9 +
    1.10  * Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.
    1.11  
    1.12  * Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
     2.1 --- a/doc-src/Codegen/Thy/Introduction.thy	Fri Aug 27 14:24:26 2010 +0200
     2.2 +++ b/doc-src/Codegen/Thy/Introduction.thy	Fri Aug 27 14:25:07 2010 +0200
     2.3 @@ -8,8 +8,9 @@
     2.4    This tutorial introduces the code generator facilities of @{text
     2.5    "Isabelle/HOL"}.  It allows to turn (a certain class of) HOL
     2.6    specifications into corresponding executable code in the programming
     2.7 -  languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml} and
     2.8 -  @{text Haskell} \cite{haskell-revised-report}.
     2.9 +  languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml},
    2.10 +  @{text Haskell} \cite{haskell-revised-report} and @{text Scala}
    2.11 +  \cite{scala-overview-tech-report}.
    2.12  
    2.13    To profit from this tutorial, some familiarity and experience with
    2.14    @{theory HOL} \cite{isa-tutorial} and its basic theories is assumed.
    2.15 @@ -78,8 +79,8 @@
    2.16    target language identifier and a freely chosen module name.  A file
    2.17    name denotes the destination to store the generated code.  Note that
    2.18    the semantics of the destination depends on the target language: for
    2.19 -  @{text SML} and @{text OCaml} it denotes a \emph{file}, for @{text
    2.20 -  Haskell} it denotes a \emph{directory} where a file named as the
    2.21 +  @{text SML}, @{text OCaml} and @{text Scala} it denotes a \emph{file},
    2.22 +  for @{text Haskell} it denotes a \emph{directory} where a file named as the
    2.23    module name (with extension @{text ".hs"}) is written:
    2.24  *}
    2.25  
     3.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Aug 27 14:24:26 2010 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Aug 27 14:25:07 2010 +0200
     3.3 @@ -968,7 +968,8 @@
     3.4  
     3.5    \medskip One framework generates code from functional programs
     3.6    (including overloading using type classes) to SML \cite{SML}, OCaml
     3.7 -  \cite{OCaml} and Haskell \cite{haskell-revised-report}.
     3.8 +  \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
     3.9 +  \cite{scala-overview-tech-report}.
    3.10    Conceptually, code generation is split up in three steps:
    3.11    \emph{selection} of code theorems, \emph{translation} into an
    3.12    abstract executable view and \emph{serialization} to a specific
    3.13 @@ -1015,7 +1016,7 @@
    3.14      class: nameref
    3.15      ;
    3.16  
    3.17 -    target: 'OCaml' | 'SML' | 'Haskell'
    3.18 +    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
    3.19      ;
    3.20  
    3.21      'code' ( 'del' | 'abstype' | 'abstract' ) ?
    3.22 @@ -1088,7 +1089,7 @@
    3.23    after the @{keyword "module_name"} keyword; then \emph{all} code is
    3.24    placed in this module.
    3.25  
    3.26 -  For \emph{SML} and \emph{OCaml}, the file specification refers to a
    3.27 +  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
    3.28    single file; for \emph{Haskell}, it refers to a whole directory,
    3.29    where code is generated in multiple files reflecting the module
    3.30    hierarchy.  Omitting the file specification denotes standard
     4.1 --- a/doc-src/manual.bib	Fri Aug 27 14:24:26 2010 +0200
     4.2 +++ b/doc-src/manual.bib	Fri Aug 27 14:25:07 2010 +0200
     4.3 @@ -984,6 +984,14 @@
     4.4  
     4.5  %O
     4.6  
     4.7 +@TechReport{scala-overview-tech-report,
     4.8 +  author =       {Martin Odersky and al.},
     4.9 +  title =        {An Overview of the Scala Programming Language},
    4.10 +  institution =  {EPFL Lausanne, Switzerland},
    4.11 +  year =         2004,
    4.12 +  number =       {IC/2004/64}
    4.13 +}
    4.14 +
    4.15  @Manual{pvs-language,
    4.16    title		= {The {PVS} specification language},
    4.17    author	= {S. Owre and N. Shankar and J. M. Rushby},