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

   application of theorem proving systems in the area of
   software development and verification, its relevance manifests
   for running test cases and rapid prototyping.  In logical
   calculi like constructive type theory,
   a notion of executability is implicit due to the nature
-  of the calculus.  In contrast, specifications in Isabelle/HOL
+  of the calculus.  In contrast, specifications in Isabelle
   can be highly non-executable.  In order to bridge
   the gap between logic and executable specifications,
   an explicit non-trivial transformation has to be applied:
   code generation.
 

   Isabelle system \cite{isa-tutorial}.
   Generic in the sense that the
   \qn{target language} for which code shall ultimately be
   generated is not fixed but may be an arbitrary state-of-the-art
   functional programming language (currently, the implementation
-  supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}).
+  supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell
+  \cite{haskell-revised-report}).
   We aim to provide a
   versatile environment
   suitable for software development and verification,
   structuring the process
   of code generation into a small set of orthogonal principles
   while achieving a big coverage of application areas
   with maximum flexibility.
 
-  For readers, some familiarity and experience
-  with the ingredients
-  of the HOL \emph{Main} theory is assumed.
+  Conceptually the code generator framework is part
+  of Isabelle's @{text Pure} meta logic; the object logic
+  @{text HOL} which is an extension of @{text Pure}
+  already comes with a reasonable framework setup and thus provides
+  a good working horse for raising code-generation-driven
+  applications.  So, we assume some familiarity and experience
+  with the ingredients of the @{text HOL} \emph{Main} theory
+  (see also \cite{isa-tutorial}).
 *}
 
 
 subsection {* Overview *}
 
 text {*
   The code generator aims to be usable with no further ado
   in most cases while allowing for detailed customization.
-  This manifests in the structure of this tutorial: this introduction
-  continues with a short introduction of concepts.  Section
+  This manifests in the structure of this tutorial:
+  we start with a generic example \secref{sec:example}
+  and introduce code generation concepts \secref{sec:concept}.
+  Section
   \secref{sec:basics} explains how to use the framework naively,
   presuming a reasonable default setup.  Then, section
   \secref{sec:advanced} deals with advanced topics,
   introducing further aspects of the code generator framework
   in a motivation-driven manner.  Last, section \secref{sec:ml}

     is supposed to replace the already established code generator
     by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
     So, for the moment, there are two distinct code generators
     in Isabelle.
     Also note that while the framework itself is largely
-    object-logic independent, only HOL provides a reasonable
+    object-logic independent, only @{text HOL} provides a reasonable
     framework setup.    
   \end{warn}
 *}
 
 
-subsection {* An exmaple: a simple theory of search trees *}
+section {* An example: a simple theory of search trees \label{sec:example} *}
+
+text {*
+  When writing executable specifications, it is convenient to use
+  three existing packages: the datatype package for defining
+  datatypes, the function package for (recursive) functions,
+  and the class package for overloaded definitions.
+
+  We develope a small theory of search trees; trees are represented
+  as a datatype with key type @{typ "'a"} and value type @{typ "'b"}:
+*}
 
 datatype ('a, 'b) searchtree = Leaf "'a\<Colon>linorder" 'b
   | Branch "('a, 'b) searchtree" "'a" "('a, 'b) searchtree"
+
+text {*
+  \noindent Note that we have constrained the type of keys
+  to the class of total orders, @{text linorder}.
+
+  We define @{text find} and @{text update} functions:
+*}
 
 fun
   find :: "('a\<Colon>linorder, 'b) searchtree \<Rightarrow> 'a \<Rightarrow> 'b option" where
   "find (Leaf key val) it = (if it = key then Some val else None)"
   | "find (Branch t1 key t2) it = (if it \<le> key then find t1 it else find t2 it)"

     if it \<le> key
       then (Branch (update (it, entry) t1) key t2)
       else (Branch t1 key (update (it, entry) t2))
    )"
 
+text {*
+  \noindent For testing purpose, we define a small example
+  using natural numbers @{typ nat} (which are a @{text linorder})
+  as keys and strings values:
+*}
+
 fun
   example :: "nat \<Rightarrow> (nat, string) searchtree" where
   "example n = update (n, ''bar'') (Leaf 0 ''foo'')"
 
+text {*
+  \noindent Then we generate code
+*}
+
 code_gen example (*<*)(SML #)(*>*)(SML "examples/tree.ML")
 
 text {*
+  \noindent which looks like:
   \lstsml{Thy/examples/tree.ML}
 *}
 
-subsection {* Code generation process *}
+
+section {* Code generation concepts and process \label{sec:concept} *}
 
 text {*
   \begin{figure}[h]
   \centering
   \includegraphics[width=0.7\textwidth]{codegen_process}

   fac :: "nat \<Rightarrow> nat" where
     "fac 0 = 1"
   | "fac (Suc n) = Suc n * fac n"
 
 text {*
-  This executable specification is now turned to SML code:
+  \noindent This executable specification is now turned to SML code:
 *}
 
 code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac.ML")
 
 text {*
-  The @{text "\<CODEGEN>"} command takes a space-separated list of
+  \noindent  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.

   code:
 
   \lstsml{Thy/examples/fac.ML}
 
   The code generator will complain when a required
-  ingredient does not provide a executable counterpart.
-  This is the case if an involved type is not a datatype:
-*}
-
-(*<*)
-setup {* Sign.add_path "foo" *}
-(*>*)
-
-typedecl 'a foo
-
-definition
-  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "bar x y = y"
-
-(*<*)
-hide type foo
-hide const bar
-
-setup {* Sign.parent_path *}
-
-datatype 'a foo = Foo
-
-definition
-  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "bar x y = y"
-(*>*)
-
-code_gen bar (SML "examples/fail_type.ML")
-
-text {*
-  \noindent will result in an error. Likewise, generating code
+  ingredient does not provide a executable counterpart,
+  e.g.~generating code
   for constants not yielding
-  a defining equation will fail, e.g.~the Hilbert choice
-  operation @{text "SOME"}:
+  a defining equation (e.g.~the Hilbert choice
+  operation @{text "SOME"}):
 *}
 
 (*<*)
 setup {* Sign.add_path "foo" *}
 (*>*)

   "pick_some = hd"
 (*>*)
 
 code_gen pick_some (SML "examples/fail_const.ML")
 
+text {* \noindent will fail. *}
+
 subsection {* Theorem selection *}
 
 text {*
   The list of all defining equations in a theory may be inspected
   using the @{text "\<PRINTCODESETUP>"} command:

 
 text {*
   \noindent which displays a table of constant with corresponding
   defining equations (the additional stuff displayed
   shall not bother us for the moment). If this table does
-  not provide at least one function
-  equation, the table of primitive definitions is searched
+  not provide at least one defining
+  equation for a particular constant, 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 @{text "\<FUN>"},
   @{text "\<FUNCTION>"}, @{text "\<PRIMREC>"}

 text {*
   \noindent print all cached defining equations (i.e.~\emph{after}
   any applied transformation).  A
   list of constants may be given; their function
   equations are added to the cache if not already present.
-*}
+
+  Similarly, the @{text "\<CODEDEPS>"} command shows a graph
+  visualizing dependencies between defining equations.
+*}
+
 
 
 section {* Recipes and advanced topics \label{sec:advanced} *}
 
 text {*

 text {*
   would mean nothing else than to introduce the evil
   sort constraint by hand.
 *}
 
+
+subsection {* Constructor sets for datatypes *}
+
+text {*
+  \fixme
+*}
+
+
 subsection {* Cyclic module dependencies *}
 
 text {*
   Sometimes the awkward situation occurs that dependencies
   between definitions introduce cyclic dependencies

   constants by unique identifiers.
 *}
 
 text %mlref {*
   \begin{mldecls}
-  @{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"} \\
+  @{index_ML_type CodegenConsts.const: "string * string option"} \\
+  @{index_ML CodegenConsts.const_of_cexpr: "theory -> string * typ -> CodegenConsts.const"} \\
  \end{mldecls}
 
   \begin{description}
 
   \item @{ML_type CodegenConsts.const} is the identifier type:
      the product of a \emph{string} with a list of \emph{typs}.
      The \emph{string} is the constant name as represented inside Isabelle;
-     the \emph{typs} are a type instantiation in the sense of System F,
-     with canonical names for type variables.
-
-  \item @{ML CodegenConsts.norm_of_typ}~@{text thy}~@{text "(constname, typ)"}
-     maps a constant expression @{text "(constname, typ)"} to its canonical identifier.
-
-  \item @{ML CodegenConsts.typ_of_inst}~@{text thy}~@{text const}
-     maps a canonical identifier @{text const} to a constant
-     expression with appropriate type.
+     for overloaded constants, the attached \emph{string option}
+     is either @{text SOME} type constructor denoting an instance,
+     or @{text NONE} for the polymorphic constant.
+
+  \item @{ML CodegenConsts.const_of_cexpr}~@{text thy}~@{text "(constname, typ)"}
+     maps a constant expression @{text "(constname, typ)"}
+     to its canonical identifier.
 
   \end{description}
 *}
 
 subsection {* Executable theory content: codegen\_data.ML *}

 
 subsubsection {* Managing executable content *}
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\
+  @{index_ML CodegenData.add_func: "bool -> thm -> theory -> theory"} \\
   @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\
   @{index_ML CodegenData.add_funcl: "CodegenConsts.const * thm list Susp.T -> theory -> theory"} \\
   @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\
   @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\
   @{index_ML CodegenData.add_inline_proc: "string * (theory -> cterm list -> thm list)

 
 text %mlref {*
   \begin{mldecls}
   @{index_ML CodegenConsts.const_ord: "CodegenConsts.const * CodegenConsts.const -> order"} \\
   @{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\
-  @{index_ML CodegenConsts.consts_of: "theory -> term -> CodegenConsts.const list"} \\
   @{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\
   @{index_ML_structure CodegenConsts.Consttab} \\
   @{index_ML CodegenFunc.typ_func: "thm -> typ"} \\
   @{index_ML CodegenFunc.rewrite_func: "thm list -> thm -> thm"} \\
   \end{mldecls}

   \item @{ML CodegenConsts.const_ord},~@{ML CodegenConsts.eq_const}
      provide order and equality on constant identifiers.
 
   \item @{ML_struct CodegenConsts.Consttab}
      provides table structures with constant identifiers as keys.
-
-  \item @{ML CodegenConsts.consts_of}~@{text thy}~@{text t}
-     returns all constant identifiers mentioned in a term @{text t}.
 
   \item @{ML CodegenConsts.read_const}~@{text thy}~@{text s}
      reads a constant as a concrete term expression @{text s}.
 
   \item @{ML CodegenFunc.typ_func}~@{text thm}