{-# LANGUAGE CPP #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Core.Data
( SBool, SWord8, SWord16, SWord32, SWord64
, SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble, SChar, SString, SList
, SEither, SMaybe
, STuple, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7, STuple8
, RCSet(..), SSet
, nan, infinity, sNaN, sInfinity, RoundingMode(..), SRoundingMode
, sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero
, sRNE, sRNA, sRTP, sRTN, sRTZ
, SymVal(..)
, CV(..), CVal(..), AlgReal(..), AlgRealPoly(..), ExtCV(..), GeneralizedCV(..), isRegularCV, cvSameType, cvToBool
, mkConstCV ,liftCV2, mapCV, mapCV2
, SV(..), trueSV, falseSV, trueCV, falseCV, normCV
, SVal(..)
, sTrue, sFalse, sNot, (.&&), (.||), (.<+>), (.~&), (.~|), (.=>), (.<=>), sAnd, sOr, sAny, sAll, fromBool
, SBV(..), NodeId(..), mkSymSBV
, ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), SArray(..)
, sbvToSV, sbvToSymSV, forceSVArg
, SBVExpr(..), newExpr
, cache, Cached, uncache, uncacheAI, HasKind(..)
, Op(..), PBOp(..), FPOp(..), StrOp(..), SeqOp(..), RegExp(..), NamedSymVar, getTableIndex
, SBVPgm(..), Symbolic, runSymbolic, State, getPathCondition, extendPathCondition
, inSMTMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..)
, SolverContext(..), internalVariable, internalConstraint, isCodeGenMode
, SBVType(..), newUninterpreted, addAxiom
, Quantifier(..), needsExistentials
, SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension, smtLibReservedNames
, SolverCapabilities(..)
, extractSymbolicSimulationState
, SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..)
, OptimizeStyle(..), Penalty(..), Objective(..)
, QueryState(..), QueryT(..), SMTProblem(..)
) where
import GHC.Generics (Generic)
import GHC.Exts (IsList(..))
import Control.DeepSeq (NFData(..))
import Control.Monad.Trans (liftIO)
import Data.Int (Int8, Int16, Int32, Int64)
import Data.Word (Word8, Word16, Word32, Word64)
import Data.List (elemIndex)
import Data.Maybe (fromMaybe)
import Data.Proxy
import Data.Typeable (Typeable)
import qualified Data.Generics as G (Data(..))
import System.Random
import Data.SBV.Core.AlgReals
import Data.SBV.Core.Kind
import Data.SBV.Core.Concrete
import Data.SBV.Core.Symbolic
import Data.SBV.Core.Operations
import Data.SBV.Control.Types
import Data.SBV.SMT.SMTLibNames
import Data.SBV.Utils.Lib
getPathCondition :: State -> SBool
getPathCondition :: State -> SBool
getPathCondition st :: State
st = SVal -> SBool
forall a. SVal -> SBV a
SBV (State -> SVal
getSValPathCondition State
st)
extendPathCondition :: State -> (SBool -> SBool) -> State
extendPathCondition :: State -> (SBool -> SBool) -> State
extendPathCondition st :: State
st f :: SBool -> SBool
f = State -> (SVal -> SVal) -> State
extendSValPathCondition State
st (SBool -> SVal
forall a. SBV a -> SVal
unSBV (SBool -> SVal) -> (SVal -> SBool) -> SVal -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBool -> SBool
f (SBool -> SBool) -> (SVal -> SBool) -> SVal -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> SBool
forall a. SVal -> SBV a
SBV)
newtype SBV a = SBV { SBV a -> SVal
unSBV :: SVal }
deriving ((forall x. SBV a -> Rep (SBV a) x)
-> (forall x. Rep (SBV a) x -> SBV a) -> Generic (SBV a)
forall x. Rep (SBV a) x -> SBV a
forall x. SBV a -> Rep (SBV a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SBV a) x -> SBV a
forall a x. SBV a -> Rep (SBV a) x
$cto :: forall a x. Rep (SBV a) x -> SBV a
$cfrom :: forall a x. SBV a -> Rep (SBV a) x
Generic, SBV a -> ()
(SBV a -> ()) -> NFData (SBV a)
forall a. SBV a -> ()
forall a. (a -> ()) -> NFData a
rnf :: SBV a -> ()
$crnf :: forall a. SBV a -> ()
NFData)
type SBool = SBV Bool
type SWord8 = SBV Word8
type SWord16 = SBV Word16
type SWord32 = SBV Word32
type SWord64 = SBV Word64
type SInt8 = SBV Int8
type SInt16 = SBV Int16
type SInt32 = SBV Int32
type SInt64 = SBV Int64
type SInteger = SBV Integer
type SReal = SBV AlgReal
type SFloat = SBV Float
type SDouble = SBV Double
type SChar = SBV Char
type SString = SBV String
type SList a = SBV [a]
type SEither a b = SBV (Either a b)
type SMaybe a = SBV (Maybe a)
type SSet a = SBV (RCSet a)
type STuple a b = SBV (a, b)
type STuple2 a b = SBV (a, b)
type STuple3 a b c = SBV (a, b, c)
type STuple4 a b c d = SBV (a, b, c, d)
type STuple5 a b c d e = SBV (a, b, c, d, e)
type STuple6 a b c d e f = SBV (a, b, c, d, e, f)
type STuple7 a b c d e f g = SBV (a, b, c, d, e, f, g)
type STuple8 a b c d e f g h = SBV (a, b, c, d, e, f, g, h)
instance SymVal [a] => IsList (SList a) where
type Item (SList a) = a
fromList :: [Item (SList a)] -> SList a
fromList = [Item (SList a)] -> SList a
forall a. SymVal a => a -> SBV a
literal
toList :: SList a -> [Item (SList a)]
toList x :: SList a
x = [a] -> Maybe [a] -> [a]
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> [a]
forall a. HasCallStack => [Char] -> a
error "IsList.toList used in a symbolic context!") (SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
x)
nan :: Floating a => a
nan :: a
nan = 0a -> a -> a
forall a. Fractional a => a -> a -> a
/0
infinity :: Floating a => a
infinity :: a
infinity = 1a -> a -> a
forall a. Fractional a => a -> a -> a
/0
sNaN :: (Floating a, SymVal a) => SBV a
sNaN :: SBV a
sNaN = a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
forall a. Floating a => a
nan
sInfinity :: (Floating a, SymVal a) => SBV a
sInfinity :: SBV a
sInfinity = a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
forall a. Floating a => a
infinity
newtype SMTProblem = SMTProblem {SMTProblem -> SMTConfig -> SMTLibPgm
smtLibPgm :: SMTConfig -> SMTLibPgm}
sTrue :: SBool
sTrue :: SBool
sTrue = SVal -> SBool
forall a. SVal -> SBV a
SBV (Bool -> SVal
svBool Bool
True)
sFalse :: SBool
sFalse :: SBool
sFalse = SVal -> SBool
forall a. SVal -> SBV a
SBV (Bool -> SVal
svBool Bool
False)
sNot :: SBool -> SBool
sNot :: SBool -> SBool
sNot (SBV b :: SVal
b) = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SVal
svNot SVal
b)
infixr 3 .&&
(.&&) :: SBool -> SBool -> SBool
SBV x :: SVal
x .&& :: SBool -> SBool -> SBool
.&& SBV y :: SVal
y = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal
x SVal -> SVal -> SVal
`svAnd` SVal
y)
infixr 2 .||
(.||) :: SBool -> SBool -> SBool
SBV x :: SVal
x .|| :: SBool -> SBool -> SBool
.|| SBV y :: SVal
y = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal
x SVal -> SVal -> SVal
`svOr` SVal
y)
infixl 6 .<+>
(.<+>) :: SBool -> SBool -> SBool
SBV x :: SVal
x .<+> :: SBool -> SBool -> SBool
.<+> SBV y :: SVal
y = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal
x SVal -> SVal -> SVal
`svXOr` SVal
y)
infixr 3 .~&
(.~&) :: SBool -> SBool -> SBool
x :: SBool
x .~& :: SBool -> SBool -> SBool
.~& y :: SBool
y = SBool -> SBool
sNot (SBool
x SBool -> SBool -> SBool
.&& SBool
y)
infixr 2 .~|
(.~|) :: SBool -> SBool -> SBool
x :: SBool
x .~| :: SBool -> SBool -> SBool
.~| y :: SBool
y = SBool -> SBool
sNot (SBool
x SBool -> SBool -> SBool
.|| SBool
y)
infixr 1 .=>
(.=>) :: SBool -> SBool -> SBool
x :: SBool
x .=> :: SBool -> SBool -> SBool
.=> y :: SBool
y = SBool -> SBool
sNot SBool
x SBool -> SBool -> SBool
.|| SBool
y
infixr 1 .<=>
(.<=>) :: SBool -> SBool -> SBool
x :: SBool
x .<=> :: SBool -> SBool -> SBool
.<=> y :: SBool
y = (SBool
x SBool -> SBool -> SBool
.&& SBool
y) SBool -> SBool -> SBool
.|| (SBool -> SBool
sNot SBool
x SBool -> SBool -> SBool
.&& SBool -> SBool
sNot SBool
y)
fromBool :: Bool -> SBool
fromBool :: Bool -> SBool
fromBool True = SBool
sTrue
fromBool False = SBool
sFalse
sAnd :: [SBool] -> SBool
sAnd :: [SBool] -> SBool
sAnd = (SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SBool -> SBool -> SBool
(.&&) SBool
sTrue
sOr :: [SBool] -> SBool
sOr :: [SBool] -> SBool
sOr = (SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SBool -> SBool -> SBool
(.||) SBool
sFalse
sAny :: (a -> SBool) -> [a] -> SBool
sAny :: (a -> SBool) -> [a] -> SBool
sAny f :: a -> SBool
f = [SBool] -> SBool
sOr ([SBool] -> SBool) -> ([a] -> [SBool]) -> [a] -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> SBool) -> [a] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map a -> SBool
f
sAll :: (a -> SBool) -> [a] -> SBool
sAll :: (a -> SBool) -> [a] -> SBool
sAll f :: a -> SBool
f = [SBool] -> SBool
sAnd ([SBool] -> SBool) -> ([a] -> [SBool]) -> [a] -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> SBool) -> [a] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map a -> SBool
f
instance SymVal RoundingMode
type SRoundingMode = SBV RoundingMode
sRoundNearestTiesToEven :: SRoundingMode
sRoundNearestTiesToEven :: SBV RoundingMode
sRoundNearestTiesToEven = RoundingMode -> SBV RoundingMode
forall a. SymVal a => a -> SBV a
literal RoundingMode
RoundNearestTiesToEven
sRoundNearestTiesToAway :: SRoundingMode
sRoundNearestTiesToAway :: SBV RoundingMode
sRoundNearestTiesToAway = RoundingMode -> SBV RoundingMode
forall a. SymVal a => a -> SBV a
literal RoundingMode
RoundNearestTiesToAway
sRoundTowardPositive :: SRoundingMode
sRoundTowardPositive :: SBV RoundingMode
sRoundTowardPositive = RoundingMode -> SBV RoundingMode
forall a. SymVal a => a -> SBV a
literal RoundingMode
RoundTowardPositive
sRoundTowardNegative :: SRoundingMode
sRoundTowardNegative :: SBV RoundingMode
sRoundTowardNegative = RoundingMode -> SBV RoundingMode
forall a. SymVal a => a -> SBV a
literal RoundingMode
RoundTowardNegative
sRoundTowardZero :: SRoundingMode
sRoundTowardZero :: SBV RoundingMode
sRoundTowardZero = RoundingMode -> SBV RoundingMode
forall a. SymVal a => a -> SBV a
literal RoundingMode
RoundTowardZero
sRNE :: SRoundingMode
sRNE :: SBV RoundingMode
sRNE = SBV RoundingMode
sRoundNearestTiesToEven
sRNA :: SRoundingMode
sRNA :: SBV RoundingMode
sRNA = SBV RoundingMode
sRoundNearestTiesToAway
sRTP :: SRoundingMode
sRTP :: SBV RoundingMode
sRTP = SBV RoundingMode
sRoundTowardPositive
sRTN :: SRoundingMode
sRTN :: SBV RoundingMode
sRTN = SBV RoundingMode
sRoundTowardNegative
sRTZ :: SRoundingMode
sRTZ :: SBV RoundingMode
sRTZ = SBV RoundingMode
sRoundTowardZero
instance Show (SBV a) where
show :: SBV a -> [Char]
show (SBV sv :: SVal
sv) = SVal -> [Char]
forall a. Show a => a -> [Char]
show SVal
sv
instance Eq (SBV a) where
SBV a :: SVal
a == :: SBV a -> SBV a -> Bool
== SBV b :: SVal
b = SVal
a SVal -> SVal -> Bool
forall a. Eq a => a -> a -> Bool
== SVal
b
SBV a :: SVal
a /= :: SBV a -> SBV a -> Bool
/= SBV b :: SVal
b = SVal
a SVal -> SVal -> Bool
forall a. Eq a => a -> a -> Bool
/= SVal
b
instance HasKind a => HasKind (SBV a) where
kindOf :: SBV a -> Kind
kindOf _ = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
sbvToSV :: State -> SBV a -> IO SV
sbvToSV :: State -> SBV a -> IO SV
sbvToSV st :: State
st (SBV s :: SVal
s) = State -> SVal -> IO SV
svToSV State
st SVal
s
mkSymSBV :: forall a m. MonadSymbolic m => Maybe Quantifier -> Kind -> Maybe String -> m (SBV a)
mkSymSBV :: Maybe Quantifier -> Kind -> Maybe [Char] -> m (SBV a)
mkSymSBV mbQ :: Maybe Quantifier
mbQ k :: Kind
k mbNm :: Maybe [Char]
mbNm = SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> m SVal -> m (SBV a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv m State -> (State -> m SVal) -> m SVal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SVal -> m SVal
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe [Char] -> State -> IO SVal
svMkSymVar Maybe Quantifier
mbQ Kind
k Maybe [Char]
mbNm)
sbvToSymSV :: MonadSymbolic m => SBV a -> m SV
sbvToSymSV :: SBV a -> m SV
sbvToSymSV sbv :: SBV a
sbv = do
State
st <- m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
IO SV -> m SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sbv
class SolverContext m where
constrain :: SBool -> m ()
softConstrain :: SBool -> m ()
namedConstraint :: String -> SBool -> m ()
constrainWithAttribute :: [(String, String)] -> SBool -> m ()
setInfo :: String -> [String] -> m ()
setOption :: SMTOption -> m ()
setLogic :: Logic -> m ()
setTimeOut :: Integer -> m ()
contextState :: m State
{-# MINIMAL constrain, softConstrain, namedConstraint, constrainWithAttribute, setOption, contextState #-}
setTimeOut t :: Integer
t = SMTOption -> m ()
forall (m :: * -> *). SolverContext m => SMTOption -> m ()
setOption (SMTOption -> m ()) -> SMTOption -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> SMTOption
OptionKeyword ":timeout" [Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
t]
setLogic = SMTOption -> m ()
forall (m :: * -> *). SolverContext m => SMTOption -> m ()
setOption (SMTOption -> m ()) -> (Logic -> SMTOption) -> Logic -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Logic -> SMTOption
SetLogic
setInfo k :: [Char]
k = SMTOption -> m ()
forall (m :: * -> *). SolverContext m => SMTOption -> m ()
setOption (SMTOption -> m ()) -> ([[Char]] -> SMTOption) -> [[Char]] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]] -> SMTOption
SetInfo [Char]
k
class Outputtable a where
output :: MonadSymbolic m => a -> m a
instance Outputtable (SBV a) where
output :: SBV a -> m (SBV a)
output i :: SBV a
i = do
SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
outputSVal (SBV a -> SVal
forall a. SBV a -> SVal
unSBV SBV a
i)
SBV a -> m (SBV a)
forall (m :: * -> *) a. Monad m => a -> m a
return SBV a
i
instance Outputtable a => Outputtable [a] where
output :: [a] -> m [a]
output = (a -> m a) -> [a] -> m [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output
instance Outputtable () where
output :: () -> m ()
output = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return
instance (Outputtable a, Outputtable b) => Outputtable (a, b) where
output :: (a, b) -> m (a, b)
output = (a -> b -> (a, b))
-> (a -> m a) -> (b -> m b) -> (a, b) -> m (a, b)
forall (m :: * -> *) a' b' r a b.
Monad m =>
(a' -> b' -> r) -> (a -> m a') -> (b -> m b') -> (a, b) -> m r
mlift2 (,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output
instance (Outputtable a, Outputtable b, Outputtable c) => Outputtable (a, b, c) where
output :: (a, b, c) -> m (a, b, c)
output = (a -> b -> c -> (a, b, c))
-> (a -> m a)
-> (b -> m b)
-> (c -> m c)
-> (a, b, c)
-> m (a, b, c)
forall (m :: * -> *) a' b' c' r a b c.
Monad m =>
(a' -> b' -> c' -> r)
-> (a -> m a') -> (b -> m b') -> (c -> m c') -> (a, b, c) -> m r
mlift3 (,,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output c -> m c
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output
instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d) => Outputtable (a, b, c, d) where
output :: (a, b, c, d) -> m (a, b, c, d)
output = (a -> b -> c -> d -> (a, b, c, d))
-> (a -> m a)
-> (b -> m b)
-> (c -> m c)
-> (d -> m d)
-> (a, b, c, d)
-> m (a, b, c, d)
forall (m :: * -> *) a' b' c' d' r a b c d.
Monad m =>
(a' -> b' -> c' -> d' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (a, b, c, d)
-> m r
mlift4 (,,,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output c -> m c
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output d -> m d
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output
instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e) => Outputtable (a, b, c, d, e) where
output :: (a, b, c, d, e) -> m (a, b, c, d, e)
output = (a -> b -> c -> d -> e -> (a, b, c, d, e))
-> (a -> m a)
-> (b -> m b)
-> (c -> m c)
-> (d -> m d)
-> (e -> m e)
-> (a, b, c, d, e)
-> m (a, b, c, d, e)
forall (m :: * -> *) a' b' c' d' e' r a b c d e.
Monad m =>
(a' -> b' -> c' -> d' -> e' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (e -> m e')
-> (a, b, c, d, e)
-> m r
mlift5 (,,,,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output c -> m c
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output d -> m d
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output e -> m e
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output
instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f) => Outputtable (a, b, c, d, e, f) where
output :: (a, b, c, d, e, f) -> m (a, b, c, d, e, f)
output = (a -> b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> (a -> m a)
-> (b -> m b)
-> (c -> m c)
-> (d -> m d)
-> (e -> m e)
-> (f -> m f)
-> (a, b, c, d, e, f)
-> m (a, b, c, d, e, f)
forall (m :: * -> *) a' b' c' d' e' f' r a b c d e f.
Monad m =>
(a' -> b' -> c' -> d' -> e' -> f' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (e -> m e')
-> (f -> m f')
-> (a, b, c, d, e, f)
-> m r
mlift6 (,,,,,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output c -> m c
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output d -> m d
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output e -> m e
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output f -> m f
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output
instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g) => Outputtable (a, b, c, d, e, f, g) where
output :: (a, b, c, d, e, f, g) -> m (a, b, c, d, e, f, g)
output = (a -> b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> (a -> m a)
-> (b -> m b)
-> (c -> m c)
-> (d -> m d)
-> (e -> m e)
-> (f -> m f)
-> (g -> m g)
-> (a, b, c, d, e, f, g)
-> m (a, b, c, d, e, f, g)
forall (m :: * -> *) a' b' c' d' e' f' g' r a b c d e f g.
Monad m =>
(a' -> b' -> c' -> d' -> e' -> f' -> g' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (e -> m e')
-> (f -> m f')
-> (g -> m g')
-> (a, b, c, d, e, f, g)
-> m r
mlift7 (,,,,,,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output c -> m c
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output d -> m d
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output e -> m e
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output f -> m f
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output g -> m g
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output
instance (Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g, Outputtable h) => Outputtable (a, b, c, d, e, f, g, h) where
output :: (a, b, c, d, e, f, g, h) -> m (a, b, c, d, e, f, g, h)
output = (a -> b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> (a -> m a)
-> (b -> m b)
-> (c -> m c)
-> (d -> m d)
-> (e -> m e)
-> (f -> m f)
-> (g -> m g)
-> (h -> m h)
-> (a, b, c, d, e, f, g, h)
-> m (a, b, c, d, e, f, g, h)
forall (m :: * -> *) a' b' c' d' e' f' g' h' r a b c d e f g h.
Monad m =>
(a' -> b' -> c' -> d' -> e' -> f' -> g' -> h' -> r)
-> (a -> m a')
-> (b -> m b')
-> (c -> m c')
-> (d -> m d')
-> (e -> m e')
-> (f -> m f')
-> (g -> m g')
-> (h -> m h')
-> (a, b, c, d, e, f, g, h)
-> m r
mlift8 (,,,,,,,) a -> m a
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output b -> m b
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output c -> m c
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output d -> m d
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output e -> m e
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output f -> m f
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output g -> m g
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output h -> m h
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output
class (HasKind a, Typeable a) => SymVal a where
mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV a)
literal :: a -> SBV a
fromCV :: CV -> a
isConcretely :: SBV a -> (a -> Bool) -> Bool
default mkSymVal :: (MonadSymbolic m, Read a, G.Data a) => Maybe Quantifier -> Maybe String -> m (SBV a)
mkSymVal mbQ :: Maybe Quantifier
mbQ mbNm :: Maybe [Char]
mbNm = SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> m SVal -> m (SBV a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv m State -> (State -> m SVal) -> m SVal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SVal -> m SVal
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe [Char] -> State -> IO SVal
svMkSymVar Maybe Quantifier
mbQ Kind
k Maybe [Char]
mbNm)
where
k :: Kind
k = a -> Kind
forall a. (Read a, Data a) => a -> Kind
constructUKind (a
forall a. HasCallStack => a
undefined :: a)
default literal :: Show a => a -> SBV a
literal x :: a
x = let k :: Kind
k@(KUninterpreted _ conts :: Either [Char] [[Char]]
conts) = a -> Kind
forall a. HasKind a => a -> Kind
kindOf a
x
sx :: [Char]
sx = a -> [Char]
forall a. Show a => a -> [Char]
show a
x
mbIdx :: Maybe Int
mbIdx = case Either [Char] [[Char]]
conts of
Right xs :: [[Char]]
xs -> [Char]
sx [Char] -> [[Char]] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
`elemIndex` [[Char]]
xs
_ -> Maybe Int
forall a. Maybe a
Nothing
in SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (Kind -> CVal -> CV
CV Kind
k ((Maybe Int, [Char]) -> CVal
CUserSort (Maybe Int
mbIdx, [Char]
sx))))
default fromCV :: Read a => CV -> a
fromCV (CV _ (CUserSort (_, s :: [Char]
s))) = [Char] -> a
forall a. Read a => [Char] -> a
read [Char]
s
fromCV cv :: CV
cv = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ "Cannot convert CV " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ CV -> [Char]
forall a. Show a => a -> [Char]
show CV
cv [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ " to kind " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> [Char]
forall a. Show a => a -> [Char]
show (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a))
isConcretely s :: SBV a
s p :: a -> Bool
p
| Just i :: a
i <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s = a -> Bool
p a
i
| Bool
True = Bool
False
forall :: MonadSymbolic m => String -> m (SBV a)
forall = Maybe Quantifier -> Maybe [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
Maybe Quantifier -> Maybe [Char] -> m (SBV a)
mkSymVal (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
ALL) (Maybe [Char] -> m (SBV a))
-> ([Char] -> Maybe [Char]) -> [Char] -> m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just
forall_ :: MonadSymbolic m => m (SBV a)
forall_ = Maybe Quantifier -> Maybe [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
Maybe Quantifier -> Maybe [Char] -> m (SBV a)
mkSymVal (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
ALL) Maybe [Char]
forall a. Maybe a
Nothing
mkForallVars :: MonadSymbolic m => Int -> m [SBV a]
mkForallVars n :: Int
n = (Int -> m (SBV a)) -> [Int] -> m [SBV a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (m (SBV a) -> Int -> m (SBV a)
forall a b. a -> b -> a
const m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_) [1 .. Int
n]
exists :: MonadSymbolic m => String -> m (SBV a)
exists = Maybe Quantifier -> Maybe [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
Maybe Quantifier -> Maybe [Char] -> m (SBV a)
mkSymVal (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
EX) (Maybe [Char] -> m (SBV a))
-> ([Char] -> Maybe [Char]) -> [Char] -> m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just
exists_ :: MonadSymbolic m => m (SBV a)
exists_ = Maybe Quantifier -> Maybe [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
Maybe Quantifier -> Maybe [Char] -> m (SBV a)
mkSymVal (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
EX) Maybe [Char]
forall a. Maybe a
Nothing
mkExistVars :: MonadSymbolic m => Int -> m [SBV a]
mkExistVars n :: Int
n = (Int -> m (SBV a)) -> [Int] -> m [SBV a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (m (SBV a) -> Int -> m (SBV a)
forall a b. a -> b -> a
const m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_) [1 .. Int
n]
free :: MonadSymbolic m => String -> m (SBV a)
free = Maybe Quantifier -> Maybe [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
Maybe Quantifier -> Maybe [Char] -> m (SBV a)
mkSymVal Maybe Quantifier
forall a. Maybe a
Nothing (Maybe [Char] -> m (SBV a))
-> ([Char] -> Maybe [Char]) -> [Char] -> m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just
free_ :: MonadSymbolic m => m (SBV a)
free_ = Maybe Quantifier -> Maybe [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
Maybe Quantifier -> Maybe [Char] -> m (SBV a)
mkSymVal Maybe Quantifier
forall a. Maybe a
Nothing Maybe [Char]
forall a. Maybe a
Nothing
mkFreeVars :: MonadSymbolic m => Int -> m [SBV a]
mkFreeVars n :: Int
n = (Int -> m (SBV a)) -> [Int] -> m [SBV a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (m (SBV a) -> Int -> m (SBV a)
forall a b. a -> b -> a
const m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_) [1 .. Int
n]
symbolic :: MonadSymbolic m => String -> m (SBV a)
symbolic = [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[Char] -> m (SBV a)
free
symbolics :: MonadSymbolic m => [String] -> m [SBV a]
symbolics = ([Char] -> m (SBV a)) -> [[Char]] -> m [SBV a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [Char] -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[Char] -> m (SBV a)
symbolic
unliteral :: SBV a -> Maybe a
unliteral (SBV (SVal _ (Left c :: CV
c))) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ CV -> a
forall a. SymVal a => CV -> a
fromCV CV
c
unliteral _ = Maybe a
forall a. Maybe a
Nothing
isConcrete :: SBV a -> Bool
isConcrete (SBV (SVal _ (Left _))) = Bool
True
isConcrete _ = Bool
False
isSymbolic :: SBV a -> Bool
isSymbolic = Bool -> Bool
not (Bool -> Bool) -> (SBV a -> Bool) -> SBV a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> Bool
forall a. SymVal a => SBV a -> Bool
isConcrete
instance (Random a, SymVal a) => Random (SBV a) where
randomR :: (SBV a, SBV a) -> g -> (SBV a, g)
randomR (l :: SBV a
l, h :: SBV a
h) g :: g
g = case (SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
l, SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
h) of
(Just lb :: a
lb, Just hb :: a
hb) -> let (v :: a
v, g' :: g
g') = (a, a) -> g -> (a, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (a
lb, a
hb) g
g in (a -> SBV a
forall a. SymVal a => a -> SBV a
literal (a
v :: a), g
g')
_ -> [Char] -> (SBV a, g)
forall a. HasCallStack => [Char] -> a
error "SBV.Random: Cannot generate random values with symbolic bounds"
random :: g -> (SBV a, g)
random g :: g
g = let (v :: a
v, g' :: g
g') = g -> (a, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g in (a -> SBV a
forall a. SymVal a => a -> SBV a
literal (a
v :: a) , g
g')
class SymArray array where
newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b)
newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b)
readArray :: array a b -> SBV a -> SBV b
writeArray :: SymVal b => array a b -> SBV a -> SBV b -> array a b
mergeArrays :: SymVal b => SBV Bool -> array a b -> array a b -> array a b
newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (array a b)
{-# MINIMAL readArray, writeArray, mergeArrays, ((newArray_, newArray) | newArrayInState) #-}
newArray_ mbVal :: Maybe (SBV b)
mbVal = m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv m State -> (State -> m (array a b)) -> m (array a b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO (array a b) -> m (array a b)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (array a b) -> m (array a b))
-> (State -> IO (array a b)) -> State -> m (array a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
newArrayInState Maybe [Char]
forall a. Maybe a
Nothing Maybe (SBV b)
mbVal
newArray nm :: [Char]
nm mbVal :: Maybe (SBV b)
mbVal = m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv m State -> (State -> m (array a b)) -> m (array a b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO (array a b) -> m (array a b)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (array a b) -> m (array a b))
-> (State -> IO (array a b)) -> State -> m (array a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
newArrayInState ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
nm) Maybe (SBV b)
mbVal
newArrayInState = [Char] -> Maybe [Char] -> Maybe (SBV b) -> State -> IO (array a b)
forall a. HasCallStack => [Char] -> a
error "undefined: newArrayInState"
newtype SArray a b = SArray { SArray a b -> SArr
unSArray :: SArr }
instance (HasKind a, HasKind b) => Show (SArray a b) where
show :: SArray a b -> [Char]
show SArray{} = "SArray<" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Proxy a -> [Char]
forall a. HasKind a => a -> [Char]
showType (Proxy a
forall k (t :: k). Proxy t
Proxy @a) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ":" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Proxy b -> [Char]
forall a. HasKind a => a -> [Char]
showType (Proxy b
forall k (t :: k). Proxy t
Proxy @b) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ">"
instance SymArray SArray where
readArray :: SArray a b -> SBV a -> SBV b
readArray (SArray arr :: SArr
arr) (SBV a :: SVal
a) = SVal -> SBV b
forall a. SVal -> SBV a
SBV (SArr -> SVal -> SVal
readSArr SArr
arr SVal
a)
writeArray :: SArray a b -> SBV a -> SBV b -> SArray a b
writeArray (SArray arr :: SArr
arr) (SBV a :: SVal
a) (SBV b :: SVal
b) = SArr -> SArray a b
forall a b. SArr -> SArray a b
SArray (SArr -> SVal -> SVal -> SArr
writeSArr SArr
arr SVal
a SVal
b)
mergeArrays :: SBool -> SArray a b -> SArray a b -> SArray a b
mergeArrays (SBV t :: SVal
t) (SArray a :: SArr
a) (SArray b :: SArr
b) = SArr -> SArray a b
forall a b. SArr -> SArray a b
SArray (SVal -> SArr -> SArr -> SArr
mergeSArr SVal
t SArr
a SArr
b)
newArrayInState :: forall a b. (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SArray a b)
newArrayInState :: Maybe [Char] -> Maybe (SBV b) -> State -> IO (SArray a b)
newArrayInState mbNm :: Maybe [Char]
mbNm mbVal :: Maybe (SBV b)
mbVal st :: State
st = do (Kind -> IO ()) -> [Kind] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (State -> Kind -> IO ()
registerKind State
st) [Kind
aknd, Kind
bknd]
SArr -> SArray a b
forall a b. SArr -> SArray a b
SArray (SArr -> SArray a b) -> IO SArr -> IO (SArray a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State -> (Kind, Kind) -> (Int -> [Char]) -> Maybe SVal -> IO SArr
newSArr State
st (Kind
aknd, Kind
bknd) (Maybe [Char] -> Int -> [Char]
forall a. Show a => Maybe [Char] -> a -> [Char]
mkNm Maybe [Char]
mbNm) (SBV b -> SVal
forall a. SBV a -> SVal
unSBV (SBV b -> SVal) -> Maybe (SBV b) -> Maybe SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (SBV b)
mbVal)
where mkNm :: Maybe [Char] -> a -> [Char]
mkNm Nothing t :: a
t = "array_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
t
mkNm (Just nm :: [Char]
nm) _ = [Char]
nm
aknd :: Kind
aknd = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
bknd :: Kind
bknd = Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)
newtype SFunArray a b = SFunArray { SFunArray a b -> SFunArr
unSFunArray :: SFunArr }
instance (HasKind a, HasKind b) => Show (SFunArray a b) where
show :: SFunArray a b -> [Char]
show SFunArray{} = "SFunArray<" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Proxy a -> [Char]
forall a. HasKind a => a -> [Char]
showType (Proxy a
forall k (t :: k). Proxy t
Proxy @a) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ":" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Proxy b -> [Char]
forall a. HasKind a => a -> [Char]
showType (Proxy b
forall k (t :: k). Proxy t
Proxy @b) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ">"
instance SymArray SFunArray where
readArray :: SFunArray a b -> SBV a -> SBV b
readArray (SFunArray arr :: SFunArr
arr) (SBV a :: SVal
a) = SVal -> SBV b
forall a. SVal -> SBV a
SBV (SFunArr -> SVal -> SVal
readSFunArr SFunArr
arr SVal
a)
writeArray :: SFunArray a b -> SBV a -> SBV b -> SFunArray a b
writeArray (SFunArray arr :: SFunArr
arr) (SBV a :: SVal
a) (SBV b :: SVal
b) = SFunArr -> SFunArray a b
forall a b. SFunArr -> SFunArray a b
SFunArray (SFunArr -> SVal -> SVal -> SFunArr
writeSFunArr SFunArr
arr SVal
a SVal
b)
mergeArrays :: SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b
mergeArrays (SBV t :: SVal
t) (SFunArray a :: SFunArr
a) (SFunArray b :: SFunArr
b) = SFunArr -> SFunArray a b
forall a b. SFunArr -> SFunArray a b
SFunArray (SVal -> SFunArr -> SFunArr -> SFunArr
mergeSFunArr SVal
t SFunArr
a SFunArr
b)
newArrayInState :: forall a b. (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SFunArray a b)
newArrayInState :: Maybe [Char] -> Maybe (SBV b) -> State -> IO (SFunArray a b)
newArrayInState mbNm :: Maybe [Char]
mbNm mbVal :: Maybe (SBV b)
mbVal st :: State
st = do (Kind -> IO ()) -> [Kind] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (State -> Kind -> IO ()
registerKind State
st) [Kind
aknd, Kind
bknd]
SFunArr -> SFunArray a b
forall a b. SFunArr -> SFunArray a b
SFunArray (SFunArr -> SFunArray a b) -> IO SFunArr -> IO (SFunArray a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State
-> (Kind, Kind) -> (Int -> [Char]) -> Maybe SVal -> IO SFunArr
newSFunArr State
st (Kind
aknd, Kind
bknd) (Maybe [Char] -> Int -> [Char]
forall a. Show a => Maybe [Char] -> a -> [Char]
mkNm Maybe [Char]
mbNm) (SBV b -> SVal
forall a. SBV a -> SVal
unSBV (SBV b -> SVal) -> Maybe (SBV b) -> Maybe SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (SBV b)
mbVal)
where mkNm :: Maybe [Char] -> a -> [Char]
mkNm Nothing t :: a
t = "funArray_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
t
mkNm (Just nm :: [Char]
nm) _ = [Char]
nm
aknd :: Kind
aknd = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
bknd :: Kind
bknd = Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)