--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed May 30 21:09:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed May 30 21:09:13 2007 +0200
@@ -161,13 +161,15 @@
\begin{isamarkuptext}%
\noindent For testing purpose, we define a small example
using natural numbers \isa{nat} (which are a \isa{linorder})
- as keys and strings values:%
+ as keys and list of nats as values:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
+\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ example\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharparenleft}nat{\isacharcomma}\ string{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}example\ n\ {\isacharequal}\ update\ {\isacharparenleft}n{\isacharcomma}\ {\isacharprime}{\isacharprime}bar{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}Leaf\ {\isadigit{0}}\ {\isacharprime}{\isacharprime}foo{\isacharprime}{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}%
+\ \ example\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat{\isacharcomma}\ nat\ list{\isacharparenright}\ searchtree{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}example\ {\isacharequal}\ update\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharcomma}\ {\isacharbrackleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}update\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isacharcomma}\ {\isacharbrackleft}Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \ \ {\isacharparenleft}update\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ {\isacharbrackleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}Leaf\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent Then we generate code%
\end{isamarkuptext}%
@@ -585,7 +587,7 @@
integer literals in target languages.
\item[\isa{Pretty{\isacharunderscore}Char}] represents \isa{HOL} characters by
character literals in target languages.
- \item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr},
+ \item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char},
but also offers treatment of character codes; includes
\isa{Pretty{\isacharunderscore}Int}.
\item[\isa{ExecutableSet}] allows to generate code
@@ -918,11 +920,12 @@
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:%
+ monomorphic parametric types (where type constructors
+ are referred to by natural numbers):%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
-\ monotype\ {\isacharequal}\ Mono\ string\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
+\ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof
@@ -939,9 +942,9 @@
\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
+ 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
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
+ \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{instance} and \isa{function} definitions,
but the SML serializer does not support this.
@@ -1823,7 +1826,6 @@
\medskip
\begin{tabular}{l}
- \isa{val\ name{\isacharcolon}\ string} \\
\isa{type\ T} \\
\isa{val\ empty{\isacharcolon}\ T} \\
\isa{val\ merge{\isacharcolon}\ Pretty{\isachardot}pp\ {\isasymrightarrow}\ T\ {\isacharasterisk}\ T\ {\isasymrightarrow}\ T} \\
@@ -1832,8 +1834,6 @@
\begin{description}
- \item \isa{name} is a system-wide unique name identifying the data.
-
\item \isa{T} the type of data to store.
\item \isa{empty} initial (empty) data.
@@ -1856,7 +1856,6 @@
\medskip
\begin{tabular}{l}
- \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ theory} \\
\isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
\isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
\isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
@@ -1864,8 +1863,6 @@
\begin{description}
- \item \isa{init} initialization during theory setup.
-
\item \isa{get} retrieval of the current data.
\item \isa{change} update of current data (cached!)
@@ -1893,15 +1890,11 @@
\medskip
\begin{tabular}{l}
- \isa{val\ name{\isacharcolon}\ string} \\
\isa{val\ rewrites{\isacharcolon}\ theory\ {\isasymrightarrow}\ thm\ list}
\end{tabular}
\begin{description}
- \item \isa{name} is a system-wide unique name identifying
- this particular system of defining equations.
-
\item \isa{rewrites} specifies a set of theory-dependent
rewrite rules which are added to the preprocessor setup;
if no additional preprocessing is required, pass
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Wed May 30 21:09:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Wed May 30 21:09:13 2007 +0200
@@ -16,23 +16,9 @@
end; (*struct Nat*)
-structure Code_Generator =
-struct
-
-type 'a eq = {eq : 'a -> 'a -> bool};
-fun eq (A_:'a eq) = #eq A_;
-
-end; (*struct Code_Generator*)
-
structure List =
struct
-datatype nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 |
- Nibble5 | Nibble6 | Nibble7 | Nibble8 | Nibble9 | NibbleA | NibbleB |
- NibbleC | NibbleD | NibbleE | NibbleF;
-
-datatype char = Char of nibble * nibble;
-
fun zip xs (y :: ys) =
(case xs of [] => [] | z :: zs => (z, y) :: zip zs ys)
| zip xs [] = [];
@@ -40,274 +26,6 @@
fun null (x :: xs) = false
| null [] = true;
-fun eq_nibble Nibble0 Nibble0 = true
- | eq_nibble Nibble1 Nibble1 = true
- | eq_nibble Nibble2 Nibble2 = true
- | eq_nibble Nibble3 Nibble3 = true
- | eq_nibble Nibble4 Nibble4 = true
- | eq_nibble Nibble5 Nibble5 = true
- | eq_nibble Nibble6 Nibble6 = true
- | eq_nibble Nibble7 Nibble7 = true
- | eq_nibble Nibble8 Nibble8 = true
- | eq_nibble Nibble9 Nibble9 = true
- | eq_nibble NibbleA NibbleA = true
- | eq_nibble NibbleB NibbleB = true
- | eq_nibble NibbleC NibbleC = true
- | eq_nibble NibbleD NibbleD = true
- | eq_nibble NibbleE NibbleE = true
- | eq_nibble NibbleF NibbleF = true
- | eq_nibble Nibble0 Nibble1 = false
- | eq_nibble Nibble0 Nibble2 = false
- | eq_nibble Nibble0 Nibble3 = false
- | eq_nibble Nibble0 Nibble4 = false
- | eq_nibble Nibble0 Nibble5 = false
- | eq_nibble Nibble0 Nibble6 = false
- | eq_nibble Nibble0 Nibble7 = false
- | eq_nibble Nibble0 Nibble8 = false
- | eq_nibble Nibble0 Nibble9 = false
- | eq_nibble Nibble0 NibbleA = false
- | eq_nibble Nibble0 NibbleB = false
- | eq_nibble Nibble0 NibbleC = false
- | eq_nibble Nibble0 NibbleD = false
- | eq_nibble Nibble0 NibbleE = false
- | eq_nibble Nibble0 NibbleF = false
- | eq_nibble Nibble1 Nibble2 = false
- | eq_nibble Nibble1 Nibble3 = false
- | eq_nibble Nibble1 Nibble4 = false
- | eq_nibble Nibble1 Nibble5 = false
- | eq_nibble Nibble1 Nibble6 = false
- | eq_nibble Nibble1 Nibble7 = false
- | eq_nibble Nibble1 Nibble8 = false
- | eq_nibble Nibble1 Nibble9 = false
- | eq_nibble Nibble1 NibbleA = false
- | eq_nibble Nibble1 NibbleB = false
- | eq_nibble Nibble1 NibbleC = false
- | eq_nibble Nibble1 NibbleD = false
- | eq_nibble Nibble1 NibbleE = false
- | eq_nibble Nibble1 NibbleF = false
- | eq_nibble Nibble2 Nibble3 = false
- | eq_nibble Nibble2 Nibble4 = false
- | eq_nibble Nibble2 Nibble5 = false
- | eq_nibble Nibble2 Nibble6 = false
- | eq_nibble Nibble2 Nibble7 = false
- | eq_nibble Nibble2 Nibble8 = false
- | eq_nibble Nibble2 Nibble9 = false
- | eq_nibble Nibble2 NibbleA = false
- | eq_nibble Nibble2 NibbleB = false
- | eq_nibble Nibble2 NibbleC = false
- | eq_nibble Nibble2 NibbleD = false
- | eq_nibble Nibble2 NibbleE = false
- | eq_nibble Nibble2 NibbleF = false
- | eq_nibble Nibble3 Nibble4 = false
- | eq_nibble Nibble3 Nibble5 = false
- | eq_nibble Nibble3 Nibble6 = false
- | eq_nibble Nibble3 Nibble7 = false
- | eq_nibble Nibble3 Nibble8 = false
- | eq_nibble Nibble3 Nibble9 = false
- | eq_nibble Nibble3 NibbleA = false
- | eq_nibble Nibble3 NibbleB = false
- | eq_nibble Nibble3 NibbleC = false
- | eq_nibble Nibble3 NibbleD = false
- | eq_nibble Nibble3 NibbleE = false
- | eq_nibble Nibble3 NibbleF = false
- | eq_nibble Nibble4 Nibble5 = false
- | eq_nibble Nibble4 Nibble6 = false
- | eq_nibble Nibble4 Nibble7 = false
- | eq_nibble Nibble4 Nibble8 = false
- | eq_nibble Nibble4 Nibble9 = false
- | eq_nibble Nibble4 NibbleA = false
- | eq_nibble Nibble4 NibbleB = false
- | eq_nibble Nibble4 NibbleC = false
- | eq_nibble Nibble4 NibbleD = false
- | eq_nibble Nibble4 NibbleE = false
- | eq_nibble Nibble4 NibbleF = false
- | eq_nibble Nibble5 Nibble6 = false
- | eq_nibble Nibble5 Nibble7 = false
- | eq_nibble Nibble5 Nibble8 = false
- | eq_nibble Nibble5 Nibble9 = false
- | eq_nibble Nibble5 NibbleA = false
- | eq_nibble Nibble5 NibbleB = false
- | eq_nibble Nibble5 NibbleC = false
- | eq_nibble Nibble5 NibbleD = false
- | eq_nibble Nibble5 NibbleE = false
- | eq_nibble Nibble5 NibbleF = false
- | eq_nibble Nibble6 Nibble7 = false
- | eq_nibble Nibble6 Nibble8 = false
- | eq_nibble Nibble6 Nibble9 = false
- | eq_nibble Nibble6 NibbleA = false
- | eq_nibble Nibble6 NibbleB = false
- | eq_nibble Nibble6 NibbleC = false
- | eq_nibble Nibble6 NibbleD = false
- | eq_nibble Nibble6 NibbleE = false
- | eq_nibble Nibble6 NibbleF = false
- | eq_nibble Nibble7 Nibble8 = false
- | eq_nibble Nibble7 Nibble9 = false
- | eq_nibble Nibble7 NibbleA = false
- | eq_nibble Nibble7 NibbleB = false
- | eq_nibble Nibble7 NibbleC = false
- | eq_nibble Nibble7 NibbleD = false
- | eq_nibble Nibble7 NibbleE = false
- | eq_nibble Nibble7 NibbleF = false
- | eq_nibble Nibble8 Nibble9 = false
- | eq_nibble Nibble8 NibbleA = false
- | eq_nibble Nibble8 NibbleB = false
- | eq_nibble Nibble8 NibbleC = false
- | eq_nibble Nibble8 NibbleD = false
- | eq_nibble Nibble8 NibbleE = false
- | eq_nibble Nibble8 NibbleF = false
- | eq_nibble Nibble9 NibbleA = false
- | eq_nibble Nibble9 NibbleB = false
- | eq_nibble Nibble9 NibbleC = false
- | eq_nibble Nibble9 NibbleD = false
- | eq_nibble Nibble9 NibbleE = false
- | eq_nibble Nibble9 NibbleF = false
- | eq_nibble NibbleA NibbleB = false
- | eq_nibble NibbleA NibbleC = false
- | eq_nibble NibbleA NibbleD = false
- | eq_nibble NibbleA NibbleE = false
- | eq_nibble NibbleA NibbleF = false
- | eq_nibble NibbleB NibbleC = false
- | eq_nibble NibbleB NibbleD = false
- | eq_nibble NibbleB NibbleE = false
- | eq_nibble NibbleB NibbleF = false
- | eq_nibble NibbleC NibbleD = false
- | eq_nibble NibbleC NibbleE = false
- | eq_nibble NibbleC NibbleF = false
- | eq_nibble NibbleD NibbleE = false
- | eq_nibble NibbleD NibbleF = false
- | eq_nibble NibbleE NibbleF = false
- | eq_nibble Nibble1 Nibble0 = false
- | eq_nibble Nibble2 Nibble0 = false
- | eq_nibble Nibble3 Nibble0 = false
- | eq_nibble Nibble4 Nibble0 = false
- | eq_nibble Nibble5 Nibble0 = false
- | eq_nibble Nibble6 Nibble0 = false
- | eq_nibble Nibble7 Nibble0 = false
- | eq_nibble Nibble8 Nibble0 = false
- | eq_nibble Nibble9 Nibble0 = false
- | eq_nibble NibbleA Nibble0 = false
- | eq_nibble NibbleB Nibble0 = false
- | eq_nibble NibbleC Nibble0 = false
- | eq_nibble NibbleD Nibble0 = false
- | eq_nibble NibbleE Nibble0 = false
- | eq_nibble NibbleF Nibble0 = false
- | eq_nibble Nibble2 Nibble1 = false
- | eq_nibble Nibble3 Nibble1 = false
- | eq_nibble Nibble4 Nibble1 = false
- | eq_nibble Nibble5 Nibble1 = false
- | eq_nibble Nibble6 Nibble1 = false
- | eq_nibble Nibble7 Nibble1 = false
- | eq_nibble Nibble8 Nibble1 = false
- | eq_nibble Nibble9 Nibble1 = false
- | eq_nibble NibbleA Nibble1 = false
- | eq_nibble NibbleB Nibble1 = false
- | eq_nibble NibbleC Nibble1 = false
- | eq_nibble NibbleD Nibble1 = false
- | eq_nibble NibbleE Nibble1 = false
- | eq_nibble NibbleF Nibble1 = false
- | eq_nibble Nibble3 Nibble2 = false
- | eq_nibble Nibble4 Nibble2 = false
- | eq_nibble Nibble5 Nibble2 = false
- | eq_nibble Nibble6 Nibble2 = false
- | eq_nibble Nibble7 Nibble2 = false
- | eq_nibble Nibble8 Nibble2 = false
- | eq_nibble Nibble9 Nibble2 = false
- | eq_nibble NibbleA Nibble2 = false
- | eq_nibble NibbleB Nibble2 = false
- | eq_nibble NibbleC Nibble2 = false
- | eq_nibble NibbleD Nibble2 = false
- | eq_nibble NibbleE Nibble2 = false
- | eq_nibble NibbleF Nibble2 = false
- | eq_nibble Nibble4 Nibble3 = false
- | eq_nibble Nibble5 Nibble3 = false
- | eq_nibble Nibble6 Nibble3 = false
- | eq_nibble Nibble7 Nibble3 = false
- | eq_nibble Nibble8 Nibble3 = false
- | eq_nibble Nibble9 Nibble3 = false
- | eq_nibble NibbleA Nibble3 = false
- | eq_nibble NibbleB Nibble3 = false
- | eq_nibble NibbleC Nibble3 = false
- | eq_nibble NibbleD Nibble3 = false
- | eq_nibble NibbleE Nibble3 = false
- | eq_nibble NibbleF Nibble3 = false
- | eq_nibble Nibble5 Nibble4 = false
- | eq_nibble Nibble6 Nibble4 = false
- | eq_nibble Nibble7 Nibble4 = false
- | eq_nibble Nibble8 Nibble4 = false
- | eq_nibble Nibble9 Nibble4 = false
- | eq_nibble NibbleA Nibble4 = false
- | eq_nibble NibbleB Nibble4 = false
- | eq_nibble NibbleC Nibble4 = false
- | eq_nibble NibbleD Nibble4 = false
- | eq_nibble NibbleE Nibble4 = false
- | eq_nibble NibbleF Nibble4 = false
- | eq_nibble Nibble6 Nibble5 = false
- | eq_nibble Nibble7 Nibble5 = false
- | eq_nibble Nibble8 Nibble5 = false
- | eq_nibble Nibble9 Nibble5 = false
- | eq_nibble NibbleA Nibble5 = false
- | eq_nibble NibbleB Nibble5 = false
- | eq_nibble NibbleC Nibble5 = false
- | eq_nibble NibbleD Nibble5 = false
- | eq_nibble NibbleE Nibble5 = false
- | eq_nibble NibbleF Nibble5 = false
- | eq_nibble Nibble7 Nibble6 = false
- | eq_nibble Nibble8 Nibble6 = false
- | eq_nibble Nibble9 Nibble6 = false
- | eq_nibble NibbleA Nibble6 = false
- | eq_nibble NibbleB Nibble6 = false
- | eq_nibble NibbleC Nibble6 = false
- | eq_nibble NibbleD Nibble6 = false
- | eq_nibble NibbleE Nibble6 = false
- | eq_nibble NibbleF Nibble6 = false
- | eq_nibble Nibble8 Nibble7 = false
- | eq_nibble Nibble9 Nibble7 = false
- | eq_nibble NibbleA Nibble7 = false
- | eq_nibble NibbleB Nibble7 = false
- | eq_nibble NibbleC Nibble7 = false
- | eq_nibble NibbleD Nibble7 = false
- | eq_nibble NibbleE Nibble7 = false
- | eq_nibble NibbleF Nibble7 = false
- | eq_nibble Nibble9 Nibble8 = false
- | eq_nibble NibbleA Nibble8 = false
- | eq_nibble NibbleB Nibble8 = false
- | eq_nibble NibbleC Nibble8 = false
- | eq_nibble NibbleD Nibble8 = false
- | eq_nibble NibbleE Nibble8 = false
- | eq_nibble NibbleF Nibble8 = false
- | eq_nibble NibbleA Nibble9 = false
- | eq_nibble NibbleB Nibble9 = false
- | eq_nibble NibbleC Nibble9 = false
- | eq_nibble NibbleD Nibble9 = false
- | eq_nibble NibbleE Nibble9 = false
- | eq_nibble NibbleF Nibble9 = false
- | eq_nibble NibbleB NibbleA = false
- | eq_nibble NibbleC NibbleA = false
- | eq_nibble NibbleD NibbleA = false
- | eq_nibble NibbleE NibbleA = false
- | eq_nibble NibbleF NibbleA = false
- | eq_nibble NibbleC NibbleB = false
- | eq_nibble NibbleD NibbleB = false
- | eq_nibble NibbleE NibbleB = false
- | eq_nibble NibbleF NibbleB = false
- | eq_nibble NibbleD NibbleC = false
- | eq_nibble NibbleE NibbleC = false
- | eq_nibble NibbleF NibbleC = false
- | eq_nibble NibbleE NibbleD = false
- | eq_nibble NibbleF NibbleD = false
- | eq_nibble NibbleF NibbleE = false;
-
-fun eq_char (Char (nibble1, nibble2)) (Char (nibble1', nibble2')) =
- eq_nibble nibble1 nibble1' andalso eq_nibble nibble2 nibble2';
-
-val eq_chara = {eq = eq_char} : char Code_Generator.eq;
-
-fun eq_list A_ [] [] = true
- | eq_list A_ (a :: lista) (a' :: list') =
- Code_Generator.eq A_ a a' andalso eq_list A_ lista list'
- | eq_list A_ [] (a :: b) = false
- | eq_list A_ (a :: b) [] = false;
-
fun list_all p (x :: xs) = p x andalso list_all p xs
| list_all p [] = true;
@@ -327,10 +45,10 @@
structure Codegen =
struct
-datatype monotype = Mono of List.char list * monotype list;
+datatype monotype = Mono of Nat.nat * monotype list;
fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
- List.eq_list List.eq_chara tyco1 tyco2 andalso
+ Nat.eq_nat tyco1 tyco2 andalso
List.list_all2 eq_monotype typargs1 typargs2;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Wed May 30 21:09:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Wed May 30 21:09:13 2007 +0200
@@ -40,17 +40,6 @@
end; (*struct Nat*)
-structure List =
-struct
-
-datatype nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 |
- Nibble5 | Nibble6 | Nibble7 | Nibble8 | Nibble9 | NibbleA | NibbleB |
- NibbleC | NibbleD | NibbleE | NibbleF;
-
-datatype char = Char of nibble * nibble;
-
-end; (*struct List*)
-
structure Codegen =
struct
@@ -67,16 +56,16 @@
then Branch (Leaf (it, entry), it, Leaf (key, vala))
else Branch (Leaf (key, vala), it, Leaf (it, entry))));
-fun example n =
+val example : (Nat.nat, (Nat.nat list)) searchtree =
update (Nat.eq_nata, Nat.ord_nat)
- (n, [List.Char (List.Nibble6, List.Nibble2),
- List.Char (List.Nibble6, List.Nibble1),
- List.Char (List.Nibble7, List.Nibble2)])
- (Leaf
- (Nat.Zero_nat,
- [List.Char (List.Nibble6, List.Nibble6),
- List.Char (List.Nibble6, List.NibbleF),
- List.Char (List.Nibble6, List.NibbleF)]));
+ (Nat.Suc (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))),
+ [Nat.Suc (Nat.Suc Nat.Zero_nat), Nat.Suc (Nat.Suc Nat.Zero_nat)])
+ (update (Nat.eq_nata, Nat.ord_nat)
+ (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat)),
+ [Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))])
+ (update (Nat.eq_nata, Nat.ord_nat)
+ (Nat.Suc (Nat.Suc Nat.Zero_nat), [Nat.Suc (Nat.Suc Nat.Zero_nat)])
+ (Leaf (Nat.Suc Nat.Zero_nat, []))));
end; (*struct Codegen*)
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Wed May 30 21:09:12 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Wed May 30 21:09:13 2007 +0200
@@ -185,8 +185,8 @@
"+" > HOL.plus_class.plus :: "[nat,nat]=>nat"
"*" > HOL.times_class.times :: "[nat,nat]=>nat"
"-" > HOL.minus_class.minus :: "[nat,nat]=>nat"
- MIN > Orderings.min :: "[nat,nat]=>nat"
- MAX > Orderings.max :: "[nat,nat]=>nat"
+ MIN > Orderings.ord_class.min :: "[nat,nat]=>nat"
+ MAX > Orderings.ord_class.max :: "[nat,nat]=>nat"
DIV > Divides.div_class.div :: "[nat,nat]=>nat"
MOD > Divides.div_class.mod :: "[nat,nat]=>nat"
EXP > Nat.power_class.power :: "[nat,nat]=>nat";
--- a/src/HOL/Import/HOL/arithmetic.imp Wed May 30 21:09:12 2007 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp Wed May 30 21:09:13 2007 +0200
@@ -14,8 +14,8 @@
"NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2"
"NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1"
"NUMERAL" > "HOL4Compat.NUMERAL"
- "MIN" > "Orderings.min" :: "nat => nat => nat"
- "MAX" > "Orderings.max" :: "nat => nat => nat"
+ "MIN" > "Orderings.ord_class.min" :: "nat => nat => nat"
+ "MAX" > "Orderings.ord_class.max" :: "nat => nat => nat"
"FUNPOW" > "HOL4Compat.FUNPOW"
"EXP" > "Nat.power_class.power" :: "nat => nat => nat"
"DIV" > "Divides.div_class.div" :: "nat => nat => nat"