updated doc
authorhaftmann
Thu Apr 26 13:32:55 2007 +0200 (2007-04-26)
changeset 22798e3962371f568
parent 22797 4b77a43f7f58
child 22799 ed7d53db2170
updated doc
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml
doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML
doc-src/IsarAdvanced/Codegen/codegen.tex
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Apr 26 12:00:12 2007 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Apr 26 13:32:55 2007 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4    \emph{type classes}. A defining equation as a first approximation
     1.5    is a theorem of the form @{text "f t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n \<equiv> t"}
     1.6    (an equation headed by a constant @{text f} with arguments
     1.7 -  @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}.
     1.8 +  @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}).
     1.9    Code generation aims to turn defining equations
    1.10    into a functional program by running through
    1.11    a process (see figure \ref{fig:process}):
    1.12 @@ -245,15 +245,12 @@
    1.13    a defining equation (e.g.~the Hilbert choice
    1.14    operation @{text "SOME"}):
    1.15  *}
    1.16 -
    1.17  (*<*)
    1.18  setup {* Sign.add_path "foo" *}
    1.19  (*>*)
    1.20 -
    1.21  definition
    1.22    pick_some :: "'a list \<Rightarrow> 'a" where
    1.23    "pick_some xs = (SOME x. x \<in> set xs)"
    1.24 -
    1.25  (*<*)
    1.26  hide const pick_some
    1.27  
    1.28 @@ -263,7 +260,6 @@
    1.29    pick_some :: "'a list \<Rightarrow> 'a" where
    1.30    "pick_some = hd"
    1.31  (*>*)
    1.32 -
    1.33  code_gen pick_some (SML "examples/fail_const.ML")
    1.34  
    1.35  text {* \noindent will fail. *}
    1.36 @@ -285,7 +281,7 @@
    1.37    The typical HOL tools are already set up in a way that
    1.38    function definitions introduced by @{text "\<DEFINITION>"},
    1.39    @{text "\<FUN>"},
    1.40 -  @{text "\<FUNCTION>"}, @{text "\<PRIMREC>"}
    1.41 +  @{text "\<FUNCTION>"}, @{text "\<PRIMREC>"},
    1.42    @{text "\<RECDEF>"} are implicitly propagated
    1.43    to this defining equation table. Specific theorems may be
    1.44    selected using an attribute: \emph{code func}. As example,
    1.45 @@ -300,7 +296,7 @@
    1.46      if n < k then v else pick xs (n - k))"
    1.47  
    1.48  text {*
    1.49 -  We want to eliminate the explicit destruction
    1.50 +  \noindent We want to eliminate the explicit destruction
    1.51    of @{term x} to @{term "(k, v)"}:
    1.52  *}
    1.53  
    1.54 @@ -311,11 +307,11 @@
    1.55  code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick1.ML")
    1.56  
    1.57  text {*
    1.58 -  This theorem is now added to the defining equation table:
    1.59 +  \noindent This theorem now is used for generating code:
    1.60  
    1.61    \lstsml{Thy/examples/pick1.ML}
    1.62  
    1.63 -  It might be convenient to remove the pointless original
    1.64 +  \noindent It might be convenient to remove the pointless original
    1.65    equation, using the \emph{nofunc} attribute:
    1.66  *}
    1.67  
    1.68 @@ -326,7 +322,7 @@
    1.69  text {*
    1.70    \lstsml{Thy/examples/pick2.ML}
    1.71  
    1.72 -  Syntactic redundancies are implicitly dropped. For example,
    1.73 +  \noindent Syntactic redundancies are implicitly dropped. For example,
    1.74    using a modified version of the @{const fac} function
    1.75    as defining equation, the then redundant (since
    1.76    syntactically subsumed) original defining equations
    1.77 @@ -358,7 +354,7 @@
    1.78    here we just illustrate its impact on code generation.
    1.79  
    1.80    In a target language, type classes may be represented
    1.81 -  natively (as in the case of Haskell). For languages
    1.82 +  natively (as in the case of Haskell).  For languages
    1.83    like SML, they are implemented using \emph{dictionaries}.
    1.84    Our following example specifies a class \qt{null},
    1.85    assigning to each of its inhabitants a \qt{null} value:
    1.86 @@ -367,12 +363,11 @@
    1.87  class null = type +
    1.88    fixes null :: 'a
    1.89  
    1.90 -consts
    1.91 +fun
    1.92    head :: "'a\<Colon>null list \<Rightarrow> 'a"
    1.93 -
    1.94 -primrec
    1.95 +where
    1.96    "head [] = null"
    1.97 -  "head (x#xs) = x"
    1.98 +  | "head (x#xs) = x"
    1.99  
   1.100  text {*
   1.101    We provide some instances for our @{text null}:
   1.102 @@ -406,8 +401,9 @@
   1.103  
   1.104  text {*
   1.105    \lsthaskell{Thy/examples/Codegen.hs}
   1.106 +  \noindent (we have left out all other modules).
   1.107  
   1.108 -  (we have left out all other modules).
   1.109 +  \medskip
   1.110  
   1.111    The whole code in SML with explicit dictionary passing:
   1.112  *}
   1.113 @@ -416,51 +412,21 @@
   1.114  
   1.115  text {*
   1.116    \lstsml{Thy/examples/class.ML}
   1.117 -*}
   1.118  
   1.119 -text {*
   1.120 -  or in OCaml:
   1.121 +  \medskip
   1.122 +
   1.123 +  \noindent or in OCaml:
   1.124  *}
   1.125  
   1.126  code_gen dummy (OCaml "examples/class.ocaml")
   1.127  
   1.128  text {*
   1.129    \lstsml{Thy/examples/class.ocaml}
   1.130 +
   1.131 +  \medskip The explicit association of constants
   1.132 +  to classes can be inspected using the @{text "\<PRINTCLASSES>"}
   1.133  *}
   1.134  
   1.135 -subsection {* Incremental code generation *}
   1.136 -
   1.137 -text {*
   1.138 -  Code generation is \emph{incremental}: theorems
   1.139 -  and abstract intermediate code are cached and extended on demand.
   1.140 -  The cache may be partially or fully dropped if the underlying
   1.141 -  executable content of the theory changes.
   1.142 -  Implementation of caching is supposed to transparently
   1.143 -  hid away the details from the user.  Anyway, caching
   1.144 -  reaches the surface by using a slightly more general form
   1.145 -  of the @{text "\<CODEGEN>"}: either the list of constants or the
   1.146 -  list of serialization expressions may be dropped.  If no
   1.147 -  serialization expressions are given, only abstract code
   1.148 -  is generated and cached; if no constants are given, the
   1.149 -  current cache is serialized.
   1.150 -
   1.151 -  For explorative purpose, the
   1.152 -  @{text "\<CODETHMS>"} command may prove useful:
   1.153 -*}
   1.154 -
   1.155 -code_thms
   1.156 -
   1.157 -text {*
   1.158 -  \noindent print all cached defining equations (i.e.~\emph{after}
   1.159 -  any applied transformation).  A
   1.160 -  list of constants may be given; their function
   1.161 -  equations are added to the cache if not already present.
   1.162 -
   1.163 -  Similarly, the @{text "\<CODEDEPS>"} command shows a graph
   1.164 -  visualizing dependencies between defining equations.
   1.165 -*}
   1.166 -
   1.167 -
   1.168  
   1.169  section {* Recipes and advanced topics \label{sec:advanced} *}
   1.170  
   1.171 @@ -481,7 +447,7 @@
   1.172    \end{itemize}
   1.173  *}
   1.174  
   1.175 -subsection {* Library theories *}
   1.176 +subsection {* Library theories \label{sec:library} *}
   1.177  
   1.178  text {*
   1.179    The HOL \emph{Main} theory already provides a code generator setup
   1.180 @@ -492,6 +458,13 @@
   1.181  
   1.182    \begin{description}
   1.183  
   1.184 +    \item[@{text "Pretty_Int"}] represents HOL integers by big
   1.185 +       integer literals in target languages.
   1.186 +    \item[@{text "Pretty_Char"}] represents HOL characters by 
   1.187 +       character literals in target languages.
   1.188 +    \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char_chr"},
   1.189 +       but also offers treatment of character codes; includes
   1.190 +       @{text "Pretty_Int"}.
   1.191      \item[@{text "ExecutableSet"}] allows to generate code
   1.192         for finite sets using lists.
   1.193      \item[@{text "ExecutableRat"}] \label{exec_rat} implements rational
   1.194 @@ -499,10 +472,10 @@
   1.195      \item[@{text "EfficientNat"}] \label{eff_nat} implements natural numbers by integers,
   1.196         which in general will result in higher efficency; pattern
   1.197         matching with @{const "0\<Colon>nat"} / @{const "Suc"}
   1.198 -       is eliminated.
   1.199 +       is eliminated;  includes @{text "Pretty_Int"}.
   1.200      \item[@{text "MLString"}] provides an additional datatype @{text "mlstring"};
   1.201         in the HOL default setup, strings in HOL are mapped to list
   1.202 -       of chars in SML; values of type @{text "mlstring"} are
   1.203 +       of HOL characters in SML; values of type @{text "mlstring"} are
   1.204         mapped to strings in SML.
   1.205  
   1.206    \end{description}
   1.207 @@ -524,7 +497,6 @@
   1.208    equation, but never to the constant heading the left hand side.
   1.209    Inline theorems may be declared an undeclared using the
   1.210    \emph{code inline} or \emph{code noinline} attribute respectively.
   1.211 -
   1.212    Some common applications:
   1.213  *}
   1.214  
   1.215 @@ -585,8 +557,148 @@
   1.216    \end{warn}
   1.217  *}
   1.218  
   1.219 +
   1.220 +subsection {* Concerning operational equality *}
   1.221 +
   1.222 +text {*
   1.223 +  Surely you have already noticed how equality is treated
   1.224 +  by the code generator:
   1.225 +*}
   1.226 +
   1.227 +fun
   1.228 +  collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.229 +    "collect_duplicates xs ys [] = xs"
   1.230 +  | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
   1.231 +      then if z \<in> set ys
   1.232 +        then collect_duplicates xs ys zs
   1.233 +        else collect_duplicates xs (z#ys) zs
   1.234 +      else collect_duplicates (z#xs) (z#ys) zs)"
   1.235 +
   1.236 +text {*
   1.237 +  The membership test during preprocessing is rewritten,
   1.238 +  resulting in @{const List.memberl}, which itself
   1.239 +  performs an explicit equality check.
   1.240 +*}
   1.241 +
   1.242 +code_gen collect_duplicates (*<*)(SML #)(*>*)(SML "examples/collect_duplicates.ML")
   1.243 +
   1.244 +text {*
   1.245 +  \lstsml{Thy/examples/collect_duplicates.ML}
   1.246 +*}
   1.247 +
   1.248 +text {*
   1.249 +  Obviously, polymorphic equality is implemented the Haskell
   1.250 +  way using a type class.  How is this achieved?  By an
   1.251 +  almost trivial definition in the HOL setup:
   1.252 +*}
   1.253 +(*<*)
   1.254 +setup {* Sign.add_path "foo" *}
   1.255 +consts "op =" :: "'a"
   1.256 +(*>*)
   1.257 +class eq (attach "op =") = type
   1.258 +
   1.259 +text {*
   1.260 +  This merely introduces a class @{text eq} with corresponding
   1.261 +  operation @{text "op ="};
   1.262 +  the preprocessing framework does the rest.
   1.263 +  For datatypes, instances of @{text eq} are implicitly derived
   1.264 +  when possible.
   1.265 +
   1.266 +  Though this @{text eq} class is designed to get rarely in
   1.267 +  the way, a subtlety
   1.268 +  enters the stage when definitions of overloaded constants
   1.269 +  are dependent on operational equality.  For example, let
   1.270 +  us define a lexicographic ordering on tuples:
   1.271 +*}
   1.272 +(*<*)
   1.273 +hide (open) "class" eq
   1.274 +hide (open) const "op ="
   1.275 +setup {* Sign.parent_path *}
   1.276 +(*>*)
   1.277 +instance * :: (ord, ord) ord
   1.278 +  less_prod_def:
   1.279 +    "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
   1.280 +    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
   1.281 +  less_eq_prod_def:
   1.282 +    "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
   1.283 +    x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" ..
   1.284 +
   1.285 +lemmas [code nofunc] = less_prod_def less_eq_prod_def
   1.286 +
   1.287 +lemma ord_prod [code func(*<*), code nofunc(*>*)]:
   1.288 +  "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
   1.289 +  "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
   1.290 +  unfolding less_prod_def less_eq_prod_def by simp_all
   1.291 +
   1.292 +text {*
   1.293 +  Then code generation will fail.  Why?  The definition
   1.294 +  of @{const "op \<le>"} depends on equality on both arguments,
   1.295 +  which are polymorphic and impose an additional @{text eq}
   1.296 +  class constraint, thus violating the type discipline
   1.297 +  for class operations.
   1.298 +
   1.299 +  The solution is to add @{text eq} explicitly to the first sort arguments in the
   1.300 +  code theorems:
   1.301 +*}
   1.302 +
   1.303 +lemma ord_prod_code [code func]:
   1.304 +  "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow>
   1.305 +    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
   1.306 +  "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow>
   1.307 +    x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
   1.308 +  unfolding ord_prod by rule+
   1.309 +
   1.310 +text {*
   1.311 +  \noindent Then code generation succeeds:
   1.312 +*}
   1.313 +
   1.314 +code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   1.315 +  (*<*)(SML #)(*>*)(SML "examples/lexicographic.ML")
   1.316 +
   1.317 +text {*
   1.318 +  \lstsml{Thy/examples/lexicographic.ML}
   1.319 +*}
   1.320 +
   1.321 +text {*
   1.322 +  In general, code theorems for overloaded constants may have more
   1.323 +  restrictive sort constraints than the underlying instance relation
   1.324 +  between class and type constructor as long as the whole system of
   1.325 +  constraints is coregular; code theorems violating coregularity
   1.326 +  are rejected immediately.  Consequently, it might be necessary
   1.327 +  to delete disturbing theorems in the code theorem table,
   1.328 +  as we have done here with the original definitions @{text less_prod_def}
   1.329 +  and @{text less_eq_prod_def}.
   1.330 +*}
   1.331 +
   1.332 +
   1.333 +subsection {* Programs as sets of theorems *}
   1.334 +
   1.335 +text {*
   1.336 +  As told in \secref{sec:concept}, code generation is based
   1.337 +  on a structured collection of code theorems.
   1.338 +  For explorative purpose, this collection
   1.339 +  may be inspected using the @{text "\<CODETHMS>"} command:
   1.340 +*}
   1.341 +
   1.342 +code_thms "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.343 +
   1.344 +text {*
   1.345 +  \noindent prints a table with \emph{all} defining equations
   1.346 +  for @{const "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}, including
   1.347 +  \emph{all} defining equations those equations depend
   1.348 +  on recursivly.  @{text "\<CODETHMS>"} provides a convenient
   1.349 +  mechanism to inspect the impact of a preprocessor setup
   1.350 +  on defining equations.
   1.351 +  
   1.352 +  Similarly, the @{text "\<CODEDEPS>"} command shows a graph
   1.353 +  visualizing dependencies between defining equations.
   1.354 +*}
   1.355 +
   1.356 +
   1.357  subsection {* Customizing serialization  *}
   1.358  
   1.359 +subsubsection {* Basics *}
   1.360 +
   1.361  text {*
   1.362    Consider the following function and its corresponding
   1.363    SML code:
   1.364 @@ -595,20 +707,18 @@
   1.365  fun
   1.366    in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
   1.367    "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
   1.368 -
   1.369  (*<*)
   1.370  code_type %tt bool
   1.371    (SML)
   1.372  code_const %tt True and False and "op \<and>" and Not
   1.373    (SML and and and)
   1.374  (*>*)
   1.375 -
   1.376  code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_literal.ML")
   1.377  
   1.378  text {*
   1.379    \lstsml{Thy/examples/bool_literal.ML}
   1.380  
   1.381 -  Though this is correct code, it is a little bit unsatisfactory:
   1.382 +  \noindent Though this is correct code, it is a little bit unsatisfactory:
   1.383    boolean values and operators are materialized as distinguished
   1.384    entities with have nothing to do with the SML-builtin notion
   1.385    of \qt{bool}.  This results in less readable code;
   1.386 @@ -651,7 +761,7 @@
   1.387  text {*
   1.388    \lstsml{Thy/examples/bool_mlbool.ML}
   1.389  
   1.390 -  This still is not perfect: the parentheses
   1.391 +  \noindent This still is not perfect: the parentheses
   1.392    around the \qt{andalso} expression are superfluous.
   1.393    Though the serializer
   1.394    by no means attempts to imitate the rich Isabelle syntax
   1.395 @@ -667,20 +777,19 @@
   1.396  text {*
   1.397    \lstsml{Thy/examples/bool_infix.ML}
   1.398  
   1.399 +  \medskip
   1.400 +
   1.401    Next, we try to map HOL pairs to SML pairs, using the
   1.402    infix ``@{verbatim "*"}'' type constructor and parentheses:
   1.403  *}
   1.404 -
   1.405  (*<*)
   1.406  code_type *
   1.407    (SML)
   1.408  code_const Pair
   1.409    (SML)
   1.410  (*>*)
   1.411 -
   1.412  code_type %tt *
   1.413    (SML infix 2 "*")
   1.414 -
   1.415  code_const %tt Pair
   1.416    (SML "!((_),/ (_))")
   1.417  
   1.418 @@ -693,44 +802,7 @@
   1.419    inserts a space which may be used as a break if necessary
   1.420    during pretty printing.
   1.421  
   1.422 -  So far, we did only provide more idiomatic serializations for
   1.423 -  constructs which would be executable on their own.  Target-specific
   1.424 -  serializations may also be used to \emph{implement} constructs
   1.425 -  which have no explicit notion of executability.  For example,
   1.426 -  take the HOL integers:
   1.427 -*}
   1.428 -
   1.429 -definition
   1.430 -  double_inc :: "int \<Rightarrow> int" where
   1.431 -  "double_inc k = 2 * k + 1"
   1.432 -
   1.433 -code_gen double_inc (SML "examples/integers.ML")
   1.434 -
   1.435 -text {*
   1.436 -  will fail: @{typ int} in HOL is implemented using a quotient
   1.437 -  type, which does not provide any notion of executability.
   1.438 -  \footnote{Eventually, we also want to provide executability
   1.439 -  for quotients.}.  However, we could use the SML builtin
   1.440 -  integers:
   1.441 -*}
   1.442 -
   1.443 -code_type %tt int
   1.444 -  (SML "IntInf.int")
   1.445 -
   1.446 -code_const %tt "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   1.447 -    and "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   1.448 -  (SML "IntInf.+ (_, _)" and "IntInf.* (_, _)")
   1.449 -
   1.450 -code_gen double_inc (*<*)(SML #)(*>*)(SML "examples/integers.ML")
   1.451 -
   1.452 -text {*
   1.453 -  resulting in:
   1.454 -
   1.455 -  \lstsml{Thy/examples/integers.ML}
   1.456 -*}
   1.457 -
   1.458 -text {*
   1.459 -  These examples give a glimpse what powerful mechanisms
   1.460 +  These examples give a glimpse what mechanisms
   1.461    custom serializations provide; however their usage
   1.462    requires careful thinking in order not to introduce
   1.463    inconsistencies -- or, in other words:
   1.464 @@ -748,169 +820,6 @@
   1.465    a recommended tutorial on how to use them properly.
   1.466  *}
   1.467  
   1.468 -subsection {* Concerning operational equality *}
   1.469 -
   1.470 -text {*
   1.471 -  Surely you have already noticed how equality is treated
   1.472 -  by the code generator:
   1.473 -*}
   1.474 -
   1.475 -fun
   1.476 -  collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.477 -    "collect_duplicates xs ys [] = xs"
   1.478 -  | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
   1.479 -      then if z \<in> set ys
   1.480 -        then collect_duplicates xs ys zs
   1.481 -        else collect_duplicates xs (z#ys) zs
   1.482 -      else collect_duplicates (z#xs) (z#ys) zs)"
   1.483 -
   1.484 -text {*
   1.485 -  The membership test during preprocessing is rewritten,
   1.486 -  resulting in @{const List.memberl}, which itself
   1.487 -  performs an explicit equality check.
   1.488 -*}
   1.489 -
   1.490 -code_gen collect_duplicates (*<*)(SML #)(*>*)(SML "examples/collect_duplicates.ML")
   1.491 -
   1.492 -text {*
   1.493 -  \lstsml{Thy/examples/collect_duplicates.ML}
   1.494 -*}
   1.495 -
   1.496 -text {*
   1.497 -  Obviously, polymorphic equality is implemented the Haskell
   1.498 -  way using a type class.  How is this achieved?  By an
   1.499 -  almost trivial definition in the HOL setup:
   1.500 -*}
   1.501 -
   1.502 -(*<*)
   1.503 -setup {* Sign.add_path "foo" *}
   1.504 -consts "op =" :: "'a"
   1.505 -(*>*)
   1.506 -
   1.507 -class eq (attach "op =") = type
   1.508 -
   1.509 -text {*
   1.510 -  This merely introduces a class @{text eq} with corresponding
   1.511 -  operation @{text "op ="};
   1.512 -  the preprocessing framework does the rest.
   1.513 -*}
   1.514 -
   1.515 -(*<*)
   1.516 -hide (open) "class" eq
   1.517 -hide (open) const "op ="
   1.518 -setup {* Sign.parent_path *}
   1.519 -(*>*)
   1.520 -
   1.521 -text {*
   1.522 -  For datatypes, instances of @{text eq} are implicitly derived
   1.523 -  when possible.
   1.524 -
   1.525 -  Though this class is designed to get rarely in the way, there
   1.526 -  are some cases when it suddenly comes to surface:
   1.527 -*}
   1.528 -
   1.529 -subsubsection {* typedecls interpreted by customary serializations *}
   1.530 -
   1.531 -text {*
   1.532 -  A common idiom is to use unspecified types for formalizations
   1.533 -  and interpret them for a specific target language:
   1.534 -*}
   1.535 -
   1.536 -typedecl key
   1.537 -
   1.538 -fun
   1.539 -  lookup :: "(key \<times> 'a) list \<Rightarrow> key \<Rightarrow> 'a option" where
   1.540 -    "lookup [] l = None"
   1.541 -  | "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)"
   1.542 -
   1.543 -code_type %tt key
   1.544 -  (SML "string")
   1.545 -
   1.546 -text {*
   1.547 -  This, though, is not sufficient: @{typ key} is no instance
   1.548 -  of @{text eq} since @{typ key} is no datatype; the instance
   1.549 -  has to be declared manually, including a serialization
   1.550 -  for the particular instance of @{const "op ="}:
   1.551 -*}
   1.552 -
   1.553 -instance key :: eq ..
   1.554 -
   1.555 -code_const %tt "op = \<Colon> key \<Rightarrow> key \<Rightarrow> bool"
   1.556 -  (SML "!((_ : string) = _)")
   1.557 -
   1.558 -text {*
   1.559 -  Then everything goes fine:
   1.560 -*}
   1.561 -
   1.562 -code_gen lookup (*<*)(SML #)(*>*)(SML "examples/lookup.ML")
   1.563 -
   1.564 -text {*
   1.565 -  \lstsml{Thy/examples/lookup.ML}
   1.566 -*}
   1.567 -
   1.568 -subsubsection {* lexicographic orderings *}
   1.569 -
   1.570 -text {*
   1.571 -  Another subtlety
   1.572 -  enters the stage when definitions of overloaded constants
   1.573 -  are dependent on operational equality.  For example, let
   1.574 -  us define a lexicographic ordering on tuples:
   1.575 -*}
   1.576 -
   1.577 -instance * :: (ord, ord) ord
   1.578 -  less_prod_def: "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
   1.579 -    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
   1.580 -  less_eq_prod_def: "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
   1.581 -    x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" ..
   1.582 -
   1.583 -lemmas [code nofunc] = less_prod_def less_eq_prod_def
   1.584 -
   1.585 -lemma ord_prod [code func]:
   1.586 -  "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
   1.587 -  "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
   1.588 -  unfolding less_prod_def less_eq_prod_def by simp_all
   1.589 -
   1.590 -text {*
   1.591 -  Then code generation will fail.  Why?  The definition
   1.592 -  of @{const "op \<le>"} depends on equality on both arguments,
   1.593 -  which are polymorphic and impose an additional @{text eq}
   1.594 -  class constraint, thus violating the type discipline
   1.595 -  for class operations.
   1.596 -
   1.597 -  The solution is to add @{text eq} explicitly to the first sort arguments in the
   1.598 -  code theorems:
   1.599 -*}
   1.600 -
   1.601 -(*<*)
   1.602 -lemmas [code nofunc] = ord_prod
   1.603 -(*>*)
   1.604 -
   1.605 -lemma ord_prod_code [code func]:
   1.606 -  "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
   1.607 -  "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
   1.608 -  unfolding ord_prod by rule+
   1.609 -
   1.610 -text {*
   1.611 -  Then code generation succeeds:
   1.612 -*}
   1.613 -
   1.614 -code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   1.615 -  (*<*)(SML #)(*>*)(SML "examples/lexicographic.ML")
   1.616 -
   1.617 -text {*
   1.618 -  \lstsml{Thy/examples/lexicographic.ML}
   1.619 -*}
   1.620 -
   1.621 -text {*
   1.622 -  In general, code theorems for overloaded constants may have more
   1.623 -  restrictive sort constraints than the underlying instance relation
   1.624 -  between class and type constructor as long as the whole system of
   1.625 -  constraints is coregular; code theorems violating coregularity
   1.626 -  are rejected immediately.  Consequently, it might be necessary
   1.627 -  to delete disturbing theorems in the code theorem table,
   1.628 -  as we have done here with the original definitions @{text less_prod_def}
   1.629 -  and @{text less_eq_prod_def}.
   1.630 -*}
   1.631  
   1.632  subsubsection {* Haskell serialization *}
   1.633  
   1.634 @@ -921,23 +830,12 @@
   1.635    for the class (@{text "\<CODECLASS>"}) and its operation:
   1.636  *}
   1.637  
   1.638 -(*<*)
   1.639 -setup {* Sign.add_path "bar" *}
   1.640 -class eq = type + fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.641 -(*>*)
   1.642 -
   1.643  code_class %tt eq
   1.644 -  (Haskell "Eq" where eq \<equiv> "(==)")
   1.645 +  (Haskell "Eq" where "op =" \<equiv> "(==)")
   1.646  
   1.647 -code_const %tt eq
   1.648 +code_const %tt "op ="
   1.649    (Haskell infixl 4 "==")
   1.650  
   1.651 -(*<*)
   1.652 -hide "class" eq
   1.653 -hide const eq
   1.654 -setup {* Sign.parent_path *}
   1.655 -(*>*)
   1.656 -
   1.657  text {*
   1.658    A problem now occurs whenever a type which
   1.659    is an instance of @{text eq} in HOL is mapped
   1.660 @@ -962,86 +860,57 @@
   1.661  code_instance %tt bar :: eq
   1.662    (Haskell -)
   1.663  
   1.664 -subsection {* Types matter *}
   1.665  
   1.666 -text {*
   1.667 -  Imagine the following quick-and-dirty setup for implementing
   1.668 -  some kind of sets as lists in SML:
   1.669 -*}
   1.670 -
   1.671 -code_type %tt set
   1.672 -  (SML "_ list")
   1.673 -
   1.674 -code_const %tt "{}" and insert
   1.675 -  (SML "![]" and infixl 7 "::")
   1.676 -
   1.677 -definition
   1.678 -  dummy_set :: "(nat \<Rightarrow> nat) set" where
   1.679 -  "dummy_set = {Suc}"
   1.680 -
   1.681 -text {*
   1.682 -  Then code generation for @{const dummy_set} will fail.
   1.683 -  Why? A glimpse at the defining equations will offer:
   1.684 -*}
   1.685 -
   1.686 -code_thms insert
   1.687 +subsubsection {* Pretty printing *}
   1.688  
   1.689  text {*
   1.690 -  This reveals the defining equation @{thm insert_def}
   1.691 -  for @{const insert}, which is operationally meaningless
   1.692 -  but forces an equality constraint on the set members
   1.693 -  (which is not satisfiable if the set members are functions).
   1.694 -  Even when using set of natural numbers (which are an instance
   1.695 -  of \emph{eq}), we run into a problem:
   1.696 -*}
   1.697 -
   1.698 -definition
   1.699 -  foobar_set :: "nat set" where
   1.700 -  "foobar_set = {0, 1, 2}"
   1.701 -
   1.702 -text {*
   1.703 -  In this case the serializer would complain that @{const insert}
   1.704 -  expects dictionaries (namely an \emph{eq} dictionary) but
   1.705 -  has also been given a customary serialization.
   1.706 -
   1.707 -  \fixme[needs rewrite] The solution to this dilemma:
   1.708 +  The serializer provides ML interfaces to set up
   1.709 +  pretty serializations for expressions like lists, numerals
   1.710 +  and characters;  these are
   1.711 +  monolithic stubs and should only be used with the
   1.712 +  theories introduces in \secref{sec:library}.
   1.713  *}
   1.714  
   1.715 -lemma [code func]:
   1.716 -  "insert = insert" ..
   1.717 -
   1.718 -code_gen dummy_set foobar_set (*<*)(SML #)(*>*)(SML "examples/dirty_set.ML")
   1.719 -
   1.720 -text {*
   1.721 -  \lstsml{Thy/examples/dirty_set.ML}
   1.722 -
   1.723 -  Reflexive defining equations by convention are dropped:
   1.724 -*}
   1.725 -
   1.726 -code_thms insert
   1.727 -
   1.728 -text {*
   1.729 -  will show \emph{no} defining equations for insert.
   1.730 -
   1.731 -  Note that the sort constraints of reflexive equations
   1.732 -  are considered; so
   1.733 -*}
   1.734 -
   1.735 -lemma [code func]:
   1.736 -  "(insert \<Colon> 'a\<Colon>eq \<Rightarrow> 'a set \<Rightarrow> 'a set) = insert" ..
   1.737 -
   1.738 -text {*
   1.739 -  would mean nothing else than to introduce the evil
   1.740 -  sort constraint by hand.
   1.741 -*}
   1.742 -
   1.743 -
   1.744  subsection {* Constructor sets for datatypes *}
   1.745  
   1.746  text {*
   1.747 -  \fixme
   1.748 +  Conceptually, any datatype is spanned by a set of
   1.749 +  \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"}
   1.750 +  where @{text "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is excactly the set of \emph{all}
   1.751 +  type variables in @{text "\<tau>"}.  The HOL datatype package
   1.752 +  by default registers any new datatype in the table
   1.753 +  of datatypes, which may be inspected using
   1.754 +  the @{text "\<PRINTCODESETUP>"} command.
   1.755 +
   1.756 +  In some cases, it may be convenient to alter or
   1.757 +  extend this table;  as an example, we show
   1.758 +  how to implement finite sets by lists
   1.759 +  using the conversion @{term [source] "set \<Colon> 'a list \<Rightarrow> 'a set"}
   1.760 +  as constructor:
   1.761  *}
   1.762  
   1.763 +code_datatype set
   1.764 +
   1.765 +lemma [code func]: "{} = set []" by simp
   1.766 +
   1.767 +lemma [code func]: "insert x (set xs) = set (x#xs)" by simp
   1.768 +
   1.769 +lemma [code func]: "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
   1.770 +
   1.771 +lemma [code func]: "xs \<union> set ys = foldr insert ys xs" by (induct ys) simp_all
   1.772 +
   1.773 +lemma [code func]: "\<Union>set xs = foldr (op \<union>) xs {}" by (induct xs) simp_all
   1.774 +
   1.775 +code_gen "{}" insert "op \<in>" "op \<union>" "Union" (*<*)(SML #)(*>*)(SML "examples/set_list.ML")
   1.776 +
   1.777 +text {*
   1.778 +  \lstsml{Thy/examples/set_list.ML}
   1.779 +
   1.780 +  \medskip
   1.781 +
   1.782 +  Changing the representation of existing datatypes requires
   1.783 +  some care with respect to pattern matching and such.
   1.784 +*}
   1.785  
   1.786  subsection {* Cyclic module dependencies *}
   1.787  
   1.788 @@ -1069,6 +938,22 @@
   1.789    at serialization time.
   1.790  *}
   1.791  
   1.792 +subsection {* Incremental code generation *}
   1.793 +
   1.794 +text {*
   1.795 +  Code generation is \emph{incremental}: theorems
   1.796 +  and abstract intermediate code are cached and extended on demand.
   1.797 +  The cache may be partially or fully dropped if the underlying
   1.798 +  executable content of the theory changes.
   1.799 +  Implementation of caching is supposed to transparently
   1.800 +  hid away the details from the user.  Anyway, caching
   1.801 +  reaches the surface by using a slightly more general form
   1.802 +  of the @{text "\<CODETHMS>"}, @{text "\<CODEDEPS>"}
   1.803 +  and @{text "\<CODEGEN>"} commands: the list of constants
   1.804 +  may be omitted.  Then, all constants with code theorems
   1.805 +  in the current cache are referred to.
   1.806 +*}
   1.807 +
   1.808  subsection {* Axiomatic extensions *}
   1.809  
   1.810  text {*
   1.811 @@ -1145,6 +1030,8 @@
   1.812  text {*
   1.813    \lstsml{Thy/examples/arbitrary.ML}
   1.814  
   1.815 +  \medskip
   1.816 +
   1.817    Another axiomatic extension is code generation
   1.818    for abstracted types.  For this, the  
   1.819    @{text "ExecutableRat"} (see \secref{exec_rat})
   1.820 @@ -1370,13 +1257,13 @@
   1.821  
   1.822    \item @{text merge} merging two data slots.
   1.823  
   1.824 -  \item @{text purge}~@{text thy}~@{text cs} propagates changes in executable content;
   1.825 +  \item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content;
   1.826      if possible, the current theory context is handed over
   1.827      as argument @{text thy} (if there is no current theory context (e.g.~during
   1.828 -    theory merge, @{ML NONE}); @{text cs} indicates the kind
   1.829 +    theory merge, @{ML NONE}); @{text consts} indicates the kind
   1.830      of change: @{ML NONE} stands for a fundamental change
   1.831 -    which invalidates any existing code, @{text "SOME cs"}
   1.832 -    hints that executable content for constants @{text cs}
   1.833 +    which invalidates any existing code, @{text "SOME consts"}
   1.834 +    hints that executable content for constants @{text consts}
   1.835      has changed.
   1.836  
   1.837    \end{description}
   1.838 @@ -1406,19 +1293,61 @@
   1.839    \end{description}
   1.840  *}
   1.841  
   1.842 -(* subsubsection {* Building implementable systems fo defining equations *}
   1.843 +subsubsection {* Building implementable systems fo defining equations *}
   1.844  
   1.845  text {*
   1.846    Out of the executable content of a theory, a normalized
   1.847    defining equation systems may be constructed containing
   1.848    function definitions for constants.  The system is cached
   1.849    until its underlying executable content changes.
   1.850 +
   1.851 +  Defining equations are retrieved by instantiation
   1.852 +  of the functor @{ML_functor CodegenFuncgrRetrieval}
   1.853 +  which takes two arguments:
   1.854 +
   1.855 +  \medskip
   1.856 +  \begin{tabular}{l}
   1.857 +  @{text "val name: string"} \\
   1.858 +  @{text "val rewrites: theory \<rightarrow> thm list"}
   1.859 +  \end{tabular}
   1.860 +
   1.861 +  \begin{description}
   1.862 +
   1.863 +  \item @{text name} is a system-wide unique name identifying
   1.864 +    this particular system of defining equations.
   1.865 +
   1.866 +  \item @{text rewrites} specifies a set of theory-dependent
   1.867 +    rewrite rules which are added to the preprocessor setup;
   1.868 +    if no additional preprocessing is required, pass
   1.869 +    a function returning an empty list.
   1.870 +
   1.871 +  \end{description}
   1.872 +
   1.873 +  An instance of @{ML_functor CodegenFuncgrRetrieval} in essence
   1.874 +  provides the following interface:
   1.875 +
   1.876 +  \medskip
   1.877 +  \begin{tabular}{l}
   1.878 +  @{text "make: theory \<rightarrow> CodegenConsts.const list \<rightarrow> CodegenFuncgr.T"} \\
   1.879 +  \end{tabular}
   1.880 +
   1.881 +  \begin{description}
   1.882 +
   1.883 +  \item @{text make}~@{text thy}~@{text consts} returns
   1.884 +    a system of defining equations which is guaranteed
   1.885 +    to contain all defining equations for constants @{text consts}
   1.886 +    including all defining equations any defining equation
   1.887 +    for any constant in @{text consts} depends on.
   1.888 +
   1.889 +  \end{description}
   1.890 +
   1.891 +  Systems of defining equations are graphs accesible by the
   1.892 +  following operations:
   1.893  *}
   1.894  
   1.895  text %mlref {*
   1.896    \begin{mldecls}
   1.897    @{index_ML_type CodegenFuncgr.T} \\
   1.898 -  @{index_ML CodegenFuncgr.make: "theory -> CodegenConsts.const list -> CodegenFuncgr.T"} \\
   1.899    @{index_ML CodegenFuncgr.funcs: "CodegenFuncgr.T -> CodegenConsts.const -> thm list"} \\
   1.900    @{index_ML CodegenFuncgr.typ: "CodegenFuncgr.T -> CodegenConsts.const -> typ"} \\
   1.901    @{index_ML CodegenFuncgr.deps: "CodegenFuncgr.T
   1.902 @@ -1431,20 +1360,15 @@
   1.903    \item @{ML_type CodegenFuncgr.T} represents
   1.904      a normalized defining equation system.
   1.905  
   1.906 -  \item @{ML CodegenFuncgr.make}~@{text thy}~@{text cs}
   1.907 -    returns a normalized defining equation system,
   1.908 -    with the assertion that it contains any function
   1.909 -    definition for constants @{text cs} (if existing).
   1.910 +  \item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text const}
   1.911 +    retrieves defining equiations for constant @{text const}.
   1.912  
   1.913 -  \item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text c}
   1.914 -    retrieves function definition for constant @{text c}.
   1.915 +  \item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text const}
   1.916 +    retrieves function type for constant @{text const}.
   1.917  
   1.918 -  \item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text c}
   1.919 -    retrieves function type for constant @{text c}.
   1.920 -
   1.921 -  \item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text cs}
   1.922 +  \item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text consts}
   1.923      returns the transitive closure of dependencies for
   1.924 -    constants @{text cs} as a partitioning where each partition
   1.925 +    constants @{text consts} as a partitioning where each partition
   1.926      corresponds to a strongly connected component of
   1.927      dependencies and any partition does \emph{not}
   1.928      depend on partitions further left.
   1.929 @@ -1453,7 +1377,7 @@
   1.930      returns all currently represented constants.
   1.931  
   1.932    \end{description}
   1.933 -*} *)
   1.934 +*}
   1.935  
   1.936  subsubsection {* Datatype hooks *}
   1.937  
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Apr 26 12:00:12 2007 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Apr 26 13:32:55 2007 +0200
     2.3 @@ -198,7 +198,7 @@
     2.4    \emph{type classes}. A defining equation as a first approximation
     2.5    is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t}
     2.6    (an equation headed by a constant \isa{f} with arguments
     2.7 -  \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}.
     2.8 +  \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}).
     2.9    Code generation aims to turn defining equations
    2.10    into a functional program by running through
    2.11    a process (see figure \ref{fig:process}):
    2.12 @@ -290,14 +290,12 @@
    2.13  {\isafoldML}%
    2.14  %
    2.15  \isadelimML
    2.16 -\isanewline
    2.17  %
    2.18  \endisadelimML
    2.19  \isacommand{definition}\isamarkupfalse%
    2.20  \isanewline
    2.21  \ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
    2.22 -\ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
    2.23 -%
    2.24 +\ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}%
    2.25  \isadelimML
    2.26  %
    2.27  \endisadelimML
    2.28 @@ -310,7 +308,6 @@
    2.29  \isadelimML
    2.30  %
    2.31  \endisadelimML
    2.32 -\isanewline
    2.33  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    2.34  \ pick{\isacharunderscore}some\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
    2.35  \begin{isamarkuptext}%
    2.36 @@ -337,7 +334,7 @@
    2.37    The typical HOL tools are already set up in a way that
    2.38    function definitions introduced by \isa{{\isasymDEFINITION}},
    2.39    \isa{{\isasymFUN}},
    2.40 -  \isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}}
    2.41 +  \isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}},
    2.42    \isa{{\isasymRECDEF}} are implicitly propagated
    2.43    to this defining equation table. Specific theorems may be
    2.44    selected using an attribute: \emph{code func}. As example,
    2.45 @@ -353,7 +350,7 @@
    2.46  \ \ {\isachardoublequoteopen}pick\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}let\ {\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharequal}\ x\ in\isanewline
    2.47  \ \ \ \ if\ n\ {\isacharless}\ k\ then\ v\ else\ pick\ xs\ {\isacharparenleft}n\ {\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
    2.48  \begin{isamarkuptext}%
    2.49 -We want to eliminate the explicit destruction
    2.50 +\noindent We want to eliminate the explicit destruction
    2.51    of \isa{x} to \isa{{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}}:%
    2.52  \end{isamarkuptext}%
    2.53  \isamarkuptrue%
    2.54 @@ -379,11 +376,11 @@
    2.55  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    2.56  \ pick\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
    2.57  \begin{isamarkuptext}%
    2.58 -This theorem is now added to the defining equation table:
    2.59 +\noindent This theorem now is used for generating code:
    2.60  
    2.61    \lstsml{Thy/examples/pick1.ML}
    2.62  
    2.63 -  It might be convenient to remove the pointless original
    2.64 +  \noindent It might be convenient to remove the pointless original
    2.65    equation, using the \emph{nofunc} attribute:%
    2.66  \end{isamarkuptext}%
    2.67  \isamarkuptrue%
    2.68 @@ -395,7 +392,7 @@
    2.69  \begin{isamarkuptext}%
    2.70  \lstsml{Thy/examples/pick2.ML}
    2.71  
    2.72 -  Syntactic redundancies are implicitly dropped. For example,
    2.73 +  \noindent Syntactic redundancies are implicitly dropped. For example,
    2.74    using a modified version of the \isa{fac} function
    2.75    as defining equation, the then redundant (since
    2.76    syntactically subsumed) original defining equations
    2.77 @@ -445,7 +442,7 @@
    2.78    here we just illustrate its impact on code generation.
    2.79  
    2.80    In a target language, type classes may be represented
    2.81 -  natively (as in the case of Haskell). For languages
    2.82 +  natively (as in the case of Haskell).  For languages
    2.83    like SML, they are implemented using \emph{dictionaries}.
    2.84    Our following example specifies a class \qt{null},
    2.85    assigning to each of its inhabitants a \qt{null} value:%
    2.86 @@ -455,14 +452,12 @@
    2.87  \ null\ {\isacharequal}\ type\ {\isacharplus}\isanewline
    2.88  \ \ \isakeyword{fixes}\ null\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
    2.89  \isanewline
    2.90 -\isacommand{consts}\isamarkupfalse%
    2.91 +\isacommand{fun}\isamarkupfalse%
    2.92  \isanewline
    2.93  \ \ head\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}null\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
    2.94 -\isanewline
    2.95 -\isacommand{primrec}\isamarkupfalse%
    2.96 -\isanewline
    2.97 +\isakeyword{where}\isanewline
    2.98  \ \ {\isachardoublequoteopen}head\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ null{\isachardoublequoteclose}\isanewline
    2.99 -\ \ {\isachardoublequoteopen}head\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}%
   2.100 +\ \ {\isacharbar}\ {\isachardoublequoteopen}head\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}%
   2.101  \begin{isamarkuptext}%
   2.102  We provide some instances for our \isa{null}:%
   2.103  \end{isamarkuptext}%
   2.104 @@ -522,8 +517,9 @@
   2.105  \ dummy\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}%
   2.106  \begin{isamarkuptext}%
   2.107  \lsthaskell{Thy/examples/Codegen.hs}
   2.108 +  \noindent (we have left out all other modules).
   2.109  
   2.110 -  (we have left out all other modules).
   2.111 +  \medskip
   2.112  
   2.113    The whole code in SML with explicit dictionary passing:%
   2.114  \end{isamarkuptext}%
   2.115 @@ -531,53 +527,20 @@
   2.116  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   2.117  \ dummy\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   2.118  \begin{isamarkuptext}%
   2.119 -\lstsml{Thy/examples/class.ML}%
   2.120 -\end{isamarkuptext}%
   2.121 -\isamarkuptrue%
   2.122 -%
   2.123 -\begin{isamarkuptext}%
   2.124 -or in OCaml:%
   2.125 +\lstsml{Thy/examples/class.ML}
   2.126 +
   2.127 +  \medskip
   2.128 +
   2.129 +  \noindent or in OCaml:%
   2.130  \end{isamarkuptext}%
   2.131  \isamarkuptrue%
   2.132  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   2.133  \ dummy\ {\isacharparenleft}OCaml\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}{\isacharparenright}%
   2.134  \begin{isamarkuptext}%
   2.135 -\lstsml{Thy/examples/class.ocaml}%
   2.136 -\end{isamarkuptext}%
   2.137 -\isamarkuptrue%
   2.138 -%
   2.139 -\isamarkupsubsection{Incremental code generation%
   2.140 -}
   2.141 -\isamarkuptrue%
   2.142 -%
   2.143 -\begin{isamarkuptext}%
   2.144 -Code generation is \emph{incremental}: theorems
   2.145 -  and abstract intermediate code are cached and extended on demand.
   2.146 -  The cache may be partially or fully dropped if the underlying
   2.147 -  executable content of the theory changes.
   2.148 -  Implementation of caching is supposed to transparently
   2.149 -  hid away the details from the user.  Anyway, caching
   2.150 -  reaches the surface by using a slightly more general form
   2.151 -  of the \isa{{\isasymCODEGEN}}: either the list of constants or the
   2.152 -  list of serialization expressions may be dropped.  If no
   2.153 -  serialization expressions are given, only abstract code
   2.154 -  is generated and cached; if no constants are given, the
   2.155 -  current cache is serialized.
   2.156 +\lstsml{Thy/examples/class.ocaml}
   2.157  
   2.158 -  For explorative purpose, the
   2.159 -  \isa{{\isasymCODETHMS}} command may prove useful:%
   2.160 -\end{isamarkuptext}%
   2.161 -\isamarkuptrue%
   2.162 -\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
   2.163 -%
   2.164 -\begin{isamarkuptext}%
   2.165 -\noindent print all cached defining equations (i.e.~\emph{after}
   2.166 -  any applied transformation).  A
   2.167 -  list of constants may be given; their function
   2.168 -  equations are added to the cache if not already present.
   2.169 -
   2.170 -  Similarly, the \isa{{\isasymCODEDEPS}} command shows a graph
   2.171 -  visualizing dependencies between defining equations.%
   2.172 +  \medskip The explicit association of constants
   2.173 +  to classes can be inspected using the \isa{{\isasymPRINTCLASSES}}%
   2.174  \end{isamarkuptext}%
   2.175  \isamarkuptrue%
   2.176  %
   2.177 @@ -603,7 +566,7 @@
   2.178  \end{isamarkuptext}%
   2.179  \isamarkuptrue%
   2.180  %
   2.181 -\isamarkupsubsection{Library theories%
   2.182 +\isamarkupsubsection{Library theories \label{sec:library}%
   2.183  }
   2.184  \isamarkuptrue%
   2.185  %
   2.186 @@ -616,6 +579,13 @@
   2.187  
   2.188    \begin{description}
   2.189  
   2.190 +    \item[\isa{Pretty{\isacharunderscore}Int}] represents HOL integers by big
   2.191 +       integer literals in target languages.
   2.192 +    \item[\isa{Pretty{\isacharunderscore}Char}] represents HOL characters by 
   2.193 +       character literals in target languages.
   2.194 +    \item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr},
   2.195 +       but also offers treatment of character codes; includes
   2.196 +       \isa{Pretty{\isacharunderscore}Int}.
   2.197      \item[\isa{ExecutableSet}] allows to generate code
   2.198         for finite sets using lists.
   2.199      \item[\isa{ExecutableRat}] \label{exec_rat} implements rational
   2.200 @@ -623,10 +593,10 @@
   2.201      \item[\isa{EfficientNat}] \label{eff_nat} implements natural numbers by integers,
   2.202         which in general will result in higher efficency; pattern
   2.203         matching with \isa{{\isadigit{0}}} / \isa{Suc}
   2.204 -       is eliminated.
   2.205 +       is eliminated;  includes \isa{Pretty{\isacharunderscore}Int}.
   2.206      \item[\isa{MLString}] provides an additional datatype \isa{mlstring};
   2.207         in the HOL default setup, strings in HOL are mapped to list
   2.208 -       of chars in SML; values of type \isa{mlstring} are
   2.209 +       of HOL characters in SML; values of type \isa{mlstring} are
   2.210         mapped to strings in SML.
   2.211  
   2.212    \end{description}%
   2.213 @@ -651,7 +621,6 @@
   2.214    equation, but never to the constant heading the left hand side.
   2.215    Inline theorems may be declared an undeclared using the
   2.216    \emph{code inline} or \emph{code noinline} attribute respectively.
   2.217 -
   2.218    Some common applications:%
   2.219  \end{isamarkuptext}%
   2.220  \isamarkuptrue%
   2.221 @@ -745,10 +714,222 @@
   2.222  \end{isamarkuptext}%
   2.223  \isamarkuptrue%
   2.224  %
   2.225 +\isamarkupsubsection{Concerning operational equality%
   2.226 +}
   2.227 +\isamarkuptrue%
   2.228 +%
   2.229 +\begin{isamarkuptext}%
   2.230 +Surely you have already noticed how equality is treated
   2.231 +  by the code generator:%
   2.232 +\end{isamarkuptext}%
   2.233 +\isamarkuptrue%
   2.234 +\isacommand{fun}\isamarkupfalse%
   2.235 +\isanewline
   2.236 +\ \ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   2.237 +\ \ \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
   2.238 +\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
   2.239 +\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
   2.240 +\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
   2.241 +\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
   2.242 +\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
   2.243 +\begin{isamarkuptext}%
   2.244 +The membership test during preprocessing is rewritten,
   2.245 +  resulting in \isa{op\ mem}, which itself
   2.246 +  performs an explicit equality check.%
   2.247 +\end{isamarkuptext}%
   2.248 +\isamarkuptrue%
   2.249 +\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   2.250 +\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   2.251 +\begin{isamarkuptext}%
   2.252 +\lstsml{Thy/examples/collect_duplicates.ML}%
   2.253 +\end{isamarkuptext}%
   2.254 +\isamarkuptrue%
   2.255 +%
   2.256 +\begin{isamarkuptext}%
   2.257 +Obviously, polymorphic equality is implemented the Haskell
   2.258 +  way using a type class.  How is this achieved?  By an
   2.259 +  almost trivial definition in the HOL setup:%
   2.260 +\end{isamarkuptext}%
   2.261 +\isamarkuptrue%
   2.262 +%
   2.263 +\isadelimML
   2.264 +%
   2.265 +\endisadelimML
   2.266 +%
   2.267 +\isatagML
   2.268 +%
   2.269 +\endisatagML
   2.270 +{\isafoldML}%
   2.271 +%
   2.272 +\isadelimML
   2.273 +%
   2.274 +\endisadelimML
   2.275 +\isacommand{class}\isamarkupfalse%
   2.276 +\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ type%
   2.277 +\begin{isamarkuptext}%
   2.278 +This merely introduces a class \isa{eq} with corresponding
   2.279 +  operation \isa{op\ {\isacharequal}};
   2.280 +  the preprocessing framework does the rest.
   2.281 +  For datatypes, instances of \isa{eq} are implicitly derived
   2.282 +  when possible.
   2.283 +
   2.284 +  Though this \isa{eq} class is designed to get rarely in
   2.285 +  the way, a subtlety
   2.286 +  enters the stage when definitions of overloaded constants
   2.287 +  are dependent on operational equality.  For example, let
   2.288 +  us define a lexicographic ordering on tuples:%
   2.289 +\end{isamarkuptext}%
   2.290 +\isamarkuptrue%
   2.291 +%
   2.292 +\isadelimML
   2.293 +%
   2.294 +\endisadelimML
   2.295 +%
   2.296 +\isatagML
   2.297 +%
   2.298 +\endisatagML
   2.299 +{\isafoldML}%
   2.300 +%
   2.301 +\isadelimML
   2.302 +%
   2.303 +\endisadelimML
   2.304 +\isacommand{instance}\isamarkupfalse%
   2.305 +\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
   2.306 +\ \ less{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\isanewline
   2.307 +\ \ \ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
   2.308 +\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.309 +\ \ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\isanewline
   2.310 +\ \ \ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
   2.311 +\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
   2.312 +\isadelimproof
   2.313 +\ %
   2.314 +\endisadelimproof
   2.315 +%
   2.316 +\isatagproof
   2.317 +\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   2.318 +%
   2.319 +\endisatagproof
   2.320 +{\isafoldproof}%
   2.321 +%
   2.322 +\isadelimproof
   2.323 +%
   2.324 +\endisadelimproof
   2.325 +\isanewline
   2.326 +\isanewline
   2.327 +\isacommand{lemmas}\isamarkupfalse%
   2.328 +\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline
   2.329 +\isanewline
   2.330 +\isacommand{lemma}\isamarkupfalse%
   2.331 +\ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   2.332 +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.333 +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.334 +%
   2.335 +\isadelimproof
   2.336 +\ \ %
   2.337 +\endisadelimproof
   2.338 +%
   2.339 +\isatagproof
   2.340 +\isacommand{unfolding}\isamarkupfalse%
   2.341 +\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   2.342 +\ simp{\isacharunderscore}all%
   2.343 +\endisatagproof
   2.344 +{\isafoldproof}%
   2.345 +%
   2.346 +\isadelimproof
   2.347 +%
   2.348 +\endisadelimproof
   2.349 +%
   2.350 +\begin{isamarkuptext}%
   2.351 +Then code generation will fail.  Why?  The definition
   2.352 +  of \isa{op\ {\isasymle}} depends on equality on both arguments,
   2.353 +  which are polymorphic and impose an additional \isa{eq}
   2.354 +  class constraint, thus violating the type discipline
   2.355 +  for class operations.
   2.356 +
   2.357 +  The solution is to add \isa{eq} explicitly to the first sort arguments in the
   2.358 +  code theorems:%
   2.359 +\end{isamarkuptext}%
   2.360 +\isamarkuptrue%
   2.361 +\isacommand{lemma}\isamarkupfalse%
   2.362 +\ ord{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   2.363 +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
   2.364 +\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.365 +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
   2.366 +\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.367 +%
   2.368 +\isadelimproof
   2.369 +\ \ %
   2.370 +\endisadelimproof
   2.371 +%
   2.372 +\isatagproof
   2.373 +\isacommand{unfolding}\isamarkupfalse%
   2.374 +\ ord{\isacharunderscore}prod\ \isacommand{by}\isamarkupfalse%
   2.375 +\ rule{\isacharplus}%
   2.376 +\endisatagproof
   2.377 +{\isafoldproof}%
   2.378 +%
   2.379 +\isadelimproof
   2.380 +%
   2.381 +\endisadelimproof
   2.382 +%
   2.383 +\begin{isamarkuptext}%
   2.384 +\noindent Then code generation succeeds:%
   2.385 +\end{isamarkuptext}%
   2.386 +\isamarkuptrue%
   2.387 +\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   2.388 +\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   2.389 +\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   2.390 +\begin{isamarkuptext}%
   2.391 +\lstsml{Thy/examples/lexicographic.ML}%
   2.392 +\end{isamarkuptext}%
   2.393 +\isamarkuptrue%
   2.394 +%
   2.395 +\begin{isamarkuptext}%
   2.396 +In general, code theorems for overloaded constants may have more
   2.397 +  restrictive sort constraints than the underlying instance relation
   2.398 +  between class and type constructor as long as the whole system of
   2.399 +  constraints is coregular; code theorems violating coregularity
   2.400 +  are rejected immediately.  Consequently, it might be necessary
   2.401 +  to delete disturbing theorems in the code theorem table,
   2.402 +  as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def}
   2.403 +  and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.%
   2.404 +\end{isamarkuptext}%
   2.405 +\isamarkuptrue%
   2.406 +%
   2.407 +\isamarkupsubsection{Programs as sets of theorems%
   2.408 +}
   2.409 +\isamarkuptrue%
   2.410 +%
   2.411 +\begin{isamarkuptext}%
   2.412 +As told in \secref{sec:concept}, code generation is based
   2.413 +  on a structured collection of code theorems.
   2.414 +  For explorative purpose, this collection
   2.415 +  may be inspected using the \isa{{\isasymCODETHMS}} command:%
   2.416 +\end{isamarkuptext}%
   2.417 +\isamarkuptrue%
   2.418 +\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
   2.419 +\ {\isachardoublequoteopen}op\ mod\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}%
   2.420 +\begin{isamarkuptext}%
   2.421 +\noindent prints a table with \emph{all} defining equations
   2.422 +  for \isa{op\ mod}, including
   2.423 +  \emph{all} defining equations those equations depend
   2.424 +  on recursivly.  \isa{{\isasymCODETHMS}} provides a convenient
   2.425 +  mechanism to inspect the impact of a preprocessor setup
   2.426 +  on defining equations.
   2.427 +  
   2.428 +  Similarly, the \isa{{\isasymCODEDEPS}} command shows a graph
   2.429 +  visualizing dependencies between defining equations.%
   2.430 +\end{isamarkuptext}%
   2.431 +\isamarkuptrue%
   2.432 +%
   2.433  \isamarkupsubsection{Customizing serialization%
   2.434  }
   2.435  \isamarkuptrue%
   2.436  %
   2.437 +\isamarkupsubsubsection{Basics%
   2.438 +}
   2.439 +\isamarkuptrue%
   2.440 +%
   2.441  \begin{isamarkuptext}%
   2.442  Consider the following function and its corresponding
   2.443    SML code:%
   2.444 @@ -757,8 +938,7 @@
   2.445  \isacommand{fun}\isamarkupfalse%
   2.446  \isanewline
   2.447  \ \ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   2.448 -\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}\isanewline
   2.449 -%
   2.450 +\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
   2.451  \isadelimtt
   2.452  %
   2.453  \endisadelimtt
   2.454 @@ -769,7 +949,6 @@
   2.455  {\isafoldtt}%
   2.456  %
   2.457  \isadelimtt
   2.458 -\isanewline
   2.459  %
   2.460  \endisadelimtt
   2.461  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   2.462 @@ -777,7 +956,7 @@
   2.463  \begin{isamarkuptext}%
   2.464  \lstsml{Thy/examples/bool_literal.ML}
   2.465  
   2.466 -  Though this is correct code, it is a little bit unsatisfactory:
   2.467 +  \noindent Though this is correct code, it is a little bit unsatisfactory:
   2.468    boolean values and operators are materialized as distinguished
   2.469    entities with have nothing to do with the SML-builtin notion
   2.470    of \qt{bool}.  This results in less readable code;
   2.471 @@ -834,7 +1013,7 @@
   2.472  \begin{isamarkuptext}%
   2.473  \lstsml{Thy/examples/bool_mlbool.ML}
   2.474  
   2.475 -  This still is not perfect: the parentheses
   2.476 +  \noindent This still is not perfect: the parentheses
   2.477    around the \qt{andalso} expression are superfluous.
   2.478    Though the serializer
   2.479    by no means attempts to imitate the rich Isabelle syntax
   2.480 @@ -864,11 +1043,12 @@
   2.481  \begin{isamarkuptext}%
   2.482  \lstsml{Thy/examples/bool_infix.ML}
   2.483  
   2.484 +  \medskip
   2.485 +
   2.486    Next, we try to map HOL pairs to SML pairs, using the
   2.487    infix ``\verb|*|'' type constructor and parentheses:%
   2.488  \end{isamarkuptext}%
   2.489  \isamarkuptrue%
   2.490 -\isanewline
   2.491  %
   2.492  \isadelimtt
   2.493  %
   2.494 @@ -878,7 +1058,6 @@
   2.495  \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   2.496  \ {\isacharasterisk}\isanewline
   2.497  \ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   2.498 -\isanewline
   2.499  \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   2.500  \ Pair\isanewline
   2.501  \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
   2.502 @@ -898,61 +1077,7 @@
   2.503    inserts a space which may be used as a break if necessary
   2.504    during pretty printing.
   2.505  
   2.506 -  So far, we did only provide more idiomatic serializations for
   2.507 -  constructs which would be executable on their own.  Target-specific
   2.508 -  serializations may also be used to \emph{implement} constructs
   2.509 -  which have no explicit notion of executability.  For example,
   2.510 -  take the HOL integers:%
   2.511 -\end{isamarkuptext}%
   2.512 -\isamarkuptrue%
   2.513 -\isacommand{definition}\isamarkupfalse%
   2.514 -\isanewline
   2.515 -\ \ double{\isacharunderscore}inc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   2.516 -\ \ {\isachardoublequoteopen}double{\isacharunderscore}inc\ k\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
   2.517 -\isanewline
   2.518 -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   2.519 -\ double{\isacharunderscore}inc\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}integers{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   2.520 -\begin{isamarkuptext}%
   2.521 -will fail: \isa{int} in HOL is implemented using a quotient
   2.522 -  type, which does not provide any notion of executability.
   2.523 -  \footnote{Eventually, we also want to provide executability
   2.524 -  for quotients.}.  However, we could use the SML builtin
   2.525 -  integers:%
   2.526 -\end{isamarkuptext}%
   2.527 -\isamarkuptrue%
   2.528 -%
   2.529 -\isadelimtt
   2.530 -%
   2.531 -\endisadelimtt
   2.532 -%
   2.533 -\isatagtt
   2.534 -\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   2.535 -\ int\isanewline
   2.536 -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}int{\isachardoublequoteclose}{\isacharparenright}\isanewline
   2.537 -\isanewline
   2.538 -\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   2.539 -\ {\isachardoublequoteopen}op\ {\isacharplus}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
   2.540 -\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isacharasterisk}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
   2.541 -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
   2.542 -\endisatagtt
   2.543 -{\isafoldtt}%
   2.544 -%
   2.545 -\isadelimtt
   2.546 -%
   2.547 -\endisadelimtt
   2.548 -\isanewline
   2.549 -\isanewline
   2.550 -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   2.551 -\ double{\isacharunderscore}inc\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}integers{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   2.552 -\begin{isamarkuptext}%
   2.553 -resulting in:
   2.554 -
   2.555 -  \lstsml{Thy/examples/integers.ML}%
   2.556 -\end{isamarkuptext}%
   2.557 -\isamarkuptrue%
   2.558 -%
   2.559 -\begin{isamarkuptext}%
   2.560 -These examples give a glimpse what powerful mechanisms
   2.561 +  These examples give a glimpse what mechanisms
   2.562    custom serializations provide; however their usage
   2.563    requires careful thinking in order not to introduce
   2.564    inconsistencies -- or, in other words:
   2.565 @@ -971,284 +1096,6 @@
   2.566  \end{isamarkuptext}%
   2.567  \isamarkuptrue%
   2.568  %
   2.569 -\isamarkupsubsection{Concerning operational equality%
   2.570 -}
   2.571 -\isamarkuptrue%
   2.572 -%
   2.573 -\begin{isamarkuptext}%
   2.574 -Surely you have already noticed how equality is treated
   2.575 -  by the code generator:%
   2.576 -\end{isamarkuptext}%
   2.577 -\isamarkuptrue%
   2.578 -\isacommand{fun}\isamarkupfalse%
   2.579 -\isanewline
   2.580 -\ \ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   2.581 -\ \ \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
   2.582 -\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
   2.583 -\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
   2.584 -\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
   2.585 -\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
   2.586 -\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
   2.587 -\begin{isamarkuptext}%
   2.588 -The membership test during preprocessing is rewritten,
   2.589 -  resulting in \isa{op\ mem}, which itself
   2.590 -  performs an explicit equality check.%
   2.591 -\end{isamarkuptext}%
   2.592 -\isamarkuptrue%
   2.593 -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   2.594 -\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   2.595 -\begin{isamarkuptext}%
   2.596 -\lstsml{Thy/examples/collect_duplicates.ML}%
   2.597 -\end{isamarkuptext}%
   2.598 -\isamarkuptrue%
   2.599 -%
   2.600 -\begin{isamarkuptext}%
   2.601 -Obviously, polymorphic equality is implemented the Haskell
   2.602 -  way using a type class.  How is this achieved?  By an
   2.603 -  almost trivial definition in the HOL setup:%
   2.604 -\end{isamarkuptext}%
   2.605 -\isamarkuptrue%
   2.606 -%
   2.607 -\isadelimML
   2.608 -%
   2.609 -\endisadelimML
   2.610 -%
   2.611 -\isatagML
   2.612 -%
   2.613 -\endisatagML
   2.614 -{\isafoldML}%
   2.615 -%
   2.616 -\isadelimML
   2.617 -%
   2.618 -\endisadelimML
   2.619 -\isanewline
   2.620 -\isacommand{class}\isamarkupfalse%
   2.621 -\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ type%
   2.622 -\begin{isamarkuptext}%
   2.623 -This merely introduces a class \isa{eq} with corresponding
   2.624 -  operation \isa{op\ {\isacharequal}};
   2.625 -  the preprocessing framework does the rest.%
   2.626 -\end{isamarkuptext}%
   2.627 -\isamarkuptrue%
   2.628 -%
   2.629 -\isadelimML
   2.630 -%
   2.631 -\endisadelimML
   2.632 -%
   2.633 -\isatagML
   2.634 -%
   2.635 -\endisatagML
   2.636 -{\isafoldML}%
   2.637 -%
   2.638 -\isadelimML
   2.639 -%
   2.640 -\endisadelimML
   2.641 -%
   2.642 -\begin{isamarkuptext}%
   2.643 -For datatypes, instances of \isa{eq} are implicitly derived
   2.644 -  when possible.
   2.645 -
   2.646 -  Though this class is designed to get rarely in the way, there
   2.647 -  are some cases when it suddenly comes to surface:%
   2.648 -\end{isamarkuptext}%
   2.649 -\isamarkuptrue%
   2.650 -%
   2.651 -\isamarkupsubsubsection{typedecls interpreted by customary serializations%
   2.652 -}
   2.653 -\isamarkuptrue%
   2.654 -%
   2.655 -\begin{isamarkuptext}%
   2.656 -A common idiom is to use unspecified types for formalizations
   2.657 -  and interpret them for a specific target language:%
   2.658 -\end{isamarkuptext}%
   2.659 -\isamarkuptrue%
   2.660 -\isacommand{typedecl}\isamarkupfalse%
   2.661 -\ key\isanewline
   2.662 -\isanewline
   2.663 -\isacommand{fun}\isamarkupfalse%
   2.664 -\isanewline
   2.665 -\ \ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}key\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ list\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ {\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   2.666 -\ \ \ \ {\isachardoublequoteopen}lookup\ {\isacharbrackleft}{\isacharbrackright}\ l\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
   2.667 -\ \ {\isacharbar}\ {\isachardoublequoteopen}lookup\ {\isacharparenleft}{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharhash}\ xs{\isacharparenright}\ l\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isacharequal}\ l\ then\ Some\ v\ else\ lookup\ xs\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.668 -%
   2.669 -\isadelimtt
   2.670 -\isanewline
   2.671 -%
   2.672 -\endisadelimtt
   2.673 -%
   2.674 -\isatagtt
   2.675 -\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   2.676 -\ key\isanewline
   2.677 -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}string{\isachardoublequoteclose}{\isacharparenright}%
   2.678 -\endisatagtt
   2.679 -{\isafoldtt}%
   2.680 -%
   2.681 -\isadelimtt
   2.682 -%
   2.683 -\endisadelimtt
   2.684 -%
   2.685 -\begin{isamarkuptext}%
   2.686 -This, though, is not sufficient: \isa{key} is no instance
   2.687 -  of \isa{eq} since \isa{key} is no datatype; the instance
   2.688 -  has to be declared manually, including a serialization
   2.689 -  for the particular instance of \isa{op\ {\isacharequal}}:%
   2.690 -\end{isamarkuptext}%
   2.691 -\isamarkuptrue%
   2.692 -\isacommand{instance}\isamarkupfalse%
   2.693 -\ key\ {\isacharcolon}{\isacharcolon}\ eq%
   2.694 -\isadelimproof
   2.695 -\ %
   2.696 -\endisadelimproof
   2.697 -%
   2.698 -\isatagproof
   2.699 -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   2.700 -%
   2.701 -\endisatagproof
   2.702 -{\isafoldproof}%
   2.703 -%
   2.704 -\isadelimproof
   2.705 -%
   2.706 -\endisadelimproof
   2.707 -\isanewline
   2.708 -%
   2.709 -\isadelimtt
   2.710 -\isanewline
   2.711 -%
   2.712 -\endisadelimtt
   2.713 -%
   2.714 -\isatagtt
   2.715 -\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   2.716 -\ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isasymColon}\ key\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   2.717 -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ string{\isacharparenright}\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
   2.718 -\endisatagtt
   2.719 -{\isafoldtt}%
   2.720 -%
   2.721 -\isadelimtt
   2.722 -%
   2.723 -\endisadelimtt
   2.724 -%
   2.725 -\begin{isamarkuptext}%
   2.726 -Then everything goes fine:%
   2.727 -\end{isamarkuptext}%
   2.728 -\isamarkuptrue%
   2.729 -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   2.730 -\ lookup\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lookup{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   2.731 -\begin{isamarkuptext}%
   2.732 -\lstsml{Thy/examples/lookup.ML}%
   2.733 -\end{isamarkuptext}%
   2.734 -\isamarkuptrue%
   2.735 -%
   2.736 -\isamarkupsubsubsection{lexicographic orderings%
   2.737 -}
   2.738 -\isamarkuptrue%
   2.739 -%
   2.740 -\begin{isamarkuptext}%
   2.741 -Another subtlety
   2.742 -  enters the stage when definitions of overloaded constants
   2.743 -  are dependent on operational equality.  For example, let
   2.744 -  us define a lexicographic ordering on tuples:%
   2.745 -\end{isamarkuptext}%
   2.746 -\isamarkuptrue%
   2.747 -\isacommand{instance}\isamarkupfalse%
   2.748 -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
   2.749 -\ \ less{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
   2.750 -\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.751 -\ \ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
   2.752 -\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
   2.753 -\isadelimproof
   2.754 -\ %
   2.755 -\endisadelimproof
   2.756 -%
   2.757 -\isatagproof
   2.758 -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   2.759 -%
   2.760 -\endisatagproof
   2.761 -{\isafoldproof}%
   2.762 -%
   2.763 -\isadelimproof
   2.764 -%
   2.765 -\endisadelimproof
   2.766 -\isanewline
   2.767 -\isanewline
   2.768 -\isacommand{lemmas}\isamarkupfalse%
   2.769 -\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline
   2.770 -\isanewline
   2.771 -\isacommand{lemma}\isamarkupfalse%
   2.772 -\ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   2.773 -\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.774 -\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.775 -%
   2.776 -\isadelimproof
   2.777 -\ \ %
   2.778 -\endisadelimproof
   2.779 -%
   2.780 -\isatagproof
   2.781 -\isacommand{unfolding}\isamarkupfalse%
   2.782 -\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   2.783 -\ simp{\isacharunderscore}all%
   2.784 -\endisatagproof
   2.785 -{\isafoldproof}%
   2.786 -%
   2.787 -\isadelimproof
   2.788 -%
   2.789 -\endisadelimproof
   2.790 -%
   2.791 -\begin{isamarkuptext}%
   2.792 -Then code generation will fail.  Why?  The definition
   2.793 -  of \isa{op\ {\isasymle}} depends on equality on both arguments,
   2.794 -  which are polymorphic and impose an additional \isa{eq}
   2.795 -  class constraint, thus violating the type discipline
   2.796 -  for class operations.
   2.797 -
   2.798 -  The solution is to add \isa{eq} explicitly to the first sort arguments in the
   2.799 -  code theorems:%
   2.800 -\end{isamarkuptext}%
   2.801 -\isamarkuptrue%
   2.802 -\isanewline
   2.803 -\isacommand{lemma}\isamarkupfalse%
   2.804 -\ ord{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   2.805 -\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.806 -\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   2.807 -%
   2.808 -\isadelimproof
   2.809 -\ \ %
   2.810 -\endisadelimproof
   2.811 -%
   2.812 -\isatagproof
   2.813 -\isacommand{unfolding}\isamarkupfalse%
   2.814 -\ ord{\isacharunderscore}prod\ \isacommand{by}\isamarkupfalse%
   2.815 -\ rule{\isacharplus}%
   2.816 -\endisatagproof
   2.817 -{\isafoldproof}%
   2.818 -%
   2.819 -\isadelimproof
   2.820 -%
   2.821 -\endisadelimproof
   2.822 -%
   2.823 -\begin{isamarkuptext}%
   2.824 -Then code generation succeeds:%
   2.825 -\end{isamarkuptext}%
   2.826 -\isamarkuptrue%
   2.827 -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   2.828 -\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   2.829 -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   2.830 -\begin{isamarkuptext}%
   2.831 -\lstsml{Thy/examples/lexicographic.ML}%
   2.832 -\end{isamarkuptext}%
   2.833 -\isamarkuptrue%
   2.834 -%
   2.835 -\begin{isamarkuptext}%
   2.836 -In general, code theorems for overloaded constants may have more
   2.837 -  restrictive sort constraints than the underlying instance relation
   2.838 -  between class and type constructor as long as the whole system of
   2.839 -  constraints is coregular; code theorems violating coregularity
   2.840 -  are rejected immediately.  Consequently, it might be necessary
   2.841 -  to delete disturbing theorems in the code theorem table,
   2.842 -  as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def}
   2.843 -  and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.%
   2.844 -\end{isamarkuptext}%
   2.845 -\isamarkuptrue%
   2.846 -%
   2.847  \isamarkupsubsubsection{Haskell serialization%
   2.848  }
   2.849  \isamarkuptrue%
   2.850 @@ -1261,20 +1108,6 @@
   2.851  \end{isamarkuptext}%
   2.852  \isamarkuptrue%
   2.853  %
   2.854 -\isadelimML
   2.855 -%
   2.856 -\endisadelimML
   2.857 -%
   2.858 -\isatagML
   2.859 -%
   2.860 -\endisatagML
   2.861 -{\isafoldML}%
   2.862 -%
   2.863 -\isadelimML
   2.864 -%
   2.865 -\endisadelimML
   2.866 -\isanewline
   2.867 -%
   2.868  \isadelimtt
   2.869  %
   2.870  \endisadelimtt
   2.871 @@ -1282,12 +1115,11 @@
   2.872  \isatagtt
   2.873  \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
   2.874  \ eq\isanewline
   2.875 -\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ eq\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   2.876 +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   2.877  \isanewline
   2.878  \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   2.879 -\ eq\isanewline
   2.880 -\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   2.881 -%
   2.882 +\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
   2.883 +\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
   2.884  \endisatagtt
   2.885  {\isafoldtt}%
   2.886  %
   2.887 @@ -1295,19 +1127,6 @@
   2.888  %
   2.889  \endisadelimtt
   2.890  %
   2.891 -\isadelimML
   2.892 -%
   2.893 -\endisadelimML
   2.894 -%
   2.895 -\isatagML
   2.896 -%
   2.897 -\endisatagML
   2.898 -{\isafoldML}%
   2.899 -%
   2.900 -\isadelimML
   2.901 -%
   2.902 -\endisadelimML
   2.903 -%
   2.904  \begin{isamarkuptext}%
   2.905  A problem now occurs whenever a type which
   2.906    is an instance of \isa{eq} in HOL is mapped
   2.907 @@ -1374,78 +1193,119 @@
   2.908  %
   2.909  \endisadelimtt
   2.910  %
   2.911 -\isamarkupsubsection{Types matter%
   2.912 +\isamarkupsubsubsection{Pretty printing%
   2.913 +}
   2.914 +\isamarkuptrue%
   2.915 +%
   2.916 +\begin{isamarkuptext}%
   2.917 +The serializer provides ML interfaces to set up
   2.918 +  pretty serializations for expressions like lists, numerals
   2.919 +  and characters;  these are
   2.920 +  monolithic stubs and should only be used with the
   2.921 +  theories introduces in \secref{sec:library}.%
   2.922 +\end{isamarkuptext}%
   2.923 +\isamarkuptrue%
   2.924 +%
   2.925 +\isamarkupsubsection{Constructor sets for datatypes%
   2.926  }
   2.927  \isamarkuptrue%
   2.928  %
   2.929  \begin{isamarkuptext}%
   2.930 -Imagine the following quick-and-dirty setup for implementing
   2.931 -  some kind of sets as lists in SML:%
   2.932 +Conceptually, any datatype is spanned by a set of
   2.933 +  \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n}
   2.934 +  where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is excactly the set of \emph{all}
   2.935 +  type variables in \isa{{\isasymtau}}.  The HOL datatype package
   2.936 +  by default registers any new datatype in the table
   2.937 +  of datatypes, which may be inspected using
   2.938 +  the \isa{{\isasymPRINTCODESETUP}} command.
   2.939 +
   2.940 +  In some cases, it may be convenient to alter or
   2.941 +  extend this table;  as an example, we show
   2.942 +  how to implement finite sets by lists
   2.943 +  using the conversion \isa{{\isachardoublequote}set\ {\isasymColon}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequote}}
   2.944 +  as constructor:%
   2.945  \end{isamarkuptext}%
   2.946  \isamarkuptrue%
   2.947 -%
   2.948 -\isadelimtt
   2.949 -%
   2.950 -\endisadelimtt
   2.951 -%
   2.952 -\isatagtt
   2.953 -\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
   2.954 +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
   2.955  \ set\isanewline
   2.956 -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharunderscore}\ list{\isachardoublequoteclose}{\isacharparenright}\isanewline
   2.957 -\isanewline
   2.958 -\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   2.959 -\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ insert\isanewline
   2.960 -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{and}\ \isakeyword{infixl}\ {\isadigit{7}}\ {\isachardoublequoteopen}{\isacharcolon}{\isacharcolon}{\isachardoublequoteclose}{\isacharparenright}%
   2.961 -\endisatagtt
   2.962 -{\isafoldtt}%
   2.963 -%
   2.964 -\isadelimtt
   2.965 -%
   2.966 -\endisadelimtt
   2.967 -\isanewline
   2.968 -\isanewline
   2.969 -\isacommand{definition}\isamarkupfalse%
   2.970  \isanewline
   2.971 -\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   2.972 -\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}Suc{\isacharbraceright}{\isachardoublequoteclose}%
   2.973 -\begin{isamarkuptext}%
   2.974 -Then code generation for \isa{dummy{\isacharunderscore}set} will fail.
   2.975 -  Why? A glimpse at the defining equations will offer:%
   2.976 -\end{isamarkuptext}%
   2.977 -\isamarkuptrue%
   2.978 -\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
   2.979 -\ insert%
   2.980 -\begin{isamarkuptext}%
   2.981 -This reveals the defining equation \isa{insert\ {\isacharquery}a\ {\isacharquery}B\ {\isasymequiv}\ {\isacharbraceleft}x{\isachardot}\ x\ {\isacharequal}\ {\isacharquery}a{\isacharbraceright}\ {\isasymunion}\ {\isacharquery}B}
   2.982 -  for \isa{insert}, which is operationally meaningless
   2.983 -  but forces an equality constraint on the set members
   2.984 -  (which is not satisfiable if the set members are functions).
   2.985 -  Even when using set of natural numbers (which are an instance
   2.986 -  of \emph{eq}), we run into a problem:%
   2.987 -\end{isamarkuptext}%
   2.988 -\isamarkuptrue%
   2.989 -\isacommand{definition}\isamarkupfalse%
   2.990 -\isanewline
   2.991 -\ \ foobar{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   2.992 -\ \ {\isachardoublequoteopen}foobar{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequoteclose}%
   2.993 -\begin{isamarkuptext}%
   2.994 -In this case the serializer would complain that \isa{insert}
   2.995 -  expects dictionaries (namely an \emph{eq} dictionary) but
   2.996 -  has also been given a customary serialization.
   2.997 -
   2.998 -  \fixme[needs rewrite] The solution to this dilemma:%
   2.999 -\end{isamarkuptext}%
  2.1000 -\isamarkuptrue%
  2.1001  \isacommand{lemma}\isamarkupfalse%
  2.1002 -\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
  2.1003 -\ \ {\isachardoublequoteopen}insert\ {\isacharequal}\ insert{\isachardoublequoteclose}%
  2.1004 +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}\ {\isacharequal}\ set\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}%
  2.1005  \isadelimproof
  2.1006  \ %
  2.1007  \endisadelimproof
  2.1008  %
  2.1009  \isatagproof
  2.1010 -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
  2.1011 +\isacommand{by}\isamarkupfalse%
  2.1012 +\ simp%
  2.1013 +\endisatagproof
  2.1014 +{\isafoldproof}%
  2.1015 +%
  2.1016 +\isadelimproof
  2.1017 +%
  2.1018 +\endisadelimproof
  2.1019 +\isanewline
  2.1020 +\isanewline
  2.1021 +\isacommand{lemma}\isamarkupfalse%
  2.1022 +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}insert\ x\ {\isacharparenleft}set\ xs{\isacharparenright}\ {\isacharequal}\ set\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}{\isachardoublequoteclose}%
  2.1023 +\isadelimproof
  2.1024 +\ %
  2.1025 +\endisadelimproof
  2.1026 +%
  2.1027 +\isatagproof
  2.1028 +\isacommand{by}\isamarkupfalse%
  2.1029 +\ simp%
  2.1030 +\endisatagproof
  2.1031 +{\isafoldproof}%
  2.1032 +%
  2.1033 +\isadelimproof
  2.1034 +%
  2.1035 +\endisadelimproof
  2.1036 +\isanewline
  2.1037 +\isanewline
  2.1038 +\isacommand{lemma}\isamarkupfalse%
  2.1039 +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}%
  2.1040 +\isadelimproof
  2.1041 +\ %
  2.1042 +\endisadelimproof
  2.1043  %
  2.1044 +\isatagproof
  2.1045 +\isacommand{by}\isamarkupfalse%
  2.1046 +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
  2.1047 +\endisatagproof
  2.1048 +{\isafoldproof}%
  2.1049 +%
  2.1050 +\isadelimproof
  2.1051 +%
  2.1052 +\endisadelimproof
  2.1053 +\isanewline
  2.1054 +\isanewline
  2.1055 +\isacommand{lemma}\isamarkupfalse%
  2.1056 +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymunion}\ set\ ys\ {\isacharequal}\ foldr\ insert\ ys\ xs{\isachardoublequoteclose}%
  2.1057 +\isadelimproof
  2.1058 +\ %
  2.1059 +\endisadelimproof
  2.1060 +%
  2.1061 +\isatagproof
  2.1062 +\isacommand{by}\isamarkupfalse%
  2.1063 +\ {\isacharparenleft}induct\ ys{\isacharparenright}\ simp{\isacharunderscore}all%
  2.1064 +\endisatagproof
  2.1065 +{\isafoldproof}%
  2.1066 +%
  2.1067 +\isadelimproof
  2.1068 +%
  2.1069 +\endisadelimproof
  2.1070 +\isanewline
  2.1071 +\isanewline
  2.1072 +\isacommand{lemma}\isamarkupfalse%
  2.1073 +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymUnion}set\ xs\ {\isacharequal}\ foldr\ {\isacharparenleft}op\ {\isasymunion}{\isacharparenright}\ xs\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}%
  2.1074 +\isadelimproof
  2.1075 +\ %
  2.1076 +\endisadelimproof
  2.1077 +%
  2.1078 +\isatagproof
  2.1079 +\isacommand{by}\isamarkupfalse%
  2.1080 +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
  2.1081  \endisatagproof
  2.1082  {\isafoldproof}%
  2.1083  %
  2.1084 @@ -1455,51 +1315,14 @@
  2.1085  \isanewline
  2.1086  \isanewline
  2.1087  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
  2.1088 -\ dummy{\isacharunderscore}set\ foobar{\isacharunderscore}set\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}dirty{\isacharunderscore}set{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
  2.1089 +\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ insert\ {\isachardoublequoteopen}op\ {\isasymin}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymunion}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Union{\isachardoublequoteclose}\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}set{\isacharunderscore}list{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
  2.1090  \begin{isamarkuptext}%
  2.1091 -\lstsml{Thy/examples/dirty_set.ML}
  2.1092 -
  2.1093 -  Reflexive defining equations by convention are dropped:%
  2.1094 -\end{isamarkuptext}%
  2.1095 -\isamarkuptrue%
  2.1096 -\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
  2.1097 -\ insert%
  2.1098 -\begin{isamarkuptext}%
  2.1099 -will show \emph{no} defining equations for insert.
  2.1100 +\lstsml{Thy/examples/set_list.ML}
  2.1101  
  2.1102 -  Note that the sort constraints of reflexive equations
  2.1103 -  are considered; so%
  2.1104 -\end{isamarkuptext}%
  2.1105 -\isamarkuptrue%
  2.1106 -\isacommand{lemma}\isamarkupfalse%
  2.1107 -\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
  2.1108 -\ \ {\isachardoublequoteopen}{\isacharparenleft}insert\ {\isasymColon}\ {\isacharprime}a{\isasymColon}eq\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}\ {\isacharequal}\ insert{\isachardoublequoteclose}%
  2.1109 -\isadelimproof
  2.1110 -\ %
  2.1111 -\endisadelimproof
  2.1112 -%
  2.1113 -\isatagproof
  2.1114 -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
  2.1115 -%
  2.1116 -\endisatagproof
  2.1117 -{\isafoldproof}%
  2.1118 -%
  2.1119 -\isadelimproof
  2.1120 -%
  2.1121 -\endisadelimproof
  2.1122 -%
  2.1123 -\begin{isamarkuptext}%
  2.1124 -would mean nothing else than to introduce the evil
  2.1125 -  sort constraint by hand.%
  2.1126 -\end{isamarkuptext}%
  2.1127 -\isamarkuptrue%
  2.1128 -%
  2.1129 -\isamarkupsubsection{Constructor sets for datatypes%
  2.1130 -}
  2.1131 -\isamarkuptrue%
  2.1132 -%
  2.1133 -\begin{isamarkuptext}%
  2.1134 -\fixme%
  2.1135 +  \medskip
  2.1136 +
  2.1137 +  Changing the representation of existing datatypes requires
  2.1138 +  some care with respect to pattern matching and such.%
  2.1139  \end{isamarkuptext}%
  2.1140  \isamarkuptrue%
  2.1141  %
  2.1142 @@ -1532,6 +1355,25 @@
  2.1143  \end{isamarkuptext}%
  2.1144  \isamarkuptrue%
  2.1145  %
  2.1146 +\isamarkupsubsection{Incremental code generation%
  2.1147 +}
  2.1148 +\isamarkuptrue%
  2.1149 +%
  2.1150 +\begin{isamarkuptext}%
  2.1151 +Code generation is \emph{incremental}: theorems
  2.1152 +  and abstract intermediate code are cached and extended on demand.
  2.1153 +  The cache may be partially or fully dropped if the underlying
  2.1154 +  executable content of the theory changes.
  2.1155 +  Implementation of caching is supposed to transparently
  2.1156 +  hid away the details from the user.  Anyway, caching
  2.1157 +  reaches the surface by using a slightly more general form
  2.1158 +  of the \isa{{\isasymCODETHMS}}, \isa{{\isasymCODEDEPS}}
  2.1159 +  and \isa{{\isasymCODEGEN}} commands: the list of constants
  2.1160 +  may be omitted.  Then, all constants with code theorems
  2.1161 +  in the current cache are referred to.%
  2.1162 +\end{isamarkuptext}%
  2.1163 +\isamarkuptrue%
  2.1164 +%
  2.1165  \isamarkupsubsection{Axiomatic extensions%
  2.1166  }
  2.1167  \isamarkuptrue%
  2.1168 @@ -1611,6 +1453,8 @@
  2.1169  \begin{isamarkuptext}%
  2.1170  \lstsml{Thy/examples/arbitrary.ML}
  2.1171  
  2.1172 +  \medskip
  2.1173 +
  2.1174    Another axiomatic extension is code generation
  2.1175    for abstracted types.  For this, the  
  2.1176    \isa{ExecutableRat} (see \secref{exec_rat})
  2.1177 @@ -1911,13 +1755,13 @@
  2.1178  
  2.1179    \item \isa{merge} merging two data slots.
  2.1180  
  2.1181 -  \item \isa{purge}~\isa{thy}~\isa{cs} propagates changes in executable content;
  2.1182 +  \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content;
  2.1183      if possible, the current theory context is handed over
  2.1184      as argument \isa{thy} (if there is no current theory context (e.g.~during
  2.1185 -    theory merge, \verb|NONE|); \isa{cs} indicates the kind
  2.1186 +    theory merge, \verb|NONE|); \isa{consts} indicates the kind
  2.1187      of change: \verb|NONE| stands for a fundamental change
  2.1188 -    which invalidates any existing code, \isa{SOME\ cs}
  2.1189 -    hints that executable content for constants \isa{cs}
  2.1190 +    which invalidates any existing code, \isa{SOME\ consts}
  2.1191 +    hints that executable content for constants \isa{consts}
  2.1192      has changed.
  2.1193  
  2.1194    \end{description}
  2.1195 @@ -1948,6 +1792,109 @@
  2.1196  \end{isamarkuptext}%
  2.1197  \isamarkuptrue%
  2.1198  %
  2.1199 +\isamarkupsubsubsection{Building implementable systems fo defining equations%
  2.1200 +}
  2.1201 +\isamarkuptrue%
  2.1202 +%
  2.1203 +\begin{isamarkuptext}%
  2.1204 +Out of the executable content of a theory, a normalized
  2.1205 +  defining equation systems may be constructed containing
  2.1206 +  function definitions for constants.  The system is cached
  2.1207 +  until its underlying executable content changes.
  2.1208 +
  2.1209 +  Defining equations are retrieved by instantiation
  2.1210 +  of the functor \verb|CodegenFuncgrRetrieval|
  2.1211 +  which takes two arguments:
  2.1212 +
  2.1213 +  \medskip
  2.1214 +  \begin{tabular}{l}
  2.1215 +  \isa{val\ name{\isacharcolon}\ string} \\
  2.1216 +  \isa{val\ rewrites{\isacharcolon}\ theory\ {\isasymrightarrow}\ thm\ list}
  2.1217 +  \end{tabular}
  2.1218 +
  2.1219 +  \begin{description}
  2.1220 +
  2.1221 +  \item \isa{name} is a system-wide unique name identifying
  2.1222 +    this particular system of defining equations.
  2.1223 +
  2.1224 +  \item \isa{rewrites} specifies a set of theory-dependent
  2.1225 +    rewrite rules which are added to the preprocessor setup;
  2.1226 +    if no additional preprocessing is required, pass
  2.1227 +    a function returning an empty list.
  2.1228 +
  2.1229 +  \end{description}
  2.1230 +
  2.1231 +  An instance of \verb|CodegenFuncgrRetrieval| in essence
  2.1232 +  provides the following interface:
  2.1233 +
  2.1234 +  \medskip
  2.1235 +  \begin{tabular}{l}
  2.1236 +  \isa{make{\isacharcolon}\ theory\ {\isasymrightarrow}\ CodegenConsts{\isachardot}const\ list\ {\isasymrightarrow}\ CodegenFuncgr{\isachardot}T} \\
  2.1237 +  \end{tabular}
  2.1238 +
  2.1239 +  \begin{description}
  2.1240 +
  2.1241 +  \item \isa{make}~\isa{thy}~\isa{consts} returns
  2.1242 +    a system of defining equations which is guaranteed
  2.1243 +    to contain all defining equations for constants \isa{consts}
  2.1244 +    including all defining equations any defining equation
  2.1245 +    for any constant in \isa{consts} depends on.
  2.1246 +
  2.1247 +  \end{description}
  2.1248 +
  2.1249 +  Systems of defining equations are graphs accesible by the
  2.1250 +  following operations:%
  2.1251 +\end{isamarkuptext}%
  2.1252 +\isamarkuptrue%
  2.1253 +%
  2.1254 +\isadelimmlref
  2.1255 +%
  2.1256 +\endisadelimmlref
  2.1257 +%
  2.1258 +\isatagmlref
  2.1259 +%
  2.1260 +\begin{isamarkuptext}%
  2.1261 +\begin{mldecls}
  2.1262 +  \indexmltype{CodegenFuncgr.T}\verb|type CodegenFuncgr.T| \\
  2.1263 +  \indexml{CodegenFuncgr.funcs}\verb|CodegenFuncgr.funcs: CodegenFuncgr.T -> CodegenConsts.const -> thm list| \\
  2.1264 +  \indexml{CodegenFuncgr.typ}\verb|CodegenFuncgr.typ: CodegenFuncgr.T -> CodegenConsts.const -> typ| \\
  2.1265 +  \indexml{CodegenFuncgr.deps}\verb|CodegenFuncgr.deps: CodegenFuncgr.T|\isasep\isanewline%
  2.1266 +\verb|    -> CodegenConsts.const list -> CodegenConsts.const list list| \\
  2.1267 +  \indexml{CodegenFuncgr.all}\verb|CodegenFuncgr.all: CodegenFuncgr.T -> CodegenConsts.const list|
  2.1268 +  \end{mldecls}
  2.1269 +
  2.1270 +  \begin{description}
  2.1271 +
  2.1272 +  \item \verb|CodegenFuncgr.T| represents
  2.1273 +    a normalized defining equation system.
  2.1274 +
  2.1275 +  \item \verb|CodegenFuncgr.funcs|~\isa{funcgr}~\isa{const}
  2.1276 +    retrieves defining equiations for constant \isa{const}.
  2.1277 +
  2.1278 +  \item \verb|CodegenFuncgr.typ|~\isa{funcgr}~\isa{const}
  2.1279 +    retrieves function type for constant \isa{const}.
  2.1280 +
  2.1281 +  \item \verb|CodegenFuncgr.deps|~\isa{funcgr}~\isa{consts}
  2.1282 +    returns the transitive closure of dependencies for
  2.1283 +    constants \isa{consts} as a partitioning where each partition
  2.1284 +    corresponds to a strongly connected component of
  2.1285 +    dependencies and any partition does \emph{not}
  2.1286 +    depend on partitions further left.
  2.1287 +
  2.1288 +  \item \verb|CodegenFuncgr.all|~\isa{funcgr}
  2.1289 +    returns all currently represented constants.
  2.1290 +
  2.1291 +  \end{description}%
  2.1292 +\end{isamarkuptext}%
  2.1293 +\isamarkuptrue%
  2.1294 +%
  2.1295 +\endisatagmlref
  2.1296 +{\isafoldmlref}%
  2.1297 +%
  2.1298 +\isadelimmlref
  2.1299 +%
  2.1300 +\endisadelimmlref
  2.1301 +%
  2.1302  \isamarkupsubsubsection{Datatype hooks%
  2.1303  }
  2.1304  \isamarkuptrue%
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Apr 26 12:00:12 2007 +0200
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Apr 26 13:32:55 2007 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4    nulla :: a;
     3.5  };
     3.6  
     3.7 -heada :: (Codegen.Null a) => [a] -> a;
     3.8 +heada :: (Codegen.Null b) => [b] -> b;
     3.9  heada (x : xs) = x;
    3.10  heada [] = Codegen.nulla;
    3.11  
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Apr 26 12:00:12 2007 +0200
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Apr 26 13:32:55 2007 +0200
     4.3 @@ -14,8 +14,8 @@
     4.4  type 'a null = {null : 'a};
     4.5  fun null (A_:'a null) = #null A_;
     4.6  
     4.7 -fun head A_ (x :: xs) = x
     4.8 -  | head A_ [] = null A_;
     4.9 +fun head B_ (x :: xs) = x
    4.10 +  | head B_ [] = null B_;
    4.11  
    4.12  val null_option : 'a option = NONE;
    4.13  
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Thu Apr 26 12:00:12 2007 +0200
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Thu Apr 26 13:32:55 2007 +0200
     5.3 @@ -14,8 +14,8 @@
     5.4  type 'a null = {null : 'a};;
     5.5  let null _A = _A.null;;
     5.6  
     5.7 -let rec head _A = function x :: xs -> x
     5.8 -                  | [] -> null _A;;
     5.9 +let rec head _B = function x :: xs -> x
    5.10 +                  | [] -> null _B;;
    5.11  
    5.12  let rec null_option = None;;
    5.13  
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Apr 26 12:00:12 2007 +0200
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Apr 26 13:32:55 2007 +0200
     6.3 @@ -21,12 +21,12 @@
     6.4  structure Codegen = 
     6.5  struct
     6.6  
     6.7 -fun collect_duplicates A_ xs ys (z :: zs) =
     6.8 -  (if List.memberl A_ z xs
     6.9 -    then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
    6.10 -           else collect_duplicates A_ xs (z :: ys) zs)
    6.11 -    else collect_duplicates A_ (z :: xs) (z :: ys) zs)
    6.12 -  | collect_duplicates A_ xs ys [] = xs;
    6.13 +fun collect_duplicates B_ xs ys (z :: zs) =
    6.14 +  (if List.memberl B_ z xs
    6.15 +    then (if List.memberl B_ z ys then collect_duplicates B_ xs ys zs
    6.16 +           else collect_duplicates B_ xs (z :: ys) zs)
    6.17 +    else collect_duplicates B_ (z :: xs) (z :: ys) zs)
    6.18 +  | collect_duplicates B_ xs ys [] = xs;
    6.19  
    6.20  end; (*struct Codegen*)
    6.21  
     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Thu Apr 26 12:00:12 2007 +0200
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Thu Apr 26 13:32:55 2007 +0200
     7.3 @@ -11,9 +11,73 @@
     7.4  structure Integer = 
     7.5  struct
     7.6  
     7.7 +datatype bit = B0 | B1;
     7.8 +
     7.9 +datatype int = Pls | Min | Bit of int * bit | Number_of_int of int;
    7.10 +
    7.11 +fun pred (Bit (k, B0)) = Bit (pred k, B1)
    7.12 +  | pred (Bit (k, B1)) = Bit (k, B0)
    7.13 +  | pred Min = Bit (Min, B0)
    7.14 +  | pred Pls = Min;
    7.15 +
    7.16 +fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w)
    7.17 +  | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0)
    7.18 +  | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1)
    7.19 +  | uminus_int Min = Bit (Pls, B1)
    7.20 +  | uminus_int Pls = Pls;
    7.21 +
    7.22 +fun succ (Bit (k, B0)) = Bit (k, B1)
    7.23 +  | succ (Bit (k, B1)) = Bit (succ k, B0)
    7.24 +  | succ Min = Pls
    7.25 +  | succ Pls = Bit (Pls, B1);
    7.26 +
    7.27 +fun plus_int (Number_of_int v) (Number_of_int w) =
    7.28 +  Number_of_int (plus_int v w)
    7.29 +  | plus_int k Min = pred k
    7.30 +  | plus_int k Pls = k
    7.31 +  | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0)
    7.32 +  | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1)
    7.33 +  | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b)
    7.34 +  | plus_int Min k = pred k
    7.35 +  | plus_int Pls k = k;
    7.36 +
    7.37 +fun minus_int (Number_of_int v) (Number_of_int w) =
    7.38 +  Number_of_int (plus_int v (uminus_int w))
    7.39 +  | minus_int z w = plus_int z (uminus_int w);
    7.40 +
    7.41 +fun less_eq_int (Number_of_int k) (Number_of_int l) = less_eq_int k l
    7.42 +  | less_eq_int (Bit (k1, B1)) (Bit (k2, B0)) = less_int k1 k2
    7.43 +  | less_eq_int (Bit (k1, v)) (Bit (k2, B1)) = less_eq_int k1 k2
    7.44 +  | less_eq_int (Bit (k1, B0)) (Bit (k2, v)) = less_eq_int k1 k2
    7.45 +  | less_eq_int (Bit (k, v)) Min = less_eq_int k Min
    7.46 +  | less_eq_int (Bit (k, B1)) Pls = less_int k Pls
    7.47 +  | less_eq_int (Bit (k, B0)) Pls = less_eq_int k Pls
    7.48 +  | less_eq_int Min (Bit (k, B1)) = less_eq_int Min k
    7.49 +  | less_eq_int Min (Bit (k, B0)) = less_int Min k
    7.50 +  | less_eq_int Min Min = true
    7.51 +  | less_eq_int Min Pls = true
    7.52 +  | less_eq_int Pls (Bit (k, v)) = less_eq_int Pls k
    7.53 +  | less_eq_int Pls Min = false
    7.54 +  | less_eq_int Pls Pls = true
    7.55 +and less_int (Number_of_int k) (Number_of_int l) = less_int k l
    7.56 +  | less_int (Bit (k1, B0)) (Bit (k2, B1)) = less_eq_int k1 k2
    7.57 +  | less_int (Bit (k1, B1)) (Bit (k2, v)) = less_int k1 k2
    7.58 +  | less_int (Bit (k1, v)) (Bit (k2, B0)) = less_int k1 k2
    7.59 +  | less_int (Bit (k, B1)) Min = less_int k Min
    7.60 +  | less_int (Bit (k, B0)) Min = less_eq_int k Min
    7.61 +  | less_int (Bit (k, v)) Pls = less_int k Pls
    7.62 +  | less_int Min (Bit (k, v)) = less_int Min k
    7.63 +  | less_int Min Min = false
    7.64 +  | less_int Min Pls = true
    7.65 +  | less_int Pls (Bit (k, B1)) = less_eq_int Pls k
    7.66 +  | less_int Pls (Bit (k, B0)) = less_int Pls k
    7.67 +  | less_int Pls Min = false
    7.68 +  | less_int Pls Pls = false;
    7.69 +
    7.70  fun nat_aux n i =
    7.71 -  (if IntInf.<= (i, (0 : IntInf.int)) then n
    7.72 -    else nat_aux (Nat.Suc n) (IntInf.- (i, (1 : IntInf.int))));
    7.73 +  (if less_eq_int i (Number_of_int Pls) then n
    7.74 +    else nat_aux (Nat.Suc n)
    7.75 +           (minus_int i (Number_of_int (Bit (Pls, B1)))));
    7.76  
    7.77  fun nat i = nat_aux Nat.Zero_nat i;
    7.78  
    7.79 @@ -26,7 +90,12 @@
    7.80  
    7.81  val foobar_set : Nat.nat list =
    7.82    Nat.Zero_nat ::
    7.83 -    (Nat.Suc Nat.Zero_nat :: (Integer.nat (2 : IntInf.int) :: []));
    7.84 +    (Nat.Suc Nat.Zero_nat ::
    7.85 +      (Integer.nat
    7.86 +         (Integer.Number_of_int
    7.87 +           (Integer.Bit
    7.88 +             (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0)))
    7.89 +        :: []));
    7.90  
    7.91  end; (*struct Codegen*)
    7.92  
     8.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Thu Apr 26 12:00:12 2007 +0200
     8.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Thu Apr 26 13:32:55 2007 +0200
     8.3 @@ -1,11 +1,58 @@
     8.4  structure ROOT = 
     8.5  struct
     8.6  
     8.7 +structure Integer = 
     8.8 +struct
     8.9 +
    8.10 +datatype bit = B0 | B1;
    8.11 +
    8.12 +datatype int = Pls | Min | Bit of int * bit | Number_of_int of int;
    8.13 +
    8.14 +fun pred (Bit (k, B0)) = Bit (pred k, B1)
    8.15 +  | pred (Bit (k, B1)) = Bit (k, B0)
    8.16 +  | pred Min = Bit (Min, B0)
    8.17 +  | pred Pls = Min;
    8.18 +
    8.19 +fun succ (Bit (k, B0)) = Bit (k, B1)
    8.20 +  | succ (Bit (k, B1)) = Bit (succ k, B0)
    8.21 +  | succ Min = Pls
    8.22 +  | succ Pls = Bit (Pls, B1);
    8.23 +
    8.24 +fun plus_int (Number_of_int v) (Number_of_int w) =
    8.25 +  Number_of_int (plus_int v w)
    8.26 +  | plus_int k Min = pred k
    8.27 +  | plus_int k Pls = k
    8.28 +  | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0)
    8.29 +  | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1)
    8.30 +  | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b)
    8.31 +  | plus_int Min k = pred k
    8.32 +  | plus_int Pls k = k;
    8.33 +
    8.34 +fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w)
    8.35 +  | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0)
    8.36 +  | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1)
    8.37 +  | uminus_int Min = Bit (Pls, B1)
    8.38 +  | uminus_int Pls = Pls;
    8.39 +
    8.40 +fun times_int (Number_of_int v) (Number_of_int w) =
    8.41 +  Number_of_int (times_int v w)
    8.42 +  | times_int (Bit (k, B0)) l = Bit (times_int k l, B0)
    8.43 +  | times_int (Bit (k, B1)) l = plus_int (Bit (times_int k l, B0)) l
    8.44 +  | times_int Min k = uminus_int k
    8.45 +  | times_int Pls w = Pls;
    8.46 +
    8.47 +end; (*struct Integer*)
    8.48 +
    8.49  structure Codegen = 
    8.50  struct
    8.51  
    8.52  fun double_inc k =
    8.53 -  IntInf.+ ((IntInf.* ((2 : IntInf.int), k)), (1 : IntInf.int));
    8.54 +  Integer.plus_int
    8.55 +    (Integer.times_int
    8.56 +      (Integer.Number_of_int
    8.57 +        (Integer.Bit (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0)))
    8.58 +      k)
    8.59 +    (Integer.Number_of_int (Integer.Bit (Integer.Pls, Integer.B1)));
    8.60  
    8.61  end; (*struct Codegen*)
    8.62  
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Thu Apr 26 13:32:55 2007 +0200
     9.3 @@ -0,0 +1,41 @@
     9.4 +structure ROOT = 
     9.5 +struct
     9.6 +
     9.7 +structure Code_Generator = 
     9.8 +struct
     9.9 +
    9.10 +type 'a eq = {op_eq : 'a -> 'a -> bool};
    9.11 +fun op_eq (A_:'a eq) = #op_eq A_;
    9.12 +
    9.13 +end; (*struct Code_Generator*)
    9.14 +
    9.15 +structure List = 
    9.16 +struct
    9.17 +
    9.18 +fun foldr f (x :: xs) a = f x (foldr f xs a)
    9.19 +  | foldr f [] a = a;
    9.20 +
    9.21 +fun memberl A_ x (y :: ys) =
    9.22 +  Code_Generator.op_eq A_ x y orelse memberl A_ x ys
    9.23 +  | memberl A_ x [] = false;
    9.24 +
    9.25 +end; (*struct List*)
    9.26 +
    9.27 +structure Set = 
    9.28 +struct
    9.29 +
    9.30 +datatype 'a set = Set of 'a list;
    9.31 +
    9.32 +fun opa A_ x (Set xs) = List.memberl A_ x xs;
    9.33 +
    9.34 +val empty : 'a set = Set [];
    9.35 +
    9.36 +fun insert x (Set xs) = Set (x :: xs);
    9.37 +
    9.38 +fun op_Un xs (Set ys) = List.foldr insert ys xs;
    9.39 +
    9.40 +fun union (Set xs) = List.foldr op_Un xs empty;
    9.41 +
    9.42 +end; (*struct Set*)
    9.43 +
    9.44 +end; (*struct ROOT*)
    10.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Thu Apr 26 12:00:12 2007 +0200
    10.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Thu Apr 26 13:32:55 2007 +0200
    10.3 @@ -47,6 +47,8 @@
    10.4    Nibble5 | Nibble6 | Nibble7 | Nibble8 | Nibble9 | NibbleA | NibbleB |
    10.5    NibbleC | NibbleD | NibbleE | NibbleF;
    10.6  
    10.7 +datatype char = Char of nibble * nibble;
    10.8 +
    10.9  end; (*struct List*)
   10.10  
   10.11  structure Codegen = 
   10.12 @@ -55,19 +57,26 @@
   10.13  datatype ('a, 'b) searchtree = Leaf of 'a * 'b |
   10.14    Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree;
   10.15  
   10.16 -fun update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) =
   10.17 -  (if Orderings.less_eq A2_ it key
   10.18 -    then Branch (update (A1_, A2_) (it, entry) t1, key, t2)
   10.19 -    else Branch (t1, key, update (A1_, A2_) (it, entry) t2))
   10.20 -  | update (A1_, A2_) (it, entry) (Leaf (key, vala)) =
   10.21 -    (if Code_Generator.op_eq A1_ it key then Leaf (key, entry)
   10.22 -      else (if Orderings.less_eq A2_ it key
   10.23 +fun update (C1_, C2_) (it, entry) (Branch (t1, key, t2)) =
   10.24 +  (if Orderings.less_eq C2_ it key
   10.25 +    then Branch (update (C1_, C2_) (it, entry) t1, key, t2)
   10.26 +    else Branch (t1, key, update (C1_, C2_) (it, entry) t2))
   10.27 +  | update (C1_, C2_) (it, entry) (Leaf (key, vala)) =
   10.28 +    (if Code_Generator.op_eq C1_ it key then Leaf (key, entry)
   10.29 +      else (if Orderings.less_eq C2_ it key
   10.30               then Branch (Leaf (it, entry), it, Leaf (key, vala))
   10.31               else Branch (Leaf (key, vala), it, Leaf (it, entry))));
   10.32  
   10.33  fun example n =
   10.34 -  update (Nat.eq_nat, Nat.ord_nat) (n, [#"b", #"a", #"r"])
   10.35 -    (Leaf (Nat.Zero_nat, [#"f", #"o", #"o"]));
   10.36 +  update (Nat.eq_nat, Nat.ord_nat)
   10.37 +    (n, [List.Char (List.Nibble6, List.Nibble2),
   10.38 +          List.Char (List.Nibble6, List.Nibble1),
   10.39 +          List.Char (List.Nibble7, List.Nibble2)])
   10.40 +    (Leaf
   10.41 +      (Nat.Zero_nat,
   10.42 +        [List.Char (List.Nibble6, List.Nibble6),
   10.43 +          List.Char (List.Nibble6, List.NibbleF),
   10.44 +          List.Char (List.Nibble6, List.NibbleF)]));
   10.45  
   10.46  end; (*struct Codegen*)
   10.47  
    11.1 --- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Thu Apr 26 12:00:12 2007 +0200
    11.2 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Thu Apr 26 13:32:55 2007 +0200
    11.3 @@ -44,6 +44,7 @@
    11.4  \newcommand{\isasymCODEAXIOMS}{\cmd{code\_axioms}}
    11.5  \newcommand{\isasymCODEABSTYPE}{\cmd{code\_abstype}}
    11.6  \newcommand{\isasymPRINTCODESETUP}{\cmd{print\_codesetup}}
    11.7 +\newcommand{\isasymPRINTCLASSES}{\cmd{print\_classes}}
    11.8  \newcommand{\isasymCODETHMS}{\cmd{code\_thms}}
    11.9  \newcommand{\isasymCODEDEPS}{\cmd{code\_deps}}
   11.10  \newcommand{\isasymFUN}{\cmd{fun}}