{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric      #-}

module Language.Fixpoint.Smt.Bitvector
       ( -- * Constructor
         Bv (..)

         -- * Sizes
       , BvSize (..)

         -- * Operators
       , BvOp (..)

         -- * BitVector Sort Constructor
       , mkSort

         -- * BitVector Expression Constructor
       , eOp

         -- * BitVector Type Constructor
       , bvTyCon

       ) where

import           Data.Generics           (Data)
import qualified Data.Text               as T
import           Data.Typeable           (Typeable)
import           GHC.Generics            (Generic)
import           Language.Fixpoint.Types.Names
import           Language.Fixpoint.Types

data Bv     = Bv !BvSize !String

data BvSize = S32   | S64
              deriving (BvSize -> BvSize -> Bool
(BvSize -> BvSize -> Bool)
-> (BvSize -> BvSize -> Bool) -> Eq BvSize
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BvSize -> BvSize -> Bool
$c/= :: BvSize -> BvSize -> Bool
== :: BvSize -> BvSize -> Bool
$c== :: BvSize -> BvSize -> Bool
Eq, Eq BvSize
Eq BvSize
-> (BvSize -> BvSize -> Ordering)
-> (BvSize -> BvSize -> Bool)
-> (BvSize -> BvSize -> Bool)
-> (BvSize -> BvSize -> Bool)
-> (BvSize -> BvSize -> Bool)
-> (BvSize -> BvSize -> BvSize)
-> (BvSize -> BvSize -> BvSize)
-> Ord BvSize
BvSize -> BvSize -> Bool
BvSize -> BvSize -> Ordering
BvSize -> BvSize -> BvSize
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 :: BvSize -> BvSize -> BvSize
$cmin :: BvSize -> BvSize -> BvSize
max :: BvSize -> BvSize -> BvSize
$cmax :: BvSize -> BvSize -> BvSize
>= :: BvSize -> BvSize -> Bool
$c>= :: BvSize -> BvSize -> Bool
> :: BvSize -> BvSize -> Bool
$c> :: BvSize -> BvSize -> Bool
<= :: BvSize -> BvSize -> Bool
$c<= :: BvSize -> BvSize -> Bool
< :: BvSize -> BvSize -> Bool
$c< :: BvSize -> BvSize -> Bool
compare :: BvSize -> BvSize -> Ordering
$ccompare :: BvSize -> BvSize -> Ordering
$cp1Ord :: Eq BvSize
Ord, Int -> BvSize -> ShowS
[BvSize] -> ShowS
BvSize -> String
(Int -> BvSize -> ShowS)
-> (BvSize -> String) -> ([BvSize] -> ShowS) -> Show BvSize
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BvSize] -> ShowS
$cshowList :: [BvSize] -> ShowS
show :: BvSize -> String
$cshow :: BvSize -> String
showsPrec :: Int -> BvSize -> ShowS
$cshowsPrec :: Int -> BvSize -> ShowS
Show, Typeable BvSize
DataType
Constr
Typeable BvSize
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> BvSize -> c BvSize)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BvSize)
-> (BvSize -> Constr)
-> (BvSize -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BvSize))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BvSize))
-> ((forall b. Data b => b -> b) -> BvSize -> BvSize)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BvSize -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BvSize -> r)
-> (forall u. (forall d. Data d => d -> u) -> BvSize -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> BvSize -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BvSize -> m BvSize)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BvSize -> m BvSize)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BvSize -> m BvSize)
-> Data BvSize
BvSize -> DataType
BvSize -> Constr
(forall b. Data b => b -> b) -> BvSize -> BvSize
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BvSize -> c BvSize
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BvSize
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BvSize -> u
forall u. (forall d. Data d => d -> u) -> BvSize -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BvSize -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BvSize -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BvSize -> m BvSize
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BvSize -> m BvSize
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BvSize
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BvSize -> c BvSize
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BvSize)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BvSize)
$cS64 :: Constr
$cS32 :: Constr
$tBvSize :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> BvSize -> m BvSize
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BvSize -> m BvSize
gmapMp :: (forall d. Data d => d -> m d) -> BvSize -> m BvSize
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BvSize -> m BvSize
gmapM :: (forall d. Data d => d -> m d) -> BvSize -> m BvSize
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BvSize -> m BvSize
gmapQi :: Int -> (forall d. Data d => d -> u) -> BvSize -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BvSize -> u
gmapQ :: (forall d. Data d => d -> u) -> BvSize -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BvSize -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BvSize -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BvSize -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BvSize -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BvSize -> r
gmapT :: (forall b. Data b => b -> b) -> BvSize -> BvSize
$cgmapT :: (forall b. Data b => b -> b) -> BvSize -> BvSize
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BvSize)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BvSize)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c BvSize)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BvSize)
dataTypeOf :: BvSize -> DataType
$cdataTypeOf :: BvSize -> DataType
toConstr :: BvSize -> Constr
$ctoConstr :: BvSize -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BvSize
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BvSize
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BvSize -> c BvSize
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BvSize -> c BvSize
$cp1Data :: Typeable BvSize
Data, Typeable, (forall x. BvSize -> Rep BvSize x)
-> (forall x. Rep BvSize x -> BvSize) -> Generic BvSize
forall x. Rep BvSize x -> BvSize
forall x. BvSize -> Rep BvSize x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep BvSize x -> BvSize
$cfrom :: forall x. BvSize -> Rep BvSize x
Generic)

data BvOp   = BvAnd | BvOr
              deriving (BvOp -> BvOp -> Bool
(BvOp -> BvOp -> Bool) -> (BvOp -> BvOp -> Bool) -> Eq BvOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BvOp -> BvOp -> Bool
$c/= :: BvOp -> BvOp -> Bool
== :: BvOp -> BvOp -> Bool
$c== :: BvOp -> BvOp -> Bool
Eq, Eq BvOp
Eq BvOp
-> (BvOp -> BvOp -> Ordering)
-> (BvOp -> BvOp -> Bool)
-> (BvOp -> BvOp -> Bool)
-> (BvOp -> BvOp -> Bool)
-> (BvOp -> BvOp -> Bool)
-> (BvOp -> BvOp -> BvOp)
-> (BvOp -> BvOp -> BvOp)
-> Ord BvOp
BvOp -> BvOp -> Bool
BvOp -> BvOp -> Ordering
BvOp -> BvOp -> BvOp
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 :: BvOp -> BvOp -> BvOp
$cmin :: BvOp -> BvOp -> BvOp
max :: BvOp -> BvOp -> BvOp
$cmax :: BvOp -> BvOp -> BvOp
>= :: BvOp -> BvOp -> Bool
$c>= :: BvOp -> BvOp -> Bool
> :: BvOp -> BvOp -> Bool
$c> :: BvOp -> BvOp -> Bool
<= :: BvOp -> BvOp -> Bool
$c<= :: BvOp -> BvOp -> Bool
< :: BvOp -> BvOp -> Bool
$c< :: BvOp -> BvOp -> Bool
compare :: BvOp -> BvOp -> Ordering
$ccompare :: BvOp -> BvOp -> Ordering
$cp1Ord :: Eq BvOp
Ord, Int -> BvOp -> ShowS
[BvOp] -> ShowS
BvOp -> String
(Int -> BvOp -> ShowS)
-> (BvOp -> String) -> ([BvOp] -> ShowS) -> Show BvOp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BvOp] -> ShowS
$cshowList :: [BvOp] -> ShowS
show :: BvOp -> String
$cshow :: BvOp -> String
showsPrec :: Int -> BvOp -> ShowS
$cshowsPrec :: Int -> BvOp -> ShowS
Show, Typeable BvOp
DataType
Constr
Typeable BvOp
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> BvOp -> c BvOp)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BvOp)
-> (BvOp -> Constr)
-> (BvOp -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BvOp))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BvOp))
-> ((forall b. Data b => b -> b) -> BvOp -> BvOp)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BvOp -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BvOp -> r)
-> (forall u. (forall d. Data d => d -> u) -> BvOp -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> BvOp -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BvOp -> m BvOp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BvOp -> m BvOp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BvOp -> m BvOp)
-> Data BvOp
BvOp -> DataType
BvOp -> Constr
(forall b. Data b => b -> b) -> BvOp -> BvOp
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BvOp -> c BvOp
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BvOp
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BvOp -> u
forall u. (forall d. Data d => d -> u) -> BvOp -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BvOp -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BvOp -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BvOp -> m BvOp
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BvOp -> m BvOp
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BvOp
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BvOp -> c BvOp
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BvOp)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BvOp)
$cBvOr :: Constr
$cBvAnd :: Constr
$tBvOp :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> BvOp -> m BvOp
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BvOp -> m BvOp
gmapMp :: (forall d. Data d => d -> m d) -> BvOp -> m BvOp
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BvOp -> m BvOp
gmapM :: (forall d. Data d => d -> m d) -> BvOp -> m BvOp
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BvOp -> m BvOp
gmapQi :: Int -> (forall d. Data d => d -> u) -> BvOp -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BvOp -> u
gmapQ :: (forall d. Data d => d -> u) -> BvOp -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BvOp -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BvOp -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BvOp -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BvOp -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BvOp -> r
gmapT :: (forall b. Data b => b -> b) -> BvOp -> BvOp
$cgmapT :: (forall b. Data b => b -> b) -> BvOp -> BvOp
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BvOp)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BvOp)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c BvOp)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BvOp)
dataTypeOf :: BvOp -> DataType
$cdataTypeOf :: BvOp -> DataType
toConstr :: BvOp -> Constr
$ctoConstr :: BvOp -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BvOp
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BvOp
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BvOp -> c BvOp
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BvOp -> c BvOp
$cp1Data :: Typeable BvOp
Data, Typeable, (forall x. BvOp -> Rep BvOp x)
-> (forall x. Rep BvOp x -> BvOp) -> Generic BvOp
forall x. Rep BvOp x -> BvOp
forall x. BvOp -> Rep BvOp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep BvOp x -> BvOp
$cfrom :: forall x. BvOp -> Rep BvOp x
Generic)

-- | Construct the bitvector `Sort` from its `BvSize`
mkSort :: BvSize -> Sort
mkSort :: BvSize -> Sort
mkSort BvSize
s = Sort -> [Sort] -> Sort
fApp (FTycon -> Sort
fTyconSort FTycon
bvTyCon) [ FTycon -> Sort
fTyconSort (BvSize -> FTycon
sizeTyCon BvSize
s) ]

bvTyCon :: FTycon
bvTyCon :: FTycon
bvTyCon = LocSymbol -> FTycon
symbolFTycon (LocSymbol -> FTycon) -> LocSymbol -> FTycon
forall a b. (a -> b) -> a -> b
$ Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
bitVecName

sizeTyCon    :: BvSize -> FTycon
sizeTyCon :: BvSize -> FTycon
sizeTyCon    = LocSymbol -> FTycon
symbolFTycon (LocSymbol -> FTycon) -> (BvSize -> LocSymbol) -> BvSize -> FTycon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Symbol -> LocSymbol) -> (BvSize -> Symbol) -> BvSize -> LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BvSize -> Symbol
sizeName

sizeName :: BvSize -> Symbol
sizeName :: BvSize -> Symbol
sizeName BvSize
S32 = Symbol
size32Name
sizeName BvSize
S64 = Symbol
size64Name

-- | Construct an `Expr` using a raw string, e.g. (Bv S32 "#x02000000")
instance Expression Bv where
  expr :: Bv -> Expr
expr (Bv BvSize
sz String
v) = Constant -> Expr
ECon (Constant -> Expr) -> Constant -> Expr
forall a b. (a -> b) -> a -> b
$ Text -> Sort -> Constant
L (String -> Text
T.pack String
v) (BvSize -> Sort
mkSort BvSize
sz)

-- | Apply some bitvector operator to a list of arguments
eOp :: BvOp -> [Expr] -> Expr
eOp :: BvOp -> [Expr] -> Expr
eOp BvOp
b [Expr]
es = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ BvOp -> Symbol
opName BvOp
b) [Expr]
es

opName :: BvOp -> Symbol
opName :: BvOp -> Symbol
opName BvOp
BvAnd = Symbol
bvAndName
opName BvOp
BvOr  = Symbol
bvOrName


-- sizeSort     = (`FApp` [fObj $ dummyLoc $ symbol "obj"]) . sizeTC
-- s32TyCon     = symbolFTycon $ dummyLoc size32Name
-- s64TyCon     = symbolFTycon $ dummyLoc size64Name