The Trilean structure

The Trilean structure implements a three-valued logic that includes a representation for unknown. It is loosely based on a Java API.

Synopsis

signature TRILEAN
structure Trilean : TRILEAN

Interface

datatype t = F | T | U

val toString : t -> string

val fromString : string -> t option
val scan : (char,'a) StringCvt.reader -> (t,'a) StringCvt.reader

val fromBool : bool -> t
val toBool : t -> bool option

val isTrue : t -> bool
val isFalse : t -> bool
val isKnown : t -> bool
val isUnknown : t -> bool

val not3 : t -> t
val and3 : t * t -> t
val or3 : t * t -> t

val exists3 : ('a -> t) -> 'a list -> t
val all3 : ('a -> t) -> 'a list -> t

Description

(* three-valued logic: false, true, or unknown *) datatype t = …​:: the representation of three-value logic. The constructors are

+

F

represents true

T

represents false

U

represents unknown

val toString : t -> string

toString tri returns a string representation of tri, where F maps to "false", T maps to "true", and U maps to "unknown".

val scan : (char,'a) StringCvt.reader -> (t,'a) StringCvt.reader

(* convert a string to a Trilean value; we accept "f", "t", "u",

  • "unk", "false", "true", and "unknown" (case insensitive) as valid

  • strings. *)

val fromString : string -> t option

converts a string to a Trilean value; it is equivalent to StringCvt.scanString scan.

val fromBool : bool -> t

maps a Boolean to its corresponding Trilean value.

val toBool : t -> bool option

converts a Trilean value to an optional Boolean, where U is mapped to NONE

val isTrue : t -> bool

isTrue tri returns true if tri is T and false otherwise.

val isFalse : t -> bool

isTrue tri returns true if tri is F and false otherwise.

val isKnown : t -> bool

isTrue tri returns false if tri is U and true otherwise.

val isUnknown : t -> bool

isTrue tri returns true if tri is U and false otherwise.

val not3 : t -> t

not3 tri returns the logical negation of tri; it behaves like Bool.not if its argument is known and returns U for not3 U.

val and3 : t * t -> t

and3 (a, b) returns the logical conjunction of a and b

val or3 : t * t -> t

or3 (a, b) returns the logical negation

val exists3 : ('a -> t) -> 'a list -> t

exists3 pred xs returns T if there exists an element x in xs for which pred x returns T, and F if pred returns F for all elements in xs; otherwise it returns U.

val all3 : ('a -> t) -> 'a list -> t

all3 pred xs returns T if pred x returns T for every x in xs, it returns F if pred x returns F for at least one x in xs, and otherwise returns U.

See Also