-----------------------------------------------------------------------------
-- |
-- 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 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 <- svToSymSV r
                    modify' (\CgState
s -> CgState
s { cgInputs = (nm, CgAtomic sv) : cgInputs s })
                    return 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 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
                sws <- mapM svToSymSV rs
                modify' (\CgState
s -> CgState
s { cgInputs = (nm, CgArray sws) : cgInputs s })
                return 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 <- svToSymSV v
                     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
                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
                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 <- svToSymSV v
                  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
                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
                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 r  <- SBVCodeGen (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall (m :: * -> *). MonadSymbolic m => m (SBV a)
free_
                sv <- sbvToSymSV r
                modify' (\CgState
s -> CgState
s { cgInputs = (nm, CgAtomic sv) : cgInputs s })
                return 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 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]
                sws <- mapM sbvToSymSV rs
                modify' (\CgState
s -> CgState
s { cgInputs = (nm, CgArray sws) : cgInputs s })
                return 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 -> 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 <- sbvToSymSV v
                   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
                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
                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 -> 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 <- sbvToSymSV v
                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
                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
                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
   ((retVal, st'), 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' { cgInputs  = reverse (cgInputs st')
                , cgOutputs = reverse (cgOutputs st')
                }
       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]
allNamedVars [FilePath] -> [FilePath] -> [FilePath]
forall a. Eq a => [a] -> [a] -> [a]
\\ [FilePath] -> [FilePath]
forall a. Eq a => [a] -> [a]
nub [FilePath]
allNamedVars
   unless (null dupNames) $
        error $ "SBV.codeGen: " ++ show nm ++ " has following argument names duplicated: " ++ unwords dupNames

   return (retVal, cgFinalConfig st, translate l (cgFinalConfig st) nm st 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

        b <- FilePath -> IO Bool
doesDirectoryExist FilePath
dirName
        unless b $ do unless overWrite $ putStrLn $ "Creating directory " ++ show dirName ++ ".."
                      createDirectoryIfMissing True dirName

        dups <- filterM (\FilePath
fn -> FilePath -> IO Bool
doesFileExist (FilePath
dirName FilePath -> FilePath -> FilePath
</> FilePath
fn)) (map fst files)

        goOn <- case (overWrite, 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
                                  resp <- IO FilePath
getLine
                                  return $ map toLower resp `isPrefixOf` "yes"

        if goOn then do mapM_ renderFile files
                        unless overWrite $ putStrLn "Done."
                else putStrLn "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