| changeset 309 | ed797395fab6 |
| parent 308 | c90f4ec30d43 |
| child 310 | 007922777ff1 |
| 308:c90f4ec30d43 | 309:ed797395fab6 |
|---|---|
506 text {* |
506 text {* |
507 These two functions can be used to avoid explicit @{text "lets"} for |
507 These two functions can be used to avoid explicit @{text "lets"} for |
508 intermediate values in functions that return pairs. Suppose for example you |
508 intermediate values in functions that return pairs. Suppose for example you |
509 want to separate a list of integers into two lists according to a |
509 want to separate a list of integers into two lists according to a |
510 treshold. For example if the treshold is @{ML "5"}, the list @{ML |
510 treshold. For example if the treshold is @{ML "5"}, the list @{ML |
511 "[1,6,2,5,3,4]"} should be separated to @{ML "([1,2,3,4], [6,5])"}. You |
511 "[1,6,2,5,3,4]"} should be separated to @{ML "([1,2,3,4], [6,5])"}. This |
512 can implement this function more concisely as |
512 function can be implemented as |
513 *} |
513 *} |
514 |
514 |
515 ML{*fun separate i [] = ([], []) |
515 ML{*fun separate i [] = ([], []) |
516 | separate i (x::xs) = |
516 | separate i (x::xs) = |
517 let |
517 let |
519 in |
519 in |
520 if i <= x then (los, x::grs) else (x::los, grs) |
520 if i <= x then (los, x::grs) else (x::los, grs) |
521 end*} |
521 end*} |
522 |
522 |
523 text {* |
523 text {* |
524 where however the return value of the recursive |
524 where however the return value of the recursive call is bound explicitly to |
525 call is bound explicitly to the pair @{ML "(los, grs)" for los grs}. |
525 the pair @{ML "(los, grs)" for los grs}. You can implement this function |
526 This function can equally be written as |
526 more concisely as |
527 *} |
527 *} |
528 |
528 |
529 ML{*fun separate i [] = ([], []) |
529 ML{*fun separate i [] = ([], []) |
530 | separate i (x::xs) = |
530 | separate i (x::xs) = |
531 if i <= x |
531 if i <= x |
532 then separate i xs ||> cons x |
532 then separate i xs ||> cons x |
533 else separate i xs |>> cons x*} |
533 else separate i xs |>> cons x*} |
534 |
534 |
535 text {* |
535 text {* |
536 where no explicit @{text "let"} is needed. While in this example the gain is |
536 avoiding the explicit @{text "let"}. While in this example the gain is only |
537 only small, in more complicated situations the benefit of avoiding @{text "lets"} |
537 small, in more complicated situations the benefit of avoiding @{text "lets"} |
538 can be substantial. |
538 can be substantial. |
539 |
539 |
540 With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair. |
540 With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair. |
541 This combinator is defined as |
541 This combinator is defined as |
542 *} |
542 *} |
543 |
543 |
1062 Similarly the function @{ML [index] subst_bounds}, replaces lose bound |
1062 Similarly the function @{ML [index] subst_bounds}, replaces lose bound |
1063 variables with terms. To see how this function works, let us implement a |
1063 variables with terms. To see how this function works, let us implement a |
1064 function that strips off the outermost quantifiers in a term. |
1064 function that strips off the outermost quantifiers in a term. |
1065 *} |
1065 *} |
1066 |
1066 |
1067 ML {* |
|
1068 subst_bounds ([Free ("x", @{typ nat}), Free ("y", @{typ bool})], |
|
1069 (Bound 1 $ Bound 0)) |
|
1070 *} |
|
1071 |
|
1072 |
|
1073 ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) = |
1067 ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) = |
1074 strip_alls t |>> cons (Free (n, T)) |
1068 strip_alls t |>> cons (Free (n, T)) |
1075 | strip_alls t = ([], t) *} |
1069 | strip_alls t = ([], t) *} |
1076 |
1070 |
1077 text {* |
1071 text {* |
1078 The function returns a pair consisting of the stripped off variables and |
1072 The function returns a pair consisting of the stripped off variables and |
1079 the body of the universal quantifications. For example |
1073 the body of the universal quantifications. For example |