text\<open>
The Isabelle command \<^theory_text>\<open>ML\<close> allows to embed Isabelle/ML source into the
formal text. It is type-checked, compiled, and run within that environment.
Note that side-effects should be avoided, unless the intention isto change global parameters of the run-time environment (rare).
ML top-level bindings are managed within the theorycontext. \<close>
ML \<open>1 + 1\<close>
ML \<open>val a = 1\<close>
ML \<open>val b = 1\<close>
ML \<open>val c = a + b\<close>
subsection \<open>Antiquotations\<close>
text\<open>
There are some language extensions (via antiquotations), as explained in the
``Isabelle/Isar implementation manual'', chapter 0. \<close>
ML \<open>length []\<close>
ML \<open>\<^assert> (length [] = 0)\<close>
text\<open>Formal entities from the surrounding context may be referenced as
follows:\<close>
term"1 + 1"\<comment> \<open>term within theory source\<close>
ML \<open>\<^term>\<open>1 + 1\<close> (* term as symbolic ML datatype value *)\<close>
ML \<open>\<^term>\<open>1 + (1::int)\<close>\<close>
ML \<open> (* formal source with position information *)
val s = \<open>1 + 1\<close>;
(* read term via old-style string interface *)
val t = Syntax.read_term \<^context> (Syntax.implode_input s); \<close>
subsection \<open>Recursive ML evaluation\<close>
ML \<open>
ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
ML \<open>val b = @{thm sym}\<close>;
val c = @{thm trans}
val thms = [a, b, c]; \<close>
subsection \<open>IDE support\<close>
text\<open>
ML embedded into the Isabelle environment is connected to the Prover IDE.
Poly/ML provides:
\<^item> precise positions for warnings / errors \<^item> markup for defining positions of identifiers \<^item> markup for inferred types of sub-expressions \<^item> pretty-printing of ML values with markup \<^item> completion of ML names \<^item> source-level debugger \<close>
ML \<open>fn i => fn list => length list + i\<close>
subsection \<open>Example: factorial and ackermann function in Isabelle/ML\<close>
ML \<open> fun factorial 0 = 1
| factorial n = n * factorial (n - 1) \<close>
ML \<open>factorial 42\<close>
ML \<open>factorial 10000 div factorial 9999\<close>
Note that within Isabelle theory documents, the top-level command boundary
may not be transgressed without special precautions. This is normally
managed by the system when performing parallel proof checking. \<close>
ML \<open>
val x = Future.fork (fn () => ackermann 3 10);
val y = Future.fork (fn () => ackermann 3 10);
val z = Future.join x + Future.join y \<close>
text\<open>
The \<^ML_structure>\<open>Par_List\<close> module provides high-level combinators for
parallel list operations. \<close>
ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close>
ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close>
subsection \<open>Function specifications in Isabelle/HOL\<close>
fun factorial :: "nat \ nat" where "factorial 0 = 1"
| "factorial (Suc n) = Suc n * factorial n"
term"factorial 4"\<comment> \<open>symbolic term\<close> value"factorial 4"\<comment> \<open>evaluation via ML code generation in the background\<close>
declare [[ML_source_trace]]
ML \<open>\<^term>\<open>factorial 4\<close>\<close> \<comment> \<open>symbolic term in ML\<close>
ML \<open>@{code "factorial"}\<close> \<comment> \<open>ML code from function specification\<close>
fun ackermann :: "nat \ nat \ nat" where "ackermann 0 n = n + 1"
| "ackermann (Suc m) 0 = ackermann m 1"
| "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)"
value"ackermann 3 5"
end
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
