# HG changeset patch
# User haftmann
# Date 1178689984 -7200
# Node ID ebde66a71ab0cdca39792b812da465e5f131f8be
# Parent  5804926e0379aaa257c09a4f87d78890cee19bd6
continued

diff -r 5804926e0379 -r ebde66a71ab0 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Wed May 09 01:56:59 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Wed May 09 07:53:04 2007 +0200
@@ -671,8 +671,49 @@
   to delete disturbing theorems in the code theorem table,
   as we have done here with the original definitions @{text less_prod_def}
   and @{text less_eq_prod_def}.
+
+  In some cases, the automatically derived defining equations
+  for equality on a particular type may not be appropriate.
+  As example, watch the following datatype representing
+  monomorphic parametric types:
 *}
 
+datatype monotype = Mono string "monotype list"
+(*<*)
+lemma monotype_eq:
+  "Mono tyco1 typargs1 = Mono tyco2 typargs2 \<equiv> 
+     tyco1 = tyco2 \<and> typargs1 = typargs2" by simp
+(*>*)
+
+text {*
+  Then code generation for SML would fail with a message
+  that the generated code conains illegal mutual dependencies:
+  the theorem @{thm monotype_eq} already requires the
+  instance @{text "monotype \<Colon> eq"}, which itself requires
+  @{thm monotype_eq};  Haskell has no problem with mutually
+  recursive @{text instance} and @{text function} definitions,
+  but the SML serializer does not support this.
+
+  In such cases, you have to provide you own equality equations
+  involving auxiliary constants.  In our case,
+  @{const [show_types] list_all2} can do the job:
+*}
+
+lemma monotype_eq_list_all2 [code func]:
+  "Mono tyco1 typargs1 = Mono tyco2 typargs2 \<longleftrightarrow>
+     tyco1 = tyco2 \<and> list_all2 (op =) typargs1 typargs2"
+  by (simp add: list_all2_eq [symmetric])
+
+text {*
+  does not depend on instance @{text "monotype \<Colon> eq"}:
+*}
+
+code_gen "op = :: monotype \<Rightarrow> monotype \<Rightarrow> bool"
+  (*<*)in SML(*>*)in SML file "examples/monotype.ML"
+
+text {*
+  \lstsml{Thy/examples/monotype.ML}
+*}
 
 subsection {* Programs as sets of theorems *}
 
diff -r 5804926e0379 -r ebde66a71ab0 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Wed May 09 01:56:59 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Wed May 09 07:53:04 2007 +0200
@@ -902,7 +902,71 @@
   are rejected immediately.  Consequently, it might be necessary
   to delete disturbing theorems in the code theorem table,
   as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def}
-  and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.%
+  and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.
+
+  In some cases, the automatically derived defining equations
+  for equality on a particular type may not be appropriate.
+  As example, watch the following datatype representing
+  monomorphic parametric types:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ monotype\ {\isacharequal}\ Mono\ string\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Then code generation for SML would fail with a message
+  that the generated code conains illegal mutual dependencies:
+  the theorem \isa{Mono\ {\isacharquery}tyco{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}typargs{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharequal}\ Mono\ {\isacharquery}tyco{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}typargs{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isasymequiv}\ {\isacharquery}tyco{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharequal}\ {\isacharquery}tyco{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isasymand}\ {\isacharquery}typargs{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharequal}\ {\isacharquery}typargs{\isadigit{2}}{\isachardot}{\isadigit{0}}} already requires the
+  instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
+  \isa{Mono\ {\isacharquery}tyco{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}typargs{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharequal}\ Mono\ {\isacharquery}tyco{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}typargs{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isasymequiv}\ {\isacharquery}tyco{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharequal}\ {\isacharquery}tyco{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isasymand}\ {\isacharquery}typargs{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharequal}\ {\isacharquery}typargs{\isadigit{2}}{\isachardot}{\isadigit{0}}};  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 you own equality equations
+  involving auxiliary constants.  In our case,
+  \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymlongleftrightarrow}\isanewline
+\ \ \ \ \ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ {\isacharparenleft}op\ {\isacharequal}{\isacharparenright}\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isacharcolon}{\isacharcolon}\ monotype\ {\isasymRightarrow}\ monotype\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}monotype{\isachardot}ML{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/monotype.ML}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %