{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FunctionalDependencies     #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures             #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE NoMonomorphismRestriction  #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE TypeSynonymInstances       #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE CPP                        #-}

module Language.Verification.Core where

import           Control.Exception
import           Data.Typeable            ((:~:) (..), Typeable)
import           Data.Functor.Compose

import           Control.Lens             hiding ((.>))
import           Control.Monad.Except
import           Control.Monad.Reader
import           Control.Monad.State

import           Data.Map                 (Map)
import           Data.SBV                 hiding (OrdSymbolic (..), ( # ))

import           Language.Expression
import           Language.Expression.Prop (LogicOp, Prop)

--------------------------------------------------------------------------------
--  Variables
--------------------------------------------------------------------------------

class (Typeable v, Ord (VarKey v), Show (VarKey v), Typeable (VarKey v)) => VerifiableVar v where
  type VarKey v
  type VarSym v :: * -> *
  type VarEnv v :: *

  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)

--------------------------------------------------------------------------------
--  Verifier Monad
--------------------------------------------------------------------------------

data VerifierError v
  = VEMismatchedSymbolType (VarKey v)
  -- ^ The same variable was used for two different symbol types
  | VESbvException String String
  -- ^ When running a query, SBV threw an exception

deriving instance Show (VarKey v) => Show (VerifierError v)
deriving instance Typeable (VarKey v) => Typeable (VerifierError v)

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

  displayException :: VerifierError v -> String
displayException = \case
    VEMismatchedSymbolType VarKey v
l ->
      String
"variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ l -> String
forall a. Show a => a -> String
show l
VarKey v
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" was used at two different types"

    VESbvException String
message (String
_ {- location -}) ->
      String
"exception from SBV:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
message

newtype Verifier v a =
  Verifier
  { Verifier v a -> ReaderT SMTConfig (ExceptT (VerifierError v) IO) a
getVerifier :: ReaderT SMTConfig (ExceptT (VerifierError v) IO) a
  }
  deriving ( a -> Verifier v b -> Verifier v a
(a -> b) -> Verifier v a -> Verifier v b
(forall a b. (a -> b) -> Verifier v a -> Verifier v b)
-> (forall a b. a -> Verifier v b -> Verifier v a)
-> Functor (Verifier v)
forall a b. a -> Verifier v b -> Verifier v a
forall a b. (a -> b) -> Verifier v a -> Verifier v b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (v :: * -> *) a b. a -> Verifier v b -> Verifier v a
forall (v :: * -> *) a b. (a -> b) -> Verifier v a -> Verifier v b
<$ :: a -> Verifier v b -> Verifier v a
$c<$ :: forall (v :: * -> *) a b. a -> Verifier v b -> Verifier v a
fmap :: (a -> b) -> Verifier v a -> Verifier v b
$cfmap :: forall (v :: * -> *) a b. (a -> b) -> Verifier v a -> Verifier v b
Functor
           , Functor (Verifier v)
a -> Verifier v a
Functor (Verifier v)
-> (forall a. a -> Verifier v a)
-> (forall a b.
    Verifier v (a -> b) -> Verifier v a -> Verifier v b)
-> (forall a b c.
    (a -> b -> c) -> Verifier v a -> Verifier v b -> Verifier v c)
-> (forall a b. Verifier v a -> Verifier v b -> Verifier v b)
-> (forall a b. Verifier v a -> Verifier v b -> Verifier v a)
-> Applicative (Verifier v)
Verifier v a -> Verifier v b -> Verifier v b
Verifier v a -> Verifier v b -> Verifier v a
Verifier v (a -> b) -> Verifier v a -> Verifier v b
(a -> b -> c) -> Verifier v a -> Verifier v b -> Verifier v c
forall a. a -> Verifier v a
forall a b. Verifier v a -> Verifier v b -> Verifier v a
forall a b. Verifier v a -> Verifier v b -> Verifier v b
forall a b. Verifier v (a -> b) -> Verifier v a -> Verifier v b
forall a b c.
(a -> b -> c) -> Verifier v a -> Verifier v b -> Verifier v c
forall (v :: * -> *). Functor (Verifier v)
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
forall (v :: * -> *) a. a -> Verifier v a
forall (v :: * -> *) a b.
Verifier v a -> Verifier v b -> Verifier v a
forall (v :: * -> *) a b.
Verifier v a -> Verifier v b -> Verifier v b
forall (v :: * -> *) a b.
Verifier v (a -> b) -> Verifier v a -> Verifier v b
forall (v :: * -> *) a b c.
(a -> b -> c) -> Verifier v a -> Verifier v b -> Verifier v c
<* :: Verifier v a -> Verifier v b -> Verifier v a
$c<* :: forall (v :: * -> *) a b.
Verifier v a -> Verifier v b -> Verifier v a
*> :: Verifier v a -> Verifier v b -> Verifier v b
$c*> :: forall (v :: * -> *) a b.
Verifier v a -> Verifier v b -> Verifier v b
liftA2 :: (a -> b -> c) -> Verifier v a -> Verifier v b -> Verifier v c
$cliftA2 :: forall (v :: * -> *) a b c.
(a -> b -> c) -> Verifier v a -> Verifier v b -> Verifier v c
<*> :: Verifier v (a -> b) -> Verifier v a -> Verifier v b
$c<*> :: forall (v :: * -> *) a b.
Verifier v (a -> b) -> Verifier v a -> Verifier v b
pure :: a -> Verifier v a
$cpure :: forall (v :: * -> *) a. a -> Verifier v a
$cp1Applicative :: forall (v :: * -> *). Functor (Verifier v)
Applicative
           , Applicative (Verifier v)
a -> Verifier v a
Applicative (Verifier v)
-> (forall a b.
    Verifier v a -> (a -> Verifier v b) -> Verifier v b)
-> (forall a b. Verifier v a -> Verifier v b -> Verifier v b)
-> (forall a. a -> Verifier v a)
-> Monad (Verifier v)
Verifier v a -> (a -> Verifier v b) -> Verifier v b
Verifier v a -> Verifier v b -> Verifier v b
forall a. a -> Verifier v a
forall a b. Verifier v a -> Verifier v b -> Verifier v b
forall a b. Verifier v a -> (a -> Verifier v b) -> Verifier v b
forall (v :: * -> *). Applicative (Verifier v)
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
forall (v :: * -> *) a. a -> Verifier v a
forall (v :: * -> *) a b.
Verifier v a -> Verifier v b -> Verifier v b
forall (v :: * -> *) a b.
Verifier v a -> (a -> Verifier v b) -> Verifier v b
return :: a -> Verifier v a
$creturn :: forall (v :: * -> *) a. a -> Verifier v a
>> :: Verifier v a -> Verifier v b -> Verifier v b
$c>> :: forall (v :: * -> *) a b.
Verifier v a -> Verifier v b -> Verifier v b
>>= :: Verifier v a -> (a -> Verifier v b) -> Verifier v b
$c>>= :: forall (v :: * -> *) a b.
Verifier v a -> (a -> Verifier v b) -> Verifier v b
$cp1Monad :: forall (v :: * -> *). Applicative (Verifier v)
Monad
           , Monad (Verifier v)
Monad (Verifier v)
-> (forall a. IO a -> Verifier v a) -> MonadIO (Verifier v)
IO a -> Verifier v a
forall a. IO a -> Verifier v a
forall (v :: * -> *). Monad (Verifier v)
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
forall (v :: * -> *) a. IO a -> Verifier v a
liftIO :: IO a -> Verifier v a
$cliftIO :: forall (v :: * -> *) a. IO a -> Verifier v a
$cp1MonadIO :: forall (v :: * -> *). Monad (Verifier v)
MonadIO
           , MonadReader SMTConfig
           , MonadError (VerifierError v)
           )

runVerifierWith
  :: (VerifiableVar v)
  => SMTConfig
  -> Verifier v a
  -> IO (Either (VerifierError v) a)
runVerifierWith :: SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)
runVerifierWith SMTConfig
config (Verifier ReaderT SMTConfig (ExceptT (VerifierError v) IO) a
action) = ExceptT (VerifierError v) IO a -> IO (Either (VerifierError v) a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ReaderT SMTConfig (ExceptT (VerifierError v) IO) a
-> SMTConfig -> ExceptT (VerifierError v) IO a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT SMTConfig (ExceptT (VerifierError v) IO) a
action SMTConfig
config)

runVerifier
  :: VerifiableVar v
  => Verifier v a -> IO (Either (VerifierError v) a)
runVerifier :: Verifier v a -> IO (Either (VerifierError v) a)
runVerifier = SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)
forall (v :: * -> *) a.
VerifiableVar v =>
SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)
runVerifierWith SMTConfig
defaultSMTCfg

--------------------------------------------------------------------------------
--  Query Monad
--------------------------------------------------------------------------------

data SomeSym v where
  SomeSym :: VarSym v a -> SomeSym v

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

newtype Query v a =
  Query
  { Query v a -> ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) a
getQuery :: ReaderT (VarEnv v) (
      StateT (QueryState v) Symbolic) a
  }
  deriving ( a -> Query v b -> Query v a
(a -> b) -> Query v a -> Query v b
(forall a b. (a -> b) -> Query v a -> Query v b)
-> (forall a b. a -> Query v b -> Query v a) -> Functor (Query v)
forall a b. a -> Query v b -> Query v a
forall a b. (a -> b) -> Query v a -> Query v b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (v :: * -> *) a b. a -> Query v b -> Query v a
forall (v :: * -> *) a b. (a -> b) -> Query v a -> Query v b
<$ :: a -> Query v b -> Query v a
$c<$ :: forall (v :: * -> *) a b. a -> Query v b -> Query v a
fmap :: (a -> b) -> Query v a -> Query v b
$cfmap :: forall (v :: * -> *) a b. (a -> b) -> Query v a -> Query v b
Functor
           , Functor (Query v)
a -> Query v a
Functor (Query v)
-> (forall a. a -> Query v a)
-> (forall a b. Query v (a -> b) -> Query v a -> Query v b)
-> (forall a b c.
    (a -> b -> c) -> Query v a -> Query v b -> Query v c)
-> (forall a b. Query v a -> Query v b -> Query v b)
-> (forall a b. Query v a -> Query v b -> Query v a)
-> Applicative (Query v)
Query v a -> Query v b -> Query v b
Query v a -> Query v b -> Query v a
Query v (a -> b) -> Query v a -> Query v b
(a -> b -> c) -> Query v a -> Query v b -> Query v c
forall a. a -> Query v a
forall a b. Query v a -> Query v b -> Query v a
forall a b. Query v a -> Query v b -> Query v b
forall a b. Query v (a -> b) -> Query v a -> Query v b
forall a b c. (a -> b -> c) -> Query v a -> Query v b -> Query v c
forall (v :: * -> *). Functor (Query v)
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
forall (v :: * -> *) a. a -> Query v a
forall (v :: * -> *) a b. Query v a -> Query v b -> Query v a
forall (v :: * -> *) a b. Query v a -> Query v b -> Query v b
forall (v :: * -> *) a b.
Query v (a -> b) -> Query v a -> Query v b
forall (v :: * -> *) a b c.
(a -> b -> c) -> Query v a -> Query v b -> Query v c
<* :: Query v a -> Query v b -> Query v a
$c<* :: forall (v :: * -> *) a b. Query v a -> Query v b -> Query v a
*> :: Query v a -> Query v b -> Query v b
$c*> :: forall (v :: * -> *) a b. Query v a -> Query v b -> Query v b
liftA2 :: (a -> b -> c) -> Query v a -> Query v b -> Query v c
$cliftA2 :: forall (v :: * -> *) a b c.
(a -> b -> c) -> Query v a -> Query v b -> Query v c
<*> :: Query v (a -> b) -> Query v a -> Query v b
$c<*> :: forall (v :: * -> *) a b.
Query v (a -> b) -> Query v a -> Query v b
pure :: a -> Query v a
$cpure :: forall (v :: * -> *) a. a -> Query v a
$cp1Applicative :: forall (v :: * -> *). Functor (Query v)
Applicative
           , Applicative (Query v)
a -> Query v a
Applicative (Query v)
-> (forall a b. Query v a -> (a -> Query v b) -> Query v b)
-> (forall a b. Query v a -> Query v b -> Query v b)
-> (forall a. a -> Query v a)
-> Monad (Query v)
Query v a -> (a -> Query v b) -> Query v b
Query v a -> Query v b -> Query v b
forall a. a -> Query v a
forall a b. Query v a -> Query v b -> Query v b
forall a b. Query v a -> (a -> Query v b) -> Query v b
forall (v :: * -> *). Applicative (Query v)
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
forall (v :: * -> *) a. a -> Query v a
forall (v :: * -> *) a b. Query v a -> Query v b -> Query v b
forall (v :: * -> *) a b.
Query v a -> (a -> Query v b) -> Query v b
return :: a -> Query v a
$creturn :: forall (v :: * -> *) a. a -> Query v a
>> :: Query v a -> Query v b -> Query v b
$c>> :: forall (v :: * -> *) a b. Query v a -> Query v b -> Query v b
>>= :: Query v a -> (a -> Query v b) -> Query v b
$c>>= :: forall (v :: * -> *) a b.
Query v a -> (a -> Query v b) -> Query v b
$cp1Monad :: forall (v :: * -> *). Applicative (Query v)
Monad
           , Monad (Query v)
Monad (Query v)
-> (forall a. IO a -> Query v a) -> MonadIO (Query v)
IO a -> Query v a
forall a. IO a -> Query v a
forall (v :: * -> *). Monad (Query v)
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
forall (v :: * -> *) a. IO a -> Query v a
liftIO :: IO a -> Query v a
$cliftIO :: forall (v :: * -> *) a. IO a -> Query v a
$cp1MonadIO :: forall (v :: * -> *). Monad (Query v)
MonadIO
#if MIN_VERSION_base(4,13,0)
           , Monad (Query v)
Monad (Query v)
-> (forall a. String -> Query v a) -> MonadFail (Query v)
String -> Query v a
forall a. String -> Query v a
forall (v :: * -> *). Monad (Query v)
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
forall (v :: * -> *) a. String -> Query v a
fail :: String -> Query v a
$cfail :: forall (v :: * -> *) a. String -> Query v a
$cp1MonadFail :: forall (v :: * -> *). Monad (Query v)
MonadFail      -- required since GHC 8.8
#endif
           )

query :: (VerifiableVar v) => Query v SBool -> VarEnv v -> Verifier v Bool
query :: Query v SBool -> VarEnv v -> Verifier v Bool
query (Query ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) SBool
action) VarEnv v
env = do
  SMTConfig
cfg <- Verifier v SMTConfig
forall r (m :: * -> *). MonadReader r m => m r
ask
  let predicate :: Symbolic SBool
predicate = StateT (QueryState v) Symbolic SBool
-> QueryState v -> Symbolic SBool
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) SBool
-> VarEnv v -> StateT (QueryState v) Symbolic SBool
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) SBool
action VarEnv v
env) QueryState v
forall a. Monoid a => a
mempty
      smtResult :: IO (Either (VerifierError v) Bool)
smtResult =
        (Bool -> Either (VerifierError v) Bool
forall a b. b -> Either a b
Right (Bool -> Either (VerifierError v) Bool)
-> IO Bool -> IO (Either (VerifierError v) Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SMTConfig -> Symbolic SBool -> IO Bool
forall a. Provable a => SMTConfig -> a -> IO Bool
isTheoremWith SMTConfig
cfg Symbolic SBool
predicate) IO (Either (VerifierError v) Bool)
-> [Handler (Either (VerifierError v) Bool)]
-> IO (Either (VerifierError v) Bool)
forall a. IO a -> [Handler a] -> IO a
`catches`
        [ (VerifierError v -> IO (Either (VerifierError v) Bool))
-> Handler (Either (VerifierError v) Bool)
forall a e. Exception e => (e -> IO a) -> Handler a
Handler (\VerifierError v
ex -> Either (VerifierError v) Bool -> IO (Either (VerifierError v) Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (VerifierError v -> Either (VerifierError v) Bool
forall a b. a -> Either a b
Left VerifierError v
ex))
        , (ErrorCall -> IO (Either (VerifierError v) Bool))
-> Handler (Either (VerifierError v) Bool)
forall a e. Exception e => (e -> IO a) -> Handler a
Handler (\(ErrorCallWithLocation String
message String
location) ->
                     Either (VerifierError v) Bool -> IO (Either (VerifierError v) Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (VerifierError v -> Either (VerifierError v) Bool
forall a b. a -> Either a b
Left (String -> String -> VerifierError v
forall (v :: * -> *). String -> String -> VerifierError v
VESbvException String
message String
location)))
        ]

  IO (Either (VerifierError v) Bool)
-> Verifier v (Either (VerifierError v) Bool)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (Either (VerifierError v) Bool)
smtResult Verifier v (Either (VerifierError v) Bool)
-> (Either (VerifierError v) Bool -> Verifier v Bool)
-> Verifier v Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (VerifierError v -> Verifier v Bool)
-> (Bool -> Verifier v Bool)
-> Either (VerifierError v) Bool
-> Verifier v Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either VerifierError v -> Verifier v Bool
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Bool -> Verifier v Bool
forall (m :: * -> *) a. Monad m => a -> m a
return

--------------------------------------------------------------------------------
--  Query actions
--------------------------------------------------------------------------------

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 :: (forall a. Query v a -> m a)
-> (forall a. VarSym v a -> m (k a)) -> Prop (expr v) b -> m (k b)
evalProp forall a. Query v a -> m a
liftQuery forall a. VarSym v a -> m (k a)
liftVar = (forall b. expr v b -> m (k b)) -> Prop (expr v) b -> m (k b)
forall u (k :: u -> *) (h :: (u -> *) -> u -> *) (f :: * -> *)
       (t :: u -> *) (a :: u).
(HFoldableAt k h, HTraversable h, Applicative f) =>
(forall (b :: u). t b -> f (k b)) -> h t a -> f (k a)
hfoldTraverse ((forall b. v b -> m (k b)) -> expr v b -> m (k b)
forall u (k :: u -> *) (h :: (u -> *) -> u -> *) (f :: * -> *)
       (t :: u -> *) (a :: u).
(HFoldableAt k h, HTraversable h, Applicative f) =>
(forall (b :: u). t b -> f (k b)) -> h t a -> f (k a)
hfoldTraverse (VarSym v b -> m (k b)
forall a. VarSym v a -> m (k a)
liftVar (VarSym v b -> m (k b))
-> (v b -> m (VarSym v b)) -> v b -> m (k b)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Query v (VarSym v b) -> m (VarSym v b)
forall a. Query v a -> m a
liftQuery (Query v (VarSym v b) -> m (VarSym v b))
-> (v b -> Query v (VarSym v b)) -> v b -> m (VarSym v b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v b -> Query v (VarSym v b)
forall (v :: * -> *) a.
(VerifiableVar v, Exception (VerifierError v)) =>
v a -> Query v (VarSym v a)
symbolVar))

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)
evalProp' :: (forall a. Query v a -> m a)
-> (forall a. VarSym v a -> m (k a)) -> Prop (expr v) b -> m (k b)
evalProp' forall a. Query v a -> m a
liftQuery forall a. VarSym v a -> m (k a)
liftVar = (forall b. expr v b -> m (k b)) -> Prop (expr v) b -> m (k b)
forall k1 (f :: * -> *) (k2 :: k1 -> *) (h :: (k1 -> *) -> k1 -> *)
       (t :: k1 -> *) (a :: k1).
(HFoldableAt (Compose f k2) h, Applicative f) =>
(forall (b :: k1). t b -> f (k2 b)) -> h t a -> f (k2 a)
hfoldMapA ((forall b. v b -> m (k b)) -> expr v b -> m (k b)
forall k1 (f :: * -> *) (k2 :: k1 -> *) (h :: (k1 -> *) -> k1 -> *)
       (t :: k1 -> *) (a :: k1).
(HFoldableAt (Compose f k2) h, Applicative f) =>
(forall (b :: k1). t b -> f (k2 b)) -> h t a -> f (k2 a)
hfoldMapA (VarSym v b -> m (k b)
forall a. VarSym v a -> m (k a)
liftVar (VarSym v b -> m (k b))
-> (v b -> m (VarSym v b)) -> v b -> m (k b)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Query v (VarSym v b) -> m (VarSym v b)
forall a. Query v a -> m a
liftQuery (Query v (VarSym v b) -> m (VarSym v b))
-> (v b -> Query v (VarSym v b)) -> v b -> m (VarSym v b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v b -> Query v (VarSym v b)
forall (v :: * -> *) a.
(VerifiableVar v, Exception (VerifierError v)) =>
v a -> Query v (VarSym v a)
symbolVar))

evalPropSimple
  :: ( HMonad expr
     , HTraversable expr
     , VerifiableVar v
     , Exception (VerifierError v)
     , HFoldableAt SBV expr
     , VarSym v ~ SBV
     )
  => Prop (expr v) b
  -> Query v (SBV b)
evalPropSimple :: Prop (expr v) b -> Query v (SBV b)
evalPropSimple = (forall a. Query v a -> Query v a)
-> (forall a. VarSym v a -> Query v (SBV a))
-> Prop (expr v) b
-> Query v (SBV b)
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) (k :: * -> *)
       (m :: * -> *) b.
(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 forall a. a -> a
forall a. Query v a -> Query v a
id forall a. VarSym v a -> Query v (SBV a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure

--------------------------------------------------------------------------------
--  Combinators
--------------------------------------------------------------------------------

-- | 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.
subVar
  :: (HPointed expr, VerifiableVar v, Eq (VarKey v))
  => expr v a
  -> v a
  -> v b
  -> expr v b
subVar :: expr v a -> v a -> v b -> expr v b
subVar expr v a
newExpr v a
targetVar v b
thisVar =
  let targetName :: VarKey v
targetName = v a -> VarKey v
forall (v :: * -> *) a. VerifiableVar v => v a -> VarKey v
varKey v a
targetVar
      thisName :: VarKey v
thisName = v b -> VarKey v
forall (v :: * -> *) a. VerifiableVar v => v a -> VarKey v
varKey v b
thisVar
  in case v b -> v a -> Maybe (b :~: a)
forall (v :: * -> *) a b.
VerifiableVar v =>
v a -> v b -> Maybe (a :~: b)
eqVarTypes v b
thisVar v a
targetVar of
       Just b :~: a
Refl | VarKey v
thisName VarKey v -> VarKey v -> Bool
forall a. Eq a => a -> a -> Bool
== VarKey v
targetName -> expr v a
expr v b
newExpr
       Maybe (b :~: a)
_         -> v b -> expr v b
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure v b
thisVar

--------------------------------------------------------------------------------
--  Internal Functions
--------------------------------------------------------------------------------

liftSymbolic :: Symbolic a -> Query v a
liftSymbolic :: Symbolic a -> Query v a
liftSymbolic = ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) a -> Query v a
forall (v :: * -> *) a.
ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) a -> Query v a
Query (ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) a
 -> Query v a)
-> (Symbolic a
    -> ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) a)
-> Symbolic a
-> Query v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT (QueryState v) Symbolic a
-> ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT (QueryState v) Symbolic a
 -> ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) a)
-> (Symbolic a -> StateT (QueryState v) Symbolic a)
-> Symbolic a
-> ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbolic a -> StateT (QueryState v) Symbolic a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

throwQuery :: (Exception (VerifierError v)) => VerifierError v -> Query v a
throwQuery :: VerifierError v -> Query v a
throwQuery = IO a -> Query v a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> Query v a)
-> (VerifierError v -> IO a) -> VerifierError v -> Query v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerifierError v -> IO a
forall e a. Exception e => e -> IO a
throwIO

symbolVar :: (VerifiableVar v, Exception (VerifierError v)) => v a -> Query v (VarSym v a)
symbolVar :: v a -> Query v (VarSym v a)
symbolVar v a
theVar = do
  let varLoc :: VarKey v
varLoc = v a -> VarKey v
forall (v :: * -> *) a. VerifiableVar v => v a -> VarKey v
varKey v a
theVar
  Maybe (SomeSym v)
storedSymbol <- ReaderT
  (VarEnv v) (StateT (QueryState v) Symbolic) (Maybe (SomeSym v))
-> Query v (Maybe (SomeSym v))
forall (v :: * -> *) a.
ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) a -> Query v a
Query (ReaderT
   (VarEnv v) (StateT (QueryState v) Symbolic) (Maybe (SomeSym v))
 -> Query v (Maybe (SomeSym v)))
-> ReaderT
     (VarEnv v) (StateT (QueryState v) Symbolic) (Maybe (SomeSym v))
-> Query v (Maybe (SomeSym v))
forall a b. (a -> b) -> a -> b
$ Getting (Maybe (SomeSym v)) (QueryState v) (Maybe (SomeSym v))
-> ReaderT
     (VarEnv v) (StateT (QueryState v) Symbolic) (Maybe (SomeSym v))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use (Index (QueryState v)
-> Lens' (QueryState v) (Maybe (IxValue (QueryState v)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (QueryState v)
VarKey v
varLoc)

  case Maybe (SomeSym v)
storedSymbol of
    Just (SomeSym VarSym v a
x) -> case v a -> VarSym v a -> Maybe (VarSym v a)
forall (v :: * -> *) a b.
VerifiableVar v =>
v a -> VarSym v b -> Maybe (VarSym v a)
castVarSym v a
theVar VarSym v a
x of
      Just VarSym v a
y  -> VarSym v a -> Query v (VarSym v a)
forall (m :: * -> *) a. Monad m => a -> m a
return VarSym v a
y
      Maybe (VarSym v a)
Nothing -> VerifierError v -> Query v (VarSym v a)
forall (v :: * -> *) a.
Exception (VerifierError v) =>
VerifierError v -> Query v a
throwQuery (VarKey v -> VerifierError v
forall (v :: * -> *). VarKey v -> VerifierError v
VEMismatchedSymbolType VarKey v
varLoc)
    Maybe (SomeSym v)
Nothing -> do
      VarSym v a
newSymbol <- Symbolic (VarSym v a) -> Query v (VarSym v a)
forall a (v :: * -> *). Symbolic a -> Query v a
liftSymbolic (Symbolic (VarSym v a) -> Query v (VarSym v a))
-> (VarEnv v -> Symbolic (VarSym v a))
-> VarEnv v
-> Query v (VarSym v a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v a -> VarEnv v -> Symbolic (VarSym v a)
forall (v :: * -> *) a.
VerifiableVar v =>
v a -> VarEnv v -> Symbolic (VarSym v a)
symForVar v a
theVar (VarEnv v -> Query v (VarSym v a))
-> Query v (VarEnv v) -> Query v (VarSym v a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) (VarEnv v)
-> Query v (VarEnv v)
forall (v :: * -> *) a.
ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) a -> Query v a
Query ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) (VarEnv v)
forall r (m :: * -> *). MonadReader r m => m r
ask
      ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) ()
-> Query v ()
forall (v :: * -> *) a.
ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) a -> Query v a
Query (ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) ()
 -> Query v ())
-> ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) ()
-> Query v ()
forall a b. (a -> b) -> a -> b
$ Index (QueryState v)
-> Lens' (QueryState v) (Maybe (IxValue (QueryState v)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (QueryState v)
VarKey v
varLoc ((Maybe (SomeSym v) -> Identity (Maybe (SomeSym v)))
 -> QueryState v -> Identity (QueryState v))
-> Maybe (SomeSym v)
-> ReaderT (VarEnv v) (StateT (QueryState v) Symbolic) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= SomeSym v -> Maybe (SomeSym v)
forall a. a -> Maybe a
Just (VarSym v a -> SomeSym v
forall (v :: * -> *) a. VarSym v a -> SomeSym v
SomeSym VarSym v a
newSymbol)
      VarSym v a -> Query v (VarSym v a)
forall (m :: * -> *) a. Monad m => a -> m a
return VarSym v a
newSymbol