verifiable-expressions-0.6.0: An intermediate language for Hoare logic style verification.

Safe HaskellNone
LanguageHaskell2010

Language.Expression.Prop

Contents

Description

Propositions and combinators for conveniently constructing them.

Synopsis

Proposition Types

type Prop = HFree LogicOp Source #

Propositions over general expressions.

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

Propositions over expressions with the given list of operators.

DSL

expr :: expr a -> Prop expr a Source #

Lift an expression into the land of propositions.

plit :: Bool -> Prop expr Bool Source #

pnot :: Prop expr Bool -> Prop expr Bool Source #

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

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

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

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

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

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

HTraversable

data LogicOp t a where Source #

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 Source # 
Instance details

Defined in Language.Expression.Prop

Methods

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

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

HFunctor LogicOp Source # 
Instance details

Defined in Language.Expression.Prop

Methods

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

HFoldableAt Identity LogicOp Source # 
Instance details

Defined in Language.Expression.Prop

Methods

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

HFoldableAt SBV LogicOp Source # 
Instance details

Defined in Language.Expression.Prop

Methods

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

Pretty2 LogicOp Source # 
Instance details

Defined in Language.Expression.Prop

Methods

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

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