module Data.SBV.Compilers.CodeGen where
import Control.Monad.Trans
import Control.Monad.State.Lazy
import Data.Char (toLower)
import Data.List (nub, isPrefixOf, intersperse, (\\))
import System.Directory (createDirectory, doesDirectoryExist, doesFileExist)
import System.FilePath ((</>))
import Text.PrettyPrint.HughesPJ (Doc, render, vcat)
import Data.SBV.BitVectors.Data
class CgTarget a where
targetName :: a -> String
translate :: a -> Bool -> [Integer] -> String -> CgState -> Result -> CgPgmBundle
data CgConfig = CgConfig {
cgRTC :: Bool
, cgDriverVals :: [Integer]
}
defaultCgConfig :: CgConfig
defaultCgConfig = CgConfig { cgRTC = False, cgDriverVals = [] }
data CgVal = CgAtomic SW
| CgArray [SW]
data CgState = CgState {
cgInputs :: [(String, CgVal)]
, cgOutputs :: [(String, CgVal)]
, cgReturns :: [CgVal]
, cgFinalConfig :: CgConfig
}
initCgState :: CgState
initCgState = CgState {
cgInputs = []
, cgOutputs = []
, cgReturns = []
, cgFinalConfig = defaultCgConfig
}
newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a)
deriving (Monad, MonadIO, MonadState CgState)
liftSymbolic :: Symbolic a -> SBVCodeGen a
liftSymbolic = SBVCodeGen . lift
cgSBVToSW :: SBV a -> SBVCodeGen SW
cgSBVToSW = liftSymbolic . sbvToSymSW
cgPerformRTCs :: Bool -> SBVCodeGen ()
cgPerformRTCs b = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgRTC = b } })
cgSetDriverValues :: [Integer] -> SBVCodeGen ()
cgSetDriverValues vs = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgDriverVals = vs } })
cgInput :: (HasSignAndSize a, SymWord a) => String -> SBVCodeGen (SBV a)
cgInput nm = do r <- liftSymbolic free_
sw <- cgSBVToSW r
modify (\s -> s { cgInputs = (nm, CgAtomic sw) : cgInputs s })
return r
cgInputArr :: (HasSignAndSize a, SymWord 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 <- liftSymbolic $ (mapM (const free_) [1..sz])
sws <- mapM cgSBVToSW rs
modify (\s -> s { cgInputs = (nm, CgArray sws) : cgInputs s })
return rs
cgOutput :: (HasSignAndSize a, SymWord a) => String -> SBV a -> SBVCodeGen ()
cgOutput nm v = do _ <- liftSymbolic (output v)
sw <- cgSBVToSW v
modify (\s -> s { cgOutputs = (nm, CgAtomic sw) : cgOutputs s })
cgOutputArr :: (HasSignAndSize a, SymWord 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 _ <- liftSymbolic (mapM output vs)
sws <- mapM cgSBVToSW vs
modify (\s -> s { cgOutputs = (nm, CgArray sws) : cgOutputs s })
where sz = length vs
cgReturn :: (HasSignAndSize a, SymWord a) => SBV a -> SBVCodeGen ()
cgReturn v = do _ <- liftSymbolic (output v)
sw <- cgSBVToSW v
modify (\s -> s { cgReturns = CgAtomic sw : cgReturns s })
cgReturnArr :: (HasSignAndSize a, SymWord a) => [SBV a] -> SBVCodeGen ()
cgReturnArr vs
| sz < 1 = error $ "SBV.cgReturnArr: Array returns must have at least one element, received " ++ show sz
| True = do _ <- liftSymbolic (mapM output vs)
sws <- mapM cgSBVToSW vs
modify (\s -> s { cgReturns = CgArray sws : cgReturns s })
where sz = length vs
newtype CgPgmBundle = CgPgmBundle [(FilePath, (CgPgmKind, [Doc]))]
data CgPgmKind = CgMakefile
| CgHeader [Doc]
| CgSource
| CgDriver
instance Show CgPgmBundle where
show (CgPgmBundle fs) = concat $ intersperse "\n" $ map showFile fs
showFile :: (FilePath, (CgPgmKind, [Doc])) -> String
showFile (f, (_, ds)) = "== BEGIN: " ++ show f ++ " ================\n"
++ render (vcat ds)
++ "== END: " ++ show f ++ " =================="
codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle
codeGen l cgConfig nm (SBVCodeGen comp) = do
(((), st'), res) <- runSymbolic' $ runStateT comp initCgState { cgFinalConfig = cgConfig }
let st = st' { cgInputs = reverse (cgInputs st')
, cgOutputs = reverse (cgOutputs st')
}
allNamedVars = map fst (cgInputs st ++ cgOutputs st)
dupNames = allNamedVars \\ nub allNamedVars
when (not (null dupNames)) $ do
error $ "SBV.codeGen: " ++ show nm ++ " has following argument names duplicated: " ++ unwords dupNames
let finalCfg = cgFinalConfig st
return $ translate l (cgRTC finalCfg) (cgDriverVals finalCfg) nm st res
renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO ()
renderCgPgmBundle Nothing bundle = putStrLn $ show bundle
renderCgPgmBundle (Just dirName) (CgPgmBundle files) = do
b <- doesDirectoryExist dirName
when (not b) $ do putStrLn $ "Creating directory " ++ show dirName ++ ".."
createDirectory dirName
dups <- filterM (\fn -> doesFileExist (dirName </> fn)) (map fst files)
goOn <- case dups of
[] -> return True
_ -> do putStrLn $ "Code generation would override the following " ++ (if length dups == 1 then "file:" else "files:")
mapM_ (\fn -> putStrLn ("\t" ++ fn)) dups
putStr "Continue? [yn] "
resp <- getLine
return $ map toLower resp `isPrefixOf` "yes"
if goOn then do mapM_ renderFile files
putStrLn "Done."
else putStrLn "Aborting."
where renderFile (f, (_, ds)) = do let fn = dirName </> f
putStrLn $ "Generating: " ++ show fn ++ ".."
writeFile fn (render (vcat ds))