--- a/NEWS Mon Oct 25 13:36:20 2010 +0200
+++ b/NEWS Mon Oct 25 16:18:00 2010 +0200
@@ -6,6 +6,8 @@
*** General ***
+* Significantly improved Isabelle/Isar implementation manual.
+
* Explicit treatment of UTF8 sequences as Isabelle symbols, such that
a Unicode character is treated as a single symbol, not a sequence of
non-ASCII bytes as before. Since Isabelle/ML string literals may
@@ -317,6 +319,10 @@
*** ML ***
+* Antiquotation @{assert} inlines a function bool -> unit that raises
+Fail if the argument is false. Due to inlining the source position of
+failed assertions is included in the error output.
+
* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
meaning.
--- a/doc-src/IsarImplementation/Thy/Base.thy Mon Oct 25 13:36:20 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Base.thy Mon Oct 25 16:18:00 2010 +0200
@@ -3,10 +3,4 @@
uses "../../antiquote_setup.ML"
begin
-(* FIXME move to src/Pure/ML/ml_antiquote.ML *)
-ML {*
- ML_Antiquote.inline "assert"
- (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")")
-*}
-
end
--- a/doc-src/IsarImplementation/Thy/Isar.thy Mon Oct 25 13:36:20 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Isar.thy Mon Oct 25 16:18:00 2010 +0200
@@ -4,9 +4,9 @@
chapter {* Isar language elements *}
-text {*
- The Isar proof language (see also \cite[\S2]{isabelle-isar-ref})
- consists of three main categories of language elements:
+text {* The Isar proof language (see also
+ \cite[\S2]{isabelle-isar-ref}) consists of three main categories of
+ language elements as follows.
\begin{enumerate}
@@ -44,12 +44,12 @@
text {* A \emph{proof command} is state transition of the Isar/VM
proof interpreter.
- In principle, Isar proof commands could be defined in
- user-space as well. The system is built like that in the first
- place: part of the commands are primitive, the other part is defined
- as derived elements. Adding to the genuine structured proof
- language requires profound understanding of the Isar/VM machinery,
- though, so this is beyond the scope of this manual.
+ In principle, Isar proof commands could be defined in user-space as
+ well. The system is built like that in the first place: one part of
+ the commands are primitive, the other part is defined as derived
+ elements. Adding to the genuine structured proof language requires
+ profound understanding of the Isar/VM machinery, though, so this is
+ beyond the scope of this manual.
What can be done realistically is to define some diagnostic commands
that inspect the general state of the Isar/VM, and report some
@@ -58,11 +58,10 @@
goals (if available).
Another common application is to define a toplevel command that
- poses a problem to the user as Isar proof state and stores the final
- result in a suitable context data slot. Thus a proof can be
+ poses a problem to the user as Isar proof state and processes the
+ final result relatively to the context. Thus a proof can be
incorporated into the context of some user-space tool, without
- modifying the Isar proof language itself.
-*}
+ modifying the Isar proof language itself. *}
text %mlref {*
\begin{mldecls}
@@ -131,13 +130,14 @@
storing named facts). Note that at this generic level the target
context is specified as @{ML_type Proof.context}, but the usual
wrapping of toplevel proofs into command transactions will provide a
- @{ML_type local_theory} here (see also \chref{ch:local-theory}).
- This usually affects the way how results are stored.
+ @{ML_type local_theory} here (\chref{ch:local-theory}). This
+ affects the way how results are stored.
The @{text "statement"} is given as a nested list of terms, each
associated with optional @{keyword "is"} patterns as usual in the
- Isar source language. The original list structure over terms is
- turned into one over theorems when @{text "after_qed"} is invoked.
+ Isar source language. The original nested list structure over terms
+ is turned into one over theorems when @{text "after_qed"} is
+ invoked.
\end{description}
*}
@@ -212,15 +212,15 @@
\end{itemize}
- \medskip Syntactically, the language of proof methods is embedded
- into Isar as arguments to certain commands, e.g.\ @{command "by"} or
- @{command apply}. User-space additions are reasonably easy by
- plugging suitable method-valued parser functions into the framework,
- using the @{command method_setup} command, for example.
+ \medskip Syntactically, the language of proof methods appears as
+ arguments to Isar commands like @{command "by"} or @{command apply}.
+ User-space additions are reasonably easy by plugging suitable
+ method-valued parser functions into the framework, using the
+ @{command method_setup} command, for example.
To get a better idea about the range of possibilities, consider the
- following Isar proof schemes. First some general form of structured
- proof text:
+ following Isar proof schemes. This is the general form of
+ structured proof text:
\medskip
\begin{tabular}{l}
@@ -231,15 +231,15 @@
\end{tabular}
\medskip
- The goal configuration consists of @{text "facts\<^sub>1"} and @{text
- "facts\<^sub>2"} appended in that order, and various @{text "props"} being
- claimed here. The @{text "initial_method"} is invoked with facts
- and goals together and refines the problem to something that is
- handled recursively in the proof @{text "body"}. The @{text
- "terminal_method"} has another chance to finish-off any remaining
+ The goal configuration consists of @{text "facts\<^sub>1"} and
+ @{text "facts\<^sub>2"} appended in that order, and various @{text
+ "props"} being claimed. The @{text "initial_method"} is invoked
+ with facts and goals together and refines the problem to something
+ that is handled recursively in the proof @{text "body"}. The @{text
+ "terminal_method"} has another chance to finish any remaining
subgoals, but it does not see the facts of the initial step.
- \medskip The second pattern illustrates unstructured proof scripts:
+ \medskip This pattern illustrates unstructured proof scripts:
\medskip
\begin{tabular}{l}
@@ -251,14 +251,14 @@
\end{tabular}
\medskip
- The @{text "method\<^sub>1"} operates on the original claim together while
+ The @{text "method\<^sub>1"} operates on the original claim while
using @{text "facts\<^sub>1"}. Since the @{command apply} command
- structurally resets the facts, the @{text "method\<^sub>2"} will operate on
- the remaining goal state without facts. The @{text "method\<^sub>3"} will
- see again a collection of @{text "facts\<^sub>3"} that has been inserted
- into the script explicitly.
+ structurally resets the facts, the @{text "method\<^sub>2"} will
+ operate on the remaining goal state without facts. The @{text
+ "method\<^sub>3"} will see again a collection of @{text
+ "facts\<^sub>3"} that has been inserted into the script explicitly.
- \medskip Empirically, Isar proof methods can be categorized as
+ \medskip Empirically, any Isar proof method can be categorized as
follows.
\begin{enumerate}
@@ -268,7 +268,8 @@
Example: @{method "induct"}, which is also a ``raw'' method since it
operates on the internal representation of simultaneous claims as
- Pure conjunction, instead of separate subgoals.
+ Pure conjunction (\secref{{sec:logic-aux}}), instead of separate
+ subgoals (\secref{sec::tactical-goals}).
\item \emph{Structured method} with strong emphasis on facts outside
the goal state.
@@ -285,8 +286,8 @@
\item \emph{Old-style tactic emulation} with detailed numeric goal
addressing and explicit references to entities of the internal goal
state (which are otherwise invisible from proper Isar proof text).
- To make the special non-standard status clear, the naming convention
- @{text "foo_tac"} needs to be observed.
+ The naming convention @{text "foo_tac"} makes this special
+ non-standard status clear.
Example: @{method "rule_tac"}.
@@ -396,9 +397,9 @@
The @{ML Attrib.thms} parser produces a list of theorems from the
usual Isar syntax involving attribute expressions etc.\ (syntax
- category @{syntax thmrefs}). The resulting @{verbatim thms} are
- added to @{ML HOL_basic_ss} which already contains the basic
- Simplifier setup for HOL.
+ category @{syntax thmrefs}) \cite{isabelle-isar-ref}. The resulting
+ @{verbatim thms} are added to @{ML HOL_basic_ss} which already
+ contains the basic Simplifier setup for HOL.
The tactic @{ML asm_full_simp_tac} is the one that is also used in
method @{method simp} by default. The extra wrapping by the @{ML
@@ -478,8 +479,8 @@
``simple'' methods, i.e.\ the goal facts are merely inserted as goal
premises by the @{ML SIMPLE_METHOD'} or @{ML SIMPLE_METHOD} wrapper.
For proof methods that are similar to the standard collection of
- @{method simp}, @{method blast}, @{method auto} little more can be
- done here.
+ @{method simp}, @{method blast}, @{method fast}, @{method auto}
+ there is little more that can be done.
Note that using the primary goal facts in the same manner as the
method arguments obtained via concrete syntax or the context does
@@ -503,8 +504,8 @@
manner, such as a discrimination net that is indexed by the
left-hand sides of rewrite rules. For variations on the Simplifier,
re-use of the existing type @{ML_type simpset} is adequate, but
- scalability requires it be maintained statically within the context
- data, not dynamically on each tool invocation. *}
+ scalability would require it be maintained statically within the
+ context data, not dynamically on each tool invocation. *}
section {* Attributes \label{sec:attributes} *}
--- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Oct 25 13:36:20 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Oct 25 16:18:00 2010 +0200
@@ -784,7 +784,7 @@
*}
-subsection {* Auxiliary definitions *}
+subsection {* Auxiliary definitions \label{sec:logic-aux} *}
text {*
Theory @{text "Pure"} provides a few auxiliary definitions, see
--- a/doc-src/IsarImplementation/Thy/ML.thy Mon Oct 25 13:36:20 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Mon Oct 25 16:18:00 2010 +0200
@@ -10,12 +10,12 @@
environment. This covers a variety of aspects that are geared
towards an efficient and robust platform for applications of formal
logic with fully foundational proof construction --- according to
- the well-known \emph{LCF principle}. There are specific library
- modules and infrastructure to address the needs for such difficult
- tasks. For example, the raw parallel programming model of Poly/ML
- is presented as considerably more abstract concept of \emph{future
- values}, which is then used to augment the inference kernel, proof
- interpreter, and theory loader accordingly.
+ the well-known \emph{LCF principle}. There is specific
+ infrastructure with library modules to address the needs of this
+ difficult task. For example, the raw parallel programming model of
+ Poly/ML is presented as considerably more abstract concept of
+ \emph{future values}, which is then used to augment the inference
+ kernel, proof interpreter, and theory loader accordingly.
The main aspects of Isabelle/ML are introduced below. These
first-hand explanations should help to understand how proper
@@ -47,14 +47,14 @@
standardization. A coding style that is changed every few years or
with every new contributor is no style at all, because consistency
is quickly lost. Global consistency is hard to achieve, though.
- One should always strife at least for local consistency of modules
- and sub-systems, without deviating from some general principles how
- to write Isabelle/ML.
+ Nonetheless, one should always strive at least for local consistency
+ of modules and sub-systems, without deviating from some general
+ principles how to write Isabelle/ML.
- In a sense, a common coding style is like an \emph{orthography} for
- the sources: it helps to read quickly over the text and see through
- the main points, without getting distracted by accidental
- presentation of free-style source.
+ In a sense, good coding style is like an \emph{orthography} for the
+ sources: it helps to read quickly over the text and see through the
+ main points, without getting distracted by accidental presentation
+ of free-style code.
*}
@@ -63,7 +63,7 @@
text {* Isabelle source files have a certain standardized header
format (with precise spacing) that follows ancient traditions
reaching back to the earliest versions of the system by Larry
- Paulson. E.g.\ see @{"file" "~~/src/Pure/thm.ML"}.
+ Paulson. See @{"file" "~~/src/Pure/thm.ML"}, for example.
The header includes at least @{verbatim Title} and @{verbatim
Author} entries, followed by a prose description of the purpose of
@@ -71,8 +71,8 @@
paragraphs of explanations.
The rest of the file is divided into sections, subsections,
- subsubsections, paragraphs etc.\ using some a layout via ML comments
- as follows.
+ subsubsections, paragraphs etc.\ using a simple layout via ML
+ comments as follows.
\begin{verbatim}
(*** section ***)
@@ -84,8 +84,8 @@
(*short paragraph*)
(*
- long paragraph
- more text
+ long paragraph,
+ with more text
*)
\end{verbatim}
@@ -94,7 +94,7 @@
as in the example above).
\medskip The precise wording of the prose text given in these
- headings is chosen carefully to indicate the main theme of the
+ headings is chosen carefully to introduce the main theme of the
subsequent formal ML text.
*}
@@ -106,31 +106,29 @@
\paragraph{Notation.} A name consists of 1--3 \emph{words} (rarely
4, but not more) that are separated by underscore. There are three
- variants concerning upper or lower case letters, which are just for
+ variants concerning upper or lower case letters, which are used for
certain ML categories as follows:
\medskip
\begin{tabular}{lll}
variant & example & ML categories \\\hline
lower-case & @{verbatim foo_bar} & values, types, record fields \\
- capitalized & @{verbatim Foo_Bar} & datatype constructors, \\
- & & structures, functors \\
- upper-case & @{verbatim FOO_BAR} & special values (combinators), \\
- & & exception constructors, signatures \\
+ capitalized & @{verbatim Foo_Bar} & datatype constructors, structures, functors \\
+ upper-case & @{verbatim FOO_BAR} & special values, exception constructors, signatures \\
\end{tabular}
\medskip
For historical reasons, many capitalized names omit underscores,
e.g.\ old-style @{verbatim FooBar} instead of @{verbatim Foo_Bar}.
- Genuine mixed-case names are \emph{not} used --- clear division of
- words is essential for readability.\footnote{Camel-case was invented
- to workaround the lack of underscore in some early non-ASCII
- character sets and keywords. Later it became a habitual in some
- language communities that are now strong in numbers.}
+ Genuine mixed-case names are \emph{not} used, bacause clear division
+ of words is essential for readability.\footnote{Camel-case was
+ invented to workaround the lack of underscore in some early
+ non-ASCII character sets. Later it became habitual in some language
+ communities that are now strong in numbers.}
A single (capital) character does not count as ``word'' in this
- respect: some Isabelle/ML are suffixed by extra markers like this:
- @{verbatim foo_barT}.
+ respect: some Isabelle/ML names are suffixed by extra markers like
+ this: @{verbatim foo_barT}.
Name variants are produced by adding 1--3 primes, e.g.\ @{verbatim
foo'}, @{verbatim foo''}, or @{verbatim foo'''}, but not @{verbatim
@@ -142,11 +140,11 @@
explicit qualification, as in @{ML Syntax.string_of_term} for
example. When devising names for structures and their components it
is important aim at eye-catching compositions of both parts, because
- this is how they are always seen in the sources and documentation.
- For the same reasons, aliases of well-known library functions should
- be avoided.
+ this is how they are seen in the sources and documentation. For the
+ same reasons, aliases of well-known library functions should be
+ avoided.
- Local names of function abstraction or case/lets bindings are
+ Local names of function abstraction or case/let bindings are
typically shorter, sometimes using only rudiments of ``words'',
while still avoiding cryptic shorthands. An auxiliary function
called @{verbatim helper}, @{verbatim aux}, or @{verbatim f} is
@@ -184,8 +182,8 @@
\end{verbatim}
- \paragraph{Specific conventions.} Here are some important specific
- name forms that occur frequently in the sources.
+ \paragraph{Specific conventions.} Here are some specific name forms
+ that occur frequently in the sources.
\begin{itemize}
@@ -211,8 +209,7 @@
\item Variables of the main context types of the Isabelle/Isar
framework (\secref{sec:context} and \chref{ch:local-theory}) have
- firm naming conventions to allow to visualize the their data flow
- via plain regular expressions in the editor. In particular:
+ firm naming conventions as follows:
\begin{itemize}
@@ -225,17 +222,20 @@
\item generic contexts are called @{verbatim context}, rarely
@{verbatim ctxt}
- \item local theories are called @{verbatim lthy}, unless there is an
- implicit conversion to a general proof context (semantic super-type)
+ \item local theories are called @{verbatim lthy}, except for local
+ theories that are treated as proof context (which is a semantic
+ super-type)
\end{itemize}
Variations with primed or decimal numbers are always possible, as
- well as ``sematic prefixes'' like @{verbatim foo_thy} or @{verbatim
+ well as sematic prefixes like @{verbatim foo_thy} or @{verbatim
bar_ctxt}, but the base conventions above need to be preserved.
+ This allows to visualize the their data flow via plain regular
+ expressions in the editor.
- \item The main logical entities (\secref{ch:logic}) also have
- established naming convention:
+ \item The main logical entities (\secref{ch:logic}) have established
+ naming convention as follows:
\begin{itemize}
@@ -259,9 +259,8 @@
Proper semantic names override these conventions completely. For
example, the left-hand side of an equation (as a term) can be called
- @{verbatim lhs} (not @{verbatim lhs_tm}). Or a term that is treated
- specifically as a variable can be called @{verbatim v} or @{verbatim
- x}.
+ @{verbatim lhs} (not @{verbatim lhs_tm}). Or a term that is known
+ to be a variable can be called @{verbatim v} or @{verbatim x}.
\end{itemize}
*}
@@ -275,11 +274,11 @@
programming.
\paragraph{Line length} is 80 characters according to ancient
- standards, but we allow as much as 100 characters, not
- more.\footnote{Readability requires to keep the beginning of a line
+ standards, but we allow as much as 100 characters (not
+ more).\footnote{Readability requires to keep the beginning of a line
in view while watching its end. Modern wide-screen displays do not
- change the way how the human brain works. As a rule of thumb,
- sources need to be printable on plain paper.} The extra 20
+ change the way how the human brain works. Sources also need to be
+ printable on plain paper with reasonable font-size.} The extra 20
characters acknowledge the space requirements due to qualified
library references in Isabelle/ML.
@@ -319,7 +318,8 @@
Note that the space between @{verbatim g} and the pair @{verbatim
"(a, b)"} follows the important principle of
\emph{compositionality}: the layout of @{verbatim "g p"} does not
- change when @{verbatim "p"} is refined to a concrete pair.
+ change when @{verbatim "p"} is refined to the concrete pair
+ @{verbatim "(a, b)"}.
\paragraph{Indentation} uses plain spaces, never hard
tabulators.\footnote{Tabulators were invented to move the carriage
@@ -329,7 +329,7 @@
editor configuration.}
Each level of nesting is indented by 2 spaces, sometimes 1, very
- rarely 4, never 8.
+ rarely 4, never 8 or any other odd number.
Indentation follows a simple logical format that only depends on the
nesting depth, not the accidental length of the text that initiates
@@ -362,18 +362,18 @@
\emph{maintainability}) etc.
\medskip For similar reasons, any kind of two-dimensional or tabular
- layouts, ASCII-art with lines or boxes of stars etc. should be
+ layouts, ASCII-art with lines or boxes of asterisks etc.\ should be
avoided.
- \paragraph{Complex expressions} consisting of multi-clausal function
- definitions, @{verbatim case}, @{verbatim handle}, @{verbatim let},
- or combinations require special attention. The syntax of Standard
- ML is a bit too ambitious in admitting too much variance that can
- distort the meaning of the text.
+ \paragraph{Complex expressions} that consist of multi-clausal
+ function definitions, @{verbatim handle}, @{verbatim case},
+ @{verbatim let} (and combinations) require special attention. The
+ syntax of Standard ML is quite ambitious and admits a lot of
+ variance that can distort the meaning of the text.
- Clauses of @{verbatim fun}, @{verbatim fn}, @{verbatim case},
- @{verbatim handle} get extra indentation to indicate the nesting
- clearly. For example:
+ Clauses of @{verbatim fun}, @{verbatim fn}, @{verbatim handle},
+ @{verbatim case} get extra indentation to indicate the nesting
+ clearly. Example:
\begin{verbatim}
(* RIGHT *)
@@ -394,8 +394,8 @@
Body expressions consisting of @{verbatim case} or @{verbatim let}
require care to maintain compositionality, to prevent loss of
- logical indentation where it is particularly imporant to see the
- structure of the text later on. Example:
+ logical indentation where it is especially important to see the
+ structure of the text. Example:
\begin{verbatim}
(* RIGHT *)
@@ -426,8 +426,8 @@
\end{verbatim}
Extra parentheses around @{verbatim case} expressions are optional,
- but help to analyse the nesting easily based on simple string
- matching in the editor.
+ but help to analyse the nesting based on character matching in the
+ editor.
\medskip There are two main exceptions to the overall principle of
compositionality in the layout of complex expressions.
@@ -448,7 +448,7 @@
\item @{verbatim fn} abstractions are often layed-out as if they
would lack any structure by themselves. This traditional form is
motivated by the possibility to shift function arguments back and
- forth wrt.\ additional combinators. For example:
+ forth wrt.\ additional combinators. Example:
\begin{verbatim}
(* RIGHT *)
@@ -493,34 +493,35 @@
(mainly Poly/ML, but also SML/NJ).
Isabelle/Pure marks the point where the original ML toplevel is
- superseded by the Isar toplevel that maintains a uniform environment
- for arbitrary ML values (see also \secref{sec:context}). This
- formal context holds logical entities as well as ML compiler
- bindings, among many other things. Raw Standard ML is never
- encountered again after the initial bootstrap of Isabelle/Pure.
+ superseded by the Isar toplevel that maintains a uniform context for
+ arbitrary ML values (see also \secref{sec:context}). This formal
+ environment holds ML compiler bindings, logical entities, and many
+ other things. Raw SML is never encountered again after the initial
+ bootstrap of Isabelle/Pure.
- Object-logics such as Isabelle/HOL are built within the
- Isabelle/ML/Isar environment of Pure by introducing suitable
- theories with associated ML text, either inlined or as separate
- files. Thus Isabelle/HOL is defined as a regular user-space
- application within the Isabelle framework. Further add-on tools can
- be implemented in ML within the Isar context in the same manner: ML
- is part of the regular user-space repertoire of Isabelle.
+ Object-logics like Isabelle/HOL are built within the
+ Isabelle/ML/Isar environment by introducing suitable theories with
+ associated ML modules, either inlined or as separate files. Thus
+ Isabelle/HOL is defined as a regular user-space application within
+ the Isabelle framework. Further add-on tools can be implemented in
+ ML within the Isar context in the same manner: ML is part of the
+ standard repertoire of Isabelle, and there is no distinction between
+ ``user'' and ``developer'' in this respect.
*}
subsection {* Isar ML commands *}
-text {* The primary Isar source language provides various facilities
- to open a ``window'' to the underlying ML compiler. Especially see
- @{command_ref "use"} and @{command_ref "ML"}, which work exactly the
+text {* The primary Isar source language provides facilities to ``open
+ a window'' to the underlying ML compiler. Especially see the Isar
+ commands @{command_ref "use"} and @{command_ref "ML"}: both work the
same way, only the source text is provided via a file vs.\ inlined,
respectively. Apart from embedding ML into the main theory
definition like that, there are many more commands that refer to ML
source, such as @{command_ref setup} or @{command_ref declaration}.
- An example of even more fine-grained embedding of ML into Isar is
- the proof method @{method_ref tactic}, which refines the pending goal state
- via a given expression of type @{ML_type tactic}.
+ Even more fine-grained embedding of ML into Isar is encountered in
+ the proof method @{method_ref tactic}, which refines the pending
+ goal state via a given expression of type @{ML_type tactic}.
*}
text %mlex {* The following artificial example demonstrates some ML
@@ -534,7 +535,7 @@
| factorial n = n * factorial (n - 1)
*}
-text {* Here the ML environment is really managed by Isabelle, i.e.\
+text {* Here the ML environment is already managed by Isabelle, i.e.\
the @{ML factorial} function is not yet accessible in the preceding
paragraph, nor in a different theory that is independent from the
current one in the import hierarchy.
@@ -542,33 +543,32 @@
Removing the above ML declaration from the source text will remove
any trace of this definition as expected. The Isabelle/ML toplevel
environment is managed in a \emph{stateless} way: unlike the raw ML
- toplevel or similar command loops of Computer Algebra systems, there
- are no global side-effects involved here.\footnote{Such a stateless
- compilation environment is also a prerequisite for robust parallel
- compilation within independent nodes of the implicit theory
- development graph.}
+ toplevel there are no global side-effects involved
+ here.\footnote{Such a stateless compilation environment is also a
+ prerequisite for robust parallel compilation within independent
+ nodes of the implicit theory development graph.}
- \medskip The next example shows how to embed ML into Isar proofs.
- Instead of @{command_ref "ML"} for theory mode, we use @{command_ref
- "ML_prf"} for proof mode. As illustrated below, its effect on the
- ML environment is local to the whole proof body, while ignoring its
- internal block structure. *}
+ \medskip The next example shows how to embed ML into Isar proofs, using
+ @{command_ref "ML_prf"} instead of Instead of @{command_ref "ML"}.
+ As illustrated below, the effect on the ML environment is local to
+ the whole proof body, ignoring the block structure.
+*}
example_proof
ML_prf %"ML" {* val a = 1 *}
- { -- {* Isar block structure ignored by ML environment *}
+ {
ML_prf %"ML" {* val b = a + 1 *}
} -- {* Isar block structure ignored by ML environment *}
ML_prf %"ML" {* val c = b + 1 *}
qed
text {* By side-stepping the normal scoping rules for Isar proof
- blocks, embedded ML code can refer to the different contexts
- explicitly, and manipulate corresponding entities, e.g.\ export a
- fact from a block context.
+ blocks, embedded ML code can refer to the different contexts and
+ manipulate corresponding entities, e.g.\ export a fact from a block
+ context.
\medskip Two further ML commands are useful in certain situations:
- @{command_ref ML_val} and @{command_ref ML_command} are both
+ @{command_ref ML_val} and @{command_ref ML_command} are
\emph{diagnostic} in the sense that there is no effect on the
underlying environment, and can thus used anywhere (even outside a
theory). The examples below produce long strings of digits by
@@ -591,14 +591,14 @@
formal context is passed as a thread-local reference variable. Thus
ML code may access the theory context during compilation, by reading
or writing the (local) theory under construction. Note that such
- direct access to the compile-time context is rare; in practice it is
- typically via some derived ML functions.
+ direct access to the compile-time context is rare. In practice it
+ is typically done via some derived ML functions instead.
*}
text %mlref {*
\begin{mldecls}
@{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
- @{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\
+ @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
@{index_ML bind_thms: "string * thm list -> unit"} \\
@{index_ML bind_thm: "string * thm -> unit"} \\
\end{mldecls}
@@ -620,11 +620,11 @@
put into a global ``standard'' format before being stored.
\item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a
- singleton theorem.
+ singleton fact.
\end{description}
- It is very important to note that the above functions are really
+ It is important to note that the above functions are really
restricted to the compile time, even though the ML compiler is
invoked at run-time. The majority of ML code either uses static
antiquotations (\secref{sec:ML-antiq}) or refers to the theory or
@@ -635,9 +635,8 @@
subsection {* Antiquotations \label{sec:ML-antiq} *}
text {* A very important consequence of embedding SML into Isar is the
- concept of \emph{ML antiquotation}. First, the standard token
- language of ML is augmented by special syntactic entities of the
- following form:
+ concept of \emph{ML antiquotation}. The standard token language of
+ ML is augmented by special syntactic entities of the following form:
\indexouternonterm{antiquote}
\begin{rail}
@@ -646,8 +645,8 @@
\end{rail}
Here @{syntax nameref} and @{syntax args} are regular outer syntax
- categories. Note that attributes and proof methods use similar
- syntax.
+ categories \cite{isabelle-isar-ref}. Attributes and proof methods
+ use similar syntax.
\medskip A regular antiquotation @{text "@{name args}"} processes
its arguments by the usual means of the Isar source language, and
@@ -664,7 +663,7 @@
effect by introducing local blocks within the pre-compilation
environment.
- \medskip See also \cite{Wenzel-Chaieb:2007b} for a slightly broader
+ \medskip See also \cite{Wenzel-Chaieb:2007b} for a broader
perspective on Isabelle/ML antiquotations. *}
text %mlantiq {*
@@ -698,10 +697,9 @@
\end{description}
*}
-text %mlex {* The following artificial example gives a first
- impression about using the antiquotation elements introduced so far,
- together with the basic @{text "@{thm}"} antiquotation defined
- later.
+text %mlex {* The following artificial example gives some impression
+ about the antiquotation elements introduced so far, together with
+ the important @{text "@{thm}"} antiquotation defined later.
*}
ML {*
@@ -712,9 +710,9 @@
\<rbrace>
*}
-text {*
- The extra block delimiters do not affect the compiled code itself, i.e.\
- function @{ML foo} is available in the present context.
+text {* The extra block delimiters do not affect the compiled code
+ itself, i.e.\ function @{ML foo} is available in the present context
+ of this paragraph.
*}
@@ -727,19 +725,19 @@
functions in that setting can save a lot of extra boiler-plate of
redundant shuffling of arguments, auxiliary abstractions etc.
- First of all, functions are usually \emph{curried}: the idea of
- @{text "f"} taking @{text "n"} arguments of type @{text "\<tau>\<^sub>i"} (for
- @{text "i \<in> {1, \<dots> n}"}) with result @{text "\<tau>"} is represented by
- the iterated function space @{text "\<tau>\<^sub>1 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>"}. This is
- isomorphic to the encoding via tuples @{text "\<tau>\<^sub>1 \<times> \<dots> \<times> \<tau>\<^sub>n \<rightarrow> \<tau>"}, but
- the curried version fits more smoothly into the basic
- calculus.\footnote{The difference is even more significant in
- higher-order logic, because additional the redundant tuple structure
- needs to be accommodated by formal reasoning.}
+ Functions are usually \emph{curried}: the idea of turning arguments
+ of type @{text "\<tau>\<^sub>i"} (for @{text "i \<in> {1, \<dots> n}"}) into a result of
+ type @{text "\<tau>"} is represented by the iterated function space
+ @{text "\<tau>\<^sub>1 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>"}. This is isomorphic to the well-known
+ encoding via tuples @{text "\<tau>\<^sub>1 \<times> \<dots> \<times> \<tau>\<^sub>n \<rightarrow> \<tau>"}, but the curried
+ version fits more smoothly into the basic calculus.\footnote{The
+ difference is even more significant in higher-order logic, because
+ the redundant tuple structure needs to be accommodated by formal
+ reasoning.}
Currying gives some flexiblity due to \emph{partial application}. A
function @{text "f: \<tau>\<^sub>1 \<rightarrow> \<tau>\<^bsub>2\<^esub> \<rightarrow> \<tau>"} can be applied to @{text "x: \<tau>\<^sub>1"}
- and the remaining @{text "(f x): \<tau>\<^sub>2 \<rightarrow> \<tau>"} passed to other functions
+ and the remaining @{text "(f x): \<tau>\<^sub>2 \<rightarrow> \<tau>"} passed to another function
etc. How well this works in practice depends on the order of
arguments. In the worst case, arguments are arranged erratically,
and using a function in a certain situation always requires some
@@ -747,11 +745,10 @@
decorate the code with meaningless permutations of arguments.
This can be avoided by \emph{canonical argument order}, which
- observes certain standard patterns of function definitions and
- minimizes adhoc permutations in their application. In Isabelle/ML,
- large portions of non-trivial source code are written without ever
- using the infamous function @{text "swap: \<alpha> \<times> \<beta> \<rightarrow> \<beta> \<times> \<alpha>"} or the
- combinator @{text "C: (\<alpha> \<rightarrow> \<beta> \<rightarrow> \<gamma>) \<rightarrow> (\<beta> \<rightarrow> \<alpha> \<rightarrow> \<gamma>)"}, which is not even
+ observes certain standard patterns and minimizes adhoc permutations
+ in their application. In Isabelle/ML, large portions text can be
+ written without ever using @{text "swap: \<alpha> \<times> \<beta> \<rightarrow> \<beta> \<times> \<alpha>"}, or the
+ combinator @{text "C: (\<alpha> \<rightarrow> \<beta> \<rightarrow> \<gamma>) \<rightarrow> (\<beta> \<rightarrow> \<alpha> \<rightarrow> \<gamma>)"} that is not even
defined in our library.
\medskip The basic idea is that arguments that vary less are moved
@@ -779,15 +776,16 @@
concrete container. The argument order makes it easy to use other
combinators: @{text "forall (member B) list"} will check a list of
elements for membership in @{text "B"} etc. Often the explicit
- @{text "list"} is pointless and can be contracted in the application
- @{text "forall (member B)"} to get directly a predicate again.
+ @{text "list"} is pointless and can be contracted to @{text "forall
+ (member B)"} to get directly a predicate again.
- The update operation naturally ``varies'' the container, so it moves
+ In contrast, an update operation varies the container, so it moves
to the right: @{text "insert a"} is a function @{text "\<beta> \<rightarrow> \<beta>"} to
insert a value @{text "a"}. These can be composed naturally as
- follows: @{text "insert c \<circ> insert b \<circ> insert a"}. This works well,
- apart from some awkwardness due to conventional mathematical
- function composition, which can be easily amended as follows.
+ @{text "insert c \<circ> insert b \<circ> insert a"}. The slightly awkward
+ inversion if the composition order is due to conventional
+ mathematical notation, which can be easily amended as explained
+ below.
*}
@@ -795,10 +793,10 @@
text {* Regular function application and infix notation works best for
relatively deeply structured expressions, e.g.\ @{text "h (f x y + g
- z)"}. The important special case if \emph{linear transformation}
- applies a cascade of functions as follows: @{text "f\<^sub>n (\<dots> (f\<^sub>1 x))"}.
- This becomes hard to read and maintain if the functions are
- themselves complex expressions. The notation can be significantly
+ z)"}. The important special case of \emph{linear transformation}
+ applies a cascade of functions @{text "f\<^sub>n (\<dots> (f\<^sub>1 x))"}. This
+ becomes hard to read and maintain if the functions are themselves
+ given as complex expressions. The notation can be significantly
improved by introducing \emph{forward} versions of application and
composition as follows:
@@ -840,7 +838,7 @@
subsection {* Canonical iteration *}
text {* As explained above, a function @{text "f: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>"} can be
- understood as update on a configuration of type @{text "\<beta>"} that is
+ understood as update on a configuration of type @{text "\<beta>"},
parametrized by arguments of type @{text "\<alpha>"}. Given @{text "a: \<alpha>"}
the partial application @{text "(f a): \<beta> \<rightarrow> \<beta>"} operates
homogeneously on @{text "\<beta>"}. This can be iterated naturally over a
@@ -890,10 +888,10 @@
The literature on functional programming provides a multitude of
combinators called @{text "foldl"}, @{text "foldr"} etc. SML97
provides its own variations as @{ML List.foldl} and @{ML
- List.foldr}, while the classic Isabelle library still has the
- slightly more convenient historic @{ML Library.foldl} and @{ML
- Library.foldr}. To avoid further confusion, all of this should be
- ignored, and @{ML fold} (or @{ML fold_rev}) used exclusively.
+ List.foldr}, while the classic Isabelle library also has the
+ historic @{ML Library.foldl} and @{ML Library.foldr}. To avoid
+ further confusion, all of this should be ignored, and @{ML fold} (or
+ @{ML fold_rev}) used exclusively.
\end{warn}
*}
@@ -918,8 +916,9 @@
memory (``deforestation''), but requires some practice to read and
write it fluently.
- \medskip The next example elaborates this idea and demonstrates fast
- accumulation of tree content using a text buffer.
+ \medskip The next example elaborates the idea of canonical
+ iteration, demonstrating fast accumulation of tree content using a
+ text buffer.
*}
ML {*
@@ -943,31 +942,28 @@
text {* The slow part of @{ML slow_content} is the @{ML implode} of
the recursive results, because it copies previously produced strings
- afresh.
+ again.
The incremental @{ML add_content} avoids this by operating on a
- buffer that is passed-through in a linear fashion. Using @{verbatim
- "#>"} and contraction over the actual @{ML_type "Buffer.T"} argument
- saves some additional boiler-plate, but requires again some
- practice. Of course, the two @{ML "Buffer.add"} invocations with
- concatenated strings could have been split into smaller parts, but
- this would have obfuscated the source without making a big
- difference in allocations. Here we have done some
+ buffer that is passed through in a linear fashion. Using @{verbatim
+ "#>"} and contraction over the actual buffer argument saves some
+ additional boiler-plate. Of course, the two @{ML "Buffer.add"}
+ invocations with concatenated strings could have been split into
+ smaller parts, but this would have obfuscated the source without
+ making a big difference in allocations. Here we have done some
peephole-optimization for the sake of readability.
Another benefit of @{ML add_content} is its ``open'' form as a
- function on @{ML_type Buffer.T} that can be continued in further
- linear transformations, folding etc. Thus it is more compositional
- than the naive @{ML slow_content}. As a realistic example, compare
- the slightly old-style @{ML "Term.maxidx_of_term: term -> int"} with
- the newer @{ML "Term.maxidx_term: term -> int -> int"} in
- Isabelle/Pure.
+ function on buffers that can be continued in further linear
+ transformations, folding etc. Thus it is more compositional than
+ the naive @{ML slow_content}. As realistic example, compare the
+ old-style @{ML "Term.maxidx_of_term: term -> int"} with the newer
+ @{ML "Term.maxidx_term: term -> int -> int"} in Isabelle/Pure.
- Note that @{ML fast_content} above is only defined for completeness
- of the example. In many practical situations, it is customary to
- defined the incremental @{ML add_content} only and leave the
- initialization and termination to the concrete application by the
- user.
+ Note that @{ML fast_content} above is only defined as example. In
+ many practical situations, it is customary to provide the
+ incremental @{ML add_content} only and leave the initialization and
+ termination to the concrete application by the user.
*}
@@ -1016,12 +1012,12 @@
\item @{ML warning}~@{text "text"} outputs @{text "text"} as
warning, which typically means some extra emphasis on the front-end
- side (color highlighting, icon).
+ side (color highlighting, icons, etc.).
\item @{ML error}~@{text "text"} raises exception @{ML ERROR}~@{text
"text"} and thus lets the Isar toplevel print @{text "text"} on the
error channel, which typically means some extra emphasis on the
- front-end side (color highlighting, icon).
+ front-end side (color highlighting, icons, etc.).
This assumes that the exception is not handled before the command
terminates. Handling exception @{ML ERROR}~@{text "text"} is a
@@ -1032,7 +1028,7 @@
The actual error channel is accessed via @{ML Output.error_msg}, but
the interaction protocol of Proof~General \emph{crashes} if that
function is used in regular ML code: error output and toplevel
- command failure always need to coincide here.
+ command failure always need to coincide.
\end{warn}
\end{description}
@@ -1046,14 +1042,14 @@
some system console log, with a low chance that the user will ever
see it. Moreover, as a genuine side-effect on global process
channels, there is no proper way to retract output when Isar command
- transactions are reset.
+ transactions are reset by the system.
\end{warn}
\begin{warn}
The message channels should be used in a message-oriented manner.
- This means that multi-line output that logically belongs together
- needs to be issued by a \emph{single} invocation of @{ML writeln}
- etc. with the functional concatenation of all message constituents.
+ This means that multi-line output that logically belongs together is
+ issued by a \emph{single} invocation of @{ML writeln} etc.\ with the
+ functional concatenation of all message constituents.
\end{warn}
*}
@@ -1108,16 +1104,16 @@
These exceptions indicate a genuine breakdown of the program, so the
main purpose is to determine quickly what has happened where.
Traditionally, the (short) exception message would include the name
- of an ML function, although this no longer necessary, because the ML
- runtime system prints a detailed source position of the
+ of an ML function, although this is no longer necessary, because the
+ ML runtime system prints a detailed source position of the
corresponding @{verbatim raise} keyword.
\medskip User modules can always introduce their own custom
exceptions locally, e.g.\ to organize internal failures robustly
without overlapping with existing exceptions. Exceptions that are
exposed in module signatures require extra care, though, and should
- \emph{not} be introduced by default. Surprise by end-users or ML
- users of a module can be often minimized by using plain user errors.
+ \emph{not} be introduced by default. Surprise by users of a module
+ can be often minimized by using plain user errors instead.
\paragraph{Interrupts.} These indicate arbitrary system events:
both the ML runtime system and the Isabelle/ML infrastructure signal
@@ -1131,7 +1127,7 @@
that intercepts interrupts becomes dependent on physical effects of
the environment. Even worse, exception handling patterns that are
too general by accident, e.g.\ by mispelled exception constructors,
- will cover interrupts unintentionally, and thus render the program
+ will cover interrupts unintentionally and thus render the program
semantics ill-defined.
Note that the Interrupt exception dates back to the original SML90
@@ -1139,8 +1135,8 @@
avoid its malign impact on ML program semantics, but without
providing a viable alternative. Isabelle/ML recovers physical
interruptibility (which an indispensable tool to implement managed
- evaluation of Isar command transactions), but requires user code to
- be strictly transparent wrt.\ interrupts.
+ evaluation of command transactions), but requires user code to be
+ strictly transparent wrt.\ interrupts.
\begin{warn}
Isabelle/ML user code needs to terminate promptly on interruption,
@@ -1174,8 +1170,8 @@
\item @{ML can} is similar to @{ML try} with more abstract result.
\item @{ML ERROR}~@{text "msg"} represents user errors; this
- exception is always raised via the @{ML error} function (see
- \secref{sec:message-channels}).
+ exception is normally raised indirectly via the @{ML error} function
+ (see \secref{sec:message-channels}).
\item @{ML Fail}~@{text "msg"} represents general program failures.
@@ -1187,12 +1183,11 @@
while preserving its implicit position information (if possible,
depending on the ML platform).
- \item @{ML exception_trace}~@{verbatim "(fn _ =>"}~@{text
+ \item @{ML exception_trace}~@{verbatim "(fn () =>"}~@{text
"e"}@{verbatim ")"} evaluates expression @{text "e"} while printing
a full trace of its stack of nested exceptions (if possible,
- depending on the ML platform).\footnote{In various versions of
- Poly/ML the trace will appear on raw stdout of the Isabelle
- process.}
+ depending on the ML platform).\footnote{In versions of Poly/ML the
+ trace will appear on raw stdout of the Isabelle process.}
Inserting @{ML exception_trace} into ML code temporarily is useful
for debugging, but not suitable for production code.
@@ -1207,10 +1202,10 @@
\begin{description}
- \item @{text "@{assert}"} inlines a function @{text "bool \<Rightarrow> unit"}
- that raises @{ML Fail} if the argument is @{ML false}. Due to
- inlining the source position of failed assertions is included in the
- error output.
+ \item @{text "@{assert}"} inlines a function
+ @{ML_type "bool -> unit"} that raises @{ML Fail} if the argument is
+ @{ML false}. Due to inlining the source position of failed
+ assertions is included in the error output.
\end{description}
*}
@@ -1218,12 +1213,12 @@
section {* Basic data types *}
-text {* The basis library proposal of SML97 need to be treated with
+text {* The basis library proposal of SML97 needs to be treated with
caution. Many of its operations simply do not fit with important
Isabelle/ML conventions (like ``canonical argument order'', see
- \secref{sec:canonical-argument-order}), others can cause serious
- problems with the parallel evaluation model of Isabelle/ML (such as
- @{ML TextIO.print} or @{ML OS.Process.system}).
+ \secref{sec:canonical-argument-order}), others cause problems with
+ the parallel evaluation model of Isabelle/ML (such as @{ML
+ TextIO.print} or @{ML OS.Process.system}).
Subsequently we give a brief overview of important operations on
basic ML data types.
@@ -1240,7 +1235,7 @@
\begin{description}
\item Type @{ML_type char} is \emph{not} used. The smallest textual
- unit in Isabelle is represented a ``symbol'' (see
+ unit in Isabelle is represented as a ``symbol'' (see
\secref{sec:symbols}).
\end{description}
@@ -1263,11 +1258,10 @@
This works uniformly for all supported ML platforms (Poly/ML and
SML/NJ).
- Literal integers in ML text (e.g.\ @{ML
- 123456789012345678901234567890}) are forced to be of this one true
+ Literal integers in ML text are forced to be of this one true
integer type --- overloading of SML97 is disabled.
- Structure @{ML_struct IntInf} of SML97 is obsolete, always use
+ Structure @{ML_struct IntInf} of SML97 is obsolete and superseded by
@{ML_struct Int}. Structure @{ML_struct Integer} in @{"file"
"~~/src/Pure/General/integer.ML"} provides some additional
operations.
@@ -1328,7 +1322,7 @@
Note that @{ML insert} is conservative about elements that are
already a @{ML member} of the list, while @{ML update} ensures that
- the last entry is always put in front. The latter discipline is
+ the latest entry is always put in front. The latter discipline is
often more appropriate in declarations of context data
(\secref{sec:context-data}) that are issued by the user in Isar
source: more recent declarations normally take precedence over
@@ -1337,12 +1331,12 @@
\end{description}
*}
-text %mlex {* Using canonical @{ML fold} together with canonical @{ML
- cons}, or similar standard operations, alternates the orientation of
- data. The is quite natural and should not altered forcible by
- inserting extra applications @{ML rev}. The alternative @{ML
- fold_rev} can be used in the relatively few situations, where
- alternation should be prevented.
+text %mlex {* Using canonical @{ML fold} together with @{ML cons}, or
+ similar standard operations, alternates the orientation of data.
+ The is quite natural and should not be altered forcible by inserting
+ extra applications of @{ML rev}. The alternative @{ML fold_rev} can
+ be used in the few situations, where alternation should be
+ prevented.
*}
ML {*
@@ -1393,7 +1387,8 @@
\item @{ML AList.lookup}, @{ML AList.defined}, @{ML AList.update}
implement the main ``framework operations'' for mappings in
- Isabelle/ML, with standard conventions for names and types.
+ Isabelle/ML, following standard conventions for their names and
+ types.
Note that a function called @{text lookup} is obliged to express its
partiality via an explicit option element. There is no choice to
@@ -1473,7 +1468,7 @@
Isabelle/Isar exploits the inherent structure of theories and proofs
to support \emph{implicit parallelism} to a large extent. LCF-style
- theorem provides almost ideal conditions for that; see also
+ theorem provides almost ideal conditions for that, see also
\cite{Wenzel:2009}. This means, significant parts of theory and
proof checking is parallelized by default. A maximum speedup-factor
of 3.0 on 4 cores and 5.0 on 8 cores can be
@@ -1486,11 +1481,10 @@
\medskip ML threads lack the memory protection of separate
processes, and operate concurrently on shared heap memory. This has
- the advantage that results of independent computations are
- immediately available to other threads: abstract values can be
- passed between threads without copying or awkward serialization that
- is typically required for explicit message passing between separate
- processes.
+ the advantage that results of independent computations are directly
+ available to other threads: abstract values can be passed without
+ copying or awkward serialization that is typically required for
+ separate processes.
To make shared-memory multi-threading work robustly and efficiently,
some programming guidelines need to be observed. While the ML
@@ -1535,15 +1529,15 @@
channels, environment variables, current working directory.
\item Writable resources in the file-system that are shared among
- different threads or other processes.
+ different threads or external processes.
\end{itemize}
Isabelle/ML provides various mechanisms to avoid critical shared
- resources in most practical situations. As last resort there are
- some mechanisms for explicit synchronization. The following
- guidelines help to make Isabelle/ML programs work smoothly in a
- concurrent environment.
+ resources in most situations. As last resort there are some
+ mechanisms for explicit synchronization. The following guidelines
+ help to make Isabelle/ML programs work smoothly in a concurrent
+ environment.
\begin{itemize}
@@ -1553,7 +1547,7 @@
plain value and user tools can get/map their own data in a purely
functional manner. Configuration options within the context
(\secref{sec:config-options}) provide simple drop-in replacements
- for formerly writable flags.
+ for historic reference variables.
\item Keep components with local state information re-entrant.
Instead of poking initial values into (private) global references, a
@@ -1669,8 +1663,8 @@
Entering the critical section without contention is very fast, and
several basic system operations do so frequently. Each thread
- should leave the critical section quickly, otherwise parallel
- performance may degrade.
+ should stay within the critical section quickly only very briefly,
+ otherwise parallel performance may degrade.
\item @{ML CRITICAL} is the same as @{ML NAMED_CRITICAL} with empty
name argument.
@@ -1684,26 +1678,22 @@
\item @{ML Synchronized.guarded_access}~@{text "var f"} lets the
function @{text "f"} operate within a critical section on the state
- @{text "x"} as follows: if @{text "f x"} produces @{ML NONE}, we
- continue to wait on the internal condition variable, expecting that
+ @{text "x"} as follows: if @{text "f x"} produces @{ML NONE}, it
+ continues to wait on the internal condition variable, expecting that
some other thread will eventually change the content in a suitable
- manner; if @{text "f x"} produces @{ML SOME}~@{text "(y, x')"} we
- are satisfied and assign the new state value @{text "x'"}, broadcast
- a signal to all waiting threads on the associated condition
- variable, and return the result @{text "y"}.
+ manner; if @{text "f x"} produces @{ML SOME}~@{text "(y, x')"} it is
+ satisfied and assigns the new state value @{text "x'"}, broadcasts a
+ signal to all waiting threads on the associated condition variable,
+ and returns the result @{text "y"}.
\end{description}
- There are some further variants of the general @{ML
+ There are some further variants of the @{ML
Synchronized.guarded_access} combinator, see @{"file"
"~~/src/Pure/Concurrent/synchronized.ML"} for details.
*}
-text %mlex {* See @{"file" "~~/src/Pure/Concurrent/mailbox.ML"} how to
- implement a mailbox as synchronized variable over a purely
- functional queue.
-
- \medskip The following example implements a counter that produces
+text %mlex {* The following example implements a counter that produces
positive integers that are unique over the runtime of the Isabelle
process:
*}
@@ -1726,4 +1716,8 @@
@{assert} (a <> b);
*}
+text {* \medskip See @{"file" "~~/src/Pure/Concurrent/mailbox.ML"} how
+ to implement a mailbox as synchronized variable over a purely
+ functional queue. *}
+
end
\ No newline at end of file
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Mon Oct 25 13:36:20 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Mon Oct 25 16:18:00 2010 +0200
@@ -640,7 +640,7 @@
setup my_flag_setup
text {* Now the user can refer to @{attribute my_flag} in
- declarations, while we can retrieve the current value from the
+ declarations, while ML tools can retrieve the current value from the
context via @{ML Config.get}. *}
ML_val {* @{assert} (Config.get @{context} my_flag = false) *}
@@ -897,7 +897,7 @@
@{assert} (list2 = ["x", "xa", "a", "aa", "'a", "'aa"]);
*}
-text {* \medskip The same works reletively to the formal context as
+text {* \medskip The same works relatively to the formal context as
follows. *}
locale ex = fixes a b c :: 'a
@@ -1210,13 +1210,13 @@
*}
text %mlex {* The following example yields the source position of some
- concrete binding inlined into the text.
+ concrete binding inlined into the text:
*}
ML {* Binding.pos_of @{binding here} *}
text {* \medskip That position can be also printed in a message as
- follows. *}
+ follows: *}
ML_command {*
writeln
@@ -1225,6 +1225,7 @@
text {* This illustrates a key virtue of formalized bindings as
opposed to raw specifications of base names: the system can use this
- additional information for advanced feedback given to the user. *}
+ additional information for feedback given to the user (error
+ messages etc.). *}
end
--- a/doc-src/IsarImplementation/Thy/Proof.thy Mon Oct 25 13:36:20 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Mon Oct 25 16:18:00 2010 +0200
@@ -180,13 +180,12 @@
val t2 = Syntax.read_term ctxt2 "x"; (*x::nat is enforced*)
*}
-text {* In the above example, the starting context had been derived
- from the toplevel theory, which means that fixed variables are
- internalized literally: @{verbatim "x"} is mapped again to
- @{verbatim "x"}, and attempting to fix it again in the subsequent
- context is an error. Alternatively, fixed parameters can be renamed
- explicitly as follows:
-*}
+text {* In the above example, the starting context is derived from the
+ toplevel theory, which means that fixed variables are internalized
+ literally: @{verbatim "x"} is mapped again to @{verbatim "x"}, and
+ attempting to fix it again in the subsequent context is an error.
+ Alternatively, fixed parameters can be renamed explicitly as
+ follows: *}
ML {*
val ctxt0 = @{context};
--- a/doc-src/IsarImplementation/Thy/document/Base.tex Mon Oct 25 13:36:20 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Base.tex Mon Oct 25 16:18:00 2010 +0200
@@ -11,41 +11,8 @@
\ Base\isanewline
\isakeyword{imports}\ Main\isanewline
\isakeyword{uses}\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isacharslash}{\isachardot}{\isachardot}{\isacharslash}antiquote{\isacharunderscore}setup{\isachardot}ML{\isachardoublequoteclose}\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-\isanewline
-%
-\endisadelimtheory
-\isanewline
-%
-\isadelimML
+\isakeyword{begin}\isanewline
\isanewline
-%
-\endisadelimML
-%
-\isatagML
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\isanewline
-\ \ ML{\isacharunderscore}Antiquote{\isachardot}inline\ {\isachardoublequote}assert{\isachardoublequote}\isanewline
-\ \ \ \ {\isacharparenleft}Scan{\isachardot}succeed\ {\isachardoublequote}{\isacharparenleft}fn\ b\ {\isacharequal}{\isachargreater}\ if\ b\ then\ {\isacharparenleft}{\isacharparenright}\ else\ raise\ General{\isachardot}Fail\ {\isacharbackslash}{\isachardoublequote}Assertion\ failed{\isacharbackslash}{\isachardoublequote}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isanewline
-{\isacharverbatimclose}%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-\isanewline
-%
-\endisadelimML
-%
-\isadelimtheory
-\isanewline
-%
-\endisadelimtheory
-%
-\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
--- a/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Oct 25 13:36:20 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Oct 25 16:18:00 2010 +0200
@@ -23,8 +23,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The Isar proof language (see also \cite[\S2]{isabelle-isar-ref})
- consists of three main categories of language elements:
+The Isar proof language (see also
+ \cite[\S2]{isabelle-isar-ref}) consists of three main categories of
+ language elements as follows.
\begin{enumerate}
@@ -63,12 +64,12 @@
A \emph{proof command} is state transition of the Isar/VM
proof interpreter.
- In principle, Isar proof commands could be defined in
- user-space as well. The system is built like that in the first
- place: part of the commands are primitive, the other part is defined
- as derived elements. Adding to the genuine structured proof
- language requires profound understanding of the Isar/VM machinery,
- though, so this is beyond the scope of this manual.
+ In principle, Isar proof commands could be defined in user-space as
+ well. The system is built like that in the first place: one part of
+ the commands are primitive, the other part is defined as derived
+ elements. Adding to the genuine structured proof language requires
+ profound understanding of the Isar/VM machinery, though, so this is
+ beyond the scope of this manual.
What can be done realistically is to define some diagnostic commands
that inspect the general state of the Isar/VM, and report some
@@ -77,8 +78,8 @@
goals (if available).
Another common application is to define a toplevel command that
- poses a problem to the user as Isar proof state and stores the final
- result in a suitable context data slot. Thus a proof can be
+ poses a problem to the user as Isar proof state and processes the
+ final result relatively to the context. Thus a proof can be
incorporated into the context of some user-space tool, without
modifying the Isar proof language itself.%
\end{isamarkuptext}%
@@ -154,13 +155,14 @@
storing named facts). Note that at this generic level the target
context is specified as \verb|Proof.context|, but the usual
wrapping of toplevel proofs into command transactions will provide a
- \verb|local_theory| here (see also \chref{ch:local-theory}).
- This usually affects the way how results are stored.
+ \verb|local_theory| here (\chref{ch:local-theory}). This
+ affects the way how results are stored.
The \isa{statement} is given as a nested list of terms, each
associated with optional \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns as usual in the
- Isar source language. The original list structure over terms is
- turned into one over theorems when \isa{after{\isacharunderscore}qed} is invoked.
+ Isar source language. The original nested list structure over terms
+ is turned into one over theorems when \isa{after{\isacharunderscore}qed} is
+ invoked.
\end{description}%
\end{isamarkuptext}%
@@ -324,15 +326,15 @@
\end{itemize}
- \medskip Syntactically, the language of proof methods is embedded
- into Isar as arguments to certain commands, e.g.\ \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}} or
- \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}. User-space additions are reasonably easy by
- plugging suitable method-valued parser functions into the framework,
- using the \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}} command, for example.
+ \medskip Syntactically, the language of proof methods appears as
+ arguments to Isar commands like \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}} or \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}.
+ User-space additions are reasonably easy by plugging suitable
+ method-valued parser functions into the framework, using the
+ \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}} command, for example.
To get a better idea about the range of possibilities, consider the
- following Isar proof schemes. First some general form of structured
- proof text:
+ following Isar proof schemes. This is the general form of
+ structured proof text:
\medskip
\begin{tabular}{l}
@@ -343,13 +345,13 @@
\end{tabular}
\medskip
- The goal configuration consists of \isa{facts\isactrlsub {\isadigit{1}}} and \isa{facts\isactrlsub {\isadigit{2}}} appended in that order, and various \isa{props} being
- claimed here. The \isa{initial{\isacharunderscore}method} is invoked with facts
- and goals together and refines the problem to something that is
- handled recursively in the proof \isa{body}. The \isa{terminal{\isacharunderscore}method} has another chance to finish-off any remaining
+ The goal configuration consists of \isa{facts\isactrlsub {\isadigit{1}}} and
+ \isa{facts\isactrlsub {\isadigit{2}}} appended in that order, and various \isa{props} being claimed. The \isa{initial{\isacharunderscore}method} is invoked
+ with facts and goals together and refines the problem to something
+ that is handled recursively in the proof \isa{body}. The \isa{terminal{\isacharunderscore}method} has another chance to finish any remaining
subgoals, but it does not see the facts of the initial step.
- \medskip The second pattern illustrates unstructured proof scripts:
+ \medskip This pattern illustrates unstructured proof scripts:
\medskip
\begin{tabular}{l}
@@ -361,14 +363,12 @@
\end{tabular}
\medskip
- The \isa{method\isactrlsub {\isadigit{1}}} operates on the original claim together while
+ The \isa{method\isactrlsub {\isadigit{1}}} operates on the original claim while
using \isa{facts\isactrlsub {\isadigit{1}}}. Since the \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} command
- structurally resets the facts, the \isa{method\isactrlsub {\isadigit{2}}} will operate on
- the remaining goal state without facts. The \isa{method\isactrlsub {\isadigit{3}}} will
- see again a collection of \isa{facts\isactrlsub {\isadigit{3}}} that has been inserted
- into the script explicitly.
+ structurally resets the facts, the \isa{method\isactrlsub {\isadigit{2}}} will
+ operate on the remaining goal state without facts. The \isa{method\isactrlsub {\isadigit{3}}} will see again a collection of \isa{facts\isactrlsub {\isadigit{3}}} that has been inserted into the script explicitly.
- \medskip Empirically, Isar proof methods can be categorized as
+ \medskip Empirically, any Isar proof method can be categorized as
follows.
\begin{enumerate}
@@ -378,7 +378,8 @@
Example: \hyperlink{method.induct}{\mbox{\isa{induct}}}, which is also a ``raw'' method since it
operates on the internal representation of simultaneous claims as
- Pure conjunction, instead of separate subgoals.
+ Pure conjunction (\secref{{sec:logic-aux}}), instead of separate
+ subgoals (\secref{sec::tactical-goals}).
\item \emph{Structured method} with strong emphasis on facts outside
the goal state.
@@ -395,8 +396,8 @@
\item \emph{Old-style tactic emulation} with detailed numeric goal
addressing and explicit references to entities of the internal goal
state (which are otherwise invisible from proper Isar proof text).
- To make the special non-standard status clear, the naming convention
- \isa{foo{\isacharunderscore}tac} needs to be observed.
+ The naming convention \isa{foo{\isacharunderscore}tac} makes this special
+ non-standard status clear.
Example: \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}}.
@@ -610,9 +611,9 @@
The \verb|Attrib.thms| parser produces a list of theorems from the
usual Isar syntax involving attribute expressions etc.\ (syntax
- category \hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}). The resulting \verb|thms| are
- added to \verb|HOL_basic_ss| which already contains the basic
- Simplifier setup for HOL.
+ category \hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}) \cite{isabelle-isar-ref}. The resulting
+ \verb|thms| are added to \verb|HOL_basic_ss| which already
+ contains the basic Simplifier setup for HOL.
The tactic \verb|asm_full_simp_tac| is the one that is also used in
method \hyperlink{method.simp}{\mbox{\isa{simp}}} by default. The extra wrapping by the \verb|CHANGED| tactical ensures progress of simplification: identical goal
@@ -795,8 +796,8 @@
``simple'' methods, i.e.\ the goal facts are merely inserted as goal
premises by the \verb|SIMPLE_METHOD'| or \verb|SIMPLE_METHOD| wrapper.
For proof methods that are similar to the standard collection of
- \hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.blast}{\mbox{\isa{blast}}}, \hyperlink{method.auto}{\mbox{\isa{auto}}} little more can be
- done here.
+ \hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.blast}{\mbox{\isa{blast}}}, \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.auto}{\mbox{\isa{auto}}}
+ there is little more that can be done.
Note that using the primary goal facts in the same manner as the
method arguments obtained via concrete syntax or the context does
@@ -819,8 +820,8 @@
manner, such as a discrimination net that is indexed by the
left-hand sides of rewrite rules. For variations on the Simplifier,
re-use of the existing type \verb|simpset| is adequate, but
- scalability requires it be maintained statically within the context
- data, not dynamically on each tool invocation.%
+ scalability would require it be maintained statically within the
+ context data, not dynamically on each tool invocation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Oct 25 13:36:20 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Oct 25 16:18:00 2010 +0200
@@ -829,7 +829,7 @@
%
\endisadelimmlantiq
%
-\isamarkupsubsection{Auxiliary definitions%
+\isamarkupsubsection{Auxiliary definitions \label{sec:logic-aux}%
}
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Mon Oct 25 13:36:20 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Mon Oct 25 16:18:00 2010 +0200
@@ -29,12 +29,12 @@
environment. This covers a variety of aspects that are geared
towards an efficient and robust platform for applications of formal
logic with fully foundational proof construction --- according to
- the well-known \emph{LCF principle}. There are specific library
- modules and infrastructure to address the needs for such difficult
- tasks. For example, the raw parallel programming model of Poly/ML
- is presented as considerably more abstract concept of \emph{future
- values}, which is then used to augment the inference kernel, proof
- interpreter, and theory loader accordingly.
+ the well-known \emph{LCF principle}. There is specific
+ infrastructure with library modules to address the needs of this
+ difficult task. For example, the raw parallel programming model of
+ Poly/ML is presented as considerably more abstract concept of
+ \emph{future values}, which is then used to augment the inference
+ kernel, proof interpreter, and theory loader accordingly.
The main aspects of Isabelle/ML are introduced below. These
first-hand explanations should help to understand how proper
@@ -70,14 +70,14 @@
standardization. A coding style that is changed every few years or
with every new contributor is no style at all, because consistency
is quickly lost. Global consistency is hard to achieve, though.
- One should always strife at least for local consistency of modules
- and sub-systems, without deviating from some general principles how
- to write Isabelle/ML.
+ Nonetheless, one should always strive at least for local consistency
+ of modules and sub-systems, without deviating from some general
+ principles how to write Isabelle/ML.
- In a sense, a common coding style is like an \emph{orthography} for
- the sources: it helps to read quickly over the text and see through
- the main points, without getting distracted by accidental
- presentation of free-style source.%
+ In a sense, good coding style is like an \emph{orthography} for the
+ sources: it helps to read quickly over the text and see through the
+ main points, without getting distracted by accidental presentation
+ of free-style code.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -89,15 +89,15 @@
Isabelle source files have a certain standardized header
format (with precise spacing) that follows ancient traditions
reaching back to the earliest versions of the system by Larry
- Paulson. E.g.\ see \hyperlink{file.~~/src/Pure/thm.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}thm{\isachardot}ML}}}}.
+ Paulson. See \hyperlink{file.~~/src/Pure/thm.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}thm{\isachardot}ML}}}}, for example.
The header includes at least \verb|Title| and \verb|Author| entries, followed by a prose description of the purpose of
the module. The latter can range from a single line to several
paragraphs of explanations.
The rest of the file is divided into sections, subsections,
- subsubsections, paragraphs etc.\ using some a layout via ML comments
- as follows.
+ subsubsections, paragraphs etc.\ using a simple layout via ML
+ comments as follows.
\begin{verbatim}
(*** section ***)
@@ -109,8 +109,8 @@
(*short paragraph*)
(*
- long paragraph
- more text
+ long paragraph,
+ with more text
*)
\end{verbatim}
@@ -119,7 +119,7 @@
as in the example above).
\medskip The precise wording of the prose text given in these
- headings is chosen carefully to indicate the main theme of the
+ headings is chosen carefully to introduce the main theme of the
subsequent formal ML text.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -134,31 +134,29 @@
\paragraph{Notation.} A name consists of 1--3 \emph{words} (rarely
4, but not more) that are separated by underscore. There are three
- variants concerning upper or lower case letters, which are just for
+ variants concerning upper or lower case letters, which are used for
certain ML categories as follows:
\medskip
\begin{tabular}{lll}
variant & example & ML categories \\\hline
lower-case & \verb|foo_bar| & values, types, record fields \\
- capitalized & \verb|Foo_Bar| & datatype constructors, \\
- & & structures, functors \\
- upper-case & \verb|FOO_BAR| & special values (combinators), \\
- & & exception constructors, signatures \\
+ capitalized & \verb|Foo_Bar| & datatype constructors, structures, functors \\
+ upper-case & \verb|FOO_BAR| & special values, exception constructors, signatures \\
\end{tabular}
\medskip
For historical reasons, many capitalized names omit underscores,
e.g.\ old-style \verb|FooBar| instead of \verb|Foo_Bar|.
- Genuine mixed-case names are \emph{not} used --- clear division of
- words is essential for readability.\footnote{Camel-case was invented
- to workaround the lack of underscore in some early non-ASCII
- character sets and keywords. Later it became a habitual in some
- language communities that are now strong in numbers.}
+ Genuine mixed-case names are \emph{not} used, bacause clear division
+ of words is essential for readability.\footnote{Camel-case was
+ invented to workaround the lack of underscore in some early
+ non-ASCII character sets. Later it became habitual in some language
+ communities that are now strong in numbers.}
A single (capital) character does not count as ``word'' in this
- respect: some Isabelle/ML are suffixed by extra markers like this:
- \verb|foo_barT|.
+ respect: some Isabelle/ML names are suffixed by extra markers like
+ this: \verb|foo_barT|.
Name variants are produced by adding 1--3 primes, e.g.\ \verb|foo'|, \verb|foo''|, or \verb|foo'''|, but not \verb|foo''''| or more. Decimal digits scale better to larger numbers,
e.g.\ \verb|foo0|, \verb|foo1|, \verb|foo42|.
@@ -168,11 +166,11 @@
explicit qualification, as in \verb|Syntax.string_of_term| for
example. When devising names for structures and their components it
is important aim at eye-catching compositions of both parts, because
- this is how they are always seen in the sources and documentation.
- For the same reasons, aliases of well-known library functions should
- be avoided.
+ this is how they are seen in the sources and documentation. For the
+ same reasons, aliases of well-known library functions should be
+ avoided.
- Local names of function abstraction or case/lets bindings are
+ Local names of function abstraction or case/let bindings are
typically shorter, sometimes using only rudiments of ``words'',
while still avoiding cryptic shorthands. An auxiliary function
called \verb|helper|, \verb|aux|, or \verb|f| is
@@ -210,8 +208,8 @@
\end{verbatim}
- \paragraph{Specific conventions.} Here are some important specific
- name forms that occur frequently in the sources.
+ \paragraph{Specific conventions.} Here are some specific name forms
+ that occur frequently in the sources.
\begin{itemize}
@@ -236,8 +234,7 @@
\item Variables of the main context types of the Isabelle/Isar
framework (\secref{sec:context} and \chref{ch:local-theory}) have
- firm naming conventions to allow to visualize the their data flow
- via plain regular expressions in the editor. In particular:
+ firm naming conventions as follows:
\begin{itemize}
@@ -249,16 +246,19 @@
\item generic contexts are called \verb|context|, rarely
\verb|ctxt|
- \item local theories are called \verb|lthy|, unless there is an
- implicit conversion to a general proof context (semantic super-type)
+ \item local theories are called \verb|lthy|, except for local
+ theories that are treated as proof context (which is a semantic
+ super-type)
\end{itemize}
Variations with primed or decimal numbers are always possible, as
- well as ``sematic prefixes'' like \verb|foo_thy| or \verb|bar_ctxt|, but the base conventions above need to be preserved.
+ well as sematic prefixes like \verb|foo_thy| or \verb|bar_ctxt|, but the base conventions above need to be preserved.
+ This allows to visualize the their data flow via plain regular
+ expressions in the editor.
- \item The main logical entities (\secref{ch:logic}) also have
- established naming convention:
+ \item The main logical entities (\secref{ch:logic}) have established
+ naming convention as follows:
\begin{itemize}
@@ -278,8 +278,8 @@
Proper semantic names override these conventions completely. For
example, the left-hand side of an equation (as a term) can be called
- \verb|lhs| (not \verb|lhs_tm|). Or a term that is treated
- specifically as a variable can be called \verb|v| or \verb|x|.
+ \verb|lhs| (not \verb|lhs_tm|). Or a term that is known
+ to be a variable can be called \verb|v| or \verb|x|.
\end{itemize}%
\end{isamarkuptext}%
@@ -296,11 +296,11 @@
programming.
\paragraph{Line length} is 80 characters according to ancient
- standards, but we allow as much as 100 characters, not
- more.\footnote{Readability requires to keep the beginning of a line
+ standards, but we allow as much as 100 characters (not
+ more).\footnote{Readability requires to keep the beginning of a line
in view while watching its end. Modern wide-screen displays do not
- change the way how the human brain works. As a rule of thumb,
- sources need to be printable on plain paper.} The extra 20
+ change the way how the human brain works. Sources also need to be
+ printable on plain paper with reasonable font-size.} The extra 20
characters acknowledge the space requirements due to qualified
library references in Isabelle/ML.
@@ -339,7 +339,8 @@
curried function, or \verb|g (a, b)| for a tupled function.
Note that the space between \verb|g| and the pair \verb|(a, b)| follows the important principle of
\emph{compositionality}: the layout of \verb|g p| does not
- change when \verb|p| is refined to a concrete pair.
+ change when \verb|p| is refined to the concrete pair
+ \verb|(a, b)|.
\paragraph{Indentation} uses plain spaces, never hard
tabulators.\footnote{Tabulators were invented to move the carriage
@@ -349,7 +350,7 @@
editor configuration.}
Each level of nesting is indented by 2 spaces, sometimes 1, very
- rarely 4, never 8.
+ rarely 4, never 8 or any other odd number.
Indentation follows a simple logical format that only depends on the
nesting depth, not the accidental length of the text that initiates
@@ -382,18 +383,18 @@
\emph{maintainability}) etc.
\medskip For similar reasons, any kind of two-dimensional or tabular
- layouts, ASCII-art with lines or boxes of stars etc. should be
+ layouts, ASCII-art with lines or boxes of asterisks etc.\ should be
avoided.
- \paragraph{Complex expressions} consisting of multi-clausal function
- definitions, \verb|case|, \verb|handle|, \verb|let|,
- or combinations require special attention. The syntax of Standard
- ML is a bit too ambitious in admitting too much variance that can
- distort the meaning of the text.
+ \paragraph{Complex expressions} that consist of multi-clausal
+ function definitions, \verb|handle|, \verb|case|,
+ \verb|let| (and combinations) require special attention. The
+ syntax of Standard ML is quite ambitious and admits a lot of
+ variance that can distort the meaning of the text.
- Clauses of \verb|fun|, \verb|fn|, \verb|case|,
- \verb|handle| get extra indentation to indicate the nesting
- clearly. For example:
+ Clauses of \verb|fun|, \verb|fn|, \verb|handle|,
+ \verb|case| get extra indentation to indicate the nesting
+ clearly. Example:
\begin{verbatim}
(* RIGHT *)
@@ -414,8 +415,8 @@
Body expressions consisting of \verb|case| or \verb|let|
require care to maintain compositionality, to prevent loss of
- logical indentation where it is particularly imporant to see the
- structure of the text later on. Example:
+ logical indentation where it is especially important to see the
+ structure of the text. Example:
\begin{verbatim}
(* RIGHT *)
@@ -446,8 +447,8 @@
\end{verbatim}
Extra parentheses around \verb|case| expressions are optional,
- but help to analyse the nesting easily based on simple string
- matching in the editor.
+ but help to analyse the nesting based on character matching in the
+ editor.
\medskip There are two main exceptions to the overall principle of
compositionality in the layout of complex expressions.
@@ -468,7 +469,7 @@
\item \verb|fn| abstractions are often layed-out as if they
would lack any structure by themselves. This traditional form is
motivated by the possibility to shift function arguments back and
- forth wrt.\ additional combinators. For example:
+ forth wrt.\ additional combinators. Example:
\begin{verbatim}
(* RIGHT *)
@@ -516,19 +517,20 @@
(mainly Poly/ML, but also SML/NJ).
Isabelle/Pure marks the point where the original ML toplevel is
- superseded by the Isar toplevel that maintains a uniform environment
- for arbitrary ML values (see also \secref{sec:context}). This
- formal context holds logical entities as well as ML compiler
- bindings, among many other things. Raw Standard ML is never
- encountered again after the initial bootstrap of Isabelle/Pure.
+ superseded by the Isar toplevel that maintains a uniform context for
+ arbitrary ML values (see also \secref{sec:context}). This formal
+ environment holds ML compiler bindings, logical entities, and many
+ other things. Raw SML is never encountered again after the initial
+ bootstrap of Isabelle/Pure.
- Object-logics such as Isabelle/HOL are built within the
- Isabelle/ML/Isar environment of Pure by introducing suitable
- theories with associated ML text, either inlined or as separate
- files. Thus Isabelle/HOL is defined as a regular user-space
- application within the Isabelle framework. Further add-on tools can
- be implemented in ML within the Isar context in the same manner: ML
- is part of the regular user-space repertoire of Isabelle.%
+ Object-logics like Isabelle/HOL are built within the
+ Isabelle/ML/Isar environment by introducing suitable theories with
+ associated ML modules, either inlined or as separate files. Thus
+ Isabelle/HOL is defined as a regular user-space application within
+ the Isabelle framework. Further add-on tools can be implemented in
+ ML within the Isar context in the same manner: ML is part of the
+ standard repertoire of Isabelle, and there is no distinction between
+ ``user'' and ``developer'' in this respect.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -537,16 +539,16 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The primary Isar source language provides various facilities
- to open a ``window'' to the underlying ML compiler. Especially see
- \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} and \indexref{}{command}{ML}\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which work exactly the
+The primary Isar source language provides facilities to ``open
+ a window'' to the underlying ML compiler. Especially see the Isar
+ commands \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} and \indexref{}{command}{ML}\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}: both work the
same way, only the source text is provided via a file vs.\ inlined,
respectively. Apart from embedding ML into the main theory
definition like that, there are many more commands that refer to ML
source, such as \indexref{}{command}{setup}\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} or \indexref{}{command}{declaration}\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}.
- An example of even more fine-grained embedding of ML into Isar is
- the proof method \indexref{}{method}{tactic}\hyperlink{method.tactic}{\mbox{\isa{tactic}}}, which refines the pending goal state
- via a given expression of type \verb|tactic|.%
+ Even more fine-grained embedding of ML into Isar is encountered in
+ the proof method \indexref{}{method}{tactic}\hyperlink{method.tactic}{\mbox{\isa{tactic}}}, which refines the pending
+ goal state via a given expression of type \verb|tactic|.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -589,7 +591,7 @@
\endisadelimML
%
\begin{isamarkuptext}%
-Here the ML environment is really managed by Isabelle, i.e.\
+Here the ML environment is already managed by Isabelle, i.e.\
the \verb|factorial| function is not yet accessible in the preceding
paragraph, nor in a different theory that is independent from the
current one in the import hierarchy.
@@ -597,16 +599,15 @@
Removing the above ML declaration from the source text will remove
any trace of this definition as expected. The Isabelle/ML toplevel
environment is managed in a \emph{stateless} way: unlike the raw ML
- toplevel or similar command loops of Computer Algebra systems, there
- are no global side-effects involved here.\footnote{Such a stateless
- compilation environment is also a prerequisite for robust parallel
- compilation within independent nodes of the implicit theory
- development graph.}
+ toplevel there are no global side-effects involved
+ here.\footnote{Such a stateless compilation environment is also a
+ prerequisite for robust parallel compilation within independent
+ nodes of the implicit theory development graph.}
- \medskip The next example shows how to embed ML into Isar proofs.
- Instead of \indexref{}{command}{ML}\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} for theory mode, we use \indexref{}{command}{ML\_prf}\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} for proof mode. As illustrated below, its effect on the
- ML environment is local to the whole proof body, while ignoring its
- internal block structure.%
+ \medskip The next example shows how to embed ML into Isar proofs, using
+ \indexref{}{command}{ML\_prf}\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} instead of Instead of \indexref{}{command}{ML}\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}.
+ As illustrated below, the effect on the ML environment is local to
+ the whole proof body, ignoring the block structure.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
@@ -620,9 +621,6 @@
\isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
\ {\isacharverbatimopen}\ val\ a\ {\isacharequal}\ {\isadigit{1}}\ {\isacharverbatimclose}\isanewline
\ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
-\ %
-\isamarkupcmt{Isar block structure ignored by ML environment%
-}
\isanewline
\ \ \ \ \isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
\ {\isacharverbatimopen}\ val\ b\ {\isacharequal}\ a\ {\isacharplus}\ {\isadigit{1}}\ {\isacharverbatimclose}\isanewline
@@ -644,12 +642,12 @@
%
\begin{isamarkuptext}%
By side-stepping the normal scoping rules for Isar proof
- blocks, embedded ML code can refer to the different contexts
- explicitly, and manipulate corresponding entities, e.g.\ export a
- fact from a block context.
+ blocks, embedded ML code can refer to the different contexts and
+ manipulate corresponding entities, e.g.\ export a fact from a block
+ context.
\medskip Two further ML commands are useful in certain situations:
- \indexref{}{command}{ML\_val}\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \indexref{}{command}{ML\_command}\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are both
+ \indexref{}{command}{ML\_val}\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \indexref{}{command}{ML\_command}\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are
\emph{diagnostic} in the sense that there is no effect on the
underlying environment, and can thus used anywhere (even outside a
theory). The examples below produce long strings of digits by
@@ -719,8 +717,8 @@
formal context is passed as a thread-local reference variable. Thus
ML code may access the theory context during compilation, by reading
or writing the (local) theory under construction. Note that such
- direct access to the compile-time context is rare; in practice it is
- typically via some derived ML functions.%
+ direct access to the compile-time context is rare. In practice it
+ is typically done via some derived ML functions instead.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -733,7 +731,7 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{ML\_Context.the\_generic\_context}\verb|ML_Context.the_generic_context: unit -> Context.generic| \\
- \indexdef{}{ML}{Context.$>$$>$}\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
+ \indexdef{}{ML}{Context.$>$$>$}\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
\indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
\indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
\end{mldecls}
@@ -755,11 +753,11 @@
put into a global ``standard'' format before being stored.
\item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a
- singleton theorem.
+ singleton fact.
\end{description}
- It is very important to note that the above functions are really
+ It is important to note that the above functions are really
restricted to the compile time, even though the ML compiler is
invoked at run-time. The majority of ML code either uses static
antiquotations (\secref{sec:ML-antiq}) or refers to the theory or
@@ -780,9 +778,8 @@
%
\begin{isamarkuptext}%
A very important consequence of embedding SML into Isar is the
- concept of \emph{ML antiquotation}. First, the standard token
- language of ML is augmented by special syntactic entities of the
- following form:
+ concept of \emph{ML antiquotation}. The standard token language of
+ ML is augmented by special syntactic entities of the following form:
\indexouternonterm{antiquote}
\begin{rail}
@@ -791,8 +788,8 @@
\end{rail}
Here \hyperlink{syntax.nameref}{\mbox{\isa{nameref}}} and \hyperlink{syntax.args}{\mbox{\isa{args}}} are regular outer syntax
- categories. Note that attributes and proof methods use similar
- syntax.
+ categories \cite{isabelle-isar-ref}. Attributes and proof methods
+ use similar syntax.
\medskip A regular antiquotation \isa{{\isacharat}{\isacharbraceleft}name\ args{\isacharbraceright}} processes
its arguments by the usual means of the Isar source language, and
@@ -808,7 +805,7 @@
effect by introducing local blocks within the pre-compilation
environment.
- \medskip See also \cite{Wenzel-Chaieb:2007b} for a slightly broader
+ \medskip See also \cite{Wenzel-Chaieb:2007b} for a broader
perspective on Isabelle/ML antiquotations.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -863,10 +860,9 @@
\isatagmlex
%
\begin{isamarkuptext}%
-The following artificial example gives a first
- impression about using the antiquotation elements introduced so far,
- together with the basic \isa{{\isacharat}{\isacharbraceleft}thm{\isacharbraceright}} antiquotation defined
- later.%
+The following artificial example gives some impression
+ about the antiquotation elements introduced so far, together with
+ the important \isa{{\isacharat}{\isacharbraceleft}thm{\isacharbraceright}} antiquotation defined later.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -910,8 +906,9 @@
\endisadelimML
%
\begin{isamarkuptext}%
-The extra block delimiters do not affect the compiled code itself, i.e.\
- function \verb|foo| is available in the present context.%
+The extra block delimiters do not affect the compiled code
+ itself, i.e.\ function \verb|foo| is available in the present context
+ of this paragraph.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -926,19 +923,19 @@
functions in that setting can save a lot of extra boiler-plate of
redundant shuffling of arguments, auxiliary abstractions etc.
- First of all, functions are usually \emph{curried}: the idea of
- \isa{f} taking \isa{n} arguments of type \isa{{\isasymtau}\isactrlsub i} (for
- \isa{i\ {\isasymin}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ n{\isacharbraceright}}) with result \isa{{\isasymtau}} is represented by
- the iterated function space \isa{{\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymrightarrow}\ {\isasymdots}\ {\isasymrightarrow}\ {\isasymtau}\isactrlsub n\ {\isasymrightarrow}\ {\isasymtau}}. This is
- isomorphic to the encoding via tuples \isa{{\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymtimes}\ {\isasymdots}\ {\isasymtimes}\ {\isasymtau}\isactrlsub n\ {\isasymrightarrow}\ {\isasymtau}}, but
- the curried version fits more smoothly into the basic
- calculus.\footnote{The difference is even more significant in
- higher-order logic, because additional the redundant tuple structure
- needs to be accommodated by formal reasoning.}
+ Functions are usually \emph{curried}: the idea of turning arguments
+ of type \isa{{\isasymtau}\isactrlsub i} (for \isa{i\ {\isasymin}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ n{\isacharbraceright}}) into a result of
+ type \isa{{\isasymtau}} is represented by the iterated function space
+ \isa{{\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymrightarrow}\ {\isasymdots}\ {\isasymrightarrow}\ {\isasymtau}\isactrlsub n\ {\isasymrightarrow}\ {\isasymtau}}. This is isomorphic to the well-known
+ encoding via tuples \isa{{\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymtimes}\ {\isasymdots}\ {\isasymtimes}\ {\isasymtau}\isactrlsub n\ {\isasymrightarrow}\ {\isasymtau}}, but the curried
+ version fits more smoothly into the basic calculus.\footnote{The
+ difference is even more significant in higher-order logic, because
+ the redundant tuple structure needs to be accommodated by formal
+ reasoning.}
Currying gives some flexiblity due to \emph{partial application}. A
function \isa{f{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymrightarrow}\ {\isasymtau}\isactrlbsub {\isadigit{2}}\isactrlesub \ {\isasymrightarrow}\ {\isasymtau}} can be applied to \isa{x{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}}
- and the remaining \isa{{\isacharparenleft}f\ x{\isacharparenright}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{2}}\ {\isasymrightarrow}\ {\isasymtau}} passed to other functions
+ and the remaining \isa{{\isacharparenleft}f\ x{\isacharparenright}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{2}}\ {\isasymrightarrow}\ {\isasymtau}} passed to another function
etc. How well this works in practice depends on the order of
arguments. In the worst case, arguments are arranged erratically,
and using a function in a certain situation always requires some
@@ -946,11 +943,10 @@
decorate the code with meaningless permutations of arguments.
This can be avoided by \emph{canonical argument order}, which
- observes certain standard patterns of function definitions and
- minimizes adhoc permutations in their application. In Isabelle/ML,
- large portions of non-trivial source code are written without ever
- using the infamous function \isa{swap{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymtimes}\ {\isasymalpha}} or the
- combinator \isa{C{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}\ {\isasymrightarrow}\ {\isacharparenleft}{\isasymbeta}\ {\isasymrightarrow}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}}, which is not even
+ observes certain standard patterns and minimizes adhoc permutations
+ in their application. In Isabelle/ML, large portions text can be
+ written without ever using \isa{swap{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymtimes}\ {\isasymalpha}}, or the
+ combinator \isa{C{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}\ {\isasymrightarrow}\ {\isacharparenleft}{\isasymbeta}\ {\isasymrightarrow}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}} that is not even
defined in our library.
\medskip The basic idea is that arguments that vary less are moved
@@ -977,15 +973,15 @@
concrete container. The argument order makes it easy to use other
combinators: \isa{forall\ {\isacharparenleft}member\ B{\isacharparenright}\ list} will check a list of
elements for membership in \isa{B} etc. Often the explicit
- \isa{list} is pointless and can be contracted in the application
- \isa{forall\ {\isacharparenleft}member\ B{\isacharparenright}} to get directly a predicate again.
+ \isa{list} is pointless and can be contracted to \isa{forall\ {\isacharparenleft}member\ B{\isacharparenright}} to get directly a predicate again.
- The update operation naturally ``varies'' the container, so it moves
+ In contrast, an update operation varies the container, so it moves
to the right: \isa{insert\ a} is a function \isa{{\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} to
insert a value \isa{a}. These can be composed naturally as
- follows: \isa{insert\ c\ {\isasymcirc}\ insert\ b\ {\isasymcirc}\ insert\ a}. This works well,
- apart from some awkwardness due to conventional mathematical
- function composition, which can be easily amended as follows.%
+ \isa{insert\ c\ {\isasymcirc}\ insert\ b\ {\isasymcirc}\ insert\ a}. The slightly awkward
+ inversion if the composition order is due to conventional
+ mathematical notation, which can be easily amended as explained
+ below.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -995,10 +991,10 @@
%
\begin{isamarkuptext}%
Regular function application and infix notation works best for
- relatively deeply structured expressions, e.g.\ \isa{h\ {\isacharparenleft}f\ x\ y\ {\isacharplus}\ g\ z{\isacharparenright}}. The important special case if \emph{linear transformation}
- applies a cascade of functions as follows: \isa{f\isactrlsub n\ {\isacharparenleft}{\isasymdots}\ {\isacharparenleft}f\isactrlsub {\isadigit{1}}\ x{\isacharparenright}{\isacharparenright}}.
- This becomes hard to read and maintain if the functions are
- themselves complex expressions. The notation can be significantly
+ relatively deeply structured expressions, e.g.\ \isa{h\ {\isacharparenleft}f\ x\ y\ {\isacharplus}\ g\ z{\isacharparenright}}. The important special case of \emph{linear transformation}
+ applies a cascade of functions \isa{f\isactrlsub n\ {\isacharparenleft}{\isasymdots}\ {\isacharparenleft}f\isactrlsub {\isadigit{1}}\ x{\isacharparenright}{\isacharparenright}}. This
+ becomes hard to read and maintain if the functions are themselves
+ given as complex expressions. The notation can be significantly
improved by introducing \emph{forward} versions of application and
composition as follows:
@@ -1056,7 +1052,7 @@
%
\begin{isamarkuptext}%
As explained above, a function \isa{f{\isacharcolon}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} can be
- understood as update on a configuration of type \isa{{\isasymbeta}} that is
+ understood as update on a configuration of type \isa{{\isasymbeta}},
parametrized by arguments of type \isa{{\isasymalpha}}. Given \isa{a{\isacharcolon}\ {\isasymalpha}}
the partial application \isa{{\isacharparenleft}f\ a{\isacharparenright}{\isacharcolon}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} operates
homogeneously on \isa{{\isasymbeta}}. This can be iterated naturally over a
@@ -1106,9 +1102,10 @@
\begin{warn}
The literature on functional programming provides a multitude of
combinators called \isa{foldl}, \isa{foldr} etc. SML97
- provides its own variations as \verb|List.foldl| and \verb|List.foldr|, while the classic Isabelle library still has the
- slightly more convenient historic \verb|Library.foldl| and \verb|Library.foldr|. To avoid further confusion, all of this should be
- ignored, and \verb|fold| (or \verb|fold_rev|) used exclusively.
+ provides its own variations as \verb|List.foldl| and \verb|List.foldr|, while the classic Isabelle library also has the
+ historic \verb|Library.foldl| and \verb|Library.foldr|. To avoid
+ further confusion, all of this should be ignored, and \verb|fold| (or
+ \verb|fold_rev|) used exclusively.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1173,8 +1170,9 @@
memory (``deforestation''), but requires some practice to read and
write it fluently.
- \medskip The next example elaborates this idea and demonstrates fast
- accumulation of tree content using a text buffer.%
+ \medskip The next example elaborates the idea of canonical
+ iteration, demonstrating fast accumulation of tree content using a
+ text buffer.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1212,30 +1210,27 @@
\begin{isamarkuptext}%
The slow part of \verb|slow_content| is the \verb|implode| of
the recursive results, because it copies previously produced strings
- afresh.
+ again.
The incremental \verb|add_content| avoids this by operating on a
- buffer that is passed-through in a linear fashion. Using \verb|#>| and contraction over the actual \verb|Buffer.T| argument
- saves some additional boiler-plate, but requires again some
- practice. Of course, the two \verb|Buffer.add| invocations with
- concatenated strings could have been split into smaller parts, but
- this would have obfuscated the source without making a big
- difference in allocations. Here we have done some
+ buffer that is passed through in a linear fashion. Using \verb|#>| and contraction over the actual buffer argument saves some
+ additional boiler-plate. Of course, the two \verb|Buffer.add|
+ invocations with concatenated strings could have been split into
+ smaller parts, but this would have obfuscated the source without
+ making a big difference in allocations. Here we have done some
peephole-optimization for the sake of readability.
Another benefit of \verb|add_content| is its ``open'' form as a
- function on \verb|Buffer.T| that can be continued in further
- linear transformations, folding etc. Thus it is more compositional
- than the naive \verb|slow_content|. As a realistic example, compare
- the slightly old-style \verb|Term.maxidx_of_term: term -> int| with
- the newer \verb|Term.maxidx_term: term -> int -> int| in
- Isabelle/Pure.
+ function on buffers that can be continued in further linear
+ transformations, folding etc. Thus it is more compositional than
+ the naive \verb|slow_content|. As realistic example, compare the
+ old-style \verb|Term.maxidx_of_term: term -> int| with the newer
+ \verb|Term.maxidx_term: term -> int -> int| in Isabelle/Pure.
- Note that \verb|fast_content| above is only defined for completeness
- of the example. In many practical situations, it is customary to
- defined the incremental \verb|add_content| only and leave the
- initialization and termination to the concrete application by the
- user.%
+ Note that \verb|fast_content| above is only defined as example. In
+ many practical situations, it is customary to provide the
+ incremental \verb|add_content| only and leave the initialization and
+ termination to the concrete application by the user.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1293,11 +1288,11 @@
\item \verb|warning|~\isa{text} outputs \isa{text} as
warning, which typically means some extra emphasis on the front-end
- side (color highlighting, icon).
+ side (color highlighting, icons, etc.).
\item \verb|error|~\isa{text} raises exception \verb|ERROR|~\isa{text} and thus lets the Isar toplevel print \isa{text} on the
error channel, which typically means some extra emphasis on the
- front-end side (color highlighting, icon).
+ front-end side (color highlighting, icons, etc.).
This assumes that the exception is not handled before the command
terminates. Handling exception \verb|ERROR|~\isa{text} is a
@@ -1308,7 +1303,7 @@
The actual error channel is accessed via \verb|Output.error_msg|, but
the interaction protocol of Proof~General \emph{crashes} if that
function is used in regular ML code: error output and toplevel
- command failure always need to coincide here.
+ command failure always need to coincide.
\end{warn}
\end{description}
@@ -1322,14 +1317,14 @@
some system console log, with a low chance that the user will ever
see it. Moreover, as a genuine side-effect on global process
channels, there is no proper way to retract output when Isar command
- transactions are reset.
+ transactions are reset by the system.
\end{warn}
\begin{warn}
The message channels should be used in a message-oriented manner.
- This means that multi-line output that logically belongs together
- needs to be issued by a \emph{single} invocation of \verb|writeln|
- etc. with the functional concatenation of all message constituents.
+ This means that multi-line output that logically belongs together is
+ issued by a \emph{single} invocation of \verb|writeln| etc.\ with the
+ functional concatenation of all message constituents.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1421,16 +1416,16 @@
These exceptions indicate a genuine breakdown of the program, so the
main purpose is to determine quickly what has happened where.
Traditionally, the (short) exception message would include the name
- of an ML function, although this no longer necessary, because the ML
- runtime system prints a detailed source position of the
+ of an ML function, although this is no longer necessary, because the
+ ML runtime system prints a detailed source position of the
corresponding \verb|raise| keyword.
\medskip User modules can always introduce their own custom
exceptions locally, e.g.\ to organize internal failures robustly
without overlapping with existing exceptions. Exceptions that are
exposed in module signatures require extra care, though, and should
- \emph{not} be introduced by default. Surprise by end-users or ML
- users of a module can be often minimized by using plain user errors.
+ \emph{not} be introduced by default. Surprise by users of a module
+ can be often minimized by using plain user errors instead.
\paragraph{Interrupts.} These indicate arbitrary system events:
both the ML runtime system and the Isabelle/ML infrastructure signal
@@ -1444,7 +1439,7 @@
that intercepts interrupts becomes dependent on physical effects of
the environment. Even worse, exception handling patterns that are
too general by accident, e.g.\ by mispelled exception constructors,
- will cover interrupts unintentionally, and thus render the program
+ will cover interrupts unintentionally and thus render the program
semantics ill-defined.
Note that the Interrupt exception dates back to the original SML90
@@ -1452,8 +1447,8 @@
avoid its malign impact on ML program semantics, but without
providing a viable alternative. Isabelle/ML recovers physical
interruptibility (which an indispensable tool to implement managed
- evaluation of Isar command transactions), but requires user code to
- be strictly transparent wrt.\ interrupts.
+ evaluation of command transactions), but requires user code to be
+ strictly transparent wrt.\ interrupts.
\begin{warn}
Isabelle/ML user code needs to terminate promptly on interruption,
@@ -1493,8 +1488,8 @@
\item \verb|can| is similar to \verb|try| with more abstract result.
\item \verb|ERROR|~\isa{msg} represents user errors; this
- exception is always raised via the \verb|error| function (see
- \secref{sec:message-channels}).
+ exception is normally raised indirectly via the \verb|error| function
+ (see \secref{sec:message-channels}).
\item \verb|Fail|~\isa{msg} represents general program failures.
@@ -1506,11 +1501,10 @@
while preserving its implicit position information (if possible,
depending on the ML platform).
- \item \verb|exception_trace|~\verb|(fn _ =>|~\isa{e}\verb|)| evaluates expression \isa{e} while printing
+ \item \verb|exception_trace|~\verb|(fn () =>|~\isa{e}\verb|)| evaluates expression \isa{e} while printing
a full trace of its stack of nested exceptions (if possible,
- depending on the ML platform).\footnote{In various versions of
- Poly/ML the trace will appear on raw stdout of the Isabelle
- process.}
+ depending on the ML platform).\footnote{In versions of Poly/ML the
+ trace will appear on raw stdout of the Isabelle process.}
Inserting \verb|exception_trace| into ML code temporarily is useful
for debugging, but not suitable for production code.
@@ -1539,10 +1533,10 @@
\begin{description}
- \item \isa{{\isacharat}{\isacharbraceleft}assert{\isacharbraceright}} inlines a function \isa{bool\ {\isasymRightarrow}\ unit}
- that raises \verb|Fail| if the argument is \verb|false|. Due to
- inlining the source position of failed assertions is included in the
- error output.
+ \item \isa{{\isacharat}{\isacharbraceleft}assert{\isacharbraceright}} inlines a function
+ \verb|bool -> unit| that raises \verb|Fail| if the argument is
+ \verb|false|. Due to inlining the source position of failed
+ assertions is included in the error output.
\end{description}%
\end{isamarkuptext}%
@@ -1560,12 +1554,11 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The basis library proposal of SML97 need to be treated with
+The basis library proposal of SML97 needs to be treated with
caution. Many of its operations simply do not fit with important
Isabelle/ML conventions (like ``canonical argument order'', see
- \secref{sec:canonical-argument-order}), others can cause serious
- problems with the parallel evaluation model of Isabelle/ML (such as
- \verb|TextIO.print| or \verb|OS.Process.system|).
+ \secref{sec:canonical-argument-order}), others cause problems with
+ the parallel evaluation model of Isabelle/ML (such as \verb|TextIO.print| or \verb|OS.Process.system|).
Subsequently we give a brief overview of important operations on
basic ML data types.%
@@ -1590,7 +1583,7 @@
\begin{description}
\item Type \verb|char| is \emph{not} used. The smallest textual
- unit in Isabelle is represented a ``symbol'' (see
+ unit in Isabelle is represented as a ``symbol'' (see
\secref{sec:symbols}).
\end{description}%
@@ -1628,10 +1621,10 @@
This works uniformly for all supported ML platforms (Poly/ML and
SML/NJ).
- Literal integers in ML text (e.g.\ \verb|123456789012345678901234567890|) are forced to be of this one true
+ Literal integers in ML text are forced to be of this one true
integer type --- overloading of SML97 is disabled.
- Structure \verb|IntInf| of SML97 is obsolete, always use
+ Structure \verb|IntInf| of SML97 is obsolete and superseded by
\verb|Int|. Structure \verb|Integer| in \hyperlink{file.~~/src/Pure/General/integer.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}General{\isacharslash}integer{\isachardot}ML}}}} provides some additional
operations.
@@ -1726,7 +1719,7 @@
Note that \verb|insert| is conservative about elements that are
already a \verb|member| of the list, while \verb|update| ensures that
- the last entry is always put in front. The latter discipline is
+ the latest entry is always put in front. The latter discipline is
often more appropriate in declarations of context data
(\secref{sec:context-data}) that are issued by the user in Isar
source: more recent declarations normally take precedence over
@@ -1750,10 +1743,12 @@
\isatagmlex
%
\begin{isamarkuptext}%
-Using canonical \verb|fold| together with canonical \verb|cons|, or similar standard operations, alternates the orientation of
- data. The is quite natural and should not altered forcible by
- inserting extra applications \verb|rev|. The alternative \verb|fold_rev| can be used in the relatively few situations, where
- alternation should be prevented.%
+Using canonical \verb|fold| together with \verb|cons|, or
+ similar standard operations, alternates the orientation of data.
+ The is quite natural and should not be altered forcible by inserting
+ extra applications of \verb|rev|. The alternative \verb|fold_rev| can
+ be used in the few situations, where alternation should be
+ prevented.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1852,7 +1847,8 @@
\item \verb|AList.lookup|, \verb|AList.defined|, \verb|AList.update|
implement the main ``framework operations'' for mappings in
- Isabelle/ML, with standard conventions for names and types.
+ Isabelle/ML, following standard conventions for their names and
+ types.
Note that a function called \isa{lookup} is obliged to express its
partiality via an explicit option element. There is no choice to
@@ -1954,7 +1950,7 @@
Isabelle/Isar exploits the inherent structure of theories and proofs
to support \emph{implicit parallelism} to a large extent. LCF-style
- theorem provides almost ideal conditions for that; see also
+ theorem provides almost ideal conditions for that, see also
\cite{Wenzel:2009}. This means, significant parts of theory and
proof checking is parallelized by default. A maximum speedup-factor
of 3.0 on 4 cores and 5.0 on 8 cores can be
@@ -1967,11 +1963,10 @@
\medskip ML threads lack the memory protection of separate
processes, and operate concurrently on shared heap memory. This has
- the advantage that results of independent computations are
- immediately available to other threads: abstract values can be
- passed between threads without copying or awkward serialization that
- is typically required for explicit message passing between separate
- processes.
+ the advantage that results of independent computations are directly
+ available to other threads: abstract values can be passed without
+ copying or awkward serialization that is typically required for
+ separate processes.
To make shared-memory multi-threading work robustly and efficiently,
some programming guidelines need to be observed. While the ML
@@ -2019,15 +2014,15 @@
channels, environment variables, current working directory.
\item Writable resources in the file-system that are shared among
- different threads or other processes.
+ different threads or external processes.
\end{itemize}
Isabelle/ML provides various mechanisms to avoid critical shared
- resources in most practical situations. As last resort there are
- some mechanisms for explicit synchronization. The following
- guidelines help to make Isabelle/ML programs work smoothly in a
- concurrent environment.
+ resources in most situations. As last resort there are some
+ mechanisms for explicit synchronization. The following guidelines
+ help to make Isabelle/ML programs work smoothly in a concurrent
+ environment.
\begin{itemize}
@@ -2037,7 +2032,7 @@
plain value and user tools can get/map their own data in a purely
functional manner. Configuration options within the context
(\secref{sec:config-options}) provide simple drop-in replacements
- for formerly writable flags.
+ for historic reference variables.
\item Keep components with local state information re-entrant.
Instead of poking initial values into (private) global references, a
@@ -2208,8 +2203,8 @@
Entering the critical section without contention is very fast, and
several basic system operations do so frequently. Each thread
- should leave the critical section quickly, otherwise parallel
- performance may degrade.
+ should stay within the critical section quickly only very briefly,
+ otherwise parallel performance may degrade.
\item \verb|CRITICAL| is the same as \verb|NAMED_CRITICAL| with empty
name argument.
@@ -2222,17 +2217,17 @@
\item \verb|Synchronized.guarded_access|~\isa{var\ f} lets the
function \isa{f} operate within a critical section on the state
- \isa{x} as follows: if \isa{f\ x} produces \verb|NONE|, we
- continue to wait on the internal condition variable, expecting that
+ \isa{x} as follows: if \isa{f\ x} produces \verb|NONE|, it
+ continues to wait on the internal condition variable, expecting that
some other thread will eventually change the content in a suitable
- manner; if \isa{f\ x} produces \verb|SOME|~\isa{{\isacharparenleft}y{\isacharcomma}\ x{\isacharprime}{\isacharparenright}} we
- are satisfied and assign the new state value \isa{x{\isacharprime}}, broadcast
- a signal to all waiting threads on the associated condition
- variable, and return the result \isa{y}.
+ manner; if \isa{f\ x} produces \verb|SOME|~\isa{{\isacharparenleft}y{\isacharcomma}\ x{\isacharprime}{\isacharparenright}} it is
+ satisfied and assigns the new state value \isa{x{\isacharprime}}, broadcasts a
+ signal to all waiting threads on the associated condition variable,
+ and returns the result \isa{y}.
\end{description}
- There are some further variants of the general \verb|Synchronized.guarded_access| combinator, see \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}synchronized{\isachardot}ML}}}} for details.%
+ There are some further variants of the \verb|Synchronized.guarded_access| combinator, see \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}synchronized{\isachardot}ML}}}} for details.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -2250,11 +2245,7 @@
\isatagmlex
%
\begin{isamarkuptext}%
-See \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}mailbox{\isachardot}ML}}}} how to
- implement a mailbox as synchronized variable over a purely
- functional queue.
-
- \medskip The following example implements a counter that produces
+The following example implements a counter that produces
positive integers that are unique over the runtime of the Isabelle
process:%
\end{isamarkuptext}%
@@ -2301,10 +2292,15 @@
\isadelimML
%
\endisadelimML
-\isanewline
+%
+\begin{isamarkuptext}%
+\medskip See \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}mailbox{\isachardot}ML}}}} how
+ to implement a mailbox as synchronized variable over a purely
+ functional queue.%
+\end{isamarkuptext}%
+\isamarkuptrue%
%
\isadelimtheory
-\isanewline
%
\endisadelimtheory
%
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon Oct 25 13:36:20 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon Oct 25 16:18:00 2010 +0200
@@ -874,7 +874,7 @@
%
\begin{isamarkuptext}%
Now the user can refer to \hyperlink{attribute.my-flag}{\mbox{\isa{my{\isacharunderscore}flag}}} in
- declarations, while we can retrieve the current value from the
+ declarations, while ML tools can retrieve the current value from the
context via \verb|Config.get|.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1323,7 +1323,7 @@
\endisadelimML
%
\begin{isamarkuptext}%
-\medskip The same works reletively to the formal context as
+\medskip The same works relatively to the formal context as
follows.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1726,7 +1726,7 @@
%
\begin{isamarkuptext}%
The following example yields the source position of some
- concrete binding inlined into the text.%
+ concrete binding inlined into the text:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1757,7 +1757,7 @@
%
\begin{isamarkuptext}%
\medskip That position can be also printed in a message as
- follows.%
+ follows:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1785,7 +1785,8 @@
\begin{isamarkuptext}%
This illustrates a key virtue of formalized bindings as
opposed to raw specifications of base names: the system can use this
- additional information for advanced feedback given to the user.%
+ additional information for feedback given to the user (error
+ messages etc.).%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Mon Oct 25 13:36:20 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Mon Oct 25 16:18:00 2010 +0200
@@ -299,12 +299,12 @@
\endisadelimML
%
\begin{isamarkuptext}%
-In the above example, the starting context had been derived
- from the toplevel theory, which means that fixed variables are
- internalized literally: \verb|x| is mapped again to
- \verb|x|, and attempting to fix it again in the subsequent
- context is an error. Alternatively, fixed parameters can be renamed
- explicitly as follows:%
+In the above example, the starting context is derived from the
+ toplevel theory, which means that fixed variables are internalized
+ literally: \verb|x| is mapped again to \verb|x|, and
+ attempting to fix it again in the subsequent context is an error.
+ Alternatively, fixed parameters can be renamed explicitly as
+ follows:%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/src/Pure/General/output.ML Mon Oct 25 13:36:20 2010 +0200
+++ b/src/Pure/General/output.ML Mon Oct 25 16:18:00 2010 +0200
@@ -36,7 +36,6 @@
val tracing_fn: (output -> unit) Unsynchronized.ref
val warning_fn: (output -> unit) Unsynchronized.ref
val error_fn: (output -> unit) Unsynchronized.ref
- val debug_fn: (output -> unit) Unsynchronized.ref
val prompt_fn: (output -> unit) Unsynchronized.ref
val status_fn: (output -> unit) Unsynchronized.ref
val report_fn: (output -> unit) Unsynchronized.ref
@@ -44,8 +43,6 @@
val prompt: string -> unit
val status: string -> unit
val report: string -> unit
- val debugging: bool Unsynchronized.ref
- val debug: (unit -> string) -> unit
end;
structure Output: OUTPUT =
@@ -93,7 +90,6 @@
val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
-val debug_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "::: ");
val prompt_fn = Unsynchronized.ref raw_stdout;
val status_fn = Unsynchronized.ref (fn _: string => ());
val report_fn = Unsynchronized.ref (fn _: string => ());
@@ -109,9 +105,6 @@
fun legacy_feature s = warning ("Legacy feature! " ^ s);
-val debugging = Unsynchronized.ref false;
-fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
-
(** timing **)
--- a/src/Pure/ML/ml_antiquote.ML Mon Oct 25 13:36:20 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Mon Oct 25 16:18:00 2010 +0200
@@ -57,6 +57,9 @@
(** misc antiquotations **)
+val _ = inline "assert"
+ (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")");
+
val _ = inline "make_string" (Scan.succeed ml_make_string);
val _ = value "binding"
--- a/src/Pure/thm.ML Mon Oct 25 13:36:20 2010 +0200
+++ b/src/Pure/thm.ML Mon Oct 25 16:18:00 2010 +0200
@@ -335,14 +335,14 @@
(*** Derivations and Theorems ***)
abstype thm = Thm of
- deriv * (*derivation*)
- {thy_ref: theory_ref, (*dynamic reference to theory*)
- tags: Properties.T, (*additional annotations/comments*)
- maxidx: int, (*maximum index of any Var or TVar*)
- shyps: sort Ord_List.T, (*sort hypotheses*)
- hyps: term Ord_List.T, (*hypotheses*)
- tpairs: (term * term) list, (*flex-flex pairs*)
- prop: term} (*conclusion*)
+ deriv * (*derivation*)
+ {thy_ref: theory_ref, (*dynamic reference to theory*)
+ tags: Properties.T, (*additional annotations/comments*)
+ maxidx: int, (*maximum index of any Var or TVar*)
+ shyps: sort Ord_List.T, (*sort hypotheses*)
+ hyps: term Ord_List.T, (*hypotheses*)
+ tpairs: (term * term) list, (*flex-flex pairs*)
+ prop: term} (*conclusion*)
and deriv = Deriv of
{promises: (serial * thm future) Ord_List.T,
body: Proofterm.proof_body}
--- a/src/Pure/variable.ML Mon Oct 25 13:36:20 2010 +0200
+++ b/src/Pure/variable.ML Mon Oct 25 16:18:00 2010 +0200
@@ -77,7 +77,7 @@
binds: (typ * term) Vartab.table, (*term bindings*)
type_occs: string list Symtab.table, (*type variables -- possibly within term variables*)
maxidx: int, (*maximum var index*)
- sorts: sort Ord_List.T, (*declared sort occurrences*)
+ sorts: sort Ord_List.T, (*declared sort occurrences*)
constraints:
typ Vartab.table * (*type constraints*)
sort Vartab.table}; (*default sorts*)