{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.IR.SymPrim.Data.SymPrim
( Sym (..),
SymBool,
SymInteger,
(-->),
type (=~>),
type (-~>),
SymWordN,
SymIntN,
symSize,
symsSize,
ModelSymPair (..),
)
where
import Control.DeepSeq
import Control.Monad.Except
import Data.Bits
import Data.Hashable
import Data.Int
import Data.Proxy
import Data.String
import Data.Word
import GHC.Generics
import GHC.TypeLits
import Grisette.Core.Data.Class.BitVector
import Grisette.Core.Data.Class.Bool
import Grisette.Core.Data.Class.Error
import Grisette.Core.Data.Class.Evaluate
import Grisette.Core.Data.Class.ExtractSymbolics
import Grisette.Core.Data.Class.Function
import Grisette.Core.Data.Class.GenSym
import Grisette.Core.Data.Class.Integer
import Grisette.Core.Data.Class.Mergeable
import Grisette.Core.Data.Class.ModelOps
import Grisette.Core.Data.Class.SOrd
import Grisette.Core.Data.Class.SimpleMergeable
import Grisette.Core.Data.Class.Solvable
import Grisette.Core.Data.Class.Substitute
import Grisette.Core.Data.Class.ToCon
import Grisette.Core.Data.Class.ToSym
import Grisette.IR.SymPrim.Data.BV
import Grisette.IR.SymPrim.Data.IntBitwidth
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
import Grisette.IR.SymPrim.Data.Prim.Model
import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integer
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
import Grisette.IR.SymPrim.Data.TabularFun
import Grisette.Lib.Control.Monad
import Language.Haskell.TH.Syntax
newtype Sym a = Sym {forall a. Sym a -> Term a
underlyingTerm :: Term a} deriving (forall a (m :: * -> *). Quote m => Sym a -> m Exp
forall a (m :: * -> *). Quote m => Sym a -> Code m (Sym a)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => Sym a -> m Exp
forall (m :: * -> *). Quote m => Sym a -> Code m (Sym a)
liftTyped :: forall (m :: * -> *). Quote m => Sym a -> Code m (Sym a)
$cliftTyped :: forall a (m :: * -> *). Quote m => Sym a -> Code m (Sym a)
lift :: forall (m :: * -> *). Quote m => Sym a -> m Exp
$clift :: forall a (m :: * -> *). Quote m => Sym a -> m Exp
Lift, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Sym a) x -> Sym a
forall a x. Sym a -> Rep (Sym a) x
$cto :: forall a x. Rep (Sym a) x -> Sym a
$cfrom :: forall a x. Sym a -> Rep (Sym a) x
Generic)
instance NFData (Sym a) where
rnf :: Sym a -> ()
rnf (Sym Term a
t) = forall a. NFData a => a -> ()
rnf Term a
t
instance (SupportedPrim a) => Solvable a (Sym a) where
con :: a -> Sym a
con = forall a. Term a -> Sym a
Sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm
ssym :: String -> Sym a
ssym = forall a. Term a -> Sym a
Sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. (SupportedPrim t, Typeable t) => String -> Term t
ssymTerm
isym :: String -> Int -> Sym a
isym String
str Int
i = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t. (SupportedPrim t, Typeable t) => String -> Int -> Term t
isymTerm String
str Int
i
sinfosym :: forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
String -> a -> Sym a
sinfosym String
str a
info = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t a.
(SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a,
Show a, Hashable a) =>
String -> a -> Term t
sinfosymTerm String
str a
info
iinfosym :: forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
String -> Int -> a -> Sym a
iinfosym String
str Int
i a
info = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t a.
(SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a,
Show a, Hashable a) =>
String -> Int -> a -> Term t
iinfosymTerm String
str Int
i a
info
conView :: Sym a -> Maybe a
conView (Sym (ConTerm Int
_ a
t)) = forall a. a -> Maybe a
Just a
t
conView Sym a
_ = forall a. Maybe a
Nothing
instance (SupportedPrim t) => IsString (Sym t) where
fromString :: String -> Sym t
fromString = forall c t. Solvable c t => String -> t
ssym
instance (SupportedPrim a) => ToSym (Sym a) (Sym a) where
toSym :: Sym a -> Sym a
toSym = forall a. a -> a
id
instance (SupportedPrim a) => ToSym a (Sym a) where
toSym :: a -> Sym a
toSym = forall c t. Solvable c t => c -> t
con
instance (SupportedPrim a) => ToCon (Sym a) (Sym a) where
toCon :: Sym a -> Maybe (Sym a)
toCon = forall a. a -> Maybe a
Just
instance (SupportedPrim a) => ToCon (Sym a) a where
toCon :: Sym a -> Maybe a
toCon = forall c t. Solvable c t => t -> Maybe c
conView
instance (SupportedPrim a) => EvaluateSym (Sym a) where
evaluateSym :: Bool -> Model -> Sym a -> Sym a
evaluateSym Bool
fillDefault Model
model (Sym Term a
t) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall a. SupportedPrim a => Bool -> Model -> Term a -> Term a
evaluateTerm Bool
fillDefault Model
model Term a
t
instance (SupportedPrim a) => ExtractSymbolics (Sym a) where
extractSymbolics :: Sym a -> SymbolSet
extractSymbolics (Sym Term a
t) = HashSet SomeTypedSymbol -> SymbolSet
SymbolSet forall a b. (a -> b) -> a -> b
$ forall a. SupportedPrim a => Term a -> HashSet SomeTypedSymbol
extractSymbolicsTerm Term a
t
instance (SupportedPrim a) => Show (Sym a) where
show :: Sym a -> String
show (Sym Term a
t) = forall t. SupportedPrim t => Term t -> String
pformat Term a
t
instance (SupportedPrim a) => Hashable (Sym a) where
hashWithSalt :: Int -> Sym a -> Int
hashWithSalt Int
s (Sym Term a
v) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term a
v
instance (SupportedPrim a) => Eq (Sym a) where
(Sym Term a
l) == :: Sym a -> Sym a -> Bool
== (Sym Term a
r) = Term a
l forall a. Eq a => a -> a -> Bool
== Term a
r
#define SEQ_SYM(type) \
instance (SupportedPrim type) => SEq (Sym type) where \
(Sym l) ==~ (Sym r) = Sym $ pevalEqvTerm l r
#define SORD_SYM(type) \
instance (SupportedPrim type) => SOrd (Sym type) where \
(Sym a) <=~ (Sym b) = Sym $ withPrim (Proxy @type) $ pevalLeNumTerm a b; \
(Sym a) <~ (Sym b) = Sym $ withPrim (Proxy @type) $ pevalLtNumTerm a b; \
(Sym a) >=~ (Sym b) = Sym $ withPrim (Proxy @type) $ pevalGeNumTerm a b; \
(Sym a) >~ (Sym b) = Sym $ withPrim (Proxy @type) $ pevalGtNumTerm a b; \
a `symCompare` b = \
withPrim (Proxy @type) $ mrgIf \
(a <~ b) \
(mrgReturn LT) \
(mrgIf (a ==~ b) (mrgReturn EQ) (mrgReturn GT))
#if 1
SEQ_SYM(Bool)
SEQ_SYM(Integer)
SEQ_SYM((IntN n))
SEQ_SYM((WordN n))
SORD_SYM(Integer)
SORD_SYM((IntN n))
SORD_SYM((WordN n))
#endif
type SymBool = Sym Bool
instance SOrd (Sym Bool) where
Sym Bool
l <=~ :: Sym Bool -> Sym Bool -> Sym Bool
<=~ Sym Bool
r = forall b. LogicalOp b => b -> b
nots Sym Bool
l forall b. LogicalOp b => b -> b -> b
||~ Sym Bool
r
Sym Bool
l <~ :: Sym Bool -> Sym Bool -> Sym Bool
<~ Sym Bool
r = forall b. LogicalOp b => b -> b
nots Sym Bool
l forall b. LogicalOp b => b -> b -> b
&&~ Sym Bool
r
Sym Bool
l >=~ :: Sym Bool -> Sym Bool -> Sym Bool
>=~ Sym Bool
r = Sym Bool
l forall b. LogicalOp b => b -> b -> b
||~ forall b. LogicalOp b => b -> b
nots Sym Bool
r
Sym Bool
l >~ :: Sym Bool -> Sym Bool -> Sym Bool
>~ Sym Bool
r = Sym Bool
l forall b. LogicalOp b => b -> b -> b
&&~ forall b. LogicalOp b => b -> b
nots Sym Bool
r
symCompare :: Sym Bool -> Sym Bool -> UnionM Ordering
symCompare Sym Bool
l Sym Bool
r =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
Sym Bool -> u a -> u a -> u a
mrgIf
(forall b. LogicalOp b => b -> b
nots Sym Bool
l forall b. LogicalOp b => b -> b -> b
&&~ Sym Bool
r)
(forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn Ordering
LT)
(forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
Sym Bool -> u a -> u a -> u a
mrgIf (Sym Bool
l forall a. SEq a => a -> a -> Sym Bool
==~ Sym Bool
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))
instance SymBoolOp (Sym Bool)
type SymInteger = Sym Integer
instance Num (Sym Integer) where
(Sym Term Integer
l) + :: Sym Integer -> Sym Integer -> Sym Integer
+ (Sym Term Integer
r) = forall a. Term a -> Sym a
Sym 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
(Sym Term Integer
l) - :: Sym Integer -> Sym Integer -> Sym Integer
- (Sym Term Integer
r) = forall a. Term a -> Sym a
Sym 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
(Sym Term Integer
l) * :: Sym Integer -> Sym Integer -> Sym Integer
* (Sym Term Integer
r) = forall a. Term a -> Sym a
Sym 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 :: Sym Integer -> Sym Integer
negate (Sym Term Integer
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term Integer
v
abs :: Sym Integer -> Sym Integer
abs (Sym Term Integer
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm Term Integer
v
signum :: Sym Integer -> Sym Integer
signum (Sym Term Integer
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm Term Integer
v
fromInteger :: Integer -> Sym Integer
fromInteger = forall c t. Solvable c t => c -> t
con
instance SignedDivMod (Sym Integer) where
divs :: forall e (uf :: * -> *).
(MonadError e uf, MonadUnion uf,
TransformError ArithException e) =>
Sym Integer -> Sym Integer -> uf (Sym Integer)
divs (Sym Term Integer
l) rs :: Sym Integer
rs@(Sym Term Integer
r) =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
Sym Bool -> u a -> u a -> u a
mrgIf
(Sym Integer
rs forall a. SEq a => a -> a -> Sym Bool
==~ forall c t. Solvable c t => c -> t
con Integer
0)
(forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall from to. TransformError from to => from -> to
transformError ArithException
DivideByZero)
(forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn forall a b. (a -> b) -> a -> b
$ forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
pevalDivIntegerTerm Term Integer
l Term Integer
r)
mods :: forall e (uf :: * -> *).
(MonadError e uf, MonadUnion uf,
TransformError ArithException e) =>
Sym Integer -> Sym Integer -> uf (Sym Integer)
mods (Sym Term Integer
l) rs :: Sym Integer
rs@(Sym Term Integer
r) =
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
Sym Bool -> u a -> u a -> u a
mrgIf
(Sym Integer
rs forall a. SEq a => a -> a -> Sym Bool
==~ forall c t. Solvable c t => c -> t
con Integer
0)
(forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall from to. TransformError from to => from -> to
transformError ArithException
DivideByZero)
(forall (u :: * -> *) a. (MonadUnion u, Mergeable a) => a -> u a
mrgReturn forall a b. (a -> b) -> a -> b
$ forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
pevalModIntegerTerm Term Integer
l Term Integer
r)
instance SymIntegerOp (Sym Integer)
type SymIntN n = Sym (IntN n)
instance (SupportedPrim (IntN n)) => Num (Sym (IntN n)) where
(Sym Term (IntN n)
l) + :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)
+ (Sym Term (IntN n)
r) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term (IntN n)
l Term (IntN n)
r
(Sym Term (IntN n)
l) - :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)
- (Sym Term (IntN n)
r) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm Term (IntN n)
l Term (IntN n)
r
(Sym Term (IntN n)
l) * :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)
* (Sym Term (IntN n)
r) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term (IntN n)
l Term (IntN n)
r
negate :: Sym (IntN n) -> Sym (IntN n)
negate (Sym Term (IntN n)
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term (IntN n)
v
abs :: Sym (IntN n) -> Sym (IntN n)
abs (Sym Term (IntN n)
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm Term (IntN n)
v
signum :: Sym (IntN n) -> Sym (IntN n)
signum (Sym Term (IntN n)
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm Term (IntN n)
v
fromInteger :: Integer -> Sym (IntN n)
fromInteger Integer
i = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall c t. Solvable c t => c -> t
con forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
i
instance (SupportedPrim (IntN n)) => Bits (Sym (IntN n)) where
Sym Term (IntN n)
l .&. :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)
.&. Sym Term (IntN n)
r = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAndBitsTerm Term (IntN n)
l Term (IntN n)
r
Sym Term (IntN n)
l .|. :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)
.|. Sym Term (IntN n)
r = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalOrBitsTerm Term (IntN n)
l Term (IntN n)
r
Sym Term (IntN n)
l xor :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)
`xor` Sym Term (IntN n)
r = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm Term (IntN n)
l Term (IntN n)
r
complement :: Sym (IntN n) -> Sym (IntN n)
complement (Sym Term (IntN n)
n) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm Term (IntN n)
n
shift :: Sym (IntN n) -> Int -> Sym (IntN n)
shift (Sym Term (IntN n)
n) Int
i = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
pevalShiftBitsTerm Term (IntN n)
n Int
i
rotate :: Sym (IntN n) -> Int -> Sym (IntN n)
rotate (Sym Term (IntN n)
n) Int
i = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
pevalRotateBitsTerm Term (IntN n)
n Int
i
bitSize :: Sym (IntN n) -> Int
bitSize Sym (IntN n)
_ = forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
bitSizeMaybe :: Sym (IntN n) -> Maybe Int
bitSizeMaybe Sym (IntN n)
_ = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
isSigned :: Sym (IntN n) -> Bool
isSigned Sym (IntN n)
_ = Bool
True
testBit :: Sym (IntN n) -> Int -> Bool
testBit (Con IntN n
n) = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int -> Bool
testBit IntN n
n
testBit Sym (IntN n)
_ = forall a. HasCallStack => String -> a
error String
"You cannot call testBit on symbolic variables"
bit :: Int -> Sym (IntN n)
bit = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall c t. Solvable c t => c -> t
con forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bits a => Int -> a
bit
popCount :: Sym (IntN n) -> Int
popCount (Con IntN n
n) = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(IntN n)) forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int
popCount IntN n
n
popCount Sym (IntN n)
_ = forall a. HasCallStack => String -> a
error String
"You cannot call popCount on symbolic variables"
instance
(KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') =>
BVConcat (Sym (IntN n)) (Sym (IntN w)) (Sym (IntN w'))
where
bvconcat :: Sym (IntN n) -> Sym (IntN w) -> Sym (IntN w')
bvconcat (Sym Term (IntN n)
l) (Sym Term (IntN w)
r) = forall a. Term a -> Sym a
Sym (forall (s :: Nat -> *) (w :: Nat) (w' :: Nat) (w'' :: Nat).
(SupportedPrim (s w), SupportedPrim (s w'), SupportedPrim (s w''),
KnownNat w, KnownNat w', KnownNat w'',
BVConcat (s w) (s w') (s w'')) =>
Term (s w) -> Term (s w') -> Term (s w'')
pevalBVConcatTerm Term (IntN n)
l Term (IntN w)
r)
instance
( KnownNat w,
KnownNat w',
1 <= w,
1 <= w',
w <= w',
w + 1 <= w',
1 <= w' - w,
KnownNat (w' - w)
) =>
BVExtend (Sym (IntN w)) w' (Sym (IntN w'))
where
bvzeroExtend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (IntN w) -> Sym (IntN w')
bvzeroExtend proxy w'
_ (Sym Term (IntN w)
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
(bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
SupportedPrim (bv a), SupportedPrim (bv b)) =>
Bool -> proxy n -> Term (bv a) -> Term (bv b)
pevalBVExtendTerm Bool
False (forall {k} (t :: k). Proxy t
Proxy @w') Term (IntN w)
v
bvsignExtend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (IntN w) -> Sym (IntN w')
bvsignExtend proxy w'
_ (Sym Term (IntN w)
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
(bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
SupportedPrim (bv a), SupportedPrim (bv b)) =>
Bool -> proxy n -> Term (bv a) -> Term (bv b)
pevalBVExtendTerm Bool
True (forall {k} (t :: k). Proxy t
Proxy @w') Term (IntN w)
v
bvextend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (IntN w) -> Sym (IntN w')
bvextend = forall bv1 (n :: Nat) bv2 (proxy :: Nat -> *).
BVExtend bv1 n bv2 =>
proxy n -> bv1 -> bv2
bvsignExtend
instance
( KnownNat ix,
KnownNat w,
KnownNat ow,
ix + w <= ow,
1 <= ow,
1 <= w
) =>
BVSelect (Sym (IntN ow)) ix w (Sym (IntN w))
where
bvselect :: forall (proxy :: Nat -> *).
proxy ix -> proxy w -> Sym (IntN ow) -> Sym (IntN w)
bvselect proxy ix
pix proxy w
pw (Sym Term (IntN ow)
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall (bv :: Nat -> *) (a :: Nat) (ix :: Nat) (w :: Nat)
(proxy :: Nat -> *).
(SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a,
KnownNat w, KnownNat ix, BVSelect (bv a) ix w (bv w)) =>
proxy ix -> proxy w -> Term (bv a) -> Term (bv w)
pevalBVSelectTerm proxy ix
pix proxy w
pw Term (IntN ow)
v
#define TOSYM_MACHINE_INTEGER(int, bv) \
instance ToSym int (Sym (bv)) where \
toSym = fromIntegral
#define TOCON_MACHINE_INTEGER(bvw, n, int) \
instance ToCon (Sym (bvw n)) int where \
toCon (Con (bvw v :: bvw n)) = Just $ fromIntegral v; \
toCon _ = Nothing
#if 1
TOSYM_MACHINE_INTEGER(Int8, IntN 8)
TOSYM_MACHINE_INTEGER(Int16, IntN 16)
TOSYM_MACHINE_INTEGER(Int32, IntN 32)
TOSYM_MACHINE_INTEGER(Int64, IntN 64)
TOSYM_MACHINE_INTEGER(Word8, WordN 8)
TOSYM_MACHINE_INTEGER(Word16, WordN 16)
TOSYM_MACHINE_INTEGER(Word32, WordN 32)
TOSYM_MACHINE_INTEGER(Word64, WordN 64)
TOSYM_MACHINE_INTEGER(Int, IntN $intBitwidthQ)
TOSYM_MACHINE_INTEGER(Word, WordN $intBitwidthQ)
TOCON_MACHINE_INTEGER(IntN, 8, Int8)
TOCON_MACHINE_INTEGER(IntN, 16, Int16)
TOCON_MACHINE_INTEGER(IntN, 32, Int32)
TOCON_MACHINE_INTEGER(IntN, 64, Int64)
TOCON_MACHINE_INTEGER(WordN, 8, Word8)
TOCON_MACHINE_INTEGER(WordN, 16, Word16)
TOCON_MACHINE_INTEGER(WordN, 32, Word32)
TOCON_MACHINE_INTEGER(WordN, 64, Word64)
TOCON_MACHINE_INTEGER(IntN, $intBitwidthQ, Int)
TOCON_MACHINE_INTEGER(WordN, $intBitwidthQ, Word)
#endif
type SymWordN n = Sym (WordN n)
instance (SupportedPrim (WordN n)) => Num (Sym (WordN n)) where
(Sym Term (WordN n)
l) + :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)
+ (Sym Term (WordN n)
r) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term (WordN n)
l Term (WordN n)
r
(Sym Term (WordN n)
l) - :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)
- (Sym Term (WordN n)
r) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm Term (WordN n)
l Term (WordN n)
r
(Sym Term (WordN n)
l) * :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)
* (Sym Term (WordN n)
r) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term (WordN n)
l Term (WordN n)
r
negate :: Sym (WordN n) -> Sym (WordN n)
negate (Sym Term (WordN n)
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term (WordN n)
v
abs :: Sym (WordN n) -> Sym (WordN n)
abs (Sym Term (WordN n)
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm Term (WordN n)
v
signum :: Sym (WordN n) -> Sym (WordN n)
signum (Sym Term (WordN n)
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm Term (WordN n)
v
fromInteger :: Integer -> Sym (WordN n)
fromInteger Integer
i = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall c t. Solvable c t => c -> t
con forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
i
instance
(KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') =>
BVConcat (Sym (WordN n)) (Sym (WordN w)) (Sym (WordN w'))
where
bvconcat :: Sym (WordN n) -> Sym (WordN w) -> Sym (WordN w')
bvconcat (Sym Term (WordN n)
l) (Sym Term (WordN w)
r) = forall a. Term a -> Sym a
Sym (forall (s :: Nat -> *) (w :: Nat) (w' :: Nat) (w'' :: Nat).
(SupportedPrim (s w), SupportedPrim (s w'), SupportedPrim (s w''),
KnownNat w, KnownNat w', KnownNat w'',
BVConcat (s w) (s w') (s w'')) =>
Term (s w) -> Term (s w') -> Term (s w'')
pevalBVConcatTerm Term (WordN n)
l Term (WordN w)
r)
instance
( KnownNat w,
KnownNat w',
1 <= w,
1 <= w',
w + 1 <= w',
w <= w',
1 <= w' - w,
KnownNat (w' - w)
) =>
BVExtend (Sym (WordN w)) w' (Sym (WordN w'))
where
bvzeroExtend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (WordN w) -> Sym (WordN w')
bvzeroExtend proxy w'
_ (Sym Term (WordN w)
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
(bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
SupportedPrim (bv a), SupportedPrim (bv b)) =>
Bool -> proxy n -> Term (bv a) -> Term (bv b)
pevalBVExtendTerm Bool
False (forall {k} (t :: k). Proxy t
Proxy @w') Term (WordN w)
v
bvsignExtend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (WordN w) -> Sym (WordN w')
bvsignExtend proxy w'
_ (Sym Term (WordN w)
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
(bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
SupportedPrim (bv a), SupportedPrim (bv b)) =>
Bool -> proxy n -> Term (bv a) -> Term (bv b)
pevalBVExtendTerm Bool
True (forall {k} (t :: k). Proxy t
Proxy @w') Term (WordN w)
v
bvextend :: forall (proxy :: Nat -> *).
proxy w' -> Sym (WordN w) -> Sym (WordN w')
bvextend = forall bv1 (n :: Nat) bv2 (proxy :: Nat -> *).
BVExtend bv1 n bv2 =>
proxy n -> bv1 -> bv2
bvzeroExtend
instance
( KnownNat ix,
KnownNat w,
KnownNat ow,
ix + w <= ow,
1 <= ow,
1 <= w
) =>
BVSelect (Sym (WordN ow)) ix w (Sym (WordN w))
where
bvselect :: forall (proxy :: Nat -> *).
proxy ix -> proxy w -> Sym (WordN ow) -> Sym (WordN w)
bvselect proxy ix
pix proxy w
pw (Sym Term (WordN ow)
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall (bv :: Nat -> *) (a :: Nat) (ix :: Nat) (w :: Nat)
(proxy :: Nat -> *).
(SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a,
KnownNat w, KnownNat ix, BVSelect (bv a) ix w (bv w)) =>
proxy ix -> proxy w -> Term (bv a) -> Term (bv w)
pevalBVSelectTerm proxy ix
pix proxy w
pw Term (WordN ow)
v
instance (SupportedPrim (WordN n)) => Bits (Sym (WordN n)) where
Sym Term (WordN n)
l .&. :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)
.&. Sym Term (WordN n)
r = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAndBitsTerm Term (WordN n)
l Term (WordN n)
r
Sym Term (WordN n)
l .|. :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)
.|. Sym Term (WordN n)
r = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalOrBitsTerm Term (WordN n)
l Term (WordN n)
r
Sym Term (WordN n)
l xor :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)
`xor` Sym Term (WordN n)
r = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm Term (WordN n)
l Term (WordN n)
r
complement :: Sym (WordN n) -> Sym (WordN n)
complement (Sym Term (WordN n)
n) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm Term (WordN n)
n
shift :: Sym (WordN n) -> Int -> Sym (WordN n)
shift (Sym Term (WordN n)
n) Int
i = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
pevalShiftBitsTerm Term (WordN n)
n Int
i
rotate :: Sym (WordN n) -> Int -> Sym (WordN n)
rotate (Sym Term (WordN n)
n) Int
i = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
pevalRotateBitsTerm Term (WordN n)
n Int
i
bitSize :: Sym (WordN n) -> Int
bitSize Sym (WordN n)
_ = forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
bitSizeMaybe :: Sym (WordN n) -> Maybe Int
bitSizeMaybe Sym (WordN n)
_ = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
isSigned :: Sym (WordN n) -> Bool
isSigned Sym (WordN n)
_ = Bool
False
testBit :: Sym (WordN n) -> Int -> Bool
testBit (Con WordN n
n) = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int -> Bool
testBit WordN n
n
testBit Sym (WordN n)
_ = forall a. HasCallStack => String -> a
error String
"You cannot call testBit on symbolic variables"
bit :: Int -> Sym (WordN n)
bit = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall c t. Solvable c t => c -> t
con forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bits a => Int -> a
bit
popCount :: Sym (WordN n) -> Int
popCount (Con WordN n
n) = forall t (proxy :: * -> *) a.
SupportedPrim t =>
proxy t -> (PrimConstraint t => a) -> a
withPrim (forall {k} (t :: k). Proxy t
Proxy @(WordN n)) forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int
popCount WordN n
n
popCount Sym (WordN n)
_ = forall a. HasCallStack => String -> a
error String
"You cannot call popCount on symbolic variables"
type a =~> b = Sym (a =-> b)
infixr 0 =~>
instance (SupportedPrim a, SupportedPrim b) => Function (a =~> b) where
type Arg (a =~> b) = Sym a
type Ret (a =~> b) = Sym b
(Sym Term (a =-> b)
f) # :: (a =~> b) -> Arg (a =~> b) -> Ret (a =~> b)
# (Sym Term a
t) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> Term a -> Term b
pevalTabularFunApplyTerm Term (a =-> b)
f Term a
t
type a -~> b = Sym (a --> b)
infixr 0 -~>
instance (SupportedPrim a, SupportedPrim b) => Function (a -~> b) where
type Arg (a -~> b) = Sym a
type Ret (a -~> b) = Sym b
(Sym Term (a --> b)
f) # :: (a -~> b) -> Arg (a -~> b) -> Ret (a -~> b)
# (Sym Term a
t) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm Term (a --> b)
f Term a
t
symsSize :: [Sym a] -> Int
symsSize :: forall a. [Sym a] -> 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 a. Sym a -> Term a
underlyingTerm
symSize :: Sym a -> Int
symSize :: forall a. Sym a -> Int
symSize = forall a. Term a -> Int
termSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Sym a -> Term a
underlyingTerm
data ModelSymPair t = (Sym t) := t deriving (Int -> ModelSymPair t -> ShowS
forall t. SupportedPrim t => Int -> ModelSymPair t -> ShowS
forall t. SupportedPrim t => [ModelSymPair t] -> ShowS
forall t. SupportedPrim t => ModelSymPair t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModelSymPair t] -> ShowS
$cshowList :: forall t. SupportedPrim t => [ModelSymPair t] -> ShowS
show :: ModelSymPair t -> String
$cshow :: forall t. SupportedPrim t => ModelSymPair t -> String
showsPrec :: Int -> ModelSymPair t -> ShowS
$cshowsPrec :: forall t. SupportedPrim t => Int -> ModelSymPair t -> ShowS
Show)
instance ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol where
buildModel :: ModelSymPair t -> Model
buildModel (Sym (SymTerm Int
_ TypedSymbol t
sym) := t
val) = forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol t
sym t
val forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
buildModel ModelSymPair t
_ = forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"
instance
ModelRep
( ModelSymPair a,
ModelSymPair b
)
Model
SymbolSet
TypedSymbol
where
buildModel :: (ModelSymPair a, ModelSymPair b) -> Model
buildModel
( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2
) =
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
buildModel (ModelSymPair a, ModelSymPair b)
_ = forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"
instance
ModelRep
( ModelSymPair a,
ModelSymPair b,
ModelSymPair c
)
Model
SymbolSet
TypedSymbol
where
buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c) -> Model
buildModel
( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2,
Sym (SymTerm Int
_ TypedSymbol c
sym3) := c
val3
) =
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c)
_ = forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"
instance
ModelRep
( ModelSymPair a,
ModelSymPair b,
ModelSymPair c,
ModelSymPair d
)
Model
SymbolSet
TypedSymbol
where
buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d)
-> Model
buildModel
( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2,
Sym (SymTerm Int
_ TypedSymbol c
sym3) := c
val3,
Sym (SymTerm Int
_ TypedSymbol d
sym4) := d
val4
) =
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d)
_ = forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"
instance
ModelRep
( ModelSymPair a,
ModelSymPair b,
ModelSymPair c,
ModelSymPair d,
ModelSymPair e
)
Model
SymbolSet
TypedSymbol
where
buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
ModelSymPair e)
-> Model
buildModel
( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2,
Sym (SymTerm Int
_ TypedSymbol c
sym3) := c
val3,
Sym (SymTerm Int
_ TypedSymbol d
sym4) := d
val4,
Sym (SymTerm Int
_ TypedSymbol e
sym5) := e
val5
) =
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
ModelSymPair e)
_ = forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"
instance
ModelRep
( ModelSymPair a,
ModelSymPair b,
ModelSymPair c,
ModelSymPair d,
ModelSymPair e,
ModelSymPair f
)
Model
SymbolSet
TypedSymbol
where
buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
ModelSymPair e, ModelSymPair f)
-> Model
buildModel
( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2,
Sym (SymTerm Int
_ TypedSymbol c
sym3) := c
val3,
Sym (SymTerm Int
_ TypedSymbol d
sym4) := d
val4,
Sym (SymTerm Int
_ TypedSymbol e
sym5) := e
val5,
Sym (SymTerm Int
_ TypedSymbol f
sym6) := f
val6
) =
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol f
sym6 f
val6
forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
ModelSymPair e, ModelSymPair f)
_ = forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"
instance
ModelRep
( ModelSymPair a,
ModelSymPair b,
ModelSymPair c,
ModelSymPair d,
ModelSymPair e,
ModelSymPair f,
ModelSymPair g
)
Model
SymbolSet
TypedSymbol
where
buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
ModelSymPair e, ModelSymPair f, ModelSymPair g)
-> Model
buildModel
( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2,
Sym (SymTerm Int
_ TypedSymbol c
sym3) := c
val3,
Sym (SymTerm Int
_ TypedSymbol d
sym4) := d
val4,
Sym (SymTerm Int
_ TypedSymbol e
sym5) := e
val5,
Sym (SymTerm Int
_ TypedSymbol f
sym6) := f
val6,
Sym (SymTerm Int
_ TypedSymbol g
sym7) := g
val7
) =
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol f
sym6 f
val6
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol g
sym7 g
val7
forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
ModelSymPair e, ModelSymPair f, ModelSymPair g)
_ = forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"
instance
ModelRep
( ModelSymPair a,
ModelSymPair b,
ModelSymPair c,
ModelSymPair d,
ModelSymPair e,
ModelSymPair f,
ModelSymPair g,
ModelSymPair h
)
Model
SymbolSet
TypedSymbol
where
buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h)
-> Model
buildModel
( Sym (SymTerm Int
_ TypedSymbol a
sym1) := a
val1,
Sym (SymTerm Int
_ TypedSymbol b
sym2) := b
val2,
Sym (SymTerm Int
_ TypedSymbol c
sym3) := c
val3,
Sym (SymTerm Int
_ TypedSymbol d
sym4) := d
val4,
Sym (SymTerm Int
_ TypedSymbol e
sym5) := e
val5,
Sym (SymTerm Int
_ TypedSymbol f
sym6) := f
val6,
Sym (SymTerm Int
_ TypedSymbol g
sym7) := g
val7,
Sym (SymTerm Int
_ TypedSymbol h
sym8) := h
val8
) =
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol f
sym6 f
val6
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol g
sym7 g
val7
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol h
sym8 h
val8
forall a b. (a -> b) -> a -> b
$ forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
buildModel (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d,
ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h)
_ = forall a. HasCallStack => String -> a
error String
"buildModel: should only use symbolic constants"
instance (SupportedPrim a, SupportedPrim b) => Function (a --> b) where
type Arg (a --> b) = Sym a
type Ret (a --> b) = Sym b
(GeneralFun TypedSymbol a
arg Term b
tm) # :: (a --> b) -> Arg (a --> b) -> Ret (a --> b)
# (Sym Term a
v) = forall a. Term a -> Sym a
Sym forall a b. (a -> b) -> a -> b
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
arg Term a
v Term b
tm
(-->) :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Sym b -> a --> b
--> :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Sym b -> a --> b
(-->) TypedSymbol a
arg (Sym Term b
v) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol a
arg Term b
v