src/Pure/item_net.ML
author bulwahn
Tue Aug 31 08:00:53 2010 +0200 (2010-08-31)
changeset 38950 62578950e748
parent 36296 5cc547abd995
child 42810 2425068fe13a
permissions -rw-r--r--
storing options for prolog code generation in the theory
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@33372
    11
  val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
wenzelm@30559
    12
  val content: 'a T -> 'a list
wenzelm@11776
    13
  val retrieve: 'a T -> term -> 'a list
wenzelm@36296
    14
  val member: 'a T -> 'a -> bool
wenzelm@8298
    15
  val merge: 'a T * 'a T -> 'a T
wenzelm@33372
    16
  val remove: 'a -> 'a T -> 'a T
wenzelm@33372
    17
  val update: 'a -> 'a T -> 'a T
wenzelm@8298
    18
end;
wenzelm@8298
    19
wenzelm@30559
    20
structure Item_Net: ITEM_NET =
wenzelm@8298
    21
struct
wenzelm@8298
    22
wenzelm@30559
    23
(* datatype *)
wenzelm@8298
    24
wenzelm@8298
    25
datatype 'a T =
wenzelm@30559
    26
  Items of {
wenzelm@8298
    27
    eq: 'a * 'a -> bool,
wenzelm@33372
    28
    index: 'a -> term list,
wenzelm@30559
    29
    content: 'a list,
wenzelm@8298
    30
    next: int,
wenzelm@12385
    31
    net: (int * 'a) Net.net};
wenzelm@8298
    32
wenzelm@30559
    33
fun mk_items eq index content next net =
wenzelm@30559
    34
  Items {eq = eq, index = index, content = content, next = next, net = net};
wenzelm@8298
    35
wenzelm@33372
    36
fun init eq index = mk_items eq index [] ~1 Net.empty;
wenzelm@33372
    37
wenzelm@30559
    38
fun content (Items {content, ...}) = content;
wenzelm@30559
    39
fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
wenzelm@8298
    40
wenzelm@8298
    41
wenzelm@33372
    42
(* standard operations *)
wenzelm@8298
    43
wenzelm@33721
    44
fun member (Items {eq, index, content, net, ...}) x =
wenzelm@33721
    45
  (case index x of
wenzelm@33721
    46
    [] => Library.member eq content x
wenzelm@33721
    47
  | t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t));
wenzelm@8298
    48
wenzelm@33372
    49
fun cons x (Items {eq, index, content, next, net}) =
wenzelm@30559
    50
  mk_items eq index (x :: content) (next - 1)
wenzelm@33721
    51
    (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
wenzelm@33372
    52
wenzelm@33372
    53
fun merge (items1, Items {content = content2, ...}) =
wenzelm@33372
    54
  fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
wenzelm@8298
    55
wenzelm@33372
    56
fun remove x (items as Items {eq, index, content, next, net}) =
wenzelm@33372
    57
  if member items x then
wenzelm@33372
    58
    mk_items eq index (Library.remove eq x content) next
wenzelm@33372
    59
      (fold (fn t => Net.delete_term_safe (eq o pairself #2) (t, (0, x))) (index x) net)
wenzelm@33372
    60
  else items;
wenzelm@8298
    61
wenzelm@33372
    62
fun update x items = cons x (remove x items);
wenzelm@8298
    63
wenzelm@8298
    64
end;