src/Pure/item_net.ML
author wenzelm
Mon Dec 04 22:54:31 2017 +0100 (20 months ago)
changeset 67131 85d10959c2e4
parent 62165 b10046b14dd8
child 68126 5da8b97d9183
permissions -rw-r--r--
tuned signature;
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@42810
    13
  val length: 'a T -> int
wenzelm@11776
    14
  val retrieve: 'a T -> term -> 'a list
lammich@53941
    15
  val retrieve_matching: 'a T -> term -> 'a list
wenzelm@36296
    16
  val member: 'a T -> 'a -> bool
wenzelm@60946
    17
  val lookup: 'a T -> 'a -> 'a list
wenzelm@8298
    18
  val merge: 'a T * 'a T -> 'a T
wenzelm@33372
    19
  val remove: 'a -> 'a T -> 'a T
wenzelm@33372
    20
  val update: 'a -> 'a T -> 'a T
wenzelm@62165
    21
  val filter: ('a -> bool) -> 'a T -> 'a T
wenzelm@8298
    22
end;
wenzelm@8298
    23
wenzelm@30559
    24
structure Item_Net: ITEM_NET =
wenzelm@8298
    25
struct
wenzelm@8298
    26
wenzelm@30559
    27
(* datatype *)
wenzelm@8298
    28
wenzelm@8298
    29
datatype 'a T =
wenzelm@30559
    30
  Items of {
wenzelm@8298
    31
    eq: 'a * 'a -> bool,
wenzelm@33372
    32
    index: 'a -> term list,
wenzelm@30559
    33
    content: 'a list,
wenzelm@8298
    34
    next: int,
wenzelm@12385
    35
    net: (int * 'a) Net.net};
wenzelm@8298
    36
wenzelm@30559
    37
fun mk_items eq index content next net =
wenzelm@30559
    38
  Items {eq = eq, index = index, content = content, next = next, net = net};
wenzelm@8298
    39
wenzelm@33372
    40
fun init eq index = mk_items eq index [] ~1 Net.empty;
wenzelm@33372
    41
wenzelm@30559
    42
fun content (Items {content, ...}) = content;
wenzelm@42810
    43
fun length items = List.length (content items);
wenzelm@30559
    44
fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
lammich@53941
    45
fun retrieve_matching (Items {net, ...}) = order_list o Net.match_term net;
wenzelm@8298
    46
wenzelm@8298
    47
wenzelm@33372
    48
(* standard operations *)
wenzelm@8298
    49
wenzelm@33721
    50
fun member (Items {eq, index, content, net, ...}) x =
wenzelm@33721
    51
  (case index x of
wenzelm@33721
    52
    [] => Library.member eq content x
wenzelm@33721
    53
  | t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t));
wenzelm@8298
    54
wenzelm@60946
    55
fun lookup (Items {eq, index, content, net, ...}) x =
wenzelm@60946
    56
  (case index x of
wenzelm@60946
    57
    [] => content
wenzelm@60946
    58
  | t :: _ => map #2 (Net.unify_term net t))
wenzelm@60946
    59
  |> filter (fn y => eq (x, y));
wenzelm@60946
    60
wenzelm@33372
    61
fun cons x (Items {eq, index, content, next, net}) =
wenzelm@30559
    62
  mk_items eq index (x :: content) (next - 1)
wenzelm@33721
    63
    (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
wenzelm@33372
    64
wenzelm@55741
    65
fun merge
wenzelm@55741
    66
    (items1 as Items {net = net1, ...},
wenzelm@55741
    67
     items2 as Items {net = net2, content = content2, ...}) =
wenzelm@55741
    68
  if pointer_eq (net1, net2) then items1
wenzelm@55741
    69
  else if Net.is_empty net1 then items2
wenzelm@55741
    70
  else fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
wenzelm@8298
    71
wenzelm@33372
    72
fun remove x (items as Items {eq, index, content, next, net}) =
wenzelm@33372
    73
  if member items x then
wenzelm@33372
    74
    mk_items eq index (Library.remove eq x content) next
wenzelm@59058
    75
      (fold (fn t => Net.delete_term_safe (eq o apply2 #2) (t, (0, x))) (index x) net)
wenzelm@33372
    76
  else items;
wenzelm@8298
    77
wenzelm@33372
    78
fun update x items = cons x (remove x items);
wenzelm@8298
    79
wenzelm@62165
    80
fun filter pred items =
wenzelm@62165
    81
  fold (fn x => not (pred x) ? remove x) (content items) items;
wenzelm@62165
    82
wenzelm@8298
    83
end;