author haftmann Thu Apr 26 13:32:55 2007 +0200 (2007-04-26) changeset 22798 e3962371f568 parent 22797 4b77a43f7f58 child 22799 ed7d53db2170
updated doc
     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.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.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.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.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.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.16 -\isanewline
2.17  %
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.26  %
2.28 @@ -310,7 +308,6 @@
2.30  %
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.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.106  \begin{isamarkuptext}%
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.264 +%
2.266 +%
2.267 +\isatagML
2.268 +%
2.269 +\endisatagML
2.270 +{\isafoldML}%
2.271 +%
2.273 +%
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.293 +%
2.295 +%
2.296 +\isatagML
2.297 +%
2.298 +\endisatagML
2.299 +{\isafoldML}%
2.300 +%
2.302 +%
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.309 +\ \ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\isanewline
2.313 +\ %
2.315 +%
2.316 +\isatagproof
2.317 +\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
2.318 +%
2.319 +\endisatagproof
2.320 +{\isafoldproof}%
2.321 +%
2.323 +%
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.334 +%
2.336 +\ \ %
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.347 +%
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.367 +%
2.369 +\ \ %
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.380 +%
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.452  %
2.454 @@ -769,7 +949,6 @@
2.455  {\isafoldtt}%
2.456  %
2.458 -\isanewline
2.459  %
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.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.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.530 -%
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.546 -%
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.608 -%
2.610 -%
2.611 -\isatagML
2.612 -%
2.613 -\endisatagML
2.614 -{\isafoldML}%
2.615 -%
2.617 -%
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.630 -%
2.632 -%
2.633 -\isatagML
2.634 -%
2.635 -\endisatagML
2.636 -{\isafoldML}%
2.637 -%
2.639 -%
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.670 -\isanewline
2.671 -%
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.682 -%
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.695 -\ %
2.697 -%
2.698 -\isatagproof
2.699 -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
2.700 -%
2.701 -\endisatagproof
2.702 -{\isafoldproof}%
2.703 -%
2.705 -%
2.707 -\isanewline
2.708 -%
2.710 -\isanewline
2.711 -%
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.722 -%
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.754 -\ %
2.756 -%
2.757 -\isatagproof
2.758 -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
2.759 -%
2.760 -\endisatagproof
2.761 -{\isafoldproof}%
2.762 -%
2.764 -%
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.775 -%
2.777 -\ \ %
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.788 -%
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.807 -%
2.809 -\ \ %
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.820 -%
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.848  }
2.849  \isamarkuptrue%
2.850 @@ -1261,20 +1108,6 @@
2.851  \end{isamarkuptext}%
2.852  \isamarkuptrue%
2.853  %
2.855 -%
2.857 -%
2.858 -\isatagML
2.859 -%
2.860 -\endisatagML
2.861 -{\isafoldML}%
2.862 -%
2.864 -%
2.866 -\isanewline
2.867 -%
2.869  %
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.881 -%
2.882 +\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
2.884  \endisatagtt
2.885  {\isafoldtt}%
2.886  %
2.887 @@ -1295,19 +1127,6 @@
2.888  %
2.890  %
2.892 -%
2.894 -%
2.895 -\isatagML
2.896 -%
2.897 -\endisatagML
2.898 -{\isafoldML}%
2.899 -%
2.901 -%
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.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.949 -%
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.965 -%
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.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.1006  \ %
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.1017 +%
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.1024 +\ %
2.1026 +%
2.1027 +\isatagproof
2.1028 +\isacommand{by}\isamarkupfalse%
2.1029 +\ simp%
2.1030 +\endisatagproof
2.1031 +{\isafoldproof}%
2.1032 +%
2.1034 +%
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.1041 +\ %
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.1051 +%
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.1058 +\ %
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.1068 +%
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.1075 +\ %
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.1110 -\ %
2.1112 -%
2.1113 -\isatagproof
2.1114 -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
2.1115 -%
2.1116 -\endisatagproof
2.1117 -{\isafoldproof}%
2.1118 -%
2.1120 -%
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.1255 +%
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.1299 +%
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.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}}