--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Mon May 26 17:55:39 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Wed May 28 11:05:47 2008 +0200
@@ -147,7 +147,7 @@
\noindent Then we generate code
*}
-export_code example (*<*)in SML(*>*)in SML file "examples/tree.ML"
+export_code example (*<*)in SML (*>*)in SML file "examples/tree.ML"
text {*
\noindent which looks like:
@@ -762,22 +762,102 @@
the @{text "\<PRINTCODESETUP>"} command.
In some cases, it may be convenient to alter or
- extend this table; as an example FIXME
+ extend this table; as an example, we will develope an alternative
+ representation of natural numbers as binary digits, whose
+ size does increase logarithmically with its value, not linear
+ \footnote{Indeed, the @{text "Efficient_Nat"} theory \ref{eff_nat}
+ does something similar}. First, the digit representation:
+*}
+
+definition Dig0 :: "nat \<Rightarrow> nat" where
+ "Dig0 n = 2 * n"
+
+definition Dig1 :: "nat \<Rightarrow> nat" where
+ "Dig1 n = Suc (2 * n)"
+
+text {*
+ \noindent We will use these two ">digits"< to represent natural numbers
+ in binary digits, e.g.:
+*}
+
+lemma 42: "42 = Dig0 (Dig1 (Dig0 (Dig1 (Dig0 1))))"
+ by (simp add: Dig0_def Dig1_def)
+
+text {*
+ \noindent Of course we also have to provide proper code equations for
+ the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
*}
-(* {* code_datatype ... *}
+lemma plus_Dig [code func]:
+ "0 + n = n"
+ "m + 0 = m"
+ "1 + Dig0 n = Dig1 n"
+ "Dig0 m + 1 = Dig1 m"
+ "1 + Dig1 n = Dig0 (n + 1)"
+ "Dig1 m + 1 = Dig0 (m + 1)"
+ "Dig0 m + Dig0 n = Dig0 (m + n)"
+ "Dig0 m + Dig1 n = Dig1 (m + n)"
+ "Dig1 m + Dig0 n = Dig1 (m + n)"
+ "Dig1 m + Dig1 n = Dig0 (m + n + 1)"
+ by (simp_all add: Dig0_def Dig1_def)
+
+text {*
+ \noindent We then instruct the code generator to view @{term "0\<Colon>nat"},
+ @{term "1\<Colon>nat"}, @{term Dig0} and @{term Dig1} as
+ datatype constructors:
+*}
+
+code_datatype "0\<Colon>nat" "1\<Colon>nat" Dig0 Dig1
- {* export_code "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML" *}
+text {*
+ \noindent For the former constructor @{term Suc}, we provide a code
+ equation and remove some parts of the default code generator setup
+ which are an obstacle here:
+*}
+
+lemma Suc_Dig [code func]:
+ "Suc n = n + 1"
+ by simp
- {* \lstsml{Thy/examples/set_list.ML} *} *)
+declare One_nat_def [code inline del]
+declare add_Suc_shift [code func del]
+
+text {*
+ \noindent This yields the following code:
+*}
+
+export_code "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" (*<*)in SML(*>*) in SML file "examples/nat_binary.ML"
+
+text {* \lstsml{Thy/examples/nat_binary.ML} *}
text {*
\medskip
- Changing the representation of existing datatypes requires
- some care with respect to pattern matching and such.
+ From this example, it can be easily glimpsed that using own constructor sets
+ is a little delicate since it changes the set of valid patterns for values
+ of that type. Without going into much detail, here some practical hints:
+
+ \begin{itemize}
+ \item When changing the constuctor set for datatypes, take care to
+ provide an alternative for the @{text case} combinator (e.g. by replacing
+ it using the preprocessor).
+ \item Values in the target language need not to be normalized -- different
+ values in the target language may represent the same value in the
+ logic (e.g. @{text "Dig1 0 = 1"}).
+ \item Usually, a good methodology to deal with the subleties of pattern
+ matching is to see the type as an abstract type: provide a set
+ of operations which operate on the concrete representation of the type,
+ and derive further operations by combinations of these primitive ones,
+ without relying on a particular representation.
+ \end{itemize}
*}
+code_datatype %invisible "0::nat" Suc
+declare %invisible plus_Dig [code func del]
+declare %invisible One_nat_def [code inline]
+declare %invisible add_Suc_shift [code func]
+lemma %invisible [code func]: "0 + n = (n \<Colon> nat)" by simp
+
subsection {* Customizing serialization *}
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Mon May 26 17:55:39 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed May 28 11:05:47 2008 +0200
@@ -993,18 +993,168 @@
the \isa{{\isasymPRINTCODESETUP}} command.
In some cases, it may be convenient to alter or
- extend this table; as an example FIXME%
+ extend this table; as an example, we will develope an alternative
+ representation of natural numbers as binary digits, whose
+ size does increase logarithmically with its value, not linear
+ \footnote{Indeed, the \isa{Efficient{\isacharunderscore}Nat} theory \ref{eff_nat}
+ does something similar}. First, the digit representation:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent We will use these two ">digits"< to represent natural numbers
+ in binary digits, e.g.:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isadigit{4}}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent Of course we also have to provide proper code equations for
+ the operations, e.g. \isa{op\ {\isacharplus}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{1}}\ m{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent We then instruct the code generator to view \isa{{\isadigit{0}}},
+ \isa{{\isadigit{1}}}, \isa{Dig{\isadigit{0}}} and \isa{Dig{\isadigit{1}}} as
+ datatype constructors:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isadigit{0}}{\isasymColon}nat{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isasymColon}nat{\isachardoublequoteclose}\ Dig{\isadigit{0}}\ Dig{\isadigit{1}}%
+\begin{isamarkuptext}%
+\noindent For the former constructor \isa{Suc}, we provide a code
+ equation and remove some parts of the default code generator setup
+ which are an obstacle here:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}%
+\begin{isamarkuptext}%
+\noindent This yields the following code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ {\isacharplus}\ {\isasymColon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}nat{\isacharunderscore}binary{\isachardot}ML{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/nat_binary.ML}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
\medskip
- Changing the representation of existing datatypes requires
- some care with respect to pattern matching and such.%
+ From this example, it can be easily glimpsed that using own constructor sets
+ is a little delicate since it changes the set of valid patterns for values
+ of that type. Without going into much detail, here some practical hints:
+
+ \begin{itemize}
+ \item When changing the constuctor set for datatypes, take care to
+ provide an alternative for the \isa{case} combinator (e.g. by replacing
+ it using the preprocessor).
+ \item Values in the target language need not to be normalized -- different
+ values in the target language may represent the same value in the
+ logic (e.g. \isa{Dig{\isadigit{1}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}}).
+ \item Usually, a good methodology to deal with the subleties of pattern
+ matching is to see the type as an abstract type: provide a set
+ of operations which operate on the concrete representation of the type,
+ and derive further operations by combinations of these primitive ones,
+ without relying on a particular representation.
+ \end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
\isamarkupsubsection{Customizing serialization%
}
\isamarkuptrue%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/nat_binary.ML Wed May 28 11:05:47 2008 +0200
@@ -0,0 +1,17 @@
+structure Nat =
+struct
+
+datatype nat = Dig1 of nat | Dig0 of nat | One_nat | Zero_nat;
+
+fun plus_nat (Dig1 m) (Dig1 n) = Dig0 (plus_nat (plus_nat m n) One_nat)
+ | plus_nat (Dig1 m) (Dig0 n) = Dig1 (plus_nat m n)
+ | plus_nat (Dig0 m) (Dig1 n) = Dig1 (plus_nat m n)
+ | plus_nat (Dig0 m) (Dig0 n) = Dig0 (plus_nat m n)
+ | plus_nat (Dig1 m) One_nat = Dig0 (plus_nat m One_nat)
+ | plus_nat One_nat (Dig1 n) = Dig0 (plus_nat n One_nat)
+ | plus_nat (Dig0 m) One_nat = Dig1 m
+ | plus_nat One_nat (Dig0 n) = Dig1 n
+ | plus_nat m Zero_nat = m
+ | plus_nat Zero_nat n = n;
+
+end; (*struct Nat*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Mon May 26 17:55:39 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-structure HOL =
-struct
-
-type 'a eq = {eq : 'a -> 'a -> bool};
-fun eq (A_:'a eq) = #eq A_;
-
-fun eqop A_ a = eq A_ a;
-
-end; (*struct HOL*)
-
-structure List =
-struct
-
-fun foldr f (x :: xs) a = f x (foldr f xs a)
- | foldr f [] a = a;
-
-fun member A_ x (y :: ys) =
- (if HOL.eqop A_ y x then true else member A_ x ys)
- | member A_ x [] = false;
-
-end; (*struct List*)
-
-structure Set =
-struct
-
-datatype 'a set = Set of 'a list;
-
-val empty : 'a set = Set [];
-
-fun insert x (Set xs) = Set (x :: xs);
-
-fun uniona xs (Set ys) = List.foldr insert ys xs;
-
-fun member A_ x (Set xs) = List.member A_ x xs;
-
-fun unionaa (Set xs) = List.foldr uniona xs empty;
-
-end; (*struct Set*)