292 text {* |
292 text {* |
293 Another reason why the let-bindings in the code above are better to be |
293 Another reason why the let-bindings in the code above are better to be |
294 avoided: it is more than easy to get the intermediate values wrong, not to |
294 avoided: it is more than easy to get the intermediate values wrong, not to |
295 mention the nightmares the maintenance of this code causes! |
295 mention the nightmares the maintenance of this code causes! |
296 |
296 |
297 In the context of Isabelle, a ``real world'' example for a function written in |
297 In Isabelle, a ``real world'' example for a function written in |
298 the waterfall fashion might be the following code: |
298 the waterfall fashion might be the following code: |
299 *} |
299 *} |
300 |
300 |
301 ML %linenosgray{*fun apply_fresh_args f ctxt = |
301 ML %linenosgray{*fun apply_fresh_args f ctxt = |
302 f |> fastype_of |
302 f |> fastype_of |
396 This combinator is defined as |
396 This combinator is defined as |
397 *} |
397 *} |
398 |
398 |
399 ML{*fun (x, y) |-> f = f x y*} |
399 ML{*fun (x, y) |-> f = f x y*} |
400 |
400 |
401 text {* and can be used to write the following roundabout version |
401 text {* |
|
402 and can be used to write the following roundabout version |
402 of the @{text double} function: |
403 of the @{text double} function: |
403 *} |
404 *} |
404 |
405 |
405 ML{*fun double x = |
406 ML{*fun double x = |
406 x |> (fn x => (x, x)) |
407 x |> (fn x => (x, x)) |
407 |-> (fn x => fn y => x + y)*} |
408 |-> (fn x => fn y => x + y)*} |
408 |
409 |
|
410 text {* |
|
411 The combinator @{ML ||>>} plays a central rôle whenever your task is to update a |
|
412 theory and the update also produces a side-result (for example a theorem). Functions |
|
413 for such tasks return a pair whose second component is the theory and the fist |
|
414 component is the side-result. Using @{ML ||>>}, you can do conveniently the update |
|
415 and also accumulate the side-results. Considder the following simple function. |
|
416 *} |
|
417 |
|
418 ML %linenosgray{*fun acc_incs x = |
|
419 x |> (fn x => ("", x)) |
|
420 ||>> (fn x => (x, x + 1)) |
|
421 ||>> (fn x => (x, x + 1)) |
|
422 ||>> (fn x => (x, x + 1))*} |
|
423 |
|
424 text {* |
|
425 The purpose of Line 2 is to just pair up the argument with a dummy value (since |
|
426 @{ML "||>>"} operates on pairs). Each of the next three lines just increment |
|
427 the value by one, but also nest the intrermediate results to the left. For example |
|
428 |
|
429 @{ML_response [display,gray] |
|
430 "acc_incs 1" |
|
431 "((((\"\", 1), 2), 3), 4)"} |
|
432 |
|
433 You can continue this chain with: |
|
434 |
|
435 @{ML_response [display,gray] |
|
436 "acc_incs 1 ||>> (fn x => (x, x + 2))" |
|
437 "(((((\"\", 1), 2), 3), 4), 6)"} |
|
438 |
|
439 (FIXME: maybe give a ``real world'' example) |
|
440 *} |
|
441 |
409 text {* |
442 text {* |
410 Recall that @{ML "|>"} is the reverse function application. Recall also that |
443 Recall that @{ML "|>"} is the reverse function application. Recall also that |
411 the related |
444 the related |
412 reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"}, |
445 reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"}, |
413 @{ML "|>>"} and @{ML "||>"} described above have related combinators for function |
446 @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"} described above have related combinators for |
414 composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, |
447 function composition, namely @{ML "#->"}, @{ML "#>>"}, @{ML "##>"} and @{ML "##>>"}. |
415 for example, the function @{text double} can also be written as: |
448 Using @{ML "#->"}, for example, the function @{text double} can also be written as: |
416 *} |
449 *} |
417 |
450 |
418 ML{*val double = |
451 ML{*val double = |
419 (fn x => (x, x)) |
452 (fn x => (x, x)) |
420 #-> (fn x => fn y => x + y)*} |
453 #-> (fn x => fn y => x + y)*} |