Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: item_net.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/item_net.ML
    Author:     Markus Wenzel, TU Muenchen

Efficient storage of items indexed by terms; preserves order and
prefers later entries.
*)

signature ITEM_NET =
sig
  type 'a T
  val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
  val is_empty: 'a T -> bool
  val content: 'a T -> 'a list
  val length: 'a T -> int
  val retrieve: 'a T -> term -> 'a list
  val retrieve_matching: 'a T -> term -> 'a list
  val member: 'a T -> 'a -> bool
  val lookup: 'a T -> 'a -> 'a list
  val merge: 'a T * 'a T -> 'a T
  val remove: 'a -> 'a T -> 'a T
  val update: 'a -> 'a T -> 'a T
  val filter: ('a -> bool) -> 'a T -> 'a T
end;

structure Item_Net: ITEM_NET =
struct

(* datatype *)

datatype 'a T =
  Items of {
    eq: 'a * 'a -> bool,
    index: 'a -> term list,
    content: 'a list,
    next: int,
    net: (int * 'a) Net.net};

fun mk_items eq index content next net =
  Items {eq = eq, index = index, content = content, next = next, net = net};

fun init eq index = mk_items eq index [] ~1 Net.empty;
fun is_empty (Items {content, ...}) = null content;

fun content (Items {content, ...}) = content;
fun length items = List.length (content items);
fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
fun retrieve_matching (Items {net, ...}) = order_list o Net.match_term net;

(* standard operations *)

fun member (Items {eq, index, content, net, ...}) x =
  (case index x of
    [] => Library.member eq content x
  | t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t));

fun lookup (Items {eq, index, content, net, ...}) x =
  (case index x of
    [] => content
  | t :: _ => map #2 (Net.unify_term net t))
  |> filter (fn y => eq (x, y));

fun cons x (Items {eq, index, content, next, net}) =
  mk_items eq index (x :: content) (next - 1)
    (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);

fun merge (items1, items2) =
  if pointer_eq (items1, items2) then items1
  else if is_empty items1 then items2
  else fold_rev (fn y => if member items1 y then I else cons y) (content items2) items1;

fun remove x (items as Items {eq, index, content, next, net}) =
  if member items x then
    mk_items eq index (Library.remove eq x content) next
      (fold (fn t => Net.delete_term_safe (eq o apply2 #2) (t, (0, x))) (index x) net)
  else items;

fun update x items = cons x (remove x items);

fun filter pred items =
  fold (fn x => not (pred x) ? remove x) (content items) items;

end;

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.