--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/Foundations.thy Fri Aug 13 14:40:15 2010 +0200
@@ -0,0 +1,432 @@
+theory Foundations
+imports Introduction
+begin
+
+section {* Code generation foundations \label{sec:program} *}
+
+subsection {* The @{text "Isabelle/HOL"} default setup *}
+
+text {*
+ We have already seen how by default equations stemming from
+ @{command definition}, @{command primrec} and @{command fun}
+ statements are used for code generation. This default behaviour
+ can be changed, e.g.\ by providing different code equations.
+ The customisations shown in this section are \emph{safe}
+ as regards correctness: all programs that can be generated are partially
+ correct.
+*}
+
+subsection {* Selecting code equations *}
+
+text {*
+ Coming back to our introductory example, we
+ could provide an alternative code equations for @{const dequeue}
+ explicitly:
+*}
+
+lemma %quote [code]:
+ "dequeue (AQueue xs []) =
+ (if xs = [] then (None, AQueue [] [])
+ else dequeue (AQueue [] (rev xs)))"
+ "dequeue (AQueue xs (y # ys)) =
+ (Some y, AQueue xs ys)"
+ by (cases xs, simp_all) (cases "rev xs", simp_all)
+
+text {*
+ \noindent The annotation @{text "[code]"} is an @{text Isar}
+ @{text attribute} which states that the given theorems should be
+ considered as code equations for a @{text fun} statement --
+ the corresponding constant is determined syntactically. The resulting code:
+*}
+
+text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
+
+text {*
+ \noindent You may note that the equality test @{term "xs = []"} has been
+ replaced by the predicate @{term "null xs"}. This is due to the default
+ setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
+
+ Changing the default constructor set of datatypes is also
+ possible. See \secref{sec:datatypes} for an example.
+
+ As told in \secref{sec:concept}, code generation is based
+ on a structured collection of code theorems.
+ This collection
+ may be inspected using the @{command code_thms} command:
+*}
+
+code_thms %quote dequeue
+
+text {*
+ \noindent prints a table with \emph{all} code equations
+ for @{const dequeue}, including
+ \emph{all} code equations those equations depend
+ on recursively.
+
+ Similarly, the @{command code_deps} command shows a graph
+ visualising dependencies between code equations.
+*}
+
+subsection {* @{text class} and @{text instantiation} *}
+
+text {*
+ Concerning type classes and code generation, let us examine an example
+ from abstract algebra:
+*}
+
+class %quote semigroup =
+ fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
+ assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
+
+class %quote monoid = semigroup +
+ fixes neutral :: 'a ("\<one>")
+ assumes neutl: "\<one> \<otimes> x = x"
+ and neutr: "x \<otimes> \<one> = x"
+
+instantiation %quote nat :: monoid
+begin
+
+primrec %quote mult_nat where
+ "0 \<otimes> n = (0\<Colon>nat)"
+ | "Suc m \<otimes> n = n + m \<otimes> n"
+
+definition %quote neutral_nat where
+ "\<one> = Suc 0"
+
+lemma %quote add_mult_distrib:
+ fixes n m q :: nat
+ shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
+ by (induct n) simp_all
+
+instance %quote proof
+ fix m n q :: nat
+ show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
+ by (induct m) (simp_all add: add_mult_distrib)
+ show "\<one> \<otimes> n = n"
+ by (simp add: neutral_nat_def)
+ show "m \<otimes> \<one> = m"
+ by (induct m) (simp_all add: neutral_nat_def)
+qed
+
+end %quote
+
+text {*
+ \noindent We define the natural operation of the natural numbers
+ on monoids:
+*}
+
+primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+ "pow 0 a = \<one>"
+ | "pow (Suc n) a = a \<otimes> pow n a"
+
+text {*
+ \noindent This we use to define the discrete exponentiation function:
+*}
+
+definition %quote bexp :: "nat \<Rightarrow> nat" where
+ "bexp n = pow n (Suc (Suc 0))"
+
+text {*
+ \noindent The corresponding code in Haskell uses that language's native classes:
+*}
+
+text %quote {*@{code_stmts bexp (Haskell)}*}
+
+text {*
+ \noindent This is a convenient place to show how explicit dictionary construction
+ manifests in generated code (here, the same example in @{text SML})
+ \cite{Haftmann-Nipkow:2010:code}:
+*}
+
+text %quote {*@{code_stmts bexp (SML)}*}
+
+text {*
+ \noindent Note the parameters with trailing underscore (@{verbatim "A_"}),
+ which are the dictionary parameters.
+*}
+
+subsection {* The preprocessor \label{sec:preproc} *}
+
+text {*
+ Before selected function theorems are turned into abstract
+ code, a chain of definitional transformation steps is carried
+ out: \emph{preprocessing}. In essence, the preprocessor
+ consists of two components: a \emph{simpset} and \emph{function transformers}.
+
+ The \emph{simpset} can apply the full generality of the
+ Isabelle simplifier. Due to the interpretation of theorems as code
+ 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. An important special case are
+ \emph{unfold theorems}, which may be declared and removed using
+ the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
+ attribute, respectively.
+
+ Some common applications:
+*}
+
+text_raw {*
+ \begin{itemize}
+*}
+
+text {*
+ \item replacing non-executable constructs by executable ones:
+*}
+
+lemma %quote [code_unfold]:
+ "x \<in> set xs \<longleftrightarrow> List.member xs x" by (fact in_set_member)
+
+text {*
+ \item eliminating superfluous constants:
+*}
+
+lemma %quote [code_unfold]:
+ "1 = Suc 0" by (fact One_nat_def)
+
+text {*
+ \item replacing executable but inconvenient constructs:
+*}
+
+lemma %quote [code_unfold]:
+ "xs = [] \<longleftrightarrow> List.null xs" by (fact eq_Nil_null)
+
+text_raw {*
+ \end{itemize}
+*}
+
+text {*
+ \noindent \emph{Function transformers} provide a very 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 @{term "0\<Colon>nat"} / @{const Suc}
+ pattern elimination implemented in
+ theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this
+ interface.
+
+ \noindent The current setup of the preprocessor may be inspected using
+ the @{command print_codeproc} command.
+ @{command code_thms} provides a convenient
+ mechanism to inspect the impact of a preprocessor setup
+ on code equations.
+
+ \begin{warn}
+
+ Attribute @{attribute code_unfold} also applies to the
+ preprocessor of the ancient @{text "SML code generator"}; in case
+ this is not what you intend, use @{attribute code_inline} instead.
+ \end{warn}
+*}
+
+subsection {* Datatypes \label{sec:datatypes} *}
+
+text {*
+ Conceptually, any datatype is spanned by a set of
+ \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
+ "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
+ @{text "\<tau>"}. The HOL datatype package by default registers any new
+ datatype in the table of datatypes, which may be inspected using the
+ @{command print_codesetup} command.
+
+ In some cases, it is appropriate to alter or extend this table. As
+ an example, we will develop an alternative representation of the
+ queue example given in \secref{sec:intro}. The amortised
+ representation is convenient for generating code but exposes its
+ \qt{implementation} details, which may be cumbersome when proving
+ theorems about it. Therefore, here is a simple, straightforward
+ representation of queues:
+*}
+
+datatype %quote 'a queue = Queue "'a list"
+
+definition %quote empty :: "'a queue" where
+ "empty = Queue []"
+
+primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
+ "enqueue x (Queue xs) = Queue (xs @ [x])"
+
+fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
+ "dequeue (Queue []) = (None, Queue [])"
+ | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
+
+text {*
+ \noindent This we can use directly for proving; for executing,
+ we provide an alternative characterisation:
+*}
+
+definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
+ "AQueue xs ys = Queue (ys @ rev xs)"
+
+code_datatype %quote AQueue
+
+text {*
+ \noindent Here we define a \qt{constructor} @{const "AQueue"} which
+ is defined in terms of @{text "Queue"} and interprets its arguments
+ according to what the \emph{content} of an amortised queue is supposed
+ to be. Equipped with this, we are able to prove the following equations
+ for our primitive queue operations which \qt{implement} the simple
+ queues in an amortised fashion:
+*}
+
+lemma %quote empty_AQueue [code]:
+ "empty = AQueue [] []"
+ unfolding AQueue_def empty_def by simp
+
+lemma %quote enqueue_AQueue [code]:
+ "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
+ unfolding AQueue_def by simp
+
+lemma %quote dequeue_AQueue [code]:
+ "dequeue (AQueue xs []) =
+ (if xs = [] then (None, AQueue [] [])
+ else dequeue (AQueue [] (rev xs)))"
+ "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
+ unfolding AQueue_def by simp_all
+
+text {*
+ \noindent For completeness, we provide a substitute for the
+ @{text case} combinator on queues:
+*}
+
+lemma %quote queue_case_AQueue [code]:
+ "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
+ unfolding AQueue_def by simp
+
+text {*
+ \noindent The resulting code looks as expected:
+*}
+
+text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
+
+text {*
+ \noindent From this example, it can be glimpsed that using own
+ constructor sets is a little delicate since it changes the set of
+ valid patterns for values of that type. Without going into much
+ detail, here some practical hints:
+
+ \begin{itemize}
+
+ \item When changing the constructor set for datatypes, take care
+ to provide alternative equations for the @{text case} combinator.
+
+ \item Values in the target language need not to be normalised --
+ different values in the target language may represent the same
+ value in the logic.
+
+ \item Usually, a good methodology to deal with the subtleties of
+ pattern matching is to see the type as an abstract type: provide
+ a set of operations which operate on the concrete representation
+ of the type, and derive further operations by combinations of
+ these primitive ones, without relying on a particular
+ representation.
+
+ \end{itemize}
+*}
+
+
+subsection {* Equality *}
+
+text {*
+ Surely you have already noticed how equality is treated
+ by the code generator:
+*}
+
+primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ "collect_duplicates xs ys [] = xs"
+ | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
+ then if z \<in> set ys
+ then collect_duplicates xs ys zs
+ else collect_duplicates xs (z#ys) zs
+ else collect_duplicates (z#xs) (z#ys) zs)"
+
+text {*
+ \noindent During preprocessing, the membership test is rewritten,
+ resulting in @{const List.member}, which itself
+ performs an explicit equality check.
+*}
+
+text %quote {*@{code_stmts collect_duplicates (SML)}*}
+
+text {*
+ \noindent Obviously, polymorphic equality is implemented the Haskell
+ way using a type class. How is this achieved? HOL introduces
+ an explicit class @{class eq} with a corresponding operation
+ @{const eq_class.eq} such that @{thm eq [no_vars]}.
+ The preprocessing framework does the rest by propagating the
+ @{class eq} constraints through all dependent code equations.
+ For datatypes, instances of @{class eq} are implicitly derived
+ when possible. For other types, you may instantiate @{text eq}
+ manually like any other type class.
+*}
+
+
+subsection {* Explicit partiality *}
+
+text {*
+ Partiality usually enters the game by partial patterns, as
+ in the following example, again for amortised queues:
+*}
+
+definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
+ "strict_dequeue q = (case dequeue q
+ of (Some x, q') \<Rightarrow> (x, q'))"
+
+lemma %quote strict_dequeue_AQueue [code]:
+ "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
+ "strict_dequeue (AQueue xs []) =
+ (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
+ by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits)
+
+text {*
+ \noindent In the corresponding code, there is no equation
+ for the pattern @{term "AQueue [] []"}:
+*}
+
+text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
+
+text {*
+ \noindent In some cases it is desirable to have this
+ pseudo-\qt{partiality} more explicitly, e.g.~as follows:
+*}
+
+axiomatization %quote empty_queue :: 'a
+
+definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
+ "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"
+
+lemma %quote strict_dequeue'_AQueue [code]:
+ "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue
+ else strict_dequeue' (AQueue [] (rev xs)))"
+ "strict_dequeue' (AQueue xs (y # ys)) =
+ (y, AQueue xs ys)"
+ by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits)
+
+text {*
+ Observe that on the right hand side of the definition of @{const
+ "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
+
+ Normally, if constants without any code equations occur in a
+ program, the code generator complains (since in most cases this is
+ indeed an error). But such constants can also be thought
+ of as function definitions which always fail,
+ since there is never a successful pattern match on the left hand
+ side. In order to categorise a constant into that category
+ explicitly, use @{command "code_abort"}:
+*}
+
+code_abort %quote empty_queue
+
+text {*
+ \noindent Then the code generator will just insert an error or
+ exception at the appropriate position:
+*}
+
+text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
+
+text {*
+ \noindent This feature however is rarely needed in practice.
+ Note also that the @{text HOL} default setup already declares
+ @{const undefined} as @{command "code_abort"}, which is most
+ likely to be used in such situations.
+*}
+
+end
--- a/doc-src/Codegen/Thy/Further.thy Fri Aug 13 13:43:55 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Fri Aug 13 14:40:15 2010 +0200
@@ -191,4 +191,140 @@
the framework described there is available in theory @{theory Imperative_HOL}.
*}
+
+subsection {* ML system interfaces \label{sec:ml} *}
+
+text {*
+ Since the code generator framework not only aims to provide
+ a nice Isar interface but also to form a base for
+ code-generation-based applications, here a short
+ description of the most important ML interfaces.
+*}
+
+subsubsection {* Managing executable content *}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
+ @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
+ @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
+ @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\
+ @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
+ -> theory -> theory"} \\
+ @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
+ @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
+ @{index_ML Code.get_type: "theory -> string
+ -> (string * sort) list * ((string * string list) * typ list) list"} \\
+ @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function
+ theorem @{text "thm"} to executable content.
+
+ \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function
+ theorem @{text "thm"} from executable content, if present.
+
+ \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
+ the preprocessor simpset.
+
+ \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
+ function transformer @{text f} (named @{text name}) to executable content;
+ @{text f} is a transformer of the code equations belonging
+ to a certain function definition, depending on the
+ current theory context. Returning @{text NONE} indicates that no
+ transformation took place; otherwise, the whole process will be iterated
+ with the new code equations.
+
+ \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
+ function transformer named @{text name} from executable content.
+
+ \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
+ a datatype to executable content, with generation
+ set @{text cs}.
+
+ \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
+ returns type constructor corresponding to
+ constructor @{text const}; returns @{text NONE}
+ if @{text const} is no constructor.
+
+ \end{description}
+*}
+
+subsubsection {* Auxiliary *}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML Code.read_const: "theory -> string -> string"}
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML Code.read_const}~@{text thy}~@{text s}
+ reads a constant as a concrete term expression @{text s}.
+
+ \end{description}
+
+*}
+
+subsubsection {* Data depending on the theory's executable content *}
+
+text {*
+ Implementing code generator applications on top
+ of the framework set out so far usually not only
+ involves using those primitive interfaces
+ but also storing code-dependent data and various
+ other things.
+
+ Due to incrementality of code generation, changes in the
+ theory's executable content have to be propagated in a
+ certain fashion. Additionally, such changes may occur
+ not only during theory extension but also during theory
+ merge, which is a little bit nasty from an implementation
+ point of view. The framework provides a solution
+ to this technical challenge by providing a functorial
+ data slot @{ML_functor Code_Data}; on instantiation
+ of this functor, the following types and operations
+ are required:
+
+ \medskip
+ \begin{tabular}{l}
+ @{text "type T"} \\
+ @{text "val empty: T"} \\
+ \end{tabular}
+
+ \begin{description}
+
+ \item @{text T} the type of data to store.
+
+ \item @{text empty} initial (empty) data.
+
+ \end{description}
+
+ \noindent An instance of @{ML_functor Code_Data} provides the following
+ interface:
+
+ \medskip
+ \begin{tabular}{l}
+ @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
+ @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
+ \end{tabular}
+
+ \begin{description}
+
+ \item @{text change} update of current data (cached!)
+ by giving a continuation.
+
+ \item @{text change_yield} update with side result.
+
+ \end{description}
+*}
+
+text {*
+ \bigskip
+
+ \emph{Happy proving, happy hacking!}
+*}
+
end
--- a/doc-src/Codegen/Thy/Inductive_Predicate.thy Fri Aug 13 13:43:55 2010 +0200
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Fri Aug 13 14:40:15 2010 +0200
@@ -2,7 +2,7 @@
imports Setup
begin
-subsection {* Inductive Predicates *}
+section {* Inductive Predicates *}
(*<*)
hide_const append
--- a/doc-src/Codegen/Thy/Introduction.thy Fri Aug 13 13:43:55 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Fri Aug 13 14:40:15 2010 +0200
@@ -2,7 +2,17 @@
imports Setup
begin
-section {* Introduction and Overview *}
+section {* Introduction *}
+
+subsection {* Code generation fundamental: shallow embedding *}
+
+subsection {* A quick start with the @{text "Isabelle/HOL"} toolbox *}
+
+subsection {* Type classes *}
+
+subsection {* How to continue from here *}
+
+subsection {* If something goes utterly wrong *}
text {*
This tutorial introduces a generic code generator for the
--- a/doc-src/Codegen/Thy/ML.thy Fri Aug 13 13:43:55 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-theory "ML"
-imports Setup
-begin
-
-section {* ML system interfaces \label{sec:ml} *}
-
-text {*
- Since the code generator framework not only aims to provide
- a nice Isar interface but also to form a base for
- code-generation-based applications, here a short
- description of the most important ML interfaces.
-*}
-
-subsection {* Executable theory content: @{text Code} *}
-
-text {*
- This Pure module implements the core notions of
- executable content of a theory.
-*}
-
-subsubsection {* Managing executable content *}
-
-text %mlref {*
- \begin{mldecls}
- @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
- @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
- @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
- @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\
- @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
- -> theory -> theory"} \\
- @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
- @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
- @{index_ML Code.get_type: "theory -> string
- -> (string * sort) list * ((string * string list) * typ list) list"} \\
- @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
- \end{mldecls}
-
- \begin{description}
-
- \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function
- theorem @{text "thm"} to executable content.
-
- \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function
- theorem @{text "thm"} from executable content, if present.
-
- \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
- the preprocessor simpset.
-
- \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
- function transformer @{text f} (named @{text name}) to executable content;
- @{text f} is a transformer of the code equations belonging
- to a certain function definition, depending on the
- current theory context. Returning @{text NONE} indicates that no
- transformation took place; otherwise, the whole process will be iterated
- with the new code equations.
-
- \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
- function transformer named @{text name} from executable content.
-
- \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
- a datatype to executable content, with generation
- set @{text cs}.
-
- \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
- returns type constructor corresponding to
- constructor @{text const}; returns @{text NONE}
- if @{text const} is no constructor.
-
- \end{description}
-*}
-
-subsection {* Auxiliary *}
-
-text %mlref {*
- \begin{mldecls}
- @{index_ML Code.read_const: "theory -> string -> string"}
- \end{mldecls}
-
- \begin{description}
-
- \item @{ML Code.read_const}~@{text thy}~@{text s}
- reads a constant as a concrete term expression @{text s}.
-
- \end{description}
-
-*}
-
-subsection {* Implementing code generator applications *}
-
-text {*
- Implementing code generator applications on top
- of the framework set out so far usually not only
- involves using those primitive interfaces
- but also storing code-dependent data and various
- other things.
-*}
-
-subsubsection {* Data depending on the theory's executable content *}
-
-text {*
- Due to incrementality of code generation, changes in the
- theory's executable content have to be propagated in a
- certain fashion. Additionally, such changes may occur
- not only during theory extension but also during theory
- merge, which is a little bit nasty from an implementation
- point of view. The framework provides a solution
- to this technical challenge by providing a functorial
- data slot @{ML_functor Code_Data}; on instantiation
- of this functor, the following types and operations
- are required:
-
- \medskip
- \begin{tabular}{l}
- @{text "type T"} \\
- @{text "val empty: T"} \\
- @{text "val purge: theory \<rightarrow> string list option \<rightarrow> T \<rightarrow> T"}
- \end{tabular}
-
- \begin{description}
-
- \item @{text T} the type of data to store.
-
- \item @{text empty} initial (empty) data.
-
- \item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content;
- @{text consts} indicates the kind
- of change: @{ML NONE} stands for a fundamental change
- which invalidates any existing code, @{text "SOME consts"}
- hints that executable content for constants @{text consts}
- has changed.
-
- \end{description}
-
- \noindent An instance of @{ML_functor Code_Data} provides the following
- interface:
-
- \medskip
- \begin{tabular}{l}
- @{text "get: theory \<rightarrow> T"} \\
- @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
- @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
- \end{tabular}
-
- \begin{description}
-
- \item @{text get} retrieval of the current data.
-
- \item @{text change} update of current data (cached!)
- by giving a continuation.
-
- \item @{text change_yield} update with side result.
-
- \end{description}
-*}
-
-text {*
- \bigskip
-
- \emph{Happy proving, happy hacking!}
-*}
-
-end
--- a/doc-src/Codegen/Thy/Program.thy Fri Aug 13 13:43:55 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,432 +0,0 @@
-theory Program
-imports Introduction
-begin
-
-section {* Turning Theories into Programs \label{sec:program} *}
-
-subsection {* The @{text "Isabelle/HOL"} default setup *}
-
-text {*
- We have already seen how by default equations stemming from
- @{command definition}, @{command primrec} and @{command fun}
- statements are used for code generation. This default behaviour
- can be changed, e.g.\ by providing different code equations.
- The customisations shown in this section are \emph{safe}
- as regards correctness: all programs that can be generated are partially
- correct.
-*}
-
-subsection {* Selecting code equations *}
-
-text {*
- Coming back to our introductory example, we
- could provide an alternative code equations for @{const dequeue}
- explicitly:
-*}
-
-lemma %quote [code]:
- "dequeue (AQueue xs []) =
- (if xs = [] then (None, AQueue [] [])
- else dequeue (AQueue [] (rev xs)))"
- "dequeue (AQueue xs (y # ys)) =
- (Some y, AQueue xs ys)"
- by (cases xs, simp_all) (cases "rev xs", simp_all)
-
-text {*
- \noindent The annotation @{text "[code]"} is an @{text Isar}
- @{text attribute} which states that the given theorems should be
- considered as code equations for a @{text fun} statement --
- the corresponding constant is determined syntactically. The resulting code:
-*}
-
-text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
-
-text {*
- \noindent You may note that the equality test @{term "xs = []"} has been
- replaced by the predicate @{term "null xs"}. This is due to the default
- setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
-
- Changing the default constructor set of datatypes is also
- possible. See \secref{sec:datatypes} for an example.
-
- As told in \secref{sec:concept}, code generation is based
- on a structured collection of code theorems.
- This collection
- may be inspected using the @{command code_thms} command:
-*}
-
-code_thms %quote dequeue
-
-text {*
- \noindent prints a table with \emph{all} code equations
- for @{const dequeue}, including
- \emph{all} code equations those equations depend
- on recursively.
-
- Similarly, the @{command code_deps} command shows a graph
- visualising dependencies between code equations.
-*}
-
-subsection {* @{text class} and @{text instantiation} *}
-
-text {*
- Concerning type classes and code generation, let us examine an example
- from abstract algebra:
-*}
-
-class %quote semigroup =
- fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
- assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
-
-class %quote monoid = semigroup +
- fixes neutral :: 'a ("\<one>")
- assumes neutl: "\<one> \<otimes> x = x"
- and neutr: "x \<otimes> \<one> = x"
-
-instantiation %quote nat :: monoid
-begin
-
-primrec %quote mult_nat where
- "0 \<otimes> n = (0\<Colon>nat)"
- | "Suc m \<otimes> n = n + m \<otimes> n"
-
-definition %quote neutral_nat where
- "\<one> = Suc 0"
-
-lemma %quote add_mult_distrib:
- fixes n m q :: nat
- shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
- by (induct n) simp_all
-
-instance %quote proof
- fix m n q :: nat
- show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
- by (induct m) (simp_all add: add_mult_distrib)
- show "\<one> \<otimes> n = n"
- by (simp add: neutral_nat_def)
- show "m \<otimes> \<one> = m"
- by (induct m) (simp_all add: neutral_nat_def)
-qed
-
-end %quote
-
-text {*
- \noindent We define the natural operation of the natural numbers
- on monoids:
-*}
-
-primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
- "pow 0 a = \<one>"
- | "pow (Suc n) a = a \<otimes> pow n a"
-
-text {*
- \noindent This we use to define the discrete exponentiation function:
-*}
-
-definition %quote bexp :: "nat \<Rightarrow> nat" where
- "bexp n = pow n (Suc (Suc 0))"
-
-text {*
- \noindent The corresponding code in Haskell uses that language's native classes:
-*}
-
-text %quote {*@{code_stmts bexp (Haskell)}*}
-
-text {*
- \noindent This is a convenient place to show how explicit dictionary construction
- manifests in generated code (here, the same example in @{text SML})
- \cite{Haftmann-Nipkow:2010:code}:
-*}
-
-text %quote {*@{code_stmts bexp (SML)}*}
-
-text {*
- \noindent Note the parameters with trailing underscore (@{verbatim "A_"}),
- which are the dictionary parameters.
-*}
-
-subsection {* The preprocessor \label{sec:preproc} *}
-
-text {*
- Before selected function theorems are turned into abstract
- code, a chain of definitional transformation steps is carried
- out: \emph{preprocessing}. In essence, the preprocessor
- consists of two components: a \emph{simpset} and \emph{function transformers}.
-
- The \emph{simpset} can apply the full generality of the
- Isabelle simplifier. Due to the interpretation of theorems as code
- 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. An important special case are
- \emph{unfold theorems}, which may be declared and removed using
- the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
- attribute, respectively.
-
- Some common applications:
-*}
-
-text_raw {*
- \begin{itemize}
-*}
-
-text {*
- \item replacing non-executable constructs by executable ones:
-*}
-
-lemma %quote [code_unfold]:
- "x \<in> set xs \<longleftrightarrow> List.member xs x" by (fact in_set_member)
-
-text {*
- \item eliminating superfluous constants:
-*}
-
-lemma %quote [code_unfold]:
- "1 = Suc 0" by (fact One_nat_def)
-
-text {*
- \item replacing executable but inconvenient constructs:
-*}
-
-lemma %quote [code_unfold]:
- "xs = [] \<longleftrightarrow> List.null xs" by (fact eq_Nil_null)
-
-text_raw {*
- \end{itemize}
-*}
-
-text {*
- \noindent \emph{Function transformers} provide a very 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 @{term "0\<Colon>nat"} / @{const Suc}
- pattern elimination implemented in
- theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this
- interface.
-
- \noindent The current setup of the preprocessor may be inspected using
- the @{command print_codeproc} command.
- @{command code_thms} provides a convenient
- mechanism to inspect the impact of a preprocessor setup
- on code equations.
-
- \begin{warn}
-
- Attribute @{attribute code_unfold} also applies to the
- preprocessor of the ancient @{text "SML code generator"}; in case
- this is not what you intend, use @{attribute code_inline} instead.
- \end{warn}
-*}
-
-subsection {* Datatypes \label{sec:datatypes} *}
-
-text {*
- Conceptually, any datatype is spanned by a set of
- \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
- "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
- @{text "\<tau>"}. The HOL datatype package by default registers any new
- datatype in the table of datatypes, which may be inspected using the
- @{command print_codesetup} command.
-
- In some cases, it is appropriate to alter or extend this table. As
- an example, we will develop an alternative representation of the
- queue example given in \secref{sec:intro}. The amortised
- representation is convenient for generating code but exposes its
- \qt{implementation} details, which may be cumbersome when proving
- theorems about it. Therefore, here is a simple, straightforward
- representation of queues:
-*}
-
-datatype %quote 'a queue = Queue "'a list"
-
-definition %quote empty :: "'a queue" where
- "empty = Queue []"
-
-primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
- "enqueue x (Queue xs) = Queue (xs @ [x])"
-
-fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
- "dequeue (Queue []) = (None, Queue [])"
- | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
-
-text {*
- \noindent This we can use directly for proving; for executing,
- we provide an alternative characterisation:
-*}
-
-definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
- "AQueue xs ys = Queue (ys @ rev xs)"
-
-code_datatype %quote AQueue
-
-text {*
- \noindent Here we define a \qt{constructor} @{const "AQueue"} which
- is defined in terms of @{text "Queue"} and interprets its arguments
- according to what the \emph{content} of an amortised queue is supposed
- to be. Equipped with this, we are able to prove the following equations
- for our primitive queue operations which \qt{implement} the simple
- queues in an amortised fashion:
-*}
-
-lemma %quote empty_AQueue [code]:
- "empty = AQueue [] []"
- unfolding AQueue_def empty_def by simp
-
-lemma %quote enqueue_AQueue [code]:
- "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
- unfolding AQueue_def by simp
-
-lemma %quote dequeue_AQueue [code]:
- "dequeue (AQueue xs []) =
- (if xs = [] then (None, AQueue [] [])
- else dequeue (AQueue [] (rev xs)))"
- "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
- unfolding AQueue_def by simp_all
-
-text {*
- \noindent For completeness, we provide a substitute for the
- @{text case} combinator on queues:
-*}
-
-lemma %quote queue_case_AQueue [code]:
- "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
- unfolding AQueue_def by simp
-
-text {*
- \noindent The resulting code looks as expected:
-*}
-
-text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
-
-text {*
- \noindent From this example, it can be glimpsed that using own
- constructor sets is a little delicate since it changes the set of
- valid patterns for values of that type. Without going into much
- detail, here some practical hints:
-
- \begin{itemize}
-
- \item When changing the constructor set for datatypes, take care
- to provide alternative equations for the @{text case} combinator.
-
- \item Values in the target language need not to be normalised --
- different values in the target language may represent the same
- value in the logic.
-
- \item Usually, a good methodology to deal with the subtleties of
- pattern matching is to see the type as an abstract type: provide
- a set of operations which operate on the concrete representation
- of the type, and derive further operations by combinations of
- these primitive ones, without relying on a particular
- representation.
-
- \end{itemize}
-*}
-
-
-subsection {* Equality *}
-
-text {*
- Surely you have already noticed how equality is treated
- by the code generator:
-*}
-
-primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "collect_duplicates xs ys [] = xs"
- | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
- then if z \<in> set ys
- then collect_duplicates xs ys zs
- else collect_duplicates xs (z#ys) zs
- else collect_duplicates (z#xs) (z#ys) zs)"
-
-text {*
- \noindent During preprocessing, the membership test is rewritten,
- resulting in @{const List.member}, which itself
- performs an explicit equality check.
-*}
-
-text %quote {*@{code_stmts collect_duplicates (SML)}*}
-
-text {*
- \noindent Obviously, polymorphic equality is implemented the Haskell
- way using a type class. How is this achieved? HOL introduces
- an explicit class @{class eq} with a corresponding operation
- @{const eq_class.eq} such that @{thm eq [no_vars]}.
- The preprocessing framework does the rest by propagating the
- @{class eq} constraints through all dependent code equations.
- For datatypes, instances of @{class eq} are implicitly derived
- when possible. For other types, you may instantiate @{text eq}
- manually like any other type class.
-*}
-
-
-subsection {* Explicit partiality *}
-
-text {*
- Partiality usually enters the game by partial patterns, as
- in the following example, again for amortised queues:
-*}
-
-definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
- "strict_dequeue q = (case dequeue q
- of (Some x, q') \<Rightarrow> (x, q'))"
-
-lemma %quote strict_dequeue_AQueue [code]:
- "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
- "strict_dequeue (AQueue xs []) =
- (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
- by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits)
-
-text {*
- \noindent In the corresponding code, there is no equation
- for the pattern @{term "AQueue [] []"}:
-*}
-
-text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
-
-text {*
- \noindent In some cases it is desirable to have this
- pseudo-\qt{partiality} more explicitly, e.g.~as follows:
-*}
-
-axiomatization %quote empty_queue :: 'a
-
-definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
- "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"
-
-lemma %quote strict_dequeue'_AQueue [code]:
- "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue
- else strict_dequeue' (AQueue [] (rev xs)))"
- "strict_dequeue' (AQueue xs (y # ys)) =
- (y, AQueue xs ys)"
- by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits)
-
-text {*
- Observe that on the right hand side of the definition of @{const
- "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
-
- Normally, if constants without any code equations occur in a
- program, the code generator complains (since in most cases this is
- indeed an error). But such constants can also be thought
- of as function definitions which always fail,
- since there is never a successful pattern match on the left hand
- side. In order to categorise a constant into that category
- explicitly, use @{command "code_abort"}:
-*}
-
-code_abort %quote empty_queue
-
-text {*
- \noindent Then the code generator will just insert an error or
- exception at the appropriate position:
-*}
-
-text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
-
-text {*
- \noindent This feature however is rarely needed in practice.
- Note also that the @{text HOL} default setup already declares
- @{const undefined} as @{command "code_abort"}, which is most
- likely to be used in such situations.
-*}
-
-end
--- a/doc-src/Codegen/Thy/ROOT.ML Fri Aug 13 13:43:55 2010 +0200
+++ b/doc-src/Codegen/Thy/ROOT.ML Fri Aug 13 14:40:15 2010 +0200
@@ -1,10 +1,9 @@
no_document use_thy "Setup";
-no_document use_thys ["Efficient_Nat"];
use_thy "Introduction";
-use_thy "Program";
+use_thy "Foundations";
+use_thy "Refinement";
use_thy "Inductive_Predicate";
use_thy "Adaptation";
use_thy "Further";
-use_thy "ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/Refinement.thy Fri Aug 13 14:40:15 2010 +0200
@@ -0,0 +1,7 @@
+theory Refinement
+imports Setup
+begin
+
+section {* Program and datatype refinement \label{sec:refinement} *}
+
+end
--- a/doc-src/Codegen/Thy/document/Further.tex Fri Aug 13 13:43:55 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Fri Aug 13 14:40:15 2010 +0200
@@ -389,6 +389,179 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{ML system interfaces \label{sec:ml}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Since the code generator framework not only aims to provide
+ a nice Isar interface but also to form a base for
+ code-generation-based applications, here a short
+ description of the most important ML interfaces.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Managing executable content%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
+ \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
+ \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
+ \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
+ \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
+\verb| -> theory -> theory| \\
+ \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
+ \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
+ \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
+\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\
+ \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
+ theorem \isa{thm} to executable content.
+
+ \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
+ theorem \isa{thm} from executable content, if present.
+
+ \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
+ the preprocessor simpset.
+
+ \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
+ function transformer \isa{f} (named \isa{name}) to executable content;
+ \isa{f} is a transformer of the code equations belonging
+ to a certain function definition, depending on the
+ current theory context. Returning \isa{NONE} indicates that no
+ transformation took place; otherwise, the whole process will be iterated
+ with the new code equations.
+
+ \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes
+ function transformer named \isa{name} from executable content.
+
+ \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
+ a datatype to executable content, with generation
+ set \isa{cs}.
+
+ \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const}
+ returns type constructor corresponding to
+ constructor \isa{const}; returns \isa{NONE}
+ if \isa{const} is no constructor.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsubsection{Auxiliary%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Code.read_const|~\isa{thy}~\isa{s}
+ reads a constant as a concrete term expression \isa{s}.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsubsection{Data depending on the theory's executable content%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Implementing code generator applications on top
+ of the framework set out so far usually not only
+ involves using those primitive interfaces
+ but also storing code-dependent data and various
+ other things.
+
+ Due to incrementality of code generation, changes in the
+ theory's executable content have to be propagated in a
+ certain fashion. Additionally, such changes may occur
+ not only during theory extension but also during theory
+ merge, which is a little bit nasty from an implementation
+ point of view. The framework provides a solution
+ to this technical challenge by providing a functorial
+ data slot \verb|Code_Data|; on instantiation
+ of this functor, the following types and operations
+ are required:
+
+ \medskip
+ \begin{tabular}{l}
+ \isa{type\ T} \\
+ \isa{val\ empty{\isacharcolon}\ T} \\
+ \end{tabular}
+
+ \begin{description}
+
+ \item \isa{T} the type of data to store.
+
+ \item \isa{empty} initial (empty) data.
+
+ \end{description}
+
+ \noindent An instance of \verb|Code_Data| provides the following
+ interface:
+
+ \medskip
+ \begin{tabular}{l}
+ \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
+ \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
+ \end{tabular}
+
+ \begin{description}
+
+ \item \isa{change} update of current data (cached!)
+ by giving a continuation.
+
+ \item \isa{change{\isacharunderscore}yield} update with side result.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\bigskip
+
+ \emph{Happy proving, happy hacking!}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Fri Aug 13 13:43:55 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Fri Aug 13 14:40:15 2010 +0200
@@ -18,7 +18,7 @@
%
\endisadelimtheory
%
-\isamarkupsubsection{Inductive Predicates%
+\isamarkupsection{Inductive Predicates%
}
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Fri Aug 13 13:43:55 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Fri Aug 13 14:40:15 2010 +0200
@@ -18,7 +18,27 @@
%
\endisadelimtheory
%
-\isamarkupsection{Introduction and Overview%
+\isamarkupsection{Introduction%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Code generation fundamental: shallow embedding%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{A quick start with the \isa{Isabelle{\isacharslash}HOL} toolbox%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Type classes%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{How to continue from here%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{If something goes utterly wrong%
}
\isamarkuptrue%
%
--- a/doc-src/Codegen/codegen.tex Fri Aug 13 13:43:55 2010 +0200
+++ b/doc-src/Codegen/codegen.tex Fri Aug 13 14:40:15 2010 +0200
@@ -31,11 +31,11 @@
\clearfirst
\input{Thy/document/Introduction.tex}
-\input{Thy/document/Program.tex}
+\input{Thy/document/Foundations.tex}
+\input{Thy/document/Refinement.tex}
\input{Thy/document/Inductive_Predicate.tex}
\input{Thy/document/Adaptation.tex}
\input{Thy/document/Further.tex}
-\input{Thy/document/ML.tex}
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing