Language.Expression.Prop

Propositions and combinators for conveniently constructing them.

Proposition Types

type Prop = HFree LogicOp

Propositions over general expressions.

type Prop' ops v = Prop (HFree' ops v)

Propositions over expressions with the given list of operators.

DSL

expr :: expr a -> Prop expr a

Lift an expression into the land of propositions.

plit :: Bool -> Prop expr Bool

pnot :: Prop expr Bool -> Prop expr Bool

(*&&) :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool infixl 3

(*||) :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool infixl 2

(*->) :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool infixr 1

(*<->) :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool infix 1

propAnd :: [Prop expr Bool] -> Prop expr Bool

propOr :: [Prop expr Bool] -> Prop expr Bool

HTraversable

data LogicOp t a where

Logical operations

Constructors

LogLit :: Bool -> LogicOp t Bool

LogNot :: t Bool -> LogicOp t Bool

LogAnd :: t Bool -> t Bool -> LogicOp t Bool

LogOr :: t Bool -> t Bool -> LogicOp t Bool

LogImpl :: t Bool -> t Bool -> LogicOp t Bool

LogEquiv :: t Bool -> t Bool -> LogicOp t Bool

Instances

HTraversable LogicOp

Defined in Language.Expression.Prop

Methods

htraverse :: Applicative f => (forall (b :: u). t b -> f (t' b)) -> LogicOp t a -> f (LogicOp t' a)

hsequence :: Applicative f => LogicOp (Compose f t) a -> f (LogicOp t a)

HFunctor LogicOp

Defined in Language.Expression.Prop

Methods

hmap :: (forall (b :: u). t b -> t' b) -> LogicOp t a -> LogicOp t' a

HFoldableAt Identity LogicOp

Defined in Language.Expression.Prop

Methods

hfoldMap :: (forall (b :: k). t b -> Identity b) -> LogicOp t a -> Identity a

HFoldableAt SBV LogicOp

Defined in Language.Expression.Prop

Methods

hfoldMap :: (forall (b :: k). t b -> SBV b) -> LogicOp t a -> SBV a

Pretty2 LogicOp

Defined in Language.Expression.Prop

Methods

pretty2 :: Pretty1 t => LogicOp t a -> String

prettys2Prec :: Pretty1 t => Int -> LogicOp t a -> ShowS