src/Pure/item_net.ML
changeset 30559 e5987a7ac5df
parent 29606 fedb8be05f24
child 33372 f380fbd6e329
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/item_net.ML	Tue Mar 17 14:12:06 2009 +0100
     1.3 @@ -0,0 +1,58 @@
     1.4 +(*  Title:      Pure/item_net.ML
     1.5 +    Author:     Markus Wenzel, TU Muenchen
     1.6 +
     1.7 +Efficient storage of items indexed by terms; preserves order and
     1.8 +prefers later entries.
     1.9 +*)
    1.10 +
    1.11 +signature ITEM_NET =
    1.12 +sig
    1.13 +  type 'a T
    1.14 +  val content: 'a T -> 'a list
    1.15 +  val retrieve: 'a T -> term -> 'a list
    1.16 +  val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
    1.17 +  val merge: 'a T * 'a T -> 'a T
    1.18 +  val delete: 'a -> 'a T -> 'a T
    1.19 +  val insert: 'a -> 'a T -> 'a T
    1.20 +end;
    1.21 +
    1.22 +structure Item_Net: ITEM_NET =
    1.23 +struct
    1.24 +
    1.25 +(* datatype *)
    1.26 +
    1.27 +datatype 'a T =
    1.28 +  Items of {
    1.29 +    eq: 'a * 'a -> bool,
    1.30 +    index: 'a -> term,
    1.31 +    content: 'a list,
    1.32 +    next: int,
    1.33 +    net: (int * 'a) Net.net};
    1.34 +
    1.35 +fun mk_items eq index content next net =
    1.36 +  Items {eq = eq, index = index, content = content, next = next, net = net};
    1.37 +
    1.38 +fun content (Items {content, ...}) = content;
    1.39 +fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
    1.40 +
    1.41 +
    1.42 +(* build net *)
    1.43 +
    1.44 +fun init eq index = mk_items eq index [] ~1 Net.empty;
    1.45 +
    1.46 +fun add 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 +
    1.50 +fun merge (Items {eq, index, content = content1, ...}, Items {content = content2, ...}) =
    1.51 +  let val content = Library.merge eq (content1, content2)
    1.52 +  in fold_rev add content (init eq index) end;
    1.53 +
    1.54 +fun delete x (items as Items {eq, index, content, next, net}) =
    1.55 +  if not (member eq content x) then items
    1.56 +  else mk_items eq index (remove eq x content) next
    1.57 +    (Net.delete_term (eq o pairself #2) (index x, (0, x)) net);
    1.58 +
    1.59 +fun insert x items = add x (delete x items);   (*ensure that added entry gets precedence*)
    1.60 +
    1.61 +end;