53935
|
1 |
(* Title: HOL/ex/ML.thy
|
|
2 |
Author: Makarius
|
|
3 |
*)
|
|
4 |
|
|
5 |
header {* Isabelle/ML basics *}
|
|
6 |
|
|
7 |
theory "ML"
|
|
8 |
imports Main
|
|
9 |
begin
|
|
10 |
|
|
11 |
section {* ML expressions *}
|
|
12 |
|
|
13 |
text {*
|
|
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.
|
|
21 |
*}
|
|
22 |
|
|
23 |
ML {* 1 + 1 *}
|
|
24 |
|
|
25 |
ML {* val a = 1 *}
|
|
26 |
ML {* val b = 1 *}
|
|
27 |
ML {* val c = a + b *}
|
|
28 |
|
|
29 |
|
|
30 |
section {* Antiquotations *}
|
|
31 |
|
|
32 |
text {* There are some language extensions (via antiquotations), as explained in
|
|
33 |
the "Isabelle/Isar implementation manual", chapter 0. *}
|
|
34 |
|
|
35 |
ML {* length [] *}
|
|
36 |
ML {* @{assert} (length [] = 0) *}
|
|
37 |
|
|
38 |
|
|
39 |
text {* Formal entities from the surrounding context may be referenced as
|
|
40 |
follows: *}
|
|
41 |
|
|
42 |
term "1 + 1" -- "term within theory source"
|
|
43 |
|
|
44 |
ML {*
|
|
45 |
@{term "1 + 1"} (* term as symbolic ML datatype value *)
|
|
46 |
*}
|
|
47 |
|
|
48 |
ML {*
|
|
49 |
@{term "1 + (1::int)"}
|
|
50 |
*}
|
|
51 |
|
|
52 |
|
|
53 |
section {* IDE support *}
|
|
54 |
|
|
55 |
text {*
|
|
56 |
ML embedded into the Isabelle environment is connected to the Prover IDE.
|
|
57 |
Poly/ML provides:
|
53948
|
58 |
\begin{itemize}
|
|
59 |
\item precise positions for warnings / errors
|
|
60 |
\item markup for defining positions of identifiers
|
|
61 |
\item markup for inferred types of sub-expressions
|
|
62 |
\end{itemize}
|
53935
|
63 |
*}
|
|
64 |
|
|
65 |
ML {* fn i => fn list => length list + i *}
|
|
66 |
|
|
67 |
|
|
68 |
section {* Example: factorial and ackermann function in Isabelle/ML *}
|
|
69 |
|
|
70 |
ML {*
|
|
71 |
fun factorial 0 = 1
|
|
72 |
| factorial n = n * factorial (n - 1)
|
|
73 |
*}
|
|
74 |
|
|
75 |
ML "factorial 42"
|
|
76 |
ML "factorial 10000 div factorial 9999"
|
|
77 |
|
|
78 |
text {*
|
54703
|
79 |
See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}
|
53935
|
80 |
*}
|
|
81 |
|
|
82 |
ML {*
|
|
83 |
fun ackermann 0 n = n + 1
|
|
84 |
| ackermann m 0 = ackermann (m - 1) 1
|
|
85 |
| ackermann m n = ackermann (m - 1) (ackermann m (n - 1))
|
|
86 |
*}
|
|
87 |
|
|
88 |
ML {* timeit (fn () => ackermann 3 10) *}
|
|
89 |
|
|
90 |
|
|
91 |
section {* Parallel Isabelle/ML *}
|
|
92 |
|
|
93 |
text {*
|
|
94 |
Future.fork/join/cancel manage parallel evaluation.
|
|
95 |
|
|
96 |
Note that within Isabelle theory documents, the top-level command boundary may
|
|
97 |
not be transgressed without special precautions. This is normally managed by
|
|
98 |
the system when performing parallel proof checking. *}
|
|
99 |
|
|
100 |
ML {*
|
|
101 |
val x = Future.fork (fn () => ackermann 3 10);
|
|
102 |
val y = Future.fork (fn () => ackermann 3 10);
|
|
103 |
val z = Future.join x + Future.join y
|
|
104 |
*}
|
|
105 |
|
|
106 |
text {*
|
|
107 |
The @{ML_struct Par_List} module provides high-level combinators for
|
|
108 |
parallel list operations. *}
|
|
109 |
|
|
110 |
ML {* timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10)) *}
|
|
111 |
ML {* timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10)) *}
|
|
112 |
|
|
113 |
|
|
114 |
section {* Function specifications in Isabelle/HOL *}
|
|
115 |
|
|
116 |
fun factorial :: "nat \<Rightarrow> nat"
|
|
117 |
where
|
|
118 |
"factorial 0 = 1"
|
|
119 |
| "factorial (Suc n) = Suc n * factorial n"
|
|
120 |
|
|
121 |
term "factorial 4" -- "symbolic term"
|
|
122 |
value "factorial 4" -- "evaluation via ML code generation in the background"
|
|
123 |
|
|
124 |
declare [[ML_trace]]
|
|
125 |
ML {* @{term "factorial 4"} *} -- "symbolic term in ML"
|
|
126 |
ML {* @{code "factorial"} *} -- "ML code from function specification"
|
|
127 |
|
|
128 |
|
|
129 |
fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat"
|
|
130 |
where
|
|
131 |
"ackermann 0 n = n + 1"
|
|
132 |
| "ackermann (Suc m) 0 = ackermann m 1"
|
|
133 |
| "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)"
|
|
134 |
|
|
135 |
value "ackermann 3 5"
|
|
136 |
|
|
137 |
end
|
|
138 |
|