--- 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 @@
later additions in expressiveness}.
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
provides definitions for overloaded functions.
@@ -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 @@
later additions in expressiveness}.
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} \\
- \hspace*{4ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isacharampersand}{\isacharampersand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
+ \hspace*{4ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
\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
provides definitions for overloaded functions.
@@ -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 @@
\endisadelimproof
%
\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 @@
\isadelimML
%
\endisadelimML
-\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 \cite{haskell-revised-report}).
+ supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell
+ \cite{haskell-revised-report}).
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
+ (see also \cite{isa-tutorial}).
*}
@@ -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:
+ we start with a generic example \secref{sec:example}
+ 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
\secref{sec:advanced} deals with advanced topics,
@@ -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}
in parentheses. These start with a \qn{target language}
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:
-*}
-
-(*<*)
-setup {* Sign.add_path "foo" *}
-(*>*)
-
-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
equations are added to the cache if not already present.
+
+ Similarly, the @{text "\<CODEDEPS>"} command shows a graph
+ visualizing dependencies between defining equations.
*}
+
section {* Recipes and advanced topics \label{sec:advanced} *}
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}.
-
\item @{ML CodegenConsts.read_const}~@{text thy}~@{text s}
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 \cite{haskell-revised-report}).
+ supports SML \cite{SML}, OCaml \cite{OCaml} and Haskell
+ \cite{haskell-revised-report}).
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
+ (see also \cite{isa-tutorial}).%
\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:
+ we start with a generic example \secref{sec:example}
+ 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
\secref{sec:advanced} deals with advanced topics,
@@ -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 @@
\ \ \ \ {\isachardoublequoteopen}fac\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ {\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}
in parentheses. These start with a \qn{target language}
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%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-\isanewline
-%
-\endisadelimML
-\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
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-\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
- equations are added to the cache if not already present.%
+ equations are added to the cache if not already present.
+
+ 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.add-func}\verb|CodegenData.add_func: thm -> theory -> theory| \\
+ \indexml{CodegenData.add-func}\verb|CodegenData.add_func: bool -> thm -> theory -> theory| \\
\indexml{CodegenData.del-func}\verb|CodegenData.del_func: thm -> theory -> theory| \\
\indexml{CodegenData.add-funcl}\verb|CodegenData.add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory| \\
\indexml{CodegenData.add-inline}\verb|CodegenData.add_inline: 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| \\
\indexml{CodegenConsts.read-const}\verb|CodegenConsts.read_const: theory -> string -> CodegenConsts.const| \\
\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}.
-
\item \verb|CodegenConsts.read_const|~\isa{thy}~\isa{s}
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 @@
%!PS-Adobe-2.0
-%%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] (Sign.add_consts_i [dummy_const] thy)"}
+ @{ML "Theory.add_defs_i false false [dummy_def]
+ (Sign.add_consts_i [dummy_const] thy)"}.
With increasing numbers of applications, this code gets quite unreadable.
Using composition, at least the nesting of brackets may be reduced:
- @{ML "(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i [dummy_const]) thy"}
+ @{ML "(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i
+ [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:
- \verb|Theory.add_defs_i false false [dummy_def] (Sign.add_consts_i [dummy_const] thy)|
+ \verb|Theory.add_defs_i false false [dummy_def]|\isasep\isanewline%
+\verb| (Sign.add_consts_i [dummy_const] thy)|.
With increasing numbers of applications, this code gets quite unreadable.
Using composition, at least the nesting of brackets may be reduced:
- \verb|(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i [dummy_const]) thy|
+ \verb|(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i|\isasep\isanewline%
+\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 @@
\endisadelimmlref
%
\begin{isamarkuptext}%
-FIXME transformations involving side results%
+\noindent FIXME transformations involving side results%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -269,7 +273,9 @@
\endisadelimmlref
%
\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 @@
%
\endisadelimmlref
%
+\begin{isamarkuptext}%
+\noindent FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Options and partiality%
}
\isamarkuptrue%
@@ -326,7 +337,13 @@
\endisadelimmlref
%
\begin{isamarkuptext}%
-FIXME%
+Standard selector functions on \isa{option}s are provided.
+ The \verb|try| and \verb|can| functions provide a convenient
+ interface for handling exceptions -- both take as arguments
+ a function \isa{f} together with a parameter \isa{x}
+ and catch any exception during the evaluation of the application
+ of \isa{f} to \isa{x}, either return a lifted result
+ (\verb|NONE| on failure) or a boolean value (\verb|false| on failure).%
\end{isamarkuptext}%
\isamarkuptrue%
%