--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Thu Oct 02 17:18:22 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Thu Oct 02 17:18:36 2008 +0200
@@ -784,7 +784,7 @@
\newline%
\verb|fun eqop A_ a b = eq A_ a b;|\newline%
\newline%
-\verb|fun member A_ x (y :: ys) = (if eqop A_ y x then true else member A_ x ys)|\newline%
+\verb|fun member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys|\newline%
\verb| |\verb,|,\verb| member A_ x [] = false;|\newline%
\newline%
\verb|fun collect_duplicates A_ xs ys (z :: zs) =|\newline%
@@ -987,12 +987,12 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-Then code generation for SML would fail with a message
+\noindent Then code generation for SML would fail with a message
that the generated code contains illegal mutual dependencies:
- the theorem \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}} already requires the
+ the theorem \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}} already requires the
instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
- \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}}; Haskell has no problem with mutually
- recursive \isa{inst} and \isa{fun} definitions,
+ \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}}; Haskell has no problem with mutually
+ recursive \isa{instance} and \isa{function} definitions,
but the SML serializer does not support this.
In such cases, you have to provide your own equality equations
@@ -1009,7 +1009,7 @@
\isacommand{lemma}\isamarkupfalse%
\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
-\ \ \ \ \ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
\endisatagquoteme
@@ -1036,13 +1036,8 @@
\verb|structure Example = |\newline%
\verb|struct|\newline%
\newline%
-\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
-\verb|fun eq (A_:'a eq) = #eq A_;|\newline%
-\newline%
\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
\newline%
-\verb|fun eqop A_ a b = eq A_ a b;|\newline%
-\newline%
\verb|fun null (x :: xs) = false|\newline%
\verb| |\verb,|,\verb| null [] = true;|\newline%
\newline%
@@ -1051,8 +1046,6 @@
\verb| |\verb,|,\verb| eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'|\newline%
\verb| |\verb,|,\verb| eq_nat Zero_nat Zero_nat = true;|\newline%
\newline%
-\verb|val eq_nata = {eq = eq_nat} : nat eq;|\newline%
-\newline%
\verb|datatype monotype = Mono of nat * monotype list;|\newline%
\newline%
\verb|fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys|\newline%
@@ -1060,8 +1053,7 @@
\verb| |\verb,|,\verb| list_all2 p [] ys = null ys;|\newline%
\newline%
\verb|fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =|\newline%
-\verb| eqop eq_nata tyco1 tyco2 andalso|\newline%
-\verb| list_all2 eq_monotype typargs1 typargs2;|\newline%
+\verb| eq_nat tyco1 tyco2 andalso list_all2 eq_monotype typargs1 typargs2;|\newline%
\newline%
\verb|end; (*struct Example*)|%
\end{isamarkuptext}%
@@ -1074,12 +1066,166 @@
%
\endisadelimquoteme
%
-\isamarkupsubsection{Partiality%
+\isamarkupsubsection{Explicit partiality%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, examples: maps%
+Partiality usually enters the game by partial patterns, as
+ in the following example, again for amortised queues:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{fun}\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}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent In the corresponding code, there is no equation
+ for the pattern \isa{Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|strict_dequeue :: forall a. Queue a -> (a, Queue a);|\newline%
+\verb|strict_dequeue (Queue xs (y : ys)) = (y, Queue xs ys);|\newline%
+\verb|strict_dequeue (Queue xs []) =|\newline%
+\verb| let {|\newline%
+\verb| (y : ys) = rev xs;|\newline%
+\verb| } in (y, Queue [] ys);|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent In some cases it is desirable to have this
+ pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{axiomatization}\isamarkupfalse%
+\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
+\isanewline
+\isacommand{function}\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
+\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%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\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.
+
+ Normally, if constants without any defining 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 categorize a constant into
+ that category explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
+\ empty{\isacharunderscore}queue%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent Then the code generator will just insert an error or
+ exception at the appropriate position:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|empty_queue :: forall a. a;|\newline%
+\verb|empty_queue = error "empty_queue";|\newline%
+\newline%
+\verb|strict_dequeue' :: forall a. Queue a -> (a, Queue a);|\newline%
+\verb|strict_dequeue' (Queue xs []) =|\newline%
+\verb| (if nulla xs then empty_queue else strict_dequeue' (Queue [] (rev xs)));|\newline%
+\verb|strict_dequeue' (Queue xs (y : ys)) = (y, Queue xs ys);|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent This feature however is rarely needed in practice.
+ Note also that the \isa{HOL} default setup already declares
+ \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
+ likely to be used in such situations.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1097,7 +1243,7 @@
%
\endisadelimtheory
\isanewline
-\end{isabellebody}%
+\ \end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"