# HG changeset patch
# User wenzelm
# Date 1257105339 -3600
# Node ID f380fbd6e32902eabcde87b71fa0d363462ffd02
# Parent  d74dc1b549308f5f0bb0cd0c447a43cbd573e3d6
allow multi-index;
more scalable merge;
renamed delete to remove, and insert to update (standard naming conventions);
tuned;

diff -r d74dc1b54930 -r f380fbd6e329 src/Pure/item_net.ML
--- a/src/Pure/item_net.ML	Sun Nov 01 20:55:14 2009 +0100
+++ b/src/Pure/item_net.ML	Sun Nov 01 20:55:39 2009 +0100
@@ -8,12 +8,12 @@
 signature ITEM_NET =
 sig
   type 'a T
+  val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
   val content: 'a T -> 'a list
   val retrieve: 'a T -> term -> 'a list
-  val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
   val merge: 'a T * 'a T -> 'a T
-  val delete: 'a -> 'a T -> 'a T
-  val insert: 'a -> 'a T -> 'a T
+  val remove: 'a -> 'a T -> 'a T
+  val update: 'a -> 'a T -> 'a T
 end;
 
 structure Item_Net: ITEM_NET =
@@ -24,7 +24,7 @@
 datatype 'a T =
   Items of {
     eq: 'a * 'a -> bool,
-    index: 'a -> term,
+    index: 'a -> term list,
     content: 'a list,
     next: int,
     net: (int * 'a) Net.net};
@@ -32,27 +32,31 @@
 fun mk_items eq index content next net =
   Items {eq = eq, index = index, content = content, next = next, net = net};
 
+fun init eq index = mk_items eq index [] ~1 Net.empty;
+
 fun content (Items {content, ...}) = content;
 fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
 
 
-(* build net *)
+(* standard operations *)
 
-fun init eq index = mk_items eq index [] ~1 Net.empty;
+fun member (Items {eq, index, net, ...}) x =
+  exists (fn t => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t)) (index x);
 
-fun add x (Items {eq, index, content, next, net}) =
+fun cons x (Items {eq, index, content, next, net}) =
   mk_items eq index (x :: content) (next - 1)
-    (Net.insert_term (K false) (index x, (next, x)) net);
+    (fold (fn t => Net.insert_term_safe (eq o pairself #2) (t, (next, x))) (index x) net);
+
 
-fun merge (Items {eq, index, content = content1, ...}, Items {content = content2, ...}) =
-  let val content = Library.merge eq (content1, content2)
-  in fold_rev add content (init eq index) end;
+fun merge (items1, Items {content = content2, ...}) =
+  fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
 
-fun delete x (items as Items {eq, index, content, next, net}) =
-  if not (member eq content x) then items
-  else mk_items eq index (remove eq x content) next
-    (Net.delete_term (eq o pairself #2) (index x, (0, x)) net);
+fun remove x (items as Items {eq, index, content, next, net}) =
+  if member items x then
+    mk_items eq index (Library.remove eq x content) next
+      (fold (fn t => Net.delete_term_safe (eq o pairself #2) (t, (0, x))) (index x) net)
+  else items;
 
-fun insert x items = add x (delete x items);   (*ensure that added entry gets precedence*)
+fun update x items = cons x (remove x items);
 
 end;