forked from Isabelle_DOF/Isabelle_DOF
2342 lines
121 KiB
Plaintext
2342 lines
121 KiB
Plaintext
(*************************************************************************
|
||
* Copyright (C)
|
||
* 2019-2021 The University of Exeter
|
||
* 2018-2021 The University of Paris-Saclay
|
||
* 2018 The University of Sheffield
|
||
*
|
||
* License:
|
||
* This program can be redistributed and/or modified under the terms
|
||
* of the 2-clause BSD-style license.
|
||
*
|
||
* SPDX-License-Identifier: BSD-2-Clause
|
||
*************************************************************************)
|
||
|
||
(*<*)
|
||
theory TR_MyCommentedIsabelle
|
||
imports "Isabelle_DOF.technical_report"
|
||
|
||
begin
|
||
|
||
define_shortcut* isabelle \<rightleftharpoons> \<open>Isabelle/HOL\<close>
|
||
|
||
open_monitor*[this::report]
|
||
(*>*)
|
||
|
||
title*[tit::title]\<open>My Personal, Eclectic Isabelle Programming Manual\<close>
|
||
subtitle*[stit::subtitle]\<open>Version : Isabelle 2020\<close>
|
||
text*[bu::author,
|
||
email = "''wolff@lri.fr''",
|
||
affiliation = "\<open>Université Paris-Saclay, LRI, France\<close>"]\<open>Burkhart Wolff\<close>
|
||
|
||
|
||
text*[abs::abstract,
|
||
keywordlist="[''LCF-Architecture'',''Isabelle'',''SML'',''PIDE'',''Programming Guide'',
|
||
''Tactic Programming'']"]\<open>
|
||
While Isabelle is mostly known as "logical framework" underlying \<^isabelle> and thus commonly
|
||
understood as an interactive theorem prover, it actually provides a system framework for
|
||
developing a wide spectrum of applications. A particular strength of the Isabelle framework is
|
||
the combination of document editing, formal verification, and code generation.
|
||
|
||
This is a programming-tutorial of \<^isabelle>, conceived as a complementary
|
||
text to the unfortunately somewhat outdated "The Isabelle Cookbook" in
|
||
\<^url>\<open>https://nms.kcl.ac.uk/christian.urban/Cookbook/\<close>. The reader is encouraged
|
||
not only to consider the generated .pdf, but also consult the loadable version in Isabelle/jEdit
|
||
@{cite "DBLP:journals/corr/Wenzel14"} in order to make experiments on the running code.
|
||
|
||
This text is written itself in Isabelle/Isar using a specific document ontology
|
||
for technical reports. It is intended to be a "living document", i.e. it is not only
|
||
used for generating a static, conventional .pdf, but also for direct interactive
|
||
exploration in Isabelle/jEdit. This way, types, intermediate results of computations and
|
||
checks can be repeated by the reader who is invited to interact with this document.
|
||
Moreover, the textual parts have been enriched with a maximum of formal content
|
||
which makes this text re-checkable at each load and easier maintainable.
|
||
\<close>
|
||
|
||
chapter*[intro::introduction]\<open> Introduction \<close>
|
||
|
||
text\<open> \<^vs>\<open>-0.5cm\<close>
|
||
While Isabelle @{cite "DBLP:books/sp/NipkowPW02"} is mostly known as part of Isabelle/HOL
|
||
(an interactive theorem prover), it actually provides a system framework for developing a wide
|
||
spectrum of applications. A particular strength of the Isabelle framework is the combination
|
||
of text editing, formal verification, and code generation. This is a programming-tutorial of
|
||
Isabelle and Isabelle/HOL, a complementary text to the unfortunately somewhat outdated
|
||
"The Isabelle Cookbook" in \<^url>\<open>https://nms.kcl.ac.uk/christian.urban/Cookbook/\<close>.
|
||
The present text is also complementary to the current version of
|
||
\<^url>\<open>https://isabelle.in.tum.de/dist/Isabelle2021/doc/isar-ref.pdf\<close>
|
||
"The Isabelle/Isar Implementation" by Makarius Wenzel in that it focusses on subjects
|
||
not covered there, or presents alternative explanations for which I believe, based on my
|
||
experiences with students and Phds, that they are helpful.
|
||
For the present programming manual, the reader is encouraged not only to consider the generated
|
||
.pdf, but also consult the loadable version
|
||
in Isabelle/jedit in order to make experiments on the running code. This text is written
|
||
itself in Isabelle/Isar using a specific document ontology for technical reports. It is
|
||
intended to be a "living document", i.e. it is not only used for generating a static,
|
||
conventional .pdf, but also for direct interactive exploration in Isabelle/jEdit. This way,
|
||
types, intermediate results of computations and checks can be repeated by the reader who is
|
||
invited to interact with this document. Moreover, the textual parts have been enriched with a
|
||
maximum of formal content which makes this text re-checkable at each load and easier
|
||
maintainable. \<close>
|
||
|
||
figure*[architecture::figure,relative_width="70",src="''figures/isabelle-architecture''"]\<open>
|
||
The system architecture of Isabelle (left-hand side) and the asynchronous communication
|
||
between the Isabelle system and the IDE (right-hand side). \<close>
|
||
|
||
text\<open>This programming tutorial roughly follows the Isabelle system architecture shown in
|
||
\<^figure>\<open>architecture\<close>, and, to be more precise, more or less in the bottom-up order.
|
||
|
||
We start from the basic underlying SML platform over the Kernels to the tactical layer
|
||
and end with a discussion over the front-end technologies. \<^vs>\<open>-1.0cm\<close>
|
||
\<close>
|
||
|
||
chapter*[t1::technical]\<open> SML and Fundamental SML libraries \<close>
|
||
|
||
section*[t11::technical] "ML, Text and Antiquotations"
|
||
|
||
text\<open>Isabelle is written in SML, the "Standard Meta-Language", which is an impure functional
|
||
programming language allowing, in principle, mutable variables and side effects.
|
||
The following Isabelle/Isar commands allow for accessing the underlying SML interpreter
|
||
of Isabelle directly. In the example, a mutable variable X is declared, initialized to 0 and
|
||
updated; and finally re-evaluated leading to output: \<close>
|
||
|
||
ML\<open>
|
||
val X = Unsynchronized.ref 0;
|
||
X:= !X + 1;
|
||
X
|
||
\<close>
|
||
|
||
text\<open>However, since Isabelle is a platform involving parallel execution, concurrent computing, and,
|
||
as an interactive environment, involves backtracking / re-evaluation as a consequence of user-
|
||
interaction, imperative programming is discouraged and nearly never used in the entire Isabelle
|
||
code-base @{cite "DBLP:conf/mkm/BarrasGHRTWW13"}.
|
||
The preferred programming style is purely functional: \<close>
|
||
|
||
ML\<open>
|
||
fun fac x = if x = 0 then 1 else x * fac(x-1) ;
|
||
fac 10;
|
||
\<close>
|
||
text\<open>or:\<close>
|
||
ML\<open>
|
||
type state = { a : int, b : string}
|
||
fun incr_state ({a, b}:state) = {a=a+1, b=b}
|
||
\<close>
|
||
|
||
text\<open> The faculty function is defined and executed; the (sub)-interpreter in Isar
|
||
works in the conventional read-execute-print loop for each statement separated by a ";".
|
||
Functions, types, data-types etc. can be grouped to modules (called \<^emph>\<open>structures\<close>) which can
|
||
be constrained to interfaces (called \<^emph>\<open>signatures\<close>) and even be parametric structures
|
||
(called \<^emph>\<open>functors\<close>). \<close>
|
||
|
||
text\<open> The Isabelle/Isar interpreter (called \<^emph>\<open>toplevel\<close> ) is extensible; by a mixture of SML
|
||
and Isar-commands, domain-specific components can be developed and integrated into the system
|
||
on the fly. Actually, the Isabelle system code-base consists mainly of SML and \<^verbatim>\<open>.thy\<close>-files
|
||
containing such mixtures of Isar commands and SML. \<close>
|
||
|
||
text\<open> Besides the ML-command used in the above examples, there are a number of commands
|
||
representing text-elements in Isabelle/Isar; text commands can be interleaved arbitrarily
|
||
with other commands. Text in text-commands may use LaTeX and is used for type-setting
|
||
documentations in a kind of literate programming style. \<close>
|
||
|
||
text\<open>So: the text command for:\<close>
|
||
|
||
text\<open>\<^emph>\<open>This is a text.\<close>\<close>
|
||
|
||
text\<open>... is represented in the integrated source (the \<^verbatim>\<open>.thy\<close> file) by:\<close>
|
||
|
||
text\<open> \<open>*\<open>This is a text.\<close>\<close>\<close>
|
||
|
||
text\<open>and displayed in the Isabelle/jEdit front-end at the sceen by:\<close>
|
||
|
||
figure*[fig2::figure, relative_width="60", placement="pl_h", src="''figures/text-element''"]
|
||
\<open>A text-element as presented in Isabelle/jEdit.\<close>
|
||
|
||
text\<open>The text-commands, ML-commands (and in principle any other command) can be seen as
|
||
\<^emph>\<open>quotations\<close> over the underlying SML environment (similar to OCaml or Haskell).
|
||
Linking these different sorts of quotations with each other and the underlying SML-environment
|
||
is supported via \<^emph>\<open>antiquotations\<close>'s. Generally speaking, antiquotations are a kind of semantic
|
||
macro whose arguments were checked, interpreted and expanded using the underlying system
|
||
state. This paves the way for a programming technique to specify expressions or patterns in an
|
||
anti-quotation in various contexts, be it in an ML fragment or a documentation fragment.
|
||
Anti-quotations as "semantic macros" can produce a value for the surrounding context
|
||
(ML, text, HOL, whatever) depending on local arguments and the underlying logical context.
|
||
|
||
The way an antiquotation is specified depends on the quotation expander: typically, this is a
|
||
specific character and an identifier, or specific parentheses and a complete expression or
|
||
pattern.\<close>
|
||
|
||
text\<open> In Isabelle documentations, antiquotation's were heavily used to enrich literate explanations
|
||
and documentations by "formal content", i.e. machine-checked, typed references
|
||
to all sorts of entities in the context of the interpreting environment.
|
||
Formal content allows for coping with sources that rapidly evolve and were developed by
|
||
distributed teams as is typical in open-source developments.
|
||
|
||
A paradigmatic example for antiquotation in documentation text snippets and program snippets is here:
|
||
\<^item> \<^theory_text>\<open>text\<open>@{footnote \<open>sdf\<close>}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\<close>\<close>
|
||
\<^item> @{theory_text [display]
|
||
\<open> val x = @{thm refl};
|
||
val _ = @{term "A \<longrightarrow> B"}
|
||
val y = @{typ "'a list"}
|
||
\<close>
|
||
}
|
||
\<close>
|
||
|
||
(*<*) (* example to execute: *)
|
||
text\<open> @{footnote \<open>sdf\<close>}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\<close>
|
||
ML\<open>
|
||
val x = @{thm refl};
|
||
val _ = @{term "A \<longrightarrow> B"}
|
||
val y = @{typ "'a list"}
|
||
\<close>
|
||
(*>*)
|
||
|
||
text\<open>\<^vs>\<open>-1.0cm\<close>... which we will describe in more detail later. \<close>
|
||
|
||
text\<open>In a way, anti-quotations implement a kind of
|
||
literate specification style in text, models, code, proofs, etc., which become alltogether
|
||
elements of one global \<^emph>\<open>integrated document\<close> in which mutual dependencies can be machine-checked
|
||
(i.e. \<open>formal\<close> in this sense).
|
||
Attempting to maximize the \<open>formal content\<close> is a way to ensure "Agile Development" (AD) of an
|
||
integrated document development, in the sense that it allows to give immediate feedback
|
||
with respect to changes which enable thus the popular AD-objective \<^emph>\<open>embrace change\<close>.
|
||
Note that while we adhere to this objective, we do not depend or encourage popular AD methods
|
||
and processes such as SCRUM. \<close>
|
||
|
||
paragraph\<open>
|
||
A maximum of formal content inside text documentation also ensures the
|
||
consistency of this present text with the underlying Isabelle version.\<close>
|
||
|
||
section\<open>The Isabelle/Pure bootstrap\<close>
|
||
|
||
text\<open>It is instructive to study the fundamental bootstrapping sequence of the Isabelle system;
|
||
it is written in the Isar format and gives an idea of the global module dependencies:
|
||
\<^file>\<open>~~/src/Pure/ROOT.ML\<close>. Loading this file
|
||
(for example by hovering over this hyperlink in the antiquotation holding control or
|
||
command key in Isabelle/jEdit and activating it) allows the Isabelle IDE
|
||
to support hyperlinking \<^emph>\<open>inside\<close> the Isabelle source.\<close>
|
||
|
||
text\<open>The bootstrapping sequence is also reflected in the following diagram @{figure "architecture"}.\<close>
|
||
|
||
|
||
section*[t12::technical] "Elements of the SML library"
|
||
text\<open>Elements of the \<^file>\<open>~~/src/Pure/General/basics.ML\<close> SML library
|
||
are basic exceptions. Note that exceptions should be catched individually, uncatched exceptions
|
||
except those generated by the specific "error" function are discouraged in Isabelle
|
||
source programming since they might produce races in the internal Isabelle evaluation.
|
||
% TODO:
|
||
% The following exceptions are defined in $ML_SOURCES/basis/General.sml
|
||
% and in $ISABELLE_HOME/src/Pure/general/scan.ml
|
||
% ans not in \<^file>\<open>~~/src/Pure/General/basics.ML\<close>
|
||
|
||
\<^item> \<^ML>\<open>Bind : exn\<close> \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> \<^ML>\<open>Chr : exn\<close> \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> \<^ML>\<open>Div : exn\<close> \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> \<^ML>\<open>Domain : exn\<close> \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> \<^ML>\<open>Fail : string -> exn\<close>, \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> \<^ML>\<open>Match : exn\<close>, relevant for pattern matching \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> \<^ML>\<open>Overflow : exn\<close> \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> \<^ML>\<open>Size : exn\<close> \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> \<^ML>\<open>Span : exn\<close> \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> \<^ML>\<open>Subscript : exn\<close> \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> \<^ML>\<open>exnName : exn -> string\<close>, very interesting to query an unknown \<open>exception\<close> \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> \<^ML>\<open>exnMessage: exn -> string\<close> \<^vs>\<open>-0.3 cm\<close>
|
||
\<close> (* typesetting as table ? *)
|
||
|
||
text*[squiggols::technical]
|
||
\<open>\<^noindent> Finally, a number of commonly used "squigglish" combinators is listed:
|
||
|
||
\<^item> @{ML "op ! : 'a Unsynchronized.ref->'a"}, access operation on a program variable \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> @{ML "op := : ('a Unsynchronized.ref * 'a)->unit"}, update operation on program variable\<^vs>\<open>-0.3cm\<close>
|
||
\<^item> @{ML "op #> : ('a->'b) * ('b->'c)->'a->'c"}, a reversed function composition \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> @{ML "I: 'a -> 'a"}, the I combinator \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> @{ML "K: 'a -> 'b -> 'a"}, the K combinator \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> @{ML "op o : (('b->'c) * ('a->'b))->'a->'c"}, function composition \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> @{ML "op || : ('a->'b) * ('a->'b) -> 'a -> 'b"}, parse alternative \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> @{ML "op -- : ('a->'b*'c) * ('c->'d*'e)->'a->('b*'d)*'e"}, parse pair \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> @{ML "op |-- : ('a->'b*'c) * ('c->'d*'e)->'a->'d*'e"}, parse pair, forget right \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> @{ML "op --| : ('a->'b*'c) * ('c->'d*'e)->'a->'b*'e"}, parse pair, forget left \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> @{ML "op ? : bool * ('a->'a)->'a->'a"}, if then else \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> @{ML "ignore : 'a->unit"}, force execution, but ignore result \<^vs>\<open>-0.3cm\<close>
|
||
\<^item> @{ML "op before: ('a*unit) -> 'a"} \<^vs>\<open>-0.8cm\<close>
|
||
% TODO:
|
||
% Again the definitions of these operators span multiple files
|
||
% and not just \<^file>\<open>~~/src/Pure/General/basics.ML\<close>.
|
||
\<close>
|
||
|
||
text\<open>\<^noindent> Some basic examples for the programming style using these combinators can be found in the
|
||
"The Isabelle Cookbook" section 2.3.\<close>
|
||
|
||
text\<open>An omnipresent data-structure in the Isabelle SML sources are tables
|
||
implemented in @{file "$ISABELLE_HOME/src/Pure/General/table.ML"}. These
|
||
generic tables are presented in an efficient purely functional implementation using
|
||
balanced 2-3 trees. Key operations are:\<close>
|
||
ML\<open>
|
||
signature TABLE_reduced =
|
||
sig
|
||
type key
|
||
type 'a table
|
||
exception DUP of key
|
||
exception SAME
|
||
exception UNDEF of key
|
||
val empty: 'a table
|
||
val dest: 'a table -> (key * 'a) list
|
||
val keys: 'a table -> key list
|
||
val lookup_key: 'a table -> key -> (key * 'a) option
|
||
val lookup: 'a table -> key -> 'a option
|
||
val defined: 'a table -> key -> bool
|
||
val update: key * 'a -> 'a table -> 'a table
|
||
(* ... *)
|
||
end
|
||
\<close>
|
||
text\<open>... where \<^verbatim>\<open>key\<close> is usually just a synonym for string.\<close>
|
||
|
||
chapter*[t2::technical] \<open> Prover Architecture \<close>
|
||
|
||
section*[t21::technical] \<open> The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts \<close>
|
||
|
||
text\<open> What I call the 'Nano-Kernel' in Isabelle can also be seen as an acyclic theory graph.
|
||
The meat of it can be found in the file @{file "$ISABELLE_HOME/src/Pure/context.ML"}.
|
||
My notion is a bit criticisable since this component, which provides the type of @{ML_type theory}
|
||
and @{ML_type Proof.context}, is not that Nano after all.
|
||
However, these type are pretty empty place-holders at that level and the content of
|
||
@{file "$ISABELLE_HOME/src/Pure/theory.ML"} is registered much later.
|
||
The sources themselves mention it as "Fundamental Structure".
|
||
In principle, theories and proof contexts could be REGISTERED as user data inside contexts.
|
||
The chosen specialization is therefore an acceptable meddling of the abstraction "Nano-Kernel"
|
||
and its application context: Isabelle.
|
||
|
||
Makarius himself says about this structure:
|
||
|
||
"Generic theory contexts with unique identity, arbitrarily typed data,
|
||
monotonic development graph and history support. Generic proof
|
||
contexts with arbitrarily typed data."
|
||
% NOTE:
|
||
% Add the reference.
|
||
|
||
In my words: a context is essentially a container with
|
||
\<^item> an id
|
||
\<^item> a list of parents (so: the graph structure)
|
||
\<^item> a time stamp and
|
||
\<^item> a sub-context relation (which uses a combination of the id and the time-stamp to
|
||
establish this relation very fast whenever needed; it plays a crucial role for the
|
||
context transfer in the kernel.
|
||
|
||
|
||
A context comes in form of three 'flavours':
|
||
\<^item> theories : \<^ML_type>\<open>theory\<close>'s, containing a syntax and axioms, but also
|
||
user-defined data and configuration information.
|
||
\<^item> Proof-Contexts: \<^ML_type>\<open>Proof.context\<close>
|
||
containing theories but also additional information if Isar goes into prove-mode.
|
||
In general a richer structure than theories coping also with fixes, facts, goals,
|
||
in order to support the structured Isar proof-style.
|
||
\<^item> Generic: \<^ML_type>\<open>Context.generic\<close>, i.e. the sum of both.
|
||
|
||
All context have to be seen as mutable; so there are usually transformations defined on them
|
||
which are possible as long as a particular protocol (\<^verbatim>\<open>begin_thy\<close> - \<^verbatim>\<open>end_thy\<close> etc) are respected.
|
||
|
||
Contexts come with type user-defined data which is mutable through the entire lifetime of
|
||
a context.
|
||
\<close>
|
||
|
||
subsection*[t212::technical]\<open> Mechanism 1 : Core Interface. \<close>
|
||
text\<open>To be found in @{file "$ISABELLE_HOME/src/Pure/context.ML"}:\<close>
|
||
|
||
text\<open>
|
||
\<^item> \<^ML>\<open>Context.parents_of: theory -> theory list\<close> gets the (direct) parent theories
|
||
\<^item> \<^ML>\<open>Context.ancestors_of: theory -> theory list\<close> gets the imported theories
|
||
\<^item> \<^ML>\<open>Context.proper_subthy : theory * theory -> bool\<close> subcontext test
|
||
\<^item> \<^ML>\<open>Context.Proof: Proof.context -> Context.generic \<close> A constructor embedding local contexts
|
||
\<^item> \<^ML>\<open>Context.proof_of : Context.generic -> Proof.context\<close> the inverse
|
||
\<^item> \<^ML>\<open>Context.theory_name : theory -> string\<close>
|
||
\<^item> \<^ML>\<open>Context.map_theory: (theory -> theory) -> Context.generic -> Context.generic\<close>
|
||
\<close>
|
||
|
||
text\<open>The structure \<^ML_structure>\<open>Proof_Context\<close> provides a key data-structures concerning contexts:
|
||
|
||
\<^item> \<^ML>\<open> Proof_Context.init_global: theory -> Proof.context\<close>
|
||
embeds a global context into a local context
|
||
\<^item> \<^ML>\<open> Context.Proof: Proof.context -> Context.generic \<close>
|
||
the path to a generic Context, i.e. a sum-type of global and local contexts
|
||
in order to simplify system interfaces
|
||
\<^item> \<^ML>\<open> Proof_Context.get_global: theory -> string -> Proof.context\<close>
|
||
\<close>
|
||
|
||
|
||
subsection*[t213::example]\<open>Mechanism 2 : Extending the Global Context \<open>\<theta>\<close> by User Data \<close>
|
||
|
||
text\<open>A central mechanism for constructing user-defined data is by the \<^ML_functor>\<open>Generic_Data\<close>-functor.
|
||
A plugin needing some data \<^verbatim>\<open>T\<close> and providing it with implementations for an
|
||
\<^verbatim>\<open>empty\<close>, and operations \<^verbatim>\<open>merge\<close> and \<^verbatim>\<open>extend\<close>, can construct a lense with operations
|
||
\<^verbatim>\<open>get\<close> and \<^verbatim>\<open>put\<close> that attach this data into the generic system context. Rather than using
|
||
unsynchronized SML mutable variables, this is the mechanism to introduce component local
|
||
data in Isabelle, which allows to manage this data for the necessary backtrack and synchronization
|
||
features in the pervasively parallel evaluation framework that Isabelle as a system represents.\<close>
|
||
|
||
ML \<open>
|
||
datatype X = mt
|
||
val init = mt;
|
||
val ext = I
|
||
fun merge (X,Y) = mt
|
||
|
||
structure Data = Generic_Data
|
||
(
|
||
type T = X
|
||
val empty = init
|
||
val extend = ext
|
||
val merge = merge
|
||
);
|
||
\<close>
|
||
text\<open> This generates the result structure \<^ML_structure>\<open>Data\<close> by a functor instantiation
|
||
with the functions:
|
||
|
||
\<^item> \<^ML>\<open> Data.get : Context.generic -> Data.T\<close>
|
||
\<^item> \<^ML>\<open> Data.put : Data.T -> Context.generic -> Context.generic\<close>
|
||
\<^item> \<^ML>\<open> Data.map : (Data.T -> Data.T) -> Context.generic -> Context.generic\<close>
|
||
\<^item> ... and other variants to do this on theories ...
|
||
\<close>
|
||
|
||
|
||
section*[lcfk::technical]\<open>The LCF-Kernel: \<^ML_type>\<open>term\<close>s, \<^ML_type>\<open>typ\<close>es, \<^ML_type>\<open>theory\<close>s,
|
||
\<^ML_type>\<open> Proof.context\<close>s, \<^ML_type>\<open>thm\<close>s \<close>
|
||
text\<open>The classical LCF-style \<^emph>\<open>kernel\<close> is about
|
||
\<^enum> Types and terms of a typed \<open>\<lambda>\<close>-Calculus including constant symbols,
|
||
free variables, \<open>\<lambda>\<close>-binder and application,
|
||
\<^enum> An infrastructure to define types and terms, a \<^emph>\<open>signature\<close> in structure \<^ML_structure>\<open>Sign\<close>
|
||
that also assigns to constant symbols types and concrete syntax managed in structure
|
||
\<^ML_structure>\<open>Syntax\<close>
|
||
\<^enum> An abstract type \<^ML_type>\<open>thm\<close> for \<^emph>\<open>theorem\<close> and logical operations on them
|
||
\<^enum> (Isabelle specific): a notion of \<^ML_type>\<open>theory\<close>, i.e. a container
|
||
providing a signature and set (list) of theorems.
|
||
\<close>
|
||
|
||
|
||
subsection*[termstypes::technical]\<open> Terms and Types \<close>
|
||
text \<open>The basic data-structure \<^ML_structure>\<open>Term\<close> of the kernel is contained in file
|
||
@{file "$ISABELLE_HOME/src/Pure/term.ML"}. At a glance, the highlights are summarized as follows: \<close>
|
||
(* Methodologically doubtful: nothing guarantees that TERM' corresponds to what is Isabelle reality*)
|
||
ML\<open>
|
||
signature TERM' = sig
|
||
(* ... *)
|
||
type indexname = string * int
|
||
type class = string
|
||
type sort = class list
|
||
type arity = string * sort list * sort
|
||
datatype typ =
|
||
Type of string * typ list |
|
||
TFree of string * sort |
|
||
TVar of indexname * sort
|
||
datatype term =
|
||
Const of string * typ |
|
||
Free of string * typ |
|
||
Var of indexname * typ |
|
||
Bound of int |
|
||
Abs of string * typ * term |
|
||
$ of term * term (* the infix operator for the application *)
|
||
exception TYPE of string * typ list * term list
|
||
exception TERM of string * term list
|
||
(* ... *)
|
||
end
|
||
\<close>
|
||
|
||
(* methodologically better: *)
|
||
text\<open>\<^noindent> Basic types introduced by structure \<^ML_structure>\<open>Term\<close> are:
|
||
|
||
\<^item> \<^ML_type>\<open>Term.indexname\<close> which is a synonym to \<^ML_type>\<open>string * int\<close>
|
||
\<^item> \<^ML_type>\<open>Term.class\<close> which is a synonym to \<^ML_type>\<open>string\<close>
|
||
\<^item> \<^ML_type>\<open>Term.sort\<close> which is a synonym to \<^ML_type>\<open>class list\<close>
|
||
\<^item> \<^ML_type>\<open>Term.arity\<close> which is a synonym to \<^ML_type>\<open> string * sort list * sort\<close>
|
||
|
||
\<^item> \<^ML_type>\<open>Term.typ\<close> has the following constructors:
|
||
\<^enum> \<^ML>\<open>Term.Type: string * typ list -> typ\<close> : The universal type constructor. Note that
|
||
\<open>Type("fun", [A,B])\<close> denotes the function space \<open>A \<Rightarrow> B\<close> at the ML level.
|
||
\<^enum> \<^ML>\<open>Term.TFree: string * sort -> typ\<close> introduces free-type variables, pretty-printed
|
||
by \<open>'a,'b,'c,...\<close>. In deduction, they are treated as constants.
|
||
\<^enum> \<^ML>\<open>Term.TVar: indexname * sort -> typ\<close> introduces schematic type variables, pretty-printed
|
||
by \<open>?'a,?'b,?'c,...\<close>. In deduction, they were instantiated by the unification process.
|
||
|
||
\<^item> \<^ML_type>\<open>Term.term\<close> implements the heart of a Curry-style typed \<open>\<lambda>\<close>-calculus.
|
||
It has the following constructors:
|
||
\<^enum> \<^ML>\<open>Term.Const: string * typ -> term\<close> for \<^emph>\<open>constant symbols\<close>,
|
||
\<^enum> \<^ML>\<open>Term.Free: string * typ -> term\<close> for \<^emph>\<open>free variable symbols\<close>,
|
||
\<^enum> \<^ML>\<open>Term.Var: indexname * typ -> term\<close> for \<^emph>\<open>schematic variables\<close>, \<^eg>, \<open>?X\<close>, \<open>?Y\<close>, \<open>?Z\<close>, ...
|
||
\<^enum> \<^ML>\<open>Term.Bound: int -> term\<close> for bound variables encoded as deBruin indices,
|
||
\<^enum> \<^ML>\<open>Term.Abs: string * typ * term -> term\<close> for the \<^emph>\<open>abstraction\<close>
|
||
\<^enum> \<^ML>\<open>op $ : term * term -> term\<close> denotes the infix operator for the \<^emph>\<open>application\<close>
|
||
|
||
\<^item> \<^ML_structure>\<open>Term\<close> provides also a number of core-exceptions relevant for type inference and
|
||
term destruction: \<^ML>\<open>Term.TYPE: string * typ list * term list -> exn\<close> and
|
||
\<^ML>\<open>Term.TERM: string * term list -> exn\<close>.
|
||
\<close>
|
||
|
||
text\<open>This core-data structure of the Isabelle Kernel is accessible in the Isabelle/ML environment
|
||
and serves as basis for programmed extensions concerning syntax, type-checking, and advanced
|
||
tactic programming over kernel primitives and higher API's. There are a number of anti-quotations
|
||
giving support for this task; since @{ML Const}-names are long-names revealing information
|
||
of the potentially evolving library structure, the use of anti-quotations leads to a safer programming
|
||
style of tactics and became therefore standard in the entire Isabelle code-base.
|
||
\<close>
|
||
|
||
text\<open>The following examples show how term- and type-level antiquotations are used and that
|
||
they can both be used for term-construction as well as term-destruction (pattern-matching):\<close>
|
||
|
||
ML\<open> val Const ("HOL.implies", @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"})
|
||
$ Free ("A", @{typ "bool"})
|
||
$ Free ("B", @{typ "bool"})
|
||
= @{term "A \<longrightarrow> B"};
|
||
|
||
val "HOL.bool" = @{type_name "bool"};
|
||
|
||
(* three ways to write type bool: *)
|
||
val Type("fun",[s,Type("fun",[@{typ "bool"},Type(@{type_name "bool"},[])])]) = @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"};
|
||
|
||
\<close>
|
||
text\<open>
|
||
% NOTE:
|
||
% The quotes disappear in the pdf document output.
|
||
|
||
\<close>
|
||
text\<open>Note that the SML interpreter is configured that he will actually print a type
|
||
\<^verbatim>\<open>Type("HOL.bool",[])\<close> just as \<^verbatim>\<open>"bool": typ\<close>, so a compact notation looking
|
||
pretty much like a string. This can be confusing at times.\<close>
|
||
|
||
text\<open>Note, furthermore, that there is a programming API for the HOL-instance of Isabelle:
|
||
it is contained in @{file "$ISABELLE_HOME/src/HOL/Tools/hologic.ML"}. It offers many
|
||
operators of the HOL logic specific constructors and destructors:\<close>
|
||
|
||
text*[T2::technical]\<open>
|
||
\<^enum> \<^ML>\<open>HOLogic.boolT : typ\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.mk_Trueprop : term -> term\<close>, the embedder of bool to prop fundamental for HOL \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.dest_Trueprop : term -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.Trueprop_conv : conv -> conv\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.mk_setT : typ -> typ\<close>, the ML level type constructor set \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.dest_setT : typ -> typ\<close>, the ML level type destructor for set \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.Collect_const : typ -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.mk_Collect : string * typ * term -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.mk_mem : term * term -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.dest_mem : term -> term * term\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.mk_set : typ -> term list -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.conj_intr : Proof.context -> thm -> thm -> thm\<close>, some HOL-level derived-inferences \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.conj_elim : Proof.context -> thm -> thm * thm\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.conj_elims : Proof.context -> thm -> thm list\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.conj : term\<close> , some ML level logical constructors \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.disj : term\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.imp : term\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.Not : term\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.mk_not : term -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.mk_conj : term * term -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.dest_conj : term -> term list\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> \<^ML>\<open>HOLogic.conjuncts : term -> term list\<close> \<^vs>\<open>-0.2cm\<close>
|
||
\<^enum> ...
|
||
\<close>
|
||
|
||
text*[T3::technical]\<open>In this style, extensions can be defined such as:\<close>
|
||
|
||
ML\<open>fun optionT t = Type(@{type_name "Option.option"},[t]); \<close>
|
||
|
||
subsection\<open> Type-Certification (=checking that a type annotation is consistent) \<close>
|
||
|
||
text\<open>
|
||
\<^enum> \<^ML>\<open>Type.typ_instance: Type.tsig -> typ * typ -> bool (* raises TYPE_MATCH *) \<close>
|
||
\<^enum> \<^ML>\<open> Term.dummyT : typ \<close> is a joker type that can be added as place-holder during term
|
||
construction. Jokers can be eliminated by the type inference. \<close>
|
||
|
||
|
||
text*[T4::technical]\<open>
|
||
\<^enum> \<^ML>\<open>Sign.typ_instance: theory -> typ * typ -> bool\<close>
|
||
\<^enum> \<^ML>\<open>Sign.typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv\<close>
|
||
\<^enum> \<^ML>\<open>Sign.typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int\<close>
|
||
\<^enum> \<^ML>\<open>Sign.const_type: theory -> string -> typ option\<close>
|
||
\<^enum> \<^ML>\<open>Sign.certify_term: theory -> term -> term * typ * int\<close>, the function for CERTIFICATION of types
|
||
\<^enum> \<^ML>\<open>Sign.cert_term: theory -> term -> term\<close>, short-cut for the latter
|
||
\<^enum> \<^ML>\<open>Sign.tsig_of: theory -> Type.tsig\<close>, projects from a theory the type signature
|
||
\<close>
|
||
text\<open>
|
||
\<^ML>\<open>Sign.typ_match\<close> etc. is actually an abstract wrapper on the structure
|
||
\<^ML_structure>\<open>Type\<close> which contains the heart of the type inference.
|
||
It also contains the type substitution type \<^ML_type>\<open>Type.tyenv\<close> which is
|
||
is actually a type synonym for \<^ML_type>\<open>(sort * typ) Vartab.table\<close>
|
||
which in itself is a synonym for \<^ML_type>\<open>'a Symtab.table\<close>, so
|
||
possesses the usual \<^ML>\<open>Symtab.empty\<close> and \<^ML>\<open>Symtab.dest\<close> operations. \<close>
|
||
|
||
text\<open>Note that \<^emph>\<open>polymorphic variables\<close> are treated like constant symbols
|
||
in the type inference; thus, the following test, that one type is an instance of the
|
||
other, yields false:\<close>
|
||
|
||
subsubsection*[exo4::example]\<open> Example:\<close>
|
||
|
||
ML\<open>
|
||
val ty = @{typ "'a option"};
|
||
val ty' = @{typ "int option"};
|
||
|
||
val Type("List.list",[S]) = @{typ "('a) list"}; (* decomposition example *)
|
||
|
||
val false = Sign.typ_instance @{theory}(ty', ty);
|
||
\<close>
|
||
text\<open>In order to make the type inference work, one has to consider \<^emph>\<open>schematic\<close>
|
||
type variables, which are more and more hidden from the Isar interface. Consequently,
|
||
the typ antiquotation above will not work for schematic type variables and we have
|
||
to construct them by hand on the SML level: \<close>
|
||
|
||
ML\<open> val t_schematic = Type("List.list",[TVar(("'a",0),@{sort "HOL.type"})]); \<close>
|
||
|
||
text\<open> MIND THE "'" !!! Ommitting it leads at times to VERY strange behaviour ...\<close>
|
||
|
||
text \<open>On this basis, the following \<^ML_type>\<open>Type.tyenv\<close> is constructed: \<close>
|
||
ML\<open>
|
||
val tyenv = Sign.typ_match ( @{theory})
|
||
(t_schematic, @{typ "int list"})
|
||
(Vartab.empty);
|
||
val [(("'a", 0), (["HOL.type"], @{typ "int"}))] = Vartab.dest tyenv;
|
||
\<close>
|
||
|
||
text\<open> Type generalization --- the conversion between free type variables and schematic
|
||
type variables --- is apparently no longer part of the standard API (there is a slightly
|
||
more general replacement in \<^ML>\<open>Term_Subst.generalizeT_same\<close>, however). Here is a way to
|
||
overcome this by a self-baked generalization function:\<close>
|
||
|
||
ML\<open>
|
||
val generalize_typ = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,0),sort));
|
||
val generalize_term = Term.map_types generalize_typ;
|
||
val true = Sign.typ_instance @{theory} (ty', generalize_typ ty)
|
||
\<close>
|
||
text\<open>... or more general variants thereof that are parameterized by the indexes for schematic
|
||
type variables instead of assuming just @{ML "0"}. \<close>
|
||
|
||
text\<open> Example:\<close>
|
||
ML\<open>val t = generalize_term @{term "[]"}\<close>
|
||
|
||
text\<open>Now we turn to the crucial issue of type-instantiation and with a given type environment
|
||
\<^ML>\<open>tyenv\<close>. For this purpose, one has to switch to the low-level interface
|
||
\<^ML_structure>\<open>Term_Subst\<close>. \<close>
|
||
|
||
subsection\<open>More operations on types\<close>
|
||
|
||
text\<open>
|
||
\<^item> \<^ML>\<open>Term_Subst.map_types_same : (typ -> typ) -> term -> term\<close>
|
||
\<^item> \<^ML>\<open>Term_Subst.map_aterms_same : (term -> term) -> term -> term\<close>
|
||
\<^item> \<^ML>\<open>Term_Subst.instantiate: typ TVars.table * term Vars.table -> term -> term\<close>
|
||
\<^item> \<^ML>\<open>Term_Subst.instantiateT: typ TVars.table -> typ -> typ\<close>
|
||
\<^item> \<^ML>\<open>Term_Subst.generalizeT: Names.set -> int -> typ -> typ\<close>
|
||
this is the standard type generalisation function !!!
|
||
only type-frees in the string-list were taken into account.
|
||
\<^item> \<^ML>\<open>Term_Subst.generalize: Names.set * Names.set -> int -> term -> term\<close>
|
||
this is the standard term generalisation function !!!
|
||
only type-frees and frees in the string-lists were taken
|
||
into account.
|
||
\<close>
|
||
|
||
|
||
|
||
text \<open>Apparently, a bizarre conversion between the old-style interface and
|
||
the new-style \<^ML>\<open>tyenv\<close> is necessary. See the following example.\<close>
|
||
ML\<open>
|
||
val S = Vartab.dest tyenv : (Vartab.key * (sort * typ)) list;
|
||
val S' = (map (fn (s,(t,u)) => ((s,t),u)) S) : ((indexname * sort) * typ) list;
|
||
(* it took me quite some time to find out that these two type representations,
|
||
obscured by a number of type-synonyms, where actually identical. *)
|
||
val S''= TVars.make S': typ TVars.table
|
||
val ty = t_schematic;
|
||
val ty' = Term_Subst.instantiateT S'' t_schematic;
|
||
|
||
(* Don't know how to build a typ TVars.table *)
|
||
val t = (generalize_term @{term "[]"});
|
||
|
||
val t' = Term_Subst.map_types_same (Term_Subst.instantiateT (TVars.make S')) (t)
|
||
(* or alternatively : *)
|
||
val t'' = Term.map_types (Term_Subst.instantiateT S'') (t)
|
||
\<close>
|
||
|
||
text\<open>A more abstract env for variable management in tactic proofs. A bit difficult to use
|
||
outside the very closed-up tracks of conventional use...\<close>
|
||
|
||
ML\<open> Consts.the_const; (* T is a kind of signature ... *)
|
||
Variable.import_terms;
|
||
Vartab.update;\<close>
|
||
|
||
subsection*[t232::technical]\<open> Type-Inference (= inferring consistent type information if possible) \<close>
|
||
|
||
text\<open> Type inference eliminates also joker-types such as @{ML dummyT} and produces
|
||
instances for schematic type variables where necessary. In the case of success,
|
||
it produces a certifiable term. \<close>
|
||
ML\<open> Type_Infer_Context.infer_types: Proof.context -> term list -> term list \<close>
|
||
|
||
subsection*[t237::technical]\<open>Constructing Terms without Type-Inference\<close>
|
||
text\<open>Using @{ML "Type_Infer_Context.infer_types"} is not quite unproblematic: since the type
|
||
inference can construct types for largely underspecified terms, it may happen that under
|
||
some circumstances, tactics and proof-attempts fail since just some internal term representation
|
||
was too general. A more defensive strategy is already sketched --- but neither explicitely
|
||
mentioned nor worked out in the interface in @{ML_structure HOLogic}. The idea is to have
|
||
advanced term constructors that construct the right term from the leaves, which were by convention
|
||
fully type-annotated (so: this does not work for terms with dangling @(ML Bound)'s).
|
||
|
||
Operations like @{ML "HOLogic.mk_prod"} or @{ML "HOLogic.mk_fst"} or @{ML "HOLogic.mk_eq"} do
|
||
exactly this by using an internal pure bottom-up type-inference @{ML "fastype_of"}.
|
||
The following routines are written in the same style complement the existing API
|
||
@{ML_structure HOLogic}.
|
||
\<close>
|
||
|
||
ML\<open>
|
||
fun mk_None ty = let val none = \<^const_name>\<open>Option.option.None\<close>
|
||
val none_ty = ty --> Type(\<^type_name>\<open>option\<close>,[ty])
|
||
in Const(none, none_ty)
|
||
end;
|
||
fun mk_Some t = let val some = \<^const_name>\<open>Option.option.Some\<close>
|
||
val ty = fastype_of t
|
||
val some_ty = ty --> Type(\<^type_name>\<open>option\<close>,[ty])
|
||
in Const(some, some_ty) $ t
|
||
end;
|
||
|
||
fun mk_undefined (@{typ "unit"}) = Const (\<^const_name>\<open>Product_Type.Unity\<close>, \<^typ>\<open>unit\<close>)
|
||
|mk_undefined t = Const (\<^const_name>\<open>HOL.undefined\<close>, t)
|
||
|
||
fun meta_eq_const T = Const (\<^const_name>\<open>Pure.eq\<close>, T --> T --> propT);
|
||
|
||
fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u;
|
||
|
||
\<close>
|
||
|
||
subsection\<open>Another Approach for Typed Parsing\<close>
|
||
|
||
text\<open>Another example for influencing @{ML "Syntax.read_term"} by modifying
|
||
the @{ML_type "Proof.context"}: \<close>
|
||
|
||
definition "zz = ()"
|
||
ML\<open>@{term zz}\<close> (* So : @(term "zz"} is now a constant*)
|
||
ML\<open>val Free ("zz", ty) = Proof_Context.add_fixes
|
||
[(@{binding "zz"}, SOME @{typ nat}, NoSyn)] @{context}
|
||
|> (fn (S, ctxt) => (writeln (String.concat S);
|
||
Syntax.read_term ctxt "zz"));
|
||
(* So : @(term "zz"} is here a free variable. *) \<close>
|
||
ML\<open>@{term zz}\<close> (* So : @(term "zz"} is now a constant again.*)
|
||
locale Z =
|
||
fixes zz :: nat
|
||
begin
|
||
ML\<open>@{term "(zz)"}\<close>
|
||
end
|
||
|
||
lemma True
|
||
proof - fix a :: nat
|
||
show True
|
||
ML_prf \<open>@{term a}\<close>
|
||
term a
|
||
oops
|
||
|
||
|
||
|
||
|
||
|
||
subsection*[t233::technical]\<open> Theories and the Signature API\<close>
|
||
text\<open>
|
||
\<^enum> \<^ML>\<open>Sign.tsig_of : theory -> Type.tsig\<close> extracts the type-signature of a theory
|
||
\<^enum> \<^ML>\<open>Sign.syn_of : theory -> Syntax.syntax\<close> extracts the constant-symbol signature
|
||
\<^enum> \<^ML>\<open>Sign.of_sort : theory -> typ * sort -> bool\<close> decides that a type belongs to a sort.
|
||
\<close>
|
||
|
||
subsection*[t234::technical]\<open>\<^ML_structure>\<open>Thm\<close>'s and the LCF-Style, "Mikro"-Kernel \<close>
|
||
text\<open>
|
||
The basic constructors and operations on theorems \<^file>\<open>$ISABELLE_HOME/src/Pure/thm.ML\<close>,
|
||
a set of derived (Pure) inferences can be found in \<^file>\<open>$ISABELLE_HOME/src/Pure/drule.ML\<close>.
|
||
|
||
The main types provided by structure \<^verbatim>\<open>thm\<close> are certified types \<^ML_type>\<open>Thm.ctyp\<close>,
|
||
certified terms \<^ML_type>\<open>Thm.cterm\<close>, \<^ML_type>\<open>Thm.thm\<close> as well as conversions \<^ML_type>\<open>Thm.conv\<close>
|
||
\<^ie>, transformation operations of \<^ML_type>\<open>Thm.thm\<close>s to logically equivalent ones.
|
||
|
||
Errors were reported with the \<^ML>\<open>CTERM: string * cterm list -> exn\<close>-exceptions.
|
||
|
||
Over this kernel, two infix main operations were provided:
|
||
\<^enum> \<^ML>\<open>op RS: thm * thm -> thm\<close> resolved the conclusion of left argument into the left-most
|
||
assumption of the right arguement, while
|
||
\<^enum> \<^ML>\<open>op RSN: thm * (int * thm) -> thm\<close> resolves the conclusion of the left argument into
|
||
the nth assumption of the right argument, so generalizes \<^ML>\<open>op RS\<close>.
|
||
|
||
Errors of the resolution operations were reported by
|
||
\<^ML>\<open>THM : string * int * thm list -> exn\<close>.
|
||
|
||
At a glance, the very heart of the kernel is represented as follows (UNSAFE):
|
||
\<close>
|
||
|
||
ML\<open>
|
||
signature BASIC_THM' =
|
||
sig
|
||
type ctyp
|
||
type cterm
|
||
exception CTERM of string * cterm list
|
||
type thm
|
||
type conv = cterm -> thm
|
||
exception THM of string * int * thm list
|
||
val RSN: thm * (int * thm) -> thm
|
||
val RS: thm * thm -> thm
|
||
end;
|
||
\<close>
|
||
|
||
text\<open>Certification of types and terms on the kernel-level is done by the generators:\<close>
|
||
text\<open>
|
||
\<^item> \<^ML>\<open> Thm.global_ctyp_of: theory -> typ -> ctyp\<close>
|
||
\<^item> \<^ML>\<open> Thm.ctyp_of: Proof.context -> typ -> ctyp\<close>
|
||
\<^item> \<^ML>\<open> Thm.global_cterm_of: theory -> term -> cterm\<close>
|
||
\<^item> \<^ML>\<open> Thm.cterm_of: Proof.context -> term -> cterm\<close>
|
||
\<close>
|
||
|
||
|
||
text\<open>... which perform type-checking in the given theory context in order to make a type
|
||
or term "admissible" for the kernel.\<close>
|
||
|
||
text\<open>These operations were internally used in the ML-antiquotation:\<open>ML\<open>\<^cterm>\<open>zero\<close>\<close>\<close> yielding:\<close>
|
||
ML\<open>\<^cterm>\<open>zero\<close>\<close>
|
||
|
||
text\<open> We come now to the very heart of the LCF-Kernel of Isabelle, which
|
||
provides the fundamental inference rules of Isabelle/Pure.
|
||
|
||
Besides a number of destructors on \<^ML_type>\<open>thm\<close>'s,
|
||
the abstract data-type \<^ML_type>\<open>thm\<close> is used for logical objects of the form
|
||
\<open>\<Gamma> \<turnstile>\<^sub>\<theta> \<phi>\<close>, where \<open>\<Gamma>\<close> represents a set of local assumptions,
|
||
\<open>\<theta>\<close> the global context or \<^ML_type>\<open>theory\<close> in which a formula \<open>\<phi>\<close>
|
||
has been constructed just by applying the following operations representing
|
||
the logical kernel inference rules:
|
||
|
||
\<^item> \<^ML>\<open> Thm.assume: cterm -> thm\<close>
|
||
\<^item> \<^ML>\<open> Thm.implies_intr: cterm -> thm -> thm\<close>
|
||
\<^item> \<^ML>\<open> Thm.implies_elim: thm -> thm -> thm\<close>
|
||
\<^item> \<^ML>\<open> Thm.forall_intr: cterm -> thm -> thm\<close>
|
||
\<^item> \<^ML>\<open> Thm.forall_elim: cterm -> thm -> thm\<close>
|
||
\<^item> \<^ML>\<open> Thm.transfer : theory -> thm -> thm\<close>
|
||
\<^item> \<^ML>\<open> Thm.generalize: Names.set * Names.set -> int -> thm -> thm\<close>
|
||
\<^item> \<^ML>\<open> Thm.instantiate: ctyp TVars.table * cterm Vars.table -> thm -> thm\<close>
|
||
\<close>
|
||
|
||
text\<open> They reflect the Pure logic depicted in a number of presentations such as
|
||
M. Wenzel, \<^emph>\<open>Parallel Proof Checking in Isabelle/Isar\<close>, PLMMS 2009, or simiular papers.
|
||
Notated as logical inference rules, these operations were presented as follows:
|
||
\<close>
|
||
|
||
side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-kernel1''",
|
||
caption="''Pure Kernel Inference Rules I ''",relative_width="48",
|
||
src="''figures/pure-inferences-I''",anchor2="''fig-kernel2''",
|
||
caption2="''Pure Kernel Inference Rules II''",relative_width2="47",
|
||
src2="''figures/pure-inferences-II''"]\<open> \<close>
|
||
|
||
(*
|
||
figure*[kir1::figure,relative_width="100",src="''figures/pure-inferences-I''"]
|
||
\<open> Pure Kernel Inference Rules I.\<close>
|
||
figure*[kir2::figure,relative_width="100",src="''figures/pure-inferences-II''"]
|
||
\<open> Pure Kernel Inference Rules II. \<close>
|
||
*)
|
||
|
||
text\<open>Note that the transfer rule:
|
||
\[
|
||
\begin{prooftree}
|
||
\<open>\<Gamma> \<turnstile>\<^sub>\<theta> \<phi>\<close> \qquad \qquad \<open>\<theta> \<sqsubseteq> \<theta>'\<close>
|
||
\justifies
|
||
\<open>\<Gamma> \<turnstile>\<^sub>\<theta>\<^sub>' \<phi>\<close> \qquad \qquad
|
||
\end{prooftree}
|
||
\]
|
||
which is a consequence of explicit theories characteristic for Isabelle's LCF-kernel design
|
||
and a remarkable difference to its sisters HOL-Light and HOL4; instead of transfer, these systems
|
||
reconstruct proofs in an enlarged global context instead of taking the result and converting it.\<close>
|
||
|
||
text\<open>Besides the meta-logical (Pure) implication \<open>_ \<Longrightarrow> _\<close>, the Kernel axiomatizes
|
||
also a Pure-Equality \<open>_ \<equiv> _\<close> used for definitions of constant symbols:
|
||
\<^item> \<^ML>\<open> Thm.reflexive: cterm -> thm\<close>
|
||
\<^item> \<^ML>\<open> Thm.symmetric: thm -> thm\<close>
|
||
\<^item> \<^ML>\<open> Thm.transitive: thm -> thm -> thm\<close>
|
||
\<close>
|
||
|
||
text\<open>The operation \<^ML>\<open> Thm.trivial: cterm -> thm \<close>
|
||
... produces the elementary tautologies of the form \<^prop>\<open>A \<Longrightarrow> A\<close>,
|
||
an operation used to start a backward-style proof.\<close>
|
||
|
||
text\<open>The elementary conversions are:
|
||
|
||
\<^item> \<^ML>\<open>Thm.beta_conversion: bool -> conv\<close>
|
||
\<^item> \<^ML>\<open>Thm.eta_conversion: conv\<close>
|
||
\<^item> \<^ML>\<open>Thm.eta_long_conversion: conv\<close>
|
||
\<close>
|
||
|
||
text\<open>On the level of \<^ML_structure>\<open>Drule\<close>, a number of higher-level operations is established,
|
||
which is in part accessible by a number of forward-reasoning notations on Isar-level.
|
||
|
||
\<^item> \<^ML>\<open> op RLN: thm list * (int * thm list) -> thm list\<close>
|
||
\<^item> \<^ML>\<open> op RL: thm list * thm list -> thm list\<close>
|
||
\<^item> \<^ML>\<open> op MRS: thm list * thm -> thm\<close>
|
||
\<^item> \<^ML>\<open> op OF: thm * thm list -> thm\<close>
|
||
\<^item> \<^ML>\<open> op COMP: thm * thm -> thm\<close>
|
||
\<close>
|
||
|
||
|
||
subsection*[t235::technical]\<open> \<^ML_structure>\<open>Theory\<close>'s \<close>
|
||
|
||
text \<open> This structure yields the abstract datatype \<^ML_structure>\<open>Theory\<close> which becomes the content of
|
||
\<^ML_type>\<open>Context.theory\<close>. In a way, the LCF-Kernel registers itself into the Nano-Kernel,
|
||
which inspired me (bu) to this naming. However, not that this is a mental model: the Nano-Kernel
|
||
offers ab initio many operations directly linked to its main purpose: incommodating the
|
||
micro-kernel and its management of local and global contexts.
|
||
\<close>
|
||
|
||
text\<open>
|
||
@{theory_text [display]
|
||
\<open>
|
||
intern Theory.Thy;
|
||
|
||
datatype thy = Thy of
|
||
{pos: Position.T,
|
||
id: serial,
|
||
axioms: term Name_Space.table,
|
||
defs: Defs.T,
|
||
wrappers: wrapper list * wrapper list};
|
||
\<close>}
|
||
|
||
\<^item> \<^ML>\<open>Theory.check: {long: bool} -> Proof.context -> string * Position.T -> theory\<close>
|
||
\<^item> \<^ML>\<open>Theory.local_setup: (Proof.context -> Proof.context) -> unit\<close>
|
||
\<^item> \<^ML>\<open>Theory.setup: (theory -> theory) -> unit\<close> (* The thing to extend the table of "command"s with parser - callbacks. *)
|
||
\<^item> \<^ML>\<open>Theory.get_markup: theory -> Markup.T\<close>
|
||
\<^item> \<^ML>\<open>Theory.axiom_table: theory -> term Name_Space.table\<close>
|
||
\<^item> \<^ML>\<open>Theory.axiom_space: theory -> Name_Space.T\<close>
|
||
\<^item> \<^ML>\<open>Theory.all_axioms_of: theory -> (string * term) list\<close>
|
||
\<^item> \<^ML>\<open>Theory.defs_of: theory -> Defs.T\<close>
|
||
\<^item> \<^ML>\<open>Theory.join_theory: theory list -> theory\<close>
|
||
\<^item> \<^ML>\<open>Theory.at_begin: (theory -> theory option) -> theory -> theory\<close>
|
||
\<^item> \<^ML>\<open>Theory.at_end: (theory -> theory option) -> theory -> theory\<close>
|
||
\<^item> \<^ML>\<open>Theory.begin_theory: string * Position.T -> theory list -> theory\<close>
|
||
\<^item> \<^ML>\<open>Theory.end_theory: theory -> theory\<close>
|
||
\<close>
|
||
|
||
section*[t26::technical]\<open>Advanced Specification Constructs\<close>
|
||
text\<open>Isabelle is built around the idea that system components were built on top
|
||
of the kernel in order to give the user high-level specification constructs
|
||
--- rather than inside as in the Coq kernel that foresees, for example, data-types
|
||
and primitive recursors already in the basic \<open>\<lambda>\<close>-term language.
|
||
Therefore, records, definitions, type-definitions, recursive function definitions
|
||
are supported by packages that belong to the \<^emph>\<open>components\<close> strata.
|
||
With the exception of the \<^ML>\<open>Specification.axiomatization\<close> construct, they
|
||
are all-together built as composition of conservative extensions.
|
||
|
||
The components are a bit scattered in the architecture. A relatively recent and
|
||
high-level component (more low-level components such as \<^ML>\<open>Global_Theory.add_defs\<close>
|
||
exist) for definitions and axiomatizations is here:
|
||
\<close>
|
||
|
||
text\<open>
|
||
\<^item> \<^ML>\<open>Specification.definition: (binding * typ option * mixfix) option ->
|
||
(binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
|
||
local_theory -> (term * (string * thm)) * local_theory\<close>
|
||
\<^item> \<^ML>\<open>Specification.definition_cmd: (binding * string option * mixfix) option ->
|
||
(binding * string option * mixfix) list -> string list -> Attrib.binding * string ->
|
||
bool -> local_theory -> (term * (string * thm)) * local_theory\<close>
|
||
\<^item> \<^ML>\<open>Specification.axiomatization: (binding * typ option * mixfix) list ->
|
||
(binding * typ option * mixfix) list -> term list ->
|
||
(Attrib.binding * term) list -> theory -> (term list * thm list) * theory\<close>
|
||
\<^item> \<^ML>\<open>Specification.axiomatization_cmd: (binding * string option * mixfix) list ->
|
||
(binding * string option * mixfix) list -> string list ->
|
||
(Attrib.binding * string) list -> theory -> (term list * thm list) * theory\<close>
|
||
\<^item> \<^ML>\<open>Specification.axiom: Attrib.binding * term -> theory -> thm * theory\<close>
|
||
\<^item> \<^ML>\<open>Specification.abbreviation: Syntax.mode -> (binding * typ option * mixfix) option ->
|
||
(binding * typ option * mixfix) list -> term -> bool -> local_theory -> local_theory\<close>
|
||
\<^item> \<^ML>\<open>Specification.abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option ->
|
||
(binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory\<close>
|
||
\<close>
|
||
|
||
|
||
text\<open>
|
||
Note that the interface is mostly based on \<^ML_type>\<open>local_theory\<close>, which is a synonym to
|
||
\<^ML_type>\<open>Proof.context\<close>. Need to lift this to a global system transition ?
|
||
Don't worry, \<^ML>\<open>Named_Target.theory_map: (local_theory -> local_theory) -> theory -> theory\<close>
|
||
does the trick.
|
||
\<close>
|
||
|
||
subsection*[t261::example]\<open>Example\<close>
|
||
|
||
text\<open>Suppose that we want do \<^theory_text>\<open>definition I :: "'a \<Rightarrow> 'a" where "I x = x"\<close> at the ML-level.
|
||
We construct our defining equation and embed it as a \<^typ>\<open>prop\<close> into Pure.
|
||
\<close>
|
||
ML\<open> val ty = @{typ "'a"}
|
||
val term = HOLogic.mk_eq (Free("I",ty -->ty) $ Free("x", ty), Free("x", ty));
|
||
val term_prop = HOLogic.mk_Trueprop term\<close>
|
||
text\<open>Recall the notes on defensive term construction wrt. typing in @{docitem "t237"}.
|
||
Then the trick is done by:\<close>
|
||
|
||
setup\<open>
|
||
let
|
||
fun mk_def name p =
|
||
let val nameb = Binding.make(name,p)
|
||
val ty_global = ty --> ty
|
||
val args = (((SOME(nameb,SOME ty_global,NoSyn),(Binding.empty_atts,term_prop)),[]),[])
|
||
val cmd = (fn (((decl, spec), prems), params) =>
|
||
#2 o Specification.definition decl params prems spec)
|
||
in cmd args
|
||
end;
|
||
in Named_Target.theory_map (mk_def "I" @{here} )
|
||
end\<close>
|
||
|
||
thm I_def
|
||
text\<open>Voilà.\<close>
|
||
|
||
section*[t24::technical]\<open>Backward Proofs: Tactics, Tacticals and Goal-States\<close>
|
||
|
||
text\<open>At this point, we leave the Pure-Kernel and start to describe the first layer on top
|
||
of it, involving support for specific styles of reasoning and automation of reasoning.\<close>
|
||
|
||
text\<open> \<^ML_type>\<open>tactic\<close>'s are in principle \<^emph>\<open>relations\<close> on theorems \<^ML_type>\<open>thm\<close>; the relation is
|
||
lazy and encoded as function of type \<^ML_type>\<open>thm -> thm Seq.seq\<close>.
|
||
This gives a natural way to represent the fact that HO-Unification
|
||
(and therefore the mechanism of rule-instantiation) are non-deterministic in principle.
|
||
Heuristics may choose particular preferences between
|
||
the theorems in the range of this relation, but the Isabelle Design accepts this fundamental
|
||
fact reflected at this point in the prover architecture.
|
||
This potentially infinite relation is implemented by a function of theorems to lazy lists
|
||
over theorems, which gives both sufficient structure for heuristic
|
||
considerations as well as a nice algebra, called \<^ML_structure>\<open>Tactical\<close>'s, providing a bottom element
|
||
\<^ML>\<open>no_tac\<close> (the function that always fails), the top-element \<^ML>\<open>all_tac\<close>
|
||
(the function that never fails), sequential composition \<^ML>\<open>op THEN\<close>, (serialized)
|
||
non-deterministic composition \<^ML>\<open>op ORELSE\<close>, conditionals, repetitions over lists, etc.
|
||
The following is an excerpt of \<^file>\<open>~~/src/Pure/tactical.ML\<close>:\<close>
|
||
|
||
|
||
text\<open> More specialized variants of \<^ML_structure>\<open>Tactical\<close>'s are:
|
||
|
||
\<^item> \<^ML>\<open>op THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic\<close> -- lifted version
|
||
\<^item> \<^ML>\<open>op ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic\<close> -- lifted version
|
||
\<^item> \<^ML>\<open>op TRY: tactic -> tactic\<close> -- option
|
||
\<^item> \<^ML>\<open>op EVERY: tactic list -> tactic\<close> -- sequential enchainment
|
||
\<^item> \<^ML>\<open>op EVERY': ('a -> tactic) list -> 'a -> tactic\<close> -- lifted version
|
||
\<^item> \<^ML>\<open>op FIRST: tactic list -> tactic\<close> -- alternative enchainment
|
||
\<^item> etc.
|
||
|
||
\<close>
|
||
|
||
|
||
text\<open>The next layer in the architecture describes \<^ML_type>\<open>tactic\<close>'s, i.e. basic operations on
|
||
theorems in a backward reasoning style (bottom up development of proof-trees). An initial
|
||
goal-state for some property \<^prop>\<open>A\<close> --- the \<^emph>\<open>goal\<close> --- is constructed via the kernel
|
||
\<^ML>\<open>Thm.trivial\<close>-operation into \<^prop>\<open>A \<Longrightarrow> A\<close>, and tactics either refine the premises --- the
|
||
\<^emph>\<open>subgoals\<close> of this meta-implication --- producing more and more of them or eliminate them
|
||
in subsequent goal-states. Subgoals of the form \<^prop>\<open>B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> A \<Longrightarrow> B\<^sub>3 \<Longrightarrow> B\<^sub>4 \<Longrightarrow> A\<close> can be
|
||
eliminated via the \<^ML>\<open>Tactic.assume_tac\<close>-tactic, and a subgoal \<^prop>\<open>C\<^sub>m\<close> can be refined via the
|
||
theorem \<^prop>\<open>E\<^sub>1 \<Longrightarrow> E\<^sub>2 \<Longrightarrow> E\<^sub>3 \<Longrightarrow> C\<^sub>m\<close> the \<^ML>\<open>Tactic.resolve_tac\<close> - tactic to new subgoals
|
||
\<^prop>\<open>E\<^sub>1\<close>, \<^prop>\<open>E\<^sub>2\<close>, \<^prop>\<open>E\<^sub>3\<close>. In case that a theorem used for resolution has no premise \<^prop>\<open>E\<^sub>i\<close>,
|
||
the subgoal \<^prop>\<open>C\<^sub>m\<close> is also eliminated ("closed").
|
||
|
||
The following abstract of the most commonly used \<^ML_type>\<open>tactic\<close>'s drawn from
|
||
\<^file>\<open>~~/src/Pure/tactic.ML\<close> are summarized as follows:
|
||
|
||
\<^item> \<^ML>\<open> assume_tac: Proof.context -> int -> tactic\<close>
|
||
\<^item> \<^ML>\<open> compose_tac: Proof.context -> (bool * thm * int) -> int -> tactic\<close>
|
||
\<^item> \<^ML>\<open> resolve_tac: Proof.context -> thm list -> int -> tactic\<close>
|
||
\<^item> \<^ML>\<open> eresolve_tac: Proof.context -> thm list -> int -> tactic\<close>
|
||
\<^item> \<^ML>\<open> forward_tac: Proof.context -> thm list -> int -> tactic\<close>
|
||
\<^item> \<^ML>\<open> dresolve_tac: Proof.context -> thm list -> int -> tactic\<close>
|
||
\<^item> \<^ML>\<open> rotate_tac: int -> int -> tactic\<close>
|
||
\<^item> \<^ML>\<open> defer_tac: int -> tactic\<close>
|
||
\<^item> \<^ML>\<open> prefer_tac: int -> tactic\<close>
|
||
\<^item> ...
|
||
\<close>
|
||
|
||
text\<open>Note that "applying a rule" is a fairly complex operation in the Extended Isabelle Kernel,
|
||
i.e. the tactic layer. It involves at least four phases, interfacing a theorem
|
||
coming from the global context $\theta$ (=theory), be it axiom or derived, into a given goal-state.
|
||
\<^item> \<^emph>\<open>generalization\<close>. All free variables in the theorem were replaced by schematic variables.
|
||
For example, \<^term>\<open>x + y = y + x\<close> is converted into
|
||
\<open>?x + ?y = ?y + ?x\<close>.
|
||
By the way, type variables were treated equally.
|
||
\<^item> \<^emph>\<open>lifting over assumptions\<close>. If a subgoal is of the form:
|
||
\<^prop>\<open>B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> A\<close> and we have a theorem \<^prop>\<open>D\<^sub>1 \<Longrightarrow> D\<^sub>2 \<Longrightarrow> A\<close>, then before
|
||
applying the theorem, the premisses were \<^emph>\<open>lifted\<close> resulting in the logical refinement:
|
||
\<^prop>\<open>(B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> D\<^sub>1) \<Longrightarrow> (B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> D\<^sub>2) \<Longrightarrow> A\<close>. Now, \<^ML>\<open>resolve_tac\<close>, for example,
|
||
will replace the subgoal \<^prop>\<open>B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> A\<close> by the subgoals
|
||
\<^prop>\<open>B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> D\<^sub>1\<close> and \<^prop>\<open>B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> D\<^sub>2\<close>. Of course, if the theorem wouldn't
|
||
have assumptions \<^prop>\<open>D\<^sub>1\<close> and \<^prop>\<open>D\<^sub>2\<close>, the subgoal \<^prop>\<open>A\<close> would be replaced by
|
||
\<^bold>\<open>nothing\<close>, i.e. deleted.
|
||
\<^item> \<^emph>\<open>lifting over parameters\<close>. If a subgoal is meta-quantified like in:
|
||
\<^prop>\<open>\<And> x y z. A x y z\<close>, then a theorem like \<^prop>\<open>D\<^sub>1 \<Longrightarrow> D\<^sub>2 \<Longrightarrow> A\<close> is \<^emph>\<open>lifted\<close>
|
||
to \<^prop>\<open>\<And> x y z. D\<^sub>1' \<Longrightarrow> D\<^sub>2' \<Longrightarrow> A'\<close>, too. Since free variables occurring in \<^prop>\<open>D\<^sub>1\<close>,
|
||
\<^prop>\<open>D\<^sub>2\<close> and \<^prop>\<open>A\<close> have been replaced by schematic variables (see phase one),
|
||
they must be replaced by parameterized schematic variables, i. e. a kind of skolem function.
|
||
For example, \<open>?x + ?y = ?y + ?x\<close> would be lifted to
|
||
\<open>\<And> x y z. ?x x y z + ?y x y z = ?y x y z + ?x x y z\<close>. This way, the lifted theorem
|
||
can be instantiated by the parameters \<open>x y z\<close> representing "fresh free variables"
|
||
used for this sub-proof. This mechanism implements their logically correct bookkeeping via
|
||
kernel primitives.
|
||
\<^item> \<^emph>\<open>Higher-order unification (of schematic type and term variables)\<close>.
|
||
Finally, for all these schematic variables, a solution must be found.
|
||
In the case of \<^ML>\<open>resolve_tac\<close>, the conclusion of the (doubly lifted) theorem must
|
||
be equal to the conclusion of the subgoal, so \<^term>\<open>A\<close> must be \<open>\<alpha>/\<beta>\<close>-equivalent to
|
||
\<^term>\<open>A'\<close> in the example above, which is established by a higher-order unification
|
||
process. It is a bit unfortunate that for implementation efficiency reasons, a very substantial
|
||
part of the code for HO-unification is in the kernel module \<^ML_type>\<open>thm\<close>, which makes this
|
||
critical component of the architecture larger than necessary.
|
||
\<close>
|
||
|
||
text\<open>In a way, the two lifting processes represent an implementation of the conversion between
|
||
Gentzen Natural Deduction (to which Isabelle/Pure is geared) reasoning and
|
||
Gentzen Sequent Deduction.\<close>
|
||
|
||
|
||
section*[goalp::technical]\<open>The classical goal package\<close>
|
||
text\<open>The main mechanism in Isabelle as an LCF-style system is to produce \<^ML_type>\<open>thm\<close>'s
|
||
in backward-style via tactics as described in @{technical "t24"}. Given a context
|
||
--- be it global as \<^ML_type>\<open>theory\<close> or be it inside a proof-context as \<^ML_type>\<open>Proof.context\<close>,
|
||
user-programmed verification of (type-checked) terms or just strings can be done via the
|
||
operations:
|
||
|
||
\<^item> \<^ML>\<open>Goal.prove_internal : Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm\<close>
|
||
\<^item> \<^ML>\<open>Goal.prove_global : theory -> string list -> term list -> term ->
|
||
({context: Proof.context, prems: thm list} -> tactic) -> thm\<close>
|
||
\<^item> ... and many more variants.
|
||
\<close>
|
||
|
||
subsection*[ex211::example]\<open>Proof Example (Low-level)\<close>
|
||
|
||
text\<open>Take this proof at Isar Level as example:\<close>
|
||
|
||
lemma X : "(10::int) + 2 = 12" by simp
|
||
|
||
declare X[simp]
|
||
|
||
text\<open>This represents itself at the SML interface as follows:\<close>
|
||
|
||
ML\<open>
|
||
structure SimpleSampleProof =
|
||
struct
|
||
|
||
val tt = HOLogic.mk_Trueprop (Syntax.read_term @{context} "(10::int) + 2 = 12");
|
||
(* read_term parses and type-checks its string argument;
|
||
HOLogic.mk_Trueprop wraps the embedder from @{ML_type "bool"} to
|
||
@{ML_type "prop"} from Pure. *)
|
||
|
||
fun derive_thm name term lthy =
|
||
Goal.prove lthy (* global context *)
|
||
[name] (* name ? *)
|
||
[] (* local assumption context *)
|
||
(term) (* parsed goal *)
|
||
(fn _ => simp_tac lthy 1) (* proof tactic *)
|
||
|> Thm.close_derivation \<^here> (* some cleanups *);
|
||
|
||
val thm111_intern = derive_thm "thm111" tt @{context} (* just for fun at the ML level *)
|
||
|
||
fun store_thm name thm lthy =
|
||
lthy |> snd o Local_Theory.note ((Binding.name name, []), [thm])
|
||
|
||
|
||
val prove_n_store = (Named_Target.theory_map(fn lthy =>
|
||
let val thm = derive_thm "thm111" tt lthy
|
||
in lthy |> store_thm "thm111" thm end));
|
||
|
||
end
|
||
\<close>
|
||
|
||
text\<open>Converting a local theory transformation into a global one:\<close>
|
||
setup\<open>SimpleSampleProof.prove_n_store\<close>
|
||
|
||
text\<open>... and there it is in the global (Isar) context:\<close>
|
||
thm "thm111"
|
||
|
||
|
||
|
||
|
||
|
||
section\<open>Toplevel --- aka. ''The Isar Engine''\<close>
|
||
|
||
text\<open> The main structure of the Isar-engine is \<^ML_structure>\<open>Toplevel\<close>.
|
||
The Isar Toplevel (aka "the Isar engine" or the "Isar Interpreter") is a transaction
|
||
machine sitting over the Isabelle Kernel steering some asynchronous evaluation during the
|
||
evaluation of Isabelle/Isar input, usually stemming from processing Isabelle \<^verbatim>\<open>.thy\<close>-files. \<close>
|
||
|
||
subsection*[tplstate::technical] \<open>Toplevel Transaction Management in the Isar-Engine\<close>
|
||
text\<open>
|
||
The structure \<^ML_structure>\<open>Toplevel\<close> provides an internal \<^ML_type>\<open>state\<close> with the
|
||
necessary infrastructure --- i.e. the operations to pack and unpack theories and
|
||
queries on it:
|
||
|
||
\<^item> \<^ML>\<open> Toplevel.theory_toplevel: theory -> Toplevel.state\<close>
|
||
\<^item> \<^ML>\<open> Toplevel.init_toplevel: unit -> Toplevel.state\<close>
|
||
\<^item> \<^ML>\<open> Toplevel.is_toplevel: Toplevel.state -> bool\<close>
|
||
\<^item> \<^ML>\<open> Toplevel.is_theory: Toplevel.state -> bool\<close>
|
||
\<^item> \<^ML>\<open> Toplevel.is_proof: Toplevel.state -> bool\<close>
|
||
\<^item> \<^ML>\<open> Toplevel.is_skipped_proof: Toplevel.state -> bool\<close>
|
||
\<^item> \<^ML>\<open> Toplevel.level: Toplevel.state -> int\<close>
|
||
\<^item> \<^ML>\<open> Toplevel.context_of: Toplevel.state -> Proof.context\<close>
|
||
extracts the local context
|
||
\<^item> \<^ML>\<open> Toplevel.generic_theory_of: Toplevel.state -> generic_theory\<close>
|
||
extracts the generic (local or global) context
|
||
\<^item> \<^ML>\<open> Toplevel.theory_of: Toplevel.state -> theory\<close>
|
||
extracts the global context
|
||
\<^item> \<^ML>\<open> Toplevel.proof_of: Toplevel.state -> Proof.state\<close>
|
||
\<^item> \<^ML>\<open> Toplevel.presentation_context: Toplevel.state -> Proof.context\<close>
|
||
\<^item> ...
|
||
\<close>
|
||
|
||
text\<open> Type \<^ML_type>\<open>Toplevel.state\<close> represents Isar toplevel states, which are normally
|
||
manipulated through the concept of toplevel transitions only.
|
||
This type is constructed as the sum of \<^emph>\<open>empty state\<close>, \<^ML_type>\<open>Context.generic\<close>
|
||
(synonym to \<^ML_type>\<open>generic_theory\<close>) and enriched versions of proof states or
|
||
abort proofs.
|
||
\<close>
|
||
|
||
|
||
subsection*[transmgt::technical] \<open>Toplevel Transaction Management in the Isar-Engine\<close>
|
||
|
||
text\<open> The extensibility of Isabelle as a system framework depends on a number of tables,
|
||
into which various concepts commands, ML-antiquotations, text-antiquotations, cartouches, ...
|
||
can be entered via a late-binding on the fly.
|
||
|
||
The main operations to toplevel transitions are:
|
||
|
||
\<^item> \<^ML>\<open>Toplevel.keep: (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition\<close>
|
||
adjoins a diagnostic command
|
||
\<^item> \<^ML>\<open>Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition\<close>
|
||
adjoins a theory transformer.
|
||
\<^item> \<^ML>\<open>Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition\<close>
|
||
\<^item> \<^ML>\<open>Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition\<close>
|
||
\<^item> \<^ML>\<open>Toplevel.exit: Toplevel.transition -> Toplevel.transition\<close>
|
||
\<^item> \<^ML>\<open>Toplevel.ignored: Position.T -> Toplevel.transition\<close>
|
||
\<^item> \<^ML>\<open>Toplevel.present_local_theory: (xstring * Position.T) option ->
|
||
(Toplevel.state -> Latex.text) -> Toplevel.transition -> Toplevel.transition\<close>
|
||
|
||
\<close>
|
||
subsection*[cmdbinding::technical] \<open>Toplevel Transaction Management in the Isar-Engine\<close>
|
||
text\<open>
|
||
Toplevel transitions can finally be registered together with commandkeywords and
|
||
IDE information into the toplevel.
|
||
The global type of this key function for extending the Isar toplevel is, together
|
||
with a few query operations on the state of the toplevel:
|
||
\<^item> \<^ML>\<open>Outer_Syntax.command : Outer_Syntax.command_keyword -> string ->
|
||
(Toplevel.transition -> Toplevel.transition) parser -> unit\<close>,
|
||
\<^item> \<^ML>\<open>Document.state : unit -> Document.state\<close>, giving the state as a "collection" of named
|
||
nodes, each consisting of an editable list of commands, associated with asynchronous
|
||
execution process,
|
||
\<^item> \<^ML>\<open>Session.get_keywords : unit -> Keyword.keywords\<close>, this looks to be session global,
|
||
\<^item> \<^ML>\<open>Thy_Header.get_keywords : theory -> Keyword.keywords\<close> this looks to be just theory global.
|
||
|
||
|
||
A paradigmatic example is the \<^ML>\<open>Outer_Syntax.command\<close>-operation, which ---
|
||
representing itself as a toplevel system transition --- allows to define a new
|
||
command section and bind its syntax and semantics at a specific keyword.
|
||
Calling \<^ML>\<open>Outer_Syntax.command\<close> creates an implicit \<^ML>\<open>Theory.setup\<close> with an entry
|
||
for a call-back function, which happens to be a parser that must have as side-effect
|
||
a Toplevel-transition-transition.
|
||
Registers \<^ML_type>\<open>Toplevel.transition -> Toplevel.transition\<close> parsers to the
|
||
Isar interpreter.\<close>
|
||
|
||
text\<open>The file \<^file>\<open>~~/src/HOL/Examples/Commands.thy\<close> shows some example Isar command definitions, with the
|
||
all-important theory header declarations for outer syntax keywords.\<close>
|
||
|
||
text\<open>@{ML_structure Pure_Syn}\<close>
|
||
|
||
subsubsection*[ex1137::example]\<open>Examples: \<^theory_text>\<open>text\<close>\<close>
|
||
text\<open> The integration of the \<^theory_text>\<open>text\<close>-command is done as follows:
|
||
|
||
@{ML [display]\<open>
|
||
Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
|
||
(Parse.opt_target -- Parse.document_source >> Document_Output.document_output
|
||
{markdown = true, markup = I})
|
||
\<close>}
|
||
|
||
where \<^ML>\<open>Document_Output.document_output\<close> is the defining operation for the
|
||
"diagnostic" (=side-effect-free) toplevel operation.
|
||
\<^ML>\<open>Document_Output.document_output\<close> looks as follows:
|
||
|
||
@{ML [display]\<open>let fun document_reports txt =
|
||
let val pos = Input.pos_of txt in
|
||
[(pos, Markup.language_document (Input.is_delimited txt)),
|
||
(pos, Markup.plain_text)]
|
||
end;
|
||
fun document_output {markdown, markup} (loc, txt) =
|
||
let
|
||
fun output st =
|
||
let
|
||
val ctxt = Toplevel.presentation_context st;
|
||
val _ = Context_Position.reports ctxt (document_reports txt);
|
||
in txt |> Document_Output.output_document ctxt {markdown = markdown} |> markup end;
|
||
in
|
||
Toplevel.present (fn st =>
|
||
(case loc of
|
||
NONE => output st
|
||
| SOME (_, pos) =>
|
||
error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
|
||
Toplevel.present_local_theory loc output
|
||
end in () end
|
||
\<close>}
|
||
\<close>
|
||
|
||
subsubsection*[ex1138::example]\<open>Examples: \<^theory_text>\<open>ML\<close>\<close>
|
||
|
||
text\<open>
|
||
The integration of the \<^theory_text>\<open>ML\<close>-command is done as follows:
|
||
|
||
@{ML [display]\<open>
|
||
Outer_Syntax.command ("ML", \<^here>) "ML text within theory or local theory"
|
||
(Parse.ML_source >> (fn source =>
|
||
Toplevel.generic_theory
|
||
(ML_Context.exec (fn () =>
|
||
ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
|
||
Local_Theory.propagate_ml_env)))
|
||
\<close>}
|
||
\<close>
|
||
|
||
|
||
subsection\<open>Miscellaneous\<close>
|
||
|
||
text\<open>Here are a few queries relevant for the global config of the isar engine:\<close>
|
||
ML\<open> Document.state();\<close>
|
||
ML\<open> Session.get_keywords(); (* this looks to be session global. *) \<close>
|
||
ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
|
||
|
||
|
||
subsection*[conf::technical]\<open> Configuration Flags in the Isar-engine. \<close>
|
||
text\<open>The toplevel also provides an infrastructure for managing configuration options
|
||
for system components. Based on a sum-type @{ML_type Config.value }
|
||
with the alternatives \<^verbatim>\<open> Bool of bool | Int of int | Real of real | String of string\<close>
|
||
and building the parametric configuration types @{ML_type "'a Config.T" } and the
|
||
instance \<^verbatim>\<open>type raw = value T\<close>, for all registered configurations the protocol:
|
||
|
||
|
||
\<^item> \<^ML>\<open>Config.get : Proof.context -> 'a Config.T -> 'a\<close>
|
||
\<^item> \<^ML>\<open>Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context\<close>
|
||
\<^item> \<^ML>\<open>Config.put: 'a Config.T -> 'a -> Proof.context -> Proof.context\<close>
|
||
\<^item> \<^ML>\<open>Config.get_global: theory -> 'a Config.T -> 'a\<close>
|
||
\<^item> \<^ML>\<open>Config.map_global: 'a Config.T -> ('a -> 'a) -> theory -> theory\<close>
|
||
\<^item> \<^ML>\<open>Config.put_global: 'a Config.T -> 'a -> theory -> theory\<close>
|
||
\<^item> ... etc. is defined.
|
||
\<close>
|
||
|
||
|
||
subsubsection*[ex::example]\<open>Example registration of a config attribute \<close>
|
||
text\<open>The attribute XS232 is initialized by false:\<close>
|
||
ML\<open>
|
||
val (XS232, XS232_setup)
|
||
= Attrib.config_bool \<^binding>\<open>XS232\<close> (K false);
|
||
|
||
val _ = Theory.setup XS232_setup;\<close>
|
||
|
||
text \<open>... which could also be achieved by \<open>setup\<open>XS232_setup\<close>\<close>. \<close>
|
||
|
||
subsubsection*[ex33333::example]\<open>Defining a high-level attribute:\<close>
|
||
ML\<open>
|
||
Attrib.setup \<^binding>\<open>simp\<close> (Attrib.add_del Simplifier.simp_add Simplifier.simp_del)
|
||
"declaration of Simplifier rewrite rule"
|
||
\<close>
|
||
|
||
|
||
subsection*[ex333::example]\<open>A Hack:\<close>
|
||
|
||
text\<open>Another mechanism are global synchronised variables:\<close>
|
||
ML\<open>
|
||
|
||
val C = Synchronized.var "Pretty.modes" "latEEex";
|
||
(* Synchronized: a mechanism to bookkeep global
|
||
variables with synchronization mechanism included *)
|
||
Synchronized.value C;\<close>
|
||
|
||
|
||
subsection*[ex213::example]\<open>A Definition Command (High-level)\<close>
|
||
|
||
text\<open>A quite complex example is drawn from the Theory \<^verbatim>\<open>Clean\<close>; it generates \<close>
|
||
|
||
ML\<open>Specification.definition\<close>
|
||
|
||
ML\<open>
|
||
structure HLDefinitionSample =
|
||
struct
|
||
fun cmd (decl, spec, prems, params) = #2 o Specification.definition decl params prems spec
|
||
|
||
fun MON_SE_T res state = state --> optionT(HOLogic.mk_prodT(res,state));
|
||
|
||
fun push_eq binding name_op rty sty lthy =
|
||
let val mty = MON_SE_T rty sty
|
||
val thy = Proof_Context.theory_of lthy
|
||
val term = Free("\<sigma>",sty)
|
||
in mk_meta_eq((Free(name_op, mty) $ Free("\<sigma>",sty)),
|
||
mk_Some ( HOLogic.mk_prod (mk_undefined rty,term)))
|
||
|
||
end;
|
||
|
||
fun mk_push_name binding = Binding.prefix_name "push_" binding
|
||
|
||
fun mk_push_def binding sty lthy =
|
||
let val name = mk_push_name binding
|
||
val rty = \<^typ>\<open>unit\<close>
|
||
val eq = push_eq binding (Binding.name_of name) rty sty lthy
|
||
val mty = MON_SE_T rty sty
|
||
val args = (SOME(name, SOME mty, NoSyn), (Binding.empty_atts,eq),[],[])
|
||
in cmd args lthy end;
|
||
|
||
val define_test = Named_Target.theory_map (mk_push_def (Binding.name "test") @{typ "'a"})
|
||
|
||
end
|
||
\<close>
|
||
|
||
setup\<open>HLDefinitionSample.define_test\<close>
|
||
|
||
subsection*[ex212::example]\<open>Proof Example (High-level)\<close>
|
||
|
||
text\<open>The Isar-toplevel refers to a level of "specification constructs"; i.e. to a level with
|
||
more high-level commands that represent internally quite complex theory transformations;
|
||
with the exception of the axiomatization constructs, they are alltogether logically conservative.
|
||
The proof command interface behind \<open>lemma\<close> or \<open>theorem\<close> uses a structure capturing the
|
||
syntactic @{ML_structure Element}'s of the \<open>fix\<close>, \<open>assume\<close>, \<open>shows\<close> structuring.
|
||
\<close>
|
||
|
||
text\<open>By the way, the Isar-language Element interface can by found under @{ML_structure Element}:
|
||
\<^enum> @{ML "Element.Fixes : (binding * 'a option * mixfix) list -> ('a, 'b, 'c) Element.ctxt"}
|
||
\<^enum> @{ML "Element.Assumes: (Attrib.binding * ('a * 'a list) list) list -> ('b, 'a, 'c) Element.ctxt"}
|
||
\<^enum> @{ML "Element.Notes: string * (Attrib.binding * ('a * Token.src list) list) list
|
||
-> ('b, 'c, 'a) Element.ctxt"}
|
||
\<^enum> @{ML "Element.Shows: (Attrib.binding * ('a * 'a list) list) list -> ('b, 'a) Element.stmt"}
|
||
\<close>
|
||
|
||
(* UNCHECKED ! ! ! *)
|
||
|
||
ML\<open>
|
||
fun lemma1 lemma_name goals_to_prove a lthy =
|
||
let val lemma_name_bdg =(Binding.make (lemma_name, @{here}), [])
|
||
val attrs' = ["simp"] (* ?????? *)
|
||
in lthy |>
|
||
Specification.theorem_cmd true
|
||
Thm.theoremK NONE (K I)
|
||
Binding.empty_atts [] []
|
||
(Element.Shows [(lemma_name_bdg,[(goals_to_prove, attrs')])])
|
||
true (* disp ??? *)
|
||
end
|
||
|
||
fun lemma1' lemma_name goals_to_prove a b lthy =
|
||
let fun gen_attribute_token simp lthy =
|
||
List.map (fn s => Attrib.check_src lthy [Token.make_string (s, Position.none)])
|
||
(if simp then ["simp", "code_unfold"] else [])
|
||
val lemma_name_bdg =(Binding.make (lemma_name, @{here}), gen_attribute_token true lthy)
|
||
in lthy |> #2 o Specification.theorems Thm.theoremK a b true end
|
||
\<close>
|
||
|
||
|
||
chapter*[frontend::technical]\<open>Front-End \<close>
|
||
text\<open>In the following chapter, we turn to the right part of the system architecture
|
||
shown in \<^figure>\<open>architecture\<close>:
|
||
The PIDE ("Prover-IDE") layer @{cite "DBLP:conf/itp/Wenzel14"}
|
||
consisting of a part written in SML and another in SCALA.
|
||
Roughly speaking, PIDE implements "continuous build - continuous check" - functionality
|
||
over a textual, albeit generic document model. It transforms user modifications
|
||
of text elements in an instance of this model into increments (edits) and communicates
|
||
them to the Isabelle system. The latter reacts by the creation of a multitude of light-weight
|
||
reevaluation threads resulting in an asynchronous stream of markup that is used to annotate text
|
||
elements. Such markup is used to highlight, e.g., variables
|
||
or keywords with specific colors, to hyper-linking bound variables to their defining occurrences,
|
||
or to annotate type-information to terms which becomes displayed by specific
|
||
user-gestures on demand (hovering), etc.
|
||
Note that PIDE is not an editor, it is the framework that
|
||
coordinates these asynchronous information streams and optimizes it to a certain
|
||
extent (outdated markup referring to modified text is dropped, and
|
||
corresponding re-calculations are oriented to the user focus, for example).
|
||
Four concrete editors --- also called PIDE applications --- have been implemented:
|
||
|
||
\<^enum> an Eclipse plugin (developped by an Edinburg-group, based on an very old PIDE version),
|
||
\<^enum> a Visual-Studio Code plugin (developed by Makarius Wenzel),
|
||
currently based on a fairly old PIDE version,
|
||
\<^enum> clide, a web-client supporting javascript and HTML5
|
||
(developed by a group at University Bremen, based on a very old PIDE version), and
|
||
\<^enum> the most commonly used: the plugin in JEdit - Editor,
|
||
(developed by Makarius Wenzel, current PIDE version.)\<close>
|
||
|
||
text\<open>The document model forsees a number of text files, which are organized in form of an
|
||
acyclic graph. Such graphs can be grouped into \<^emph>\<open>sessions\<close> and "frozen" to binaries in order
|
||
to avoid long compilation times. Text files have an abstract name serving as identity (the
|
||
mapping to file-paths in an underlying file-system is done in an own build management).
|
||
The primary format of the text files is \<^verbatim>\<open>.thy\<close> (historically for: theory),
|
||
secondary formats can be \<^verbatim>\<open>.sty\<close>,\<^verbatim>\<open>.tex\<close>, \<^verbatim>\<open>.png\<close>, \<^verbatim>\<open>.pdf\<close>, or other files processed
|
||
by Isabelle and listed in a configuration processed by the build system.\<close>
|
||
|
||
figure*[fig3::figure, relative_width="100",src="''figures/document-model''"]
|
||
\<open>A Theory-Graph in the Document Model\<close>
|
||
|
||
text\<open>A \<^verbatim>\<open>.thy\<close> file consists of a \<^emph>\<open>header\<close>, a \<^emph>\<open>context-definition\<close> and
|
||
a \<^emph>\<open>body\<close> consisting of a sequence of \<^emph>\<open>commands\<close>. Even the header consists of
|
||
a sequence of commands used for introductory text elements not depending on any context
|
||
information (so: practically excluding any form of text antiquotation (see above)).
|
||
The context-definition contains an \<^emph>\<open>import\<close> and a \<^emph>\<open>keyword\<close> section;
|
||
for example:
|
||
@{theory_text [display] \<open>
|
||
theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||
imports Main
|
||
RegExpInterface (* Interface to functional regular automata for monitoring *)
|
||
Assert
|
||
|
||
keywords "+=" ":=" "accepts" "rejects"
|
||
\<close>}
|
||
where \<^verbatim>\<open>Isa_DOF\<close> is the abstract name of the text-file, \<^verbatim>\<open>Main\<close> etc. refer to imported
|
||
text files (recall that the import relation must be acyclic). \<^emph>\<open>keyword\<close>s are used to separate
|
||
commands form each other;
|
||
predefined commands allow for the dynamic creation of new commands similarly
|
||
to the definition of new functions in an interpreter shell (or: toplevel, see above.).
|
||
A command starts with a pre-declared keyword and specific syntax of this command;
|
||
the declaration of a keyword is only allowed in the same \<^verbatim>\<open>.thy\<close>-file where
|
||
the corresponding new command is defined. The semantics of the command is expressed
|
||
in ML and consists of a @{ML_type "Toplevel.transition -> Toplevel.transition"}
|
||
function. Thus, the Isar-toplevel supports the generic document model
|
||
and allows for user-programmed extensions.\<close>
|
||
|
||
text\<open>In the traditional literature, Isabelle \<^verbatim>\<open>.thy\<close>-files
|
||
were said to be processed by two types of parsers:
|
||
\<^enum> the "outer-syntax" (i.e. the syntax for commands) is processed
|
||
by a lexer-library and parser combinators built on top, and
|
||
\<^enum> the "inner-syntax" (i.e. the syntax for @{term \<open>\<Lambda>\<close>}-terms)
|
||
with an evolved, eight-layer parsing and pretty-printing process
|
||
based on an Earley-algorithm.
|
||
\<close>
|
||
|
||
text\<open>This picture is less and less true for a number of reasons:
|
||
\<^enum> With the advent of \<open>\<open> ... \<close>\<close>, a mechanism for
|
||
\<^emph>\<open>cascade-syntax\<close> came to the Isabelle platform that introduces a flexible means
|
||
to change parsing contexts \<^emph>\<open>and\<close> parsing technologies.
|
||
\<^enum> Inside the term-parser levels, the concept of \<^emph>\<open>cartouche\<close> can be used
|
||
to escape the parser and its underlying parsing technology.
|
||
\<^enum> Outside, in the traditional toplevel-parsers, the
|
||
\<open>\<open> ... \<close>\<close> is becoming more and more enforced
|
||
(some years ago, syntax like \<open>term{* ... *}\<close> was replaced by
|
||
syntax \<open>term\<open> ... \<close>\<close>. This makes technical support of cascade syntax
|
||
more and more easy.
|
||
\<^enum> The Lexer infra-structure is already rather generic; nothing prevents to
|
||
add beside the lexer - configurations for ML-Parsers, Toplevel Command Syntax
|
||
parsers, mathematical notation parsers for $\lambda$-terms new pillars
|
||
of parsing technologies, say, for parsing C or Rust or JavaScript inside
|
||
Isabelle.
|
||
\<close>
|
||
|
||
|
||
section\<open>Basics: string, bstring and xstring\<close>
|
||
text\<open>\<^ML_type>\<open>string\<close> is the basic library type from the SML library
|
||
in structure \<^ML_structure>\<open>String\<close>. Many Isabelle operations produce
|
||
or require formats thereof introduced as type synonyms
|
||
\<^ML_type>\<open>bstring\<close> (defined in structure \<^ML_structure>\<open>Binding\<close>)
|
||
and \<^ML_type>\<open>xstring\<close> (defined in structure \<^ML_structure>\<open>Name_Space\<close>).
|
||
Unfortunately, the abstraction is not tight and combinations with
|
||
elementary routines might produce quite crappy results.\<close>
|
||
|
||
ML\<open>val b = Binding.name_of @{binding \<open>here\<close>}\<close>
|
||
text\<open>... produces the system output \<^verbatim>\<open>val it = "here": bstring\<close>,
|
||
but note that it is misleading to believe it is just a string.\<close>
|
||
|
||
ML\<open>String.explode b\<close> (* is harmless, but *)
|
||
ML\<open>String.explode(Binding.name_of
|
||
(Binding.conglomerate[Binding.qualified_name "X.x", @{binding "here"}] ))\<close>
|
||
text\<open>... which leads to the output \<^verbatim>\<open>val it = [#"x", #"_", #"h", #"e", #"r", #"e"]: char list\<close>\<close>
|
||
|
||
text\<open> However, there is an own XML parser for this format. See Section Markup. \<close>
|
||
|
||
ML\<open> fun dark_matter x = XML.content_of (YXML.parse_body x)\<close>
|
||
|
||
(* MORE TO COME *)
|
||
|
||
section\<open>Positions\<close>
|
||
text\<open>A basic data-structure relevant for PIDE are \<^emph>\<open>positions\<close>; beyond the usual line- and column
|
||
information they can represent ranges, list of ranges, and the name of the atomic sub-document
|
||
in which they are contained. In the command:\<close>
|
||
ML\<open>
|
||
val pos = @{here};
|
||
val markup = Position.here pos;
|
||
writeln ("And a link to the declaration of 'here' is "^markup)\<close>
|
||
|
||
(* \<^here> *)
|
||
text\<open> ... uses the antiquotation @{ML "@{here}"} to infer from the system lexer the actual position
|
||
of itself in the global document, converts it to markup (a string-representation of it) and sends
|
||
it via the usual @{ML "writeln"} to the interface. \<close>
|
||
|
||
figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"]
|
||
\<open>Output with hyperlinked position.\<close>
|
||
|
||
text\<open>@{figure \<open>hyplinkout\<close>} shows the produced output where the little house-like symbol in the
|
||
display is hyperlinked to the position of @{ML "@{here}"} in the ML sample above.\<close>
|
||
|
||
section\<open>Markup and Low-level Markup Reporting\<close>
|
||
text\<open>The structures @{ML_structure Markup} and @{ML_structure Properties} represent the basic
|
||
annotation data which is part of the protocol sent from Isabelle to the front-end.
|
||
They are qualified as "quasi-abstract", which means they are intended to be an abstraction of
|
||
the serialized, textual presentation of the protocol. Markups are structurally a pair of a key
|
||
and properties; @{ML_structure Markup} provides a number of such \<^emph>\<open>key\<close>s for annotation classes
|
||
such as "constant", "fixed", "cartouche", some of them quite obscure. Here is a code sample
|
||
from \<^theory_text>\<open>Isabelle_DOF\<close>. A markup must be tagged with an id; this is done by the @{ML serial}-function
|
||
discussed earlier. Markup operations were used for hyperlinking applications to binding
|
||
occurrences, info for hovering, infos for type ... \<close>
|
||
|
||
ML\<open>
|
||
(* Position.report is also a type consisting of a pair of a position and markup. *)
|
||
(* It would solve all my problems if I find a way to infer the defining Position.report
|
||
from a type definition occurence ... *)
|
||
|
||
Position.report: Position.T -> Markup.T -> unit;
|
||
Position.reports: Position.report list -> unit;
|
||
(* ? ? ? I think this is the magic thing that sends reports to the GUI. *)
|
||
Markup.entity : string -> string -> Markup.T;
|
||
Markup.properties : Properties.T -> Markup.T -> Markup.T ;
|
||
Properties.get : Properties.T -> string -> string option;
|
||
Markup.enclose : Markup.T -> string -> string;
|
||
|
||
(* example for setting a link, the def flag controls if it is a defining or a binding
|
||
occurence of an item *)
|
||
Markup.theoryN : string;
|
||
|
||
fun theory_markup refN (def:bool) (name:string) (id:serial) (pos:Position.T) =
|
||
if id = 0 then Markup.empty
|
||
else Position.make_entity_markup {def = def} id refN (name, pos);
|
||
|
||
serial(); (* A global, lock-guarded serial counter used to produce unique identifiers,
|
||
be it on the level of thy-internal states or as reference in markup in
|
||
PIDE *)
|
||
\<close>
|
||
|
||
|
||
subsection\<open>A simple Example\<close>
|
||
ML\<open>
|
||
local
|
||
|
||
val docclassN = "doc_class";
|
||
|
||
(* derived from: theory_markup; def for "defining occurrence" (true) in contrast to
|
||
"referring occurence" (false). *)
|
||
val docclass_markup = theory_markup docclassN
|
||
|
||
in
|
||
|
||
fun report_defining_occurrence pos cid =
|
||
let val id = serial ()
|
||
val markup_of_cid = docclass_markup true cid id pos
|
||
in Position.report pos markup_of_cid end;
|
||
|
||
end
|
||
\<close>
|
||
|
||
text\<open>The @\<open>ML report_defining_occurrence\<close>-function above takes a position and a "cid" parsed
|
||
in the Front-End, converts this into markup together with a unique number identifying this
|
||
markup, and sends this as a report to the Front-End. \<close>
|
||
|
||
|
||
subsection\<open>A Slightly more Complex Example\<close>
|
||
text\<open>Note that this example is only animated in the integrated source of this document;
|
||
it is essential that is executed inside Isabelle/jEdit. \<close>
|
||
ML \<open>
|
||
|
||
fun markup_tvar def_name ps (name, id) =
|
||
let
|
||
fun markup_elem name = (name, (name, []): Markup.T);
|
||
val (tvarN, tvar) = markup_elem ((case def_name of SOME name => name | _ => "") ^ "'s nickname is");
|
||
val entity = Markup.entity tvarN name (* ??? *)
|
||
val def = def_name = NONE
|
||
in
|
||
tvar ::
|
||
(if def then I else cons (Markup.keyword_properties Markup.ML_keyword3))
|
||
(map (fn pos => Position.make_entity_markup {def = def} id tvarN (name, pos) ) ps)
|
||
end
|
||
|
||
(* Position.make_entity_markup {def = def} id refN (name, pos) *)
|
||
|
||
fun report [] _ _ = I
|
||
| report ps markup x =
|
||
let val ms = markup x
|
||
in fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps end
|
||
\<close>
|
||
|
||
ML \<open>
|
||
local
|
||
val data = \<comment> \<open>Derived from Yakoub's example ;-)\<close>
|
||
|
||
[ (\<open>Frédéric 1er\<close>, \<open>King of Naples\<close>)
|
||
, (\<open>Frédéric II\<close>, \<open>King of Sicily\<close>)
|
||
, (\<open>Frédéric III\<close>, \<open>the Handsome\<close>)
|
||
, (\<open>Frédéric IV\<close>, \<open>of the Empty Pockets\<close>)
|
||
, (\<open>Frédéric V\<close>, \<open>King of Denmark–Norway\<close>)
|
||
, (\<open>Frédéric VI\<close>, \<open>the Knight\<close>)
|
||
, (\<open>Frédéric VII\<close>, \<open>Count of Toggenburg\<close>)
|
||
, (\<open>Frédéric VIII\<close>, \<open>Count of Zollern\<close>)
|
||
, (\<open>Frédéric IX\<close>, \<open>the Old\<close>)
|
||
, (\<open>Frédéric X\<close>, \<open>the Younger\<close>) ]
|
||
|
||
val (tab0, markup) =
|
||
fold_map (fn (name, msg) => fn reports =>
|
||
let val id = serial ()
|
||
val pos = [Input.pos_of name]
|
||
in
|
||
( (fst(Input.source_content msg), (name, pos, id))
|
||
, report pos (markup_tvar NONE pos) (fst(Input.source_content name), id) reports)
|
||
end)
|
||
data
|
||
[]
|
||
|
||
val () = Position.reports_text markup
|
||
in
|
||
val tab = Symtab.make tab0
|
||
end
|
||
\<close>
|
||
|
||
ML \<open>
|
||
val _ =
|
||
fold (fn input =>
|
||
let
|
||
val pos1' = Input.pos_of input
|
||
fun ctnt name0 = fst(Input.source_content name0)
|
||
val pos1 = [pos1']
|
||
val msg1 = fst(Input.source_content input)
|
||
val msg2 = "No persons were found to have such nickname"
|
||
in
|
||
case Symtab.lookup tab (fst(Input.source_content input)) of
|
||
NONE => tap (fn _ => Output.information (msg2 ^ Position.here_list pos1))
|
||
(cons ((pos1', Markup.bad ()), ""))
|
||
| SOME (name0, pos0, id) => report pos1 (markup_tvar (SOME (ctnt name0)) pos0) (msg1, id)
|
||
end)
|
||
[ \<open>the Knight\<close> \<comment> \<open>Example of a correct retrieval (CTRL + Hovering shows what we are expecting)\<close>
|
||
, \<open>the Handsome\<close> \<comment> \<open>Example of a correct retrieval (CTRL + Hovering shows what we are expecting)\<close>
|
||
, \<open>the Spy\<close> \<comment> \<open>Example of a failure to retrieve the person in \<^ML>\<open>tab\<close>\<close>
|
||
]
|
||
[]
|
||
|> Position.reports_text
|
||
\<close>
|
||
|
||
text\<open>The pudding comes with the eating: \<close>
|
||
|
||
subsection\<open>Environment Structured Reporting\<close>
|
||
|
||
text\<open> The structure \<^ML_structure>\<open>Name_Space\<close> offers an own infra-structure for names and
|
||
manages the markup accordingly. MORE TO COME\<close>
|
||
text\<open> \<^ML_type>\<open>'a Name_Space.table\<close> \<close>
|
||
|
||
|
||
section\<open>The System Lexer and Token Issues\<close>
|
||
text\<open>Four syntactic contexts are predefined in Isabelle (others can be added):
|
||
the ML context, the text context, the Isar-command context and the term-context, referring
|
||
to different needs of the Isabelle Framework as an extensible framework supporting incremental,
|
||
partially programmable extensions and as a Framework geared towards Formal Proofs and therefore
|
||
mathematical notations. The basic data-structure for the lexical treatment of these elements
|
||
are \<^ML_structure>\<open>Token\<close>'s. \<close>
|
||
|
||
subsection\<open>Tokens\<close>
|
||
|
||
text\<open>The basic entity that lexers treat are \<^emph>\<open>tokens\<close>. defined in \<^ML_structure>\<open>Token\<close>
|
||
It provides a classification infrastructure, the references to positions and Markup
|
||
as well as way's to annotate tokens with (some) values they denote:\<close>
|
||
|
||
|
||
ML\<open>
|
||
local
|
||
open Token
|
||
|
||
type dummy = Token.T
|
||
type src = Token.T list
|
||
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
|
||
|
||
type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring}
|
||
|
||
|
||
val _ = Token.is_command : Token.T -> bool;
|
||
val _ = Token.content_of : Token.T -> string; (* textueller kern eines Tokens. *)
|
||
|
||
|
||
val _ = pos_of: T -> Position.T
|
||
|
||
(*
|
||
datatype kind =
|
||
(*immediate source*)
|
||
Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
|
||
Float | Space |
|
||
(*delimited content*)
|
||
String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option |
|
||
(*special content*)
|
||
Error of string | EOF
|
||
|
||
datatype value =
|
||
Source of src |
|
||
Literal of bool * Markup.T |
|
||
Name of name_value * morphism |
|
||
Typ of typ |
|
||
Term of term |
|
||
Fact of string option * thm list |
|
||
Attribute of morphism -> attribute |
|
||
Declaration of declaration |
|
||
Files of file Exn.result list
|
||
|
||
|
||
*)
|
||
in val _ = ()
|
||
end
|
||
\<close>
|
||
|
||
|
||
|
||
subsection\<open>A Lexer Configuration Example\<close>
|
||
|
||
ML\<open>
|
||
(* MORE TO COME *)
|
||
\<close>
|
||
|
||
|
||
section\<open> Combinator Parsing \<close>
|
||
text\<open>Parsing Combinators go back to monadic programming as advocated by Wadler et. al, and has been
|
||
worked out @{cite "DBLP:journals/jfp/Hutton92"}. Parsing combinators are one of the two
|
||
major parsing technologies of the Isabelle front-end, in particular for the outer-syntax used
|
||
for the parsing of toplevel-commands. The core of the combinator library is
|
||
\<^ML_structure>\<open>Scan\<close> providing the \<^ML_type>\<open>'a parser\<close> which is a synonym for
|
||
\<^ML_type>\<open>Token.T list -> 'a * Token.T list\<close>.
|
||
|
||
"parsers" are actually interpreters; an \<^ML_type>\<open>'a parser\<close> is a function that parses
|
||
an input stream and computes (=evaluates) it into \<open>'a\<close>.
|
||
|
||
\<^item> \<^theory_text>\<open>type 'a parser = Token.T list -> 'a * Token.T list\<close>
|
||
\<^item> \<^theory_text>\<open> type 'a context_parser = Context.generic * Token.T list ->
|
||
'a * (Context.generic * Token.T list)\<close>
|
||
|
||
Since the semantics of an Isabelle command is a \<^ML_type>\<open>Toplevel.transition -> Toplevel.transition \<close>
|
||
or theory \<^ML_type>\<open>theory -> theory\<close> function, i.e. a global system transition,
|
||
"parsers" of that type can be constructed and be bound as call-back functions
|
||
to a table in the Toplevel-structure of Isar.
|
||
|
||
The library also provides a bunch of infix parsing combinators, notably:
|
||
|
||
\<^item> \<^ML>\<open>op !! : ('a * message option -> message) -> ('a -> 'b) -> 'a -> 'b\<close>
|
||
(*apply function*)
|
||
\<^item> \<^ML>\<open>op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c\<close>
|
||
(*alternative*)
|
||
\<^item> \<^ML>\<open> op || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b\<close>
|
||
(*sequential pairing*)
|
||
\<^item> \<^ML>\<open>op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e\<close>
|
||
(*dependent pairing*)
|
||
\<^item> \<^ML>\<open> op :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e\<close>
|
||
(*projections*)
|
||
\<^item> \<^ML>\<open>op :|-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> 'd * 'e\<close>
|
||
\<^item> \<^ML>\<open>op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e\<close>
|
||
concatenate and forget first parse result
|
||
\<^item> \<^ML>\<open>op --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e\<close>
|
||
concatenate and forget second parse result
|
||
\<^item> \<^ML>\<open>op ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c\<close>
|
||
\<^item> \<^ML>\<open>op ::: : ('a -> 'b * 'c) * ('c -> 'b list * 'd) -> 'a -> 'b list * 'd\<close>
|
||
\<^item> \<^ML>\<open>op @@@ : ('a -> 'b list * 'c) * ('c -> 'b list * 'd) -> 'a -> 'b list * 'd\<close>
|
||
parse one element literal
|
||
\<^item> \<^ML>\<open>op $$ : string -> string list -> string * string list\<close>
|
||
\<^item> \<^ML>\<open>op ~$$ : string -> string list -> string * string list\<close>
|
||
\<close>
|
||
|
||
|
||
subsection\<open>Examples and Useful Glue\<close>
|
||
ML\<open>
|
||
|
||
(* conversion between these two : *)
|
||
|
||
fun parser2contextparser pars (ctxt, toks) = let val (a, toks') = pars toks
|
||
in (a,(ctxt, toks')) end;
|
||
val _ = parser2contextparser : 'a parser -> 'a context_parser;
|
||
|
||
(* bah, it's the same as Scan.lift *)
|
||
val _ = Scan.lift Args.cartouche_input : Input.source context_parser;\<close>
|
||
|
||
subsection\<open>Advanced Parser Library\<close>
|
||
|
||
text\<open>There are two parts. A general multi-purpose parsing combinator library is
|
||
found under @{ML_structure "Parse"}, providing basic functionality for parsing strings
|
||
or integers. There is also an important combinator that reads the current position information
|
||
out of the input stream:
|
||
|
||
\<^item> \<^ML>\<open>Parse.nat: int parser\<close>
|
||
\<^item> \<^ML>\<open>Parse.int: int parser\<close>
|
||
\<^item> \<^ML>\<open>Parse.enum_positions: string -> 'a parser -> ('a list * Position.T list) parser\<close>
|
||
\<^item> \<^ML>\<open>Parse.enum : string -> 'a parser -> 'a list parser\<close>
|
||
\<^item> \<^ML>\<open>Parse.input: 'a parser -> Input.source parser\<close>
|
||
|
||
\<^item> \<^ML>\<open>Parse.enum': string -> 'a context_parser -> 'a list context_parser\<close>
|
||
\<^item> \<^ML>\<open>Parse.!!! : (Token.T list -> 'a) -> Token.T list -> 'a\<close>
|
||
\<^item> \<^ML>\<open>Parse.position: 'a parser -> ('a * Position.T) parser\<close>
|
||
|
||
\<^item> \<^ML>\<open>Parse.position Args.cartouche_input\<close>
|
||
\<close>
|
||
|
||
text\<open>The second part is much more high-level, and can be found under \<^ML_structure>\<open>Args\<close>.
|
||
In parts, these combinators are again based on more low-level combinators, in parts they serve as
|
||
an interface to the underlying Earley-parser for mathematical notation used in types and terms.
|
||
This is perhaps meant with the fairly cryptic comment:
|
||
"Quasi-inner syntax based on outer tokens: concrete argument syntax of
|
||
attributes, methods etc." at the beginning of this structure.\<close>
|
||
|
||
text\<open> Some more combinators
|
||
\<^item>\<^ML>\<open>Args.symbolic : Token.T parser\<close>
|
||
\<^item>\<^ML>\<open>Args.$$$ : string -> string parser\<close>
|
||
\<^item>\<^ML>\<open>Args.maybe : 'a parser -> 'a option parser\<close>
|
||
\<^item>\<^ML>\<open>Args.name_token: Token.T parser\<close>
|
||
|
||
Common Isar Syntax
|
||
\<^item>\<^ML>\<open>Args.colon: string parser\<close>
|
||
\<^item>\<^ML>\<open>Args.query: string parser\<close>
|
||
\<^item>\<^ML>\<open>Args.bang: string parser\<close>
|
||
\<^item>\<^ML>\<open>Args.query_colon: string parser\<close>
|
||
\<^item>\<^ML>\<open>Args.bang_colon: string parser\<close>
|
||
\<^item>\<^ML>\<open>Args.parens: 'a parser -> 'a parser\<close>
|
||
\<^item>\<^ML>\<open>Args.bracks: 'a parser -> 'a parser\<close>
|
||
\<^item>\<^ML>\<open>Args.mode: string -> bool parser\<close>
|
||
\<^item>\<^ML>\<open>Args.name: string parser\<close>
|
||
\<^item>\<^ML>\<open>Args.name_position: (string * Position.T) parser\<close>
|
||
\<^item>\<^ML>\<open>Args.cartouche_inner_syntax: string parser\<close>
|
||
\<^item>\<^ML>\<open>Args.cartouche_input: Input.source parser\<close>
|
||
\<^item>\<^ML>\<open>Args.text_token: Token.T parser \<close>
|
||
|
||
|
||
Common Isar Syntax
|
||
\<^item>\<^ML>\<open>Args.text_input: Input.source parser\<close>
|
||
\<^item>\<^ML>\<open>Args.text : string parser\<close>
|
||
\<^item>\<^ML>\<open>Args.binding : Binding.binding parser\<close>
|
||
|
||
Common Stuff related to Inner Syntax Parsing
|
||
\<^item>\<^ML>\<open>Args.alt_name: string parser\<close>
|
||
\<^item>\<^ML>\<open>Args.liberal_name : string parser\<close>
|
||
\<^item>\<^ML>\<open>Args.var: indexname parser\<close>
|
||
\<^item>\<^ML>\<open>Args.internal_source: Token.src parser\<close>
|
||
\<^item>\<^ML>\<open>Args.internal_name: Token.name_value parser\<close>
|
||
\<^item>\<^ML>\<open>Args.internal_typ : typ parser\<close>
|
||
\<^item>\<^ML>\<open>Args.internal_term: term parser\<close>
|
||
\<^item>\<^ML>\<open>Args.internal_fact: thm list parser\<close>
|
||
\<^item>\<^ML>\<open>Args.internal_attribute: (morphism -> attribute) parser\<close>
|
||
\<^item>\<^ML>\<open>Args.internal_declaration: declaration parser\<close>
|
||
\<^item>\<^ML>\<open>Args.alt_name : string parser\<close>
|
||
\<^item>\<^ML>\<open>Args.liberal_name: string parser\<close>
|
||
|
||
|
||
|
||
Common Isar Syntax
|
||
\<^item>\<^ML>\<open>Args.named_source: (Token.T -> Token.src) -> Token.src parser\<close>
|
||
\<^item>\<^ML>\<open>Args.named_typ : (string -> typ) -> typ parser\<close>
|
||
\<^item>\<^ML>\<open>Args.named_term : (string -> term) -> term parser\<close>
|
||
\<^item>\<^ML>\<open>Args.text_declaration: (Input.source -> declaration) -> declaration parser\<close>
|
||
\<^item>\<^ML>\<open>Args.cartouche_declaration: (Input.source -> declaration) -> declaration parser\<close>
|
||
\<^item>\<^ML>\<open>Args.typ_abbrev : typ context_parser\<close>
|
||
\<^item>\<^ML>\<open>Args.typ: typ context_parser\<close>
|
||
\<^item>\<^ML>\<open>Args.term: term context_parser\<close>
|
||
\<^item>\<^ML>\<open>Args.term_pattern: term context_parser\<close>
|
||
\<^item>\<^ML>\<open>Args.term_abbrev : term context_parser \<close>
|
||
\<^item>\<^ML>\<open>Args.named_source: (Token.T -> Token.src) -> Token.src parser\<close>
|
||
\<^item>\<^ML>\<open>Args.named_typ : (string -> typ) -> typ parser\<close>
|
||
\<^item>\<^ML>\<open>Args.named_term: (string -> term) -> term parser\<close>
|
||
\<^item>\<^ML>\<open>Args.text_declaration: (Input.source -> declaration) -> declaration parser\<close>
|
||
\<^item>\<^ML>\<open>Args.cartouche_declaration: (Input.source -> declaration) -> declaration parser\<close>
|
||
|
||
Syntax for some major Pure commands in Isar
|
||
\<^item>\<^ML>\<open>Args.prop: term context_parser\<close>
|
||
\<^item>\<^ML>\<open>Args.type_name: {proper: bool, strict: bool} -> string context_parser\<close>
|
||
\<^item>\<^ML>\<open>Args.const: {proper: bool, strict: bool} -> string context_parser\<close>
|
||
\<^item>\<^ML>\<open>Args.goal_spec: ((int -> tactic) -> tactic) context_parser\<close>
|
||
\<^item>\<^ML>\<open>Args.context: Proof.context context_parser\<close>
|
||
\<^item>\<^ML>\<open>Args.theory: theory context_parser\<close>
|
||
|
||
\<close>
|
||
|
||
|
||
|
||
subsection\<open> Bindings \<close>
|
||
|
||
text\<open> The structure \<^ML_structure>\<open>Binding\<close> serves as
|
||
\<open>structured name bindings\<close>, as says the description, i.e. a mechanism to basically
|
||
associate an input string-fragment to its position. This concept is vital in all parsing processes
|
||
and the interaction with PIDE.
|
||
|
||
Key are two things:
|
||
\<^enum> the type-synonym \<^ML_type>\<open>bstring\<close> which is synonym to \<^ML_type>\<open>string\<close>
|
||
and intended for "primitive names to be bound"
|
||
\<^enum> the projection \<^ML>\<open>Binding.pos_of : Binding.binding -> Position.T\<close>
|
||
\<^enum> the constructor establishing a binding \<^ML>\<open>Binding.make: bstring * Position.T -> Binding.binding\<close>
|
||
|
||
\<close>
|
||
|
||
|
||
subsubsection\<open> Example \<close>
|
||
|
||
text\<open>Since this is so common in interface programming, there are a number of antiquotations\<close>
|
||
ML\<open>
|
||
val H = @{binding here}; (* There are "bindings" consisting of a text-span and a position,
|
||
where "positions" are absolute references to a file *)
|
||
|
||
Binding.pos_of H; (* clicking on "H" activates the hyperlink to the defining occ of "H" above *)
|
||
(* {offset=23, end_offset=27, id=-17214}: Position.T *)
|
||
|
||
(* a modern way to construct a binding is by the following code antiquotation : *)
|
||
\<^binding>\<open>theory\<close>
|
||
|
||
\<close>
|
||
|
||
subsection \<open>Input streams. \<close>
|
||
text\<open>Reads as : Generic input with position and range information, to be processed in a
|
||
left-to right manner. Preferable to strings if used for larger data.
|
||
|
||
Constructor: \<^ML>\<open>Input.source_explode : Input.source -> Symbol_Pos.T list\<close>
|
||
|
||
\<close>
|
||
|
||
subsubsection \<open>Example :Input streams. \<close>
|
||
|
||
ML\<open> Input.source_explode (Input.string " f @{thm refl}");
|
||
|
||
(* If stemming from the input window, this can be something like:
|
||
|
||
[(" ", {offset=14, id=-2769}), ("f", {offset=15, id=-2769}), (" ", {offset=16, id=-2769}),
|
||
("@", {offset=17, id=-2769}), ("{", {offset=18, id=-2769}), ("t", {offset=19, id=-2769}),
|
||
("h", {offset=20, id=-2769}), ("m", {offset=21, id=-2769}), (" ", {offset=22, id=-2769}),
|
||
("r", {offset=23, id=-2769}), ("e", {offset=24, id=-2769}), ("f", {offset=25, id=-2769}),
|
||
("l", {offset=26, id=-2769}), ("}", {offset=27, id=-2769})]
|
||
*)
|
||
|
||
\<close>
|
||
|
||
|
||
section\<open>Term Parsing\<close>
|
||
|
||
text\<open>The heart of the parsers for mathematical notation, based on an Earley-parser that can cope
|
||
with incremental changes of the grammar as required for sophisticated mathematical output, is hidden
|
||
behind the API described in this section.\<close>
|
||
|
||
text\<open> Note that the naming underlies the following convention.
|
||
There are:
|
||
\<^enum> "parser"s
|
||
\<^enum> type-"checker"s, which usually also englobe the markup generation for PIDE
|
||
\<^enum> "reader"s which do both together with pretty-printing
|
||
|
||
This is encapsulated in the data structure @{ML_structure Syntax} ---
|
||
the table with const symbols, print and ast translations, ... The latter is accessible, e.g.
|
||
from a Proof context via @{ML Proof_Context.syn_of}.
|
||
\<close>
|
||
|
||
text\<open> Inner Syntax Parsing combinators for elementary Isabelle Lexems\<close>
|
||
text\<open>
|
||
\<^item> \<^ML>\<open> Syntax.parse_sort : Proof.context -> string -> sort\<close>
|
||
\<^item> \<^ML>\<open> Syntax.parse_typ : Proof.context -> string -> typ\<close>
|
||
\<^item> \<^ML>\<open> Syntax.parse_term : Proof.context -> string -> term\<close>
|
||
\<^item> \<^ML>\<open> Syntax.parse_prop : Proof.context -> string -> term\<close>
|
||
\<^item> \<^ML>\<open> Syntax.check_term : Proof.context -> term -> term\<close>
|
||
\<^item> \<^ML>\<open> Syntax.check_props: Proof.context -> term list -> term list\<close>
|
||
\<^item> \<^ML>\<open> Syntax.uncheck_sort: Proof.context -> sort -> sort\<close>
|
||
\<^item> \<^ML>\<open> Syntax.uncheck_typs: Proof.context -> typ list -> typ list\<close>
|
||
\<^item> \<^ML>\<open> Syntax.uncheck_terms: Proof.context -> term list -> term list\<close>
|
||
\<close>
|
||
|
||
text\<open>In contrast to mere parsing, the following operators provide also type-checking
|
||
and internal reporting to PIDE --- see below. I did not find a mechanism to address
|
||
the internal serial-numbers used for the PIDE protocol, however, rumours have it
|
||
that such a thing exists. The variants \<^verbatim>\<open>_global\<close> work on theories instead on
|
||
\<^ML_type>\<open>Proof.context\<close>s.\<close>
|
||
|
||
text\<open>
|
||
\<^item> \<^ML>\<open>Syntax.read_sort: Proof.context -> string -> sort\<close>
|
||
\<^item> \<^ML>\<open>Syntax.read_typ : Proof.context -> string -> typ\<close>
|
||
\<^item> \<^ML>\<open>Syntax.read_term: Proof.context -> string -> term\<close>
|
||
\<^item> \<^ML>\<open>Syntax.read_typs: Proof.context -> string list -> typ list\<close>
|
||
\<^item> \<^ML>\<open>Syntax.read_sort_global: theory -> string -> sort\<close>
|
||
\<^item> \<^ML>\<open>Syntax.read_typ_global: theory -> string -> typ\<close>
|
||
\<^item> \<^ML>\<open>Syntax.read_term_global: theory -> string -> term\<close>
|
||
\<^item> \<^ML>\<open>Syntax.read_prop_global: theory -> string -> term\<close>
|
||
\<close>
|
||
text \<open>The following operations are concerned with the conversion of pretty-prints
|
||
and, from there, the generation of (non-layouted) strings :
|
||
|
||
\<^item> \<^ML>\<open>Syntax.pretty_term:Proof.context -> term -> Pretty.T\<close>
|
||
\<^item> \<^ML>\<open>Syntax.pretty_typ:Proof.context -> typ -> Pretty.T \<close>
|
||
\<^item> \<^ML>\<open>Syntax.pretty_sort:Proof.context -> sort -> Pretty.T \<close>
|
||
\<^item> \<^ML>\<open>Syntax.pretty_classrel: Proof.context -> class list -> Pretty.T\<close>
|
||
\<^item> \<^ML>\<open>Syntax.pretty_arity: Proof.context -> arity -> Pretty.T\<close>
|
||
\<^item> \<^ML>\<open>Syntax.string_of_term: Proof.context -> term -> string \<close>
|
||
\<^item> \<^ML>\<open>Syntax.string_of_typ: Proof.context -> typ -> string \<close>
|
||
\<^item> \<^ML>\<open>Syntax.lookup_const : Syntax.syntax -> string -> string option\<close>
|
||
\<close>
|
||
|
||
|
||
|
||
|
||
|
||
|
||
text\<open>
|
||
Note that \<^ML>\<open>Syntax.install_operations\<close> is a late-binding interface, i.e. a collection of
|
||
"hooks" used to resolve an apparent architectural cycle.
|
||
The real work is done in \<^file>\<open>~~/src/Pure/Syntax/syntax_phases.ML\<close>
|
||
|
||
Even the parsers and type checkers stemming from the theory-structure are registered via
|
||
hooks (this can be confusing at times). Main phases of inner syntax processing, with standard
|
||
implementations of parse/unparse operations were treated this way.
|
||
At the very very end in, it sets up the entire syntax engine (the hooks) via:
|
||
|
||
\<^theory_text>\<open>Theory.setup
|
||
(Syntax.install_operations
|
||
{parse_sort = parse_sort,
|
||
parse_typ = parse_typ,
|
||
parse_term = parse_term false,
|
||
parse_prop = parse_term true,
|
||
unparse_sort = unparse_sort,
|
||
unparse_typ = unparse_typ,
|
||
unparse_term = unparse_term,
|
||
check_typs = check_typs,
|
||
check_terms = check_terms,
|
||
check_props = check_props,
|
||
uncheck_typs = uncheck_typs,
|
||
uncheck_terms = uncheck_terms})
|
||
\<close>
|
||
\<close>
|
||
|
||
|
||
|
||
(*
|
||
Document_Antiquotation
|
||
*)
|
||
|
||
subsection*[ex33::example] \<open>Example\<close>
|
||
|
||
ML\<open>
|
||
|
||
(* here follows the definition of the attribute parser : *)
|
||
val Z = let val attribute = Parse.position Parse.name --
|
||
Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
|
||
in (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) end ;
|
||
|
||
|
||
(* Here is the code to register the above parsers as text antiquotations into the Isabelle
|
||
Framework: *)
|
||
Document_Output.antiquotation_pretty_source \<^binding>\<open>theory\<close>
|
||
(Scan.lift (Parse.position Parse.embedded));
|
||
|
||
Document_Output.antiquotation_raw \<^binding>\<open>file\<close>
|
||
(Scan.lift (Parse.position Parse.path)) ;
|
||
|
||
\<close>
|
||
|
||
text\<open>where we have the registration of the action
|
||
\<^ML>\<open>Scan.lift (Parse.position Args.cartouche_input)\<close>
|
||
to be bound to the \<open>name\<close> as a whole is a system
|
||
transaction that, of course, has the type \<^ML_type>\<open>theory -> theory\<close> :
|
||
|
||
@{ML [display] \<open>
|
||
(fn name => (Document_Output.antiquotation_pretty_source
|
||
name
|
||
(Scan.lift (Parse.position Args.cartouche_input))))
|
||
: binding ->
|
||
(Proof.context -> Input.source * Position.T -> Pretty.T) ->
|
||
theory -> theory
|
||
\<close>}
|
||
\<close>
|
||
|
||
|
||
section \<open> Output: Very Low Level \<close>
|
||
text\<open> For re-directing the output channels, the structure \<^ML_structure>\<open>Output\<close> may be relevant:
|
||
\<^ML>\<open>Output.output:string -> string\<close> is the structure for the "hooks" with the target devices.
|
||
\<close>
|
||
|
||
ML\<open> Output.output "bla_1:" \<close>
|
||
|
||
text\<open>It provides a number of hooks that can be used for redirection hacks ...\<close>
|
||
|
||
section \<open> Output: LaTeX \<close>
|
||
text\<open>The heart of the LaTeX generator is to be found in the structure \<^ML_structure>\<open>Document_Output\<close>.
|
||
This is an own parsing and writing process, with the risc that a parsed file in the IDE parsing
|
||
process can not be parsed for the LaTeX Generator. The reason is twofold:
|
||
|
||
\<^enum> The LaTeX Generator makes a rough attempt to mimic the LayOut in the thy-file; thus, its
|
||
spacing is relevant.
|
||
\<^enum> there is a special bracket \<open>(*<*)\<close> ... \<open>(*>*)\<close> that allows to specify input that is checked by
|
||
Isabelle, but excluded from the LaTeX generator (this is handled in an own sub-parser
|
||
called \<^ML>\<open>Document_Source.improper\<close> where also other forms of comment parsers are provided.
|
||
|
||
Since Isabelle2018, an own AST is provided for the LaTeX syntax, analogously to
|
||
\<^ML_structure>\<open>Pretty\<close>. Key functions of this structure \<^ML_structure>\<open>Latex\<close> are:
|
||
|
||
\<^item>\<^ML>\<open>Latex.string: string -> Latex.text\<close>
|
||
\<^item>\<^ML>\<open>Latex.text: string * Position.T -> Latex.text\<close>
|
||
|
||
\<^item>\<^ML>\<open>Latex.output_name: string -> string\<close>
|
||
\<^item>\<^ML>\<open>Latex.output_ascii: string -> string\<close>
|
||
\<^item>\<^ML>\<open>Latex.output_symbols: Symbol.symbol list -> string\<close>
|
||
|
||
|
||
\<^item>\<^ML>\<open>Latex.environment: string -> Latex.text -> Latex.text\<close>
|
||
|
||
\<^item>\<^ML>\<open>Latex.block: Latex.text -> XML.tree\<close>
|
||
\<close>
|
||
|
||
|
||
|
||
ML\<open> Latex.output_ascii;
|
||
Latex.environment "isa" (Latex.string "bg");
|
||
Latex.output_ascii "a_b:c'é";
|
||
(* Note: *)
|
||
space_implode "sd &e sf dfg" ["qs","er","alpa"];
|
||
\<close>
|
||
|
||
text\<open>Here is an abstract of the main interface to @{ML_structure Document_Output}:\<close>
|
||
|
||
text\<open>
|
||
\<^item>\<^ML>\<open>Document_Output.output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text \<close>
|
||
\<^item>\<^ML>\<open>Document_Output.output_token: Proof.context -> Token.T -> Latex.text \<close>
|
||
\<^item>\<^ML>\<open>Document_Output.output_source: Proof.context -> string -> Latex.text \<close>
|
||
\<^item>\<^ML>\<open>Document_Output.present_thy: Options.T -> theory -> Document_Output.segment list -> Latex.text \<close>
|
||
|
||
\<^item>\<^ML>\<open>Document_Output.isabelle: Proof.context -> Latex.text -> Latex.text\<close>
|
||
\<^item>\<^ML>\<open>Document_Output.isabelle_typewriter: Proof.context -> Latex.text -> Latex.text\<close>
|
||
\<^item>\<^ML>\<open>Document_Output.typewriter: Proof.context -> string -> Latex.text\<close>
|
||
\<^item>\<^ML>\<open>Document_Output.verbatim: Proof.context -> string -> Latex.text\<close>
|
||
\<^item>\<^ML>\<open>Document_Output.source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text\<close>
|
||
\<^item>\<^ML>\<open>Document_Output.pretty: Proof.context -> Pretty.T -> Latex.text\<close>
|
||
\<^item>\<^ML>\<open>Document_Output.pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text\<close>
|
||
\<^item>\<^ML>\<open>Document_Output.pretty_items: Proof.context -> Pretty.T list -> Latex.text\<close>
|
||
\<^item>\<^ML>\<open>Document_Output.pretty_items_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T list -> Latex.text\<close>
|
||
|
||
Finally a number of antiquotation registries :
|
||
|
||
\<^item>\<^ML>\<open>Document_Output.antiquotation_pretty:
|
||
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory\<close>
|
||
\<^item>\<^ML>\<open>Document_Output.antiquotation_pretty_source:
|
||
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory\<close>
|
||
\<^item>\<^ML>\<open>Document_Output.antiquotation_raw:
|
||
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory\<close>
|
||
\<^item>\<^ML>\<open>Document_Output.antiquotation_verbatim:
|
||
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory\<close>
|
||
\<close>
|
||
|
||
|
||
text\<open> Thus, \<^ML_structure>\<open>Syntax_Phases\<close> does the actual work of markup generation, including
|
||
markup generation and generation of reports. Look at the following snippet:
|
||
\<open>
|
||
fun check_typs ctxt raw_tys =
|
||
let
|
||
val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
|
||
val _ = if Context_Position.is_visible ctxt then Output.report sorting_report else ();
|
||
in
|
||
tys
|
||
|> apply_typ_check ctxt
|
||
|> Term_Sharing.typs (Proof_Context.theory_of ctxt)
|
||
end;
|
||
\<close>
|
||
|
||
which is the real implementation behind \<^ML>\<open>Syntax.check_typ\<close>
|
||
|
||
\<open>
|
||
fun check_terms ctxt raw_ts =
|
||
let
|
||
val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts;
|
||
val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts';
|
||
|
||
val tys = map (Logic.mk_type o snd) ps;
|
||
val (ts', tys') = ts @ tys
|
||
|> apply_term_check ctxt
|
||
|> chop (length ts);
|
||
val typing_report =
|
||
fold2 (fn (pos, _) => fn ty =>
|
||
if Position.is_reported pos then
|
||
cons (Position.reported_text pos Markup.typing
|
||
(Syntax.string_of_typ ctxt (Logic.dest_type ty)))
|
||
else I) ps tys' [];
|
||
|
||
val _ =
|
||
if Context_Position.is_visible ctxt then Output.report (sorting_report @ typing_report)
|
||
else ();
|
||
in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
|
||
\<close>
|
||
|
||
which is the real implementation behind \<^ML>\<open>Syntax.check_term\<close>. As one can see, check-routines
|
||
internally generate the markup.
|
||
\<close>
|
||
|
||
|
||
section*[cartouches::technical]\<open>Inner Syntax Cartouches\<close>
|
||
text\<open> The cascade-syntax principle underlying recent isabelle versions requires a
|
||
particular mechanism, called "cartouche" by Makarius who was influenced by French
|
||
Wine and French culture when designing this.
|
||
|
||
When parsing terms or types (via the Earley Parser), a standard mechanism for
|
||
calling another parser inside the current process is needed that is bound to the
|
||
\<open>(\<open>)\<close> ... \<open>(\<close>)\<close> paranthesis'. \<close>
|
||
|
||
text\<open>The following example --- drawn from the Isabelle/DOF implementation --- allows
|
||
to parse UTF8 - Unicode strings as alternative to @{term "''abc''"} HOL-strings.\<close>
|
||
|
||
ML\<open>\<comment> \<open>Dynamic setup of inner syntax cartouche\<close>
|
||
|
||
|
||
(* Author: Frédéric Tuong, Université Paris-Saclay *)
|
||
(* Title: HOL/ex/Cartouche_Examples.thy
|
||
Author: Makarius *)
|
||
local
|
||
fun mk_char (f_char, f_cons, _) (s, _) accu =
|
||
fold
|
||
(fn c => fn (accu, l) =>
|
||
(f_char c accu, f_cons c l))
|
||
(rev (map Char.ord (String.explode s)))
|
||
accu;
|
||
|
||
fun mk_string (_, _, f_nil) accu [] = (accu, f_nil)
|
||
| mk_string f accu (s :: ss) = mk_char f s (mk_string f accu ss);
|
||
in
|
||
fun string_tr f f_mk accu content args =
|
||
let fun err () = raise TERM ("string_tr", args) in
|
||
(case args of
|
||
[(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
|
||
(case Term_Position.decode_position p of
|
||
SOME (pos, _) => c $ f (mk_string f_mk accu (content (s, pos))) $ p
|
||
| NONE => err ())
|
||
| _ => err ())
|
||
end;
|
||
end;
|
||
\<close>
|
||
|
||
syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> _" ("_")
|
||
|
||
ML\<open>
|
||
structure Cartouche_Grammar = struct
|
||
fun list_comb_mk cst n c = list_comb (Syntax.const cst, String_Syntax.mk_bits_syntax n c)
|
||
val nil1 = Syntax.const @{const_syntax String.empty_literal}
|
||
fun cons1 c l = list_comb_mk @{const_syntax String.Literal} 7 c $ l
|
||
|
||
val default =
|
||
[ ( "char list"
|
||
, ( Const (@{const_syntax Nil}, @{typ "char list"})
|
||
, fn c => fn l => Syntax.const @{const_syntax Cons} $ list_comb_mk @{const_syntax Char} 8 c $ l
|
||
, snd))
|
||
, ( "String.literal", (nil1, cons1, snd))]
|
||
end
|
||
\<close>
|
||
|
||
ML\<open>
|
||
fun parse_translation_cartouche binding l f_integer accu =
|
||
let val cartouche_type = Attrib.setup_config_string binding (K (fst (hd l)))
|
||
(* if there is no type specified, by default we set the first element
|
||
to be the default type of cartouches *) in
|
||
fn ctxt =>
|
||
let val cart_type = Config.get ctxt cartouche_type in
|
||
case List.find (fn (s, _) => s = cart_type) l of
|
||
NONE => error ("Unregistered return type for the cartouche: \"" ^ cart_type ^ "\"")
|
||
| SOME (_, (nil0, cons, f)) =>
|
||
string_tr f (f_integer, cons, nil0) accu (Symbol_Pos.cartouche_content o Symbol_Pos.explode)
|
||
end
|
||
end
|
||
\<close>
|
||
|
||
text\<open>The following registration of this cartouche for strings is fails because it has
|
||
already been done in the surrounding Isabelle/DOF environment...
|
||
\<^verbatim>\<open>
|
||
parse_translation \<open>
|
||
[( @{syntax_const "_cartouche_string"}
|
||
, parse_translation_cartouche \<^binding>\<open>cartouche_type\<close> Cartouche_Grammar.default (K I) ())]
|
||
\<close>
|
||
\<close>
|
||
\<close>
|
||
|
||
text\<open> Test for this cartouche... \<close>
|
||
term "\<open>A \<Longrightarrow> B\<close> = ''''"
|
||
|
||
|
||
|
||
chapter*[c::conclusion]\<open>Conclusion\<close>
|
||
text\<open> This interactive Isabelle Programming Cook-Book represents my current way
|
||
to view and explain Isabelle programming API's to students and collaborators.
|
||
It differs from the reference manual in some places on purpose, since I believe
|
||
that a lot of internal Isabelle API's need a more conceptual view on what is happening
|
||
(even if this conceptual view is at times over-abstracting a little).
|
||
It is written in Isabelle/DOF and conceived as "living document" (a term that I owe to
|
||
Simon Foster), i.e. as hypertext-heavy text making direct references to the Isabelle API's
|
||
which were checked whenever this document is re-visited in Isabelle/jEdit.
|
||
|
||
All hints and contributions of collegues and collaborators are greatly welcomed; all errors
|
||
and the roughness of this presentation is entirely my fault.
|
||
\<close>
|
||
(*<*)
|
||
|
||
paragraph\<open>Many thanks to Frederic Tuong, who contributed some example such as the string
|
||
cartouche for Unicode Character Denotations as well as many local hints for improvements.\<close>
|
||
|
||
section*[bib::bibliography]\<open>Bibliography\<close>
|
||
|
||
close_monitor*[this]
|
||
check_doc_global
|
||
|
||
end
|
||
(*>*)
|