| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.Verification.Core
- 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 #
Minimal complete definition
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
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 |
Constructors
| Verifier | |
Fields
| |
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 #