author | paulson <lp15@cam.ac.uk> |
Fri, 23 Feb 2018 09:28:14 +0000 | |
changeset 67691 | db202a00a29c |
parent 63680 | 6e1e8b5abbfa |
child 69597 | ff784d5a5bfb |
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> |
61757 | 14 |
The Isabelle command \<^theory_text>\<open>ML\<close> allows to embed Isabelle/ML source into the |
15 |
formal text. It is type-checked, compiled, and run within that environment. |
|
53935 | 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 |
|
61757 | 32 |
text \<open> |
33 |
There are some language extensions (via antiquotations), as explained in the |
|
34 |
``Isabelle/Isar implementation manual'', chapter 0. |
|
35 |
\<close> |
|
53935 | 36 |
|
58616 | 37 |
ML \<open>length []\<close> |
38 |
ML \<open>@{assert} (length [] = 0)\<close> |
|
53935 | 39 |
|
40 |
||
58616 | 41 |
text \<open>Formal entities from the surrounding context may be referenced as |
42 |
follows:\<close> |
|
43 |
||
61757 | 44 |
term "1 + 1" \<comment> \<open>term within theory source\<close> |
58616 | 45 |
|
46 |
ML \<open>@{term "1 + 1"} (* term as symbolic ML datatype value *)\<close> |
|
53935 | 47 |
|
58616 | 48 |
ML \<open>@{term "1 + (1::int)"}\<close> |
49 |
||
50 |
||
61757 | 51 |
ML \<open> |
52 |
(* formal source with position information *) |
|
53 |
val s = \<open>1 + 1\<close>; |
|
54 |
||
55 |
(* read term via old-style string interface *) |
|
56 |
val t = Syntax.read_term @{context} (Syntax.implode_input s); |
|
57 |
\<close> |
|
58 |
||
62910
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
61757
diff
changeset
|
59 |
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
61757
diff
changeset
|
60 |
section \<open>Recursive ML evaluation\<close> |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
61757
diff
changeset
|
61 |
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
61757
diff
changeset
|
62 |
ML \<open> |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
61757
diff
changeset
|
63 |
ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>; |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
61757
diff
changeset
|
64 |
ML \<open>val b = @{thm sym}\<close>; |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
61757
diff
changeset
|
65 |
val c = @{thm trans} |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
61757
diff
changeset
|
66 |
val thms = [a, b, c]; |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
61757
diff
changeset
|
67 |
\<close> |
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
61757
diff
changeset
|
68 |
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
61757
diff
changeset
|
69 |
|
58616 | 70 |
section \<open>IDE support\<close> |
71 |
||
72 |
text \<open> |
|
53935 | 73 |
ML embedded into the Isabelle environment is connected to the Prover IDE. |
74 |
Poly/ML provides: |
|
61757 | 75 |
|
76 |
\<^item> precise positions for warnings / errors |
|
77 |
\<^item> markup for defining positions of identifiers |
|
78 |
\<^item> markup for inferred types of sub-expressions |
|
79 |
\<^item> pretty-printing of ML values with markup |
|
80 |
\<^item> completion of ML names |
|
81 |
\<^item> source-level debugger |
|
58616 | 82 |
\<close> |
53935 | 83 |
|
58616 | 84 |
ML \<open>fn i => fn list => length list + i\<close> |
53935 | 85 |
|
86 |
||
58616 | 87 |
section \<open>Example: factorial and ackermann function in Isabelle/ML\<close> |
53935 | 88 |
|
58616 | 89 |
ML \<open> |
53935 | 90 |
fun factorial 0 = 1 |
91 |
| factorial n = n * factorial (n - 1) |
|
58616 | 92 |
\<close> |
53935 | 93 |
|
58616 | 94 |
ML \<open>factorial 42\<close> |
95 |
ML \<open>factorial 10000 div factorial 9999\<close> |
|
53935 | 96 |
|
63680 | 97 |
text \<open>See \<^url>\<open>http://mathworld.wolfram.com/AckermannFunction.html\<close>.\<close> |
58616 | 98 |
|
99 |
ML \<open> |
|
53935 | 100 |
fun ackermann 0 n = n + 1 |
101 |
| ackermann m 0 = ackermann (m - 1) 1 |
|
102 |
| ackermann m n = ackermann (m - 1) (ackermann m (n - 1)) |
|
58616 | 103 |
\<close> |
53935 | 104 |
|
58616 | 105 |
ML \<open>timeit (fn () => ackermann 3 10)\<close> |
53935 | 106 |
|
107 |
||
58616 | 108 |
section \<open>Parallel Isabelle/ML\<close> |
53935 | 109 |
|
58616 | 110 |
text \<open> |
53935 | 111 |
Future.fork/join/cancel manage parallel evaluation. |
112 |
||
61757 | 113 |
Note that within Isabelle theory documents, the top-level command boundary |
114 |
may not be transgressed without special precautions. This is normally |
|
115 |
managed by the system when performing parallel proof checking. |
|
116 |
\<close> |
|
53935 | 117 |
|
58616 | 118 |
ML \<open> |
53935 | 119 |
val x = Future.fork (fn () => ackermann 3 10); |
120 |
val y = Future.fork (fn () => ackermann 3 10); |
|
121 |
val z = Future.join x + Future.join y |
|
58616 | 122 |
\<close> |
53935 | 123 |
|
61757 | 124 |
text \<open> |
125 |
The @{ML_structure Par_List} module provides high-level combinators for |
|
126 |
parallel list operations. |
|
127 |
\<close> |
|
53935 | 128 |
|
58616 | 129 |
ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close> |
130 |
ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close> |
|
53935 | 131 |
|
132 |
||
58616 | 133 |
section \<open>Function specifications in Isabelle/HOL\<close> |
53935 | 134 |
|
135 |
fun factorial :: "nat \<Rightarrow> nat" |
|
136 |
where |
|
137 |
"factorial 0 = 1" |
|
138 |
| "factorial (Suc n) = Suc n * factorial n" |
|
139 |
||
61757 | 140 |
term "factorial 4" \<comment> \<open>symbolic term\<close> |
141 |
value "factorial 4" \<comment> \<open>evaluation via ML code generation in the background\<close> |
|
53935 | 142 |
|
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
|
143 |
declare [[ML_source_trace]] |
61757 | 144 |
ML \<open>@{term "factorial 4"}\<close> \<comment> \<open>symbolic term in ML\<close> |
145 |
ML \<open>@{code "factorial"}\<close> \<comment> \<open>ML code from function specification\<close> |
|
53935 | 146 |
|
147 |
||
148 |
fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
149 |
where |
|
150 |
"ackermann 0 n = n + 1" |
|
151 |
| "ackermann (Suc m) 0 = ackermann m 1" |
|
152 |
| "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)" |
|
153 |
||
154 |
value "ackermann 3 5" |
|
155 |
||
156 |
end |
|
157 |