doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex

 \begin{isamarkuptext}%
 \noindent Then we generate code%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ example\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent which looks like:
   \lstsml{Thy/examples/tree.ML}%
 \end{isamarkuptext}%
 \isamarkuptrue%

 \begin{isamarkuptext}%
 \noindent This executable specification is now turned to SML code:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ fac\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent  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
-  depending on the target. In the SML case, a filename
-  is given where to write the generated code to.
+  These start with a \qn{target language}
+  identifier, followed by a file specification
+  where to write the generated code to.
 
   Internally, the defining equations for all selected
   constants are taken, including any transitively required
   constants, datatypes and classes, resulting in the following
   code:

 %
 \isadelimML
 %
 \endisadelimML
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ pick{\isacharunderscore}some\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ pick{\isacharunderscore}some\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent will fail.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

 \isanewline
 %
 \endisadelimproof
 \isanewline
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ pick\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ pick\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent This theorem now is used for generating code:
 
   \lstsml{Thy/examples/pick1.ML}
 
   \noindent It might be convenient to remove the pointless original
-  equation, using the \emph{nofunc} attribute:%
+  equation, using the \emph{func del} attribute:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemmas}\isamarkupfalse%
-\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ pick{\isachardot}simps\ \isanewline
+\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\ {\isacharequal}\ pick{\isachardot}simps\ \isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ pick\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ pick\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/pick2.ML}
 
   \noindent Syntactic redundancies are implicitly dropped. For example,
   using a modified version of the \isa{fac} function

 \isanewline
 %
 \endisadelimproof
 \isanewline
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isacharunderscore}case{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ fac\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isacharunderscore}case{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/fac_case.ML}
 
   \begin{warn}
     The attributes \emph{code} and \emph{code del}
     associated with the existing code generator also apply to
     the new one: \emph{code} implies \emph{code func},
-    and \emph{code del} implies \emph{code nofunc}.
+    and \emph{code del} implies \emph{code func del}.
   \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Type classes%

 Type classes offer a suitable occasion to introduce
   the Haskell serializer.  Its usage is almost the same
   as SML, but, in accordance with conventions
   some Haskell systems enforce, each module ends
   up in a single file. The module hierarchy is reflected in
-  the file system, with root given by the user.%
+  the file system, with root directory given as file specification.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ dummy\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}%
+\ dummy\ \isakeyword{in}\ Haskell\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lsthaskell{Thy/examples/Codegen.hs}
   \noindent (we have left out all other modules).
 
   \medskip
 
   The whole code in SML with explicit dictionary passing:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ dummy\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ dummy\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/class.ML}
 
   \medskip
 
   \noindent or in OCaml:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ dummy\ {\isacharparenleft}OCaml\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}{\isacharparenright}%
+\ dummy\ \isakeyword{in}\ OCaml\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/class.ocaml}
 
   \medskip The explicit association of constants
-  to classes can be inspected using the \isa{{\isasymPRINTCLASSES}}%
+  to classes can be inspected using the \isa{{\isasymPRINTCLASSES}}
+  command.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsection{Recipes and advanced topics \label{sec:advanced}%
 }

   defining equation.  Due to the interpretation of theorems
   of defining equations, rewrites are applied to the right
   hand side and the arguments of the left hand side of an
   equation, but never to the constant heading the left hand side.
   Inline theorems may be declared an undeclared using the
-  \emph{code inline} or \emph{code noinline} attribute respectively.
+  \emph{code inline} or \emph{code inline del} attribute respectively.
   Some common applications:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \begin{itemize}
-     \item replacing non-executable constructs by executable ones: \\
-\isacommand{lemma}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\item replacing non-executable constructs by executable ones:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \isacommand{lemma}\isamarkupfalse%
 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}%
+\ \ \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}%
 \isadelimproof
 \ %
 \endisadelimproof
 %
 \isatagproof

 %
 \isadelimproof
 %
 \endisadelimproof
 %
-\item eliminating superfluous constants: \\
-\isacommand{lemma}\isamarkupfalse%
+\begin{isamarkuptext}%
+\item eliminating superfluous constants:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \isacommand{lemma}\isamarkupfalse%
 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}%
+\ \ \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}%
 \isadelimproof
 \ %
 \endisadelimproof
 %
 \isatagproof

 %
 \isadelimproof
 %
 \endisadelimproof
 %
-\item replacing executable but inconvenient constructs: \\
-\isacommand{lemma}\isamarkupfalse%
+\begin{isamarkuptext}%
+\item replacing executable but inconvenient constructs:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \isacommand{lemma}\isamarkupfalse%
 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}%
+\ \ \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}%
 \isadelimproof
 \ %
 \endisadelimproof
 %
 \isatagproof

 \endisadelimproof
 %
 \end{itemize}
 %
 \begin{isamarkuptext}%
-The current set of inline theorems may be inspected using
+\noindent The current set of inline theorems may be inspected using
   the \isa{{\isasymPRINTCODESETUP}} command.
 
   \emph{Inline procedures} are a generalized version of inline
   theorems written in ML -- rewrite rules are generated dependent
   on the function theorems for a certain function.  One

   resulting in \isa{op\ mem}, which itself
   performs an explicit equality check.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ collect{\isacharunderscore}duplicates\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/collect_duplicates.ML}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

 %
 \endisadelimproof
 \isanewline
 \isanewline
 \isacommand{lemmas}\isamarkupfalse%
-\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline
+\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline
 \isanewline
 \isacommand{lemma}\isamarkupfalse%
 \ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\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
 \ \ {\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

 \noindent Then code generation succeeds:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
 \ {\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
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/lexicographic.ML}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

 %
 \isadelimtt
 %
 \endisadelimtt
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}literal{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ in{\isacharunderscore}interval\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}literal{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/bool_literal.ML}
 
   \noindent Though this is correct code, it is a little bit unsatisfactory:
   boolean values and operators are materialized as distinguished

 
   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{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/bool_mlbool.ML}
 
   \noindent This still is not perfect: the parentheses
   around the \qt{andalso} expression are superfluous.

 %
 \endisadelimtt
 \isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}infix{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}infix{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/bool_infix.ML}
 
   \medskip
 

 %
 \endisadelimproof
 \isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ insert\ {\isachardoublequoteopen}op\ {\isasymin}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymunion}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Union{\isachardoublequoteclose}\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}set{\isacharunderscore}list{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ insert\ {\isachardoublequoteopen}op\ {\isasymin}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymunion}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Union{\isachardoublequoteclose}\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}set{\isacharunderscore}list{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/set_list.ML}
 
   \medskip
 

 \ \ dummy{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ \ \ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ Some\ x{\isachardoublequoteclose}\isanewline
 \ \ {\isacharbar}\ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ dummy{\isacharunderscore}option\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}arbitrary{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ dummy{\isacharunderscore}option\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}arbitrary{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/arbitrary.ML}
 
   \medskip