--- a/doc-src/Codegen/Thy/document/Further.tex Mon Aug 27 22:31:16 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,624 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Further}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Further\isanewline
-\isakeyword{imports}\ Setup\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsection{Further issues \label{sec:further}%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Specialities of the \isa{Scala} target language \label{sec:scala}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\isa{Scala} deviates from languages of the ML family in a couple
- of aspects; those which affect code generation mainly have to do with
- \isa{Scala}'s type system:
-
- \begin{itemize}
-
- \item \isa{Scala} prefers tupled syntax over curried syntax.
-
- \item \isa{Scala} sacrifices Hindely-Milner type inference for a
- much more rich type system with subtyping etc. For this reason
- type arguments sometimes have to be given explicitly in square
- brackets (mimicking System F syntax).
-
- \item In contrast to \isa{Haskell} where most specialities of
- the type system are implemented using \emph{type classes},
- \isa{Scala} provides a sophisticated system of \emph{implicit
- arguments}.
-
- \end{itemize}
-
- \noindent Concerning currying, the \isa{Scala} serializer counts
- arguments in code equations to determine how many arguments
- shall be tupled; remaining arguments and abstractions in terms
- rather than function definitions are always curried.
-
- The second aspect affects user-defined adaptations with \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}. For regular terms, the \isa{Scala} serializer prints
- all type arguments explicitly. For user-defined term adaptations
- this is only possible for adaptations which take no arguments: here
- the type arguments are just appended. Otherwise they are ignored;
- hence user-defined adaptations for polymorphic constants have to be
- designed very carefully to avoid ambiguity.
-
- Isabelle's type classes are mapped onto \isa{Scala} implicits; in
- cases with diamonds in the subclass hierarchy this can lead to
- ambiguities in the generated code:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{class}\isamarkupfalse%
-\ class{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \isakeyword{fixes}\ foo\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{class}\isamarkupfalse%
-\ class{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ class{\isadigit{1}}\isanewline
-\isanewline
-\isacommand{class}\isamarkupfalse%
-\ class{\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ class{\isadigit{1}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Here both \isa{class{\isadigit{2}}} and \isa{class{\isadigit{3}}} inherit from \isa{class{\isadigit{1}}},
- forming the upper part of a diamond.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{definition}\isamarkupfalse%
-\ bar\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{7B}{\isacharbraceleft}}class{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ class{\isadigit{3}}{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}bar\ {\isaliteral{3D}{\isacharequal}}\ foo{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This yields the following code:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotetypewriter
-%
-\endisadelimquotetypewriter
-%
-\isatagquotetypewriter
-%
-\begin{isamarkuptext}%
-object\ Example\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\isanewline
-trait\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}foo{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-def\ foo{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}foo{\isaliteral{60}{\isacharbackquote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-trait\ class{\isadigit{2}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-trait\ class{\isadigit{3}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-def\ bar{\isaliteral{5B}{\isacharbrackleft}}A\ {\isaliteral{3A}{\isacharcolon}}\ class{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}\ class{\isadigit{3}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ foo{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{2A}{\isacharasterisk}}\ object\ Example\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\isanewline%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquotetypewriter
-{\isafoldquotetypewriter}%
-%
-\isadelimquotetypewriter
-%
-\endisadelimquotetypewriter
-%
-\begin{isamarkuptext}%
-\noindent This code is rejected by the \isa{Scala} compiler: in
- the definition of \isa{bar}, it is not clear from where to derive
- the implicit argument for \isa{foo}.
-
- The solution to the problem is to close the diamond by a further
- class with inherits from both \isa{class{\isadigit{2}}} and \isa{class{\isadigit{3}}}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{class}\isamarkupfalse%
-\ class{\isadigit{4}}\ {\isaliteral{3D}{\isacharequal}}\ class{\isadigit{2}}\ {\isaliteral{2B}{\isacharplus}}\ class{\isadigit{3}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Then the offending code equation can be restricted to
- \isa{class{\isadigit{4}}}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}bar\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}class{\isadigit{4}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ foo{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}simp\ only{\isaliteral{3A}{\isacharcolon}}\ bar{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent with the following code:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotetypewriter
-%
-\endisadelimquotetypewriter
-%
-\isatagquotetypewriter
-%
-\begin{isamarkuptext}%
-object\ Example\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\isanewline
-trait\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}foo{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-def\ foo{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}foo{\isaliteral{60}{\isacharbackquote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-trait\ class{\isadigit{3}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-trait\ class{\isadigit{2}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ class{\isadigit{1}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-trait\ class{\isadigit{4}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ class{\isadigit{2}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ with\ class{\isadigit{3}}{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-def\ bar{\isaliteral{5B}{\isacharbrackleft}}A\ {\isaliteral{3A}{\isacharcolon}}\ class{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ foo{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{2A}{\isacharasterisk}}\ object\ Example\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\isanewline%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquotetypewriter
-{\isafoldquotetypewriter}%
-%
-\isadelimquotetypewriter
-%
-\endisadelimquotetypewriter
-%
-\begin{isamarkuptext}%
-\noindent which exposes no ambiguity.
-
- Since the preprocessor (cf.~\secref{sec:preproc}) propagates sort
- constraints through a system of code equations, it is usually not
- very difficult to identify the set of code equations which actually
- needs more restricted sort constraints.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Modules namespace%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} command it is possible to
- leave out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}} part; then code is
- distributed over different modules, where the module name space
- roughly is induced by the Isabelle theory name space.
-
- Then sometimes the awkward situation occurs that dependencies
- between definitions introduce cyclic dependencies between modules,
- which in the \isa{Haskell} world leaves you to the mercy of the
- \isa{Haskell} implementation you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible.
-
- A solution is to declare module names explicitly. Let use assume
- the three cyclically dependent modules are named \emph{A}, \emph{B}
- and \emph{C}. Then, by stating%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}\isamarkupfalse%
-\ SML\isanewline
-\ \ A\ ABC\isanewline
-\ \ B\ ABC\isanewline
-\ \ C\ ABC%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent we explicitly map all those modules on \emph{ABC},
- resulting in an ad-hoc merge of this three modules at serialisation
- time.%
-\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\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \isakeyword{fixes}\ power\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isakeyword{assumes}\ power{\isaliteral{5F}{\isacharunderscore}}commute{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}power\ x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ power\ y\ {\isaliteral{3D}{\isacharequal}}\ power\ y\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ power\ x{\isaliteral{22}{\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\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}powers\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ id{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}powers\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ power\ x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ powers\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ powers{\isaliteral{5F}{\isacharunderscore}}append{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}powers\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ powers\ xs\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ powers\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}induct\ xs{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ powers{\isaliteral{5F}{\isacharunderscore}}power{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}powers\ xs\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ power\ x\ {\isaliteral{3D}{\isacharequal}}\ power\ x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ powers\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}induct\ xs{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ del{\isaliteral{3A}{\isacharcolon}}\ o{\isaliteral{5F}{\isacharunderscore}}apply\ id{\isaliteral{5F}{\isacharunderscore}}apply\ add{\isaliteral{3A}{\isacharcolon}}\ o{\isaliteral{5F}{\isacharunderscore}}assoc\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
-\ \ \ \ \ \ simp\ del{\isaliteral{3A}{\isacharcolon}}\ o{\isaliteral{5F}{\isacharunderscore}}apply\ add{\isaliteral{3A}{\isacharcolon}}\ o{\isaliteral{5F}{\isacharunderscore}}assoc\ power{\isaliteral{5F}{\isacharunderscore}}commute{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ powers{\isaliteral{5F}{\isacharunderscore}}rev{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}powers\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ powers\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}induct\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ powers{\isaliteral{5F}{\isacharunderscore}}append\ powers{\isaliteral{5F}{\isacharunderscore}}power{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-After an interpretation of this locale (say, \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} \isa{fun{\isaliteral{5F}{\isacharunderscore}}power{\isaliteral{3A}{\isacharcolon}}} \isa{{\isaliteral{22}{\isachardoublequote}}power\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ f\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}), one would expect to have a constant \isa{fun{\isaliteral{5F}{\isacharunderscore}}power{\isaliteral{2E}{\isachardot}}powers\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a} for which code
- can be generated. But this not the case: internally, the term
- \isa{fun{\isaliteral{5F}{\isacharunderscore}}power{\isaliteral{2E}{\isachardot}}powers} is an abbreviation for the foundational
- term \isa{{\isaliteral{22}{\isachardoublequote}}power{\isaliteral{2E}{\isachardot}}powers\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ f\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
- (see \cite{isabelle-locale} for the details behind).
-
- Fortunately, 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\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-\ \ {\isaliteral{5B}{\isacharbrackleft}}code\ del{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}funpows\ {\isaliteral{3D}{\isacharequal}}\ power{\isaliteral{2E}{\isachardot}}powers\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n\ f{\isaliteral{2E}{\isachardot}}\ f\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent In general, the pattern is \isa{c\ {\isaliteral{3D}{\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\ {\isaliteral{3D}{\isacharequal}}\ c}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{interpretation}\isamarkupfalse%
-\ fun{\isaliteral{5F}{\isacharunderscore}}power{\isaliteral{3A}{\isacharcolon}}\ power\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ f\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}power{\isaliteral{2E}{\isachardot}}powers\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n\ f{\isaliteral{2E}{\isachardot}}\ f\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ funpows{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ unfold{\isaliteral{5F}{\isacharunderscore}}locales\isanewline
-\ \ \ \ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ fun{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}iff\ funpow{\isaliteral{5F}{\isacharunderscore}}mult\ mult{\isaliteral{5F}{\isacharunderscore}}commute\ funpows{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\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%
-%
-\isadelimquotetypewriter
-%
-\endisadelimquotetypewriter
-%
-\isatagquotetypewriter
-%
-\begin{isamarkuptext}%
-funpow\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-funpow\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ f\ {\isaliteral{3D}{\isacharequal}}\ id{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-funpow\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ f\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{2E}{\isachardot}}\ funpow\ n\ f{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-funpows\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5B}{\isacharbrackleft}}Nat{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-funpows\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ id{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-funpows\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ funpow\ x\ {\isaliteral{2E}{\isachardot}}\ funpows\ xs{\isaliteral{3B}{\isacharsemicolon}}\isanewline%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquotetypewriter
-{\isafoldquotetypewriter}%
-%
-\isadelimquotetypewriter
-%
-\endisadelimquotetypewriter
-%
-\isamarkupsubsection{Imperative data structures%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If you consider imperative data structures as inevitable for a
- specific application, you should consider \emph{Imperative
- Functional Programming with Isabelle/HOL}
- \cite{bulwahn-et-al:2008:imperative}; the framework described there
- is available in session \isa{Imperative{\isaliteral{5F}{\isacharunderscore}}HOL}, together with a
- short primer document.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{ML system interfaces \label{sec:ml}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Since the code generator framework not only aims to provide a nice
- Isar interface but also to form a base for code-generation-based
- applications, here a short description of the most fundamental ML
- interfaces.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Managing executable content%
-}
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
- \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
- \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
- \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
- \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
- \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: |\isasep\isanewline%
-\verb| string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
-\verb| -> theory -> theory| \\
- \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
- \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
- \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
-\verb| -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool| \\
- \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
- \end{mldecls}
-
- \begin{description}
-
- \item \verb|Code.read_const|~\isa{thy}~\isa{s}
- reads a constant as a concrete term expression \isa{s}.
-
- \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
- theorem \isa{thm} to executable content.
-
- \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
- theorem \isa{thm} from executable content, if present.
-
- \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
- the preprocessor simpset.
-
- \item \verb|Code_Preproc.add_functrans|~\isa{{\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ f{\isaliteral{29}{\isacharparenright}}}~\isa{thy} adds
- function transformer \isa{f} (named \isa{name}) to executable content;
- \isa{f} is a transformer of the code equations belonging
- to a certain function definition, depending on the
- current theory context. Returning \isa{NONE} indicates that no
- transformation took place; otherwise, the whole process will be iterated
- with the new code equations.
-
- \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes
- function transformer named \isa{name} from executable content.
-
- \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
- a datatype to executable content, with generation
- set \isa{cs}.
-
- \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const}
- returns type constructor corresponding to
- constructor \isa{const}; returns \isa{NONE}
- if \isa{const} is no constructor.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isamarkupsubsubsection{Data depending on the theory's executable content%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Implementing code generator applications on top of the framework set
- out so far usually not only involves using those primitive
- interfaces but also storing code-dependent data and various other
- things.
-
- Due to incrementality of code generation, changes in the theory's
- executable content have to be propagated in a certain fashion.
- Additionally, such changes may occur not only during theory
- extension but also during theory merge, which is a little bit nasty
- from an implementation point of view. The framework provides a
- solution to this technical challenge by providing a functorial data
- slot \verb|Code_Data|; on instantiation of this functor, the
- following types and operations are required:
-
- \medskip
- \begin{tabular}{l}
- \isa{type\ T} \\
- \isa{val\ empty{\isaliteral{3A}{\isacharcolon}}\ T} \\
- \end{tabular}
-
- \begin{description}
-
- \item \isa{T} the type of data to store.
-
- \item \isa{empty} initial (empty) data.
-
- \end{description}
-
- \noindent An instance of \verb|Code_Data| provides the
- following interface:
-
- \medskip
- \begin{tabular}{l}
- \isa{change{\isaliteral{3A}{\isacharcolon}}\ theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ T} \\
- \isa{change{\isaliteral{5F}{\isacharunderscore}}yield{\isaliteral{3A}{\isacharcolon}}\ theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}T\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2A}{\isacharasterisk}}\ T{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2A}{\isacharasterisk}}\ T}
- \end{tabular}
-
- \begin{description}
-
- \item \isa{change} update of current data (cached!) by giving a
- continuation.
-
- \item \isa{change{\isaliteral{5F}{\isacharunderscore}}yield} update with side result.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: