Rerefined.Predicate.Logical

Documentation

data LogicOp

Logical binary operator.

No need to disambiguate that these are binary operators, because there's only one logical unary operator Not.

Constructors

And

Or

Nand

Nor

Xor

Xnor

data Logical (op :: LogicOp) l r

A logical binary operation on two predicates.

Instances

(Predicate l, Predicate r, ReifyLogicOp op) => Predicate (Logical op l r :: Type)

Defined in Rerefined.Predicate.Logical

Methods

predicateName :: Proxy# (Logical op l r) -> Int -> ShowS

(Refine l a, Refine r a, ReifyLogicOp op) => Refine (Logical op l r :: Type) a

Defined in Rerefined.Predicate.Logical

Methods

validate :: Proxy# (Logical op l r) -> a -> Maybe (RefineFailure String)

class ReifyLogicOp (op :: LogicOp) where

Reify a logical binary operator type tag.

Methods

reifyLogicOpPretty :: String

reifyLogicOp :: (String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a

Instances

ReifyLogicOp 'And

Defined in Rerefined.Predicate.Logical

Methods

reifyLogicOpPretty :: String

reifyLogicOp :: (String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a

ReifyLogicOp 'Nand

Defined in Rerefined.Predicate.Logical

Methods

reifyLogicOpPretty :: String

reifyLogicOp :: (String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a

ReifyLogicOp 'Nor

Defined in Rerefined.Predicate.Logical

Methods

reifyLogicOpPretty :: String

reifyLogicOp :: (String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a

ReifyLogicOp 'Or

Defined in Rerefined.Predicate.Logical

Methods

reifyLogicOpPretty :: String

reifyLogicOp :: (String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a

ReifyLogicOp 'Xnor

Defined in Rerefined.Predicate.Logical

Methods

reifyLogicOpPretty :: String

reifyLogicOp :: (String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a

ReifyLogicOp 'Xor

Defined in Rerefined.Predicate.Logical

Methods

reifyLogicOpPretty :: String

reifyLogicOp :: (String -> [a] -> Maybe a) -> Maybe a -> Maybe a -> Maybe a

data Not p

Instances

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

Defined in Rerefined.Predicate.Logical

Methods

predicateName :: Proxy# (Not p) -> Int -> ShowS

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

Defined in Rerefined.Predicate.Logical

Methods

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

rerefineDeMorgans1 :: Refined (Not (Logical Or l r)) a -> Refined (Logical And (Not l) (Not r)) a

rerefineDeMorgans2 :: Refined (Not (Logical And l r)) a -> Refined (Logical Or (Not l) (Not r)) a