--- a/CONTRIBUTORS Tue Aug 17 13:10:58 2010 +0200
+++ b/CONTRIBUTORS Tue Aug 17 14:33:44 2010 +0200
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* July 2010: Florian Haftmann, TUM
+ Reworking and extension of the Isabelle/HOL framework.
+
Contributions to Isabelle2009-2
--------------------------------------
--- a/NEWS Tue Aug 17 13:10:58 2010 +0200
+++ b/NEWS Tue Aug 17 14:33:44 2010 +0200
@@ -35,11 +35,17 @@
*** HOL ***
+* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
+INCOMPATIBILITY.
+
+* Quickcheck in locales considers interpretations of that locale for
+counter example search.
+
* Theory Library/Monad_Syntax provides do-syntax for monad types. Syntax
in Library/State_Monad has been changed to avoid ambiguities.
INCOMPATIBILITY.
-* code generator: export_code without explicit file declaration prints
+* Code generator: export_code without explicit file declaration prints
to standard output. INCOMPATIBILITY.
* Abolished symbol type names: "prod" and "sum" replace "*" and "+"
@@ -121,8 +127,8 @@
INCOMPATIBILITY.
* Inductive package: offers new command "inductive_simps" to automatically
- derive instantiated and simplified equations for inductive predicates,
- similar to inductive_cases.
+derive instantiated and simplified equations for inductive predicates,
+similar to inductive_cases.
*** ML ***
--- a/doc-src/Codegen/Thy/Foundations.thy Tue Aug 17 13:10:58 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Tue Aug 17 14:33:44 2010 +0200
@@ -7,7 +7,6 @@
subsection {* Code generator architecture \label{sec:architecture} *}
text {*
-
The code generator is actually a framework consisting of different
components which can be customised individually.
--- a/doc-src/Codegen/Thy/Refinement.thy Tue Aug 17 13:10:58 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy Tue Aug 17 14:33:44 2010 +0200
@@ -70,23 +70,17 @@
text %quote {*@{code_stmts fib (consts) fib fib_step (Haskell)}*}
-subsection {* Datatypes \label{sec:datatypes} *}
+subsection {* Datatype refinement *}
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:
+ Selecting specific code equations \emph{and} datatype constructors
+ leads to datatype refinement. 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"
@@ -115,7 +109,18 @@
\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
+ to be.
+
+ The prerequisite for datatype constructors is only syntactical: a
+ constructor must be 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>"}; then @{text "\<kappa>"} is its corresponding datatype. The
+ HOL datatype package by default registers any new datatype with its
+ constructors, but this may be changed using @{command
+ code_datatype}; the currently chosen constructors can be inspected
+ using the @{command print_codesetup} command.
+
+ 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:
*}
@@ -151,28 +156,21 @@
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.
+ The same techniques can also be applied to types which are not
+ specified as datatypes, e.g.~type @{typ int} is originally specified
+ as quotient type by means of @{command typedef}, but for code
+ generation constants allowing construction of binary numeral values
+ are used as constructors for @{typ int}.
- \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.
+ This approach however fails if the representation of a type demands
+ invariants; this issue is discussed in the next section.
+*}
+
- \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.
+subsection {* Datatype refinement involving invariants *}
- \end{itemize}
+text {*
+ FIXME
*}
end
--- a/doc-src/Codegen/Thy/Setup.thy Tue Aug 17 13:10:58 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy Tue Aug 17 14:33:44 2010 +0200
@@ -1,5 +1,5 @@
theory Setup
-imports Complex_Main
+imports Complex_Main More_List
uses
"../../antiquote_setup.ML"
"../../more_antiquote.ML"
--- a/doc-src/Codegen/Thy/document/Introduction.tex Tue Aug 17 13:10:58 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Aug 17 14:33:44 2010 +0200
@@ -141,7 +141,8 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val id :~'a -> 'a\\
+\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
\hspace*{0pt} ~val rev :~'a list -> 'a list\\
\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
\hspace*{0pt} ~val empty :~'a queue\\
@@ -149,10 +150,12 @@
\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
-\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}fun id x = (fn xa => xa) x;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun fold f [] = id\\
+\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
\hspace*{0pt}\\
\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
\hspace*{0pt}\\
--- a/doc-src/Codegen/Thy/document/Refinement.tex Tue Aug 17 13:10:58 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Tue Aug 17 14:33:44 2010 +0200
@@ -191,24 +191,19 @@
%
\endisadelimquote
%
-\isamarkupsubsection{Datatypes \label{sec:datatypes}%
+\isamarkupsubsection{Datatype refinement%
}
\isamarkuptrue%
%
\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.
-
- 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:%
+Selecting specific code equations \emph{and} datatype constructors
+ leads to datatype refinement. 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:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -267,7 +262,16 @@
\noindent Here we define a \qt{constructor} \isa{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
+ to be.
+
+ The prerequisite for datatype constructors is only syntactical: a
+ constructor must be 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}}; then \isa{{\isasymkappa}} is its corresponding datatype. The
+ HOL datatype package by default registers any new datatype with its
+ constructors, but this may be changed using \hyperlink{command.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}; the currently chosen constructors can be inspected
+ using the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
+
+ 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}%
@@ -347,7 +351,8 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val id :~'a -> 'a\\
+\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
\hspace*{0pt} ~val rev :~'a list -> 'a list\\
\hspace*{0pt} ~val null :~'a list -> bool\\
\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
@@ -356,10 +361,12 @@
\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
-\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}fun id x = (fn xa => xa) x;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun fold f [] = id\\
+\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
\hspace*{0pt}\\
\hspace*{0pt}fun null [] = true\\
\hspace*{0pt} ~| null (x ::~xs) = false;\\
@@ -387,28 +394,23 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\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 \isa{case} combinator.
+The same techniques can also be applied to types which are not
+ specified as datatypes, e.g.~type \isa{int} is originally specified
+ as quotient type by means of \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}, but for code
+ generation constants allowing construction of binary numeral values
+ are used as constructors for \isa{int}.
- \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}%
+ This approach however fails if the representation of a type demands
+ invariants; this issue is discussed in the next section.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Datatype refinement involving invariants%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/examples/example.ML Tue Aug 17 13:10:58 2010 +0200
+++ b/doc-src/Codegen/Thy/examples/example.ML Tue Aug 17 14:33:44 2010 +0200
@@ -1,5 +1,6 @@
structure Example : sig
- val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
+ val id : 'a -> 'a
+ val fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val rev : 'a list -> 'a list
datatype 'a queue = AQueue of 'a list * 'a list
val empty : 'a queue
@@ -7,10 +8,12 @@
val enqueue : 'a -> 'a queue -> 'a queue
end = struct
-fun foldl f a [] = a
- | foldl f a (x :: xs) = foldl f (f a x) xs;
+fun id x = (fn xa => xa) x;
-fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;
+fun fold f [] = id
+ | fold f (x :: xs) = fold f xs o f x;
+
+fun rev xs = fold (fn a => fn b => a :: b) xs [];
datatype 'a queue = AQueue of 'a list * 'a list;
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Aug 17 13:10:58 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Aug 17 14:33:44 2010 +0200
@@ -1018,7 +1018,7 @@
target: 'OCaml' | 'SML' | 'Haskell'
;
- 'code' ( 'del' ) ?
+ 'code' ( 'del' | 'abstype' | 'abstract' ) ?
;
'code\_abort' ( const + )
@@ -1104,9 +1104,11 @@
declaration.
\item @{attribute (HOL) code} explicitly selects (or with option
- ``@{text "del"}'' deselects) a code equation for code
- generation. Usually packages introducing code equations provide
- a reasonable default setup for selection.
+ ``@{text "del"}'' deselects) a code equation for code generation.
+ Usually packages introducing code equations provide a reasonable
+ default setup for selection. Variants @{text "code abstype"} and
+ @{text "code abstract"} declare abstract datatype certificates or
+ code equations on abstract datatype representations respectively.
\item @{command (HOL) "code_abort"} declares constants which are not
required to have a definition by means of code equations; if
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Aug 17 13:10:58 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Aug 17 14:33:44 2010 +0200
@@ -1034,7 +1034,7 @@
target: 'OCaml' | 'SML' | 'Haskell'
;
- 'code' ( 'del' ) ?
+ 'code' ( 'del' | 'abstype' | 'abstract' ) ?
;
'code\_abort' ( const + )
@@ -1117,9 +1117,11 @@
declaration.
\item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
- ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
- generation. Usually packages introducing code equations provide
- a reasonable default setup for selection.
+ ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
+ Usually packages introducing code equations provide a reasonable
+ default setup for selection. Variants \isa{{\isachardoublequote}code\ abstype{\isachardoublequote}} and
+ \isa{{\isachardoublequote}code\ abstract{\isachardoublequote}} declare abstract datatype certificates or
+ code equations on abstract datatype representations respectively.
\item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
required to have a definition by means of code equations; if