products/sources/formale Sprachen/PVS/topology/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: tree_paths.prf   Sprache: SML

Untersuchung 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;

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.16Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff