author haftmann Wed May 28 11:05:47 2008 +0200 (2008-05-28) changeset 26999 284c871d3acb parent 26998 2c4032d59586 child 27000 e8a40d8b7897
     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 +definition Dig0 :: "nat \<Rightarrow> nat" where
1.25 +  "Dig0 n = 2 * n"
1.26 +
1.27 +definition Dig1 :: "nat \<Rightarrow> nat" where
1.28 +  "Dig1 n = Suc (2 * n)"
1.29 +
1.30 +text {*
1.31 +  \noindent We will use these two ">digits"< to represent natural numbers
1.32 +  in binary digits, e.g.:
1.33 +*}
1.34 +
1.35 +lemma 42: "42 = Dig0 (Dig1 (Dig0 (Dig1 (Dig0 1))))"
1.36 +  by (simp add: Dig0_def Dig1_def)
1.37 +
1.38 +text {*
1.39 +  \noindent Of course we also have to provide proper code equations for
1.40 +  the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
1.41  *}
1.42
1.43 -(* {* code_datatype ... *}
1.44 +lemma plus_Dig [code func]:
1.45 +  "0 + n = n"
1.46 +  "m + 0 = m"
1.47 +  "1 + Dig0 n = Dig1 n"
1.48 +  "Dig0 m + 1 = Dig1 m"
1.49 +  "1 + Dig1 n = Dig0 (n + 1)"
1.50 +  "Dig1 m + 1 = Dig0 (m + 1)"
1.51 +  "Dig0 m + Dig0 n = Dig0 (m + n)"
1.52 +  "Dig0 m + Dig1 n = Dig1 (m + n)"
1.53 +  "Dig1 m + Dig0 n = Dig1 (m + n)"
1.54 +  "Dig1 m + Dig1 n = Dig0 (m + n + 1)"
1.55 +  by (simp_all add: Dig0_def Dig1_def)
1.56 +
1.57 +text {*
1.58 +  \noindent We then instruct the code generator to view @{term "0\<Colon>nat"},
1.59 +  @{term "1\<Colon>nat"}, @{term Dig0} and @{term Dig1} as
1.60 +  datatype constructors:
1.61 +*}
1.62 +
1.63 +code_datatype "0\<Colon>nat" "1\<Colon>nat" Dig0 Dig1
1.64
1.65 -   {* export_code "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML" *}
1.66 +text {*
1.67 +  \noindent For the former constructor @{term Suc}, we provide a code
1.68 +  equation and remove some parts of the default code generator setup
1.69 +  which are an obstacle here:
1.70 +*}
1.71 +
1.72 +lemma Suc_Dig [code func]:
1.73 +  "Suc n = n + 1"
1.74 +  by simp
1.75
1.76 -  {* \lstsml{Thy/examples/set_list.ML} *} *)
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.18 +\isanewline
2.19 +\isacommand{definition}\isamarkupfalse%
2.20 +\ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
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.29 +%
2.31 +\ \ %
2.33 +%
2.34 +\isatagproof
2.35 +\isacommand{by}\isamarkupfalse%
2.37 +\endisatagproof
2.38 +{\isafoldproof}%
2.39 +%
2.41 +%
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.61 +%
2.63 +\ \ %
2.65 +%
2.66 +\isatagproof
2.67 +\isacommand{by}\isamarkupfalse%
2.69 +\endisatagproof
2.70 +{\isafoldproof}%
2.71 +%
2.73 +%
2.75 +%
2.76 +\begin{isamarkuptext}%
2.77 +\noindent We then instruct the code generator to view \isa{{\isadigit{0}}},
2.79 +  datatype constructors:%
2.80 +\end{isamarkuptext}%
2.81 +\isamarkuptrue%
2.82 +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
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.95 +\ \ %
2.97 +%
2.98 +\isatagproof
2.99 +\isacommand{by}\isamarkupfalse%
2.100 +\ simp%
2.101 +\endisatagproof
2.102 +{\isafoldproof}%
2.103 +%
2.105 +\isanewline
2.106 +%
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.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.150 +%
2.152 +%
2.153 +\isataginvisible
2.154 +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
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.169 +%
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*)