# HG changeset patch # User haftmann # Date 1187161058 -7200 # Node ID 165648d5679feafb6653de3ff58d7df08daab925 # Parent cf82c471f9ee4667253947335a3b2244cf84c4ac updated diff -r cf82c471f9ee -r 165648d5679f doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Tue Aug 14 23:23:09 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Wed Aug 15 08:57:38 2007 +0200 @@ -1242,88 +1242,6 @@ \end{description} *} -subsubsection {* Building implementable systems fo defining equations *} - -text {* - Out of the executable content of a theory, a normalized - defining equation systems may be constructed containing - function definitions for constants. The system is cached - until its underlying executable content changes. - - Defining equations are retrieved by instantiation - of the functor @{ML_functor CodeFuncgrRetrieval} - which takes two arguments: - - \medskip - \begin{tabular}{l} - @{text "val rewrites: theory \ thm list"} - \end{tabular} - - \begin{description} - - \item @{text rewrites} specifies a set of theory-dependent - rewrite rules which are added to the preprocessor setup; - if no additional preprocessing is required, pass - a function returning an empty list. - - \end{description} - - An instance of @{ML_functor CodeFuncgrRetrieval} in essence - provides the following interface: - - \medskip - \begin{tabular}{l} - @{text "make: theory \ CodeUnit.const list \ CodeFuncgr.T"} \\ - \end{tabular} - - \begin{description} - - \item @{text make}~@{text thy}~@{text consts} returns - a system of defining equations which is guaranteed - to contain all defining equations for constants @{text consts} - including all defining equations any defining equation - for any constant in @{text consts} depends on. - - \end{description} - - Systems of defining equations are graphs accesible by the - following operations: -*} - -text %mlref {* - \begin{mldecls} - @{index_ML_type CodeFuncgr.T} \\ - @{index_ML CodeFuncgr.funcs: "CodeFuncgr.T -> CodeUnit.const -> thm list"} \\ - @{index_ML CodeFuncgr.typ: "CodeFuncgr.T -> CodeUnit.const -> typ"} \\ - @{index_ML CodeFuncgr.deps: "CodeFuncgr.T - -> CodeUnit.const list -> CodeUnit.const list list"} \\ - @{index_ML CodeFuncgr.all: "CodeFuncgr.T -> CodeUnit.const list"} - \end{mldecls} - - \begin{description} - - \item @{ML_type CodeFuncgr.T} represents - a normalized defining equation system. - - \item @{ML CodeFuncgr.funcs}~@{text funcgr}~@{text const} - retrieves defining equiations for constant @{text const}. - - \item @{ML CodeFuncgr.typ}~@{text funcgr}~@{text const} - retrieves function type for constant @{text const}. - - \item @{ML CodeFuncgr.deps}~@{text funcgr}~@{text consts} - returns the transitive closure of dependencies for - constants @{text consts} as a partitioning where each partition - corresponds to a strongly connected component of - dependencies and any partition does \emph{not} - depend on partitions further left. - - \item @{ML CodeFuncgr.all}~@{text funcgr} - returns all currently represented constants. - - \end{description} -*} - subsubsection {* Datatype hooks *} text {* diff -r cf82c471f9ee -r 165648d5679f doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Tue Aug 14 23:23:09 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed Aug 15 08:57:38 2007 +0200 @@ -590,7 +590,7 @@ \item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char}, but also offers treatment of character codes; includes \isa{Pretty{\isacharunderscore}Int}. - \item[\isa{Executable{\isacharunderscore}Set}] \label{exec_set} allows to generate code + \item[\isa{Executable{\isacharunderscore}Set}] allows to generate code for finite sets using lists. \item[\isa{Executable{\isacharunderscore}Rat}] implements rational numbers. @@ -1452,91 +1452,12 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Axiomatic extensions% +\isamarkupsubsection{Code generation and proof extraction% } \isamarkuptrue% % \begin{isamarkuptext}% -\begin{warn} - The extensions introduced in this section, though working - in practice, are not the cream of the crop, as you - will notice during reading. They will - eventually be replaced by more mature approaches. - \end{warn} - - Sometimes equalities are taken for granted which are - not derivable inside the HOL logic but are silently assumed - to hold for executable code. For example, we may want - to identify the famous HOL constant \isa{arbitrary} - of type \isa{{\isacharprime}a\ option} with \isa{None}. - By brute force:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{axiomatization}\isamarkupfalse% -\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}arbitrary\ {\isacharequal}\ None{\isachardoublequoteclose}% -\begin{isamarkuptext}% -However this has to be considered harmful since this axiom, - though probably justifiable for generated code, could - introduce serious inconsistencies into the logic. - - So, there is a distinguished construct for stating axiomatic - equalities of constants which apply only for code generation. - Before introducing this, here is a convenient place to describe - shortly how to deal with some restrictions the type discipline - imposes. - - By itself, the constant \isa{arbitrary} is a non-overloaded - polymorphic constant. So, there is no way to distinguish - different versions of \isa{arbitrary} for different types - inside the code generator framework. However, inlining - theorems together with auxiliary constants provide a solution:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{definition}\isamarkupfalse% -\isanewline -\ \ arbitrary{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isacharbrackleft}symmetric{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}arbitrary{\isacharunderscore}option\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}% -\begin{isamarkuptext}% -By that, we replace any \isa{arbitrary} with option type - by \isa{arbitrary{\isacharunderscore}option} in defining equations. - - For technical reasons, we further have to provide a - synonym for \isa{None} which in code generator view - is a function rather than a term constructor:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{definition}\isamarkupfalse% -\isanewline -\ \ {\isachardoublequoteopen}None{\isacharprime}\ {\isacharequal}\ None{\isachardoublequoteclose}% -\begin{isamarkuptext}% -Then finally we are enabled to use \isa{{\isasymCODEAXIOMS}}:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{code{\isacharunderscore}axioms}\isamarkupfalse% -\isanewline -\ \ arbitrary{\isacharunderscore}option\ {\isasymequiv}\ None{\isacharprime}% -\begin{isamarkuptext}% -A dummy example:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{fun}\isamarkupfalse% -\isanewline -\ \ dummy{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ \ \ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ Some\ x{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ dummy{\isacharunderscore}option\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}arbitrary{\isachardot}ML{\isachardoublequoteclose}% -\begin{isamarkuptext}% -\lstsml{Thy/examples/arbitrary.ML} - - \medskip - - Another axiomatic extension is code generation - for abstracted types. For this, the - \isa{Executable{\isacharunderscore}Set} theory (see \secref{exec_set}) - forms a good example.% +\fixme% \end{isamarkuptext}% \isamarkuptrue% % @@ -1833,105 +1754,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsubsection{Building implementable systems fo defining equations% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Out of the executable content of a theory, a normalized - defining equation systems may be constructed containing - function definitions for constants. The system is cached - until its underlying executable content changes. - - Defining equations are retrieved by instantiation - of the functor \verb|CodeFuncgrRetrieval| - which takes two arguments: - - \medskip - \begin{tabular}{l} - \isa{val\ rewrites{\isacharcolon}\ theory\ {\isasymrightarrow}\ thm\ list} - \end{tabular} - - \begin{description} - - \item \isa{rewrites} specifies a set of theory-dependent - rewrite rules which are added to the preprocessor setup; - if no additional preprocessing is required, pass - a function returning an empty list. - - \end{description} - - An instance of \verb|CodeFuncgrRetrieval| in essence - provides the following interface: - - \medskip - \begin{tabular}{l} - \isa{make{\isacharcolon}\ theory\ {\isasymrightarrow}\ CodeUnit{\isachardot}const\ list\ {\isasymrightarrow}\ CodeFuncgr{\isachardot}T} \\ - \end{tabular} - - \begin{description} - - \item \isa{make}~\isa{thy}~\isa{consts} returns - a system of defining equations which is guaranteed - to contain all defining equations for constants \isa{consts} - including all defining equations any defining equation - for any constant in \isa{consts} depends on. - - \end{description} - - Systems of defining equations are graphs accesible by the - following operations:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimmlref -% -\endisadelimmlref -% -\isatagmlref -% -\begin{isamarkuptext}% -\begin{mldecls} - \indexmltype{CodeFuncgr.T}\verb|type CodeFuncgr.T| \\ - \indexml{CodeFuncgr.funcs}\verb|CodeFuncgr.funcs: CodeFuncgr.T -> CodeUnit.const -> thm list| \\ - \indexml{CodeFuncgr.typ}\verb|CodeFuncgr.typ: CodeFuncgr.T -> CodeUnit.const -> typ| \\ - \indexml{CodeFuncgr.deps}\verb|CodeFuncgr.deps: CodeFuncgr.T|\isasep\isanewline% -\verb| -> CodeUnit.const list -> CodeUnit.const list list| \\ - \indexml{CodeFuncgr.all}\verb|CodeFuncgr.all: CodeFuncgr.T -> CodeUnit.const list| - \end{mldecls} - - \begin{description} - - \item \verb|CodeFuncgr.T| represents - a normalized defining equation system. - - \item \verb|CodeFuncgr.funcs|~\isa{funcgr}~\isa{const} - retrieves defining equiations for constant \isa{const}. - - \item \verb|CodeFuncgr.typ|~\isa{funcgr}~\isa{const} - retrieves function type for constant \isa{const}. - - \item \verb|CodeFuncgr.deps|~\isa{funcgr}~\isa{consts} - returns the transitive closure of dependencies for - constants \isa{consts} as a partitioning where each partition - corresponds to a strongly connected component of - dependencies and any partition does \emph{not} - depend on partitions further left. - - \item \verb|CodeFuncgr.all|~\isa{funcgr} - returns all currently represented constants. - - \end{description}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagmlref -{\isafoldmlref}% -% -\isadelimmlref -% -\endisadelimmlref -% \isamarkupsubsubsection{Datatype hooks% } \isamarkuptrue%