src/Pure/item_net.ML
author blanchet
Fri, 20 Dec 2013 20:36:38 +0100
changeset 54838 16511f84913c
parent 53941 54874871aa06
child 55741 b969263fcf02
permissions -rw-r--r--
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30559
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
     1
(*  Title:      Pure/item_net.ML
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     3
30559
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
     4
Efficient storage of items indexed by terms; preserves order and
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
     5
prefers later entries.
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     6
*)
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     7
30559
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
     8
signature ITEM_NET =
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
     9
sig
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    10
  type 'a T
33372
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    11
  val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
30559
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
    12
  val content: 'a T -> 'a list
42810
2425068fe13a slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents: 36296
diff changeset
    13
  val length: 'a T -> int
11776
d4f9de0bde28 support weight;
wenzelm
parents: 11693
diff changeset
    14
  val retrieve: 'a T -> term -> 'a list
53941
54874871aa06 Added Item_Net.retrieve_matching
lammich <lammich@in.tum.de>
parents: 42810
diff changeset
    15
  val retrieve_matching: 'a T -> term -> 'a list
36296
5cc547abd995 Item_Net/Named_Thms: export efficient member operation;
wenzelm
parents: 33721
diff changeset
    16
  val member: 'a T -> 'a -> bool
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    17
  val merge: 'a T * 'a T -> 'a T
33372
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    18
  val remove: 'a -> 'a T -> 'a T
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    19
  val update: 'a -> 'a T -> 'a T
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    20
end;
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    21
30559
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
    22
structure Item_Net: ITEM_NET =
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    23
struct
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    24
30559
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
    25
(* datatype *)
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    26
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    27
datatype 'a T =
30559
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
    28
  Items of {
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    29
    eq: 'a * 'a -> bool,
33372
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    30
    index: 'a -> term list,
30559
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
    31
    content: 'a list,
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    32
    next: int,
12385
389d11fb62c8 removed unused functionality (weight etc.);
wenzelm
parents: 12290
diff changeset
    33
    net: (int * 'a) Net.net};
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    34
30559
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
    35
fun mk_items eq index content next net =
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
    36
  Items {eq = eq, index = index, content = content, next = next, net = net};
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    37
33372
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    38
fun init eq index = mk_items eq index [] ~1 Net.empty;
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    39
30559
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
    40
fun content (Items {content, ...}) = content;
42810
2425068fe13a slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents: 36296
diff changeset
    41
fun length items = List.length (content items);
30559
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
    42
fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
53941
54874871aa06 Added Item_Net.retrieve_matching
lammich <lammich@in.tum.de>
parents: 42810
diff changeset
    43
fun retrieve_matching (Items {net, ...}) = order_list o Net.match_term net;
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    44
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    45
33372
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    46
(* standard operations *)
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    47
33721
f15c9ded9676 member/cons: slightly more correct treatment of multi-index, notably empty one;
wenzelm
parents: 33372
diff changeset
    48
fun member (Items {eq, index, content, net, ...}) x =
f15c9ded9676 member/cons: slightly more correct treatment of multi-index, notably empty one;
wenzelm
parents: 33372
diff changeset
    49
  (case index x of
f15c9ded9676 member/cons: slightly more correct treatment of multi-index, notably empty one;
wenzelm
parents: 33372
diff changeset
    50
    [] => Library.member eq content x
f15c9ded9676 member/cons: slightly more correct treatment of multi-index, notably empty one;
wenzelm
parents: 33372
diff changeset
    51
  | t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t));
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    52
33372
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    53
fun cons x (Items {eq, index, content, next, net}) =
30559
e5987a7ac5df turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents: 29606
diff changeset
    54
  mk_items eq index (x :: content) (next - 1)
33721
f15c9ded9676 member/cons: slightly more correct treatment of multi-index, notably empty one;
wenzelm
parents: 33372
diff changeset
    55
    (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
33372
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    56
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    57
fun merge (items1, Items {content = content2, ...}) =
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    58
  fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    59
33372
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    60
fun remove x (items as Items {eq, index, content, next, net}) =
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    61
  if member items x then
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    62
    mk_items eq index (Library.remove eq x content) next
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    63
      (fold (fn t => Net.delete_term_safe (eq o pairself #2) (t, (0, x))) (index x) net)
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    64
  else items;
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    65
33372
f380fbd6e329 allow multi-index;
wenzelm
parents: 30559
diff changeset
    66
fun update x items = cons x (remove x items);
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    67
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents:
diff changeset
    68
end;