author | wenzelm |

Fri Jul 01 14:41:58 2005 +0200 (2005-07-01) | |

changeset 16654 | d964cbaa6c1c |

parent 16653 | c12c2f411f77 |

child 16655 | 3e4d726aaed1 |

low-level tuning of fold, fold_rev, foldl_map;

1.1 --- a/src/Pure/library.ML Fri Jul 01 14:41:57 2005 +0200 1.2 +++ b/src/Pure/library.ML Fri Jul 01 14:41:58 2005 +0200 1.3 @@ -450,18 +450,27 @@ 1.4 1.5 (* fold *) 1.6 1.7 -fun fold _ [] y = y 1.8 - | fold f (x :: xs) y = fold f xs (f x y); 1.9 - 1.10 -fun fold_rev _ [] y = y 1.11 - | fold_rev f (x :: xs) y = f x (fold_rev f xs y); 1.12 +fun fold f = 1.13 + let 1.14 + fun fold_aux [] y = y 1.15 + | fold_aux (x :: xs) y = fold_aux xs (f x y); 1.16 + in fold_aux end; 1.17 1.18 -fun foldl_map _ (x, []) = (x, []) 1.19 - | foldl_map f (x, y :: ys) = 1.20 - let 1.21 - val (x', y') = f (x, y); 1.22 - val (x'', ys') = foldl_map f (x', ys); 1.23 - in (x'', y' :: ys') end; 1.24 +fun fold_rev f = 1.25 + let 1.26 + fun fold_aux [] y = y 1.27 + | fold_aux (x :: xs) y = f x (fold_aux xs y); 1.28 + in fold_aux end; 1.29 + 1.30 +fun foldl_map f = 1.31 + let 1.32 + fun fold_aux (x, []) = (x, []) 1.33 + | fold_aux (x, y :: ys) = 1.34 + let 1.35 + val (x', y') = f (x, y); 1.36 + val (x'', ys') = fold_aux (x', ys); 1.37 + in (x'', y' :: ys') end; 1.38 + in fold_aux end; 1.39 1.40 (*the following versions of fold are designed to fit nicely with infixes*) 1.41