|
1 (* Title: Pure/General/alist.ML |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 |
|
5 Association lists -- lists of (key, value) pairs with unique keys. |
|
6 A light-weight representation of finite mappings; |
|
7 see also Pure/General/table.ML for a more scalable implementation. |
|
8 *) |
|
9 |
|
10 signature ALIST = |
|
11 sig |
|
12 val lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option |
|
13 val defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool |
|
14 val update: ('a * 'a -> bool) -> ('a * 'b) |
|
15 -> ('a * 'b) list -> ('a * 'b) list |
|
16 val default: ('a * 'a -> bool) -> ('a * 'b) |
|
17 -> ('a * 'b) list -> ('a * 'b) list |
|
18 val delete: ('a * 'b -> bool) -> 'a |
|
19 -> ('b * 'c) list -> ('b * 'c) list |
|
20 val map_entry: ('a * 'b -> bool) -> 'a -> ('c -> 'c) |
|
21 -> ('b * 'c) list -> ('b * 'c) list |
|
22 end; |
|
23 |
|
24 structure AList: ALIST = |
|
25 struct |
|
26 |
|
27 fun lookup _ [] _ = NONE |
|
28 | lookup eq ((key, value)::xs) key' = |
|
29 if eq (key', key) then SOME value |
|
30 else lookup eq xs key'; |
|
31 |
|
32 fun defined _ [] _ = false |
|
33 | defined eq ((key, value)::xs) key' = |
|
34 eq (key', key) orelse defined eq xs key'; |
|
35 |
|
36 fun update eq (key, value) xs = |
|
37 let |
|
38 fun upd ((x as (key', _))::xs) = |
|
39 if eq (key, key') |
|
40 then (key, value)::xs |
|
41 else x :: upd xs |
|
42 in if defined eq xs key then upd xs else (key, value)::xs end; |
|
43 |
|
44 fun default eq (key, value) xs = |
|
45 if defined eq xs key then xs else (key, value)::xs; |
|
46 |
|
47 fun map_entry eq _ _ [] = [] |
|
48 | map_entry eq key' f ((x as (key, value))::xs) = |
|
49 if eq (key', key) then ((key, f value)::xs) |
|
50 else x :: map_entry eq key' f xs; |
|
51 |
|
52 fun delete eq key xs = |
|
53 let |
|
54 fun del ((x as (key', _))::xs) = |
|
55 if eq (key, key') then xs |
|
56 else x :: del xs; |
|
57 in if defined eq xs key then del xs else xs end; |
|
58 |
|
59 end; |