-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.CodeGeneration.Uninterpreted
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates the use of uninterpreted functions for the purposes of
-- code generation. This facility is important when we want to take
-- advantage of native libraries in the target platform, or when we'd
-- like to hand-generate code for certain functions for various
-- purposes, such as efficiency, or reliability.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.CodeGeneration.Uninterpreted where

import Data.Maybe (fromMaybe)

import Data.SBV
import Data.SBV.Tools.CodeGen

-- | A definition of shiftLeft that can deal with variable length shifts.
-- (Note that the ``shiftL`` method from the 'Bits' class requires an 'Int' shift
-- amount.) Unfortunately, this'll generate rather clumsy C code due to the
-- use of tables etc., so we uninterpret it for code generation purposes
-- using the 'cgUninterpret' function.
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 String
"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 -- the C code we'd like SBV to spit out when generating code. Note that this is
        -- arbitrary C code. In this case we just used a macro, but it could be a function,
        -- text that includes files etc. It should essentially bring the name SBV_SHIFTLEFT
        -- used above into scope when compiled. If no code is needed, one can also just
        -- provide the empty list for the same effect. Also see 'cgAddDecl', 'cgAddLDFlags',
        -- and 'cgAddPrototype' functions for further variations.
        cCode :: [String]
cCode = [String
"#define SBV_SHIFTLEFT(x, y) ((x) << (y))"]
        -- the Haskell code we'd like SBV to use when running inside Haskell or when
        -- translated to SMTLib for verification purposes. This is good old Haskell
        -- code, as one would typically write.
        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)

-- | Test function that uses shiftLeft defined above. When used as a normal Haskell function
-- or in verification the definition is fully used, i.e., no uninterpretation happens. To wit,
-- we have:
--
--  >>> tstShiftLeft 3 4 5
--  224 :: SWord32
--
--  >>> prove $ \x y -> tstShiftLeft x y 0 .== x + y
--  Q.E.D.
tstShiftLeft ::  SWord32 -> SWord32 -> SWord32 -> SWord32
tstShiftLeft :: SWord32 -> SWord32 -> SWord32 -> SWord32
tstShiftLeft SWord32
x SWord32
y 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

-- | Generate C code for "tstShiftLeft". In this case, SBV will *use* the user given definition
-- verbatim, instead of generating code for it. (Also see the functions 'cgAddDecl', 'cgAddLDFlags',
-- and 'cgAddPrototype'.)
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
                [SWord32
x, SWord32
y, SWord32
z] <- Int -> String -> SBVCodeGen [SWord32]
forall a. SymVal a => Int -> String -> SBVCodeGen [SBV a]
cgInputArr Int
3 String
"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