doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy

 *}
 
 code_gen fac (SML "examples/fac.ML")
 
 text {*
-  The \isasymCODEGEN command takes a space-separated list of
+  The @{text "\<CODEGEN>"} 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.

 
 subsection {* Theorem selection *}
 
 text {*
   The list of all function equations in a theory may be inspected
-  using the \isasymPRINTCODETHMS command:
+  using the @{text "\<PRINTCODETHMS>"} command:
 *}
 
 print_codethms
 
 text {*

   not provide at least one function
   equation, the table of primitive definitions is searched
   whether it provides one.
 
   The typical HOL tools are already set up in a way that
-  function definitions introduced by \isasymFUN, \isasymFUNCTION,
-  \isasymPRIMREC, \isasymRECDEF are implicitly propagated
+  function definitions introduced by @{text "\<FUN>"},
+  @{text "\<FUNCTION>"}, @{text "\<PRIMREC>"}
+  @{text "\<RECDEF>"} are implicitly propagated
   to this function equation table. Specific theorems may be
   selected using an attribute: \emph{code func}. As example,
   a weight selector function:
 *}
 

   The cache may be partially or fully dropped if the underlying
   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 \isasymCODEGEN: either the list of constants or the
+  of the @{text "\<CODEGEN>"}: either the list of constants or the
   list of serialization expressions may be dropped.  If no
   serialization expressions are given, only abstract code
   is generated and cached; if no constants are given, the
   current cache is serialized.
 
-  For explorative reasons, an extended version of the
-  \isasymCODEGEN command may prove useful:
+  For explorative purpose, an extended version of the
+  @{text "\<CODEGEN>"} command may prove useful:
 *}
 
 print_codethms ()
 
 text {*

   library; beside being useful in applications, they may serve
   as a tutorial for customizing the code generator setup.
 
   \begin{description}
 
-    \item[ExecutableSet] allows to generate code
+    \item[@{theory "ExecutableSet"}] allows to generate code
        for finite sets using lists.
-    \item[ExecutableRat] \label{exec_rat} implements rational
+    \item[@{theory "ExecutableRat"}] \label{exec_rat} implements rational
        numbers as triples @{text "(sign, enumerator, denominator)"}.
-    \item[EfficientNat] \label{eff_nat} implements natural numbers by integers,
+    \item[@{theory "EfficientNat"}] \label{eff_nat} implements natural numbers by integers,
        which in general will result in higher efficency; pattern
        matching with @{const "0\<Colon>nat"} / @{const "Suc"}
        is eliminated.
-    \item[MLString] provides an additional datatype @{text "mlstring"};
+    \item[@{theory "MLString"}] provides an additional datatype @{text "mlstring"};
        in the HOL default setup, strings in HOL are mapped to list
        of chars in SML; values of type @{text "mlstring"} are
        mapped to strings in SML.
 
   \end{description}

   \end{itemize}
 *}
 
 text {*
   The current set of inline theorems may be inspected using
-  the \isasymPRINTCODETHMS command.
+  the @{text "\<PRINTCODETHMS>"} 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
   application is the implicit expanding of @{typ nat} numerals

 
   \emph{Generic preprocessors} provide a most general interface,
   transforming a list of function theorems to another
   list of function theorems, provided that neither the heading
   constant nor its type change.  The @{const "0\<Colon>nat"} / @{const Suc}
-  pattern elimination implemented in \secref{eff_nat} uses this
+  pattern elimination implemented in
+  theory @{theory "EfficientNat"} (\secref{eff_nat}) uses this
   interface.
 
   \begin{warn}
     The order in which single preprocessing steps are carried
     out currently is not specified; in particular, preprocessing

 (*<*)
 declare in_interval.simps [code func]
 (*>*)
 
 (*<*)
-code_type bool
+code_type %tt bool
   (SML)
-code_const True and False and "op \<and>" and Not
+code_const %tt True and False and "op \<and>" and Not
   (SML and and and)
 (*>*)
 
-code_gen in_interval (SML "examples/bool1.ML")
-
-text {*
-  \lstsml{Thy/examples/bool1.ML}
+code_gen in_interval (SML "examples/bool_literal.ML")
+
+text {*
+  \lstsml{Thy/examples/bool_literal.ML}
 
   Though this is correct code, it is a little bit unsatisfactory:
   boolean values and operators are materialized as distinguished
   entities with have nothing to do with the SML-builtin notion
   of \qt{bool}.  This results in less readable code;

   the existing SML \qt{bool} would be used.  To map
   the HOL \qt{bool} on SML \qt{bool}, we may use
   \qn{custom serializations}:
 *}
 
-code_type bool
+code_type %tt bool
   (SML "bool")
-code_const True and False and "op \<and>"
+code_const %tt True and False and "op \<and>"
   (SML "true" and "false" and "_ andalso _")
 
 text {*
-  The \isasymCODETYPE commad takes a type constructor
+  The @{text "\<CODETYPE>"} commad takes a type constructor
   as arguments together with a list of custom serializations.
   Each custom serialization starts with a target language
   identifier followed by an expression, which during
   code serialization is inserted whenever the type constructor
-  would occur.  For constants, \isasymCODECONST implements
-  the corresponding mechanism.  Each \qt{\_} in
+  would occur.  For constants, @{text "\<CODECONST>"} implements
+  the corresponding mechanism.  Each ``@{verbatim "_"}'' in
   a serialization expression is treated as a placeholder
   for the type constructor's (the constant's) arguments.
 *}
 
 code_reserved SML
   bool true false
 
 text {*
   To assert that the existing \qt{bool}, \qt{true} and \qt{false}
-  is not used for generated code, we use \isasymCODERESERVED.
+  is not used for generated code, we use @{text "\<CODERESERVED>"}.
 
   After this setup, code looks quite more readable:
 *}
 
-code_gen in_interval (SML "examples/bool2.ML")
-
-text {*
-  \lstsml{Thy/examples/bool2.ML}
+code_gen in_interval (SML "examples/bool_mlbool.ML")
+
+text {*
+  \lstsml{Thy/examples/bool_mlbool.ML}
 
   This still is not perfect: the parentheses
-  around \qt{andalso} are superfluous.  Though the serializer
+  around the \qt{andalso} expression are superfluous.
+  Though the serializer
   by no means attempts to imitate the rich Isabelle syntax
   framework, it provides some common idioms, notably
   associative infixes with precedences which may be used here:
 *}
 
-code_const "op \<and>"
+code_const %tt "op \<and>"
   (SML infixl 1 "andalso")
 
-code_gen in_interval (SML "examples/bool3.ML")
-
-text {*
-  \lstsml{Thy/examples/bool3.ML}
+code_gen in_interval (SML "examples/bool_infix.ML")
+
+text {*
+  \lstsml{Thy/examples/bool_infix.ML}
 
   Next, we try to map HOL pairs to SML pairs, using the
-  infix \qt{ * } type constructor and parentheses:
+  infix ``@{verbatim "*"}'' type constructor and parentheses:
 *}
 
 (*<*)
 code_type *
   (SML)
 code_const Pair
   (SML)
 (*>*)
 
-code_type *
+code_type %tt *
   (SML infix 2 "*")
 
-code_const Pair
+code_const %tt Pair
   (SML "!((_),/ (_))")
 
 text {*
-  The initial bang \qt{!} tells the serializer to never put
+  The initial bang ``@{verbatim "!"}'' tells the serializer to never put
   parentheses around the whole expression (they are already present),
   while the parentheses around argument place holders
   tell not to put parentheses around the arguments.
-  The slash \qt{/} (followed by arbitrary white space)
+  The slash ``@{verbatim "/"}'' (followed by arbitrary white space)
   inserts a space which may be used as a break if necessary
   during pretty printing.
 
   So far, we did only provide more idiomatic serializations for
   constructs which would be executable on their own.  Target-specific

   \footnote{Eventually, we also want to provide executability
   for quotients.}.  However, we could use the SML builtin
   integers:
 *}
 
-code_type int
+code_type %tt int
   (SML "IntInf.int")
 
-code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
+code_const %tt "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
     and "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   (SML "IntInf.+ (_, _)" and "IntInf.* (_, _)")
 
 code_gen double_inc (SML "examples/integers.ML")
 

   inconsistencies -- or, in other words:
   custom serializations are completely axiomatic.
 
   A further noteworthy details is that any special
   character in a custom serialization may be quoted
-  using \qt{'}; thus, in \qt{fn '\_ => \_} the first
-  \qt{'\_} is a proper underscore while the
-  second \qt{\_} is a placeholder.
+  using ``@{verbatim "'"}''; thus, in
+  ``@{verbatim "fn '_ => _"}'' the first
+  ``@{verbatim "_"}'' is a proper underscore while the
+  second ``@{verbatim "_"}'' is a placeholder.
 
   The HOL theories provide further
   examples for custom serializations and form
   a recommended tutorial on how to use them properly.
 *}

 
 text {*
   Examine the following:
 *}
 
-code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const %tt "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!(_ : IntInf.int = _)")
 
 text {*
   What is wrong here? Since @{const "op ="} is nothing else then
   a plain constant, this customary serialization will refer
   to polymorphic equality @{const "op = \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool"}.
   Instead, we want the specific equality on @{typ int},
   by using the overloaded constant @{const "Code_Generator.eq"}:
 *}
 
-code_const "Code_Generator.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const %tt "Code_Generator.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!(_ : IntInf.int = _)")
 
 subsubsection {* typedecls interpreted by customary serializations *}
 
 text {*

 termination by (auto_term "measure (length o fst)")
 (*<*)
 lemmas [code func] = lookup.simps
 (*>*)
 
-code_type key
+code_type %tt key
   (SML "string")
 
 text {*
   This, though, is not sufficient: @{typ key} is no instance
   of @{text eq} since @{typ key} is no datatype; the instance

   for the particular instance of @{const "Code_Generator.eq"}:
 *}
 
 instance key :: eq ..
 
-code_const "Code_Generator.eq \<Colon> key \<Rightarrow> key \<Rightarrow> bool"
+code_const %tt "Code_Generator.eq \<Colon> key \<Rightarrow> key \<Rightarrow> bool"
   (SML "!(_ : string = _)")
 
 text {*
   Then everything goes fine:
 *}

 
 text {*
   For convenience, the default
   HOL setup for Haskell maps the @{text eq} class to
   its counterpart in Haskell, giving custom serializations
-  for the class (\isasymCODECLASS) and its operation:
+  for the class (@{text "\<CODECLASS>"}) and its operation:
 *}
 
 (*<*)
 setup {* Sign.add_path "bar" *}
 class eq = fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 (*>*)
 
-code_class eq
+code_class %tt eq
   (Haskell "Eq" where eq \<equiv> "(==)")
 
-code_const eq
+code_const %tt eq
   (Haskell infixl 4 "==")
 
 (*<*)
 hide "class" eq
 hide const eq

 
 typedecl bar
 
 instance bar :: eq ..
 
-code_type bar
+code_type %tt bar
   (Haskell "Integer")
 
 text {*
     The code generator would produce
     an additional instance, which of course is rejected.
     To suppress this additional instance, use
-    \isasymCODEINSTANCE:
-*}
-
-code_instance bar :: eq
+    @{text "\<CODEINSTANCE>"}:
+*}
+
+code_instance %tt bar :: eq
   (Haskell -)
 
 subsection {* Types matter *}
 
 text {*
   Imagine the following quick-and-dirty setup for implementing
   some kind of sets as lists in SML:
 *}
 
-code_type set
+code_type %tt set
   (SML "_ list")
 
-code_const "{}" and insert
+code_const %tt "{}" and insert
   (SML "![]" and infixl 7 "::")
 
 definition
   dummy_set :: "(nat \<Rightarrow> nat) set"
   "dummy_set = {Suc}"

   to identify the famous HOL constant @{const arbitrary}
   of type @{typ "'a option"} with @{const None}.
   By brute force:
 *}
 
-axioms
-  arbitrary_option: "arbitrary = None"
+axiomatization where
+  "arbitrary = None"
 
 text {*
   However this has to be considered harmful since this axiom,
   though probably justifiable for generated code, could
   introduce serious inconsistencies into the logic.

 
 definition
   "None' = None"
 
 text {*
-  Then finally we are enabled to use \isasymCODEAXIOMS:
+  Then finally we are enabled to use @{text "\<CODEAXIOMS>"}:
 *}
 
 code_axioms
   arbitrary_option \<equiv> None'
 

 text {*
   \lstsml{Thy/examples/arbitrary.ML}
 
   Another axiomatic extension is code generation
   for abstracted types.  For this, the  
-  \emph{ExecutableRat} (see \secref{exec_rat})
+  @{theory "ExecutableRat"} (see \secref{exec_rat})
   forms a good example.
 *}
 
 
 section {* ML interfaces \label{sec:ml} *}

   constants by unique identifiers.
 *}
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML_type CodegenConsts.const} \\
+  @{index_ML_type CodegenConsts.const: "string * typ list"} \\
   @{index_ML CodegenConsts.norm_of_typ: "theory -> string * typ -> CodegenConsts.const"} \\
   @{index_ML CodegenConsts.typ_of_inst: "theory -> CodegenConsts.const -> string * typ"} \\
  \end{mldecls}
 
   \begin{description}

 
 subsubsection {* Suspended theorems *}
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML_type CodegenData.lthms} \\
   @{index_ML CodegenData.lazy: "(unit -> thm list) -> CodegenData.lthms"}
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML_type CodegenData.lthms} is an abstract view
-     on suspended theorems.  Suspensions are evaluated on demand.
-
   \item @{ML CodegenData.lazy}~@{text f} turns an abstract
-     theorem computation @{text f} into suspended theorems.
+     theorem computation @{text f} into a suspension of theorems.
 
   \end{description}
 *}
 
 subsubsection {* Executable content *}
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML_type CodegenData.lthms} \\
   @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\
   @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\
   @{index_ML CodegenData.add_funcl: "CodegenConsts.const * CodegenData.lthms -> theory -> theory"} \\
   @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\
   @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\

 
 subsubsection {* Datatype hooks *}
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML_type DatatypeHooks.hook} \\
+  @{index_ML_type DatatypeHooks.hook: "string list -> theory -> theory"} \\
   @{index_ML DatatypeHooks.add: "DatatypeHooks.hook -> theory -> theory"}
   \end{mldecls}
 *}
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML_type TypecopyPackage.info} \\
+  @{index_ML_type TypecopyPackage.info: "{
+    vs: (string * sort) list,
+    constr: string,
+    typ: typ,
+    inject: thm,
+    proj: string * typ,
+    proj_def: thm
+  }"} \\
   @{index_ML TypecopyPackage.add_typecopy: "
     bstring * string list -> typ -> (bstring * bstring) option
     -> theory -> (string * TypecopyPackage.info) * theory"} \\
   @{index_ML TypecopyPackage.get_typecopies: "theory -> string list"} \\
   @{index_ML TypecopyPackage.get_typecopy_info: "theory

   \end{mldecls}
 *}
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML_type DatatypeCodegen.hook} \\
+  @{index_ML_type DatatypeCodegen.hook: "(string * (bool * ((string * sort) list * (string * typ list) list))) list
+    -> theory -> theory"} \\
   @{index_ML DatatypeCodegen.add_codetypes_hook_bootstrap: "
       DatatypeCodegen.hook -> theory -> theory"}
   \end{mldecls}
 *}