continued tutorial
authorhaftmann
Fri Nov 03 14:22:33 2006 +0100 (2006-11-03)
changeset 21147737a94f047e3
parent 21146 c6f103e57c94
child 21148 3a64d58a9f49
continued tutorial
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/bool2.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/bool3.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Nov 03 14:22:31 2006 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Nov 03 14:22:33 2006 +0100
     1.3 @@ -1,10 +1,18 @@
     1.4  
     1.5  (* $Id$ *)
     1.6  
     1.7 +(*<*)
     1.8  theory Codegen
     1.9  imports Main
    1.10 +uses "../../../IsarImplementation/Thy/setup.ML"
    1.11  begin
    1.12  
    1.13 +ML {*
    1.14 +CodegenSerializer.sml_code_width := 74;
    1.15 +*}
    1.16 +
    1.17 +(*>*)
    1.18 +
    1.19  chapter {* Code generation from Isabelle theories *}
    1.20  
    1.21  section {* Introduction *}
    1.22 @@ -48,7 +56,7 @@
    1.23    The code generator aims to be usable with no further ado
    1.24    in most cases while allowing for detailed customization.
    1.25    This manifests in the structure of this tutorial: this introduction
    1.26 -  continous with a short introduction of concepts.  Section
    1.27 +  continues with a short introduction of concepts.  Section
    1.28    \secref{sec:basics} explains how to use the framework naivly,
    1.29    presuming a reasonable default setup.  Then, section
    1.30    \secref{sec:advanced} deals with advanced topics,
    1.31 @@ -60,7 +68,7 @@
    1.32      Ultimately, the code generator which this tutorial deals with
    1.33      is supposed to replace the already established code generator
    1.34      by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
    1.35 -    So, for the momennt, there are two distinct code generators
    1.36 +    So, for the moment, there are two distinct code generators
    1.37      in Isabelle.
    1.38      Also note that while the framework itself is largely
    1.39      object-logic independent, only HOL provides a reasonable
    1.40 @@ -307,12 +315,12 @@
    1.41  text {*
    1.42    Type classes enter the game via the Isar class package.
    1.43    For a short introduction how to use it, see \cite{isabelle-classes};
    1.44 -  here we just illustrate its relation on code generation.
    1.45 +  here we just illustrate its impact on code generation.
    1.46  
    1.47    In a target language, type classes may be represented
    1.48    nativly (as in the case of Haskell). For languages
    1.49    like SML, they are implemented using \emph{dictionaries}.
    1.50 -  Our following example specified a class \qt{null},
    1.51 +  Our following example specifiedsa class \qt{null},
    1.52    assigning to each of its inhabitants a \qt{null} value:
    1.53  *}
    1.54  
    1.55 @@ -353,7 +361,8 @@
    1.56  *}
    1.57  
    1.58  code_gen dummy (Haskell "examples/")
    1.59 -  (* NOTE: you may use Haskell only once in this document *)
    1.60 +  (* NOTE: you may use Haskell only once in this document, otherwise
    1.61 +  you have to work in distinct subdirectories *)
    1.62  
    1.63  text {*
    1.64    \lsthaskell{Thy/examples/Codegen.hs}
    1.65 @@ -436,7 +445,7 @@
    1.66      \item[EfficientNat] implements natural numbers by integers,
    1.67         which in geneal will result in higher efficency; pattern
    1.68         matching with @{const "0\<Colon>nat"} / @{const "Suc"}
    1.69 -       is eliminated.
    1.70 +       is eliminated. \label{eff_nat}
    1.71      \item[MLString] provides an additional datatype @{text "mlstring"};
    1.72         in the HOL default setup, strings in HOL are mapped to list
    1.73         of chars in SML; values of type @{text "mlstring"} are
    1.74 @@ -448,24 +457,507 @@
    1.75  subsection {* Preprocessing *}
    1.76  
    1.77  text {*
    1.78 -  
    1.79 +  Before selected function theorems are turned into abstract
    1.80 +  code, a chain of definitional transformation steps is carried
    1.81 +  out: \emph{preprocessing}. There are three possibilites
    1.82 +  to customize preprocessing: \emph{inline theorems},
    1.83 +  \emph{inline procedures} and \emph{generic preprocessors}.
    1.84 +
    1.85 +  \emph{Inline theorems} are rewriting rules applied to each
    1.86 +  function equation.  Due to the interpretation of theorems
    1.87 +  of function equations, rewrites are applied to the right
    1.88 +  hand side and the arguments of the left hand side of an
    1.89 +  equation, but never to the constant heading the left hand side.
    1.90 +  Inline theorems may be declared an undeclared using the
    1.91 +  \emph{code inline} or \emph{code noinline} attribute respectivly.
    1.92 +
    1.93 +  Some common applications:
    1.94 +*}
    1.95 +
    1.96 +text_raw {*
    1.97 +  \begin{itemize}
    1.98 +     \item replacing non-executable constructs by executable ones: \\
    1.99 +*}     
   1.100 +
   1.101 +lemma [code inline]:
   1.102 +  "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
   1.103 +
   1.104 +text_raw {*
   1.105 +     \item eliminating superfluous constants: \\
   1.106 +*}
   1.107 +
   1.108 +lemma [code inline]:
   1.109 +  "1 = Suc 0" by simp
   1.110 +
   1.111 +text_raw {*
   1.112 +     \item replacing executable but inconvenient constructs: \\
   1.113  *}
   1.114  
   1.115 -(* preprocessing, print_codethms () *)
   1.116 +lemma [code inline]:
   1.117 +  "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
   1.118 +
   1.119 +text_raw {*
   1.120 +  \end{itemize}
   1.121 +*}
   1.122 +
   1.123 +text {*
   1.124 +  The current set of inline theorems may be inspected using
   1.125 +  the \isasymPRINTCODETHMS command.
   1.126 +
   1.127 +  \emph{Inline procedures} are a generalized version of inline
   1.128 +  theorems written in ML -- rewrite rules are generated dependent
   1.129 +  on the function theorems for a certain function.  One
   1.130 +  application is the implicit expanding of @{typ nat} numerals
   1.131 +  to @{const "0\<Colon>nat"} / @{const Suc} representation.  See further
   1.132 +  \secref{sec:ml}
   1.133 +
   1.134 +  \emph{Generic preprocessors} provide a most general interface,
   1.135 +  transforming a list of function theorems to another
   1.136 +  list of function theorems, provided that neither the heading
   1.137 +  constant nor its type change.  The @{const "0\<Colon>nat"} / @{const Suc}
   1.138 +  pattern elimination implemented in \secref{eff_nat} uses this
   1.139 +  interface.
   1.140 +
   1.141 +  \begin{warn}
   1.142 +    The order in which single preprocessing steps are carried
   1.143 +    out currently is not specified; in particular, preprocessing
   1.144 +    is \emph{no} fixpoint process.  Keep this in mind when
   1.145 +    setting up the preprocessor.
   1.146 +
   1.147 +    Further, the attribute \emph{code unfold}
   1.148 +    associated with the existing code generator also applies to
   1.149 +    the new one: \emph{code unfold} implies \emph{code inline}.
   1.150 +  \end{warn}
   1.151 +*}
   1.152  
   1.153  subsection {* Customizing serialization  *}
   1.154  
   1.155 -(* code_reserved *)
   1.156 -(* existing libraries, understanding the type game, reflexive equations, code inline code_constsubst, code_abstype*)
   1.157 +text {*
   1.158 +  Consider the following function and its corresponding
   1.159 +  SML code:
   1.160 +*}
   1.161 +
   1.162 +fun
   1.163 +  in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
   1.164 +  "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
   1.165 +termination by (auto_term "{}")
   1.166 +(*<*)
   1.167 +declare in_interval.simps [code func]
   1.168 +(*>*)
   1.169 +
   1.170 +(*<*)
   1.171 +code_type bool
   1.172 +  (SML)
   1.173 +code_const True and False and "op \<and>" and Not
   1.174 +  (SML and and and)
   1.175 +(*>*)
   1.176 +
   1.177 +code_gen in_interval (SML "examples/bool1.ML")
   1.178 +
   1.179 +text {*
   1.180 +  \lstsml{Thy/examples/bool1.ML}
   1.181 +
   1.182 +  Though this is correct code, it is a little bit unsatisfactory:
   1.183 +  boolean values and operators are materialized as distinguished
   1.184 +  entities with have nothing to do with the SML-builtin notion
   1.185 +  of \qt{bool}.  This results in less readable code;
   1.186 +  additionally, eager evaluation may cause programs to
   1.187 +  loop or break which would perfectly terminate when
   1.188 +  the existing SML \qt{bool} would be used.  To map
   1.189 +  the HOL \qt{bool} on SML \qt{bool}, we may use
   1.190 +  \qn{custom serializations}:
   1.191 +*}
   1.192 +
   1.193 +code_type bool
   1.194 +  (SML "bool")
   1.195 +code_const True and False and "op \<and>"
   1.196 +  (SML "true" and "false" and "_ andalso _")
   1.197 +
   1.198 +text {*
   1.199 +  The \isasymCODETYPE commad takes a type constructor
   1.200 +  as arguments together with a list of custom serializations.
   1.201 +  Each custom serialization starts with a target language
   1.202 +  identifier followed by an expression, which during
   1.203 +  code serialization is inserted whenever the type constructor
   1.204 +  would occur.  For constants, \isasymCODECONST implements
   1.205 +  the corresponding mechanism.  Each \qt{\_} in
   1.206 +  a serialization expression is treated as a placeholder
   1.207 +  for the type constructor's (the constant's) arguments.
   1.208 +*}
   1.209 +
   1.210 +code_reserved SML
   1.211 +  bool true false
   1.212 +
   1.213 +text {*
   1.214 +  To assert that the existing \qt{bool}, \qt{true} and \qt{false}
   1.215 +  is not used for generated code, we use \isasymCODERESERVED.
   1.216 +
   1.217 +  After this setup, code looks quite more readable:
   1.218 +*}
   1.219 +
   1.220 +code_gen in_interval (SML "examples/bool2.ML")
   1.221 +
   1.222 +text {*
   1.223 +  \lstsml{Thy/examples/bool2.ML}
   1.224 +
   1.225 +  This still is not perfect: the parentheses
   1.226 +  around \qt{andalso} are superfluos.  Though the serializer
   1.227 +  by no means attempts to imitate the rich Isabelle syntax
   1.228 +  framework, it provides some common idioms, notably
   1.229 +  associative infixes with precedences which may be used here:
   1.230 +*}
   1.231 +
   1.232 +code_const "op \<and>"
   1.233 +  (SML infixl 1 "andalso")
   1.234 +
   1.235 +code_gen in_interval (SML "examples/bool3.ML")
   1.236 +
   1.237 +text {*
   1.238 +  \lstsml{Thy/examples/bool3.ML}
   1.239 +
   1.240 +  Next, we try to map HOL pairs to SML pairs, using the
   1.241 +  infix \qt{ * } type constructor and parentheses:
   1.242 +*}
   1.243 +
   1.244 +(*<*)
   1.245 +code_type *
   1.246 +  (SML)
   1.247 +code_const Pair
   1.248 +  (SML)
   1.249 +(*>*)
   1.250 +
   1.251 +code_type *
   1.252 +  (SML infix 2 "*")
   1.253 +
   1.254 +code_const Pair
   1.255 +  (SML "!((_),/ (_))")
   1.256 +
   1.257 +text {*
   1.258 +  The initial bang \qt{!} tells the serializer to never put
   1.259 +  parentheses around the whole expression (they are already present),
   1.260 +  while the parentheses around argument place holders
   1.261 +  tell not to put parentheses around the arguments.
   1.262 +  The slash \qt{/} (followed by arbitrary white space)
   1.263 +  inserts a space which may be used as a break if necessary
   1.264 +  during pretty printing.
   1.265 +
   1.266 +  So far, 
   1.267 +*}
   1.268 +
   1.269 +code_type int
   1.270 +  (SML "IntInf.int")
   1.271 +  (Haskell "Integer")
   1.272 +
   1.273 +code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   1.274 +    and "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   1.275 +    and "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   1.276 +  (SML "IntInf.+ (_, _)" and "IntInf.- (_, _)" and "IntInf.* (_, _)")
   1.277 +  (Haskell infixl 6 "+" and infixl 6 "-" and infixl 7 "*")
   1.278 +
   1.279 +(* quote with ' HOL Setup, careful *)
   1.280 +
   1.281 +
   1.282 +(* Better ops, code_moduleprolog *)
   1.283 +(* code_modulename *)
   1.284 +
   1.285 +
   1.286 +subsection {* Types matter  *}
   1.287 +
   1.288 +(* shadowing by user-defined serilizations, understanding the type game,
   1.289 +reflexive equations, dangerous equations *)
   1.290 +
   1.291 +subsection {* Concerning operational equality *}
   1.292 +
   1.293 +text {*
   1.294 +  Surely you have already noticed how equality is treated
   1.295 +  by the code generator:
   1.296 +*}
   1.297 +
   1.298 +fun
   1.299 +  collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.300 +  "collect_duplicates xs ys [] = xs"
   1.301 +  "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
   1.302 +    then if z \<in> set ys
   1.303 +      then collect_duplicates xs ys zs
   1.304 +      else collect_duplicates xs (z#ys) zs
   1.305 +    else collect_duplicates (z#xs) (z#ys) zs)"
   1.306 +termination by (auto_term "measure (length o snd o snd)")
   1.307 +(*<*)
   1.308 +lemmas [code func] = collect_duplicates.simps
   1.309 +(*>*)
   1.310 +
   1.311 +text {*
   1.312 +  The membership test during preprocessing is rewritting,
   1.313 +  resulting in @{const List.memberl}, which itself
   1.314 +  performs an explicit equality check.
   1.315 +*}
   1.316 +
   1.317 +code_gen collect_duplicates (SML "examples/collect_duplicates.ML")
   1.318 +
   1.319 +text {*
   1.320 +  \lstsml{Thy/examples/collect_duplicates.ML}
   1.321 +*}
   1.322 +
   1.323 +text {*
   1.324 +  Obviously, polymorphic equality is implemented the Haskell
   1.325 +  way using a type class.  How is this achieved?  By an
   1.326 +  almost trivial definition in the HOL setup:
   1.327 +*}
   1.328 +
   1.329 +(*<*)
   1.330 +setup {* Sign.add_path "foo" *}
   1.331 +(*>*)
   1.332 +
   1.333 +class eq =
   1.334 +  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.335 +
   1.336 +defs
   1.337 +  eq [symmetric(*, code inline, code func*)]: "eq \<equiv> (op =)"
   1.338 +
   1.339 +text {*
   1.340 +  This merely introduces a class @{text eq} with corresponding
   1.341 +  operation @{const eq}, which by definition is isomorphic
   1.342 +  to @{const "op ="}; the preprocessing framework does the rest.
   1.343 +*}
   1.344 +
   1.345 +(*<*)
   1.346 +lemmas [code noinline] = eq
   1.347 +
   1.348 +hide (open) "class" eq
   1.349 +hide (open) const eq
   1.350 +
   1.351 +lemmas [symmetric, code func] = eq_def
   1.352 +
   1.353 +setup {* Sign.parent_path *}
   1.354 +(*>*)
   1.355 +
   1.356 +text {*
   1.357 +  For datatypes, instances of @{text eq} are implicitly derived
   1.358 +  when possible.
   1.359 +
   1.360 +  Though this class is designed to get rarely in the way, there
   1.361 +  are some cases when it suddenly comes to surface:
   1.362 +*}
   1.363 +
   1.364 +text_raw {*
   1.365 +  \begin {description}
   1.366 +    \item[code lemmas and customary serializations for equality]
   1.367 +      Examine the following: \\
   1.368 +*}
   1.369 +
   1.370 +code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   1.371 +  (SML "!(_ : IntInf.int = _)")
   1.372 +
   1.373 +text_raw {*
   1.374 +  \\ What is wrong here? Since @{const "op ="} is nothing else then
   1.375 +  a plain constant, this customary serialization will refer
   1.376 +  to polymorphic equality @{const "op = \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool"}.
   1.377 +  Instead, we want the specific equality on @{typ int},
   1.378 +  by using the overloaded constant @{const "Code_Generator.eq"}: \\
   1.379 +*}
   1.380 +
   1.381 +code_const "Code_Generator.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   1.382 +  (SML "!(_ : IntInf.int = _)")
   1.383 +
   1.384 +text_raw {*
   1.385 +  \\ \item[typedecls interpretated by customary serializations] A
   1.386 +  common idiom is to use unspecified types for formalizations
   1.387 +  and interpret them for a specific target language: \\
   1.388 +*}
   1.389 +
   1.390 +typedecl key
   1.391 +
   1.392 +fun
   1.393 +  lookup :: "(key \<times> 'a) list \<Rightarrow> key \<Rightarrow> 'a option" where
   1.394 +  "lookup [] l = None"
   1.395 +  "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)"
   1.396 +termination by (auto_term "measure (length o fst)")
   1.397 +(*<*)
   1.398 +lemmas [code func] = lookup.simps
   1.399 +(*>*)
   1.400 +
   1.401 +code_type key
   1.402 +  (SML "string")
   1.403 +
   1.404 +text_raw {*
   1.405 +  \\ This, though, is not sufficient: @{typ key} is no instance
   1.406 +  of @{text eq} since @{typ key} is no datatype; the instance
   1.407 +  has to be declared manually, including a serialization
   1.408 +  for the particular instance of @{const "Code_Generator.eq"}: \\
   1.409 +*}
   1.410 +
   1.411 +instance key :: eq ..
   1.412 +
   1.413 +code_const "Code_Generator.eq \<Colon> key \<Rightarrow> key \<Rightarrow> bool"
   1.414 +  (SML "!(_ : string = _)")
   1.415 +
   1.416 +text_raw {*
   1.417 +  \\ Then everything goes fine: \\
   1.418 +*}
   1.419 +
   1.420 +code_gen lookup (SML "examples/lookup.ML")
   1.421 +
   1.422 +text {*
   1.423 +  \lstsml{Thy/examples/lookup.ML}
   1.424 +*}
   1.425 +
   1.426 +text_raw {*
   1.427 +  \item[lexicographic orderings and corregularity] Another sublety
   1.428 +  enters the stage when definitions of overloaded constants
   1.429 +  are dependent on operational equality.  For example, let
   1.430 +  us define a lexicographic ordering on tuples: \\
   1.431 +*}
   1.432 +
   1.433 +(*<*)
   1.434 +(*setup {* Sign.add_path "foo" *}
   1.435 +
   1.436 +class ord = ord*)
   1.437 +(*>*)
   1.438 +
   1.439 +(*
   1.440 +instance * :: ("{eq, ord}", ord) ord
   1.441 +  "p1 < p2 \<equiv> let (x1, y1) = p1; (x2, y2) = p2 in
   1.442 +    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
   1.443 +  "p1 \<le> p2 \<equiv> p1 < p2 \<or> p1 = p2" ..
   1.444 +*)
   1.445 +
   1.446 +(*<*)
   1.447 +(*hide (open) "class" ord
   1.448 +setup {* Sign.parent_path *}*)
   1.449 +(*>*)
   1.450 +
   1.451 +text_raw {*
   1.452 +  \\ Then code generation will fail.  Why?  The definition
   1.453 +  of @{const "op \<le>"} depends on equality on both arguments,
   1.454 +  which are polymorhpic and impose an additional @{text eq}
   1.455 +  class constraint, thus violating the type discipline
   1.456 +  for class operations.
   1.457 +
   1.458 +  The solution is to add @{text eq} to both sort arguments: \\
   1.459 +*}
   1.460 +
   1.461 +instance * :: ("{eq, ord}", "{eq, ord}") ord
   1.462 +  "p1 < p2 \<equiv> let (x1, y1) = p1; (x2, y2) = p2 in
   1.463 +    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
   1.464 +  "p1 \<le> p2 \<equiv> p1 < p2 \<or> p1 = p2" ..
   1.465 +
   1.466 +text_raw {*
   1.467 +  \\ Then code generation succeeds: \\
   1.468 +*}
   1.469 +
   1.470 +code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>{eq, ord} \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   1.471 +  (SML "examples/lexicographic.ML")
   1.472 +
   1.473 +text {*
   1.474 +  \lstsml{Thy/examples/lexicographic.ML}
   1.475 +*}
   1.476 +
   1.477 +text_raw {*
   1.478 +  \item[Haskell serialization]
   1.479 +*}
   1.480 +
   1.481 +text_raw {*
   1.482 +  \end {description}
   1.483 +*}
   1.484 +
   1.485 +
   1.486 +subsection {* Axiomatic extensions *}
   1.487 +
   1.488 +text {*
   1.489 +  \begin{warn}
   1.490 +    The extensions introduced in this section, though working
   1.491 +    in practice, are not the cream of the crop.  They will
   1.492 +    eventually be replaced by more mature approaches.
   1.493 +  \end{warn}
   1.494 +*}
   1.495 +
   1.496 +(* existing libraries, code inline code_constsubst, code_abstype*)
   1.497  
   1.498  section {* ML interfaces \label{sec:ml} *}
   1.499  
   1.500 -(* under developement *)
   1.501 +subsection {* Constants with type discipline: codegen\_consts.ML *}
   1.502 +
   1.503 +text %mlref {*
   1.504 +  \begin{mldecls}
   1.505 +  @{index_ML_type CodegenConsts.const} \\
   1.506 +  @{index_ML CodegenConsts.inst_of_typ: "theory -> string * typ -> CodegenConsts.const"} \\
   1.507 +  @{index_ML CodegenConsts.typ_of_inst: "theory -> CodegenConsts.const -> string * typ"} \\
   1.508 +  @{index_ML CodegenConsts.norm: "theory -> CodegenConsts.const -> CodegenConsts.const"} \\
   1.509 +  @{index_ML CodegenConsts.norm_of_typ: "theory -> string * typ -> CodegenConsts.const"}
   1.510 +  \end{mldecls}
   1.511 +*}
   1.512 +
   1.513 +subsection {* Executable theory content: codegen\_data.ML *}
   1.514 +
   1.515 +text {*
   1.516 +  This Pure module implements the core notions of
   1.517 +  executable content of a theory.
   1.518 +*}
   1.519 +
   1.520 +subsubsection {* Suspended theorems *}
   1.521 +
   1.522 +text %mlref {*
   1.523 +  \begin{mldecls}
   1.524 +  @{index_ML_type CodegenData.lthms} \\
   1.525 +  @{index_ML CodegenData.lazy: "(unit -> thm list) -> CodegenData.lthms"}
   1.526 +  \end{mldecls}
   1.527 +*}
   1.528 +
   1.529 +subsubsection {* Executable content *}
   1.530  
   1.531 -subsection {* codegen\_data.ML *}
   1.532 +text %mlref {*
   1.533 +  \begin{mldecls}
   1.534 +  @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\
   1.535 +  @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\
   1.536 +  @{index_ML CodegenData.add_funcl: "CodegenConsts.const * CodegenData.lthms -> theory -> theory"} \\
   1.537 +  @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list) * CodegenData.lthms) -> theory -> theory"} \\
   1.538 +  @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\
   1.539 +  @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\
   1.540 +  @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\
   1.541 +  @{index_ML CodegenData.add_inline_proc: "(theory -> cterm list -> thm list) -> theory -> theory"} \\
   1.542 +  @{index_ML CodegenData.add_preproc: "(theory -> thm list -> thm list) -> theory -> theory"} \\
   1.543 +  @{index_ML CodegenData.these_funcs: "theory -> CodegenConsts.const -> thm list"} \\
   1.544 +  @{index_ML CodegenData.get_datatype: "theory -> string -> ((string * sort) list * (string * typ list) list) option"} \\
   1.545 +  @{index_ML CodegenData.get_datatype_of_constr: "theory -> CodegenConsts.const -> string option"}
   1.546 +  \end{mldecls}
   1.547 +
   1.548 +  \begin{description}
   1.549 +
   1.550 +  \item @{ML CodegenData.add_func}~@{text "thm"}
   1.551 +
   1.552 +  \end{description}
   1.553 +*}
   1.554 +
   1.555 +subsection {* Further auxiliary *}
   1.556 +
   1.557 +text %mlref {*
   1.558 +  \begin{mldecls}
   1.559 +  @{index_ML CodegenConsts.const_ord: "CodegenConsts.const * CodegenConsts.const -> order"} \\
   1.560 +  @{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\
   1.561 +  @{index_ML CodegenConsts.consts_of: "theory -> term -> CodegenConsts.const list"} \\
   1.562 +  @{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\
   1.563 +  @{index_ML_structure CodegenConsts.Consttab} \\
   1.564 +  @{index_ML CodegenData.typ_func: "theory -> thm -> typ"} \\
   1.565 +  @{index_ML CodegenData.rewrite_func: "thm list -> thm -> thm"} \\
   1.566 +  \end{mldecls}
   1.567 +*}
   1.568  
   1.569  subsection {* Implementing code generator applications *}
   1.570  
   1.571 -(* hooks *)
   1.572 +text {*
   1.573 +  \begin{warn}
   1.574 +    Some interfaces discussed here have not reached
   1.575 +    a final state yet.
   1.576 +    Changes likely to occur in future.
   1.577 +  \end{warn}
   1.578 +*}
   1.579 +
   1.580 +subsubsection {* Data depending on the theory's executable content *}
   1.581 +
   1.582 +subsubsection {* Datatype hooks *}
   1.583 +
   1.584 +text {*
   1.585 +  \emph{Happy proving, happy hacking!}
   1.586 +*}
   1.587  
   1.588  end
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML	Fri Nov 03 14:22:31 2006 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML	Fri Nov 03 14:22:33 2006 +0100
     2.3 @@ -1,8 +1,4 @@
     2.4  
     2.5  (* $Id$ *)
     2.6  
     2.7 -CodegenSerializer.sml_code_width := 74;
     2.8 -
     2.9 -CodegenSerializer.sml_code_width := 74;
    2.10 -
    2.11  use_thy "Codegen";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Nov 03 14:22:33 2006 +0100
     3.3 @@ -0,0 +1,18 @@
     3.4 +module Codegen where
     3.5 +import qualified IntDef
     3.6 +
     3.7 +class Null a where
     3.8 +  null :: a
     3.9 +
    3.10 +head :: (Codegen.Null a_1) => [a_1] -> a_1
    3.11 +head (y : xs) = y
    3.12 +head [] = Codegen.null
    3.13 +
    3.14 +null_option :: Maybe b
    3.15 +null_option = Nothing
    3.16 +
    3.17 +instance Codegen.Null (Maybe b) where
    3.18 +  null = Codegen.null_option
    3.19 +
    3.20 +dummy :: Maybe IntDef.Nat
    3.21 +dummy = Codegen.head [Just (IntDef.Succ_nat IntDef.Zero_nat), Nothing]
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML	Fri Nov 03 14:22:33 2006 +0100
     4.3 @@ -0,0 +1,40 @@
     4.4 +structure ROOT = 
     4.5 +struct
     4.6 +
     4.7 +structure HOL = 
     4.8 +struct
     4.9 +
    4.10 +datatype boola = True | False;
    4.11 +
    4.12 +fun nota False = True
    4.13 +  | nota True = False;
    4.14 +
    4.15 +fun op_conj y True = y
    4.16 +  | op_conj x False = False
    4.17 +  | op_conj True ya = ya
    4.18 +  | op_conj False xa = False;
    4.19 +
    4.20 +end; (*struct HOL*)
    4.21 +
    4.22 +structure IntDef = 
    4.23 +struct
    4.24 +
    4.25 +datatype nat = Zero_nat | Succ_nat of nat;
    4.26 +
    4.27 +fun less_nat Zero_nat (Succ_nat n) = HOL.True
    4.28 +  | less_nat na Zero_nat = HOL.False
    4.29 +  | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb;
    4.30 +
    4.31 +fun less_eq_nat m n = HOL.nota (less_nat n m);
    4.32 +
    4.33 +end; (*struct IntDef*)
    4.34 +
    4.35 +structure Codegen = 
    4.36 +struct
    4.37 +
    4.38 +fun in_interval (k, l) n =
    4.39 +  HOL.op_conj (IntDef.less_eq_nat k n) (IntDef.less_eq_nat n l);
    4.40 +
    4.41 +end; (*struct Codegen*)
    4.42 +
    4.43 +end; (*struct ROOT*)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool2.ML	Fri Nov 03 14:22:33 2006 +0100
     5.3 @@ -0,0 +1,33 @@
     5.4 +structure ROOT = 
     5.5 +struct
     5.6 +
     5.7 +structure HOL = 
     5.8 +struct
     5.9 +
    5.10 +fun nota false = true
    5.11 +  | nota true = false;
    5.12 +
    5.13 +end; (*struct HOL*)
    5.14 +
    5.15 +structure IntDef = 
    5.16 +struct
    5.17 +
    5.18 +datatype nat = Zero_nat | Succ_nat of nat;
    5.19 +
    5.20 +fun less_nat Zero_nat (Succ_nat n) = true
    5.21 +  | less_nat na Zero_nat = false
    5.22 +  | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb;
    5.23 +
    5.24 +fun less_eq_nat m n = HOL.nota (less_nat n m);
    5.25 +
    5.26 +end; (*struct IntDef*)
    5.27 +
    5.28 +structure Codegen = 
    5.29 +struct
    5.30 +
    5.31 +fun in_interval (k, l) n =
    5.32 +  (IntDef.less_eq_nat k n) andalso (IntDef.less_eq_nat n l);
    5.33 +
    5.34 +end; (*struct Codegen*)
    5.35 +
    5.36 +end; (*struct ROOT*)
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool3.ML	Fri Nov 03 14:22:33 2006 +0100
     6.3 @@ -0,0 +1,33 @@
     6.4 +structure ROOT = 
     6.5 +struct
     6.6 +
     6.7 +structure HOL = 
     6.8 +struct
     6.9 +
    6.10 +fun nota false = true
    6.11 +  | nota true = false;
    6.12 +
    6.13 +end; (*struct HOL*)
    6.14 +
    6.15 +structure IntDef = 
    6.16 +struct
    6.17 +
    6.18 +datatype nat = Zero_nat | Succ_nat of nat;
    6.19 +
    6.20 +fun less_nat Zero_nat (Succ_nat n) = true
    6.21 +  | less_nat na Zero_nat = false
    6.22 +  | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb;
    6.23 +
    6.24 +fun less_eq_nat m n = HOL.nota (less_nat n m);
    6.25 +
    6.26 +end; (*struct IntDef*)
    6.27 +
    6.28 +structure Codegen = 
    6.29 +struct
    6.30 +
    6.31 +fun in_interval (k, l) n =
    6.32 +  IntDef.less_eq_nat k n andalso IntDef.less_eq_nat n l;
    6.33 +
    6.34 +end; (*struct Codegen*)
    6.35 +
    6.36 +end; (*struct ROOT*)
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Nov 03 14:22:33 2006 +0100
     7.3 @@ -0,0 +1,29 @@
     7.4 +structure ROOT = 
     7.5 +struct
     7.6 +
     7.7 +structure IntDef = 
     7.8 +struct
     7.9 +
    7.10 +datatype nat = Zero_nat | Succ_nat of nat;
    7.11 +
    7.12 +end; (*struct IntDef*)
    7.13 +
    7.14 +structure Codegen = 
    7.15 +struct
    7.16 +
    7.17 +type 'a null = {null_ : 'a};
    7.18 +fun Null (A_:'a null) = #null_ A_;
    7.19 +
    7.20 +fun head (A_1_:'a_1 null) (y :: xs) = y
    7.21 +  | head (A_1_:'a_1 null) [] = Null A_1_;
    7.22 +
    7.23 +val null_option : 'b option = NONE;
    7.24 +
    7.25 +fun null_optiona () = {null_ = null_option} : ('b option) null
    7.26 +
    7.27 +val dummy : IntDef.nat option =
    7.28 +  head (null_optiona ()) [SOME (IntDef.Succ_nat IntDef.Zero_nat), NONE];
    7.29 +
    7.30 +end; (*struct Codegen*)
    7.31 +
    7.32 +end; (*struct ROOT*)
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Nov 03 14:22:33 2006 +0100
     8.3 @@ -0,0 +1,40 @@
     8.4 +structure ROOT = 
     8.5 +struct
     8.6 +
     8.7 +structure Code_Generator = 
     8.8 +struct
     8.9 +
    8.10 +type 'a eq = {eq_ : 'a -> 'a -> bool};
    8.11 +fun Eq (A_:'a eq) = #eq_ A_;
    8.12 +
    8.13 +end; (*struct Code_Generator*)
    8.14 +
    8.15 +structure HOL = 
    8.16 +struct
    8.17 +
    8.18 +fun op_eq (A_:'a Code_Generator.eq) a b = Code_Generator.Eq A_ a b;
    8.19 +
    8.20 +end; (*struct HOL*)
    8.21 +
    8.22 +structure List = 
    8.23 +struct
    8.24 +
    8.25 +fun memberl (A_1_:'a_1 Code_Generator.eq) x (y :: ys) =
    8.26 +  HOL.op_eq A_1_ x y orelse memberl A_1_ x ys
    8.27 +  | memberl (A_1_:'a_1 Code_Generator.eq) xa [] = false;
    8.28 +
    8.29 +end; (*struct List*)
    8.30 +
    8.31 +structure Codegen = 
    8.32 +struct
    8.33 +
    8.34 +fun collect_duplicates (A_:'a Code_Generator.eq) xs ys (z :: zs) =
    8.35 +  (if List.memberl A_ z xs
    8.36 +    then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
    8.37 +           else collect_duplicates A_ xs (z :: ys) zs)
    8.38 +    else collect_duplicates A_ (z :: xs) (z :: ys) zs)
    8.39 +  | collect_duplicates (A_:'a Code_Generator.eq) y ysa [] = y;
    8.40 +
    8.41 +end; (*struct Codegen*)
    8.42 +
    8.43 +end; (*struct ROOT*)
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Fri Nov 03 14:22:33 2006 +0100
     9.3 @@ -0,0 +1,25 @@
     9.4 +structure ROOT = 
     9.5 +struct
     9.6 +
     9.7 +structure IntDef = 
     9.8 +struct
     9.9 +
    9.10 +datatype nat = Zero_nat | Succ_nat of nat;
    9.11 +
    9.12 +fun plus_nat (Succ_nat m) n = plus_nat m (Succ_nat n)
    9.13 +  | plus_nat Zero_nat y = y;
    9.14 +
    9.15 +fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n)
    9.16 +  | times_nat Zero_nat na = Zero_nat;
    9.17 +
    9.18 +end; (*struct IntDef*)
    9.19 +
    9.20 +structure Codegen = 
    9.21 +struct
    9.22 +
    9.23 +fun fac (IntDef.Succ_nat n) = IntDef.times_nat (IntDef.Succ_nat n) (fac n)
    9.24 +  | fac IntDef.Zero_nat = IntDef.Succ_nat IntDef.Zero_nat;
    9.25 +
    9.26 +end; (*struct Codegen*)
    9.27 +
    9.28 +end; (*struct ROOT*)
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Fri Nov 03 14:22:33 2006 +0100
    10.3 @@ -0,0 +1,26 @@
    10.4 +structure ROOT = 
    10.5 +struct
    10.6 +
    10.7 +structure IntDef = 
    10.8 +struct
    10.9 +
   10.10 +datatype nat = Zero_nat | Succ_nat of nat;
   10.11 +
   10.12 +fun plus_nat (Succ_nat m) n = plus_nat m (Succ_nat n)
   10.13 +  | plus_nat Zero_nat y = y;
   10.14 +
   10.15 +fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n)
   10.16 +  | times_nat Zero_nat na = Zero_nat;
   10.17 +
   10.18 +end; (*struct IntDef*)
   10.19 +
   10.20 +structure Codegen = 
   10.21 +struct
   10.22 +
   10.23 +fun fac n =
   10.24 +  (case n of IntDef.Zero_nat => IntDef.Succ_nat IntDef.Zero_nat
   10.25 +     | IntDef.Succ_nat ma => IntDef.times_nat n (fac ma));
   10.26 +
   10.27 +end; (*struct Codegen*)
   10.28 +
   10.29 +end; (*struct ROOT*)
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Fri Nov 03 14:22:33 2006 +0100
    11.3 @@ -0,0 +1,51 @@
    11.4 +structure ROOT = 
    11.5 +struct
    11.6 +
    11.7 +structure Code_Generator = 
    11.8 +struct
    11.9 +
   11.10 +type 'a eq = {eq_ : 'a -> 'a -> bool};
   11.11 +fun Eq (A_:'a eq) = #eq_ A_;
   11.12 +
   11.13 +end; (*struct Code_Generator*)
   11.14 +
   11.15 +structure Product_Type = 
   11.16 +struct
   11.17 +
   11.18 +fun eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq) (x1, y1)
   11.19 +  (x2, y2) = Code_Generator.Eq A_ x1 x2 andalso Code_Generator.Eq B_ y1 y2;
   11.20 +
   11.21 +end; (*struct Product_Type*)
   11.22 +
   11.23 +structure Orderings = 
   11.24 +struct
   11.25 +
   11.26 +type 'a ord =
   11.27 +  {Code_Generator__eq : 'a Code_Generator.eq, less_eq_ : 'a -> 'a -> bool,
   11.28 +    less_ : 'a -> 'a -> bool};
   11.29 +fun Less_eq (A_:'a ord) = #less_eq_ A_;
   11.30 +fun Less (A_:'a ord) = #less_ A_;
   11.31 +
   11.32 +end; (*struct Orderings*)
   11.33 +
   11.34 +structure Codegen = 
   11.35 +struct
   11.36 +
   11.37 +fun less_prod (B_:'b Orderings.ord) (C_:'c Orderings.ord) p1 p2 =
   11.38 +  let
   11.39 +    val (x1a, y1a) = p1;
   11.40 +    val (x2a, y2a) = p2;
   11.41 +  in
   11.42 +    Orderings.Less B_ x1a x2a orelse
   11.43 +      Code_Generator.Eq (#Code_Generator__eq B_) x1a x2a andalso
   11.44 +        Orderings.Less C_ y1a y2a
   11.45 +  end;
   11.46 +
   11.47 +fun less_eq_prod (B_:'b Orderings.ord) (C_:'c Orderings.ord) p1 p2 =
   11.48 +  less_prod B_ C_ p1 p2 orelse
   11.49 +    Product_Type.eq_prod (#Code_Generator__eq B_) (#Code_Generator__eq C_)
   11.50 +      p1 p2;
   11.51 +
   11.52 +end; (*struct Codegen*)
   11.53 +
   11.54 +end; (*struct ROOT*)
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML	Fri Nov 03 14:22:33 2006 +0100
    12.3 @@ -0,0 +1,13 @@
    12.4 +structure ROOT = 
    12.5 +struct
    12.6 +
    12.7 +structure Codegen = 
    12.8 +struct
    12.9 +
   12.10 +fun lookup ((k, v) :: xs) l =
   12.11 +  (if (k : string = l) then SOME v else lookup xs l)
   12.12 +  | lookup [] la = NONE;
   12.13 +
   12.14 +end; (*struct Codegen*)
   12.15 +
   12.16 +end; (*struct ROOT*)
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Fri Nov 03 14:22:33 2006 +0100
    13.3 @@ -0,0 +1,34 @@
    13.4 +structure ROOT = 
    13.5 +struct
    13.6 +
    13.7 +structure IntDef = 
    13.8 +struct
    13.9 +
   13.10 +datatype nat = Zero_nat | Succ_nat of nat;
   13.11 +
   13.12 +fun less_nat Zero_nat (Succ_nat n) = true
   13.13 +  | less_nat na Zero_nat = false
   13.14 +  | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb;
   13.15 +
   13.16 +fun minus_nat (Succ_nat m) (Succ_nat n) = minus_nat m n
   13.17 +  | minus_nat Zero_nat na = Zero_nat
   13.18 +  | minus_nat y Zero_nat = y;
   13.19 +
   13.20 +end; (*struct IntDef*)
   13.21 +
   13.22 +structure Codegen = 
   13.23 +struct
   13.24 +
   13.25 +fun pick ((k, v) :: xs) n =
   13.26 +  (if IntDef.less_nat n k then v else pick xs (IntDef.minus_nat n k))
   13.27 +  | pick (x :: xsa) na =
   13.28 +    let
   13.29 +      val (ka, va) = x;
   13.30 +    in
   13.31 +      (if IntDef.less_nat na ka then va
   13.32 +        else pick xsa (IntDef.minus_nat na ka))
   13.33 +    end;
   13.34 +
   13.35 +end; (*struct Codegen*)
   13.36 +
   13.37 +end; (*struct ROOT*)
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Fri Nov 03 14:22:33 2006 +0100
    14.3 @@ -0,0 +1,27 @@
    14.4 +structure ROOT = 
    14.5 +struct
    14.6 +
    14.7 +structure IntDef = 
    14.8 +struct
    14.9 +
   14.10 +datatype nat = Zero_nat | Succ_nat of nat;
   14.11 +
   14.12 +fun less_nat Zero_nat (Succ_nat n) = true
   14.13 +  | less_nat na Zero_nat = false
   14.14 +  | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb;
   14.15 +
   14.16 +fun minus_nat (Succ_nat m) (Succ_nat n) = minus_nat m n
   14.17 +  | minus_nat Zero_nat na = Zero_nat
   14.18 +  | minus_nat y Zero_nat = y;
   14.19 +
   14.20 +end; (*struct IntDef*)
   14.21 +
   14.22 +structure Codegen = 
   14.23 +struct
   14.24 +
   14.25 +fun pick ((k, v) :: xs) n =
   14.26 +  (if IntDef.less_nat n k then v else pick xs (IntDef.minus_nat n k));
   14.27 +
   14.28 +end; (*struct Codegen*)
   14.29 +
   14.30 +end; (*struct ROOT*)