1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Mon May 26 17:55:39 2008 +0200
1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Wed May 28 11:05:47 2008 +0200
1.3 @@ -147,7 +147,7 @@
1.4 \noindent Then we generate code
1.5 *}
1.6
1.7 -export_code example (*<*)in SML(*>*)in SML file "examples/tree.ML"
1.8 +export_code example (*<*)in SML (*>*)in SML file "examples/tree.ML"
1.9
1.10 text {*
1.11 \noindent which looks like:
1.12 @@ -762,22 +762,102 @@
1.13 the @{text "\<PRINTCODESETUP>"} command.
1.14
1.15 In some cases, it may be convenient to alter or
1.16 - extend this table; as an example FIXME
1.17 + extend this table; as an example, we will develope an alternative
1.18 + representation of natural numbers as binary digits, whose
1.19 + size does increase logarithmically with its value, not linear
1.20 + \footnote{Indeed, the @{text "Efficient_Nat"} theory \ref{eff_nat}
1.21 + does something similar}. First, the digit representation:
1.22 *}
1.23
1.24 -(* {* code_datatype ... *}
1.25 +definition Dig0 :: "nat \<Rightarrow> nat" where
1.26 + "Dig0 n = 2 * n"
1.27
1.28 - {* export_code "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML" *}
1.29 +definition Dig1 :: "nat \<Rightarrow> nat" where
1.30 + "Dig1 n = Suc (2 * n)"
1.31
1.32 - {* \lstsml{Thy/examples/set_list.ML} *} *)
1.33 +text {*
1.34 + \noindent We will use these two ">digits"< to represent natural numbers
1.35 + in binary digits, e.g.:
1.36 +*}
1.37 +
1.38 +lemma 42: "42 = Dig0 (Dig1 (Dig0 (Dig1 (Dig0 1))))"
1.39 + by (simp add: Dig0_def Dig1_def)
1.40 +
1.41 +text {*
1.42 + \noindent Of course we also have to provide proper code equations for
1.43 + the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
1.44 +*}
1.45 +
1.46 +lemma plus_Dig [code func]:
1.47 + "0 + n = n"
1.48 + "m + 0 = m"
1.49 + "1 + Dig0 n = Dig1 n"
1.50 + "Dig0 m + 1 = Dig1 m"
1.51 + "1 + Dig1 n = Dig0 (n + 1)"
1.52 + "Dig1 m + 1 = Dig0 (m + 1)"
1.53 + "Dig0 m + Dig0 n = Dig0 (m + n)"
1.54 + "Dig0 m + Dig1 n = Dig1 (m + n)"
1.55 + "Dig1 m + Dig0 n = Dig1 (m + n)"
1.56 + "Dig1 m + Dig1 n = Dig0 (m + n + 1)"
1.57 + by (simp_all add: Dig0_def Dig1_def)
1.58 +
1.59 +text {*
1.60 + \noindent We then instruct the code generator to view @{term "0\<Colon>nat"},
1.61 + @{term "1\<Colon>nat"}, @{term Dig0} and @{term Dig1} as
1.62 + datatype constructors:
1.63 +*}
1.64 +
1.65 +code_datatype "0\<Colon>nat" "1\<Colon>nat" Dig0 Dig1
1.66 +
1.67 +text {*
1.68 + \noindent For the former constructor @{term Suc}, we provide a code
1.69 + equation and remove some parts of the default code generator setup
1.70 + which are an obstacle here:
1.71 +*}
1.72 +
1.73 +lemma Suc_Dig [code func]:
1.74 + "Suc n = n + 1"
1.75 + by simp
1.76 +
1.77 +declare One_nat_def [code inline del]
1.78 +declare add_Suc_shift [code func del]
1.79 +
1.80 +text {*
1.81 + \noindent This yields the following code:
1.82 +*}
1.83 +
1.84 +export_code "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" (*<*)in SML(*>*) in SML file "examples/nat_binary.ML"
1.85 +
1.86 +text {* \lstsml{Thy/examples/nat_binary.ML} *}
1.87
1.88 text {*
1.89 \medskip
1.90
1.91 - Changing the representation of existing datatypes requires
1.92 - some care with respect to pattern matching and such.
1.93 + From this example, it can be easily glimpsed that using own constructor sets
1.94 + is a little delicate since it changes the set of valid patterns for values
1.95 + of that type. Without going into much detail, here some practical hints:
1.96 +
1.97 + \begin{itemize}
1.98 + \item When changing the constuctor set for datatypes, take care to
1.99 + provide an alternative for the @{text case} combinator (e.g. by replacing
1.100 + it using the preprocessor).
1.101 + \item Values in the target language need not to be normalized -- different
1.102 + values in the target language may represent the same value in the
1.103 + logic (e.g. @{text "Dig1 0 = 1"}).
1.104 + \item Usually, a good methodology to deal with the subleties of pattern
1.105 + matching is to see the type as an abstract type: provide a set
1.106 + of operations which operate on the concrete representation of the type,
1.107 + and derive further operations by combinations of these primitive ones,
1.108 + without relying on a particular representation.
1.109 + \end{itemize}
1.110 *}
1.111
1.112 +code_datatype %invisible "0::nat" Suc
1.113 +declare %invisible plus_Dig [code func del]
1.114 +declare %invisible One_nat_def [code inline]
1.115 +declare %invisible add_Suc_shift [code func]
1.116 +lemma %invisible [code func]: "0 + n = (n \<Colon> nat)" by simp
1.117 +
1.118
1.119 subsection {* Customizing serialization *}
1.120
2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Mon May 26 17:55:39 2008 +0200
2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed May 28 11:05:47 2008 +0200
2.3 @@ -993,18 +993,168 @@
2.4 the \isa{{\isasymPRINTCODESETUP}} command.
2.5
2.6 In some cases, it may be convenient to alter or
2.7 - extend this table; as an example FIXME%
2.8 + extend this table; as an example, we will develope an alternative
2.9 + representation of natural numbers as binary digits, whose
2.10 + size does increase logarithmically with its value, not linear
2.11 + \footnote{Indeed, the \isa{Efficient{\isacharunderscore}Nat} theory \ref{eff_nat}
2.12 + does something similar}. First, the digit representation:%
2.13 +\end{isamarkuptext}%
2.14 +\isamarkuptrue%
2.15 +\isacommand{definition}\isamarkupfalse%
2.16 +\ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.17 +\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline
2.18 +\isanewline
2.19 +\isacommand{definition}\isamarkupfalse%
2.20 +\ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.21 +\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}%
2.22 +\begin{isamarkuptext}%
2.23 +\noindent We will use these two ">digits"< to represent natural numbers
2.24 + in binary digits, e.g.:%
2.25 +\end{isamarkuptext}%
2.26 +\isamarkuptrue%
2.27 +\isacommand{lemma}\isamarkupfalse%
2.28 +\ {\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
2.29 +%
2.30 +\isadelimproof
2.31 +\ \ %
2.32 +\endisadelimproof
2.33 +%
2.34 +\isatagproof
2.35 +\isacommand{by}\isamarkupfalse%
2.36 +\ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
2.37 +\endisatagproof
2.38 +{\isafoldproof}%
2.39 +%
2.40 +\isadelimproof
2.41 +%
2.42 +\endisadelimproof
2.43 +%
2.44 +\begin{isamarkuptext}%
2.45 +\noindent Of course we also have to provide proper code equations for
2.46 + the operations, e.g. \isa{op\ {\isacharplus}}:%
2.47 +\end{isamarkuptext}%
2.48 +\isamarkuptrue%
2.49 +\isacommand{lemma}\isamarkupfalse%
2.50 +\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
2.51 +\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
2.52 +\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
2.53 +\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
2.54 +\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{1}}\ m{\isachardoublequoteclose}\isanewline
2.55 +\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.56 +\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.57 +\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.58 +\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.59 +\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.60 +\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.61 +%
2.62 +\isadelimproof
2.63 +\ \ %
2.64 +\endisadelimproof
2.65 +%
2.66 +\isatagproof
2.67 +\isacommand{by}\isamarkupfalse%
2.68 +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
2.69 +\endisatagproof
2.70 +{\isafoldproof}%
2.71 +%
2.72 +\isadelimproof
2.73 +%
2.74 +\endisadelimproof
2.75 +%
2.76 +\begin{isamarkuptext}%
2.77 +\noindent We then instruct the code generator to view \isa{{\isadigit{0}}},
2.78 + \isa{{\isadigit{1}}}, \isa{Dig{\isadigit{0}}} and \isa{Dig{\isadigit{1}}} as
2.79 + datatype constructors:%
2.80 +\end{isamarkuptext}%
2.81 +\isamarkuptrue%
2.82 +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
2.83 +\ {\isachardoublequoteopen}{\isadigit{0}}{\isasymColon}nat{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isasymColon}nat{\isachardoublequoteclose}\ Dig{\isadigit{0}}\ Dig{\isadigit{1}}%
2.84 +\begin{isamarkuptext}%
2.85 +\noindent For the former constructor \isa{Suc}, we provide a code
2.86 + equation and remove some parts of the default code generator setup
2.87 + which are an obstacle here:%
2.88 +\end{isamarkuptext}%
2.89 +\isamarkuptrue%
2.90 +\isacommand{lemma}\isamarkupfalse%
2.91 +\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
2.92 +\ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
2.93 +%
2.94 +\isadelimproof
2.95 +\ \ %
2.96 +\endisadelimproof
2.97 +%
2.98 +\isatagproof
2.99 +\isacommand{by}\isamarkupfalse%
2.100 +\ simp%
2.101 +\endisatagproof
2.102 +{\isafoldproof}%
2.103 +%
2.104 +\isadelimproof
2.105 +\isanewline
2.106 +%
2.107 +\endisadelimproof
2.108 +\isanewline
2.109 +\isacommand{declare}\isamarkupfalse%
2.110 +\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
2.111 +\isacommand{declare}\isamarkupfalse%
2.112 +\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}%
2.113 +\begin{isamarkuptext}%
2.114 +\noindent This yields the following code:%
2.115 +\end{isamarkuptext}%
2.116 +\isamarkuptrue%
2.117 +\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
2.118 +\ {\isachardoublequoteopen}op\ {\isacharplus}\ {\isasymColon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}nat{\isacharunderscore}binary{\isachardot}ML{\isachardoublequoteclose}%
2.119 +\begin{isamarkuptext}%
2.120 +\lstsml{Thy/examples/nat_binary.ML}%
2.121 \end{isamarkuptext}%
2.122 \isamarkuptrue%
2.123 %
2.124 \begin{isamarkuptext}%
2.125 \medskip
2.126
2.127 - Changing the representation of existing datatypes requires
2.128 - some care with respect to pattern matching and such.%
2.129 + From this example, it can be easily glimpsed that using own constructor sets
2.130 + is a little delicate since it changes the set of valid patterns for values
2.131 + of that type. Without going into much detail, here some practical hints:
2.132 +
2.133 + \begin{itemize}
2.134 + \item When changing the constuctor set for datatypes, take care to
2.135 + provide an alternative for the \isa{case} combinator (e.g. by replacing
2.136 + it using the preprocessor).
2.137 + \item Values in the target language need not to be normalized -- different
2.138 + values in the target language may represent the same value in the
2.139 + logic (e.g. \isa{Dig{\isadigit{1}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}}).
2.140 + \item Usually, a good methodology to deal with the subleties of pattern
2.141 + matching is to see the type as an abstract type: provide a set
2.142 + of operations which operate on the concrete representation of the type,
2.143 + and derive further operations by combinations of these primitive ones,
2.144 + without relying on a particular representation.
2.145 + \end{itemize}%
2.146 \end{isamarkuptext}%
2.147 \isamarkuptrue%
2.148 %
2.149 +\isadeliminvisible
2.150 +%
2.151 +\endisadeliminvisible
2.152 +%
2.153 +\isataginvisible
2.154 +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
2.155 +\ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
2.156 +\isacommand{declare}\isamarkupfalse%
2.157 +\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline
2.158 +\isacommand{declare}\isamarkupfalse%
2.159 +\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
2.160 +\isacommand{declare}\isamarkupfalse%
2.161 +\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline
2.162 +\isacommand{lemma}\isamarkupfalse%
2.163 +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
2.164 +\ simp%
2.165 +\endisataginvisible
2.166 +{\isafoldinvisible}%
2.167 +%
2.168 +\isadeliminvisible
2.169 +%
2.170 +\endisadeliminvisible
2.171 +%
2.172 \isamarkupsubsection{Customizing serialization%
2.173 }
2.174 \isamarkuptrue%
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/nat_binary.ML Wed May 28 11:05:47 2008 +0200
3.3 @@ -0,0 +1,17 @@
3.4 +structure Nat =
3.5 +struct
3.6 +
3.7 +datatype nat = Dig1 of nat | Dig0 of nat | One_nat | Zero_nat;
3.8 +
3.9 +fun plus_nat (Dig1 m) (Dig1 n) = Dig0 (plus_nat (plus_nat m n) One_nat)
3.10 + | plus_nat (Dig1 m) (Dig0 n) = Dig1 (plus_nat m n)
3.11 + | plus_nat (Dig0 m) (Dig1 n) = Dig1 (plus_nat m n)
3.12 + | plus_nat (Dig0 m) (Dig0 n) = Dig0 (plus_nat m n)
3.13 + | plus_nat (Dig1 m) One_nat = Dig0 (plus_nat m One_nat)
3.14 + | plus_nat One_nat (Dig1 n) = Dig0 (plus_nat n One_nat)
3.15 + | plus_nat (Dig0 m) One_nat = Dig1 m
3.16 + | plus_nat One_nat (Dig0 n) = Dig1 n
3.17 + | plus_nat m Zero_nat = m
3.18 + | plus_nat Zero_nat n = n;
3.19 +
3.20 +end; (*struct Nat*)
4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Mon May 26 17:55:39 2008 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,38 +0,0 @@
4.4 -structure HOL =
4.5 -struct
4.6 -
4.7 -type 'a eq = {eq : 'a -> 'a -> bool};
4.8 -fun eq (A_:'a eq) = #eq A_;
4.9 -
4.10 -fun eqop A_ a = eq A_ a;
4.11 -
4.12 -end; (*struct HOL*)
4.13 -
4.14 -structure List =
4.15 -struct
4.16 -
4.17 -fun foldr f (x :: xs) a = f x (foldr f xs a)
4.18 - | foldr f [] a = a;
4.19 -
4.20 -fun member A_ x (y :: ys) =
4.21 - (if HOL.eqop A_ y x then true else member A_ x ys)
4.22 - | member A_ x [] = false;
4.23 -
4.24 -end; (*struct List*)
4.25 -
4.26 -structure Set =
4.27 -struct
4.28 -
4.29 -datatype 'a set = Set of 'a list;
4.30 -
4.31 -val empty : 'a set = Set [];
4.32 -
4.33 -fun insert x (Set xs) = Set (x :: xs);
4.34 -
4.35 -fun uniona xs (Set ys) = List.foldr insert ys xs;
4.36 -
4.37 -fun member A_ x (Set xs) = List.member A_ x xs;
4.38 -
4.39 -fun unionaa (Set xs) = List.foldr uniona xs empty;
4.40 -
4.41 -end; (*struct Set*)