9 begin |
9 begin |
10 |
10 |
11 section \<open>ML expressions\<close> |
11 section \<open>ML expressions\<close> |
12 |
12 |
13 text \<open> |
13 text \<open> |
14 The Isabelle command 'ML' allows to embed Isabelle/ML source into the formal |
14 The Isabelle command \<^theory_text>\<open>ML\<close> allows to embed Isabelle/ML source into the |
15 text. It is type-checked, compiled, and run within that environment. |
15 formal text. It is type-checked, compiled, and run within that environment. |
16 |
16 |
17 Note that side-effects should be avoided, unless the intention is to change |
17 Note that side-effects should be avoided, unless the intention is to change |
18 global parameters of the run-time environment (rare). |
18 global parameters of the run-time environment (rare). |
19 |
19 |
20 ML top-level bindings are managed within the theory context. |
20 ML top-level bindings are managed within the theory context. |
27 ML \<open>val c = a + b\<close> |
27 ML \<open>val c = a + b\<close> |
28 |
28 |
29 |
29 |
30 section \<open>Antiquotations\<close> |
30 section \<open>Antiquotations\<close> |
31 |
31 |
32 text \<open>There are some language extensions (via antiquotations), as explained in |
32 text \<open> |
33 the ``Isabelle/Isar implementation manual'', chapter 0.\<close> |
33 There are some language extensions (via antiquotations), as explained in the |
|
34 ``Isabelle/Isar implementation manual'', chapter 0. |
|
35 \<close> |
34 |
36 |
35 ML \<open>length []\<close> |
37 ML \<open>length []\<close> |
36 ML \<open>@{assert} (length [] = 0)\<close> |
38 ML \<open>@{assert} (length [] = 0)\<close> |
37 |
39 |
38 |
40 |
39 text \<open>Formal entities from the surrounding context may be referenced as |
41 text \<open>Formal entities from the surrounding context may be referenced as |
40 follows:\<close> |
42 follows:\<close> |
41 |
43 |
42 term "1 + 1" -- \<open>term within theory source\<close> |
44 term "1 + 1" \<comment> \<open>term within theory source\<close> |
43 |
45 |
44 ML \<open>@{term "1 + 1"} (* term as symbolic ML datatype value *)\<close> |
46 ML \<open>@{term "1 + 1"} (* term as symbolic ML datatype value *)\<close> |
45 |
47 |
46 ML \<open>@{term "1 + (1::int)"}\<close> |
48 ML \<open>@{term "1 + (1::int)"}\<close> |
47 |
49 |
48 |
50 |
|
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 |
49 section \<open>IDE support\<close> |
59 section \<open>IDE support\<close> |
50 |
60 |
51 text \<open> |
61 text \<open> |
52 ML embedded into the Isabelle environment is connected to the Prover IDE. |
62 ML embedded into the Isabelle environment is connected to the Prover IDE. |
53 Poly/ML provides: |
63 Poly/ML provides: |
54 \begin{itemize} |
64 |
55 \item precise positions for warnings / errors |
65 \<^item> precise positions for warnings / errors |
56 \item markup for defining positions of identifiers |
66 \<^item> markup for defining positions of identifiers |
57 \item markup for inferred types of sub-expressions |
67 \<^item> markup for inferred types of sub-expressions |
58 \end{itemize} |
68 \<^item> pretty-printing of ML values with markup |
|
69 \<^item> completion of ML names |
|
70 \<^item> source-level debugger |
59 \<close> |
71 \<close> |
60 |
72 |
61 ML \<open>fn i => fn list => length list + i\<close> |
73 ML \<open>fn i => fn list => length list + i\<close> |
62 |
74 |
63 |
75 |
85 section \<open>Parallel Isabelle/ML\<close> |
97 section \<open>Parallel Isabelle/ML\<close> |
86 |
98 |
87 text \<open> |
99 text \<open> |
88 Future.fork/join/cancel manage parallel evaluation. |
100 Future.fork/join/cancel manage parallel evaluation. |
89 |
101 |
90 Note that within Isabelle theory documents, the top-level command boundary may |
102 Note that within Isabelle theory documents, the top-level command boundary |
91 not be transgressed without special precautions. This is normally managed by |
103 may not be transgressed without special precautions. This is normally |
92 the system when performing parallel proof checking.\<close> |
104 managed by the system when performing parallel proof checking. |
|
105 \<close> |
93 |
106 |
94 ML \<open> |
107 ML \<open> |
95 val x = Future.fork (fn () => ackermann 3 10); |
108 val x = Future.fork (fn () => ackermann 3 10); |
96 val y = Future.fork (fn () => ackermann 3 10); |
109 val y = Future.fork (fn () => ackermann 3 10); |
97 val z = Future.join x + Future.join y |
110 val z = Future.join x + Future.join y |
98 \<close> |
111 \<close> |
99 |
112 |
100 text \<open>The @{ML_structure Par_List} module provides high-level combinators |
113 text \<open> |
101 for parallel list operations.\<close> |
114 The @{ML_structure Par_List} module provides high-level combinators for |
|
115 parallel list operations. |
|
116 \<close> |
102 |
117 |
103 ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close> |
118 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> |
119 ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close> |
105 |
120 |
106 |
121 |
109 fun factorial :: "nat \<Rightarrow> nat" |
124 fun factorial :: "nat \<Rightarrow> nat" |
110 where |
125 where |
111 "factorial 0 = 1" |
126 "factorial 0 = 1" |
112 | "factorial (Suc n) = Suc n * factorial n" |
127 | "factorial (Suc n) = Suc n * factorial n" |
113 |
128 |
114 term "factorial 4" -- \<open>symbolic term\<close> |
129 term "factorial 4" \<comment> \<open>symbolic term\<close> |
115 value "factorial 4" -- \<open>evaluation via ML code generation in the background\<close> |
130 value "factorial 4" \<comment> \<open>evaluation via ML code generation in the background\<close> |
116 |
131 |
117 declare [[ML_source_trace]] |
132 declare [[ML_source_trace]] |
118 ML \<open>@{term "factorial 4"}\<close> -- \<open>symbolic term in ML\<close> |
133 ML \<open>@{term "factorial 4"}\<close> \<comment> \<open>symbolic term in ML\<close> |
119 ML \<open>@{code "factorial"}\<close> -- \<open>ML code from function specification\<close> |
134 ML \<open>@{code "factorial"}\<close> \<comment> \<open>ML code from function specification\<close> |
120 |
135 |
121 |
136 |
122 fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
137 fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
123 where |
138 where |
124 "ackermann 0 n = n + 1" |
139 "ackermann 0 n = n + 1" |