src/Pure/item_net.ML
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 68126 5da8b97d9183
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
     1 (*  Title:      Pure/item_net.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Efficient storage of items indexed by terms; preserves order and
     5 prefers later entries.
     6 *)
     7 
     8 signature ITEM_NET =
     9 sig
    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
    23 end;
    24 
    25 structure Item_Net: ITEM_NET =
    26 struct
    27 
    28 (* datatype *)
    29 
    30 datatype '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 
    38 fun mk_items eq index content next net =
    39   Items {eq = eq, index = index, content = content, next = next, net = net};
    40 
    41 fun init eq index = mk_items eq index [] ~1 Net.empty;
    42 fun is_empty (Items {content, ...}) = null content;
    43 
    44 fun content (Items {content, ...}) = content;
    45 fun length items = List.length (content items);
    46 fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
    47 fun retrieve_matching (Items {net, ...}) = order_list o Net.match_term net;
    48 
    49 
    50 (* standard operations *)
    51 
    52 fun 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 
    57 fun 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 
    63 fun 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 
    67 fun 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 
    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
    75       (fold (fn t => Net.delete_term_safe (eq o apply2 #2) (t, (0, x))) (index x) net)
    76   else items;
    77 
    78 fun update x items = cons x (remove x items);
    79 
    80 fun filter pred items =
    81   fold (fn x => not (pred x) ? remove x) (content items) items;
    82 
    83 end;