author haftmann Fri, 30 Mar 2007 16:18:59 +0200 changeset 22550 c5039bee2602 parent 22549 ab23925c64d6 child 22551 e52f5400e331
updated
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Thu Mar 29 14:21:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Mar 30 16:18:59 2007 +0200
@@ -80,7 +80,7 @@
As a canonical example, a polymorphic equality function
@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different
-  types for @{text "\<alpha>"}, which is achieves by splitting introduction
+  types for @{text "\<alpha>"}, which is achieved by splitting introduction
of the @{text eq} function from its overloaded definitions by means
of @{text class} and @{text instance} declarations:

@@ -94,13 +94,13 @@
\hspace*{4ex}@{text "eq (Suc n) (Suc m) = eq n m"}

\medskip\noindent\hspace*{2ex}@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
-  \hspace*{4ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 && eq y1 y2"}
+  \hspace*{4ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}

\medskip\noindent\hspace*{2ex}@{text "class ord extends eq where"} \\
\hspace*{4ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
\hspace*{4ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}

-  \medskip Type variables are annotated with (finitly many) classes;
+  \medskip\noindent Type variables are annotated with (finitly many) classes;
these annotations are assertions that a particular polymorphic type

@@ -113,7 +113,9 @@
so, it is naturally desirable that type classes do not only
provide functions (class operations) but also state specifications
implementations must obey.  For example, the @{text "class eq"}
-  above could be given the following specification:
+  above could be given the following specification, demanding that
+  @{text "class eq"} is an equivalence relation obeying reflexivity,
+  symmetry and transitivity:

\medskip\noindent\hspace*{2ex}@{text "class eq where"} \\
\hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
@@ -122,7 +124,7 @@
\hspace*{4ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
\hspace*{4ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}

-  \medskip From a theoretic point of view, type classes are leightweight
+  \medskip\noindent From a theoretic point of view, type classes are leightweight
modules; Haskell type classes may be emulated by
SML functors \cite{classes_modules}.
Isabelle/Isar offers a discipline of type classes which brings
@@ -137,8 +139,8 @@
\item with a direct link to the Isabelle module system (aka locales).
\end{enumerate}

-  Isar type classes also directly support code generation
-  in as Haskell like fashion.
+  \noindent Isar type classes also directly support code generation
+  in a Haskell like fashion.

This tutorial demonstrates common elements of structured specifications
and abstract reasoning with type classes by the algebraic hierarchy of
@@ -203,7 +205,7 @@
proof goals and should conveniently always be the first method applied
in an instantiation proof.

-  Another instance of @{text "semigroup"} are the natural numbers:
+  \medskip Another instance of @{text "semigroup"} are the natural numbers:
*}

instance nat :: semigroup
@@ -214,7 +216,7 @@
qed

text {*
-  Also @{text "list"}s form a semigroup with @{const "op @"} as
+  \noindent Also @{text "list"}s form a semigroup with @{const "op @"} as
operation:
*}

@@ -319,7 +321,8 @@
proof
fix i :: int
have "-i + i = 0" by simp
-      then show "i\<div> \<otimes> i = \<one>" unfolding mult_int_def and neutral_int_def and inverse_int_def .
+      then show "i\<div> \<otimes> i = \<one>"
+      unfolding mult_int_def and neutral_int_def and inverse_int_def .
qed

section {* Type classes as locales *}
@@ -340,28 +343,29 @@
text {*
\noindent essentially introduces the locale
*}
-
(*<*) setup {* Sign.add_path "foo" *} (*>*)
-
locale idem =
fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
assumes idem: "f (f x) = f x"

-text {* \noindent together with corresponding constant(s) and axclass *}
+text {* \noindent together with corresponding constant(s): *}

consts f :: "\<alpha> \<Rightarrow> \<alpha>"

+text {*
+  \noindent The connection to the type system is done by means
+  of a primitive axclass
+*}
+
axclass idem < type
idem: "f (f x) = f x"

-text {* This axclass is coupled to the locale by means of an interpretation: *}
+text {* \noindent together with a corresponding interpretation: *}

interpretation idem_class:
idem ["f \<Colon> ('a\<Colon>idem) \<Rightarrow> \<alpha>"]
by unfold_locales (rule idem)
-
(*<*) setup {* Sign.parent_path *} (*>*)
-
text {*
This give you at hand the full power of the Isabelle module system;
conclusions in locale @{text idem} are implicitly propagated
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Mar 29 14:21:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Mar 30 16:18:59 2007 +0200
@@ -59,7 +59,7 @@
As a canonical example, a polymorphic equality function
\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different
-  types for \isa{{\isasymalpha}}, which is achieves by splitting introduction
+  types for \isa{{\isasymalpha}}, which is achieved by splitting introduction
of the \isa{eq} function from its overloaded definitions by means
of \isa{class} and \isa{instance} declarations:

@@ -73,13 +73,13 @@
\hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}

\medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\

\medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\
\hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
\hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}

-  \medskip Type variables are annotated with (finitly many) classes;
+  \medskip\noindent Type variables are annotated with (finitly many) classes;
these annotations are assertions that a particular polymorphic type

@@ -92,7 +92,9 @@
so, it is naturally desirable that type classes do not only
provide functions (class operations) but also state specifications
implementations must obey.  For example, the \isa{class\ eq}
-  above could be given the following specification:
+  above could be given the following specification, demanding that
+  \isa{class\ eq} is an equivalence relation obeying reflexivity,
+  symmetry and transitivity:

\medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\
\hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
@@ -101,7 +103,7 @@
\hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
\hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}

-  \medskip From a theoretic point of view, type classes are leightweight
+  \medskip\noindent From a theoretic point of view, type classes are leightweight
modules; Haskell type classes may be emulated by
SML functors \cite{classes_modules}.
Isabelle/Isar offers a discipline of type classes which brings
@@ -116,8 +118,8 @@
\item with a direct link to the Isabelle module system (aka locales).
\end{enumerate}

-  Isar type classes also directly support code generation
-  in as Haskell like fashion.
+  \noindent Isar type classes also directly support code generation
+  in a Haskell like fashion.

This tutorial demonstrates common elements of structured specifications
and abstract reasoning with type classes by the algebraic hierarchy of
@@ -207,7 +209,7 @@
proof goals and should conveniently always be the first method applied
in an instantiation proof.

-  Another instance of \isa{semigroup} are the natural numbers:%
+  \medskip Another instance of \isa{semigroup} are the natural numbers:%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \ \ \isacommand{instance}\isamarkupfalse%
@@ -237,7 +239,7 @@
%
\begin{isamarkuptext}%
-Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as
+\noindent Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as
operation:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -489,7 +491,8 @@
\ simp\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
+\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ neutral{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
@@ -537,23 +540,26 @@
%
-\isanewline
\isacommand{locale}\isamarkupfalse%
\ idem\ {\isacharequal}\isanewline
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-\noindent together with corresponding constant(s) and axclass%
+\noindent together with corresponding constant(s):%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isamarkupfalse%
-\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
-\isanewline
+\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent The connection to the type system is done by means
+  of a primitive axclass%
+\end{isamarkuptext}%
+\isamarkuptrue%
\isacommand{axclass}\isamarkupfalse%
\ idem\ {\isacharless}\ type\isanewline
\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-This axclass is coupled to the locale by means of an interpretation:%
+together with a corresponding interpretation:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{interpretation}\isamarkupfalse%
@@ -566,8 +572,7 @@
%
\isatagproof
\isacommand{by}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}\isanewline
-%
+\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Mar 29 14:21:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Mar 30 16:18:59 2007 +0200
@@ -26,7 +26,7 @@
for running test cases and rapid prototyping.  In logical
calculi like constructive type theory,
a notion of executability is implicit due to the nature
-  of the calculus.  In contrast, specifications in Isabelle/HOL
+  of the calculus.  In contrast, specifications in Isabelle
can be highly non-executable.  In order to bridge
the gap between logic and executable specifications,
an explicit non-trivial transformation has to be applied:
@@ -38,7 +38,8 @@
\qn{target language} for which code shall ultimately be
generated is not fixed but may be an arbitrary state-of-the-art
functional programming language (currently, the implementation
+  supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell
We aim to provide a
versatile environment
suitable for software development and verification,
@@ -47,9 +48,14 @@
while achieving a big coverage of application areas
with maximum flexibility.

-  For readers, some familiarity and experience
-  with the ingredients
-  of the HOL \emph{Main} theory is assumed.
+  Conceptually the code generator framework is part
+  of Isabelle's @{text Pure} meta logic; the object logic
+  @{text HOL} which is an extension of @{text Pure}
+  already comes with a reasonable framework setup and thus provides
+  a good working horse for raising code-generation-driven
+  applications.  So, we assume some familiarity and experience
+  with the ingredients of the @{text HOL} \emph{Main} theory
*}

@@ -58,8 +64,10 @@
text {*
The code generator aims to be usable with no further ado
in most cases while allowing for detailed customization.
-  This manifests in the structure of this tutorial: this introduction
-  continues with a short introduction of concepts.  Section
+  This manifests in the structure of this tutorial:
+  and introduce code generation concepts \secref{sec:concept}.
+  Section
\secref{sec:basics} explains how to use the framework naively,
presuming a reasonable default setup.  Then, section
@@ -74,17 +82,34 @@
So, for the moment, there are two distinct code generators
in Isabelle.
Also note that while the framework itself is largely
-    object-logic independent, only HOL provides a reasonable
+    object-logic independent, only @{text HOL} provides a reasonable
framework setup.
\end{warn}
*}

-subsection {* An exmaple: a simple theory of search trees *}
+section {* An example: a simple theory of search trees \label{sec:example} *}
+
+text {*
+  When writing executable specifications, it is convenient to use
+  three existing packages: the datatype package for defining
+  datatypes, the function package for (recursive) functions,
+  and the class package for overloaded definitions.
+
+  We develope a small theory of search trees; trees are represented
+  as a datatype with key type @{typ "'a"} and value type @{typ "'b"}:
+*}

datatype ('a, 'b) searchtree = Leaf "'a\<Colon>linorder" 'b
| Branch "('a, 'b) searchtree" "'a" "('a, 'b) searchtree"

+text {*
+  \noindent Note that we have constrained the type of keys
+  to the class of total orders, @{text linorder}.
+
+  We define @{text find} and @{text update} functions:
+*}
+
fun
find :: "('a\<Colon>linorder, 'b) searchtree \<Rightarrow> 'a \<Rightarrow> 'b option" where
"find (Leaf key val) it = (if it = key then Some val else None)"
@@ -104,17 +129,29 @@
else (Branch t1 key (update (it, entry) t2))
)"

+text {*
+  \noindent For testing purpose, we define a small example
+  using natural numbers @{typ nat} (which are a @{text linorder})
+  as keys and strings values:
+*}
+
fun
example :: "nat \<Rightarrow> (nat, string) searchtree" where
"example n = update (n, ''bar'') (Leaf 0 ''foo'')"

+text {*
+  \noindent Then we generate code
+*}
+
code_gen example (*<*)(SML #)(*>*)(SML "examples/tree.ML")

text {*
+  \noindent which looks like:
\lstsml{Thy/examples/tree.ML}
*}

-subsection {* Code generation process *}
+
+section {* Code generation concepts and process \label{sec:concept} *}

text {*
\begin{figure}[h]
@@ -181,13 +218,13 @@
| "fac (Suc n) = Suc n * fac n"

text {*
-  This executable specification is now turned to SML code:
+  \noindent This executable specification is now turned to SML code:
*}

code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac.ML")

text {*
-  The @{text "\<CODEGEN>"} command takes a space-separated list of
+  \noindent  The @{text "\<CODEGEN>"} command takes a space-separated list of
constants together with \qn{serialization directives}
identifier, followed by arguments, their semantics
@@ -202,40 +239,11 @@
\lstsml{Thy/examples/fac.ML}

The code generator will complain when a required
-  ingredient does not provide a executable counterpart.
-  This is the case if an involved type is not a datatype:
-*}
-
-(*<*)
-(*>*)
-
-typedecl 'a foo
-
-definition
-  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "bar x y = y"
-
-(*<*)
-hide type foo
-hide const bar
-
-setup {* Sign.parent_path *}
-
-datatype 'a foo = Foo
-
-definition
-  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "bar x y = y"
-(*>*)
-
-code_gen bar (SML "examples/fail_type.ML")
-
-text {*
-  \noindent will result in an error. Likewise, generating code
+  ingredient does not provide a executable counterpart,
+  e.g.~generating code
for constants not yielding
-  a defining equation will fail, e.g.~the Hilbert choice
-  operation @{text "SOME"}:
+  a defining equation (e.g.~the Hilbert choice
+  operation @{text "SOME"}):
*}

(*<*)
@@ -258,6 +266,8 @@

code_gen pick_some (SML "examples/fail_const.ML")

+text {* \noindent will fail. *}
+
subsection {* Theorem selection *}

text {*
@@ -271,8 +281,9 @@
\noindent which displays a table of constant with corresponding
defining equations (the additional stuff displayed
shall not bother us for the moment). If this table does
-  not provide at least one function
-  equation, the table of primitive definitions is searched
+  not provide at least one defining
+  equation for a particular constant, the table of primitive
+  definitions is searched
whether it provides one.

The typical HOL tools are already set up in a way that
@@ -447,9 +458,13 @@
any applied transformation).  A
list of constants may be given; their function
+
+  Similarly, the @{text "\<CODEDEPS>"} command shows a graph
+  visualizing dependencies between defining equations.
*}

+

text {*
@@ -1020,6 +1035,14 @@
sort constraint by hand.
*}

+
+subsection {* Constructor sets for datatypes *}
+
+text {*
+  \fixme
+*}
+
+
subsection {* Cyclic module dependencies *}

text {*
@@ -1147,9 +1170,8 @@

text %mlref {*
\begin{mldecls}
-  @{index_ML_type CodegenConsts.const: "string * typ list"} \\
-  @{index_ML CodegenConsts.norm_of_typ: "theory -> string * typ -> CodegenConsts.const"} \\
-  @{index_ML CodegenConsts.typ_of_inst: "theory -> CodegenConsts.const -> string * typ"} \\
+  @{index_ML_type CodegenConsts.const: "string * string option"} \\
+  @{index_ML CodegenConsts.const_of_cexpr: "theory -> string * typ -> CodegenConsts.const"} \\
\end{mldecls}

\begin{description}
@@ -1157,15 +1179,13 @@
\item @{ML_type CodegenConsts.const} is the identifier type:
the product of a \emph{string} with a list of \emph{typs}.
The \emph{string} is the constant name as represented inside Isabelle;
-     the \emph{typs} are a type instantiation in the sense of System F,
-     with canonical names for type variables.
+     for overloaded constants, the attached \emph{string option}
+     is either @{text SOME} type constructor denoting an instance,
+     or @{text NONE} for the polymorphic constant.

-  \item @{ML CodegenConsts.norm_of_typ}~@{text thy}~@{text "(constname, typ)"}
-     maps a constant expression @{text "(constname, typ)"} to its canonical identifier.
-
-  \item @{ML CodegenConsts.typ_of_inst}~@{text thy}~@{text const}
-     maps a canonical identifier @{text const} to a constant
-     expression with appropriate type.
+  \item @{ML CodegenConsts.const_of_cexpr}~@{text thy}~@{text "(constname, typ)"}
+     maps a constant expression @{text "(constname, typ)"}
+     to its canonical identifier.

\end{description}
*}
@@ -1196,7 +1216,7 @@

text %mlref {*
\begin{mldecls}
-  @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\
+  @{index_ML CodegenData.add_func: "bool -> thm -> theory -> theory"} \\
@{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\
@{index_ML CodegenData.add_funcl: "CodegenConsts.const * thm list Susp.T -> theory -> theory"} \\
@{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\
@@ -1272,7 +1292,6 @@
\begin{mldecls}
@{index_ML CodegenConsts.const_ord: "CodegenConsts.const * CodegenConsts.const -> order"} \\
@{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\
-  @{index_ML CodegenConsts.consts_of: "theory -> term -> CodegenConsts.const list"} \\
@{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\
@{index_ML_structure CodegenConsts.Consttab} \\
@{index_ML CodegenFunc.typ_func: "thm -> typ"} \\
@@ -1287,9 +1306,6 @@
\item @{ML_struct CodegenConsts.Consttab}
provides table structures with constant identifiers as keys.

-  \item @{ML CodegenConsts.consts_of}~@{text thy}~@{text t}
-     returns all constant identifiers mentioned in a term @{text t}.
-
reads a constant as a concrete term expression @{text s}.

--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Mar 29 14:21:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri Mar 30 16:18:59 2007 +0200
@@ -49,7 +49,7 @@
for running test cases and rapid prototyping.  In logical
calculi like constructive type theory,
a notion of executability is implicit due to the nature
-  of the calculus.  In contrast, specifications in Isabelle/HOL
+  of the calculus.  In contrast, specifications in Isabelle
can be highly non-executable.  In order to bridge
the gap between logic and executable specifications,
an explicit non-trivial transformation has to be applied:
@@ -61,7 +61,8 @@
\qn{target language} for which code shall ultimately be
generated is not fixed but may be an arbitrary state-of-the-art
functional programming language (currently, the implementation
+  supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell
We aim to provide a
versatile environment
suitable for software development and verification,
@@ -70,9 +71,14 @@
while achieving a big coverage of application areas
with maximum flexibility.

-  For readers, some familiarity and experience
-  with the ingredients
-  of the HOL \emph{Main} theory is assumed.%
+  Conceptually the code generator framework is part
+  of Isabelle's \isa{Pure} meta logic; the object logic
+  \isa{HOL} which is an extension of \isa{Pure}
+  already comes with a reasonable framework setup and thus provides
+  a good working horse for raising code-generation-driven
+  applications.  So, we assume some familiarity and experience
+  with the ingredients of the \isa{HOL} \emph{Main} theory
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -83,8 +89,10 @@
\begin{isamarkuptext}%
The code generator aims to be usable with no further ado
in most cases while allowing for detailed customization.
-  This manifests in the structure of this tutorial: this introduction
-  continues with a short introduction of concepts.  Section
+  This manifests in the structure of this tutorial:
+  and introduce code generation concepts \secref{sec:concept}.
+  Section
\secref{sec:basics} explains how to use the framework naively,
presuming a reasonable default setup.  Then, section
@@ -99,19 +107,36 @@
So, for the moment, there are two distinct code generators
in Isabelle.
Also note that while the framework itself is largely
-    object-logic independent, only HOL provides a reasonable
+    object-logic independent, only \isa{HOL} provides a reasonable
framework setup.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{An exmaple: a simple theory of search trees%
+\isamarkupsection{An example: a simple theory of search trees \label{sec:example}%
}
\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+When writing executable specifications, it is convenient to use
+  three existing packages: the datatype package for defining
+  datatypes, the function package for (recursive) functions,
+  and the class package for overloaded definitions.
+
+  We develope a small theory of search trees; trees are represented
+  as a datatype with key type \isa{{\isacharprime}a} and value type \isa{{\isacharprime}b}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isacharequal}\ Leaf\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}linorder{\isachardoublequoteclose}\ {\isacharprime}b\isanewline
-\ \ {\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\isanewline
-\isanewline
+\ \ {\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent Note that we have constrained the type of keys
+  to the class of total orders, \isa{linorder}.
+
+  We define \isa{find} and \isa{update} functions:%
+\end{isamarkuptext}%
+\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\isanewline
\ \ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isasymColon}linorder{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
@@ -131,21 +156,30 @@
\ \ \ \ if\ it\ {\isasymle}\ key\isanewline
\ \ \ \ \ \ then\ {\isacharparenleft}Branch\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{1}}{\isacharparenright}\ key\ t{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ else\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{2}}{\isacharparenright}{\isacharparenright}\isanewline
-\ \ \ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
+\ \ \ {\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent For testing purpose, we define a small example
+  using natural numbers \isa{nat} (which are a \isa{linorder})
+  as keys and strings values:%
+\end{isamarkuptext}%
+\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\isanewline
\ \ example\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharparenleft}nat{\isacharcomma}\ string{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}example\ n\ {\isacharequal}\ update\ {\isacharparenleft}n{\isacharcomma}\ {\isacharprime}{\isacharprime}bar{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}Leaf\ {\isadigit{0}}\ {\isacharprime}{\isacharprime}foo{\isacharprime}{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
+\ \ {\isachardoublequoteopen}example\ n\ {\isacharequal}\ update\ {\isacharparenleft}n{\isacharcomma}\ {\isacharprime}{\isacharprime}bar{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}Leaf\ {\isadigit{0}}\ {\isacharprime}{\isacharprime}foo{\isacharprime}{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent Then we generate code%
+\end{isamarkuptext}%
+\isamarkuptrue%
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
\ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
\begin{isamarkuptext}%
-\lstsml{Thy/examples/tree.ML}%
+\noindent which looks like:
+  \lstsml{Thy/examples/tree.ML}%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Code generation process%
+\isamarkupsection{Code generation concepts and process \label{sec:concept}%
}
\isamarkuptrue%
%
@@ -217,13 +251,13 @@
\ \ {\isacharbar}\ {\isachardoublequoteopen}fac\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharasterisk}\ fac\ n{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-This executable specification is now turned to SML code:%
+\noindent This executable specification is now turned to SML code:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
\ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
\begin{isamarkuptext}%
-The \isa{{\isasymCODEGEN}} command takes a space-separated list of
+\noindent  The \isa{{\isasymCODEGEN}} command takes a space-separated list of
constants together with \qn{serialization directives}
identifier, followed by arguments, their semantics
@@ -238,52 +272,11 @@
\lstsml{Thy/examples/fac.ML}

The code generator will complain when a required
-  ingredient does not provide a executable counterpart.
-  This is the case if an involved type is not a datatype:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-%
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isanewline
-%
-\isacommand{typedecl}\isamarkupfalse%
-\ {\isacharprime}a\ foo\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ bar\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ foo\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}bar\ x\ y\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
-%
-%
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-%
-\isanewline
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ bar\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}type{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent will result in an error. Likewise, generating code
+  ingredient does not provide a executable counterpart,
+  e.g.~generating code
for constants not yielding
-  a defining equation will fail, e.g.~the Hilbert choice
-  operation \isa{SOME}:%
+  a defining equation (e.g.~the Hilbert choice
+  operation \isa{SOME}):%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -320,6 +313,11 @@
\isanewline
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
\ pick{\isacharunderscore}some\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent will fail.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Theorem selection%
}
\isamarkuptrue%
@@ -335,8 +333,9 @@
\noindent which displays a table of constant with corresponding
defining equations (the additional stuff displayed
shall not bother us for the moment). If this table does
-  not provide at least one function
-  equation, the table of primitive definitions is searched
+  not provide at least one defining
+  equation for a particular constant, the table of primitive
+  definitions is searched
whether it provides one.

The typical HOL tools are already set up in a way that
@@ -578,7 +577,10 @@
\noindent print all cached defining equations (i.e.~\emph{after}
any applied transformation).  A
list of constants may be given; their function
+
+  Similarly, the \isa{{\isasymCODEDEPS}} command shows a graph
+  visualizing dependencies between defining equations.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1491,6 +1493,15 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Constructor sets for datatypes%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\fixme%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Cyclic module dependencies%
}
\isamarkuptrue%
@@ -1636,9 +1647,8 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
-  \indexmltype{CodegenConsts.const}\verb|type CodegenConsts.const = string * typ list| \\
-  \indexml{CodegenConsts.norm-of-typ}\verb|CodegenConsts.norm_of_typ: theory -> string * typ -> CodegenConsts.const| \\
-  \indexml{CodegenConsts.typ-of-inst}\verb|CodegenConsts.typ_of_inst: theory -> CodegenConsts.const -> string * typ| \\
+  \indexmltype{CodegenConsts.const}\verb|type CodegenConsts.const = string * string option| \\
+  \indexml{CodegenConsts.const-of-cexpr}\verb|CodegenConsts.const_of_cexpr: theory -> string * typ -> CodegenConsts.const| \\
\end{mldecls}

\begin{description}
@@ -1646,15 +1656,13 @@
\item \verb|CodegenConsts.const| is the identifier type:
the product of a \emph{string} with a list of \emph{typs}.
The \emph{string} is the constant name as represented inside Isabelle;
-     the \emph{typs} are a type instantiation in the sense of System F,
-     with canonical names for type variables.
+     for overloaded constants, the attached \emph{string option}
+     is either \isa{SOME} type constructor denoting an instance,
+     or \isa{NONE} for the polymorphic constant.

-  \item \verb|CodegenConsts.norm_of_typ|~\isa{thy}~\isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}}
-     maps a constant expression \isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}} to its canonical identifier.
-
-  \item \verb|CodegenConsts.typ_of_inst|~\isa{thy}~\isa{const}
-     maps a canonical identifier \isa{const} to a constant
-     expression with appropriate type.
+  \item \verb|CodegenConsts.const_of_cexpr|~\isa{thy}~\isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}}
+     maps a constant expression \isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}}
+     to its canonical identifier.

\end{description}%
\end{isamarkuptext}%
@@ -1720,7 +1728,7 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{CodegenData.del-func}\verb|CodegenData.del_func: thm -> theory -> theory| \\
@@ -1812,7 +1820,6 @@
\begin{mldecls}
\indexml{CodegenConsts.const-ord}\verb|CodegenConsts.const_ord: CodegenConsts.const * CodegenConsts.const -> order| \\
\indexml{CodegenConsts.eq-const}\verb|CodegenConsts.eq_const: CodegenConsts.const * CodegenConsts.const -> bool| \\
-  \indexml{CodegenConsts.consts-of}\verb|CodegenConsts.consts_of: theory -> term -> CodegenConsts.const list| \\
\indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\
\indexml{CodegenFunc.typ-func}\verb|CodegenFunc.typ_func: thm -> typ| \\
@@ -1827,9 +1834,6 @@
\item \verb|CodegenConsts.Consttab|
provides table structures with constant identifiers as keys.

-  \item \verb|CodegenConsts.consts_of|~\isa{thy}~\isa{t}
-     returns all constant identifiers mentioned in a term \isa{t}.
-
reads a constant as a concrete term expression \isa{s}.

--- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Thu Mar 29 14:21:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Fri Mar 30 16:18:59 2007 +0200
@@ -33,6 +33,7 @@
\newcommand{\isasymNOTE}{\cmd{note}}
\newcommand{\isasymIN}{\cmd{in}}
\newcommand{\isasymCODEGEN}{\cmd{code\_gen}}
+\newcommand{\isasymCODEDATATYPE}{\cmd{code\_datatype}}
\newcommand{\isasymCODECONST}{\cmd{code\_const}}
\newcommand{\isasymCODETYPE}{\cmd{code\_type}}
\newcommand{\isasymCODECLASS}{\cmd{code\_class}}
@@ -44,6 +45,7 @@
\newcommand{\isasymCODEABSTYPE}{\cmd{code\_abstype}}
\newcommand{\isasymPRINTCODESETUP}{\cmd{print\_codesetup}}
\newcommand{\isasymCODETHMS}{\cmd{code\_thms}}
+\newcommand{\isasymCODEDEPS}{\cmd{code\_deps}}
\newcommand{\isasymFUN}{\cmd{fun}}
\newcommand{\isasymFUNCTION}{\cmd{function}}
\newcommand{\isasymPRIMREC}{\cmd{primrec}}
Binary file doc-src/IsarAdvanced/Codegen/codegen_process.pdf has changed
--- a/doc-src/IsarAdvanced/Codegen/codegen_process.ps	Thu Mar 29 14:21:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen_process.ps	Fri Mar 30 16:18:59 2007 +0200
@@ -1,5 +1,5 @@
-%%Creator: dot version 2.2 (Tue Mar 22 18:02:44 UTC 2005)
+%%Creator: dot version 2.2 (Mon Sep 12 23:33:36 UTC 2005)
%%For: (haftmann) Florian Haftmann
%%Title: _anonymous_0
%%Pages: (atend)
@@ -369,39 +369,39 @@
stroke
end grestore

-%	code_thm
+%	def_eqn
gsave 10 dict begin
-newpath 392 198 moveto
-294 198 lineto
-294 162 lineto
-392 162 lineto
+newpath 403 198 moveto
+283 198 lineto
+283 162 lineto
+403 162 lineto
closepath
stroke
gsave 10 dict begin
-302 175 moveto
-(code theorems)
-[6.24 6.96 6.96 6.24 3.6 4.08 6.96 6.24 6.96 4.56 6.24 10.8 5.52]
+291 175 moveto
+(defining equations)
+[6.96 6.24 4.8 3.84 6.96 3.84 6.96 6.96 3.6 6.24 6.72 6.96 6.24 3.84 3.84 6.96 6.96 5.52]
xshow
end grestore
end grestore

-%	preprocessing -> code_thm
+%	preprocessing -> def_eqn
newpath 236 180 moveto
-252 180 268 180 284 180 curveto
+248 180 260 180 273 180 curveto
stroke
gsave 10 dict begin
solid
1 setlinewidth
0.000 0.000 0.000 edgecolor
-newpath 284 184 moveto
-294 180 lineto
-284 177 lineto
+newpath 273 184 moveto
+283 180 lineto
+273 177 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-newpath 284 184 moveto
-294 180 lineto
-284 177 lineto
+newpath 273 184 moveto
+283 180 lineto
+273 177 lineto
closepath
stroke
end grestore
@@ -484,19 +484,19 @@
stroke
end grestore

-%	extraction
+%	translation
gsave 10 dict begin
-343 126 41 18 ellipse_path
+343 126 43 18 ellipse_path
stroke
gsave 10 dict begin
-315 121 moveto
-(extraction)
-[5.76 6.96 3.84 4.56 6.24 6.24 3.84 3.84 6.96 6.96]
+313 121 moveto
+(translation)
+[3.84 4.56 6.24 6.96 5.52 3.84 6.24 3.84 3.84 6.96 6.96]
xshow
end grestore
end grestore

-%	code_thm -> extraction
+%	def_eqn -> translation
newpath 343 162 moveto
343 159 343 157 343 154 curveto
stroke
@@ -533,7 +533,7 @@
end grestore
end grestore

-%	extraction -> iml
+%	translation -> iml
newpath 343 108 moveto
343 105 343 103 343 100 curveto
stroke
--- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Mar 29 14:21:47 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Fri Mar 30 16:18:59 2007 +0200
@@ -128,14 +128,18 @@
continued by an application of a function @{text "g \<Colon> foo \<Rightarrow> bar"},
and so on.  As a canoncial example, take primitive functions enriching
theories by constants and definitions:
-  @{ML "Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory"}
-  and @{ML "Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory"}.
+  @{ML "Sign.add_consts_i: (string * typ * mixfix) list -> theory
+-> theory"}
+  and @{ML "Theory.add_defs_i: bool -> bool
+-> (bstring * term) list -> theory -> theory"}.
Written with naive application, an addition of a constant with
a corresponding definition would look like:
+  @{ML "Theory.add_defs_i false false [dummy_def]
With increasing numbers of applications, this code gets quite unreadable.
Using composition, at least the nesting of brackets may be reduced:
+  [dummy_const]) thy"}.
What remains unsatisfactory is that things are written down in the opposite order
as they actually happen''.
*}
@@ -156,7 +160,7 @@
*}

text {*
-  When iterating over a list of parameters @{text "[x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<Colon> 'a list"},
+  \noindent When iterating over a list of parameters @{text "[x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<Colon> 'a list"},
the @{ML fold} combinator lifts a single function @{text "f \<Colon> 'a -> 'b -> 'b"}:
@{text "y |> fold f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv> y |> f x\<^isub>1 |> f x\<^isub>2 |> \<dots> |> f x\<^isub>n"}
*}
@@ -172,7 +176,7 @@
*}

text {*
-  FIXME transformations involving side results
+  \noindent FIXME transformations involving side results
*}

text %mlref {*
@@ -186,7 +190,9 @@
*}

text {*
-  FIXME higher-order variants
+  \noindent All those linear combinators also exist in higher-order
+  variants which do not expect a value on the left hand side
+  but a function.
*}

text %mlref {*
@@ -196,6 +202,10 @@
\end{mldecls}
*}

+text {*
+  \noindent FIXME
+*}
+
section {* Options and partiality *}

text %mlref {*
@@ -211,7 +221,15 @@
\end{mldecls}
*}

-text FIXME
+text {*
+  Standard selector functions on @{text option}s are provided.
+  The @{ML try} and @{ML can} functions provide a convenient
+  interface for handling exceptions -- both take as arguments
+  a function @{text f} together with a parameter @{text x}
+  and catch any exception during the evaluation of the application
+  of @{text f} to @{text x}, either return a lifted result
+  (@{ML NONE} on failure) or a boolean value (@{ML false} on failure).
+*}

section {* Common data structures *}

--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Mar 29 14:21:47 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Fri Mar 30 16:18:59 2007 +0200
@@ -172,14 +172,18 @@
continued by an application of a function \isa{g\ {\isasymColon}\ foo\ {\isasymRightarrow}\ bar},
and so on.  As a canoncial example, take primitive functions enriching
theories by constants and definitions:
-  \verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory|
-  and \verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory|.
+  \verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory|\isasep\isanewline%
+\verb|-> theory|
+  and \verb|Theory.add_defs_i: bool -> bool|\isasep\isanewline%
+\verb|-> (bstring * term) list -> theory -> theory|.
Written with naive application, an addition of a constant with
a corresponding definition would look like:
With increasing numbers of applications, this code gets quite unreadable.
Using composition, at least the nesting of brackets may be reduced:
+\verb|  [dummy_const]) thy|.
What remains unsatisfactory is that things are written down in the opposite order
as they actually happen''.%
\end{isamarkuptext}%
@@ -209,7 +213,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-When iterating over a list of parameters \isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymColon}\ {\isacharprime}a\ list},
+\noindent When iterating over a list of parameters \isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymColon}\ {\isacharprime}a\ list},
the \verb|fold| combinator lifts a single function \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}:
\isa{y\ {\isacharbar}{\isachargreater}\ fold\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub n}%
\end{isamarkuptext}%
@@ -240,7 +244,7 @@
%
\begin{isamarkuptext}%
-FIXME transformations involving side results%
+\noindent FIXME transformations involving side results%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -269,7 +273,9 @@
%
\begin{isamarkuptext}%
-FIXME higher-order variants%
+\noindent All those linear combinators also exist in higher-order
+  variants which do not expect a value on the left hand side
+  but a function.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -294,6 +300,11 @@
%
%
+\begin{isamarkuptext}%
+\noindent FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Options and partiality%
}
\isamarkuptrue%
@@ -326,7 +337,13 @@
%