1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Codegen/Thy/Foundations.thy Fri Aug 13 14:41:27 2010 +0200
1.3 @@ -0,0 +1,432 @@
1.4 +theory Foundations
1.5 +imports Introduction
1.6 +begin
1.7 +
1.8 +section {* Code generation foundations \label{sec:program} *}
1.9 +
1.10 +subsection {* The @{text "Isabelle/HOL"} default setup *}
1.11 +
1.12 +text {*
1.13 + We have already seen how by default equations stemming from
1.14 + @{command definition}, @{command primrec} and @{command fun}
1.15 + statements are used for code generation. This default behaviour
1.16 + can be changed, e.g.\ by providing different code equations.
1.17 + The customisations shown in this section are \emph{safe}
1.18 + as regards correctness: all programs that can be generated are partially
1.19 + correct.
1.20 +*}
1.21 +
1.22 +subsection {* Selecting code equations *}
1.23 +
1.24 +text {*
1.25 + Coming back to our introductory example, we
1.26 + could provide an alternative code equations for @{const dequeue}
1.27 + explicitly:
1.28 +*}
1.29 +
1.30 +lemma %quote [code]:
1.31 + "dequeue (AQueue xs []) =
1.32 + (if xs = [] then (None, AQueue [] [])
1.33 + else dequeue (AQueue [] (rev xs)))"
1.34 + "dequeue (AQueue xs (y # ys)) =
1.35 + (Some y, AQueue xs ys)"
1.36 + by (cases xs, simp_all) (cases "rev xs", simp_all)
1.37 +
1.38 +text {*
1.39 + \noindent The annotation @{text "[code]"} is an @{text Isar}
1.40 + @{text attribute} which states that the given theorems should be
1.41 + considered as code equations for a @{text fun} statement --
1.42 + the corresponding constant is determined syntactically. The resulting code:
1.43 +*}
1.44 +
1.45 +text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
1.46 +
1.47 +text {*
1.48 + \noindent You may note that the equality test @{term "xs = []"} has been
1.49 + replaced by the predicate @{term "null xs"}. This is due to the default
1.50 + setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
1.51 +
1.52 + Changing the default constructor set of datatypes is also
1.53 + possible. See \secref{sec:datatypes} for an example.
1.54 +
1.55 + As told in \secref{sec:concept}, code generation is based
1.56 + on a structured collection of code theorems.
1.57 + This collection
1.58 + may be inspected using the @{command code_thms} command:
1.59 +*}
1.60 +
1.61 +code_thms %quote dequeue
1.62 +
1.63 +text {*
1.64 + \noindent prints a table with \emph{all} code equations
1.65 + for @{const dequeue}, including
1.66 + \emph{all} code equations those equations depend
1.67 + on recursively.
1.68 +
1.69 + Similarly, the @{command code_deps} command shows a graph
1.70 + visualising dependencies between code equations.
1.71 +*}
1.72 +
1.73 +subsection {* @{text class} and @{text instantiation} *}
1.74 +
1.75 +text {*
1.76 + Concerning type classes and code generation, let us examine an example
1.77 + from abstract algebra:
1.78 +*}
1.79 +
1.80 +class %quote semigroup =
1.81 + fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
1.82 + assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
1.83 +
1.84 +class %quote monoid = semigroup +
1.85 + fixes neutral :: 'a ("\<one>")
1.86 + assumes neutl: "\<one> \<otimes> x = x"
1.87 + and neutr: "x \<otimes> \<one> = x"
1.88 +
1.89 +instantiation %quote nat :: monoid
1.90 +begin
1.91 +
1.92 +primrec %quote mult_nat where
1.93 + "0 \<otimes> n = (0\<Colon>nat)"
1.94 + | "Suc m \<otimes> n = n + m \<otimes> n"
1.95 +
1.96 +definition %quote neutral_nat where
1.97 + "\<one> = Suc 0"
1.98 +
1.99 +lemma %quote add_mult_distrib:
1.100 + fixes n m q :: nat
1.101 + shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
1.102 + by (induct n) simp_all
1.103 +
1.104 +instance %quote proof
1.105 + fix m n q :: nat
1.106 + show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
1.107 + by (induct m) (simp_all add: add_mult_distrib)
1.108 + show "\<one> \<otimes> n = n"
1.109 + by (simp add: neutral_nat_def)
1.110 + show "m \<otimes> \<one> = m"
1.111 + by (induct m) (simp_all add: neutral_nat_def)
1.112 +qed
1.113 +
1.114 +end %quote
1.115 +
1.116 +text {*
1.117 + \noindent We define the natural operation of the natural numbers
1.118 + on monoids:
1.119 +*}
1.120 +
1.121 +primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
1.122 + "pow 0 a = \<one>"
1.123 + | "pow (Suc n) a = a \<otimes> pow n a"
1.124 +
1.125 +text {*
1.126 + \noindent This we use to define the discrete exponentiation function:
1.127 +*}
1.128 +
1.129 +definition %quote bexp :: "nat \<Rightarrow> nat" where
1.130 + "bexp n = pow n (Suc (Suc 0))"
1.131 +
1.132 +text {*
1.133 + \noindent The corresponding code in Haskell uses that language's native classes:
1.134 +*}
1.135 +
1.136 +text %quote {*@{code_stmts bexp (Haskell)}*}
1.137 +
1.138 +text {*
1.139 + \noindent This is a convenient place to show how explicit dictionary construction
1.140 + manifests in generated code (here, the same example in @{text SML})
1.141 + \cite{Haftmann-Nipkow:2010:code}:
1.142 +*}
1.143 +
1.144 +text %quote {*@{code_stmts bexp (SML)}*}
1.145 +
1.146 +text {*
1.147 + \noindent Note the parameters with trailing underscore (@{verbatim "A_"}),
1.148 + which are the dictionary parameters.
1.149 +*}
1.150 +
1.151 +subsection {* The preprocessor \label{sec:preproc} *}
1.152 +
1.153 +text {*
1.154 + Before selected function theorems are turned into abstract
1.155 + code, a chain of definitional transformation steps is carried
1.156 + out: \emph{preprocessing}. In essence, the preprocessor
1.157 + consists of two components: a \emph{simpset} and \emph{function transformers}.
1.158 +
1.159 + The \emph{simpset} can apply the full generality of the
1.160 + Isabelle simplifier. Due to the interpretation of theorems as code
1.161 + equations, rewrites are applied to the right hand side and the
1.162 + arguments of the left hand side of an equation, but never to the
1.163 + constant heading the left hand side. An important special case are
1.164 + \emph{unfold theorems}, which may be declared and removed using
1.165 + the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
1.166 + attribute, respectively.
1.167 +
1.168 + Some common applications:
1.169 +*}
1.170 +
1.171 +text_raw {*
1.172 + \begin{itemize}
1.173 +*}
1.174 +
1.175 +text {*
1.176 + \item replacing non-executable constructs by executable ones:
1.177 +*}
1.178 +
1.179 +lemma %quote [code_unfold]:
1.180 + "x \<in> set xs \<longleftrightarrow> List.member xs x" by (fact in_set_member)
1.181 +
1.182 +text {*
1.183 + \item eliminating superfluous constants:
1.184 +*}
1.185 +
1.186 +lemma %quote [code_unfold]:
1.187 + "1 = Suc 0" by (fact One_nat_def)
1.188 +
1.189 +text {*
1.190 + \item replacing executable but inconvenient constructs:
1.191 +*}
1.192 +
1.193 +lemma %quote [code_unfold]:
1.194 + "xs = [] \<longleftrightarrow> List.null xs" by (fact eq_Nil_null)
1.195 +
1.196 +text_raw {*
1.197 + \end{itemize}
1.198 +*}
1.199 +
1.200 +text {*
1.201 + \noindent \emph{Function transformers} provide a very general interface,
1.202 + transforming a list of function theorems to another
1.203 + list of function theorems, provided that neither the heading
1.204 + constant nor its type change. The @{term "0\<Colon>nat"} / @{const Suc}
1.205 + pattern elimination implemented in
1.206 + theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this
1.207 + interface.
1.208 +
1.209 + \noindent The current setup of the preprocessor may be inspected using
1.210 + the @{command print_codeproc} command.
1.211 + @{command code_thms} provides a convenient
1.212 + mechanism to inspect the impact of a preprocessor setup
1.213 + on code equations.
1.214 +
1.215 + \begin{warn}
1.216 +
1.217 + Attribute @{attribute code_unfold} also applies to the
1.218 + preprocessor of the ancient @{text "SML code generator"}; in case
1.219 + this is not what you intend, use @{attribute code_inline} instead.
1.220 + \end{warn}
1.221 +*}
1.222 +
1.223 +subsection {* Datatypes \label{sec:datatypes} *}
1.224 +
1.225 +text {*
1.226 + Conceptually, any datatype is spanned by a set of
1.227 + \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
1.228 + "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
1.229 + @{text "\<tau>"}. The HOL datatype package by default registers any new
1.230 + datatype in the table of datatypes, which may be inspected using the
1.231 + @{command print_codesetup} command.
1.232 +
1.233 + In some cases, it is appropriate to alter or extend this table. As
1.234 + an example, we will develop an alternative representation of the
1.235 + queue example given in \secref{sec:intro}. The amortised
1.236 + representation is convenient for generating code but exposes its
1.237 + \qt{implementation} details, which may be cumbersome when proving
1.238 + theorems about it. Therefore, here is a simple, straightforward
1.239 + representation of queues:
1.240 +*}
1.241 +
1.242 +datatype %quote 'a queue = Queue "'a list"
1.243 +
1.244 +definition %quote empty :: "'a queue" where
1.245 + "empty = Queue []"
1.246 +
1.247 +primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
1.248 + "enqueue x (Queue xs) = Queue (xs @ [x])"
1.249 +
1.250 +fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
1.251 + "dequeue (Queue []) = (None, Queue [])"
1.252 + | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
1.253 +
1.254 +text {*
1.255 + \noindent This we can use directly for proving; for executing,
1.256 + we provide an alternative characterisation:
1.257 +*}
1.258 +
1.259 +definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
1.260 + "AQueue xs ys = Queue (ys @ rev xs)"
1.261 +
1.262 +code_datatype %quote AQueue
1.263 +
1.264 +text {*
1.265 + \noindent Here we define a \qt{constructor} @{const "AQueue"} which
1.266 + is defined in terms of @{text "Queue"} and interprets its arguments
1.267 + according to what the \emph{content} of an amortised queue is supposed
1.268 + to be. Equipped with this, we are able to prove the following equations
1.269 + for our primitive queue operations which \qt{implement} the simple
1.270 + queues in an amortised fashion:
1.271 +*}
1.272 +
1.273 +lemma %quote empty_AQueue [code]:
1.274 + "empty = AQueue [] []"
1.275 + unfolding AQueue_def empty_def by simp
1.276 +
1.277 +lemma %quote enqueue_AQueue [code]:
1.278 + "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
1.279 + unfolding AQueue_def by simp
1.280 +
1.281 +lemma %quote dequeue_AQueue [code]:
1.282 + "dequeue (AQueue xs []) =
1.283 + (if xs = [] then (None, AQueue [] [])
1.284 + else dequeue (AQueue [] (rev xs)))"
1.285 + "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
1.286 + unfolding AQueue_def by simp_all
1.287 +
1.288 +text {*
1.289 + \noindent For completeness, we provide a substitute for the
1.290 + @{text case} combinator on queues:
1.291 +*}
1.292 +
1.293 +lemma %quote queue_case_AQueue [code]:
1.294 + "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
1.295 + unfolding AQueue_def by simp
1.296 +
1.297 +text {*
1.298 + \noindent The resulting code looks as expected:
1.299 +*}
1.300 +
1.301 +text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
1.302 +
1.303 +text {*
1.304 + \noindent From this example, it can be glimpsed that using own
1.305 + constructor sets is a little delicate since it changes the set of
1.306 + valid patterns for values of that type. Without going into much
1.307 + detail, here some practical hints:
1.308 +
1.309 + \begin{itemize}
1.310 +
1.311 + \item When changing the constructor set for datatypes, take care
1.312 + to provide alternative equations for the @{text case} combinator.
1.313 +
1.314 + \item Values in the target language need not to be normalised --
1.315 + different values in the target language may represent the same
1.316 + value in the logic.
1.317 +
1.318 + \item Usually, a good methodology to deal with the subtleties of
1.319 + pattern matching is to see the type as an abstract type: provide
1.320 + a set of operations which operate on the concrete representation
1.321 + of the type, and derive further operations by combinations of
1.322 + these primitive ones, without relying on a particular
1.323 + representation.
1.324 +
1.325 + \end{itemize}
1.326 +*}
1.327 +
1.328 +
1.329 +subsection {* Equality *}
1.330 +
1.331 +text {*
1.332 + Surely you have already noticed how equality is treated
1.333 + by the code generator:
1.334 +*}
1.335 +
1.336 +primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
1.337 + "collect_duplicates xs ys [] = xs"
1.338 + | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
1.339 + then if z \<in> set ys
1.340 + then collect_duplicates xs ys zs
1.341 + else collect_duplicates xs (z#ys) zs
1.342 + else collect_duplicates (z#xs) (z#ys) zs)"
1.343 +
1.344 +text {*
1.345 + \noindent During preprocessing, the membership test is rewritten,
1.346 + resulting in @{const List.member}, which itself
1.347 + performs an explicit equality check.
1.348 +*}
1.349 +
1.350 +text %quote {*@{code_stmts collect_duplicates (SML)}*}
1.351 +
1.352 +text {*
1.353 + \noindent Obviously, polymorphic equality is implemented the Haskell
1.354 + way using a type class. How is this achieved? HOL introduces
1.355 + an explicit class @{class eq} with a corresponding operation
1.356 + @{const eq_class.eq} such that @{thm eq [no_vars]}.
1.357 + The preprocessing framework does the rest by propagating the
1.358 + @{class eq} constraints through all dependent code equations.
1.359 + For datatypes, instances of @{class eq} are implicitly derived
1.360 + when possible. For other types, you may instantiate @{text eq}
1.361 + manually like any other type class.
1.362 +*}
1.363 +
1.364 +
1.365 +subsection {* Explicit partiality *}
1.366 +
1.367 +text {*
1.368 + Partiality usually enters the game by partial patterns, as
1.369 + in the following example, again for amortised queues:
1.370 +*}
1.371 +
1.372 +definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
1.373 + "strict_dequeue q = (case dequeue q
1.374 + of (Some x, q') \<Rightarrow> (x, q'))"
1.375 +
1.376 +lemma %quote strict_dequeue_AQueue [code]:
1.377 + "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
1.378 + "strict_dequeue (AQueue xs []) =
1.379 + (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
1.380 + by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits)
1.381 +
1.382 +text {*
1.383 + \noindent In the corresponding code, there is no equation
1.384 + for the pattern @{term "AQueue [] []"}:
1.385 +*}
1.386 +
1.387 +text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
1.388 +
1.389 +text {*
1.390 + \noindent In some cases it is desirable to have this
1.391 + pseudo-\qt{partiality} more explicitly, e.g.~as follows:
1.392 +*}
1.393 +
1.394 +axiomatization %quote empty_queue :: 'a
1.395 +
1.396 +definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
1.397 + "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"
1.398 +
1.399 +lemma %quote strict_dequeue'_AQueue [code]:
1.400 + "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue
1.401 + else strict_dequeue' (AQueue [] (rev xs)))"
1.402 + "strict_dequeue' (AQueue xs (y # ys)) =
1.403 + (y, AQueue xs ys)"
1.404 + by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits)
1.405 +
1.406 +text {*
1.407 + Observe that on the right hand side of the definition of @{const
1.408 + "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
1.409 +
1.410 + Normally, if constants without any code equations occur in a
1.411 + program, the code generator complains (since in most cases this is
1.412 + indeed an error). But such constants can also be thought
1.413 + of as function definitions which always fail,
1.414 + since there is never a successful pattern match on the left hand
1.415 + side. In order to categorise a constant into that category
1.416 + explicitly, use @{command "code_abort"}:
1.417 +*}
1.418 +
1.419 +code_abort %quote empty_queue
1.420 +
1.421 +text {*
1.422 + \noindent Then the code generator will just insert an error or
1.423 + exception at the appropriate position:
1.424 +*}
1.425 +
1.426 +text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
1.427 +
1.428 +text {*
1.429 + \noindent This feature however is rarely needed in practice.
1.430 + Note also that the @{text HOL} default setup already declares
1.431 + @{const undefined} as @{command "code_abort"}, which is most
1.432 + likely to be used in such situations.
1.433 +*}
1.434 +
1.435 +end
2.1 --- a/doc-src/Codegen/Thy/Further.thy Fri Aug 13 12:15:25 2010 +0200
2.2 +++ b/doc-src/Codegen/Thy/Further.thy Fri Aug 13 14:41:27 2010 +0200
2.3 @@ -191,4 +191,140 @@
2.4 the framework described there is available in theory @{theory Imperative_HOL}.
2.5 *}
2.6
2.7 +
2.8 +subsection {* ML system interfaces \label{sec:ml} *}
2.9 +
2.10 +text {*
2.11 + Since the code generator framework not only aims to provide
2.12 + a nice Isar interface but also to form a base for
2.13 + code-generation-based applications, here a short
2.14 + description of the most important ML interfaces.
2.15 +*}
2.16 +
2.17 +subsubsection {* Managing executable content *}
2.18 +
2.19 +text %mlref {*
2.20 + \begin{mldecls}
2.21 + @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
2.22 + @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
2.23 + @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
2.24 + @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\
2.25 + @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
2.26 + -> theory -> theory"} \\
2.27 + @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
2.28 + @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
2.29 + @{index_ML Code.get_type: "theory -> string
2.30 + -> (string * sort) list * ((string * string list) * typ list) list"} \\
2.31 + @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
2.32 + \end{mldecls}
2.33 +
2.34 + \begin{description}
2.35 +
2.36 + \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function
2.37 + theorem @{text "thm"} to executable content.
2.38 +
2.39 + \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function
2.40 + theorem @{text "thm"} from executable content, if present.
2.41 +
2.42 + \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
2.43 + the preprocessor simpset.
2.44 +
2.45 + \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
2.46 + function transformer @{text f} (named @{text name}) to executable content;
2.47 + @{text f} is a transformer of the code equations belonging
2.48 + to a certain function definition, depending on the
2.49 + current theory context. Returning @{text NONE} indicates that no
2.50 + transformation took place; otherwise, the whole process will be iterated
2.51 + with the new code equations.
2.52 +
2.53 + \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
2.54 + function transformer named @{text name} from executable content.
2.55 +
2.56 + \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
2.57 + a datatype to executable content, with generation
2.58 + set @{text cs}.
2.59 +
2.60 + \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
2.61 + returns type constructor corresponding to
2.62 + constructor @{text const}; returns @{text NONE}
2.63 + if @{text const} is no constructor.
2.64 +
2.65 + \end{description}
2.66 +*}
2.67 +
2.68 +subsubsection {* Auxiliary *}
2.69 +
2.70 +text %mlref {*
2.71 + \begin{mldecls}
2.72 + @{index_ML Code.read_const: "theory -> string -> string"}
2.73 + \end{mldecls}
2.74 +
2.75 + \begin{description}
2.76 +
2.77 + \item @{ML Code.read_const}~@{text thy}~@{text s}
2.78 + reads a constant as a concrete term expression @{text s}.
2.79 +
2.80 + \end{description}
2.81 +
2.82 +*}
2.83 +
2.84 +subsubsection {* Data depending on the theory's executable content *}
2.85 +
2.86 +text {*
2.87 + Implementing code generator applications on top
2.88 + of the framework set out so far usually not only
2.89 + involves using those primitive interfaces
2.90 + but also storing code-dependent data and various
2.91 + other things.
2.92 +
2.93 + Due to incrementality of code generation, changes in the
2.94 + theory's executable content have to be propagated in a
2.95 + certain fashion. Additionally, such changes may occur
2.96 + not only during theory extension but also during theory
2.97 + merge, which is a little bit nasty from an implementation
2.98 + point of view. The framework provides a solution
2.99 + to this technical challenge by providing a functorial
2.100 + data slot @{ML_functor Code_Data}; on instantiation
2.101 + of this functor, the following types and operations
2.102 + are required:
2.103 +
2.104 + \medskip
2.105 + \begin{tabular}{l}
2.106 + @{text "type T"} \\
2.107 + @{text "val empty: T"} \\
2.108 + \end{tabular}
2.109 +
2.110 + \begin{description}
2.111 +
2.112 + \item @{text T} the type of data to store.
2.113 +
2.114 + \item @{text empty} initial (empty) data.
2.115 +
2.116 + \end{description}
2.117 +
2.118 + \noindent An instance of @{ML_functor Code_Data} provides the following
2.119 + interface:
2.120 +
2.121 + \medskip
2.122 + \begin{tabular}{l}
2.123 + @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
2.124 + @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
2.125 + \end{tabular}
2.126 +
2.127 + \begin{description}
2.128 +
2.129 + \item @{text change} update of current data (cached!)
2.130 + by giving a continuation.
2.131 +
2.132 + \item @{text change_yield} update with side result.
2.133 +
2.134 + \end{description}
2.135 +*}
2.136 +
2.137 +text {*
2.138 + \bigskip
2.139 +
2.140 + \emph{Happy proving, happy hacking!}
2.141 +*}
2.142 +
2.143 end
3.1 --- a/doc-src/Codegen/Thy/Inductive_Predicate.thy Fri Aug 13 12:15:25 2010 +0200
3.2 +++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Fri Aug 13 14:41:27 2010 +0200
3.3 @@ -2,7 +2,7 @@
3.4 imports Setup
3.5 begin
3.6
3.7 -subsection {* Inductive Predicates *}
3.8 +section {* Inductive Predicates *}
3.9 (*<*)
3.10 hide_const append
3.11
4.1 --- a/doc-src/Codegen/Thy/Introduction.thy Fri Aug 13 12:15:25 2010 +0200
4.2 +++ b/doc-src/Codegen/Thy/Introduction.thy Fri Aug 13 14:41:27 2010 +0200
4.3 @@ -2,7 +2,17 @@
4.4 imports Setup
4.5 begin
4.6
4.7 -section {* Introduction and Overview *}
4.8 +section {* Introduction *}
4.9 +
4.10 +subsection {* Code generation fundamental: shallow embedding *}
4.11 +
4.12 +subsection {* A quick start with the @{text "Isabelle/HOL"} toolbox *}
4.13 +
4.14 +subsection {* Type classes *}
4.15 +
4.16 +subsection {* How to continue from here *}
4.17 +
4.18 +subsection {* If something goes utterly wrong *}
4.19
4.20 text {*
4.21 This tutorial introduces a generic code generator for the
4.22 @@ -111,6 +121,29 @@
4.23 for more details see \secref{sec:further}.
4.24 *}
4.25
4.26 +subsection {* If something utterly fails *}
4.27 +
4.28 +text {*
4.29 + Under certain circumstances, the code generator fails to produce
4.30 + code entirely.
4.31 +
4.32 + \begin{description}
4.33 +
4.34 + \ditem{generate only one module}
4.35 +
4.36 + \ditem{check with a different target language}
4.37 +
4.38 + \ditem{inspect code equations}
4.39 +
4.40 + \ditem{inspect preprocessor setup}
4.41 +
4.42 + \ditem{generate exceptions}
4.43 +
4.44 + \ditem{remove offending code equations}
4.45 +
4.46 + \end{description}
4.47 +*}
4.48 +
4.49 subsection {* Code generator architecture \label{sec:concept} *}
4.50
4.51 text {*
5.1 --- a/doc-src/Codegen/Thy/ML.thy Fri Aug 13 12:15:25 2010 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,162 +0,0 @@
5.4 -theory "ML"
5.5 -imports Setup
5.6 -begin
5.7 -
5.8 -section {* ML system interfaces \label{sec:ml} *}
5.9 -
5.10 -text {*
5.11 - Since the code generator framework not only aims to provide
5.12 - a nice Isar interface but also to form a base for
5.13 - code-generation-based applications, here a short
5.14 - description of the most important ML interfaces.
5.15 -*}
5.16 -
5.17 -subsection {* Executable theory content: @{text Code} *}
5.18 -
5.19 -text {*
5.20 - This Pure module implements the core notions of
5.21 - executable content of a theory.
5.22 -*}
5.23 -
5.24 -subsubsection {* Managing executable content *}
5.25 -
5.26 -text %mlref {*
5.27 - \begin{mldecls}
5.28 - @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
5.29 - @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
5.30 - @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
5.31 - @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\
5.32 - @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
5.33 - -> theory -> theory"} \\
5.34 - @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
5.35 - @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
5.36 - @{index_ML Code.get_type: "theory -> string
5.37 - -> (string * sort) list * ((string * string list) * typ list) list"} \\
5.38 - @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
5.39 - \end{mldecls}
5.40 -
5.41 - \begin{description}
5.42 -
5.43 - \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function
5.44 - theorem @{text "thm"} to executable content.
5.45 -
5.46 - \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function
5.47 - theorem @{text "thm"} from executable content, if present.
5.48 -
5.49 - \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
5.50 - the preprocessor simpset.
5.51 -
5.52 - \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
5.53 - function transformer @{text f} (named @{text name}) to executable content;
5.54 - @{text f} is a transformer of the code equations belonging
5.55 - to a certain function definition, depending on the
5.56 - current theory context. Returning @{text NONE} indicates that no
5.57 - transformation took place; otherwise, the whole process will be iterated
5.58 - with the new code equations.
5.59 -
5.60 - \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
5.61 - function transformer named @{text name} from executable content.
5.62 -
5.63 - \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
5.64 - a datatype to executable content, with generation
5.65 - set @{text cs}.
5.66 -
5.67 - \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
5.68 - returns type constructor corresponding to
5.69 - constructor @{text const}; returns @{text NONE}
5.70 - if @{text const} is no constructor.
5.71 -
5.72 - \end{description}
5.73 -*}
5.74 -
5.75 -subsection {* Auxiliary *}
5.76 -
5.77 -text %mlref {*
5.78 - \begin{mldecls}
5.79 - @{index_ML Code.read_const: "theory -> string -> string"}
5.80 - \end{mldecls}
5.81 -
5.82 - \begin{description}
5.83 -
5.84 - \item @{ML Code.read_const}~@{text thy}~@{text s}
5.85 - reads a constant as a concrete term expression @{text s}.
5.86 -
5.87 - \end{description}
5.88 -
5.89 -*}
5.90 -
5.91 -subsection {* Implementing code generator applications *}
5.92 -
5.93 -text {*
5.94 - Implementing code generator applications on top
5.95 - of the framework set out so far usually not only
5.96 - involves using those primitive interfaces
5.97 - but also storing code-dependent data and various
5.98 - other things.
5.99 -*}
5.100 -
5.101 -subsubsection {* Data depending on the theory's executable content *}
5.102 -
5.103 -text {*
5.104 - Due to incrementality of code generation, changes in the
5.105 - theory's executable content have to be propagated in a
5.106 - certain fashion. Additionally, such changes may occur
5.107 - not only during theory extension but also during theory
5.108 - merge, which is a little bit nasty from an implementation
5.109 - point of view. The framework provides a solution
5.110 - to this technical challenge by providing a functorial
5.111 - data slot @{ML_functor Code_Data}; on instantiation
5.112 - of this functor, the following types and operations
5.113 - are required:
5.114 -
5.115 - \medskip
5.116 - \begin{tabular}{l}
5.117 - @{text "type T"} \\
5.118 - @{text "val empty: T"} \\
5.119 - @{text "val purge: theory \<rightarrow> string list option \<rightarrow> T \<rightarrow> T"}
5.120 - \end{tabular}
5.121 -
5.122 - \begin{description}
5.123 -
5.124 - \item @{text T} the type of data to store.
5.125 -
5.126 - \item @{text empty} initial (empty) data.
5.127 -
5.128 - \item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content;
5.129 - @{text consts} indicates the kind
5.130 - of change: @{ML NONE} stands for a fundamental change
5.131 - which invalidates any existing code, @{text "SOME consts"}
5.132 - hints that executable content for constants @{text consts}
5.133 - has changed.
5.134 -
5.135 - \end{description}
5.136 -
5.137 - \noindent An instance of @{ML_functor Code_Data} provides the following
5.138 - interface:
5.139 -
5.140 - \medskip
5.141 - \begin{tabular}{l}
5.142 - @{text "get: theory \<rightarrow> T"} \\
5.143 - @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
5.144 - @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
5.145 - \end{tabular}
5.146 -
5.147 - \begin{description}
5.148 -
5.149 - \item @{text get} retrieval of the current data.
5.150 -
5.151 - \item @{text change} update of current data (cached!)
5.152 - by giving a continuation.
5.153 -
5.154 - \item @{text change_yield} update with side result.
5.155 -
5.156 - \end{description}
5.157 -*}
5.158 -
5.159 -text {*
5.160 - \bigskip
5.161 -
5.162 - \emph{Happy proving, happy hacking!}
5.163 -*}
5.164 -
5.165 -end
6.1 --- a/doc-src/Codegen/Thy/Program.thy Fri Aug 13 12:15:25 2010 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,432 +0,0 @@
6.4 -theory Program
6.5 -imports Introduction
6.6 -begin
6.7 -
6.8 -section {* Turning Theories into Programs \label{sec:program} *}
6.9 -
6.10 -subsection {* The @{text "Isabelle/HOL"} default setup *}
6.11 -
6.12 -text {*
6.13 - We have already seen how by default equations stemming from
6.14 - @{command definition}, @{command primrec} and @{command fun}
6.15 - statements are used for code generation. This default behaviour
6.16 - can be changed, e.g.\ by providing different code equations.
6.17 - The customisations shown in this section are \emph{safe}
6.18 - as regards correctness: all programs that can be generated are partially
6.19 - correct.
6.20 -*}
6.21 -
6.22 -subsection {* Selecting code equations *}
6.23 -
6.24 -text {*
6.25 - Coming back to our introductory example, we
6.26 - could provide an alternative code equations for @{const dequeue}
6.27 - explicitly:
6.28 -*}
6.29 -
6.30 -lemma %quote [code]:
6.31 - "dequeue (AQueue xs []) =
6.32 - (if xs = [] then (None, AQueue [] [])
6.33 - else dequeue (AQueue [] (rev xs)))"
6.34 - "dequeue (AQueue xs (y # ys)) =
6.35 - (Some y, AQueue xs ys)"
6.36 - by (cases xs, simp_all) (cases "rev xs", simp_all)
6.37 -
6.38 -text {*
6.39 - \noindent The annotation @{text "[code]"} is an @{text Isar}
6.40 - @{text attribute} which states that the given theorems should be
6.41 - considered as code equations for a @{text fun} statement --
6.42 - the corresponding constant is determined syntactically. The resulting code:
6.43 -*}
6.44 -
6.45 -text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
6.46 -
6.47 -text {*
6.48 - \noindent You may note that the equality test @{term "xs = []"} has been
6.49 - replaced by the predicate @{term "null xs"}. This is due to the default
6.50 - setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
6.51 -
6.52 - Changing the default constructor set of datatypes is also
6.53 - possible. See \secref{sec:datatypes} for an example.
6.54 -
6.55 - As told in \secref{sec:concept}, code generation is based
6.56 - on a structured collection of code theorems.
6.57 - This collection
6.58 - may be inspected using the @{command code_thms} command:
6.59 -*}
6.60 -
6.61 -code_thms %quote dequeue
6.62 -
6.63 -text {*
6.64 - \noindent prints a table with \emph{all} code equations
6.65 - for @{const dequeue}, including
6.66 - \emph{all} code equations those equations depend
6.67 - on recursively.
6.68 -
6.69 - Similarly, the @{command code_deps} command shows a graph
6.70 - visualising dependencies between code equations.
6.71 -*}
6.72 -
6.73 -subsection {* @{text class} and @{text instantiation} *}
6.74 -
6.75 -text {*
6.76 - Concerning type classes and code generation, let us examine an example
6.77 - from abstract algebra:
6.78 -*}
6.79 -
6.80 -class %quote semigroup =
6.81 - fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
6.82 - assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
6.83 -
6.84 -class %quote monoid = semigroup +
6.85 - fixes neutral :: 'a ("\<one>")
6.86 - assumes neutl: "\<one> \<otimes> x = x"
6.87 - and neutr: "x \<otimes> \<one> = x"
6.88 -
6.89 -instantiation %quote nat :: monoid
6.90 -begin
6.91 -
6.92 -primrec %quote mult_nat where
6.93 - "0 \<otimes> n = (0\<Colon>nat)"
6.94 - | "Suc m \<otimes> n = n + m \<otimes> n"
6.95 -
6.96 -definition %quote neutral_nat where
6.97 - "\<one> = Suc 0"
6.98 -
6.99 -lemma %quote add_mult_distrib:
6.100 - fixes n m q :: nat
6.101 - shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
6.102 - by (induct n) simp_all
6.103 -
6.104 -instance %quote proof
6.105 - fix m n q :: nat
6.106 - show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
6.107 - by (induct m) (simp_all add: add_mult_distrib)
6.108 - show "\<one> \<otimes> n = n"
6.109 - by (simp add: neutral_nat_def)
6.110 - show "m \<otimes> \<one> = m"
6.111 - by (induct m) (simp_all add: neutral_nat_def)
6.112 -qed
6.113 -
6.114 -end %quote
6.115 -
6.116 -text {*
6.117 - \noindent We define the natural operation of the natural numbers
6.118 - on monoids:
6.119 -*}
6.120 -
6.121 -primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
6.122 - "pow 0 a = \<one>"
6.123 - | "pow (Suc n) a = a \<otimes> pow n a"
6.124 -
6.125 -text {*
6.126 - \noindent This we use to define the discrete exponentiation function:
6.127 -*}
6.128 -
6.129 -definition %quote bexp :: "nat \<Rightarrow> nat" where
6.130 - "bexp n = pow n (Suc (Suc 0))"
6.131 -
6.132 -text {*
6.133 - \noindent The corresponding code in Haskell uses that language's native classes:
6.134 -*}
6.135 -
6.136 -text %quote {*@{code_stmts bexp (Haskell)}*}
6.137 -
6.138 -text {*
6.139 - \noindent This is a convenient place to show how explicit dictionary construction
6.140 - manifests in generated code (here, the same example in @{text SML})
6.141 - \cite{Haftmann-Nipkow:2010:code}:
6.142 -*}
6.143 -
6.144 -text %quote {*@{code_stmts bexp (SML)}*}
6.145 -
6.146 -text {*
6.147 - \noindent Note the parameters with trailing underscore (@{verbatim "A_"}),
6.148 - which are the dictionary parameters.
6.149 -*}
6.150 -
6.151 -subsection {* The preprocessor \label{sec:preproc} *}
6.152 -
6.153 -text {*
6.154 - Before selected function theorems are turned into abstract
6.155 - code, a chain of definitional transformation steps is carried
6.156 - out: \emph{preprocessing}. In essence, the preprocessor
6.157 - consists of two components: a \emph{simpset} and \emph{function transformers}.
6.158 -
6.159 - The \emph{simpset} can apply the full generality of the
6.160 - Isabelle simplifier. Due to the interpretation of theorems as code
6.161 - equations, rewrites are applied to the right hand side and the
6.162 - arguments of the left hand side of an equation, but never to the
6.163 - constant heading the left hand side. An important special case are
6.164 - \emph{unfold theorems}, which may be declared and removed using
6.165 - the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
6.166 - attribute, respectively.
6.167 -
6.168 - Some common applications:
6.169 -*}
6.170 -
6.171 -text_raw {*
6.172 - \begin{itemize}
6.173 -*}
6.174 -
6.175 -text {*
6.176 - \item replacing non-executable constructs by executable ones:
6.177 -*}
6.178 -
6.179 -lemma %quote [code_unfold]:
6.180 - "x \<in> set xs \<longleftrightarrow> List.member xs x" by (fact in_set_member)
6.181 -
6.182 -text {*
6.183 - \item eliminating superfluous constants:
6.184 -*}
6.185 -
6.186 -lemma %quote [code_unfold]:
6.187 - "1 = Suc 0" by (fact One_nat_def)
6.188 -
6.189 -text {*
6.190 - \item replacing executable but inconvenient constructs:
6.191 -*}
6.192 -
6.193 -lemma %quote [code_unfold]:
6.194 - "xs = [] \<longleftrightarrow> List.null xs" by (fact eq_Nil_null)
6.195 -
6.196 -text_raw {*
6.197 - \end{itemize}
6.198 -*}
6.199 -
6.200 -text {*
6.201 - \noindent \emph{Function transformers} provide a very general interface,
6.202 - transforming a list of function theorems to another
6.203 - list of function theorems, provided that neither the heading
6.204 - constant nor its type change. The @{term "0\<Colon>nat"} / @{const Suc}
6.205 - pattern elimination implemented in
6.206 - theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this
6.207 - interface.
6.208 -
6.209 - \noindent The current setup of the preprocessor may be inspected using
6.210 - the @{command print_codeproc} command.
6.211 - @{command code_thms} provides a convenient
6.212 - mechanism to inspect the impact of a preprocessor setup
6.213 - on code equations.
6.214 -
6.215 - \begin{warn}
6.216 -
6.217 - Attribute @{attribute code_unfold} also applies to the
6.218 - preprocessor of the ancient @{text "SML code generator"}; in case
6.219 - this is not what you intend, use @{attribute code_inline} instead.
6.220 - \end{warn}
6.221 -*}
6.222 -
6.223 -subsection {* Datatypes \label{sec:datatypes} *}
6.224 -
6.225 -text {*
6.226 - Conceptually, any datatype is spanned by a set of
6.227 - \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
6.228 - "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
6.229 - @{text "\<tau>"}. The HOL datatype package by default registers any new
6.230 - datatype in the table of datatypes, which may be inspected using the
6.231 - @{command print_codesetup} command.
6.232 -
6.233 - In some cases, it is appropriate to alter or extend this table. As
6.234 - an example, we will develop an alternative representation of the
6.235 - queue example given in \secref{sec:intro}. The amortised
6.236 - representation is convenient for generating code but exposes its
6.237 - \qt{implementation} details, which may be cumbersome when proving
6.238 - theorems about it. Therefore, here is a simple, straightforward
6.239 - representation of queues:
6.240 -*}
6.241 -
6.242 -datatype %quote 'a queue = Queue "'a list"
6.243 -
6.244 -definition %quote empty :: "'a queue" where
6.245 - "empty = Queue []"
6.246 -
6.247 -primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
6.248 - "enqueue x (Queue xs) = Queue (xs @ [x])"
6.249 -
6.250 -fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
6.251 - "dequeue (Queue []) = (None, Queue [])"
6.252 - | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
6.253 -
6.254 -text {*
6.255 - \noindent This we can use directly for proving; for executing,
6.256 - we provide an alternative characterisation:
6.257 -*}
6.258 -
6.259 -definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
6.260 - "AQueue xs ys = Queue (ys @ rev xs)"
6.261 -
6.262 -code_datatype %quote AQueue
6.263 -
6.264 -text {*
6.265 - \noindent Here we define a \qt{constructor} @{const "AQueue"} which
6.266 - is defined in terms of @{text "Queue"} and interprets its arguments
6.267 - according to what the \emph{content} of an amortised queue is supposed
6.268 - to be. Equipped with this, we are able to prove the following equations
6.269 - for our primitive queue operations which \qt{implement} the simple
6.270 - queues in an amortised fashion:
6.271 -*}
6.272 -
6.273 -lemma %quote empty_AQueue [code]:
6.274 - "empty = AQueue [] []"
6.275 - unfolding AQueue_def empty_def by simp
6.276 -
6.277 -lemma %quote enqueue_AQueue [code]:
6.278 - "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
6.279 - unfolding AQueue_def by simp
6.280 -
6.281 -lemma %quote dequeue_AQueue [code]:
6.282 - "dequeue (AQueue xs []) =
6.283 - (if xs = [] then (None, AQueue [] [])
6.284 - else dequeue (AQueue [] (rev xs)))"
6.285 - "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
6.286 - unfolding AQueue_def by simp_all
6.287 -
6.288 -text {*
6.289 - \noindent For completeness, we provide a substitute for the
6.290 - @{text case} combinator on queues:
6.291 -*}
6.292 -
6.293 -lemma %quote queue_case_AQueue [code]:
6.294 - "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
6.295 - unfolding AQueue_def by simp
6.296 -
6.297 -text {*
6.298 - \noindent The resulting code looks as expected:
6.299 -*}
6.300 -
6.301 -text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
6.302 -
6.303 -text {*
6.304 - \noindent From this example, it can be glimpsed that using own
6.305 - constructor sets is a little delicate since it changes the set of
6.306 - valid patterns for values of that type. Without going into much
6.307 - detail, here some practical hints:
6.308 -
6.309 - \begin{itemize}
6.310 -
6.311 - \item When changing the constructor set for datatypes, take care
6.312 - to provide alternative equations for the @{text case} combinator.
6.313 -
6.314 - \item Values in the target language need not to be normalised --
6.315 - different values in the target language may represent the same
6.316 - value in the logic.
6.317 -
6.318 - \item Usually, a good methodology to deal with the subtleties of
6.319 - pattern matching is to see the type as an abstract type: provide
6.320 - a set of operations which operate on the concrete representation
6.321 - of the type, and derive further operations by combinations of
6.322 - these primitive ones, without relying on a particular
6.323 - representation.
6.324 -
6.325 - \end{itemize}
6.326 -*}
6.327 -
6.328 -
6.329 -subsection {* Equality *}
6.330 -
6.331 -text {*
6.332 - Surely you have already noticed how equality is treated
6.333 - by the code generator:
6.334 -*}
6.335 -
6.336 -primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
6.337 - "collect_duplicates xs ys [] = xs"
6.338 - | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
6.339 - then if z \<in> set ys
6.340 - then collect_duplicates xs ys zs
6.341 - else collect_duplicates xs (z#ys) zs
6.342 - else collect_duplicates (z#xs) (z#ys) zs)"
6.343 -
6.344 -text {*
6.345 - \noindent During preprocessing, the membership test is rewritten,
6.346 - resulting in @{const List.member}, which itself
6.347 - performs an explicit equality check.
6.348 -*}
6.349 -
6.350 -text %quote {*@{code_stmts collect_duplicates (SML)}*}
6.351 -
6.352 -text {*
6.353 - \noindent Obviously, polymorphic equality is implemented the Haskell
6.354 - way using a type class. How is this achieved? HOL introduces
6.355 - an explicit class @{class eq} with a corresponding operation
6.356 - @{const eq_class.eq} such that @{thm eq [no_vars]}.
6.357 - The preprocessing framework does the rest by propagating the
6.358 - @{class eq} constraints through all dependent code equations.
6.359 - For datatypes, instances of @{class eq} are implicitly derived
6.360 - when possible. For other types, you may instantiate @{text eq}
6.361 - manually like any other type class.
6.362 -*}
6.363 -
6.364 -
6.365 -subsection {* Explicit partiality *}
6.366 -
6.367 -text {*
6.368 - Partiality usually enters the game by partial patterns, as
6.369 - in the following example, again for amortised queues:
6.370 -*}
6.371 -
6.372 -definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
6.373 - "strict_dequeue q = (case dequeue q
6.374 - of (Some x, q') \<Rightarrow> (x, q'))"
6.375 -
6.376 -lemma %quote strict_dequeue_AQueue [code]:
6.377 - "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
6.378 - "strict_dequeue (AQueue xs []) =
6.379 - (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
6.380 - by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits)
6.381 -
6.382 -text {*
6.383 - \noindent In the corresponding code, there is no equation
6.384 - for the pattern @{term "AQueue [] []"}:
6.385 -*}
6.386 -
6.387 -text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
6.388 -
6.389 -text {*
6.390 - \noindent In some cases it is desirable to have this
6.391 - pseudo-\qt{partiality} more explicitly, e.g.~as follows:
6.392 -*}
6.393 -
6.394 -axiomatization %quote empty_queue :: 'a
6.395 -
6.396 -definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
6.397 - "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"
6.398 -
6.399 -lemma %quote strict_dequeue'_AQueue [code]:
6.400 - "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue
6.401 - else strict_dequeue' (AQueue [] (rev xs)))"
6.402 - "strict_dequeue' (AQueue xs (y # ys)) =
6.403 - (y, AQueue xs ys)"
6.404 - by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits)
6.405 -
6.406 -text {*
6.407 - Observe that on the right hand side of the definition of @{const
6.408 - "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
6.409 -
6.410 - Normally, if constants without any code equations occur in a
6.411 - program, the code generator complains (since in most cases this is
6.412 - indeed an error). But such constants can also be thought
6.413 - of as function definitions which always fail,
6.414 - since there is never a successful pattern match on the left hand
6.415 - side. In order to categorise a constant into that category
6.416 - explicitly, use @{command "code_abort"}:
6.417 -*}
6.418 -
6.419 -code_abort %quote empty_queue
6.420 -
6.421 -text {*
6.422 - \noindent Then the code generator will just insert an error or
6.423 - exception at the appropriate position:
6.424 -*}
6.425 -
6.426 -text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
6.427 -
6.428 -text {*
6.429 - \noindent This feature however is rarely needed in practice.
6.430 - Note also that the @{text HOL} default setup already declares
6.431 - @{const undefined} as @{command "code_abort"}, which is most
6.432 - likely to be used in such situations.
6.433 -*}
6.434 -
6.435 -end
7.1 --- a/doc-src/Codegen/Thy/ROOT.ML Fri Aug 13 12:15:25 2010 +0200
7.2 +++ b/doc-src/Codegen/Thy/ROOT.ML Fri Aug 13 14:41:27 2010 +0200
7.3 @@ -1,10 +1,9 @@
7.4
7.5 no_document use_thy "Setup";
7.6 -no_document use_thys ["Efficient_Nat"];
7.7
7.8 use_thy "Introduction";
7.9 -use_thy "Program";
7.10 +use_thy "Foundations";
7.11 +use_thy "Refinement";
7.12 use_thy "Inductive_Predicate";
7.13 use_thy "Adaptation";
7.14 use_thy "Further";
7.15 -use_thy "ML";
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/doc-src/Codegen/Thy/Refinement.thy Fri Aug 13 14:41:27 2010 +0200
8.3 @@ -0,0 +1,7 @@
8.4 +theory Refinement
8.5 +imports Setup
8.6 +begin
8.7 +
8.8 +section {* Program and datatype refinement \label{sec:refinement} *}
8.9 +
8.10 +end
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/doc-src/Codegen/Thy/document/Foundations.tex Fri Aug 13 14:41:27 2010 +0200
9.3 @@ -0,0 +1,1013 @@
9.4 +%
9.5 +\begin{isabellebody}%
9.6 +\def\isabellecontext{Foundations}%
9.7 +%
9.8 +\isadelimtheory
9.9 +%
9.10 +\endisadelimtheory
9.11 +%
9.12 +\isatagtheory
9.13 +\isacommand{theory}\isamarkupfalse%
9.14 +\ Foundations\isanewline
9.15 +\isakeyword{imports}\ Introduction\isanewline
9.16 +\isakeyword{begin}%
9.17 +\endisatagtheory
9.18 +{\isafoldtheory}%
9.19 +%
9.20 +\isadelimtheory
9.21 +%
9.22 +\endisadelimtheory
9.23 +%
9.24 +\isamarkupsection{Code generation foundations \label{sec:program}%
9.25 +}
9.26 +\isamarkuptrue%
9.27 +%
9.28 +\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup%
9.29 +}
9.30 +\isamarkuptrue%
9.31 +%
9.32 +\begin{isamarkuptext}%
9.33 +We have already seen how by default equations stemming from
9.34 + \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}, \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
9.35 + statements are used for code generation. This default behaviour
9.36 + can be changed, e.g.\ by providing different code equations.
9.37 + The customisations shown in this section are \emph{safe}
9.38 + as regards correctness: all programs that can be generated are partially
9.39 + correct.%
9.40 +\end{isamarkuptext}%
9.41 +\isamarkuptrue%
9.42 +%
9.43 +\isamarkupsubsection{Selecting code equations%
9.44 +}
9.45 +\isamarkuptrue%
9.46 +%
9.47 +\begin{isamarkuptext}%
9.48 +Coming back to our introductory example, we
9.49 + could provide an alternative code equations for \isa{dequeue}
9.50 + explicitly:%
9.51 +\end{isamarkuptext}%
9.52 +\isamarkuptrue%
9.53 +%
9.54 +\isadelimquote
9.55 +%
9.56 +\endisadelimquote
9.57 +%
9.58 +\isatagquote
9.59 +\isacommand{lemma}\isamarkupfalse%
9.60 +\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
9.61 +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
9.62 +\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
9.63 +\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.64 +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
9.65 +\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.66 +\ \ \isacommand{by}\isamarkupfalse%
9.67 +\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
9.68 +\endisatagquote
9.69 +{\isafoldquote}%
9.70 +%
9.71 +\isadelimquote
9.72 +%
9.73 +\endisadelimquote
9.74 +%
9.75 +\begin{isamarkuptext}%
9.76 +\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
9.77 + \isa{attribute} which states that the given theorems should be
9.78 + considered as code equations for a \isa{fun} statement --
9.79 + the corresponding constant is determined syntactically. The resulting code:%
9.80 +\end{isamarkuptext}%
9.81 +\isamarkuptrue%
9.82 +%
9.83 +\isadelimquote
9.84 +%
9.85 +\endisadelimquote
9.86 +%
9.87 +\isatagquote
9.88 +%
9.89 +\begin{isamarkuptext}%
9.90 +\isatypewriter%
9.91 +\noindent%
9.92 +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
9.93 +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
9.94 +\hspace*{0pt}dequeue (AQueue xs []) =\\
9.95 +\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
9.96 +\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
9.97 +\end{isamarkuptext}%
9.98 +\isamarkuptrue%
9.99 +%
9.100 +\endisatagquote
9.101 +{\isafoldquote}%
9.102 +%
9.103 +\isadelimquote
9.104 +%
9.105 +\endisadelimquote
9.106 +%
9.107 +\begin{isamarkuptext}%
9.108 +\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been
9.109 + replaced by the predicate \isa{null\ xs}. This is due to the default
9.110 + setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
9.111 +
9.112 + Changing the default constructor set of datatypes is also
9.113 + possible. See \secref{sec:datatypes} for an example.
9.114 +
9.115 + As told in \secref{sec:concept}, code generation is based
9.116 + on a structured collection of code theorems.
9.117 + This collection
9.118 + may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
9.119 +\end{isamarkuptext}%
9.120 +\isamarkuptrue%
9.121 +%
9.122 +\isadelimquote
9.123 +%
9.124 +\endisadelimquote
9.125 +%
9.126 +\isatagquote
9.127 +\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
9.128 +\ dequeue%
9.129 +\endisatagquote
9.130 +{\isafoldquote}%
9.131 +%
9.132 +\isadelimquote
9.133 +%
9.134 +\endisadelimquote
9.135 +%
9.136 +\begin{isamarkuptext}%
9.137 +\noindent prints a table with \emph{all} code equations
9.138 + for \isa{dequeue}, including
9.139 + \emph{all} code equations those equations depend
9.140 + on recursively.
9.141 +
9.142 + Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph
9.143 + visualising dependencies between code equations.%
9.144 +\end{isamarkuptext}%
9.145 +\isamarkuptrue%
9.146 +%
9.147 +\isamarkupsubsection{\isa{class} and \isa{instantiation}%
9.148 +}
9.149 +\isamarkuptrue%
9.150 +%
9.151 +\begin{isamarkuptext}%
9.152 +Concerning type classes and code generation, let us examine an example
9.153 + from abstract algebra:%
9.154 +\end{isamarkuptext}%
9.155 +\isamarkuptrue%
9.156 +%
9.157 +\isadelimquote
9.158 +%
9.159 +\endisadelimquote
9.160 +%
9.161 +\isatagquote
9.162 +\isacommand{class}\isamarkupfalse%
9.163 +\ semigroup\ {\isacharequal}\isanewline
9.164 +\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
9.165 +\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.166 +\isanewline
9.167 +\isacommand{class}\isamarkupfalse%
9.168 +\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
9.169 +\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
9.170 +\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
9.171 +\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
9.172 +\isanewline
9.173 +\isacommand{instantiation}\isamarkupfalse%
9.174 +\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
9.175 +\isakeyword{begin}\isanewline
9.176 +\isanewline
9.177 +\isacommand{primrec}\isamarkupfalse%
9.178 +\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
9.179 +\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.180 +\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline
9.181 +\isanewline
9.182 +\isacommand{definition}\isamarkupfalse%
9.183 +\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
9.184 +\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
9.185 +\isanewline
9.186 +\isacommand{lemma}\isamarkupfalse%
9.187 +\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline
9.188 +\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
9.189 +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline
9.190 +\ \ \isacommand{by}\isamarkupfalse%
9.191 +\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
9.192 +\isanewline
9.193 +\isacommand{instance}\isamarkupfalse%
9.194 +\ \isacommand{proof}\isamarkupfalse%
9.195 +\isanewline
9.196 +\ \ \isacommand{fix}\isamarkupfalse%
9.197 +\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
9.198 +\ \ \isacommand{show}\isamarkupfalse%
9.199 +\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.200 +\ \ \ \ \isacommand{by}\isamarkupfalse%
9.201 +\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline
9.202 +\ \ \isacommand{show}\isamarkupfalse%
9.203 +\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
9.204 +\ \ \ \ \isacommand{by}\isamarkupfalse%
9.205 +\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
9.206 +\ \ \isacommand{show}\isamarkupfalse%
9.207 +\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
9.208 +\ \ \ \ \isacommand{by}\isamarkupfalse%
9.209 +\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
9.210 +\isacommand{qed}\isamarkupfalse%
9.211 +\isanewline
9.212 +\isanewline
9.213 +\isacommand{end}\isamarkupfalse%
9.214 +%
9.215 +\endisatagquote
9.216 +{\isafoldquote}%
9.217 +%
9.218 +\isadelimquote
9.219 +%
9.220 +\endisadelimquote
9.221 +%
9.222 +\begin{isamarkuptext}%
9.223 +\noindent We define the natural operation of the natural numbers
9.224 + on monoids:%
9.225 +\end{isamarkuptext}%
9.226 +\isamarkuptrue%
9.227 +%
9.228 +\isadelimquote
9.229 +%
9.230 +\endisadelimquote
9.231 +%
9.232 +\isatagquote
9.233 +\isacommand{primrec}\isamarkupfalse%
9.234 +\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
9.235 +\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
9.236 +\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
9.237 +\endisatagquote
9.238 +{\isafoldquote}%
9.239 +%
9.240 +\isadelimquote
9.241 +%
9.242 +\endisadelimquote
9.243 +%
9.244 +\begin{isamarkuptext}%
9.245 +\noindent This we use to define the discrete exponentiation function:%
9.246 +\end{isamarkuptext}%
9.247 +\isamarkuptrue%
9.248 +%
9.249 +\isadelimquote
9.250 +%
9.251 +\endisadelimquote
9.252 +%
9.253 +\isatagquote
9.254 +\isacommand{definition}\isamarkupfalse%
9.255 +\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
9.256 +\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
9.257 +\endisatagquote
9.258 +{\isafoldquote}%
9.259 +%
9.260 +\isadelimquote
9.261 +%
9.262 +\endisadelimquote
9.263 +%
9.264 +\begin{isamarkuptext}%
9.265 +\noindent The corresponding code in Haskell uses that language's native classes:%
9.266 +\end{isamarkuptext}%
9.267 +\isamarkuptrue%
9.268 +%
9.269 +\isadelimquote
9.270 +%
9.271 +\endisadelimquote
9.272 +%
9.273 +\isatagquote
9.274 +%
9.275 +\begin{isamarkuptext}%
9.276 +\isatypewriter%
9.277 +\noindent%
9.278 +\hspace*{0pt}module Example where {\char123}\\
9.279 +\hspace*{0pt}\\
9.280 +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
9.281 +\hspace*{0pt}\\
9.282 +\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
9.283 +\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
9.284 +\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
9.285 +\hspace*{0pt}\\
9.286 +\hspace*{0pt}class Semigroup a where {\char123}\\
9.287 +\hspace*{0pt} ~mult ::~a -> a -> a;\\
9.288 +\hspace*{0pt}{\char125};\\
9.289 +\hspace*{0pt}\\
9.290 +\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
9.291 +\hspace*{0pt} ~neutral ::~a;\\
9.292 +\hspace*{0pt}{\char125};\\
9.293 +\hspace*{0pt}\\
9.294 +\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
9.295 +\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
9.296 +\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
9.297 +\hspace*{0pt}\\
9.298 +\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
9.299 +\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
9.300 +\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
9.301 +\hspace*{0pt}\\
9.302 +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
9.303 +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
9.304 +\hspace*{0pt}\\
9.305 +\hspace*{0pt}instance Semigroup Nat where {\char123}\\
9.306 +\hspace*{0pt} ~mult = mult{\char95}nat;\\
9.307 +\hspace*{0pt}{\char125};\\
9.308 +\hspace*{0pt}\\
9.309 +\hspace*{0pt}instance Monoid Nat where {\char123}\\
9.310 +\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
9.311 +\hspace*{0pt}{\char125};\\
9.312 +\hspace*{0pt}\\
9.313 +\hspace*{0pt}bexp ::~Nat -> Nat;\\
9.314 +\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
9.315 +\hspace*{0pt}\\
9.316 +\hspace*{0pt}{\char125}%
9.317 +\end{isamarkuptext}%
9.318 +\isamarkuptrue%
9.319 +%
9.320 +\endisatagquote
9.321 +{\isafoldquote}%
9.322 +%
9.323 +\isadelimquote
9.324 +%
9.325 +\endisadelimquote
9.326 +%
9.327 +\begin{isamarkuptext}%
9.328 +\noindent This is a convenient place to show how explicit dictionary construction
9.329 + manifests in generated code (here, the same example in \isa{SML})
9.330 + \cite{Haftmann-Nipkow:2010:code}:%
9.331 +\end{isamarkuptext}%
9.332 +\isamarkuptrue%
9.333 +%
9.334 +\isadelimquote
9.335 +%
9.336 +\endisadelimquote
9.337 +%
9.338 +\isatagquote
9.339 +%
9.340 +\begin{isamarkuptext}%
9.341 +\isatypewriter%
9.342 +\noindent%
9.343 +\hspace*{0pt}structure Example :~sig\\
9.344 +\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
9.345 +\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
9.346 +\hspace*{0pt} ~type 'a semigroup\\
9.347 +\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
9.348 +\hspace*{0pt} ~type 'a monoid\\
9.349 +\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
9.350 +\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
9.351 +\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
9.352 +\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
9.353 +\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
9.354 +\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\
9.355 +\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\
9.356 +\hspace*{0pt} ~val bexp :~nat -> nat\\
9.357 +\hspace*{0pt}end = struct\\
9.358 +\hspace*{0pt}\\
9.359 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
9.360 +\hspace*{0pt}\\
9.361 +\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
9.362 +\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
9.363 +\hspace*{0pt}\\
9.364 +\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
9.365 +\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
9.366 +\hspace*{0pt}\\
9.367 +\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
9.368 +\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
9.369 +\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
9.370 +\hspace*{0pt}\\
9.371 +\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
9.372 +\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
9.373 +\hspace*{0pt}\\
9.374 +\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
9.375 +\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
9.376 +\hspace*{0pt}\\
9.377 +\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
9.378 +\hspace*{0pt}\\
9.379 +\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
9.380 +\hspace*{0pt}\\
9.381 +\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
9.382 +\hspace*{0pt} ~:~nat monoid;\\
9.383 +\hspace*{0pt}\\
9.384 +\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
9.385 +\hspace*{0pt}\\
9.386 +\hspace*{0pt}end;~(*struct Example*)%
9.387 +\end{isamarkuptext}%
9.388 +\isamarkuptrue%
9.389 +%
9.390 +\endisatagquote
9.391 +{\isafoldquote}%
9.392 +%
9.393 +\isadelimquote
9.394 +%
9.395 +\endisadelimquote
9.396 +%
9.397 +\begin{isamarkuptext}%
9.398 +\noindent Note the parameters with trailing underscore (\verb|A_|),
9.399 + which are the dictionary parameters.%
9.400 +\end{isamarkuptext}%
9.401 +\isamarkuptrue%
9.402 +%
9.403 +\isamarkupsubsection{The preprocessor \label{sec:preproc}%
9.404 +}
9.405 +\isamarkuptrue%
9.406 +%
9.407 +\begin{isamarkuptext}%
9.408 +Before selected function theorems are turned into abstract
9.409 + code, a chain of definitional transformation steps is carried
9.410 + out: \emph{preprocessing}. In essence, the preprocessor
9.411 + consists of two components: a \emph{simpset} and \emph{function transformers}.
9.412 +
9.413 + The \emph{simpset} can apply the full generality of the
9.414 + Isabelle simplifier. Due to the interpretation of theorems as code
9.415 + equations, rewrites are applied to the right hand side and the
9.416 + arguments of the left hand side of an equation, but never to the
9.417 + constant heading the left hand side. An important special case are
9.418 + \emph{unfold theorems}, which may be declared and removed using
9.419 + the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
9.420 + attribute, respectively.
9.421 +
9.422 + Some common applications:%
9.423 +\end{isamarkuptext}%
9.424 +\isamarkuptrue%
9.425 +%
9.426 +\begin{itemize}
9.427 +%
9.428 +\begin{isamarkuptext}%
9.429 +\item replacing non-executable constructs by executable ones:%
9.430 +\end{isamarkuptext}%
9.431 +\isamarkuptrue%
9.432 +%
9.433 +\isadelimquote
9.434 +%
9.435 +\endisadelimquote
9.436 +%
9.437 +\isatagquote
9.438 +\isacommand{lemma}\isamarkupfalse%
9.439 +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
9.440 +\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
9.441 +\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}%
9.442 +\endisatagquote
9.443 +{\isafoldquote}%
9.444 +%
9.445 +\isadelimquote
9.446 +%
9.447 +\endisadelimquote
9.448 +%
9.449 +\begin{isamarkuptext}%
9.450 +\item eliminating superfluous constants:%
9.451 +\end{isamarkuptext}%
9.452 +\isamarkuptrue%
9.453 +%
9.454 +\isadelimquote
9.455 +%
9.456 +\endisadelimquote
9.457 +%
9.458 +\isatagquote
9.459 +\isacommand{lemma}\isamarkupfalse%
9.460 +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
9.461 +\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
9.462 +\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
9.463 +\endisatagquote
9.464 +{\isafoldquote}%
9.465 +%
9.466 +\isadelimquote
9.467 +%
9.468 +\endisadelimquote
9.469 +%
9.470 +\begin{isamarkuptext}%
9.471 +\item replacing executable but inconvenient constructs:%
9.472 +\end{isamarkuptext}%
9.473 +\isamarkuptrue%
9.474 +%
9.475 +\isadelimquote
9.476 +%
9.477 +\endisadelimquote
9.478 +%
9.479 +\isatagquote
9.480 +\isacommand{lemma}\isamarkupfalse%
9.481 +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
9.482 +\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
9.483 +\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}%
9.484 +\endisatagquote
9.485 +{\isafoldquote}%
9.486 +%
9.487 +\isadelimquote
9.488 +%
9.489 +\endisadelimquote
9.490 +%
9.491 +\end{itemize}
9.492 +%
9.493 +\begin{isamarkuptext}%
9.494 +\noindent \emph{Function transformers} provide a very general interface,
9.495 + transforming a list of function theorems to another
9.496 + list of function theorems, provided that neither the heading
9.497 + constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc}
9.498 + pattern elimination implemented in
9.499 + theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this
9.500 + interface.
9.501 +
9.502 + \noindent The current setup of the preprocessor may be inspected using
9.503 + the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command.
9.504 + \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
9.505 + mechanism to inspect the impact of a preprocessor setup
9.506 + on code equations.
9.507 +
9.508 + \begin{warn}
9.509 +
9.510 + Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
9.511 + preprocessor of the ancient \isa{SML\ code\ generator}; in case
9.512 + this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
9.513 + \end{warn}%
9.514 +\end{isamarkuptext}%
9.515 +\isamarkuptrue%
9.516 +%
9.517 +\isamarkupsubsection{Datatypes \label{sec:datatypes}%
9.518 +}
9.519 +\isamarkuptrue%
9.520 +%
9.521 +\begin{isamarkuptext}%
9.522 +Conceptually, any datatype is spanned by a set of
9.523 + \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in
9.524 + \isa{{\isasymtau}}. The HOL datatype package by default registers any new
9.525 + datatype in the table of datatypes, which may be inspected using the
9.526 + \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
9.527 +
9.528 + In some cases, it is appropriate to alter or extend this table. As
9.529 + an example, we will develop an alternative representation of the
9.530 + queue example given in \secref{sec:intro}. The amortised
9.531 + representation is convenient for generating code but exposes its
9.532 + \qt{implementation} details, which may be cumbersome when proving
9.533 + theorems about it. Therefore, here is a simple, straightforward
9.534 + representation of queues:%
9.535 +\end{isamarkuptext}%
9.536 +\isamarkuptrue%
9.537 +%
9.538 +\isadelimquote
9.539 +%
9.540 +\endisadelimquote
9.541 +%
9.542 +\isatagquote
9.543 +\isacommand{datatype}\isamarkupfalse%
9.544 +\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
9.545 +\isanewline
9.546 +\isacommand{definition}\isamarkupfalse%
9.547 +\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
9.548 +\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
9.549 +\isanewline
9.550 +\isacommand{primrec}\isamarkupfalse%
9.551 +\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
9.552 +\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.553 +\isanewline
9.554 +\isacommand{fun}\isamarkupfalse%
9.555 +\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
9.556 +\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.557 +\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
9.558 +\endisatagquote
9.559 +{\isafoldquote}%
9.560 +%
9.561 +\isadelimquote
9.562 +%
9.563 +\endisadelimquote
9.564 +%
9.565 +\begin{isamarkuptext}%
9.566 +\noindent This we can use directly for proving; for executing,
9.567 + we provide an alternative characterisation:%
9.568 +\end{isamarkuptext}%
9.569 +\isamarkuptrue%
9.570 +%
9.571 +\isadelimquote
9.572 +%
9.573 +\endisadelimquote
9.574 +%
9.575 +\isatagquote
9.576 +\isacommand{definition}\isamarkupfalse%
9.577 +\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
9.578 +\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.579 +\isanewline
9.580 +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
9.581 +\ AQueue%
9.582 +\endisatagquote
9.583 +{\isafoldquote}%
9.584 +%
9.585 +\isadelimquote
9.586 +%
9.587 +\endisadelimquote
9.588 +%
9.589 +\begin{isamarkuptext}%
9.590 +\noindent Here we define a \qt{constructor} \isa{AQueue} which
9.591 + is defined in terms of \isa{Queue} and interprets its arguments
9.592 + according to what the \emph{content} of an amortised queue is supposed
9.593 + to be. Equipped with this, we are able to prove the following equations
9.594 + for our primitive queue operations which \qt{implement} the simple
9.595 + queues in an amortised fashion:%
9.596 +\end{isamarkuptext}%
9.597 +\isamarkuptrue%
9.598 +%
9.599 +\isadelimquote
9.600 +%
9.601 +\endisadelimquote
9.602 +%
9.603 +\isatagquote
9.604 +\isacommand{lemma}\isamarkupfalse%
9.605 +\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
9.606 +\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
9.607 +\ \ \isacommand{unfolding}\isamarkupfalse%
9.608 +\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
9.609 +\ simp\isanewline
9.610 +\isanewline
9.611 +\isacommand{lemma}\isamarkupfalse%
9.612 +\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
9.613 +\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
9.614 +\ \ \isacommand{unfolding}\isamarkupfalse%
9.615 +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
9.616 +\ simp\isanewline
9.617 +\isanewline
9.618 +\isacommand{lemma}\isamarkupfalse%
9.619 +\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
9.620 +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
9.621 +\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
9.622 +\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.623 +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.624 +\ \ \isacommand{unfolding}\isamarkupfalse%
9.625 +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
9.626 +\ simp{\isacharunderscore}all%
9.627 +\endisatagquote
9.628 +{\isafoldquote}%
9.629 +%
9.630 +\isadelimquote
9.631 +%
9.632 +\endisadelimquote
9.633 +%
9.634 +\begin{isamarkuptext}%
9.635 +\noindent For completeness, we provide a substitute for the
9.636 + \isa{case} combinator on queues:%
9.637 +\end{isamarkuptext}%
9.638 +\isamarkuptrue%
9.639 +%
9.640 +\isadelimquote
9.641 +%
9.642 +\endisadelimquote
9.643 +%
9.644 +\isatagquote
9.645 +\isacommand{lemma}\isamarkupfalse%
9.646 +\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
9.647 +\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.648 +\ \ \isacommand{unfolding}\isamarkupfalse%
9.649 +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
9.650 +\ simp%
9.651 +\endisatagquote
9.652 +{\isafoldquote}%
9.653 +%
9.654 +\isadelimquote
9.655 +%
9.656 +\endisadelimquote
9.657 +%
9.658 +\begin{isamarkuptext}%
9.659 +\noindent The resulting code looks as expected:%
9.660 +\end{isamarkuptext}%
9.661 +\isamarkuptrue%
9.662 +%
9.663 +\isadelimquote
9.664 +%
9.665 +\endisadelimquote
9.666 +%
9.667 +\isatagquote
9.668 +%
9.669 +\begin{isamarkuptext}%
9.670 +\isatypewriter%
9.671 +\noindent%
9.672 +\hspace*{0pt}structure Example :~sig\\
9.673 +\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
9.674 +\hspace*{0pt} ~val rev :~'a list -> 'a list\\
9.675 +\hspace*{0pt} ~val null :~'a list -> bool\\
9.676 +\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
9.677 +\hspace*{0pt} ~val empty :~'a queue\\
9.678 +\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
9.679 +\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
9.680 +\hspace*{0pt}end = struct\\
9.681 +\hspace*{0pt}\\
9.682 +\hspace*{0pt}fun foldl f a [] = a\\
9.683 +\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
9.684 +\hspace*{0pt}\\
9.685 +\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
9.686 +\hspace*{0pt}\\
9.687 +\hspace*{0pt}fun null [] = true\\
9.688 +\hspace*{0pt} ~| null (x ::~xs) = false;\\
9.689 +\hspace*{0pt}\\
9.690 +\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
9.691 +\hspace*{0pt}\\
9.692 +\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
9.693 +\hspace*{0pt}\\
9.694 +\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
9.695 +\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
9.696 +\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
9.697 +\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
9.698 +\hspace*{0pt}\\
9.699 +\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
9.700 +\hspace*{0pt}\\
9.701 +\hspace*{0pt}end;~(*struct Example*)%
9.702 +\end{isamarkuptext}%
9.703 +\isamarkuptrue%
9.704 +%
9.705 +\endisatagquote
9.706 +{\isafoldquote}%
9.707 +%
9.708 +\isadelimquote
9.709 +%
9.710 +\endisadelimquote
9.711 +%
9.712 +\begin{isamarkuptext}%
9.713 +\noindent From this example, it can be glimpsed that using own
9.714 + constructor sets is a little delicate since it changes the set of
9.715 + valid patterns for values of that type. Without going into much
9.716 + detail, here some practical hints:
9.717 +
9.718 + \begin{itemize}
9.719 +
9.720 + \item When changing the constructor set for datatypes, take care
9.721 + to provide alternative equations for the \isa{case} combinator.
9.722 +
9.723 + \item Values in the target language need not to be normalised --
9.724 + different values in the target language may represent the same
9.725 + value in the logic.
9.726 +
9.727 + \item Usually, a good methodology to deal with the subtleties of
9.728 + pattern matching is to see the type as an abstract type: provide
9.729 + a set of operations which operate on the concrete representation
9.730 + of the type, and derive further operations by combinations of
9.731 + these primitive ones, without relying on a particular
9.732 + representation.
9.733 +
9.734 + \end{itemize}%
9.735 +\end{isamarkuptext}%
9.736 +\isamarkuptrue%
9.737 +%
9.738 +\isamarkupsubsection{Equality%
9.739 +}
9.740 +\isamarkuptrue%
9.741 +%
9.742 +\begin{isamarkuptext}%
9.743 +Surely you have already noticed how equality is treated
9.744 + by the code generator:%
9.745 +\end{isamarkuptext}%
9.746 +\isamarkuptrue%
9.747 +%
9.748 +\isadelimquote
9.749 +%
9.750 +\endisadelimquote
9.751 +%
9.752 +\isatagquote
9.753 +\isacommand{primrec}\isamarkupfalse%
9.754 +\ 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
9.755 +\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
9.756 +\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
9.757 +\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
9.758 +\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
9.759 +\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
9.760 +\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
9.761 +\endisatagquote
9.762 +{\isafoldquote}%
9.763 +%
9.764 +\isadelimquote
9.765 +%
9.766 +\endisadelimquote
9.767 +%
9.768 +\begin{isamarkuptext}%
9.769 +\noindent During preprocessing, the membership test is rewritten,
9.770 + resulting in \isa{List{\isachardot}member}, which itself
9.771 + performs an explicit equality check.%
9.772 +\end{isamarkuptext}%
9.773 +\isamarkuptrue%
9.774 +%
9.775 +\isadelimquote
9.776 +%
9.777 +\endisadelimquote
9.778 +%
9.779 +\isatagquote
9.780 +%
9.781 +\begin{isamarkuptext}%
9.782 +\isatypewriter%
9.783 +\noindent%
9.784 +\hspace*{0pt}structure Example :~sig\\
9.785 +\hspace*{0pt} ~type 'a eq\\
9.786 +\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
9.787 +\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
9.788 +\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\
9.789 +\hspace*{0pt} ~val collect{\char95}duplicates :\\
9.790 +\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
9.791 +\hspace*{0pt}end = struct\\
9.792 +\hspace*{0pt}\\
9.793 +\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
9.794 +\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\
9.795 +\hspace*{0pt}\\
9.796 +\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
9.797 +\hspace*{0pt}\\
9.798 +\hspace*{0pt}fun member A{\char95}~[] y = false\\
9.799 +\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\
9.800 +\hspace*{0pt}\\
9.801 +\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
9.802 +\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
9.803 +\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
9.804 +\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
9.805 +\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
9.806 +\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
9.807 +\hspace*{0pt}\\
9.808 +\hspace*{0pt}end;~(*struct Example*)%
9.809 +\end{isamarkuptext}%
9.810 +\isamarkuptrue%
9.811 +%
9.812 +\endisatagquote
9.813 +{\isafoldquote}%
9.814 +%
9.815 +\isadelimquote
9.816 +%
9.817 +\endisadelimquote
9.818 +%
9.819 +\begin{isamarkuptext}%
9.820 +\noindent Obviously, polymorphic equality is implemented the Haskell
9.821 + way using a type class. How is this achieved? HOL introduces
9.822 + an explicit class \isa{eq} with a corresponding operation
9.823 + \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.
9.824 + The preprocessing framework does the rest by propagating the
9.825 + \isa{eq} constraints through all dependent code equations.
9.826 + For datatypes, instances of \isa{eq} are implicitly derived
9.827 + when possible. For other types, you may instantiate \isa{eq}
9.828 + manually like any other type class.%
9.829 +\end{isamarkuptext}%
9.830 +\isamarkuptrue%
9.831 +%
9.832 +\isamarkupsubsection{Explicit partiality%
9.833 +}
9.834 +\isamarkuptrue%
9.835 +%
9.836 +\begin{isamarkuptext}%
9.837 +Partiality usually enters the game by partial patterns, as
9.838 + in the following example, again for amortised queues:%
9.839 +\end{isamarkuptext}%
9.840 +\isamarkuptrue%
9.841 +%
9.842 +\isadelimquote
9.843 +%
9.844 +\endisadelimquote
9.845 +%
9.846 +\isatagquote
9.847 +\isacommand{definition}\isamarkupfalse%
9.848 +\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
9.849 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline
9.850 +\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.851 +\isanewline
9.852 +\isacommand{lemma}\isamarkupfalse%
9.853 +\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
9.854 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.855 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
9.856 +\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.857 +\ \ \isacommand{by}\isamarkupfalse%
9.858 +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
9.859 +\endisatagquote
9.860 +{\isafoldquote}%
9.861 +%
9.862 +\isadelimquote
9.863 +%
9.864 +\endisadelimquote
9.865 +%
9.866 +\begin{isamarkuptext}%
9.867 +\noindent In the corresponding code, there is no equation
9.868 + for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
9.869 +\end{isamarkuptext}%
9.870 +\isamarkuptrue%
9.871 +%
9.872 +\isadelimquote
9.873 +%
9.874 +\endisadelimquote
9.875 +%
9.876 +\isatagquote
9.877 +%
9.878 +\begin{isamarkuptext}%
9.879 +\isatypewriter%
9.880 +\noindent%
9.881 +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
9.882 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
9.883 +\hspace*{0pt} ~let {\char123}\\
9.884 +\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
9.885 +\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
9.886 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
9.887 +\end{isamarkuptext}%
9.888 +\isamarkuptrue%
9.889 +%
9.890 +\endisatagquote
9.891 +{\isafoldquote}%
9.892 +%
9.893 +\isadelimquote
9.894 +%
9.895 +\endisadelimquote
9.896 +%
9.897 +\begin{isamarkuptext}%
9.898 +\noindent In some cases it is desirable to have this
9.899 + pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
9.900 +\end{isamarkuptext}%
9.901 +\isamarkuptrue%
9.902 +%
9.903 +\isadelimquote
9.904 +%
9.905 +\endisadelimquote
9.906 +%
9.907 +\isatagquote
9.908 +\isacommand{axiomatization}\isamarkupfalse%
9.909 +\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
9.910 +\isanewline
9.911 +\isacommand{definition}\isamarkupfalse%
9.912 +\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
9.913 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.914 +\isanewline
9.915 +\isacommand{lemma}\isamarkupfalse%
9.916 +\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
9.917 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
9.918 +\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.919 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
9.920 +\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
9.921 +\ \ \isacommand{by}\isamarkupfalse%
9.922 +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
9.923 +\endisatagquote
9.924 +{\isafoldquote}%
9.925 +%
9.926 +\isadelimquote
9.927 +%
9.928 +\endisadelimquote
9.929 +%
9.930 +\begin{isamarkuptext}%
9.931 +Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs.
9.932 +
9.933 + Normally, if constants without any code equations occur in a
9.934 + program, the code generator complains (since in most cases this is
9.935 + indeed an error). But such constants can also be thought
9.936 + of as function definitions which always fail,
9.937 + since there is never a successful pattern match on the left hand
9.938 + side. In order to categorise a constant into that category
9.939 + explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
9.940 +\end{isamarkuptext}%
9.941 +\isamarkuptrue%
9.942 +%
9.943 +\isadelimquote
9.944 +%
9.945 +\endisadelimquote
9.946 +%
9.947 +\isatagquote
9.948 +\isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
9.949 +\ empty{\isacharunderscore}queue%
9.950 +\endisatagquote
9.951 +{\isafoldquote}%
9.952 +%
9.953 +\isadelimquote
9.954 +%
9.955 +\endisadelimquote
9.956 +%
9.957 +\begin{isamarkuptext}%
9.958 +\noindent Then the code generator will just insert an error or
9.959 + exception at the appropriate position:%
9.960 +\end{isamarkuptext}%
9.961 +\isamarkuptrue%
9.962 +%
9.963 +\isadelimquote
9.964 +%
9.965 +\endisadelimquote
9.966 +%
9.967 +\isatagquote
9.968 +%
9.969 +\begin{isamarkuptext}%
9.970 +\isatypewriter%
9.971 +\noindent%
9.972 +\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
9.973 +\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
9.974 +\hspace*{0pt}\\
9.975 +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
9.976 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
9.977 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
9.978 +\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
9.979 +\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
9.980 +\end{isamarkuptext}%
9.981 +\isamarkuptrue%
9.982 +%
9.983 +\endisatagquote
9.984 +{\isafoldquote}%
9.985 +%
9.986 +\isadelimquote
9.987 +%
9.988 +\endisadelimquote
9.989 +%
9.990 +\begin{isamarkuptext}%
9.991 +\noindent This feature however is rarely needed in practice.
9.992 + Note also that the \isa{HOL} default setup already declares
9.993 + \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
9.994 + likely to be used in such situations.%
9.995 +\end{isamarkuptext}%
9.996 +\isamarkuptrue%
9.997 +%
9.998 +\isadelimtheory
9.999 +%
9.1000 +\endisadelimtheory
9.1001 +%
9.1002 +\isatagtheory
9.1003 +\isacommand{end}\isamarkupfalse%
9.1004 +%
9.1005 +\endisatagtheory
9.1006 +{\isafoldtheory}%
9.1007 +%
9.1008 +\isadelimtheory
9.1009 +%
9.1010 +\endisadelimtheory
9.1011 +\isanewline
9.1012 +\end{isabellebody}%
9.1013 +%%% Local Variables:
9.1014 +%%% mode: latex
9.1015 +%%% TeX-master: "root"
9.1016 +%%% End:
10.1 --- a/doc-src/Codegen/Thy/document/Further.tex Fri Aug 13 12:15:25 2010 +0200
10.2 +++ b/doc-src/Codegen/Thy/document/Further.tex Fri Aug 13 14:41:27 2010 +0200
10.3 @@ -389,6 +389,179 @@
10.4 \end{isamarkuptext}%
10.5 \isamarkuptrue%
10.6 %
10.7 +\isamarkupsubsection{ML system interfaces \label{sec:ml}%
10.8 +}
10.9 +\isamarkuptrue%
10.10 +%
10.11 +\begin{isamarkuptext}%
10.12 +Since the code generator framework not only aims to provide
10.13 + a nice Isar interface but also to form a base for
10.14 + code-generation-based applications, here a short
10.15 + description of the most important ML interfaces.%
10.16 +\end{isamarkuptext}%
10.17 +\isamarkuptrue%
10.18 +%
10.19 +\isamarkupsubsubsection{Managing executable content%
10.20 +}
10.21 +\isamarkuptrue%
10.22 +%
10.23 +\isadelimmlref
10.24 +%
10.25 +\endisadelimmlref
10.26 +%
10.27 +\isatagmlref
10.28 +%
10.29 +\begin{isamarkuptext}%
10.30 +\begin{mldecls}
10.31 + \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
10.32 + \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
10.33 + \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
10.34 + \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
10.35 + \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
10.36 +\verb| -> theory -> theory| \\
10.37 + \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
10.38 + \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
10.39 + \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
10.40 +\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\
10.41 + \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
10.42 + \end{mldecls}
10.43 +
10.44 + \begin{description}
10.45 +
10.46 + \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
10.47 + theorem \isa{thm} to executable content.
10.48 +
10.49 + \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
10.50 + theorem \isa{thm} from executable content, if present.
10.51 +
10.52 + \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
10.53 + the preprocessor simpset.
10.54 +
10.55 + \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
10.56 + function transformer \isa{f} (named \isa{name}) to executable content;
10.57 + \isa{f} is a transformer of the code equations belonging
10.58 + to a certain function definition, depending on the
10.59 + current theory context. Returning \isa{NONE} indicates that no
10.60 + transformation took place; otherwise, the whole process will be iterated
10.61 + with the new code equations.
10.62 +
10.63 + \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes
10.64 + function transformer named \isa{name} from executable content.
10.65 +
10.66 + \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
10.67 + a datatype to executable content, with generation
10.68 + set \isa{cs}.
10.69 +
10.70 + \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const}
10.71 + returns type constructor corresponding to
10.72 + constructor \isa{const}; returns \isa{NONE}
10.73 + if \isa{const} is no constructor.
10.74 +
10.75 + \end{description}%
10.76 +\end{isamarkuptext}%
10.77 +\isamarkuptrue%
10.78 +%
10.79 +\endisatagmlref
10.80 +{\isafoldmlref}%
10.81 +%
10.82 +\isadelimmlref
10.83 +%
10.84 +\endisadelimmlref
10.85 +%
10.86 +\isamarkupsubsubsection{Auxiliary%
10.87 +}
10.88 +\isamarkuptrue%
10.89 +%
10.90 +\isadelimmlref
10.91 +%
10.92 +\endisadelimmlref
10.93 +%
10.94 +\isatagmlref
10.95 +%
10.96 +\begin{isamarkuptext}%
10.97 +\begin{mldecls}
10.98 + \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
10.99 + \end{mldecls}
10.100 +
10.101 + \begin{description}
10.102 +
10.103 + \item \verb|Code.read_const|~\isa{thy}~\isa{s}
10.104 + reads a constant as a concrete term expression \isa{s}.
10.105 +
10.106 + \end{description}%
10.107 +\end{isamarkuptext}%
10.108 +\isamarkuptrue%
10.109 +%
10.110 +\endisatagmlref
10.111 +{\isafoldmlref}%
10.112 +%
10.113 +\isadelimmlref
10.114 +%
10.115 +\endisadelimmlref
10.116 +%
10.117 +\isamarkupsubsubsection{Data depending on the theory's executable content%
10.118 +}
10.119 +\isamarkuptrue%
10.120 +%
10.121 +\begin{isamarkuptext}%
10.122 +Implementing code generator applications on top
10.123 + of the framework set out so far usually not only
10.124 + involves using those primitive interfaces
10.125 + but also storing code-dependent data and various
10.126 + other things.
10.127 +
10.128 + Due to incrementality of code generation, changes in the
10.129 + theory's executable content have to be propagated in a
10.130 + certain fashion. Additionally, such changes may occur
10.131 + not only during theory extension but also during theory
10.132 + merge, which is a little bit nasty from an implementation
10.133 + point of view. The framework provides a solution
10.134 + to this technical challenge by providing a functorial
10.135 + data slot \verb|Code_Data|; on instantiation
10.136 + of this functor, the following types and operations
10.137 + are required:
10.138 +
10.139 + \medskip
10.140 + \begin{tabular}{l}
10.141 + \isa{type\ T} \\
10.142 + \isa{val\ empty{\isacharcolon}\ T} \\
10.143 + \end{tabular}
10.144 +
10.145 + \begin{description}
10.146 +
10.147 + \item \isa{T} the type of data to store.
10.148 +
10.149 + \item \isa{empty} initial (empty) data.
10.150 +
10.151 + \end{description}
10.152 +
10.153 + \noindent An instance of \verb|Code_Data| provides the following
10.154 + interface:
10.155 +
10.156 + \medskip
10.157 + \begin{tabular}{l}
10.158 + \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
10.159 + \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
10.160 + \end{tabular}
10.161 +
10.162 + \begin{description}
10.163 +
10.164 + \item \isa{change} update of current data (cached!)
10.165 + by giving a continuation.
10.166 +
10.167 + \item \isa{change{\isacharunderscore}yield} update with side result.
10.168 +
10.169 + \end{description}%
10.170 +\end{isamarkuptext}%
10.171 +\isamarkuptrue%
10.172 +%
10.173 +\begin{isamarkuptext}%
10.174 +\bigskip
10.175 +
10.176 + \emph{Happy proving, happy hacking!}%
10.177 +\end{isamarkuptext}%
10.178 +\isamarkuptrue%
10.179 +%
10.180 \isadelimtheory
10.181 %
10.182 \endisadelimtheory
11.1 --- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Fri Aug 13 12:15:25 2010 +0200
11.2 +++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Fri Aug 13 14:41:27 2010 +0200
11.3 @@ -18,7 +18,7 @@
11.4 %
11.5 \endisadelimtheory
11.6 %
11.7 -\isamarkupsubsection{Inductive Predicates%
11.8 +\isamarkupsection{Inductive Predicates%
11.9 }
11.10 \isamarkuptrue%
11.11 %
12.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex Fri Aug 13 12:15:25 2010 +0200
12.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Fri Aug 13 14:41:27 2010 +0200
12.3 @@ -18,7 +18,27 @@
12.4 %
12.5 \endisadelimtheory
12.6 %
12.7 -\isamarkupsection{Introduction and Overview%
12.8 +\isamarkupsection{Introduction%
12.9 +}
12.10 +\isamarkuptrue%
12.11 +%
12.12 +\isamarkupsubsection{Code generation fundamental: shallow embedding%
12.13 +}
12.14 +\isamarkuptrue%
12.15 +%
12.16 +\isamarkupsubsection{A quick start with the \isa{Isabelle{\isacharslash}HOL} toolbox%
12.17 +}
12.18 +\isamarkuptrue%
12.19 +%
12.20 +\isamarkupsubsection{Type classes%
12.21 +}
12.22 +\isamarkuptrue%
12.23 +%
12.24 +\isamarkupsubsection{How to continue from here%
12.25 +}
12.26 +\isamarkuptrue%
12.27 +%
12.28 +\isamarkupsubsection{If something goes utterly wrong%
12.29 }
12.30 \isamarkuptrue%
12.31 %
12.32 @@ -263,6 +283,32 @@
12.33 \end{isamarkuptext}%
12.34 \isamarkuptrue%
12.35 %
12.36 +\isamarkupsubsection{If something utterly fails%
12.37 +}
12.38 +\isamarkuptrue%
12.39 +%
12.40 +\begin{isamarkuptext}%
12.41 +Under certain circumstances, the code generator fails to produce
12.42 + code entirely.
12.43 +
12.44 + \begin{description}
12.45 +
12.46 + \ditem{generate only one module}
12.47 +
12.48 + \ditem{check with a different target language}
12.49 +
12.50 + \ditem{inspect code equations}
12.51 +
12.52 + \ditem{inspect preprocessor setup}
12.53 +
12.54 + \ditem{generate exceptions}
12.55 +
12.56 + \ditem{remove offending code equations}
12.57 +
12.58 + \end{description}%
12.59 +\end{isamarkuptext}%
12.60 +\isamarkuptrue%
12.61 +%
12.62 \isamarkupsubsection{Code generator architecture \label{sec:concept}%
12.63 }
12.64 \isamarkuptrue%
13.1 --- a/doc-src/Codegen/Thy/document/ML.tex Fri Aug 13 12:15:25 2010 +0200
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,240 +0,0 @@
13.4 -%
13.5 -\begin{isabellebody}%
13.6 -\def\isabellecontext{ML}%
13.7 -%
13.8 -\isadelimtheory
13.9 -%
13.10 -\endisadelimtheory
13.11 -%
13.12 -\isatagtheory
13.13 -\isacommand{theory}\isamarkupfalse%
13.14 -\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\isanewline
13.15 -\isakeyword{imports}\ Setup\isanewline
13.16 -\isakeyword{begin}%
13.17 -\endisatagtheory
13.18 -{\isafoldtheory}%
13.19 -%
13.20 -\isadelimtheory
13.21 -%
13.22 -\endisadelimtheory
13.23 -%
13.24 -\isamarkupsection{ML system interfaces \label{sec:ml}%
13.25 -}
13.26 -\isamarkuptrue%
13.27 -%
13.28 -\begin{isamarkuptext}%
13.29 -Since the code generator framework not only aims to provide
13.30 - a nice Isar interface but also to form a base for
13.31 - code-generation-based applications, here a short
13.32 - description of the most important ML interfaces.%
13.33 -\end{isamarkuptext}%
13.34 -\isamarkuptrue%
13.35 -%
13.36 -\isamarkupsubsection{Executable theory content: \isa{Code}%
13.37 -}
13.38 -\isamarkuptrue%
13.39 -%
13.40 -\begin{isamarkuptext}%
13.41 -This Pure module implements the core notions of
13.42 - executable content of a theory.%
13.43 -\end{isamarkuptext}%
13.44 -\isamarkuptrue%
13.45 -%
13.46 -\isamarkupsubsubsection{Managing executable content%
13.47 -}
13.48 -\isamarkuptrue%
13.49 -%
13.50 -\isadelimmlref
13.51 -%
13.52 -\endisadelimmlref
13.53 -%
13.54 -\isatagmlref
13.55 -%
13.56 -\begin{isamarkuptext}%
13.57 -\begin{mldecls}
13.58 - \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
13.59 - \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
13.60 - \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
13.61 - \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
13.62 - \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
13.63 -\verb| -> theory -> theory| \\
13.64 - \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
13.65 - \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
13.66 - \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
13.67 -\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\
13.68 - \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
13.69 - \end{mldecls}
13.70 -
13.71 - \begin{description}
13.72 -
13.73 - \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
13.74 - theorem \isa{thm} to executable content.
13.75 -
13.76 - \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
13.77 - theorem \isa{thm} from executable content, if present.
13.78 -
13.79 - \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
13.80 - the preprocessor simpset.
13.81 -
13.82 - \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
13.83 - function transformer \isa{f} (named \isa{name}) to executable content;
13.84 - \isa{f} is a transformer of the code equations belonging
13.85 - to a certain function definition, depending on the
13.86 - current theory context. Returning \isa{NONE} indicates that no
13.87 - transformation took place; otherwise, the whole process will be iterated
13.88 - with the new code equations.
13.89 -
13.90 - \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes
13.91 - function transformer named \isa{name} from executable content.
13.92 -
13.93 - \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
13.94 - a datatype to executable content, with generation
13.95 - set \isa{cs}.
13.96 -
13.97 - \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const}
13.98 - returns type constructor corresponding to
13.99 - constructor \isa{const}; returns \isa{NONE}
13.100 - if \isa{const} is no constructor.
13.101 -
13.102 - \end{description}%
13.103 -\end{isamarkuptext}%
13.104 -\isamarkuptrue%
13.105 -%
13.106 -\endisatagmlref
13.107 -{\isafoldmlref}%
13.108 -%
13.109 -\isadelimmlref
13.110 -%
13.111 -\endisadelimmlref
13.112 -%
13.113 -\isamarkupsubsection{Auxiliary%
13.114 -}
13.115 -\isamarkuptrue%
13.116 -%
13.117 -\isadelimmlref
13.118 -%
13.119 -\endisadelimmlref
13.120 -%
13.121 -\isatagmlref
13.122 -%
13.123 -\begin{isamarkuptext}%
13.124 -\begin{mldecls}
13.125 - \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
13.126 - \end{mldecls}
13.127 -
13.128 - \begin{description}
13.129 -
13.130 - \item \verb|Code.read_const|~\isa{thy}~\isa{s}
13.131 - reads a constant as a concrete term expression \isa{s}.
13.132 -
13.133 - \end{description}%
13.134 -\end{isamarkuptext}%
13.135 -\isamarkuptrue%
13.136 -%
13.137 -\endisatagmlref
13.138 -{\isafoldmlref}%
13.139 -%
13.140 -\isadelimmlref
13.141 -%
13.142 -\endisadelimmlref
13.143 -%
13.144 -\isamarkupsubsection{Implementing code generator applications%
13.145 -}
13.146 -\isamarkuptrue%
13.147 -%
13.148 -\begin{isamarkuptext}%
13.149 -Implementing code generator applications on top
13.150 - of the framework set out so far usually not only
13.151 - involves using those primitive interfaces
13.152 - but also storing code-dependent data and various
13.153 - other things.%
13.154 -\end{isamarkuptext}%
13.155 -\isamarkuptrue%
13.156 -%
13.157 -\isamarkupsubsubsection{Data depending on the theory's executable content%
13.158 -}
13.159 -\isamarkuptrue%
13.160 -%
13.161 -\begin{isamarkuptext}%
13.162 -Due to incrementality of code generation, changes in the
13.163 - theory's executable content have to be propagated in a
13.164 - certain fashion. Additionally, such changes may occur
13.165 - not only during theory extension but also during theory
13.166 - merge, which is a little bit nasty from an implementation
13.167 - point of view. The framework provides a solution
13.168 - to this technical challenge by providing a functorial
13.169 - data slot \verb|Code_Data|; on instantiation
13.170 - of this functor, the following types and operations
13.171 - are required:
13.172 -
13.173 - \medskip
13.174 - \begin{tabular}{l}
13.175 - \isa{type\ T} \\
13.176 - \isa{val\ empty{\isacharcolon}\ T} \\
13.177 - \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ string\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
13.178 - \end{tabular}
13.179 -
13.180 - \begin{description}
13.181 -
13.182 - \item \isa{T} the type of data to store.
13.183 -
13.184 - \item \isa{empty} initial (empty) data.
13.185 -
13.186 - \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content;
13.187 - \isa{consts} indicates the kind
13.188 - of change: \verb|NONE| stands for a fundamental change
13.189 - which invalidates any existing code, \isa{SOME\ consts}
13.190 - hints that executable content for constants \isa{consts}
13.191 - has changed.
13.192 -
13.193 - \end{description}
13.194 -
13.195 - \noindent An instance of \verb|Code_Data| provides the following
13.196 - interface:
13.197 -
13.198 - \medskip
13.199 - \begin{tabular}{l}
13.200 - \isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
13.201 - \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
13.202 - \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
13.203 - \end{tabular}
13.204 -
13.205 - \begin{description}
13.206 -
13.207 - \item \isa{get} retrieval of the current data.
13.208 -
13.209 - \item \isa{change} update of current data (cached!)
13.210 - by giving a continuation.
13.211 -
13.212 - \item \isa{change{\isacharunderscore}yield} update with side result.
13.213 -
13.214 - \end{description}%
13.215 -\end{isamarkuptext}%
13.216 -\isamarkuptrue%
13.217 -%
13.218 -\begin{isamarkuptext}%
13.219 -\bigskip
13.220 -
13.221 - \emph{Happy proving, happy hacking!}%
13.222 -\end{isamarkuptext}%
13.223 -\isamarkuptrue%
13.224 -%
13.225 -\isadelimtheory
13.226 -%
13.227 -\endisadelimtheory
13.228 -%
13.229 -\isatagtheory
13.230 -\isacommand{end}\isamarkupfalse%
13.231 -%
13.232 -\endisatagtheory
13.233 -{\isafoldtheory}%
13.234 -%
13.235 -\isadelimtheory
13.236 -%
13.237 -\endisadelimtheory
13.238 -\isanewline
13.239 -\end{isabellebody}%
13.240 -%%% Local Variables:
13.241 -%%% mode: latex
13.242 -%%% TeX-master: "root"
13.243 -%%% End:
14.1 --- a/doc-src/Codegen/Thy/document/Program.tex Fri Aug 13 12:15:25 2010 +0200
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,1013 +0,0 @@
14.4 -%
14.5 -\begin{isabellebody}%
14.6 -\def\isabellecontext{Program}%
14.7 -%
14.8 -\isadelimtheory
14.9 -%
14.10 -\endisadelimtheory
14.11 -%
14.12 -\isatagtheory
14.13 -\isacommand{theory}\isamarkupfalse%
14.14 -\ Program\isanewline
14.15 -\isakeyword{imports}\ Introduction\isanewline
14.16 -\isakeyword{begin}%
14.17 -\endisatagtheory
14.18 -{\isafoldtheory}%
14.19 -%
14.20 -\isadelimtheory
14.21 -%
14.22 -\endisadelimtheory
14.23 -%
14.24 -\isamarkupsection{Turning Theories into Programs \label{sec:program}%
14.25 -}
14.26 -\isamarkuptrue%
14.27 -%
14.28 -\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup%
14.29 -}
14.30 -\isamarkuptrue%
14.31 -%
14.32 -\begin{isamarkuptext}%
14.33 -We have already seen how by default equations stemming from
14.34 - \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}, \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
14.35 - statements are used for code generation. This default behaviour
14.36 - can be changed, e.g.\ by providing different code equations.
14.37 - The customisations shown in this section are \emph{safe}
14.38 - as regards correctness: all programs that can be generated are partially
14.39 - correct.%
14.40 -\end{isamarkuptext}%
14.41 -\isamarkuptrue%
14.42 -%
14.43 -\isamarkupsubsection{Selecting code equations%
14.44 -}
14.45 -\isamarkuptrue%
14.46 -%
14.47 -\begin{isamarkuptext}%
14.48 -Coming back to our introductory example, we
14.49 - could provide an alternative code equations for \isa{dequeue}
14.50 - explicitly:%
14.51 -\end{isamarkuptext}%
14.52 -\isamarkuptrue%
14.53 -%
14.54 -\isadelimquote
14.55 -%
14.56 -\endisadelimquote
14.57 -%
14.58 -\isatagquote
14.59 -\isacommand{lemma}\isamarkupfalse%
14.60 -\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
14.61 -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
14.62 -\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
14.63 -\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.64 -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
14.65 -\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.66 -\ \ \isacommand{by}\isamarkupfalse%
14.67 -\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
14.68 -\endisatagquote
14.69 -{\isafoldquote}%
14.70 -%
14.71 -\isadelimquote
14.72 -%
14.73 -\endisadelimquote
14.74 -%
14.75 -\begin{isamarkuptext}%
14.76 -\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
14.77 - \isa{attribute} which states that the given theorems should be
14.78 - considered as code equations for a \isa{fun} statement --
14.79 - the corresponding constant is determined syntactically. The resulting code:%
14.80 -\end{isamarkuptext}%
14.81 -\isamarkuptrue%
14.82 -%
14.83 -\isadelimquote
14.84 -%
14.85 -\endisadelimquote
14.86 -%
14.87 -\isatagquote
14.88 -%
14.89 -\begin{isamarkuptext}%
14.90 -\isatypewriter%
14.91 -\noindent%
14.92 -\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
14.93 -\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
14.94 -\hspace*{0pt}dequeue (AQueue xs []) =\\
14.95 -\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
14.96 -\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
14.97 -\end{isamarkuptext}%
14.98 -\isamarkuptrue%
14.99 -%
14.100 -\endisatagquote
14.101 -{\isafoldquote}%
14.102 -%
14.103 -\isadelimquote
14.104 -%
14.105 -\endisadelimquote
14.106 -%
14.107 -\begin{isamarkuptext}%
14.108 -\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been
14.109 - replaced by the predicate \isa{null\ xs}. This is due to the default
14.110 - setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
14.111 -
14.112 - Changing the default constructor set of datatypes is also
14.113 - possible. See \secref{sec:datatypes} for an example.
14.114 -
14.115 - As told in \secref{sec:concept}, code generation is based
14.116 - on a structured collection of code theorems.
14.117 - This collection
14.118 - may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
14.119 -\end{isamarkuptext}%
14.120 -\isamarkuptrue%
14.121 -%
14.122 -\isadelimquote
14.123 -%
14.124 -\endisadelimquote
14.125 -%
14.126 -\isatagquote
14.127 -\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
14.128 -\ dequeue%
14.129 -\endisatagquote
14.130 -{\isafoldquote}%
14.131 -%
14.132 -\isadelimquote
14.133 -%
14.134 -\endisadelimquote
14.135 -%
14.136 -\begin{isamarkuptext}%
14.137 -\noindent prints a table with \emph{all} code equations
14.138 - for \isa{dequeue}, including
14.139 - \emph{all} code equations those equations depend
14.140 - on recursively.
14.141 -
14.142 - Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph
14.143 - visualising dependencies between code equations.%
14.144 -\end{isamarkuptext}%
14.145 -\isamarkuptrue%
14.146 -%
14.147 -\isamarkupsubsection{\isa{class} and \isa{instantiation}%
14.148 -}
14.149 -\isamarkuptrue%
14.150 -%
14.151 -\begin{isamarkuptext}%
14.152 -Concerning type classes and code generation, let us examine an example
14.153 - from abstract algebra:%
14.154 -\end{isamarkuptext}%
14.155 -\isamarkuptrue%
14.156 -%
14.157 -\isadelimquote
14.158 -%
14.159 -\endisadelimquote
14.160 -%
14.161 -\isatagquote
14.162 -\isacommand{class}\isamarkupfalse%
14.163 -\ semigroup\ {\isacharequal}\isanewline
14.164 -\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
14.165 -\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.166 -\isanewline
14.167 -\isacommand{class}\isamarkupfalse%
14.168 -\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
14.169 -\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
14.170 -\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
14.171 -\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
14.172 -\isanewline
14.173 -\isacommand{instantiation}\isamarkupfalse%
14.174 -\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
14.175 -\isakeyword{begin}\isanewline
14.176 -\isanewline
14.177 -\isacommand{primrec}\isamarkupfalse%
14.178 -\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
14.179 -\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.180 -\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline
14.181 -\isanewline
14.182 -\isacommand{definition}\isamarkupfalse%
14.183 -\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
14.184 -\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
14.185 -\isanewline
14.186 -\isacommand{lemma}\isamarkupfalse%
14.187 -\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline
14.188 -\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
14.189 -\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline
14.190 -\ \ \isacommand{by}\isamarkupfalse%
14.191 -\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
14.192 -\isanewline
14.193 -\isacommand{instance}\isamarkupfalse%
14.194 -\ \isacommand{proof}\isamarkupfalse%
14.195 -\isanewline
14.196 -\ \ \isacommand{fix}\isamarkupfalse%
14.197 -\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
14.198 -\ \ \isacommand{show}\isamarkupfalse%
14.199 -\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.200 -\ \ \ \ \isacommand{by}\isamarkupfalse%
14.201 -\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline
14.202 -\ \ \isacommand{show}\isamarkupfalse%
14.203 -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
14.204 -\ \ \ \ \isacommand{by}\isamarkupfalse%
14.205 -\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
14.206 -\ \ \isacommand{show}\isamarkupfalse%
14.207 -\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
14.208 -\ \ \ \ \isacommand{by}\isamarkupfalse%
14.209 -\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
14.210 -\isacommand{qed}\isamarkupfalse%
14.211 -\isanewline
14.212 -\isanewline
14.213 -\isacommand{end}\isamarkupfalse%
14.214 -%
14.215 -\endisatagquote
14.216 -{\isafoldquote}%
14.217 -%
14.218 -\isadelimquote
14.219 -%
14.220 -\endisadelimquote
14.221 -%
14.222 -\begin{isamarkuptext}%
14.223 -\noindent We define the natural operation of the natural numbers
14.224 - on monoids:%
14.225 -\end{isamarkuptext}%
14.226 -\isamarkuptrue%
14.227 -%
14.228 -\isadelimquote
14.229 -%
14.230 -\endisadelimquote
14.231 -%
14.232 -\isatagquote
14.233 -\isacommand{primrec}\isamarkupfalse%
14.234 -\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
14.235 -\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
14.236 -\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
14.237 -\endisatagquote
14.238 -{\isafoldquote}%
14.239 -%
14.240 -\isadelimquote
14.241 -%
14.242 -\endisadelimquote
14.243 -%
14.244 -\begin{isamarkuptext}%
14.245 -\noindent This we use to define the discrete exponentiation function:%
14.246 -\end{isamarkuptext}%
14.247 -\isamarkuptrue%
14.248 -%
14.249 -\isadelimquote
14.250 -%
14.251 -\endisadelimquote
14.252 -%
14.253 -\isatagquote
14.254 -\isacommand{definition}\isamarkupfalse%
14.255 -\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
14.256 -\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
14.257 -\endisatagquote
14.258 -{\isafoldquote}%
14.259 -%
14.260 -\isadelimquote
14.261 -%
14.262 -\endisadelimquote
14.263 -%
14.264 -\begin{isamarkuptext}%
14.265 -\noindent The corresponding code in Haskell uses that language's native classes:%
14.266 -\end{isamarkuptext}%
14.267 -\isamarkuptrue%
14.268 -%
14.269 -\isadelimquote
14.270 -%
14.271 -\endisadelimquote
14.272 -%
14.273 -\isatagquote
14.274 -%
14.275 -\begin{isamarkuptext}%
14.276 -\isatypewriter%
14.277 -\noindent%
14.278 -\hspace*{0pt}module Example where {\char123}\\
14.279 -\hspace*{0pt}\\
14.280 -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
14.281 -\hspace*{0pt}\\
14.282 -\hspace*{0pt}class Semigroup a where {\char123}\\
14.283 -\hspace*{0pt} ~mult ::~a -> a -> a;\\
14.284 -\hspace*{0pt}{\char125};\\
14.285 -\hspace*{0pt}\\
14.286 -\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
14.287 -\hspace*{0pt} ~neutral ::~a;\\
14.288 -\hspace*{0pt}{\char125};\\
14.289 -\hspace*{0pt}\\
14.290 -\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
14.291 -\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
14.292 -\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
14.293 -\hspace*{0pt}\\
14.294 -\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
14.295 -\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
14.296 -\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
14.297 -\hspace*{0pt}\\
14.298 -\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
14.299 -\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
14.300 -\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
14.301 -\hspace*{0pt}\\
14.302 -\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
14.303 -\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
14.304 -\hspace*{0pt}\\
14.305 -\hspace*{0pt}instance Semigroup Nat where {\char123}\\
14.306 -\hspace*{0pt} ~mult = mult{\char95}nat;\\
14.307 -\hspace*{0pt}{\char125};\\
14.308 -\hspace*{0pt}\\
14.309 -\hspace*{0pt}instance Monoid Nat where {\char123}\\
14.310 -\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
14.311 -\hspace*{0pt}{\char125};\\
14.312 -\hspace*{0pt}\\
14.313 -\hspace*{0pt}bexp ::~Nat -> Nat;\\
14.314 -\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
14.315 -\hspace*{0pt}\\
14.316 -\hspace*{0pt}{\char125}%
14.317 -\end{isamarkuptext}%
14.318 -\isamarkuptrue%
14.319 -%
14.320 -\endisatagquote
14.321 -{\isafoldquote}%
14.322 -%
14.323 -\isadelimquote
14.324 -%
14.325 -\endisadelimquote
14.326 -%
14.327 -\begin{isamarkuptext}%
14.328 -\noindent This is a convenient place to show how explicit dictionary construction
14.329 - manifests in generated code (here, the same example in \isa{SML})
14.330 - \cite{Haftmann-Nipkow:2010:code}:%
14.331 -\end{isamarkuptext}%
14.332 -\isamarkuptrue%
14.333 -%
14.334 -\isadelimquote
14.335 -%
14.336 -\endisadelimquote
14.337 -%
14.338 -\isatagquote
14.339 -%
14.340 -\begin{isamarkuptext}%
14.341 -\isatypewriter%
14.342 -\noindent%
14.343 -\hspace*{0pt}structure Example :~sig\\
14.344 -\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
14.345 -\hspace*{0pt} ~type 'a semigroup\\
14.346 -\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
14.347 -\hspace*{0pt} ~type 'a monoid\\
14.348 -\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
14.349 -\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
14.350 -\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
14.351 -\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
14.352 -\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
14.353 -\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
14.354 -\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\
14.355 -\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\
14.356 -\hspace*{0pt} ~val bexp :~nat -> nat\\
14.357 -\hspace*{0pt}end = struct\\
14.358 -\hspace*{0pt}\\
14.359 -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
14.360 -\hspace*{0pt}\\
14.361 -\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
14.362 -\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
14.363 -\hspace*{0pt}\\
14.364 -\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
14.365 -\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
14.366 -\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
14.367 -\hspace*{0pt}\\
14.368 -\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
14.369 -\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
14.370 -\hspace*{0pt}\\
14.371 -\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
14.372 -\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
14.373 -\hspace*{0pt}\\
14.374 -\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
14.375 -\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
14.376 -\hspace*{0pt}\\
14.377 -\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
14.378 -\hspace*{0pt}\\
14.379 -\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
14.380 -\hspace*{0pt}\\
14.381 -\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
14.382 -\hspace*{0pt} ~:~nat monoid;\\
14.383 -\hspace*{0pt}\\
14.384 -\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
14.385 -\hspace*{0pt}\\
14.386 -\hspace*{0pt}end;~(*struct Example*)%
14.387 -\end{isamarkuptext}%
14.388 -\isamarkuptrue%
14.389 -%
14.390 -\endisatagquote
14.391 -{\isafoldquote}%
14.392 -%
14.393 -\isadelimquote
14.394 -%
14.395 -\endisadelimquote
14.396 -%
14.397 -\begin{isamarkuptext}%
14.398 -\noindent Note the parameters with trailing underscore (\verb|A_|),
14.399 - which are the dictionary parameters.%
14.400 -\end{isamarkuptext}%
14.401 -\isamarkuptrue%
14.402 -%
14.403 -\isamarkupsubsection{The preprocessor \label{sec:preproc}%
14.404 -}
14.405 -\isamarkuptrue%
14.406 -%
14.407 -\begin{isamarkuptext}%
14.408 -Before selected function theorems are turned into abstract
14.409 - code, a chain of definitional transformation steps is carried
14.410 - out: \emph{preprocessing}. In essence, the preprocessor
14.411 - consists of two components: a \emph{simpset} and \emph{function transformers}.
14.412 -
14.413 - The \emph{simpset} can apply the full generality of the
14.414 - Isabelle simplifier. Due to the interpretation of theorems as code
14.415 - equations, rewrites are applied to the right hand side and the
14.416 - arguments of the left hand side of an equation, but never to the
14.417 - constant heading the left hand side. An important special case are
14.418 - \emph{unfold theorems}, which may be declared and removed using
14.419 - the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
14.420 - attribute, respectively.
14.421 -
14.422 - Some common applications:%
14.423 -\end{isamarkuptext}%
14.424 -\isamarkuptrue%
14.425 -%
14.426 -\begin{itemize}
14.427 -%
14.428 -\begin{isamarkuptext}%
14.429 -\item replacing non-executable constructs by executable ones:%
14.430 -\end{isamarkuptext}%
14.431 -\isamarkuptrue%
14.432 -%
14.433 -\isadelimquote
14.434 -%
14.435 -\endisadelimquote
14.436 -%
14.437 -\isatagquote
14.438 -\isacommand{lemma}\isamarkupfalse%
14.439 -\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
14.440 -\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
14.441 -\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}%
14.442 -\endisatagquote
14.443 -{\isafoldquote}%
14.444 -%
14.445 -\isadelimquote
14.446 -%
14.447 -\endisadelimquote
14.448 -%
14.449 -\begin{isamarkuptext}%
14.450 -\item eliminating superfluous constants:%
14.451 -\end{isamarkuptext}%
14.452 -\isamarkuptrue%
14.453 -%
14.454 -\isadelimquote
14.455 -%
14.456 -\endisadelimquote
14.457 -%
14.458 -\isatagquote
14.459 -\isacommand{lemma}\isamarkupfalse%
14.460 -\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
14.461 -\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
14.462 -\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
14.463 -\endisatagquote
14.464 -{\isafoldquote}%
14.465 -%
14.466 -\isadelimquote
14.467 -%
14.468 -\endisadelimquote
14.469 -%
14.470 -\begin{isamarkuptext}%
14.471 -\item replacing executable but inconvenient constructs:%
14.472 -\end{isamarkuptext}%
14.473 -\isamarkuptrue%
14.474 -%
14.475 -\isadelimquote
14.476 -%
14.477 -\endisadelimquote
14.478 -%
14.479 -\isatagquote
14.480 -\isacommand{lemma}\isamarkupfalse%
14.481 -\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
14.482 -\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
14.483 -\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}%
14.484 -\endisatagquote
14.485 -{\isafoldquote}%
14.486 -%
14.487 -\isadelimquote
14.488 -%
14.489 -\endisadelimquote
14.490 -%
14.491 -\end{itemize}
14.492 -%
14.493 -\begin{isamarkuptext}%
14.494 -\noindent \emph{Function transformers} provide a very general interface,
14.495 - transforming a list of function theorems to another
14.496 - list of function theorems, provided that neither the heading
14.497 - constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc}
14.498 - pattern elimination implemented in
14.499 - theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this
14.500 - interface.
14.501 -
14.502 - \noindent The current setup of the preprocessor may be inspected using
14.503 - the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command.
14.504 - \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
14.505 - mechanism to inspect the impact of a preprocessor setup
14.506 - on code equations.
14.507 -
14.508 - \begin{warn}
14.509 -
14.510 - Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
14.511 - preprocessor of the ancient \isa{SML\ code\ generator}; in case
14.512 - this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
14.513 - \end{warn}%
14.514 -\end{isamarkuptext}%
14.515 -\isamarkuptrue%
14.516 -%
14.517 -\isamarkupsubsection{Datatypes \label{sec:datatypes}%
14.518 -}
14.519 -\isamarkuptrue%
14.520 -%
14.521 -\begin{isamarkuptext}%
14.522 -Conceptually, any datatype is spanned by a set of
14.523 - \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in
14.524 - \isa{{\isasymtau}}. The HOL datatype package by default registers any new
14.525 - datatype in the table of datatypes, which may be inspected using the
14.526 - \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
14.527 -
14.528 - In some cases, it is appropriate to alter or extend this table. As
14.529 - an example, we will develop an alternative representation of the
14.530 - queue example given in \secref{sec:intro}. The amortised
14.531 - representation is convenient for generating code but exposes its
14.532 - \qt{implementation} details, which may be cumbersome when proving
14.533 - theorems about it. Therefore, here is a simple, straightforward
14.534 - representation of queues:%
14.535 -\end{isamarkuptext}%
14.536 -\isamarkuptrue%
14.537 -%
14.538 -\isadelimquote
14.539 -%
14.540 -\endisadelimquote
14.541 -%
14.542 -\isatagquote
14.543 -\isacommand{datatype}\isamarkupfalse%
14.544 -\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
14.545 -\isanewline
14.546 -\isacommand{definition}\isamarkupfalse%
14.547 -\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
14.548 -\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
14.549 -\isanewline
14.550 -\isacommand{primrec}\isamarkupfalse%
14.551 -\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
14.552 -\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.553 -\isanewline
14.554 -\isacommand{fun}\isamarkupfalse%
14.555 -\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
14.556 -\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.557 -\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
14.558 -\endisatagquote
14.559 -{\isafoldquote}%
14.560 -%
14.561 -\isadelimquote
14.562 -%
14.563 -\endisadelimquote
14.564 -%
14.565 -\begin{isamarkuptext}%
14.566 -\noindent This we can use directly for proving; for executing,
14.567 - we provide an alternative characterisation:%
14.568 -\end{isamarkuptext}%
14.569 -\isamarkuptrue%
14.570 -%
14.571 -\isadelimquote
14.572 -%
14.573 -\endisadelimquote
14.574 -%
14.575 -\isatagquote
14.576 -\isacommand{definition}\isamarkupfalse%
14.577 -\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
14.578 -\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.579 -\isanewline
14.580 -\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
14.581 -\ AQueue%
14.582 -\endisatagquote
14.583 -{\isafoldquote}%
14.584 -%
14.585 -\isadelimquote
14.586 -%
14.587 -\endisadelimquote
14.588 -%
14.589 -\begin{isamarkuptext}%
14.590 -\noindent Here we define a \qt{constructor} \isa{AQueue} which
14.591 - is defined in terms of \isa{Queue} and interprets its arguments
14.592 - according to what the \emph{content} of an amortised queue is supposed
14.593 - to be. Equipped with this, we are able to prove the following equations
14.594 - for our primitive queue operations which \qt{implement} the simple
14.595 - queues in an amortised fashion:%
14.596 -\end{isamarkuptext}%
14.597 -\isamarkuptrue%
14.598 -%
14.599 -\isadelimquote
14.600 -%
14.601 -\endisadelimquote
14.602 -%
14.603 -\isatagquote
14.604 -\isacommand{lemma}\isamarkupfalse%
14.605 -\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
14.606 -\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
14.607 -\ \ \isacommand{unfolding}\isamarkupfalse%
14.608 -\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
14.609 -\ simp\isanewline
14.610 -\isanewline
14.611 -\isacommand{lemma}\isamarkupfalse%
14.612 -\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
14.613 -\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
14.614 -\ \ \isacommand{unfolding}\isamarkupfalse%
14.615 -\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
14.616 -\ simp\isanewline
14.617 -\isanewline
14.618 -\isacommand{lemma}\isamarkupfalse%
14.619 -\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
14.620 -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
14.621 -\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
14.622 -\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.623 -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.624 -\ \ \isacommand{unfolding}\isamarkupfalse%
14.625 -\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
14.626 -\ simp{\isacharunderscore}all%
14.627 -\endisatagquote
14.628 -{\isafoldquote}%
14.629 -%
14.630 -\isadelimquote
14.631 -%
14.632 -\endisadelimquote
14.633 -%
14.634 -\begin{isamarkuptext}%
14.635 -\noindent For completeness, we provide a substitute for the
14.636 - \isa{case} combinator on queues:%
14.637 -\end{isamarkuptext}%
14.638 -\isamarkuptrue%
14.639 -%
14.640 -\isadelimquote
14.641 -%
14.642 -\endisadelimquote
14.643 -%
14.644 -\isatagquote
14.645 -\isacommand{lemma}\isamarkupfalse%
14.646 -\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
14.647 -\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.648 -\ \ \isacommand{unfolding}\isamarkupfalse%
14.649 -\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
14.650 -\ simp%
14.651 -\endisatagquote
14.652 -{\isafoldquote}%
14.653 -%
14.654 -\isadelimquote
14.655 -%
14.656 -\endisadelimquote
14.657 -%
14.658 -\begin{isamarkuptext}%
14.659 -\noindent The resulting code looks as expected:%
14.660 -\end{isamarkuptext}%
14.661 -\isamarkuptrue%
14.662 -%
14.663 -\isadelimquote
14.664 -%
14.665 -\endisadelimquote
14.666 -%
14.667 -\isatagquote
14.668 -%
14.669 -\begin{isamarkuptext}%
14.670 -\isatypewriter%
14.671 -\noindent%
14.672 -\hspace*{0pt}structure Example :~sig\\
14.673 -\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
14.674 -\hspace*{0pt} ~val rev :~'a list -> 'a list\\
14.675 -\hspace*{0pt} ~val null :~'a list -> bool\\
14.676 -\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
14.677 -\hspace*{0pt} ~val empty :~'a queue\\
14.678 -\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
14.679 -\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
14.680 -\hspace*{0pt}end = struct\\
14.681 -\hspace*{0pt}\\
14.682 -\hspace*{0pt}fun foldl f a [] = a\\
14.683 -\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
14.684 -\hspace*{0pt}\\
14.685 -\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
14.686 -\hspace*{0pt}\\
14.687 -\hspace*{0pt}fun null [] = true\\
14.688 -\hspace*{0pt} ~| null (x ::~xs) = false;\\
14.689 -\hspace*{0pt}\\
14.690 -\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
14.691 -\hspace*{0pt}\\
14.692 -\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
14.693 -\hspace*{0pt}\\
14.694 -\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
14.695 -\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
14.696 -\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
14.697 -\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
14.698 -\hspace*{0pt}\\
14.699 -\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
14.700 -\hspace*{0pt}\\
14.701 -\hspace*{0pt}end;~(*struct Example*)%
14.702 -\end{isamarkuptext}%
14.703 -\isamarkuptrue%
14.704 -%
14.705 -\endisatagquote
14.706 -{\isafoldquote}%
14.707 -%
14.708 -\isadelimquote
14.709 -%
14.710 -\endisadelimquote
14.711 -%
14.712 -\begin{isamarkuptext}%
14.713 -\noindent From this example, it can be glimpsed that using own
14.714 - constructor sets is a little delicate since it changes the set of
14.715 - valid patterns for values of that type. Without going into much
14.716 - detail, here some practical hints:
14.717 -
14.718 - \begin{itemize}
14.719 -
14.720 - \item When changing the constructor set for datatypes, take care
14.721 - to provide alternative equations for the \isa{case} combinator.
14.722 -
14.723 - \item Values in the target language need not to be normalised --
14.724 - different values in the target language may represent the same
14.725 - value in the logic.
14.726 -
14.727 - \item Usually, a good methodology to deal with the subtleties of
14.728 - pattern matching is to see the type as an abstract type: provide
14.729 - a set of operations which operate on the concrete representation
14.730 - of the type, and derive further operations by combinations of
14.731 - these primitive ones, without relying on a particular
14.732 - representation.
14.733 -
14.734 - \end{itemize}%
14.735 -\end{isamarkuptext}%
14.736 -\isamarkuptrue%
14.737 -%
14.738 -\isamarkupsubsection{Equality%
14.739 -}
14.740 -\isamarkuptrue%
14.741 -%
14.742 -\begin{isamarkuptext}%
14.743 -Surely you have already noticed how equality is treated
14.744 - by the code generator:%
14.745 -\end{isamarkuptext}%
14.746 -\isamarkuptrue%
14.747 -%
14.748 -\isadelimquote
14.749 -%
14.750 -\endisadelimquote
14.751 -%
14.752 -\isatagquote
14.753 -\isacommand{primrec}\isamarkupfalse%
14.754 -\ 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
14.755 -\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
14.756 -\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
14.757 -\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
14.758 -\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
14.759 -\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
14.760 -\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
14.761 -\endisatagquote
14.762 -{\isafoldquote}%
14.763 -%
14.764 -\isadelimquote
14.765 -%
14.766 -\endisadelimquote
14.767 -%
14.768 -\begin{isamarkuptext}%
14.769 -\noindent During preprocessing, the membership test is rewritten,
14.770 - resulting in \isa{List{\isachardot}member}, which itself
14.771 - performs an explicit equality check.%
14.772 -\end{isamarkuptext}%
14.773 -\isamarkuptrue%
14.774 -%
14.775 -\isadelimquote
14.776 -%
14.777 -\endisadelimquote
14.778 -%
14.779 -\isatagquote
14.780 -%
14.781 -\begin{isamarkuptext}%
14.782 -\isatypewriter%
14.783 -\noindent%
14.784 -\hspace*{0pt}structure Example :~sig\\
14.785 -\hspace*{0pt} ~type 'a eq\\
14.786 -\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
14.787 -\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
14.788 -\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\
14.789 -\hspace*{0pt} ~val collect{\char95}duplicates :\\
14.790 -\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
14.791 -\hspace*{0pt}end = struct\\
14.792 -\hspace*{0pt}\\
14.793 -\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
14.794 -\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\
14.795 -\hspace*{0pt}\\
14.796 -\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
14.797 -\hspace*{0pt}\\
14.798 -\hspace*{0pt}fun member A{\char95}~[] y = false\\
14.799 -\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\
14.800 -\hspace*{0pt}\\
14.801 -\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
14.802 -\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
14.803 -\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
14.804 -\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
14.805 -\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
14.806 -\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
14.807 -\hspace*{0pt}\\
14.808 -\hspace*{0pt}end;~(*struct Example*)%
14.809 -\end{isamarkuptext}%
14.810 -\isamarkuptrue%
14.811 -%
14.812 -\endisatagquote
14.813 -{\isafoldquote}%
14.814 -%
14.815 -\isadelimquote
14.816 -%
14.817 -\endisadelimquote
14.818 -%
14.819 -\begin{isamarkuptext}%
14.820 -\noindent Obviously, polymorphic equality is implemented the Haskell
14.821 - way using a type class. How is this achieved? HOL introduces
14.822 - an explicit class \isa{eq} with a corresponding operation
14.823 - \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.
14.824 - The preprocessing framework does the rest by propagating the
14.825 - \isa{eq} constraints through all dependent code equations.
14.826 - For datatypes, instances of \isa{eq} are implicitly derived
14.827 - when possible. For other types, you may instantiate \isa{eq}
14.828 - manually like any other type class.%
14.829 -\end{isamarkuptext}%
14.830 -\isamarkuptrue%
14.831 -%
14.832 -\isamarkupsubsection{Explicit partiality%
14.833 -}
14.834 -\isamarkuptrue%
14.835 -%
14.836 -\begin{isamarkuptext}%
14.837 -Partiality usually enters the game by partial patterns, as
14.838 - in the following example, again for amortised queues:%
14.839 -\end{isamarkuptext}%
14.840 -\isamarkuptrue%
14.841 -%
14.842 -\isadelimquote
14.843 -%
14.844 -\endisadelimquote
14.845 -%
14.846 -\isatagquote
14.847 -\isacommand{definition}\isamarkupfalse%
14.848 -\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
14.849 -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline
14.850 -\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.851 -\isanewline
14.852 -\isacommand{lemma}\isamarkupfalse%
14.853 -\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
14.854 -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.855 -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
14.856 -\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.857 -\ \ \isacommand{by}\isamarkupfalse%
14.858 -\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
14.859 -\endisatagquote
14.860 -{\isafoldquote}%
14.861 -%
14.862 -\isadelimquote
14.863 -%
14.864 -\endisadelimquote
14.865 -%
14.866 -\begin{isamarkuptext}%
14.867 -\noindent In the corresponding code, there is no equation
14.868 - for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
14.869 -\end{isamarkuptext}%
14.870 -\isamarkuptrue%
14.871 -%
14.872 -\isadelimquote
14.873 -%
14.874 -\endisadelimquote
14.875 -%
14.876 -\isatagquote
14.877 -%
14.878 -\begin{isamarkuptext}%
14.879 -\isatypewriter%
14.880 -\noindent%
14.881 -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
14.882 -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
14.883 -\hspace*{0pt} ~let {\char123}\\
14.884 -\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
14.885 -\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
14.886 -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
14.887 -\end{isamarkuptext}%
14.888 -\isamarkuptrue%
14.889 -%
14.890 -\endisatagquote
14.891 -{\isafoldquote}%
14.892 -%
14.893 -\isadelimquote
14.894 -%
14.895 -\endisadelimquote
14.896 -%
14.897 -\begin{isamarkuptext}%
14.898 -\noindent In some cases it is desirable to have this
14.899 - pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
14.900 -\end{isamarkuptext}%
14.901 -\isamarkuptrue%
14.902 -%
14.903 -\isadelimquote
14.904 -%
14.905 -\endisadelimquote
14.906 -%
14.907 -\isatagquote
14.908 -\isacommand{axiomatization}\isamarkupfalse%
14.909 -\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
14.910 -\isanewline
14.911 -\isacommand{definition}\isamarkupfalse%
14.912 -\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
14.913 -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.914 -\isanewline
14.915 -\isacommand{lemma}\isamarkupfalse%
14.916 -\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
14.917 -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
14.918 -\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.919 -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
14.920 -\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
14.921 -\ \ \isacommand{by}\isamarkupfalse%
14.922 -\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
14.923 -\endisatagquote
14.924 -{\isafoldquote}%
14.925 -%
14.926 -\isadelimquote
14.927 -%
14.928 -\endisadelimquote
14.929 -%
14.930 -\begin{isamarkuptext}%
14.931 -Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs.
14.932 -
14.933 - Normally, if constants without any code equations occur in a
14.934 - program, the code generator complains (since in most cases this is
14.935 - indeed an error). But such constants can also be thought
14.936 - of as function definitions which always fail,
14.937 - since there is never a successful pattern match on the left hand
14.938 - side. In order to categorise a constant into that category
14.939 - explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
14.940 -\end{isamarkuptext}%
14.941 -\isamarkuptrue%
14.942 -%
14.943 -\isadelimquote
14.944 -%
14.945 -\endisadelimquote
14.946 -%
14.947 -\isatagquote
14.948 -\isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
14.949 -\ empty{\isacharunderscore}queue%
14.950 -\endisatagquote
14.951 -{\isafoldquote}%
14.952 -%
14.953 -\isadelimquote
14.954 -%
14.955 -\endisadelimquote
14.956 -%
14.957 -\begin{isamarkuptext}%
14.958 -\noindent Then the code generator will just insert an error or
14.959 - exception at the appropriate position:%
14.960 -\end{isamarkuptext}%
14.961 -\isamarkuptrue%
14.962 -%
14.963 -\isadelimquote
14.964 -%
14.965 -\endisadelimquote
14.966 -%
14.967 -\isatagquote
14.968 -%
14.969 -\begin{isamarkuptext}%
14.970 -\isatypewriter%
14.971 -\noindent%
14.972 -\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
14.973 -\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
14.974 -\hspace*{0pt}\\
14.975 -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
14.976 -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
14.977 -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
14.978 -\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
14.979 -\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
14.980 -\end{isamarkuptext}%
14.981 -\isamarkuptrue%
14.982 -%
14.983 -\endisatagquote
14.984 -{\isafoldquote}%
14.985 -%
14.986 -\isadelimquote
14.987 -%
14.988 -\endisadelimquote
14.989 -%
14.990 -\begin{isamarkuptext}%
14.991 -\noindent This feature however is rarely needed in practice.
14.992 - Note also that the \isa{HOL} default setup already declares
14.993 - \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
14.994 - likely to be used in such situations.%
14.995 -\end{isamarkuptext}%
14.996 -\isamarkuptrue%
14.997 -%
14.998 -\isadelimtheory
14.999 -%
14.1000 -\endisadelimtheory
14.1001 -%
14.1002 -\isatagtheory
14.1003 -\isacommand{end}\isamarkupfalse%
14.1004 -%
14.1005 -\endisatagtheory
14.1006 -{\isafoldtheory}%
14.1007 -%
14.1008 -\isadelimtheory
14.1009 -%
14.1010 -\endisadelimtheory
14.1011 -\isanewline
14.1012 -\end{isabellebody}%
14.1013 -%%% Local Variables:
14.1014 -%%% mode: latex
14.1015 -%%% TeX-master: "root"
14.1016 -%%% End:
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Fri Aug 13 14:41:27 2010 +0200
15.3 @@ -0,0 +1,43 @@
15.4 +%
15.5 +\begin{isabellebody}%
15.6 +\def\isabellecontext{Refinement}%
15.7 +%
15.8 +\isadelimtheory
15.9 +%
15.10 +\endisadelimtheory
15.11 +%
15.12 +\isatagtheory
15.13 +\isacommand{theory}\isamarkupfalse%
15.14 +\ Refinement\isanewline
15.15 +\isakeyword{imports}\ Setup\isanewline
15.16 +\isakeyword{begin}%
15.17 +\endisatagtheory
15.18 +{\isafoldtheory}%
15.19 +%
15.20 +\isadelimtheory
15.21 +%
15.22 +\endisadelimtheory
15.23 +%
15.24 +\isamarkupsection{Program and datatype refinement \label{sec:refinement}%
15.25 +}
15.26 +\isamarkuptrue%
15.27 +%
15.28 +\isadelimtheory
15.29 +%
15.30 +\endisadelimtheory
15.31 +%
15.32 +\isatagtheory
15.33 +\isacommand{end}\isamarkupfalse%
15.34 +%
15.35 +\endisatagtheory
15.36 +{\isafoldtheory}%
15.37 +%
15.38 +\isadelimtheory
15.39 +%
15.40 +\endisadelimtheory
15.41 +\isanewline
15.42 +\end{isabellebody}%
15.43 +%%% Local Variables:
15.44 +%%% mode: latex
15.45 +%%% TeX-master: "root"
15.46 +%%% End:
16.1 --- a/doc-src/Codegen/codegen.tex Fri Aug 13 12:15:25 2010 +0200
16.2 +++ b/doc-src/Codegen/codegen.tex Fri Aug 13 14:41:27 2010 +0200
16.3 @@ -20,9 +20,9 @@
16.4 \maketitle
16.5
16.6 \begin{abstract}
16.7 - \noindent This tutorial gives an introduction to a generic code generator framework in Isabelle
16.8 - for generating executable code in functional programming languages from logical
16.9 - specifications in Isabelle/HOL.
16.10 + \noindent This tutorial introduces the code generator facilities of Isabelle/HOL.
16.11 + They empower the user to turn HOL specifications into corresponding executable
16.12 + programs in the languages SML, OCaml and Haskell.
16.13 \end{abstract}
16.14
16.15 \thispagestyle{empty}\clearpage
16.16 @@ -31,11 +31,11 @@
16.17 \clearfirst
16.18
16.19 \input{Thy/document/Introduction.tex}
16.20 -\input{Thy/document/Program.tex}
16.21 +\input{Thy/document/Foundations.tex}
16.22 +\input{Thy/document/Refinement.tex}
16.23 \input{Thy/document/Inductive_Predicate.tex}
16.24 \input{Thy/document/Adaptation.tex}
16.25 \input{Thy/document/Further.tex}
16.26 -\input{Thy/document/ML.tex}
16.27
16.28 \begingroup
16.29 \bibliographystyle{plain} \small\raggedright\frenchspacing
17.1 --- a/doc-src/Codegen/style.sty Fri Aug 13 12:15:25 2010 +0200
17.2 +++ b/doc-src/Codegen/style.sty Fri Aug 13 14:41:27 2010 +0200
17.3 @@ -15,6 +15,7 @@
17.4
17.5 %% typographic conventions
17.6 \newcommand{\qt}[1]{``{#1}''}
17.7 +\newcommand{\ditem}[1]{\item[\isastyletext #1]}
17.8
17.9 %% verbatim text
17.10 \newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}