28 merely reflect snapshots that are never really up-to-date.} *} |
28 merely reflect snapshots that are never really up-to-date.} *} |
29 |
29 |
30 |
30 |
31 section {* SML embedded into Isabelle/Isar *} |
31 section {* SML embedded into Isabelle/Isar *} |
32 |
32 |
33 text {* ML and Isabelle/Isar are intertwined via an open-ended |
33 text {* ML and Isar are intertwined via an open-ended bootstrap |
34 bootstrap process that provides more and more programming facilities |
34 process that provides more and more programming facilities and |
35 and logical content in an alternating manner. Bootstrapping starts |
35 logical content in an alternating manner. Bootstrapping starts from |
36 from the raw environment of existing implementations of Standard ML |
36 the raw environment of existing implementations of Standard ML |
37 (most notably Poly/ML but also SML/NJ). Isabelle/Pure marks the |
37 (mainly Poly/ML, but also SML/NJ). |
38 point where the original ML toplevel is superseded by the Isar |
|
39 toplevel that maintains a uniform environment for arbitrary ML |
|
40 values (see also \secref{sec:context}). This formal context holds |
|
41 logical entities as well as ML compiler bindings, among many other |
|
42 things. |
|
43 |
38 |
44 Object-logics, such as Isabelle/HOL, are built within the |
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. |
|
45 |
|
46 Object-logics such as Isabelle/HOL are built within the |
45 Isabelle/ML/Isar environment of Pure by introducing suitable |
47 Isabelle/ML/Isar environment of Pure by introducing suitable |
46 theories with associated ML text (either inlined or as separate |
48 theories with associated ML text, either inlined or as separate |
47 files). |
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. |
|
53 *} |
48 |
54 |
49 Implementing tools within the Isabelle framework means to work with |
|
50 ML within the Isar context in the same manner: raw Standard ML is |
|
51 normally never encountered again. |
|
52 *} |
|
53 |
55 |
54 section {* Isar ML commands *} |
56 section {* Isar ML commands *} |
55 |
57 |
56 text {* The primary Isar source language provides various facilities |
58 text {* The primary Isar source language provides various facilities |
57 to open a ``window'' to the underlying ML compiler. Especially see |
59 to open a ``window'' to the underlying ML compiler. Especially see |
58 @{command_ref "use"} and @{command_ref "ML"} in |
60 @{command_ref "use"} and @{command_ref "ML"}, which work exactly the |
59 \cite{isabelle-isar-ref} --- both commands are exactly the same, |
61 same way, only the source text is provided via a file vs.\ inlined, |
60 only the source text is provided via a file vs.\ inlined, |
62 respectively. Apart from embedding ML into the main theory |
61 respectively. *} |
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 *} |
62 |
69 |
63 text %mlex {* The following artificial example demonstrates basic ML |
70 text %mlex {* The following artificial example demonstrates some ML |
64 programming within the implicit Isar theory context, without |
71 toplevel declarations within the implicit Isar theory context. This |
65 referring to logical entities yet. |
72 is regular functional programming without referring to logical |
|
73 entities yet. |
66 *} |
74 *} |
67 |
75 |
68 ML {* |
76 ML {* |
69 fun factorial 0 = 1 |
77 fun factorial 0 = 1 |
70 | factorial n = n * factorial (n - 1) |
78 | factorial n = n * factorial (n - 1) |
71 *} |
79 *} |
72 |
80 |
73 text {* \noindent The ML binding of @{ML factorial} is really managed |
81 text {* \noindent Here the ML environment is really managed by |
74 by the Isabelle environment, i.e.\ that function is not yet |
82 Isabelle, i.e.\ the @{ML factorial} function is not yet accessible |
75 accessible in the preceding paragraph, nor in a different theory |
83 in the preceding paragraph, nor in a different theory that is |
76 that is independent from the current one in the import hierarchy. |
84 independent from the current one in the import hierarchy. |
77 |
85 |
78 Removing the above ML declaration from the source text will remove |
86 Removing the above ML declaration from the source text will remove |
79 any trace of this definition as expected. The Isabelle/ML toplevel |
87 any trace of this definition as expected. The Isabelle/ML toplevel |
80 environment is managed in a \emph{stateless} way: unlike the raw ML |
88 environment is managed in a \emph{stateless} way: unlike the raw ML |
81 toplevel, there are no global side-effects involved. |
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.} |
82 |
94 |
83 \bigskip The next example shows how to embed ML into Isar proofs. |
95 \bigskip The next example shows how to embed ML into Isar proofs. |
84 Instead of @{command_ref "ML"} for theory text, we use @{command_ref |
96 Instead of @{command_ref "ML"} for theory mode, we use @{command_ref |
85 "ML_prf"}: its effect on the ML environment is local to the whole |
97 "ML_prf"} for proof mode. As illustrated below, its effect on the |
86 proof body, while ignoring its internal block structure. *} |
98 ML environment is local to the whole proof body, while ignoring its |
|
99 internal block structure. |
|
100 *} |
87 |
101 |
88 example_proof |
102 example_proof |
89 ML_prf {* val a = 1 *} |
103 ML_prf {* val a = 1 *} |
90 { -- {* proof block ignored by ML environment *} |
104 { -- {* Isar block structure ignored by ML environment *} |
91 ML_prf {* val b = a + 1 *} |
105 ML_prf {* val b = a + 1 *} |
92 } -- {* proof block ignored by ML environment *} |
106 } -- {* Isar block structure ignored by ML environment *} |
93 ML_prf {* val c = b + 1 *} |
107 ML_prf {* val c = b + 1 *} |
94 qed |
108 qed |
95 |
109 |
96 text {* \noindent By side-stepping the normal Isar scoping rules, |
110 text {* \noindent By side-stepping the normal scoping rules for Isar |
97 embedded ML code can refer to the different contexts explicitly, and |
111 proof blocks, embedded ML code can refer to the different contexts |
98 manipulate corresponding entities, e.g.\ export a fact from a |
112 explicitly, and manipulate corresponding entities, e.g.\ export a |
99 block context. |
113 fact from a block context. |
100 |
114 |
101 \bigskip The diagnostic ML commands @{command_ref ML_val} and |
115 \bigskip Two further ML commands are useful in certain situations: |
102 @{command_ref ML_command} do not affect the underlying context, and |
116 @{command_ref ML_val} and @{command_ref ML_command} are both |
103 can be used anywhere, e.g.\ to produce long strings of digits as |
117 \emph{diagnostic} in the sense that there is no effect on the |
104 follows: *} |
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 *} |
105 |
124 |
106 ML_val {* factorial 100 *} |
125 ML_val {* factorial 100 *} |
107 ML_command {* writeln (string_of_int (factorial 100)) *} |
126 ML_command {* writeln (string_of_int (factorial 100)) *} |
108 |
127 |
109 example_proof |
128 example_proof |
110 ML_val {* factorial 100 *} |
129 ML_val {* factorial 100 *} (* FIXME check/fix indentation *) |
111 ML_command {* writeln (string_of_int (factorial 100)) *} |
130 ML_command {* writeln (string_of_int (factorial 100)) *} |
112 qed |
131 qed |
113 |
|
114 text {* \noindent Note that @{command ML_val} and @{command |
|
115 ML_command} only differ in the output (or lack thereof) of ML |
|
116 toplevel results. *} |
|
117 |
132 |
118 |
133 |
119 section {* Compile-time context *} |
134 section {* Compile-time context *} |
120 |
135 |
121 text FIXME |
136 text FIXME |