author | wenzelm |
Fri, 08 Oct 2010 17:41:51 +0100 | |
changeset 39825 | f9066b94bf07 |
parent 39824 | 679075565542 |
child 39827 | d829ce302ca4 |
permissions | -rw-r--r-- |
29755 | 1 |
theory "ML" |
2 |
imports Base |
|
3 |
begin |
|
18538 | 4 |
|
39822 | 5 |
chapter {* Isabelle/ML *} |
20489 | 6 |
|
39823 | 7 |
text {* Isabelle/ML is best understood as a certain culture based on |
8 |
Standard ML. Thus it is not a new programming language, but a |
|
9 |
certain way to use SML at an advanced level within the Isabelle |
|
10 |
environment. This covers a variety of aspects that are geared |
|
11 |
towards an efficient and robust platform for applications of formal |
|
12 |
logic with fully foundational proof construction --- according to |
|
13 |
the well-known \emph{LCF principle}. There are specific library |
|
14 |
modules and infrastructure to address the needs for such difficult |
|
15 |
tasks. For example, the raw parallel programming model of Poly/ML |
|
16 |
is presented as considerably more abstract concept of \emph{future |
|
17 |
values}, which is then used to augment the inference kernel, proof |
|
18 |
interpreter, and theory loader accordingly. |
|
19 |
||
20 |
The main aspects of Isabelle/ML are introduced below. These |
|
21 |
first-hand explanations should help to understand how proper |
|
22 |
Isabelle/ML is to be read and written, and to get access to the |
|
23 |
wealth of experience that is expressed in the source text and its |
|
24 |
history of changes.\footnote{See |
|
25 |
\url{http://isabelle.in.tum.de/repos/isabelle} for the full |
|
26 |
Mercurial history. There are symbolic tags to refer to official |
|
27 |
Isabelle releases, as opposed to arbitrary \emph{tip} versions that |
|
28 |
merely reflect snapshots that are never really up-to-date.} *} |
|
29 |
||
30 |
||
31 |
section {* SML embedded into Isabelle/Isar *} |
|
32 |
||
39824 | 33 |
text {* ML and Isar are intertwined via an open-ended bootstrap |
34 |
process that provides more and more programming facilities and |
|
35 |
logical content in an alternating manner. Bootstrapping starts from |
|
36 |
the raw environment of existing implementations of Standard ML |
|
37 |
(mainly Poly/ML, but also SML/NJ). |
|
39823 | 38 |
|
39824 | 39 |
Isabelle/Pure marks the point where the original ML toplevel is |
40 |
superseded by the Isar toplevel that maintains a uniform environment |
|
41 |
for arbitrary ML values (see also \secref{sec:context}). This |
|
42 |
formal context holds logical entities as well as ML compiler |
|
43 |
bindings, among many other things. Raw Standard ML is never |
|
44 |
encountered again after the initial bootstrap of Isabelle/Pure. |
|
39823 | 45 |
|
39824 | 46 |
Object-logics such as Isabelle/HOL are built within the |
47 |
Isabelle/ML/Isar environment of Pure by introducing suitable |
|
48 |
theories with associated ML text, either inlined or as separate |
|
49 |
files. Thus Isabelle/HOL is defined as a regular user-space |
|
50 |
application within the Isabelle framework. Further add-on tools can |
|
51 |
be implemented in ML within the Isar context in the same manner: ML |
|
52 |
is part of the regular user-space repertoire of Isabelle. |
|
39823 | 53 |
*} |
54 |
||
39824 | 55 |
|
39823 | 56 |
section {* Isar ML commands *} |
57 |
||
58 |
text {* The primary Isar source language provides various facilities |
|
59 |
to open a ``window'' to the underlying ML compiler. Especially see |
|
39824 | 60 |
@{command_ref "use"} and @{command_ref "ML"}, which work exactly the |
61 |
same way, only the source text is provided via a file vs.\ inlined, |
|
62 |
respectively. Apart from embedding ML into the main theory |
|
63 |
definition like that, there are many more commands that refer to ML |
|
64 |
source, such as @{command_ref setup} or @{command_ref declaration}. |
|
65 |
An example of even more fine-grained embedding of ML into Isar is |
|
66 |
the proof method @{method_ref tactic}, which refines the pending goal state |
|
67 |
via a given expression of type @{ML_type tactic}. |
|
68 |
*} |
|
39823 | 69 |
|
39824 | 70 |
text %mlex {* The following artificial example demonstrates some ML |
71 |
toplevel declarations within the implicit Isar theory context. This |
|
72 |
is regular functional programming without referring to logical |
|
73 |
entities yet. |
|
39823 | 74 |
*} |
75 |
||
76 |
ML {* |
|
77 |
fun factorial 0 = 1 |
|
78 |
| factorial n = n * factorial (n - 1) |
|
79 |
*} |
|
80 |
||
39824 | 81 |
text {* \noindent Here the ML environment is really managed by |
82 |
Isabelle, i.e.\ the @{ML factorial} function is not yet accessible |
|
83 |
in the preceding paragraph, nor in a different theory that is |
|
84 |
independent from the current one in the import hierarchy. |
|
39823 | 85 |
|
86 |
Removing the above ML declaration from the source text will remove |
|
87 |
any trace of this definition as expected. The Isabelle/ML toplevel |
|
88 |
environment is managed in a \emph{stateless} way: unlike the raw ML |
|
39824 | 89 |
toplevel or similar command loops of Computer Algebra systems, there |
90 |
are no global side-effects involved here.\footnote{Such a stateless |
|
91 |
compilation environment is also a prerequisite for robust parallel |
|
92 |
compilation within independent nodes of the implicit theory |
|
93 |
development graph.} |
|
39823 | 94 |
|
95 |
\bigskip The next example shows how to embed ML into Isar proofs. |
|
39824 | 96 |
Instead of @{command_ref "ML"} for theory mode, we use @{command_ref |
97 |
"ML_prf"} for proof mode. As illustrated below, its effect on the |
|
98 |
ML environment is local to the whole proof body, while ignoring its |
|
99 |
internal block structure. |
|
100 |
*} |
|
39823 | 101 |
|
102 |
example_proof |
|
103 |
ML_prf {* val a = 1 *} |
|
39824 | 104 |
{ -- {* Isar block structure ignored by ML environment *} |
39823 | 105 |
ML_prf {* val b = a + 1 *} |
39824 | 106 |
} -- {* Isar block structure ignored by ML environment *} |
39823 | 107 |
ML_prf {* val c = b + 1 *} |
108 |
qed |
|
109 |
||
39824 | 110 |
text {* \noindent By side-stepping the normal scoping rules for Isar |
111 |
proof blocks, embedded ML code can refer to the different contexts |
|
112 |
explicitly, and manipulate corresponding entities, e.g.\ export a |
|
113 |
fact from a block context. |
|
39823 | 114 |
|
39824 | 115 |
\bigskip Two further ML commands are useful in certain situations: |
116 |
@{command_ref ML_val} and @{command_ref ML_command} are both |
|
117 |
\emph{diagnostic} in the sense that there is no effect on the |
|
118 |
underlying environment, and can thus used anywhere (even outside a |
|
119 |
theory). The examples below produce long strings of digits by |
|
120 |
invoking @{ML factorial}: @{command ML_val} already takes care of |
|
121 |
printing the ML toplevel result, but @{command ML_command} is silent |
|
122 |
so we produce an explicit output message. |
|
123 |
*} |
|
39823 | 124 |
|
125 |
ML_val {* factorial 100 *} |
|
126 |
ML_command {* writeln (string_of_int (factorial 100)) *} |
|
127 |
||
128 |
example_proof |
|
39824 | 129 |
ML_val {* factorial 100 *} (* FIXME check/fix indentation *) |
39823 | 130 |
ML_command {* writeln (string_of_int (factorial 100)) *} |
131 |
qed |
|
132 |
||
133 |
||
134 |
section {* Compile-time context *} |
|
135 |
||
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
136 |
text {* Whenever the ML compiler is invoked within Isabelle/Isar, the |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
137 |
formal context is passed as a thread-local reference variable. Thus |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
138 |
ML code may access the theory context during compilation, by reading |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
139 |
or writing the (local) theory under construction. Note that such |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
140 |
direct access to the compile-time context is rare; in practice it is |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
141 |
typically via some derived ML functions. |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
142 |
*} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
143 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
144 |
text %mlref {* |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
145 |
\begin{mldecls} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
146 |
@{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\ |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
147 |
@{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\ |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
148 |
\end{mldecls} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
149 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
150 |
\begin{description} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
151 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
152 |
\item @{ML "ML_Context.the_generic_context ()"} refers to the theory |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
153 |
context of the ML toplevel --- at compile time. ML code needs to |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
154 |
take care to refer to @{ML "ML_Context.the_generic_context ()"} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
155 |
correctly. Recall that evaluation of a function body is delayed |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
156 |
until actual runtime. |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
157 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
158 |
\item @{ML "Context.>>"}~@{text f} applies context transformation |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
159 |
@{text f} to the implicit context of the ML toplevel. |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
160 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
161 |
\end{description} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
162 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
163 |
It is very important to note that the above functions are really |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
164 |
restricted to the compile time, even though the ML compiler is |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
165 |
invoked at runtime. The majority of ML code either uses static |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
166 |
antiquotations (\secref{sec:ML-antiq}) or refers to the theory or |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
167 |
proof context at run-time, by explicit functional abstraction. |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
168 |
*} |
39823 | 169 |
|
170 |
||
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
171 |
section {* Antiquotations \label{sec:ML-antiq} *} |
39823 | 172 |
|
173 |
text FIXME |
|
174 |
||
175 |
||
30270
61811c9224a6
dummy changes to produce a new changeset of these files;
wenzelm
parents:
29755
diff
changeset
|
176 |
end |