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

Safe HaskellNone
LanguageHaskell2010

Language.Verification.Core

Synopsis

Documentation

class (Typeable v, Ord (VarKey v), Show (VarKey v), Typeable (VarKey v)) => VerifiableVar v where Source #

Minimal complete definition

symForVar, varKey, eqVarTypes, castVarSym

Associated Types

type VarKey v Source #

type VarSym v :: * -> * Source #

type VarEnv v :: * Source #

Methods

symForVar :: v a -> VarEnv v -> Symbolic (VarSym v a) Source #

varKey :: v a -> VarKey v Source #

eqVarTypes :: v a -> v b -> Maybe (a :~: b) Source #

castVarSym :: v a -> VarSym v b -> Maybe (VarSym v a) Source #

data VerifierError v Source #

Constructors

VEMismatchedSymbolType (VarKey v)

The same variable was used for two different symbol types

VESbvException String String

When running a query, SBV threw an exception

newtype Verifier v a Source #

Constructors

Verifier 

Instances

MonadReader SMTConfig (Verifier v) Source # 

Methods

ask :: Verifier v SMTConfig #

local :: (SMTConfig -> SMTConfig) -> Verifier v a -> Verifier v a #

reader :: (SMTConfig -> a) -> Verifier v a #

Monad (Verifier v) Source # 

Methods

(>>=) :: Verifier v a -> (a -> Verifier v b) -> Verifier v b #

(>>) :: Verifier v a -> Verifier v b -> Verifier v b #

return :: a -> Verifier v a #

fail :: String -> Verifier v a #

Functor (Verifier v) Source # 

Methods

fmap :: (a -> b) -> Verifier v a -> Verifier v b #

(<$) :: a -> Verifier v b -> Verifier v a #

Applicative (Verifier v) Source # 

Methods

pure :: a -> Verifier v a #

(<*>) :: Verifier v (a -> b) -> Verifier v a -> Verifier v b #

liftA2 :: (a -> b -> c) -> Verifier v a -> Verifier v b -> Verifier v c #

(*>) :: Verifier v a -> Verifier v b -> Verifier v b #

(<*) :: Verifier v a -> Verifier v b -> Verifier v a #

MonadIO (Verifier v) Source # 

Methods

liftIO :: IO a -> Verifier v a #

MonadError (VerifierError v) (Verifier v) Source # 

Methods

throwError :: VerifierError v -> Verifier v a #

catchError :: Verifier v a -> (VerifierError v -> Verifier v a) -> Verifier v a #

data SomeSym v where Source #

Constructors

SomeSym :: VarSym v a -> SomeSym v 

type QueryState v = Map (VarKey v) (SomeSym v) Source #

newtype Query v a Source #

Constructors

Query 

Instances

Monad (Query v) Source # 

Methods

(>>=) :: Query v a -> (a -> Query v b) -> Query v b #

(>>) :: Query v a -> Query v b -> Query v b #

return :: a -> Query v a #

fail :: String -> Query v a #

Functor (Query v) Source # 

Methods

fmap :: (a -> b) -> Query v a -> Query v b #

(<$) :: a -> Query v b -> Query v a #

Applicative (Query v) Source # 

Methods

pure :: a -> Query v a #

(<*>) :: Query v (a -> b) -> Query v a -> Query v b #

liftA2 :: (a -> b -> c) -> Query v a -> Query v b -> Query v c #

(*>) :: Query v a -> Query v b -> Query v b #

(<*) :: Query v a -> Query v b -> Query v a #

MonadIO (Query v) Source # 

Methods

liftIO :: IO a -> Query v a #

evalProp :: (HMonad expr, HTraversable expr, VerifiableVar v, Exception (VerifierError v), HFoldableAt k expr, HFoldableAt k LogicOp, Monad m) => (forall a. Query v a -> m a) -> (forall a. VarSym v a -> m (k a)) -> Prop (expr v) b -> m (k b) Source #

evalProp' :: (HMonad expr, HTraversable expr, VerifiableVar v, Exception (VerifierError v), HFoldableAt (Compose m k) expr, HFoldableAt (Compose m k) LogicOp, Monad m) => (forall a. Query v a -> m a) -> (forall a. VarSym v a -> m (k a)) -> Prop (expr v) b -> m (k b) Source #

subVar :: (HPointed expr, VerifiableVar v, Eq (VarKey v)) => expr v a -> v a -> v b -> expr v b Source #

If the two variables match in both type and name, return the given expression. Otherwise, return an expression just containing this variable.

This is substitution into an expression, where the old expression is just a variable.