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

#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            = forall a. Maybe a
Nothing
                           , cgReal :: Maybe CgSRealType
cgReal               = 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
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
<* :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
$c<* :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
*> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
$c*> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
liftA2 :: forall a b c.
(a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
$cliftA2 :: forall a b c.
(a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
<*> :: forall a b. SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
$c<*> :: forall a b. SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
pure :: forall a. a -> SBVCodeGen a
$cpure :: forall a. a -> SBVCodeGen a
Applicative, 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
<$ :: forall a b. a -> SBVCodeGen b -> SBVCodeGen a
$c<$ :: forall a b. a -> SBVCodeGen b -> SBVCodeGen a
fmap :: forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b
$cfmap :: forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b
Functor, Applicative 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
return :: forall a. a -> SBVCodeGen a
$creturn :: forall a. a -> SBVCodeGen a
>> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
$c>> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
>>= :: forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
$c>>= :: forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
Monad, Monad SBVCodeGen
forall a. IO a -> SBVCodeGen a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> SBVCodeGen a
$cliftIO :: forall a. IO a -> SBVCodeGen a
MonadIO, MonadState CgState
                            , MonadIO SBVCodeGen
SBVCodeGen State
forall (m :: * -> *). MonadIO m -> m State -> MonadSymbolic m
symbolicEnv :: SBVCodeGen State
$csymbolicEnv :: SBVCodeGen State
MonadSymbolic
#if MIN_VERSION_base(4,11,0)
                            , Monad SBVCodeGen
forall a. FilePath -> SBVCodeGen a
forall (m :: * -> *).
Monad m -> (forall a. FilePath -> m a) -> MonadFail m
fail :: forall a. FilePath -> SBVCodeGen a
$cfail :: 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 = forall a. StateT CgState Symbolic a -> SBVCodeGen a
SBVCodeGen forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgRTC :: Bool
cgRTC = Bool
b } })

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

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

-- 'Show' instance for 'cgSRealType' displays values as they would be used in a C program
instance Show CgSRealType where
  show :: CgSRealType -> 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 = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s {cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgReal :: Maybe CgSRealType
cgReal = forall a. a -> Maybe a
Just CgSRealType
rt }})

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

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

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

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

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

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


-- | Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.
cgAddDecl :: [String] -> SBVCodeGen ()
cgAddDecl :: [FilePath] -> SBVCodeGen ()
cgAddDecl [FilePath]
ss = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgDecls :: [FilePath]
cgDecls = CgState -> [FilePath]
cgDecls CgState
s forall a. [a] -> [a] -> [a]
++ [FilePath]
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 = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgLDFlags :: [FilePath]
cgLDFlags = CgState -> [FilePath]
cgLDFlags CgState
s forall a. [a] -> [a] -> [a]
++ [FilePath]
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  <- forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarContext -> Kind -> Maybe FilePath -> State -> IO SVal
svMkSymVar (Maybe Quantifier -> VarContext
NonQueryVar (forall a. a -> Maybe a
Just Quantifier
ALL)) Kind
k forall a. Maybe a
Nothing
                    SV
sv <- forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV SVal
r
                    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgInputs :: [(FilePath, CgVal)]
cgInputs = (FilePath
nm, SV -> CgVal
CgAtomic SV
sv) forall a. a -> [a] -> [a]
: CgState -> [(FilePath, CgVal)]
cgInputs CgState
s })
                    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 forall a. Ord a => a -> a -> Bool
< Int
1 = forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ FilePath
"SBV.cgInputArr: Array inputs must have at least one element, given " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show Int
sz forall a. [a] -> [a] -> [a]
++ FilePath
" for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show FilePath
nm
  | Bool
True   = do [SVal]
rs  <- forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
sz forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarContext -> Kind -> Maybe FilePath -> State -> IO SVal
svMkSymVar (Maybe Quantifier -> VarContext
NonQueryVar (forall a. a -> Maybe a
Just Quantifier
ALL)) Kind
k forall a. Maybe a
Nothing
                [SV]
sws <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV [SVal]
rs
                forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgInputs :: [(FilePath, CgVal)]
cgInputs = (FilePath
nm, [SV] -> CgVal
CgArray [SV]
sws) forall a. a -> [a] -> [a]
: CgState -> [(FilePath, CgVal)]
cgInputs CgState
s })
                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 ()
_ <- forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
outputSVal SVal
v
                     SV
sv <- forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV SVal
v
                     forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgOutputs :: [(FilePath, CgVal)]
cgOutputs = (FilePath
nm, SV -> CgVal
CgAtomic SV
sv) forall a. a -> [a] -> [a]
: CgState -> [(FilePath, CgVal)]
cgOutputs CgState
s })

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

-- | Creates a returned (unnamed) array value in the generated code.
svCgReturnArr :: [SVal] -> SBVCodeGen ()
svCgReturnArr :: [SVal] -> SBVCodeGen ()
svCgReturnArr [SVal]
vs
  | Int
sz forall a. Ord a => a -> a -> Bool
< Int
1 = forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ FilePath
"SBV.cgReturnArr: Array returns must have at least one element, received " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show Int
sz
  | Bool
True   = do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
outputSVal [SVal]
vs
                [SV]
sws <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV [SVal]
vs
                forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgReturns :: [CgVal]
cgReturns = [SV] -> CgVal
CgArray [SV]
sws forall a. a -> [a] -> [a]
: CgState -> [CgVal]
cgReturns CgState
s })
  where sz :: Int
sz = 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 <- forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvForall_
                SV
sv <- forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV SBV a
r
                forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgInputs :: [(FilePath, CgVal)]
cgInputs = (FilePath
nm, SV -> CgVal
CgAtomic SV
sv) forall a. a -> [a] -> [a]
: CgState -> [(FilePath, CgVal)]
cgInputs CgState
s })
                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 forall a. Ord a => a -> a -> Bool
< Int
1 = forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ FilePath
"SBV.cgInputArr: Array inputs must have at least one element, given " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show Int
sz forall a. [a] -> [a] -> [a]
++ FilePath
" for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show FilePath
nm
  | Bool
True   = do [SBV a]
rs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvForall_) [Int
1..Int
sz]
                [SV]
sws <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV [SBV a]
rs
                forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgInputs :: [(FilePath, CgVal)]
cgInputs = (FilePath
nm, [SV] -> CgVal
CgArray [SV]
sws) forall a. a -> [a] -> [a]
: CgState -> [(FilePath, CgVal)]
cgInputs CgState
s })
                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
_ <- forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
v
                   SV
sv <- forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV SBV a
v
                   forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgOutputs :: [(FilePath, CgVal)]
cgOutputs = (FilePath
nm, SV -> CgVal
CgAtomic SV
sv) forall a. a -> [a] -> [a]
: CgState -> [(FilePath, CgVal)]
cgOutputs CgState
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 forall a. Ord a => a -> a -> Bool
< Int
1 = forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ FilePath
"SBV.cgOutputArr: Array outputs must have at least one element, received " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show Int
sz forall a. [a] -> [a] -> [a]
++ FilePath
" for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show FilePath
nm
  | Bool
True   = do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output [SBV a]
vs
                [SV]
sws <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV [SBV a]
vs
                forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgOutputs :: [(FilePath, CgVal)]
cgOutputs = (FilePath
nm, [SV] -> CgVal
CgArray [SV]
sws) forall a. a -> [a] -> [a]
: CgState -> [(FilePath, CgVal)]
cgOutputs CgState
s })
  where sz :: Int
sz = 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
_ <- forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
v
                SV
sv <- forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV SBV a
v
                forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgReturns :: [CgVal]
cgReturns = SV -> CgVal
CgAtomic SV
sv forall a. a -> [a] -> [a]
: CgState -> [CgVal]
cgReturns CgState
s })

-- | Creates a returned (unnamed) array value in the generated code.
cgReturnArr :: SymVal a => [SBV a] -> SBVCodeGen ()
cgReturnArr :: forall a. SymVal a => [SBV a] -> SBVCodeGen ()
cgReturnArr [SBV a]
vs
  | Int
sz forall a. Ord a => a -> a -> Bool
< Int
1 = forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ FilePath
"SBV.cgReturnArr: Array returns must have at least one element, received " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show Int
sz
  | Bool
True   = do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output [SBV a]
vs
                [SV]
sws <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV [SBV a]
vs
                forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\CgState
s -> CgState
s { cgReturns :: [CgVal]
cgReturns = [SV] -> CgVal
CgArray [SV]
sws forall a. a -> [a] -> [a]
: CgState -> [CgVal]
cgReturns CgState
s })
  where sz :: Int
sz = 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) = forall a. [a] -> [[a]] -> [a]
intercalate FilePath
"\n" forall a b. (a -> b) -> a -> b
$ 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: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show FilePath
f forall a. [a] -> [a] -> [a]
++ FilePath
" ================\n"
                                forall a. [a] -> [a] -> [a]
++ Doc -> FilePath
render' ([Doc] -> Doc
vcat [Doc]
ds)
                                forall a. [a] -> [a] -> [a]
++ FilePath
"== END: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show FilePath
f 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) <- forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic SBVRunMode
CodeGen forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT CgState Symbolic a
comp CgState
initCgState { cgFinalConfig :: CgConfig
cgFinalConfig = CgConfig
cgConfig }
   let st :: CgState
st = CgState
st' { cgInputs :: [(FilePath, CgVal)]
cgInputs       = forall a. [a] -> [a]
reverse (CgState -> [(FilePath, CgVal)]
cgInputs CgState
st')
                , cgOutputs :: [(FilePath, CgVal)]
cgOutputs      = forall a. [a] -> [a]
reverse (CgState -> [(FilePath, CgVal)]
cgOutputs CgState
st')
                }
       allNamedVars :: [FilePath]
allNamedVars = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (CgState -> [(FilePath, CgVal)]
cgInputs CgState
st forall a. [a] -> [a] -> [a]
++ CgState -> [(FilePath, CgVal)]
cgOutputs CgState
st)
       dupNames :: [FilePath]
dupNames = [FilePath]
allNamedVars forall a. Eq a => [a] -> [a] -> [a]
\\ forall a. Eq a => [a] -> [a]
nub [FilePath]
allNamedVars
   forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
dupNames) forall a b. (a -> b) -> a -> b
$
        forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ FilePath
"SBV.codeGen: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show FilePath
nm forall a. [a] -> [a] -> [a]
++ FilePath
" has following argument names duplicated: " forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
unwords [FilePath]
dupNames

   forall (m :: * -> *) a. Monad m => a -> m a
return (a
retVal, CgState -> CgConfig
cgFinalConfig CgState
st, 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)              = 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
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b forall a b. (a -> b) -> a -> b
$ do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
overWrite forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ FilePath
"Creating directory " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show FilePath
dirName forall a. [a] -> [a] -> [a]
++ FilePath
".."
                      Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True FilePath
dirName

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

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

        if Bool
goOn then do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {a}. (FilePath, (a, [Doc])) -> IO ()
renderFile [(FilePath, (CgPgmKind, [Doc]))]
files
                        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
overWrite 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 -> ShowS
</> FilePath
f
                                     forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
overWrite forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ FilePath
"Generating: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show FilePath
fn 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ShowS
clean forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
lines forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> FilePath
P.render
  where clean :: ShowS
clean FilePath
x | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace FilePath
x = FilePath
""
                | Bool
True          = FilePath
x