Rerefined.Predicate.Logical

Documentation

data And l r

Logical conjunction. Also AND logic gate.

Instances

(Predicate l, Predicate r) => Predicate (And l r :: Type)

Precedence of 3 (matching &&).

Defined in Rerefined.Predicate.Logical.And

Associated Types

type PredicateName d (And l r) :: Symbol

(Refine l a, Refine r a, KnownPredicateName (And l r)) => Refine (And l r :: Type) a

Defined in Rerefined.Predicate.Logical.And

Methods

validate :: Proxy# (And l r) -> a -> Maybe RefineFailure

type PredicateName d (And l r :: Type)

Defined in Rerefined.Predicate.Logical.And

type PredicateName d (And l r :: Type) = PredicateNameBOp " \8743 " 3 d l r

data Iff l r

Logical biconditional ("if and only if"). Also the XNOR logic gate, or equivalence (loosely).

Instances

(Predicate l, Predicate r) => Predicate (Iff l r :: Type)

Precedence of 4 (matching ==).

Defined in Rerefined.Predicate.Logical.Iff

Associated Types

type PredicateName d (Iff l r) :: Symbol

(Refine l a, Refine r a, KnownPredicateName (Iff l r)) => Refine (Iff l r :: Type) a

Defined in Rerefined.Predicate.Logical.Iff

Methods

validate :: Proxy# (Iff l r) -> a -> Maybe RefineFailure

type PredicateName d (Iff l r :: Type)

Defined in Rerefined.Predicate.Logical.Iff

type PredicateName d (Iff l r :: Type) = PredicateNameBOp " \8596 " 4 d l r

data If l r

Logical implication. "If l then r".

Instances

(Predicate l, Predicate r) => Predicate (If l r :: Type)

Precedence of 4 (matching ==).

Defined in Rerefined.Predicate.Logical.If

Associated Types

type PredicateName d (If l r) :: Symbol

(Refine l a, Refine r a, KnownPredicateName (If l r)) => Refine (If l r :: Type) a

Defined in Rerefined.Predicate.Logical.If

Methods

validate :: Proxy# (If l r) -> a -> Maybe RefineFailure

type PredicateName d (If l r :: Type)

Defined in Rerefined.Predicate.Logical.If

type PredicateName d (If l r :: Type) = PredicateNameBOp " \8594 " 4 d l r

data Nand l r

NAND logic gate. Also called the Sheffer stroke, or non-conjunction.

Instances

(Predicate l, Predicate r) => Predicate (Nand l r :: Type)

Precedence of 3 (matching &&).

Defined in Rerefined.Predicate.Logical.Nand

Associated Types

type PredicateName d (Nand l r) :: Symbol

(Refine l a, Refine r a, KnownPredicateName (Nand l r)) => Refine (Nand l r :: Type) a

Defined in Rerefined.Predicate.Logical.Nand

Methods

validate :: Proxy# (Nand l r) -> a -> Maybe RefineFailure

type PredicateName d (Nand l r :: Type)

Defined in Rerefined.Predicate.Logical.Nand

type PredicateName d (Nand l r :: Type) = PredicateNameBOp " \8892 " 3 d l r

data Nor l r

NOR logic gate. Also called non-disjunction, or joint denial.

Instances

(Predicate l, Predicate r) => Predicate (Nor l r :: Type)

Precedence of 2 (matching ||).

Defined in Rerefined.Predicate.Logical.Nor

Associated Types

type PredicateName d (Nor l r) :: Symbol

(Refine l a, Refine r a, KnownPredicateName (Nor l r)) => Refine (Nor l r :: Type) a

Defined in Rerefined.Predicate.Logical.Nor

Methods

validate :: Proxy# (Nor l r) -> a -> Maybe RefineFailure

type PredicateName d (Nor l r :: Type)

Defined in Rerefined.Predicate.Logical.Nor

type PredicateName d (Nor l r :: Type) = PredicateNameBOp " \8893 " 2 d l r

data Not p

Logical negation. Also NOT logic gate, or logical complement.

Instances

Predicate p => Predicate (Not p :: Type)

Precedence of 9 (one below function application).

Defined in Rerefined.Predicate.Logical.Not

Associated Types

type PredicateName d (Not p) :: Symbol

(Refine p a, KnownPredicateName (Not p)) => Refine (Not p :: Type) a

Defined in Rerefined.Predicate.Logical.Not

Methods

validate :: Proxy# (Not p) -> a -> Maybe RefineFailure

type PredicateName d (Not p :: Type)

Defined in Rerefined.Predicate.Logical.Not

type PredicateName d (Not p :: Type) = ShowParen (d > 9) ("\172 " ++ PredicateName 10 p)

data Or l r

Logical disjunction. Also OR logic gate.

Instances

ReifyRelOp GTE

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp GTE :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp LTE

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp LTE :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp NEQ

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp NEQ :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

(Predicate l, Predicate r) => Predicate (Or l r :: Type)

Precedence of 2 (matching ||).

Defined in Rerefined.Predicate.Logical.Or

Associated Types

type PredicateName d (Or l r) :: Symbol

ReifyRelOp (Or 'EQ 'GT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'GT) :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp (Or 'EQ 'LT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'EQ 'LT) :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

ReifyRelOp (Or 'GT 'LT)

Defined in Rerefined.Predicate.Relational.Internal

Associated Types

type ShowRelOp (Or 'GT 'LT) :: Symbol

Methods

reifyRelOp :: Ord a => a -> a -> Bool

(Refine l a, Refine r a, KnownPredicateName (Or l r)) => Refine (Or l r :: Type) a

Defined in Rerefined.Predicate.Logical.Or

Methods

validate :: Proxy# (Or l r) -> a -> Maybe RefineFailure

type ShowRelOp GTE

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp GTE = ">="

type ShowRelOp LTE

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp LTE = "<="

type ShowRelOp NEQ

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp NEQ = "/="

type PredicateName d (Or l r :: Type)

Defined in Rerefined.Predicate.Logical.Or

type PredicateName d (Or l r :: Type) = PredicateNameBOp " \8744 " 2 d l r

type ShowRelOp (Or 'EQ 'GT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'EQ 'GT) = ShowRelOp GTE

type ShowRelOp (Or 'EQ 'LT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'EQ 'LT) = ShowRelOp LTE

type ShowRelOp (Or 'GT 'LT)

Hidden instance. You won't see this if you use the type synonyms.

Defined in Rerefined.Predicate.Relational.Internal

type ShowRelOp (Or 'GT 'LT) = ShowRelOp NEQ

data Xor l r

Logical exclusive disjunction. Also XOR logic gate.

Instances

(Predicate l, Predicate r) => Predicate (Xor l r :: Type)

Precedence of 4 (matching ==).

Defined in Rerefined.Predicate.Logical.Xor

Associated Types

type PredicateName d (Xor l r) :: Symbol

(Refine l a, Refine r a, KnownPredicateName (Xor l r)) => Refine (Xor l r :: Type) a

Defined in Rerefined.Predicate.Logical.Xor

Methods

validate :: Proxy# (Xor l r) -> a -> Maybe RefineFailure

type PredicateName d (Xor l r :: Type)

Defined in Rerefined.Predicate.Logical.Xor

type PredicateName d (Xor l r :: Type) = PredicateNameBOp " \8853 " 4 d l r

type family NormalizeLogicalStep op l r where ...

Equations

NormalizeLogicalStep Or l l = Cont l

NormalizeLogicalStep And l l = Cont l

NormalizeLogicalStep Nand l l = Cont1 (Not l)

NormalizeLogicalStep op l r = Done (op l r)

type family NormalizeLogical1Step op p where ...

Equations

NormalizeLogical1Step Not (Not p) = Cont p

NormalizeLogical1Step op p = Done (op p)

data Result kl

Constructors

Done Type

Cont kl

Cont1 Type

type family Idk1' p where ...

Equations

Idk1' (Not p) = Idk1 (NormalizeLogical1Step Not p)

Idk1' p = p