| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.Verification.Core
Synopsis
- class (Typeable v, Ord (VarKey v), Show (VarKey v), Typeable (VarKey v)) => VerifiableVar v where
- data VerifierError v
- newtype Verifier v a = Verifier {
- getVerifier :: ReaderT SMTConfig (ExceptT (VerifierError v) IO) 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
- type QueryState v = Map (VarKey v) (SomeSym v)
- newtype Query v a = Query {}
- 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
- 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)
Documentation
class (Typeable v, Ord (VarKey v), Show (VarKey v), Typeable (VarKey v)) => VerifiableVar v where 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 #
Instances
| VerifiableVar (WhileVar String) Source # | |
Defined in Language.While.Syntax Associated Types type VarKey (WhileVar String) :: Type Source # Methods symForVar :: WhileVar String a -> VarEnv (WhileVar String) -> Symbolic (VarSym (WhileVar String) a) Source # varKey :: WhileVar String a -> VarKey (WhileVar String) Source # eqVarTypes :: WhileVar String a -> WhileVar String b -> Maybe (a :~: b) Source # castVarSym :: WhileVar String a -> VarSym (WhileVar String) b -> Maybe (VarSym (WhileVar String) 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 |
Instances
| Show (VarKey v) => Show (VerifierError v) Source # | |
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) Source # | |
Defined in Language.Verification.Core Methods toException :: VerifierError v -> SomeException # fromException :: SomeException -> Maybe (VerifierError v) # displayException :: VerifierError v -> String # | |
| MonadError (VerifierError v) (Verifier v) Source # | |
Defined in Language.Verification.Core Methods throwError :: VerifierError v -> Verifier v a # catchError :: Verifier v a -> (VerifierError v -> Verifier v a) -> Verifier v a # | |
Constructors
| Verifier | |
Fields
| |
Instances
| MonadReader SMTConfig (Verifier v) Source # | |
| Monad (Verifier v) Source # | |
| Functor (Verifier v) Source # | |
| Applicative (Verifier v) Source # | |
Defined in Language.Verification.Core | |
| MonadIO (Verifier v) Source # | |
Defined in Language.Verification.Core | |
| MonadError (VerifierError v) (Verifier v) Source # | |
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) Source #
runVerifier :: VerifiableVar v => Verifier v a -> IO (Either (VerifierError v) a) Source #
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 #
evalPropSimple :: (HMonad expr, HTraversable expr, VerifiableVar v, Exception (VerifierError v), HFoldableAt SBV expr, VarSym v ~ SBV) => Prop (expr v) b -> Query v (SBV 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.
liftSymbolic :: Symbolic a -> Query v a Source #
throwQuery :: Exception (VerifierError v) => VerifierError v -> Query v a Source #
symbolVar :: (VerifiableVar v, Exception (VerifierError v)) => v a -> Query v (VarSym v a) Source #