--- a/doc-src/Codegen/Thy/Adaptation.thy Wed Dec 23 08:31:15 2009 +0100
+++ b/doc-src/Codegen/Thy/Adaptation.thy Wed Dec 23 08:31:33 2009 +0100
@@ -38,10 +38,10 @@
\begin{itemize}
\item The safe configuration methods act uniformly on every target language,
- whereas for adaptation you have to treat each target language separate.
+ whereas for adaptation you have to treat each target language separately.
\item Application is extremely tedious since there is no abstraction
which would allow for a static check, making it easy to produce garbage.
- \item More or less subtle errors can be introduced unconsciously.
+ \item Subtle errors can be introduced unconsciously.
\end{itemize}
\noindent However, even if you ought refrain from setting up adaptation
--- a/doc-src/Codegen/Thy/Further.thy Wed Dec 23 08:31:15 2009 +0100
+++ b/doc-src/Codegen/Thy/Further.thy Wed Dec 23 08:31:33 2009 +0100
@@ -7,8 +7,8 @@
subsection {* Further reading *}
text {*
- Do dive deeper into the issue of code generation, you should visit
- the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} which
+ 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.
*}
@@ -36,7 +36,7 @@
B ABC
C ABC
-text {*
+text {*\noindent
we explicitly map all those modules on \emph{ABC},
resulting in an ad-hoc merge of this three modules
at serialisation time.
@@ -47,7 +47,7 @@
text {*
Code generation may also be used to \emph{evaluate} expressions
(using @{text SML} as target language of course).
- For instance, the @{command value} allows to reduce an expression to a
+ For instance, the @{command value} reduces an expression to a
normal form with respect to the underlying code equations:
*}
@@ -106,7 +106,7 @@
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});
+ \cite{bulwahn-et-al:2008:imperative};
the framework described there is available in theory @{theory Imperative_HOL}.
*}
--- a/doc-src/Codegen/Thy/Introduction.thy Wed Dec 23 08:31:15 2009 +0100
+++ b/doc-src/Codegen/Thy/Introduction.thy Wed Dec 23 08:31:33 2009 +0100
@@ -7,25 +7,24 @@
text {*
This tutorial introduces a generic code generator for the
@{text Isabelle} system.
- Generic in the sense that the
- \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
+ 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} which is an extension of @{theory Pure}
+ @{theory HOL} \cite{isa-tutorial}, which is an extension of @{theory Pure},
already comes with a reasonable framework setup and thus provides
- a good working horse for raising code-generation-driven
+ 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.
- (see also \cite{isa-tutorial}).
The code generator aims to be usable with no further ado
- in most cases while allowing for detailed customisation.
- This manifests in the structure of this tutorial: after a short
+ 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
@@ -58,7 +57,7 @@
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
- allows to turn those into functional programs immediately.
+ 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:
*}
@@ -102,7 +101,7 @@
module_name Example file "examples/"
text {*
- \noindent This is how the corresponding code in @{text Haskell} looks like:
+ \noindent This is the corresponding code in @{text Haskell}:
*}
text %quote {*@{code_stmts empty enqueue dequeue (Haskell)}*}
@@ -117,7 +116,7 @@
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 inevitable to gain some understanding
+ and adapt the code generator, it is necessary to gain some understanding
how it works.
\begin{figure}[h]
@@ -142,16 +141,15 @@
\begin{itemize}
- \item Starting point is a collection of raw code equations in a
- theory; due to proof irrelevance it is not relevant where they
- stem from but typically they are either descendant of specification
- tools or explicit proofs by the user.
+ \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 Before these raw code equations are continued
- with, they can be subjected to theorem transformations. This
- \qn{preprocessor} is an interface which allows to apply the full
+ \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 the preprocessing step is a
+ generation. The result of preprocessing is a
structured collection of code equations.
\item These code equations are \qn{translated} to a program in an
--- a/doc-src/Codegen/Thy/Program.thy Wed Dec 23 08:31:15 2009 +0100
+++ b/doc-src/Codegen/Thy/Program.thy Wed Dec 23 08:31:33 2009 +0100
@@ -8,12 +8,11 @@
text {*
We have already seen how by default equations stemming from
- @{command definition}/@{command primrec}/@{command fun}
+ @{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.
- All kinds of customisation shown in this section is \emph{safe}
- in the sense that the user does not have to worry about
- correctness -- all programs generatable that way are partially
+ 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.
*}
@@ -52,7 +51,7 @@
As told in \secref{sec:concept}, code generation is based
on a structured collection of code theorems.
- For explorative purpose, this collection
+ This collection
may be inspected using the @{command code_thms} command:
*}
@@ -128,7 +127,7 @@
"bexp n = pow n (Suc (Suc 0))"
text {*
- \noindent The corresponding code:
+ \noindent The corresponding code in Haskell uses that language's native classes:
*}
text %quote {*@{code_stmts bexp (Haskell)}*}
@@ -141,7 +140,7 @@
text %quote {*@{code_stmts bexp (SML)}*}
text {*
- \noindent Note the parameters with trailing underscore (@{verbatim "A_"})
+ \noindent Note the parameters with trailing underscore (@{verbatim "A_"}),
which are the dictionary parameters.
*}
@@ -153,14 +152,14 @@
out: \emph{preprocessing}. In essence, the preprocessor
consists of two components: a \emph{simpset} and \emph{function transformers}.
- The \emph{simpset} allows to employ the full generality of the
+ 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 undeclared using
+ \emph{unfold theorems}, which may be declared and removed using
the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
- attribute respectively.
+ attribute, respectively.
Some common applications:
*}
@@ -232,7 +231,7 @@
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 a simple, straightforward
+ theorems about it. Therefore, here is a simple, straightforward
representation of queues:
*}
@@ -402,13 +401,12 @@
text {*
Observe that on the right hand side of the definition of @{const
- "strict_dequeue'"} the constant @{const empty_queue} occurs
- which is unspecified.
+ "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
Normally, if constants without any code equations occur in a
program, the code generator complains (since in most cases this is
- not what the user expects). But such constants can also be thought
- of as function definitions with no equations which always fail,
+ indeed an error). But such constants can also be thought
+ of as function definitions which always fail,
since there is never a successful pattern match on the left hand
side. In order to categorise a constant into that category
explicitly, use @{command "code_abort"}:
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Wed Dec 23 08:31:15 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed Dec 23 08:31:33 2009 +0100
@@ -72,10 +72,10 @@
\begin{itemize}
\item The safe configuration methods act uniformly on every target language,
- whereas for adaptation you have to treat each target language separate.
+ whereas for adaptation you have to treat each target language separately.
\item Application is extremely tedious since there is no abstraction
which would allow for a static check, making it easy to produce garbage.
- \item More or less subtle errors can be introduced unconsciously.
+ \item Subtle errors can be introduced unconsciously.
\end{itemize}
\noindent However, even if you ought refrain from setting up adaptation
@@ -229,24 +229,30 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~datatype boola = True | False\\
+\hspace*{0pt} ~val anda :~boola -> boola -> boola\\
+\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> boola\\
+\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> boola\\
+\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> boola\\
+\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
\hspace*{0pt}\\
\hspace*{0pt}datatype boola = True | False;\\
\hspace*{0pt}\\
\hspace*{0pt}fun anda p True = p\\
-\hspace*{0pt} ~| anda p False = False\\
-\hspace*{0pt} ~| anda True p = p\\
-\hspace*{0pt} ~| anda False p = False;\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~anda p False = False\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~anda True p = p\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~anda False p = False;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
+\hspace*{0pt}fun less{\char123}{\char92}isacharunderscore{\char125}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~= less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}nat n Zero{\char95}nat = False\\
+\hspace*{0pt}and less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = less{\char95}nat m n\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = True;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
+\hspace*{0pt}fun in{\char123}{\char92}isacharunderscore{\char125}interval (k,~l) n = anda {\char123}{\char92}isacharparenleft{\char125}less{\char95}eq{\char95}nat k n{\char123}{\char92}isacharparenright{\char125}~{\char123}{\char92}isacharparenleft{\char125}less{\char95}eq{\char95}nat n l{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -312,17 +318,21 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> bool\\
+\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> bool\\
+\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> bool\\
+\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
+\hspace*{0pt}fun less{\char123}{\char92}isacharunderscore{\char125}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~= less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}nat n Zero{\char95}nat = false\\
+\hspace*{0pt}and less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = less{\char95}nat m n\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = true;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
+\hspace*{0pt}fun in{\char123}{\char92}isacharunderscore{\char125}interval (k,~l) n = {\char123}{\char92}isacharparenleft{\char125}less{\char95}eq{\char95}nat k n{\char123}{\char92}isacharparenright{\char125}~andalso {\char123}{\char92}isacharparenleft{\char125}less{\char95}eq{\char95}nat n l{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -369,17 +379,21 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~val less{\char95}nat :~nat -> nat -> bool\\
+\hspace*{0pt} ~val less{\char95}eq{\char95}nat :~nat -> nat -> bool\\
+\hspace*{0pt} ~val in{\char95}interval :~nat * nat -> nat -> bool\\
+\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
-\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
-\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
+\hspace*{0pt}fun less{\char123}{\char92}isacharunderscore{\char125}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~= less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}nat n Zero{\char95}nat = false\\
+\hspace*{0pt}and less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = less{\char95}nat m n\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~less{\char123}{\char92}isacharunderscore{\char125}eq{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = true;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
+\hspace*{0pt}fun in{\char123}{\char92}isacharunderscore{\char125}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
--- a/doc-src/Codegen/Thy/document/Further.tex Wed Dec 23 08:31:15 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Further.tex Wed Dec 23 08:31:33 2009 +0100
@@ -27,8 +27,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Do dive deeper into the issue of code generation, you should visit
- the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} which
+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.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -73,7 +73,8 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-we explicitly map all those modules on \emph{ABC},
+\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}%
@@ -86,7 +87,7 @@
\begin{isamarkuptext}%
Code generation may also be used to \emph{evaluate} expressions
(using \isa{SML} as target language of course).
- For instance, the \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} allows to reduce an expression to a
+ For instance, the \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} reduces an expression to a
normal form with respect to the underlying code equations:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -219,7 +220,7 @@
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});
+ \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%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Dec 23 08:31:15 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Dec 23 08:31:33 2009 +0100
@@ -25,25 +25,24 @@
\begin{isamarkuptext}%
This tutorial introduces a generic code generator for the
\isa{Isabelle} system.
- Generic in the sense that the
- \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
+ 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}}} which is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}
+ \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 working horse for raising code-generation-driven
+ 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.
- (see also \cite{isa-tutorial}).
The code generator aims to be usable with no further ado
- in most cases while allowing for detailed customisation.
- This manifests in the structure of this tutorial: after a short
+ 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
@@ -78,7 +77,7 @@
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
- allows to turn those into functional programs immediately.
+ 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}%
@@ -147,31 +146,38 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~val foldl :~{\char123}{\char92}isacharparenleft{\char125}'a -> 'b -> 'a{\char123}{\char92}isacharparenright{\char125}~-> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val rev :~'a list -> 'a list\\
+\hspace*{0pt} ~val list{\char95}case :~'a -> {\char123}{\char92}isacharparenleft{\char125}'b -> 'b list -> 'a{\char123}{\char92}isacharparenright{\char125}~-> 'b list -> 'a\\
+\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list{\char92}~{\char123}{\char92}isacharasterisk{\char125}~'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} ~{\char123}{\char92}isacharbar{\char125}~foldl f a {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharparenright{\char125}~= foldl f {\char123}{\char92}isacharparenleft{\char125}f a x{\char123}{\char92}isacharparenright{\char125}~xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun rev xs = foldl {\char123}{\char92}isacharparenleft{\char125}fn xsa => fn x => x ::~xsa{\char123}{\char92}isacharparenright{\char125}~[] xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun list{\char95}case f1 f2 (a ::~lista) = f2 a lista\\
-\hspace*{0pt} ~| list{\char95}case f1 f2 [] = f1;\\
+\hspace*{0pt}fun list{\char123}{\char92}isacharunderscore{\char125}case f1 f2 {\char123}{\char92}isacharparenleft{\char125}a ::~lista{\char123}{\char92}isacharparenright{\char125}~= f2 a lista\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~list{\char123}{\char92}isacharunderscore{\char125}case f1 f2 [] = f1;\\
\hspace*{0pt}\\
-\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
+\hspace*{0pt}datatype 'a queue = AQueue of 'a list{\char92}~{\char123}{\char92}isacharasterisk{\char125}~'a list;\\
\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
+\hspace*{0pt}val empty :~'a queue = AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\
-\hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
-\hspace*{0pt} ~| dequeue (AQueue (v ::~va,~[])) =\\
+\hspace*{0pt}fun dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (NONE,~AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125})\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~y ::~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (SOME y,~AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125})\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}v ::~va{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~=\\
\hspace*{0pt} ~~~let\\
-\hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\
+\hspace*{0pt} ~~~~~val y ::~ys = rev {\char123}{\char92}isacharparenleft{\char125}v ::~va{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt} ~~~in\\
-\hspace*{0pt} ~~~~~(SOME y,~AQueue ([],~ys))\\
+\hspace*{0pt} ~~~~~(SOME y,~AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125})\\
\hspace*{0pt} ~~~end;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
+\hspace*{0pt}fun enqueue x {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= AQueue {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -213,7 +219,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent This is how the corresponding code in \isa{Haskell} looks like:%
+\noindent This is the corresponding code in \isa{Haskell}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -228,16 +234,15 @@
\noindent%
\hspace*{0pt}module Example where {\char123}\\
\hspace*{0pt}\\
-\hspace*{0pt}\\
-\hspace*{0pt}foldla ::~forall a b.~(a -> b -> a) -> a -> [b] -> a;\\
+\hspace*{0pt}foldla ::~forall a b.~{\char123}{\char92}isacharparenleft{\char125}a -> b -> a{\char123}{\char92}isacharparenright{\char125}~-> a -> [b] -> a;\\
\hspace*{0pt}foldla f a [] = a;\\
-\hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\
+\hspace*{0pt}foldla f a {\char123}{\char92}isacharparenleft{\char125}x :~xs{\char123}{\char92}isacharparenright{\char125}~= foldla f {\char123}{\char92}isacharparenleft{\char125}f a x{\char123}{\char92}isacharparenright{\char125}~xs;\\
\hspace*{0pt}\\
\hspace*{0pt}rev ::~forall a.~[a] -> [a];\\
-\hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\
+\hspace*{0pt}rev xs = foldla {\char123}{\char92}isacharparenleft{\char125}{\char92}~xsa x -> x :~xsa{\char123}{\char92}isacharparenright{\char125}~[] xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}list{\char95}case ::~forall a b.~a -> (b -> [b] -> a) -> [b] -> a;\\
-\hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\
+\hspace*{0pt}list{\char95}case ::~forall a b.~a -> {\char123}{\char92}isacharparenleft{\char125}b -> [b] -> a{\char123}{\char92}isacharparenright{\char125}~-> [b] -> a;\\
+\hspace*{0pt}list{\char95}case f1 f2 {\char123}{\char92}isacharparenleft{\char125}a :~list{\char123}{\char92}isacharparenright{\char125}~= f2 a list;\\
\hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\
\hspace*{0pt}\\
\hspace*{0pt}data Queue a = AQueue [a] [a];\\
@@ -246,15 +251,15 @@
\hspace*{0pt}empty = AQueue [] [];\\
\hspace*{0pt}\\
\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
-\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
-\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
+\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue [] []{\char123}{\char92}isacharparenright{\char125}~= (Nothing,~AQueue [] []);\\
+\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs {\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}v :~va{\char123}{\char92}isacharparenright{\char125}~[]{\char123}{\char92}isacharparenright{\char125}~=\\
\hspace*{0pt} ~let {\char123}\\
-\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
+\hspace*{0pt} ~~~{\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}~= rev {\char123}{\char92}isacharparenleft{\char125}v :~va{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
\hspace*{0pt}\\
\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
-\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
+\hspace*{0pt}enqueue x {\char123}{\char92}isacharparenleft{\char125}AQueue xs ys{\char123}{\char92}isacharparenright{\char125}~= AQueue {\char123}{\char92}isacharparenleft{\char125}x :~xs{\char123}{\char92}isacharparenright{\char125}~ys;\\
\hspace*{0pt}\\
\hspace*{0pt}{\char125}%
\end{isamarkuptext}%
@@ -280,7 +285,7 @@
\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 inevitable to gain some understanding
+ and adapt the code generator, it is necessary to gain some understanding
how it works.
\begin{figure}[h]
@@ -305,16 +310,15 @@
\begin{itemize}
- \item Starting point is a collection of raw code equations in a
- theory; due to proof irrelevance it is not relevant where they
- stem from but typically they are either descendant of specification
- tools or explicit proofs by the user.
+ \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 Before these raw code equations are continued
- with, they can be subjected to theorem transformations. This
- \qn{preprocessor} is an interface which allows to apply the full
+ \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 the preprocessing step is a
+ generation. The result of preprocessing is a
structured collection of code equations.
\item These code equations are \qn{translated} to a program in an
--- a/doc-src/Codegen/Thy/document/Program.tex Wed Dec 23 08:31:15 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Program.tex Wed Dec 23 08:31:33 2009 +0100
@@ -28,12 +28,11 @@
%
\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}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
+ \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.
- All kinds of customisation shown in this section is \emph{safe}
- in the sense that the user does not have to worry about
- correctness -- all programs generatable that way are partially
+ 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%
@@ -88,10 +87,10 @@
\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}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs {\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs []{\char123}{\char92}isacharparenright{\char125}~=\\
\hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\
-\hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));%
+\hspace*{0pt} ~~~else dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue [] {\char123}{\char92}isacharparenleft{\char125}rev xs{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125});%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -112,7 +111,7 @@
As told in \secref{sec:concept}, code generation is based
on a structured collection of code theorems.
- For explorative purpose, this collection
+ This collection
may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -260,7 +259,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The corresponding code:%
+\noindent The corresponding code in Haskell uses that language's native classes:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -275,23 +274,22 @@
\noindent%
\hspace*{0pt}module Example where {\char123}\\
\hspace*{0pt}\\
-\hspace*{0pt}\\
\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
\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}class {\char123}{\char92}isacharparenleft{\char125}Semigroup a{\char123}{\char92}isacharparenright{\char125}~=> 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 ::~forall a.~{\char123}{\char92}isacharparenleft{\char125}Monoid a{\char123}{\char92}isacharparenright{\char125}~=> Nat -> a -> a;\\
\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
-\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
+\hspace*{0pt}pow {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~a = mult a {\char123}{\char92}isacharparenleft{\char125}pow n a{\char123}{\char92}isacharparenright{\char125};\\
\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 {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = plus{\char95}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
\hspace*{0pt}\\
\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
@@ -299,7 +297,7 @@
\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}mult{\char95}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = plus{\char95}nat n {\char123}{\char92}isacharparenleft{\char125}mult{\char95}nat m n{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}instance Semigroup Nat where {\char123}\\
\hspace*{0pt} ~mult = mult{\char95}nat;\\
@@ -310,7 +308,7 @@
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}bexp ::~Nat -> Nat;\\
-\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
+\hspace*{0pt}bexp n = pow n {\char123}{\char92}isacharparenleft{\char125}Suc {\char123}{\char92}isacharparenleft{\char125}Suc Zero{\char95}nat{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}{\char125}%
\end{isamarkuptext}%
@@ -338,35 +336,48 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~type 'a semigroup\\
+\hspace*{0pt} ~val mult :~'a semigroup{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> 'a\\
+\hspace*{0pt} ~type 'a monoid\\
+\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a semigroup\\
+\hspace*{0pt} ~val neutral :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a\\
+\hspace*{0pt} ~val pow :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~nat -> 'a -> 'a\\
+\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
+\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
+\hspace*{0pt} ~val mult{\char95}nat :~nat -> 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}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
-\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
+\hspace*{0pt}type 'a semigroup = {\char123}{\char92}isacharbraceleft{\char125}mult :~'a -> 'a -> 'a{\char123}{\char92}isacharbraceright{\char125}{\char123}{\char92}isacharsemicolon{\char125}\\
+\hspace*{0pt}val mult = {\char35}mult :~'a semigroup{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> 'a;\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}semigroup{\char95}monoid A{\char95};\\
-\hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\
+\hspace*{0pt}type 'a monoid = {\char123}{\char92}isacharbraceleft{\char125}semigroup{\char95}monoid :~'a semigroup{\char123}{\char92}isacharcomma{\char125}~neutral :~'a{\char123}{\char92}isacharbraceright{\char125}{\char123}{\char92}isacharsemicolon{\char125}\\
+\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a semigroup;\\
+\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'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} ~{\char123}{\char92}isacharbar{\char125}~pow A{\char95}~{\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}~a = mult {\char123}{\char92}isacharparenleft{\char125}semigroup{\char95}monoid A{\char95}{\char123}{\char92}isacharparenright{\char125}~a {\char123}{\char92}isacharparenleft{\char125}pow A{\char95}~n a{\char123}{\char92}isacharparenright{\char125};\\
\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}fun plus{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = plus{\char95}nat m {\char123}{\char92}isacharparenleft{\char125}Suc n{\char123}{\char92}isacharparenright{\char125}\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~plus{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = n;\\
\hspace*{0pt}\\
\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
\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}fun mult{\char123}{\char92}isacharunderscore{\char125}nat Zero{\char95}nat n = Zero{\char95}nat\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~mult{\char123}{\char92}isacharunderscore{\char125}nat {\char123}{\char92}isacharparenleft{\char125}Suc m{\char123}{\char92}isacharparenright{\char125}~n = plus{\char95}nat n {\char123}{\char92}isacharparenleft{\char125}mult{\char95}nat m n{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
-\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
+\hspace*{0pt}val semigroup{\char95}nat = {\char123}{\char92}isacharbraceleft{\char125}mult = mult{\char95}nat{\char123}{\char92}isacharbraceright{\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}val monoid{\char95}nat = {\char123}{\char92}isacharbraceleft{\char125}semigroup{\char95}monoid = semigroup{\char95}nat{\char123}{\char92}isacharcomma{\char125}~neutral = neutral{\char95}nat{\char123}{\char92}isacharbraceright{\char125}\\
\hspace*{0pt} ~:~nat monoid;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
+\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n {\char123}{\char92}isacharparenleft{\char125}Suc {\char123}{\char92}isacharparenleft{\char125}Suc Zero{\char95}nat{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -380,7 +391,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Note the parameters with trailing underscore (\verb|A_|)
+\noindent Note the parameters with trailing underscore (\verb|A_|),
which are the dictionary parameters.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -395,14 +406,14 @@
out: \emph{preprocessing}. In essence, the preprocessor
consists of two components: a \emph{simpset} and \emph{function transformers}.
- The \emph{simpset} allows to employ the full generality of the
+ 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 undeclared using
+ \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.
+ attribute, respectively.
Some common applications:%
\end{isamarkuptext}%
@@ -515,7 +526,7 @@
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 a simple, straightforward
+ theorems about it. Therefore, here is a simple, straightforward
representation of queues:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -654,27 +665,34 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~val foldl :~{\char123}{\char92}isacharparenleft{\char125}'a -> 'b -> 'a{\char123}{\char92}isacharparenright{\char125}~-> '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{\char92}~{\char123}{\char92}isacharasterisk{\char125}~'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} ~{\char123}{\char92}isacharbar{\char125}~foldl f a {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharparenright{\char125}~= foldl f {\char123}{\char92}isacharparenleft{\char125}f a x{\char123}{\char92}isacharparenright{\char125}~xs;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun rev xs = foldl {\char123}{\char92}isacharparenleft{\char125}fn xsa => fn x => x ::~xsa{\char123}{\char92}isacharparenright{\char125}~[] xs;\\
\hspace*{0pt}\\
\hspace*{0pt}fun null [] = true\\
-\hspace*{0pt} ~| null (x ::~xs) = false;\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~null {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharparenright{\char125}~= false;\\
\hspace*{0pt}\\
-\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
+\hspace*{0pt}datatype 'a queue = AQueue of 'a list{\char92}~{\char123}{\char92}isacharasterisk{\char125}~'a list;\\
\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
+\hspace*{0pt}val empty :~'a queue = AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125};\\
\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}fun dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~y ::~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (SOME y,~AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125})\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~=\\
+\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~[]{\char123}{\char92}isacharparenright{\char125})\\
+\hspace*{0pt} ~~~~~else dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}[]{\char123}{\char92}isacharcomma{\char125}~rev xs{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125});\\
\hspace*{0pt}\\
-\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
+\hspace*{0pt}fun enqueue x {\char123}{\char92}isacharparenleft{\char125}AQueue {\char123}{\char92}isacharparenleft{\char125}xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= AQueue {\char123}{\char92}isacharparenleft{\char125}x ::~xs{\char123}{\char92}isacharcomma{\char125}~ys{\char123}{\char92}isacharparenright{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -759,23 +777,29 @@
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt}{\char92}~{\char92}~type 'a eq\\
+\hspace*{0pt} ~val eq :~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> bool\\
+\hspace*{0pt} ~val eqa :~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> bool\\
+\hspace*{0pt} ~val member :~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a list -> bool\\
+\hspace*{0pt} ~val collect{\char95}duplicates :\\
+\hspace*{0pt} ~~~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a list -> 'a list -> 'a list -> 'a list\\
+\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
-\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
+\hspace*{0pt}type 'a eq = {\char123}{\char92}isacharbraceleft{\char125}eq :~'a -> 'a -> bool{\char123}{\char92}isacharbraceright{\char125}{\char123}{\char92}isacharsemicolon{\char125}\\
+\hspace*{0pt}val eq = {\char35}eq :~'a eq{\char92}~{\char123}{\char92}isacharminus{\char125}{\char123}{\char92}isachargreater{\char125}~'a -> 'a -> bool;\\
\hspace*{0pt}\\
\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
\hspace*{0pt}\\
\hspace*{0pt}fun member A{\char95}~x [] = false\\
-\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~member A{\char95}~x {\char123}{\char92}isacharparenleft{\char125}y ::~ys{\char123}{\char92}isacharparenright{\char125}~= eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
-\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
+\hspace*{0pt}fun collect{\char123}{\char92}isacharunderscore{\char125}duplicates A{\char95}~xs ys [] = xs\\
+\hspace*{0pt} ~{\char123}{\char92}isacharbar{\char125}~collect{\char123}{\char92}isacharunderscore{\char125}duplicates A{\char95}~xs ys {\char123}{\char92}isacharparenleft{\char125}z ::~zs{\char123}{\char92}isacharparenright{\char125}~=\\
\hspace*{0pt} ~~~(if member A{\char95}~z xs\\
\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
-\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
-\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
+\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs {\char123}{\char92}isacharparenleft{\char125}z ::~ys{\char123}{\char92}isacharparenright{\char125}~zs)\\
+\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~{\char123}{\char92}isacharparenleft{\char125}z ::~xs{\char123}{\char92}isacharparenright{\char125}~{\char123}{\char92}isacharparenleft{\char125}z ::~ys{\char123}{\char92}isacharparenright{\char125}~zs);\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
@@ -851,11 +875,11 @@
\isatypewriter%
\noindent%
\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
+\hspace*{0pt}strict{\char95}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs []{\char123}{\char92}isacharparenright{\char125}~=\\
\hspace*{0pt} ~let {\char123}\\
-\hspace*{0pt} ~~~(y :~ys) = rev xs;\\
+\hspace*{0pt} ~~~{\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}~= rev xs;\\
\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
+\hspace*{0pt}strict{\char95}dequeue {\char123}{\char92}isacharparenleft{\char125}AQueue xs {\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (y,~AQueue xs ys);%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -900,13 +924,12 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}} the constant \isa{empty{\isacharunderscore}queue} occurs
- which is unspecified.
+Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs.
Normally, if constants without any code equations occur in a
program, the code generator complains (since in most cases this is
- not what the user expects). But such constants can also be thought
- of as function definitions with no equations which always fail,
+ indeed an error). But such constants can also be thought
+ of as function definitions which always fail,
since there is never a successful pattern match on the left hand
side. In order to categorise a constant into that category
explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
@@ -946,10 +969,10 @@
\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
\hspace*{0pt}\\
\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\
+\hspace*{0pt}strict{\char95}dequeue' {\char123}{\char92}isacharparenleft{\char125}AQueue xs {\char123}{\char92}isacharparenleft{\char125}y :~ys{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125}~= (y,~AQueue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue' {\char123}{\char92}isacharparenleft{\char125}AQueue xs []{\char123}{\char92}isacharparenright{\char125}~=\\
\hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\
-\hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));%
+\hspace*{0pt} ~~~else strict{\char95}dequeue' {\char123}{\char92}isacharparenleft{\char125}AQueue [] {\char123}{\char92}isacharparenleft{\char125}rev xs{\char123}{\char92}isacharparenright{\char125}{\char123}{\char92}isacharparenright{\char125});%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/exn.ML Wed Dec 23 08:31:33 2009 +0100
@@ -0,0 +1,61 @@
+(* Title: Pure/General/exn.ML
+ Author: Makarius
+
+Extra support for exceptions.
+*)
+
+signature EXN =
+sig
+ datatype 'a result = Result of 'a | Exn of exn
+ val get_result: 'a result -> 'a option
+ val get_exn: 'a result -> exn option
+ val capture: ('a -> 'b) -> 'a -> 'b result
+ val release: 'a result -> 'a
+ exception Interrupt
+ exception EXCEPTIONS of exn list
+ val flatten: exn -> exn list
+ val flatten_list: exn list -> exn list
+ val release_all: 'a result list -> 'a list
+ val release_first: 'a result list -> 'a list
+end;
+
+structure Exn: EXN =
+struct
+
+(* runtime exceptions as values *)
+
+datatype 'a result =
+ Result of 'a |
+ Exn of exn;
+
+fun get_result (Result x) = SOME x
+ | get_result _ = NONE;
+
+fun get_exn (Exn exn) = SOME exn
+ | get_exn _ = NONE;
+
+fun capture f x = Result (f x) handle e => Exn e;
+
+fun release (Result y) = y
+ | release (Exn e) = reraise e;
+
+
+(* interrupt and nested exceptions *)
+
+exception Interrupt = Interrupt;
+exception EXCEPTIONS of exn list;
+
+fun flatten Interrupt = []
+ | flatten (EXCEPTIONS exns) = flatten_list exns
+ | flatten exn = [exn]
+and flatten_list exns = List.concat (map flatten exns);
+
+fun release_all results =
+ if List.all (fn Result _ => true | _ => false) results
+ then map (fn Result x => x) results
+ else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
+
+fun release_first results = release_all results
+ handle EXCEPTIONS (exn :: _) => reraise exn;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/exn.scala Wed Dec 23 08:31:33 2009 +0100
@@ -0,0 +1,28 @@
+/* Title: Pure/General/exn.scala
+ Author: Makarius
+
+Extra support for exceptions.
+*/
+
+package isabelle
+
+
+object Exn
+{
+ /* runtime exceptions as values */
+
+ sealed abstract class Result[A]
+ case class Res[A](val result: A) extends Result[A]
+ case class Exn[A](val exn: Exception) extends Result[A]
+
+ def capture[A](e: => A): Result[A] =
+ try { Res(e) }
+ catch { case exn: RuntimeException => Exn[A](exn) }
+
+ def release[A](result: Result[A]): A =
+ result match {
+ case Res(x) => x
+ case Exn(exn) => throw exn
+ }
+}
+
--- a/src/Pure/General/scan.scala Wed Dec 23 08:31:15 2009 +0100
+++ b/src/Pure/General/scan.scala Wed Dec 23 08:31:33 2009 +0100
@@ -91,7 +91,8 @@
Tree(tree.branches +
(c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1))))
}
- } else tree
+ }
+ else tree
val old = this
new Lexicon { override val main_tree = extend(old.main_tree, 0) }
}
@@ -102,32 +103,182 @@
def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
- /* RegexParsers methods */
+ /** RegexParsers methods **/
override val whiteSpace = "".r
- def keyword: Parser[String] = new Parser[String] {
+
+ /* keywords from lexicon */
+
+ def keyword: Parser[String] = new Parser[String]
+ {
def apply(in: Input) =
{
val source = in.source
val offset = in.offset
val len = source.length - offset
- def scan(tree: Tree, text: String, i: Int): String =
+ def scan(tree: Tree, result: String, i: Int): String =
{
if (i < len) {
tree.branches.get(source.charAt(offset + i)) match {
- case Some((s, tr)) => scan(tr, if (s.isEmpty) text else s, i + 1)
- case None => text
+ case Some((s, tr)) => scan(tr, if (s.isEmpty) result else s, i + 1)
+ case None => result
}
- } else text
+ }
+ else result
}
- val text = scan(main_tree, "", 0)
- if (text.isEmpty) Failure("keyword expected", in)
- else Success(text, in.drop(text.length))
+ val result = scan(main_tree, "", 0)
+ if (result.isEmpty) Failure("keyword expected", in)
+ else Success(result, in.drop(result.length))
}
}.named("keyword")
+
+ /* symbols */
+
+ def symbols(pred: String => Boolean, min_count: Int, max_count: Int): Parser[String] =
+ new Parser[String]
+ {
+ def apply(in: Input) =
+ {
+ val start = in.offset
+ val end = in.source.length
+ val matcher = new Symbol.Matcher(in.source)
+
+ var i = start
+ var count = 0
+ var finished = false
+ while (!finished) {
+ if (i < end && count < max_count) {
+ val n = matcher(i, end)
+ val sym = in.source.subSequence(i, i + n).toString
+ if (pred(sym)) { i += n; count += 1 }
+ else finished = true
+ }
+ else finished = true
+ }
+ if (count < min_count) Failure("bad input", in)
+ else Success(in.source.subSequence(start, i).toString, in.drop(i - start))
+ }
+ }.named("symbols")
+
+ def one(pred: String => Boolean): Parser[String] = symbols(pred, 1, 1)
+ def many(pred: String => Boolean): Parser[String] = symbols(pred, 0, Integer.MAX_VALUE)
+ def many1(pred: String => Boolean): Parser[String] = symbols(pred, 1, Integer.MAX_VALUE)
+
+
+ /* quoted strings */
+
+ private def quoted(quote: String): Parser[String] =
+ {
+ quote ~
+ rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_closed(sym)) |
+ "\\" + quote | "\\\\" |
+ (("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ~
+ quote ^^ { case x ~ ys ~ z => x + ys.mkString + z }
+ }.named("quoted")
+
+ def quoted_content(quote: String, source: String): String =
+ {
+ require(parseAll(quoted(quote), source).successful)
+ source.substring(1, source.length - 1) // FIXME proper escapes, recode utf8 (!?)
+ }
+
+
+ /* verbatim text */
+
+ private def verbatim: Parser[String] =
+ {
+ "{*" ~ rep(many1(sym => sym != "*" && Symbol.is_closed(sym)) | """\*(?!\})""".r) ~ "*}" ^^
+ { case x ~ ys ~ z => x + ys.mkString + z }
+ }.named("verbatim")
+
+ def verbatim_content(source: String): String =
+ {
+ require(parseAll(verbatim, source).successful)
+ source.substring(2, source.length - 2)
+ }
+
+
+ /* nested comments */
+
+ def comment: Parser[String] = new Parser[String]
+ {
+ val comment_text =
+ rep(many1(sym => sym != "*" && sym != "(" && Symbol.is_closed(sym)) |
+ """\*(?!\))|\((?!\*)""".r)
+ val comment_open = "(*" ~ comment_text ^^ (_ => ())
+ val comment_close = comment_text ~ "*)" ^^ (_ => ())
+
+ def apply(in: Input) =
+ {
+ var rest = in
+ def try_parse(p: Parser[Unit]): Boolean =
+ {
+ parse(p, rest) match {
+ case Success(_, next) => { rest = next; true }
+ case _ => false
+ }
+ }
+ var depth = 0
+ var finished = false
+ while (!finished) {
+ if (try_parse(comment_open)) depth += 1
+ else if (depth > 0 && try_parse(comment_close)) depth -= 1
+ else finished = true
+ }
+ if (in.offset < rest.offset && depth == 0)
+ Success(in.source.subSequence(in.offset, rest.offset).toString, rest)
+ else Failure("comment expected", in)
+ }
+ }.named("comment")
+
+ def comment_content(source: String): String =
+ {
+ require(parseAll(comment, source).successful)
+ source.substring(2, source.length - 2)
+ }
+
+
+ /* outer syntax tokens */
+
+ def token(symbols: Symbol.Interpretation, is_command: String => Boolean):
+ Parser[Outer_Lex.Token] =
+ {
+ import Outer_Lex._
+
+ val id = one(symbols.is_letter) ~ many(symbols.is_letdig) ^^ { case x ~ y => x + y }
+ val nat = many1(symbols.is_digit)
+ val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
+
+ val ident = id ~ rep("." ~> id) ^^
+ { case x ~ Nil => Ident(x)
+ case x ~ ys => Long_Ident((x :: ys).mkString(".")) }
+
+ val var_ = "?" ~ id_nat ^^ { case x ~ y => Var(x + y) }
+ val type_ident = "'" ~ id ^^ { case x ~ y => Type_Ident(x + y) }
+ val type_var = "?'" ~ id_nat ^^ { case x ~ y => Type_Var(x + y) }
+ val nat_ = nat ^^ Nat
+
+ val sym_ident =
+ (many1(symbols.is_symbolic_char) |
+ one(sym => symbols.is_symbolic(sym) & Symbol.is_closed(sym))) ^^ Sym_Ident
+
+ val space = many1(symbols.is_blank) ^^ Space
+
+ val string = quoted("\"") ^^ String_Token
+ val alt_string = quoted("`") ^^ Alt_String_Token
+
+ val bad_input = many1(sym => !(symbols.is_blank(sym))) ^^ Bad_Input
+
+
+ /* tokens */
+
+ (space | (string | (alt_string | (verbatim ^^ Verbatim | comment ^^ Comment)))) |
+ ((ident | (var_ | (type_ident | (type_var | (nat_ | sym_ident))))) |||
+ keyword ^^ (x => if (is_command(x)) Command(x) else Keyword(x))) |
+ bad_input
+ }
}
}
-
--- a/src/Pure/General/symbol.scala Wed Dec 23 08:31:15 2009 +0100
+++ b/src/Pure/General/symbol.scala Wed Dec 23 08:31:33 2009 +0100
@@ -29,36 +29,45 @@
// total pattern
val regex = new Regex(plain + "|" + symbol + "|" + bad_symbol + "| .")
- // prefix of another symbol
- def is_open(s: CharSequence): Boolean =
+
+ /* basic matching */
+
+ def is_closed(c: Char): Boolean =
+ !(c == '\\' || Character.isHighSurrogate(c))
+
+ def is_closed(s: CharSequence): Boolean =
{
- val len = s.length
- len == 1 && Character.isHighSurrogate(s.charAt(0)) ||
- s == "\\" ||
- s == "\\<" ||
- len > 2 && s.charAt(len - 1) != '>'
+ if (s.length == 1) is_closed(s.charAt(0))
+ else !bad_symbol.pattern.matcher(s).matches
+ }
+
+ class Matcher(text: CharSequence)
+ {
+ private val matcher = regex.pattern.matcher(text)
+ def apply(start: Int, end: Int): Int =
+ {
+ require(0 <= start && start < end && end <= text.length)
+ if (is_closed(text.charAt(start))) 1
+ else {
+ matcher.region(start, end).lookingAt
+ matcher.group.length
+ }
+ }
}
/* elements */
- private def could_open(c: Char): Boolean =
- c == '\\' || Character.isHighSurrogate(c)
-
- def elements(text: CharSequence) = new Iterator[String] {
- private val matcher = regex.pattern.matcher(text)
+ def elements(text: CharSequence) = new Iterator[CharSequence]
+ {
+ private val matcher = new Matcher(text)
private var i = 0
def hasNext = i < text.length
def next = {
- val len =
- if (could_open(text.charAt(i))) {
- matcher.region(i, text.length).lookingAt
- matcher.group.length
- }
- else 1
- val s = text.subSequence(i, i + len)
- i += len
- s.toString
+ val n = matcher(i, text.length)
+ val s = text.subSequence(i, i + n)
+ i += n
+ s
}
}
@@ -70,20 +79,15 @@
case class Entry(chr: Int, sym: Int)
val index: Array[Entry] =
{
- val matcher = regex.pattern.matcher(text)
+ val matcher = new Matcher(text)
val buf = new mutable.ArrayBuffer[Entry]
var chr = 0
var sym = 0
while (chr < text.length) {
- val len =
- if (could_open(text.charAt(chr))) {
- matcher.region(chr, text.length).lookingAt
- matcher.group.length
- }
- else 1
- chr += len
+ val n = matcher(chr, text.length)
+ chr += n
sym += 1
- if (len > 1) buf += Entry(chr, sym)
+ if (n > 1) buf += Entry(chr, sym)
}
buf.toArray
}
@@ -152,7 +156,7 @@
/** Symbol interpretation **/
- class Interpretation(symbol_decls: Iterator[String])
+ class Interpretation(symbol_decls: List[String])
{
/* read symbols */
@@ -179,13 +183,14 @@
}
private val symbols: List[(String, Map[String, String])] =
- for (decl <- symbol_decls.toList if !empty.pattern.matcher(decl).matches)
+ for (decl <- symbol_decls if !empty.pattern.matcher(decl).matches)
yield read_decl(decl)
/* misc properties */
- val names: Map[String, String] = {
+ val names: Map[String, String] =
+ {
val name = new Regex("""\\<([A-Za-z][A-Za-z0-9_']*)>""")
Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
}
@@ -216,5 +221,66 @@
def decode(text: String): String = decoder.recode(text)
def encode(text: String): String = encoder.recode(text)
+
+
+ /* classification */
+
+ private object Decode_Set
+ {
+ def apply(elems: String*): Set[String] =
+ {
+ val content = elems.toList
+ Set((content ::: content.map(decode)): _*)
+ }
+ }
+
+ private val letters = Decode_Set(
+ "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
+ "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
+ "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
+ "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z",
+
+ "\\<A>", "\\<B>", "\\<C>", "\\<D>", "\\<E>", "\\<F>", "\\<G>",
+ "\\<H>", "\\<I>", "\\<J>", "\\<K>", "\\<L>", "\\<M>", "\\<N>",
+ "\\<O>", "\\<P>", "\\<Q>", "\\<R>", "\\<S>", "\\<T>", "\\<U>",
+ "\\<V>", "\\<W>", "\\<X>", "\\<Y>", "\\<Z>", "\\<a>", "\\<b>",
+ "\\<c>", "\\<d>", "\\<e>", "\\<f>", "\\<g>", "\\<h>", "\\<i>",
+ "\\<j>", "\\<k>", "\\<l>", "\\<m>", "\\<n>", "\\<o>", "\\<p>",
+ "\\<q>", "\\<r>", "\\<s>", "\\<t>", "\\<u>", "\\<v>", "\\<w>",
+ "\\<x>", "\\<y>", "\\<z>",
+
+ "\\<AA>", "\\<BB>", "\\<CC>", "\\<DD>", "\\<EE>", "\\<FF>",
+ "\\<GG>", "\\<HH>", "\\<II>", "\\<JJ>", "\\<KK>", "\\<LL>",
+ "\\<MM>", "\\<NN>", "\\<OO>", "\\<PP>", "\\<QQ>", "\\<RR>",
+ "\\<SS>", "\\<TT>", "\\<UU>", "\\<VV>", "\\<WW>", "\\<XX>",
+ "\\<YY>", "\\<ZZ>", "\\<aa>", "\\<bb>", "\\<cc>", "\\<dd>",
+ "\\<ee>", "\\<ff>", "\\<gg>", "\\<hh>", "\\<ii>", "\\<jj>",
+ "\\<kk>", "\\<ll>", "\\<mm>", "\\<nn>", "\\<oo>", "\\<pp>",
+ "\\<qq>", "\\<rr>", "\\<ss>", "\\<tt>", "\\<uu>", "\\<vv>",
+ "\\<ww>", "\\<xx>", "\\<yy>", "\\<zz>",
+
+ "\\<alpha>", "\\<beta>", "\\<gamma>", "\\<delta>", "\\<epsilon>",
+ "\\<zeta>", "\\<eta>", "\\<theta>", "\\<iota>", "\\<kappa>",
+ "\\<mu>", "\\<nu>", "\\<xi>", "\\<pi>", "\\<rho>", "\\<sigma>",
+ "\\<tau>", "\\<upsilon>", "\\<phi>", "\\<chi>", "\\<psi>",
+ "\\<omega>", "\\<Gamma>", "\\<Delta>", "\\<Theta>", "\\<Lambda>",
+ "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
+ "\\<Psi>", "\\<Omega>",
+
+ "\\<^isub>", "\\<^isup>")
+
+ private val blanks =
+ Decode_Set(" ", "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
+
+ private val sym_chars =
+ Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
+
+ def is_letter(sym: String): Boolean = letters.contains(sym)
+ def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'
+ def is_quasi(sym: String): Boolean = sym == "_" || sym == "'"
+ def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
+ def is_blank(sym: String): Boolean = blanks.contains(sym)
+ def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym)
+ def is_symbolic(sym: String): Boolean = sym.startsWith("\\<") && !sym.startsWith("\\<^")
}
}
--- a/src/Pure/IsaMakefile Wed Dec 23 08:31:15 2009 +0100
+++ b/src/Pure/IsaMakefile Wed Dec 23 08:31:33 2009 +0100
@@ -23,7 +23,7 @@
BOOTSTRAP_FILES = ML-Systems/compiler_polyml-5.0.ML \
ML-Systems/compiler_polyml-5.2.ML ML-Systems/compiler_polyml-5.3.ML \
- ML-Systems/exn.ML ML-Systems/ml_name_space.ML \
+ ML-Systems/ml_name_space.ML \
ML-Systems/ml_pretty.ML ML-Systems/mosml.ML \
ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \
ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \
@@ -51,38 +51,38 @@
Concurrent/synchronized_sequential.ML Concurrent/task_queue.ML \
General/alist.ML General/antiquote.ML General/balanced_tree.ML \
General/basics.ML General/binding.ML General/buffer.ML \
- General/file.ML General/graph.ML General/heap.ML General/integer.ML \
- General/long_name.ML General/markup.ML General/name_space.ML \
- General/ord_list.ML General/output.ML General/path.ML \
- General/position.ML General/pretty.ML General/print_mode.ML \
- General/properties.ML General/queue.ML General/same.ML \
- General/scan.ML General/secure.ML General/seq.ML General/source.ML \
- General/stack.ML General/symbol.ML General/symbol_pos.ML \
- General/table.ML General/url.ML General/xml.ML General/yxml.ML \
- Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML \
- Isar/class.ML Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \
- Isar/context_rules.ML Isar/element.ML Isar/expression.ML \
- Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML \
- Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \
- Isar/locale.ML Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \
- Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
- Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \
- Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
- Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML \
- Isar/skip_proof.ML Isar/spec_parse.ML Isar/spec_rules.ML \
- Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \
- Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML \
- ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \
- ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \
- ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML \
- ML-Systems/use_context.ML Proof/extraction.ML \
- Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
- Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML \
- ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \
- ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML \
- ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML \
- ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML \
- ProofGeneral/proof_general_emacs.ML \
+ General/exn.ML General/file.ML General/graph.ML General/heap.ML \
+ General/integer.ML General/long_name.ML General/markup.ML \
+ General/name_space.ML General/ord_list.ML General/output.ML \
+ General/path.ML General/position.ML General/pretty.ML \
+ General/print_mode.ML General/properties.ML General/queue.ML \
+ General/same.ML General/scan.ML General/secure.ML General/seq.ML \
+ General/source.ML General/stack.ML General/symbol.ML \
+ General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML \
+ General/yxml.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
+ Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
+ Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
+ Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \
+ Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
+ Isar/local_theory.ML Isar/locale.ML Isar/method.ML \
+ Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
+ Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
+ Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
+ Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
+ Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML \
+ Isar/spec_parse.ML Isar/spec_rules.ML Isar/specification.ML \
+ Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML \
+ ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML \
+ ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML \
+ ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
+ ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \
+ Proof/extraction.ML Proof/proof_rewrite_rules.ML \
+ Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
+ ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
+ ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \
+ ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \
+ ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \
+ ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML \
ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \
Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \
@@ -121,14 +121,15 @@
## Scala material
-SCALA_FILES = General/event_bus.scala General/linear_set.scala \
- General/markup.scala General/position.scala General/scan.scala \
- General/swing_thread.scala General/symbol.scala General/xml.scala \
- General/yxml.scala Isar/isar_document.scala Isar/outer_keyword.scala \
- System/cygwin.scala System/gui_setup.scala \
- System/isabelle_process.scala System/isabelle_syntax.scala \
- System/isabelle_system.scala System/platform.scala \
- Thy/completion.scala Thy/html.scala Thy/thy_header.scala
+SCALA_FILES = General/event_bus.scala General/exn.scala \
+ General/linear_set.scala General/markup.scala General/position.scala \
+ General/scan.scala General/swing_thread.scala General/symbol.scala \
+ General/xml.scala General/yxml.scala Isar/isar_document.scala \
+ Isar/outer_keyword.scala Isar/outer_lex.scala System/cygwin.scala \
+ System/gui_setup.scala System/isabelle_process.scala \
+ System/isabelle_syntax.scala System/isabelle_system.scala \
+ System/platform.scala Thy/completion.scala Thy/html.scala \
+ Thy/thy_header.scala library.scala
JAR_DIR = $(ISABELLE_HOME)/lib/classes
PURE_JAR = $(JAR_DIR)/Pure.jar
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/outer_lex.scala Wed Dec 23 08:31:33 2009 +0100
@@ -0,0 +1,100 @@
+/* Title: Pure/Isar/outer_lex.scala
+ Author: Makarius
+
+Outer lexical syntax for Isabelle/Isar.
+*/
+
+package isabelle
+
+
+object Outer_Lex
+{
+ sealed abstract class Token
+ {
+ def source: String
+ def content: String = source
+
+ def is_delimited: Boolean = false
+ def is_name: Boolean = false
+ def is_xname: Boolean = false
+ def is_text: Boolean = false
+ def is_space: Boolean = false
+ def is_comment: Boolean = false
+ def is_proper: Boolean = !(is_space || is_comment)
+ }
+
+ case class Command(val source: String) extends Token
+
+ case class Keyword(val source: String) extends Token
+
+ case class Ident(val source: String) extends Token
+ {
+ override def is_name = true
+ override def is_xname = true
+ override def is_text = true
+ }
+
+ case class Long_Ident(val source: String) extends Token
+ {
+ override def is_xname = true
+ override def is_text = true
+ }
+
+ case class Sym_Ident(val source: String) extends Token
+ {
+ override def is_name = true
+ override def is_xname = true
+ override def is_text = true
+ }
+
+ case class Var(val source: String) extends Token
+
+ case class Type_Ident(val source: String) extends Token
+
+ case class Type_Var(val source: String) extends Token
+
+ case class Nat(val source: String) extends Token
+ {
+ override def is_name = true
+ override def is_xname = true
+ override def is_text = true
+ }
+
+ case class String_Token(val source: String) extends Token
+ {
+ override def content = Scan.Lexicon.empty.quoted_content("\"", source)
+ override def is_delimited = true
+ override def is_name = true
+ override def is_xname = true
+ override def is_text = true
+ }
+
+ case class Alt_String_Token(val source: String) extends Token
+ {
+ override def content = Scan.Lexicon.empty.quoted_content("`", source)
+ override def is_delimited = true
+ }
+
+ case class Verbatim(val source: String) extends Token
+ {
+ override def content = Scan.Lexicon.empty.verbatim_content(source)
+ override def is_delimited = true
+ override def is_text = true
+ }
+
+ case class Space(val source: String) extends Token
+ {
+ override def is_space = true
+ }
+
+ case class Comment(val source: String) extends Token
+ {
+ override def content = Scan.Lexicon.empty.comment_content(source)
+ override def is_delimited = true
+ override def is_comment = true
+ }
+
+ case class Bad_Input(val source: String) extends Token
+ case class Unparsed(val source: String) extends Token
+}
+
--- a/src/Pure/ML-Systems/exn.ML Wed Dec 23 08:31:15 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-(* Title: Pure/ML-Systems/exn.ML
- Author: Makarius
-
-Extra support for exceptions.
-*)
-
-signature EXN =
-sig
- datatype 'a result = Exn of exn | Result of 'a
- val get_result: 'a result -> 'a option
- val get_exn: 'a result -> exn option
- val capture: ('a -> 'b) -> 'a -> 'b result
- val release: 'a result -> 'a
- exception Interrupt
- exception EXCEPTIONS of exn list
- val flatten: exn -> exn list
- val flatten_list: exn list -> exn list
- val release_all: 'a result list -> 'a list
- val release_first: 'a result list -> 'a list
-end;
-
-structure Exn: EXN =
-struct
-
-(* runtime exceptions as values *)
-
-datatype 'a result =
- Result of 'a |
- Exn of exn;
-
-fun get_result (Result x) = SOME x
- | get_result _ = NONE;
-
-fun get_exn (Exn exn) = SOME exn
- | get_exn _ = NONE;
-
-fun capture f x = Result (f x) handle e => Exn e;
-
-fun release (Result y) = y
- | release (Exn e) = reraise e;
-
-
-(* interrupt and nested exceptions *)
-
-exception Interrupt = Interrupt;
-exception EXCEPTIONS of exn list;
-
-fun flatten Interrupt = []
- | flatten (EXCEPTIONS exns) = flatten_list exns
- | flatten exn = [exn]
-and flatten_list exns = List.concat (map flatten exns);
-
-fun release_all results =
- if List.all (fn Result _ => true | _ => false) results
- then map (fn Result x => x) results
- else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
-
-fun release_first results = release_all results
- handle EXCEPTIONS (exn :: _) => reraise exn;
-
-end;
--- a/src/Pure/ML-Systems/mosml.ML Wed Dec 23 08:31:15 2009 +0100
+++ b/src/Pure/ML-Systems/mosml.ML Wed Dec 23 08:31:33 2009 +0100
@@ -41,7 +41,7 @@
fun reraise exn = raise exn;
use "ML-Systems/unsynchronized.ML";
-use "ML-Systems/exn.ML";
+use "General/exn.ML";
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/multithreading.ML";
--- a/src/Pure/ML-Systems/polyml_common.ML Wed Dec 23 08:31:15 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Wed Dec 23 08:31:33 2009 +0100
@@ -5,7 +5,7 @@
exception Interrupt = SML90.Interrupt;
-use "ML-Systems/exn.ML";
+use "General/exn.ML";
use "ML-Systems/multithreading.ML";
use "ML-Systems/time_limit.ML";
use "ML-Systems/timing.ML";
--- a/src/Pure/ML-Systems/smlnj.ML Wed Dec 23 08:31:15 2009 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Wed Dec 23 08:31:33 2009 +0100
@@ -9,7 +9,7 @@
use "ML-Systems/proper_int.ML";
use "ML-Systems/unsynchronized.ML";
use "ML-Systems/overloading_smlnj.ML";
-use "ML-Systems/exn.ML";
+use "General/exn.ML";
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/multithreading.ML";
--- a/src/Pure/System/isabelle_system.scala Wed Dec 23 08:31:15 2009 +0100
+++ b/src/Pure/System/isabelle_system.scala Wed Dec 23 08:31:33 2009 +0100
@@ -316,14 +316,14 @@
/* symbols */
- private def read_symbols(path: String): Iterator[String] =
+ private def read_symbols(path: String): List[String] =
{
val file = new File(platform_path(path))
- if (file.isFile) Source.fromFile(file).getLines
- else Iterator.empty
+ if (file.isFile) Source.fromFile(file).getLines.toList
+ else Nil
}
val symbols = new Symbol.Interpretation(
- read_symbols("$ISABELLE_HOME/etc/symbols") ++
+ read_symbols("$ISABELLE_HOME/etc/symbols") :::
read_symbols("$ISABELLE_HOME_USER/etc/symbols"))
--- a/src/Pure/Thy/completion.scala Wed Dec 23 08:31:15 2009 +0100
+++ b/src/Pure/Thy/completion.scala Wed Dec 23 08:31:33 2009 +0100
@@ -12,34 +12,6 @@
private object Completion
{
- /** String/CharSequence utilities */
-
- def length_ord(s1: String, s2: String): Boolean =
- s1.length < s2.length || s1.length == s2.length && s1 <= s2
-
- class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
- {
- require(0 <= start && start <= end && end <= text.length)
-
- def this(text: CharSequence) = this(text, 0, text.length)
-
- def length: Int = end - start
- def charAt(i: Int): Char = text.charAt(end - i - 1)
-
- def subSequence(i: Int, j: Int): CharSequence =
- if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
- else throw new IndexOutOfBoundsException
-
- override def toString: String =
- {
- val buf = new StringBuilder(length)
- for (i <- 0 until length)
- buf.append(charAt(i))
- buf.toString
- }
- }
-
-
/** word completion **/
val word_regex = "[a-zA-Z0-9_']+".r
@@ -55,7 +27,7 @@
def read(in: CharSequence): Option[String] =
{
- val rev_in = new Reverse(in)
+ val rev_in = new Library.Reverse(in)
parse((rev_symbol | rev_symb | word) ^^ (_.reverse), rev_in) match {
case Success(result, _) => Some(result)
case _ => None
@@ -113,7 +85,7 @@
def complete(line: CharSequence): Option[(String, List[String])] =
{
- abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match {
+ abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
case abbrevs_lex.Success(rev_a, _) =>
val (word, c) = abbrevs_map(rev_a)
if (word == c) None
@@ -123,7 +95,7 @@
case Some(word) =>
words_lex.completions(word).map(words_map(_)).filter(_ != word) match {
case Nil => None
- case cs => Some (word, cs.sort(Completion.length_ord _))
+ case cs => Some(word, cs.sort(_ < _))
}
case None => None
}
--- a/src/Pure/Thy/html.scala Wed Dec 23 08:31:15 2009 +0100
+++ b/src/Pure/Thy/html.scala Wed Dec 23 08:31:33 2009 +0100
@@ -49,7 +49,7 @@
flush()
ts + elem
}
- val syms = Symbol.elements(txt)
+ val syms = Symbol.elements(txt).map(_.toString)
while (syms.hasNext) {
val s1 = syms.next
def s2() = if (syms.hasNext) syms.next else ""
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/library.scala Wed Dec 23 08:31:33 2009 +0100
@@ -0,0 +1,49 @@
+/* Title: Pure/library.scala
+ Author: Makarius
+
+Basic library.
+*/
+
+package isabelle
+
+import java.lang.System
+
+
+object Library
+{
+ /* reverse CharSequence */
+
+ class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
+ {
+ require(0 <= start && start <= end && end <= text.length)
+
+ def this(text: CharSequence) = this(text, 0, text.length)
+
+ def length: Int = end - start
+ def charAt(i: Int): Char = text.charAt(end - i - 1)
+
+ def subSequence(i: Int, j: Int): CharSequence =
+ if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
+ else throw new IndexOutOfBoundsException
+
+ override def toString: String =
+ {
+ val buf = new StringBuilder(length)
+ for (i <- 0 until length)
+ buf.append(charAt(i))
+ buf.toString
+ }
+ }
+
+
+ /* timing */
+
+ def timeit[A](e: => A) =
+ {
+ val start = System.currentTimeMillis()
+ val result = Exn.capture(e)
+ val stop = System.currentTimeMillis()
+ System.err.println((stop - start) + "ms elapsed time")
+ Exn.release(result)
+ }
+}