added make and find
authorhaftmann
Tue Sep 20 08:23:59 2005 +0200 (2005-09-20)
changeset 17497539319bd6162
parent 17496 26535df536ae
child 17498 d83af87bbdc5
added make and find
src/Pure/General/alist.ML
     1.1 --- a/src/Pure/General/alist.ML	Tue Sep 20 08:21:49 2005 +0200
     1.2 +++ b/src/Pure/General/alist.ML	Tue Sep 20 08:23:59 2005 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4    val map_entry: ('a * 'b -> bool) -> 'a -> ('c -> 'c)
     1.5      -> ('b * 'c) list -> ('b * 'c) list
     1.6    val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
     1.7 +  val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
     1.8  end;
     1.9  
    1.10  structure AList: ALIST =
    1.11 @@ -63,4 +64,10 @@
    1.12    let fun keypair x = (x, keyfun x)
    1.13    in map keypair end;
    1.14  
    1.15 +fun find eq [] _ = []
    1.16 +  | find eq ((key, value) :: xs) value' =
    1.17 +      let
    1.18 +        val values = find eq xs value'
    1.19 +      in if eq (value', value) then key :: values else values end;
    1.20 +
    1.21  end;