added new code_datatype example
authorhaftmann
Wed May 28 11:05:47 2008 +0200 (2008-05-28)
changeset 26999284c871d3acb
parent 26998 2c4032d59586
child 27000 e8a40d8b7897
added new code_datatype example
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
doc-src/IsarAdvanced/Codegen/Thy/examples/nat_binary.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML
     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.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*)