sbv-14.8: Data/SBV/Compilers/CodeGen.hs
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Compilers.CodeGen
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Code generation utilities
-----------------------------------------------------------------------------
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternSynonyms #-}
{-# 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, cgArrayEqualityLimit, cgRegexLimits
, CgRegexLimits(..), defaultCgRegexLimits, cgSetRegexLimits
, cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert, cgOverwriteFiles, cgShowU8UsingHex
, cgIntegerSize, cgSRealType, CgSRealType(..)
-- * Infrastructure
, CgTarget(..), CgConfig(..), CgState(..), CgPgmBundle(..)
, CgPgmKind(CgMakefile, CgHeader, CgCHeader, CgSource, CgDriver), CgCHeader(..), 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(..), addNewSMTOption, imposeConstraint, newInternalVariable, outputSVal, svMkSymVar, svToSymSV, VarContext(..))
import Data.SBV.Provers.Prover(defaultSMTCfg)
-- | 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 {
cgRTC :: Bool -- ^ If 'True', check finite table indices and select the supplied default when out of bounds.
, cgInteger :: Maybe Int -- ^ Optional lossy bit-size for representing SInteger; 'Nothing' selects exact GMP integers
, cgReal :: Maybe CgSRealType -- ^ Optional lossy representation for SReal; 'Nothing' selects exact GMP rationals
, cgDriverVals :: [Integer] -- ^ Values to use for the driver program generated, useful for generating non-random drivers.
, cgGenDriver :: Bool -- ^ If 'True', will generate a driver program
, cgGenMakefile :: Bool -- ^ If 'True', will generate a makefile
, cgIgnoreAsserts :: Bool -- ^ If 'True', will ignore 'Data.SBV.sAssert' calls
, cgOverwriteGenerated :: Bool -- ^ If 'True', will overwrite the generated files without prompting.
, cgShowU8InHex :: Bool -- ^ If 'True', then 8-bit unsigned values will be shown in hex as well, otherwise decimal. (Other types always shown in hex.)
, cgArrayEqualityMaxKeys :: Integer -- ^ Maximum key-domain size for exhaustive array equality in the current C backend.
, cgRegexMaxStates :: Integer -- ^ Maximum states explored per regex membership or language comparison.
, cgRegexMaxNodes :: Integer -- ^ Maximum nodes in a regex expression, including intermediate derivatives.
, cgRegexMaxWork :: Integer -- ^ Maximum charged generation work per regex operation; not a runtime input bound.
}
-- | Default options for code generation. Run-time checks are disabled, driver
-- values are random, and any 'SInteger' or rational 'SReal' values use exact
-- GMP representations.
defaultCgConfig :: CgConfig
defaultCgConfig = CgConfig { cgRTC = False
, cgInteger = Nothing
, cgReal = Nothing
, cgDriverVals = []
, cgGenDriver = True
, cgGenMakefile = True
, cgIgnoreAsserts = False
, cgOverwriteGenerated = False
, cgShowU8InHex = False
, cgArrayEqualityMaxKeys = 256
, cgRegexMaxStates = 1024
, cgRegexMaxNodes = 4096
, cgRegexMaxWork = 16000000
}
-- | Abstraction of target language values
data CgVal = CgAtomic SV
| CgArray [SV]
-- | Code-generation state
data CgState = CgState {
cgInputs :: [(String, CgVal)]
, cgOutputs :: [(String, CgVal)]
, cgReturns :: [CgVal]
, cgPrototypes :: [String] -- extra stuff that goes into the header
, cgDecls :: [String] -- extra stuff that goes into the top of the file
, cgLDFlags :: [String] -- extra options that go to the linker
, cgFinalConfig :: CgConfig
}
-- | Initial configuration for code-generation
initCgState :: CgState
initCgState = CgState {
cgInputs = []
, cgOutputs = []
, cgReturns = []
, cgPrototypes = []
, cgDecls = []
, cgLDFlags = []
, cgFinalConfig = 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 ( Applicative, Functor, Monad, MonadIO, MonadState CgState
, MonadSymbolic
, MonadFail
)
-- | Code-generation computations support hard symbolic constraints. Target
-- backends decide which constraint variants have executable semantics.
instance SolverContext SBVCodeGen where
constrain = imposeConstraint False [] . unSBV . quantifiedBool
softConstrain = imposeConstraint True [] . unSBV . quantifiedBool
namedConstraint nm = imposeConstraint False [(":named", nm)] . unSBV . quantifiedBool
constrainWithAttribute attrs = imposeConstraint False attrs . unSBV . quantifiedBool
contextState = symbolicEnv
setOption = addNewSMTOption
internalVariable kind = do
state <- contextState
sv <- liftIO $ newInternalVariable state kind
pure $ SBV $ SVal kind $ Right $ cache $ const $ pure sv
-- | Reach into symbolic monad from code-generation
cgSym :: Symbolic a -> SBVCodeGen a
cgSym = SBVCodeGen . lift
-- | Enable bounds checks for finite table selection. Out-of-range indices
-- select the supplied default. With checks disabled (the default), callers
-- must guarantee in-range indices. This setting does not disable assertions,
-- executable constraints, ownership checks, or exact bit-vector shift
-- semantics in the current C backend. Wide bit-vector and GMP indices always
-- retain their bounds check before conversion to a machine index.
cgPerformRTCs :: Bool -> SBVCodeGen ()
cgPerformRTCs b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgRTC = b } })
-- | Set the maximum number of keys enumerated by an array equality comparison
-- in the current C backend. The default is 256. Larger or infinite domains
-- are rejected during generation; equality is never approximated. Zero
-- disables exhaustive array equality. Negative limits are invalid.
--
-- For example, @cgArrayEqualityLimit 65536@ permits comparing arrays indexed
-- by 'SWord16', at the cost of up to 65,536 lookups in each array per comparison.
-- The setting also applies inside generated defined functions and array lambdas.
--
-- >>> import Data.SBV
-- >>> import Data.SBV.Internals (compileToC')
-- >>> :{
-- let compareArrays = do
-- cgArrayEqualityLimit 65536
-- left <- cgInput "left" :: SBVCodeGen (SArray Word16 Word8)
-- right <- cgInput "right" :: SBVCodeGen (SArray Word16 Word8)
-- cgReturn (left .== right)
-- :}
--
-- >>> (_, _, generated) <- compileToC' "compareArrays" compareArrays
-- >>> length (show generated) `seq` pure ()
cgArrayEqualityLimit :: Integer -> SBVCodeGen ()
cgArrayEqualityLimit limit
| limit < 0 = error "SBV.cgArrayEqualityLimit: The limit must be nonnegative."
| True = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgArrayEqualityMaxKeys = limit } })
-- | Bound dependency-free C regex compilation: maximum explored states,
-- expression nodes, and generation work, respectively. Defaults are 1024,
-- 4096, and 16000000. Exceeding a budget fails during generation, never by
-- approximating the language or limiting runtime input length. Zero disables
-- regex compilation; negative limits are invalid. Limits apply independently
-- to each operation, also inside defined functions and library components.
--
-- For example, @cgRegexLimits 4096 8192 64000000@ permits larger automata and
-- intermediate expressions, at the cost of more generation time and memory.
-- See "Data.SBV.Tools.CodeGen" for an executable generation example.
cgRegexLimits :: Integer -> Integer -> Integer -> SBVCodeGen ()
cgRegexLimits states nodes work
| any (< 0) [states, nodes, work] = error "SBV.cgRegexLimits: Limits must be nonnegative."
| True = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgRegexMaxStates = states
, cgRegexMaxNodes = nodes
, cgRegexMaxWork = work
} })
-- | Named limits for dependency-free regex compilation. Work is a conservative
-- generation allowance, not a promise that every smaller automaton will fit.
data CgRegexLimits = CgRegexLimits
{ regexMaxStates :: Integer -- ^ Maximum explored automaton states.
, regexMaxNodes :: Integer -- ^ Maximum nodes per intermediate expression.
, regexMaxWork :: Integer -- ^ Maximum charged construction work.
} deriving (Eq, Show)
-- | The default regex budgets, suitable for record updates.
defaultCgRegexLimits :: CgRegexLimits
defaultCgRegexLimits = CgRegexLimits (cgRegexMaxStates defaultCgConfig)
(cgRegexMaxNodes defaultCgConfig)
(cgRegexMaxWork defaultCgConfig)
-- | Configure regex budgets using named fields. The positional 'cgRegexLimits'
-- remains available for compatibility.
--
-- >>> let larger = defaultCgRegexLimits { regexMaxStates = 4096, regexMaxWork = 64000000 }
-- >>> regexMaxNodes larger == regexMaxNodes defaultCgRegexLimits
-- True
cgSetRegexLimits :: CgRegexLimits -> SBVCodeGen ()
cgSetRegexLimits limits = cgRegexLimits (regexMaxStates limits) (regexMaxNodes limits) (regexMaxWork limits)
-- | 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. Without this setting, generated C uses
-- exact GMP integers in the current backend. The Legacy backend instead rejects
-- SInteger programs unless this mapping is specified.
cgIntegerSize :: Int -> SBVCodeGen ()
cgIntegerSize i
| i `notElem` [8, 16, 32, 64]
= error $ "SBV.cgIntegerSize: Argument must be one of 8, 16, 32, or 64. Received: " ++ show i
| True
= modify' (\s -> 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 Eq
-- 'Show' instance for 'cgSRealType' displays values as they would be used in a C program
instance Show CgSRealType where
show CgFloat = "float"
show CgDouble = "double"
show CgLongDouble = "long double"
-- | Sets the C type to be used for representing the 'SReal' type in the generated C code.
-- The setting can be one of C's @"float"@, @"double"@, or @"long double"@, types, depending
-- on the precision needed. Note that this is essentially unsafe as the semantics of
-- infinite precision SReal values becomes reduced to the corresponding floating point type in
-- C, and hence it is subject to rounding errors. Without this setting,
-- generated C uses exact GMP rationals for rational-valued computations in the
-- current backend. The Legacy backend requires an explicit mapping instead.
cgSRealType :: CgSRealType -> SBVCodeGen ()
cgSRealType rt = modify' (\s -> 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 b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgGenDriver = b } })
-- | Should we generate a Makefile? Default: 'True'.
cgGenerateMakefile :: Bool -> SBVCodeGen ()
cgGenerateMakefile b = modify' (\s -> 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 vs = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgDriverVals = vs } })
-- | Ignore assertions (those generated by 'Data.SBV.sAssert' calls) in the generated C code
cgIgnoreSAssert :: Bool -> SBVCodeGen ()
cgIgnoreSAssert b = modify' (\s -> 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 ss = modify' (\s -> let old = cgPrototypes s
new = if null old then ss else old ++ [""] ++ ss
in 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 b = modify' (\s -> 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 b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgShowU8InHex = b } })
-- | Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.
-- External implementations must represent pure mathematical functions: their
-- results must depend only on their arguments, with no observable side effects.
-- The compiler may eliminate unused calls or share equal applications.
cgAddDecl :: [String] -> SBVCodeGen ()
cgAddDecl ss = modify' (\s -> 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 ss = modify' (\s -> s { cgLDFlags = cgLDFlags s ++ ss })
-- | Creates an atomic input in the generated code.
svCgInput :: Kind -> String -> SBVCodeGen SVal
svCgInput k nm = do r <- symbolicEnv >>= liftIO . svMkSymVar (NonQueryVar (Just ALL)) k Nothing
sv <- svToSymSV r
modify' (\s -> s { cgInputs = (nm, CgAtomic sv) : cgInputs s })
pure r
-- | Creates an array input in the generated code.
svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
svCgInputArr k sz nm
| sz < 1 = error $ "SBV.cgInputArr: Array inputs must have at least one element, given " ++ show sz ++ " for " ++ show nm
| True = do rs <- symbolicEnv >>= liftIO . replicateM sz . svMkSymVar (NonQueryVar (Just ALL)) k Nothing
sws <- mapM svToSymSV rs
modify' (\s -> s { cgInputs = (nm, CgArray sws) : cgInputs s })
pure rs
-- | Creates an atomic output in the generated code.
svCgOutput :: String -> SVal -> SBVCodeGen ()
svCgOutput nm v = do _ <- outputSVal v
sv <- svToSymSV v
modify' (\s -> s { cgOutputs = (nm, CgAtomic sv) : cgOutputs s })
-- | Creates an array output in the generated code.
svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
svCgOutputArr nm vs
| sz < 1 = error $ "SBV.cgOutputArr: Array outputs must have at least one element, received " ++ show sz ++ " for " ++ show nm
| True = do mapM_ outputSVal vs
sws <- mapM svToSymSV vs
modify' (\s -> s { cgOutputs = (nm, CgArray sws) : cgOutputs s })
where sz = length vs
-- | Creates a returned (unnamed) value in the generated code.
svCgReturn :: SVal -> SBVCodeGen ()
svCgReturn v = do _ <- outputSVal v
sv <- svToSymSV v
modify' (\s -> s { cgReturns = CgAtomic sv : cgReturns s })
-- | Creates a returned (unnamed) array value in the generated code.
svCgReturnArr :: [SVal] -> SBVCodeGen ()
svCgReturnArr vs
| sz < 1 = error $ "SBV.cgReturnArr: Array returns must have at least one element, received " ++ show sz
| True = do mapM_ outputSVal vs
sws <- mapM svToSymSV vs
modify' (\s -> s { cgReturns = CgArray sws : cgReturns s })
where sz = length vs
-- | Creates an atomic input in the generated code.
cgInput :: SymVal a => String -> SBVCodeGen (SBV a)
cgInput nm = do r <- free_
sv <- sbvToSymSV r
modify' (\s -> s { cgInputs = (nm, CgAtomic sv) : cgInputs s })
pure r
-- | Creates an array input in the generated code.
cgInputArr :: SymVal a => Int -> String -> SBVCodeGen [SBV a]
cgInputArr sz nm
| sz < 1 = error $ "SBV.cgInputArr: Array inputs must have at least one element, given " ++ show sz ++ " for " ++ show nm
| True = do rs <- mapM (const free_) [1..sz]
sws <- mapM sbvToSymSV rs
modify' (\s -> s { cgInputs = (nm, CgArray sws) : cgInputs s })
pure rs
-- | Creates an atomic output in the generated code.
cgOutput :: String -> SBV a -> SBVCodeGen ()
cgOutput nm v = do _ <- output v
sv <- sbvToSymSV v
modify' (\s -> s { cgOutputs = (nm, CgAtomic sv) : cgOutputs s })
-- | Creates an array output in the generated code.
cgOutputArr :: SymVal a => String -> [SBV a] -> SBVCodeGen ()
cgOutputArr nm vs
| sz < 1 = error $ "SBV.cgOutputArr: Array outputs must have at least one element, received " ++ show sz ++ " for " ++ show nm
| True = do mapM_ output vs
sws <- mapM sbvToSymSV vs
modify' (\s -> s { cgOutputs = (nm, CgArray sws) : cgOutputs s })
where sz = length vs
-- | Creates a returned (unnamed) value in the generated code.
cgReturn :: SBV a -> SBVCodeGen ()
cgReturn v = do _ <- output v
sv <- sbvToSymSV v
modify' (\s -> s { cgReturns = CgAtomic sv : cgReturns s })
-- | Creates a returned (unnamed) array value in the generated code.
cgReturnArr :: SymVal a => [SBV a] -> SBVCodeGen ()
cgReturnArr vs
| sz < 1 = error $ "SBV.cgReturnArr: Array returns must have at least one element, received " ++ show sz
| True = do mapM_ output vs
sws <- mapM sbvToSymSV vs
modify' (\s -> s { cgReturns = CgArray sws : cgReturns s })
where sz = length 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
| CgHeaderInternal [Doc] (Maybe CgCHeader)
| CgSource
| CgDriver
-- | Header signatures, as exposed by the original bundle interface. Matches
-- headers from both backends; construction produces a header without private
-- merge metadata. Existing four-way matches on 'CgPgmKind' remain exhaustive.
pattern CgHeader :: [Doc] -> CgPgmKind
pattern CgHeader signatures <- CgHeaderInternal signatures _
where CgHeader signatures = CgHeaderInternal signatures Nothing
-- | Structured metadata for current-backend header merging. This is a more
-- specific view of 'CgHeader', not an additional kind of generated file.
pattern CgCHeader :: CgCHeader -> CgPgmKind
pattern CgCHeader metadata <- CgHeaderInternal _ (Just metadata)
where CgCHeader metadata = CgHeaderInternal (cgHeaderSignatures metadata) (Just metadata)
{-# COMPLETE CgMakefile, CgHeader, CgSource, CgDriver #-}
-- | Structured C header metadata used when combining current-backend bundles.
-- 'CgHeader' provides the compatibility view for both backends.
data CgCHeader = CgCHeaderInfo
{ cgHeaderFloating :: Bool -- ^ Requires IEEE floating-point compilation.
, cgHeaderTypes :: Doc -- ^ Runtime type declarations.
, cgHeaderSignatures :: [Doc] -- ^ Public entry points.
, cgHeaderPrototypes :: Doc -- ^ User-supplied prototypes.
}
-- | Is this a driver program?
isCgDriver :: CgPgmKind -> Bool
isCgDriver CgDriver = True
isCgDriver _ = False
-- | Is this a make file?
isCgMakefile :: CgPgmKind -> Bool
isCgMakefile CgMakefile{} = True
isCgMakefile _ = False
-- A simple way to print bundles, mostly for debugging purposes.
instance Show CgPgmBundle where
show (CgPgmBundle _ fs) = intercalate "\n" $ map showFile fs
where showFile :: (FilePath, (CgPgmKind, [Doc])) -> String
showFile (f, (_, ds)) = "== BEGIN: " ++ show f ++ " ================\n"
++ render' (vcat ds)
++ "== END: " ++ show f ++ " =================="
-- | Generate code for a symbolic program, returning a Code-gen bundle, i.e., collection
-- of makefiles, source code, headers, etc.
codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
codeGen l cgConfig nm (SBVCodeGen comp) = do
((retVal, st'), res) <- runSymbolic defaultSMTCfg CodeGen $ runStateT comp initCgState { cgFinalConfig = cgConfig }
let st = st' { cgInputs = reverse (cgInputs st')
, cgOutputs = reverse (cgOutputs st')
, cgReturns = reverse (cgReturns st')
}
allNamedVars = map fst (cgInputs st ++ cgOutputs st)
dupNames = allNamedVars \\ nub allNamedVars
unless (null dupNames) $
error $ "SBV.codeGen: " ++ show nm ++ " has following argument names duplicated: " ++ unwords dupNames
pure (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 Nothing (_ , bundle) = print bundle
renderCgPgmBundle (Just dirName) (cfg, CgPgmBundle _ files) = do
b <- doesDirectoryExist dirName
unless b $ do unless overWrite $ putStrLn $ "Creating directory " ++ show dirName ++ ".."
createDirectoryIfMissing True dirName
dups <- filterM (\fn -> doesFileExist (dirName </> fn)) (map fst files)
goOn <- case (overWrite, dups) of
(True, _) -> pure True
(_, []) -> pure True
_ -> do putStrLn $ "Code generation would overwrite the following " ++ (if length dups == 1 then "file:" else "files:")
mapM_ (\fn -> putStrLn ('\t' : fn)) dups
putStr "Continue? [yn] "
hFlush stdout
resp <- getLine
pure $ map toLower resp `isPrefixOf` "yes"
if goOn then do mapM_ renderFile files
unless overWrite $ putStrLn "Done."
else putStrLn "Aborting."
where overWrite = cgOverwriteGenerated cfg
renderFile (f, (_, ds)) = do let fn = dirName </> f
unless overWrite $ putStrLn $ "Generating: " ++ show fn ++ ".."
writeFile fn (render' (vcat 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' = unlines . map clean . lines . P.render
where clean x | all isSpace x = ""
| True = x