wenzelm@30296
|
1 |
%
|
wenzelm@30296
|
2 |
\begin{isabellebody}%
|
wenzelm@30296
|
3 |
\def\isabellecontext{Integration}%
|
wenzelm@30296
|
4 |
%
|
wenzelm@30296
|
5 |
\isadelimtheory
|
wenzelm@30296
|
6 |
%
|
wenzelm@30296
|
7 |
\endisadelimtheory
|
wenzelm@30296
|
8 |
%
|
wenzelm@30296
|
9 |
\isatagtheory
|
wenzelm@30296
|
10 |
\isacommand{theory}\isamarkupfalse%
|
wenzelm@30296
|
11 |
\ Integration\isanewline
|
wenzelm@30296
|
12 |
\isakeyword{imports}\ Base\isanewline
|
wenzelm@30296
|
13 |
\isakeyword{begin}%
|
wenzelm@30296
|
14 |
\endisatagtheory
|
wenzelm@30296
|
15 |
{\isafoldtheory}%
|
wenzelm@30296
|
16 |
%
|
wenzelm@30296
|
17 |
\isadelimtheory
|
wenzelm@30296
|
18 |
%
|
wenzelm@30296
|
19 |
\endisadelimtheory
|
wenzelm@30296
|
20 |
%
|
wenzelm@30296
|
21 |
\isamarkupchapter{System integration%
|
wenzelm@30296
|
22 |
}
|
wenzelm@30296
|
23 |
\isamarkuptrue%
|
wenzelm@30296
|
24 |
%
|
wenzelm@30296
|
25 |
\isamarkupsection{Isar toplevel \label{sec:isar-toplevel}%
|
wenzelm@30296
|
26 |
}
|
wenzelm@30296
|
27 |
\isamarkuptrue%
|
wenzelm@30296
|
28 |
%
|
wenzelm@30296
|
29 |
\begin{isamarkuptext}%
|
wenzelm@30296
|
30 |
The Isar toplevel may be considered the centeral hub of the
|
wenzelm@30296
|
31 |
Isabelle/Isar system, where all key components and sub-systems are
|
wenzelm@30296
|
32 |
integrated into a single read-eval-print loop of Isar commands. We
|
wenzelm@30296
|
33 |
shall even incorporate the existing {\ML} toplevel of the compiler
|
wenzelm@30296
|
34 |
and run-time system (cf.\ \secref{sec:ML-toplevel}).
|
wenzelm@30296
|
35 |
|
wenzelm@30296
|
36 |
Isabelle/Isar departs from the original ``LCF system architecture''
|
wenzelm@30296
|
37 |
where {\ML} was really The Meta Language for defining theories and
|
wenzelm@30296
|
38 |
conducting proofs. Instead, {\ML} now only serves as the
|
wenzelm@30296
|
39 |
implementation language for the system (and user extensions), while
|
wenzelm@30296
|
40 |
the specific Isar toplevel supports the concepts of theory and proof
|
wenzelm@30296
|
41 |
development natively. This includes the graph structure of theories
|
wenzelm@30296
|
42 |
and the block structure of proofs, support for unlimited undo,
|
wenzelm@30296
|
43 |
facilities for tracing, debugging, timing, profiling etc.
|
wenzelm@30296
|
44 |
|
wenzelm@30296
|
45 |
\medskip The toplevel maintains an implicit state, which is
|
wenzelm@30296
|
46 |
transformed by a sequence of transitions -- either interactively or
|
wenzelm@30296
|
47 |
in batch-mode. In interactive mode, Isar state transitions are
|
wenzelm@30296
|
48 |
encapsulated as safe transactions, such that both failure and undo
|
wenzelm@30296
|
49 |
are handled conveniently without destroying the underlying draft
|
wenzelm@30296
|
50 |
theory (cf.~\secref{sec:context-theory}). In batch mode,
|
wenzelm@30296
|
51 |
transitions operate in a linear (destructive) fashion, such that
|
wenzelm@30296
|
52 |
error conditions abort the present attempt to construct a theory or
|
wenzelm@30296
|
53 |
proof altogether.
|
wenzelm@30296
|
54 |
|
wenzelm@30296
|
55 |
The toplevel state is a disjoint sum of empty \isa{toplevel}, or
|
wenzelm@30296
|
56 |
\isa{theory}, or \isa{proof}. On entering the main Isar loop we
|
wenzelm@30296
|
57 |
start with an empty toplevel. A theory is commenced by giving a
|
wenzelm@30296
|
58 |
\isa{{\isasymTHEORY}} header; within a theory we may issue theory
|
wenzelm@30296
|
59 |
commands such as \isa{{\isasymDEFINITION}}, or state a \isa{{\isasymTHEOREM}} to be proven. Now we are within a proof state, with a
|
wenzelm@30296
|
60 |
rich collection of Isar proof commands for structured proof
|
wenzelm@30296
|
61 |
composition, or unstructured proof scripts. When the proof is
|
wenzelm@30296
|
62 |
concluded we get back to the theory, which is then updated by
|
wenzelm@30296
|
63 |
storing the resulting fact. Further theory declarations or theorem
|
wenzelm@30296
|
64 |
statements with proofs may follow, until we eventually conclude the
|
wenzelm@30296
|
65 |
theory development by issuing \isa{{\isasymEND}}. The resulting theory
|
wenzelm@30296
|
66 |
is then stored within the theory database and we are back to the
|
wenzelm@30296
|
67 |
empty toplevel.
|
wenzelm@30296
|
68 |
|
wenzelm@30296
|
69 |
In addition to these proper state transformations, there are also
|
wenzelm@30296
|
70 |
some diagnostic commands for peeking at the toplevel state without
|
wenzelm@30296
|
71 |
modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
|
wenzelm@30296
|
72 |
\isakeyword{print-cases}).%
|
wenzelm@30296
|
73 |
\end{isamarkuptext}%
|
wenzelm@30296
|
74 |
\isamarkuptrue%
|
wenzelm@30296
|
75 |
%
|
wenzelm@30296
|
76 |
\isadelimmlref
|
wenzelm@30296
|
77 |
%
|
wenzelm@30296
|
78 |
\endisadelimmlref
|
wenzelm@30296
|
79 |
%
|
wenzelm@30296
|
80 |
\isatagmlref
|
wenzelm@30296
|
81 |
%
|
wenzelm@30296
|
82 |
\begin{isamarkuptext}%
|
wenzelm@30296
|
83 |
\begin{mldecls}
|
wenzelm@30296
|
84 |
\indexdef{}{ML type}{Toplevel.state}\verb|type Toplevel.state| \\
|
wenzelm@30296
|
85 |
\indexdef{}{ML}{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
|
wenzelm@30296
|
86 |
\indexdef{}{ML}{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
|
wenzelm@30296
|
87 |
\indexdef{}{ML}{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
|
wenzelm@30296
|
88 |
\indexdef{}{ML}{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
|
wenzelm@32836
|
89 |
\indexdef{}{ML}{Toplevel.debug}\verb|Toplevel.debug: bool Unsynchronized.ref| \\
|
wenzelm@32836
|
90 |
\indexdef{}{ML}{Toplevel.timing}\verb|Toplevel.timing: bool Unsynchronized.ref| \\
|
wenzelm@32836
|
91 |
\indexdef{}{ML}{Toplevel.profiling}\verb|Toplevel.profiling: int Unsynchronized.ref| \\
|
wenzelm@30296
|
92 |
\end{mldecls}
|
wenzelm@30296
|
93 |
|
wenzelm@30296
|
94 |
\begin{description}
|
wenzelm@30296
|
95 |
|
wenzelm@30296
|
96 |
\item \verb|Toplevel.state| represents Isar toplevel states,
|
wenzelm@30296
|
97 |
which are normally manipulated through the concept of toplevel
|
wenzelm@30296
|
98 |
transitions only (\secref{sec:toplevel-transition}). Also note that
|
wenzelm@30296
|
99 |
a raw toplevel state is subject to the same linearity restrictions
|
wenzelm@30296
|
100 |
as a theory context (cf.~\secref{sec:context-theory}).
|
wenzelm@30296
|
101 |
|
wenzelm@30296
|
102 |
\item \verb|Toplevel.UNDEF| is raised for undefined toplevel
|
wenzelm@30296
|
103 |
operations. Many operations work only partially for certain cases,
|
wenzelm@30296
|
104 |
since \verb|Toplevel.state| is a sum type.
|
wenzelm@30296
|
105 |
|
wenzelm@30296
|
106 |
\item \verb|Toplevel.is_toplevel|~\isa{state} checks for an empty
|
wenzelm@30296
|
107 |
toplevel state.
|
wenzelm@30296
|
108 |
|
wenzelm@35001
|
109 |
\item \verb|Toplevel.theory_of|~\isa{state} selects the
|
wenzelm@35001
|
110 |
background theory of \isa{state}, raises \verb|Toplevel.UNDEF|
|
wenzelm@35001
|
111 |
for an empty toplevel state.
|
wenzelm@30296
|
112 |
|
wenzelm@30296
|
113 |
\item \verb|Toplevel.proof_of|~\isa{state} selects the Isar proof
|
wenzelm@30296
|
114 |
state if available, otherwise raises \verb|Toplevel.UNDEF|.
|
wenzelm@30296
|
115 |
|
wenzelm@32836
|
116 |
\item \verb|Toplevel.debug := true| makes the toplevel print further
|
wenzelm@30296
|
117 |
details about internal error conditions, exceptions being raised
|
wenzelm@30296
|
118 |
etc.
|
wenzelm@30296
|
119 |
|
wenzelm@32836
|
120 |
\item \verb|Toplevel.timing := true| makes the toplevel print timing
|
wenzelm@30296
|
121 |
information for each Isar command being executed.
|
wenzelm@30296
|
122 |
|
wenzelm@30296
|
123 |
\item \verb|Toplevel.profiling|~\verb|:=|~\isa{n} controls
|
wenzelm@30296
|
124 |
low-level profiling of the underlying {\ML} runtime system. For
|
wenzelm@30296
|
125 |
Poly/ML, \isa{n\ {\isacharequal}\ {\isadigit{1}}} means time and \isa{n\ {\isacharequal}\ {\isadigit{2}}} space
|
wenzelm@30296
|
126 |
profiling.
|
wenzelm@30296
|
127 |
|
wenzelm@30296
|
128 |
\end{description}%
|
wenzelm@30296
|
129 |
\end{isamarkuptext}%
|
wenzelm@30296
|
130 |
\isamarkuptrue%
|
wenzelm@30296
|
131 |
%
|
wenzelm@30296
|
132 |
\endisatagmlref
|
wenzelm@30296
|
133 |
{\isafoldmlref}%
|
wenzelm@30296
|
134 |
%
|
wenzelm@30296
|
135 |
\isadelimmlref
|
wenzelm@30296
|
136 |
%
|
wenzelm@30296
|
137 |
\endisadelimmlref
|
wenzelm@30296
|
138 |
%
|
wenzelm@30296
|
139 |
\isamarkupsubsection{Toplevel transitions \label{sec:toplevel-transition}%
|
wenzelm@30296
|
140 |
}
|
wenzelm@30296
|
141 |
\isamarkuptrue%
|
wenzelm@30296
|
142 |
%
|
wenzelm@30296
|
143 |
\begin{isamarkuptext}%
|
wenzelm@30296
|
144 |
An Isar toplevel transition consists of a partial function on the
|
wenzelm@30296
|
145 |
toplevel state, with additional information for diagnostics and
|
wenzelm@30296
|
146 |
error reporting: there are fields for command name, source position,
|
wenzelm@30296
|
147 |
optional source text, as well as flags for interactive-only commands
|
wenzelm@30296
|
148 |
(which issue a warning in batch-mode), printing of result state,
|
wenzelm@30296
|
149 |
etc.
|
wenzelm@30296
|
150 |
|
wenzelm@30296
|
151 |
The operational part is represented as the sequential union of a
|
wenzelm@30296
|
152 |
list of partial functions, which are tried in turn until the first
|
wenzelm@30296
|
153 |
one succeeds. This acts like an outer case-expression for various
|
wenzelm@35001
|
154 |
alternative state transitions. For example, \isakeyword{qed} works
|
wenzelm@30296
|
155 |
differently for a local proofs vs.\ the global ending of the main
|
wenzelm@30296
|
156 |
proof.
|
wenzelm@30296
|
157 |
|
wenzelm@30296
|
158 |
Toplevel transitions are composed via transition transformers.
|
wenzelm@30296
|
159 |
Internally, Isar commands are put together from an empty transition
|
wenzelm@35001
|
160 |
extended by name and source position. It is then left to the
|
wenzelm@35001
|
161 |
individual command parser to turn the given concrete syntax into a
|
wenzelm@35001
|
162 |
suitable transition transformer that adjoins actual operations on a
|
wenzelm@35001
|
163 |
theory or proof state etc.%
|
wenzelm@30296
|
164 |
\end{isamarkuptext}%
|
wenzelm@30296
|
165 |
\isamarkuptrue%
|
wenzelm@30296
|
166 |
%
|
wenzelm@30296
|
167 |
\isadelimmlref
|
wenzelm@30296
|
168 |
%
|
wenzelm@30296
|
169 |
\endisadelimmlref
|
wenzelm@30296
|
170 |
%
|
wenzelm@30296
|
171 |
\isatagmlref
|
wenzelm@30296
|
172 |
%
|
wenzelm@30296
|
173 |
\begin{isamarkuptext}%
|
wenzelm@30296
|
174 |
\begin{mldecls}
|
wenzelm@30296
|
175 |
\indexdef{}{ML}{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
|
wenzelm@30296
|
176 |
\indexdef{}{ML}{Toplevel.no\_timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
|
wenzelm@30296
|
177 |
\indexdef{}{ML}{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
|
wenzelm@30296
|
178 |
\verb| Toplevel.transition -> Toplevel.transition| \\
|
wenzelm@30296
|
179 |
\indexdef{}{ML}{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
|
wenzelm@30296
|
180 |
\verb| Toplevel.transition -> Toplevel.transition| \\
|
wenzelm@30296
|
181 |
\indexdef{}{ML}{Toplevel.theory\_to\_proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
|
wenzelm@30296
|
182 |
\verb| Toplevel.transition -> Toplevel.transition| \\
|
wenzelm@30296
|
183 |
\indexdef{}{ML}{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
|
wenzelm@30296
|
184 |
\verb| Toplevel.transition -> Toplevel.transition| \\
|
wenzelm@30296
|
185 |
\indexdef{}{ML}{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
|
wenzelm@30296
|
186 |
\verb| Toplevel.transition -> Toplevel.transition| \\
|
wenzelm@30296
|
187 |
\indexdef{}{ML}{Toplevel.end\_proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
|
wenzelm@30296
|
188 |
\verb| Toplevel.transition -> Toplevel.transition| \\
|
wenzelm@30296
|
189 |
\end{mldecls}
|
wenzelm@30296
|
190 |
|
wenzelm@30296
|
191 |
\begin{description}
|
wenzelm@30296
|
192 |
|
wenzelm@30296
|
193 |
\item \verb|Toplevel.print|~\isa{tr} sets the print flag, which
|
wenzelm@30296
|
194 |
causes the toplevel loop to echo the result state (in interactive
|
wenzelm@30296
|
195 |
mode).
|
wenzelm@30296
|
196 |
|
wenzelm@30296
|
197 |
\item \verb|Toplevel.no_timing|~\isa{tr} indicates that the
|
wenzelm@30296
|
198 |
transition should never show timing information, e.g.\ because it is
|
wenzelm@30296
|
199 |
a diagnostic command.
|
wenzelm@30296
|
200 |
|
wenzelm@30296
|
201 |
\item \verb|Toplevel.keep|~\isa{tr} adjoins a diagnostic
|
wenzelm@30296
|
202 |
function.
|
wenzelm@30296
|
203 |
|
wenzelm@30296
|
204 |
\item \verb|Toplevel.theory|~\isa{tr} adjoins a theory
|
wenzelm@30296
|
205 |
transformer.
|
wenzelm@30296
|
206 |
|
wenzelm@30296
|
207 |
\item \verb|Toplevel.theory_to_proof|~\isa{tr} adjoins a global
|
wenzelm@30296
|
208 |
goal function, which turns a theory into a proof state. The theory
|
wenzelm@30296
|
209 |
may be changed before entering the proof; the generic Isar goal
|
wenzelm@30296
|
210 |
setup includes an argument that specifies how to apply the proven
|
wenzelm@30296
|
211 |
result to the theory, when the proof is finished.
|
wenzelm@30296
|
212 |
|
wenzelm@30296
|
213 |
\item \verb|Toplevel.proof|~\isa{tr} adjoins a deterministic
|
wenzelm@30296
|
214 |
proof command, with a singleton result.
|
wenzelm@30296
|
215 |
|
wenzelm@30296
|
216 |
\item \verb|Toplevel.proofs|~\isa{tr} adjoins a general proof
|
wenzelm@30296
|
217 |
command, with zero or more result states (represented as a lazy
|
wenzelm@30296
|
218 |
list).
|
wenzelm@30296
|
219 |
|
wenzelm@30296
|
220 |
\item \verb|Toplevel.end_proof|~\isa{tr} adjoins a concluding
|
wenzelm@30296
|
221 |
proof command, that returns the resulting theory, after storing the
|
wenzelm@30296
|
222 |
resulting facts in the context etc.
|
wenzelm@30296
|
223 |
|
wenzelm@30296
|
224 |
\end{description}%
|
wenzelm@30296
|
225 |
\end{isamarkuptext}%
|
wenzelm@30296
|
226 |
\isamarkuptrue%
|
wenzelm@30296
|
227 |
%
|
wenzelm@30296
|
228 |
\endisatagmlref
|
wenzelm@30296
|
229 |
{\isafoldmlref}%
|
wenzelm@30296
|
230 |
%
|
wenzelm@30296
|
231 |
\isadelimmlref
|
wenzelm@30296
|
232 |
%
|
wenzelm@30296
|
233 |
\endisadelimmlref
|
wenzelm@30296
|
234 |
%
|
wenzelm@30296
|
235 |
\isamarkupsubsection{Toplevel control%
|
wenzelm@30296
|
236 |
}
|
wenzelm@30296
|
237 |
\isamarkuptrue%
|
wenzelm@30296
|
238 |
%
|
wenzelm@30296
|
239 |
\begin{isamarkuptext}%
|
wenzelm@30296
|
240 |
There are a few special control commands that modify the behavior
|
wenzelm@30296
|
241 |
the toplevel itself, and only make sense in interactive mode. Under
|
wenzelm@30296
|
242 |
normal circumstances, the user encounters these only implicitly as
|
wenzelm@30296
|
243 |
part of the protocol between the Isabelle/Isar system and a
|
wenzelm@35001
|
244 |
user-interface such as Proof~General.
|
wenzelm@30296
|
245 |
|
wenzelm@30296
|
246 |
\begin{description}
|
wenzelm@30296
|
247 |
|
wenzelm@30296
|
248 |
\item \isacommand{undo} follows the three-level hierarchy of empty
|
wenzelm@30296
|
249 |
toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
|
wenzelm@30296
|
250 |
previous proof context, undo after a proof reverts to the theory
|
wenzelm@30296
|
251 |
before the initial goal statement, undo of a theory command reverts
|
wenzelm@30296
|
252 |
to the previous theory value, undo of a theory header discontinues
|
wenzelm@30296
|
253 |
the current theory development and removes it from the theory
|
wenzelm@30296
|
254 |
database (\secref{sec:theory-database}).
|
wenzelm@30296
|
255 |
|
wenzelm@30296
|
256 |
\item \isacommand{kill} aborts the current level of development:
|
wenzelm@30296
|
257 |
kill in a proof context reverts to the theory before the initial
|
wenzelm@30296
|
258 |
goal statement, kill in a theory context aborts the current theory
|
wenzelm@30296
|
259 |
development, removing it from the database.
|
wenzelm@30296
|
260 |
|
wenzelm@30296
|
261 |
\item \isacommand{exit} drops out of the Isar toplevel into the
|
wenzelm@30296
|
262 |
underlying {\ML} toplevel (\secref{sec:ML-toplevel}). The Isar
|
wenzelm@30296
|
263 |
toplevel state is preserved and may be continued later.
|
wenzelm@30296
|
264 |
|
wenzelm@30296
|
265 |
\item \isacommand{quit} terminates the Isabelle/Isar process without
|
wenzelm@30296
|
266 |
saving.
|
wenzelm@30296
|
267 |
|
wenzelm@30296
|
268 |
\end{description}%
|
wenzelm@30296
|
269 |
\end{isamarkuptext}%
|
wenzelm@30296
|
270 |
\isamarkuptrue%
|
wenzelm@30296
|
271 |
%
|
wenzelm@30296
|
272 |
\isamarkupsection{ML toplevel \label{sec:ML-toplevel}%
|
wenzelm@30296
|
273 |
}
|
wenzelm@30296
|
274 |
\isamarkuptrue%
|
wenzelm@30296
|
275 |
%
|
wenzelm@30296
|
276 |
\begin{isamarkuptext}%
|
wenzelm@30296
|
277 |
The {\ML} toplevel provides a read-compile-eval-print loop for {\ML}
|
wenzelm@30296
|
278 |
values, types, structures, and functors. {\ML} declarations operate
|
wenzelm@30296
|
279 |
on the global system state, which consists of the compiler
|
wenzelm@30296
|
280 |
environment plus the values of {\ML} reference variables. There is
|
wenzelm@30296
|
281 |
no clean way to undo {\ML} declarations, except for reverting to a
|
wenzelm@30296
|
282 |
previously saved state of the whole Isabelle process. {\ML} input
|
wenzelm@30296
|
283 |
is either read interactively from a TTY, or from a string (usually
|
wenzelm@30296
|
284 |
within a theory text), or from a source file (usually loaded from a
|
wenzelm@30296
|
285 |
theory).
|
wenzelm@30296
|
286 |
|
wenzelm@30296
|
287 |
Whenever the {\ML} toplevel is active, the current Isabelle theory
|
wenzelm@30296
|
288 |
context is passed as an internal reference variable. Thus {\ML}
|
wenzelm@30296
|
289 |
code may access the theory context during compilation, it may even
|
wenzelm@30296
|
290 |
change the value of a theory being under construction --- while
|
wenzelm@30296
|
291 |
observing the usual linearity restrictions
|
wenzelm@30296
|
292 |
(cf.~\secref{sec:context-theory}).%
|
wenzelm@30296
|
293 |
\end{isamarkuptext}%
|
wenzelm@30296
|
294 |
\isamarkuptrue%
|
wenzelm@30296
|
295 |
%
|
wenzelm@30296
|
296 |
\isadelimmlref
|
wenzelm@30296
|
297 |
%
|
wenzelm@30296
|
298 |
\endisadelimmlref
|
wenzelm@30296
|
299 |
%
|
wenzelm@30296
|
300 |
\isatagmlref
|
wenzelm@30296
|
301 |
%
|
wenzelm@30296
|
302 |
\begin{isamarkuptext}%
|
wenzelm@30296
|
303 |
\begin{mldecls}
|
wenzelm@32189
|
304 |
\indexdef{}{ML}{ML\_Context.the\_generic\_context}\verb|ML_Context.the_generic_context: unit -> Context.generic| \\
|
wenzelm@30296
|
305 |
\indexdef{}{ML}{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
|
wenzelm@30296
|
306 |
\end{mldecls}
|
wenzelm@30296
|
307 |
|
wenzelm@30296
|
308 |
\begin{description}
|
wenzelm@30296
|
309 |
|
wenzelm@32189
|
310 |
\item \verb|ML_Context.the_generic_context ()| refers to the theory
|
wenzelm@32189
|
311 |
context of the {\ML} toplevel --- at compile time! {\ML} code needs
|
wenzelm@32189
|
312 |
to take care to refer to \verb|ML_Context.the_generic_context ()|
|
wenzelm@32189
|
313 |
correctly. Recall that evaluation of a function body is delayed
|
wenzelm@32189
|
314 |
until actual runtime. Moreover, persistent {\ML} toplevel bindings
|
wenzelm@32189
|
315 |
to an unfinished theory should be avoided: code should either
|
wenzelm@32189
|
316 |
project out the desired information immediately, or produce an
|
wenzelm@32189
|
317 |
explicit \verb|theory_ref| (cf.\ \secref{sec:context-theory}).
|
wenzelm@30296
|
318 |
|
wenzelm@30296
|
319 |
\item \verb|Context.>>|~\isa{f} applies context transformation
|
wenzelm@30296
|
320 |
\isa{f} to the implicit context of the {\ML} toplevel.
|
wenzelm@30296
|
321 |
|
wenzelm@30296
|
322 |
\end{description}
|
wenzelm@30296
|
323 |
|
wenzelm@30296
|
324 |
It is very important to note that the above functions are really
|
wenzelm@30296
|
325 |
restricted to the compile time, even though the {\ML} compiler is
|
wenzelm@30296
|
326 |
invoked at runtime! The majority of {\ML} code uses explicit
|
wenzelm@30296
|
327 |
functional arguments of a theory or proof context instead. Thus it
|
wenzelm@30296
|
328 |
may be invoked for an arbitrary context later on, without having to
|
wenzelm@30296
|
329 |
worry about any operational details.
|
wenzelm@30296
|
330 |
|
wenzelm@30296
|
331 |
\bigskip
|
wenzelm@30296
|
332 |
|
wenzelm@30296
|
333 |
\begin{mldecls}
|
wenzelm@30296
|
334 |
\indexdef{}{ML}{Isar.main}\verb|Isar.main: unit -> unit| \\
|
wenzelm@30296
|
335 |
\indexdef{}{ML}{Isar.loop}\verb|Isar.loop: unit -> unit| \\
|
wenzelm@30296
|
336 |
\indexdef{}{ML}{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
|
wenzelm@30296
|
337 |
\indexdef{}{ML}{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
|
wenzelm@30296
|
338 |
\indexdef{}{ML}{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
|
wenzelm@33293
|
339 |
\indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit ->|\isasep\isanewline%
|
wenzelm@33293
|
340 |
\verb| {context: Proof.context, facts: thm list, goal: thm}| \\
|
wenzelm@30296
|
341 |
\end{mldecls}
|
wenzelm@30296
|
342 |
|
wenzelm@30296
|
343 |
\begin{description}
|
wenzelm@30296
|
344 |
|
wenzelm@30296
|
345 |
\item \verb|Isar.main ()| invokes the Isar toplevel from {\ML},
|
wenzelm@30296
|
346 |
initializing an empty toplevel state.
|
wenzelm@30296
|
347 |
|
wenzelm@30296
|
348 |
\item \verb|Isar.loop ()| continues the Isar toplevel with the
|
wenzelm@30296
|
349 |
current state, after having dropped out of the Isar toplevel loop.
|
wenzelm@30296
|
350 |
|
wenzelm@30296
|
351 |
\item \verb|Isar.state ()| and \verb|Isar.exn ()| get current
|
wenzelm@30296
|
352 |
toplevel state and error condition, respectively. This only works
|
wenzelm@30296
|
353 |
after having dropped out of the Isar toplevel loop.
|
wenzelm@30296
|
354 |
|
wenzelm@30296
|
355 |
\item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|, analogous to \verb|Context.proof_of|
|
wenzelm@30296
|
356 |
(\secref{sec:generic-context}).
|
wenzelm@30296
|
357 |
|
wenzelm@33293
|
358 |
\item \verb|Isar.goal ()| produces the full Isar goal state,
|
wenzelm@33293
|
359 |
consisting of proof context, facts that have been indicated for
|
wenzelm@33293
|
360 |
immediate use, and the tactical goal according to
|
wenzelm@30296
|
361 |
\secref{sec:tactical-goals}.
|
wenzelm@30296
|
362 |
|
wenzelm@30296
|
363 |
\end{description}%
|
wenzelm@30296
|
364 |
\end{isamarkuptext}%
|
wenzelm@30296
|
365 |
\isamarkuptrue%
|
wenzelm@30296
|
366 |
%
|
wenzelm@30296
|
367 |
\endisatagmlref
|
wenzelm@30296
|
368 |
{\isafoldmlref}%
|
wenzelm@30296
|
369 |
%
|
wenzelm@30296
|
370 |
\isadelimmlref
|
wenzelm@30296
|
371 |
%
|
wenzelm@30296
|
372 |
\endisadelimmlref
|
wenzelm@30296
|
373 |
%
|
wenzelm@30296
|
374 |
\isamarkupsection{Theory database \label{sec:theory-database}%
|
wenzelm@30296
|
375 |
}
|
wenzelm@30296
|
376 |
\isamarkuptrue%
|
wenzelm@30296
|
377 |
%
|
wenzelm@30296
|
378 |
\begin{isamarkuptext}%
|
wenzelm@30296
|
379 |
The theory database maintains a collection of theories, together
|
wenzelm@30296
|
380 |
with some administrative information about their original sources,
|
wenzelm@30296
|
381 |
which are held in an external store (i.e.\ some directory within the
|
wenzelm@30296
|
382 |
regular file system).
|
wenzelm@30296
|
383 |
|
wenzelm@30296
|
384 |
The theory database is organized as a directed acyclic graph;
|
wenzelm@30296
|
385 |
entries are referenced by theory name. Although some additional
|
wenzelm@30296
|
386 |
interfaces allow to include a directory specification as well, this
|
wenzelm@30296
|
387 |
is only a hint to the underlying theory loader. The internal theory
|
wenzelm@30296
|
388 |
name space is flat!
|
wenzelm@30296
|
389 |
|
wenzelm@30296
|
390 |
Theory \isa{A} is associated with the main theory file \isa{A}\verb,.thy,, which needs to be accessible through the theory
|
wenzelm@30296
|
391 |
loader path. Any number of additional {\ML} source files may be
|
wenzelm@30296
|
392 |
associated with each theory, by declaring these dependencies in the
|
wenzelm@30296
|
393 |
theory header as \isa{{\isasymUSES}}, and loading them consecutively
|
wenzelm@30296
|
394 |
within the theory context. The system keeps track of incoming {\ML}
|
wenzelm@35001
|
395 |
sources and associates them with the current theory.
|
wenzelm@30296
|
396 |
|
wenzelm@30296
|
397 |
The basic internal actions of the theory database are \isa{update}, \isa{outdate}, and \isa{remove}:
|
wenzelm@30296
|
398 |
|
wenzelm@30296
|
399 |
\begin{itemize}
|
wenzelm@30296
|
400 |
|
wenzelm@30296
|
401 |
\item \isa{update\ A} introduces a link of \isa{A} with a
|
wenzelm@30296
|
402 |
\isa{theory} value of the same name; it asserts that the theory
|
wenzelm@30296
|
403 |
sources are now consistent with that value;
|
wenzelm@30296
|
404 |
|
wenzelm@30296
|
405 |
\item \isa{outdate\ A} invalidates the link of a theory database
|
wenzelm@30296
|
406 |
entry to its sources, but retains the present theory value;
|
wenzelm@30296
|
407 |
|
wenzelm@30296
|
408 |
\item \isa{remove\ A} deletes entry \isa{A} from the theory
|
wenzelm@30296
|
409 |
database.
|
wenzelm@30296
|
410 |
|
wenzelm@30296
|
411 |
\end{itemize}
|
wenzelm@30296
|
412 |
|
wenzelm@30296
|
413 |
These actions are propagated to sub- or super-graphs of a theory
|
wenzelm@30296
|
414 |
entry as expected, in order to preserve global consistency of the
|
wenzelm@30296
|
415 |
state of all loaded theories with the sources of the external store.
|
wenzelm@30296
|
416 |
This implies certain causalities between actions: \isa{update}
|
wenzelm@30296
|
417 |
or \isa{outdate} of an entry will \isa{outdate} all
|
wenzelm@30296
|
418 |
descendants; \isa{remove} will \isa{remove} all descendants.
|
wenzelm@30296
|
419 |
|
wenzelm@30296
|
420 |
\medskip There are separate user-level interfaces to operate on the
|
wenzelm@30296
|
421 |
theory database directly or indirectly. The primitive actions then
|
wenzelm@30296
|
422 |
just happen automatically while working with the system. In
|
wenzelm@30296
|
423 |
particular, processing a theory header \isa{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensures that the
|
wenzelm@30296
|
424 |
sub-graph of the collective imports \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}
|
wenzelm@30296
|
425 |
is up-to-date, too. Earlier theories are reloaded as required, with
|
wenzelm@30296
|
426 |
\isa{update} actions proceeding in topological order according to
|
wenzelm@30296
|
427 |
theory dependencies. There may be also a wave of implied \isa{outdate} actions for derived theory nodes until a stable situation
|
wenzelm@30296
|
428 |
is achieved eventually.%
|
wenzelm@30296
|
429 |
\end{isamarkuptext}%
|
wenzelm@30296
|
430 |
\isamarkuptrue%
|
wenzelm@30296
|
431 |
%
|
wenzelm@30296
|
432 |
\isadelimmlref
|
wenzelm@30296
|
433 |
%
|
wenzelm@30296
|
434 |
\endisadelimmlref
|
wenzelm@30296
|
435 |
%
|
wenzelm@30296
|
436 |
\isatagmlref
|
wenzelm@30296
|
437 |
%
|
wenzelm@30296
|
438 |
\begin{isamarkuptext}%
|
wenzelm@30296
|
439 |
\begin{mldecls}
|
wenzelm@30296
|
440 |
\indexdef{}{ML}{theory}\verb|theory: string -> theory| \\
|
wenzelm@30296
|
441 |
\indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
|
wenzelm@30296
|
442 |
\indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
|
wenzelm@37216
|
443 |
\indexdef{}{ML}{Thy\_Info.touch\_thy}\verb|Thy_Info.touch_thy: string -> unit| \\
|
wenzelm@37216
|
444 |
\indexdef{}{ML}{Thy\_Info.remove\_thy}\verb|Thy_Info.remove_thy: string -> unit| \\[1ex]
|
wenzelm@37216
|
445 |
\indexdef{}{ML}{Thy\_Info.begin\_theory}\verb|Thy_Info.begin_theory|\verb|: ... -> bool -> theory| \\
|
wenzelm@37216
|
446 |
\indexdef{}{ML}{Thy\_Info.end\_theory}\verb|Thy_Info.end_theory: theory -> unit| \\
|
wenzelm@37216
|
447 |
\indexdef{}{ML}{Thy\_Info.register\_theory}\verb|Thy_Info.register_theory: theory -> unit| \\[1ex]
|
wenzelm@30296
|
448 |
\verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
|
wenzelm@37216
|
449 |
\indexdef{}{ML}{Thy\_Info.add\_hook}\verb|Thy_Info.add_hook: (Thy_Info.action -> string -> unit) -> unit| \\
|
wenzelm@30296
|
450 |
\end{mldecls}
|
wenzelm@30296
|
451 |
|
wenzelm@30296
|
452 |
\begin{description}
|
wenzelm@30296
|
453 |
|
wenzelm@30296
|
454 |
\item \verb|theory|~\isa{A} retrieves the theory value presently
|
wenzelm@30296
|
455 |
associated with name \isa{A}. Note that the result might be
|
wenzelm@30296
|
456 |
outdated.
|
wenzelm@30296
|
457 |
|
wenzelm@30296
|
458 |
\item \verb|use_thy|~\isa{A} ensures that theory \isa{A} is fully
|
wenzelm@30296
|
459 |
up-to-date wrt.\ the external file store, reloading outdated
|
wenzelm@35001
|
460 |
ancestors as required. In batch mode, the simultaneous \verb|use_thys| should be used exclusively.
|
wenzelm@30296
|
461 |
|
wenzelm@30296
|
462 |
\item \verb|use_thys| is similar to \verb|use_thy|, but handles
|
wenzelm@30296
|
463 |
several theories simultaneously. Thus it acts like processing the
|
wenzelm@30296
|
464 |
import header of a theory, without performing the merge of the
|
wenzelm@35001
|
465 |
result. By loading a whole sub-graph of theories like that, the
|
wenzelm@35001
|
466 |
intrinsic parallelism can be exploited by the system, to speedup
|
wenzelm@35001
|
467 |
loading.
|
wenzelm@30296
|
468 |
|
wenzelm@37216
|
469 |
\item \verb|Thy_Info.touch_thy|~\isa{A} performs and \isa{outdate} action
|
wenzelm@30296
|
470 |
on theory \isa{A} and all descendants.
|
wenzelm@30296
|
471 |
|
wenzelm@37216
|
472 |
\item \verb|Thy_Info.remove_thy|~\isa{A} deletes theory \isa{A} and all
|
wenzelm@30296
|
473 |
descendants from the theory database.
|
wenzelm@30296
|
474 |
|
wenzelm@37216
|
475 |
\item \verb|Thy_Info.begin_theory| is the basic operation behind a
|
wenzelm@35001
|
476 |
\isa{{\isasymTHEORY}} header declaration. This {\ML} function is
|
wenzelm@30296
|
477 |
normally not invoked directly.
|
wenzelm@30296
|
478 |
|
wenzelm@37216
|
479 |
\item \verb|Thy_Info.end_theory| concludes the loading of a theory
|
wenzelm@30296
|
480 |
proper and stores the result in the theory database.
|
wenzelm@30296
|
481 |
|
wenzelm@37216
|
482 |
\item \verb|Thy_Info.register_theory|~\isa{text\ thy} registers an
|
wenzelm@30296
|
483 |
existing theory value with the theory loader database. There is no
|
wenzelm@30296
|
484 |
management of associated sources.
|
wenzelm@30296
|
485 |
|
wenzelm@37216
|
486 |
\item \verb|Thy_Info.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions. The function will be
|
wenzelm@30296
|
487 |
invoked with the action and theory name being involved; thus derived
|
wenzelm@30296
|
488 |
actions may be performed in associated system components, e.g.\
|
wenzelm@30296
|
489 |
maintaining the state of an editor for the theory sources.
|
wenzelm@30296
|
490 |
|
wenzelm@30296
|
491 |
The kind and order of actions occurring in practice depends both on
|
wenzelm@30296
|
492 |
user interactions and the internal process of resolving theory
|
wenzelm@30296
|
493 |
imports. Hooks should not rely on a particular policy here! Any
|
wenzelm@30296
|
494 |
exceptions raised by the hook are ignored.
|
wenzelm@30296
|
495 |
|
wenzelm@30296
|
496 |
\end{description}%
|
wenzelm@30296
|
497 |
\end{isamarkuptext}%
|
wenzelm@30296
|
498 |
\isamarkuptrue%
|
wenzelm@30296
|
499 |
%
|
wenzelm@30296
|
500 |
\endisatagmlref
|
wenzelm@30296
|
501 |
{\isafoldmlref}%
|
wenzelm@30296
|
502 |
%
|
wenzelm@30296
|
503 |
\isadelimmlref
|
wenzelm@30296
|
504 |
%
|
wenzelm@30296
|
505 |
\endisadelimmlref
|
wenzelm@30296
|
506 |
%
|
wenzelm@30296
|
507 |
\isadelimtheory
|
wenzelm@30296
|
508 |
%
|
wenzelm@30296
|
509 |
\endisadelimtheory
|
wenzelm@30296
|
510 |
%
|
wenzelm@30296
|
511 |
\isatagtheory
|
wenzelm@30296
|
512 |
\isacommand{end}\isamarkupfalse%
|
wenzelm@30296
|
513 |
%
|
wenzelm@30296
|
514 |
\endisatagtheory
|
wenzelm@30296
|
515 |
{\isafoldtheory}%
|
wenzelm@30296
|
516 |
%
|
wenzelm@30296
|
517 |
\isadelimtheory
|
wenzelm@30296
|
518 |
%
|
wenzelm@30296
|
519 |
\endisadelimtheory
|
wenzelm@30296
|
520 |
\isanewline
|
wenzelm@30296
|
521 |
\end{isabellebody}%
|
wenzelm@30296
|
522 |
%%% Local Variables:
|
wenzelm@30296
|
523 |
%%% mode: latex
|
wenzelm@30296
|
524 |
%%% TeX-master: "root"
|
wenzelm@30296
|
525 |
%%% End:
|