# HG changeset patch # User haftmann # Date 1282048424 -7200 # Node ID 0e4565062017171717a2a4e19671234e82d542f5 # Parent b8760b6e7c65b8a00f5a3d9366fd4975ba13fc94# Parent 34d3de1254cdca14b837418b5debe919004479e9 merged diff -r b8760b6e7c65 -r 0e4565062017 CONTRIBUTORS --- 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 -------------------------------------- diff -r b8760b6e7c65 -r 0e4565062017 NEWS --- 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 *** diff -r b8760b6e7c65 -r 0e4565062017 doc-src/Codegen/Thy/Foundations.thy --- 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. diff -r b8760b6e7c65 -r 0e4565062017 doc-src/Codegen/Thy/Refinement.thy --- 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 "\ = \ \ \ \\<^isub>1 \ \\<^isub>n"} where @{text - "{\\<^isub>1, \, \\<^isub>n}"} is exactly the set of \emph{all} type variables in - @{text "\"}. 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 "\ = \ \ \ \\<^isub>1 \ \\<^isub>n"} where @{text + "{\\<^isub>1, \, \\<^isub>n}"} is exactly the set of \emph{all} type variables in + @{text "\"}; then @{text "\"} 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 diff -r b8760b6e7c65 -r 0e4565062017 doc-src/Codegen/Thy/Setup.thy --- 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" diff -r b8760b6e7c65 -r 0e4565062017 doc-src/Codegen/Thy/document/Introduction.tex --- 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}\\ diff -r b8760b6e7c65 -r 0e4565062017 doc-src/Codegen/Thy/document/Refinement.tex --- 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% % diff -r b8760b6e7c65 -r 0e4565062017 doc-src/Codegen/Thy/examples/example.ML --- 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; diff -r b8760b6e7c65 -r 0e4565062017 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 diff -r b8760b6e7c65 -r 0e4565062017 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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