    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Transformers.SymbolicEval
    -- Copyright : (c) Brian Schroeder
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- A demonstration of the use of the 'SymbolicT' and 'QueryT' transformers in
    -- the setting of symbolic program evaluation.
    --
    -- In this example, we perform symbolic evaluation across three steps:
    --
    -- 1. allocate free variables, so we can extract a model after evaluation
    -- 2. perform symbolic evaluation of a program and an associated property
    -- 3. querying the solver for whether it's possible to find a set of program
    --    inputs that falsify the property. if there is, we extract a model.
    --
    -- To simplify the example, our programs always have exactly two integer inputs
    -- named @x@ and @y@.
    -----------------------------------------------------------------------------

    {-# LANGUAGE DeriveFunctor              #-}
    {-# LANGUAGE GADTs                      #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE KindSignatures             #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Transformers.SymbolicEval where

    import Control.Monad.Except   (Except, ExceptT, MonadError, mapExceptT, runExceptT, throwError)
    import Control.Monad.Identity (Identity(runIdentity))
    import Control.Monad.IO.Class (MonadIO)
    import Control.Monad.Reader   (MonadReader(reader), asks, ReaderT, runReaderT)
    import Control.Monad.Trans    (lift)

    import Data.SBV.Dynamic   (SVal)
    import Data.SBV.Internals (SBV(SBV), unSBV)
    import Data.SBV.Trans
    import Data.SBV.Trans.Control

    -- * Allocation of symbolic variables, so we can extract a model later.

    -- | Monad for allocating free variables.
    newtype Alloc a = Alloc { Alloc a -> SymbolicT (ExceptT String IO) a
    runAlloc :: SymbolicT (ExceptT String IO) a }
        deriving (a -> Alloc b -> Alloc a
    (a -> b) -> Alloc a -> Alloc b
    (forall a b. (a -> b) -> Alloc a -> Alloc b)
    -> (forall a b. a -> Alloc b -> Alloc a) -> Functor Alloc
    forall a b. a -> Alloc b -> Alloc a
    forall a b. (a -> b) -> Alloc a -> Alloc b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> Alloc b -> Alloc a
    $c<$ :: forall a b. a -> Alloc b -> Alloc a
    fmap :: (a -> b) -> Alloc a -> Alloc b
    $cfmap :: forall a b. (a -> b) -> Alloc a -> Alloc b
    Functor, Functor Alloc
    a -> Alloc a
    Functor Alloc =>
    (forall a. a -> Alloc a)
    -> (forall a b. Alloc (a -> b) -> Alloc a -> Alloc b)
    -> (forall a b c. (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c)
    -> (forall a b. Alloc a -> Alloc b -> Alloc b)
    -> (forall a b. Alloc a -> Alloc b -> Alloc a)
    -> Applicative Alloc
    Alloc a -> Alloc b -> Alloc b
    Alloc a -> Alloc b -> Alloc a
    Alloc (a -> b) -> Alloc a -> Alloc b
    (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c
    forall a. a -> Alloc a
    forall a b. Alloc a -> Alloc b -> Alloc a
    forall a b. Alloc a -> Alloc b -> Alloc b
    forall a b. Alloc (a -> b) -> Alloc a -> Alloc b
    forall a b c. (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    <* :: Alloc a -> Alloc b -> Alloc a
    $c<* :: forall a b. Alloc a -> Alloc b -> Alloc a
    *> :: Alloc a -> Alloc b -> Alloc b
    $c*> :: forall a b. Alloc a -> Alloc b -> Alloc b
    liftA2 :: (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c
    $cliftA2 :: forall a b c. (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c
    <*> :: Alloc (a -> b) -> Alloc a -> Alloc b
    $c<*> :: forall a b. Alloc (a -> b) -> Alloc a -> Alloc b
    pure :: a -> Alloc a
    $cpure :: forall a. a -> Alloc a
    $cp1Applicative :: Functor Alloc
    Applicative, Applicative Alloc
    a -> Alloc a
    Applicative Alloc =>
    (forall a b. Alloc a -> (a -> Alloc b) -> Alloc b)
    -> (forall a b. Alloc a -> Alloc b -> Alloc b)
    -> (forall a. a -> Alloc a)
    -> Monad Alloc
    Alloc a -> (a -> Alloc b) -> Alloc b
    Alloc a -> Alloc b -> Alloc b
    forall a. a -> Alloc a
    forall a b. Alloc a -> Alloc b -> Alloc b
    forall a b. Alloc a -> (a -> Alloc b) -> Alloc b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    return :: a -> Alloc a
    $creturn :: forall a. a -> Alloc a
    >> :: Alloc a -> Alloc b -> Alloc b
    $c>> :: forall a b. Alloc a -> Alloc b -> Alloc b
    >>= :: Alloc a -> (a -> Alloc b) -> Alloc b
    $c>>= :: forall a b. Alloc a -> (a -> Alloc b) -> Alloc b
    $cp1Monad :: Applicative Alloc
    Monad, Monad Alloc
    Monad Alloc => (forall a. IO a -> Alloc a) -> MonadIO Alloc
    IO a -> Alloc a
    forall a. IO a -> Alloc a
    forall (m :: * -> *).
    Monad m =>
    (forall a. IO a -> m a) -> MonadIO m
    liftIO :: IO a -> Alloc a
    $cliftIO :: forall a. IO a -> Alloc a
    $cp1MonadIO :: Monad Alloc
    MonadIO,
                  MonadError String, MonadIO Alloc
    Alloc State
    MonadIO Alloc => Alloc State -> MonadSymbolic Alloc
    forall (m :: * -> *). MonadIO m => m State -> MonadSymbolic m
    symbolicEnv :: Alloc State
    $csymbolicEnv :: Alloc State
    $cp1MonadSymbolic :: MonadIO Alloc
    MonadSymbolic)

    -- | Environment holding allocated variables.
    data Env = Env { Env -> SBV Integer
    envX   :: SBV Integer
                   , Env -> SBV Integer
    envY   :: SBV Integer
                   , Env -> Maybe SVal
    result :: Maybe SVal -- could be integer or bool. during
                                          -- program evaluation, this is Nothing.
                                          -- we only have a value during property
                                          -- evaluation.
                   }
        deriving (Env -> Env -> Bool
    (Env -> Env -> Bool) -> (Env -> Env -> Bool) -> Eq Env
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Env -> Env -> Bool
    $c/= :: Env -> Env -> Bool
    == :: Env -> Env -> Bool
    $c== :: Env -> Env -> Bool
    Eq, Int -> Env -> ShowS
    [Env] -> ShowS
    Env -> String
    (Int -> Env -> ShowS)
    -> (Env -> String) -> ([Env] -> ShowS) -> Show Env
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Env] -> ShowS
    $cshowList :: [Env] -> ShowS
    show :: Env -> String
    $cshow :: Env -> String
    showsPrec :: Int -> Env -> ShowS
    $cshowsPrec :: Int -> Env -> ShowS
    Show)

    -- | Allocate an integer variable with the provided name.
    alloc :: String -> Alloc (SBV Integer)
    alloc :: String -> Alloc (SBV Integer)
    alloc "" = String -> Alloc (SBV Integer)
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError "tried to allocate unnamed value"
    alloc nm :: String
    nm = String -> Alloc (SBV Integer)
    forall a (m :: * -> *).
    (SymVal a, MonadSymbolic m) =>
    String -> m (SBV a)
    free String
    nm

    -- | Allocate an 'Env' holding all input variables for the program.
    allocEnv :: Alloc Env
    allocEnv :: Alloc Env
    allocEnv = do
        SBV Integer
    x <- String -> Alloc (SBV Integer)
    alloc "x"
        SBV Integer
    y <- String -> Alloc (SBV Integer)
    alloc "y"
        Env -> Alloc Env
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Env -> Alloc Env) -> Env -> Alloc Env
    forall a b. (a -> b) -> a -> b
    $ SBV Integer -> SBV Integer -> Maybe SVal -> Env
    Env SBV Integer
    x SBV Integer
    y Maybe SVal
    forall a. Maybe a
    Nothing

    -- * Symbolic term evaluation

    -- | The term language we use to express programs and properties.
    data Term :: * -> * where
        Var         :: String                       -> Term r
        Lit         :: Integer                      -> Term Integer
        Plus        :: Term Integer -> Term Integer -> Term Integer
        LessThan    :: Term Integer -> Term Integer -> Term Bool
        GreaterThan :: Term Integer -> Term Integer -> Term Bool
        Equals      :: Term Integer -> Term Integer -> Term Bool
        Not         :: Term Bool                    -> Term Bool
        Or          :: Term Bool    -> Term Bool    -> Term Bool
        And         :: Term Bool    -> Term Bool    -> Term Bool
        Implies     :: Term Bool    -> Term Bool    -> Term Bool

    -- | Monad for performing symbolic evaluation.
    newtype Eval a = Eval { Eval a -> ReaderT Env (Except String) a
    unEval :: ReaderT Env (Except String) a }
        deriving (a -> Eval b -> Eval a
    (a -> b) -> Eval a -> Eval b
    (forall a b. (a -> b) -> Eval a -> Eval b)
    -> (forall a b. a -> Eval b -> Eval a) -> Functor Eval
    forall a b. a -> Eval b -> Eval a
    forall a b. (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> Eval b -> Eval a
    $c<$ :: forall a b. a -> Eval b -> Eval a
    fmap :: (a -> b) -> Eval a -> Eval b
    $cfmap :: forall a b. (a -> b) -> Eval a -> Eval b
    Functor, Functor Eval
    a -> Eval a
    Functor Eval =>
    (forall a. a -> Eval a)
    -> (forall a b. Eval (a -> b) -> Eval a -> Eval b)
    -> (forall a b c. (a -> b -> c) -> Eval a -> Eval b -> Eval c)
    -> (forall a b. Eval a -> Eval b -> Eval b)
    -> (forall a b. Eval a -> Eval b -> Eval a)
    -> Applicative Eval
    Eval a -> Eval b -> Eval b
    Eval a -> Eval b -> Eval a
    Eval (a -> b) -> Eval a -> Eval b
    (a -> b -> c) -> Eval a -> Eval b -> Eval c
    forall a. a -> Eval a
    forall a b. Eval a -> Eval b -> Eval a
    forall a b. Eval a -> Eval b -> Eval b
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall a b c. (a -> b -> c) -> Eval a -> Eval b -> Eval c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    <* :: Eval a -> Eval b -> Eval a
    $c<* :: forall a b. Eval a -> Eval b -> Eval a
    *> :: Eval a -> Eval b -> Eval b
    $c*> :: forall a b. Eval a -> Eval b -> Eval b
    liftA2 :: (a -> b -> c) -> Eval a -> Eval b -> Eval c
    $cliftA2 :: forall a b c. (a -> b -> c) -> Eval a -> Eval b -> Eval c
    <*> :: Eval (a -> b) -> Eval a -> Eval b
    $c<*> :: forall a b. Eval (a -> b) -> Eval a -> Eval b
    pure :: a -> Eval a
    $cpure :: forall a. a -> Eval a
    $cp1Applicative :: Functor Eval
    Applicative, Applicative Eval
    a -> Eval a
    Applicative Eval =>
    (forall a b. Eval a -> (a -> Eval b) -> Eval b)
    -> (forall a b. Eval a -> Eval b -> Eval b)
    -> (forall a. a -> Eval a)
    -> Monad Eval
    Eval a -> (a -> Eval b) -> Eval b
    Eval a -> Eval b -> Eval b
    forall a. a -> Eval a
    forall a b. Eval a -> Eval b -> Eval b
    forall a b. Eval a -> (a -> Eval b) -> Eval b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    return :: a -> Eval a
    $creturn :: forall a. a -> Eval a
    >> :: Eval a -> Eval b -> Eval b
    $c>> :: forall a b. Eval a -> Eval b -> Eval b
    >>= :: Eval a -> (a -> Eval b) -> Eval b
    $c>>= :: forall a b. Eval a -> (a -> Eval b) -> Eval b
    $cp1Monad :: Applicative Eval
    Monad, MonadReader Env, MonadError String)

    -- | Unsafe cast for symbolic values. In production code, we would check types instead.
    unsafeCastSBV :: SBV a -> SBV b
    unsafeCastSBV :: SBV a -> SBV b
    unsafeCastSBV = SVal -> SBV b
    forall a. SVal -> SBV a
    SBV (SVal -> SBV b) -> (SBV a -> SVal) -> SBV a -> SBV b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV a -> SVal
    forall a. SBV a -> SVal
    unSBV

    -- | Symbolic evaluation function for 'Term'.
    eval :: Term r -> Eval (SBV r)
    eval :: Term r -> Eval (SBV r)
    eval (Var "x")           = (Env -> SBV r) -> Eval (SBV r)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ((Env -> SBV r) -> Eval (SBV r)) -> (Env -> SBV r) -> Eval (SBV r)
    forall a b. (a -> b) -> a -> b
    $ SBV Integer -> SBV r
    forall a b. SBV a -> SBV b
    unsafeCastSBV (SBV Integer -> SBV r) -> (Env -> SBV Integer) -> Env -> SBV r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Env -> SBV Integer
    envX
    eval (Var "y")           = (Env -> SBV r) -> Eval (SBV r)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ((Env -> SBV r) -> Eval (SBV r)) -> (Env -> SBV r) -> Eval (SBV r)
    forall a b. (a -> b) -> a -> b
    $ SBV Integer -> SBV r
    forall a b. SBV a -> SBV b
    unsafeCastSBV (SBV Integer -> SBV r) -> (Env -> SBV Integer) -> Env -> SBV r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Env -> SBV Integer
    envY
    eval (Var "result")      = do Maybe SVal
    mRes <- (Env -> Maybe SVal) -> Eval (Maybe SVal)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    reader Env -> Maybe SVal
    result
                                  case Maybe SVal
    mRes of
                                    Nothing -> String -> Eval (SBV r)
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError "unknown variable"
                                    Just sv :: SVal
    sv -> SBV r -> Eval (SBV r)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBV r -> Eval (SBV r)) -> SBV r -> Eval (SBV r)
    forall a b. (a -> b) -> a -> b
    $ SVal -> SBV r
    forall a. SVal -> SBV a
    SBV SVal
    sv
    eval (Var _)             = String -> Eval (SBV r)
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError "unknown variable"
    eval (Lit i :: Integer
    i)             = SBV Integer -> Eval (SBV r)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBV Integer -> Eval (SBV r)) -> SBV Integer -> Eval (SBV r)
    forall a b. (a -> b) -> a -> b
    $ Integer -> SBV Integer
    forall a. SymVal a => a -> SBV a
    literal Integer
    i
    eval (Plus        t1 :: Term Integer
    t1 t2 :: Term Integer
    t2) = SBV Integer -> SBV Integer -> SBV Integer
    forall a. Num a => a -> a -> a
    (+)   (SBV Integer -> SBV Integer -> SBV Integer)
    -> Eval (SBV Integer) -> Eval (SBV Integer -> SBV Integer)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term Integer -> Eval (SBV Integer)
    forall r. Term r -> Eval (SBV r)
    eval Term Integer
    t1 Eval (SBV Integer -> SBV Integer)
    -> Eval (SBV Integer) -> Eval (SBV Integer)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term Integer -> Eval (SBV Integer)
    forall r. Term r -> Eval (SBV r)
    eval Term Integer
    t2
    eval (LessThan    t1 :: Term Integer
    t1 t2 :: Term Integer
    t2) = SBV Integer -> SBV Integer -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    (.<)  (SBV Integer -> SBV Integer -> SBool)
    -> Eval (SBV Integer) -> Eval (SBV Integer -> SBool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term Integer -> Eval (SBV Integer)
    forall r. Term r -> Eval (SBV r)
    eval Term Integer
    t1 Eval (SBV Integer -> SBool) -> Eval (SBV Integer) -> Eval SBool
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term Integer -> Eval (SBV Integer)
    forall r. Term r -> Eval (SBV r)
    eval Term Integer
    t2
    eval (GreaterThan t1 :: Term Integer
    t1 t2 :: Term Integer
    t2) = SBV Integer -> SBV Integer -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    (.>)  (SBV Integer -> SBV Integer -> SBool)
    -> Eval (SBV Integer) -> Eval (SBV Integer -> SBool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term Integer -> Eval (SBV Integer)
    forall r. Term r -> Eval (SBV r)
    eval Term Integer
    t1 Eval (SBV Integer -> SBool) -> Eval (SBV Integer) -> Eval SBool
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term Integer -> Eval (SBV Integer)
    forall r. Term r -> Eval (SBV r)
    eval Term Integer
    t2
    eval (Equals      t1 :: Term Integer
    t1 t2 :: Term Integer
    t2) = SBV Integer -> SBV Integer -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    (.==) (SBV Integer -> SBV Integer -> SBool)
    -> Eval (SBV Integer) -> Eval (SBV Integer -> SBool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term Integer -> Eval (SBV Integer)
    forall r. Term r -> Eval (SBV r)
    eval Term Integer
    t1 Eval (SBV Integer -> SBool) -> Eval (SBV Integer) -> Eval SBool
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term Integer -> Eval (SBV Integer)
    forall r. Term r -> Eval (SBV r)
    eval Term Integer
    t2
    eval (Not         t :: Term Bool
    t)     = SBool -> SBool
    sNot  (SBool -> SBool) -> Eval SBool -> Eval SBool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term Bool -> Eval SBool
    forall r. Term r -> Eval (SBV r)
    eval Term Bool
    t
    eval (Or          t1 :: Term Bool
    t1 t2 :: Term Bool
    t2) = SBool -> SBool -> SBool
    (.||) (SBool -> SBool -> SBool) -> Eval SBool -> Eval (SBool -> SBool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term Bool -> Eval SBool
    forall r. Term r -> Eval (SBV r)
    eval Term Bool
    t1 Eval (SBool -> SBool) -> Eval SBool -> Eval SBool
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term Bool -> Eval SBool
    forall r. Term r -> Eval (SBV r)
    eval Term Bool
    t2
    eval (And         t1 :: Term Bool
    t1 t2 :: Term Bool
    t2) = SBool -> SBool -> SBool
    (.&&) (SBool -> SBool -> SBool) -> Eval SBool -> Eval (SBool -> SBool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term Bool -> Eval SBool
    forall r. Term r -> Eval (SBV r)
    eval Term Bool
    t1 Eval (SBool -> SBool) -> Eval SBool -> Eval SBool
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term Bool -> Eval SBool
    forall r. Term r -> Eval (SBV r)
    eval Term Bool
    t2
    eval (Implies     t1 :: Term Bool
    t1 t2 :: Term Bool
    t2) = SBool -> SBool -> SBool
    (.=>) (SBool -> SBool -> SBool) -> Eval SBool -> Eval (SBool -> SBool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term Bool -> Eval SBool
    forall r. Term r -> Eval (SBV r)
    eval Term Bool
    t1 Eval (SBool -> SBool) -> Eval SBool -> Eval SBool
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term Bool -> Eval SBool
    forall r. Term r -> Eval (SBV r)
    eval Term Bool
    t2

    -- | Runs symbolic evaluation, sending a 'Term' to a symbolic value (or
    -- failing). Used for symbolic evaluation of programs and properties.
    runEval :: Env -> Term a -> Except String (SBV a)
    runEval :: Env -> Term a -> Except String (SBV a)
    runEval env :: Env
    env term :: Term a
    term = ReaderT Env (Except String) (SBV a) -> Env -> Except String (SBV a)
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT (Eval (SBV a) -> ReaderT Env (Except String) (SBV a)
    forall a. Eval a -> ReaderT Env (Except String) a
    unEval (Eval (SBV a) -> ReaderT Env (Except String) (SBV a))
    -> Eval (SBV a) -> ReaderT Env (Except String) (SBV a)
    forall a b. (a -> b) -> a -> b
    $ Term a -> Eval (SBV a)
    forall r. Term r -> Eval (SBV r)
    eval Term a
    term) Env
    env

    -- | A program that can reference two input variables, @x@ and @y@.
    newtype Program a = Program (Term a)

    -- | A symbolic value representing the result of running a program -- its
    -- output.
    newtype Result = Result SVal

    -- | Makes a 'Result' from a symbolic value.
    mkResult :: SBV a -> Result
    mkResult :: SBV a -> Result
    mkResult = SVal -> Result
    Result (SVal -> Result) -> (SBV a -> SVal) -> SBV a -> Result
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SBV a -> SVal
    forall a. SBV a -> SVal
    unSBV

    -- | Performs symbolic evaluation of a 'Program'.
    runProgramEval :: Env -> Program a -> Except String Result
    runProgramEval :: Env -> Program a -> Except String Result
    runProgramEval env :: Env
    env (Program term :: Term a
    term) = SBV a -> Result
    forall a. SBV a -> Result
    mkResult (SBV a -> Result)
    -> ExceptT String Identity (SBV a) -> Except String Result
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Env -> Term a -> ExceptT String Identity (SBV a)
    forall a. Env -> Term a -> Except String (SBV a)
    runEval Env
    env Term a
    term

    -- * Property evaluation

    -- | A property describes a quality of a 'Program'. It is a 'Term' yields a
    -- boolean value.
    newtype Property = Property (Term Bool)

    -- | Performs symbolic evaluation of a 'Property.
    runPropertyEval :: Result -> Env -> Property -> Except String (SBV Bool)
    runPropertyEval :: Result -> Env -> Property -> Except String SBool
    runPropertyEval (Result res :: SVal
    res) env :: Env
    env (Property term :: Term Bool
    term) =
        Env -> Term Bool -> Except String SBool
    forall a. Env -> Term a -> Except String (SBV a)
    runEval (Env
    env { result :: Maybe SVal
    result = SVal -> Maybe SVal
    forall a. a -> Maybe a
    Just SVal
    res }) Term Bool
    term

    -- * Checking whether a program satisfies a property

    -- | The result of 'check'ing the combination of a 'Program' and a 'Property'.
    data CheckResult = Proved | Counterexample Integer Integer
        deriving (CheckResult -> CheckResult -> Bool
    (CheckResult -> CheckResult -> Bool)
    -> (CheckResult -> CheckResult -> Bool) -> Eq CheckResult
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: CheckResult -> CheckResult -> Bool
    $c/= :: CheckResult -> CheckResult -> Bool
    == :: CheckResult -> CheckResult -> Bool
    $c== :: CheckResult -> CheckResult -> Bool
    Eq, Int -> CheckResult -> ShowS
    [CheckResult] -> ShowS
    CheckResult -> String
    (Int -> CheckResult -> ShowS)
    -> (CheckResult -> String)
    -> ([CheckResult] -> ShowS)
    -> Show CheckResult
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [CheckResult] -> ShowS
    $cshowList :: [CheckResult] -> ShowS
    show :: CheckResult -> String
    $cshow :: CheckResult -> String
    showsPrec :: Int -> CheckResult -> ShowS
    $cshowsPrec :: Int -> CheckResult -> ShowS
    Show)

    -- | Sends an 'Identity' computation to an arbitrary monadic computation.
    generalize :: Monad m => Identity a -> m a
    generalize :: Identity a -> m a
    generalize = a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (a -> m a) -> (Identity a -> a) -> Identity a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Identity a -> a
    forall a. Identity a -> a
    runIdentity

    -- | Monad for querying a solver.
    newtype Q a = Q { Q a -> QueryT (ExceptT String IO) a
    runQ :: QueryT (ExceptT String IO) a }
        deriving (a -> Q b -> Q a
    (a -> b) -> Q a -> Q b
    (forall a b. (a -> b) -> Q a -> Q b)
    -> (forall a b. a -> Q b -> Q a) -> Functor Q
    forall a b. a -> Q b -> Q a
    forall a b. (a -> b) -> Q a -> Q b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> Q b -> Q a
    $c<$ :: forall a b. a -> Q b -> Q a
    fmap :: (a -> b) -> Q a -> Q b
    $cfmap :: forall a b. (a -> b) -> Q a -> Q b
    Functor, Functor Q
    a -> Q a
    Functor Q =>
    (forall a. a -> Q a)
    -> (forall a b. Q (a -> b) -> Q a -> Q b)
    -> (forall a b c. (a -> b -> c) -> Q a -> Q b -> Q c)
    -> (forall a b. Q a -> Q b -> Q b)
    -> (forall a b. Q a -> Q b -> Q a)
    -> Applicative Q
    Q a -> Q b -> Q b
    Q a -> Q b -> Q a
    Q (a -> b) -> Q a -> Q b
    (a -> b -> c) -> Q a -> Q b -> Q c
    forall a. a -> Q a
    forall a b. Q a -> Q b -> Q a
    forall a b. Q a -> Q b -> Q b
    forall a b. Q (a -> b) -> Q a -> Q b
    forall a b c. (a -> b -> c) -> Q a -> Q b -> Q c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    <* :: Q a -> Q b -> Q a
    $c<* :: forall a b. Q a -> Q b -> Q a
    *> :: Q a -> Q b -> Q b
    $c*> :: forall a b. Q a -> Q b -> Q b
    liftA2 :: (a -> b -> c) -> Q a -> Q b -> Q c
    $cliftA2 :: forall a b c. (a -> b -> c) -> Q a -> Q b -> Q c
    <*> :: Q (a -> b) -> Q a -> Q b
    $c<*> :: forall a b. Q (a -> b) -> Q a -> Q b
    pure :: a -> Q a
    $cpure :: forall a. a -> Q a
    $cp1Applicative :: Functor Q
    Applicative, Applicative Q
    a -> Q a
    Applicative Q =>
    (forall a b. Q a -> (a -> Q b) -> Q b)
    -> (forall a b. Q a -> Q b -> Q b)
    -> (forall a. a -> Q a)
    -> Monad Q
    Q a -> (a -> Q b) -> Q b
    Q a -> Q b -> Q b
    forall a. a -> Q a
    forall a b. Q a -> Q b -> Q b
    forall a b. Q a -> (a -> Q b) -> Q b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    return :: a -> Q a
    $creturn :: forall a. a -> Q a
    >> :: Q a -> Q b -> Q b
    $c>> :: forall a b. Q a -> Q b -> Q b
    >>= :: Q a -> (a -> Q b) -> Q b
    $c>>= :: forall a b. Q a -> (a -> Q b) -> Q b
    $cp1Monad :: Applicative Q
    Monad, Monad Q
    Monad Q => (forall a. IO a -> Q a) -> MonadIO Q
    IO a -> Q a
    forall a. IO a -> Q a
    forall (m :: * -> *).
    Monad m =>
    (forall a. IO a -> m a) -> MonadIO m
    liftIO :: IO a -> Q a
    $cliftIO :: forall a. IO a -> Q a
    $cp1MonadIO :: Monad Q
    MonadIO, MonadError String, Monad Q
    Q State
    Monad Q => Q State -> MonadQuery Q
    forall (m :: * -> *). Monad m => m State -> MonadQuery m
    queryState :: Q State
    $cqueryState :: Q State
    $cp1MonadQuery :: Monad Q
    MonadQuery)

    -- | Creates a computation that queries a solver and yields a 'CheckResult'.
    mkQuery :: Env -> Q CheckResult
    mkQuery :: Env -> Q CheckResult
    mkQuery env :: Env
    env = do
        CheckSatResult
    satResult <- Q CheckSatResult
    forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
    checkSat
        case CheckSatResult
    satResult of
            Sat   -> Integer -> Integer -> CheckResult
    Counterexample (Integer -> Integer -> CheckResult)
    -> Q Integer -> Q (Integer -> CheckResult)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SBV Integer -> Q Integer
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m, SymVal a) =>
    SBV a -> m a
    getValue (Env -> SBV Integer
    envX Env
    env)
                                    Q (Integer -> CheckResult) -> Q Integer -> Q CheckResult
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV Integer -> Q Integer
    forall (m :: * -> *) a.
    (MonadIO m, MonadQuery m, SymVal a) =>
    SBV a -> m a
    getValue (Env -> SBV Integer
    envY Env
    env)
            Unsat -> CheckResult -> Q CheckResult
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CheckResult
    Proved
            Unk   -> String -> Q CheckResult
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError "unknown"

    -- | Checks a 'Property' of a 'Program' (or fails).
    check :: Program a -> Property -> IO (Either String CheckResult)
    check :: Program a -> Property -> IO (Either String CheckResult)
    check program :: Program a
    program prop :: Property
    prop = ExceptT String IO CheckResult -> IO (Either String CheckResult)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT String IO CheckResult -> IO (Either String CheckResult))
    -> ExceptT String IO CheckResult -> IO (Either String CheckResult)
    forall a b. (a -> b) -> a -> b
    $ SMTConfig
    -> SymbolicT (ExceptT String IO) CheckResult
    -> ExceptT String IO CheckResult
    forall (m :: * -> *) a.
    MonadIO m =>
    SMTConfig -> SymbolicT m a -> m a
    runSMTWith SMTConfig
    z3 (SymbolicT (ExceptT String IO) CheckResult
     -> ExceptT String IO CheckResult)
    -> SymbolicT (ExceptT String IO) CheckResult
    -> ExceptT String IO CheckResult
    forall a b. (a -> b) -> a -> b
    $ do
        Env
    env <- Alloc Env -> SymbolicT (ExceptT String IO) Env
    forall a. Alloc a -> SymbolicT (ExceptT String IO) a
    runAlloc Alloc Env
    allocEnv
        SBool
    test <- ExceptT String IO SBool -> SymbolicT (ExceptT String IO) SBool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (ExceptT String IO SBool -> SymbolicT (ExceptT String IO) SBool)
    -> ExceptT String IO SBool -> SymbolicT (ExceptT String IO) SBool
    forall a b. (a -> b) -> a -> b
    $ (Identity (Either String SBool) -> IO (Either String SBool))
    -> Except String SBool -> ExceptT String IO SBool
    forall (m :: * -> *) e a (n :: * -> *) e' b.
    (m (Either e a) -> n (Either e' b))
    -> ExceptT e m a -> ExceptT e' n b
    mapExceptT Identity (Either String SBool) -> IO (Either String SBool)
    forall (m :: * -> *) a. Monad m => Identity a -> m a
    generalize (Except String SBool -> ExceptT String IO SBool)
    -> Except String SBool -> ExceptT String IO SBool
    forall a b. (a -> b) -> a -> b
    $ do
            Result
    res <- Env -> Program a -> Except String Result
    forall a. Env -> Program a -> Except String Result
    runProgramEval Env
    env Program a
    program
            Result -> Env -> Property -> Except String SBool
    runPropertyEval Result
    res Env
    env Property
    prop
        SBool -> SymbolicT (ExceptT String IO) ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT (ExceptT String IO) ())
    -> SBool -> SymbolicT (ExceptT String IO) ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot SBool
    test
        QueryT (ExceptT String IO) CheckResult
    -> SymbolicT (ExceptT String IO) CheckResult
    forall (m :: * -> *) a. ExtractIO m => QueryT m a -> SymbolicT m a
    query (QueryT (ExceptT String IO) CheckResult
     -> SymbolicT (ExceptT String IO) CheckResult)
    -> QueryT (ExceptT String IO) CheckResult
    -> SymbolicT (ExceptT String IO) CheckResult
    forall a b. (a -> b) -> a -> b
    $ Q CheckResult -> QueryT (ExceptT String IO) CheckResult
    forall a. Q a -> QueryT (ExceptT String IO) a
    runQ (Q CheckResult -> QueryT (ExceptT String IO) CheckResult)
    -> Q CheckResult -> QueryT (ExceptT String IO) CheckResult
    forall a b. (a -> b) -> a -> b
    $ Env -> Q CheckResult
    mkQuery Env
    env

    -- * Some examples

    -- | Check that @x+y+1@ generates a counter-example for the property that the
    -- result is less than @10@ when @x+y@ is at least @9@. We have:
    --
    -- >>> ex1
    -- Right (Counterexample 0 9)
    ex1 :: IO (Either String CheckResult)
    ex1 :: IO (Either String CheckResult)
    ex1 = Program Integer -> Property -> IO (Either String CheckResult)
    forall a. Program a -> Property -> IO (Either String CheckResult)
    check (Term Integer -> Program Integer
    forall a. Term a -> Program a
    Program  (Term Integer -> Program Integer)
    -> Term Integer -> Program Integer
    forall a b. (a -> b) -> a -> b
    $ String -> Term Integer
    forall r. String -> Term r
    Var "x" Term Integer -> Term Integer -> Term Integer
    `Plus` Integer -> Term Integer
    Lit 1 Term Integer -> Term Integer -> Term Integer
    `Plus` String -> Term Integer
    forall r. String -> Term r
    Var "y")
                (Term Bool -> Property
    Property (Term Bool -> Property) -> Term Bool -> Property
    forall a b. (a -> b) -> a -> b
    $ String -> Term Integer
    forall r. String -> Term r
    Var "result" Term Integer -> Term Integer -> Term Bool
    `LessThan` Integer -> Term Integer
    Lit 10)

    -- | Check that the program @x+y@ correctly produces a result greater than @1@ when
    -- both @x@ and @y@ are at least @1@. We have:
    --
    -- >>> ex2
    -- Right Proved
    ex2 :: IO (Either String CheckResult)
    ex2 :: IO (Either String CheckResult)
    ex2 = Program Integer -> Property -> IO (Either String CheckResult)
    forall a. Program a -> Property -> IO (Either String CheckResult)
    check (Term Integer -> Program Integer
    forall a. Term a -> Program a
    Program  (Term Integer -> Program Integer)
    -> Term Integer -> Program Integer
    forall a b. (a -> b) -> a -> b
    $ String -> Term Integer
    forall r. String -> Term r
    Var "x" Term Integer -> Term Integer -> Term Integer
    `Plus` String -> Term Integer
    forall r. String -> Term r
    Var "y")
                (Term Bool -> Property
    Property (Term Bool -> Property) -> Term Bool -> Property
    forall a b. (a -> b) -> a -> b
    $ (Term Integer -> Term Bool
    positive (String -> Term Integer
    forall r. String -> Term r
    Var "x") Term Bool -> Term Bool -> Term Bool
    `And` Term Integer -> Term Bool
    positive (String -> Term Integer
    forall r. String -> Term r
    Var "y"))
                    Term Bool -> Term Bool -> Term Bool
    `Implies` (String -> Term Integer
    forall r. String -> Term r
    Var "result" Term Integer -> Term Integer -> Term Bool
    `GreaterThan` Integer -> Term Integer
    Lit 1))
      where positive :: Term Integer -> Term Bool
    positive t :: Term Integer
    t = Term Integer
    t Term Integer -> Term Integer -> Term Bool
    `GreaterThan` Integer -> Term Integer
    Lit 0

    -- | Check that we catch the cases properly through the monad stack when there is a
    -- syntax error, like an undefined variable. We have:
    --
    -- >>> ex3
    -- Left "unknown variable"
    ex3 :: IO (Either String CheckResult)
    ex3 :: IO (Either String CheckResult)
    ex3 = Program Any -> Property -> IO (Either String CheckResult)
    forall a. Program a -> Property -> IO (Either String CheckResult)
    check (Term Any -> Program Any
    forall a. Term a -> Program a
    Program  (Term Any -> Program Any) -> Term Any -> Program Any
    forall a b. (a -> b) -> a -> b
    $ String -> Term Any
    forall r. String -> Term r
    Var "notAValidVar")
                (Term Bool -> Property
    Property (Term Bool -> Property) -> Term Bool -> Property
    forall a b. (a -> b) -> a -> b
    $ String -> Term Integer
    forall r. String -> Term r
    Var "result" Term Integer -> Term Integer -> Term Bool
    `LessThan` Integer -> Term Integer
    Lit 10)