# HG changeset patch # User haftmann # Date 1163453483 -3600 # Node ID 74c1da5d44be58986c127fc69fe1b4c32d15004b # Parent fccc48e844f5c0ce2fbfa3c7fa2601ec4d173a88 upd diff -r fccc48e844f5 -r 74c1da5d44be doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Mon Nov 13 22:21:09 2006 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Mon Nov 13 22:31:23 2006 +0100 @@ -69,7 +69,11 @@ structuring the process of code generation into a small set of orthogonal principles while achieving a big coverage of application areas - with maximum flexibility.% + with maximum flexibility. + + For readers, some familiarity and experience + with the the ingredients + of the HOL \emph{Main} theory is assumed.% \end{isamarkuptext}% \isamarkuptrue% % @@ -107,7 +111,14 @@ \isamarkuptrue% % \begin{isamarkuptext}% -The code generator employs a notion of executability +\begin{figure}[h] + \centering + \includegraphics[width=0.7\textwidth]{codegen_process} + \caption{code generator -- processing overview} + \label{fig:process} + \end{figure} + + The code generator employs a notion of executability for three foundational executable ingredients known from functional programming: \emph{function equations}, \emph{datatypes}, and @@ -141,13 +152,6 @@ \end{itemize} - \begin{figure}[h] - \centering - \includegraphics[width=0.3\textwidth]{codegen_process} - \caption{code generator -- processing overview} - \label{fig:process} - \end{figure} - From these steps, only the two last are carried out outside the logic; by keeping this layer as thin as possible, the amount of code to trust is @@ -183,7 +187,7 @@ \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% \ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% -The \isasymCODEGEN command takes a space-separated list of +The \isa{{\isasymCODEGEN}} command takes a space-separated list of constants together with \qn{serialization directives} in parentheses. These start with a \qn{target language} identifier, followed by arguments, their semantics @@ -286,7 +290,7 @@ % \begin{isamarkuptext}% The list of all function equations in a theory may be inspected - using the \isasymPRINTCODETHMS command:% + using the \isa{{\isasymPRINTCODETHMS}} command:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{print{\isacharunderscore}codethms}\isamarkupfalse% @@ -300,8 +304,9 @@ whether it provides one. The typical HOL tools are already set up in a way that - function definitions introduced by \isasymFUN, \isasymFUNCTION, - \isasymPRIMREC, \isasymRECDEF are implicitly propagated + function definitions introduced by \isa{{\isasymFUN}}, + \isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}} + \isa{{\isasymRECDEF}} are implicitly propagated to this function equation table. Specific theorems may be selected using an attribute: \emph{code func}. As example, a weight selector function:% @@ -514,14 +519,14 @@ Implementation of caching is supposed to transparently hid away the details from the user. Anyway, caching reaches the surface by using a slightly more general form - of the \isasymCODEGEN: either the list of constants or the + of the \isa{{\isasymCODEGEN}}: either the list of constants or the list of serialization expressions may be dropped. If no serialization expressions are given, only abstract code is generated and cached; if no constants are given, the current cache is serialized. - For explorative reasons, an extended version of the - \isasymCODEGEN command may prove useful:% + For explorative purpose, an extended version of the + \isa{{\isasymCODEGEN}} command may prove useful:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{print{\isacharunderscore}codethms}\isamarkupfalse% @@ -549,7 +554,7 @@ \item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} for exhaustive syntax diagrams. - \item or \fixme{ref} which deals with foundational issues + \item or \fixme[ref] which deals with foundational issues of the code generator framework. \end{itemize}% @@ -571,12 +576,12 @@ \item[ExecutableSet] allows to generate code for finite sets using lists. - \item[ExecutableRat] implements rational + \item[ExecutableRat] \label{exec_rat} implements rational numbers as triples \isa{{\isacharparenleft}sign{\isacharcomma}\ enumerator{\isacharcomma}\ denominator{\isacharparenright}}. - \item[EfficientNat] implements natural numbers by integers, + \item[EfficientNat] \label{eff_nat} implements natural numbers by integers, which in general will result in higher efficency; pattern matching with \isa{{\isadigit{0}}} / \isa{Suc} - is eliminated. \label{eff_nat} + is eliminated. \item[MLString] provides an additional datatype \isa{mlstring}; in the HOL default setup, strings in HOL are mapped to list of chars in SML; values of type \isa{mlstring} are @@ -668,7 +673,7 @@ % \begin{isamarkuptext}% The current set of inline theorems may be inspected using - the \isasymPRINTCODETHMS command. + the \isa{{\isasymPRINTCODETHMS}} command. \emph{Inline procedures} are a generalized version of inline theorems written in ML -- rewrite rules are generated dependent @@ -681,7 +686,8 @@ transforming a list of function theorems to another list of function theorems, provided that neither the heading constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc} - pattern elimination implemented in \secref{eff_nat} uses this + pattern elimination implemented in + theory EfficientNat (\secref{eff_nat}) uses this interface. \begin{warn} @@ -709,27 +715,24 @@ \isacommand{fun}\isamarkupfalse% \isanewline \ \ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}\isanewline -\isacommand{termination}\isamarkupfalse% +\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}% +\isadelimtt % -\isadelimproof -\ % -\endisadelimproof +\endisadelimtt +% +\isatagtt % -\isatagproof -\isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}% -\endisatagproof -{\isafoldproof}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +\isanewline % -\isadelimproof -% -\endisadelimproof -\isanewline +\endisadelimtt \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}literal{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% -\lstsml{Thy/examples/bool1.ML} +\lstsml{Thy/examples/bool_literal.ML} Though this is correct code, it is a little bit unsatisfactory: boolean values and operators are materialized as distinguished @@ -742,20 +745,33 @@ \qn{custom serializations}:% \end{isamarkuptext}% \isamarkuptrue% +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt \isacommand{code{\isacharunderscore}type}\isamarkupfalse% \ bool\isanewline \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline \isacommand{code{\isacharunderscore}const}\isamarkupfalse% \ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% \begin{isamarkuptext}% -The \isasymCODETYPE commad takes a type constructor +The \isa{{\isasymCODETYPE}} commad takes a type constructor as arguments together with a list of custom serializations. Each custom serialization starts with a target language identifier followed by an expression, which during code serialization is inserted whenever the type constructor - would occur. For constants, \isasymCODECONST implements - the corresponding mechanism. Each \qt{\_} in + would occur. For constants, \isa{{\isasymCODECONST}} implements + the corresponding mechanism. Each ``\verb|_|'' in a serialization expression is treated as a placeholder for the type constructor's (the constant's) arguments.% \end{isamarkuptext}% @@ -765,37 +781,57 @@ \ \ bool\ true\ false% \begin{isamarkuptext}% To assert that the existing \qt{bool}, \qt{true} and \qt{false} - is not used for generated code, we use \isasymCODERESERVED. + is not used for generated code, we use \isa{{\isasymCODERESERVED}}. After this setup, code looks quite more readable:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% -\lstsml{Thy/examples/bool2.ML} +\lstsml{Thy/examples/bool_mlbool.ML} This still is not perfect: the parentheses - around \qt{andalso} are superfluous. Though the serializer + around the \qt{andalso} expression are superfluous. + Though the serializer by no means attempts to imitate the rich Isabelle syntax framework, it provides some common idioms, notably associative infixes with precedences which may be used here:% \end{isamarkuptext}% \isamarkuptrue% +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt \isacommand{code{\isacharunderscore}const}\isamarkupfalse% \ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline -\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}\isanewline +\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +\isanewline \isanewline \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isadigit{3}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}infix{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% -\lstsml{Thy/examples/bool3.ML} +\lstsml{Thy/examples/bool_infix.ML} Next, we try to map HOL pairs to SML pairs, using the - infix \qt{ * } type constructor and parentheses:% + infix ``\verb|*|'' type constructor and parentheses:% \end{isamarkuptext}% \isamarkuptrue% \isanewline +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt \isacommand{code{\isacharunderscore}type}\isamarkupfalse% \ {\isacharasterisk}\isanewline \ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline @@ -803,12 +839,19 @@ \isacommand{code{\isacharunderscore}const}\isamarkupfalse% \ Pair\isanewline \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% \begin{isamarkuptext}% -The initial bang \qt{!} tells the serializer to never put +The initial bang ``\verb|!|'' tells the serializer to never put parentheses around the whole expression (they are already present), while the parentheses around argument place holders tell not to put parentheses around the arguments. - The slash \qt{/} (followed by arbitrary white space) + The slash ``\verb|/|'' (followed by arbitrary white space) inserts a space which may be used as a break if necessary during pretty printing. @@ -834,6 +877,12 @@ integers:% \end{isamarkuptext}% \isamarkuptrue% +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt \isacommand{code{\isacharunderscore}type}\isamarkupfalse% \ int\isanewline \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}int{\isachardoublequoteclose}{\isacharparenright}\isanewline @@ -841,7 +890,14 @@ \isacommand{code{\isacharunderscore}const}\isamarkupfalse% \ {\isachardoublequoteopen}op\ {\isacharplus}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isacharasterisk}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +\isanewline \isanewline \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% \ double{\isacharunderscore}inc\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}integers{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% @@ -861,9 +917,10 @@ A further noteworthy details is that any special character in a custom serialization may be quoted - using \qt{'}; thus, in \qt{fn '\_ => \_} the first - \qt{'\_} is a proper underscore while the - second \qt{\_} is a placeholder. + using ``\verb|'|''; thus, in + ``\verb|fn '_ => _|'' the first + ``\verb|_|'' is a proper underscore while the + second ``\verb|_|'' is a placeholder. The HOL theories provide further examples for custom serializations and form @@ -888,25 +945,9 @@ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline -\ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isacommand{termination}\isamarkupfalse% -% -\isadelimproof -\ % -\endisadelimproof -% -\isatagproof -\isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ {\isacharparenleft}length\ o\ snd\ o\ snd{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% +\ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% -The membership test during preprocessing is rewriting, +The membership test during preprocessing is rewritten, resulting in \isa{op\ mem}, which itself performs an explicit equality check.% \end{isamarkuptext}% @@ -982,9 +1023,22 @@ Examine the following:% \end{isamarkuptext}% \isamarkuptrue% +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt \isacommand{code{\isacharunderscore}const}\isamarkupfalse% \ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% \begin{isamarkuptext}% What is wrong here? Since \isa{op\ {\isacharequal}} is nothing else then a plain constant, this customary serialization will refer @@ -993,10 +1047,23 @@ by using the overloaded constant \isa{Code{\isacharunderscore}Generator{\isachardot}eq}:% \end{isamarkuptext}% \isamarkuptrue% +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt \isacommand{code{\isacharunderscore}const}\isamarkupfalse% \ {\isachardoublequoteopen}Code{\isacharunderscore}Generator{\isachardot}eq\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% -\isamarkupsubsubsection{typedecls interpretated by customary serializations% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% +\isamarkupsubsubsection{typedecls interpreted by customary serializations% } \isamarkuptrue% % @@ -1013,25 +1080,22 @@ \ \ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}key\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ list\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ {\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline \ \ {\isachardoublequoteopen}lookup\ {\isacharbrackleft}{\isacharbrackright}\ l\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline \ \ {\isachardoublequoteopen}lookup\ {\isacharparenleft}{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharhash}\ xs{\isacharparenright}\ l\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isacharequal}\ l\ then\ Some\ v\ else\ lookup\ xs\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isacommand{termination}\isamarkupfalse% % -\isadelimproof -\ % -\endisadelimproof +\isadelimtt % -\isatagproof -\isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ {\isacharparenleft}length\ o\ fst{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% -\endisatagproof -{\isafoldproof}% +\endisadelimtt % -\isadelimproof -% -\endisadelimproof -\isanewline +\isatagtt \isacommand{code{\isacharunderscore}type}\isamarkupfalse% \ key\isanewline \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}string{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% \begin{isamarkuptext}% This, though, is not sufficient: \isa{key} is no instance of \isa{eq} since \isa{key} is no datatype; the instance @@ -1055,10 +1119,23 @@ % \endisadelimproof \isanewline +% +\isadelimtt \isanewline +% +\endisadelimtt +% +\isatagtt \isacommand{code{\isacharunderscore}const}\isamarkupfalse% \ {\isachardoublequoteopen}Code{\isacharunderscore}Generator{\isachardot}eq\ {\isasymColon}\ key\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ string\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% \begin{isamarkuptext}% Then everything goes fine:% \end{isamarkuptext}% @@ -1078,7 +1155,7 @@ Another subtlety enters the stage when definitions of overloaded constants are dependent on operational equality. For example, let - us define a lexicographic ordering on tuples: \\% + us define a lexicographic ordering on tuples:% \end{isamarkuptext}% \isamarkuptrue% % @@ -1177,7 +1254,7 @@ For convenience, the default HOL setup for Haskell maps the \isa{eq} class to its counterpart in Haskell, giving custom serializations - for the class (\isasymCODECLASS) and its operation:% + for the class (\isa{{\isasymCODECLASS}}) and its operation:% \end{isamarkuptext}% \isamarkuptrue% % @@ -1194,6 +1271,12 @@ % \endisadelimML \isanewline +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt \isacommand{code{\isacharunderscore}class}\isamarkupfalse% \ eq\isanewline \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ eq\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline @@ -1202,6 +1285,13 @@ \ eq\isanewline \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\isanewline % +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% \isadelimML % \endisadelimML @@ -1241,41 +1331,197 @@ % \endisadelimproof \isanewline +% +\isadelimtt \isanewline +% +\endisadelimtt +% +\isatagtt \isacommand{code{\isacharunderscore}type}\isamarkupfalse% \ bar\isanewline \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% \begin{isamarkuptext}% The code generator would produce an additional instance, which of course is rejected. To suppress this additional instance, use - \isasymCODEINSTANCE:% + \isa{{\isasymCODEINSTANCE}}:% \end{isamarkuptext}% \isamarkuptrue% +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt \isacommand{code{\isacharunderscore}instance}\isamarkupfalse% \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +% \isamarkupsubsection{Types matter% } \isamarkuptrue% % \begin{isamarkuptext}% Imagine the following quick-and-dirty setup for implementing - some sets as lists:% + some kind of sets as lists in SML:% \end{isamarkuptext}% \isamarkuptrue% +% +\isadelimtt +% +\endisadelimtt +% +\isatagtt \isacommand{code{\isacharunderscore}type}\isamarkupfalse% \ set\isanewline \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharunderscore}\ list{\isachardoublequoteclose}{\isacharparenright}\isanewline \isanewline \isacommand{code{\isacharunderscore}const}\isamarkupfalse% \ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ insert\isanewline -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{and}\ \isakeyword{infixl}\ {\isadigit{7}}\ {\isachardoublequoteopen}{\isacharcolon}{\isacharcolon}{\isachardoublequoteclose}{\isacharparenright}\isanewline +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{and}\ \isakeyword{infixl}\ {\isadigit{7}}\ {\isachardoublequoteopen}{\isacharcolon}{\isacharcolon}{\isachardoublequoteclose}{\isacharparenright}% +\endisatagtt +{\isafoldtt}% +% +\isadelimtt +% +\endisadelimtt +\isanewline \isanewline \isacommand{definition}\isamarkupfalse% \isanewline -\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbraceright}{\isachardoublequoteclose}% +\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}Suc{\isacharbraceright}{\isachardoublequoteclose}% +\begin{isamarkuptext}% +Then code generation for \isa{dummy{\isacharunderscore}set} will fail. + Why? A glimpse at the function equations will offer:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse% +\ {\isacharparenleft}insert{\isacharparenright}% +\begin{isamarkuptext}% +This reveals the function equation \isa{insert\ {\isacharquery}a\ {\isacharquery}B\ {\isasymequiv}\ {\isacharbraceleft}x{\isachardot}\ x\ {\isacharequal}\ {\isacharquery}a{\isacharbraceright}\ {\isasymunion}\ {\isacharquery}B} + for \isa{insert}, which is operationally meaningless + but forces an equality constraint on the set members + (which is not satisfiable if the set members are functions). + Even when using set of natural numbers (which are an instance + of \emph{eq}), we run into a problem:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{definition}\isamarkupfalse% +\isanewline +\ \ foobar{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}foobar{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequoteclose}% +\begin{isamarkuptext}% +In this case the serializer would complain that \isa{insert} + expects dictionaries (namely an \emph{eq} dictionary) but + has also been given a customary serialization. + + The solution to this dilemma:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}insert\ {\isacharequal}\ insert{\isachardoublequoteclose}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isanewline +\isacommand{code{\isacharunderscore}gen}\isamarkupfalse% +\ dummy{\isacharunderscore}set\ foobar{\isacharunderscore}set\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}dirty{\isacharunderscore}set{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\begin{isamarkuptext}% +\lstsml{Thy/examples/dirty_set.ML} + + Reflexive function equations by convention are dropped. + But their presence prevents primitive definitions to be + used as function equations:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse% +\ {\isacharparenleft}insert{\isacharparenright}% +\begin{isamarkuptext}% +will show \emph{no} function equations for insert. + + Note that the sort constraints of reflexive equations + are considered; so% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}{\isacharparenleft}insert\ {\isasymColon}\ {\isacharprime}a{\isasymColon}eq\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}\ {\isacharequal}\ insert{\isachardoublequoteclose}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +would mean nothing else than to introduce the evil + sort constraint by hand.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Cyclic module dependencies% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Sometimes the awkward situation occurs that dependencies + between definitions introduce cyclic dependencies + between modules, which in the Haskell world leaves + you to the mercy of the Haskell implementation you are using, + while for SML 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% +\isacommand{code{\isacharunderscore}modulename}\isamarkupfalse% +\ SML\isanewline +\ \ A\ ABC\isanewline +\ \ B\ ABC\isanewline +\ \ C\ ABC% +\begin{isamarkuptext}% +we explicitly map all those modules on \emph{ABC}, + resulting in an ad-hoc merge of this three modules + at serialization time.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Axiomatic extensions% } \isamarkuptrue% @@ -1283,9 +1529,81 @@ \begin{isamarkuptext}% \begin{warn} The extensions introduced in this section, though working - in practice, are not the cream of the crop. They will + 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}% + \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}\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 function 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 datatype 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 +\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}\isanewline +\isacommand{code{\isacharunderscore}gen}\isamarkupfalse% +\ dummy{\isacharunderscore}option\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}arbitrary{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\begin{isamarkuptext}% +\lstsml{Thy/examples/arbitrary.ML} + + Another axiomatic extension is code generation + for abstracted types. For this, the + ExecutableRat (see \secref{exec_rat}) + forms a good example.% \end{isamarkuptext}% \isamarkuptrue% % @@ -1293,10 +1611,24 @@ } \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 important ML interfaces.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Constants with type discipline: codegen\_consts.ML% } \isamarkuptrue% % +\begin{isamarkuptext}% +This Pure module manages identification of (probably overloaded) + constants by unique identifiers.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isadelimmlref % \endisadelimmlref @@ -1305,12 +1637,27 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexmltype{CodegenConsts.const}\verb|type CodegenConsts.const| \\ - \indexml{CodegenConsts.inst-of-typ}\verb|CodegenConsts.inst_of_typ: theory -> string * typ -> CodegenConsts.const| \\ + \indexmltype{CodegenConsts.const}\verb|type CodegenConsts.const = string * typ list| \\ + \indexml{CodegenConsts.norm-of-typ}\verb|CodegenConsts.norm_of_typ: theory -> string * typ -> CodegenConsts.const| \\ \indexml{CodegenConsts.typ-of-inst}\verb|CodegenConsts.typ_of_inst: theory -> CodegenConsts.const -> string * typ| \\ - \indexml{CodegenConsts.norm}\verb|CodegenConsts.norm: theory -> CodegenConsts.const -> CodegenConsts.const| \\ - \indexml{CodegenConsts.norm-of-typ}\verb|CodegenConsts.norm_of_typ: theory -> string * typ -> CodegenConsts.const| - \end{mldecls}% + \end{mldecls} + + \begin{description} + + \item \verb|CodegenConsts.const| is the identifier type: + the product of a \emph{string} with a list of \emph{typs}. + The \emph{string} is the constant name as represented inside Isabelle; + the \emph{typs} are a type instantiation in the sense of System F, + with canonical names for type variables. + + \item \verb|CodegenConsts.norm_of_typ|~\isa{thy}~\isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}} + maps a constant expression \isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}} to its canonical identifier. + + \item \verb|CodegenConsts.typ_of_inst|~\isa{thy}~\isa{const} + maps a canonical identifier \isa{const} to a constant + expression with appropriate type. + + \end{description}% \end{isamarkuptext}% \isamarkuptrue% % @@ -1343,9 +1690,15 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexmltype{CodegenData.lthms}\verb|type CodegenData.lthms| \\ - \indexml{CodegenData.lazy}\verb|CodegenData.lazy: (unit -> thm list) -> CodegenData.lthms| - \end{mldecls}% + \indexml{CodegenData.lazy}\verb|CodegenData.lazy: (unit -> thm list) -> thm list Susp.T| + \end{mldecls} + + \begin{description} + + \item \verb|CodegenData.lazy|~\isa{f} turns an abstract + theorem computation \isa{f} into a suspension of theorems. + + \end{description}% \end{isamarkuptext}% \isamarkuptrue% % @@ -1370,21 +1723,134 @@ \begin{mldecls} \indexml{CodegenData.add-func}\verb|CodegenData.add_func: thm -> theory -> theory| \\ \indexml{CodegenData.del-func}\verb|CodegenData.del_func: thm -> theory -> theory| \\ - \indexml{CodegenData.add-funcl}\verb|CodegenData.add_funcl: CodegenConsts.const * CodegenData.lthms -> theory -> theory| \\ - \indexml{CodegenData.add-datatype}\verb|CodegenData.add_datatype: string * (((string * sort) list * (string * typ list) list) * CodegenData.lthms) -> theory -> theory| \\ - \indexml{CodegenData.del-datatype}\verb|CodegenData.del_datatype: string -> theory -> theory| \\ + \indexml{CodegenData.add-funcl}\verb|CodegenData.add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory| \\ \indexml{CodegenData.add-inline}\verb|CodegenData.add_inline: thm -> theory -> theory| \\ \indexml{CodegenData.del-inline}\verb|CodegenData.del_inline: thm -> theory -> theory| \\ - \indexml{CodegenData.add-inline-proc}\verb|CodegenData.add_inline_proc: (theory -> cterm list -> thm list) -> theory -> theory| \\ - \indexml{CodegenData.add-preproc}\verb|CodegenData.add_preproc: (theory -> thm list -> thm list) -> theory -> theory| \\ - \indexml{CodegenData.these-funcs}\verb|CodegenData.these_funcs: theory -> CodegenConsts.const -> thm list| \\ - \indexml{CodegenData.get-datatype}\verb|CodegenData.get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) option| \\ + \indexml{CodegenData.add-inline-proc}\verb|CodegenData.add_inline_proc: (theory -> cterm list -> thm list)|\isasep\isanewline% +\verb| -> theory -> theory| \\ + \indexml{CodegenData.add-preproc}\verb|CodegenData.add_preproc: (theory -> thm list -> thm list)|\isasep\isanewline% +\verb| -> theory -> theory| \\ + \indexml{CodegenData.add-datatype}\verb|CodegenData.add_datatype: string * (((string * sort) list * (string * typ list) list)|\isasep\isanewline% +\verb| * thm list Susp.T) -> theory -> theory| \\ + \indexml{CodegenData.del-datatype}\verb|CodegenData.del_datatype: string -> theory -> theory| \\ + \indexml{CodegenData.get-datatype}\verb|CodegenData.get_datatype: theory -> string|\isasep\isanewline% +\verb| -> ((string * sort) list * (string * typ list) list) option| \\ \indexml{CodegenData.get-datatype-of-constr}\verb|CodegenData.get_datatype_of_constr: theory -> CodegenConsts.const -> string option| \end{mldecls} \begin{description} - \item \verb|CodegenData.add_func|~\isa{thm} + \item \verb|CodegenData.add_func|~\isa{thm}~\isa{thy} adds function + theorem \isa{thm} to executable content. + + \item \verb|CodegenData.del_func|~\isa{thm}~\isa{thy} removes function + theorem \isa{thm} from executable content, if present. + + \item \verb|CodegenData.add_funcl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds + suspended function equations \isa{lthms} for constant + \isa{const} to executable content. + + \item \verb|CodegenData.add_inline|~\isa{thm}~\isa{thy} adds + inlining theorem \isa{thm} to executable content. + + \item \verb|CodegenData.del_inline|~\isa{thm}~\isa{thy} remove + inlining theorem \isa{thm} from executable content, if present. + + \item \verb|CodegenData.add_inline_proc|~\isa{f}~\isa{thy} adds + inline procedure \isa{f} to executable content; + \isa{f} is a computation of rewrite rules dependent on + the current theory context and the list of all arguments + and right hand sides of the function equations belonging + to a certain function definition. + + \item \verb|CodegenData.add_preproc|~\isa{f}~\isa{thy} adds + generic preprocessor \isa{f} to executable content; + \isa{f} is a transformation of the function equations belonging + to a certain function definition, depending on the + current theory context. + + \item \verb|CodegenData.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ {\isacharparenleft}spec{\isacharcomma}\ cert{\isacharparenright}{\isacharparenright}}~\isa{thy} adds + a datatype to executable content, with type constructor + \isa{name} and specification \isa{spec}; \isa{spec} is + a pair consisting of a list of type variable with sort + constraints and a list of constructors with name + and types of arguments. The addition as datatype + has to be justified giving a certificate of suspended + theorems as witnesses for injectiveness and distinctness. + + \item \verb|CodegenData.del_datatype|~\isa{name}~\isa{thy} + remove a datatype from executable content, if present. + + \item \verb|CodegenData.get_datatype_of_constr|~\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 +% +\isamarkupsubsection{Function equation systems: codegen\_funcgr.ML% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Out of the executable content of a theory, a normalized + function equation systems may be constructed containing + function definitions for constants. The system is cached + until its underlying executable content changes.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexmltype{CodegenFuncgr.T}\verb|type CodegenFuncgr.T| \\ + \indexml{CodegenFuncgr.make}\verb|CodegenFuncgr.make: theory -> CodegenConsts.const list -> CodegenFuncgr.T| \\ + \indexml{CodegenFuncgr.funcs}\verb|CodegenFuncgr.funcs: CodegenFuncgr.T -> CodegenConsts.const -> thm list| \\ + \indexml{CodegenFuncgr.typ}\verb|CodegenFuncgr.typ: CodegenFuncgr.T -> CodegenConsts.const -> typ| \\ + \indexml{CodegenFuncgr.deps}\verb|CodegenFuncgr.deps: CodegenFuncgr.T|\isasep\isanewline% +\verb| -> CodegenConsts.const list -> CodegenConsts.const list list| \\ + \indexml{CodegenFuncgr.all}\verb|CodegenFuncgr.all: CodegenFuncgr.T -> CodegenConsts.const list| + \end{mldecls} + + \begin{description} + + \item \verb|CodegenFuncgr.T| represents + a normalized function equation system. + + \item \verb|CodegenFuncgr.make|~\isa{thy}~\isa{cs} + returns a normalized function equation system, + with the assertion that it contains any function + definition for constants \isa{cs} (if existing). + + \item \verb|CodegenFuncgr.funcs|~\isa{funcgr}~\isa{c} + retrieves function definition for constant \isa{c}. + + \item \verb|CodegenFuncgr.typ|~\isa{funcgr}~\isa{c} + retrieves function type for constant \isa{c}. + + \item \verb|CodegenFuncgr.deps|~\isa{funcgr}~\isa{cs} + returns the transitive closure of dependencies for + constants \isa{cs} 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|CodegenFuncgr.all|~\isa{funcgr} + returns all currently represented constants. \end{description}% \end{isamarkuptext}% @@ -1414,9 +1880,34 @@ \indexml{CodegenConsts.consts-of}\verb|CodegenConsts.consts_of: theory -> term -> CodegenConsts.const list| \\ \indexml{CodegenConsts.read-const}\verb|CodegenConsts.read_const: theory -> string -> CodegenConsts.const| \\ \indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\ + \indexmlstructure{CodegenFuncgr.Constgraph}\verb|structure CodegenFuncgr.Constgraph| \\ \indexml{CodegenData.typ-func}\verb|CodegenData.typ_func: theory -> thm -> typ| \\ \indexml{CodegenData.rewrite-func}\verb|CodegenData.rewrite_func: thm list -> thm -> thm| \\ - \end{mldecls}% + \end{mldecls} + + \begin{description} + + \item \verb|CodegenConsts.const_ord|,~\verb|CodegenConsts.eq_const| + provide order and equality on constant identifiers. + + \item \verb|CodegenConsts.Consttab|,~\verb|CodegenFuncgr.Constgraph| + provide advanced data structures with constant identifiers as keys. + + \item \verb|CodegenConsts.consts_of|~\isa{thy}~\isa{t} + returns all constant identifiers mentioned in a term \isa{t}. + + \item \verb|CodegenConsts.read_const|~\isa{thy}~\isa{s} + reads a constant as a concrete term expression \isa{s}. + + \item \verb|CodegenData.typ_func|~\isa{thy}~\isa{thm} + extracts the type of a constant in a function equation \isa{thm}. + + \item \verb|CodegenData.rewrite_func|~\isa{rews}~\isa{thm} + rewrites a function equation \isa{thm} with a set of rewrite + rules \isa{rews}; only arguments and right hand side are rewritten, + not the head of the function equation. + + \end{description}% \end{isamarkuptext}% \isamarkuptrue% % @@ -1432,11 +1923,19 @@ \isamarkuptrue% % \begin{isamarkuptext}% -\begin{warn} +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. + + \begin{warn} Some interfaces discussed here have not reached a final state yet. Changes likely to occur in future. - \end{warn}% + \end{warn} + + \fixme% \end{isamarkuptext}% \isamarkuptrue% % @@ -1444,12 +1943,118 @@ } \isamarkuptrue% % +\begin{isamarkuptext}% +\medskip + \begin{tabular}{l} + \isa{val\ name{\isacharcolon}\ string} \\ + \isa{type\ T} \\ + \isa{val\ empty{\isacharcolon}\ T} \\ + \isa{val\ merge{\isacharcolon}\ Pretty{\isachardot}pp\ {\isasymrightarrow}\ T\ {\isacharasterisk}\ T\ {\isasymrightarrow}\ T} \\ + \isa{val\ purge{\isacharcolon}\ theory\ option\ {\isasymrightarrow}\ CodegenConsts{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T} + \end{tabular} + + \medskip + + \begin{tabular}{l} + \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ theory} \\ + \isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\ + \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\ + \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T} + \end{tabular}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexmlfunctor{CodeDataFun}\verb|functor CodeDataFun| + \end{mldecls} + + \begin{description} + + \item \verb|CodeDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares code + dependent data according to the specification provided as + argument structure. The resulting structure provides data init and + access operations as described above. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref +% \isamarkupsubsubsection{Datatype hooks% } \isamarkuptrue% % +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% \begin{isamarkuptext}% -\emph{Happy proving, happy hacking!}% +\begin{mldecls} + \indexmltype{DatatypeHooks.hook}\verb|type DatatypeHooks.hook = string list -> theory -> theory| \\ + \indexml{DatatypeHooks.add}\verb|DatatypeHooks.add: DatatypeHooks.hook -> theory -> theory| + \end{mldecls}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexmltype{TypecopyPackage.info}\verb|type TypecopyPackage.info = {|\isasep\isanewline% +\verb| vs: (string * sort) list,|\isasep\isanewline% +\verb| constr: string,|\isasep\isanewline% +\verb| typ: typ,|\isasep\isanewline% +\verb| inject: thm,|\isasep\isanewline% +\verb| proj: string * typ,|\isasep\isanewline% +\verb| proj_def: thm|\isasep\isanewline% +\verb| }| \\ + \indexml{TypecopyPackage.add-typecopy}\verb|TypecopyPackage.add_typecopy: |\isasep\isanewline% +\verb| bstring * string list -> typ -> (bstring * bstring) option|\isasep\isanewline% +\verb| -> theory -> (string * TypecopyPackage.info) * theory| \\ + \indexml{TypecopyPackage.get-typecopies}\verb|TypecopyPackage.get_typecopies: theory -> string list| \\ + \indexml{TypecopyPackage.get-typecopy-info}\verb|TypecopyPackage.get_typecopy_info: theory|\isasep\isanewline% +\verb| -> string -> TypecopyPackage.info option| \\ + \indexmltype{TypecopyPackage.hook}\verb|type TypecopyPackage.hook| \\ + \indexml{TypecopyPackage.add-hook}\verb|TypecopyPackage.add_hook: TypecopyPackage.hook -> theory -> theory| \\ + \indexml{TypecopyPackage.get-spec}\verb|TypecopyPackage.get_spec: theory -> string|\isasep\isanewline% +\verb| -> (string * sort) list * (string * typ list) list| + \end{mldecls}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexmltype{DatatypeCodegen.hook}\verb|type DatatypeCodegen.hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list|\isasep\isanewline% +\verb| -> theory -> theory| \\ + \indexml{DatatypeCodegen.add-codetypes-hook-bootstrap}\verb|DatatypeCodegen.add_codetypes_hook_bootstrap: |\isasep\isanewline% +\verb| DatatypeCodegen.hook -> theory -> theory| + \end{mldecls}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref +% +\begin{isamarkuptext}% +\fixme +% \emph{Happy proving, happy hacking!}% \end{isamarkuptext}% \isamarkuptrue% %