7 |
7 |
8 signature ITEM_NET = |
8 signature ITEM_NET = |
9 sig |
9 sig |
10 type 'a T |
10 type 'a T |
11 val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T |
11 val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T |
|
12 val is_empty: 'a T -> bool |
12 val content: 'a T -> 'a list |
13 val content: 'a T -> 'a list |
13 val length: 'a T -> int |
14 val length: 'a T -> int |
14 val retrieve: 'a T -> term -> 'a list |
15 val retrieve: 'a T -> term -> 'a list |
15 val retrieve_matching: 'a T -> term -> 'a list |
16 val retrieve_matching: 'a T -> term -> 'a list |
16 val member: 'a T -> 'a -> bool |
17 val member: 'a T -> 'a -> bool |
36 |
37 |
37 fun mk_items eq index content next net = |
38 fun mk_items eq index content next net = |
38 Items {eq = eq, index = index, content = content, next = next, net = net}; |
39 Items {eq = eq, index = index, content = content, next = next, net = net}; |
39 |
40 |
40 fun init eq index = mk_items eq index [] ~1 Net.empty; |
41 fun init eq index = mk_items eq index [] ~1 Net.empty; |
|
42 fun is_empty (Items {content, ...}) = null content; |
41 |
43 |
42 fun content (Items {content, ...}) = content; |
44 fun content (Items {content, ...}) = content; |
43 fun length items = List.length (content items); |
45 fun length items = List.length (content items); |
44 fun retrieve (Items {net, ...}) = order_list o Net.unify_term net; |
46 fun retrieve (Items {net, ...}) = order_list o Net.unify_term net; |
45 fun retrieve_matching (Items {net, ...}) = order_list o Net.match_term net; |
47 fun retrieve_matching (Items {net, ...}) = order_list o Net.match_term net; |
60 |
62 |
61 fun cons x (Items {eq, index, content, next, net}) = |
63 fun cons x (Items {eq, index, content, next, net}) = |
62 mk_items eq index (x :: content) (next - 1) |
64 mk_items eq index (x :: content) (next - 1) |
63 (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net); |
65 (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net); |
64 |
66 |
65 fun merge |
67 fun merge (items1, items2) = |
66 (items1 as Items {net = net1, ...}, |
68 if pointer_eq (items1, items2) then items1 |
67 items2 as Items {net = net2, content = content2, ...}) = |
69 else if is_empty items1 then items2 |
68 if pointer_eq (net1, net2) then items1 |
70 else fold_rev (fn y => if member items1 y then I else cons y) (content items2) items1; |
69 else if Net.is_empty net1 then items2 |
|
70 else fold_rev (fn y => if member items1 y then I else cons y) content2 items1; |
|
71 |
71 |
72 fun remove x (items as Items {eq, index, content, next, net}) = |
72 fun remove x (items as Items {eq, index, content, next, net}) = |
73 if member items x then |
73 if member items x then |
74 mk_items eq index (Library.remove eq x content) next |
74 mk_items eq index (Library.remove eq x content) next |
75 (fold (fn t => Net.delete_term_safe (eq o apply2 #2) (t, (0, x))) (index x) net) |
75 (fold (fn t => Net.delete_term_safe (eq o apply2 #2) (t, (0, x))) (index x) net) |