author | wenzelm |
Fri, 21 Apr 2017 15:26:24 +0200 | |
changeset 65534 | b6250ee6ce79 |
parent 62165 | b10046b14dd8 |
child 68126 | 5da8b97d9183 |
permissions | -rw-r--r-- |
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 | 2 |
Author: Markus Wenzel, TU Muenchen |
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 | 6 |
*) |
7 |
||
30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
29606
diff
changeset
|
8 |
signature ITEM_NET = |
8298 | 9 |
sig |
10 |
type 'a T |
|
33372 | 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 | 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 |
60946 | 17 |
val lookup: 'a T -> 'a -> 'a list |
8298 | 18 |
val merge: 'a T * 'a T -> 'a T |
33372 | 19 |
val remove: 'a -> 'a T -> 'a T |
20 |
val update: 'a -> 'a T -> 'a T |
|
62165 | 21 |
val filter: ('a -> bool) -> 'a T -> 'a T |
8298 | 22 |
end; |
23 |
||
30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
29606
diff
changeset
|
24 |
structure Item_Net: ITEM_NET = |
8298 | 25 |
struct |
26 |
||
30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
29606
diff
changeset
|
27 |
(* datatype *) |
8298 | 28 |
|
29 |
datatype 'a T = |
|
30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
29606
diff
changeset
|
30 |
Items of { |
8298 | 31 |
eq: 'a * 'a -> bool, |
33372 | 32 |
index: 'a -> term list, |
30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
29606
diff
changeset
|
33 |
content: 'a list, |
8298 | 34 |
next: int, |
12385 | 35 |
net: (int * 'a) Net.net}; |
8298 | 36 |
|
30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
29606
diff
changeset
|
37 |
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
|
38 |
Items {eq = eq, index = index, content = content, next = next, net = net}; |
8298 | 39 |
|
33372 | 40 |
fun init eq index = mk_items eq index [] ~1 Net.empty; |
41 |
||
30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
29606
diff
changeset
|
42 |
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
|
43 |
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
|
44 |
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
|
45 |
fun retrieve_matching (Items {net, ...}) = order_list o Net.match_term net; |
8298 | 46 |
|
47 |
||
33372 | 48 |
(* standard operations *) |
8298 | 49 |
|
33721
f15c9ded9676
member/cons: slightly more correct treatment of multi-index, notably empty one;
wenzelm
parents:
33372
diff
changeset
|
50 |
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
|
51 |
(case index x of |
f15c9ded9676
member/cons: slightly more correct treatment of multi-index, notably empty one;
wenzelm
parents:
33372
diff
changeset
|
52 |
[] => Library.member eq content x |
f15c9ded9676
member/cons: slightly more correct treatment of multi-index, notably empty one;
wenzelm
parents:
33372
diff
changeset
|
53 |
| t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t)); |
8298 | 54 |
|
60946 | 55 |
fun lookup (Items {eq, index, content, net, ...}) x = |
56 |
(case index x of |
|
57 |
[] => content |
|
58 |
| t :: _ => map #2 (Net.unify_term net t)) |
|
59 |
|> filter (fn y => eq (x, y)); |
|
60 |
||
33372 | 61 |
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
|
62 |
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
|
63 |
(fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net); |
33372 | 64 |
|
55741
b969263fcf02
optimize special case according to Library.merge (see also 8fbc355100f2);
wenzelm
parents:
53941
diff
changeset
|
65 |
fun merge |
b969263fcf02
optimize special case according to Library.merge (see also 8fbc355100f2);
wenzelm
parents:
53941
diff
changeset
|
66 |
(items1 as Items {net = net1, ...}, |
b969263fcf02
optimize special case according to Library.merge (see also 8fbc355100f2);
wenzelm
parents:
53941
diff
changeset
|
67 |
items2 as Items {net = net2, content = content2, ...}) = |
b969263fcf02
optimize special case according to Library.merge (see also 8fbc355100f2);
wenzelm
parents:
53941
diff
changeset
|
68 |
if pointer_eq (net1, net2) then items1 |
b969263fcf02
optimize special case according to Library.merge (see also 8fbc355100f2);
wenzelm
parents:
53941
diff
changeset
|
69 |
else if Net.is_empty net1 then items2 |
b969263fcf02
optimize special case according to Library.merge (see also 8fbc355100f2);
wenzelm
parents:
53941
diff
changeset
|
70 |
else fold_rev (fn y => if member items1 y then I else cons y) content2 items1; |
8298 | 71 |
|
33372 | 72 |
fun remove x (items as Items {eq, index, content, next, net}) = |
73 |
if member items x then |
|
74 |
mk_items eq index (Library.remove eq x content) next |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
55741
diff
changeset
|
75 |
(fold (fn t => Net.delete_term_safe (eq o apply2 #2) (t, (0, x))) (index x) net) |
33372 | 76 |
else items; |
8298 | 77 |
|
33372 | 78 |
fun update x items = cons x (remove x items); |
8298 | 79 |
|
62165 | 80 |
fun filter pred items = |
81 |
fold (fn x => not (pred x) ? remove x) (content items) items; |
|
82 |
||
8298 | 83 |
end; |