# HG changeset patch # User haftmann # Date 1282047552 -7200 # Node ID cfe74b0eecb123e7e26392b69bd614417499dcb4 # Parent 2c46f628e6b795dd3c72047cc9472519d57f360d reworked section on simple datatype refinement diff -r 2c46f628e6b7 -r cfe74b0eecb1 doc-src/Codegen/Thy/Refinement.thy --- a/doc-src/Codegen/Thy/Refinement.thy Tue Aug 17 14:19:11 2010 +0200 +++ b/doc-src/Codegen/Thy/Refinement.thy Tue Aug 17 14:19:12 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 2c46f628e6b7 -r cfe74b0eecb1 doc-src/Codegen/Thy/document/Refinement.tex --- a/doc-src/Codegen/Thy/document/Refinement.tex Tue Aug 17 14:19:11 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Tue Aug 17 14:19:12 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% %