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