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