# HG changeset patch # User wenzelm # Date 1120221718 -7200 # Node ID d964cbaa6c1cd669f7b4fdff74db2457b4934051 # Parent c12c2f411f7759fb4bbbb227f8d8a890f2ad852f low-level tuning of fold, fold_rev, foldl_map; diff -r c12c2f411f77 -r d964cbaa6c1c src/Pure/library.ML --- 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*)