    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Tools.CodeGen
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Code-generation from SBV programs.
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Tools.CodeGen (

            -- * Code generation from symbolic programs
            -- $cCodeGeneration
              SBVCodeGen, cgSym

            -- ** Setting code-generation options
            , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile, cgOverwriteFiles, cgShowU8UsingHex

            -- ** Designating inputs
            , cgInput, cgInputArr

            -- ** Designating outputs
            , cgOutput, cgOutputArr

            -- ** Designating return values
            , cgReturn, cgReturnArr

            -- ** Code generation with uninterpreted functions
            , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert

            -- ** Code generation with 'Data.SBV.SInteger' and 'Data.SBV.SReal' types
            -- $unboundedCGen
            , cgIntegerSize, cgSRealType, CgSRealType(..)

            -- ** Compilation to C
            , compileToC, compileToCLib
           ) where

    import Data.SBV.Compilers.C
    import Data.SBV.Compilers.CodeGen

    {- $cCodeGeneration
    The SBV library can generate straight-line executable code in C. (While other target languages are
    certainly possible, currently only C is supported.) The generated code will perform no run-time memory-allocations,
    (no calls to @malloc@), so its memory usage can be predicted ahead of time. Also, the functions will execute precisely the
    same instructions in all calls, so they have predictable timing properties as well. The generated code
    has no loops or jumps, and is typically quite fast. While the generated code can be large due to complete unrolling,
    these characteristics make them suitable for use in hard real-time systems, as well as in traditional computing.
    -}

    {- $unboundedCGen
    The types 'Data.SBV.SInteger' and 'Data.SBV.SReal' are unbounded quantities that have no direct counterparts in the C language. Therefore,
    it is not possible to generate standard C code for SBV programs using these types, unless custom libraries are available. To
    overcome this, SBV allows the user to explicitly set what the corresponding types should be for these two cases, using
    the functions below. Note that while these mappings will produce valid C code, the resulting code will be subject to
    overflow/underflows for 'Data.SBV.SInteger', and rounding for 'Data.SBV.SReal', so there is an implicit loss of precision.

    If the user does /not/ specify these mappings, then SBV will
    refuse to compile programs that involve these types.
    -}