wenzelm@30559: (*  Title:      Pure/item_net.ML
wenzelm@8298:     Author:     Markus Wenzel, TU Muenchen
wenzelm@8298: 
wenzelm@30559: Efficient storage of items indexed by terms; preserves order and
wenzelm@30559: prefers later entries.
wenzelm@8298: *)
wenzelm@8298: 
wenzelm@30559: signature ITEM_NET =
wenzelm@8298: sig
wenzelm@8298:   type 'a T
wenzelm@33372:   val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
wenzelm@30559:   val content: 'a T -> 'a list
wenzelm@42810:   val length: 'a T -> int
wenzelm@11776:   val retrieve: 'a T -> term -> 'a list
wenzelm@36296:   val member: 'a T -> 'a -> bool
wenzelm@8298:   val merge: 'a T * 'a T -> 'a T
wenzelm@33372:   val remove: 'a -> 'a T -> 'a T
wenzelm@33372:   val update: 'a -> 'a T -> 'a T
wenzelm@8298: end;
wenzelm@8298: 
wenzelm@30559: structure Item_Net: ITEM_NET =
wenzelm@8298: struct
wenzelm@8298: 
wenzelm@30559: (* datatype *)
wenzelm@8298: 
wenzelm@8298: datatype 'a T =
wenzelm@30559:   Items of {
wenzelm@8298:     eq: 'a * 'a -> bool,
wenzelm@33372:     index: 'a -> term list,
wenzelm@30559:     content: 'a list,
wenzelm@8298:     next: int,
wenzelm@12385:     net: (int * 'a) Net.net};
wenzelm@8298: 
wenzelm@30559: fun mk_items eq index content next net =
wenzelm@30559:   Items {eq = eq, index = index, content = content, next = next, net = net};
wenzelm@8298: 
wenzelm@33372: fun init eq index = mk_items eq index [] ~1 Net.empty;
wenzelm@33372: 
wenzelm@30559: fun content (Items {content, ...}) = content;
wenzelm@42810: fun length items = List.length (content items);
wenzelm@30559: fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
wenzelm@8298: 
wenzelm@8298: 
wenzelm@33372: (* standard operations *)
wenzelm@8298: 
wenzelm@33721: fun member (Items {eq, index, content, net, ...}) x =
wenzelm@33721:   (case index x of
wenzelm@33721:     [] => Library.member eq content x
wenzelm@33721:   | t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t));
wenzelm@8298: 
wenzelm@33372: fun cons x (Items {eq, index, content, next, net}) =
wenzelm@30559:   mk_items eq index (x :: content) (next - 1)
wenzelm@33721:     (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
wenzelm@33372: 
wenzelm@33372: fun merge (items1, Items {content = content2, ...}) =
wenzelm@33372:   fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
wenzelm@8298: 
wenzelm@33372: fun remove x (items as Items {eq, index, content, next, net}) =
wenzelm@33372:   if member items x then
wenzelm@33372:     mk_items eq index (Library.remove eq x content) next
wenzelm@33372:       (fold (fn t => Net.delete_term_safe (eq o pairself #2) (t, (0, x))) (index x) net)
wenzelm@33372:   else items;
wenzelm@8298: 
wenzelm@33372: fun update x items = cons x (remove x items);
wenzelm@8298: 
wenzelm@8298: end;