author | wenzelm |
Sun, 02 Nov 2014 18:21:45 +0100 | |
changeset 58889 | 5b7a9633cfa8 |
parent 58616 | 4257a7f2bf39 |
child 61757 | 0d399131008f |
permissions | -rw-r--r-- |
53935 | 1 |
(* Title: HOL/ex/ML.thy |
2 |
Author: Makarius |
|
3 |
*) |
|
4 |
||
58889 | 5 |
section \<open>Isabelle/ML basics\<close> |
53935 | 6 |
|
7 |
theory "ML" |
|
8 |
imports Main |
|
9 |
begin |
|
10 |
||
58616 | 11 |
section \<open>ML expressions\<close> |
53935 | 12 |
|
58616 | 13 |
text \<open> |
53935 | 14 |
The Isabelle command 'ML' allows to embed Isabelle/ML source into the formal |
15 |
text. It is type-checked, compiled, and run within that environment. |
|
16 |
||
17 |
Note that side-effects should be avoided, unless the intention is to change |
|
18 |
global parameters of the run-time environment (rare). |
|
19 |
||
20 |
ML top-level bindings are managed within the theory context. |
|
58616 | 21 |
\<close> |
53935 | 22 |
|
58616 | 23 |
ML \<open>1 + 1\<close> |
53935 | 24 |
|
58616 | 25 |
ML \<open>val a = 1\<close> |
26 |
ML \<open>val b = 1\<close> |
|
27 |
ML \<open>val c = a + b\<close> |
|
53935 | 28 |
|
29 |
||
58616 | 30 |
section \<open>Antiquotations\<close> |
53935 | 31 |
|
58616 | 32 |
text \<open>There are some language extensions (via antiquotations), as explained in |
33 |
the ``Isabelle/Isar implementation manual'', chapter 0.\<close> |
|
53935 | 34 |
|
58616 | 35 |
ML \<open>length []\<close> |
36 |
ML \<open>@{assert} (length [] = 0)\<close> |
|
53935 | 37 |
|
38 |
||
58616 | 39 |
text \<open>Formal entities from the surrounding context may be referenced as |
40 |
follows:\<close> |
|
41 |
||
42 |
term "1 + 1" -- \<open>term within theory source\<close> |
|
43 |
||
44 |
ML \<open>@{term "1 + 1"} (* term as symbolic ML datatype value *)\<close> |
|
53935 | 45 |
|
58616 | 46 |
ML \<open>@{term "1 + (1::int)"}\<close> |
47 |
||
48 |
||
49 |
section \<open>IDE support\<close> |
|
50 |
||
51 |
text \<open> |
|
53935 | 52 |
ML embedded into the Isabelle environment is connected to the Prover IDE. |
53 |
Poly/ML provides: |
|
53948 | 54 |
\begin{itemize} |
55 |
\item precise positions for warnings / errors |
|
56 |
\item markup for defining positions of identifiers |
|
57 |
\item markup for inferred types of sub-expressions |
|
58 |
\end{itemize} |
|
58616 | 59 |
\<close> |
53935 | 60 |
|
58616 | 61 |
ML \<open>fn i => fn list => length list + i\<close> |
53935 | 62 |
|
63 |
||
58616 | 64 |
section \<open>Example: factorial and ackermann function in Isabelle/ML\<close> |
53935 | 65 |
|
58616 | 66 |
ML \<open> |
53935 | 67 |
fun factorial 0 = 1 |
68 |
| factorial n = n * factorial (n - 1) |
|
58616 | 69 |
\<close> |
53935 | 70 |
|
58616 | 71 |
ML \<open>factorial 42\<close> |
72 |
ML \<open>factorial 10000 div factorial 9999\<close> |
|
53935 | 73 |
|
58616 | 74 |
text \<open>See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}\<close> |
75 |
||
76 |
ML \<open> |
|
53935 | 77 |
fun ackermann 0 n = n + 1 |
78 |
| ackermann m 0 = ackermann (m - 1) 1 |
|
79 |
| ackermann m n = ackermann (m - 1) (ackermann m (n - 1)) |
|
58616 | 80 |
\<close> |
53935 | 81 |
|
58616 | 82 |
ML \<open>timeit (fn () => ackermann 3 10)\<close> |
53935 | 83 |
|
84 |
||
58616 | 85 |
section \<open>Parallel Isabelle/ML\<close> |
53935 | 86 |
|
58616 | 87 |
text \<open> |
53935 | 88 |
Future.fork/join/cancel manage parallel evaluation. |
89 |
||
90 |
Note that within Isabelle theory documents, the top-level command boundary may |
|
91 |
not be transgressed without special precautions. This is normally managed by |
|
58616 | 92 |
the system when performing parallel proof checking.\<close> |
53935 | 93 |
|
58616 | 94 |
ML \<open> |
53935 | 95 |
val x = Future.fork (fn () => ackermann 3 10); |
96 |
val y = Future.fork (fn () => ackermann 3 10); |
|
97 |
val z = Future.join x + Future.join y |
|
58616 | 98 |
\<close> |
53935 | 99 |
|
58616 | 100 |
text \<open>The @{ML_structure Par_List} module provides high-level combinators |
101 |
for parallel list operations.\<close> |
|
53935 | 102 |
|
58616 | 103 |
ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close> |
104 |
ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close> |
|
53935 | 105 |
|
106 |
||
58616 | 107 |
section \<open>Function specifications in Isabelle/HOL\<close> |
53935 | 108 |
|
109 |
fun factorial :: "nat \<Rightarrow> nat" |
|
110 |
where |
|
111 |
"factorial 0 = 1" |
|
112 |
| "factorial (Suc n) = Suc n * factorial n" |
|
113 |
||
58616 | 114 |
term "factorial 4" -- \<open>symbolic term\<close> |
115 |
value "factorial 4" -- \<open>evaluation via ML code generation in the background\<close> |
|
53935 | 116 |
|
56279
b4d874f6c6be
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
wenzelm
parents:
55837
diff
changeset
|
117 |
declare [[ML_source_trace]] |
58616 | 118 |
ML \<open>@{term "factorial 4"}\<close> -- \<open>symbolic term in ML\<close> |
119 |
ML \<open>@{code "factorial"}\<close> -- \<open>ML code from function specification\<close> |
|
53935 | 120 |
|
121 |
||
122 |
fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
123 |
where |
|
124 |
"ackermann 0 n = n + 1" |
|
125 |
| "ackermann (Suc m) 0 = ackermann m 1" |
|
126 |
| "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)" |
|
127 |
||
128 |
value "ackermann 3 5" |
|
129 |
||
130 |
end |
|
131 |