{-# 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 :: SBV Word32 -> SBV Word32 -> SBV Word32
shiftLeft = String
-> [String]
-> (SBV Word32 -> SBV Word32 -> SBV Word32)
-> SBV Word32
-> SBV Word32
-> SBV Word32
forall a. Uninterpreted a => String -> [String] -> a -> a
cgUninterpret String
"SBV_SHIFTLEFT" [String]
cCode SBV Word32 -> SBV Word32 -> SBV Word32
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 = [String
"#define SBV_SHIFTLEFT(x, y) ((x) << (y))"]
hCode :: SBV a -> SBV b -> SBV a
hCode 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 <- [Int
0.. SBV a -> Int
forall {a}. Bits a => a -> Int
bs SBV a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]] (a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
0)
bs :: a -> Int
bs a
x = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
error String
"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 :: SBV Word32 -> SBV Word32 -> SBV Word32 -> SBV Word32
tstShiftLeft SBV Word32
x SBV Word32
y SBV Word32
z = SBV Word32
x SBV Word32 -> SBV Word32 -> SBV Word32
`shiftLeft` SBV Word32
z SBV Word32 -> SBV Word32 -> SBV Word32
forall a. Num a => a -> a -> a
+ SBV Word32
y SBV Word32 -> SBV Word32 -> SBV Word32
`shiftLeft` SBV Word32
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 String
"tst" (SBVCodeGen () -> IO ()) -> SBVCodeGen () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
[SBV Word32
x, SBV Word32
y, SBV Word32
z] <- Int -> String -> SBVCodeGen [SBV Word32]
forall a. SymVal a => Int -> String -> SBVCodeGen [SBV a]
cgInputArr Int
3 String
"vs"
SBV Word32 -> SBVCodeGen ()
forall a. SBV a -> SBVCodeGen ()
cgReturn (SBV Word32 -> SBVCodeGen ()) -> SBV Word32 -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ SBV Word32 -> SBV Word32 -> SBV Word32 -> SBV Word32
tstShiftLeft SBV Word32
x SBV Word32
y SBV Word32
z