summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 01 Jul 2005 14:41:58 +0200 | |

changeset 16654 | d964cbaa6c1c |

parent 16653 | c12c2f411f77 |

child 16655 | 3e4d726aaed1 |

low-level tuning of fold, fold_rev, foldl_map;

--- a/src/Pure/library.ML Fri Jul 01 14:41:57 2005 +0200 +++ b/src/Pure/library.ML Fri Jul 01 14:41:58 2005 +0200 @@ -450,18 +450,27 @@ (* fold *) -fun fold _ [] y = y - | fold f (x :: xs) y = fold f xs (f x y); - -fun fold_rev _ [] y = y - | fold_rev f (x :: xs) y = f x (fold_rev f xs y); +fun fold f = + let + fun fold_aux [] y = y + | fold_aux (x :: xs) y = fold_aux xs (f x y); + in fold_aux end; -fun foldl_map _ (x, []) = (x, []) - | foldl_map f (x, y :: ys) = - let - val (x', y') = f (x, y); - val (x'', ys') = foldl_map f (x', ys); - in (x'', y' :: ys') end; +fun fold_rev f = + let + fun fold_aux [] y = y + | fold_aux (x :: xs) y = f x (fold_aux xs y); + in fold_aux end; + +fun foldl_map f = + let + fun fold_aux (x, []) = (x, []) + | fold_aux (x, y :: ys) = + let + val (x', y') = f (x, y); + val (x'', ys') = fold_aux (x', ys); + in (x'', y' :: ys') end; + in fold_aux end; (*the following versions of fold are designed to fit nicely with infixes*)