1(* Title: Pure/General/alist.ML 2 Author: Florian Haftmann, TU Muenchen 3 4Association lists -- lists of (key, value) pairs. 5*) 6 7signature AList = 8sig 9 exception DUP 10 val lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option 11 val defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool 12 val update: ('a * 'a -> bool) -> ('a * 'b) 13 -> ('a * 'b) list -> ('a * 'b) list 14 val default: ('a * 'a -> bool) -> ('a * 'b) 15 -> ('a * 'b) list -> ('a * 'b) list 16 val delete: ('a * 'b -> bool) -> 'a 17 -> ('b * 'c) list -> ('b * 'c) list 18 val map_entry: ('a * 'b -> bool) -> 'a -> ('c -> 'c) 19 -> ('b * 'c) list -> ('b * 'c) list 20 val map_entry_yield: ('a * 'b -> bool) -> 'a -> ('c -> 'd * 'c) 21 -> ('b * 'c) list -> 'd option * ('b * 'c) list 22 val map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b) 23 -> ('a * 'b) list -> ('a * 'b) list 24 val join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*) 25 -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception DUP*) 26 val merge: ('a * 'a -> bool) -> ('b * 'b -> bool) 27 -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception DUP*) 28 val make: ('a -> 'b) -> 'a list -> ('a * 'b) list 29 val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list 30 val coalesce: ('a * 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list 31 (*coalesce ranges of equal neighbour keys*) 32 val group: ('a * 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list 33end; 34