diff -r 8fda6b452f28 -r 6dfe6975bda0 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Mon Jan 26 16:09:02 2009 +0000 +++ b/CookBook/FirstSteps.thy Tue Jan 27 05:41:14 2009 +0000 @@ -510,10 +510,10 @@ section {* Combinators\label{sec:combinators} *} text {* - Perhaps one of the most puzzling aspect for a beginner when reading - existing Isabelle code special purpose combinators. At first they - seem to obstruct the comprehension of the code, but after getting familiar - with them they actually ease the understanding and also the programming. + For beginners, perhaps the most puzzling parts in the existing code of Isabelle are + the combinators. At first they seem to greatly obstruct the + comprehension of the code, but after getting familiar with them, they + actually ease the understanding and also the programming. \begin{readmore} The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"} @@ -525,15 +525,16 @@ ML{*fun I x = x*} -text {* Another combinator is @{ML K}, defined as *} +text {* Another simple combinator is @{ML K}, defined as *} ML{*fun K x = fn _ => x*} text {* It ``wraps'' a function around the argument @{text "x"}. However, this - function ignores its argument. + function ignores its argument. So @{ML K} defines a constant function + returning @{text x}. - The next combinator is reverse application, @{ML "(op |>)"}, defined as + The next combinator is reverse application, @{ML "|>"}, defined as *} ML{*fun x |> f = f x*} @@ -554,7 +555,8 @@ the first component of the pair (Line 4) and finally incrementing the first component by 4 (Line 5). This kind of cascading manipulations of values is quite common when dealing with theories (for example by adding a definition, followed by - lemmas and so on). Writing the function @{ML inc_by_five} using the reverse + lemmas and so on). It should also be familiar to anyone who has used Haskell's + do-notation. Writing the function @{ML inc_by_five} using the reverse application is much clearer than writing *} @@ -575,9 +577,13 @@ in y4 end*} text {* + Another reason why the let-bindings in the code above are better to be + avoided: it is more than easy to get the intermediate values wrong! + + (FIXME: give a real world example involving theories) - Similarly, the combinator @{ML "(op #>)"} is the reverse function + Similarly, the combinator @{ML "#>"} is the reverse function composition. It can be used to define functions as follows *} @@ -588,33 +594,30 @@ text {* which is the function composed of first the increment-by-one function and then - increment-by-two, followed by increment-by-three. Applying 6 to this function - yields - - @{ML_response [display,gray] "inc_by_six 6" "12"} - - as expected. + increment-by-two, followed by increment-by-three. - The remaining combinators add convenience for the ``waterfall method'' - of writing functions. The combinator @{ML tap} allows one to get - hold of an intermediate result (to do some side-calculations for instance). - The function *} + The remaining combinators described in this section add convenience for the + ``waterfall method'' of writing functions. The combinator @{ML tap} allows + one to get hold of an intermediate result (to do some side-calculations for + instance). The function -ML{*fun inc_by_three x = + *} + +ML %linenumbers{*fun inc_by_three x = x |> (fn x => x + 1) |> tap (fn x => tracing (makestring x)) |> (fn x => x + 2)*} text {* increments the argument first by one and then by two. In the middle, however, it uses @{ML tap} for printing the ``plus-one'' intermediate - result inside the tracing buffer. + result inside the tracing buffer (Line 3). The function @{ML tap} can only + be used for side-calculations, because any value that is computed cannot + be merged back into the ``main waterfall''. To do this, the next combinator + can be used. - The combinator @{ML "(op `)"} is similar, but applies a function to the value - and returns the result together with the original value (as pair). For example - the following function takes @{text x} as argument, and then first - increments @{text x}, but also keeps @{text x}. The intermediate result is - therefore the pair @{ML "(x + 1,x)" for x}. The function then increments the - right-hand component of the pair. + The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value + and returns the result together with the value (as a pair). For example + the function *} ML{*fun inc_as_pair x = @@ -622,7 +625,13 @@ |> (fn (x, y) => (x, y + 1))*} text {* - The combinators @{ML "(op |>>)"} and @{ML "(op ||>)"} are defined for + takes @{text x} as argument, and then first + increments @{text x}, but also keeps @{text x}. The intermediate result is + therefore the pair @{ML "(x + 1, x)" for x}. The function then increments the + right-hand component of the pair. So finally the result will be + @{ML "(x + 1, x + 1)" for x}. + + The combinators @{ML "|>>"} and @{ML "||>"} are defined for functions manipulating pairs. The first applies the function to the first component of the pair, defined as: *} @@ -636,6 +645,35 @@ ML{*fun (x, y) ||> f = (x, f y)*} text {* + With the combinator @{ML "|->"} you can re-combine the elements from a pair. + This combinator is defined as +*} + +ML{*fun (x, y) |-> f = f x y*} + +text {* and can be used to write the following version of the @{text double} function *} + +ML{*fun double x = + x |> (fn x => (x, x)) + |-> (fn x => fn y => x + y)*} + +text {* + Recall that @{ML "|>"} is the reverse function applications. The related + reverse function composition is @{ML "#>"}. In fact all combinators @{ML "|->"}, + @{ML "|>>"} and @{ML "||>"} described above have related combinators for function + composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. In this + way, the function @{text double} can also be written as +*} + +ML{*val double = + (fn x => (x, x)) + #-> (fn x => fn y => x + y)*} + + +text {* + + + (FIXME: find a good exercise for combinators) *}