doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
author haftmann
Tue Jul 15 16:02:07 2008 +0200 (2008-07-15)
changeset 27609 b23c9ad0fe7d
parent 27557 151731493264
child 28143 e5c6c4aac52c
permissions -rw-r--r--
tuned code theorem bookkeeping
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Codegen}%
     4 %
     5 \isadelimtheory
     6 \isanewline
     7 \isanewline
     8 %
     9 \endisadelimtheory
    10 %
    11 \isatagtheory
    12 %
    13 \endisatagtheory
    14 {\isafoldtheory}%
    15 %
    16 \isadelimtheory
    17 %
    18 \endisadelimtheory
    19 %
    20 \isadelimML
    21 %
    22 \endisadelimML
    23 %
    24 \isatagML
    25 %
    26 \endisatagML
    27 {\isafoldML}%
    28 %
    29 \isadelimML
    30 %
    31 \endisadelimML
    32 %
    33 \isamarkupchapter{Code generation from Isabelle theories%
    34 }
    35 \isamarkuptrue%
    36 %
    37 \isamarkupsection{Introduction%
    38 }
    39 \isamarkuptrue%
    40 %
    41 \isamarkupsubsection{Motivation%
    42 }
    43 \isamarkuptrue%
    44 %
    45 \begin{isamarkuptext}%
    46 Executing formal specifications as programs is a well-established
    47   topic in the theorem proving community.  With increasing
    48   application of theorem proving systems in the area of
    49   software development and verification, its relevance manifests
    50   for running test cases and rapid prototyping.  In logical
    51   calculi like constructive type theory,
    52   a notion of executability is implicit due to the nature
    53   of the calculus.  In contrast, specifications in Isabelle
    54   can be highly non-executable.  In order to bridge
    55   the gap between logic and executable specifications,
    56   an explicit non-trivial transformation has to be applied:
    57   code generation.
    58 
    59   This tutorial introduces a generic code generator for the
    60   Isabelle system \cite{isa-tutorial}.
    61   Generic in the sense that the
    62   \qn{target language} for which code shall ultimately be
    63   generated is not fixed but may be an arbitrary state-of-the-art
    64   functional programming language (currently, the implementation
    65   supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell
    66   \cite{haskell-revised-report}).
    67   We aim to provide a
    68   versatile environment
    69   suitable for software development and verification,
    70   structuring the process
    71   of code generation into a small set of orthogonal principles
    72   while achieving a big coverage of application areas
    73   with maximum flexibility.
    74 
    75   Conceptually the code generator framework is part
    76   of Isabelle's \isa{Pure} meta logic; the object logic
    77   \isa{HOL} which is an extension of \isa{Pure}
    78   already comes with a reasonable framework setup and thus provides
    79   a good working horse for raising code-generation-driven
    80   applications.  So, we assume some familiarity and experience
    81   with the ingredients of the \isa{HOL} \emph{Main} theory
    82   (see also \cite{isa-tutorial}).%
    83 \end{isamarkuptext}%
    84 \isamarkuptrue%
    85 %
    86 \isamarkupsubsection{Overview%
    87 }
    88 \isamarkuptrue%
    89 %
    90 \begin{isamarkuptext}%
    91 The code generator aims to be usable with no further ado
    92   in most cases while allowing for detailed customization.
    93   This manifests in the structure of this tutorial:
    94   we start with a generic example \secref{sec:example}
    95   and introduce code generation concepts \secref{sec:concept}.
    96   Section
    97   \secref{sec:basics} explains how to use the framework naively,
    98   presuming a reasonable default setup.  Then, section
    99   \secref{sec:advanced} deals with advanced topics,
   100   introducing further aspects of the code generator framework
   101   in a motivation-driven manner.  Last, section \secref{sec:ml}
   102   introduces the framework's internal programming interfaces.
   103 
   104   \begin{warn}
   105     Ultimately, the code generator which this tutorial deals with
   106     is supposed to replace the already established code generator
   107     by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
   108     So, for the moment, there are two distinct code generators
   109     in Isabelle.
   110     Also note that while the framework itself is
   111     object-logic independent, only \isa{HOL} provides a reasonable
   112     framework setup.    
   113   \end{warn}%
   114 \end{isamarkuptext}%
   115 \isamarkuptrue%
   116 %
   117 \isamarkupsection{An example: a simple theory of search trees \label{sec:example}%
   118 }
   119 \isamarkuptrue%
   120 %
   121 \begin{isamarkuptext}%
   122 When writing executable specifications using \isa{HOL},
   123   it is convenient to use
   124   three existing packages: the datatype package for defining
   125   datatypes, the function package for (recursive) functions,
   126   and the class package for overloaded definitions.
   127 
   128   We develope a small theory of search trees; trees are represented
   129   as a datatype with key type \isa{{\isacharprime}a} and value type \isa{{\isacharprime}b}:%
   130 \end{isamarkuptext}%
   131 \isamarkuptrue%
   132 \isacommand{datatype}\isamarkupfalse%
   133 \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isacharequal}\ Leaf\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}linorder{\isachardoublequoteclose}\ {\isacharprime}b\isanewline
   134 \ \ {\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}%
   135 \begin{isamarkuptext}%
   136 \noindent Note that we have constrained the type of keys
   137   to the class of total orders, \isa{linorder}.
   138 
   139   We define \isa{find} and \isa{update} functions:%
   140 \end{isamarkuptext}%
   141 \isamarkuptrue%
   142 \isacommand{primrec}\isamarkupfalse%
   143 \isanewline
   144 \ \ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isasymColon}linorder{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   145 \ \ {\isachardoublequoteopen}find\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ it\ {\isacharequal}\ {\isacharparenleft}if\ it\ {\isacharequal}\ key\ then\ Some\ val\ else\ None{\isacharparenright}{\isachardoublequoteclose}\isanewline
   146 \ \ {\isacharbar}\ {\isachardoublequoteopen}find\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ t{\isadigit{2}}{\isacharparenright}\ it\ {\isacharequal}\ {\isacharparenleft}if\ it\ {\isasymle}\ key\ then\ find\ t{\isadigit{1}}\ it\ else\ find\ t{\isadigit{2}}\ it{\isacharparenright}{\isachardoublequoteclose}\isanewline
   147 \isanewline
   148 \isacommand{fun}\isamarkupfalse%
   149 \isanewline
   150 \ \ update\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}linorder\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   151 \ \ {\isachardoublequoteopen}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}\isanewline
   152 \ \ \ \ if\ it\ {\isacharequal}\ key\ then\ Leaf\ key\ entry\isanewline
   153 \ \ \ \ \ \ else\ if\ it\ {\isasymle}\ key\isanewline
   154 \ \ \ \ \ \ then\ Branch\ {\isacharparenleft}Leaf\ it\ entry{\isacharparenright}\ it\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\isanewline
   155 \ \ \ \ \ \ else\ Branch\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ it\ {\isacharparenleft}Leaf\ it\ entry{\isacharparenright}\isanewline
   156 \ \ \ {\isacharparenright}{\isachardoublequoteclose}\isanewline
   157 \ \ {\isacharbar}\ {\isachardoublequoteopen}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ t{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}\isanewline
   158 \ \ \ \ if\ it\ {\isasymle}\ key\isanewline
   159 \ \ \ \ \ \ then\ {\isacharparenleft}Branch\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{1}}{\isacharparenright}\ key\ t{\isadigit{2}}{\isacharparenright}\isanewline
   160 \ \ \ \ \ \ else\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{2}}{\isacharparenright}{\isacharparenright}\isanewline
   161 \ \ \ {\isacharparenright}{\isachardoublequoteclose}%
   162 \begin{isamarkuptext}%
   163 \noindent For testing purpose, we define a small example
   164   using natural numbers \isa{nat} (which are a \isa{linorder})
   165   as keys and list of nats as values:%
   166 \end{isamarkuptext}%
   167 \isamarkuptrue%
   168 \isacommand{definition}\isamarkupfalse%
   169 \isanewline
   170 \ \ example\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat{\isacharcomma}\ nat\ list{\isacharparenright}\ searchtree{\isachardoublequoteclose}\isanewline
   171 \isakeyword{where}\isanewline
   172 \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ update\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharcomma}\ {\isacharbrackleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}update\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isacharcomma}\ {\isacharbrackleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\isanewline
   173 \ \ \ \ {\isacharparenleft}update\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ {\isacharbrackleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}Leaf\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
   174 \begin{isamarkuptext}%
   175 \noindent Then we generate code%
   176 \end{isamarkuptext}%
   177 \isamarkuptrue%
   178 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
   179 \ example\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}%
   180 \begin{isamarkuptext}%
   181 \noindent which looks like:
   182   \lstsml{Thy/examples/tree.ML}%
   183 \end{isamarkuptext}%
   184 \isamarkuptrue%
   185 %
   186 \isamarkupsection{Code generation concepts and process \label{sec:concept}%
   187 }
   188 \isamarkuptrue%
   189 %
   190 \begin{isamarkuptext}%
   191 \begin{figure}[h]
   192   \centering
   193   \includegraphics[width=0.7\textwidth]{codegen_process}
   194   \caption{code generator -- processing overview}
   195   \label{fig:process}
   196   \end{figure}
   197 
   198   The code generator employs a notion of executability
   199   for three foundational executable ingredients known
   200   from functional programming:
   201   \emph{defining equations}, \emph{datatypes}, and
   202   \emph{type classes}. A defining equation as a first approximation
   203   is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t}
   204   (an equation headed by a constant \isa{f} with arguments
   205   \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}).
   206   Code generation aims to turn defining equations
   207   into a functional program by running through
   208   a process (see figure \ref{fig:process}):
   209 
   210   \begin{itemize}
   211 
   212     \item Out of the vast collection of theorems proven in a
   213       \qn{theory}, a reasonable subset modeling
   214       defining equations is \qn{selected}.
   215 
   216     \item On those selected theorems, certain
   217       transformations are carried out
   218       (\qn{preprocessing}).  Their purpose is to turn theorems
   219       representing non- or badly executable
   220       specifications into equivalent but executable counterparts.
   221       The result is a structured collection of \qn{code theorems}.
   222 
   223     \item These \qn{code theorems} then are \qn{translated}
   224       into an Haskell-like intermediate
   225       language.
   226 
   227     \item Finally, out of the intermediate language the final
   228       code in the desired \qn{target language} is \qn{serialized}.
   229 
   230   \end{itemize}
   231 
   232   From these steps, only the two last are carried out
   233   outside the logic; by keeping this layer as
   234   thin as possible, the amount of code to trust is
   235   kept to a minimum.%
   236 \end{isamarkuptext}%
   237 \isamarkuptrue%
   238 %
   239 \isamarkupsection{Basics \label{sec:basics}%
   240 }
   241 \isamarkuptrue%
   242 %
   243 \isamarkupsubsection{Invoking the code generator%
   244 }
   245 \isamarkuptrue%
   246 %
   247 \begin{isamarkuptext}%
   248 Thanks to a reasonable setup of the \isa{HOL} theories, in
   249   most cases code generation proceeds without further ado:%
   250 \end{isamarkuptext}%
   251 \isamarkuptrue%
   252 \isacommand{primrec}\isamarkupfalse%
   253 \isanewline
   254 \ \ fac\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   255 \ \ \ \ {\isachardoublequoteopen}fac\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
   256 \ \ {\isacharbar}\ {\isachardoublequoteopen}fac\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharasterisk}\ fac\ n{\isachardoublequoteclose}%
   257 \begin{isamarkuptext}%
   258 \noindent This executable specification is now turned to SML code:%
   259 \end{isamarkuptext}%
   260 \isamarkuptrue%
   261 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
   262 \ fac\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}%
   263 \begin{isamarkuptext}%
   264 \noindent  The \isa{{\isasymEXPORTCODE}} command takes a space-separated list of
   265   constants together with \qn{serialization directives}
   266   These start with a \qn{target language}
   267   identifier, followed by a file specification
   268   where to write the generated code to.
   269 
   270   Internally, the defining equations for all selected
   271   constants are taken, including any transitively required
   272   constants, datatypes and classes, resulting in the following
   273   code:
   274 
   275   \lstsml{Thy/examples/fac.ML}
   276 
   277   The code generator will complain when a required
   278   ingredient does not provide a executable counterpart,
   279   e.g.~generating code
   280   for constants not yielding
   281   a defining equation (e.g.~the Hilbert choice
   282   operation \isa{SOME}):%
   283 \end{isamarkuptext}%
   284 \isamarkuptrue%
   285 %
   286 \isadelimML
   287 %
   288 \endisadelimML
   289 %
   290 \isatagML
   291 %
   292 \endisatagML
   293 {\isafoldML}%
   294 %
   295 \isadelimML
   296 %
   297 \endisadelimML
   298 \isacommand{definition}\isamarkupfalse%
   299 \isanewline
   300 \ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   301 \ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}%
   302 \isadelimML
   303 %
   304 \endisadelimML
   305 %
   306 \isatagML
   307 %
   308 \endisatagML
   309 {\isafoldML}%
   310 %
   311 \isadelimML
   312 %
   313 \endisadelimML
   314 \isanewline
   315 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
   316 \ pick{\isacharunderscore}some\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}%
   317 \begin{isamarkuptext}%
   318 \noindent will fail.%
   319 \end{isamarkuptext}%
   320 \isamarkuptrue%
   321 %
   322 \isamarkupsubsection{Theorem selection%
   323 }
   324 \isamarkuptrue%
   325 %
   326 \begin{isamarkuptext}%
   327 The list of all defining equations in a theory may be inspected
   328   using the \isa{{\isasymPRINTCODESETUP}} command:%
   329 \end{isamarkuptext}%
   330 \isamarkuptrue%
   331 \isacommand{print{\isacharunderscore}codesetup}\isamarkupfalse%
   332 %
   333 \begin{isamarkuptext}%
   334 \noindent which displays a table of constant with corresponding
   335   defining equations (the additional stuff displayed
   336   shall not bother us for the moment).
   337 
   338   The typical \isa{HOL} tools are already set up in a way that
   339   function definitions introduced by \isa{{\isasymDEFINITION}},
   340   \isa{{\isasymPRIMREC}}, \isa{{\isasymFUN}},
   341   \isa{{\isasymFUNCTION}}, \isa{{\isasymCONSTDEFS}},
   342   \isa{{\isasymRECDEF}} are implicitly propagated
   343   to this defining equation table. Specific theorems may be
   344   selected using an attribute: \emph{code func}. As example,
   345   a weight selector function:%
   346 \end{isamarkuptext}%
   347 \isamarkuptrue%
   348 \isacommand{primrec}\isamarkupfalse%
   349 \isanewline
   350 \ \ pick\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   351 \ \ {\isachardoublequoteopen}pick\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}let\ {\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharequal}\ x\ in\isanewline
   352 \ \ \ \ if\ n\ {\isacharless}\ k\ then\ v\ else\ pick\ xs\ {\isacharparenleft}n\ {\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
   353 \begin{isamarkuptext}%
   354 \noindent We want to eliminate the explicit destruction
   355   of \isa{x} to \isa{{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}}:%
   356 \end{isamarkuptext}%
   357 \isamarkuptrue%
   358 \isacommand{lemma}\isamarkupfalse%
   359 \ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   360 \ \ {\isachardoublequoteopen}pick\ {\isacharparenleft}{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}{\isacharhash}xs{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}if\ n\ {\isacharless}\ k\ then\ v\ else\ pick\ xs\ {\isacharparenleft}n\ {\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   361 %
   362 \isadelimproof
   363 \ \ %
   364 \endisadelimproof
   365 %
   366 \isatagproof
   367 \isacommand{by}\isamarkupfalse%
   368 \ simp%
   369 \endisatagproof
   370 {\isafoldproof}%
   371 %
   372 \isadelimproof
   373 \isanewline
   374 %
   375 \endisadelimproof
   376 \isanewline
   377 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
   378 \ pick\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}%
   379 \begin{isamarkuptext}%
   380 \noindent This theorem now is used for generating code:
   381 
   382   \lstsml{Thy/examples/pick1.ML}
   383 
   384   \noindent It might be convenient to remove the pointless original
   385   equation, using the \emph{func del} attribute:%
   386 \end{isamarkuptext}%
   387 \isamarkuptrue%
   388 \isacommand{lemmas}\isamarkupfalse%
   389 \ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\ {\isacharequal}\ pick{\isachardot}simps\ \isanewline
   390 \isanewline
   391 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
   392 \ pick\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}%
   393 \begin{isamarkuptext}%
   394 \lstsml{Thy/examples/pick2.ML}
   395 
   396   \noindent Syntactic redundancies are implicitly dropped. For example,
   397   using a modified version of the \isa{fac} function
   398   as defining equation, the then redundant (since
   399   syntactically subsumed) original defining equations
   400   are dropped, resulting in a warning:%
   401 \end{isamarkuptext}%
   402 \isamarkuptrue%
   403 \isacommand{lemma}\isamarkupfalse%
   404 \ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   405 \ \ {\isachardoublequoteopen}fac\ n\ {\isacharequal}\ {\isacharparenleft}case\ n\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ n\ {\isacharasterisk}\ fac\ m{\isacharparenright}{\isachardoublequoteclose}\isanewline
   406 %
   407 \isadelimproof
   408 \ \ %
   409 \endisadelimproof
   410 %
   411 \isatagproof
   412 \isacommand{by}\isamarkupfalse%
   413 \ {\isacharparenleft}cases\ n{\isacharparenright}\ simp{\isacharunderscore}all%
   414 \endisatagproof
   415 {\isafoldproof}%
   416 %
   417 \isadelimproof
   418 \isanewline
   419 %
   420 \endisadelimproof
   421 \isanewline
   422 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
   423 \ fac\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isacharunderscore}case{\isachardot}ML{\isachardoublequoteclose}%
   424 \begin{isamarkuptext}%
   425 \lstsml{Thy/examples/fac_case.ML}
   426 
   427   \begin{warn}
   428     The attributes \emph{code} and \emph{code del}
   429     associated with the existing code generator also apply to
   430     the new one: \emph{code} implies \emph{code func},
   431     and \emph{code del} implies \emph{code func del}.
   432   \end{warn}%
   433 \end{isamarkuptext}%
   434 \isamarkuptrue%
   435 %
   436 \isamarkupsubsection{Type classes%
   437 }
   438 \isamarkuptrue%
   439 %
   440 \begin{isamarkuptext}%
   441 Type classes enter the game via the Isar class package.
   442   For a short introduction how to use it, see \cite{isabelle-classes};
   443   here we just illustrate its impact on code generation.
   444 
   445   In a target language, type classes may be represented
   446   natively (as in the case of Haskell).  For languages
   447   like SML, they are implemented using \emph{dictionaries}.
   448   Our following example specifies a class \qt{null},
   449   assigning to each of its inhabitants a \qt{null} value:%
   450 \end{isamarkuptext}%
   451 \isamarkuptrue%
   452 \isacommand{class}\isamarkupfalse%
   453 \ null\ {\isacharequal}\ type\ {\isacharplus}\isanewline
   454 \ \ \isakeyword{fixes}\ null\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
   455 \isanewline
   456 \isacommand{primrec}\isamarkupfalse%
   457 \isanewline
   458 \ \ head\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}null\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   459 \ \ {\isachardoublequoteopen}head\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ null{\isachardoublequoteclose}\isanewline
   460 \ \ {\isacharbar}\ {\isachardoublequoteopen}head\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}%
   461 \begin{isamarkuptext}%
   462 \noindent  We provide some instances for our \isa{null}:%
   463 \end{isamarkuptext}%
   464 \isamarkuptrue%
   465 \isacommand{instantiation}\isamarkupfalse%
   466 \ option\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline
   467 \isakeyword{begin}\isanewline
   468 \isanewline
   469 \isacommand{definition}\isamarkupfalse%
   470 \isanewline
   471 \ \ {\isachardoublequoteopen}null\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
   472 \isanewline
   473 \isacommand{definition}\isamarkupfalse%
   474 \isanewline
   475 \ \ {\isachardoublequoteopen}null\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
   476 \isanewline
   477 \isacommand{instance}\isamarkupfalse%
   478 %
   479 \isadelimproof
   480 \ %
   481 \endisadelimproof
   482 %
   483 \isatagproof
   484 \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   485 %
   486 \endisatagproof
   487 {\isafoldproof}%
   488 %
   489 \isadelimproof
   490 %
   491 \endisadelimproof
   492 \isanewline
   493 \isanewline
   494 \isacommand{end}\isamarkupfalse%
   495 %
   496 \begin{isamarkuptext}%
   497 \noindent Constructing a dummy example:%
   498 \end{isamarkuptext}%
   499 \isamarkuptrue%
   500 \isacommand{definition}\isamarkupfalse%
   501 \isanewline
   502 \ \ {\isachardoublequoteopen}dummy\ {\isacharequal}\ head\ {\isacharbrackleft}Some\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ None{\isacharbrackright}{\isachardoublequoteclose}%
   503 \begin{isamarkuptext}%
   504 Type classes offer a suitable occasion to introduce
   505   the Haskell serializer.  Its usage is almost the same
   506   as SML, but, in accordance with conventions
   507   some Haskell systems enforce, each module ends
   508   up in a single file. The module hierarchy is reflected in
   509   the file system, with root directory given as file specification.%
   510 \end{isamarkuptext}%
   511 \isamarkuptrue%
   512 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
   513 \ dummy\ \isakeyword{in}\ Haskell\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}%
   514 \begin{isamarkuptext}%
   515 \lsthaskell{Thy/examples/Codegen.hs}
   516   \noindent (we have left out all other modules).
   517 
   518   \medskip
   519 
   520   The whole code in SML with explicit dictionary passing:%
   521 \end{isamarkuptext}%
   522 \isamarkuptrue%
   523 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
   524 \ dummy\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}%
   525 \begin{isamarkuptext}%
   526 \lstsml{Thy/examples/class.ML}
   527 
   528   \medskip
   529 
   530   \noindent or in OCaml:%
   531 \end{isamarkuptext}%
   532 \isamarkuptrue%
   533 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
   534 \ dummy\ \isakeyword{in}\ OCaml\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}%
   535 \begin{isamarkuptext}%
   536 \lstsml{Thy/examples/class.ocaml}
   537 
   538   \medskip The explicit association of constants
   539   to classes can be inspected using the \isa{{\isasymPRINTCLASSES}}
   540   command.%
   541 \end{isamarkuptext}%
   542 \isamarkuptrue%
   543 %
   544 \isamarkupsection{Recipes and advanced topics \label{sec:advanced}%
   545 }
   546 \isamarkuptrue%
   547 %
   548 \begin{isamarkuptext}%
   549 In this tutorial, we do not attempt to give an exhaustive
   550   description of the code generator framework; instead,
   551   we cast a light on advanced topics by introducing
   552   them together with practically motivated examples.  Concerning
   553   further reading, see
   554 
   555   \begin{itemize}
   556 
   557   \item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}
   558     for exhaustive syntax diagrams.
   559   \item or \cite{Haftmann-Nipkow:2007:codegen} which deals with foundational issues
   560     of the code generator framework.
   561 
   562   \end{itemize}%
   563 \end{isamarkuptext}%
   564 \isamarkuptrue%
   565 %
   566 \isamarkupsubsection{Library theories \label{sec:library}%
   567 }
   568 \isamarkuptrue%
   569 %
   570 \begin{isamarkuptext}%
   571 The \isa{HOL} \isa{Main} theory already provides a code
   572   generator setup
   573   which should be suitable for most applications. Common extensions
   574   and modifications are available by certain theories of the \isa{HOL}
   575   library; beside being useful in applications, they may serve
   576   as a tutorial for customizing the code generator setup.
   577 
   578   \begin{description}
   579 
   580     \item[\isa{Code{\isacharunderscore}Integer}] represents \isa{HOL} integers by big
   581        integer literals in target languages.
   582     \item[\isa{Code{\isacharunderscore}Char}] represents \isa{HOL} characters by 
   583        character literals in target languages.
   584     \item[\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Code{\isacharunderscore}Char},
   585        but also offers treatment of character codes; includes
   586        \isa{Code{\isacharunderscore}Integer}.
   587     \item[\isa{Efficient{\isacharunderscore}Nat}] \label{eff_nat} implements natural numbers by integers,
   588        which in general will result in higher efficency; pattern
   589        matching with \isa{{\isadigit{0}}} / \isa{Suc}
   590        is eliminated;  includes \isa{Code{\isacharunderscore}Integer}.
   591     \item[\isa{Code{\isacharunderscore}Index}] provides an additional datatype
   592        \isa{index} which is mapped to target-language built-in integers.
   593        Useful for code setups which involve e.g. indexing of
   594        target-language arrays.
   595     \item[\isa{Code{\isacharunderscore}Message}] provides an additional datatype
   596        \isa{message{\isacharunderscore}string} which is isomorphic to strings;
   597        \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
   598        Useful for code setups which involve e.g. printing (error) messages.
   599 
   600   \end{description}
   601 
   602   \begin{warn}
   603     When importing any of these theories, they should form the last
   604     items in an import list.  Since these theories adapt the
   605     code generator setup in a non-conservative fashion,
   606     strange effects may occur otherwise.
   607   \end{warn}%
   608 \end{isamarkuptext}%
   609 \isamarkuptrue%
   610 %
   611 \isamarkupsubsection{Preprocessing%
   612 }
   613 \isamarkuptrue%
   614 %
   615 \begin{isamarkuptext}%
   616 Before selected function theorems are turned into abstract
   617   code, a chain of definitional transformation steps is carried
   618   out: \emph{preprocessing}.  In essence, the preprocessor
   619   consists of two components: a \emph{simpset} and \emph{function transformers}.
   620 
   621   The \emph{simpset} allows to employ the full generality of the Isabelle
   622   simplifier.  Due to the interpretation of theorems
   623   of defining equations, rewrites are applied to the right
   624   hand side and the arguments of the left hand side of an
   625   equation, but never to the constant heading the left hand side.
   626   An important special case are \emph{inline theorems} which may be
   627   declared an undeclared using the
   628   \emph{code inline} or \emph{code inline del} attribute respectively.
   629   Some common applications:%
   630 \end{isamarkuptext}%
   631 \isamarkuptrue%
   632 %
   633 \begin{itemize}
   634 %
   635 \begin{isamarkuptext}%
   636 \item replacing non-executable constructs by executable ones:%
   637 \end{isamarkuptext}%
   638 \isamarkuptrue%
   639 \ \ \isacommand{lemma}\isamarkupfalse%
   640 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
   641 \ \ \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}%
   642 \isadelimproof
   643 \ %
   644 \endisadelimproof
   645 %
   646 \isatagproof
   647 \isacommand{by}\isamarkupfalse%
   648 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
   649 \endisatagproof
   650 {\isafoldproof}%
   651 %
   652 \isadelimproof
   653 %
   654 \endisadelimproof
   655 %
   656 \begin{isamarkuptext}%
   657 \item eliminating superfluous constants:%
   658 \end{isamarkuptext}%
   659 \isamarkuptrue%
   660 \ \ \isacommand{lemma}\isamarkupfalse%
   661 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
   662 \ \ \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}%
   663 \isadelimproof
   664 \ %
   665 \endisadelimproof
   666 %
   667 \isatagproof
   668 \isacommand{by}\isamarkupfalse%
   669 \ simp%
   670 \endisatagproof
   671 {\isafoldproof}%
   672 %
   673 \isadelimproof
   674 %
   675 \endisadelimproof
   676 %
   677 \begin{isamarkuptext}%
   678 \item replacing executable but inconvenient constructs:%
   679 \end{isamarkuptext}%
   680 \isamarkuptrue%
   681 \ \ \isacommand{lemma}\isamarkupfalse%
   682 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
   683 \ \ \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}%
   684 \isadelimproof
   685 \ %
   686 \endisadelimproof
   687 %
   688 \isatagproof
   689 \isacommand{by}\isamarkupfalse%
   690 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
   691 \endisatagproof
   692 {\isafoldproof}%
   693 %
   694 \isadelimproof
   695 %
   696 \endisadelimproof
   697 %
   698 \end{itemize}
   699 %
   700 \begin{isamarkuptext}%
   701 \emph{Function transformers} provide a very general interface,
   702   transforming a list of function theorems to another
   703   list of function theorems, provided that neither the heading
   704   constant nor its type change.  The \isa{{\isadigit{0}}} / \isa{Suc}
   705   pattern elimination implemented in
   706   theory \isa{Efficient{\isacharunderscore}Nat} (\secref{eff_nat}) uses this
   707   interface.
   708 
   709   \noindent The current setup of the preprocessor may be inspected using
   710   the \isa{{\isasymPRINTCODESETUP}} command.
   711 
   712   \begin{warn}
   713     The attribute \emph{code unfold}
   714     associated with the existing code generator also applies to
   715     the new one: \emph{code unfold} implies \emph{code inline}.
   716   \end{warn}%
   717 \end{isamarkuptext}%
   718 \isamarkuptrue%
   719 %
   720 \isamarkupsubsection{Concerning operational equality%
   721 }
   722 \isamarkuptrue%
   723 %
   724 \begin{isamarkuptext}%
   725 Surely you have already noticed how equality is treated
   726   by the code generator:%
   727 \end{isamarkuptext}%
   728 \isamarkuptrue%
   729 \isacommand{primrec}\isamarkupfalse%
   730 \isanewline
   731 \ \ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   732 \ \ \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
   733 \ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
   734 \ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
   735 \ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
   736 \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
   737 \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
   738 \begin{isamarkuptext}%
   739 The membership test during preprocessing is rewritten,
   740   resulting in \isa{op\ mem}, which itself
   741   performs an explicit equality check.%
   742 \end{isamarkuptext}%
   743 \isamarkuptrue%
   744 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
   745 \ collect{\isacharunderscore}duplicates\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}%
   746 \begin{isamarkuptext}%
   747 \lstsml{Thy/examples/collect_duplicates.ML}%
   748 \end{isamarkuptext}%
   749 \isamarkuptrue%
   750 %
   751 \begin{isamarkuptext}%
   752 Obviously, polymorphic equality is implemented the Haskell
   753   way using a type class.  How is this achieved?  HOL introduces
   754   an explicit class \isa{eq} with a corresponding operation
   755   \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ x\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}.
   756   The preprocessing framework does the rest.
   757   For datatypes, instances of \isa{eq} are implicitly derived
   758   when possible.  For other types, you may instantiate \isa{eq}
   759   manually like any other type class.
   760 
   761   Though this \isa{eq} class is designed to get rarely in
   762   the way, a subtlety
   763   enters the stage when definitions of overloaded constants
   764   are dependent on operational equality.  For example, let
   765   us define a lexicographic ordering on tuples:%
   766 \end{isamarkuptext}%
   767 \isamarkuptrue%
   768 \isacommand{instantiation}\isamarkupfalse%
   769 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
   770 \isakeyword{begin}\isanewline
   771 \isanewline
   772 \isacommand{definition}\isamarkupfalse%
   773 \isanewline
   774 \ \ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymlongleftrightarrow}\ {\isacharparenleft}let\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
   775 \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   776 \isanewline
   777 \isacommand{definition}\isamarkupfalse%
   778 \isanewline
   779 \ \ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymlongleftrightarrow}\ {\isacharparenleft}let\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
   780 \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   781 \isanewline
   782 \isacommand{instance}\isamarkupfalse%
   783 %
   784 \isadelimproof
   785 \ %
   786 \endisadelimproof
   787 %
   788 \isatagproof
   789 \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   790 %
   791 \endisatagproof
   792 {\isafoldproof}%
   793 %
   794 \isadelimproof
   795 %
   796 \endisadelimproof
   797 \isanewline
   798 \isanewline
   799 \isacommand{end}\isamarkupfalse%
   800 \isanewline
   801 \isanewline
   802 \isacommand{lemma}\isamarkupfalse%
   803 \ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   804 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   805 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   806 %
   807 \isadelimproof
   808 \ \ %
   809 \endisadelimproof
   810 %
   811 \isatagproof
   812 \isacommand{unfolding}\isamarkupfalse%
   813 \ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   814 \ simp{\isacharunderscore}all%
   815 \endisatagproof
   816 {\isafoldproof}%
   817 %
   818 \isadelimproof
   819 %
   820 \endisadelimproof
   821 %
   822 \begin{isamarkuptext}%
   823 Then code generation will fail.  Why?  The definition
   824   of \isa{op\ {\isasymle}} depends on equality on both arguments,
   825   which are polymorphic and impose an additional \isa{eq}
   826   class constraint, thus violating the type discipline
   827   for class operations.
   828 
   829   The solution is to add \isa{eq} explicitly to the first sort arguments in the
   830   code theorems:%
   831 \end{isamarkuptext}%
   832 \isamarkuptrue%
   833 \isacommand{lemma}\isamarkupfalse%
   834 \ ord{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   835 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
   836 \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   837 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
   838 \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   839 %
   840 \isadelimproof
   841 \ \ %
   842 \endisadelimproof
   843 %
   844 \isatagproof
   845 \isacommand{unfolding}\isamarkupfalse%
   846 \ ord{\isacharunderscore}prod\ \isacommand{by}\isamarkupfalse%
   847 \ rule{\isacharplus}%
   848 \endisatagproof
   849 {\isafoldproof}%
   850 %
   851 \isadelimproof
   852 %
   853 \endisadelimproof
   854 %
   855 \begin{isamarkuptext}%
   856 \noindent Then code generation succeeds:%
   857 \end{isamarkuptext}%
   858 \isamarkuptrue%
   859 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
   860 \ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   861 \ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}%
   862 \begin{isamarkuptext}%
   863 \lstsml{Thy/examples/lexicographic.ML}%
   864 \end{isamarkuptext}%
   865 \isamarkuptrue%
   866 %
   867 \begin{isamarkuptext}%
   868 In general, code theorems for overloaded constants may have more
   869   restrictive sort constraints than the underlying instance relation
   870   between class and type constructor as long as the whole system of
   871   constraints is coregular; code theorems violating coregularity
   872   are rejected immediately.  Consequently, it might be necessary
   873   to delete disturbing theorems in the code theorem table,
   874   as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def}
   875   and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.
   876 
   877   In some cases, the automatically derived defining equations
   878   for equality on a particular type may not be appropriate.
   879   As example, watch the following datatype representing
   880   monomorphic parametric types (where type constructors
   881   are referred to by natural numbers):%
   882 \end{isamarkuptext}%
   883 \isamarkuptrue%
   884 \isacommand{datatype}\isamarkupfalse%
   885 \ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
   886 \isadelimproof
   887 %
   888 \endisadelimproof
   889 %
   890 \isatagproof
   891 %
   892 \endisatagproof
   893 {\isafoldproof}%
   894 %
   895 \isadelimproof
   896 %
   897 \endisadelimproof
   898 %
   899 \begin{isamarkuptext}%
   900 Then code generation for SML would fail with a message
   901   that the generated code conains illegal mutual dependencies:
   902   the theorem \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}} already requires the
   903   instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
   904   \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}};  Haskell has no problem with mutually
   905   recursive \isa{instance} and \isa{function} definitions,
   906   but the SML serializer does not support this.
   907 
   908   In such cases, you have to provide you own equality equations
   909   involving auxiliary constants.  In our case,
   910   \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:%
   911 \end{isamarkuptext}%
   912 \isamarkuptrue%
   913 \isacommand{lemma}\isamarkupfalse%
   914 \ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   915 \ \ {\isachardoublequoteopen}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymlongleftrightarrow}\isanewline
   916 \ \ \ \ \ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ {\isacharparenleft}op\ {\isacharequal}{\isacharparenright}\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
   917 %
   918 \isadelimproof
   919 \ \ %
   920 \endisadelimproof
   921 %
   922 \isatagproof
   923 \isacommand{by}\isamarkupfalse%
   924 \ {\isacharparenleft}simp\ add{\isacharcolon}\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
   925 \endisatagproof
   926 {\isafoldproof}%
   927 %
   928 \isadelimproof
   929 %
   930 \endisadelimproof
   931 %
   932 \begin{isamarkuptext}%
   933 does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%
   934 \end{isamarkuptext}%
   935 \isamarkuptrue%
   936 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
   937 \ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isacharcolon}{\isacharcolon}\ monotype\ {\isasymRightarrow}\ monotype\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   938 \ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}monotype{\isachardot}ML{\isachardoublequoteclose}%
   939 \begin{isamarkuptext}%
   940 \lstsml{Thy/examples/monotype.ML}%
   941 \end{isamarkuptext}%
   942 \isamarkuptrue%
   943 %
   944 \isamarkupsubsection{Programs as sets of theorems%
   945 }
   946 \isamarkuptrue%
   947 %
   948 \begin{isamarkuptext}%
   949 As told in \secref{sec:concept}, code generation is based
   950   on a structured collection of code theorems.
   951   For explorative purpose, this collection
   952   may be inspected using the \isa{{\isasymCODETHMS}} command:%
   953 \end{isamarkuptext}%
   954 \isamarkuptrue%
   955 \isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
   956 \ {\isachardoublequoteopen}op\ mod\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}%
   957 \begin{isamarkuptext}%
   958 \noindent prints a table with \emph{all} defining equations
   959   for \isa{op\ mod}, including
   960   \emph{all} defining equations those equations depend
   961   on recursivly.  \isa{{\isasymCODETHMS}} provides a convenient
   962   mechanism to inspect the impact of a preprocessor setup
   963   on defining equations.
   964   
   965   Similarly, the \isa{{\isasymCODEDEPS}} command shows a graph
   966   visualizing dependencies between defining equations.%
   967 \end{isamarkuptext}%
   968 \isamarkuptrue%
   969 %
   970 \isamarkupsubsection{Constructor sets for datatypes%
   971 }
   972 \isamarkuptrue%
   973 %
   974 \begin{isamarkuptext}%
   975 Conceptually, any datatype is spanned by a set of
   976   \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n}
   977   where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is excactly the set of \emph{all}
   978   type variables in \isa{{\isasymtau}}.  The HOL datatype package
   979   by default registers any new datatype in the table
   980   of datatypes, which may be inspected using
   981   the \isa{{\isasymPRINTCODESETUP}} command.
   982 
   983   In some cases, it may be convenient to alter or
   984   extend this table;  as an example, we will develope an alternative
   985   representation of natural numbers as binary digits, whose
   986   size does increase logarithmically with its value, not linear
   987   \footnote{Indeed, the \isa{Efficient{\isacharunderscore}Nat} theory \ref{eff_nat}
   988     does something similar}.  First, the digit representation:%
   989 \end{isamarkuptext}%
   990 \isamarkuptrue%
   991 \isacommand{definition}\isamarkupfalse%
   992 \ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   993 \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline
   994 \isanewline
   995 \isacommand{definition}\isamarkupfalse%
   996 \ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   997 \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}%
   998 \begin{isamarkuptext}%
   999 \noindent We will use these two ">digits"< to represent natural numbers
  1000   in binary digits, e.g.:%
  1001 \end{isamarkuptext}%
  1002 \isamarkuptrue%
  1003 \isacommand{lemma}\isamarkupfalse%
  1004 \ {\isadigit{4}}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
  1005 %
  1006 \isadelimproof
  1007 \ \ %
  1008 \endisadelimproof
  1009 %
  1010 \isatagproof
  1011 \isacommand{by}\isamarkupfalse%
  1012 \ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
  1013 \endisatagproof
  1014 {\isafoldproof}%
  1015 %
  1016 \isadelimproof
  1017 %
  1018 \endisadelimproof
  1019 %
  1020 \begin{isamarkuptext}%
  1021 \noindent Of course we also have to provide proper code equations for
  1022   the operations, e.g. \isa{op\ {\isacharplus}}:%
  1023 \end{isamarkuptext}%
  1024 \isamarkuptrue%
  1025 \isacommand{lemma}\isamarkupfalse%
  1026 \ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
  1027 \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
  1028 \ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
  1029 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
  1030 \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{1}}\ m{\isachardoublequoteclose}\isanewline
  1031 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
  1032 \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
  1033 \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
  1034 \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
  1035 \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
  1036 \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
  1037 %
  1038 \isadelimproof
  1039 \ \ %
  1040 \endisadelimproof
  1041 %
  1042 \isatagproof
  1043 \isacommand{by}\isamarkupfalse%
  1044 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
  1045 \endisatagproof
  1046 {\isafoldproof}%
  1047 %
  1048 \isadelimproof
  1049 %
  1050 \endisadelimproof
  1051 %
  1052 \begin{isamarkuptext}%
  1053 \noindent We then instruct the code generator to view \isa{{\isadigit{0}}},
  1054   \isa{{\isadigit{1}}}, \isa{Dig{\isadigit{0}}} and \isa{Dig{\isadigit{1}}} as
  1055   datatype constructors:%
  1056 \end{isamarkuptext}%
  1057 \isamarkuptrue%
  1058 \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
  1059 \ {\isachardoublequoteopen}{\isadigit{0}}{\isasymColon}nat{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isasymColon}nat{\isachardoublequoteclose}\ Dig{\isadigit{0}}\ Dig{\isadigit{1}}%
  1060 \begin{isamarkuptext}%
  1061 \noindent For the former constructor \isa{Suc}, we provide a code
  1062   equation and remove some parts of the default code generator setup
  1063   which are an obstacle here:%
  1064 \end{isamarkuptext}%
  1065 \isamarkuptrue%
  1066 \isacommand{lemma}\isamarkupfalse%
  1067 \ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
  1068 \ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
  1069 %
  1070 \isadelimproof
  1071 \ \ %
  1072 \endisadelimproof
  1073 %
  1074 \isatagproof
  1075 \isacommand{by}\isamarkupfalse%
  1076 \ simp%
  1077 \endisatagproof
  1078 {\isafoldproof}%
  1079 %
  1080 \isadelimproof
  1081 \isanewline
  1082 %
  1083 \endisadelimproof
  1084 \isanewline
  1085 \isacommand{declare}\isamarkupfalse%
  1086 \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
  1087 \isacommand{declare}\isamarkupfalse%
  1088 \ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}%
  1089 \begin{isamarkuptext}%
  1090 \noindent This yields the following code:%
  1091 \end{isamarkuptext}%
  1092 \isamarkuptrue%
  1093 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
  1094 \ {\isachardoublequoteopen}op\ {\isacharplus}\ {\isasymColon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}nat{\isacharunderscore}binary{\isachardot}ML{\isachardoublequoteclose}%
  1095 \begin{isamarkuptext}%
  1096 \lstsml{Thy/examples/nat_binary.ML}%
  1097 \end{isamarkuptext}%
  1098 \isamarkuptrue%
  1099 %
  1100 \begin{isamarkuptext}%
  1101 \medskip
  1102 
  1103   From this example, it can be easily glimpsed that using own constructor sets
  1104   is a little delicate since it changes the set of valid patterns for values
  1105   of that type.  Without going into much detail, here some practical hints:
  1106 
  1107   \begin{itemize}
  1108     \item When changing the constuctor set for datatypes, take care to
  1109       provide an alternative for the \isa{case} combinator (e.g. by replacing
  1110       it using the preprocessor).
  1111     \item Values in the target language need not to be normalized -- different
  1112       values in the target language may represent the same value in the
  1113       logic (e.g. \isa{Dig{\isadigit{1}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}}).
  1114     \item Usually, a good methodology to deal with the subleties of pattern
  1115       matching is to see the type as an abstract type: provide a set
  1116       of operations which operate on the concrete representation of the type,
  1117       and derive further operations by combinations of these primitive ones,
  1118       without relying on a particular representation.
  1119   \end{itemize}%
  1120 \end{isamarkuptext}%
  1121 \isamarkuptrue%
  1122 %
  1123 \isadeliminvisible
  1124 %
  1125 \endisadeliminvisible
  1126 %
  1127 \isataginvisible
  1128 \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
  1129 \ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
  1130 \isacommand{declare}\isamarkupfalse%
  1131 \ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline
  1132 \isacommand{declare}\isamarkupfalse%
  1133 \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
  1134 \isacommand{declare}\isamarkupfalse%
  1135 \ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline
  1136 \isacommand{lemma}\isamarkupfalse%
  1137 \ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
  1138 \ simp%
  1139 \endisataginvisible
  1140 {\isafoldinvisible}%
  1141 %
  1142 \isadeliminvisible
  1143 %
  1144 \endisadeliminvisible
  1145 %
  1146 \isamarkupsubsection{Customizing serialization%
  1147 }
  1148 \isamarkuptrue%
  1149 %
  1150 \isamarkupsubsubsection{Basics%
  1151 }
  1152 \isamarkuptrue%
  1153 %
  1154 \begin{isamarkuptext}%
  1155 Consider the following function and its corresponding
  1156   SML code:%
  1157 \end{isamarkuptext}%
  1158 \isamarkuptrue%
  1159 \isacommand{primrec}\isamarkupfalse%
  1160 \isanewline
  1161 \ \ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
  1162 \ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
  1163 \isadelimtt
  1164 %
  1165 \endisadelimtt
  1166 %
  1167 \isatagtt
  1168 %
  1169 \endisatagtt
  1170 {\isafoldtt}%
  1171 %
  1172 \isadelimtt
  1173 %
  1174 \endisadelimtt
  1175 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
  1176 \ in{\isacharunderscore}interval\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}literal{\isachardot}ML{\isachardoublequoteclose}%
  1177 \begin{isamarkuptext}%
  1178 \lstsml{Thy/examples/bool_literal.ML}
  1179 
  1180   \noindent Though this is correct code, it is a little bit unsatisfactory:
  1181   boolean values and operators are materialized as distinguished
  1182   entities with have nothing to do with the SML-builtin notion
  1183   of \qt{bool}.  This results in less readable code;
  1184   additionally, eager evaluation may cause programs to
  1185   loop or break which would perfectly terminate when
  1186   the existing SML \qt{bool} would be used.  To map
  1187   the HOL \qt{bool} on SML \qt{bool}, we may use
  1188   \qn{custom serializations}:%
  1189 \end{isamarkuptext}%
  1190 \isamarkuptrue%
  1191 %
  1192 \isadelimtt
  1193 %
  1194 \endisadelimtt
  1195 %
  1196 \isatagtt
  1197 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
  1198 \ bool\isanewline
  1199 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
  1200 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
  1201 \ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
  1202 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
  1203 \endisatagtt
  1204 {\isafoldtt}%
  1205 %
  1206 \isadelimtt
  1207 %
  1208 \endisadelimtt
  1209 %
  1210 \begin{isamarkuptext}%
  1211 The \isa{{\isasymCODETYPE}} commad takes a type constructor
  1212   as arguments together with a list of custom serializations.
  1213   Each custom serialization starts with a target language
  1214   identifier followed by an expression, which during
  1215   code serialization is inserted whenever the type constructor
  1216   would occur.  For constants, \isa{{\isasymCODECONST}} implements
  1217   the corresponding mechanism.  Each ``\verb|_|'' in
  1218   a serialization expression is treated as a placeholder
  1219   for the type constructor's (the constant's) arguments.%
  1220 \end{isamarkuptext}%
  1221 \isamarkuptrue%
  1222 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
  1223 \ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}%
  1224 \begin{isamarkuptext}%
  1225 \lstsml{Thy/examples/bool_mlbool.ML}
  1226 
  1227   \noindent This still is not perfect: the parentheses
  1228   around the \qt{andalso} expression are superfluous.
  1229   Though the serializer
  1230   by no means attempts to imitate the rich Isabelle syntax
  1231   framework, it provides some common idioms, notably
  1232   associative infixes with precedences which may be used here:%
  1233 \end{isamarkuptext}%
  1234 \isamarkuptrue%
  1235 %
  1236 \isadelimtt
  1237 %
  1238 \endisadelimtt
  1239 %
  1240 \isatagtt
  1241 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
  1242 \ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
  1243 \ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
  1244 \endisatagtt
  1245 {\isafoldtt}%
  1246 %
  1247 \isadelimtt
  1248 %
  1249 \endisadelimtt
  1250 \isanewline
  1251 \isanewline
  1252 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
  1253 \ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}infix{\isachardot}ML{\isachardoublequoteclose}%
  1254 \begin{isamarkuptext}%
  1255 \lstsml{Thy/examples/bool_infix.ML}
  1256 
  1257   \medskip
  1258 
  1259   Next, we try to map HOL pairs to SML pairs, using the
  1260   infix ``\verb|*|'' type constructor and parentheses:%
  1261 \end{isamarkuptext}%
  1262 \isamarkuptrue%
  1263 %
  1264 \isadelimtt
  1265 %
  1266 \endisadelimtt
  1267 %
  1268 \isatagtt
  1269 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
  1270 \ {\isacharasterisk}\isanewline
  1271 \ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
  1272 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
  1273 \ Pair\isanewline
  1274 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
  1275 \endisatagtt
  1276 {\isafoldtt}%
  1277 %
  1278 \isadelimtt
  1279 %
  1280 \endisadelimtt
  1281 %
  1282 \begin{isamarkuptext}%
  1283 The initial bang ``\verb|!|'' tells the serializer to never put
  1284   parentheses around the whole expression (they are already present),
  1285   while the parentheses around argument place holders
  1286   tell not to put parentheses around the arguments.
  1287   The slash ``\verb|/|'' (followed by arbitrary white space)
  1288   inserts a space which may be used as a break if necessary
  1289   during pretty printing.
  1290 
  1291   These examples give a glimpse what mechanisms
  1292   custom serializations provide; however their usage
  1293   requires careful thinking in order not to introduce
  1294   inconsistencies -- or, in other words:
  1295   custom serializations are completely axiomatic.
  1296 
  1297   A further noteworthy details is that any special
  1298   character in a custom serialization may be quoted
  1299   using ``\verb|'|''; thus, in
  1300   ``\verb|fn '_ => _|'' the first
  1301   ``\verb|_|'' is a proper underscore while the
  1302   second ``\verb|_|'' is a placeholder.
  1303 
  1304   The HOL theories provide further
  1305   examples for custom serializations.%
  1306 \end{isamarkuptext}%
  1307 \isamarkuptrue%
  1308 %
  1309 \isamarkupsubsubsection{Haskell serialization%
  1310 }
  1311 \isamarkuptrue%
  1312 %
  1313 \begin{isamarkuptext}%
  1314 For convenience, the default
  1315   HOL setup for Haskell maps the \isa{eq} class to
  1316   its counterpart in Haskell, giving custom serializations
  1317   for the class (\isa{{\isasymCODECLASS}}) and its operation:%
  1318 \end{isamarkuptext}%
  1319 \isamarkuptrue%
  1320 %
  1321 \isadelimtt
  1322 %
  1323 \endisadelimtt
  1324 %
  1325 \isatagtt
  1326 \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
  1327 \ eq\isanewline
  1328 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
  1329 \isanewline
  1330 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
  1331 \ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
  1332 \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
  1333 \endisatagtt
  1334 {\isafoldtt}%
  1335 %
  1336 \isadelimtt
  1337 %
  1338 \endisadelimtt
  1339 %
  1340 \begin{isamarkuptext}%
  1341 A problem now occurs whenever a type which
  1342   is an instance of \isa{eq} in HOL is mapped
  1343   on a Haskell-builtin type which is also an instance
  1344   of Haskell \isa{Eq}:%
  1345 \end{isamarkuptext}%
  1346 \isamarkuptrue%
  1347 \isacommand{typedecl}\isamarkupfalse%
  1348 \ bar\isanewline
  1349 \isanewline
  1350 \isacommand{instantiation}\isamarkupfalse%
  1351 \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
  1352 \isakeyword{begin}\isanewline
  1353 \isanewline
  1354 \isacommand{definition}\isamarkupfalse%
  1355 \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
  1356 \isanewline
  1357 \isacommand{instance}\isamarkupfalse%
  1358 %
  1359 \isadelimproof
  1360 \ %
  1361 \endisadelimproof
  1362 %
  1363 \isatagproof
  1364 \isacommand{by}\isamarkupfalse%
  1365 \ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}%
  1366 \endisatagproof
  1367 {\isafoldproof}%
  1368 %
  1369 \isadelimproof
  1370 %
  1371 \endisadelimproof
  1372 \isanewline
  1373 \isanewline
  1374 \isacommand{end}\isamarkupfalse%
  1375 \isanewline
  1376 %
  1377 \isadelimtt
  1378 \isanewline
  1379 %
  1380 \endisadelimtt
  1381 %
  1382 \isatagtt
  1383 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
  1384 \ bar\isanewline
  1385 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
  1386 \endisatagtt
  1387 {\isafoldtt}%
  1388 %
  1389 \isadelimtt
  1390 %
  1391 \endisadelimtt
  1392 %
  1393 \begin{isamarkuptext}%
  1394 The code generator would produce
  1395   an additional instance, which of course is rejected.
  1396   To suppress this additional instance, use
  1397   \isa{{\isasymCODEINSTANCE}}:%
  1398 \end{isamarkuptext}%
  1399 \isamarkuptrue%
  1400 %
  1401 \isadelimtt
  1402 %
  1403 \endisadelimtt
  1404 %
  1405 \isatagtt
  1406 \isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
  1407 \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
  1408 \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
  1409 \endisatagtt
  1410 {\isafoldtt}%
  1411 %
  1412 \isadelimtt
  1413 %
  1414 \endisadelimtt
  1415 %
  1416 \isamarkupsubsubsection{Pretty printing%
  1417 }
  1418 \isamarkuptrue%
  1419 %
  1420 \begin{isamarkuptext}%
  1421 The serializer provides ML interfaces to set up
  1422   pretty serializations for expressions like lists, numerals
  1423   and characters;  these are
  1424   monolithic stubs and should only be used with the
  1425   theories introduces in \secref{sec:library}.%
  1426 \end{isamarkuptext}%
  1427 \isamarkuptrue%
  1428 %
  1429 \isamarkupsubsection{Cyclic module dependencies%
  1430 }
  1431 \isamarkuptrue%
  1432 %
  1433 \begin{isamarkuptext}%
  1434 Sometimes the awkward situation occurs that dependencies
  1435   between definitions introduce cyclic dependencies
  1436   between modules, which in the Haskell world leaves
  1437   you to the mercy of the Haskell implementation you are using,
  1438   while for SML code generation is not possible.
  1439 
  1440   A solution is to declare module names explicitly.
  1441   Let use assume the three cyclically dependent
  1442   modules are named \emph{A}, \emph{B} and \emph{C}.
  1443   Then, by stating%
  1444 \end{isamarkuptext}%
  1445 \isamarkuptrue%
  1446 \isacommand{code{\isacharunderscore}modulename}\isamarkupfalse%
  1447 \ SML\isanewline
  1448 \ \ A\ ABC\isanewline
  1449 \ \ B\ ABC\isanewline
  1450 \ \ C\ ABC%
  1451 \begin{isamarkuptext}%
  1452 we explicitly map all those modules on \emph{ABC},
  1453   resulting in an ad-hoc merge of this three modules
  1454   at serialization time.%
  1455 \end{isamarkuptext}%
  1456 \isamarkuptrue%
  1457 %
  1458 \isamarkupsubsection{Incremental code generation%
  1459 }
  1460 \isamarkuptrue%
  1461 %
  1462 \begin{isamarkuptext}%
  1463 Code generation is \emph{incremental}: theorems
  1464   and abstract intermediate code are cached and extended on demand.
  1465   The cache may be partially or fully dropped if the underlying
  1466   executable content of the theory changes.
  1467   Implementation of caching is supposed to transparently
  1468   hid away the details from the user.  Anyway, caching
  1469   reaches the surface by using a slightly more general form
  1470   of the \isa{{\isasymCODETHMS}}, \isa{{\isasymCODEDEPS}}
  1471   and \isa{{\isasymEXPORTCODE}} commands: the list of constants
  1472   may be omitted.  Then, all constants with code theorems
  1473   in the current cache are referred to.%
  1474 \end{isamarkuptext}%
  1475 \isamarkuptrue%
  1476 %
  1477 \isamarkupsection{ML interfaces \label{sec:ml}%
  1478 }
  1479 \isamarkuptrue%
  1480 %
  1481 \begin{isamarkuptext}%
  1482 Since the code generator framework not only aims to provide
  1483   a nice Isar interface but also to form a base for
  1484   code-generation-based applications, here a short
  1485   description of the most important ML interfaces.%
  1486 \end{isamarkuptext}%
  1487 \isamarkuptrue%
  1488 %
  1489 \isamarkupsubsection{Executable theory content: \isa{Code}%
  1490 }
  1491 \isamarkuptrue%
  1492 %
  1493 \begin{isamarkuptext}%
  1494 This Pure module implements the core notions of
  1495   executable content of a theory.%
  1496 \end{isamarkuptext}%
  1497 \isamarkuptrue%
  1498 %
  1499 \isamarkupsubsubsection{Managing executable content%
  1500 }
  1501 \isamarkuptrue%
  1502 %
  1503 \isadelimmlref
  1504 %
  1505 \endisadelimmlref
  1506 %
  1507 \isatagmlref
  1508 %
  1509 \begin{isamarkuptext}%
  1510 \begin{mldecls}
  1511   \indexml{Code.add\_func}\verb|Code.add_func: thm -> theory -> theory| \\
  1512   \indexml{Code.del\_func}\verb|Code.del_func: thm -> theory -> theory| \\
  1513   \indexml{Code.add\_funcl}\verb|Code.add_funcl: string * thm list Susp.T -> theory -> theory| \\
  1514   \indexml{Code.map\_pre}\verb|Code.map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
  1515   \indexml{Code.map\_post}\verb|Code.map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
  1516   \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> thm list -> thm list option)|\isasep\isanewline%
  1517 \verb|    -> theory -> theory| \\
  1518   \indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
  1519   \indexml{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
  1520   \indexml{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
  1521 \verb|    -> (string * sort) list * (string * typ list) list| \\
  1522   \indexml{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
  1523   \end{mldecls}
  1524 
  1525   \begin{description}
  1526 
  1527   \item \verb|Code.add_func|~\isa{thm}~\isa{thy} adds function
  1528      theorem \isa{thm} to executable content.
  1529 
  1530   \item \verb|Code.del_func|~\isa{thm}~\isa{thy} removes function
  1531      theorem \isa{thm} from executable content, if present.
  1532 
  1533   \item \verb|Code.add_funcl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
  1534      suspended defining equations \isa{lthms} for constant
  1535      \isa{const} to executable content.
  1536 
  1537   \item \verb|Code.map_pre|~\isa{f}~\isa{thy} changes
  1538      the preprocessor simpset.
  1539 
  1540     \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
  1541      function transformer \isa{f} (named \isa{name}) to executable content;
  1542      \isa{f} is a transformer of the defining equations belonging
  1543      to a certain function definition, depending on the
  1544      current theory context.  Returning \isa{NONE} indicates that no
  1545      transformation took place;  otherwise, the whole process will be iterated
  1546      with the new defining equations.
  1547 
  1548   \item \verb|Code.del_functrans|~\isa{name}~\isa{thy} removes
  1549      function transformer named \isa{name} from executable content.
  1550 
  1551   \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
  1552      a datatype to executable content, with generation
  1553      set \isa{cs}.
  1554 
  1555   \item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const}
  1556      returns type constructor corresponding to
  1557      constructor \isa{const}; returns \isa{NONE}
  1558      if \isa{const} is no constructor.
  1559 
  1560   \end{description}%
  1561 \end{isamarkuptext}%
  1562 \isamarkuptrue%
  1563 %
  1564 \endisatagmlref
  1565 {\isafoldmlref}%
  1566 %
  1567 \isadelimmlref
  1568 %
  1569 \endisadelimmlref
  1570 %
  1571 \isamarkupsubsection{Auxiliary%
  1572 }
  1573 \isamarkuptrue%
  1574 %
  1575 \isadelimmlref
  1576 %
  1577 \endisadelimmlref
  1578 %
  1579 \isatagmlref
  1580 %
  1581 \begin{isamarkuptext}%
  1582 \begin{mldecls}
  1583   \indexml{CodeUnit.read\_const}\verb|CodeUnit.read_const: theory -> string -> string| \\
  1584   \indexml{CodeUnit.head\_func}\verb|CodeUnit.head_func: thm -> string * ((string * sort) list * typ)| \\
  1585   \indexml{CodeUnit.rewrite\_func}\verb|CodeUnit.rewrite_func: MetaSimplifier.simpset -> thm -> thm| \\
  1586   \end{mldecls}
  1587 
  1588   \begin{description}
  1589 
  1590   \item \verb|CodeUnit.read_const|~\isa{thy}~\isa{s}
  1591      reads a constant as a concrete term expression \isa{s}.
  1592 
  1593   \item \verb|CodeUnit.head_func|~\isa{thm}
  1594      extracts the constant and its type from a defining equation \isa{thm}.
  1595 
  1596   \item \verb|CodeUnit.rewrite_func|~\isa{ss}~\isa{thm}
  1597      rewrites a defining equation \isa{thm} with a simpset \isa{ss};
  1598      only arguments and right hand side are rewritten,
  1599      not the head of the defining equation.
  1600 
  1601   \end{description}%
  1602 \end{isamarkuptext}%
  1603 \isamarkuptrue%
  1604 %
  1605 \endisatagmlref
  1606 {\isafoldmlref}%
  1607 %
  1608 \isadelimmlref
  1609 %
  1610 \endisadelimmlref
  1611 %
  1612 \isamarkupsubsection{Implementing code generator applications%
  1613 }
  1614 \isamarkuptrue%
  1615 %
  1616 \begin{isamarkuptext}%
  1617 Implementing code generator applications on top
  1618   of the framework set out so far usually not only
  1619   involves using those primitive interfaces
  1620   but also storing code-dependent data and various
  1621   other things.
  1622 
  1623   \begin{warn}
  1624     Some interfaces discussed here have not reached
  1625     a final state yet.
  1626     Changes likely to occur in future.
  1627   \end{warn}%
  1628 \end{isamarkuptext}%
  1629 \isamarkuptrue%
  1630 %
  1631 \isamarkupsubsubsection{Data depending on the theory's executable content%
  1632 }
  1633 \isamarkuptrue%
  1634 %
  1635 \begin{isamarkuptext}%
  1636 Due to incrementality of code generation, changes in the
  1637   theory's executable content have to be propagated in a
  1638   certain fashion.  Additionally, such changes may occur
  1639   not only during theory extension but also during theory
  1640   merge, which is a little bit nasty from an implementation
  1641   point of view.  The framework provides a solution
  1642   to this technical challenge by providing a functorial
  1643   data slot \verb|CodeDataFun|; on instantiation
  1644   of this functor, the following types and operations
  1645   are required:
  1646 
  1647   \medskip
  1648   \begin{tabular}{l}
  1649   \isa{type\ T} \\
  1650   \isa{val\ empty{\isacharcolon}\ T} \\
  1651   \isa{val\ merge{\isacharcolon}\ Pretty{\isachardot}pp\ {\isasymrightarrow}\ T\ {\isacharasterisk}\ T\ {\isasymrightarrow}\ T} \\
  1652   \isa{val\ purge{\isacharcolon}\ theory\ option\ {\isasymrightarrow}\ CodeUnit{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
  1653   \end{tabular}
  1654 
  1655   \begin{description}
  1656 
  1657   \item \isa{T} the type of data to store.
  1658 
  1659   \item \isa{empty} initial (empty) data.
  1660 
  1661   \item \isa{merge} merging two data slots.
  1662 
  1663   \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content;
  1664     if possible, the current theory context is handed over
  1665     as argument \isa{thy} (if there is no current theory context (e.g.~during
  1666     theory merge, \verb|NONE|); \isa{consts} indicates the kind
  1667     of change: \verb|NONE| stands for a fundamental change
  1668     which invalidates any existing code, \isa{SOME\ consts}
  1669     hints that executable content for constants \isa{consts}
  1670     has changed.
  1671 
  1672   \end{description}
  1673 
  1674   An instance of \verb|CodeDataFun| provides the following
  1675   interface:
  1676 
  1677   \medskip
  1678   \begin{tabular}{l}
  1679   \isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
  1680   \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
  1681   \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
  1682   \end{tabular}
  1683 
  1684   \begin{description}
  1685 
  1686   \item \isa{get} retrieval of the current data.
  1687 
  1688   \item \isa{change} update of current data (cached!)
  1689     by giving a continuation.
  1690 
  1691   \item \isa{change{\isacharunderscore}yield} update with side result.
  1692 
  1693   \end{description}%
  1694 \end{isamarkuptext}%
  1695 \isamarkuptrue%
  1696 %
  1697 \begin{isamarkuptext}%
  1698 \emph{Happy proving, happy hacking!}%
  1699 \end{isamarkuptext}%
  1700 \isamarkuptrue%
  1701 %
  1702 \isadelimtheory
  1703 %
  1704 \endisadelimtheory
  1705 %
  1706 \isatagtheory
  1707 \isacommand{end}\isamarkupfalse%
  1708 %
  1709 \endisatagtheory
  1710 {\isafoldtheory}%
  1711 %
  1712 \isadelimtheory
  1713 %
  1714 \endisadelimtheory
  1715 \isanewline
  1716 \end{isabellebody}%
  1717 %%% Local Variables:
  1718 %%% mode: latex
  1719 %%% TeX-master: "root"
  1720 %%% End: