# HG changeset patch
# User haftmann
# Date 1282041031 -7200
# Node ID 4c065e97ecee6cb6aafe1f492878adcd6f90e3b6
# Parent  ada5814c9d874ca678eef47101503f6ad97ef719
added section on program refinement

diff -r ada5814c9d87 -r 4c065e97ecee doc-src/Codegen/Thy/Refinement.thy
--- a/doc-src/Codegen/Thy/Refinement.thy	Tue Aug 17 12:30:30 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy	Tue Aug 17 12:30:31 2010 +0200
@@ -4,6 +4,72 @@
 
 section {* Program and datatype refinement \label{sec:refinement} *}
 
+text {*
+  Code generation by shallow embedding (cf.~\secref{sec:principle})
+  allows to choose code equations and datatype constructors freely,
+  given that some very basic syntactic properties are met; this
+  flexibility opens up mechanisms for refinement which allow to extend
+  the scope and quality of generated code dramatically.
+*}
+
+
+subsection {* Program refinement *}
+
+text {*
+  Program refinement works by choosing appropriate code equations
+  explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci
+  numbers:
+*}
+
+fun %quote fib :: "nat \<Rightarrow> nat" where
+    "fib 0 = 0"
+  | "fib (Suc 0) = Suc 0"
+  | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
+
+text {*
+  \noindent The runtime of the corresponding code grows exponential due
+  to two recursive calls:
+*}
+
+text %quote {*@{code_stmts fib (consts) fib (Haskell)}*}
+
+text {*
+  \noindent A more efficient implementation would use dynamic
+  programming, e.g.~sharing of common intermediate results between
+  recursive calls.  This idea is expressed by an auxiliary operation
+  which computes a Fibonacci number and its successor simultaneously:
+*}
+
+definition %quote fib_step :: "nat \<Rightarrow> nat \<times> nat" where
+  "fib_step n = (fib (Suc n), fib n)"
+
+text {*
+  \noindent This operation can be implemented by recursion using
+  dynamic programming:
+*}
+
+lemma %quote [code]:
+  "fib_step 0 = (Suc 0, 0)"
+  "fib_step (Suc n) = (let (m, q) = fib_step n in (m + q, m))"
+  by (simp_all add: fib_step_def)
+
+text {*
+  \noindent What remains is to implement @{const fib} by @{const
+  fib_step} as follows:
+*}
+
+lemma %quote [code]:
+  "fib 0 = 0"
+  "fib (Suc n) = fst (fib_step n)"
+  by (simp_all add: fib_step_def)
+
+text {*
+  \noindent The resulting code shows only linear growth of runtime:
+*}
+
+text %quote {*@{code_stmts fib (consts) fib fib_step (Haskell)}*}
+
+
 subsection {* Datatypes \label{sec:datatypes} *}
 
 text {*
diff -r ada5814c9d87 -r 4c065e97ecee doc-src/Codegen/Thy/document/Refinement.tex
--- a/doc-src/Codegen/Thy/document/Refinement.tex	Tue Aug 17 12:30:30 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex	Tue Aug 17 12:30:31 2010 +0200
@@ -22,6 +22,175 @@
 }
 \isamarkuptrue%
 %
+\begin{isamarkuptext}%
+Code generation by shallow embedding (cf.~\secref{sec:principle})
+  allows to choose code equations and datatype constructors freely,
+  given that some very basic syntactic properties are met; this
+  flexibility opens up mechanisms for refinement which allow to extend
+  the scope and quality of generated code dramatically.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Program refinement%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Program refinement works by choosing appropriate code equations
+  explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci
+  numbers:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{fun}\isamarkupfalse%
+\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The runtime of the corresponding code grows exponential due
+  to two recursive calls:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}fib ::~Nat -> Nat;\\
+\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\
+\hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\
+\hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent A more efficient implementation would use dynamic
+  programming, e.g.~sharing of common intermediate results between
+  recursive calls.  This idea is expressed by an auxiliary operation
+  which computes a Fibonacci number and its successor simultaneously:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymtimes}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}fib{\isacharunderscore}step\ n\ {\isacharequal}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharcomma}\ fib\ n{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This operation can be implemented by recursion using
+  dynamic programming:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}fib{\isacharunderscore}step\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}fib{\isacharunderscore}step\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}let\ {\isacharparenleft}m{\isacharcomma}\ q{\isacharparenright}\ {\isacharequal}\ fib{\isacharunderscore}step\ n\ in\ {\isacharparenleft}m\ {\isacharplus}\ q{\isacharcomma}\ m{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ fib{\isacharunderscore}step{\isacharunderscore}def{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent What remains is to implement \isa{fib} by \isa{fib{\isacharunderscore}step} as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fst\ {\isacharparenleft}fib{\isacharunderscore}step\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ fib{\isacharunderscore}step{\isacharunderscore}def{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The resulting code shows only linear growth of runtime:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\
+\hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\
+\hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\
+\hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\
+\hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\
+\hspace*{0pt}\\
+\hspace*{0pt}fib ::~Nat -> Nat;\\
+\hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\
+\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
 \isamarkupsubsection{Datatypes \label{sec:datatypes}%
 }
 \isamarkuptrue%