1(* Title: Pure/item_net.ML 2 Author: Markus Wenzel, TU Muenchen 3 4Efficient storage of items indexed by terms; preserves order and 5prefers later entries. 6*) 7 8signature ITEM_NET = 9sig 10 type 'a T 11 val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T 12 val is_empty: 'a T -> bool 13 val content: 'a T -> 'a list 14 val length: 'a T -> int 15 val retrieve: 'a T -> term -> 'a list 16 val retrieve_matching: 'a T -> term -> 'a list 17 val member: 'a T -> 'a -> bool 18 val lookup: 'a T -> 'a -> 'a list 19 val merge: 'a T * 'a T -> 'a T 20 val remove: 'a -> 'a T -> 'a T 21 val update: 'a -> 'a T -> 'a T 22 val filter: ('a -> bool) -> 'a T -> 'a T 23end; 24 25structure Item_Net: ITEM_NET = 26struct 27 28(* datatype *) 29 30datatype 'a T = 31 Items of { 32 eq: 'a * 'a -> bool, 33 index: 'a -> term list, 34 content: 'a list, 35 next: int, 36 net: (int * 'a) Net.net}; 37 38fun mk_items eq index content next net = 39 Items {eq = eq, index = index, content = content, next = next, net = net}; 40 41fun init eq index = mk_items eq index [] ~1 Net.empty; 42fun is_empty (Items {content, ...}) = null content; 43 44fun content (Items {content, ...}) = content; 45fun length items = List.length (content items); 46fun retrieve (Items {net, ...}) = order_list o Net.unify_term net; 47fun retrieve_matching (Items {net, ...}) = order_list o Net.match_term net; 48 49 50(* standard operations *) 51 52fun member (Items {eq, index, content, net, ...}) x = 53 (case index x of 54 [] => Library.member eq content x 55 | t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t)); 56 57fun lookup (Items {eq, index, content, net, ...}) x = 58 (case index x of 59 [] => content 60 | t :: _ => map #2 (Net.unify_term net t)) 61 |> filter (fn y => eq (x, y)); 62 63fun cons x (Items {eq, index, content, next, net}) = 64 mk_items eq index (x :: content) (next - 1) 65 (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net); 66 67fun merge (items1, items2) = 68 if pointer_eq (items1, items2) then items1 69 else if is_empty items1 then items2 70 else fold_rev (fn y => if member items1 y then I else cons y) (content items2) items1; 71 72fun 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 75 (fold (fn t => Net.delete_term_safe (eq o apply2 #2) (t, (0, x))) (index x) net) 76 else items; 77 78fun update x items = cons x (remove x items); 79 80fun filter pred items = 81 fold (fn x => not (pred x) ? remove x) (content items) items; 82 83end; 84