src/HOL/ex/ML.thy
 author wenzelm Mon Aug 31 21:28:08 2015 +0200 (2015-08-31) changeset 61070 b72a990adfe2 parent 58889 5b7a9633cfa8 child 61757 0d399131008f permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/ex/ML.thy

     2     Author:     Makarius

     3 *)

     4

     5 section \<open>Isabelle/ML basics\<close>

     6

     7 theory "ML"

     8 imports Main

     9 begin

    10

    11 section \<open>ML expressions\<close>

    12

    13 text \<open>

    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 \<close>

    22

    23 ML \<open>1 + 1\<close>

    24

    25 ML \<open>val a = 1\<close>

    26 ML \<open>val b = 1\<close>

    27 ML \<open>val c = a + b\<close>

    28

    29

    30 section \<open>Antiquotations\<close>

    31

    32 text \<open>There are some language extensions (via antiquotations), as explained in

    33   the Isabelle/Isar implementation manual'', chapter 0.\<close>

    34

    35 ML \<open>length []\<close>

    36 ML \<open>@{assert} (length [] = 0)\<close>

    37

    38

    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>

    45

    46 ML \<open>@{term "1 + (1::int)"}\<close>

    47

    48

    49 section \<open>IDE support\<close>

    50

    51 text \<open>

    52   ML embedded into the Isabelle environment is connected to the Prover IDE.

    53   Poly/ML provides:

    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}

    59 \<close>

    60

    61 ML \<open>fn i => fn list => length list + i\<close>

    62

    63

    64 section \<open>Example: factorial and ackermann function in Isabelle/ML\<close>

    65

    66 ML \<open>

    67   fun factorial 0 = 1

    68     | factorial n = n * factorial (n - 1)

    69 \<close>

    70

    71 ML \<open>factorial 42\<close>

    72 ML \<open>factorial 10000 div factorial 9999\<close>

    73

    74 text \<open>See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}\<close>

    75

    76 ML \<open>

    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))

    80 \<close>

    81

    82 ML \<open>timeit (fn () => ackermann 3 10)\<close>

    83

    84

    85 section \<open>Parallel Isabelle/ML\<close>

    86

    87 text \<open>

    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

    92   the system when performing parallel proof checking.\<close>

    93

    94 ML \<open>

    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

    98 \<close>

    99

   100 text \<open>The @{ML_structure Par_List} module provides high-level combinators

   101   for parallel list operations.\<close>

   102

   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>

   105

   106

   107 section \<open>Function specifications in Isabelle/HOL\<close>

   108

   109 fun factorial :: "nat \<Rightarrow> nat"

   110 where

   111   "factorial 0 = 1"

   112 | "factorial (Suc n) = Suc n * factorial n"

   113

   114 term "factorial 4"  -- \<open>symbolic term\<close>

   115 value "factorial 4"  -- \<open>evaluation via ML code generation in the background\<close>

   116

   117 declare [[ML_source_trace]]

   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>

   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