sbv-7.13: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Documentation.SBV.Examples.CodeGeneration.Uninterpreted

Description

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.

Synopsis

- shiftLeft :: SWord32 -> SWord32 -> SWord32
- tstShiftLeft :: SWord32 -> SWord32 -> SWord32 -> SWord32
- genCCode :: IO ()

# Documentation

shiftLeft :: SWord32 -> SWord32 -> SWord32 Source #

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.

tstShiftLeft :: SWord32 -> SWord32 -> SWord32 -> SWord32 Source #

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.

genCCode :: IO () Source #

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`.)