--- a/doc-src/Codegen/Thy/Refinement.thy Fri Aug 13 16:40:47 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy Mon Aug 16 10:32:14 2010 +0200
@@ -4,4 +4,109 @@
section {* Program and datatype refinement \label{sec:refinement} *}
+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:queue_example}. 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}
+*}
+
end