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

 \ \ \ \ {\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}%
 \begin{isamarkuptext}%
 \noindent Then we generate code%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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}%

 \ \ {\isacharbar}\ {\isachardoublequoteopen}fac\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharasterisk}\ fac\ n{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent This executable specification is now turned to SML code:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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
+\noindent  The \isa{{\isasymEXPORTCODE}} command takes a space-separated list of
   constants together with \qn{serialization directives}
   These start with a \qn{target language}
   identifier, followed by a file specification
   where to write the generated code to.
 

 {\isafoldML}%
 %
 \isadelimML
 %
 \endisadelimML
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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%

 \isadelimproof
 \isanewline
 %
 \endisadelimproof
 \isanewline
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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}

 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemmas}\isamarkupfalse%
 \ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\ {\isacharequal}\ pick{\isachardot}simps\ \isanewline
 \isanewline
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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,

 \isadelimproof
 \isanewline
 %
 \endisadelimproof
 \isanewline
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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}

   some Haskell systems enforce, each module ends
   up in a single file. The module hierarchy is reflected in
   the file system, with root directory given as file specification.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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

 The membership test during preprocessing is rewritten,
   resulting in \isa{op\ mem}, which itself
   performs an explicit equality check.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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%

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

 %
 \begin{isamarkuptext}%
 does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isacharcolon}{\isacharcolon}\ monotype\ {\isasymRightarrow}\ monotype\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}monotype{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/monotype.ML}%
 \end{isamarkuptext}%

 {\isafoldtt}%
 %
 \isadelimtt
 %
 \endisadelimtt
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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:

   the corresponding mechanism.  Each ``\verb|_|'' in
   a serialization expression is treated as a placeholder
   for the type constructor's (the constant's) arguments.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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

 \isadelimtt
 %
 \endisadelimtt
 \isanewline
 \isanewline
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ 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

 \isadelimproof
 %
 \endisadelimproof
 \isanewline
 \isanewline
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ {\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

   executable content of the theory changes.
   Implementation of caching is supposed to transparently
   hid away the details from the user.  Anyway, caching
   reaches the surface by using a slightly more general form
   of the \isa{{\isasymCODETHMS}}, \isa{{\isasymCODEDEPS}}
-  and \isa{{\isasymCODEGEN}} commands: the list of constants
+  and \isa{{\isasymEXPORTCODE}} commands: the list of constants
   may be omitted.  Then, all constants with code theorems
   in the current cache are referred to.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %