src/Pure/item_net.ML
author wenzelm
Thu Oct 01 23:27:05 2009 +0200 (2009-10-01)
changeset 32843 c8f5a7c8353f
parent 30559 e5987a7ac5df
child 33372 f380fbd6e329
permissions -rw-r--r--
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
     1 (*  Title:      Pure/item_net.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Efficient storage of items indexed by terms; preserves order and
     5 prefers later entries.
     6 *)
     7 
     8 signature ITEM_NET =
     9 sig
    10   type 'a T
    11   val content: 'a T -> 'a list
    12   val retrieve: 'a T -> term -> 'a list
    13   val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
    14   val merge: 'a T * 'a T -> 'a T
    15   val delete: 'a -> 'a T -> 'a T
    16   val insert: 'a -> 'a T -> 'a T
    17 end;
    18 
    19 structure Item_Net: ITEM_NET =
    20 struct
    21 
    22 (* datatype *)
    23 
    24 datatype 'a T =
    25   Items of {
    26     eq: 'a * 'a -> bool,
    27     index: 'a -> term,
    28     content: 'a list,
    29     next: int,
    30     net: (int * 'a) Net.net};
    31 
    32 fun mk_items eq index content next net =
    33   Items {eq = eq, index = index, content = content, next = next, net = net};
    34 
    35 fun content (Items {content, ...}) = content;
    36 fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
    37 
    38 
    39 (* build net *)
    40 
    41 fun init eq index = mk_items eq index [] ~1 Net.empty;
    42 
    43 fun add x (Items {eq, index, content, next, net}) =
    44   mk_items eq index (x :: content) (next - 1)
    45     (Net.insert_term (K false) (index x, (next, x)) net);
    46 
    47 fun merge (Items {eq, index, content = content1, ...}, Items {content = content2, ...}) =
    48   let val content = Library.merge eq (content1, content2)
    49   in fold_rev add content (init eq index) end;
    50 
    51 fun delete x (items as Items {eq, index, content, next, net}) =
    52   if not (member eq content x) then items
    53   else mk_items eq index (remove eq x content) next
    54     (Net.delete_term (eq o pairself #2) (index x, (0, x)) net);
    55 
    56 fun insert x items = add x (delete x items);   (*ensure that added entry gets precedence*)
    57 
    58 end;