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