{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Compilers.CodeGen (
SBVCodeGen(..), cgSym
, cgInput, cgInputArr
, cgOutput, cgOutputArr
, cgReturn, cgReturnArr
, svCgInput, svCgInputArr
, svCgOutput, svCgOutputArr
, svCgReturn, svCgReturnArr
, cgPerformRTCs, cgSetDriverValues
, cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert, cgOverwriteFiles, cgShowU8UsingHex
, cgIntegerSize, cgSRealType, CgSRealType(..)
, CgTarget(..), CgConfig(..), CgState(..), CgPgmBundle(..), CgPgmKind(..), CgVal(..)
, defaultCgConfig, initCgState, isCgDriver, isCgMakefile
, cgGenerateDriver, cgGenerateMakefile, codeGen, renderCgPgmBundle
) where
import Control.Monad (filterM, replicateM, unless)
import Control.Monad.Trans (MonadIO(liftIO), lift)
import Control.Monad.State.Lazy (MonadState, StateT(..), modify')
import Data.Char (toLower, isSpace)
import Data.List (nub, isPrefixOf, intercalate, (\\))
import System.Directory (createDirectoryIfMissing, doesDirectoryExist, doesFileExist)
import System.FilePath ((</>))
import System.IO (hFlush, stdout)
import Text.PrettyPrint.HughesPJ (Doc, vcat)
import qualified Text.PrettyPrint.HughesPJ as P (render)
import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic (MonadSymbolic(..), svToSymSV, svMkSymVar, outputSVal)
#if MIN_VERSION_base(4,11,0)
import Control.Monad.Fail as Fail
#endif
class CgTarget a where
targetName :: a -> String
translate :: a -> CgConfig -> String -> CgState -> Result -> CgPgmBundle
data CgConfig = CgConfig {
CgConfig -> Bool
cgRTC :: Bool
, CgConfig -> Maybe Int
cgInteger :: Maybe Int
, CgConfig -> Maybe CgSRealType
cgReal :: Maybe CgSRealType
, CgConfig -> [Integer]
cgDriverVals :: [Integer]
, CgConfig -> Bool
cgGenDriver :: Bool
, CgConfig -> Bool
cgGenMakefile :: Bool
, CgConfig -> Bool
cgIgnoreAsserts :: Bool
, CgConfig -> Bool
cgOverwriteGenerated :: Bool
, CgConfig -> Bool
cgShowU8InHex :: Bool
}
defaultCgConfig :: CgConfig
defaultCgConfig :: CgConfig
defaultCgConfig = CgConfig :: Bool
-> Maybe Int
-> Maybe CgSRealType
-> [Integer]
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> CgConfig
CgConfig { cgRTC :: Bool
cgRTC = Bool
False
, cgInteger :: Maybe Int
cgInteger = Maybe Int
forall a. Maybe a
Nothing
, cgReal :: Maybe CgSRealType
cgReal = Maybe CgSRealType
forall a. Maybe a
Nothing
, cgDriverVals :: [Integer]
cgDriverVals = []
, cgGenDriver :: Bool
cgGenDriver = Bool
True
, cgGenMakefile :: Bool
cgGenMakefile = Bool
True
, cgIgnoreAsserts :: Bool
cgIgnoreAsserts = Bool
False
, cgOverwriteGenerated :: Bool
cgOverwriteGenerated = Bool
False
, cgShowU8InHex :: Bool
cgShowU8InHex = Bool
False
}
data CgVal = CgAtomic SV
| CgArray [SV]
data CgState = CgState {
CgState -> [(String, CgVal)]
cgInputs :: [(String, CgVal)]
, CgState -> [(String, CgVal)]
cgOutputs :: [(String, CgVal)]
, CgState -> [CgVal]
cgReturns :: [CgVal]
, CgState -> [String]
cgPrototypes :: [String]
, CgState -> [String]
cgDecls :: [String]
, CgState -> [String]
cgLDFlags :: [String]
, CgState -> CgConfig
cgFinalConfig :: CgConfig
}
initCgState :: CgState
initCgState :: CgState
initCgState = CgState :: [(String, CgVal)]
-> [(String, CgVal)]
-> [CgVal]
-> [String]
-> [String]
-> [String]
-> CgConfig
-> CgState
CgState {
cgInputs :: [(String, CgVal)]
cgInputs = []
, cgOutputs :: [(String, CgVal)]
cgOutputs = []
, cgReturns :: [CgVal]
cgReturns = []
, cgPrototypes :: [String]
cgPrototypes = []
, cgDecls :: [String]
cgDecls = []
, cgLDFlags :: [String]
cgLDFlags = []
, cgFinalConfig :: CgConfig
cgFinalConfig = CgConfig
defaultCgConfig
}
newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a)
deriving ( Functor SBVCodeGen
a -> SBVCodeGen a
Functor SBVCodeGen =>
(forall a. a -> SBVCodeGen a)
-> (forall a b.
SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b)
-> (forall a b c.
(a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c)
-> (forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b)
-> (forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a)
-> Applicative SBVCodeGen
SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
(a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
forall a. a -> SBVCodeGen a
forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
forall a b. SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
forall a b c.
(a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
$c<* :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
*> :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
$c*> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
liftA2 :: (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
$cliftA2 :: forall a b c.
(a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c
<*> :: SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
$c<*> :: forall a b. SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b
pure :: a -> SBVCodeGen a
$cpure :: forall a. a -> SBVCodeGen a
$cp1Applicative :: Functor SBVCodeGen
Applicative, a -> SBVCodeGen b -> SBVCodeGen a
(a -> b) -> SBVCodeGen a -> SBVCodeGen b
(forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b)
-> (forall a b. a -> SBVCodeGen b -> SBVCodeGen a)
-> Functor SBVCodeGen
forall a b. a -> SBVCodeGen b -> SBVCodeGen a
forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SBVCodeGen b -> SBVCodeGen a
$c<$ :: forall a b. a -> SBVCodeGen b -> SBVCodeGen a
fmap :: (a -> b) -> SBVCodeGen a -> SBVCodeGen b
$cfmap :: forall a b. (a -> b) -> SBVCodeGen a -> SBVCodeGen b
Functor, Applicative SBVCodeGen
a -> SBVCodeGen a
Applicative SBVCodeGen =>
(forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b)
-> (forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b)
-> (forall a. a -> SBVCodeGen a)
-> Monad SBVCodeGen
SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
forall a. a -> SBVCodeGen a
forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> SBVCodeGen a
$creturn :: forall a. a -> SBVCodeGen a
>> :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
$c>> :: forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
>>= :: SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
$c>>= :: forall a b. SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b
$cp1Monad :: Applicative SBVCodeGen
Monad, Monad SBVCodeGen
Monad SBVCodeGen =>
(forall a. IO a -> SBVCodeGen a) -> MonadIO SBVCodeGen
IO a -> SBVCodeGen a
forall a. IO a -> SBVCodeGen a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> SBVCodeGen a
$cliftIO :: forall a. IO a -> SBVCodeGen a
$cp1MonadIO :: Monad SBVCodeGen
MonadIO, MonadState CgState
, MonadIO SBVCodeGen
SBVCodeGen State
MonadIO SBVCodeGen => SBVCodeGen State -> MonadSymbolic SBVCodeGen
forall (m :: * -> *). MonadIO m => m State -> MonadSymbolic m
symbolicEnv :: SBVCodeGen State
$csymbolicEnv :: SBVCodeGen State
$cp1MonadSymbolic :: MonadIO SBVCodeGen
MonadSymbolic
#if MIN_VERSION_base(4,11,0)
, Monad SBVCodeGen
Monad SBVCodeGen =>
(forall a. String -> SBVCodeGen a) -> MonadFail SBVCodeGen
String -> SBVCodeGen a
forall a. String -> SBVCodeGen a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
fail :: String -> SBVCodeGen a
$cfail :: forall a. String -> SBVCodeGen a
$cp1MonadFail :: Monad SBVCodeGen
Fail.MonadFail
#endif
)
cgSym :: Symbolic a -> SBVCodeGen a
cgSym :: Symbolic a -> SBVCodeGen a
cgSym = StateT CgState Symbolic a -> SBVCodeGen a
forall a. StateT CgState Symbolic a -> SBVCodeGen a
SBVCodeGen (StateT CgState Symbolic a -> SBVCodeGen a)
-> (Symbolic a -> StateT CgState Symbolic a)
-> Symbolic a
-> SBVCodeGen a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbolic a -> StateT CgState Symbolic a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
cgPerformRTCs :: Bool -> SBVCodeGen ()
cgPerformRTCs :: Bool -> SBVCodeGen ()
cgPerformRTCs b :: Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgRTC :: Bool
cgRTC = Bool
b } })
cgIntegerSize :: Int -> SBVCodeGen ()
cgIntegerSize :: Int -> SBVCodeGen ()
cgIntegerSize i :: Int
i
| Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [8, 16, 32, 64]
= String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ "SBV.cgIntegerSize: Argument must be one of 8, 16, 32, or 64. Received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
| Bool
True
= (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgInteger :: Maybe Int
cgInteger = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i }})
data CgSRealType = CgFloat
| CgDouble
| CgLongDouble
deriving CgSRealType -> CgSRealType -> Bool
(CgSRealType -> CgSRealType -> Bool)
-> (CgSRealType -> CgSRealType -> Bool) -> Eq CgSRealType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CgSRealType -> CgSRealType -> Bool
$c/= :: CgSRealType -> CgSRealType -> Bool
== :: CgSRealType -> CgSRealType -> Bool
$c== :: CgSRealType -> CgSRealType -> Bool
Eq
instance Show CgSRealType where
show :: CgSRealType -> String
show CgFloat = "float"
show CgDouble = "double"
show CgLongDouble = "long double"
cgSRealType :: CgSRealType -> SBVCodeGen ()
cgSRealType :: CgSRealType -> SBVCodeGen ()
cgSRealType rt :: CgSRealType
rt = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s {cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgReal :: Maybe CgSRealType
cgReal = CgSRealType -> Maybe CgSRealType
forall a. a -> Maybe a
Just CgSRealType
rt }})
cgGenerateDriver :: Bool -> SBVCodeGen ()
cgGenerateDriver :: Bool -> SBVCodeGen ()
cgGenerateDriver b :: Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgGenDriver :: Bool
cgGenDriver = Bool
b } })
cgGenerateMakefile :: Bool -> SBVCodeGen ()
cgGenerateMakefile :: Bool -> SBVCodeGen ()
cgGenerateMakefile b :: Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgGenMakefile :: Bool
cgGenMakefile = Bool
b } })
cgSetDriverValues :: [Integer] -> SBVCodeGen ()
cgSetDriverValues :: [Integer] -> SBVCodeGen ()
cgSetDriverValues vs :: [Integer]
vs = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgDriverVals :: [Integer]
cgDriverVals = [Integer]
vs } })
cgIgnoreSAssert :: Bool -> SBVCodeGen ()
cgIgnoreSAssert :: Bool -> SBVCodeGen ()
cgIgnoreSAssert b :: Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgIgnoreAsserts :: Bool
cgIgnoreAsserts = Bool
b } })
cgAddPrototype :: [String] -> SBVCodeGen ()
cgAddPrototype :: [String] -> SBVCodeGen ()
cgAddPrototype ss :: [String]
ss = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> let old :: [String]
old = CgState -> [String]
cgPrototypes CgState
s
new :: [String]
new = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
old then [String]
ss else [String]
old [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [""] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ss
in CgState
s { cgPrototypes :: [String]
cgPrototypes = [String]
new })
cgOverwriteFiles :: Bool -> SBVCodeGen ()
cgOverwriteFiles :: Bool -> SBVCodeGen ()
cgOverwriteFiles b :: Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgOverwriteGenerated :: Bool
cgOverwriteGenerated = Bool
b } })
cgShowU8UsingHex :: Bool -> SBVCodeGen ()
cgShowU8UsingHex :: Bool -> SBVCodeGen ()
cgShowU8UsingHex b :: Bool
b = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgFinalConfig :: CgConfig
cgFinalConfig = (CgState -> CgConfig
cgFinalConfig CgState
s) { cgShowU8InHex :: Bool
cgShowU8InHex = Bool
b } })
cgAddDecl :: [String] -> SBVCodeGen ()
cgAddDecl :: [String] -> SBVCodeGen ()
cgAddDecl ss :: [String]
ss = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgDecls :: [String]
cgDecls = CgState -> [String]
cgDecls CgState
s [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ss })
cgAddLDFlags :: [String] -> SBVCodeGen ()
cgAddLDFlags :: [String] -> SBVCodeGen ()
cgAddLDFlags ss :: [String]
ss = (CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgLDFlags :: [String]
cgLDFlags = CgState -> [String]
cgLDFlags CgState
s [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ss })
svCgInput :: Kind -> String -> SBVCodeGen SVal
svCgInput :: Kind -> String -> SBVCodeGen SVal
svCgInput k :: Kind
k nm :: String
nm = do SVal
r <- SBVCodeGen State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv SBVCodeGen State -> (State -> SBVCodeGen SVal) -> SBVCodeGen SVal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SVal -> SBVCodeGen SVal
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SVal -> SBVCodeGen SVal)
-> (State -> IO SVal) -> State -> SBVCodeGen SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
ALL) Kind
k Maybe String
forall a. Maybe a
Nothing
SV
sv <- SVal -> SBVCodeGen SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV SVal
r
(CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgInputs :: [(String, CgVal)]
cgInputs = (String
nm, SV -> CgVal
CgAtomic SV
sv) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgInputs CgState
s })
SVal -> SBVCodeGen SVal
forall (m :: * -> *) a. Monad m => a -> m a
return SVal
r
svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
svCgInputArr k :: Kind
k sz :: Int
sz nm :: String
nm
| Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = String -> SBVCodeGen [SVal]
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen [SVal]) -> String -> SBVCodeGen [SVal]
forall a b. (a -> b) -> a -> b
$ "SBV.cgInputArr: Array inputs must have at least one element, given " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz String -> String -> String
forall a. [a] -> [a] -> [a]
++ " for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm
| Bool
True = do [SVal]
rs <- SBVCodeGen State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv SBVCodeGen State
-> (State -> SBVCodeGen [SVal]) -> SBVCodeGen [SVal]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO [SVal] -> SBVCodeGen [SVal]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [SVal] -> SBVCodeGen [SVal])
-> (State -> IO [SVal]) -> State -> SBVCodeGen [SVal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IO SVal -> IO [SVal]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
sz (IO SVal -> IO [SVal]) -> (State -> IO SVal) -> State -> IO [SVal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
ALL) Kind
k Maybe String
forall a. Maybe a
Nothing
[SV]
sws <- (SVal -> SBVCodeGen SV) -> [SVal] -> SBVCodeGen [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SVal -> SBVCodeGen SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV [SVal]
rs
(CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgInputs :: [(String, CgVal)]
cgInputs = (String
nm, [SV] -> CgVal
CgArray [SV]
sws) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgInputs CgState
s })
[SVal] -> SBVCodeGen [SVal]
forall (m :: * -> *) a. Monad m => a -> m a
return [SVal]
rs
svCgOutput :: String -> SVal -> SBVCodeGen ()
svCgOutput :: String -> SVal -> SBVCodeGen ()
svCgOutput nm :: String
nm v :: SVal
v = do ()
_ <- SVal -> SBVCodeGen ()
forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
outputSVal SVal
v
SV
sv <- SVal -> SBVCodeGen SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV SVal
v
(CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgOutputs :: [(String, CgVal)]
cgOutputs = (String
nm, SV -> CgVal
CgAtomic SV
sv) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgOutputs CgState
s })
svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
svCgOutputArr nm :: String
nm vs :: [SVal]
vs
| Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ "SBV.cgOutputArr: Array outputs must have at least one element, received " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz String -> String -> String
forall a. [a] -> [a] -> [a]
++ " for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm
| Bool
True = do (SVal -> SBVCodeGen ()) -> [SVal] -> SBVCodeGen ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SVal -> SBVCodeGen ()
forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
outputSVal [SVal]
vs
[SV]
sws <- (SVal -> SBVCodeGen SV) -> [SVal] -> SBVCodeGen [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SVal -> SBVCodeGen SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV [SVal]
vs
(CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgOutputs :: [(String, CgVal)]
cgOutputs = (String
nm, [SV] -> CgVal
CgArray [SV]
sws) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgOutputs CgState
s })
where sz :: Int
sz = [SVal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SVal]
vs
svCgReturn :: SVal -> SBVCodeGen ()
svCgReturn :: SVal -> SBVCodeGen ()
svCgReturn v :: SVal
v = do ()
_ <- SVal -> SBVCodeGen ()
forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
outputSVal SVal
v
SV
sv <- SVal -> SBVCodeGen SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV SVal
v
(CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgReturns :: [CgVal]
cgReturns = SV -> CgVal
CgAtomic SV
sv CgVal -> [CgVal] -> [CgVal]
forall a. a -> [a] -> [a]
: CgState -> [CgVal]
cgReturns CgState
s })
svCgReturnArr :: [SVal] -> SBVCodeGen ()
svCgReturnArr :: [SVal] -> SBVCodeGen ()
svCgReturnArr vs :: [SVal]
vs
| Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ "SBV.cgReturnArr: Array returns must have at least one element, received " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz
| Bool
True = do (SVal -> SBVCodeGen ()) -> [SVal] -> SBVCodeGen ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SVal -> SBVCodeGen ()
forall (m :: * -> *). MonadSymbolic m => SVal -> m ()
outputSVal [SVal]
vs
[SV]
sws <- (SVal -> SBVCodeGen SV) -> [SVal] -> SBVCodeGen [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SVal -> SBVCodeGen SV
forall (m :: * -> *). MonadSymbolic m => SVal -> m SV
svToSymSV [SVal]
vs
(CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgReturns :: [CgVal]
cgReturns = [SV] -> CgVal
CgArray [SV]
sws CgVal -> [CgVal] -> [CgVal]
forall a. a -> [a] -> [a]
: CgState -> [CgVal]
cgReturns CgState
s })
where sz :: Int
sz = [SVal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SVal]
vs
cgInput :: SymVal a => String -> SBVCodeGen (SBV a)
cgInput :: String -> SBVCodeGen (SBV a)
cgInput nm :: String
nm = do SBV a
r <- SBVCodeGen (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_
SV
sv <- SBV a -> SBVCodeGen SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV SBV a
r
(CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgInputs :: [(String, CgVal)]
cgInputs = (String
nm, SV -> CgVal
CgAtomic SV
sv) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgInputs CgState
s })
SBV a -> SBVCodeGen (SBV a)
forall (m :: * -> *) a. Monad m => a -> m a
return SBV a
r
cgInputArr :: SymVal a => Int -> String -> SBVCodeGen [SBV a]
cgInputArr :: Int -> String -> SBVCodeGen [SBV a]
cgInputArr sz :: Int
sz nm :: String
nm
| Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = String -> SBVCodeGen [SBV a]
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen [SBV a]) -> String -> SBVCodeGen [SBV a]
forall a b. (a -> b) -> a -> b
$ "SBV.cgInputArr: Array inputs must have at least one element, given " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz String -> String -> String
forall a. [a] -> [a] -> [a]
++ " for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm
| Bool
True = do [SBV a]
rs <- (Int -> SBVCodeGen (SBV a)) -> [Int] -> SBVCodeGen [SBV a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SBVCodeGen (SBV a) -> Int -> SBVCodeGen (SBV a)
forall a b. a -> b -> a
const SBVCodeGen (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_) [1..Int
sz]
[SV]
sws <- (SBV a -> SBVCodeGen SV) -> [SBV a] -> SBVCodeGen [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SBV a -> SBVCodeGen SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV [SBV a]
rs
(CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgInputs :: [(String, CgVal)]
cgInputs = (String
nm, [SV] -> CgVal
CgArray [SV]
sws) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgInputs CgState
s })
[SBV a] -> SBVCodeGen [SBV a]
forall (m :: * -> *) a. Monad m => a -> m a
return [SBV a]
rs
cgOutput :: String -> SBV a -> SBVCodeGen ()
cgOutput :: String -> SBV a -> SBVCodeGen ()
cgOutput nm :: String
nm v :: SBV a
v = do SBV a
_ <- SBV a -> SBVCodeGen (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
v
SV
sv <- SBV a -> SBVCodeGen SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV SBV a
v
(CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgOutputs :: [(String, CgVal)]
cgOutputs = (String
nm, SV -> CgVal
CgAtomic SV
sv) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgOutputs CgState
s })
cgOutputArr :: SymVal a => String -> [SBV a] -> SBVCodeGen ()
cgOutputArr :: String -> [SBV a] -> SBVCodeGen ()
cgOutputArr nm :: String
nm vs :: [SBV a]
vs
| Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ "SBV.cgOutputArr: Array outputs must have at least one element, received " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz String -> String -> String
forall a. [a] -> [a] -> [a]
++ " for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm
| Bool
True = do (SBV a -> SBVCodeGen (SBV a)) -> [SBV a] -> SBVCodeGen ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SBV a -> SBVCodeGen (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output [SBV a]
vs
[SV]
sws <- (SBV a -> SBVCodeGen SV) -> [SBV a] -> SBVCodeGen [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SBV a -> SBVCodeGen SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV [SBV a]
vs
(CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgOutputs :: [(String, CgVal)]
cgOutputs = (String
nm, [SV] -> CgVal
CgArray [SV]
sws) (String, CgVal) -> [(String, CgVal)] -> [(String, CgVal)]
forall a. a -> [a] -> [a]
: CgState -> [(String, CgVal)]
cgOutputs CgState
s })
where sz :: Int
sz = [SBV a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBV a]
vs
cgReturn :: SBV a -> SBVCodeGen ()
cgReturn :: SBV a -> SBVCodeGen ()
cgReturn v :: SBV a
v = do SBV a
_ <- SBV a -> SBVCodeGen (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
v
SV
sv <- SBV a -> SBVCodeGen SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV SBV a
v
(CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgReturns :: [CgVal]
cgReturns = SV -> CgVal
CgAtomic SV
sv CgVal -> [CgVal] -> [CgVal]
forall a. a -> [a] -> [a]
: CgState -> [CgVal]
cgReturns CgState
s })
cgReturnArr :: SymVal a => [SBV a] -> SBVCodeGen ()
cgReturnArr :: [SBV a] -> SBVCodeGen ()
cgReturnArr vs :: [SBV a]
vs
| Int
sz Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 = String -> SBVCodeGen ()
forall a. HasCallStack => String -> a
error (String -> SBVCodeGen ()) -> String -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ "SBV.cgReturnArr: Array returns must have at least one element, received " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz
| Bool
True = do (SBV a -> SBVCodeGen (SBV a)) -> [SBV a] -> SBVCodeGen ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SBV a -> SBVCodeGen (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output [SBV a]
vs
[SV]
sws <- (SBV a -> SBVCodeGen SV) -> [SBV a] -> SBVCodeGen [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SBV a -> SBVCodeGen SV
forall (m :: * -> *) a. MonadSymbolic m => SBV a -> m SV
sbvToSymSV [SBV a]
vs
(CgState -> CgState) -> SBVCodeGen ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (\s :: CgState
s -> CgState
s { cgReturns :: [CgVal]
cgReturns = [SV] -> CgVal
CgArray [SV]
sws CgVal -> [CgVal] -> [CgVal]
forall a. a -> [a] -> [a]
: CgState -> [CgVal]
cgReturns CgState
s })
where sz :: Int
sz = [SBV a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBV a]
vs
data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))]
data CgPgmKind = CgMakefile [String]
| [Doc]
| CgSource
| CgDriver
isCgDriver :: CgPgmKind -> Bool
isCgDriver :: CgPgmKind -> Bool
isCgDriver CgDriver = Bool
True
isCgDriver _ = Bool
False
isCgMakefile :: CgPgmKind -> Bool
isCgMakefile :: CgPgmKind -> Bool
isCgMakefile CgMakefile{} = Bool
True
isCgMakefile _ = Bool
False
instance Show CgPgmBundle where
show :: CgPgmBundle -> String
show (CgPgmBundle _ fs :: [(String, (CgPgmKind, [Doc]))]
fs) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((String, (CgPgmKind, [Doc])) -> String)
-> [(String, (CgPgmKind, [Doc]))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, (CgPgmKind, [Doc])) -> String
showFile [(String, (CgPgmKind, [Doc]))]
fs
where showFile :: (FilePath, (CgPgmKind, [Doc])) -> String
showFile :: (String, (CgPgmKind, [Doc])) -> String
showFile (f :: String
f, (_, ds :: [Doc]
ds)) = "== BEGIN: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ " ================\n"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
render' ([Doc] -> Doc
vcat [Doc]
ds)
String -> String -> String
forall a. [a] -> [a] -> [a]
++ "== END: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ " =================="
codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle)
codeGen :: l
-> CgConfig
-> String
-> SBVCodeGen a
-> IO (a, CgConfig, CgPgmBundle)
codeGen l :: l
l cgConfig :: CgConfig
cgConfig nm :: String
nm (SBVCodeGen comp :: StateT CgState Symbolic a
comp) = do
((retVal :: a
retVal, st' :: CgState
st'), res :: Result
res) <- SBVRunMode
-> SymbolicT IO (a, CgState) -> IO ((a, CgState), Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic SBVRunMode
CodeGen (SymbolicT IO (a, CgState) -> IO ((a, CgState), Result))
-> SymbolicT IO (a, CgState) -> IO ((a, CgState), Result)
forall a b. (a -> b) -> a -> b
$ StateT CgState Symbolic a -> CgState -> SymbolicT IO (a, CgState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT CgState Symbolic a
comp CgState
initCgState { cgFinalConfig :: CgConfig
cgFinalConfig = CgConfig
cgConfig }
let st :: CgState
st = CgState
st' { cgInputs :: [(String, CgVal)]
cgInputs = [(String, CgVal)] -> [(String, CgVal)]
forall a. [a] -> [a]
reverse (CgState -> [(String, CgVal)]
cgInputs CgState
st')
, cgOutputs :: [(String, CgVal)]
cgOutputs = [(String, CgVal)] -> [(String, CgVal)]
forall a. [a] -> [a]
reverse (CgState -> [(String, CgVal)]
cgOutputs CgState
st')
}
allNamedVars :: [String]
allNamedVars = ((String, CgVal) -> String) -> [(String, CgVal)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, CgVal) -> String
forall a b. (a, b) -> a
fst (CgState -> [(String, CgVal)]
cgInputs CgState
st [(String, CgVal)] -> [(String, CgVal)] -> [(String, CgVal)]
forall a. [a] -> [a] -> [a]
++ CgState -> [(String, CgVal)]
cgOutputs CgState
st)
dupNames :: [String]
dupNames = [String]
allNamedVars [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ [String] -> [String]
forall a. Eq a => [a] -> [a]
nub [String]
allNamedVars
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
dupNames) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "SBV.codeGen: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " has following argument names duplicated: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
dupNames
(a, CgConfig, CgPgmBundle) -> IO (a, CgConfig, CgPgmBundle)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
retVal, CgState -> CgConfig
cgFinalConfig CgState
st, l -> CgConfig -> String -> CgState -> Result -> CgPgmBundle
forall a.
CgTarget a =>
a -> CgConfig -> String -> CgState -> Result -> CgPgmBundle
translate l
l (CgState -> CgConfig
cgFinalConfig CgState
st) String
nm CgState
st Result
res)
renderCgPgmBundle :: Maybe FilePath -> (CgConfig, CgPgmBundle) -> IO ()
renderCgPgmBundle :: Maybe String -> (CgConfig, CgPgmBundle) -> IO ()
renderCgPgmBundle Nothing (_ , bundle :: CgPgmBundle
bundle) = CgPgmBundle -> IO ()
forall a. Show a => a -> IO ()
print CgPgmBundle
bundle
renderCgPgmBundle (Just dirName :: String
dirName) (cfg :: CgConfig
cfg, CgPgmBundle _ files :: [(String, (CgPgmKind, [Doc]))]
files) = do
Bool
b <- String -> IO Bool
doesDirectoryExist String
dirName
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
overWrite (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Creating directory " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
dirName String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".."
Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
dirName
[String]
dups <- (String -> IO Bool) -> [String] -> IO [String]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (\fn :: String
fn -> String -> IO Bool
doesFileExist (String
dirName String -> String -> String
</> String
fn)) (((String, (CgPgmKind, [Doc])) -> String)
-> [(String, (CgPgmKind, [Doc]))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, (CgPgmKind, [Doc])) -> String
forall a b. (a, b) -> a
fst [(String, (CgPgmKind, [Doc]))]
files)
Bool
goOn <- case (Bool
overWrite, [String]
dups) of
(True, _) -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
(_, []) -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
_ -> do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Code generation would overwrite the following " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
dups Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then "file:" else "files:")
(String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\fn :: String
fn -> String -> IO ()
putStrLn ('\t' Char -> String -> String
forall a. a -> [a] -> [a]
: String
fn)) [String]
dups
String -> IO ()
putStr "Continue? [yn] "
Handle -> IO ()
hFlush Handle
stdout
String
resp <- IO String
getLine
Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
resp String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` "yes"
if Bool
goOn then do ((String, (CgPgmKind, [Doc])) -> IO ())
-> [(String, (CgPgmKind, [Doc]))] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String, (CgPgmKind, [Doc])) -> IO ()
forall a. (String, (a, [Doc])) -> IO ()
renderFile [(String, (CgPgmKind, [Doc]))]
files
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
overWrite (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn "Done."
else String -> IO ()
putStrLn "Aborting."
where overWrite :: Bool
overWrite = CgConfig -> Bool
cgOverwriteGenerated CgConfig
cfg
renderFile :: (String, (a, [Doc])) -> IO ()
renderFile (f :: String
f, (_, ds :: [Doc]
ds)) = do let fn :: String
fn = String
dirName String -> String -> String
</> String
f
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
overWrite (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Generating: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
fn String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".."
String -> String -> IO ()
writeFile String
fn (Doc -> String
render' ([Doc] -> Doc
vcat [Doc]
ds))
render' :: Doc -> String
render' :: Doc -> String
render' = [String] -> String
unlines ([String] -> String) -> (Doc -> [String]) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
clean ([String] -> [String]) -> (Doc -> [String]) -> Doc -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines (String -> [String]) -> (Doc -> String) -> Doc -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
P.render
where clean :: String -> String
clean x :: String
x | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
x = ""
| Bool
True = String
x