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 trireturns a string representation oftri, whereFmaps to"false",Tmaps to"true", andUmaps 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
Uis mapped toNONE val isTrue : t -> bool-
isTrue trireturnstrueiftriisTandfalseotherwise. val isFalse : t -> bool-
isTrue trireturnstrueiftriisFandfalseotherwise. val isKnown : t -> bool-
isTrue trireturnsfalseiftriisUandtrueotherwise. val isUnknown : t -> bool-
isTrue trireturnstrueiftriisUandfalseotherwise. val not3 : t -> t-
not3 trireturns the logical negation oftri; it behaves likeBool.notif its argument is known and returnsUfornot3 U. val and3 : t * t -> t-
and3 (a, b)returns the logical conjunction ofaandb val or3 : t * t -> t-
or3 (a, b)returns the logical negation val exists3 : ('a -> t) -> 'a list -> t-
exists3 pred xsreturnsTif there exists an elementxinxsfor whichpred xreturnsT, andFifpredreturnsFfor all elements inxs; otherwise it returnsU. val all3 : ('a -> t) -> 'a list -> t-
all3 pred xsreturnsTifpred xreturnsTfor everyxinxs, it returnsFifpred xreturnsFfor at least onexinxs, and otherwise returnsU.