src/Pure/basis.ML
 changeset 2884 4f2a4c27f9b5 parent 2862 3f38cbd57d47 child 3047 599cb28f8502
```--- a/src/Pure/basis.ML	Thu Apr 03 10:32:34 1997 +0200
+++ b/src/Pure/basis.ML	Thu Apr 03 10:33:33 1997 +0200
@@ -75,6 +75,24 @@
| mapPartial f (x::xs) =
(case f x of General.NONE   => mapPartial f xs
| General.SOME y => y :: mapPartial f xs);
+
+  fun find _ []        = General.NONE
+    | find p (x :: xs) = if p x then General.SOME x else find p xs;
+
+
+  (*copy the list preserving elements that satisfy the predicate*)
+  fun filter p [] = []
+    | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
+
+  (*Partition list into elements that satisfy predicate and those that don't.
+    Preserves order of elements in both lists.*)
+  fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
+      let fun part ([], answer) = answer
+	    | part (x::xs, (ys, ns)) = if p(x)
+	      then  part (xs, (x::ys, ns))
+	      else  part (xs, (ys, x::ns))
+      in  part (rev ys, ([], []))  end;
+
end;

@@ -91,14 +109,14 @@
fun map f ([], [])      = []
| map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);

-  fun exists pred =
+  fun exists p =
let fun boolf ([], [])      = false
-	  | boolf (x::xs,y::ys) = pred(x,y) orelse boolf (xs,ys)
+	  | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
in boolf end;

-  fun all pred =
+  fun all p =
let fun boolf ([], [])      = true
-	  | boolf (x::xs,y::ys) = pred(x,y) andalso boolf (xs,ys)
+	  | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
in boolf end;
end;
```