{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.CodeGeneration.Uninterpreted where
import Data.Maybe (fromMaybe)
import Data.SBV
import Data.SBV.Tools.CodeGen
shiftLeft :: SWord32 -> SWord32 -> SWord32
shiftLeft :: SWord32 -> SWord32 -> SWord32
shiftLeft = String
-> [String]
-> (SWord32 -> SWord32 -> SWord32)
-> SWord32
-> SWord32
-> SWord32
forall a. Uninterpreted a => String -> [String] -> a -> a
cgUninterpret "SBV_SHIFTLEFT" [String]
cCode SWord32 -> SWord32 -> SWord32
forall a b.
(SymVal a, SymVal b, Ord b, Ord a, Num b, Num a, Bits a) =>
SBV a -> SBV b -> SBV a
hCode
where
cCode :: [String]
cCode = ["#define SBV_SHIFTLEFT(x, y) ((x) << (y))"]
hCode :: SBV a -> SBV b -> SBV a
hCode x :: SBV a
x = [SBV a] -> SBV a -> SBV b -> SBV a
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SBV a
x SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
* a -> SBV a
forall a. SymVal a => a -> SBV a
literal (Int -> a
forall a. Bits a => Int -> a
bit Int
b) | Int
b <- [0.. SBV a -> Int
forall a. Bits a => a -> Int
bs SBV a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]] (a -> SBV a
forall a. SymVal a => a -> SBV a
literal 0)
bs :: a -> Int
bs x :: a
x = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
error "SBV.Example.CodeGeneration.Uninterpreted.shiftLeft: Unexpected non-finite usage!") (a -> Maybe Int
forall a. Bits a => a -> Maybe Int
bitSizeMaybe a
x)
tstShiftLeft :: SWord32 -> SWord32 -> SWord32 -> SWord32
tstShiftLeft :: SWord32 -> SWord32 -> SWord32 -> SWord32
tstShiftLeft x :: SWord32
x y :: SWord32
y z :: SWord32
z = SWord32
x SWord32 -> SWord32 -> SWord32
`shiftLeft` SWord32
z SWord32 -> SWord32 -> SWord32
forall a. Num a => a -> a -> a
+ SWord32
y SWord32 -> SWord32 -> SWord32
`shiftLeft` SWord32
z
genCCode :: IO ()
genCCode :: IO ()
genCCode = Maybe String -> String -> SBVCodeGen () -> IO ()
forall a. Maybe String -> String -> SBVCodeGen a -> IO a
compileToC Maybe String
forall a. Maybe a
Nothing "tst" (SBVCodeGen () -> IO ()) -> SBVCodeGen () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
[x :: SWord32
x, y :: SWord32
y, z :: SWord32
z] <- Int -> String -> SBVCodeGen [SWord32]
forall a. SymVal a => Int -> String -> SBVCodeGen [SBV a]
cgInputArr 3 "vs"
SWord32 -> SBVCodeGen ()
forall a. SBV a -> SBVCodeGen ()
cgReturn (SWord32 -> SBVCodeGen ()) -> SWord32 -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ SWord32 -> SWord32 -> SWord32 -> SWord32
tstShiftLeft SWord32
x SWord32
y SWord32
z