1(*  Title:      Pure/item_net.ML
2    Author:     Markus Wenzel, TU Muenchen
3
4Efficient storage of items indexed by terms; preserves order and
5prefers later entries.
6*)
7
8signature ITEM_NET =
9sig
10  type 'a T
11  val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
12  val is_empty: 'a T -> bool
13  val content: 'a T -> 'a list
14  val length: 'a T -> int
15  val retrieve: 'a T -> term -> 'a list
16  val retrieve_matching: 'a T -> term -> 'a list
17  val member: 'a T -> 'a -> bool
18  val lookup: 'a T -> 'a -> 'a list
19  val merge: 'a T * 'a T -> 'a T
20  val remove: 'a -> 'a T -> 'a T
21  val update: 'a -> 'a T -> 'a T
22  val filter: ('a -> bool) -> 'a T -> 'a T
23end;
24
25structure Item_Net: ITEM_NET =
26struct
27
28(* datatype *)
29
30datatype 'a T =
31  Items of {
32    eq: 'a * 'a -> bool,
33    index: 'a -> term list,
34    content: 'a list,
35    next: int,
36    net: (int * 'a) Net.net};
37
38fun mk_items eq index content next net =
39  Items {eq = eq, index = index, content = content, next = next, net = net};
40
41fun init eq index = mk_items eq index [] ~1 Net.empty;
42fun is_empty (Items {content, ...}) = null content;
43
44fun content (Items {content, ...}) = content;
45fun length items = List.length (content items);
46fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
47fun retrieve_matching (Items {net, ...}) = order_list o Net.match_term net;
48
49
50(* standard operations *)
51
52fun member (Items {eq, index, content, net, ...}) x =
53  (case index x of
54    [] => Library.member eq content x
55  | t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t));
56
57fun lookup (Items {eq, index, content, net, ...}) x =
58  (case index x of
59    [] => content
60  | t :: _ => map #2 (Net.unify_term net t))
61  |> filter (fn y => eq (x, y));
62
63fun cons x (Items {eq, index, content, next, net}) =
64  mk_items eq index (x :: content) (next - 1)
65    (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
66
67fun merge (items1, items2) =
68  if pointer_eq (items1, items2) then items1
69  else if is_empty items1 then items2
70  else fold_rev (fn y => if member items1 y then I else cons y) (content items2) items1;
71
72fun remove x (items as Items {eq, index, content, next, net}) =
73  if member items x then
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)
76  else items;
77
78fun update x items = cons x (remove x items);
79
80fun filter pred items =
81  fold (fn x => not (pred x) ? remove x) (content items) items;
82
83end;
84