module Data.SBV.Compilers.CodeGen where
import Control.Monad.Trans
import Control.Monad.State.Lazy
import Data.Char (toLower, isSpace)
import Data.List (nub, isPrefixOf, intercalate, (\\))
import System.Directory (createDirectory, doesDirectoryExist, doesFileExist)
import System.FilePath ((</>))
import Text.PrettyPrint.HughesPJ (Doc, vcat)
import qualified Text.PrettyPrint.HughesPJ as P (render)
import Data.SBV.BitVectors.Data
class CgTarget a where
targetName :: a -> String
translate :: a -> CgConfig -> String -> CgState -> Result -> CgPgmBundle
data CgConfig = CgConfig {
cgRTC :: Bool
, cgInteger :: Maybe Int
, cgReal :: Maybe CgSRealType
, cgDriverVals :: [Integer]
, cgGenDriver :: Bool
, cgGenMakefile :: Bool
}
defaultCgConfig :: CgConfig
defaultCgConfig = CgConfig { cgRTC = False, cgInteger = Nothing, cgReal = Nothing, cgDriverVals = [], cgGenDriver = True, cgGenMakefile = True }
data CgVal = CgAtomic SW
| CgArray [SW]
data CgState = CgState {
cgInputs :: [(String, CgVal)]
, cgOutputs :: [(String, CgVal)]
, cgReturns :: [CgVal]
, cgPrototypes :: [String]
, cgDecls :: [String]
, cgLDFlags :: [String]
, cgFinalConfig :: CgConfig
}
initCgState :: CgState
initCgState = CgState {
cgInputs = []
, cgOutputs = []
, cgReturns = []
, cgPrototypes = []
, cgDecls = []
, cgLDFlags = []
, 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 } })
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 }})
data CgSRealType = CgFloat
| CgDouble
| CgLongDouble
deriving Eq
instance Show CgSRealType where
show CgFloat = "float"
show CgDouble = "double"
show CgLongDouble = "long double"
cgSRealType :: CgSRealType -> SBVCodeGen ()
cgSRealType rt = modify (\s -> s {cgFinalConfig = (cgFinalConfig s) { cgReal = Just rt }})
cgGenerateDriver :: Bool -> SBVCodeGen ()
cgGenerateDriver b = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgGenDriver = b } })
cgGenerateMakefile :: Bool -> SBVCodeGen ()
cgGenerateMakefile b = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgGenMakefile = b } })
cgSetDriverValues :: [Integer] -> SBVCodeGen ()
cgSetDriverValues vs = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgDriverVals = vs } })
cgAddPrototype :: [String] -> SBVCodeGen ()
cgAddPrototype ss = modify (\s -> let old = cgPrototypes s
new = if null old then ss else old ++ [""] ++ ss
in s { cgPrototypes = new })
cgAddDecl :: [String] -> SBVCodeGen ()
cgAddDecl ss = modify (\s -> let old = cgDecls s
new = if null old then ss else old ++ [""] ++ ss
in s { cgDecls = new })
cgAddLDFlags :: [String] -> SBVCodeGen ()
cgAddLDFlags ss = modify (\s -> s { cgLDFlags = cgLDFlags s ++ ss })
cgInput :: SymWord a => String -> SBVCodeGen (SBV a)
cgInput nm = do r <- liftSymbolic forall_
sw <- cgSBVToSW r
modify (\s -> s { cgInputs = (nm, CgAtomic sw) : cgInputs s })
return r
cgInputArr :: 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 forall_) [1..sz]
sws <- mapM cgSBVToSW rs
modify (\s -> s { cgInputs = (nm, CgArray sws) : cgInputs s })
return rs
cgOutput :: 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 :: 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 :: SymWord a => SBV a -> SBVCodeGen ()
cgReturn v = do _ <- liftSymbolic (output v)
sw <- cgSBVToSW v
modify (\s -> s { cgReturns = CgAtomic sw : cgReturns s })
cgReturnArr :: 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
data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))]
data CgPgmKind = CgMakefile [String]
| CgHeader [Doc]
| CgSource
| CgDriver
isCgDriver :: CgPgmKind -> Bool
isCgDriver CgDriver = True
isCgDriver _ = False
isCgMakefile :: CgPgmKind -> Bool
isCgMakefile CgMakefile{} = True
isCgMakefile _ = False
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 ++ " =================="
codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle
codeGen l cgConfig nm (SBVCodeGen comp) = do
(((), st'), res) <- runSymbolic' CodeGen $ 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
unless (null dupNames) $
error $ "SBV.codeGen: " ++ show nm ++ " has following argument names duplicated: " ++ unwords dupNames
return $ translate l (cgFinalConfig st) nm st res
renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO ()
renderCgPgmBundle Nothing bundle = print bundle
renderCgPgmBundle (Just dirName) (CgPgmBundle _ files) = do
b <- doesDirectoryExist dirName
unless 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))
render' :: Doc -> String
render' = unlines . map clean . lines . P.render
where clean x | all isSpace x = ""
| True = x