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