{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.IR.SymPrim.Data.SymPrim
( SymBool (..),
SymInteger (..),
SymWordN (..),
SymIntN (..),
SomeSymWordN (..),
SomeSymIntN (..),
type (=~>) (..),
type (-~>) (..),
(-->),
ModelSymPair (..),
symSize,
symsSize,
SomeSym (..),
AllSyms (..),
allSymsSize,
unarySomeSymIntN,
unarySomeSymIntNR1,
binSomeSymIntN,
binSomeSymIntNR1,
binSomeSymIntNR2,
unarySomeSymWordN,
unarySomeSymWordNR1,
binSomeSymWordN,
binSomeSymWordNR1,
binSomeSymWordNR2,
)
where
import Control.DeepSeq (NFData (rnf))
import Control.Monad.Except (ExceptT (ExceptT), MonadError (throwError))
import Control.Monad.Identity
( Identity (Identity),
IdentityT (IdentityT),
)
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import Data.Bits
( Bits
( bit,
bitSize,
bitSizeMaybe,
clearBit,
complement,
complementBit,
isSigned,
popCount,
rotate,
rotateL,
rotateR,
setBit,
shift,
shiftL,
shiftR,
testBit,
unsafeShiftL,
unsafeShiftR,
xor,
zeroBits,
(.&.),
(.|.)
),
FiniteBits (finiteBitSize),
)
import qualified Data.ByteString as B
import Data.Functor.Sum (Sum)
import Data.Hashable (Hashable (hashWithSalt))
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Proxy (Proxy (Proxy))
import Data.String (IsString (fromString))
import qualified Data.Text as T
import Data.Typeable (typeRep, type (:~:) (Refl))
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Generics
( Generic (Rep, from),
K1 (K1),
M1 (M1),
U1,
type (:*:) ((:*:)),
type (:+:) (L1, R1),
)
import GHC.TypeNats
( KnownNat,
Nat,
natVal,
sameNat,
type (+),
type (<=),
)
import Generics.Deriving (Default (Default, unDefault))
import Grisette.Core.Control.Exception
( AssertionError,
VerificationConditions,
)
import Grisette.Core.Data.BV
( IntN (IntN),
SomeIntN (SomeIntN),
SomeWordN (SomeWordN),
WordN (WordN),
)
import Grisette.Core.Data.Class.BitVector
( BV (bvConcat, bvExt, bvSelect, bvSext, bvZext),
BVSignConversion (toSigned, toUnsigned),
SizedBV (sizedBVConcat, sizedBVExt, sizedBVSelect, sizedBVSext, sizedBVZext),
)
import Grisette.Core.Data.Class.Bool
( LogicalOp (nots, (&&~), (||~)),
SEq ((/=~), (==~)),
)
import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
import Grisette.Core.Data.Class.ExtractSymbolics
( ExtractSymbolics (extractSymbolics),
)
import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))
import Grisette.Core.Data.Class.GPretty (GPretty (gpretty))
import Grisette.Core.Data.Class.ModelOps
( ModelOps (emptyModel, insertValue),
ModelRep (buildModel),
)
import Grisette.Core.Data.Class.SOrd (SOrd (symCompare, (<=~), (<~), (>=~), (>~)))
import Grisette.Core.Data.Class.SafeArith
( ArithException (DivideByZero, Overflow, Underflow),
SafeDivision
( safeDiv,
safeDiv',
safeDivMod,
safeDivMod',
safeMod,
safeMod',
safeQuot,
safeQuot',
safeQuotRem,
safeQuotRem',
safeRem,
safeRem'
),
SafeLinearArith
( safeAdd,
safeAdd',
safeMinus,
safeMinus',
safeNeg,
safeNeg'
),
SymIntegerOp,
)
import Grisette.Core.Data.Class.SimpleMergeable (mrgIf)
import Grisette.Core.Data.Class.Solvable
( Solvable (con, conView, iinfosym, isym, sinfosym, ssym),
pattern Con,
)
import Grisette.Core.Data.Class.Substitute (SubstituteSym (substituteSym))
import Grisette.Core.Data.Class.ToCon (ToCon (toCon))
import Grisette.Core.Data.Class.ToSym (ToSym (toSym))
import Grisette.IR.SymPrim.Data.IntBitwidth (intBitwidthQ)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
( conTerm,
iinfosymTerm,
isymTerm,
sinfosymTerm,
ssymTerm,
symTerm,
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
( SomeTerm (SomeTerm),
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
( ConRep (ConType),
LinkedRep (underlyingTerm, wrapTerm),
SupportedPrim,
SymRep (SymType),
Term (ConTerm, SymTerm),
TypedSymbol (WithInfo),
prettyPrintTerm,
type (-->) (GeneralFun),
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
( substTerm,
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
( extractSymbolicsTerm,
pformat,
someTermsSize,
termSize,
termsSize,
)
import Grisette.IR.SymPrim.Data.Prim.Model
( Model,
SymbolSet (SymbolSet),
evaluateTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
( pevalBVConcatTerm,
pevalBVExtendTerm,
pevalBVSelectTerm,
pevalBVToSignedTerm,
pevalBVToUnsignedTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
( pevalAndBitsTerm,
pevalComplementBitsTerm,
pevalOrBitsTerm,
pevalRotateBitsTerm,
pevalShiftBitsTerm,
pevalXorBitsTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
( pevalEqvTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
( pevalGeneralFunApplyTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
( pevalDivBoundedIntegralTerm,
pevalDivIntegralTerm,
pevalModBoundedIntegralTerm,
pevalModIntegralTerm,
pevalQuotBoundedIntegralTerm,
pevalQuotIntegralTerm,
pevalRemBoundedIntegralTerm,
pevalRemIntegralTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
( pevalAbsNumTerm,
pevalAddNumTerm,
pevalGeNumTerm,
pevalGtNumTerm,
pevalLeNumTerm,
pevalLtNumTerm,
pevalMinusNumTerm,
pevalSignumNumTerm,
pevalTimesNumTerm,
pevalUMinusNumTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
( pevalTabularFunApplyTerm,
)
import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
import Grisette.Lib.Control.Monad (mrgReturn)
import Grisette.Utils.Parameterized
( KnownProof (KnownProof),
LeqProof (LeqProof),
knownAdd,
leqAddPos,
leqTrans,
unsafeKnownProof,
unsafeLeqProof,
)
import Language.Haskell.TH.Syntax (Lift)
newtype SymBool = SymBool {SymBool -> Term Bool
underlyingBoolTerm :: Term Bool}
deriving (forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymBool -> m Exp
forall (m :: * -> *). Quote m => SymBool -> Code m SymBool
liftTyped :: forall (m :: * -> *). Quote m => SymBool -> Code m SymBool
$cliftTyped :: forall (m :: * -> *). Quote m => SymBool -> Code m SymBool
lift :: forall (m :: * -> *). Quote m => SymBool -> m Exp
$clift :: forall (m :: * -> *). Quote m => SymBool -> m Exp
Lift, SymBool -> ()
forall a. (a -> ()) -> NFData a
rnf :: SymBool -> ()
$crnf :: SymBool -> ()
NFData, forall x. Rep SymBool x -> SymBool
forall x. SymBool -> Rep SymBool x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SymBool x -> SymBool
$cfrom :: forall x. SymBool -> Rep SymBool x
Generic)
newtype SymInteger = SymInteger {SymInteger -> Term Integer
underlyingIntegerTerm :: Term Integer}
deriving (forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymInteger -> m Exp
forall (m :: * -> *). Quote m => SymInteger -> Code m SymInteger
liftTyped :: forall (m :: * -> *). Quote m => SymInteger -> Code m SymInteger
$cliftTyped :: forall (m :: * -> *). Quote m => SymInteger -> Code m SymInteger
lift :: forall (m :: * -> *). Quote m => SymInteger -> m Exp
$clift :: forall (m :: * -> *). Quote m => SymInteger -> m Exp
Lift, SymInteger -> ()
forall a. (a -> ()) -> NFData a
rnf :: SymInteger -> ()
$crnf :: SymInteger -> ()
NFData, forall x. Rep SymInteger x -> SymInteger
forall x. SymInteger -> Rep SymInteger x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SymInteger x -> SymInteger
$cfrom :: forall x. SymInteger -> Rep SymInteger x
Generic)
#define QUOTE() '
#define QID(a) a
#define QRIGHT(a) QID(a)'
#define SAFE_DIVISION_FUNC(name, type, op) \
name (type l) rs@(type r) = \
mrgIf \
(rs ==~ con 0) \
(throwError DivideByZero) \
(mrgReturn $ type $ op l r); \
QRIGHT(name) t (type l) rs@(type r) = \
mrgIf \
(rs ==~ con 0) \
(throwError (t DivideByZero)) \
(mrgReturn $ type $ op l r)
#define SAFE_DIVISION_FUNC2(name, type, op1, op2) \
name (type l) rs@(type r) = \
mrgIf \
(rs ==~ con 0) \
(throwError DivideByZero) \
(mrgReturn (type $ op1 l r, type $ op2 l r)); \
QRIGHT(name) t (type l) rs@(type r) = \
mrgIf \
(rs ==~ con 0) \
(throwError (t DivideByZero)) \
(mrgReturn (type $ op1 l r, type $ op2 l r))
#if 1
instance SafeDivision ArithException SymInteger where
SAFE_DIVISION_FUNC(safeDiv, SymInteger, pevalDivIntegralTerm)
SAFE_DIVISION_FUNC(safeMod, SymInteger, pevalModIntegralTerm)
SAFE_DIVISION_FUNC(safeQuot, SymInteger, pevalQuotIntegralTerm)
SAFE_DIVISION_FUNC(safeRem, SymInteger, pevalRemIntegralTerm)
SAFE_DIVISION_FUNC2(safeDivMod, SymInteger, pevalDivIntegralTerm, pevalModIntegralTerm)
SAFE_DIVISION_FUNC2(safeQuotRem, SymInteger, pevalQuotIntegralTerm, pevalRemIntegralTerm)
#endif
instance SafeLinearArith ArithException SymInteger where
safeAdd :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymInteger -> SymInteger -> uf SymInteger
safeAdd SymInteger
ls SymInteger
rs = forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn forall a b. (a -> b) -> a -> b
$ SymInteger
ls forall a. Num a => a -> a -> a
+ SymInteger
rs
safeAdd' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger
safeAdd' ArithException -> e'
_ SymInteger
ls SymInteger
rs = forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn forall a b. (a -> b) -> a -> b
$ SymInteger
ls forall a. Num a => a -> a -> a
+ SymInteger
rs
safeNeg :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymInteger -> uf SymInteger
safeNeg SymInteger
v = forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn forall a b. (a -> b) -> a -> b
$ -SymInteger
v
safeNeg' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymInteger -> uf SymInteger
safeNeg' ArithException -> e'
_ SymInteger
v = forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn forall a b. (a -> b) -> a -> b
$ -SymInteger
v
safeMinus :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymInteger -> SymInteger -> uf SymInteger
safeMinus SymInteger
ls SymInteger
rs = forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn forall a b. (a -> b) -> a -> b
$ SymInteger
ls forall a. Num a => a -> a -> a
- SymInteger
rs
safeMinus' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger
safeMinus' ArithException -> e'
_ SymInteger
ls SymInteger
rs = forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn forall a b. (a -> b) -> a -> b
$ SymInteger
ls forall a. Num a => a -> a -> a
- SymInteger
rs
instance SymIntegerOp SymInteger
newtype SymIntN (n :: Nat) = SymIntN {forall (n :: Natural). SymIntN n -> Term (IntN n)
underlyingIntNTerm :: Term (IntN n)}
deriving (forall (n :: Natural) (m :: * -> *). Quote m => SymIntN n -> m Exp
forall (n :: Natural) (m :: * -> *).
Quote m =>
SymIntN n -> Code m (SymIntN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymIntN n -> m Exp
forall (m :: * -> *). Quote m => SymIntN n -> Code m (SymIntN n)
liftTyped :: forall (m :: * -> *). Quote m => SymIntN n -> Code m (SymIntN n)
$cliftTyped :: forall (n :: Natural) (m :: * -> *).
Quote m =>
SymIntN n -> Code m (SymIntN n)
lift :: forall (m :: * -> *). Quote m => SymIntN n -> m Exp
$clift :: forall (n :: Natural) (m :: * -> *). Quote m => SymIntN n -> m Exp
Lift, SymIntN n -> ()
forall (n :: Natural). SymIntN n -> ()
forall a. (a -> ()) -> NFData a
rnf :: SymIntN n -> ()
$crnf :: forall (n :: Natural). SymIntN n -> ()
NFData, forall (n :: Natural) x. Rep (SymIntN n) x -> SymIntN n
forall (n :: Natural) x. SymIntN n -> Rep (SymIntN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Natural) x. Rep (SymIntN n) x -> SymIntN n
$cfrom :: forall (n :: Natural) x. SymIntN n -> Rep (SymIntN n) x
Generic)
#define SAFE_DIVISION_FUNC_BOUNDED_SIGNED(name, type, op) \
name ls@(type l) rs@(type r) = \
mrgIf \
(rs ==~ con 0) \
(throwError DivideByZero) \
(mrgIf (rs ==~ con (-1) &&~ ls ==~ con minBound) \
(throwError Overflow) \
(mrgReturn $ type $ op l r)); \
QRIGHT(name) t ls@(type l) rs@(type r) = \
mrgIf \
(rs ==~ con 0) \
(throwError (t DivideByZero)) \
(mrgIf (rs ==~ con (-1) &&~ ls ==~ con minBound) \
(throwError (t Overflow)) \
(mrgReturn $ type $ op l r))
#define SAFE_DIVISION_FUNC2_BOUNDED_SIGNED(name, type, op1, op2) \
name ls@(type l) rs@(type r) = \
mrgIf \
(rs ==~ con 0) \
(throwError DivideByZero) \
(mrgIf (rs ==~ con (-1) &&~ ls ==~ con minBound) \
(throwError Overflow) \
(mrgReturn (type $ op1 l r, type $ op2 l r))); \
QRIGHT(name) t ls@(type l) rs@(type r) = \
mrgIf \
(rs ==~ con 0) \
(throwError (t DivideByZero)) \
(mrgIf (rs ==~ con (-1) &&~ ls ==~ con minBound) \
(throwError (t Overflow)) \
(mrgReturn (type $ op1 l r, type $ op2 l r)))
#if 1
instance (KnownNat n, 1 <= n) => SafeDivision ArithException (SymIntN n) where
SAFE_DIVISION_FUNC_BOUNDED_SIGNED(safeDiv, SymIntN, pevalDivBoundedIntegralTerm)
SAFE_DIVISION_FUNC(safeMod, SymIntN, pevalModBoundedIntegralTerm)
SAFE_DIVISION_FUNC_BOUNDED_SIGNED(safeQuot, SymIntN, pevalQuotBoundedIntegralTerm)
SAFE_DIVISION_FUNC(safeRem, SymIntN, pevalRemBoundedIntegralTerm)
SAFE_DIVISION_FUNC2_BOUNDED_SIGNED(safeDivMod, SymIntN, pevalDivBoundedIntegralTerm, pevalModBoundedIntegralTerm)
SAFE_DIVISION_FUNC2_BOUNDED_SIGNED(safeQuotRem, SymIntN, pevalQuotBoundedIntegralTerm, pevalRemBoundedIntegralTerm)
#endif
instance (KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) where
safeAdd :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymIntN n -> SymIntN n -> uf (SymIntN n)
safeAdd SymIntN n
ls SymIntN n
rs =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls forall a. SOrd a => a -> a -> SymBool
>~ SymIntN n
0)
(forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymIntN n
rs forall a. SOrd a => a -> a -> SymBool
>~ SymIntN n
0 forall b. LogicalOp b => b -> b -> b
&&~ SymIntN n
res forall a. SOrd a => a -> a -> SymBool
<~ SymIntN n
0) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow) (forall (m :: * -> *) a. Monad m => a -> m a
return SymIntN n
res))
( forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls forall a. SOrd a => a -> a -> SymBool
<~ SymIntN n
0 forall b. LogicalOp b => b -> b -> b
&&~ SymIntN n
rs forall a. SOrd a => a -> a -> SymBool
<~ SymIntN n
0 forall b. LogicalOp b => b -> b -> b
&&~ SymIntN n
res forall a. SOrd a => a -> a -> SymBool
>=~ SymIntN n
0)
(forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Underflow)
(forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn SymIntN n
res)
)
where
res :: SymIntN n
res = SymIntN n
ls forall a. Num a => a -> a -> a
+ SymIntN n
rs
safeAdd' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n)
safeAdd' ArithException -> e'
f SymIntN n
ls SymIntN n
rs =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls forall a. SOrd a => a -> a -> SymBool
>~ SymIntN n
0)
(forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymIntN n
rs forall a. SOrd a => a -> a -> SymBool
>~ SymIntN n
0 forall b. LogicalOp b => b -> b -> b
&&~ SymIntN n
res forall a. SOrd a => a -> a -> SymBool
<~ SymIntN n
0) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Overflow) (forall (m :: * -> *) a. Monad m => a -> m a
return SymIntN n
res))
( forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls forall a. SOrd a => a -> a -> SymBool
<~ SymIntN n
0 forall b. LogicalOp b => b -> b -> b
&&~ SymIntN n
rs forall a. SOrd a => a -> a -> SymBool
<~ SymIntN n
0 forall b. LogicalOp b => b -> b -> b
&&~ SymIntN n
res forall a. SOrd a => a -> a -> SymBool
>=~ SymIntN n
0)
(forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Underflow)
(forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn SymIntN n
res)
)
where
res :: SymIntN n
res = SymIntN n
ls forall a. Num a => a -> a -> a
+ SymIntN n
rs
safeNeg :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymIntN n -> uf (SymIntN n)
safeNeg SymIntN n
v = forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymIntN n
v forall a. SEq a => a -> a -> SymBool
==~ forall c t. Solvable c t => c -> t
con forall a. Bounded a => a
minBound) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow) (forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn forall a b. (a -> b) -> a -> b
$ -SymIntN n
v)
safeNeg' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymIntN n -> uf (SymIntN n)
safeNeg' ArithException -> e'
f SymIntN n
v = forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymIntN n
v forall a. SEq a => a -> a -> SymBool
==~ forall c t. Solvable c t => c -> t
con forall a. Bounded a => a
minBound) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Overflow) (forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn forall a b. (a -> b) -> a -> b
$ -SymIntN n
v)
safeMinus :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymIntN n -> SymIntN n -> uf (SymIntN n)
safeMinus SymIntN n
ls SymIntN n
rs =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls forall a. SOrd a => a -> a -> SymBool
>=~ SymIntN n
0)
(forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymIntN n
rs forall a. SOrd a => a -> a -> SymBool
<~ SymIntN n
0 forall b. LogicalOp b => b -> b -> b
&&~ SymIntN n
res forall a. SOrd a => a -> a -> SymBool
<~ SymIntN n
0) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow) (forall (m :: * -> *) a. Monad m => a -> m a
return SymIntN n
res))
( forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls forall a. SOrd a => a -> a -> SymBool
<~ SymIntN n
0 forall b. LogicalOp b => b -> b -> b
&&~ SymIntN n
rs forall a. SOrd a => a -> a -> SymBool
>~ SymIntN n
0 forall b. LogicalOp b => b -> b -> b
&&~ SymIntN n
res forall a. SOrd a => a -> a -> SymBool
>~ SymIntN n
0)
(forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Underflow)
(forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn SymIntN n
res)
)
where
res :: SymIntN n
res = SymIntN n
ls forall a. Num a => a -> a -> a
- SymIntN n
rs
safeMinus' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n)
safeMinus' ArithException -> e'
f SymIntN n
ls SymIntN n
rs =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls forall a. SOrd a => a -> a -> SymBool
>=~ SymIntN n
0)
(forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymIntN n
rs forall a. SOrd a => a -> a -> SymBool
<~ SymIntN n
0 forall b. LogicalOp b => b -> b -> b
&&~ SymIntN n
res forall a. SOrd a => a -> a -> SymBool
<~ SymIntN n
0) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Overflow) (forall (m :: * -> *) a. Monad m => a -> m a
return SymIntN n
res))
( forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls forall a. SOrd a => a -> a -> SymBool
<~ SymIntN n
0 forall b. LogicalOp b => b -> b -> b
&&~ SymIntN n
rs forall a. SOrd a => a -> a -> SymBool
>~ SymIntN n
0 forall b. LogicalOp b => b -> b -> b
&&~ SymIntN n
res forall a. SOrd a => a -> a -> SymBool
>~ SymIntN n
0)
(forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Underflow)
(forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn SymIntN n
res)
)
where
res :: SymIntN n
res = SymIntN n
ls forall a. Num a => a -> a -> a
- SymIntN n
rs
data SomeSymIntN where
SomeSymIntN :: (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN
unarySomeSymIntN :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> r) -> String -> SomeSymIntN -> r
unarySomeSymIntN :: forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => SymIntN n -> r)
-> String -> SomeSymIntN -> r
unarySomeSymIntN forall (n :: Natural). (KnownNat n, 1 <= n) => SymIntN n -> r
op String
_ (SomeSymIntN (SymIntN n
w :: SymIntN w)) = forall (n :: Natural). (KnownNat n, 1 <= n) => SymIntN n -> r
op SymIntN n
w
{-# INLINE unarySomeSymIntN #-}
unarySomeSymIntNR1 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n) -> String -> SomeSymIntN -> SomeSymIntN
unarySomeSymIntNR1 :: (forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n)
-> String -> SomeSymIntN -> SomeSymIntN
unarySomeSymIntNR1 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n
op String
_ (SomeSymIntN (SymIntN n
w :: SymIntN w)) = forall (con :: Natural).
(KnownNat con, 1 <= con) =>
SymIntN con -> SomeSymIntN
SomeSymIntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n
op SymIntN n
w
{-# INLINE unarySomeSymIntNR1 #-}
binSomeSymIntN :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> r) -> String -> SomeSymIntN -> SomeSymIntN -> r
binSomeSymIntN :: forall r.
(forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> r)
-> String -> SomeSymIntN -> SomeSymIntN -> r
binSomeSymIntN forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> r
op String
str (SomeSymIntN (SymIntN n
l :: SymIntN l)) (SomeSymIntN (SymIntN n
r :: SymIntN r)) =
case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
(proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> r
op SymIntN n
l SymIntN n
r
Maybe (n :~: n)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Operation " forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
" on SymIntN with different bitwidth"
{-# INLINE binSomeSymIntN #-}
binSomeSymIntNR1 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> SymIntN n) -> String -> SomeSymIntN -> SomeSymIntN -> SomeSymIntN
binSomeSymIntNR1 :: (forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> SymIntN n)
-> String -> SomeSymIntN -> SomeSymIntN -> SomeSymIntN
binSomeSymIntNR1 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> SymIntN n
op String
str (SomeSymIntN (SymIntN n
l :: SymIntN l)) (SomeSymIntN (SymIntN n
r :: SymIntN r)) =
case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
(proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> forall (con :: Natural).
(KnownNat con, 1 <= con) =>
SymIntN con -> SomeSymIntN
SomeSymIntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> SymIntN n
op SymIntN n
l SymIntN n
r
Maybe (n :~: n)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Operation " forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
" on SymIntN with different bitwidth"
{-# INLINE binSomeSymIntNR1 #-}
binSomeSymIntNR2 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n)) -> String -> SomeSymIntN -> SomeSymIntN -> (SomeSymIntN, SomeSymIntN)
binSomeSymIntNR2 :: (forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n))
-> String
-> SomeSymIntN
-> SomeSymIntN
-> (SomeSymIntN, SomeSymIntN)
binSomeSymIntNR2 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n)
op String
str (SomeSymIntN (SymIntN n
l :: SymIntN l)) (SomeSymIntN (SymIntN n
r :: SymIntN r)) =
case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
(proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl ->
case forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n)
op SymIntN n
l SymIntN n
r of
(SymIntN n
a, SymIntN n
b) -> (forall (con :: Natural).
(KnownNat con, 1 <= con) =>
SymIntN con -> SomeSymIntN
SomeSymIntN SymIntN n
a, forall (con :: Natural).
(KnownNat con, 1 <= con) =>
SymIntN con -> SomeSymIntN
SomeSymIntN SymIntN n
b)
Maybe (n :~: n)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Operation " forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
" on SymIntN with different bitwidth"
{-# INLINE binSomeSymIntNR2 #-}
newtype SymWordN (n :: Nat) = SymWordN {forall (n :: Natural). SymWordN n -> Term (WordN n)
underlyingWordNTerm :: Term (WordN n)}
deriving (forall (n :: Natural) (m :: * -> *). Quote m => SymWordN n -> m Exp
forall (n :: Natural) (m :: * -> *).
Quote m =>
SymWordN n -> Code m (SymWordN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymWordN n -> m Exp
forall (m :: * -> *). Quote m => SymWordN n -> Code m (SymWordN n)
liftTyped :: forall (m :: * -> *). Quote m => SymWordN n -> Code m (SymWordN n)
$cliftTyped :: forall (n :: Natural) (m :: * -> *).
Quote m =>
SymWordN n -> Code m (SymWordN n)
lift :: forall (m :: * -> *). Quote m => SymWordN n -> m Exp
$clift :: forall (n :: Natural) (m :: * -> *). Quote m => SymWordN n -> m Exp
Lift, SymWordN n -> ()
forall (n :: Natural). SymWordN n -> ()
forall a. (a -> ()) -> NFData a
rnf :: SymWordN n -> ()
$crnf :: forall (n :: Natural). SymWordN n -> ()
NFData, forall (n :: Natural) x. Rep (SymWordN n) x -> SymWordN n
forall (n :: Natural) x. SymWordN n -> Rep (SymWordN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Natural) x. Rep (SymWordN n) x -> SymWordN n
$cfrom :: forall (n :: Natural) x. SymWordN n -> Rep (SymWordN n) x
Generic)
#if 1
instance (KnownNat n, 1 <= n) => SafeDivision ArithException (SymWordN n) where
SAFE_DIVISION_FUNC(safeDiv, SymWordN, pevalDivIntegralTerm)
SAFE_DIVISION_FUNC(safeMod, SymWordN, pevalModIntegralTerm)
SAFE_DIVISION_FUNC(safeQuot, SymWordN, pevalQuotIntegralTerm)
SAFE_DIVISION_FUNC(safeRem, SymWordN, pevalRemIntegralTerm)
SAFE_DIVISION_FUNC2(safeDivMod, SymWordN, pevalDivIntegralTerm, pevalModIntegralTerm)
SAFE_DIVISION_FUNC2(safeQuotRem, SymWordN, pevalQuotIntegralTerm, pevalRemIntegralTerm)
#endif
instance (KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) where
safeAdd :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymWordN n -> SymWordN n -> uf (SymWordN n)
safeAdd SymWordN n
ls SymWordN n
rs =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymWordN n
ls forall a. SOrd a => a -> a -> SymBool
>~ SymWordN n
res forall b. LogicalOp b => b -> b -> b
||~ SymWordN n
rs forall a. SOrd a => a -> a -> SymBool
>~ SymWordN n
res)
(forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow)
(forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn SymWordN n
res)
where
res :: SymWordN n
res = SymWordN n
ls forall a. Num a => a -> a -> a
+ SymWordN n
rs
safeAdd' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e')
-> SymWordN n -> SymWordN n -> uf (SymWordN n)
safeAdd' ArithException -> e'
f SymWordN n
ls SymWordN n
rs =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymWordN n
ls forall a. SOrd a => a -> a -> SymBool
>~ SymWordN n
res forall b. LogicalOp b => b -> b -> b
||~ SymWordN n
rs forall a. SOrd a => a -> a -> SymBool
>~ SymWordN n
res)
(forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Overflow)
(forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn SymWordN n
res)
where
res :: SymWordN n
res = SymWordN n
ls forall a. Num a => a -> a -> a
+ SymWordN n
rs
safeNeg :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymWordN n -> uf (SymWordN n)
safeNeg SymWordN n
v = forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymWordN n
v forall a. SEq a => a -> a -> SymBool
/=~ SymWordN n
0) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Underflow) (forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn SymWordN n
v)
safeNeg' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymWordN n -> uf (SymWordN n)
safeNeg' ArithException -> e'
f SymWordN n
v = forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymWordN n
v forall a. SEq a => a -> a -> SymBool
/=~ SymWordN n
0) (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Underflow) (forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn SymWordN n
v)
safeMinus :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymWordN n -> SymWordN n -> uf (SymWordN n)
safeMinus SymWordN n
ls SymWordN n
rs =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymWordN n
rs forall a. SOrd a => a -> a -> SymBool
>~ SymWordN n
ls)
(forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Underflow)
(forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn SymWordN n
res)
where
res :: SymWordN n
res = SymWordN n
ls forall a. Num a => a -> a -> a
- SymWordN n
rs
safeMinus' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e')
-> SymWordN n -> SymWordN n -> uf (SymWordN n)
safeMinus' ArithException -> e'
f SymWordN n
ls SymWordN n
rs =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymWordN n
rs forall a. SOrd a => a -> a -> SymBool
>~ SymWordN n
ls)
(forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Underflow)
(forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn SymWordN n
res)
where
res :: SymWordN n
res = SymWordN n
ls forall a. Num a => a -> a -> a
- SymWordN n
rs
data SomeSymWordN where
SomeSymWordN :: (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN
unarySomeSymWordN :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> r) -> String -> SomeSymWordN -> r
unarySomeSymWordN :: forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => SymWordN n -> r)
-> String -> SomeSymWordN -> r
unarySomeSymWordN forall (n :: Natural). (KnownNat n, 1 <= n) => SymWordN n -> r
op String
_ (SomeSymWordN (SymWordN n
w :: SymWordN w)) = forall (n :: Natural). (KnownNat n, 1 <= n) => SymWordN n -> r
op SymWordN n
w
{-# INLINE unarySomeSymWordN #-}
unarySomeSymWordNR1 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n) -> String -> SomeSymWordN -> SomeSymWordN
unarySomeSymWordNR1 :: (forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n)
-> String -> SomeSymWordN -> SomeSymWordN
unarySomeSymWordNR1 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n
op String
_ (SomeSymWordN (SymWordN n
w :: SymWordN w)) = forall (con :: Natural).
(KnownNat con, 1 <= con) =>
SymWordN con -> SomeSymWordN
SomeSymWordN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n
op SymWordN n
w
{-# INLINE unarySomeSymWordNR1 #-}
binSomeSymWordN :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> r) -> String -> SomeSymWordN -> SomeSymWordN -> r
binSomeSymWordN :: forall r.
(forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> r)
-> String -> SomeSymWordN -> SomeSymWordN -> r
binSomeSymWordN forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> r
op String
str (SomeSymWordN (SymWordN n
l :: SymWordN l)) (SomeSymWordN (SymWordN n
r :: SymWordN r)) =
case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
(proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> r
op SymWordN n
l SymWordN n
r
Maybe (n :~: n)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Operation " forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
" on SymWordN with different bitwidth"
{-# INLINE binSomeSymWordN #-}
binSomeSymWordNR1 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> SymWordN n) -> String -> SomeSymWordN -> SomeSymWordN -> SomeSymWordN
binSomeSymWordNR1 :: (forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> SymWordN n)
-> String -> SomeSymWordN -> SomeSymWordN -> SomeSymWordN
binSomeSymWordNR1 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> SymWordN n
op String
str (SomeSymWordN (SymWordN n
l :: SymWordN l)) (SomeSymWordN (SymWordN n
r :: SymWordN r)) =
case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
(proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> forall (con :: Natural).
(KnownNat con, 1 <= con) =>
SymWordN con -> SomeSymWordN
SomeSymWordN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> SymWordN n
op SymWordN n
l SymWordN n
r
Maybe (n :~: n)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Operation " forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
" on SymWordN with different bitwidth"
{-# INLINE binSomeSymWordNR1 #-}
binSomeSymWordNR2 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n)) -> String -> SomeSymWordN -> SomeSymWordN -> (SomeSymWordN, SomeSymWordN)
binSomeSymWordNR2 :: (forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n))
-> String
-> SomeSymWordN
-> SomeSymWordN
-> (SomeSymWordN, SomeSymWordN)
binSomeSymWordNR2 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n)
op String
str (SomeSymWordN (SymWordN n
l :: SymWordN l)) (SomeSymWordN (SymWordN n
r :: SymWordN r)) =
case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
(proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl ->
case forall (n :: Natural).
(KnownNat n, 1 <= n) =>
SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n)
op SymWordN n
l SymWordN n
r of
(SymWordN n
a, SymWordN n
b) -> (forall (con :: Natural).
(KnownNat con, 1 <= con) =>
SymWordN con -> SomeSymWordN
SomeSymWordN SymWordN n
a, forall (con :: Natural).
(KnownNat con, 1 <= con) =>
SymWordN con -> SomeSymWordN
SomeSymWordN SymWordN n
b)
Maybe (n :~: n)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Operation " forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
" on SymWordN with different bitwidth"
{-# INLINE binSomeSymWordNR2 #-}
instance ConRep SymBool where
type ConType SymBool = Bool
instance SymRep Bool where
type SymType Bool = SymBool
instance LinkedRep Bool SymBool where
underlyingTerm :: SymBool -> Term Bool
underlyingTerm (SymBool Term Bool
a) = Term Bool
a
wrapTerm :: Term Bool -> SymBool
wrapTerm = Term Bool -> SymBool
SymBool
instance ConRep SymInteger where
type ConType SymInteger = Integer
instance SymRep Integer where
type SymType Integer = SymInteger
instance LinkedRep Integer SymInteger where
underlyingTerm :: SymInteger -> Term Integer
underlyingTerm (SymInteger Term Integer
a) = Term Integer
a
wrapTerm :: Term Integer -> SymInteger
wrapTerm = Term Integer -> SymInteger
SymInteger
instance (KnownNat n, 1 <= n) => ConRep (SymIntN n) where
type ConType (SymIntN n) = IntN n
instance (KnownNat n, 1 <= n) => SymRep (IntN n) where
type SymType (IntN n) = SymIntN n
instance (KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) where
underlyingTerm :: SymIntN n -> Term (IntN n)
underlyingTerm (SymIntN Term (IntN n)
a) = Term (IntN n)
a
wrapTerm :: Term (IntN n) -> SymIntN n
wrapTerm = forall (n :: Natural). Term (IntN n) -> SymIntN n
SymIntN
instance (KnownNat n, 1 <= n) => ConRep (SymWordN n) where
type ConType (SymWordN n) = WordN n
instance (KnownNat n, 1 <= n) => SymRep (WordN n) where
type SymType (WordN n) = SymWordN n
instance (KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) where
underlyingTerm :: SymWordN n -> Term (WordN n)
underlyingTerm (SymWordN Term (WordN n)
a) = Term (WordN n)
a
wrapTerm :: Term (WordN n) -> SymWordN n
wrapTerm = forall (n :: Natural). Term (WordN n) -> SymWordN n
SymWordN
data sa =~> sb where
SymTabularFun :: (LinkedRep ca sa, LinkedRep cb sb) => Term (ca =-> cb) -> sa =~> sb
infixr 0 =~>
instance (ConRep a, ConRep b) => ConRep (a =~> b) where
type ConType (a =~> b) = ConType a =-> ConType b
instance (SymRep a, SymRep b) => SymRep (a =-> b) where
type SymType (a =-> b) = SymType a =~> SymType b
instance (LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca =-> cb) (sa =~> sb) where
underlyingTerm :: (sa =~> sb) -> Term (ca =-> cb)
underlyingTerm (SymTabularFun Term (ca =-> cb)
a) = Term (ca =-> cb)
a
wrapTerm :: Term (ca =-> cb) -> sa =~> sb
wrapTerm = forall ca sa cb sb.
(LinkedRep ca sa, LinkedRep cb sb) =>
Term (ca =-> cb) -> sa =~> sb
SymTabularFun
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Function (sa =~> sb) where
type Arg (sa =~> sb) = sa
type Ret (sa =~> sb) = sb
(SymTabularFun Term (ca =-> cb)
f) # :: (sa =~> sb) -> Arg (sa =~> sb) -> Ret (sa =~> sb)
# Arg (sa =~> sb)
t = forall con sym. LinkedRep con sym => Term con -> sym
wrapTerm forall a b. (a -> b) -> a -> b
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> Term a -> Term b
pevalTabularFunApplyTerm Term (ca =-> cb)
f (forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm Arg (sa =~> sb)
t)
data sa -~> sb where
SymGeneralFun :: (LinkedRep ca sa, LinkedRep cb sb) => Term (ca --> cb) -> sa -~> sb
infixr 0 -~>
instance (ConRep a, ConRep b) => ConRep (a -~> b) where
type ConType (a -~> b) = ConType a --> ConType b
instance (SymRep ca, SymRep cb) => SymRep (ca --> cb) where
type SymType (ca --> cb) = SymType ca -~> SymType cb
instance (LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca --> cb) (sa -~> sb) where
underlyingTerm :: (sa -~> sb) -> Term (ca --> cb)
underlyingTerm (SymGeneralFun Term (ca --> cb)
a) = Term (ca --> cb)
a
wrapTerm :: Term (ca --> cb) -> sa -~> sb
wrapTerm = forall ca sa cb sb.
(LinkedRep ca sa, LinkedRep cb sb) =>
Term (ca --> cb) -> sa -~> sb
SymGeneralFun
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Function (sa -~> sb) where
type Arg (sa -~> sb) = sa
type Ret (sa -~> sb) = sb
(SymGeneralFun Term (ca --> cb)
f) # :: (sa -~> sb) -> Arg (sa -~> sb) -> Ret (sa -~> sb)
# Arg (sa -~> sb)
t = forall con sym. LinkedRep con sym => Term con -> sym
wrapTerm forall a b. (a -> b) -> a -> b
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm Term (ca --> cb)
f (forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm Arg (sa -~> sb)
t)
(-->) :: (SupportedPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedSymbol ca -> sb -> ca --> cb
--> :: forall ca cb sb.
(SupportedPrim ca, SupportedPrim cb, LinkedRep cb sb) =>
TypedSymbol ca -> sb -> ca --> cb
(-->) TypedSymbol ca
arg sb
v = forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol ca
newarg (forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol ca
arg (forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm TypedSymbol ca
newarg) (forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sb
v))
where
newarg :: TypedSymbol ca
newarg = forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo TypedSymbol ca
arg ARG
ARG
infixr 0 -->
data ARG = ARG
deriving (ARG -> ARG -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ARG -> ARG -> Bool
$c/= :: ARG -> ARG -> Bool
== :: ARG -> ARG -> Bool
$c== :: ARG -> ARG -> Bool
Eq, Eq ARG
ARG -> ARG -> Bool
ARG -> ARG -> Ordering
ARG -> ARG -> ARG
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ARG -> ARG -> ARG
$cmin :: ARG -> ARG -> ARG
max :: ARG -> ARG -> ARG
$cmax :: ARG -> ARG -> ARG
>= :: ARG -> ARG -> Bool
$c>= :: ARG -> ARG -> Bool
> :: ARG -> ARG -> Bool
$c> :: ARG -> ARG -> Bool
<= :: ARG -> ARG -> Bool
$c<= :: ARG -> ARG -> Bool
< :: ARG -> ARG -> Bool
$c< :: ARG -> ARG -> Bool
compare :: ARG -> ARG -> Ordering
$ccompare :: ARG -> ARG -> Ordering
Ord, forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => ARG -> m Exp
forall (m :: * -> *). Quote m => ARG -> Code m ARG
liftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
$cliftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
lift :: forall (m :: * -> *). Quote m => ARG -> m Exp
$clift :: forall (m :: * -> *). Quote m => ARG -> m Exp
Lift, Int -> ARG -> ShowS
[ARG] -> ShowS
ARG -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ARG] -> ShowS
$cshowList :: [ARG] -> ShowS
show :: ARG -> String
$cshow :: ARG -> String
showsPrec :: Int -> ARG -> ShowS
$cshowsPrec :: Int -> ARG -> ShowS
Show, forall x. Rep ARG x -> ARG
forall x. ARG -> Rep ARG x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ARG x -> ARG
$cfrom :: forall x. ARG -> Rep ARG x
Generic)
instance NFData ARG where
rnf :: ARG -> ()
rnf ARG
ARG = ()
instance Hashable ARG where
hashWithSalt :: Int -> ARG -> Int
hashWithSalt Int
s ARG
ARG = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int)
#define GPRETTY_SYM_SIMPLE(symtype) \
instance GPretty symtype where \
gpretty (symtype t) = prettyPrintTerm t
#define GPRETTY_SYM_BV(symtype) \
instance (KnownNat n, 1 <= n) => GPretty (symtype n) where \
gpretty (symtype t) = prettyPrintTerm t
#define GPRETTY_SYM_FUN(op, cons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb)\
=> GPretty (sa op sb) where \
gpretty (cons t) = prettyPrintTerm t
#define GPRETTY_SYM_SOME_BV(symtype) \
instance GPretty symtype where \
gpretty (symtype t) = gpretty t
#if 1
GPRETTY_SYM_SIMPLE(SymBool)
GPRETTY_SYM_SIMPLE(SymInteger)
GPRETTY_SYM_BV(SymIntN)
GPRETTY_SYM_BV(SymWordN)
GPRETTY_SYM_FUN(=~>, SymTabularFun)
GPRETTY_SYM_FUN(-~>, SymGeneralFun)
GPRETTY_SYM_SOME_BV(SomeSymIntN)
GPRETTY_SYM_SOME_BV(SomeSymWordN)
#endif
#define NUM_BV(symtype) \
instance (KnownNat n, 1 <= n) => Num (symtype n) where \
(symtype l) + (symtype r) = symtype $ pevalAddNumTerm l r; \
(symtype l) - (symtype r) = symtype $ pevalMinusNumTerm l r; \
(symtype l) * (symtype r) = symtype $ pevalTimesNumTerm l r; \
negate (symtype v) = symtype $ pevalUMinusNumTerm v; \
abs (symtype v) = symtype $ pevalAbsNumTerm v; \
signum (symtype v) = symtype $ pevalSignumNumTerm v; \
fromInteger i = con $ fromInteger i
#define NUM_SOME_BV(somety, br1, ur1) \
instance Num somety where \
(+) = br1 (+) "+"; \
{-# INLINE (+) #-}; \
(-) = br1 (-) "-"; \
{-# INLINE (-) #-}; \
(*) = br1 (*) "*"; \
{-# INLINE (*) #-}; \
negate = ur1 negate "negate"; \
{-# INLINE negate #-}; \
abs = ur1 abs "abs"; \
{-# INLINE abs #-}; \
signum = ur1 signum "signum"; \
{-# INLINE signum #-}; \
fromInteger = error "fromInteger is not defined for SomeSymWordN as no bitwidth is known"; \
{-# INLINE fromInteger #-}
#if 1
NUM_BV(SymIntN)
NUM_BV(SymWordN)
NUM_SOME_BV(SomeSymWordN, binSomeSymWordNR1, unarySomeSymWordNR1)
NUM_SOME_BV(SomeSymIntN, binSomeSymIntNR1, unarySomeSymIntNR1)
#endif
instance Num SymInteger where
(SymInteger Term Integer
l) + :: SymInteger -> SymInteger -> SymInteger
+ (SymInteger Term Integer
r) = Term Integer -> SymInteger
SymInteger forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term Integer
l Term Integer
r
(SymInteger Term Integer
l) - :: SymInteger -> SymInteger -> SymInteger
- (SymInteger Term Integer
r) = Term Integer -> SymInteger
SymInteger forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm Term Integer
l Term Integer
r
(SymInteger Term Integer
l) * :: SymInteger -> SymInteger -> SymInteger
* (SymInteger Term Integer
r) = Term Integer -> SymInteger
SymInteger forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term Integer
l Term Integer
r
negate :: SymInteger -> SymInteger
negate (SymInteger Term Integer
v) = Term Integer -> SymInteger
SymInteger forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term Integer
v
abs :: SymInteger -> SymInteger
abs (SymInteger Term Integer
v) = Term Integer -> SymInteger
SymInteger forall a b. (a -> b) -> a -> b
$ forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm Term Integer
v
signum :: SymInteger -> SymInteger
signum (SymInteger Term Integer
v) = Term Integer -> SymInteger
SymInteger forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm Term Integer
v
fromInteger :: Integer -> SymInteger
fromInteger = forall c t. Solvable c t => c -> t
con
#define BITS_BV(symtype, signed) \
instance (KnownNat n, 1 <= n) => Bits (symtype n) where \
symtype l .&. symtype r = symtype $ pevalAndBitsTerm l r; \
{-# INLINE (.&.) #-}; \
symtype l .|. symtype r = symtype $ pevalOrBitsTerm l r; \
{-# INLINE (.|.) #-}; \
symtype l `xor` symtype r = symtype $ pevalXorBitsTerm l r; \
{-# INLINE xor #-}; \
complement (symtype n) = symtype $ pevalComplementBitsTerm n; \
{-# INLINE complement #-}; \
shift (symtype n) i = symtype $ pevalShiftBitsTerm n i; \
{-# INLINE shift #-}; \
rotate (symtype n) i = symtype $ pevalRotateBitsTerm n i; \
{-# INLINE rotate #-}; \
bitSize = finiteBitSize; \
{-# INLINE bitSize #-}; \
bitSizeMaybe = Just . finiteBitSize; \
{-# INLINE bitSizeMaybe #-}; \
isSigned _ = signed; \
{-# INLINE isSigned #-}; \
testBit (Con n) = testBit n; \
testBit _ = error "You cannot call testBit on symbolic variables"; \
{-# INLINE testBit #-}; \
bit = con . bit; \
{-# INLINE bit #-}; \
popCount (Con n) = popCount n; \
popCount _ = error "You cannot call popCount on symbolic variables"; \
{-# INLINE popCount #-}
#define BITS_BV_SOME(somety, origty, br1, uf, ur1) \
instance Bits somety where \
(.&.) = br1 (.&.) ".&."; \
{-# INLINE (.&.) #-}; \
(.|.) = br1 (.|.) ".|."; \
{-# INLINE (.|.) #-}; \
xor = br1 xor "xor"; \
{-# INLINE xor #-}; \
complement = ur1 complement "complement"; \
{-# INLINE complement #-}; \
shift s i = ur1 (`shift` i) "shift" s; \
{-# INLINE shift #-}; \
rotate s i = ur1 (`rotate` i) "rotate" s; \
{-# INLINE rotate #-}; \
zeroBits = error ("zeroBits is not defined for " ++ show (typeRep (Proxy @somety)) ++ " as no bitwidth is known"); \
{-# INLINE zeroBits #-}; \
bit = error ("bit is not defined for " ++ show (typeRep (Proxy @somety)) ++ " as no bitwidth is known"); \
{-# INLINE bit #-}; \
setBit s i = ur1 (`setBit` i) "setBit" s; \
{-# INLINE setBit #-}; \
clearBit s i = ur1 (`clearBit` i) "clearBit" s; \
{-# INLINE clearBit #-}; \
complementBit s i = ur1 (`complementBit` i) "complementBit" s; \
{-# INLINE complementBit #-}; \
testBit s i = uf (`testBit` i) "testBit" s; \
{-# INLINE testBit #-}; \
bitSizeMaybe = Just . finiteBitSize; \
{-# INLINE bitSizeMaybe #-}; \
bitSize = finiteBitSize; \
{-# INLINE bitSize #-}; \
isSigned _ = False; \
{-# INLINE isSigned #-}; \
shiftL s i = ur1 (`shiftL` i) "shiftL" s; \
{-# INLINE shiftL #-}; \
unsafeShiftL s i = ur1 (`unsafeShiftL` i) "unsafeShiftL" s; \
{-# INLINE unsafeShiftL #-}; \
shiftR s i = ur1 (`shiftR` i) "shiftR" s; \
{-# INLINE shiftR #-}; \
unsafeShiftR s i = ur1 (`unsafeShiftR` i) "unsafeShiftR" s; \
{-# INLINE unsafeShiftR #-}; \
rotateL s i = ur1 (`rotateL` i) "rotateL" s; \
{-# INLINE rotateL #-}; \
rotateR s i = ur1 (`rotateR` i) "rotateR" s; \
{-# INLINE rotateR #-}; \
popCount = uf popCount "popCount"; \
{-# INLINE popCount #-}
#if 1
BITS_BV(SymIntN, True)
BITS_BV(SymWordN, False)
BITS_BV_SOME(SomeSymIntN, SymIntN, binSomeSymIntNR1, unarySomeSymIntN, unarySomeSymIntNR1)
BITS_BV_SOME(SomeSymWordN, SymWordN, binSomeSymWordNR1, unarySomeSymWordN, unarySomeSymWordNR1)
#endif
#define FINITE_BITS_BV(symtype) \
instance (KnownNat n, 1 <= n) => FiniteBits (symtype n) where \
finiteBitSize _ = fromIntegral $ natVal (Proxy @n); \
{-# INLINE finiteBitSize #-}; \
#define FINITE_BITS_BV_SOME(somety, origty) \
instance FiniteBits somety where \
finiteBitSize (somety (n :: origty n)) = fromIntegral $ natVal n; \
{-# INLINE finiteBitSize #-}
#if 1
FINITE_BITS_BV(SymIntN)
FINITE_BITS_BV(SymWordN)
FINITE_BITS_BV_SOME(SomeSymIntN, SymIntN)
FINITE_BITS_BV_SOME(SomeSymWordN, SymWordN)
#endif
#define SHOW_SIMPLE(symtype) \
instance Show symtype where \
show (symtype t) = pformat t
#define SHOW_BV(symtype) \
instance (KnownNat n, 1 <= n) => Show (symtype n) where \
show (symtype t) = pformat t
#define SHOW_FUN(op, cons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Show (sa op sb) where \
show (cons t) = pformat t
#define SHOW_BV_SOME(somety) \
instance Show somety where \
show (somety t) = show t
#if 1
SHOW_SIMPLE(SymBool)
SHOW_SIMPLE(SymInteger)
SHOW_BV(SymIntN)
SHOW_BV(SymWordN)
SHOW_FUN(=~>, SymTabularFun)
SHOW_FUN(-~>, SymGeneralFun)
SHOW_BV_SOME(SomeSymIntN)
SHOW_BV_SOME(SomeSymWordN)
#endif
#define HASHABLE_SIMPLE(symtype) \
instance Hashable symtype where \
hashWithSalt s (symtype v) = s `hashWithSalt` v
#define HASHABLE_BV(symtype) \
instance (KnownNat n, 1 <= n) => Hashable (symtype n) where \
hashWithSalt s (symtype v) = s `hashWithSalt` v
#define HASHABLE_FUN(op, cons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Hashable (sa op sb) where \
hashWithSalt s (cons v) = s `hashWithSalt` v
#define HASHABLE_BV_SOME(somety, origty) \
instance Hashable somety where \
s `hashWithSalt` (somety (w :: origty n)) = s `hashWithSalt` natVal (Proxy @n) `hashWithSalt` w
#if 1
HASHABLE_SIMPLE(SymBool)
HASHABLE_SIMPLE(SymInteger)
HASHABLE_BV(SymIntN)
HASHABLE_BV(SymWordN)
HASHABLE_FUN(=~>, SymTabularFun)
HASHABLE_FUN(-~>, SymGeneralFun)
HASHABLE_BV_SOME(SomeSymIntN, SymIntN)
HASHABLE_BV_SOME(SomeSymWordN, SymWordNInt
)
#endif
#define EQ_SIMPLE(symtype) \
instance Eq symtype where \
(symtype l) == (symtype r) = l == r
#define EQ_BV(symtype) \
instance (KnownNat n, 1 <= n) => Eq (symtype n) where \
(symtype l) == (symtype r) = l == r
#define EQ_BV_SOME(symtype, bf) \
instance Eq symtype where; \
(==) = bf (==) "=="; \
{-# INLINE (==) #-}; \
(/=) = bf (/=) "/="; \
{-# INLINE (/=) #-}
#define EQ_FUN(op, cons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Eq (sa op sb) where \
(cons l) == (cons r) = l == r
#if 1
EQ_SIMPLE(SymBool)
EQ_SIMPLE(SymInteger)
EQ_BV(SymIntN)
EQ_BV(SymWordN)
EQ_FUN(=~>, SymTabularFun)
EQ_FUN(-~>, SymGeneralFun)
EQ_BV_SOME(SomeSymIntN, binSomeSymIntN)
EQ_BV_SOME(SomeSymWordN, binSomeSymWordN)
#endif
#define IS_STRING_SIMPLE(symtype) \
instance IsString symtype where \
fromString = ssym
#define IS_STRING_BV(symtype) \
instance (KnownNat n, 1 <= n) => IsString (symtype n) where \
fromString = ssym
#define IS_STRING_FUN(op, cons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => IsString (sa op sb) where \
fromString = ssym
#if 1
IS_STRING_SIMPLE(SymBool)
IS_STRING_SIMPLE(SymInteger)
IS_STRING_BV(SymIntN)
IS_STRING_BV(SymWordN)
IS_STRING_FUN(=~>, SymTabularFunc)
IS_STRING_FUN(-~>, SymGeneralFun)
#endif
#define SOLVABLE_SIMPLE(contype, symtype) \
instance Solvable contype symtype where \
con = symtype . conTerm; \
ssym = symtype . ssymTerm; \
isym str i = symtype $ isymTerm str i; \
sinfosym str info = symtype $ sinfosymTerm str info; \
iinfosym str i info = symtype $ iinfosymTerm str i info; \
conView (symtype (ConTerm _ t)) = Just t; \
conView _ = Nothing
#define SOLVABLE_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => Solvable (contype n) (symtype n) where \
con = symtype . conTerm; \
ssym = symtype . ssymTerm; \
isym str i = symtype $ isymTerm str i; \
sinfosym str info = symtype $ sinfosymTerm str info; \
iinfosym str i info = symtype $ iinfosymTerm str i info; \
conView (symtype (ConTerm _ t)) = Just t; \
conView _ = Nothing
#define SOLVABLE_FUN(symop, conop, symcons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Solvable (conop ca cb) (symop sa sb) where \
con = symcons . conTerm; \
ssym = symcons . ssymTerm; \
isym str i = symcons $ isymTerm str i; \
sinfosym str info = symcons $ sinfosymTerm str info; \
iinfosym str i info = symcons $ iinfosymTerm str i info; \
conView (symcons (ConTerm _ t)) = Just t; \
conView _ = Nothing
#if 1
SOLVABLE_SIMPLE(Bool, SymBool)
SOLVABLE_SIMPLE(Integer, SymInteger)
SOLVABLE_BV(IntN, SymIntN)
SOLVABLE_BV(WordN, SymWordN)
SOLVABLE_FUN((=~>), (=->), SymTabularFun)
SOLVABLE_FUN((-~>), (-->), SymGeneralFun)
#endif
#define TO_SYM_SYMID_SIMPLE(symtype) \
instance ToSym symtype symtype where \
toSym = id
#define TO_SYM_SYMID_BV(symtype) \
instance (KnownNat n, 1 <= n) => ToSym (symtype n) (symtype n) where \
toSym = id
#define TO_SYM_SYMID_FUN(op) \
instance (SupportedPrim a, SupportedPrim b) => ToSym (a op b) (a op b) where \
toSym = id
#if 1
TO_SYM_SYMID_SIMPLE(SymBool)
TO_SYM_SYMID_SIMPLE(SymInteger)
TO_SYM_SYMID_BV(SymIntN)
TO_SYM_SYMID_BV(SymWordN)
TO_SYM_SYMID_FUN(=~>)
TO_SYM_SYMID_FUN(-~>)
TO_SYM_SYMID_SIMPLE(SomeSymIntN)
TO_SYM_SYMID_SIMPLE(SomeSymWordN)
#endif
#define TO_SYM_FROMCON_SIMPLE(contype, symtype) \
instance ToSym contype symtype where \
toSym = con
#define TO_SYM_FROMCON_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => ToSym (contype n) (symtype n) where \
toSym = con
#define TO_SYM_FROMCON_FUN(conop, symop) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToSym (conop ca cb) (symop sa sb) where \
toSym = con
#define TO_SYM_FROMCON_BV_SOME(contype, symtype) \
instance ToSym contype symtype where \
toSym (contype v) = symtype (con v)
#if 1
TO_SYM_FROMCON_SIMPLE(Bool, SymBool)
TO_SYM_FROMCON_SIMPLE(Integer, SymInteger)
TO_SYM_FROMCON_BV(IntN, SymIntN)
TO_SYM_FROMCON_BV(WordN, SymWordN)
TO_SYM_FROMCON_FUN((=->), (=~>))
TO_SYM_FROMCON_FUN((-->), (-~>))
TO_SYM_FROMCON_BV_SOME(SomeIntN, SomeSymIntN)
TO_SYM_FROMCON_BV_SOME(SomeWordN, SomeSymWordN)
#endif
#define TO_CON_SYMID_SIMPLE(symtype) \
instance ToCon symtype symtype where \
toCon = Just
#define TO_CON_SYMID_BV(symtype) \
instance (KnownNat n, 1 <= n) => ToCon (symtype n) (symtype n) where \
toCon = Just
#define TO_CON_SYMID_FUN(op) \
instance (SupportedPrim a, SupportedPrim b) => ToCon (a op b) (a op b) where \
toCon = Just
#if 1
TO_CON_SYMID_SIMPLE(SymBool)
TO_CON_SYMID_SIMPLE(SymInteger)
TO_CON_SYMID_BV(SymIntN)
TO_CON_SYMID_BV(SymWordN)
TO_CON_SYMID_FUN(=~>)
TO_CON_SYMID_FUN(-~>)
TO_CON_SYMID_SIMPLE(SomeSymIntN)
TO_CON_SYMID_SIMPLE(SomeSymWordN)
#endif
#define TO_CON_FROMSYM_SIMPLE(contype, symtype) \
instance ToCon symtype contype where \
toCon = conView
#define TO_CON_FROMSYM_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => ToCon (symtype n) (contype n) where \
toCon = conView
#define TO_CON_FROMSYM_FUN(conop, symop) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToCon (symop sa sb) (conop ca cb) where \
toCon = conView
#define TO_CON_FROMSYM_BV_SOME(contype, symtype) \
instance ToCon symtype contype where \
toCon (symtype v) = contype <$> conView v
#if 1
TO_CON_FROMSYM_SIMPLE(Bool, SymBool)
TO_CON_FROMSYM_SIMPLE(Integer, SymInteger)
TO_CON_FROMSYM_BV(IntN, SymIntN)
TO_CON_FROMSYM_BV(WordN, SymWordN)
TO_CON_FROMSYM_FUN((=->), (=~>))
TO_CON_FROMSYM_FUN((-->), (-~>))
TO_CON_FROMSYM_BV_SOME(SomeIntN, SomeSymIntN)
TO_CON_FROMSYM_BV_SOME(SomeWordN, SomeSymWordN)
#endif
#define TO_SYM_FROMBV_SOME(somesymbv, bv) \
instance (KnownNat n, 1 <= n) => ToSym (bv n) somesymbv where \
toSym = somesymbv . con
#if 1
TO_SYM_FROMBV_SOME(SomeSymIntN, IntN)
TO_SYM_FROMBV_SOME(SomeSymWordN, WordN)
#endif
#define TOSYM_MACHINE_INTEGER(int, bv) \
instance ToSym int (bv) where \
toSym = fromIntegral
#define TOSYM_MACHINE_INTEGER_SOME(int, somesymbv, bv, bitwidth) \
instance ToSym int somesymbv where \
toSym v = somesymbv (con (fromIntegral v :: bv bitwidth))
#define TOCON_MACHINE_INTEGER(sbvw, bvw, n, int) \
instance ToCon (sbvw n) int where \
toCon (Con (bvw v :: bvw n)) = Just $ fromIntegral v; \
toCon _ = Nothing
#if 1
TOSYM_MACHINE_INTEGER(Int8, SymIntN 8)
TOSYM_MACHINE_INTEGER(Int16, SymIntN 16)
TOSYM_MACHINE_INTEGER(Int32, SymIntN 32)
TOSYM_MACHINE_INTEGER(Int64, SymIntN 64)
TOSYM_MACHINE_INTEGER(Word8, SymWordN 8)
TOSYM_MACHINE_INTEGER(Word16, SymWordN 16)
TOSYM_MACHINE_INTEGER(Word32, SymWordN 32)
TOSYM_MACHINE_INTEGER(Word64, SymWordN 64)
TOSYM_MACHINE_INTEGER(Int, SymIntN $intBitwidthQ)
TOSYM_MACHINE_INTEGER(Word, SymWordN $intBitwidthQ)
TOSYM_MACHINE_INTEGER_SOME(Int8, SomeSymIntN, IntN, 8)
TOSYM_MACHINE_INTEGER_SOME(Int16, SomeSymIntN, IntN, 16)
TOSYM_MACHINE_INTEGER_SOME(Int32, SomeSymIntN, IntN, 32)
TOSYM_MACHINE_INTEGER_SOME(Int64, SomeSymIntN, IntN, 64)
TOSYM_MACHINE_INTEGER_SOME(Word8, SomeSymWordN, WordN, 8)
TOSYM_MACHINE_INTEGER_SOME(Word16, SomeSymWordN, WordN, 16)
TOSYM_MACHINE_INTEGER_SOME(Word32, SomeSymWordN, WordN, 32)
TOSYM_MACHINE_INTEGER_SOME(Word64, SomeSymWordN, WordN, 64)
TOSYM_MACHINE_INTEGER_SOME(Int, SomeSymIntN, IntN, $intBitwidthQ)
TOSYM_MACHINE_INTEGER_SOME(Word, SomeSymWordN, WordN, $intBitwidthQ)
TOCON_MACHINE_INTEGER(SymIntN, IntN, 8, Int8)
TOCON_MACHINE_INTEGER(SymIntN, IntN, 16, Int16)
TOCON_MACHINE_INTEGER(SymIntN, IntN, 32, Int32)
TOCON_MACHINE_INTEGER(SymIntN, IntN, 64, Int64)
TOCON_MACHINE_INTEGER(SymWordN, WordN, 8, Word8)
TOCON_MACHINE_INTEGER(SymWordN, WordN, 16, Word16)
TOCON_MACHINE_INTEGER(SymWordN, WordN, 32, Word32)
TOCON_MACHINE_INTEGER(SymWordN, WordN, 64, Word64)
TOCON_MACHINE_INTEGER(SymIntN, IntN, $intBitwidthQ, Int)
TOCON_MACHINE_INTEGER(SymWordN, WordN, $intBitwidthQ, Word)
#endif
#define EVALUATE_SYM_SIMPLE(symtype) \
instance EvaluateSym symtype where \
evaluateSym fillDefault model (symtype t) = symtype $ evaluateTerm fillDefault model t
#define EVALUATE_SYM_BV(symtype) \
instance (KnownNat n, 1 <= n) => EvaluateSym (symtype n) where \
evaluateSym fillDefault model (symtype t) = symtype $ evaluateTerm fillDefault model t
#define EVALUATE_SYM_FUN(op, cons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => EvaluateSym (sa op sb) where \
evaluateSym fillDefault model (cons t) = cons $ evaluateTerm fillDefault model t
#define EVALUATE_SYM_BV_SOME(somety, origty) \
instance EvaluateSym somety where \
evaluateSym fillDefault model (somety (origty t)) = somety $ origty $ evaluateTerm fillDefault model t
#if 1
EVALUATE_SYM_SIMPLE(SymBool)
EVALUATE_SYM_SIMPLE(SymInteger)
EVALUATE_SYM_BV(SymIntN)
EVALUATE_SYM_BV(SymWordN)
EVALUATE_SYM_FUN(=~>, SymTabularFun)
EVALUATE_SYM_FUN(-~>, SymGeneralFun)
EVALUATE_SYM_BV_SOME(SomeSymIntN, SymIntN)
EVALUATE_SYM_BV_SOME(SomeSymWordN, SymWordN)
#endif
#define EXTRACT_SYMBOLICS_SIMPLE(symtype) \
instance ExtractSymbolics symtype where \
extractSymbolics (symtype t) = SymbolSet $ extractSymbolicsTerm t
#define EXTRACT_SYMBOLICS_BV(symtype) \
instance (KnownNat n, 1 <= n) => ExtractSymbolics (symtype n) where \
extractSymbolics (symtype t) = SymbolSet $ extractSymbolicsTerm t
#define EXTRACT_SYMBOLICS_FUN(op, cons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ExtractSymbolics (sa op sb) where \
extractSymbolics (cons t) = SymbolSet $ extractSymbolicsTerm t
#define EXTRACT_SYMBOLICS_BV_SOME(somety, origty) \
instance ExtractSymbolics somety where \
extractSymbolics (somety (origty t)) = SymbolSet $ extractSymbolicsTerm t
#if 1
EXTRACT_SYMBOLICS_SIMPLE(SymBool)
EXTRACT_SYMBOLICS_SIMPLE(SymInteger)
EXTRACT_SYMBOLICS_BV(SymIntN)
EXTRACT_SYMBOLICS_BV(SymWordN)
EXTRACT_SYMBOLICS_FUN(=~>, SymTabularFun)
EXTRACT_SYMBOLICS_FUN(-~>, SymGeneralFun)
EXTRACT_SYMBOLICS_BV_SOME(SomeSymIntN, SymIntN)
EXTRACT_SYMBOLICS_BV_SOME(SomeSymWordN, SymWordN)
#endif
#define SEQ_SIMPLE(symtype) \
instance SEq symtype where \
(symtype l) ==~ (symtype r) = SymBool $ pevalEqvTerm l r
#define SEQ_BV(symtype) \
instance (KnownNat n, 1 <= n) => SEq (symtype n) where \
(symtype l) ==~ (symtype r) = SymBool $ pevalEqvTerm l r
#define SEQ_BV_SOME(somety, origty) \
instance SEq somety where \
somety (l :: origty l) ==~ somety (r :: origty r) = \
(case sameNat (Proxy @l) (Proxy @r) of \
Just Refl -> l ==~ r; \
Nothing -> con False); \
{-# INLINE (==~) #-}; \
somety (l :: origty l) /=~ somety (r :: origty r) = \
(case sameNat (Proxy @l) (Proxy @r) of \
Just Refl -> l /=~ r; \
Nothing -> con True); \
{-# INLINE (/=~) #-}
#if 1
SEQ_SIMPLE(SymBool)
SEQ_SIMPLE(SymInteger)
SEQ_BV(SymIntN)
SEQ_BV(SymWordN)
SEQ_BV_SOME(SomeSymIntN, SymIntN)
SEQ_BV_SOME(SomeSymWordN, SymWordN)
#endif
#define SORD_SIMPLE(symtype) \
instance SOrd symtype where \
(symtype a) <=~ (symtype b) = SymBool $ pevalLeNumTerm a b; \
(symtype a) <~ (symtype b) = SymBool $ pevalLtNumTerm a b; \
(symtype a) >=~ (symtype b) = SymBool $ pevalGeNumTerm a b; \
(symtype a) >~ (symtype b) = SymBool $ pevalGtNumTerm a b; \
a `symCompare` b = mrgIf \
(a <~ b) \
(mrgReturn LT) \
(mrgIf (a ==~ b) (mrgReturn EQ) (mrgReturn GT))
#define SORD_BV(symtype) \
instance (KnownNat n, 1 <= n) => SOrd (symtype n) where \
(symtype a) <=~ (symtype b) = SymBool $ pevalLeNumTerm a b; \
(symtype a) <~ (symtype b) = SymBool $ pevalLtNumTerm a b; \
(symtype a) >=~ (symtype b) = SymBool $ pevalGeNumTerm a b; \
(symtype a) >~ (symtype b) = SymBool $ pevalGtNumTerm a b; \
a `symCompare` b = mrgIf \
(a <~ b) \
(mrgReturn LT) \
(mrgIf (a ==~ b) (mrgReturn EQ) (mrgReturn GT))
#define SORD_BV_SOME(somety, bf) \
instance SOrd somety where \
(<=~) = bf (<=~) "<=~"; \
{-# INLINE (<=~) #-}; \
(<~) = bf (<~) "<~"; \
{-# INLINE (<~) #-}; \
(>=~) = bf (>=~) ">=~"; \
{-# INLINE (>=~) #-}; \
(>~) = bf (>~) ">~"; \
{-# INLINE (>~) #-}; \
symCompare = bf symCompare "symCompare"; \
{-# INLINE symCompare #-}
instance SOrd SymBool where
SymBool
l <=~ :: SymBool -> SymBool -> SymBool
<=~ SymBool
r = forall b. LogicalOp b => b -> b
nots SymBool
l forall b. LogicalOp b => b -> b -> b
||~ SymBool
r
SymBool
l <~ :: SymBool -> SymBool -> SymBool
<~ SymBool
r = forall b. LogicalOp b => b -> b
nots SymBool
l forall b. LogicalOp b => b -> b -> b
&&~ SymBool
r
SymBool
l >=~ :: SymBool -> SymBool -> SymBool
>=~ SymBool
r = SymBool
l forall b. LogicalOp b => b -> b -> b
||~ forall b. LogicalOp b => b -> b
nots SymBool
r
SymBool
l >~ :: SymBool -> SymBool -> SymBool
>~ SymBool
r = SymBool
l forall b. LogicalOp b => b -> b -> b
&&~ forall b. LogicalOp b => b -> b
nots SymBool
r
symCompare :: SymBool -> SymBool -> UnionM Ordering
symCompare SymBool
l SymBool
r =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(forall b. LogicalOp b => b -> b
nots SymBool
l forall b. LogicalOp b => b -> b -> b
&&~ SymBool
r)
(forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn Ordering
LT)
(forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymBool
l forall a. SEq a => a -> a -> SymBool
==~ SymBool
r) (forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn Ordering
EQ) (forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn Ordering
GT))
#if 1
SORD_SIMPLE(SymInteger)
SORD_BV(SymIntN)
SORD_BV(SymWordN)
SORD_BV_SOME(SomeSymIntN, binSomeSymIntN)
SORD_BV_SOME(SomeSymWordN, binSomeSymWordN)
#endif
#define SUBSTITUTE_SYM_SIMPLE(symtype) \
instance SubstituteSym symtype where \
substituteSym sym v (symtype t) = symtype $ substTerm sym (underlyingTerm v) t
#define SUBSTITUTE_SYM_BV(symtype) \
instance (KnownNat n, 1 <= n) => SubstituteSym (symtype n) where \
substituteSym sym v (symtype t) = symtype $ substTerm sym (underlyingTerm v) t
#define SUBSTITUTE_SYM_FUN(op, cons) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => SubstituteSym (sa op sb) where \
substituteSym sym v (cons t) = cons $ substTerm sym (underlyingTerm v) t
#define SUBSTITUTE_SYM_BV_SOME(somety, origty) \
instance SubstituteSym somety where \
substituteSym sym v (somety (origty t)) = somety $ origty $ substTerm sym (underlyingTerm v) t
#if 1
SUBSTITUTE_SYM_SIMPLE(SymBool)
SUBSTITUTE_SYM_SIMPLE(SymInteger)
SUBSTITUTE_SYM_BV(SymIntN)
SUBSTITUTE_SYM_BV(SymWordN)
SUBSTITUTE_SYM_FUN(=~>, SymTabularFun)
SUBSTITUTE_SYM_FUN(-~>, SymGeneralFun)
SUBSTITUTE_SYM_BV_SOME(SomeSymIntN, SymIntN)
SUBSTITUTE_SYM_BV_SOME(SomeSymWordN, SymWordN)
#endif
#define BVCONCAT_SIZED(symtype) \
sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => symtype l -> symtype r -> symtype (l + r); \
sizedBVConcat (symtype l) (symtype r) = \
case (leqAddPos pl pr, knownAdd (KnownProof @l) (KnownProof @r)) of \
(LeqProof, KnownProof) -> \
symtype (pevalBVConcatTerm l r); \
where; \
pl = Proxy :: Proxy l; \
pr = Proxy :: Proxy r
#define BVZEXT_SIZED(symtype) \
sizedBVZext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> symtype l -> symtype r; \
sizedBVZext _ (symtype v) = \
case leqTrans (LeqProof @1 @l) (LeqProof @l @r) of \
LeqProof -> symtype $ pevalBVExtendTerm False (Proxy @r) v
#define BVSEXT_SIZED(symtype) \
sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> symtype l -> symtype r; \
sizedBVSext _ (symtype v) = \
case leqTrans (LeqProof @1 @l) (LeqProof @l @r) of \
LeqProof -> symtype $ pevalBVExtendTerm True (Proxy @r) v
#define BVSELECT_SIZED(symtype) \
sizedBVSelect :: forall n ix w p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) => \
p ix -> q w -> symtype n -> symtype w; \
sizedBVSelect pix pw (symtype v) = symtype $ pevalBVSelectTerm pix pw v
#if 1
instance SizedBV SymIntN where
BVCONCAT_SIZED(SymIntN)
BVZEXT_SIZED(SymIntN)
BVSEXT_SIZED(SymIntN)
sizedBVExt :: forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> SymIntN l -> SymIntN r
sizedBVExt = forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
(proxy :: Natural -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext
BVSELECT_SIZED(SymIntN)
instance SizedBV SymWordN where
BVCONCAT_SIZED(SymWordN)
BVZEXT_SIZED(SymWordN)
BVSEXT_SIZED(SymWordN)
sizedBVExt :: forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> SymWordN l -> SymWordN r
sizedBVExt = forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
(proxy :: Natural -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext
BVSELECT_SIZED(SymWordN)
#endif
#define BVCONCAT(somety, origty) \
bvConcat (somety (a :: origty l)) (somety (b :: origty r)) = \
case (leqAddPos (Proxy @l) (Proxy @r), knownAdd @l @r KnownProof KnownProof) of \
(LeqProof, KnownProof) -> \
somety $ sizedBVConcat a b
#define BVZEXT(somety, origty) \
bvZext l (somety (a :: origty n)) \
| l < n = error "bvZext: trying to zero extend a value to a smaller size" \
| otherwise = res (Proxy @n) \
where \
n = fromIntegral $ natVal (Proxy @n); \
res :: forall (l :: Nat). Proxy l -> somety; \
res p = \
case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
(KnownProof, LeqProof, LeqProof) -> somety $ sizedBVZext p a
#define BVSEXT(somety, origty) \
bvSext l (somety (a :: origty n)) \
| l < n = error "bvZext: trying to zero extend a value to a smaller size" \
| otherwise = res (Proxy @n) \
where \
n = fromIntegral $ natVal (Proxy @n); \
res :: forall (l :: Nat). Proxy l -> somety; \
res p = \
case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
(KnownProof, LeqProof, LeqProof) -> somety $ sizedBVSext p a
#define BVSELECT(somety, origty) \
bvSelect ix w (somety (a :: origty n)) \
| ix + w > n = error "bvSelect: trying to select a bitvector outside the bounds of the input" \
| w == 0 = error "bvSelect: trying to select a bitvector of size 0" \
| otherwise = res (Proxy @n) (Proxy @n) \
where \
n = fromIntegral $ natVal (Proxy @n); \
res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> somety; \
res _ _ = \
case ( unsafeKnownProof @ix (fromIntegral ix), \
unsafeKnownProof @w (fromIntegral w), \
unsafeLeqProof @1 @w, \
unsafeLeqProof @(ix + w) @n \
) of \
(KnownProof, KnownProof, LeqProof, LeqProof) -> \
somety $ sizedBVSelect (Proxy @ix) (Proxy @w) a
#if 1
instance BV SomeSymIntN where
bvConcat :: SomeSymIntN -> SomeSymIntN -> SomeSymIntN
BVCONCAT(SomeSymIntN, SymIntN)
{-# INLINE bvConcat #-}
bvZext :: Int -> SomeSymIntN -> SomeSymIntN
BVZEXT(SomeSymIntN, SymIntN)
{-# INLINE bvZext #-}
bvSext :: Int -> SomeSymIntN -> SomeSymIntN
BVSEXT(SomeSymIntN, SymIntN)
{-# INLINE bvSext #-}
bvExt :: Int -> SomeSymIntN -> SomeSymIntN
bvExt = forall bv. BV bv => Int -> bv -> bv
bvSext
{-# INLINE bvExt #-}
bvSelect :: Int -> Int -> SomeSymIntN -> SomeSymIntN
BVSELECT(SomeSymIntN, SymIntN)
{-# INLINE bvSelect #-}
instance BV SomeSymWordN where
bvConcat :: SomeSymWordN -> SomeSymWordN -> SomeSymWordN
BVCONCAT(SomeSymWordN, SymWordN)
{-# INLINE bvConcat #-}
bvZext :: Int -> SomeSymWordN -> SomeSymWordN
BVZEXT(SomeSymWordN, SymWordN)
{-# INLINE bvZext #-}
bvSext :: Int -> SomeSymWordN -> SomeSymWordN
BVSEXT(SomeSymWordN, SymWordN)
{-# INLINE bvSext #-}
bvExt :: Int -> SomeSymWordN -> SomeSymWordN
bvExt = forall bv. BV bv => Int -> bv -> bv
bvZext
{-# INLINE bvExt #-}
bvSelect :: Int -> Int -> SomeSymWordN -> SomeSymWordN
BVSELECT(SomeSymWordN, SymWordN)
{-# INLINE bvSelect #-}
#endif
instance (KnownNat n, 1 <= n) => BVSignConversion (SymWordN n) (SymIntN n) where
toSigned :: SymWordN n -> SymIntN n
toSigned (SymWordN Term (WordN n)
n) = forall (n :: Natural). Term (IntN n) -> SymIntN n
SymIntN forall a b. (a -> b) -> a -> b
$ forall (ubv :: Natural -> *) (sbv :: Natural -> *) (n :: Natural).
(forall (n1 :: Natural).
(KnownNat n1, 1 <= n1) =>
SupportedPrim (ubv n1),
forall (n1 :: Natural).
(KnownNat n1, 1 <= n1) =>
SupportedPrim (sbv n1),
Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
BVSignConversion (ubv n) (sbv n)) =>
Term (ubv n) -> Term (sbv n)
pevalBVToSignedTerm Term (WordN n)
n
toUnsigned :: SymIntN n -> SymWordN n
toUnsigned (SymIntN Term (IntN n)
n) = forall (n :: Natural). Term (WordN n) -> SymWordN n
SymWordN forall a b. (a -> b) -> a -> b
$ forall (ubv :: Natural -> *) (sbv :: Natural -> *) (n :: Natural).
(forall (n1 :: Natural).
(KnownNat n1, 1 <= n1) =>
SupportedPrim (ubv n1),
forall (n1 :: Natural).
(KnownNat n1, 1 <= n1) =>
SupportedPrim (sbv n1),
Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
BVSignConversion (ubv n) (sbv n)) =>
Term (sbv n) -> Term (ubv n)
pevalBVToUnsignedTerm Term (IntN n)
n
instance BVSignConversion SomeSymWordN SomeSymIntN where
toSigned :: SomeSymWordN -> SomeSymIntN
toSigned (SomeSymWordN SymWordN n
n) = forall (con :: Natural).
(KnownNat con, 1 <= con) =>
SymIntN con -> SomeSymIntN
SomeSymIntN forall a b. (a -> b) -> a -> b
$ forall ubv sbv. BVSignConversion ubv sbv => ubv -> sbv
toSigned SymWordN n
n
toUnsigned :: SomeSymIntN -> SomeSymWordN
toUnsigned (SomeSymIntN SymIntN n
n) = forall (con :: Natural).
(KnownNat con, 1 <= con) =>
SymWordN con -> SomeSymWordN
SomeSymWordN forall a b. (a -> b) -> a -> b
$ forall ubv sbv. BVSignConversion ubv sbv => sbv -> ubv
toUnsigned SymIntN n
n
data ModelSymPair ct st where
(:=) :: (LinkedRep ct st) => st -> ct -> ModelSymPair ct st
instance ModelRep (ModelSymPair ct st) Model where
buildModel :: ModelSymPair ct st -> Model
buildModel (st
sym := ct
val) =
case forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm st
sym of
SymTerm Int
_ TypedSymbol ct
symbol -> forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol ct
symbol ct
val forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
Term ct
_ -> forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"
symsSize :: forall con sym. (LinkedRep con sym) => [sym] -> Int
symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int
symsSize = forall a. [Term a] -> Int
termsSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm @con)
{-# INLINE symsSize #-}
symSize :: forall con sym. (LinkedRep con sym) => sym -> Int
symSize :: forall con sym. LinkedRep con sym => sym -> Int
symSize = forall a. Term a -> Int
termSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm @con
{-# INLINE symSize #-}
data SomeSym where
SomeSym :: (LinkedRep con sym) => sym -> SomeSym
someUnderlyingTerm :: SomeSym -> SomeTerm
someUnderlyingTerm :: SomeSym -> SomeTerm
someUnderlyingTerm (SomeSym sym
s) = forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sym
s
someSymsSize :: [SomeSym] -> Int
someSymsSize :: [SomeSym] -> Int
someSymsSize = [SomeTerm] -> Int
someTermsSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SomeSym -> SomeTerm
someUnderlyingTerm
{-# INLINE someSymsSize #-}
class AllSyms a where
allSymsS :: a -> [SomeSym] -> [SomeSym]
allSymsS a
a [SomeSym]
l = forall a. AllSyms a => a -> [SomeSym]
allSyms a
a forall a. [a] -> [a] -> [a]
++ [SomeSym]
l
allSyms :: a -> [SomeSym]
allSyms a
a = forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS a
a []
{-# MINIMAL allSymsS | allSyms #-}
allSymsSize :: (AllSyms a) => a -> Int
allSymsSize :: forall a. AllSyms a => a -> Int
allSymsSize = [SomeSym] -> Int
someSymsSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AllSyms a => a -> [SomeSym]
allSyms
class AllSyms' a where
allSymsS' :: a c -> [SomeSym] -> [SomeSym]
instance (Generic a, AllSyms' (Rep a)) => AllSyms (Default a) where
allSymsS :: Default a -> [SomeSym] -> [SomeSym]
allSymsS = forall (a :: * -> *) c. AllSyms' a => a c -> [SomeSym] -> [SomeSym]
allSymsS' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. Generic a => a -> Rep a x
from forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Default a -> a
unDefault
instance AllSyms' U1 where
allSymsS' :: forall c. U1 c -> [SomeSym] -> [SomeSym]
allSymsS' U1 c
_ = forall a. a -> a
id
instance (AllSyms c) => AllSyms' (K1 i c) where
allSymsS' :: forall c. K1 i c c -> [SomeSym] -> [SomeSym]
allSymsS' (K1 c
v) = forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS c
v
instance (AllSyms' a) => AllSyms' (M1 i c a) where
allSymsS' :: forall c. M1 i c a c -> [SomeSym] -> [SomeSym]
allSymsS' (M1 a c
v) = forall (a :: * -> *) c. AllSyms' a => a c -> [SomeSym] -> [SomeSym]
allSymsS' a c
v
instance (AllSyms' a, AllSyms' b) => AllSyms' (a :+: b) where
allSymsS' :: forall c. (:+:) a b c -> [SomeSym] -> [SomeSym]
allSymsS' (L1 a c
l) = forall (a :: * -> *) c. AllSyms' a => a c -> [SomeSym] -> [SomeSym]
allSymsS' a c
l
allSymsS' (R1 b c
r) = forall (a :: * -> *) c. AllSyms' a => a c -> [SomeSym] -> [SomeSym]
allSymsS' b c
r
instance (AllSyms' a, AllSyms' b) => AllSyms' (a :*: b) where
allSymsS' :: forall c. (:*:) a b c -> [SomeSym] -> [SomeSym]
allSymsS' (a c
a :*: b c
b) = forall (a :: * -> *) c. AllSyms' a => a c -> [SomeSym] -> [SomeSym]
allSymsS' a c
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> *) c. AllSyms' a => a c -> [SomeSym] -> [SomeSym]
allSymsS' b c
b
#define CONCRETE_ALLSYMS(type) \
instance AllSyms type where \
allSymsS _ = id
#define ALLSYMS_SIMPLE(t) \
instance AllSyms t where \
allSymsS v = (SomeSym v :)
#define ALLSYMS_BV(t) \
instance (KnownNat n, 1 <= n) => AllSyms (t n) where \
allSymsS v = (SomeSym v :)
#define ALLSYMS_SOME_BV(t) \
instance AllSyms t where \
allSymsS (t v) = (SomeSym v :)
#define ALLSYMS_FUN(op) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => AllSyms (sa op sb) where \
allSymsS v = (SomeSym v :)
#if 1
CONCRETE_ALLSYMS(Bool)
CONCRETE_ALLSYMS(Integer)
CONCRETE_ALLSYMS(Char)
CONCRETE_ALLSYMS(Int)
CONCRETE_ALLSYMS(Int8)
CONCRETE_ALLSYMS(Int16)
CONCRETE_ALLSYMS(Int32)
CONCRETE_ALLSYMS(Int64)
CONCRETE_ALLSYMS(Word)
CONCRETE_ALLSYMS(Word8)
CONCRETE_ALLSYMS(Word16)
CONCRETE_ALLSYMS(Word32)
CONCRETE_ALLSYMS(Word64)
CONCRETE_ALLSYMS(B.ByteString)
CONCRETE_ALLSYMS(T.Text)
ALLSYMS_SIMPLE(SymBool)
ALLSYMS_SIMPLE(SymInteger)
ALLSYMS_BV(SymIntN)
ALLSYMS_BV(SymWordN)
ALLSYMS_SOME_BV(SomeSymIntN)
ALLSYMS_SOME_BV(SomeSymWordN)
ALLSYMS_FUN(=~>)
ALLSYMS_FUN(-~>)
#endif
instance AllSyms () where
allSymsS :: () -> [SomeSym] -> [SomeSym]
allSymsS ()
_ = forall a. a -> a
id
deriving via
(Default (Either a b))
instance
( AllSyms a,
AllSyms b
) =>
AllSyms (Either a b)
deriving via (Default (Maybe a)) instance (AllSyms a) => AllSyms (Maybe a)
deriving via (Default [a]) instance (AllSyms a) => AllSyms [a]
deriving via
(Default (a, b))
instance
(AllSyms a, AllSyms b) =>
AllSyms (a, b)
deriving via
(Default (a, b, c))
instance
( AllSyms a,
AllSyms b,
AllSyms c
) =>
AllSyms (a, b, c)
deriving via
(Default (a, b, c, d))
instance
( AllSyms a,
AllSyms b,
AllSyms c,
AllSyms d
) =>
AllSyms (a, b, c, d)
deriving via
(Default (a, b, c, d, e))
instance
( AllSyms a,
AllSyms b,
AllSyms c,
AllSyms d,
AllSyms e
) =>
AllSyms (a, b, c, d, e)
deriving via
(Default (a, b, c, d, e, f))
instance
( AllSyms a,
AllSyms b,
AllSyms c,
AllSyms d,
AllSyms e,
AllSyms f
) =>
AllSyms (a, b, c, d, e, f)
deriving via
(Default (a, b, c, d, e, f, g))
instance
( AllSyms a,
AllSyms b,
AllSyms c,
AllSyms d,
AllSyms e,
AllSyms f,
AllSyms g
) =>
AllSyms (a, b, c, d, e, f, g)
deriving via
(Default (a, b, c, d, e, f, g, h))
instance
( AllSyms a,
AllSyms b,
AllSyms c,
AllSyms d,
AllSyms e,
AllSyms f,
AllSyms g,
AllSyms h
) =>
AllSyms ((,,,,,,,) a b c d e f g h)
instance
(AllSyms (m (Maybe a))) =>
AllSyms (MaybeT m a)
where
allSymsS :: MaybeT m a -> [SomeSym] -> [SomeSym]
allSymsS (MaybeT m (Maybe a)
v) = forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS m (Maybe a)
v
instance
(AllSyms (m (Either e a))) =>
AllSyms (ExceptT e m a)
where
allSymsS :: ExceptT e m a -> [SomeSym] -> [SomeSym]
allSymsS (ExceptT m (Either e a)
v) = forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS m (Either e a)
v
deriving via
(Default (Sum f g a))
instance
(AllSyms (f a), AllSyms (g a)) =>
AllSyms (Sum f g a)
instance
(AllSyms (m (a, s))) =>
AllSyms (WriterLazy.WriterT s m a)
where
allSymsS :: WriterT s m a -> [SomeSym] -> [SomeSym]
allSymsS (WriterLazy.WriterT m (a, s)
v) = forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS m (a, s)
v
instance
(AllSyms (m (a, s))) =>
AllSyms (WriterStrict.WriterT s m a)
where
allSymsS :: WriterT s m a -> [SomeSym] -> [SomeSym]
allSymsS (WriterStrict.WriterT m (a, s)
v) = forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS m (a, s)
v
instance (AllSyms a) => AllSyms (Identity a) where
allSymsS :: Identity a -> [SomeSym] -> [SomeSym]
allSymsS (Identity a
a) = forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS a
a
instance (AllSyms (m a)) => AllSyms (IdentityT m a) where
allSymsS :: IdentityT m a -> [SomeSym] -> [SomeSym]
allSymsS (IdentityT m a
a) = forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS m a
a
deriving via (Default VerificationConditions) instance AllSyms VerificationConditions
deriving via (Default AssertionError) instance AllSyms AssertionError