package electrod

  1. Overview
  2. Docs
Formal analysis for the Electrod formal pivot language

Install 

dune-project
 Dependency

github.com Readme Changelog MPL-2.0 License Edit opam file Versions (10)

Authors

  1. D
    David Chemouil
  2. J
    Julien Brunel

Maintainers

  1. D
    David Chemouil <david.chemouil+git@onera.fr>

Sources

electrod-0.7.1.tbz
sha256=e5d2278c99128621110cd015dafcbcae9792bbf2c8bb09d7b02c57d50fa28075
sha512=e08ecf720d35b6ee72f37d780cc3da22f61e22314ffd093ff3314fb89684b863b5c96c97375d48bcb4ba2838ec8f61a495105c989f292c5dbcd095e14f52bdba

doc/electrod.libelectrod/Libelectrod/Tuple_set/index.html

Module Libelectrod.Tuple_setSource

Type for sets of tuples.

Sourcetype t

Set of tuples. Invariant: all tuples in the tuple set have the same arity

Sourceval empty : t

The empty tuple set.

Sourceval singleton : Tuple.t -> t
Sourceval add : Tuple.t -> t -> t
Sourceval of_tuples : Tuple.t list -> t

Requires: tuples is a nonempty list for tuples of the same arity.

Sourceval inferred_arity : t -> int

Arity of a tuple set. 0 if the set is empty, n > 0 otherwise.

Sourceval is_empty : t -> bool

Tells whether the tuple set denotes the empty set.

Sourceval tuples : t -> Tuple.Set.t

Tuples in a tuple set.

Sourceval union : t -> t -> t

Computes the union of two tuple sets b1 and b2.

Requires: b1 and b2 have the same arity.

Sourceval inter : t -> t -> t

Computes the intersecion of two tuple sets b1 and b2.

Sourceval product : t -> t -> t

product b1 b2 computes the flat product of b1 and b2. Recall the product is empty if any of b1 or b2 is.

Sourceval subset : t -> t -> bool

subset b1 b2 returns true if b1 is included in b2.

Sourceval override : t -> t -> t

Computes the override b1 ++ b2 of two tuple sets b1 and b2.

Sourceval lproj : t -> t -> t

Computes the left projection s <: r of a set s and a relation r.

Sourceval rproj : t -> t -> t

Computes the right projection r :> s of a relation r and a set s.

Sourceval equal : t -> t -> bool

equal b1 b2 returns true if b1 is equal b2.

Sourceval compare : t -> t -> int

Compares tuple sets against the inclusion ordering

Sourceval mem : Tuple.t -> t -> bool

mem t ts tells whether t is in ts.

Sourceval size : t -> int

Cardinality of a tuple set

Sourceval diff : t -> t -> t

Set difference.

Sourceval transpose : t -> t

Transposition.

Sourceval diagonal : t -> t

Diagonal of a set.

Sourceval join : t -> t -> t

Join of two tuple sets.

Sourceval transitive_closure : t -> t

Guess.

Sourceval transitive_closure_is : t -> t

Computes the transitive closure of a tuple set using iterative sqaures

Sourceval filter : (Tuple.t -> bool) -> t -> t

Filters tuples depending on a predicate.

Sourceval map : (Tuple.t -> Tuple.t) -> t -> t
Sourceval to_iter : t -> Tuple.t CCSet.sequence
Sourceval to_list : t -> Tuple.t list
include Intf.Print.S with type t := t
Sourceval pp : t Fmtc.t
Sourceval to_string : t -> string