added make and find
authorhaftmann
Tue, 20 Sep 2005 08:23:59 +0200
changeset 17497 539319bd6162
parent 17496 26535df536ae
child 17498 d83af87bbdc5
added make and find
src/Pure/General/alist.ML
--- a/src/Pure/General/alist.ML	Tue Sep 20 08:21:49 2005 +0200
+++ b/src/Pure/General/alist.ML	Tue Sep 20 08:23:59 2005 +0200
@@ -20,6 +20,7 @@
   val map_entry: ('a * 'b -> bool) -> 'a -> ('c -> 'c)
     -> ('b * 'c) list -> ('b * 'c) list
   val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
+  val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
 end;
 
 structure AList: ALIST =
@@ -63,4 +64,10 @@
   let fun keypair x = (x, keyfun x)
   in map keypair end;
 
+fun find eq [] _ = []
+  | find eq ((key, value) :: xs) value' =
+      let
+        val values = find eq xs value'
+      in if eq (value', value) then key :: values else values end;
+
 end;