Language.Verification.Core

Documentation

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

Associated Types

type VarKey v

type VarSym v :: * -> *

type VarEnv v :: *

Methods

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

varKey :: v a -> VarKey v

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

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

Instances

VerifiableVar (WhileVar String)

Defined in Language.While.Syntax

Associated Types

type VarKey (WhileVar String) :: Type

type VarSym (WhileVar String) :: Type -> Type

type VarEnv (WhileVar String) :: Type

Methods

symForVar :: WhileVar String a -> VarEnv (WhileVar String) -> Symbolic (VarSym (WhileVar String) a)

varKey :: WhileVar String a -> VarKey (WhileVar String)

eqVarTypes :: WhileVar String a -> WhileVar String b -> Maybe (a :~: b)

castVarSym :: WhileVar String a -> VarSym (WhileVar String) b -> Maybe (VarSym (WhileVar String) a)

data VerifierError v

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

Instances

Show (VarKey v) => Show (VerifierError v)

Defined in Language.Verification.Core

Methods

showsPrec :: Int -> VerifierError v -> ShowS

show :: VerifierError v -> String

showList :: [VerifierError v] -> ShowS

(Typeable v, l ~ VarKey v, Show l, Typeable l) => Exception (VerifierError v)

Defined in Language.Verification.Core

Methods

toException :: VerifierError v -> SomeException

fromException :: SomeException -> Maybe (VerifierError v)

displayException :: VerifierError v -> String

MonadError (VerifierError v) (Verifier v)

Defined in Language.Verification.Core

Methods

throwError :: VerifierError v -> Verifier v a

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

newtype Verifier v a

Constructors

Verifier

Fields

• getVerifier :: ReaderT SMTConfig (ExceptT (VerifierError v) IO) a

Instances

MonadReader SMTConfig (Verifier v)

Defined in Language.Verification.Core

Methods

ask :: Verifier v SMTConfig

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

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

Monad (Verifier v)

Defined in Language.Verification.Core

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)

Defined in Language.Verification.Core

Methods

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

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

Applicative (Verifier v)

Defined in Language.Verification.Core

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)

Defined in Language.Verification.Core

Methods

liftIO :: IO a -> Verifier v a

MonadError (VerifierError v) (Verifier v)

Defined in Language.Verification.Core

Methods

throwError :: VerifierError v -> Verifier v a

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

runVerifierWith :: VerifiableVar v => SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)

runVerifier :: VerifiableVar v => Verifier v a -> IO (Either (VerifierError v) a)

data SomeSym v where

Constructors

SomeSym :: VarSym v a -> SomeSym v

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

newtype Query v a

Constructors

Query

Fields

• getQuery :: ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) a

Instances

Monad (Query v)

Defined in Language.Verification.Core

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)

Defined in Language.Verification.Core

Methods

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

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

Applicative (Query v)

Defined in Language.Verification.Core

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)

Defined in Language.Verification.Core

Methods

liftIO :: IO a -> Query v a

query :: VerifiableVar v => Query v SBool -> VarEnv v -> Verifier v Bool

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)

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)

evalPropSimple :: (HMonad expr, HTraversable expr, VerifiableVar v, Exception (VerifierError v), HFoldableAt SBV expr, VarSym v ~ SBV) => Prop (expr v) b -> Query v (SBV b)

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

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.

liftSymbolic :: Symbolic a -> Query v a

throwQuery :: Exception (VerifierError v) => VerifierError v -> Query v a

symbolVar :: (VerifiableVar v, Exception (VerifierError v)) => v a -> Query v (VarSym v a)