--- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Tue Feb 03 19:37:00 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Tue Feb 03 19:37:16 2009 +0100
@@ -48,7 +48,7 @@
setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
Changing the default constructor set of datatypes is also
- possible but rarely desired in practice. See \secref{sec:datatypes} for an example.
+ 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.
@@ -75,7 +75,7 @@
from abstract algebra:
*}
-class %quote semigroup = type +
+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)"
@@ -221,97 +221,99 @@
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.
+ \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 may be convenient to alter or
- extend this table; as an example, we will develop an alternative
- representation of natural numbers as binary digits, whose
- size does increase logarithmically with its value, not linear
- \footnote{Indeed, the @{theory Efficient_Nat} theory (see \ref{eff_nat})
- does something similar}. First, the digit representation:
+ 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 a simple, straightforward
+ representation of queues:
*}
-definition %quote Dig0 :: "nat \<Rightarrow> nat" where
- "Dig0 n = 2 * n"
+datatype %quote 'a queue = Queue "'a list"
+
+definition %quote empty :: "'a queue" where
+ "empty = Queue []"
-definition %quote Dig1 :: "nat \<Rightarrow> nat" where
- "Dig1 n = Suc (2 * n)"
+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 We will use these two \qt{digits} to represent natural numbers
- in binary digits, e.g.:
-*}
-
-lemma %quote 42: "42 = Dig0 (Dig1 (Dig0 (Dig1 (Dig0 1))))"
- by (simp add: Dig0_def Dig1_def)
-
-text {*
- \noindent Of course we also have to provide proper code equations for
- the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
+ \noindent This we can use directly for proving; for executing,
+ we provide an alternative characterisation:
*}
-lemma %quote plus_Dig [code]:
- "0 + n = n"
- "m + 0 = m"
- "1 + Dig0 n = Dig1 n"
- "Dig0 m + 1 = Dig1 m"
- "1 + Dig1 n = Dig0 (n + 1)"
- "Dig1 m + 1 = Dig0 (m + 1)"
- "Dig0 m + Dig0 n = Dig0 (m + n)"
- "Dig0 m + Dig1 n = Dig1 (m + n)"
- "Dig1 m + Dig0 n = Dig1 (m + n)"
- "Dig1 m + Dig1 n = Dig0 (m + n + 1)"
- by (simp_all add: Dig0_def Dig1_def)
+definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
+ "AQueue xs ys = Queue (ys @ rev xs)"
+
+code_datatype %quote AQueue
+
+text {* *}
+
+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
-text {*
- \noindent We then instruct the code generator to view @{term "0\<Colon>nat"},
- @{term "1\<Colon>nat"}, @{term Dig0} and @{term Dig1} as
- datatype constructors:
-*}
+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 {* *}
+
+definition %quote aqueue_case [code inline]:
+ "aqueue_case = queue_case"
-code_datatype %quote "0\<Colon>nat" "1\<Colon>nat" Dig0 Dig1
+lemma %quote case_AQueue1 [code]:
+ "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
+ unfolding AQueue_def by simp
+
+lemma %quote case_AQueue2 [code]:
+ "aqueue_case f (AQueue xs ys) = f (ys @ rev xs)"
+ unfolding aqueue_case case_AQueue1 ..
+
+text {* *}
+
+text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
text {*
- \noindent For the former constructor @{term Suc}, we provide a code
- equation and remove some parts of the default code generator setup
- which are an obstacle here:
-*}
-
-lemma %quote Suc_Dig [code]:
- "Suc n = n + 1"
- by simp
-
-declare %quote One_nat_def [code inline del]
-declare %quote add_Suc_shift [code del]
-
-text {*
- \noindent This yields the following code:
-*}
-
-text %quote {*@{code_stmts "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" (SML)}*}
-
-text {*
- \noindent From this example, it can be easily 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:
+ \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 an alternative for the @{text case} combinator (e.g.~by replacing
- it using the preprocessor).
- \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 (e.g. @{term "Dig1 0 = 1"}).
- \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.
+
+ \item When changing the constructor set for datatypes, take care
+ to provide an alternative for the @{text case} combinator
+ (e.g.~by replacing it using the preprocessor).
+
+ \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}
*}
--- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Tue Feb 03 19:37:00 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Tue Feb 03 19:37:16 2009 +0100
@@ -5,7 +5,7 @@
ML {* no_document use_thys
["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL",
- "~~/src/HOL/ex/ReflectedFerrack"] *}
+ "~~/src/HOL/Reflection/Ferrack"] *}
ML_val {* Code_Target.code_width := 74 *}
--- a/src/Tools/code/code_haskell.ML Tue Feb 03 19:37:00 2009 +0100
+++ b/src/Tools/code/code_haskell.ML Tue Feb 03 19:37:16 2009 +0100
@@ -385,7 +385,7 @@
val imports = deps'
|> map NameSpace.qualifier
|> distinct (op =);
- fun pr_import_include (name, _) = str ("import " ^ name ^ ";");
+ fun pr_import_include (name, _) = str ("import qualified " ^ name ^ ";");
val pr_import_module = str o (if qualified
then prefix "import qualified "
else prefix "import ") o suffix ";";