Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/Pure/General/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 3 kB

Quelle ord_list.ML Sprache: SML

(*  Title:      Pure/General/ord_list.ML
    Author:     Makarius

Ordered lists without duplicates -- a light-weight representation of
finite sets, all operations take linear time and economize heap usage.
*)

signature ORD_LIST =
sig
  type 'a T = 'a list
  val make: ('a * 'a -> order) -> 'a list -> 'a T
  val member: ('b * 'a -> order) -> 'a T -> 'b -> bool
  val insert: ('a * 'a -> order) -> 'a -> 'a T -> 'a T
  val remove: ('b * 'a -> order) -> 'b -> 'a T -> 'a T
  val subset: ('b * 'a -> order) -> 'b T * 'a T -> bool
  val union: ('a * 'a -> order) -> 'a T -> 'a T -> 'a T
  val unions: ('a * 'a -> order) -> 'a T list -> 'a T
  val merge: ('a * 'a -> order) -> 'a T * 'a T -> 'a T
  val inter: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
  val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
end;

structure Ord_List: ORD_LIST =
struct

type 'a T = 'a list;
fun make ord = sort_distinct ord;

(* single elements *)

fun find_index ord list x =
  let
    fun find i [] = ~ i
      | find i (y :: ys) =
          (case ord (x, y) of
            LESS => ~ i
          | EQUAL => i
          | GREATER => find (i + 1) ys);
  in find 1 list end;

fun member ord list x = find_index ord list x > 0;

fun insert ord x list =
  let
    fun insrt 1 ys = x :: ys
      | insrt i (y :: ys) = y :: insrt (i - 1) ys;
    val idx = find_index ord list x;
  in if idx > 0 then list else insrt (~ idx) list end;

fun remove ord x list =
  let
    fun rmove 1 (_ :: ys) = ys
      | rmove i (y :: ys) = y :: rmove (i - 1) ys;
    val idx = find_index ord list x;
  in if idx > 0 then rmove idx list else list end;

(* lists as sets *)

fun subset ord (list1, list2) =
  let
    fun sub [] _ = true
      | sub _ [] = false
      | sub (lst1 as x :: xs) (y :: ys) =
          (case ord (x, y) of
            LESS => false
          | EQUAL => sub xs ys
          | GREATER => sub lst1 ys);
  in sub list1 list2 end;

(* algebraic operations *)

exception SAME;
fun handle_same f x = f x handle SAME => x;

(*union: insert elements of first list into second list*)
fun union ord list1 list2 =
  let
    fun unio [] _ = raise SAME
      | unio xs [] = xs
      | unio (lst1 as x :: xs) (lst2 as y :: ys) =
          (case ord (x, y) of
            LESS => x :: handle_same (unio xs) lst2
          | EQUAL => y :: unio xs ys
          | GREATER => y :: unio lst1 ys);
  in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;

fun unions ord lists =
  let
    fun unios (xs :: ys :: rest) acc = unios rest (union ord xs ys :: acc)
      | unios [xs] (ys :: acc) = unios (union ord xs ys :: acc) []
      | unios [xs] [] = xs
      | unios [] [] = []
      | unios [] acc = unios acc [];
  in unios lists [] end;

fun merge ord (list1, list2) = union ord list2 list1;

(*intersection: filter second list for elements present in first list*)
fun inter ord list1 list2 =
  let
    fun intr _ [] = raise SAME
      | intr [] _ = []
      | intr (lst1 as x :: xs) (lst2 as y :: ys) =
          (case ord (x, y) of
            LESS => intr xs lst2
          | EQUAL => y :: intr xs ys
          | GREATER => handle_same (intr lst1) ys);
  in handle_same (intr list1) list2 end;

(*subtraction: filter second list for elements NOT present in first list*)
fun subtract ord list1 list2 =
  let
    fun subtr [] _ = raise SAME
      | subtr _ [] = raise SAME
      | subtr (lst1 as x :: xs) (lst2 as y :: ys) =
          (case ord (x, y) of
            LESS => subtr xs lst2
          | EQUAL => handle_same (subtr xs) ys
          | GREATER => y :: subtr lst1 ys);
  in handle_same (subtr list1) list2 end;

end;

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.