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

    {-# LANGUAGE CPP                        #-}
    {-# LANGUAGE FlexibleInstances          #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Compilers.CodeGen (
            -- * The codegen monad
              SBVCodeGen(..), cgSym

            -- * Specifying inputs, SBV variants
            , cgInput,  cgInputArr
            , cgOutput, cgOutputArr
            , cgReturn, cgReturnArr

            -- * Specifying inputs, SVal variants
            , svCgInput,  svCgInputArr
            , svCgOutput, svCgOutputArr
            , svCgReturn, svCgReturnArr

            -- * Settings
            , cgPerformRTCs, cgSetDriverValues
            , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert, cgOverwriteFiles, cgShowU8UsingHex
            , cgIntegerSize, cgSRealType, CgSRealType(..)

            -- * Infrastructure
            , CgTarget(..), CgConfig(..), CgState(..), CgPgmBundle(..), CgPgmKind(..), CgVal(..)
            , defaultCgConfig, initCgState, isCgDriver, isCgMakefile

            -- * Generating collateral
            , cgGenerateDriver, cgGenerateMakefile, codeGen, renderCgPgmBundle
            ) where

    import Control.Monad             (filterM, replicateM, unless)
    import Control.Monad.Trans       (MonadIO(liftIO), lift)
    import Control.Monad.State.Lazy  (MonadState, StateT(..), modify')
    import Data.Char                 (toLower, isSpace)
    import Data.List                 (nub, isPrefixOf, intercalate, (\\))
    import System.Directory          (createDirectoryIfMissing, doesDirectoryExist, doesFileExist)
    import System.FilePath           ((</>))
    import System.IO                 (hFlush, stdout)

    import           Text.PrettyPrint.HughesPJ      (Doc, vcat)
    import qualified Text.PrettyPrint.HughesPJ as P (render)

    import Data.SBV.Core.Data
    import Data.SBV.Core.Symbolic (MonadSymbolic(..), svToSymSV, svMkSymVar, outputSVal)

    #if MIN_VERSION_base(4,11,0)
    import Control.Monad.Fail as Fail
    #endif

    -- | Abstract over code generation for different languages
    class CgTarget a where
      targetName :: a -> String
      translate  :: a -> CgConfig -> String -> CgState -> Result -> CgPgmBundle

    -- | Options for code-generation.
    data CgConfig = CgConfig {
              CgConfig -> Bool
    cgRTC                :: Bool               -- ^ If 'True', perform run-time-checks for index-out-of-bounds or shifting-by-large values etc.
            , CgConfig -> Maybe Int
    cgInteger            :: Maybe Int          -- ^ Bit-size to use for representing SInteger (if any)
            , CgConfig -> Maybe CgSRealType
    cgReal               :: Maybe CgSRealType  -- ^ Type to use for representing SReal (if any)
            , CgConfig -> [Integer]
    cgDriverVals         :: [Integer]          -- ^ Values to use for the driver program generated, useful for generating non-random drivers.
            , CgConfig -> Bool
    cgGenDriver          :: Bool               -- ^ If 'True', will generate a driver program
            , CgConfig -> Bool
    cgGenMakefile        :: Bool               -- ^ If 'True', will generate a makefile
            , CgConfig -> Bool
    cgIgnoreAsserts      :: Bool               -- ^ If 'True', will ignore 'Data.SBV.sAssert' calls
            , CgConfig -> Bool
    cgOverwriteGenerated :: Bool               -- ^ If 'True', will overwrite the generated files without prompting.
            , CgConfig -> Bool
    cgShowU8InHex        :: Bool               -- ^ If 'True', then 8-bit unsigned values will be shown in hex as well, otherwise decimal. (Other types always shown in hex.)
            }

    -- | Default options for code generation. The run-time checks are turned-off, and the driver values are completely random.
    defaultCgConfig :: CgConfig
    defaultCgConfig :: CgConfig
    defaultCgConfig = CgConfig :: Bool
    -> Maybe Int
    -> Maybe CgSRealType
    -> [Integer]
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> CgConfig
    CgConfig { cgRTC :: Bool
    cgRTC                = Bool
    False
                               , cgInteger :: Maybe Int
    cgInteger            = Maybe Int
    forall a. Maybe a
    Nothing
                               , cgReal :: Maybe CgSRealType
    cgReal               = Maybe CgSRealType
    forall a. Maybe a
    Nothing
                               , cgDriverVals :: [Integer]
    cgDriverVals         = []
                               , cgGenDriver :: Bool
    cgGenDriver          = Bool
    True
                               , cgGenMakefile :: Bool
    cgGenMakefile        = Bool
    True
                               , cgIgnoreAsserts :: Bool
    cgIgnoreAsserts      = Bool
    False
                               , cgOverwriteGenerated :: Bool
    cgOverwriteGenerated = Bool
    False
                               , cgShowU8InHex :: Bool
    cgShowU8InHex        = Bool
    False
                               }

    -- | Abstraction of target language values
    data CgVal = CgAtomic SV
               | CgArray  [SV]

    -- | Code-generation state
    data CgState = CgState {
              CgState -> [(String, CgVal)]
    cgInputs         :: [(String, CgVal)]
            , CgState -> [(String, CgVal)]
    cgOutputs        :: [(String, CgVal)]
            , CgState -> [CgVal]
    cgReturns        :: [CgVal]
            , CgState -> [String]
    cgPrototypes     :: [String]    -- extra stuff that goes into the header
            , CgState -> [String]
    cgDecls          :: [String]    -- extra stuff that goes into the top of the file
            , CgState -> [String]
    cgLDFlags        :: [String]    -- extra options that go to the linker
            , CgState -> CgConfig
    cgFinalConfig    :: CgConfig
            }

    -- | Initial configuration for code-generation
    initCgState :: CgState
    initCgState :: CgState
    initCgState = CgState :: [(String, CgVal)]
    -> [(String, CgVal)]
    -> [CgVal]
    -> [String]
    -> [String]
    -> [String]
    -> CgConfig
    -> CgState
    CgState {
              cgInputs :: [(String, CgVal)]
    cgInputs         = []
            , cgOutputs :: [(String, CgVal)]
    cgOutputs        = []
            , cgReturns :: [CgVal]
    cgReturns        = []
            , cgPrototypes :: [String]
    cgPrototypes     = []
            , cgDecls :: [String]
    cgDecls          = []
            , cgLDFlags :: [String]
    cgLDFlags        = []
            , cgFinalConfig :: CgConfig
    cgFinalConfig    = CgConfig
    defaultCgConfig
            }

    -- | The code-generation monad. Allows for precise layout of input values
    -- reference parameters (for returning composite values in languages such as C),
    -- and return values.
    newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a)
                       deriving ( Functor SBVCodeGen
    a -> SBVCodeGen a
    Functor SBVCodeGen =>
    (forall a. a -> SBVCodeGen a)
    -> (forall a b.
        SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b)
    -> (forall a b c.
        (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c)
    -> (forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b)
    -> (forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a)
    -> Applicative SBVCodeGen
    SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
    SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
    SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
    (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
    forall a. a -> SBVCodeGen a
    forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
    forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
    forall a b. SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
    forall a b c.
    (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    <* :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
    $c<* :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
    *> :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
    $c*> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
    liftA2 :: (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
    $cliftA2 :: forall a b c.
    (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
    <*> :: SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
    $c<*> :: forall a b. SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
    pure :: a -> SBVCodeGen a
    $cpure :: forall a. a -> SBVCodeGen a
    $cp1Applicative :: Functor SBVCodeGen
    Applicative, a -> SBVCodeGen b -> SBVCodeGen a
    (a -> b) -> SBVCodeGen a -> SBVCodeGen b
    (forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b)
    -> (forall a b. a -> SBVCodeGen b -> SBVCodeGen a)
    -> Functor SBVCodeGen
    forall a b. a -> SBVCodeGen b -> SBVCodeGen a
    forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> SBVCodeGen b -> SBVCodeGen a
    $c<$ :: forall a b. a -> SBVCodeGen b -> SBVCodeGen a
    fmap :: (a -> b) -> SBVCodeGen a -> SBVCodeGen b
    $cfmap :: forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b
    Functor, Applicative SBVCodeGen
    a -> SBVCodeGen a
    Applicative SBVCodeGen =>
    (forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b)
    -> (forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b)
    -> (forall a. a -> SBVCodeGen a)
    -> Monad SBVCodeGen
    SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
    SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
    forall a. a -> SBVCodeGen a
    forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
    forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    return :: a -> SBVCodeGen a
    $creturn :: forall a. a -> SBVCodeGen a
    >> :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
    $c>> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
    >>= :: SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
    $c>>= :: forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
    $cp1Monad :: Applicative SBVCodeGen
    Monad, Monad SBVCodeGen
    Monad SBVCodeGen =>
    (forall a. IO a -> SBVCodeGen a) -> MonadIO SBVCodeGen
    IO a -> SBVCodeGen a
    forall a. IO a -> SBVCodeGen a
    forall (m :: * -> *).
    Monad m =>
    (forall a. IO a -> m a) -> MonadIO m
    liftIO :: IO a -> SBVCodeGen a
    $cliftIO :: forall a. IO a -> SBVCodeGen a
    $cp1MonadIO :: Monad SBVCodeGen
    MonadIO, MonadState CgState
                                , MonadIO SBVCodeGen
    SBVCodeGen State
    MonadIO SBVCodeGen => SBVCodeGen State -> MonadSymbolic SBVCodeGen
    forall (m :: * -> *). MonadIO m => m State -> MonadSymbolic m
    symbolicEnv :: SBVCodeGen State
    $csymbolicEnv :: SBVCodeGen State
    $cp1MonadSymbolic :: MonadIO SBVCodeGen
    MonadSymbolic
    #if MIN_VERSION_base(4,11,0)
                                , Monad SBVCodeGen
    Monad SBVCodeGen =>
    (forall a. String -> SBVCodeGen a) -> MonadFail SBVCodeGen
    String -> SBVCodeGen a
    forall a. String -> SBVCodeGen a
    forall (m :: * -> *).
    Monad m =>
    (forall a. String -> m a) -> MonadFail m
    fail :: String -> SBVCodeGen a
    $cfail :: forall a. String -> SBVCodeGen a
    $cp1MonadFail :: Monad SBVCodeGen
    Fail.MonadFail
    #endif
                                )

    -- | Reach into symbolic monad from code-generation
    cgSym :: Symbolic a -> SBVCodeGen a
    cgSym :: Symbolic a -> SBVCodeGen a
    cgSym = StateT CgState Symbolic a -> SBVCodeGen a
    forall a. StateT CgState Symbolic a -> SBVCodeGen a
    SBVCodeGen (StateT CgState Symbolic a -> SBVCodeGen a)
    -> (Symbolic a -> StateT CgState Symbolic a)
    -> Symbolic a
    -> SBVCodeGen a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Symbolic a -> StateT CgState Symbolic a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift

    -- | Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off. Default: 'False'.
    cgPerformRTCs :: Bool -> SBVCodeGen ()
    cgPerformRTCs :: Bool -> SBVCodeGen ()
    cgPerformRTCs b :: Bool
    b = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgFinalConfig :: CgConfig
    cgFinalConfig = (CgState -> CgConfig
    cgFinalConfig CgState
    s) { cgRTC :: Bool
    cgRTC = Bool
    b } })

    -- | Sets number of bits to be used for representing the 'SInteger' type in the generated C code.
    -- The argument must be one of @8@, @16@, @32@, or @64@. Note that this is essentially unsafe as
    -- the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as
    -- typical in most C implementations.
    cgIntegerSize :: Int -> SBVCodeGen ()
    cgIntegerSize :: Int -> SBVCodeGen ()
    cgIntegerSize i :: Int
    i
      | Int
    i Int -> [Int] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [8, 16, 32, 64]
      = String -> SBVCodeGen ()
    forall a. HasCallStack => String -> a
    error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
    forall a b. (a -> b) -> a -> b
    $ "SBV.cgIntegerSize: Argument must be one of 8, 16, 32, or 64. Received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
      | Bool
    True
      = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgFinalConfig :: CgConfig
    cgFinalConfig = (CgState -> CgConfig
    cgFinalConfig CgState
    s) { cgInteger :: Maybe Int
    cgInteger = Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    i }})

    -- | Possible mappings for the 'SReal' type when translated to C. Used in conjunction
    -- with the function 'cgSRealType'. Note that the particular characteristics of the
    -- mapped types depend on the platform and the compiler used for compiling the generated
    -- C program. See <http://en.wikipedia.org/wiki/C_data_types> for details.
    data CgSRealType = CgFloat      -- ^ @float@
                     | CgDouble     -- ^ @double@
                     | CgLongDouble -- ^ @long double@
                     deriving CgSRealType -> CgSRealType -> Bool
    (CgSRealType -> CgSRealType -> Bool)
    -> (CgSRealType -> CgSRealType -> Bool) -> Eq CgSRealType
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: CgSRealType -> CgSRealType -> Bool
    $c/= :: CgSRealType -> CgSRealType -> Bool
    == :: CgSRealType -> CgSRealType -> Bool
    $c== :: CgSRealType -> CgSRealType -> Bool
    Eq

    -- 'Show' instance for 'cgSRealType' displays values as they would be used in a C program
    instance Show CgSRealType where
      show :: CgSRealType -> String
    show CgFloat      = "float"
      show CgDouble     = "double"
      show CgLongDouble = "long double"

    -- | Sets the C type to be used for representing the 'SReal' type in the generated C code.
    -- The setting can be one of C's @"float"@, @"double"@, or @"long double"@, types, depending
    -- on the precision needed. Note that this is essentially unsafe as the semantics of
    -- infinite precision SReal values becomes reduced to the corresponding floating point type in
    -- C, and hence it is subject to rounding errors.
    cgSRealType :: CgSRealType -> SBVCodeGen ()
    cgSRealType :: CgSRealType -> SBVCodeGen ()
    cgSRealType rt :: CgSRealType
    rt = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s {cgFinalConfig :: CgConfig
    cgFinalConfig = (CgState -> CgConfig
    cgFinalConfig CgState
    s) { cgReal :: Maybe CgSRealType
    cgReal = CgSRealType -> Maybe CgSRealType
    forall a. a -> Maybe a
    Just CgSRealType
    rt }})

    -- | Should we generate a driver program? Default: 'True'. When a library is generated, it will have
    -- a driver if any of the contituent functions has a driver. (See 'Data.SBV.Tools.CodeGen.compileToCLib'.)
    cgGenerateDriver :: Bool -> SBVCodeGen ()
    cgGenerateDriver :: Bool -> SBVCodeGen ()
    cgGenerateDriver b :: Bool
    b = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgFinalConfig :: CgConfig
    cgFinalConfig = (CgState -> CgConfig
    cgFinalConfig CgState
    s) { cgGenDriver :: Bool
    cgGenDriver = Bool
    b } })

    -- | Should we generate a Makefile? Default: 'True'.
    cgGenerateMakefile :: Bool -> SBVCodeGen ()
    cgGenerateMakefile :: Bool -> SBVCodeGen ()
    cgGenerateMakefile b :: Bool
    b = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgFinalConfig :: CgConfig
    cgFinalConfig = (CgState -> CgConfig
    cgFinalConfig CgState
    s) { cgGenMakefile :: Bool
    cgGenMakefile = Bool
    b } })

    -- | Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.
    cgSetDriverValues :: [Integer] -> SBVCodeGen ()
    cgSetDriverValues :: [Integer] -> SBVCodeGen ()
    cgSetDriverValues vs :: [Integer]
    vs = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgFinalConfig :: CgConfig
    cgFinalConfig = (CgState -> CgConfig
    cgFinalConfig CgState
    s) { cgDriverVals :: [Integer]
    cgDriverVals = [Integer]
    vs } })

    -- | Ignore assertions (those generated by 'Data.SBV.sAssert' calls) in the generated C code
    cgIgnoreSAssert :: Bool -> SBVCodeGen ()
    cgIgnoreSAssert :: Bool -> SBVCodeGen ()
    cgIgnoreSAssert b :: Bool
    b = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgFinalConfig :: CgConfig
    cgFinalConfig = (CgState -> CgConfig
    cgFinalConfig CgState
    s) { cgIgnoreAsserts :: Bool
    cgIgnoreAsserts = Bool
    b } })

    -- | Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.
    cgAddPrototype :: [String] -> SBVCodeGen ()
    cgAddPrototype :: [String] -> SBVCodeGen ()
    cgAddPrototype ss :: [String]
    ss = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> let old :: [String]
    old = CgState -> [String]
    cgPrototypes CgState
    s
                                           new :: [String]
    new = if [String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    old then [String]
    ss else [String]
    old [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [""] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    ss
                                       in CgState
    s { cgPrototypes :: [String]
    cgPrototypes = [String]
    new })

    -- | If passed 'True', then we will not ask the user if we're overwriting files as we generate
    -- the C code. Otherwise, we'll prompt.
    cgOverwriteFiles :: Bool -> SBVCodeGen ()
    cgOverwriteFiles :: Bool -> SBVCodeGen ()
    cgOverwriteFiles b :: Bool
    b = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgFinalConfig :: CgConfig
    cgFinalConfig = (CgState -> CgConfig
    cgFinalConfig CgState
    s) { cgOverwriteGenerated :: Bool
    cgOverwriteGenerated = Bool
    b } })

    -- | If passed 'True', then we will show 'SWord 8' type in hex. Otherwise we'll show it in decimal. All signed
    -- types are shown decimal, and all unsigned larger types are shown hexadecimal otherwise.
    cgShowU8UsingHex :: Bool -> SBVCodeGen ()
    cgShowU8UsingHex :: Bool -> SBVCodeGen ()
    cgShowU8UsingHex b :: Bool
    b = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgFinalConfig :: CgConfig
    cgFinalConfig = (CgState -> CgConfig
    cgFinalConfig CgState
    s) { cgShowU8InHex :: Bool
    cgShowU8InHex = Bool
    b } })

    -- | Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.
    cgAddDecl :: [String] -> SBVCodeGen ()
    cgAddDecl :: [String] -> SBVCodeGen ()
    cgAddDecl ss :: [String]
    ss = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgDecls :: [String]
    cgDecls = CgState -> [String]
    cgDecls CgState
    s [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    ss })

    -- | Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.
    cgAddLDFlags :: [String] -> SBVCodeGen ()
    cgAddLDFlags :: [String] -> SBVCodeGen ()
    cgAddLDFlags ss :: [String]
    ss = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgLDFlags :: [String]
    cgLDFlags = CgState -> [String]
    cgLDFlags CgState
    s [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    ss })

    -- | Creates an atomic input in the generated code.
    svCgInput :: Kind -> String -> SBVCodeGen SVal
    svCgInput :: Kind -> String -> SBVCodeGen SVal
    svCgInput k :: Kind
    k nm :: String
    nm = do SVal
    r  <- SBVCodeGen State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv SBVCodeGen State -> (State -> SBVCodeGen SVal) -> SBVCodeGen SVal
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SVal -> SBVCodeGen SVal
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SVal -> SBVCodeGen SVal)
    -> (State -> IO SVal) -> State -> SBVCodeGen SVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    ALL) Kind
    k Maybe String
    forall a. Maybe a
    Nothing
                        SV
    sv <- SVal -> SBVCodeGen SV
    forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
    svToSymSV SVal
    r
                        (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgInputs :: [(String, CgVal)]
    cgInputs = (String
    nm, SV -> CgVal
    CgAtomic SV
    sv) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
    forall a. a -> [a] -> [a]
    : CgState -> [(String, CgVal)]
    cgInputs CgState
    s })
                        SVal -> SBVCodeGen SVal
    forall (m :: * -> *) a. Monad m => a -> m a
    return SVal
    r

    -- | Creates an array input in the generated code.
    svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
    svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
    svCgInputArr k :: Kind
    k sz :: Int
    sz nm :: String
    nm
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < 1 = String -> SBVCodeGen [SVal]
    forall a. HasCallStack => String -> a
    error (String -> SBVCodeGen [SVal]) -> String -> SBVCodeGen [SVal]
    forall a b. (a -> b) -> a -> b
    $ "SBV.cgInputArr: Array inputs must have at least one element, given " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    sz String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm
      | Bool
    True   = do [SVal]
    rs  <- SBVCodeGen State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv SBVCodeGen State
    -> (State -> SBVCodeGen [SVal]) -> SBVCodeGen [SVal]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO [SVal] -> SBVCodeGen [SVal]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [SVal] -> SBVCodeGen [SVal])
    -> (State -> IO [SVal]) -> State -> SBVCodeGen [SVal]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> IO SVal -> IO [SVal]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    sz (IO SVal -> IO [SVal]) -> (State -> IO SVal) -> State -> IO [SVal]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
    svMkSymVar (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    ALL) Kind
    k Maybe String
    forall a. Maybe a
    Nothing
                    [SV]
    sws <- (SVal -> SBVCodeGen SV) -> [SVal] -> SBVCodeGen [SV]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM SVal -> SBVCodeGen SV
    forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
    svToSymSV [SVal]
    rs
                    (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgInputs :: [(String, CgVal)]
    cgInputs = (String
    nm, [SV] -> CgVal
    CgArray [SV]
    sws) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
    forall a. a -> [a] -> [a]
    : CgState -> [(String, CgVal)]
    cgInputs CgState
    s })
                    [SVal] -> SBVCodeGen [SVal]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SVal]
    rs

    -- | Creates an atomic output in the generated code.
    svCgOutput :: String -> SVal -> SBVCodeGen ()
    svCgOutput :: String -> SVal -> SBVCodeGen ()
    svCgOutput nm :: String
    nm v :: SVal
    v = do ()
    _ <- SVal -> SBVCodeGen ()
    forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
    outputSVal SVal
    v
                         SV
    sv <- SVal -> SBVCodeGen SV
    forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
    svToSymSV SVal
    v
                         (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgOutputs :: [(String, CgVal)]
    cgOutputs = (String
    nm, SV -> CgVal
    CgAtomic SV
    sv) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
    forall a. a -> [a] -> [a]
    : CgState -> [(String, CgVal)]
    cgOutputs CgState
    s })

    -- | Creates an array output in the generated code.
    svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
    svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
    svCgOutputArr nm :: String
    nm vs :: [SVal]
    vs
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < 1 = String -> SBVCodeGen ()
    forall a. HasCallStack => String -> a
    error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
    forall a b. (a -> b) -> a -> b
    $ "SBV.cgOutputArr: Array outputs must have at least one element, received " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    sz String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm
      | Bool
    True   = do (SVal -> SBVCodeGen ()) -> [SVal] -> SBVCodeGen ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ SVal -> SBVCodeGen ()
    forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
    outputSVal [SVal]
    vs
                    [SV]
    sws <- (SVal -> SBVCodeGen SV) -> [SVal] -> SBVCodeGen [SV]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM SVal -> SBVCodeGen SV
    forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
    svToSymSV [SVal]
    vs
                    (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgOutputs :: [(String, CgVal)]
    cgOutputs = (String
    nm, [SV] -> CgVal
    CgArray [SV]
    sws) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
    forall a. a -> [a] -> [a]
    : CgState -> [(String, CgVal)]
    cgOutputs CgState
    s })
      where sz :: Int
    sz = [SVal] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SVal]
    vs

    -- | Creates a returned (unnamed) value in the generated code.
    svCgReturn :: SVal -> SBVCodeGen ()
    svCgReturn :: SVal -> SBVCodeGen ()
    svCgReturn v :: SVal
    v = do ()
    _ <- SVal -> SBVCodeGen ()
    forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
    outputSVal SVal
    v
                      SV
    sv <- SVal -> SBVCodeGen SV
    forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
    svToSymSV SVal
    v
                      (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgReturns :: [CgVal]
    cgReturns = SV -> CgVal
    CgAtomic SV
    sv CgVal -> [CgVal] -> [CgVal]
    forall a. a -> [a] -> [a]
    : CgState -> [CgVal]
    cgReturns CgState
    s })

    -- | Creates a returned (unnamed) array value in the generated code.
    svCgReturnArr :: [SVal] -> SBVCodeGen ()
    svCgReturnArr :: [SVal] -> SBVCodeGen ()
    svCgReturnArr vs :: [SVal]
    vs
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < 1 = String -> SBVCodeGen ()
    forall a. HasCallStack => String -> a
    error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
    forall a b. (a -> b) -> a -> b
    $ "SBV.cgReturnArr: Array returns must have at least one element, received " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    sz
      | Bool
    True   = do (SVal -> SBVCodeGen ()) -> [SVal] -> SBVCodeGen ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ SVal -> SBVCodeGen ()
    forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
    outputSVal [SVal]
    vs
                    [SV]
    sws <- (SVal -> SBVCodeGen SV) -> [SVal] -> SBVCodeGen [SV]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM SVal -> SBVCodeGen SV
    forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
    svToSymSV [SVal]
    vs
                    (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgReturns :: [CgVal]
    cgReturns = [SV] -> CgVal
    CgArray [SV]
    sws CgVal -> [CgVal] -> [CgVal]
    forall a. a -> [a] -> [a]
    : CgState -> [CgVal]
    cgReturns CgState
    s })
      where sz :: Int
    sz = [SVal] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SVal]
    vs

    -- | Creates an atomic input in the generated code.
    cgInput :: SymVal a => String -> SBVCodeGen (SBV a)
    cgInput :: String -> SBVCodeGen (SBV a)
    cgInput nm :: String
    nm = do SBV a
    r <- SBVCodeGen (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    forall_
                    SV
    sv <- SBV a -> SBVCodeGen SV
    forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
    sbvToSymSV SBV a
    r
                    (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgInputs :: [(String, CgVal)]
    cgInputs = (String
    nm, SV -> CgVal
    CgAtomic SV
    sv) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
    forall a. a -> [a] -> [a]
    : CgState -> [(String, CgVal)]
    cgInputs CgState
    s })
                    SBV a -> SBVCodeGen (SBV a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBV a
    r

    -- | Creates an array input in the generated code.
    cgInputArr :: SymVal a => Int -> String -> SBVCodeGen [SBV a]
    cgInputArr :: Int -> String -> SBVCodeGen [SBV a]
    cgInputArr sz :: Int
    sz nm :: String
    nm
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < 1 = String -> SBVCodeGen [SBV a]
    forall a. HasCallStack => String -> a
    error (String -> SBVCodeGen [SBV a]) -> String -> SBVCodeGen [SBV a]
    forall a b. (a -> b) -> a -> b
    $ "SBV.cgInputArr: Array inputs must have at least one element, given " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    sz String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm
      | Bool
    True   = do [SBV a]
    rs <- (Int -> SBVCodeGen (SBV a)) -> [Int] -> SBVCodeGen [SBV a]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (SBVCodeGen (SBV a) -> Int -> SBVCodeGen (SBV a)
    forall a b. a -> b -> a
    const SBVCodeGen (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    forall_) [1..Int
    sz]
                    [SV]
    sws <- (SBV a -> SBVCodeGen SV) -> [SBV a] -> SBVCodeGen [SV]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM SBV a -> SBVCodeGen SV
    forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
    sbvToSymSV [SBV a]
    rs
                    (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgInputs :: [(String, CgVal)]
    cgInputs = (String
    nm, [SV] -> CgVal
    CgArray [SV]
    sws) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
    forall a. a -> [a] -> [a]
    : CgState -> [(String, CgVal)]
    cgInputs CgState
    s })
                    [SBV a] -> SBVCodeGen [SBV a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SBV a]
    rs

    -- | Creates an atomic output in the generated code.
    cgOutput :: String -> SBV a -> SBVCodeGen ()
    cgOutput :: String -> SBV a -> SBVCodeGen ()
    cgOutput nm :: String
    nm v :: SBV a
    v = do SBV a
    _ <- SBV a -> SBVCodeGen (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output SBV a
    v
                       SV
    sv <- SBV a -> SBVCodeGen SV
    forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
    sbvToSymSV SBV a
    v
                       (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgOutputs :: [(String, CgVal)]
    cgOutputs = (String
    nm, SV -> CgVal
    CgAtomic SV
    sv) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
    forall a. a -> [a] -> [a]
    : CgState -> [(String, CgVal)]
    cgOutputs CgState
    s })

    -- | Creates an array output in the generated code.
    cgOutputArr :: SymVal a => String -> [SBV a] -> SBVCodeGen ()
    cgOutputArr :: String -> [SBV a] -> SBVCodeGen ()
    cgOutputArr nm :: String
    nm vs :: [SBV a]
    vs
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < 1 = String -> SBVCodeGen ()
    forall a. HasCallStack => String -> a
    error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
    forall a b. (a -> b) -> a -> b
    $ "SBV.cgOutputArr: Array outputs must have at least one element, received " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    sz String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm
      | Bool
    True   = do (SBV a -> SBVCodeGen (SBV a)) -> [SBV a] -> SBVCodeGen ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ SBV a -> SBVCodeGen (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output [SBV a]
    vs
                    [SV]
    sws <- (SBV a -> SBVCodeGen SV) -> [SBV a] -> SBVCodeGen [SV]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM SBV a -> SBVCodeGen SV
    forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
    sbvToSymSV [SBV a]
    vs
                    (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgOutputs :: [(String, CgVal)]
    cgOutputs = (String
    nm, [SV] -> CgVal
    CgArray [SV]
    sws) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
    forall a. a -> [a] -> [a]
    : CgState -> [(String, CgVal)]
    cgOutputs CgState
    s })
      where sz :: Int
    sz = [SBV a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SBV a]
    vs

    -- | Creates a returned (unnamed) value in the generated code.
    cgReturn :: SBV a -> SBVCodeGen ()
    cgReturn :: SBV a -> SBVCodeGen ()
    cgReturn v :: SBV a
    v = do SBV a
    _ <- SBV a -> SBVCodeGen (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output SBV a
    v
                    SV
    sv <- SBV a -> SBVCodeGen SV
    forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
    sbvToSymSV SBV a
    v
                    (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgReturns :: [CgVal]
    cgReturns = SV -> CgVal
    CgAtomic SV
    sv CgVal -> [CgVal] -> [CgVal]
    forall a. a -> [a] -> [a]
    : CgState -> [CgVal]
    cgReturns CgState
    s })

    -- | Creates a returned (unnamed) array value in the generated code.
    cgReturnArr :: SymVal a => [SBV a] -> SBVCodeGen ()
    cgReturnArr :: [SBV a] -> SBVCodeGen ()
    cgReturnArr vs :: [SBV a]
    vs
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < 1 = String -> SBVCodeGen ()
    forall a. HasCallStack => String -> a
    error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
    forall a b. (a -> b) -> a -> b
    $ "SBV.cgReturnArr: Array returns must have at least one element, received " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    sz
      | Bool
    True   = do (SBV a -> SBVCodeGen (SBV a)) -> [SBV a] -> SBVCodeGen ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ SBV a -> SBVCodeGen (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output [SBV a]
    vs
                    [SV]
    sws <- (SBV a -> SBVCodeGen SV) -> [SBV a] -> SBVCodeGen [SV]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM SBV a -> SBVCodeGen SV
    forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
    sbvToSymSV [SBV a]
    vs
                    (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\s :: CgState
    s -> CgState
    s { cgReturns :: [CgVal]
    cgReturns = [SV] -> CgVal
    CgArray [SV]
    sws CgVal -> [CgVal] -> [CgVal]
    forall a. a -> [a] -> [a]
    : CgState -> [CgVal]
    cgReturns CgState
    s })
      where sz :: Int
    sz = [SBV a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SBV a]
    vs

    -- | Representation of a collection of generated programs.
    data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))]

    -- | Different kinds of "files" we can produce. Currently this is quite "C" specific.
    data CgPgmKind = CgMakefile [String]  -- list of flags to pass to linker
                   | CgHeader [Doc]
                   | CgSource
                   | CgDriver

    -- | Is this a driver program?
    isCgDriver :: CgPgmKind -> Bool
    isCgDriver :: CgPgmKind -> Bool
    isCgDriver CgDriver = Bool
    True
    isCgDriver _        = Bool
    False

    -- | Is this a make file?
    isCgMakefile :: CgPgmKind -> Bool
    isCgMakefile :: CgPgmKind -> Bool
    isCgMakefile CgMakefile{} = Bool
    True
    isCgMakefile _            = Bool
    False

    -- A simple way to print bundles, mostly for debugging purposes.
    instance Show CgPgmBundle where
       show :: CgPgmBundle -> String
    show (CgPgmBundle _ fs :: [(String, (CgPgmKind, [Doc]))]
    fs) = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ ((String, (CgPgmKind, [Doc])) -> String)
    -> [(String, (CgPgmKind, [Doc]))] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, (CgPgmKind, [Doc])) -> String
    showFile [(String, (CgPgmKind, [Doc]))]
    fs
        where showFile :: (FilePath, (CgPgmKind, [Doc])) -> String
              showFile :: (String, (CgPgmKind, [Doc])) -> String
    showFile (f :: String
    f, (_, ds :: [Doc]
    ds)) =  "== BEGIN: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    f String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " ================\n"
                                    String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    render' ([Doc] -> Doc
    vcat [Doc]
    ds)
                                    String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "== END: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    f String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " =================="

    -- | Generate code for a symbolic program, returning a Code-gen bundle, i.e., collection
    -- of makefiles, source code, headers, etc.
    codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
    codeGen :: l
    -> CgConfig
    -> String
    -> SBVCodeGen a
    -> IO (a, CgConfig, CgPgmBundle)
    codeGen l :: l
    l cgConfig :: CgConfig
    cgConfig nm :: String
    nm (SBVCodeGen comp :: StateT CgState Symbolic a
    comp) = do
       ((retVal :: a
    retVal, st' :: CgState
    st'), res :: Result
    res) <- SBVRunMode
    -> SymbolicT IO (a, CgState) -> IO ((a, CgState), Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic SBVRunMode
    CodeGen (SymbolicT IO (a, CgState) -> IO ((a, CgState), Result))
    -> SymbolicT IO (a, CgState) -> IO ((a, CgState), Result)
    forall a b. (a -> b) -> a -> b
    $ StateT CgState Symbolic a -> CgState -> SymbolicT IO (a, CgState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT StateT CgState Symbolic a
    comp CgState
    initCgState { cgFinalConfig :: CgConfig
    cgFinalConfig = CgConfig
    cgConfig }
       let st :: CgState
    st = CgState
    st' { cgInputs :: [(String, CgVal)]
    cgInputs       = [(String, CgVal)] -> [(String, CgVal)]
    forall a. [a] -> [a]
    reverse (CgState -> [(String, CgVal)]
    cgInputs CgState
    st')
                    , cgOutputs :: [(String, CgVal)]
    cgOutputs      = [(String, CgVal)] -> [(String, CgVal)]
    forall a. [a] -> [a]
    reverse (CgState -> [(String, CgVal)]
    cgOutputs CgState
    st')
                    }
           allNamedVars :: [String]
    allNamedVars = ((String, CgVal) -> String) -> [(String, CgVal)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, CgVal) -> String
    forall a b. (a, b) -> a
    fst (CgState -> [(String, CgVal)]
    cgInputs CgState
    st [(String, CgVal)] -> [(String, CgVal)] -> [(String, CgVal)]
    forall a. [a] -> [a] -> [a]
    ++ CgState -> [(String, CgVal)]
    cgOutputs CgState
    st)
           dupNames :: [String]
    dupNames = [String]
    allNamedVars [String] -> [String] -> [String]
    forall a. Eq a => [a] -> [a] -> [a]
    \\ [String] -> [String]
    forall a. Eq a => [a] -> [a]
    nub [String]
    allNamedVars
       Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    dupNames) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $
            String -> IO ()
    forall a. HasCallStack => String -> a
    error (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "SBV.codeGen: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    nm String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " has following argument names duplicated: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    dupNames

       (a, CgConfig, CgPgmBundle) -> IO (a, CgConfig, CgPgmBundle)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    retVal, CgState -> CgConfig
    cgFinalConfig CgState
    st, l -> CgConfig -> String -> CgState -> Result -> CgPgmBundle
    forall a.
    CgTarget a =>
    a -> CgConfig -> String -> CgState -> Result -> CgPgmBundle
    translate l
    l (CgState -> CgConfig
    cgFinalConfig CgState
    st) String
    nm CgState
    st Result
    res)

    -- | Render a code-gen bundle to a directory or to stdout
    renderCgPgmBundle :: Maybe FilePath -> (CgConfig, CgPgmBundle) -> IO ()
    renderCgPgmBundle :: Maybe String -> (CgConfig, CgPgmBundle) -> IO ()
    renderCgPgmBundle Nothing        (_  , bundle :: CgPgmBundle
    bundle)              = CgPgmBundle -> IO ()
    forall a. Show a => a -> IO ()
    print CgPgmBundle
    bundle
    renderCgPgmBundle (Just dirName :: String
    dirName) (cfg :: CgConfig
    cfg, CgPgmBundle _ files :: [(String, (CgPgmKind, [Doc]))]
    files) = do

            Bool
    b <- String -> IO Bool
    doesDirectoryExist String
    dirName
            Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    b (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ do Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    overWrite (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "Creating directory " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    dirName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ".."
                          Bool -> String -> IO ()
    createDirectoryIfMissing Bool
    True String
    dirName

            [String]
    dups <- (String -> IO Bool) -> [String] -> IO [String]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM (\fn :: String
    fn -> String -> IO Bool
    doesFileExist (String
    dirName String -> String -> String
    </> String
    fn)) (((String, (CgPgmKind, [Doc])) -> String)
    -> [(String, (CgPgmKind, [Doc]))] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, (CgPgmKind, [Doc])) -> String
    forall a b. (a, b) -> a
    fst [(String, (CgPgmKind, [Doc]))]
    files)

            Bool
    goOn <- case (Bool
    overWrite, [String]
    dups) of
                      (True, _) -> Bool -> IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                      (_,   []) -> Bool -> IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                      _         -> do String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "Code generation would overwrite the following " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (if [String] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [String]
    dups Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 1 then "file:" else "files:")
                                      (String -> IO ()) -> [String] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (\fn :: String
    fn -> String -> IO ()
    putStrLn ('\t' Char -> String -> String
    forall a. a -> [a] -> [a]
    : String
    fn)) [String]
    dups
                                      String -> IO ()
    putStr "Continue? [yn] "
                                      Handle -> IO ()
    hFlush Handle
    stdout
                                      String
    resp <- IO String
    getLine
                                      Bool -> IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> IO Bool) -> Bool -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ (Char -> Char) -> String -> String
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> Char
    toLower String
    resp String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` "yes"

            if Bool
    goOn then do ((String, (CgPgmKind, [Doc])) -> IO ())
    -> [(String, (CgPgmKind, [Doc]))] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (String, (CgPgmKind, [Doc])) -> IO ()
    forall a. (String, (a, [Doc])) -> IO ()
    renderFile [(String, (CgPgmKind, [Doc]))]
    files
                            Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    overWrite (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn "Done."
                    else String -> IO ()
    putStrLn "Aborting."

      where overWrite :: Bool
    overWrite = CgConfig -> Bool
    cgOverwriteGenerated CgConfig
    cfg

            renderFile :: (String, (a, [Doc])) -> IO ()
    renderFile (f :: String
    f, (_, ds :: [Doc]
    ds)) = do let fn :: String
    fn = String
    dirName String -> String -> String
    </> String
    f
                                         Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    overWrite (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "Generating: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    fn String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ".."
                                         String -> String -> IO ()
    writeFile String
    fn (Doc -> String
    render' ([Doc] -> Doc
    vcat [Doc]
    ds))

    -- | An alternative to Pretty's @render@, which might have "leading" white-space in empty lines. This version
    -- eliminates such whitespace.
    render' :: Doc -> String
    render' :: Doc -> String
    render' = [String] -> String
    unlines ([String] -> String) -> (Doc -> [String]) -> Doc -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> String
    clean ([String] -> [String]) -> (Doc -> [String]) -> Doc -> [String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> [String]
    lines (String -> [String]) -> (Doc -> String) -> Doc -> [String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> String
    P.render
      where clean :: String -> String
    clean x :: String
    x | (Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    isSpace String
    x = ""
                    | Bool
    True          = String
    x