    -----------------------------------------------------------------------------
    -- |
    -- 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, VarContext(..))

    import Data.SBV.Provers.Prover(defaultSMTCfg)

    #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 { 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 -> [(FilePath, CgVal)]
    cgInputs         :: [(String, CgVal)]
            , CgState -> [(FilePath, CgVal)]
    cgOutputs        :: [(String, CgVal)]
            , CgState -> [CgVal]
    cgReturns        :: [CgVal]
            , CgState -> [FilePath]
    cgPrototypes     :: [String]    -- extra stuff that goes into the header
            , CgState -> [FilePath]
    cgDecls          :: [String]    -- extra stuff that goes into the top of the file
            , CgState -> [FilePath]
    cgLDFlags        :: [String]    -- extra options that go to the linker
            , CgState -> CgConfig
    cgFinalConfig    :: CgConfig
            }

    -- | Initial configuration for code-generation
    initCgState :: CgState
    initCgState :: CgState
    initCgState = CgState {
              cgInputs :: [(FilePath, CgVal)]
    cgInputs         = []
            , cgOutputs :: [(FilePath, CgVal)]
    cgOutputs        = []
            , cgReturns :: [CgVal]
    cgReturns        = []
            , cgPrototypes :: [FilePath]
    cgPrototypes     = []
            , cgDecls :: [FilePath]
    cgDecls          = []
            , cgLDFlags :: [FilePath]
    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
    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
    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
    $cpure :: forall a. a -> SBVCodeGen a
    pure :: forall a. a -> SBVCodeGen a
    $c<*> :: forall a b. SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
    <*> :: forall a b. SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
    $cliftA2 :: forall a b c.
    (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
    liftA2 :: forall a b c.
    (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
    $c*> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
    *> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
    $c<* :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
    <* :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
    Applicative, (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
    $cfmap :: forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b
    fmap :: forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b
    $c<$ :: forall a b. a -> SBVCodeGen b -> SBVCodeGen a
    <$ :: forall a b. a -> SBVCodeGen b -> SBVCodeGen a
    Functor, Applicative SBVCodeGen
    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
    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
    $c>>= :: forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
    >>= :: forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
    $c>> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
    >> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
    $creturn :: forall a. a -> SBVCodeGen a
    return :: forall a. a -> SBVCodeGen a
    Monad, Monad SBVCodeGen
    Monad SBVCodeGen =>
    (forall a. IO a -> SBVCodeGen a) -> MonadIO SBVCodeGen
    forall a. IO a -> SBVCodeGen a
    forall (m :: * -> *).
    Monad m =>
    (forall a. IO a -> m a) -> MonadIO m
    $cliftIO :: forall a. IO a -> SBVCodeGen a
    liftIO :: forall a. IO a -> SBVCodeGen a
    MonadIO, MonadState CgState
                                , MonadIO SBVCodeGen
    SBVCodeGen State
    MonadIO SBVCodeGen => SBVCodeGen State -> MonadSymbolic SBVCodeGen
    forall (m :: * -> *). MonadIO m => m State -> MonadSymbolic m
    $csymbolicEnv :: SBVCodeGen State
    symbolicEnv :: SBVCodeGen State
    MonadSymbolic
    #if MIN_VERSION_base(4,11,0)
                                , Monad SBVCodeGen
    Monad SBVCodeGen =>
    (forall a. FilePath -> SBVCodeGen a) -> MonadFail SBVCodeGen
    forall a. FilePath -> SBVCodeGen a
    forall (m :: * -> *).
    Monad m =>
    (forall a. FilePath -> m a) -> MonadFail m
    $cfail :: forall a. FilePath -> SBVCodeGen a
    fail :: forall a. FilePath -> SBVCodeGen a
    Fail.MonadFail
    #endif
                                )

    -- | Reach into symbolic monad from code-generation
    cgSym :: Symbolic a -> SBVCodeGen a
    cgSym :: forall a. 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 (m :: * -> *) a. Monad m => m a -> StateT CgState m 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 Bool
    b = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\CgState
    s -> CgState
    s { cgFinalConfig = (cgFinalConfig s) { cgRTC = 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 Int
    i
      | Int
    i Int -> [Int] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [Int
    8, Int
    16, Int
    32, Int
    64]
      = FilePath -> SBVCodeGen ()
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> SBVCodeGen ()) -> FilePath -> SBVCodeGen ()
    forall a b. (a -> b) -> a -> b
    $ FilePath
    "SBV.cgIntegerSize: Argument must be one of 8, 16, 32, or 64. Received: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    i
      | Bool
    True
      = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\CgState
    s -> CgState
    s { cgFinalConfig = (cgFinalConfig s) { cgInteger = Just 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
    $c== :: CgSRealType -> CgSRealType -> Bool
    == :: CgSRealType -> CgSRealType -> Bool
    $c/= :: CgSRealType -> CgSRealType -> Bool
    /= :: 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 -> FilePath
    show CgSRealType
    CgFloat      = FilePath
    "float"
      show CgSRealType
    CgDouble     = FilePath
    "double"
      show CgSRealType
    CgLongDouble = FilePath
    "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 CgSRealType
    rt = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\CgState
    s -> CgState
    s {cgFinalConfig = (cgFinalConfig s) { cgReal = Just rt }})

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

    -- | Should we generate a Makefile? Default: 'True'.
    cgGenerateMakefile :: Bool -> SBVCodeGen ()
    cgGenerateMakefile :: Bool -> SBVCodeGen ()
    cgGenerateMakefile Bool
    b = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\CgState
    s -> CgState
    s { cgFinalConfig = (cgFinalConfig s) { cgGenMakefile = 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 [Integer]
    vs = (CgState -> CgState) -> SBVCodeGen ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' (\CgState
    s -> CgState
    s { cgFinalConfig = (cgFinalConfig s) { cgDriverVals = vs } })

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

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

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

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

    -- | Creates an atomic input in the generated code.
    svCgInput :: Kind -> String -> SBVCodeGen SVal
    svCgInput :: Kind -> FilePath -> SBVCodeGen SVal
    svCgInput Kind
    k FilePath
    nm = do SVal
    r  <- SBVCodeGen State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv SBVCodeGen State -> (State -> SBVCodeGen SVal) -> SBVCodeGen SVal
    forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SVal -> SBVCodeGen SVal
    forall a. IO a -> SBVCodeGen a
    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
    . VarContext -> Kind -> Maybe FilePath -> State -> IO SVal
    svMkSymVar (Maybe Quantifier -> VarContext
    NonQueryVar (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    ALL)) Kind
    k Maybe FilePath
    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' (\CgState
    s -> CgState
    s { cgInputs = (nm, CgAtomic sv) : cgInputs s })
                        SVal -> SBVCodeGen SVal
    forall a. a -> SBVCodeGen a
    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 -> FilePath -> SBVCodeGen [SVal]
    svCgInputArr Kind
    k Int
    sz FilePath
    nm
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    1 = FilePath -> SBVCodeGen [SVal]
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> SBVCodeGen [SVal]) -> FilePath -> SBVCodeGen [SVal]
    forall a b. (a -> b) -> a -> b
    $ FilePath
    "SBV.cgInputArr: Array inputs must have at least one element, given " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    sz FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    " for " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    nm
      | Bool
    True   = do [SVal]
    rs  <- SBVCodeGen State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv SBVCodeGen State
    -> (State -> SBVCodeGen [SVal]) -> SBVCodeGen [SVal]
    forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO [SVal] -> SBVCodeGen [SVal]
    forall a. IO a -> SBVCodeGen a
    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
    . VarContext -> Kind -> Maybe FilePath -> State -> IO SVal
    svMkSymVar (Maybe Quantifier -> VarContext
    NonQueryVar (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    ALL)) Kind
    k Maybe FilePath
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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' (\CgState
    s -> CgState
    s { cgInputs = (nm, CgArray sws) : cgInputs s })
                    [SVal] -> SBVCodeGen [SVal]
    forall a. a -> SBVCodeGen a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SVal]
    rs

    -- | Creates an atomic output in the generated code.
    svCgOutput :: String -> SVal -> SBVCodeGen ()
    svCgOutput :: FilePath -> SVal -> SBVCodeGen ()
    svCgOutput FilePath
    nm 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' (\CgState
    s -> CgState
    s { cgOutputs = (nm, CgAtomic sv) : cgOutputs s })

    -- | Creates an array output in the generated code.
    svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
    svCgOutputArr :: FilePath -> [SVal] -> SBVCodeGen ()
    svCgOutputArr FilePath
    nm [SVal]
    vs
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    1 = FilePath -> SBVCodeGen ()
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> SBVCodeGen ()) -> FilePath -> SBVCodeGen ()
    forall a b. (a -> b) -> a -> b
    $ FilePath
    "SBV.cgOutputArr: Array outputs must have at least one element, received " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    sz FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    " for " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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' (\CgState
    s -> CgState
    s { cgOutputs = (nm, CgArray sws) : cgOutputs s })
      where sz :: Int
    sz = [SVal] -> Int
    forall a. [a] -> 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 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' (\CgState
    s -> CgState
    s { cgReturns = CgAtomic sv : cgReturns s })

    -- | Creates a returned (unnamed) array value in the generated code.
    svCgReturnArr :: [SVal] -> SBVCodeGen ()
    svCgReturnArr :: [SVal] -> SBVCodeGen ()
    svCgReturnArr [SVal]
    vs
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    1 = FilePath -> SBVCodeGen ()
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> SBVCodeGen ()) -> FilePath -> SBVCodeGen ()
    forall a b. (a -> b) -> a -> b
    $ FilePath
    "SBV.cgReturnArr: Array returns must have at least one element, received " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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' (\CgState
    s -> CgState
    s { cgReturns = CgArray sws : cgReturns s })
      where sz :: Int
    sz = [SVal] -> Int
    forall a. [a] -> 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 :: forall a. SymVal a => FilePath -> SBVCodeGen (SBV a)
    cgInput FilePath
    nm = do SBV a
    r  <- SBVCodeGen (SBV a)
    forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
    forall (m :: * -> *). MonadSymbolic m => m (SBV a)
    free_
                    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' (\CgState
    s -> CgState
    s { cgInputs = (nm, CgAtomic sv) : cgInputs s })
                    SBV a -> SBVCodeGen (SBV a)
    forall a. a -> SBVCodeGen 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 :: forall a. SymVal a => Int -> FilePath -> SBVCodeGen [SBV a]
    cgInputArr Int
    sz FilePath
    nm
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    1 = FilePath -> SBVCodeGen [SBV a]
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> SBVCodeGen [SBV a]) -> FilePath -> SBVCodeGen [SBV a]
    forall a b. (a -> b) -> a -> b
    $ FilePath
    "SBV.cgInputArr: Array inputs must have at least one element, given " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    sz FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    " for " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 (m :: * -> *). MonadSymbolic m => m (SBV a)
    free_) [Int
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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' (\CgState
    s -> CgState
    s { cgInputs = (nm, CgArray sws) : cgInputs s })
                    [SBV a] -> SBVCodeGen [SBV a]
    forall a. a -> SBVCodeGen 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 :: forall a. FilePath -> SBV a -> SBVCodeGen ()
    cgOutput FilePath
    nm SBV a
    v = do SBV a
    _ <- SBV a -> SBVCodeGen (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV 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' (\CgState
    s -> CgState
    s { cgOutputs = (nm, CgAtomic sv) : cgOutputs s })

    -- | Creates an array output in the generated code.
    cgOutputArr :: SymVal a => String -> [SBV a] -> SBVCodeGen ()
    cgOutputArr :: forall a. SymVal a => FilePath -> [SBV a] -> SBVCodeGen ()
    cgOutputArr FilePath
    nm [SBV a]
    vs
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    1 = FilePath -> SBVCodeGen ()
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> SBVCodeGen ()) -> FilePath -> SBVCodeGen ()
    forall a b. (a -> b) -> a -> b
    $ FilePath
    "SBV.cgOutputArr: Array outputs must have at least one element, received " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    show Int
    sz FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    " for " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    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
    forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV 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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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' (\CgState
    s -> CgState
    s { cgOutputs = (nm, CgArray sws) : cgOutputs s })
      where sz :: Int
    sz = [SBV a] -> Int
    forall a. [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 :: forall a. SBV a -> SBVCodeGen ()
    cgReturn SBV a
    v = do SBV a
    _ <- SBV a -> SBVCodeGen (SBV a)
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV 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' (\CgState
    s -> CgState
    s { cgReturns = CgAtomic sv : cgReturns s })

    -- | Creates a returned (unnamed) array value in the generated code.
    cgReturnArr :: SymVal a => [SBV a] -> SBVCodeGen ()
    cgReturnArr :: forall a. SymVal a => [SBV a] -> SBVCodeGen ()
    cgReturnArr [SBV a]
    vs
      | Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    1 = FilePath -> SBVCodeGen ()
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> SBVCodeGen ()) -> FilePath -> SBVCodeGen ()
    forall a b. (a -> b) -> a -> b
    $ FilePath
    "SBV.cgReturnArr: Array returns must have at least one element, received " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Int -> FilePath
    forall a. Show a => a -> FilePath
    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
    forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV 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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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' (\CgState
    s -> CgState
    s { cgReturns = CgArray sws : cgReturns s })
      where sz :: Int
    sz = [SBV a] -> Int
    forall a. [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 CgPgmKind
    CgDriver = Bool
    True
    isCgDriver CgPgmKind
    _        = Bool
    False

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

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

    -- | 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 :: forall l a.
    CgTarget l =>
    l
    -> CgConfig
    -> FilePath
    -> SBVCodeGen a
    -> IO (a, CgConfig, CgPgmBundle)
    codeGen l
    l CgConfig
    cgConfig FilePath
    nm (SBVCodeGen StateT CgState Symbolic a
    comp) = do
       ((a
    retVal, CgState
    st'), Result
    res) <- SMTConfig
    -> SBVRunMode
    -> SymbolicT IO (a, CgState)
    -> IO ((a, CgState), Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SMTConfig -> SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic SMTConfig
    defaultSMTCfg 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 }
       let st :: CgState
    st = CgState
    st' { cgInputs  = reverse (cgInputs st')
                    , cgOutputs = reverse (cgOutputs st')
                    }
           allNamedVars :: [FilePath]
    allNamedVars = ((FilePath, CgVal) -> FilePath)
    -> [(FilePath, CgVal)] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath, CgVal) -> FilePath
    forall a b. (a, b) -> a
    fst (CgState -> [(FilePath, CgVal)]
    cgInputs CgState
    st [(FilePath, CgVal)] -> [(FilePath, CgVal)] -> [(FilePath, CgVal)]
    forall a. [a] -> [a] -> [a]
    ++ CgState -> [(FilePath, CgVal)]
    cgOutputs CgState
    st)
           dupNames :: [FilePath]
    dupNames = [FilePath]
    allNamedVars [FilePath] -> [FilePath] -> [FilePath]
    forall a. Eq a => [a] -> [a] -> [a]
    \\ [FilePath] -> [FilePath]
    forall a. Eq a => [a] -> [a]
    nub [FilePath]
    allNamedVars
       Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([FilePath] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [FilePath]
    dupNames) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $
            FilePath -> IO ()
    forall a. HasCallStack => FilePath -> a
    error (FilePath -> IO ()) -> FilePath -> IO ()
    forall a b. (a -> b) -> a -> b
    $ FilePath
    "SBV.codeGen: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    nm FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    " has following argument names duplicated: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ [FilePath] -> FilePath
    unwords [FilePath]
    dupNames

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

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

            Bool
    b <- FilePath -> IO Bool
    doesDirectoryExist FilePath
    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
    $ FilePath -> IO ()
    putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
    forall a b. (a -> b) -> a -> b
    $ FilePath
    "Creating directory " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    dirName FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    ".."
                          Bool -> FilePath -> IO ()
    createDirectoryIfMissing Bool
    True FilePath
    dirName

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

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

            if Bool
    goOn then do ((FilePath, (CgPgmKind, [Doc])) -> IO ())
    -> [(FilePath, (CgPgmKind, [Doc]))] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (FilePath, (CgPgmKind, [Doc])) -> IO ()
    forall {a}. (FilePath, (a, [Doc])) -> IO ()
    renderFile [(FilePath, (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
    $ FilePath -> IO ()
    putStrLn FilePath
    "Done."
                    else FilePath -> IO ()
    putStrLn FilePath
    "Aborting."

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

            renderFile :: (FilePath, (a, [Doc])) -> IO ()
    renderFile (FilePath
    f, (a
    _, [Doc]
    ds)) = do let fn :: FilePath
    fn = FilePath
    dirName FilePath -> FilePath -> FilePath
    </> FilePath
    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
    $ FilePath -> IO ()
    putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
    forall a b. (a -> b) -> a -> b
    $ FilePath
    "Generating: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    fn FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    ".."
                                         FilePath -> FilePath -> IO ()
    writeFile FilePath
    fn (Doc -> FilePath
    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 -> FilePath
    render' = [FilePath] -> FilePath
    unlines ([FilePath] -> FilePath) -> (Doc -> [FilePath]) -> Doc -> FilePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (FilePath -> FilePath) -> [FilePath] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map FilePath -> FilePath
    clean ([FilePath] -> [FilePath])
    -> (Doc -> [FilePath]) -> Doc -> [FilePath]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FilePath -> [FilePath]
    lines (FilePath -> [FilePath]) -> (Doc -> FilePath) -> Doc -> [FilePath]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> FilePath
    P.render
      where clean :: FilePath -> FilePath
    clean FilePath
    x | (Char -> Bool) -> FilePath -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    isSpace FilePath
    x = FilePath
    ""
                    | Bool
    True          = FilePath
    x