src/Pure/General/basics.ML
 changeset 23225 591af6a2f09e parent 22936 284b56463da8 child 23358 e0b5a74d7ace
```--- a/src/Pure/General/basics.ML	Sun Jun 03 23:16:52 2007 +0200
+++ b/src/Pure/General/basics.ML	Sun Jun 03 23:16:53 2007 +0200
@@ -23,7 +23,6 @@
val ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd
val ` : ('b -> 'a) -> 'b -> 'a * 'b
val tap: ('b -> 'a) -> 'b -> 'b
-  val flip: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c

(*options*)
val is_some: 'a option -> bool
@@ -40,13 +39,10 @@

(*lists*)
val cons: 'a -> 'a list -> 'a list
-  val dest: 'a list -> 'a * 'a list
val append: 'a list -> 'a list -> 'a list
val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
-  val unfold: int -> ('b -> 'a * 'b) -> 'b -> 'a list * 'b
-  val unfold_rev: int -> ('b -> 'a * 'b) -> 'b -> 'a list * 'b
end;

structure Basics: BASICS =
@@ -72,8 +68,6 @@
fun `f = fn x => (f x, x);
fun tap f = fn x => (f x; x);

-fun flip f x y = f y x;
-

(* options *)

@@ -112,56 +106,20 @@

fun cons x xs = x :: xs;

-fun dest (x :: xs) = (x, xs)
-  | dest [] = raise Empty;
-
fun append xs ys = xs @ ys;

-
-(* fold *)
+fun fold _ [] y = y
+  | fold f (x :: xs) y = fold f xs (f x y);

-fun fold f =
-  let
-    fun fld [] y = y
-      | fld (x :: xs) y = fld xs (f x y);
-  in fld end;
-
-fun fold_rev f =
-  let
-    fun fld [] y = y
-      | fld (x :: xs) y = f x (fld xs y);
-  in fld end;
+fun fold_rev _ [] y = y
+  | fold_rev f (x :: xs) y = f x (fold_rev f xs y);

-fun fold_map f =
-  let
-    fun fld [] y = ([], y)
-      | fld (x :: xs) y =
-          let
-            val (x', y') = f x y;
-            val (xs', y'') = fld xs y';
-          in (x' :: xs', y'') end;
-  in fld end;
-
-
-(* unfold -- with optional limit *)
-
-fun unfold lim f =
-  let
-    fun unfld 0 ys x = (ys, x)
-      | unfld n ys x =
-          (case try f x of
-            NONE => (ys, x)
-          | SOME (y, x') => unfld (n - 1) (y :: ys) x');
-  in unfld lim [] end;
-
-fun unfold_rev lim f =
-  let
-    fun unfld 0 x = ([], x)
-      | unfld n x =
-          (case try f x of
-            NONE => ([], x)
-          | SOME (y, x') => unfld (n - 1) x' |>> cons y);
-  in unfld lim end;
+fun fold_map _ [] y = ([], y)
+  | fold_map f (x :: xs) y =
+      let
+        val (x', y') = f x y;
+        val (xs', y'') = fold_map f xs y';
+      in (x' :: xs', y'') end;

end;
```