src/Pure/item_net.ML
changeset 33372 f380fbd6e329
parent 30559 e5987a7ac5df
child 33721 f15c9ded9676
     1.1 --- a/src/Pure/item_net.ML	Sun Nov 01 20:55:14 2009 +0100
     1.2 +++ b/src/Pure/item_net.ML	Sun Nov 01 20:55:39 2009 +0100
     1.3 @@ -8,12 +8,12 @@
     1.4  signature ITEM_NET =
     1.5  sig
     1.6    type 'a T
     1.7 +  val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
     1.8    val content: 'a T -> 'a list
     1.9    val retrieve: 'a T -> term -> 'a list
    1.10 -  val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
    1.11    val merge: 'a T * 'a T -> 'a T
    1.12 -  val delete: 'a -> 'a T -> 'a T
    1.13 -  val insert: 'a -> 'a T -> 'a T
    1.14 +  val remove: 'a -> 'a T -> 'a T
    1.15 +  val update: 'a -> 'a T -> 'a T
    1.16  end;
    1.17  
    1.18  structure Item_Net: ITEM_NET =
    1.19 @@ -24,7 +24,7 @@
    1.20  datatype 'a T =
    1.21    Items of {
    1.22      eq: 'a * 'a -> bool,
    1.23 -    index: 'a -> term,
    1.24 +    index: 'a -> term list,
    1.25      content: 'a list,
    1.26      next: int,
    1.27      net: (int * 'a) Net.net};
    1.28 @@ -32,27 +32,31 @@
    1.29  fun mk_items eq index content next net =
    1.30    Items {eq = eq, index = index, content = content, next = next, net = net};
    1.31  
    1.32 +fun init eq index = mk_items eq index [] ~1 Net.empty;
    1.33 +
    1.34  fun content (Items {content, ...}) = content;
    1.35  fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
    1.36  
    1.37  
    1.38 -(* build net *)
    1.39 +(* standard operations *)
    1.40  
    1.41 -fun init eq index = mk_items eq index [] ~1 Net.empty;
    1.42 +fun member (Items {eq, index, net, ...}) x =
    1.43 +  exists (fn t => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t)) (index x);
    1.44  
    1.45 -fun add x (Items {eq, index, content, next, net}) =
    1.46 +fun cons x (Items {eq, index, content, next, net}) =
    1.47    mk_items eq index (x :: content) (next - 1)
    1.48 -    (Net.insert_term (K false) (index x, (next, x)) net);
    1.49 +    (fold (fn t => Net.insert_term_safe (eq o pairself #2) (t, (next, x))) (index x) net);
    1.50 +
    1.51  
    1.52 -fun merge (Items {eq, index, content = content1, ...}, Items {content = content2, ...}) =
    1.53 -  let val content = Library.merge eq (content1, content2)
    1.54 -  in fold_rev add content (init eq index) end;
    1.55 +fun merge (items1, Items {content = content2, ...}) =
    1.56 +  fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
    1.57  
    1.58 -fun delete x (items as Items {eq, index, content, next, net}) =
    1.59 -  if not (member eq content x) then items
    1.60 -  else mk_items eq index (remove eq x content) next
    1.61 -    (Net.delete_term (eq o pairself #2) (index x, (0, x)) net);
    1.62 +fun remove x (items as Items {eq, index, content, next, net}) =
    1.63 +  if member items x then
    1.64 +    mk_items eq index (Library.remove eq x content) next
    1.65 +      (fold (fn t => Net.delete_term_safe (eq o pairself #2) (t, (0, x))) (index x) net)
    1.66 +  else items;
    1.67  
    1.68 -fun insert x items = add x (delete x items);   (*ensure that added entry gets precedence*)
    1.69 +fun update x items = cons x (remove x items);
    1.70  
    1.71  end;