src/Pure/item_net.ML
author wenzelm
Sat May 14 21:42:17 2011 +0200 (2011-05-14 ago)
changeset 42810 2425068fe13a
parent 36296 5cc547abd995
child 53941 54874871aa06
permissions -rw-r--r--
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
     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 init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
    12   val content: 'a T -> 'a list
    13   val length: 'a T -> int
    14   val retrieve: 'a T -> term -> 'a list
    15   val member: 'a T -> 'a -> bool
    16   val merge: 'a T * 'a T -> 'a T
    17   val remove: 'a -> 'a T -> 'a T
    18   val update: 'a -> 'a T -> 'a T
    19 end;
    20 
    21 structure Item_Net: ITEM_NET =
    22 struct
    23 
    24 (* datatype *)
    25 
    26 datatype 'a T =
    27   Items of {
    28     eq: 'a * 'a -> bool,
    29     index: 'a -> term list,
    30     content: 'a list,
    31     next: int,
    32     net: (int * 'a) Net.net};
    33 
    34 fun mk_items eq index content next net =
    35   Items {eq = eq, index = index, content = content, next = next, net = net};
    36 
    37 fun init eq index = mk_items eq index [] ~1 Net.empty;
    38 
    39 fun content (Items {content, ...}) = content;
    40 fun length items = List.length (content items);
    41 fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
    42 
    43 
    44 (* standard operations *)
    45 
    46 fun member (Items {eq, index, content, net, ...}) x =
    47   (case index x of
    48     [] => Library.member eq content x
    49   | t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t));
    50 
    51 fun cons x (Items {eq, index, content, next, net}) =
    52   mk_items eq index (x :: content) (next - 1)
    53     (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
    54 
    55 fun merge (items1, Items {content = content2, ...}) =
    56   fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
    57 
    58 fun remove x (items as Items {eq, index, content, next, net}) =
    59   if member items x then
    60     mk_items eq index (Library.remove eq x content) next
    61       (fold (fn t => Net.delete_term_safe (eq o pairself #2) (t, (0, x))) (index x) net)
    62   else items;
    63 
    64 fun update x items = cons x (remove x items);
    65 
    66 end;