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/Roqc/clib/ (Beweissystem des Inria Version 9.1.0^©) Datei vom 15.8.2025 mit Größe 3 kB

Quelle predicate.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(************************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
(*                                                                     *)
(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
(*  en Automatique.  All rights reserved.  This file is distributed    *)
(*  under the terms of the GNU Library General Public License.         *)
(*                                                                     *)
(************************************************************************)

module type OrderedType =
  sig
    type t
    val compare: t -> t -> int
  end

module type S =
  sig
    type elt
    type t
    val empty: t
    val full: t
    val is_empty: t -> bool
    val is_full: t -> bool
    val mem: elt -> t -> bool
    val singleton: elt -> t
    val add: elt -> t -> t
    val remove: elt -> t -> t
    val union: t -> t -> t
    val inter: t -> t -> t
    val diff: t -> t -> t
    val complement: t -> t
    val equal: t -> t -> bool
    val subset: t -> t -> bool
    val elements: t -> bool * elt list
    val is_finite : t -> bool
  end

module Make(Ord: OrderedType) =
  struct
    module EltSet = Set.Make(Ord)

    type elt = Ord.t

    (* (false, s) represents a set which is equal to the set s
       (true, s)  represents a set which is equal to the complement of set s *)
    type t = bool * EltSet.t

    let is_finite (b,_) = not b

    let elements (b,s) = (b, EltSet.elements s)

    let empty = (false,EltSet.empty)
    let full = (true,EltSet.empty)

    (* assumes the set is infinite *)
    let is_empty (b,s) = not b && EltSet.is_empty s
    let is_full (b,s) = b && EltSet.is_empty s

    let mem x (b,s) =
      if b then not (EltSet.mem x s) else EltSet.mem x s

    let singleton x = (false,EltSet.singleton x)

    let add x (b,s) =
      if b then (b,EltSet.remove x s)
      else (b,EltSet.add x s)

    let remove x (b,s) =
      if b then (b,EltSet.add x s)
      else (b,EltSet.remove x s)

    let complement (b,s) = (not b, s)

    let union s1 s2 =
      match (s1,s2) with
          ((false,p1),(false,p2)) -> (false,EltSet.union p1 p2)
        | ((true,n1),(true,n2)) -> (true,EltSet.inter n1 n2)
        | ((false,p1),(true,n2)) -> (true,EltSet.diff n2 p1)
        | ((true,n1),(false,p2)) -> (true,EltSet.diff n1 p2)

    let inter s1 s2 =
      complement (union (complement s1) (complement s2))

    let diff s1 s2 = inter s1 (complement s2)

    (* assumes the set is infinite *)
    let subset s1 s2 =
      match (s1,s2) with
          ((false,p1),(false,p2)) -> EltSet.subset p1 p2
        | ((true,n1),(true,n2)) -> EltSet.subset n2 n1
        | ((false,p1),(true,n2)) -> EltSet.is_empty (EltSet.inter p1 n2)
        | ((true,_),(false,_)) -> false

    (* assumes the set is infinite *)
    let equal (b1,s1) (b2,s2) =
      b1=b2 && EltSet.equal s1 s2

  end

quality100%

¤ Dauer der Verarbeitung: 0.10 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.