    -----------------------------------------------------------------------------
    -- |
    -- 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

    -- $setup
    -- >>> -- For doctest purposes only:
    -- >>> import Data.SBV

    -- | 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. SMTDefinable 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 b.
    (Ord b, SymVal b, Num b) =>
    [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