--- a/doc-src/Codegen/Thy/Foundations.thy Mon Aug 16 10:32:45 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Mon Aug 16 10:54:08 2010 +0200
@@ -230,7 +230,7 @@
*}
-subsection {* Explicit partiality *}
+subsection {* Explicit partiality \label{sec:partiality} *}
text {*
Partiality usually enters the game by partial patterns, as
@@ -305,21 +305,40 @@
text {*
Under certain circumstances, the code generator fails to produce
- code entirely.
+ code entirely. To debug these, the following hints may prove
+ helpful:
\begin{description}
- \ditem{generate only one module}
+ \ditem{\emph{Check with a different target language}.} Sometimes
+ the situation gets more clear if you switch to another target
+ language; the code generated there might give some hints what
+ prevents the code generator to produce code for the desired
+ language.
- \ditem{check with a different target language}
-
- \ditem{inspect code equations}
+ \ditem{\emph{Inspect code equations}.} Code equations are the central
+ carrier of code generation. Most problems occuring while generation
+ code can be traced to single equations which are printed as part of
+ the error message. A closer inspection of those may offer the key
+ for solving issues (cf.~\secref{sec:equations}).
- \ditem{inspect preprocessor setup}
+ \ditem{\emph{Inspect preprocessor setup}.} The preprocessor might
+ transform code equations unexpectedly; to understand an
+ inspection of its setup is necessary (cf.~\secref{sec:preproc}).
- \ditem{generate exceptions}
+ \ditem{\emph{Generate exceptions}.} If the code generator
+ complains about missing code equations, in can be helpful to
+ implement the offending constants as exceptions
+ (cf.~\secref{sec:partiality}); this allows at least for a formal
+ generation of code, whose inspection may then give clues what is
+ wrong.
- \ditem{remove offending code equations}
+ \ditem{\emph{Remove offending code equations}.} If code
+ generation is prevented by just a single equation, this can be
+ removed (cf.~\secref{sec:equations}) to allow formal code
+ generation, whose result in turn can be used to trace the
+ problem. The most prominent case here are mismatches in type
+ class signatures (\qt{wellsortedness error}).
\end{description}
*}
--- a/doc-src/Codegen/Thy/document/Foundations.tex Mon Aug 16 10:32:45 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Mon Aug 16 10:54:08 2010 +0200
@@ -396,7 +396,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Explicit partiality%
+\isamarkupsubsection{Explicit partiality \label{sec:partiality}%
}
\isamarkuptrue%
%
@@ -568,21 +568,40 @@
%
\begin{isamarkuptext}%
Under certain circumstances, the code generator fails to produce
- code entirely.
+ code entirely. To debug these, the following hints may prove
+ helpful:
\begin{description}
- \ditem{generate only one module}
+ \ditem{\emph{Check with a different target language}.} Sometimes
+ the situation gets more clear if you switch to another target
+ language; the code generated there might give some hints what
+ prevents the code generator to produce code for the desired
+ language.
- \ditem{check with a different target language}
-
- \ditem{inspect code equations}
+ \ditem{\emph{Inspect code equations}.} Code equations are the central
+ carrier of code generation. Most problems occuring while generation
+ code can be traced to single equations which are printed as part of
+ the error message. A closer inspection of those may offer the key
+ for solving issues (cf.~\secref{sec:equations}).
- \ditem{inspect preprocessor setup}
+ \ditem{\emph{Inspect preprocessor setup}.} The preprocessor might
+ transform code equations unexpectedly; to understand an
+ inspection of its setup is necessary (cf.~\secref{sec:preproc}).
- \ditem{generate exceptions}
+ \ditem{\emph{Generate exceptions}.} If the code generator
+ complains about missing code equations, in can be helpful to
+ implement the offending constants as exceptions
+ (cf.~\secref{sec:partiality}); this allows at least for a formal
+ generation of code, whose inspection may then give clues what is
+ wrong.
- \ditem{remove offending code equations}
+ \ditem{\emph{Remove offending code equations}.} If code
+ generation is prevented by just a single equation, this can be
+ removed (cf.~\secref{sec:equations}) to allow formal code
+ generation, whose result in turn can be used to trace the
+ problem. The most prominent case here are mismatches in type
+ class signatures (\qt{wellsortedness error}).
\end{description}%
\end{isamarkuptext}%