--- a/doc-src/Codegen/IsaMakefile Mon Aug 16 10:05:00 2010 +0100
+++ b/doc-src/Codegen/IsaMakefile Mon Aug 16 12:11:01 2010 +0200
@@ -24,7 +24,7 @@
Thy: $(THY)
$(THY): Thy/ROOT.ML Thy/*.thy ../antiquote_setup.ML ../more_antiquote.ML
- @$(USEDIR) HOL Thy
+ @$(USEDIR) -m no_brackets -m iff HOL Thy
@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
Thy/document/pdfsetup.sty Thy/document/session.tex
--- a/doc-src/Codegen/Thy/Foundations.thy Mon Aug 16 10:05:00 2010 +0100
+++ b/doc-src/Codegen/Thy/Foundations.thy Mon Aug 16 12:11:01 2010 +0200
@@ -2,164 +2,83 @@
imports Introduction
begin
-section {* Code generation foundations \label{sec:program} *}
-
-subsection {* The @{text "Isabelle/HOL"} default setup *}
-
-text {*
- We have already seen how by default equations stemming from
- @{command definition}, @{command primrec} and @{command fun}
- statements are used for code generation. This default behaviour
- can be changed, e.g.\ by providing different code equations.
- The customisations shown in this section are \emph{safe}
- as regards correctness: all programs that can be generated are partially
- correct.
-*}
-
-subsection {* Selecting code equations *}
-
-text {*
- Coming back to our introductory example, we
- could provide an alternative code equations for @{const dequeue}
- explicitly:
-*}
-
-lemma %quote [code]:
- "dequeue (AQueue xs []) =
- (if xs = [] then (None, AQueue [] [])
- else dequeue (AQueue [] (rev xs)))"
- "dequeue (AQueue xs (y # ys)) =
- (Some y, AQueue xs ys)"
- by (cases xs, simp_all) (cases "rev xs", simp_all)
+section {* Code generation foundations \label{sec:foundations} *}
-text {*
- \noindent The annotation @{text "[code]"} is an @{text Isar}
- @{text attribute} which states that the given theorems should be
- considered as code equations for a @{text fun} statement --
- the corresponding constant is determined syntactically. The resulting code:
-*}
-
-text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
-
-text {*
- \noindent You may note that the equality test @{term "xs = []"} has been
- replaced by the predicate @{term "null xs"}. This is due to the default
- setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
-
- Changing the default constructor set of datatypes is also
- possible. See \secref{sec:datatypes} for an example.
-
- As told in \secref{sec:concept}, code generation is based
- on a structured collection of code theorems.
- This collection
- may be inspected using the @{command code_thms} command:
-*}
-
-code_thms %quote dequeue
-
-text {*
- \noindent prints a table with \emph{all} code equations
- for @{const dequeue}, including
- \emph{all} code equations those equations depend
- on recursively.
-
- Similarly, the @{command code_deps} command shows a graph
- visualising dependencies between code equations.
-*}
-
-subsection {* @{text class} and @{text instantiation} *}
+subsection {* Code generator architecture \label{sec:architecture} *}
text {*
- Concerning type classes and code generation, let us examine an example
- from abstract algebra:
+
+ The code generator is actually a framework consisting of different
+ components which can be customised individually.
+
+ Conceptually all components operate on Isabelle's logic framework
+ @{theory Pure}. Practically, the object logic @{theory HOL}
+ provides the necessary facilities to make use of the code generator,
+ mainly since it is an extension of @{theory Pure}.
+
+ The constellation of the different components is visualized in the
+ following picture.
+
+ \begin{figure}[h]
+ \includegraphics{architecture}
+ \caption{Code generator architecture}
+ \label{fig:arch}
+ \end{figure}
+
+ \noindent Central to code generation is the notion of \emph{code
+ equations}. A code equation as a first approximation is a theorem
+ of the form @{text "f t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n \<equiv> t"} (an equation headed by a
+ constant @{text f} with arguments @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right
+ hand side @{text t}).
+
+ \begin{itemize}
+
+ \item Starting point of code generation is a collection of (raw)
+ code equations in a theory. It is not relevant where they stem
+ from, but typically they were either produced by specification
+ tools or proved explicitly by the user.
+
+ \item These raw code equations can be subjected to theorem
+ transformations. This \qn{preprocessor} (see
+ \secref{sec:preproc}) can apply the full expressiveness of
+ ML-based theorem transformations to code generation. The result
+ of preprocessing is a structured collection of code equations.
+
+ \item These code equations are \qn{translated} to a program in an
+ abstract intermediate language. Think of it as a kind of
+ \qt{Mini-Haskell} with four \qn{statements}: @{text data} (for
+ datatypes), @{text fun} (stemming from code equations), also
+ @{text class} and @{text inst} (for type classes).
+
+ \item Finally, the abstract program is \qn{serialised} into
+ concrete source code of a target language. This step only
+ produces concrete syntax but does not change the program in
+ essence; all conceptual transformations occur in the translation
+ step.
+
+ \end{itemize}
+
+ \noindent From these steps, only the last two are carried out
+ outside the logic; by keeping this layer as thin as possible, the
+ amount of code to trust is kept to a minimum.
*}
-class %quote semigroup =
- fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
- assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
-
-class %quote monoid = semigroup +
- fixes neutral :: 'a ("\<one>")
- assumes neutl: "\<one> \<otimes> x = x"
- and neutr: "x \<otimes> \<one> = x"
-
-instantiation %quote nat :: monoid
-begin
-
-primrec %quote mult_nat where
- "0 \<otimes> n = (0\<Colon>nat)"
- | "Suc m \<otimes> n = n + m \<otimes> n"
-
-definition %quote neutral_nat where
- "\<one> = Suc 0"
-
-lemma %quote add_mult_distrib:
- fixes n m q :: nat
- shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
- by (induct n) simp_all
-
-instance %quote proof
- fix m n q :: nat
- show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
- by (induct m) (simp_all add: add_mult_distrib)
- show "\<one> \<otimes> n = n"
- by (simp add: neutral_nat_def)
- show "m \<otimes> \<one> = m"
- by (induct m) (simp_all add: neutral_nat_def)
-qed
-
-end %quote
-
-text {*
- \noindent We define the natural operation of the natural numbers
- on monoids:
-*}
-
-primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
- "pow 0 a = \<one>"
- | "pow (Suc n) a = a \<otimes> pow n a"
-
-text {*
- \noindent This we use to define the discrete exponentiation function:
-*}
-
-definition %quote bexp :: "nat \<Rightarrow> nat" where
- "bexp n = pow n (Suc (Suc 0))"
-
-text {*
- \noindent The corresponding code in Haskell uses that language's native classes:
-*}
-
-text %quote {*@{code_stmts bexp (Haskell)}*}
-
-text {*
- \noindent This is a convenient place to show how explicit dictionary construction
- manifests in generated code (here, the same example in @{text SML})
- \cite{Haftmann-Nipkow:2010:code}:
-*}
-
-text %quote {*@{code_stmts bexp (SML)}*}
-
-text {*
- \noindent Note the parameters with trailing underscore (@{verbatim "A_"}),
- which are the dictionary parameters.
-*}
subsection {* The preprocessor \label{sec:preproc} *}
text {*
- Before selected function theorems are turned into abstract
- code, a chain of definitional transformation steps is carried
- out: \emph{preprocessing}. In essence, the preprocessor
- consists of two components: a \emph{simpset} and \emph{function transformers}.
+ Before selected function theorems are turned into abstract code, a
+ chain of definitional transformation steps is carried out:
+ \emph{preprocessing}. The preprocessor consists of two
+ components: a \emph{simpset} and \emph{function transformers}.
- The \emph{simpset} can apply the full generality of the
- Isabelle simplifier. Due to the interpretation of theorems as code
+ The \emph{simpset} can apply the full generality of the Isabelle
+ simplifier. Due to the interpretation of theorems as code
equations, rewrites are applied to the right hand side and the
arguments of the left hand side of an equation, but never to the
constant heading the left hand side. An important special case are
- \emph{unfold theorems}, which may be declared and removed using
- the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
+ \emph{unfold theorems}, which may be declared and removed using the
+ @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
attribute, respectively.
Some common applications:
@@ -177,189 +96,141 @@
"x \<in> set xs \<longleftrightarrow> List.member xs x" by (fact in_set_member)
text {*
- \item eliminating superfluous constants:
-*}
-
-lemma %quote [code_unfold]:
- "1 = Suc 0" by (fact One_nat_def)
-
-text {*
\item replacing executable but inconvenient constructs:
*}
lemma %quote [code_unfold]:
"xs = [] \<longleftrightarrow> List.null xs" by (fact eq_Nil_null)
+text {*
+ \item eliminating disturbing expressions:
+*}
+
+lemma %quote [code_unfold]:
+ "1 = Suc 0" by (fact One_nat_def)
+
text_raw {*
\end{itemize}
*}
text {*
- \noindent \emph{Function transformers} provide a very general interface,
- transforming a list of function theorems to another
- list of function theorems, provided that neither the heading
- constant nor its type change. The @{term "0\<Colon>nat"} / @{const Suc}
- pattern elimination implemented in
- theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this
- interface.
+ \noindent \emph{Function transformers} provide a very general
+ interface, transforming a list of function theorems to another list
+ of function theorems, provided that neither the heading constant nor
+ its type change. The @{term "0\<Colon>nat"} / @{const Suc} pattern
+ elimination implemented in theory @{theory Efficient_Nat} (see
+ \secref{eff_nat}) uses this interface.
- \noindent The current setup of the preprocessor may be inspected using
- the @{command print_codeproc} command.
- @{command code_thms} provides a convenient
- mechanism to inspect the impact of a preprocessor setup
- on code equations.
+ \noindent The current setup of the preprocessor may be inspected
+ using the @{command print_codeproc} command. @{command code_thms}
+ (see \secref{sec:equations}) provides a convenient mechanism to
+ inspect the impact of a preprocessor setup on code equations.
\begin{warn}
-
Attribute @{attribute code_unfold} also applies to the
preprocessor of the ancient @{text "SML code generator"}; in case
this is not what you intend, use @{attribute code_inline} instead.
\end{warn}
*}
-subsection {* Datatypes \label{sec:datatypes} *}
+
+subsection {* Understanding code equations \label{sec:equations} *}
text {*
- Conceptually, any datatype is spanned by a set of
- \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
- "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
- @{text "\<tau>"}. The HOL datatype package by default registers any new
- datatype in the table of datatypes, which may be inspected using the
- @{command print_codesetup} command.
+ As told in \secref{sec:principle}, the notion of code equations is
+ vital to code generation. Indeed most problems which occur in
+ practice can be resolved by an inspection of the underlying code
+ equations.
- In some cases, it is appropriate to alter or extend this table. As
- an example, we will develop an alternative representation of the
- queue example given in \secref{sec:intro}. The amortised
- representation is convenient for generating code but exposes its
- \qt{implementation} details, which may be cumbersome when proving
- theorems about it. Therefore, here is a simple, straightforward
- representation of queues:
+ It is possible to exchange the default code equations for constants
+ by explicitly proving alternative ones:
*}
-datatype %quote 'a queue = Queue "'a list"
-
-definition %quote empty :: "'a queue" where
- "empty = Queue []"
-
-primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
- "enqueue x (Queue xs) = Queue (xs @ [x])"
-
-fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
- "dequeue (Queue []) = (None, Queue [])"
- | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
+lemma %quote [code]:
+ "dequeue (AQueue xs []) =
+ (if xs = [] then (None, AQueue [] [])
+ else dequeue (AQueue [] (rev xs)))"
+ "dequeue (AQueue xs (y # ys)) =
+ (Some y, AQueue xs ys)"
+ by (cases xs, simp_all) (cases "rev xs", simp_all)
text {*
- \noindent This we can use directly for proving; for executing,
- we provide an alternative characterisation:
-*}
-
-definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
- "AQueue xs ys = Queue (ys @ rev xs)"
-
-code_datatype %quote AQueue
-
-text {*
- \noindent Here we define a \qt{constructor} @{const "AQueue"} which
- is defined in terms of @{text "Queue"} and interprets its arguments
- according to what the \emph{content} of an amortised queue is supposed
- to be. Equipped with this, we are able to prove the following equations
- for our primitive queue operations which \qt{implement} the simple
- queues in an amortised fashion:
+ \noindent The annotation @{text "[code]"} is an @{text attribute}
+ which states that the given theorems should be considered as code
+ equations for a @{text fun} statement -- the corresponding constant
+ is determined syntactically. The resulting code:
*}
-lemma %quote empty_AQueue [code]:
- "empty = AQueue [] []"
- unfolding AQueue_def empty_def by simp
-
-lemma %quote enqueue_AQueue [code]:
- "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
- unfolding AQueue_def by simp
-
-lemma %quote dequeue_AQueue [code]:
- "dequeue (AQueue xs []) =
- (if xs = [] then (None, AQueue [] [])
- else dequeue (AQueue [] (rev xs)))"
- "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
- unfolding AQueue_def by simp_all
-
-text {*
- \noindent For completeness, we provide a substitute for the
- @{text case} combinator on queues:
-*}
-
-lemma %quote queue_case_AQueue [code]:
- "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
- unfolding AQueue_def by simp
+text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
text {*
- \noindent The resulting code looks as expected:
+ \noindent You may note that the equality test @{term "xs = []"} has
+ been replaced by the predicate @{term "List.null xs"}. This is due
+ to the default setup of the \qn{preprocessor}.
+
+ This possibility to select arbitrary code equations is the key
+ technique for program and datatype refinement (see
+ \secref{sec:refinement}.
+
+ Due to the preprocessor, there is the distinction of raw code
+ equations (before preprocessing) and code equations (after
+ preprocessing).
+
+ The first can be listed (among other data) using the @{command
+ print_codesetup} command (later on in \secref{sec:refinement}
+ it will be shown how these code equations can be changed).
+
+ The code equations after preprocessing are already are blueprint of
+ the generated program and can be inspected using the @{command
+ code_thms} command:
*}
-text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
+code_thms %quote dequeue
text {*
- \noindent From this example, it can be glimpsed that using own
- constructor sets is a little delicate since it changes the set of
- valid patterns for values of that type. Without going into much
- detail, here some practical hints:
-
- \begin{itemize}
-
- \item When changing the constructor set for datatypes, take care
- to provide alternative equations for the @{text case} combinator.
-
- \item Values in the target language need not to be normalised --
- different values in the target language may represent the same
- value in the logic.
-
- \item Usually, a good methodology to deal with the subtleties of
- pattern matching is to see the type as an abstract type: provide
- a set of operations which operate on the concrete representation
- of the type, and derive further operations by combinations of
- these primitive ones, without relying on a particular
- representation.
-
- \end{itemize}
+ \noindent This prints a table with the code equations for @{const
+ dequeue}, including \emph{all} code equations those equations depend
+ on recursively. These dependencies themselves can be visualized using
+ the @{command code_deps} command.
*}
subsection {* Equality *}
text {*
- Surely you have already noticed how equality is treated
- by the code generator:
+ Implementation of equality deserves some attention. Here an example
+ function involving polymorphic equality:
*}
primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"collect_duplicates xs ys [] = xs"
- | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
- then if z \<in> set ys
- then collect_duplicates xs ys zs
- else collect_duplicates xs (z#ys) zs
- else collect_duplicates (z#xs) (z#ys) zs)"
+| "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
+ then if z \<in> set ys
+ then collect_duplicates xs ys zs
+ else collect_duplicates xs (z#ys) zs
+ else collect_duplicates (z#xs) (z#ys) zs)"
text {*
\noindent During preprocessing, the membership test is rewritten,
- resulting in @{const List.member}, which itself
- performs an explicit equality check.
+ resulting in @{const List.member}, which itself performs an explicit
+ equality check, as can be seen in the corresponding @{text SML} code:
*}
text %quote {*@{code_stmts collect_duplicates (SML)}*}
text {*
\noindent Obviously, polymorphic equality is implemented the Haskell
- way using a type class. How is this achieved? HOL introduces
- an explicit class @{class eq} with a corresponding operation
- @{const eq_class.eq} such that @{thm eq [no_vars]}.
- The preprocessing framework does the rest by propagating the
- @{class eq} constraints through all dependent code equations.
- For datatypes, instances of @{class eq} are implicitly derived
- when possible. For other types, you may instantiate @{text eq}
- manually like any other type class.
+ way using a type class. How is this achieved? HOL introduces an
+ explicit class @{class eq} with a corresponding operation @{const
+ eq_class.eq} such that @{thm eq [no_vars]}. The preprocessing
+ framework does the rest by propagating the @{class eq} constraints
+ through all dependent code equations. For datatypes, instances of
+ @{class eq} are implicitly derived when possible. For other types,
+ you may instantiate @{text eq} manually like any other type class.
*}
-subsection {* Explicit partiality *}
+subsection {* Explicit partiality \label{sec:partiality} *}
text {*
Partiality usually enters the game by partial patterns, as
@@ -374,7 +245,7 @@
"strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
"strict_dequeue (AQueue xs []) =
(case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
- by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits)
+ by (simp_all add: strict_dequeue_def) (cases xs, simp_all split: list.split)
text {*
\noindent In the corresponding code, there is no equation
@@ -398,7 +269,7 @@
else strict_dequeue' (AQueue [] (rev xs)))"
"strict_dequeue' (AQueue xs (y # ys)) =
(y, AQueue xs ys)"
- by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits)
+ by (simp_all add: strict_dequeue'_def split: list.splits)
text {*
Observe that on the right hand side of the definition of @{const
@@ -423,10 +294,53 @@
text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
text {*
- \noindent This feature however is rarely needed in practice.
- Note also that the @{text HOL} default setup already declares
- @{const undefined} as @{command "code_abort"}, which is most
- likely to be used in such situations.
+ \noindent This feature however is rarely needed in practice. Note
+ also that the HOL default setup already declares @{const undefined}
+ as @{command "code_abort"}, which is most likely to be used in such
+ situations.
+*}
+
+
+subsection {* If something goes utterly wrong \label{sec:utterly_wrong} *}
+
+text {*
+ Under certain circumstances, the code generator fails to produce
+ code entirely. To debug these, the following hints may prove
+ helpful:
+
+ \begin{description}
+
+ \ditem{\emph{Check with a different target language}.} Sometimes
+ the situation gets more clear if you switch to another target
+ language; the code generated there might give some hints what
+ prevents the code generator to produce code for the desired
+ language.
+
+ \ditem{\emph{Inspect code equations}.} Code equations are the central
+ carrier of code generation. Most problems occuring while generation
+ code can be traced to single equations which are printed as part of
+ the error message. A closer inspection of those may offer the key
+ for solving issues (cf.~\secref{sec:equations}).
+
+ \ditem{\emph{Inspect preprocessor setup}.} The preprocessor might
+ transform code equations unexpectedly; to understand an
+ inspection of its setup is necessary (cf.~\secref{sec:preproc}).
+
+ \ditem{\emph{Generate exceptions}.} If the code generator
+ complains about missing code equations, in can be helpful to
+ implement the offending constants as exceptions
+ (cf.~\secref{sec:partiality}); this allows at least for a formal
+ generation of code, whose inspection may then give clues what is
+ wrong.
+
+ \ditem{\emph{Remove offending code equations}.} If code
+ generation is prevented by just a single equation, this can be
+ removed (cf.~\secref{sec:equations}) to allow formal code
+ generation, whose result in turn can be used to trace the
+ problem. The most prominent case here are mismatches in type
+ class signatures (\qt{wellsortedness error}).
+
+ \end{description}
*}
end
--- a/doc-src/Codegen/Thy/Further.thy Mon Aug 16 10:05:00 2010 +0100
+++ b/doc-src/Codegen/Thy/Further.thy Mon Aug 16 12:11:01 2010 +0200
@@ -4,12 +4,34 @@
section {* Further issues \label{sec:further} *}
-subsection {* Further reading *}
+subsection {* Modules namespace *}
text {*
- To dive deeper into the issue of code generation, you should visit
- the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}, which
- contains exhaustive syntax diagrams.
+ When invoking the @{command export_code} command it is possible to leave
+ out the @{keyword "module_name"} part; then code is distributed over
+ different modules, where the module name space roughly is induced
+ by the Isabelle theory name space.
+
+ Then sometimes the awkward situation occurs that dependencies between
+ definitions introduce cyclic dependencies between modules, which in the
+ @{text Haskell} world leaves you to the mercy of the @{text Haskell} implementation
+ you are using, while for @{text SML}/@{text OCaml} code generation is not possible.
+
+ A solution is to declare module names explicitly.
+ Let use assume the three cyclically dependent
+ modules are named \emph{A}, \emph{B} and \emph{C}.
+ Then, by stating
+*}
+
+code_modulename %quote SML
+ A ABC
+ B ABC
+ C ABC
+
+text {*\noindent
+ we explicitly map all those modules on \emph{ABC},
+ resulting in an ad-hoc merge of this three modules
+ at serialisation time.
*}
subsection {* Locales and interpretation *}
@@ -93,35 +115,16 @@
text %quote {*@{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}*}
-subsection {* Modules *}
+subsection {* Imperative data structures *}
text {*
- When invoking the @{command export_code} command it is possible to leave
- out the @{keyword "module_name"} part; then code is distributed over
- different modules, where the module name space roughly is induced
- by the @{text Isabelle} theory name space.
-
- Then sometimes the awkward situation occurs that dependencies between
- definitions introduce cyclic dependencies between modules, which in the
- @{text Haskell} world leaves you to the mercy of the @{text Haskell} implementation
- you are using, while for @{text SML}/@{text OCaml} code generation is not possible.
-
- A solution is to declare module names explicitly.
- Let use assume the three cyclically dependent
- modules are named \emph{A}, \emph{B} and \emph{C}.
- Then, by stating
+ If you consider imperative data structures as inevitable for a
+ specific application, you should consider \emph{Imperative
+ Functional Programming with Isabelle/HOL}
+ \cite{bulwahn-et-al:2008:imperative}; the framework described there
+ is available in session @{theory Imperative_HOL}.
*}
-code_modulename %quote SML
- A ABC
- B ABC
- C ABC
-
-text {*\noindent
- we explicitly map all those modules on \emph{ABC},
- resulting in an ad-hoc merge of this three modules
- at serialisation time.
-*}
subsection {* Evaluation oracle *}
@@ -150,7 +153,14 @@
why you should not use adaptation (see \secref{sec:adaptation}) frivolously.
*}
-subsection {* Code antiquotation *}
+
+subsection {* Building evaluators *}
+
+text {*
+ FIXME
+*}
+
+subsubsection {* Code antiquotation *}
text {*
In scenarios involving techniques like reflection it is quite common
@@ -181,16 +191,6 @@
a good reference.
*}
-subsection {* Imperative data structures *}
-
-text {*
- If you consider imperative data structures as inevitable for a specific
- application, you should consider
- \emph{Imperative Functional Programming with Isabelle/HOL}
- \cite{bulwahn-et-al:2008:imperative};
- the framework described there is available in theory @{theory Imperative_HOL}.
-*}
-
subsection {* ML system interfaces \label{sec:ml} *}
@@ -321,10 +321,4 @@
\end{description}
*}
-text {*
- \bigskip
-
- \emph{Happy proving, happy hacking!}
-*}
-
end
--- a/doc-src/Codegen/Thy/Inductive_Predicate.thy Mon Aug 16 10:05:00 2010 +0100
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Mon Aug 16 12:11:01 2010 +0200
@@ -2,135 +2,164 @@
imports Setup
begin
-section {* Inductive Predicates *}
(*<*)
-hide_const append
+hide_const %invisible append
-inductive append
-where
+inductive %invisible append where
"append [] ys ys"
| "append xs ys zs ==> append (x # xs) ys (x # zs)"
+
+lemma %invisible append: "append xs ys zs = (xs @ ys = zs)"
+ by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
(*>*)
-text {*
-To execute inductive predicates, a special preprocessor, the predicate
- compiler, generates code equations from the introduction rules of the predicates.
-The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
-Consider the simple predicate @{const append} given by these two
-introduction rules:
-*}
-text %quote {*
-@{thm append.intros(1)[of ys]}\\
-\noindent@{thm append.intros(2)[of xs ys zs x]}
-*}
-text {*
-\noindent To invoke the compiler, simply use @{command_def "code_pred"}:
-*}
-code_pred %quote append .
+
+section {* Inductive Predicates \label{sec:inductive} *}
+
text {*
-\noindent The @{command "code_pred"} command takes the name
-of the inductive predicate and then you put a period to discharge
-a trivial correctness proof.
-The compiler infers possible modes
-for the predicate and produces the derived code equations.
-Modes annotate which (parts of the) arguments are to be taken as input,
-and which output. Modes are similar to types, but use the notation @{text "i"}
-for input and @{text "o"} for output.
-
-For @{term "append"}, the compiler can infer the following modes:
-\begin{itemize}
-\item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
-\item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
-\item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
-\end{itemize}
-You can compute sets of predicates using @{command_def "values"}:
+ The @{text predicate_compiler} is an extension of the code generator
+ which turns inductive specifications into equational ones, from
+ which in turn executable code can be generated. The mechanisms of
+ this compiler are described in detail in
+ \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
+
+ Consider the simple predicate @{const append} given by these two
+ introduction rules:
*}
-values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
-text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
-values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
-text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
+
+text %quote {*
+ @{thm append.intros(1)[of ys]} \\
+ @{thm append.intros(2)[of xs ys zs x]}
+*}
+
text {*
-\noindent If you are only interested in the first elements of the set
-comprehension (with respect to a depth-first search on the introduction rules), you can
-pass an argument to
-@{command "values"} to specify the number of elements you want:
+ \noindent To invoke the compiler, simply use @{command_def "code_pred"}:
*}
-values %quote 1 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
-values %quote 3 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
+code_pred %quote append .
+
+text {*
+ \noindent The @{command "code_pred"} command takes the name of the
+ inductive predicate and then you put a period to discharge a trivial
+ correctness proof. The compiler infers possible modes for the
+ predicate and produces the derived code equations. Modes annotate
+ which (parts of the) arguments are to be taken as input, and which
+ output. Modes are similar to types, but use the notation @{text "i"}
+ for input and @{text "o"} for output.
+
+ For @{term "append"}, the compiler can infer the following modes:
+ \begin{itemize}
+ \item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
+ \item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
+ \item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
+ \end{itemize}
+ You can compute sets of predicates using @{command_def "values"}:
+*}
+
+values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
+
+text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
+
+values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
+
+text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
text {*
-\noindent The @{command "values"} command can only compute set
- comprehensions for which a mode has been inferred.
+ \noindent If you are only interested in the first elements of the
+ set comprehension (with respect to a depth-first search on the
+ introduction rules), you can pass an argument to @{command "values"}
+ to specify the number of elements you want:
+*}
-The code equations for a predicate are made available as theorems with
- the suffix @{text "equation"}, and can be inspected with:
-*}
-thm %quote append.equation
+values %quote 1 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
+values %quote 3 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
+
text {*
-\noindent More advanced options are described in the following subsections.
+ \noindent The @{command "values"} command can only compute set
+ comprehensions for which a mode has been inferred.
+
+ The code equations for a predicate are made available as theorems with
+ the suffix @{text "equation"}, and can be inspected with:
*}
-subsubsection {* Alternative names for functions *}
+
+thm %quote append.equation
+
+text {*
+ \noindent More advanced options are described in the following subsections.
+*}
+
+subsection {* Alternative names for functions *}
+
text {*
-By default, the functions generated from a predicate are named after the predicate with the
-mode mangled into the name (e.g., @{text "append_i_i_o"}).
-You can specify your own names as follows:
+ By default, the functions generated from a predicate are named after
+ the predicate with the mode mangled into the name (e.g., @{text
+ "append_i_i_o"}). You can specify your own names as follows:
*}
+
code_pred %quote (modes: i => i => o => bool as concat,
o => o => i => bool as split,
i => o => i => bool as suffix) append .
-subsubsection {* Alternative introduction rules *}
+subsection {* Alternative introduction rules *}
+
text {*
-Sometimes the introduction rules of an predicate are not executable because they contain
-non-executable constants or specific modes could not be inferred.
-It is also possible that the introduction rules yield a function that loops forever
-due to the execution in a depth-first search manner.
-Therefore, you can declare alternative introduction rules for predicates with the attribute
-@{attribute "code_pred_intro"}.
-For example, the transitive closure is defined by:
+ Sometimes the introduction rules of an predicate are not executable
+ because they contain non-executable constants or specific modes
+ could not be inferred. It is also possible that the introduction
+ rules yield a function that loops forever due to the execution in a
+ depth-first search manner. Therefore, you can declare alternative
+ introduction rules for predicates with the attribute @{attribute
+ "code_pred_intro"}. For example, the transitive closure is defined
+ by:
*}
+
text %quote {*
-@{thm tranclp.intros(1)[of r a b]}\\
-\noindent @{thm tranclp.intros(2)[of r a b c]}
+ @{thm tranclp.intros(1)[of r a b]} \\
+ @{thm tranclp.intros(2)[of r a b c]}
*}
+
text {*
-\noindent These rules do not suit well for executing the transitive closure
-with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as the second rule will
-cause an infinite loop in the recursive call.
-This can be avoided using the following alternative rules which are
-declared to the predicate compiler by the attribute @{attribute "code_pred_intro"}:
+ \noindent These rules do not suit well for executing the transitive
+ closure with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as
+ the second rule will cause an infinite loop in the recursive call.
+ This can be avoided using the following alternative rules which are
+ declared to the predicate compiler by the attribute @{attribute
+ "code_pred_intro"}:
*}
+
lemma %quote [code_pred_intro]:
"r a b \<Longrightarrow> r\<^sup>+\<^sup>+ a b"
"r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
by auto
+
text {*
-\noindent After declaring all alternative rules for the transitive closure,
-you invoke @{command "code_pred"} as usual.
-As you have declared alternative rules for the predicate, you are urged to prove that these
-introduction rules are complete, i.e., that you can derive an elimination rule for the
-alternative rules:
+ \noindent After declaring all alternative rules for the transitive
+ closure, you invoke @{command "code_pred"} as usual. As you have
+ declared alternative rules for the predicate, you are urged to prove
+ that these introduction rules are complete, i.e., that you can
+ derive an elimination rule for the alternative rules:
*}
+
code_pred %quote tranclp
proof -
case tranclp
- from this converse_tranclpE[OF this(1)] show thesis by metis
+ from this converse_tranclpE [OF this(1)] show thesis by metis
qed
+
text {*
-\noindent Alternative rules can also be used for constants that have not
-been defined inductively. For example, the lexicographic order which
-is defined as: *}
-text %quote {*
-@{thm [display] lexord_def[of "r"]}
+ \noindent Alternative rules can also be used for constants that have
+ not been defined inductively. For example, the lexicographic order
+ which is defined as:
*}
-text {*
-\noindent To make it executable, you can derive the following two rules and prove the
-elimination rule:
+
+text %quote {*
+ @{thm [display] lexord_def[of "r"]}
*}
-(*<*)
-lemma append: "append xs ys zs = (xs @ ys = zs)"
-by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
-(*>*)
+
+text {*
+ \noindent To make it executable, you can derive the following two
+ rules and prove the elimination rule:
+*}
+
lemma %quote [code_pred_intro]:
"append xs (a # v) ys \<Longrightarrow> lexord r (xs, ys)"
(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*)
@@ -139,12 +168,10 @@
"append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b)
\<Longrightarrow> lexord r (xs, ys)"
(*<*)unfolding lexord_def Collect_def append mem_def apply simp
-apply (rule disjI2) by auto
-(*>*)
+apply (rule disjI2) by auto(*>*)
code_pred %quote lexord
-(*<*)
-proof -
+(*<*)proof -
fix r xs ys
assume lexord: "lexord r (xs, ys)"
assume 1: "\<And> r' xs' ys' a v. r = r' \<Longrightarrow> (xs, ys) = (xs', ys') \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
@@ -162,59 +189,81 @@
ultimately show thesis
unfolding lexord_def
by (fastsimp simp add: Collect_def)
-qed
-(*>*)
-subsubsection {* Options for values *}
+qed(*>*)
+
+
+subsection {* Options for values *}
+
text {*
-In the presence of higher-order predicates, multiple modes for some predicate could be inferred
-that are not disambiguated by the pattern of the set comprehension.
-To disambiguate the modes for the arguments of a predicate, you can state
-the modes explicitly in the @{command "values"} command.
-Consider the simple predicate @{term "succ"}:
+ In the presence of higher-order predicates, multiple modes for some
+ predicate could be inferred that are not disambiguated by the
+ pattern of the set comprehension. To disambiguate the modes for the
+ arguments of a predicate, you can state the modes explicitly in the
+ @{command "values"} command. Consider the simple predicate @{term
+ "succ"}:
*}
-inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool"
-where
+
+inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 (Suc 0)"
| "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
-code_pred succ .
+code_pred %quote succ .
text {*
-\noindent For this, the predicate compiler can infer modes @{text "o \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"},
- @{text "o \<Rightarrow> i \<Rightarrow> bool"} and @{text "i \<Rightarrow> i \<Rightarrow> bool"}.
-The invocation of @{command "values"} @{text "{n. tranclp succ 10 n}"} loops, as multiple
-modes for the predicate @{text "succ"} are possible and here the first mode @{text "o \<Rightarrow> o \<Rightarrow> bool"}
-is chosen. To choose another mode for the argument, you can declare the mode for the argument between
-the @{command "values"} and the number of elements.
+ \noindent For this, the predicate compiler can infer modes @{text "o
+ \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"}, @{text "o \<Rightarrow> i \<Rightarrow> bool"} and
+ @{text "i \<Rightarrow> i \<Rightarrow> bool"}. The invocation of @{command "values"}
+ @{text "{n. tranclp succ 10 n}"} loops, as multiple modes for the
+ predicate @{text "succ"} are possible and here the first mode @{text
+ "o \<Rightarrow> o \<Rightarrow> bool"} is chosen. To choose another mode for the argument,
+ you can declare the mode for the argument between the @{command
+ "values"} and the number of elements.
*}
+
values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
-subsubsection {* Embedding into functional code within Isabelle/HOL *}
+
+subsection {* Embedding into functional code within Isabelle/HOL *}
+
text {*
-To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
-you have a number of options:
-\begin{itemize}
-\item You want to use the first-order predicate with the mode
- where all arguments are input. Then you can use the predicate directly, e.g.
-\begin{quote}
- @{text "valid_suffix ys zs = "}\\
- @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
-\end{quote}
-\item If you know that the execution returns only one value (it is deterministic), then you can
- use the combinator @{term "Predicate.the"}, e.g., a functional concatenation of lists
- is defined with
-\begin{quote}
- @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
-\end{quote}
- Note that if the evaluation does not return a unique value, it raises a run-time error
- @{term "not_unique"}.
-\end{itemize}
+ To embed the computation of an inductive predicate into functions
+ that are defined in Isabelle/HOL, you have a number of options:
+
+ \begin{itemize}
+
+ \item You want to use the first-order predicate with the mode
+ where all arguments are input. Then you can use the predicate directly, e.g.
+
+ \begin{quote}
+ @{text "valid_suffix ys zs = "} \\
+ @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
+ \end{quote}
+
+ \item If you know that the execution returns only one value (it is
+ deterministic), then you can use the combinator @{term
+ "Predicate.the"}, e.g., a functional concatenation of lists is
+ defined with
+
+ \begin{quote}
+ @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
+ \end{quote}
+
+ Note that if the evaluation does not return a unique value, it
+ raises a run-time error @{term "not_unique"}.
+
+ \end{itemize}
*}
-subsubsection {* Further Examples *}
-text {* Further examples for compiling inductive predicates can be found in
-the @{text "HOL/ex/Predicate_Compile_ex"} theory file.
-There are also some examples in the Archive of Formal Proofs, notably
-in the @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} sessions.
+
+
+subsection {* Further Examples *}
+
+text {*
+ Further examples for compiling inductive predicates can be found in
+ the @{text "HOL/ex/Predicate_Compile_ex,thy"} theory file. There are
+ also some examples in the Archive of Formal Proofs, notably in the
+ @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
+ sessions.
*}
+
end
--- a/doc-src/Codegen/Thy/Introduction.thy Mon Aug 16 10:05:00 2010 +0100
+++ b/doc-src/Codegen/Thy/Introduction.thy Mon Aug 16 12:11:01 2010 +0200
@@ -4,71 +4,42 @@
section {* Introduction *}
-subsection {* Code generation fundamental: shallow embedding *}
-
-subsection {* A quick start with the @{text "Isabelle/HOL"} toolbox *}
+text {*
+ This tutorial introduces the code generator facilities of @{text
+ "Isabelle/HOL"}. It allows to turn (a certain class of) HOL
+ specifications into corresponding executable code in the programming
+ languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml} and
+ @{text Haskell} \cite{haskell-revised-report}.
-subsection {* Type classes *}
+ To profit from this tutorial, some familiarity and experience with
+ @{theory HOL} \cite{isa-tutorial} and its basic theories is assumed.
+*}
-subsection {* How to continue from here *}
-subsection {* If something goes utterly wrong *}
+subsection {* Code generation principle: shallow embedding \label{sec:principle} *}
text {*
- This tutorial introduces a generic code generator for the
- @{text Isabelle} system.
- The
- \qn{target language} for which code is
- generated is not fixed, but may be one of several
- functional programming languages (currently, the implementation
- supports @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml} and @{text Haskell}
- \cite{haskell-revised-report}).
-
- Conceptually the code generator framework is part
- of Isabelle's @{theory Pure} meta logic framework; the logic
- @{theory HOL} \cite{isa-tutorial}, which is an extension of @{theory Pure},
- already comes with a reasonable framework setup and thus provides
- a good basis for creating code-generation-driven
- applications. So, we assume some familiarity and experience
- with the ingredients of the @{theory HOL} distribution theories.
-
- The code generator aims to be usable with no further ado
- in most cases, while allowing for detailed customisation.
- This can be seen in the structure of this tutorial: after a short
- conceptual introduction with an example (\secref{sec:intro}),
- we discuss the generic customisation facilities (\secref{sec:program}).
- A further section (\secref{sec:adaptation}) is dedicated to the matter of
- \qn{adaptation} to specific target language environments. After some
- further issues (\secref{sec:further}) we conclude with an overview
- of some ML programming interfaces (\secref{sec:ml}).
-
- \begin{warn}
- Ultimately, the code generator which this tutorial deals with
- is supposed to replace the existing code generator
- by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
- So, for the moment, there are two distinct code generators
- in Isabelle. In case of ambiguity, we will refer to the framework
- described here as @{text "generic code generator"}, to the
- other as @{text "SML code generator"}.
- Also note that while the framework itself is
- object-logic independent, only @{theory HOL} provides a reasonable
- framework setup.
- \end{warn}
-
+ The key concept for understanding Isabelle's code generation is
+ \emph{shallow embedding}: logical entities like constants, types and
+ classes are identified with corresponding entities in the target
+ language. In particular, the carrier of a generated program's
+ semantics are \emph{equational theorems} from the logic. If we view
+ a generated program as an implementation of a higher-order rewrite
+ system, then every rewrite step performed by the program can be
+ simulated in the logic, which guarantees partial correctness
+ \cite{Haftmann-Nipkow:2010:code}.
*}
-subsection {* Code generation via shallow embedding \label{sec:intro} *}
+
+subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *}
text {*
- The key concept for understanding @{text Isabelle}'s code generation is
- \emph{shallow embedding}, i.e.~logical entities like constants, types and
- classes are identified with corresponding concepts in the target language.
+ In a HOL theory, the @{command datatype} and @{command
+ definition}/@{command primrec}/@{command fun} declarations form the
+ core of a functional programming language. By default equational
+ theorems stemming from those are used for generated code, therefore
+ \qt{naive} code generation can proceed without further ado.
- Inside @{theory HOL}, the @{command datatype} and
- @{command definition}/@{command primrec}/@{command fun} declarations form
- the core of a functional programming language. The default code generator setup
- transforms those into functional programs immediately.
- This means that \qt{naive} code generation can proceed without further ado.
For example, here a simple \qt{implementation} of amortised queues:
*}
@@ -84,7 +55,11 @@
"dequeue (AQueue [] []) = (None, AQueue [] [])"
| "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
| "dequeue (AQueue xs []) =
- (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))"
+ (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))" (*<*)
+
+lemma %invisible dequeue_nonempty_Nil [simp]:
+ "xs \<noteq> [] \<Longrightarrow> dequeue (AQueue xs []) = (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))"
+ by (cases xs) (simp_all split: list.splits) (*>*)
text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *}
@@ -96,112 +71,163 @@
text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
text {*
- \noindent The @{command export_code} command takes a space-separated list of
- constants for which code shall be generated; anything else needed for those
- is added implicitly. Then follows a target language identifier
- (@{text SML}, @{text OCaml} or @{text Haskell}) and a freely chosen module name.
- A file name denotes the destination to store the generated code. Note that
- the semantics of the destination depends on the target language: for
- @{text SML} and @{text OCaml} it denotes a \emph{file}, for @{text Haskell}
- it denotes a \emph{directory} where a file named as the module name
- (with extension @{text ".hs"}) is written:
+ \noindent The @{command export_code} command takes a space-separated
+ list of constants for which code shall be generated; anything else
+ needed for those is added implicitly. Then follows a target
+ language identifier and a freely chosen module name. A file name
+ denotes the destination to store the generated code. Note that the
+ semantics of the destination depends on the target language: for
+ @{text SML} and @{text OCaml} it denotes a \emph{file}, for @{text
+ Haskell} it denotes a \emph{directory} where a file named as the
+ module name (with extension @{text ".hs"}) is written:
*}
export_code %quote empty dequeue enqueue in Haskell
module_name Example file "examples/"
text {*
- \noindent This is the corresponding code in @{text Haskell}:
+ \noindent This is the corresponding code:
*}
text %quote {*@{code_stmts empty enqueue dequeue (Haskell)}*}
text {*
- \noindent This demonstrates the basic usage of the @{command export_code} command;
- for more details see \secref{sec:further}.
+ \noindent For more details about @{command export_code} see
+ \secref{sec:further}.
*}
-subsection {* If something utterly fails *}
+
+subsection {* Type classes *}
text {*
- Under certain circumstances, the code generator fails to produce
- code entirely.
-
- \begin{description}
-
- \ditem{generate only one module}
-
- \ditem{check with a different target language}
-
- \ditem{inspect code equations}
-
- \ditem{inspect preprocessor setup}
-
- \ditem{generate exceptions}
-
- \ditem{remove offending code equations}
-
- \end{description}
+ Code can also be generated from type classes in a Haskell-like
+ manner. For illustration here an example from abstract algebra:
*}
-subsection {* Code generator architecture \label{sec:concept} *}
+class %quote semigroup =
+ fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
+ assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
+
+class %quote monoid = semigroup +
+ fixes neutral :: 'a ("\<one>")
+ assumes neutl: "\<one> \<otimes> x = x"
+ and neutr: "x \<otimes> \<one> = x"
+
+instantiation %quote nat :: monoid
+begin
+
+primrec %quote mult_nat where
+ "0 \<otimes> n = (0\<Colon>nat)"
+ | "Suc m \<otimes> n = n + m \<otimes> n"
+
+definition %quote neutral_nat where
+ "\<one> = Suc 0"
+
+lemma %quote add_mult_distrib:
+ fixes n m q :: nat
+ shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
+ by (induct n) simp_all
+
+instance %quote proof
+ fix m n q :: nat
+ show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
+ by (induct m) (simp_all add: add_mult_distrib)
+ show "\<one> \<otimes> n = n"
+ by (simp add: neutral_nat_def)
+ show "m \<otimes> \<one> = m"
+ by (induct m) (simp_all add: neutral_nat_def)
+qed
+
+end %quote
text {*
- What you have seen so far should be already enough in a lot of cases. If you
- are content with this, you can quit reading here. Anyway, in order to customise
- and adapt the code generator, it is necessary to gain some understanding
- how it works.
+ \noindent We define the natural operation of the natural numbers
+ on monoids:
+*}
+
+primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+ "pow 0 a = \<one>"
+ | "pow (Suc n) a = a \<otimes> pow n a"
- \begin{figure}[h]
- \includegraphics{architecture}
- \caption{Code generator architecture}
- \label{fig:arch}
- \end{figure}
+text {*
+ \noindent This we use to define the discrete exponentiation
+ function:
+*}
+
+definition %quote bexp :: "nat \<Rightarrow> nat" where
+ "bexp n = pow n (Suc (Suc 0))"
+
+text {*
+ \noindent The corresponding code in Haskell uses that language's
+ native classes:
+*}
+
+text %quote {*@{code_stmts bexp (Haskell)}*}
- The code generator employs a notion of executability
- for three foundational executable ingredients known
- from functional programming:
- \emph{code equations}, \emph{datatypes}, and
- \emph{type classes}. A code equation as a first approximation
- is a theorem of the form @{text "f t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n \<equiv> t"}
- (an equation headed by a constant @{text f} with arguments
- @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}).
- Code generation aims to turn code equations
- into a functional program. This is achieved by three major
- components which operate sequentially, i.e. the result of one is
- the input
- of the next in the chain, see figure \ref{fig:arch}:
+text {*
+ \noindent This is a convenient place to show how explicit dictionary
+ construction manifests in generated code -- the same example in
+ @{text SML}:
+*}
+
+text %quote {*@{code_stmts bexp (SML)}*}
+
+text {*
+ \noindent Note the parameters with trailing underscore (@{verbatim
+ "A_"}), which are the dictionary parameters.
+*}
+
+
+subsection {* How to continue from here *}
+
+text {*
+ What you have seen so far should be already enough in a lot of
+ cases. If you are content with this, you can quit reading here.
+
+ Anyway, to understand situations where problems occur or to increase
+ the scope of code generation beyond default, it is necessary to gain
+ some understanding how the code generator actually works:
\begin{itemize}
- \item The starting point is a collection of raw code equations in a
- theory. It is not relevant where they
- stem from, but typically they were either produced by specification
- tools or proved explicitly by the user.
-
- \item These raw code equations can be subjected to theorem transformations. This
- \qn{preprocessor} can apply the full
- expressiveness of ML-based theorem transformations to code
- generation. The result of preprocessing is a
- structured collection of code equations.
+ \item The foundations of the code generator are described in
+ \secref{sec:foundations}.
+
+ \item In particular \secref{sec:utterly_wrong} gives hints how to
+ debug situations where code generation does not succeed as
+ expected.
- \item These code equations are \qn{translated} to a program in an
- abstract intermediate language. Think of it as a kind
- of \qt{Mini-Haskell} with four \qn{statements}: @{text data}
- (for datatypes), @{text fun} (stemming from code equations),
- also @{text class} and @{text inst} (for type classes).
+ \item The scope and quality of generated code can be increased
+ dramatically by applying refinement techniques, which are
+ introduced in \secref{sec:refinement}.
- \item Finally, the abstract program is \qn{serialised} into concrete
- source code of a target language.
- This step only produces concrete syntax but does not change the
- program in essence; all conceptual transformations occur in the
- translation step.
+ \item Inductive predicates can be turned executable using an
+ extension of the code generator \secref{sec:inductive}.
+
+ \item You may want to skim over the more technical sections
+ \secref{sec:adaptation} and \secref{sec:further}.
+
+ \item For exhaustive syntax diagrams etc. you should visit the
+ Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}.
\end{itemize}
- \noindent From these steps, only the two last are carried out outside the logic; by
- keeping this layer as thin as possible, the amount of code to trust is
- kept to a minimum.
+ \bigskip
+
+ \begin{center}\fbox{\fbox{\begin{minipage}{8cm}
+
+ \begin{center}\textit{Happy proving, happy hacking!}\end{center}
+
+ \end{minipage}}}\end{center}
+
+ \begin{warn}
+ There is also a more ancient code generator in Isabelle by Stefan
+ Berghofer \cite{Berghofer-Nipkow:2002}. Although its
+ functionality is covered by the code generator presented here, it
+ will sometimes show up as an artifact. In case of ambiguity, we
+ will refer to the framework described here as @{text "generic code
+ generator"}, to the other as @{text "SML code generator"}.
+ \end{warn}
*}
end
--- a/doc-src/Codegen/Thy/Refinement.thy Mon Aug 16 10:05:00 2010 +0100
+++ b/doc-src/Codegen/Thy/Refinement.thy Mon Aug 16 12:11:01 2010 +0200
@@ -4,4 +4,109 @@
section {* Program and datatype refinement \label{sec:refinement} *}
+subsection {* Datatypes \label{sec:datatypes} *}
+
+text {*
+ Conceptually, any datatype is spanned by a set of
+ \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
+ "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
+ @{text "\<tau>"}. The HOL datatype package by default registers any new
+ datatype in the table of datatypes, which may be inspected using the
+ @{command print_codesetup} command.
+
+ In some cases, it is appropriate to alter or extend this table. As
+ an example, we will develop an alternative representation of the
+ queue example given in \secref{sec:queue_example}. The amortised
+ representation is convenient for generating code but exposes its
+ \qt{implementation} details, which may be cumbersome when proving
+ theorems about it. Therefore, here is a simple, straightforward
+ representation of queues:
+*}
+
+datatype %quote 'a queue = Queue "'a list"
+
+definition %quote empty :: "'a queue" where
+ "empty = Queue []"
+
+primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
+ "enqueue x (Queue xs) = Queue (xs @ [x])"
+
+fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
+ "dequeue (Queue []) = (None, Queue [])"
+ | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
+
+text {*
+ \noindent This we can use directly for proving; for executing,
+ we provide an alternative characterisation:
+*}
+
+definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
+ "AQueue xs ys = Queue (ys @ rev xs)"
+
+code_datatype %quote AQueue
+
+text {*
+ \noindent Here we define a \qt{constructor} @{const "AQueue"} which
+ is defined in terms of @{text "Queue"} and interprets its arguments
+ according to what the \emph{content} of an amortised queue is supposed
+ to be. Equipped with this, we are able to prove the following equations
+ for our primitive queue operations which \qt{implement} the simple
+ queues in an amortised fashion:
+*}
+
+lemma %quote empty_AQueue [code]:
+ "empty = AQueue [] []"
+ unfolding AQueue_def empty_def by simp
+
+lemma %quote enqueue_AQueue [code]:
+ "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
+ unfolding AQueue_def by simp
+
+lemma %quote dequeue_AQueue [code]:
+ "dequeue (AQueue xs []) =
+ (if xs = [] then (None, AQueue [] [])
+ else dequeue (AQueue [] (rev xs)))"
+ "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
+ unfolding AQueue_def by simp_all
+
+text {*
+ \noindent For completeness, we provide a substitute for the
+ @{text case} combinator on queues:
+*}
+
+lemma %quote queue_case_AQueue [code]:
+ "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
+ unfolding AQueue_def by simp
+
+text {*
+ \noindent The resulting code looks as expected:
+*}
+
+text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
+
+text {*
+ \noindent From this example, it can be glimpsed that using own
+ constructor sets is a little delicate since it changes the set of
+ valid patterns for values of that type. Without going into much
+ detail, here some practical hints:
+
+ \begin{itemize}
+
+ \item When changing the constructor set for datatypes, take care
+ to provide alternative equations for the @{text case} combinator.
+
+ \item Values in the target language need not to be normalised --
+ different values in the target language may represent the same
+ value in the logic.
+
+ \item Usually, a good methodology to deal with the subtleties of
+ pattern matching is to see the type as an abstract type: provide
+ a set of operations which operate on the concrete representation
+ of the type, and derive further operations by combinations of
+ these primitive ones, without relying on a particular
+ representation.
+
+ \end{itemize}
+*}
+
end
--- a/doc-src/Codegen/Thy/document/Foundations.tex Mon Aug 16 10:05:00 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Mon Aug 16 12:11:01 2010 +0200
@@ -18,382 +18,68 @@
%
\endisadelimtheory
%
-\isamarkupsection{Code generation foundations \label{sec:program}%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-We have already seen how by default equations stemming from
- \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}, \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
- statements are used for code generation. This default behaviour
- can be changed, e.g.\ by providing different code equations.
- The customisations shown in this section are \emph{safe}
- as regards correctness: all programs that can be generated are partially
- correct.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Selecting code equations%
+\isamarkupsection{Code generation foundations \label{sec:foundations}%
}
\isamarkuptrue%
%
-\begin{isamarkuptext}%
-Coming back to our introductory example, we
- could provide an alternative code equations for \isa{dequeue}
- explicitly:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
- \isa{attribute} which states that the given theorems should be
- considered as code equations for a \isa{fun} statement --
- the corresponding constant is determined syntactically. The resulting code:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
-\hspace*{0pt}dequeue (AQueue xs []) =\\
-\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
-\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been
- replaced by the predicate \isa{null\ xs}. This is due to the default
- setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
-
- Changing the default constructor set of datatypes is also
- possible. See \secref{sec:datatypes} for an example.
-
- As told in \secref{sec:concept}, code generation is based
- on a structured collection of code theorems.
- This collection
- may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
-\ dequeue%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent prints a table with \emph{all} code equations
- for \isa{dequeue}, including
- \emph{all} code equations those equations depend
- on recursively.
-
- Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph
- visualising dependencies between code equations.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{\isa{class} and \isa{instantiation}%
+\isamarkupsubsection{Code generator architecture \label{sec:architecture}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Concerning type classes and code generation, let us examine an example
- from abstract algebra:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{class}\isamarkupfalse%
-\ semigroup\ {\isacharequal}\isanewline
-\ \ \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
-\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{class}\isamarkupfalse%
-\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
-\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{instantiation}\isamarkupfalse%
-\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{primrec}\isamarkupfalse%
-\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
-\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline
-\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
-\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ \isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
-\isacommand{qed}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent We define the natural operation of the natural numbers
- on monoids:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{primrec}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This we use to define the discrete exponentiation function:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{definition}\isamarkupfalse%
-\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent The corresponding code in Haskell uses that language's native classes:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}module Example where {\char123}\\
-\hspace*{0pt}\\
-\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
-\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
-\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
-\hspace*{0pt}\\
-\hspace*{0pt}class Semigroup a where {\char123}\\
-\hspace*{0pt} ~mult ::~a -> a -> a;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
-\hspace*{0pt} ~neutral ::~a;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
-\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
-\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
-\hspace*{0pt}\\
-\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
-\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
-\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
-\hspace*{0pt}\\
-\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
-\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Semigroup Nat where {\char123}\\
-\hspace*{0pt} ~mult = mult{\char95}nat;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Monoid Nat where {\char123}\\
-\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}bexp ::~Nat -> Nat;\\
-\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
-\hspace*{0pt}\\
-\hspace*{0pt}{\char125}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This is a convenient place to show how explicit dictionary construction
- manifests in generated code (here, the same example in \isa{SML})
- \cite{Haftmann-Nipkow:2010:code}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
-\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
-\hspace*{0pt} ~type 'a semigroup\\
-\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
-\hspace*{0pt} ~type 'a monoid\\
-\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
-\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
-\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
-\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
-\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
-\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\
-\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\
-\hspace*{0pt} ~val bexp :~nat -> nat\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
-\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
-\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
-\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
-\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
-\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
-\hspace*{0pt}\\
-\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
-\hspace*{0pt} ~:~nat monoid;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Note the parameters with trailing underscore (\verb|A_|),
- which are the dictionary parameters.%
+The code generator is actually a framework consisting of different
+ components which can be customised individually.
+
+ Conceptually all components operate on Isabelle's logic framework
+ \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}. Practically, the object logic \hyperlink{theory.HOL}{\mbox{\isa{HOL}}}
+ provides the necessary facilities to make use of the code generator,
+ mainly since it is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}.
+
+ The constellation of the different components is visualized in the
+ following picture.
+
+ \begin{figure}[h]
+ \includegraphics{architecture}
+ \caption{Code generator architecture}
+ \label{fig:arch}
+ \end{figure}
+
+ \noindent Central to code generation is the notion of \emph{code
+ equations}. A code equation as a first approximation is a theorem
+ of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t} (an equation headed by a
+ constant \isa{f} with arguments \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right
+ hand side \isa{t}).
+
+ \begin{itemize}
+
+ \item Starting point of code generation is a collection of (raw)
+ code equations in a theory. It is not relevant where they stem
+ from, but typically they were either produced by specification
+ tools or proved explicitly by the user.
+
+ \item These raw code equations can be subjected to theorem
+ transformations. This \qn{preprocessor} (see
+ \secref{sec:preproc}) can apply the full expressiveness of
+ ML-based theorem transformations to code generation. The result
+ of preprocessing is a structured collection of code equations.
+
+ \item These code equations are \qn{translated} to a program in an
+ abstract intermediate language. Think of it as a kind of
+ \qt{Mini-Haskell} with four \qn{statements}: \isa{data} (for
+ datatypes), \isa{fun} (stemming from code equations), also
+ \isa{class} and \isa{inst} (for type classes).
+
+ \item Finally, the abstract program is \qn{serialised} into
+ concrete source code of a target language. This step only
+ produces concrete syntax but does not change the program in
+ essence; all conceptual transformations occur in the translation
+ step.
+
+ \end{itemize}
+
+ \noindent From these steps, only the last two are carried out
+ outside the logic; by keeping this layer as thin as possible, the
+ amount of code to trust is kept to a minimum.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -402,18 +88,18 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Before selected function theorems are turned into abstract
- code, a chain of definitional transformation steps is carried
- out: \emph{preprocessing}. In essence, the preprocessor
- consists of two components: a \emph{simpset} and \emph{function transformers}.
+Before selected function theorems are turned into abstract code, a
+ chain of definitional transformation steps is carried out:
+ \emph{preprocessing}. The preprocessor consists of two
+ components: a \emph{simpset} and \emph{function transformers}.
- The \emph{simpset} can apply the full generality of the
- Isabelle simplifier. Due to the interpretation of theorems as code
+ The \emph{simpset} can apply the full generality of the Isabelle
+ simplifier. Due to the interpretation of theorems as code
equations, rewrites are applied to the right hand side and the
arguments of the left hand side of an equation, but never to the
constant heading the left hand side. An important special case are
- \emph{unfold theorems}, which may be declared and removed using
- the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
+ \emph{unfold theorems}, which may be declared and removed using the
+ \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
attribute, respectively.
Some common applications:%
@@ -444,27 +130,6 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\item eliminating superfluous constants:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
\item replacing executable but inconvenient constructs:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -485,111 +150,8 @@
%
\endisadelimquote
%
-\end{itemize}
-%
\begin{isamarkuptext}%
-\noindent \emph{Function transformers} provide a very general interface,
- transforming a list of function theorems to another
- list of function theorems, provided that neither the heading
- constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc}
- pattern elimination implemented in
- theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this
- interface.
-
- \noindent The current setup of the preprocessor may be inspected using
- the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command.
- \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
- mechanism to inspect the impact of a preprocessor setup
- on code equations.
-
- \begin{warn}
-
- Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
- preprocessor of the ancient \isa{SML\ code\ generator}; in case
- this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
- \end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Datatypes \label{sec:datatypes}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Conceptually, any datatype is spanned by a set of
- \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
- \isa{{\isasymtau}}. The HOL datatype package by default registers any new
- datatype in the table of datatypes, which may be inspected using the
- \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
-
- In some cases, it is appropriate to alter or extend this table. As
- an example, we will develop an alternative representation of the
- queue example given in \secref{sec:intro}. The amortised
- representation is convenient for generating code but exposes its
- \qt{implementation} details, which may be cumbersome when proving
- theorems about it. Therefore, here is a simple, straightforward
- representation of queues:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{datatype}\isamarkupfalse%
-\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{primrec}\isamarkupfalse%
-\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{fun}\isamarkupfalse%
-\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This we can use directly for proving; for executing,
- we provide an alternative characterisation:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{definition}\isamarkupfalse%
-\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
-\ AQueue%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Here we define a \qt{constructor} \isa{AQueue} which
- is defined in terms of \isa{Queue} and interprets its arguments
- according to what the \emph{content} of an amortised queue is supposed
- to be. Equipped with this, we are able to prove the following equations
- for our primitive queue operations which \qt{implement} the simple
- queues in an amortised fashion:%
+\item eliminating disturbing expressions:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -599,28 +161,9 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{unfolding}\isamarkupfalse%
-\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{unfolding}\isamarkupfalse%
-\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
-\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{unfolding}\isamarkupfalse%
-\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ simp{\isacharunderscore}all%
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
@@ -628,9 +171,41 @@
%
\endisadelimquote
%
+\end{itemize}
+%
\begin{isamarkuptext}%
-\noindent For completeness, we provide a substitute for the
- \isa{case} combinator on queues:%
+\noindent \emph{Function transformers} provide a very general
+ interface, transforming a list of function theorems to another list
+ of function theorems, provided that neither the heading constant nor
+ its type change. The \isa{{\isadigit{0}}} / \isa{Suc} pattern
+ elimination implemented in theory \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}} (see
+ \secref{eff_nat}) uses this interface.
+
+ \noindent The current setup of the preprocessor may be inspected
+ using the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command. \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}
+ (see \secref{sec:equations}) provides a convenient mechanism to
+ inspect the impact of a preprocessor setup on code equations.
+
+ \begin{warn}
+ Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
+ preprocessor of the ancient \isa{SML\ code\ generator}; in case
+ this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Understanding code equations \label{sec:equations}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+As told in \secref{sec:principle}, the notion of code equations is
+ vital to code generation. Indeed most problems which occur in
+ practice can be resolved by an inspection of the underlying code
+ equations.
+
+ It is possible to exchange the default code equations for constants
+ by explicitly proving alternative ones:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -640,11 +215,14 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{unfolding}\isamarkupfalse%
-\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ simp%
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
@@ -653,7 +231,10 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The resulting code looks as expected:%
+\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{attribute}
+ which states that the given theorems should be considered as code
+ equations for a \isa{fun} statement -- the corresponding constant
+ is determined syntactically. The resulting code:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -666,36 +247,11 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
-\hspace*{0pt} ~val rev :~'a list -> 'a list\\
-\hspace*{0pt} ~val null :~'a list -> bool\\
-\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
-\hspace*{0pt} ~val empty :~'a queue\\
-\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
-\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun null [] = true\\
-\hspace*{0pt} ~| null (x ::~xs) = false;\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
-\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
-\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
-\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
+\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
+\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
+\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -707,28 +263,44 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent From this example, it can be glimpsed that using own
- constructor sets is a little delicate since it changes the set of
- valid patterns for values of that type. Without going into much
- detail, here some practical hints:
+\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has
+ been replaced by the predicate \isa{List{\isachardot}null\ xs}. This is due
+ to the default setup of the \qn{preprocessor}.
- \begin{itemize}
+ This possibility to select arbitrary code equations is the key
+ technique for program and datatype refinement (see
+ \secref{sec:refinement}.
- \item When changing the constructor set for datatypes, take care
- to provide alternative equations for the \isa{case} combinator.
+ Due to the preprocessor, there is the distinction of raw code
+ equations (before preprocessing) and code equations (after
+ preprocessing).
+
+ The first can be listed (among other data) using the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command (later on in \secref{sec:refinement}
+ it will be shown how these code equations can be changed).
- \item Values in the target language need not to be normalised --
- different values in the target language may represent the same
- value in the logic.
-
- \item Usually, a good methodology to deal with the subtleties of
- pattern matching is to see the type as an abstract type: provide
- a set of operations which operate on the concrete representation
- of the type, and derive further operations by combinations of
- these primitive ones, without relying on a particular
- representation.
-
- \end{itemize}%
+ The code equations after preprocessing are already are blueprint of
+ the generated program and can be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
+\ dequeue%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This prints a table with the code equations for \isa{dequeue}, including \emph{all} code equations those equations depend
+ on recursively. These dependencies themselves can be visualized using
+ the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -737,8 +309,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Surely you have already noticed how equality is treated
- by the code generator:%
+Implementation of equality deserves some attention. Here an example
+ function involving polymorphic equality:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -750,11 +322,11 @@
\isacommand{primrec}\isamarkupfalse%
\ 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
\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
-\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
-\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
-\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
-\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
+{\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
+\ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
+\ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
+\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
+\ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
@@ -764,8 +336,8 @@
%
\begin{isamarkuptext}%
\noindent During preprocessing, the membership test is rewritten,
- resulting in \isa{List{\isachardot}member}, which itself
- performs an explicit equality check.%
+ resulting in \isa{List{\isachardot}member}, which itself performs an explicit
+ equality check, as can be seen in the corresponding \isa{SML} code:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -815,18 +387,16 @@
%
\begin{isamarkuptext}%
\noindent Obviously, polymorphic equality is implemented the Haskell
- way using a type class. How is this achieved? HOL introduces
- an explicit class \isa{eq} with a corresponding operation
- \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.
- The preprocessing framework does the rest by propagating the
- \isa{eq} constraints through all dependent code equations.
- For datatypes, instances of \isa{eq} are implicitly derived
- when possible. For other types, you may instantiate \isa{eq}
- manually like any other type class.%
+ way using a type class. How is this achieved? HOL introduces an
+ explicit class \isa{eq} with a corresponding operation \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}. The preprocessing
+ framework does the rest by propagating the \isa{eq} constraints
+ through all dependent code equations. For datatypes, instances of
+ \isa{eq} are implicitly derived when possible. For other types,
+ you may instantiate \isa{eq} manually like any other type class.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Explicit partiality%
+\isamarkupsubsection{Explicit partiality \label{sec:partiality}%
}
\isamarkuptrue%
%
@@ -852,7 +422,7 @@
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def{\isacharparenright}\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
@@ -916,7 +486,7 @@
\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
@@ -985,10 +555,55 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent This feature however is rarely needed in practice.
- Note also that the \isa{HOL} default setup already declares
- \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
- likely to be used in such situations.%
+\noindent This feature however is rarely needed in practice. Note
+ also that the HOL default setup already declares \isa{undefined}
+ as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most likely to be used in such
+ situations.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{If something goes utterly wrong \label{sec:utterly_wrong}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Under certain circumstances, the code generator fails to produce
+ code entirely. To debug these, the following hints may prove
+ helpful:
+
+ \begin{description}
+
+ \ditem{\emph{Check with a different target language}.} Sometimes
+ the situation gets more clear if you switch to another target
+ language; the code generated there might give some hints what
+ prevents the code generator to produce code for the desired
+ language.
+
+ \ditem{\emph{Inspect code equations}.} Code equations are the central
+ carrier of code generation. Most problems occuring while generation
+ code can be traced to single equations which are printed as part of
+ the error message. A closer inspection of those may offer the key
+ for solving issues (cf.~\secref{sec:equations}).
+
+ \ditem{\emph{Inspect preprocessor setup}.} The preprocessor might
+ transform code equations unexpectedly; to understand an
+ inspection of its setup is necessary (cf.~\secref{sec:preproc}).
+
+ \ditem{\emph{Generate exceptions}.} If the code generator
+ complains about missing code equations, in can be helpful to
+ implement the offending constants as exceptions
+ (cf.~\secref{sec:partiality}); this allows at least for a formal
+ generation of code, whose inspection may then give clues what is
+ wrong.
+
+ \ditem{\emph{Remove offending code equations}.} If code
+ generation is prevented by just a single equation, this can be
+ removed (cf.~\secref{sec:equations}) to allow formal code
+ generation, whose result in turn can be used to trace the
+ problem. The most prominent case here are mismatches in type
+ class signatures (\qt{wellsortedness error}).
+
+ \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Further.tex Mon Aug 16 10:05:00 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Further.tex Mon Aug 16 12:11:01 2010 +0200
@@ -22,14 +22,50 @@
}
\isamarkuptrue%
%
-\isamarkupsubsection{Further reading%
+\isamarkupsubsection{Modules namespace%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-To dive deeper into the issue of code generation, you should visit
- the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}, which
- contains exhaustive syntax diagrams.%
+When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command it is possible to leave
+ out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} part; then code is distributed over
+ different modules, where the module name space roughly is induced
+ by the Isabelle theory name space.
+
+ Then sometimes the awkward situation occurs that dependencies between
+ definitions introduce cyclic dependencies between modules, which in the
+ \isa{Haskell} world leaves you to the mercy of the \isa{Haskell} implementation
+ you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible.
+
+ A solution is to declare module names explicitly.
+ Let use assume the three cyclically dependent
+ modules are named \emph{A}, \emph{B} and \emph{C}.
+ Then, by stating%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}modulename}\isamarkupfalse%
+\ SML\isanewline
+\ \ A\ ABC\isanewline
+\ \ B\ ABC\isanewline
+\ \ C\ ABC%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent
+ we explicitly map all those modules on \emph{ABC},
+ resulting in an ad-hoc merge of this three modules
+ at serialisation time.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -197,50 +233,16 @@
%
\endisadelimquote
%
-\isamarkupsubsection{Modules%
+\isamarkupsubsection{Imperative data structures%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command it is possible to leave
- out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} part; then code is distributed over
- different modules, where the module name space roughly is induced
- by the \isa{Isabelle} theory name space.
-
- Then sometimes the awkward situation occurs that dependencies between
- definitions introduce cyclic dependencies between modules, which in the
- \isa{Haskell} world leaves you to the mercy of the \isa{Haskell} implementation
- you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible.
-
- A solution is to declare module names explicitly.
- Let use assume the three cyclically dependent
- modules are named \emph{A}, \emph{B} and \emph{C}.
- Then, by stating%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{code{\isacharunderscore}modulename}\isamarkupfalse%
-\ SML\isanewline
-\ \ A\ ABC\isanewline
-\ \ B\ ABC\isanewline
-\ \ C\ ABC%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent
- we explicitly map all those modules on \emph{ABC},
- resulting in an ad-hoc merge of this three modules
- at serialisation time.%
+If you consider imperative data structures as inevitable for a
+ specific application, you should consider \emph{Imperative
+ Functional Programming with Isabelle/HOL}
+ \cite{bulwahn-et-al:2008:imperative}; the framework described there
+ is available in session \hyperlink{theory.Imperative-HOL}{\mbox{\isa{Imperative{\isacharunderscore}HOL}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -301,7 +303,16 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Code antiquotation%
+\isamarkupsubsection{Building evaluators%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Code antiquotation%
}
\isamarkuptrue%
%
@@ -376,19 +387,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Imperative data structures%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If you consider imperative data structures as inevitable for a specific
- application, you should consider
- \emph{Imperative Functional Programming with Isabelle/HOL}
- \cite{bulwahn-et-al:2008:imperative};
- the framework described there is available in theory \hyperlink{theory.Imperative-HOL}{\mbox{\isa{Imperative{\isacharunderscore}HOL}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsubsection{ML system interfaces \label{sec:ml}%
}
\isamarkuptrue%
@@ -555,13 +553,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\begin{isamarkuptext}%
-\bigskip
-
- \emph{Happy proving, happy hacking!}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Mon Aug 16 10:05:00 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Mon Aug 16 12:11:01 2010 +0200
@@ -10,7 +10,8 @@
\isacommand{theory}\isamarkupfalse%
\ Inductive{\isacharunderscore}Predicate\isanewline
\isakeyword{imports}\ Setup\isanewline
-\isakeyword{begin}%
+\isakeyword{begin}\isanewline
+%
\endisatagtheory
{\isafoldtheory}%
%
@@ -18,16 +19,32 @@
%
\endisadelimtheory
%
-\isamarkupsection{Inductive Predicates%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isamarkupsection{Inductive Predicates \label{sec:inductive}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-To execute inductive predicates, a special preprocessor, the predicate
- compiler, generates code equations from the introduction rules of the predicates.
-The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
-Consider the simple predicate \isa{append} given by these two
-introduction rules:%
+The \isa{predicate{\isacharunderscore}compiler} is an extension of the code generator
+ which turns inductive specifications into equational ones, from
+ which in turn executable code can be generated. The mechanisms of
+ this compiler are described in detail in
+ \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
+
+ Consider the simple predicate \isa{append} given by these two
+ introduction rules:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -38,8 +55,8 @@
\isatagquote
%
\begin{isamarkuptext}%
-\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys}\\
-\noindent\isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}%
+\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys} \\
+ \isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -71,22 +88,21 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name
-of the inductive predicate and then you put a period to discharge
-a trivial correctness proof.
-The compiler infers possible modes
-for the predicate and produces the derived code equations.
-Modes annotate which (parts of the) arguments are to be taken as input,
-and which output. Modes are similar to types, but use the notation \isa{i}
-for input and \isa{o} for output.
+\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name of the
+ inductive predicate and then you put a period to discharge a trivial
+ correctness proof. The compiler infers possible modes for the
+ predicate and produces the derived code equations. Modes annotate
+ which (parts of the) arguments are to be taken as input, and which
+ output. Modes are similar to types, but use the notation \isa{i}
+ for input and \isa{o} for output.
-For \isa{append}, the compiler can infer the following modes:
-\begin{itemize}
-\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
-\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
-\item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
-\end{itemize}
-You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:%
+ For \isa{append}, the compiler can infer the following modes:
+ \begin{itemize}
+ \item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
+ \item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
+ \item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
+ \end{itemize}
+ You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -129,10 +145,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\noindent If you are only interested in the first elements of the set
-comprehension (with respect to a depth-first search on the introduction rules), you can
-pass an argument to
-\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} to specify the number of elements you want:%
+\noindent If you are only interested in the first elements of the
+ set comprehension (with respect to a depth-first search on the
+ introduction rules), you can pass an argument to \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}
+ to specify the number of elements you want:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -142,9 +158,9 @@
%
\isatagquote
\isacommand{values}\isamarkupfalse%
-\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isacommand{values}\isamarkupfalse%
-\ {\isadigit{3}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}%
+\ {\isadigit{3}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
@@ -154,10 +170,10 @@
%
\begin{isamarkuptext}%
\noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command can only compute set
- comprehensions for which a mode has been inferred.
+ comprehensions for which a mode has been inferred.
-The code equations for a predicate are made available as theorems with
- the suffix \isa{equation}, and can be inspected with:%
+ The code equations for a predicate are made available as theorems with
+ the suffix \isa{equation}, and can be inspected with:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -180,14 +196,13 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Alternative names for functions%
+\isamarkupsubsection{Alternative names for functions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-By default, the functions generated from a predicate are named after the predicate with the
-mode mangled into the name (e.g., \isa{append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}).
-You can specify your own names as follows:%
+By default, the functions generated from a predicate are named after
+ the predicate with the mode mangled into the name (e.g., \isa{append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}). You can specify your own names as follows:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -208,18 +223,18 @@
%
\endisadelimquote
%
-\isamarkupsubsubsection{Alternative introduction rules%
+\isamarkupsubsection{Alternative introduction rules%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Sometimes the introduction rules of an predicate are not executable because they contain
-non-executable constants or specific modes could not be inferred.
-It is also possible that the introduction rules yield a function that loops forever
-due to the execution in a depth-first search manner.
-Therefore, you can declare alternative introduction rules for predicates with the attribute
-\hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}.
-For example, the transitive closure is defined by:%
+Sometimes the introduction rules of an predicate are not executable
+ because they contain non-executable constants or specific modes
+ could not be inferred. It is also possible that the introduction
+ rules yield a function that loops forever due to the execution in a
+ depth-first search manner. Therefore, you can declare alternative
+ introduction rules for predicates with the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}. For example, the transitive closure is defined
+ by:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -230,8 +245,8 @@
\isatagquote
%
\begin{isamarkuptext}%
-\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b}\\
-\noindent \isa{{\isasymlbrakk}r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isacharsemicolon}\ r\ b\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}%
+\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b} \\
+ \isa{r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b\ {\isasymLongrightarrow}\ r\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -243,11 +258,11 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent These rules do not suit well for executing the transitive closure
-with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as the second rule will
-cause an infinite loop in the recursive call.
-This can be avoided using the following alternative rules which are
-declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:%
+\noindent These rules do not suit well for executing the transitive
+ closure with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as
+ the second rule will cause an infinite loop in the recursive call.
+ This can be avoided using the following alternative rules which are
+ declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -270,11 +285,11 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent After declaring all alternative rules for the transitive closure,
-you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual.
-As you have declared alternative rules for the predicate, you are urged to prove that these
-introduction rules are complete, i.e., that you can derive an elimination rule for the
-alternative rules:%
+\noindent After declaring all alternative rules for the transitive
+ closure, you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual. As you have
+ declared alternative rules for the predicate, you are urged to prove
+ that these introduction rules are complete, i.e., that you can
+ derive an elimination rule for the alternative rules:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -290,7 +305,7 @@
\ \ \isacommand{case}\isamarkupfalse%
\ tranclp\isanewline
\ \ \isacommand{from}\isamarkupfalse%
-\ this\ converse{\isacharunderscore}tranclpE{\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
+\ this\ converse{\isacharunderscore}tranclpE\ {\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
\ thesis\ \isacommand{by}\isamarkupfalse%
\ metis\isanewline
\isacommand{qed}\isamarkupfalse%
@@ -303,9 +318,9 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Alternative rules can also be used for constants that have not
-been defined inductively. For example, the lexicographic order which
-is defined as:%
+\noindent Alternative rules can also be used for constants that have
+ not been defined inductively. For example, the lexicographic order
+ which is defined as:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -333,24 +348,11 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent To make it executable, you can derive the following two rules and prove the
-elimination rule:%
+\noindent To make it executable, you can derive the following two
+ rules and prove the elimination rule:%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
\isadelimquote
%
\endisadelimquote
@@ -372,47 +374,45 @@
%
\endisadelimquote
%
-\isamarkupsubsubsection{Options for values%
+\isamarkupsubsection{Options for values%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-In the presence of higher-order predicates, multiple modes for some predicate could be inferred
-that are not disambiguated by the pattern of the set comprehension.
-To disambiguate the modes for the arguments of a predicate, you can state
-the modes explicitly in the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command.
-Consider the simple predicate \isa{succ}:%
+In the presence of higher-order predicates, multiple modes for some
+ predicate could be inferred that are not disambiguated by the
+ pattern of the set comprehension. To disambiguate the modes for the
+ arguments of a predicate, you can state the modes explicitly in the
+ \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command. Consider the simple predicate \isa{succ}:%
\end{isamarkuptext}%
\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
\isacommand{inductive}\isamarkupfalse%
-\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\isakeyword{where}\isanewline
+\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}succ\ {\isadigit{0}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}succ\ x\ y\ {\isasymLongrightarrow}\ succ\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
-\ succ%
-\isadelimproof
-\ %
-\endisadelimproof
+\ succ\ \isacommand{{\isachardot}}\isamarkupfalse%
%
-\isatagproof
-\isacommand{{\isachardot}}\isamarkupfalse%
+\endisatagquote
+{\isafoldquote}%
%
-\endisatagproof
-{\isafoldproof}%
+\isadelimquote
%
-\isadelimproof
-%
-\endisadelimproof
+\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool},
- \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}.
-The invocation of \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} \isa{{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}} loops, as multiple
-modes for the predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
-is chosen. To choose another mode for the argument, you can declare the mode for the argument between
-the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.%
+\noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and
+ \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}. The invocation of \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}
+ \isa{{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}} loops, as multiple modes for the
+ predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool} is chosen. To choose another mode for the argument,
+ you can declare the mode for the argument between the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -432,41 +432,49 @@
%
\endisadelimquote
%
-\isamarkupsubsubsection{Embedding into functional code within Isabelle/HOL%
+\isamarkupsubsection{Embedding into functional code within Isabelle/HOL%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
-you have a number of options:
-\begin{itemize}
-\item You want to use the first-order predicate with the mode
- where all arguments are input. Then you can use the predicate directly, e.g.
-\begin{quote}
- \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}}\\
- \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}}
-\end{quote}
-\item If you know that the execution returns only one value (it is deterministic), then you can
- use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists
- is defined with
-\begin{quote}
- \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}}
-\end{quote}
- Note that if the evaluation does not return a unique value, it raises a run-time error
- \isa{not{\isacharunderscore}unique}.
-\end{itemize}%
+To embed the computation of an inductive predicate into functions
+ that are defined in Isabelle/HOL, you have a number of options:
+
+ \begin{itemize}
+
+ \item You want to use the first-order predicate with the mode
+ where all arguments are input. Then you can use the predicate directly, e.g.
+
+ \begin{quote}
+ \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}} \\
+ \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}}
+ \end{quote}
+
+ \item If you know that the execution returns only one value (it is
+ deterministic), then you can use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists is
+ defined with
+
+ \begin{quote}
+ \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}}
+ \end{quote}
+
+ Note that if the evaluation does not return a unique value, it
+ raises a run-time error \isa{not{\isacharunderscore}unique}.
+
+ \end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Further Examples%
+\isamarkupsubsection{Further Examples%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Further examples for compiling inductive predicates can be found in
-the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex} theory file.
-There are also some examples in the Archive of Formal Proofs, notably
-in the \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava} sessions.%
+ the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex{\isacharcomma}thy} theory file. There are
+ also some examples in the Archive of Formal Proofs, notably in the
+ \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava}
+ sessions.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Mon Aug 16 10:05:00 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Mon Aug 16 12:11:01 2010 +0200
@@ -22,83 +22,44 @@
}
\isamarkuptrue%
%
-\isamarkupsubsection{Code generation fundamental: shallow embedding%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{A quick start with the \isa{Isabelle{\isacharslash}HOL} toolbox%
-}
+\begin{isamarkuptext}%
+This tutorial introduces the code generator facilities of \isa{Isabelle{\isacharslash}HOL}. It allows to turn (a certain class of) HOL
+ specifications into corresponding executable code in the programming
+ languages \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml} and
+ \isa{Haskell} \cite{haskell-revised-report}.
+
+ To profit from this tutorial, some familiarity and experience with
+ \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \cite{isa-tutorial} and its basic theories is assumed.%
+\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Type classes%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{How to continue from here%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{If something goes utterly wrong%
+\isamarkupsubsection{Code generation principle: shallow embedding \label{sec:principle}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-This tutorial introduces a generic code generator for the
- \isa{Isabelle} system.
- The
- \qn{target language} for which code is
- generated is not fixed, but may be one of several
- functional programming languages (currently, the implementation
- supports \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml} and \isa{Haskell}
- \cite{haskell-revised-report}).
-
- Conceptually the code generator framework is part
- of Isabelle's \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} meta logic framework; the logic
- \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \cite{isa-tutorial}, which is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}},
- already comes with a reasonable framework setup and thus provides
- a good basis for creating code-generation-driven
- applications. So, we assume some familiarity and experience
- with the ingredients of the \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} distribution theories.
-
- The code generator aims to be usable with no further ado
- in most cases, while allowing for detailed customisation.
- This can be seen in the structure of this tutorial: after a short
- conceptual introduction with an example (\secref{sec:intro}),
- we discuss the generic customisation facilities (\secref{sec:program}).
- A further section (\secref{sec:adaptation}) is dedicated to the matter of
- \qn{adaptation} to specific target language environments. After some
- further issues (\secref{sec:further}) we conclude with an overview
- of some ML programming interfaces (\secref{sec:ml}).
-
- \begin{warn}
- Ultimately, the code generator which this tutorial deals with
- is supposed to replace the existing code generator
- by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
- So, for the moment, there are two distinct code generators
- in Isabelle. In case of ambiguity, we will refer to the framework
- described here as \isa{generic\ code\ generator}, to the
- other as \isa{SML\ code\ generator}.
- Also note that while the framework itself is
- object-logic independent, only \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} provides a reasonable
- framework setup.
- \end{warn}%
+The key concept for understanding Isabelle's code generation is
+ \emph{shallow embedding}: logical entities like constants, types and
+ classes are identified with corresponding entities in the target
+ language. In particular, the carrier of a generated program's
+ semantics are \emph{equational theorems} from the logic. If we view
+ a generated program as an implementation of a higher-order rewrite
+ system, then every rewrite step performed by the program can be
+ simulated in the logic, which guarantees partial correctness
+ \cite{Haftmann-Nipkow:2010:code}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Code generation via shallow embedding \label{sec:intro}%
+\isamarkupsubsection{A quick start with the Isabelle/HOL toolbox \label{sec:queue_example}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The key concept for understanding \isa{Isabelle}'s code generation is
- \emph{shallow embedding}, i.e.~logical entities like constants, types and
- classes are identified with corresponding concepts in the target language.
+In a HOL theory, the \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} and \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} declarations form the
+ core of a functional programming language. By default equational
+ theorems stemming from those are used for generated code, therefore
+ \qt{naive} code generation can proceed without further ado.
- Inside \hyperlink{theory.HOL}{\mbox{\isa{HOL}}}, the \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} and
- \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} declarations form
- the core of a functional programming language. The default code generator setup
- transforms those into functional programs immediately.
- This means that \qt{naive} code generation can proceed without further ado.
For example, here a simple \qt{implementation} of amortised queues:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -124,7 +85,7 @@
\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ %
\endisatagquote
{\isafoldquote}%
%
@@ -132,6 +93,19 @@
%
\endisadelimquote
%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
\begin{isamarkuptext}%
\noindent Then we can generate code e.g.~for \isa{SML} as follows:%
\end{isamarkuptext}%
@@ -207,15 +181,14 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command takes a space-separated list of
- constants for which code shall be generated; anything else needed for those
- is added implicitly. Then follows a target language identifier
- (\isa{SML}, \isa{OCaml} or \isa{Haskell}) and a freely chosen module name.
- A file name denotes the destination to store the generated code. Note that
- the semantics of the destination depends on the target language: for
- \isa{SML} and \isa{OCaml} it denotes a \emph{file}, for \isa{Haskell}
- it denotes a \emph{directory} where a file named as the module name
- (with extension \isa{{\isachardot}hs}) is written:%
+\noindent The \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command takes a space-separated
+ list of constants for which code shall be generated; anything else
+ needed for those is added implicitly. Then follows a target
+ language identifier and a freely chosen module name. A file name
+ denotes the destination to store the generated code. Note that the
+ semantics of the destination depends on the target language: for
+ \isa{SML} and \isa{OCaml} it denotes a \emph{file}, for \isa{Haskell} it denotes a \emph{directory} where a file named as the
+ module name (with extension \isa{{\isachardot}hs}) is written:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -235,7 +208,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent This is the corresponding code in \isa{Haskell}:%
+\noindent This is the corresponding code:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -278,97 +251,319 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent This demonstrates the basic usage of the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command;
- for more details see \secref{sec:further}.%
+\noindent For more details about \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} see
+ \secref{sec:further}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{If something utterly fails%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Under certain circumstances, the code generator fails to produce
- code entirely.
-
- \begin{description}
-
- \ditem{generate only one module}
-
- \ditem{check with a different target language}
-
- \ditem{inspect code equations}
-
- \ditem{inspect preprocessor setup}
-
- \ditem{generate exceptions}
-
- \ditem{remove offending code equations}
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Code generator architecture \label{sec:concept}%
+\isamarkupsubsection{Type classes%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-What you have seen so far should be already enough in a lot of cases. If you
- are content with this, you can quit reading here. Anyway, in order to customise
- and adapt the code generator, it is necessary to gain some understanding
- how it works.
-
- \begin{figure}[h]
- \includegraphics{architecture}
- \caption{Code generator architecture}
- \label{fig:arch}
- \end{figure}
+Code can also be generated from type classes in a Haskell-like
+ manner. For illustration here an example from abstract algebra:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{class}\isamarkupfalse%
+\ semigroup\ {\isacharequal}\isanewline
+\ \ \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
+\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{class}\isamarkupfalse%
+\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
+\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instantiation}\isamarkupfalse%
+\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{primrec}\isamarkupfalse%
+\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline
+\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
+\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
+\isacommand{qed}\isamarkupfalse%
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent We define the natural operation of the natural numbers
+ on monoids:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{primrec}\isamarkupfalse%
+\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This we use to define the discrete exponentiation
+ function:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The corresponding code in Haskell uses that language's
+ native classes:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}module Example where {\char123}\\
+\hspace*{0pt}\\
+\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
+\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
+\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
+\hspace*{0pt}\\
+\hspace*{0pt}class Semigroup a where {\char123}\\
+\hspace*{0pt} ~mult ::~a -> a -> a;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
+\hspace*{0pt} ~neutral ::~a;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
+\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
+\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
+\hspace*{0pt}\\
+\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
+\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
+\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
+\hspace*{0pt}\\
+\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
+\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}instance Semigroup Nat where {\char123}\\
+\hspace*{0pt} ~mult = mult{\char95}nat;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}instance Monoid Nat where {\char123}\\
+\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}bexp ::~Nat -> Nat;\\
+\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
+\hspace*{0pt}\\
+\hspace*{0pt}{\char125}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This is a convenient place to show how explicit dictionary
+ construction manifests in generated code -- the same example in
+ \isa{SML}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
+\hspace*{0pt} ~type 'a semigroup\\
+\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
+\hspace*{0pt} ~type 'a monoid\\
+\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
+\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
+\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
+\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
+\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
+\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\
+\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\
+\hspace*{0pt} ~val bexp :~nat -> nat\\
+\hspace*{0pt}end = struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
+\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
+\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
+\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
+\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
+\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
+\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
+\hspace*{0pt}\\
+\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
+\hspace*{0pt} ~:~nat monoid;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
+\hspace*{0pt}\\
+\hspace*{0pt}end;~(*struct Example*)%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Note the parameters with trailing underscore (\verb|A_|), which are the dictionary parameters.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{How to continue from here%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+What you have seen so far should be already enough in a lot of
+ cases. If you are content with this, you can quit reading here.
- The code generator employs a notion of executability
- for three foundational executable ingredients known
- from functional programming:
- \emph{code equations}, \emph{datatypes}, and
- \emph{type classes}. A code equation as a first approximation
- is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t}
- (an equation headed by a constant \isa{f} with arguments
- \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}).
- Code generation aims to turn code equations
- into a functional program. This is achieved by three major
- components which operate sequentially, i.e. the result of one is
- the input
- of the next in the chain, see figure \ref{fig:arch}:
+ Anyway, to understand situations where problems occur or to increase
+ the scope of code generation beyond default, it is necessary to gain
+ some understanding how the code generator actually works:
\begin{itemize}
- \item The starting point is a collection of raw code equations in a
- theory. It is not relevant where they
- stem from, but typically they were either produced by specification
- tools or proved explicitly by the user.
-
- \item These raw code equations can be subjected to theorem transformations. This
- \qn{preprocessor} can apply the full
- expressiveness of ML-based theorem transformations to code
- generation. The result of preprocessing is a
- structured collection of code equations.
+ \item The foundations of the code generator are described in
+ \secref{sec:foundations}.
+
+ \item In particular \secref{sec:utterly_wrong} gives hints how to
+ debug situations where code generation does not succeed as
+ expected.
- \item These code equations are \qn{translated} to a program in an
- abstract intermediate language. Think of it as a kind
- of \qt{Mini-Haskell} with four \qn{statements}: \isa{data}
- (for datatypes), \isa{fun} (stemming from code equations),
- also \isa{class} and \isa{inst} (for type classes).
+ \item The scope and quality of generated code can be increased
+ dramatically by applying refinement techniques, which are
+ introduced in \secref{sec:refinement}.
- \item Finally, the abstract program is \qn{serialised} into concrete
- source code of a target language.
- This step only produces concrete syntax but does not change the
- program in essence; all conceptual transformations occur in the
- translation step.
+ \item Inductive predicates can be turned executable using an
+ extension of the code generator \secref{sec:inductive}.
+
+ \item You may want to skim over the more technical sections
+ \secref{sec:adaptation} and \secref{sec:further}.
+
+ \item For exhaustive syntax diagrams etc. you should visit the
+ Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}.
\end{itemize}
- \noindent From these steps, only the two last are carried out outside the logic; by
- keeping this layer as thin as possible, the amount of code to trust is
- kept to a minimum.%
+ \bigskip
+
+ \begin{center}\fbox{\fbox{\begin{minipage}{8cm}
+
+ \begin{center}\textit{Happy proving, happy hacking!}\end{center}
+
+ \end{minipage}}}\end{center}
+
+ \begin{warn}
+ There is also a more ancient code generator in Isabelle by Stefan
+ Berghofer \cite{Berghofer-Nipkow:2002}. Although its
+ functionality is covered by the code generator presented here, it
+ will sometimes show up as an artifact. In case of ambiguity, we
+ will refer to the framework described here as \isa{generic\ code\ generator}, to the other as \isa{SML\ code\ generator}.
+ \end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Refinement.tex Mon Aug 16 10:05:00 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Mon Aug 16 12:11:01 2010 +0200
@@ -22,6 +22,227 @@
}
\isamarkuptrue%
%
+\isamarkupsubsection{Datatypes \label{sec:datatypes}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Conceptually, any datatype is spanned by a set of
+ \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
+ \isa{{\isasymtau}}. The HOL datatype package by default registers any new
+ datatype in the table of datatypes, which may be inspected using the
+ \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
+
+ In some cases, it is appropriate to alter or extend this table. As
+ an example, we will develop an alternative representation of the
+ queue example given in \secref{sec:queue_example}. The amortised
+ representation is convenient for generating code but exposes its
+ \qt{implementation} details, which may be cumbersome when proving
+ theorems about it. Therefore, here is a simple, straightforward
+ representation of queues:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{datatype}\isamarkupfalse%
+\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{primrec}\isamarkupfalse%
+\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{fun}\isamarkupfalse%
+\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This we can use directly for proving; for executing,
+ we provide an alternative characterisation:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
+\ AQueue%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Here we define a \qt{constructor} \isa{AQueue} which
+ is defined in terms of \isa{Queue} and interprets its arguments
+ according to what the \emph{content} of an amortised queue is supposed
+ to be. Equipped with this, we are able to prove the following equations
+ for our primitive queue operations which \qt{implement} the simple
+ queues in an amortised fashion:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp{\isacharunderscore}all%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent For completeness, we provide a substitute for the
+ \isa{case} combinator on queues:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The resulting code looks as expected:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val rev :~'a list -> 'a list\\
+\hspace*{0pt} ~val null :~'a list -> bool\\
+\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
+\hspace*{0pt} ~val empty :~'a queue\\
+\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
+\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
+\hspace*{0pt}end = struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun foldl f a [] = a\\
+\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun null [] = true\\
+\hspace*{0pt} ~| null (x ::~xs) = false;\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
+\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
+\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
+\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
+\hspace*{0pt}\\
+\hspace*{0pt}end;~(*struct Example*)%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent From this example, it can be glimpsed that using own
+ constructor sets is a little delicate since it changes the set of
+ valid patterns for values of that type. Without going into much
+ detail, here some practical hints:
+
+ \begin{itemize}
+
+ \item When changing the constructor set for datatypes, take care
+ to provide alternative equations for the \isa{case} combinator.
+
+ \item Values in the target language need not to be normalised --
+ different values in the target language may represent the same
+ value in the logic.
+
+ \item Usually, a good methodology to deal with the subtleties of
+ pattern matching is to see the type as an abstract type: provide
+ a set of operations which operate on the concrete representation
+ of the type, and derive further operations by combinations of
+ these primitive ones, without relying on a particular
+ representation.
+
+ \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/manual.bib Mon Aug 16 10:05:00 2010 +0100
+++ b/doc-src/manual.bib Mon Aug 16 12:11:01 2010 +0200
@@ -520,10 +520,10 @@
title = {Code Generation via Higher-Order Rewrite Systems},
booktitle = {Functional and Logic Programming: 10th International Symposium: FLOPS 2010},
year = 2010,
- publisher = {Springer},
- series = {Lecture Notes in Computer Science},
+ publisher = Springer,
+ series = LNCS,
editor = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal},
- volume = {6009}
+ volume = 6009
}
@InProceedings{Haftmann-Wenzel:2009,
--- a/src/Pure/Isar/class_declaration.ML Mon Aug 16 10:05:00 2010 +0100
+++ b/src/Pure/Isar/class_declaration.ML Mon Aug 16 12:11:01 2010 +0200
@@ -130,8 +130,8 @@
| _ => error "Multiple type variables in class specification.";
in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
fun add_typ_check level name f = Context.proof_map
- (Syntax.add_typ_check level name (fn xs => fn ctxt =>
- let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
+ (Syntax.add_typ_check level name (fn Ts => fn ctxt =>
+ let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end));
(* preprocessing elements, retrieving base sort from type-checked elements *)
val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
@@ -140,16 +140,21 @@
#> add_typ_check ~10 "singleton_fixate" singleton_fixate;
val raw_supexpr = (map (fn sup => (sup, (("", false),
Expression.Positional []))) sups, []);
- val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy
+ val ((raw_supparams, _, raw_inferred_elems), _) = ProofContext.init_global thy
|> prep_decl raw_supexpr init_class_body raw_elems;
+ fun filter_element (Element.Fixes []) = NONE
+ | filter_element (e as Element.Fixes _) = SOME e
+ | filter_element (Element.Constrains []) = NONE
+ | filter_element (e as Element.Constrains _) = SOME e
+ | filter_element (Element.Assumes []) = NONE
+ | filter_element (e as Element.Assumes _) = SOME e
+ | filter_element (Element.Defines _) = error ("\"defines\" element not allowed in class specification.")
+ | filter_element (Element.Notes _) = error ("\"notes\" element not allowed in class specification.");
+ val inferred_elems = map_filter filter_element raw_inferred_elems;
fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
| fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
| fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
fold_types f t #> (fold o fold_types) f ts) o snd) assms
- | fold_element_types f (Element.Defines _) =
- error ("\"defines\" element not allowed in class specification.")
- | fold_element_types f (Element.Notes _) =
- error ("\"notes\" element not allowed in class specification.");
val base_sort = if null inferred_elems then proto_base_sort else
case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
of [] => error "No type variable in class specification"