author | wenzelm |
Wed, 07 May 2014 12:59:15 +0200 | |
changeset 56895 | f058120aaad4 |
parent 56594 | e3a06699a13f |
child 57341 | d6393137b161 |
permissions | -rw-r--r-- |
29755 | 1 |
theory Integration |
2 |
imports Base |
|
3 |
begin |
|
18537 | 4 |
|
5 |
chapter {* System integration *} |
|
6 |
||
20447 | 7 |
section {* Isar toplevel \label{sec:isar-toplevel} *} |
18537 | 8 |
|
48974 | 9 |
text {* The Isar toplevel may be considered the central hub of the |
18537 | 10 |
Isabelle/Isar system, where all key components and sub-systems are |
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
11 |
integrated into a single read-eval-print loop of Isar commands, |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
12 |
which also incorporates the underlying ML compiler. |
18537 | 13 |
|
20451 | 14 |
Isabelle/Isar departs from the original ``LCF system architecture'' |
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
15 |
where ML was really The Meta Language for defining theories and |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
16 |
conducting proofs. Instead, ML now only serves as the |
18537 | 17 |
implementation language for the system (and user extensions), while |
20451 | 18 |
the specific Isar toplevel supports the concepts of theory and proof |
19 |
development natively. This includes the graph structure of theories |
|
20 |
and the block structure of proofs, support for unlimited undo, |
|
21 |
facilities for tracing, debugging, timing, profiling etc. |
|
18537 | 22 |
|
23 |
\medskip The toplevel maintains an implicit state, which is |
|
24 |
transformed by a sequence of transitions -- either interactively or |
|
52788 | 25 |
in batch-mode. |
18537 | 26 |
|
27 |
The toplevel state is a disjoint sum of empty @{text toplevel}, or |
|
28 |
@{text theory}, or @{text proof}. On entering the main Isar loop we |
|
29 |
start with an empty toplevel. A theory is commenced by giving a |
|
30 |
@{text \<THEORY>} header; within a theory we may issue theory |
|
20025 | 31 |
commands such as @{text \<DEFINITION>}, or state a @{text |
32 |
\<THEOREM>} to be proven. Now we are within a proof state, with a |
|
33 |
rich collection of Isar proof commands for structured proof |
|
18537 | 34 |
composition, or unstructured proof scripts. When the proof is |
35 |
concluded we get back to the theory, which is then updated by |
|
36 |
storing the resulting fact. Further theory declarations or theorem |
|
37 |
statements with proofs may follow, until we eventually conclude the |
|
38 |
theory development by issuing @{text \<END>}. The resulting theory |
|
39 |
is then stored within the theory database and we are back to the |
|
40 |
empty toplevel. |
|
41 |
||
42 |
In addition to these proper state transformations, there are also |
|
43 |
some diagnostic commands for peeking at the toplevel state without |
|
44 |
modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term}, |
|
45 |
\isakeyword{print-cases}). |
|
46 |
*} |
|
47 |
||
48 |
text %mlref {* |
|
49 |
\begin{mldecls} |
|
50 |
@{index_ML_type Toplevel.state} \\ |
|
55838 | 51 |
@{index_ML_exception Toplevel.UNDEF} \\ |
18537 | 52 |
@{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\ |
53 |
@{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\ |
|
54 |
@{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\ |
|
32833 | 55 |
@{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\ |
56 |
@{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\ |
|
18537 | 57 |
\end{mldecls} |
58 |
||
59 |
\begin{description} |
|
60 |
||
39864 | 61 |
\item Type @{ML_type Toplevel.state} represents Isar toplevel |
62 |
states, which are normally manipulated through the concept of |
|
63 |
toplevel transitions only (\secref{sec:toplevel-transition}). Also |
|
64 |
note that a raw toplevel state is subject to the same linearity |
|
65 |
restrictions as a theory context (cf.~\secref{sec:context-theory}). |
|
18537 | 66 |
|
67 |
\item @{ML Toplevel.UNDEF} is raised for undefined toplevel |
|
20451 | 68 |
operations. Many operations work only partially for certain cases, |
69 |
since @{ML_type Toplevel.state} is a sum type. |
|
18537 | 70 |
|
20451 | 71 |
\item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty |
72 |
toplevel state. |
|
18537 | 73 |
|
34931 | 74 |
\item @{ML Toplevel.theory_of}~@{text "state"} selects the |
75 |
background theory of @{text "state"}, raises @{ML Toplevel.UNDEF} |
|
76 |
for an empty toplevel state. |
|
18537 | 77 |
|
20451 | 78 |
\item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof |
79 |
state if available, otherwise raises @{ML Toplevel.UNDEF}. |
|
18537 | 80 |
|
32833 | 81 |
\item @{ML "Toplevel.timing := true"} makes the toplevel print timing |
18537 | 82 |
information for each Isar command being executed. |
83 |
||
40149
4c35be108990
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents:
39882
diff
changeset
|
84 |
\item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls |
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
85 |
low-level profiling of the underlying ML runtime system. For |
20451 | 86 |
Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space |
87 |
profiling. |
|
18537 | 88 |
|
89 |
\end{description} |
|
90 |
*} |
|
91 |
||
39882 | 92 |
text %mlantiq {* |
93 |
\begin{matharray}{rcl} |
|
94 |
@{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\ |
|
95 |
\end{matharray} |
|
96 |
||
97 |
\begin{description} |
|
98 |
||
99 |
\item @{text "@{Isar.state}"} refers to Isar toplevel state at that |
|
100 |
point --- as abstract value. |
|
101 |
||
102 |
This only works for diagnostic ML commands, such as @{command |
|
103 |
ML_val} or @{command ML_command}. |
|
104 |
||
105 |
\end{description} |
|
106 |
*} |
|
107 |
||
18537 | 108 |
|
20451 | 109 |
subsection {* Toplevel transitions \label{sec:toplevel-transition} *} |
18537 | 110 |
|
20451 | 111 |
text {* |
112 |
An Isar toplevel transition consists of a partial function on the |
|
113 |
toplevel state, with additional information for diagnostics and |
|
114 |
error reporting: there are fields for command name, source position, |
|
115 |
optional source text, as well as flags for interactive-only commands |
|
116 |
(which issue a warning in batch-mode), printing of result state, |
|
117 |
etc. |
|
18537 | 118 |
|
20451 | 119 |
The operational part is represented as the sequential union of a |
120 |
list of partial functions, which are tried in turn until the first |
|
20475 | 121 |
one succeeds. This acts like an outer case-expression for various |
34931 | 122 |
alternative state transitions. For example, \isakeyword{qed} works |
20475 | 123 |
differently for a local proofs vs.\ the global ending of the main |
124 |
proof. |
|
18537 | 125 |
|
126 |
Toplevel transitions are composed via transition transformers. |
|
127 |
Internally, Isar commands are put together from an empty transition |
|
34931 | 128 |
extended by name and source position. It is then left to the |
129 |
individual command parser to turn the given concrete syntax into a |
|
130 |
suitable transition transformer that adjoins actual operations on a |
|
131 |
theory or proof state etc. |
|
18537 | 132 |
*} |
133 |
||
134 |
text %mlref {* |
|
135 |
\begin{mldecls} |
|
136 |
@{index_ML Toplevel.keep: "(Toplevel.state -> unit) -> |
|
137 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
138 |
@{index_ML Toplevel.theory: "(theory -> theory) -> |
|
139 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
140 |
@{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) -> |
|
141 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
142 |
@{index_ML Toplevel.proof: "(Proof.state -> Proof.state) -> |
|
143 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
49864 | 144 |
@{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) -> |
18537 | 145 |
Toplevel.transition -> Toplevel.transition"} \\ |
21168
0f869edd6cc1
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents:
20491
diff
changeset
|
146 |
@{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) -> |
18537 | 147 |
Toplevel.transition -> Toplevel.transition"} \\ |
148 |
\end{mldecls} |
|
149 |
||
150 |
\begin{description} |
|
151 |
||
20451 | 152 |
\item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic |
153 |
function. |
|
18537 | 154 |
|
20451 | 155 |
\item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory |
156 |
transformer. |
|
18537 | 157 |
|
20451 | 158 |
\item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global |
159 |
goal function, which turns a theory into a proof state. The theory |
|
160 |
may be changed before entering the proof; the generic Isar goal |
|
161 |
setup includes an argument that specifies how to apply the proven |
|
162 |
result to the theory, when the proof is finished. |
|
18558 | 163 |
|
20451 | 164 |
\item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic |
165 |
proof command, with a singleton result. |
|
18537 | 166 |
|
20451 | 167 |
\item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof |
168 |
command, with zero or more result states (represented as a lazy |
|
169 |
list). |
|
18537 | 170 |
|
21168
0f869edd6cc1
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents:
20491
diff
changeset
|
171 |
\item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding |
0f869edd6cc1
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents:
20491
diff
changeset
|
172 |
proof command, that returns the resulting theory, after storing the |
0f869edd6cc1
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents:
20491
diff
changeset
|
173 |
resulting facts in the context etc. |
18537 | 174 |
|
175 |
\end{description} |
|
176 |
*} |
|
177 |
||
178 |
||
20451 | 179 |
section {* Theory database \label{sec:theory-database} *} |
18537 | 180 |
|
20451 | 181 |
text {* |
56594 | 182 |
%FIXME update |
183 |
||
20451 | 184 |
The theory database maintains a collection of theories, together |
185 |
with some administrative information about their original sources, |
|
186 |
which are held in an external store (i.e.\ some directory within the |
|
187 |
regular file system). |
|
18537 | 188 |
|
20451 | 189 |
The theory database is organized as a directed acyclic graph; |
190 |
entries are referenced by theory name. Although some additional |
|
191 |
interfaces allow to include a directory specification as well, this |
|
192 |
is only a hint to the underlying theory loader. The internal theory |
|
193 |
name space is flat! |
|
18537 | 194 |
|
195 |
Theory @{text A} is associated with the main theory file @{text |
|
196 |
A}\verb,.thy,, which needs to be accessible through the theory |
|
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
197 |
loader path. Any number of additional ML source files may be |
18537 | 198 |
associated with each theory, by declaring these dependencies in the |
199 |
theory header as @{text \<USES>}, and loading them consecutively |
|
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
200 |
within the theory context. The system keeps track of incoming ML |
34931 | 201 |
sources and associates them with the current theory. |
18537 | 202 |
|
203 |
The basic internal actions of the theory database are @{text |
|
37982 | 204 |
"update"} and @{text "remove"}: |
18537 | 205 |
|
206 |
\begin{itemize} |
|
207 |
||
208 |
\item @{text "update A"} introduces a link of @{text "A"} with a |
|
209 |
@{text "theory"} value of the same name; it asserts that the theory |
|
20451 | 210 |
sources are now consistent with that value; |
18537 | 211 |
|
20451 | 212 |
\item @{text "remove A"} deletes entry @{text "A"} from the theory |
18537 | 213 |
database. |
214 |
||
215 |
\end{itemize} |
|
216 |
||
217 |
These actions are propagated to sub- or super-graphs of a theory |
|
20451 | 218 |
entry as expected, in order to preserve global consistency of the |
219 |
state of all loaded theories with the sources of the external store. |
|
220 |
This implies certain causalities between actions: @{text "update"} |
|
37982 | 221 |
or @{text "remove"} of an entry will @{text "remove"} all |
222 |
descendants. |
|
18537 | 223 |
|
224 |
\medskip There are separate user-level interfaces to operate on the |
|
225 |
theory database directly or indirectly. The primitive actions then |
|
226 |
just happen automatically while working with the system. In |
|
227 |
particular, processing a theory header @{text "\<THEORY> A |
|
20451 | 228 |
\<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensures that the |
18537 | 229 |
sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"} |
20451 | 230 |
is up-to-date, too. Earlier theories are reloaded as required, with |
18537 | 231 |
@{text update} actions proceeding in topological order according to |
232 |
theory dependencies. There may be also a wave of implied @{text |
|
37982 | 233 |
remove} actions for derived theory nodes until a stable situation |
18537 | 234 |
is achieved eventually. |
235 |
*} |
|
236 |
||
237 |
text %mlref {* |
|
238 |
\begin{mldecls} |
|
239 |
@{index_ML use_thy: "string -> unit"} \\ |
|
24173
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset
|
240 |
@{index_ML use_thys: "string list -> unit"} \\ |
37864 | 241 |
@{index_ML Thy_Info.get_theory: "string -> theory"} \\ |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
34931
diff
changeset
|
242 |
@{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex] |
37982 | 243 |
@{index_ML Thy_Info.register_thy: "theory -> unit"} \\[1ex] |
40149
4c35be108990
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents:
39882
diff
changeset
|
244 |
@{ML_text "datatype action = Update | Remove"} \\ |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
34931
diff
changeset
|
245 |
@{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\ |
18537 | 246 |
\end{mldecls} |
247 |
||
248 |
\begin{description} |
|
249 |
||
24173
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset
|
250 |
\item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully |
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset
|
251 |
up-to-date wrt.\ the external file store, reloading outdated |
34931 | 252 |
ancestors as required. In batch mode, the simultaneous @{ML |
253 |
use_thys} should be used exclusively. |
|
18537 | 254 |
|
24173
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset
|
255 |
\item @{ML use_thys} is similar to @{ML use_thy}, but handles |
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset
|
256 |
several theories simultaneously. Thus it acts like processing the |
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset
|
257 |
import header of a theory, without performing the merge of the |
34931 | 258 |
result. By loading a whole sub-graph of theories like that, the |
259 |
intrinsic parallelism can be exploited by the system, to speedup |
|
260 |
loading. |
|
18537 | 261 |
|
37864 | 262 |
\item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value |
263 |
presently associated with name @{text A}. Note that the result |
|
264 |
might be outdated. |
|
265 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
34931
diff
changeset
|
266 |
\item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all |
18537 | 267 |
descendants from the theory database. |
268 |
||
37982 | 269 |
\item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an |
270 |
existing theory value with the theory loader database and updates |
|
271 |
source version information according to the current file-system |
|
272 |
state. |
|
18537 | 273 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
34931
diff
changeset
|
274 |
\item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text |
18537 | 275 |
f} as a hook for theory database actions. The function will be |
276 |
invoked with the action and theory name being involved; thus derived |
|
277 |
actions may be performed in associated system components, e.g.\ |
|
20451 | 278 |
maintaining the state of an editor for the theory sources. |
18537 | 279 |
|
280 |
The kind and order of actions occurring in practice depends both on |
|
281 |
user interactions and the internal process of resolving theory |
|
282 |
imports. Hooks should not rely on a particular policy here! Any |
|
20451 | 283 |
exceptions raised by the hook are ignored. |
18537 | 284 |
|
285 |
\end{description} |
|
286 |
*} |
|
30272 | 287 |
|
18537 | 288 |
end |