--- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Thu Oct 02 17:18:22 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Thu Oct 02 17:18:36 2008 +0200
@@ -420,17 +420,17 @@
datatype %quoteme monotype = Mono nat "monotype list"
(*<*)
lemma monotype_eq:
- "Mono tyco1 typargs1 = Mono tyco2 typargs2 \<equiv>
- tyco1 = tyco2 \<and> typargs1 = typargs2" by simp
+ "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<equiv>
+ eq_class.eq tyco1 tyco2 \<and> eq_class.eq typargs1 typargs2" by (simp add: eq)
(*>*)
text {*
- 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 @{thm monotype_eq [no_vars]} already requires the
instance @{text "monotype \<Colon> eq"}, which itself requires
@{thm monotype_eq [no_vars]}; Haskell has no problem with mutually
- recursive @{text inst} and @{text fun} definitions,
+ recursive @{text instance} and @{text function} definitions,
but the SML serializer does not support this.
In such cases, you have to provide your own equality equations
@@ -440,7 +440,7 @@
lemma %quoteme monotype_eq_list_all2 [code func]:
"eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
- tyco1 = tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
+ eq_class.eq tyco1 tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
by (simp add: eq list_all2_eq [symmetric])
text {*
@@ -450,8 +450,73 @@
text %quoteme {*@{code_stmts "eq_class.eq :: monotype \<Rightarrow> monotype \<Rightarrow> bool" (SML)}*}
-subsection {* Partiality *}
+subsection {* Explicit partiality *}
+
+text {*
+ Partiality usually enters the game by partial patterns, as
+ in the following example, again for amortised queues:
+*}
+
+fun %quoteme 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))"
+
+text {*
+ \noindent In the corresponding code, there is no equation
+ for the pattern @{term "Queue [] []"}:
+*}
+
+text %quoteme {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
+
+text {*
+ \noindent In some cases it is desirable to have this
+ pseudo-\qt{partiality} more explicitly, e.g.~as follows:
+*}
+
+axiomatization %quoteme empty_queue :: 'a
+
+function %quoteme 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
-text {* @{command "code_abort"}, examples: maps *}
+termination %quoteme strict_dequeue'
+by (relation "measure (\<lambda>q::'a queue. case q of Queue xs ys \<Rightarrow> length xs)") simp_all
+
+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.
+
+ 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 @{command "code_abort"}:
+*}
+
+code_abort %quoteme empty_queue
+
+text {*
+ \noindent Then the code generator will just insert an error or
+ exception at the appropriate position:
+*}
+
+text %quoteme {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
+
+text {*
+ \noindent This feature however is rarely needed in practice.
+ Note also that the @{text HOL} default setup already declares
+ @{const undefined} as @{command "code_abort"}, which is most
+ likely to be used in such situations.
+*}
end
+
\ No newline at end of file
--- 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"