--- a/NEWS Mon Jun 14 21:49:25 2010 +0200
+++ b/NEWS Tue Jun 15 07:42:48 2010 +0200
@@ -28,6 +28,14 @@
* Removed simplifier congruence rule of "prod_case", as has for long
been the case with "split".
+* Datatype package: theorems generated for executable equality
+(class eq) carry proper names and are treated as default code
+equations.
+
+* List.thy: use various operations from the Haskell prelude when
+generating Haskell code.
+
+
New in Isabelle2009-2 (June 2010)
---------------------------------
--- a/doc-src/Codegen/Thy/Further.thy Mon Jun 14 21:49:25 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Tue Jun 15 07:42:48 2010 +0200
@@ -12,6 +12,87 @@
contains exhaustive syntax diagrams.
*}
+subsection {* Locales and interpretation *}
+
+text {*
+ A technical issue comes to surface when generating code from
+ specifications stemming from locale interpretation.
+
+ Let us assume a locale specifying a power operation
+ on arbitrary types:
+*}
+
+locale %quote power =
+ fixes power :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ assumes power_commute: "power x \<circ> power y = power y \<circ> power x"
+begin
+
+text {*
+ \noindent Inside that locale we can lift @{text power} to exponent lists
+ by means of specification relative to that locale:
+*}
+
+primrec %quote powers :: "'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
+ "powers [] = id"
+| "powers (x # xs) = power x \<circ> powers xs"
+
+lemma %quote powers_append:
+ "powers (xs @ ys) = powers xs \<circ> powers ys"
+ by (induct xs) simp_all
+
+lemma %quote powers_power:
+ "powers xs \<circ> power x = power x \<circ> powers xs"
+ by (induct xs)
+ (simp_all del: o_apply id_apply add: o_assoc [symmetric],
+ simp del: o_apply add: o_assoc power_commute)
+
+lemma %quote powers_rev:
+ "powers (rev xs) = powers xs"
+ by (induct xs) (simp_all add: powers_append powers_power)
+
+end %quote
+
+text {*
+ After an interpretation of this locale (say, @{command
+ interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f ::
+ 'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
+ "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code
+ can be generated. But this not the case: internally, the term
+ @{text "fun_power.powers"} is an abbreviation for the foundational
+ term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
+ (see \cite{isabelle-locale} for the details behind).
+
+ Furtunately, with minor effort the desired behaviour can be achieved.
+ First, a dedicated definition of the constant on which the local @{text "powers"}
+ after interpretation is supposed to be mapped on:
+*}
+
+definition %quote funpows :: "nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+ [code del]: "funpows = power.powers (\<lambda>n f. f ^^ n)"
+
+text {*
+ \noindent In general, the pattern is @{text "c = t"} where @{text c} is
+ the name of the future constant and @{text t} the foundational term
+ corresponding to the local constant after interpretation.
+
+ The interpretation itself is enriched with an equation @{text "t = c"}:
+*}
+
+interpretation %quote fun_power: power "\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n" where
+ "power.powers (\<lambda>n f. f ^^ n) = funpows"
+ by unfold_locales
+ (simp_all add: expand_fun_eq funpow_mult mult_commute funpows_def)
+
+text {*
+ \noindent This additional equation is trivially proved by the definition
+ itself.
+
+ After this setup procedure, code generation can continue as usual:
+*}
+
+text %quote {*@{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}*}
+
+
subsection {* Modules *}
text {*
--- a/doc-src/Codegen/Thy/Program.thy Mon Jun 14 21:49:25 2010 +0200
+++ b/doc-src/Codegen/Thy/Program.thy Tue Jun 15 07:42:48 2010 +0200
@@ -134,7 +134,8 @@
text {*
\noindent This is a convenient place to show how explicit dictionary construction
- manifests in generated code (here, the same example in @{text SML}):
+ manifests in generated code (here, the same example in @{text SML})
+ \cite{Haftmann-Nipkow:2010:code}:
*}
text %quote {*@{code_stmts bexp (SML)}*}
--- a/doc-src/Codegen/Thy/document/Further.tex Mon Jun 14 21:49:25 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Tue Jun 15 07:42:48 2010 +0200
@@ -33,6 +33,170 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Locales and interpretation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A technical issue comes to surface when generating code from
+ specifications stemming from locale interpretation.
+
+ Let us assume a locale specifying a power operation
+ on arbitrary types:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{locale}\isamarkupfalse%
+\ power\ {\isacharequal}\isanewline
+\ \ \isakeyword{fixes}\ power\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{assumes}\ power{\isacharunderscore}commute{\isacharcolon}\ {\isachardoublequoteopen}power\ x\ {\isasymcirc}\ power\ y\ {\isacharequal}\ power\ y\ {\isasymcirc}\ power\ x{\isachardoublequoteclose}\isanewline
+\isakeyword{begin}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Inside that locale we can lift \isa{power} to exponent lists
+ by means of specification relative to that locale:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{primrec}\isamarkupfalse%
+\ powers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}powers\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}powers\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ power\ x\ {\isasymcirc}\ powers\ xs{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ powers{\isacharunderscore}append{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}powers\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ powers\ xs\ {\isasymcirc}\ powers\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ powers{\isacharunderscore}power{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}powers\ xs\ {\isasymcirc}\ power\ x\ {\isacharequal}\ power\ x\ {\isasymcirc}\ powers\ xs{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\isanewline
+\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ del{\isacharcolon}\ o{\isacharunderscore}apply\ id{\isacharunderscore}apply\ add{\isacharcolon}\ o{\isacharunderscore}assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcomma}\isanewline
+\ \ \ \ \ \ simp\ del{\isacharcolon}\ o{\isacharunderscore}apply\ add{\isacharcolon}\ o{\isacharunderscore}assoc\ power{\isacharunderscore}commute{\isacharparenright}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ powers{\isacharunderscore}rev{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}powers\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ powers\ xs{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ powers{\isacharunderscore}append\ powers{\isacharunderscore}power{\isacharparenright}\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+After an interpretation of this locale (say, \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} \isa{fun{\isacharunderscore}power{\isacharcolon}} \isa{{\isachardoublequote}power\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}), one would expect to have a constant \isa{fun{\isacharunderscore}power{\isachardot}powers\ {\isacharcolon}{\isacharcolon}\ nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} for which code
+ can be generated. But this not the case: internally, the term
+ \isa{fun{\isacharunderscore}power{\isachardot}powers} is an abbreviation for the foundational
+ term \isa{{\isachardoublequote}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}
+ (see \cite{isabelle-locale} for the details behind).
+
+ Furtunately, with minor effort the desired behaviour can be achieved.
+ First, a dedicated definition of the constant on which the local \isa{powers}
+ after interpretation is supposed to be mapped on:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ funpows\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}funpows\ {\isacharequal}\ power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent In general, the pattern is \isa{c\ {\isacharequal}\ t} where \isa{c} is
+ the name of the future constant and \isa{t} the foundational term
+ corresponding to the local constant after interpretation.
+
+ The interpretation itself is enriched with an equation \isa{t\ {\isacharequal}\ c}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{interpretation}\isamarkupfalse%
+\ fun{\isacharunderscore}power{\isacharcolon}\ power\ {\isachardoublequoteopen}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}\ {\isacharequal}\ funpows{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ unfold{\isacharunderscore}locales\isanewline
+\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq\ funpow{\isacharunderscore}mult\ mult{\isacharunderscore}commute\ funpows{\isacharunderscore}def{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This additional equation is trivially proved by the definition
+ itself.
+
+ After this setup procedure, code generation can continue as usual:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
+\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
+\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
+\hspace*{0pt}\\
+\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
+\hspace*{0pt}funpows [] = id;\\
+\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
\isamarkupsubsection{Modules%
}
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Mon Jun 14 21:49:25 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Jun 15 07:42:48 2010 +0200
@@ -234,13 +234,6 @@
\noindent%
\hspace*{0pt}module Example where {\char123}\\
\hspace*{0pt}\\
-\hspace*{0pt}foldla ::~forall a b.~(a -> b -> a) -> a -> [b] -> a;\\
-\hspace*{0pt}foldla f a [] = a;\\
-\hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\
-\hspace*{0pt}\\
-\hspace*{0pt}rev ::~forall a.~[a] -> [a];\\
-\hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\
-\hspace*{0pt}\\
\hspace*{0pt}list{\char95}case ::~forall a b.~a -> (b -> [b] -> a) -> [b] -> a;\\
\hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\
\hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\
--- a/doc-src/Codegen/Thy/document/Program.tex Mon Jun 14 21:49:25 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex Tue Jun 15 07:42:48 2010 +0200
@@ -323,7 +323,8 @@
%
\begin{isamarkuptext}%
\noindent This is a convenient place to show how explicit dictionary construction
- manifests in generated code (here, the same example in \isa{SML}):%
+ manifests in generated code (here, the same example in \isa{SML})
+ \cite{Haftmann-Nipkow:2010:code}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/examples/Example.hs Mon Jun 14 21:49:25 2010 +0200
+++ b/doc-src/Codegen/Thy/examples/Example.hs Tue Jun 15 07:42:48 2010 +0200
@@ -2,13 +2,6 @@
module Example where {
-foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;
-foldla f a [] = a;
-foldla f a (x : xs) = foldla f (f a x) xs;
-
-rev :: forall a. [a] -> [a];
-rev xs = foldla (\ xsa x -> x : xsa) [] xs;
-
list_case :: forall a b. a -> (b -> [b] -> a) -> [b] -> a;
list_case f1 f2 (a : list) = f2 a list;
list_case f1 f2 [] = f1;
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jun 14 21:49:25 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Jun 15 07:42:48 2010 +0200
@@ -965,7 +965,214 @@
instantiates these mechanisms in a way that is amenable to end-user
applications.
- One framework generates code from both functional and relational
+ \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}.
+ 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
+ \emph{target language}. Inductive specifications can be executed
+ using the predicate compiler which operates within HOL.
+ See \cite{isabelle-codegen} for an introduction.
+
+ \begin{matharray}{rcl}
+ @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{attribute_def (HOL) code} & : & @{text attribute} \\
+ @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{attribute_def (HOL) code_inline} & : & @{text attribute} \\
+ @{attribute_def (HOL) code_post} & : & @{text attribute} \\
+ @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'export\_code' ( constexpr + ) \\
+ ( ( 'in' target ( 'module\_name' string ) ? \\
+ ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
+ ;
+
+ const: term
+ ;
+
+ constexpr: ( const | 'name.*' | '*' )
+ ;
+
+ typeconstructor: nameref
+ ;
+
+ class: nameref
+ ;
+
+ target: 'OCaml' | 'SML' | 'Haskell'
+ ;
+
+ 'code' ( 'del' ) ?
+ ;
+
+ 'code\_abort' ( const + )
+ ;
+
+ 'code\_datatype' ( const + )
+ ;
+
+ 'code_inline' ( 'del' ) ?
+ ;
+
+ 'code_post' ( 'del' ) ?
+ ;
+
+ 'code\_thms' ( constexpr + ) ?
+ ;
+
+ 'code\_deps' ( constexpr + ) ?
+ ;
+
+ 'code\_const' (const + 'and') \\
+ ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
+ ;
+
+ 'code\_type' (typeconstructor + 'and') \\
+ ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
+ ;
+
+ 'code\_class' (class + 'and') \\
+ ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
+ ;
+
+ 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
+ ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
+ ;
+
+ 'code\_reserved' target ( string + )
+ ;
+
+ 'code\_monad' const const target
+ ;
+
+ 'code\_include' target ( string ( string | '-') )
+ ;
+
+ 'code\_modulename' target ( ( string string ) + )
+ ;
+
+ syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
+ ;
+
+ \end{rail}
+
+ \begin{description}
+
+ \item @{command (HOL) "export_code"} generates code for a given list
+ of constants in the specified target language(s). If no serialization
+ instruction is given, only abstract code is generated internally.
+
+ Constants may be specified by giving them literally, referring to
+ all executable contants within a certain theory by giving @{text
+ "name.*"}, or referring to \emph{all} executable constants currently
+ available by giving @{text "*"}.
+
+ By default, for each involved theory one corresponding name space
+ module is generated. Alternativly, a module name may be specified
+ 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
+ single file; for \emph{Haskell}, it refers to a whole directory,
+ where code is generated in multiple files reflecting the module
+ hierarchy. The file specification ``@{text "-"}'' denotes standard
+ output. For \emph{SML}, omitting the file specification compiles
+ code internally in the context of the current ML session.
+
+ Serializers take an optional list of arguments in parentheses. For
+ \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
+ explicit module signatures.
+
+ For \emph{Haskell} a module name prefix may be given using the ``@{text
+ "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim
+ "deriving (Read, Show)"}'' clause to each appropriate datatype
+ declaration.
+
+ \item @{attribute (HOL) code} explicitly selects (or with option
+ ``@{text "del"}'' deselects) a code equation for code
+ generation. Usually packages introducing code equations provide
+ a reasonable default setup for selection.
+
+ \item @{command (HOL) "code_abort"} declares constants which are not
+ required to have a definition by means of code equations; if
+ needed these are implemented by program abort instead.
+
+ \item @{command (HOL) "code_datatype"} specifies a constructor set
+ for a logical type.
+
+ \item @{command (HOL) "print_codesetup"} gives an overview on
+ selected code equations and code generator datatypes.
+
+ \item @{attribute (HOL) code_inline} declares (or with
+ option ``@{text "del"}'' removes) inlining theorems which are
+ applied as rewrite rules to any code equation during
+ preprocessing.
+
+ \item @{attribute (HOL) code_post} declares (or with
+ option ``@{text "del"}'' removes) theorems which are
+ applied as rewrite rules to any result of an evaluation.
+
+ \item @{command (HOL) "print_codeproc"} prints the setup
+ of the code generator preprocessor.
+
+ \item @{command (HOL) "code_thms"} prints a list of theorems
+ representing the corresponding program containing all given
+ constants after preprocessing.
+
+ \item @{command (HOL) "code_deps"} visualizes dependencies of
+ theorems representing the corresponding program containing all given
+ constants after preprocessing.
+
+ \item @{command (HOL) "code_const"} associates a list of constants
+ with target-specific serializations; omitting a serialization
+ deletes an existing serialization.
+
+ \item @{command (HOL) "code_type"} associates a list of type
+ constructors with target-specific serializations; omitting a
+ serialization deletes an existing serialization.
+
+ \item @{command (HOL) "code_class"} associates a list of classes
+ with target-specific class names; omitting a serialization deletes
+ an existing serialization. This applies only to \emph{Haskell}.
+
+ \item @{command (HOL) "code_instance"} declares a list of type
+ constructor / class instance relations as ``already present'' for a
+ given target. Omitting a ``@{text "-"}'' deletes an existing
+ ``already present'' declaration. This applies only to
+ \emph{Haskell}.
+
+ \item @{command (HOL) "code_reserved"} declares a list of names as
+ reserved for a given target, preventing it to be shadowed by any
+ generated code.
+
+ \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
+ to generate monadic code for Haskell.
+
+ \item @{command (HOL) "code_include"} adds arbitrary named content
+ (``include'') to generated code. A ``@{text "-"}'' as last argument
+ will remove an already added ``include''.
+
+ \item @{command (HOL) "code_modulename"} declares aliasings from one
+ module name onto another.
+
+ \end{description}
+
+ The other framework generates code from both functional and relational
programs to SML. See \cite{isabelle-HOL} for further information
(this actually covers the new-style theory format as well).
@@ -1011,209 +1218,6 @@
;
\end{rail}
- \medskip The other framework generates code from functional programs
- (including overloading using type classes) to SML \cite{SML}, OCaml
- \cite{OCaml} and Haskell \cite{haskell-revised-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
- \emph{target language}. See \cite{isabelle-codegen} for an
- introduction on how to use it.
-
- \begin{matharray}{rcl}
- @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{attribute_def (HOL) code} & : & @{text attribute} \\
- \end{matharray}
-
- \begin{rail}
- 'export\_code' ( constexpr + ) \\
- ( ( 'in' target ( 'module\_name' string ) ? \\
- ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
- ;
-
- 'code\_thms' ( constexpr + ) ?
- ;
-
- 'code\_deps' ( constexpr + ) ?
- ;
-
- const: term
- ;
-
- constexpr: ( const | 'name.*' | '*' )
- ;
-
- typeconstructor: nameref
- ;
-
- class: nameref
- ;
-
- target: 'OCaml' | 'SML' | 'Haskell'
- ;
-
- 'code\_datatype' const +
- ;
-
- 'code\_const' (const + 'and') \\
- ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
- ;
-
- 'code\_type' (typeconstructor + 'and') \\
- ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
- ;
-
- 'code\_class' (class + 'and') \\
- ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
- ;
-
- 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
- ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
- ;
-
- 'code\_monad' const const target
- ;
-
- 'code\_reserved' target ( string + )
- ;
-
- 'code\_include' target ( string ( string | '-') )
- ;
-
- 'code\_modulename' target ( ( string string ) + )
- ;
-
- 'code\_abort' ( const + )
- ;
-
- syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
- ;
-
- 'code' ( 'del' ) ?
- ;
-
- 'code_unfold' ( 'del' ) ?
- ;
-
- 'code_post' ( 'del' ) ?
- ;
- \end{rail}
-
- \begin{description}
-
- \item @{command (HOL) "export_code"} is the canonical interface for
- generating and serializing code: for a given list of constants, code
- is generated for the specified target languages. If no serialization
- instruction is given, only abstract code is generated internally.
-
- Constants may be specified by giving them literally, referring to
- all executable contants within a certain theory by giving @{text
- "name.*"}, or referring to \emph{all} executable constants currently
- available by giving @{text "*"}.
-
- By default, for each involved theory one corresponding name space
- module is generated. Alternativly, a module name may be specified
- 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
- single file; for \emph{Haskell}, it refers to a whole directory,
- where code is generated in multiple files reflecting the module
- hierarchy. The file specification ``@{text "-"}'' denotes standard
- output. For \emph{SML}, omitting the file specification compiles
- code internally in the context of the current ML session.
-
- Serializers take an optional list of arguments in parentheses. For
- \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
- explicit module signatures.
-
- For \emph{Haskell} a module name prefix may be given using the ``@{text
- "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim
- "deriving (Read, Show)"}'' clause to each appropriate datatype
- declaration.
-
- \item @{command (HOL) "code_thms"} prints a list of theorems
- representing the corresponding program containing all given
- constants.
-
- \item @{command (HOL) "code_deps"} visualizes dependencies of
- theorems representing the corresponding program containing all given
- constants.
-
- \item @{command (HOL) "code_datatype"} specifies a constructor set
- for a logical type.
-
- \item @{command (HOL) "code_const"} associates a list of constants
- with target-specific serializations; omitting a serialization
- deletes an existing serialization.
-
- \item @{command (HOL) "code_type"} associates a list of type
- constructors with target-specific serializations; omitting a
- serialization deletes an existing serialization.
-
- \item @{command (HOL) "code_class"} associates a list of classes
- with target-specific class names; omitting a serialization deletes
- an existing serialization. This applies only to \emph{Haskell}.
-
- \item @{command (HOL) "code_instance"} declares a list of type
- constructor / class instance relations as ``already present'' for a
- given target. Omitting a ``@{text "-"}'' deletes an existing
- ``already present'' declaration. This applies only to
- \emph{Haskell}.
-
- \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
- to generate monadic code for Haskell.
-
- \item @{command (HOL) "code_reserved"} declares a list of names as
- reserved for a given target, preventing it to be shadowed by any
- generated code.
-
- \item @{command (HOL) "code_include"} adds arbitrary named content
- (``include'') to generated code. A ``@{text "-"}'' as last argument
- will remove an already added ``include''.
-
- \item @{command (HOL) "code_modulename"} declares aliasings from one
- module name onto another.
-
- \item @{command (HOL) "code_abort"} declares constants which are not
- required to have a definition by means of code equations; if
- needed these are implemented by program abort instead.
-
- \item @{attribute (HOL) code} explicitly selects (or with option
- ``@{text "del"}'' deselects) a code equation for code
- generation. Usually packages introducing code equations provide
- a reasonable default setup for selection.
-
- \item @{attribute (HOL) code_inline} declares (or with
- option ``@{text "del"}'' removes) inlining theorems which are
- applied as rewrite rules to any code equation during
- preprocessing.
-
- \item @{attribute (HOL) code_post} declares (or with
- option ``@{text "del"}'' removes) theorems which are
- applied as rewrite rules to any result of an evaluation.
-
- \item @{command (HOL) "print_codesetup"} gives an overview on
- selected code equations and code generator datatypes.
-
- \item @{command (HOL) "print_codeproc"} prints the setup
- of the code generator preprocessor.
-
- \end{description}
*}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jun 14 21:49:25 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Jun 15 07:42:48 2010 +0200
@@ -981,7 +981,211 @@
instantiates these mechanisms in a way that is amenable to end-user
applications.
- One framework generates code from both functional and relational
+ \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}.
+ 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
+ \emph{target language}. Inductive specifications can be executed
+ using the predicate compiler which operates within HOL.
+ See \cite{isabelle-codegen} for an introduction.
+
+ \begin{matharray}{rcl}
+ \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
+ \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
+ \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
+ \indexdef{HOL}{attribute}{code\_inline}\hypertarget{attribute.HOL.code-inline}{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}}} & : & \isa{attribute} \\
+ \indexdef{HOL}{attribute}{code\_post}\hypertarget{attribute.HOL.code-post}{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}}} & : & \isa{attribute} \\
+ \indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'export\_code' ( constexpr + ) \\
+ ( ( 'in' target ( 'module\_name' string ) ? \\
+ ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
+ ;
+
+ const: term
+ ;
+
+ constexpr: ( const | 'name.*' | '*' )
+ ;
+
+ typeconstructor: nameref
+ ;
+
+ class: nameref
+ ;
+
+ target: 'OCaml' | 'SML' | 'Haskell'
+ ;
+
+ 'code' ( 'del' ) ?
+ ;
+
+ 'code\_abort' ( const + )
+ ;
+
+ 'code\_datatype' ( const + )
+ ;
+
+ 'code_inline' ( 'del' ) ?
+ ;
+
+ 'code_post' ( 'del' ) ?
+ ;
+
+ 'code\_thms' ( constexpr + ) ?
+ ;
+
+ 'code\_deps' ( constexpr + ) ?
+ ;
+
+ 'code\_const' (const + 'and') \\
+ ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
+ ;
+
+ 'code\_type' (typeconstructor + 'and') \\
+ ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
+ ;
+
+ 'code\_class' (class + 'and') \\
+ ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
+ ;
+
+ 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
+ ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
+ ;
+
+ 'code\_reserved' target ( string + )
+ ;
+
+ 'code\_monad' const const target
+ ;
+
+ 'code\_include' target ( string ( string | '-') )
+ ;
+
+ 'code\_modulename' target ( ( string string ) + )
+ ;
+
+ syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
+ ;
+
+ \end{rail}
+
+ \begin{description}
+
+ \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} generates code for a given list
+ of constants in the specified target language(s). If no serialization
+ instruction is given, only abstract code is generated internally.
+
+ Constants may be specified by giving them literally, referring to
+ all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
+ available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}.
+
+ By default, for each involved theory one corresponding name space
+ module is generated. Alternativly, a module name may be specified
+ 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
+ single file; for \emph{Haskell}, it refers to a whole directory,
+ where code is generated in multiple files reflecting the module
+ hierarchy. The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard
+ output. For \emph{SML}, omitting the file specification compiles
+ code internally in the context of the current ML session.
+
+ Serializers take an optional list of arguments in parentheses. For
+ \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits
+ explicit module signatures.
+
+ For \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype
+ declaration.
+
+ \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
+ ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
+ generation. Usually packages introducing code equations provide
+ a reasonable default setup for selection.
+
+ \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
+ required to have a definition by means of code equations; if
+ needed these are implemented by program abort instead.
+
+ \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
+ for a logical type.
+
+ \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
+ selected code equations and code generator datatypes.
+
+ \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
+ option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
+ applied as rewrite rules to any code equation during
+ preprocessing.
+
+ \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
+ option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
+ applied as rewrite rules to any result of an evaluation.
+
+ \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup
+ of the code generator preprocessor.
+
+ \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
+ representing the corresponding program containing all given
+ constants after preprocessing.
+
+ \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} visualizes dependencies of
+ theorems representing the corresponding program containing all given
+ constants after preprocessing.
+
+ \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} associates a list of constants
+ with target-specific serializations; omitting a serialization
+ deletes an existing serialization.
+
+ \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} associates a list of type
+ constructors with target-specific serializations; omitting a
+ serialization deletes an existing serialization.
+
+ \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}} associates a list of classes
+ with target-specific class names; omitting a serialization deletes
+ an existing serialization. This applies only to \emph{Haskell}.
+
+ \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}} declares a list of type
+ constructor / class instance relations as ``already present'' for a
+ given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
+ ``already present'' declaration. This applies only to
+ \emph{Haskell}.
+
+ \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} declares a list of names as
+ reserved for a given target, preventing it to be shadowed by any
+ generated code.
+
+ \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}} provides an auxiliary mechanism
+ to generate monadic code for Haskell.
+
+ \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} adds arbitrary named content
+ (``include'') to generated code. A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument
+ will remove an already added ``include''.
+
+ \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one
+ module name onto another.
+
+ \end{description}
+
+ The other framework generates code from both functional and relational
programs to SML. See \cite{isabelle-HOL} for further information
(this actually covers the new-style theory format as well).
@@ -1025,208 +1229,7 @@
'code' (name)?
;
- \end{rail}
-
- \medskip The other framework generates code from functional programs
- (including overloading using type classes) to SML \cite{SML}, OCaml
- \cite{OCaml} and Haskell \cite{haskell-revised-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
- \emph{target language}. See \cite{isabelle-codegen} for an
- introduction on how to use it.
-
- \begin{matharray}{rcl}
- \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
- \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
- \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
- \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
- \indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
- \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
- \end{matharray}
-
- \begin{rail}
- 'export\_code' ( constexpr + ) \\
- ( ( 'in' target ( 'module\_name' string ) ? \\
- ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
- ;
-
- 'code\_thms' ( constexpr + ) ?
- ;
-
- 'code\_deps' ( constexpr + ) ?
- ;
-
- const: term
- ;
-
- constexpr: ( const | 'name.*' | '*' )
- ;
-
- typeconstructor: nameref
- ;
-
- class: nameref
- ;
-
- target: 'OCaml' | 'SML' | 'Haskell'
- ;
-
- 'code\_datatype' const +
- ;
-
- 'code\_const' (const + 'and') \\
- ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
- ;
-
- 'code\_type' (typeconstructor + 'and') \\
- ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
- ;
-
- 'code\_class' (class + 'and') \\
- ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
- ;
-
- 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
- ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
- ;
-
- 'code\_monad' const const target
- ;
-
- 'code\_reserved' target ( string + )
- ;
-
- 'code\_include' target ( string ( string | '-') )
- ;
-
- 'code\_modulename' target ( ( string string ) + )
- ;
-
- 'code\_abort' ( const + )
- ;
-
- syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
- ;
-
- 'code' ( 'del' ) ?
- ;
-
- 'code_unfold' ( 'del' ) ?
- ;
-
- 'code_post' ( 'del' ) ?
- ;
- \end{rail}
-
- \begin{description}
-
- \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} is the canonical interface for
- generating and serializing code: for a given list of constants, code
- is generated for the specified target languages. If no serialization
- instruction is given, only abstract code is generated internally.
-
- Constants may be specified by giving them literally, referring to
- all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
- available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}.
-
- By default, for each involved theory one corresponding name space
- module is generated. Alternativly, a module name may be specified
- 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
- single file; for \emph{Haskell}, it refers to a whole directory,
- where code is generated in multiple files reflecting the module
- hierarchy. The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard
- output. For \emph{SML}, omitting the file specification compiles
- code internally in the context of the current ML session.
-
- Serializers take an optional list of arguments in parentheses. For
- \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits
- explicit module signatures.
-
- For \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype
- declaration.
-
- \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
- representing the corresponding program containing all given
- constants.
-
- \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} visualizes dependencies of
- theorems representing the corresponding program containing all given
- constants.
-
- \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
- for a logical type.
-
- \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} associates a list of constants
- with target-specific serializations; omitting a serialization
- deletes an existing serialization.
-
- \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} associates a list of type
- constructors with target-specific serializations; omitting a
- serialization deletes an existing serialization.
-
- \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}} associates a list of classes
- with target-specific class names; omitting a serialization deletes
- an existing serialization. This applies only to \emph{Haskell}.
-
- \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}} declares a list of type
- constructor / class instance relations as ``already present'' for a
- given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
- ``already present'' declaration. This applies only to
- \emph{Haskell}.
-
- \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}} provides an auxiliary mechanism
- to generate monadic code for Haskell.
-
- \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} declares a list of names as
- reserved for a given target, preventing it to be shadowed by any
- generated code.
-
- \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} adds arbitrary named content
- (``include'') to generated code. A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument
- will remove an already added ``include''.
-
- \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one
- module name onto another.
-
- \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
- required to have a definition by means of code equations; if
- needed these are implemented by program abort instead.
-
- \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
- ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
- generation. Usually packages introducing code equations provide
- a reasonable default setup for selection.
-
- \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
- option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
- applied as rewrite rules to any code equation during
- preprocessing.
-
- \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
- option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
- applied as rewrite rules to any result of an evaluation.
-
- \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
- selected code equations and code generator datatypes.
-
- \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup
- of the code generator preprocessor.
-
- \end{description}%
+ \end{rail}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/manual.bib Mon Jun 14 21:49:25 2010 +0200
+++ b/doc-src/manual.bib Tue Jun 15 07:42:48 2010 +0200
@@ -130,6 +130,13 @@
@book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow},
title="Term Rewriting and All That",publisher=CUP,year=1998}
+@manual{isabelle-locale,
+ author = {Clemens Ballarin},
+ title = {Tutorial to Locales and Locale Interpretation},
+ institution = TUM,
+ note = {\url{http://isabelle.in.tum.de/doc/locales.pdf}}
+}
+
@InCollection{Barendregt-Geuvers:2001,
author = {H. Barendregt and H. Geuvers},
title = {Proof Assistants using Dependent Type Systems},
@@ -508,15 +515,15 @@
year = {2007}
}
-@TechReport{Haftmann-Nipkow:2007:codegen,
- author = {Florian Haftmann and Tobias Nipkow},
- title = {A Code Generator Framework for {Isabelle/HOL}},
- editor = {Klaus Schneider and Jens Brandt},
- booktitle = {Theorem Proving in Higher Order Logics: Emerging Trends Proceedings},
- month = {08},
- year = {2007},
- institution = {Department of Computer Science, University of Kaiserslautern},
- number = {364/07}
+@inproceedings{Haftmann-Nipkow:2010:code,
+ author = {Florian Haftmann and Tobias Nipkow},
+ title = {Code Generation via Higher-Order Rewrite Systems},
+ booktitle = {Functional and Logic Programming: 10th International Symposium: FLOPS 2010},
+ year = 2010,
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ editor = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal},
+ volume = {6009}
}
@InProceedings{Haftmann-Wenzel:2009,
--- a/src/HOL/HOL.thy Mon Jun 14 21:49:25 2010 +0200
+++ b/src/HOL/HOL.thy Tue Jun 15 07:42:48 2010 +0200
@@ -1800,8 +1800,8 @@
setup {*
Code_Preproc.map_pre (fn simpset =>
simpset addsimprocs [Simplifier.simproc_i @{theory} "eq" [@{term "op ="}]
- (fn thy => fn _ => fn t as Const (_, T) => case strip_type T
- of ((T as Type _) :: _, _) => SOME @{thm equals_eq}
+ (fn thy => fn _ => fn Const (_, T) => case strip_type T
+ of (Type _ :: _, _) => SOME @{thm equals_eq}
| _ => NONE)])
*}
--- a/src/HOL/List.thy Mon Jun 14 21:49:25 2010 +0200
+++ b/src/HOL/List.thy Tue Jun 15 07:42:48 2010 +0200
@@ -4929,4 +4929,40 @@
"list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
by(simp add: all_from_to_int_iff_ball list_ex_iff)
+
+subsubsection {* Use convenient predefined operations *}
+
+code_const "op @"
+ (SML infixr 7 "@")
+ (OCaml infixr 6 "@")
+ (Haskell infixr 5 "++")
+ (Scala infixl 7 "++")
+
+code_const map
+ (Haskell "map")
+
+code_const filter
+ (Haskell "filter")
+
+code_const concat
+ (Haskell "concat")
+
+code_const rev
+ (Haskell "rev")
+
+code_const zip
+ (Haskell "zip")
+
+code_const takeWhile
+ (Haskell "takeWhile")
+
+code_const dropWhile
+ (Haskell "dropWhile")
+
+code_const hd
+ (Haskell "head")
+
+code_const last
+ (Haskell "last")
+
end
--- a/src/HOL/Nat.thy Mon Jun 14 21:49:25 2010 +0200
+++ b/src/HOL/Nat.thy Tue Jun 15 07:42:48 2010 +0200
@@ -1203,9 +1203,9 @@
lemmas [code_unfold] = funpow_code_def [symmetric]
lemma [code]:
+ "funpow (Suc n) f = f o funpow n f"
"funpow 0 f = id"
- "funpow (Suc n) f = f o funpow n f"
- unfolding funpow_code_def by simp_all
+ by (simp_all add: funpow_code_def)
hide_const (open) funpow
@@ -1213,6 +1213,11 @@
"f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
by (induct m) simp_all
+lemma funpow_mult:
+ fixes f :: "'a \<Rightarrow> 'a"
+ shows "(f ^^ m) ^^ n = f ^^ (m * n)"
+ by (induct n) (simp_all add: funpow_add)
+
lemma funpow_swap1:
"f ((f ^^ n) x) = (f ^^ n) (f x)"
proof -
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Jun 14 21:49:25 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Jun 15 07:42:48 2010 +0200
@@ -105,12 +105,14 @@
in (thm', lthy') end;
fun tac thms = Class.intro_classes_tac []
THEN ALLGOALS (ProofContext.fact_tac thms);
+ fun prefix dtco = Binding.qualify true (Long_Name.base_name dtco) o Binding.qualify true "eq" o Binding.name;
fun add_eq_thms dtco =
Theory.checkpoint
#> `(fn thy => mk_eq_eqns thy dtco)
- #-> (fn (thms, thm) =>
- Code.add_nbe_eqn thm
- #> fold_rev Code.add_eqn thms);
+ #-> (fn (thms, thm) => PureThy.note_thmss Thm.lemmaK
+ [((prefix dtco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
+ ((prefix dtco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
+ #> snd
in
thy
|> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
--- a/src/Pure/Isar/code.ML Mon Jun 14 21:49:25 2010 +0200
+++ b/src/Pure/Isar/code.ML Tue Jun 15 07:42:48 2010 +0200
@@ -59,6 +59,9 @@
val add_default_eqn: thm -> theory -> theory
val add_default_eqn_attribute: attribute
val add_default_eqn_attrib: Attrib.src
+ val add_nbe_default_eqn: thm -> theory -> theory
+ val add_nbe_default_eqn_attribute: attribute
+ val add_nbe_default_eqn_attrib: Attrib.src
val del_eqn: thm -> theory -> theory
val del_eqns: string -> theory -> theory
val add_case: thm -> theory -> theory
@@ -1066,18 +1069,25 @@
of SOME eqn => gen_add_eqn false eqn thy
| NONE => thy;
+fun add_nbe_eqn thm thy =
+ gen_add_eqn false (mk_eqn thy (thm, false)) thy;
+
fun add_default_eqn thm thy =
case mk_eqn_liberal thy thm
of SOME eqn => gen_add_eqn true eqn thy
| NONE => thy;
-fun add_nbe_eqn thm thy =
- gen_add_eqn false (mk_eqn thy (thm, false)) thy;
-
val add_default_eqn_attribute = Thm.declaration_attribute
(fn thm => Context.mapping (add_default_eqn thm) I);
val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
+fun add_nbe_default_eqn thm thy =
+ gen_add_eqn true (mk_eqn thy (thm, false)) thy;
+
+val add_nbe_default_eqn_attribute = Thm.declaration_attribute
+ (fn thm => Context.mapping (add_nbe_default_eqn thm) I);
+val add_nbe_default_eqn_attrib = Attrib.internal (K add_nbe_default_eqn_attribute);
+
fun add_abs_eqn raw_thm thy =
let
val (abs_thm, tyco) = (apfst Thm.close_derivation o mk_abs_eqn thy) raw_thm;
--- a/src/Tools/Code/code_thingol.ML Mon Jun 14 21:49:25 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Tue Jun 15 07:42:48 2010 +0200
@@ -278,7 +278,7 @@
fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
fun namify_classrel thy = namify thy (fn (sub_class, super_class) =>
- Long_Name.base_name sub_class ^ "_" ^ Long_Name.base_name super_class)
+ Long_Name.base_name super_class ^ "_" ^ Long_Name.base_name sub_class)
(fn thy => thyname_of_class thy o fst);
(*order fits nicely with composed projections*)
fun namify_tyco thy "fun" = "Pure.fun"