# HG changeset patch # User haftmann # Date 1180552153 -7200 # Node ID ae52b82dc5d88c3dbba463e7e5b1adeed05d2474 # Parent 29e9139509281083146513f2683ca7a7085d719b updated diff -r 29e913950928 -r ae52b82dc5d8 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- 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 diff -r 29e913950928 -r ae52b82dc5d8 doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML --- 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*) diff -r 29e913950928 -r ae52b82dc5d8 doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML --- 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*) diff -r 29e913950928 -r ae52b82dc5d8 src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- 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"; diff -r 29e913950928 -r ae52b82dc5d8 src/HOL/Import/HOL/arithmetic.imp --- 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"