author | wenzelm |
Wed, 24 May 2006 01:05:02 +0200 | |
changeset 19708 | a508bde37a81 |
parent 19454 | 46a7e133f802 |
child 20142 | 7f5bb7f8b9b9 |
permissions | -rw-r--r-- |
17152 | 1 |
(* Title: Pure/General/alist.ML |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
||
19454
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
5 |
Association lists -- lists of (key, value) pairs. |
17152 | 6 |
*) |
7 |
||
8 |
signature ALIST = |
|
9 |
sig |
|
17766 | 10 |
exception DUP |
17152 | 11 |
val lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option |
12 |
val defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool |
|
13 |
val update: ('a * 'a -> bool) -> ('a * 'b) |
|
14 |
-> ('a * 'b) list -> ('a * 'b) list |
|
15 |
val default: ('a * 'a -> bool) -> ('a * 'b) |
|
16 |
-> ('a * 'b) list -> ('a * 'b) list |
|
17 |
val delete: ('a * 'b -> bool) -> 'a |
|
18 |
-> ('b * 'c) list -> ('b * 'c) list |
|
19 |
val map_entry: ('a * 'b -> bool) -> 'a -> ('c -> 'c) |
|
20 |
-> ('b * 'c) list -> ('b * 'c) list |
|
18883 | 21 |
val map_entry_yield: ('a * 'b -> bool) -> 'a -> ('c -> 'd * 'c) |
22 |
-> ('b * 'c) list -> 'd option * ('b * 'c) list |
|
17911 | 23 |
val join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b option) -> |
24 |
('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception DUP*) |
|
17766 | 25 |
val merge: ('a * 'a -> bool) -> ('b * 'b -> bool) |
17911 | 26 |
-> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception DUP*) |
19454
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
27 |
val make: ('a -> 'b) -> 'a list -> ('a * 'b) list |
17497 | 28 |
val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list |
19454
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
29 |
val coalesce: ('a * 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
30 |
(*coalesce ranges of equal neighbour keys*) |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
31 |
val group: ('a * 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list |
17152 | 32 |
end; |
33 |
||
34 |
structure AList: ALIST = |
|
35 |
struct |
|
36 |
||
17766 | 37 |
fun find_index eq xs key = |
38 |
let |
|
18926 | 39 |
fun find [] _ = ~1 |
17766 | 40 |
| find ((key', value)::xs) i = |
41 |
if eq (key, key') |
|
42 |
then i |
|
43 |
else find xs (i+1); |
|
18926 | 44 |
in find xs 0 end; |
17766 | 45 |
|
17152 | 46 |
fun lookup _ [] _ = NONE |
47 |
| lookup eq ((key, value)::xs) key' = |
|
48 |
if eq (key', key) then SOME value |
|
49 |
else lookup eq xs key'; |
|
50 |
||
51 |
fun defined _ [] _ = false |
|
52 |
| defined eq ((key, value)::xs) key' = |
|
53 |
eq (key', key) orelse defined eq xs key'; |
|
54 |
||
17766 | 55 |
fun update eq (x as (key, value)) xs = |
17152 | 56 |
let |
17766 | 57 |
val i = find_index eq xs key; |
18926 | 58 |
fun upd 0 (_::xs) = x :: xs |
17766 | 59 |
| upd i (x::xs) = x :: upd (i-1) xs; |
18926 | 60 |
in if i = ~1 then x::xs else upd i xs end; |
17152 | 61 |
|
62 |
fun default eq (key, value) xs = |
|
63 |
if defined eq xs key then xs else (key, value)::xs; |
|
64 |
||
65 |
fun delete eq key xs = |
|
66 |
let |
|
17766 | 67 |
val i = find_index eq xs key; |
18926 | 68 |
fun del 0 (_::xs) = xs |
17766 | 69 |
| del i (x::xs) = x :: del (i-1) xs; |
18926 | 70 |
in if i = ~1 then xs else del i xs end; |
17766 | 71 |
|
72 |
fun map_entry eq key f xs = |
|
73 |
let |
|
74 |
val i = find_index eq xs key; |
|
18926 | 75 |
fun mapp 0 ((x as (key, value))::xs) = (key, f value) :: xs |
17766 | 76 |
| mapp i (x::xs) = x :: mapp (i-1) xs; |
18926 | 77 |
in if i = ~1 then xs else mapp i xs end; |
17152 | 78 |
|
18883 | 79 |
fun map_entry_yield eq key f xs = |
80 |
let |
|
81 |
val i = find_index eq xs key; |
|
18926 | 82 |
fun mapp 0 ((x as (key, value))::xs) = |
18883 | 83 |
let val (r, value') = f value |
84 |
in (SOME r, (key, value') :: xs) end |
|
85 |
| mapp i (x::xs) = |
|
86 |
let val (r, xs') = mapp (i-1) xs |
|
87 |
in (r, x::xs') end; |
|
18926 | 88 |
in if i = ~1 then (NONE, xs) else mapp i xs end; |
18883 | 89 |
|
17766 | 90 |
exception DUP; |
91 |
||
17911 | 92 |
fun join eq f (xs, ys) = |
93 |
let |
|
18926 | 94 |
fun add (y as (key, value)) xs = |
17911 | 95 |
(case lookup eq xs key of |
18926 | 96 |
NONE => cons y xs |
97 |
| SOME value' => |
|
98 |
(case f key (value', value) of |
|
99 |
SOME value'' => update eq (key, value'') xs |
|
17911 | 100 |
| NONE => raise DUP)); |
18926 | 101 |
in fold_rev add ys xs end; |
17911 | 102 |
|
18926 | 103 |
fun merge eq_key eq_val = |
104 |
join eq_key (K (fn (yx as (_, x)) => if eq_val yx then SOME x else NONE)); |
|
17191 | 105 |
|
17487 | 106 |
fun make keyfun = |
107 |
let fun keypair x = (x, keyfun x) |
|
108 |
in map keypair end; |
|
109 |
||
17497 | 110 |
fun find eq [] _ = [] |
111 |
| find eq ((key, value) :: xs) value' = |
|
112 |
let |
|
17766 | 113 |
val values = find eq xs value'; |
17497 | 114 |
in if eq (value', value) then key :: values else values end; |
115 |
||
19454
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
116 |
fun coalesce eq = |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
117 |
let |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
118 |
fun vals _ [] = ([], []) |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
119 |
| vals x (lst as (y, b) :: ps) = |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
120 |
if eq (x, y) then vals x ps |>> cons b |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
121 |
else ([], lst); |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
122 |
fun coal [] = [] |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
123 |
| coal ((x, a) :: ps) = |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
124 |
let val (bs, qs) = vals x ps |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
125 |
in (x, a :: bs) :: coal qs end; |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
126 |
in coal end; |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
127 |
|
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
128 |
fun group eq xs = |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
129 |
fold_rev (fn (k, v) => default eq (k, []) #> map_entry eq k (cons v)) xs []; |
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
18926
diff
changeset
|
130 |
|
17152 | 131 |
end; |