--- a/NEWS Wed Feb 04 11:31:05 2009 +0000
+++ b/NEWS Wed Feb 04 11:32:35 2009 +0000
@@ -193,6 +193,9 @@
*** HOL ***
+* Auxiliary class "itself" has disappeared -- classes without any parameter
+are treated as expected by the 'class' command.
+
* Theory "Reflection" now resides in HOL/Library. Common reflection examples
(Cooper, MIR, Ferrack) now in distinct session directory HOL/Reflection.
--- a/doc-src/IsarAdvanced/Codegen/Thy/Further.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Further.thy Wed Feb 04 11:32:35 2009 +0000
@@ -96,7 +96,7 @@
allows to use pattern matching on constructors stemming from compiled
@{text datatypes}.
- For a less simplistic example, theory @{theory ReflectedFerrack} is
+ For a less simplistic example, theory @{theory Ferrack} is
a good reference.
*}
--- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Wed Feb 04 11:32:35 2009 +0000
@@ -65,19 +65,19 @@
For example, here a simple \qt{implementation} of amortised queues:
*}
-datatype %quote 'a queue = Queue "'a list" "'a list"
+datatype %quote 'a queue = AQueue "'a list" "'a list"
definition %quote empty :: "'a queue" where
- "empty = Queue [] []"
+ "empty = AQueue [] []"
primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
- "enqueue x (Queue xs ys) = Queue (x # xs) ys"
+ "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
- "dequeue (Queue [] []) = (None, Queue [] [])"
- | "dequeue (Queue xs (y # ys)) = (Some y, Queue xs ys)"
- | "dequeue (Queue xs []) =
- (case rev xs of y # ys \<Rightarrow> (Some y, Queue [] ys))"
+ "dequeue (AQueue [] []) = (None, AQueue [] [])"
+ | "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
+ | "dequeue (AQueue xs []) =
+ (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))"
text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *}
--- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Wed Feb 04 11:32:35 2009 +0000
@@ -26,11 +26,11 @@
*}
lemma %quote [code]:
- "dequeue (Queue xs []) =
- (if xs = [] then (None, Queue [] [])
- else dequeue (Queue [] (rev xs)))"
- "dequeue (Queue xs (y # ys)) =
- (Some y, Queue xs ys)"
+ "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 {*
@@ -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,106 +221,115 @@
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 {*
- \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:
+ \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:
*}
-code_datatype %quote "0\<Colon>nat" "1\<Colon>nat" Dig0 Dig1
+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 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:
+ \noindent For completeness, we provide a substitute for the
+ @{text case} combinator on queues:
*}
-text %quote {*@{code_stmts "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" (SML)}*}
+definition %quote
+ aqueue_case_def: "aqueue_case = queue_case"
+
+lemma %quote aqueue_case [code, code inline]:
+ "queue_case = aqueue_case"
+ unfolding aqueue_case_def ..
+
+lemma %quote case_AQueue [code]:
+ "aqueue_case f (AQueue xs ys) = f (ys @ rev xs)"
+ unfolding aqueue_case_def AQueue_def by simp
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 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 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}
*}
-code_datatype %invisible "0::nat" Suc
-declare %invisible plus_Dig [code del]
-declare %invisible One_nat_def [code inline]
-declare %invisible add_Suc_shift [code]
-lemma %invisible [code]: "0 + n = (n \<Colon> nat)" by simp
-
subsection {* Equality and wellsortedness *}
@@ -457,14 +466,19 @@
in the following example, again for amortised queues:
*}
-fun %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
- "strict_dequeue (Queue xs (y # ys)) = (y, Queue xs ys)"
- | "strict_dequeue (Queue xs []) =
- (case rev xs of y # ys \<Rightarrow> (y, Queue [] ys))"
+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 "Queue [] []"}:
+ for the pattern @{term "AQueue [] []"}:
*}
text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
@@ -476,30 +490,28 @@
axiomatization %quote empty_queue :: 'a
-function %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
- "strict_dequeue' (Queue xs []) = (if xs = [] then empty_queue
- else strict_dequeue' (Queue [] (rev xs)))"
- | "strict_dequeue' (Queue xs (y # ys)) =
- (y, Queue xs ys)"
-by pat_completeness auto
+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)"
-termination %quote strict_dequeue'
-by (relation "measure (\<lambda>q::'a queue. case q of Queue xs ys \<Rightarrow> length xs)") simp_all
+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 {*
- \noindent For technical reasons the definition of
- @{const strict_dequeue'} is more involved since it requires
- a manual termination proof. Apart from that observe that
- on the right hand side of its first equation the constant
- @{const empty_queue} occurs which is unspecified.
+ Observe that on the right hand side of the definition of @{const
+ "strict_dequeue'"} the constant @{const empty_queue} occurs
+ which is unspecified.
- Normally, if constants without any code equations occur in
- a program, the code generator complains (since in most cases
- this is not what the user expects). But such constants can also
- be thought of as function definitions with no equations 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"}:
+ Normally, if constants without any code equations occur in a
+ program, the code generator complains (since in most cases this is
+ not what the user expects). But such constants can also be thought
+ of as function definitions with no equations 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
--- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Wed Feb 04 11:32:35 2009 +0000
@@ -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/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex Wed Feb 04 11:32:35 2009 +0000
@@ -195,7 +195,7 @@
allows to use pattern matching on constructors stemming from compiled
\isa{datatypes}.
- For a less simplistic example, theory \hyperlink{theory.ReflectedFerrack}{\mbox{\isa{ReflectedFerrack}}} is
+ For a less simplistic example, theory \hyperlink{theory.Ferrack}{\mbox{\isa{Ferrack}}} is
a good reference.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex Wed Feb 04 11:32:35 2009 +0000
@@ -94,22 +94,22 @@
%
\isatagquote
\isacommand{datatype}\isamarkupfalse%
-\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
+\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{primrec}\isamarkupfalse%
\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{fun}\isamarkupfalse%
\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
@@ -162,20 +162,20 @@
\hspace*{0pt}fun list{\char95}case f1 f2 (a ::~lista) = f2 a lista\\
\hspace*{0pt} ~| list{\char95}case f1 f2 [] = f1;\\
\hspace*{0pt}\\
-\hspace*{0pt}datatype 'a queue = Queue of 'a list * 'a list;\\
+\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = Queue ([],~[])\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\
\hspace*{0pt}\\
-\hspace*{0pt}fun dequeue (Queue ([],~[])) = (NONE,~Queue ([],~[]))\\
-\hspace*{0pt} ~| dequeue (Queue (xs,~y ::~ys)) = (SOME y,~Queue (xs,~ys))\\
-\hspace*{0pt} ~| dequeue (Queue (v ::~va,~[])) =\\
+\hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\
+\hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
+\hspace*{0pt} ~| dequeue (AQueue (v ::~va,~[])) =\\
\hspace*{0pt} ~~~let\\
\hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\
\hspace*{0pt} ~~~in\\
-\hspace*{0pt} ~~~~~(SOME y,~Queue ([],~ys))\\
+\hspace*{0pt} ~~~~~(SOME y,~AQueue ([],~ys))\\
\hspace*{0pt} ~~~end;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun enqueue x (Queue (xs,~ys)) = Queue (x ::~xs,~ys);\\
+\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -244,21 +244,21 @@
\hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\
\hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\
\hspace*{0pt}\\
-\hspace*{0pt}data Queue a = Queue [a] [a];\\
+\hspace*{0pt}data Queue a = AQueue [a] [a];\\
\hspace*{0pt}\\
\hspace*{0pt}empty ::~forall a.~Queue a;\\
-\hspace*{0pt}empty = Queue [] [];\\
+\hspace*{0pt}empty = AQueue [] [];\\
\hspace*{0pt}\\
\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue (Queue [] []) = (Nothing,~Queue [] []);\\
-\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y,~Queue xs ys);\\
-\hspace*{0pt}dequeue (Queue (v :~va) []) =\\
+\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
+\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
\hspace*{0pt} ~let {\char123}\\
\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
-\hspace*{0pt} ~{\char125}~in (Just y,~Queue [] ys);\\
+\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
\hspace*{0pt}\\
\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
-\hspace*{0pt}enqueue x (Queue xs ys) = Queue (x :~xs) ys;\\
+\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
\hspace*{0pt}\\
\hspace*{0pt}{\char125}%
\end{isamarkuptext}%
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Wed Feb 04 11:32:35 2009 +0000
@@ -56,11 +56,11 @@
\isatagquote
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
\endisatagquote
@@ -88,10 +88,10 @@
\isatypewriter%
\noindent%
\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y,~Queue xs ys);\\
-\hspace*{0pt}dequeue (Queue xs []) =\\
-\hspace*{0pt} ~(if nulla xs then (Nothing,~Queue [] [])\\
-\hspace*{0pt} ~~~else dequeue (Queue [] (rev xs)));%
+\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\
+\hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -108,7 +108,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.
@@ -158,7 +158,7 @@
%
\isatagquote
\isacommand{class}\isamarkupfalse%
-\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
+\ semigroup\ {\isacharequal}\isanewline
\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
@@ -506,19 +506,51 @@
%
\begin{isamarkuptext}%
Conceptually, any datatype is spanned by a set of
- \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n}
- where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all}
- type variables in \isa{{\isasymtau}}. The HOL datatype package
- by default registers any new datatype in the table
- of datatypes, which may be inspected using
- the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
+ \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in
+ \isa{{\isasymtau}}. The HOL datatype package by default registers any new
+ datatype in the table of datatypes, which may be inspected using the
+ \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}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 \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}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:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{datatype}\isamarkupfalse%
+\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{primrec}\isamarkupfalse%
+\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{fun}\isamarkupfalse%
+\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This we can use directly for proving; for executing,
+ we provide an alternative characterisation:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -528,12 +560,11 @@
%
\isatagquote
\isacommand{definition}\isamarkupfalse%
-\ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline
+\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ \ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}%
+\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
+\ AQueue%
\endisatagquote
{\isafoldquote}%
%
@@ -542,30 +573,12 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent We will use these two \qt{digits} to represent natural numbers
- in binary digits, e.g.:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isadigit{4}}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Of course we also have to provide proper code equations for
- the operations, e.g. \isa{op\ {\isacharplus}}:%
+\noindent Here we define a \qt{constructor} \isa{Program{\isachardot}AQueue} which
+ is defined in terms of \isa{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:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -575,19 +588,28 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{1}}\ m{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
+\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp{\isacharunderscore}all%
\endisatagquote
{\isafoldquote}%
%
@@ -596,9 +618,8 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent We then instruct the code generator to view \isa{{\isadigit{0}}},
- \isa{{\isadigit{1}}}, \isa{Dig{\isadigit{0}}} and \isa{Dig{\isadigit{1}}} as
- datatype constructors:%
+\noindent For completeness, we provide a substitute for the
+ \isa{case} combinator on queues:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -607,8 +628,23 @@
\endisadelimquote
%
\isatagquote
-\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isadigit{0}}{\isasymColon}nat{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isasymColon}nat{\isachardoublequoteclose}\ Dig{\isadigit{0}}\ Dig{\isadigit{1}}%
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ aqueue{\isacharunderscore}case{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ {\isacharequal}\ queue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ aqueue{\isacharunderscore}case\ {\isacharbrackleft}code{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ {\isacharequal}\ aqueue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ aqueue{\isacharunderscore}case{\isacharunderscore}def\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ aqueue{\isacharunderscore}case{\isacharunderscore}def\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp%
\endisatagquote
{\isafoldquote}%
%
@@ -617,36 +653,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent For the former constructor \isa{Suc}, we provide a code
- equation and remove some parts of the default code generator setup
- which are an obstacle here:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isanewline
-\isacommand{declare}\isamarkupfalse%
-\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
-\isacommand{declare}\isamarkupfalse%
-\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ del{\isacharbrackright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This yields the following code:%
+\noindent The resulting code looks as expected:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -662,18 +669,24 @@
\hspace*{0pt}structure Example = \\
\hspace*{0pt}struct\\
\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Dig1 of nat | Dig0 of nat | One{\char95}nat | Zero{\char95}nat;\\
+\hspace*{0pt}fun foldl f a [] = a\\
+\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun null [] = true\\
+\hspace*{0pt} ~| null (x ::~xs) = false;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun plus{\char95}nat (Dig1 m) (Dig1 n) = Dig0 (plus{\char95}nat (plus{\char95}nat m n) One{\char95}nat)\\
-\hspace*{0pt} ~| plus{\char95}nat (Dig1 m) (Dig0 n) = Dig1 (plus{\char95}nat m n)\\
-\hspace*{0pt} ~| plus{\char95}nat (Dig0 m) (Dig1 n) = Dig1 (plus{\char95}nat m n)\\
-\hspace*{0pt} ~| plus{\char95}nat (Dig0 m) (Dig0 n) = Dig0 (plus{\char95}nat m n)\\
-\hspace*{0pt} ~| plus{\char95}nat (Dig1 m) One{\char95}nat = Dig0 (plus{\char95}nat m One{\char95}nat)\\
-\hspace*{0pt} ~| plus{\char95}nat One{\char95}nat (Dig1 n) = Dig0 (plus{\char95}nat n One{\char95}nat)\\
-\hspace*{0pt} ~| plus{\char95}nat (Dig0 m) One{\char95}nat = Dig1 m\\
-\hspace*{0pt} ~| plus{\char95}nat One{\char95}nat (Dig0 n) = Dig1 n\\
-\hspace*{0pt} ~| plus{\char95}nat m Zero{\char95}nat = m\\
-\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
+\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
+\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
+\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
+\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -687,49 +700,32 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\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 \isa{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. \isa{Dig{\isadigit{1}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{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 \isa{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}%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
-\isacommand{declare}\isamarkupfalse%
-\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ del{\isacharbrackright}\isanewline
-\isacommand{declare}\isamarkupfalse%
-\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
-\isacommand{declare}\isamarkupfalse%
-\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code{\isacharbrackright}\ \isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ simp%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
\isamarkupsubsection{Equality and wellsortedness%
}
\isamarkuptrue%
@@ -1081,11 +1077,18 @@
\endisadelimquote
%
\isatagquote
-\isacommand{fun}\isamarkupfalse%
+\isacommand{definition}\isamarkupfalse%
\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline
+\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
@@ -1095,7 +1098,7 @@
%
\begin{isamarkuptext}%
\noindent In the corresponding code, there is no equation
- for the pattern \isa{Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
+ for the pattern \isa{Program{\isachardot}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1109,11 +1112,11 @@
\isatypewriter%
\noindent%
\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y,~Queue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue (Queue xs []) =\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
\hspace*{0pt} ~let {\char123}\\
\hspace*{0pt} ~~~(y :~ys) = rev xs;\\
-\hspace*{0pt} ~{\char125}~in (y,~Queue [] ys);%
+\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1138,19 +1141,18 @@
\isacommand{axiomatization}\isamarkupfalse%
\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
\isanewline
-\isacommand{function}\isamarkupfalse%
+\isacommand{definition}\isamarkupfalse%
\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
-\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isacommand{by}\isamarkupfalse%
-\ pat{\isacharunderscore}completeness\ auto\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
-\isacommand{termination}\isamarkupfalse%
-\ strict{\isacharunderscore}dequeue{\isacharprime}\isanewline
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}q{\isacharcolon}{\isacharcolon}{\isacharprime}a\ queue{\isachardot}\ case\ q\ of\ Queue\ xs\ ys\ {\isasymRightarrow}\ length\ xs{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ simp{\isacharunderscore}all%
+\isacommand{lemma}\isamarkupfalse%
+\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
+\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
@@ -1159,19 +1161,16 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent For technical reasons the definition of
- \isa{strict{\isacharunderscore}dequeue{\isacharprime}} is more involved since it requires
- a manual termination proof. Apart from that observe that
- on the right hand side of its first equation the constant
- \isa{empty{\isacharunderscore}queue} occurs which is unspecified.
+Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}} the constant \isa{empty{\isacharunderscore}queue} occurs
+ which is unspecified.
- Normally, if constants without any code equations occur in
- a program, the code generator complains (since in most cases
- this is not what the user expects). But such constants can also
- be thought of as function definitions with no equations 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 \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
+ Normally, if constants without any code equations occur in a
+ program, the code generator complains (since in most cases this is
+ not what the user expects). But such constants can also be thought
+ of as function definitions with no equations 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 \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1208,9 +1207,10 @@
\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
\hspace*{0pt}\\
\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue' (Queue xs []) =\\
-\hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue' (Queue [] (rev xs)));\\
-\hspace*{0pt}strict{\char95}dequeue' (Queue xs (y :~ys)) = (y,~Queue xs ys);%
+\hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\
+\hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\
+\hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs Wed Feb 04 11:32:35 2009 +0000
@@ -14,20 +14,20 @@
list_case f1 f2 (a : list) = f2 a list;
list_case f1 f2 [] = f1;
-data Queue a = Queue [a] [a];
+data Queue a = AQueue [a] [a];
empty :: forall a. Queue a;
-empty = Queue [] [];
+empty = AQueue [] [];
dequeue :: forall a. Queue a -> (Maybe a, Queue a);
-dequeue (Queue [] []) = (Nothing, Queue [] []);
-dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);
-dequeue (Queue (v : va) []) =
+dequeue (AQueue [] []) = (Nothing, AQueue [] []);
+dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
+dequeue (AQueue (v : va) []) =
let {
(y : ys) = rev (v : va);
- } in (Just y, Queue [] ys);
+ } in (Just y, AQueue [] ys);
enqueue :: forall a. a -> Queue a -> Queue a;
-enqueue x (Queue xs ys) = Queue (x : xs) ys;
+enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
}
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML Wed Feb 04 11:32:35 2009 +0000
@@ -9,19 +9,19 @@
fun list_case f1 f2 (a :: lista) = f2 a lista
| list_case f1 f2 [] = f1;
-datatype 'a queue = Queue of 'a list * 'a list;
+datatype 'a queue = AQueue of 'a list * 'a list;
-val empty : 'a queue = Queue ([], [])
+val empty : 'a queue = AQueue ([], [])
-fun dequeue (Queue ([], [])) = (NONE, Queue ([], []))
- | dequeue (Queue (xs, y :: ys)) = (SOME y, Queue (xs, ys))
- | dequeue (Queue (v :: va, [])) =
+fun dequeue (AQueue ([], [])) = (NONE, AQueue ([], []))
+ | dequeue (AQueue (xs, y :: ys)) = (SOME y, AQueue (xs, ys))
+ | dequeue (AQueue (v :: va, [])) =
let
val y :: ys = rev (v :: va);
in
- (SOME y, Queue ([], ys))
+ (SOME y, AQueue ([], ys))
end;
-fun enqueue x (Queue (xs, ys)) = Queue (x :: xs, ys);
+fun enqueue x (AQueue (xs, ys)) = AQueue (x :: xs, ys);
end; (*struct Example*)
--- a/src/HOL/Finite_Set.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Finite_Set.thy Wed Feb 04 11:32:35 2009 +0000
@@ -383,7 +383,7 @@
subsection {* Class @{text finite} *}
setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
-class finite = itself +
+class finite =
assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
setup {* Sign.parent_path *}
hide const finite
--- a/src/HOL/Imperative_HOL/Array.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Imperative_HOL/Array.thy Wed Feb 04 11:32:35 2009 +0000
@@ -198,12 +198,12 @@
subsubsection {* Haskell *}
-code_type array (Haskell "STArray/ RealWorld/ _")
+code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _")
code_const Array (Haskell "error/ \"bare Array\"")
-code_const Array.new' (Haskell "newArray/ (0,/ _)")
-code_const Array.of_list' (Haskell "newListArray/ (0,/ _)")
-code_const Array.length' (Haskell "lengthArray")
-code_const Array.nth' (Haskell "readArray")
-code_const Array.upd' (Haskell "writeArray")
+code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)")
+code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)")
+code_const Array.length' (Haskell "Heap.lengthArray")
+code_const Array.nth' (Haskell "Heap.readArray")
+code_const Array.upd' (Haskell "Heap.writeArray")
end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Feb 04 11:32:35 2009 +0000
@@ -1,5 +1,4 @@
(* Title: HOL/Library/Heap_Monad.thy
- ID: $Id$
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)
@@ -375,7 +374,7 @@
text {* Adaption layer *}
-code_include Haskell "STMonad"
+code_include Haskell "Heap"
{*import qualified Control.Monad;
import qualified Control.Monad.ST;
import qualified Data.STRef;
@@ -386,9 +385,6 @@
type STRef s a = Data.STRef.STRef s a;
type STArray s a = Data.Array.ST.STArray s Int a;
-runST :: (forall s. ST s a) -> a;
-runST s = Control.Monad.ST.runST s;
-
newSTRef = Data.STRef.newSTRef;
readSTRef = Data.STRef.readSTRef;
writeSTRef = Data.STRef.writeSTRef;
@@ -408,14 +404,11 @@
writeArray :: STArray s a -> Int -> a -> ST s ();
writeArray = Data.Array.ST.writeArray;*}
-code_reserved Haskell RealWorld ST STRef Array
- runST
- newSTRef reasSTRef writeSTRef
- newArray newListArray lengthArray readArray writeArray
+code_reserved Haskell Heap
text {* Monad *}
-code_type Heap (Haskell "ST/ RealWorld/ _")
+code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
code_const Heap (Haskell "error/ \"bare Heap\"")
code_monad "op \<guillemotright>=" Haskell
code_const return (Haskell "return")
--- a/src/HOL/Imperative_HOL/Ref.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Imperative_HOL/Ref.thy Wed Feb 04 11:32:35 2009 +0000
@@ -82,10 +82,10 @@
subsubsection {* Haskell *}
-code_type ref (Haskell "STRef/ RealWorld/ _")
+code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _")
code_const Ref (Haskell "error/ \"bare Ref\"")
-code_const Ref.new (Haskell "newSTRef")
-code_const Ref.lookup (Haskell "readSTRef")
-code_const Ref.update (Haskell "writeSTRef")
+code_const Ref.new (Haskell "Heap.newSTRef")
+code_const Ref.lookup (Haskell "Heap.readSTRef")
+code_const Ref.update (Haskell "Heap.writeSTRef")
end
\ No newline at end of file
--- a/src/HOL/Library/Countable.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Library/Countable.thy Wed Feb 04 11:32:35 2009 +0000
@@ -10,7 +10,7 @@
subsection {* The class of countable types *}
-class countable = itself +
+class countable =
assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat"
lemma countable_classI:
--- a/src/HOL/Library/Efficient_Nat.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Library/Efficient_Nat.thy Wed Feb 04 11:32:35 2009 +0000
@@ -308,7 +308,7 @@
code_reserved Haskell Nat
code_type nat
- (Haskell "Nat")
+ (Haskell "Nat.Nat")
code_instance nat :: eq
(Haskell -)
--- a/src/HOL/Library/Enum.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Library/Enum.thy Wed Feb 04 11:32:35 2009 +0000
@@ -11,14 +11,14 @@
subsection {* Class @{text enum} *}
-class enum = itself +
+class enum =
fixes enum :: "'a list"
assumes UNIV_enum [code]: "UNIV = set enum"
and enum_distinct: "distinct enum"
begin
-lemma finite_enum: "finite (UNIV \<Colon> 'a set)"
- unfolding UNIV_enum ..
+subclass finite proof
+qed (simp add: UNIV_enum)
lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
--- a/src/HOL/Library/State_Monad.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Library/State_Monad.thy Wed Feb 04 11:32:35 2009 +0000
@@ -1,5 +1,4 @@
(* Title: HOL/Library/State_Monad.thy
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
*)
--- a/src/HOL/Typedef.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Typedef.thy Wed Feb 04 11:32:35 2009 +0000
@@ -119,52 +119,4 @@
use "Tools/typecopy_package.ML" setup TypecopyPackage.setup
use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
-
-text {* This class is just a workaround for classes without parameters;
- it shall disappear as soon as possible. *}
-
-class itself =
- fixes itself :: "'a itself"
-
-setup {*
-let fun add_itself tyco thy =
- let
- val vs = Name.names Name.context "'a"
- (replicate (Sign.arity_number thy tyco) @{sort type});
- val ty = Type (tyco, map TFree vs);
- val lhs = Const (@{const_name itself}, Term.itselfT ty);
- val rhs = Logic.mk_type ty;
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
- in
- thy
- |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
- |> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
- |> snd
- |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
- |> LocalTheory.exit_global
- end
-in TypedefPackage.interpretation add_itself end
-*}
-
-instantiation bool :: itself
-begin
-
-definition "itself = TYPE(bool)"
-
-instance ..
-
end
-
-instantiation "fun" :: ("type", "type") itself
-begin
-
-definition "itself = TYPE('a \<Rightarrow> 'b)"
-
-instance ..
-
-end
-
-hide (open) const itself
-
-end
--- a/src/HOL/ex/ImperativeQuicksort.thy Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/ex/ImperativeQuicksort.thy Wed Feb 04 11:32:35 2009 +0000
@@ -629,9 +629,9 @@
ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
-export_code qsort in SML_imp module_name Arr
-export_code qsort in OCaml module_name Arr file -
-export_code qsort in OCaml_imp module_name Arr file -
-export_code qsort in Haskell module_name Arr file -
+export_code qsort in SML_imp module_name QSort
+export_code qsort in OCaml module_name QSort file -
+export_code qsort in OCaml_imp module_name QSort file -
+export_code qsort in Haskell module_name QSort file -
end
\ No newline at end of file
--- a/src/Pure/Isar/class.ML Wed Feb 04 11:31:05 2009 +0000
+++ b/src/Pure/Isar/class.ML Wed Feb 04 11:32:35 2009 +0000
@@ -41,9 +41,16 @@
(Const o apsnd (map_atyps (K aT))) param_map;
val const_morph = Element.inst_morphism thy
(Symtab.empty, Symtab.make param_map_inst);
- val (([props], [(_, inst_morph)], export_morph), _) = empty_ctxt
+ val typ_morph = Element.inst_morphism thy
+ (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty);
+ val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt
|> Expression.cert_goal_expression ([(class, (("", false),
Expression.Named param_map_const))], []);
+ val (props, inst_morph) = if null param_map
+ then (raw_props |> map (Morphism.term typ_morph),
+ raw_inst_morph $> typ_morph)
+ else (raw_props, raw_inst_morph); (*FIXME proper handling in
+ locale.ML / expression.ML would be desirable*)
(* witness for canonical interpretation *)
val prop = try the_single props;
@@ -162,7 +169,7 @@
|> Sign.minimize_sort thy;
val _ = case filter_out (is_class thy) sups
of [] => ()
- | no_classes => error ("No proper classes: " ^ commas (map quote no_classes));
+ | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
val supparam_names = map fst supparams;
val _ = if has_duplicates (op =) supparam_names
--- a/src/Pure/Isar/expression.ML Wed Feb 04 11:31:05 2009 +0000
+++ b/src/Pure/Isar/expression.ML Wed Feb 04 11:32:35 2009 +0000
@@ -100,7 +100,7 @@
(* FIXME: cannot compare bindings for equality. *)
fun params_loc loc =
- (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
+ (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
fun params_inst (expr as (loc, (prfx, Positional insts))) =
let
val (ps, loc') = params_loc loc;
@@ -150,14 +150,14 @@
local
-fun prep_inst parse_term ctxt parms (Positional insts) =
+fun prep_inst prep_term ctxt parms (Positional insts) =
(insts ~~ parms) |> map (fn
- (NONE, p) => Free (p, the (Variable.default_type ctxt p)) |
- (SOME t, _) => parse_term ctxt t)
- | prep_inst parse_term ctxt parms (Named insts) =
+ (NONE, p) => Free (p, dummyT) |
+ (SOME t, _) => prep_term ctxt t)
+ | prep_inst prep_term ctxt parms (Named insts) =
parms |> map (fn p => case AList.lookup (op =) insts p of
- SOME t => parse_term ctxt t |
- NONE => Free (p, the (Variable.default_type ctxt p)));
+ SOME t => prep_term ctxt t |
+ NONE => Free (p, dummyT));
in
@@ -350,19 +350,19 @@
local
-fun prep_full_context_statement parse_typ parse_prop prep_vars_elem parse_inst prep_vars_inst prep_expr
+fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
strict do_close raw_import init_body raw_elems raw_concl ctxt1 =
let
val thy = ProofContext.theory_of ctxt1;
val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
- fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
+ fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
let
val (parm_names, parm_types) = Locale.params_of thy loc |>
map_split (fn (b, SOME T, _) => (Binding.base_name b, T))
(*FIXME return value of Locale.params_of has strange type*)
- val inst' = parse_inst ctxt parm_names inst;
+ val inst' = prep_inst ctxt parm_names inst;
val parm_types' = map (TypeInfer.paramify_vars o
Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
val inst'' = map2 TypeInfer.constrain parm_types' inst';
@@ -387,7 +387,7 @@
val fors = prep_vars_inst fixed ctxt1 |> fst;
val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
- val (_, insts', ctxt3) = fold prep_inst raw_insts (0, [], ctxt2);
+ val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
val ctxt4 = init_body ctxt3;
val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
val (insts, elems', concl, ctxt6) =
--- a/src/Tools/code/code_haskell.ML Wed Feb 04 11:31:05 2009 +0000
+++ b/src/Tools/code/code_haskell.ML Wed Feb 04 11:32:35 2009 +0000
@@ -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 ";";