module Agda.Compiler.UHC.Compiler(compilerMain) where
#if __GLASGOW_HASKELL__ <= 708
import Control.Applicative
import Data.Monoid
#endif
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.ByteString.Lazy as BS
import qualified Data.Map as M
import Data.Maybe
import System.Directory ( canonicalizePath, createDirectoryIfMissing
, setCurrentDirectory
, doesDirectoryExist
, getDirectoryContents, copyFile
)
import Data.List as L
import System.Exit
import System.FilePath hiding (normalise)
import Paths_Agda
import Agda.Compiler.CallCompiler
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import Agda.Interaction.Imports
import qualified Agda.Syntax.Concrete.Name as CN
import Agda.Syntax.Internal hiding (Term(..))
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Serialise
import Agda.Utils.FileName
import Agda.Utils.Pretty
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.IO.Directory
import Agda.Utils.Lens
import Agda.Compiler.UHC.CompileState
import Agda.Compiler.UHC.Bridge as UB
import qualified Agda.Compiler.UHC.FromAgda as FAgda
import Agda.Compiler.Common
#include "undefined.h"
import Agda.Utils.Impossible
copyUHCAgdaBase :: FilePath -> TCM ()
copyUHCAgdaBase outDir = do
dataDir <- liftIO getDataDir
let srcDir = dataDir </> "uhc-agda-base" </> "src" </> "UHC"
liftIO $ copyDirContent srcDir (outDir </> "UHC")
compilerMain :: IsMain -> Interface -> TCM ()
compilerMain isMain i = inCompilerEnv i $ do
when (not uhcBackendEnabled) $ typeError $ GenericError "Agda has been built without UHC support. To use the UHC compiler you need to reinstall Agda with 'cabal install Agda -f uhc'."
let uhc_exist = ExitSuccess
case uhc_exist of
ExitSuccess -> do
copyUHCAgdaBase =<< compileDir
doCompile isMain i $ \_ -> compileModule
case isMain of
IsMain -> do
main <- getMain i
crMain <- getCoreName1 main
runUHCMain $ Just (iModuleName i, crMain)
NotMain -> runUHCMain Nothing
ExitFailure _ -> internalError $ unlines
[ "Agda cannot find the UHC compiler."
]
compileModule :: Interface -> TCM ()
compileModule i = do
[agdaPrimInter] <- filter (("Agda.Primitive"==) . prettyShow . iModuleName)
. map miInterface . M.elems
<$> getVisitedModules
let modNm = iModuleName i
let topModuleName = toTopLevelModuleName modNm
imports <- map miInterface . catMaybes
<$> (mapM (getVisitedModule . toTopLevelModuleName . fst)
(iImportedModules i))
let imports' = if prettyShow (iModuleName i) == "Agda.Primitive"
then imports
else agdaPrimInter : imports
reportSLn "" 1 $
"Compiling: " ++ show (iModuleName i)
code <- compileDefns modNm (map iModuleName imports') i
crFile <- corePath modNm
_ <- writeCoreFile crFile code
return ()
corePath :: ModuleName -> TCM FilePath
corePath mName = do
mdir <- compileDir
let fp = mdir </> replaceExtension fp' "bcr"
liftIO $ createDirectoryIfMissing True (takeDirectory fp)
return fp
where
fp' = foldl1 (</>) $ moduleNameToCoreNameParts mName
getMain :: MonadTCM m => Interface -> m QName
getMain iface = case concatMap f defs of
[] -> typeError $ GenericError $ "Could not find main."
[x] -> return x
_ -> __IMPOSSIBLE__
where defs = HMap.toList $ iSignature iface ^. sigDefinitions
f (qn, def) = case theDef def of
(Function{}) | "main" == show (qnameName qn) -> [qn]
_ -> []
compileDefns :: ModuleName
-> [ModuleName]
-> Interface -> TCM UB.CModule
compileDefns modNm curModImps iface = do
crMod <- FAgda.fromAgdaModule modNm curModImps iface
reportSLn "uhc" 10 $ "Done generating Core for \"" ++ show modNm ++ "\"."
return crMod
writeCoreFile :: String -> UB.CModule -> TCM ()
writeCoreFile f cmod = do
useTextual <- optUHCTextualCore <$> commandLineOptions
when useTextual (do
let f' = replaceExtension f ".dbg.tcr"
reportSLn "uhc" 10 $ "Writing textual core to \"" ++ show f' ++ "\"."
liftIO $ putPPFile f' (UB.printModule defaultEHCOpts cmod) 200
)
reportSLn "uhc" 10 $ "Writing binary core to \"" ++ show f ++ "\"."
liftIO $ putSerializeFile f cmod
runUHCMain
:: Maybe (ModuleName, HsName)
-> TCM ()
runUHCMain mainInfo = do
otherFps <- mapM (corePath . iModuleName . miInterface) =<< (M.elems <$> getVisitedModules)
allFps <-
case mainInfo of
Nothing -> return otherFps
Just (mainMod, mainName) -> do
fp <- (</> "Main.bcr") <$> compileDir
let mmod = FAgda.createMainModule mainMod mainName
writeCoreFile fp mmod
return ["Main.bcr"]
let extraOpts = maybe
["--compile-only"]
((\x -> [x]) . ("--output="++) . prettyShow . last . mnameToList . fst)
mainInfo
liftIO . setCurrentDirectory =<< compileDir
callUHC1 $ ["--pkg-hide-all", "--pkg-expose=uhcbase", "--pkg-expose=base"
] ++ extraOpts ++ allFps ++ ["+RTS", "-K50m", "-RTS"]
callUHC1 :: [String] -> TCM ()
callUHC1 args = do
uhcBin <- getUhcBin
doCall <- optUHCCallUHC <$> commandLineOptions
extraArgs <- optUHCFlags <$> commandLineOptions
callCompiler doCall uhcBin (args ++ extraArgs)
getUhcBin :: TCM FilePath
getUhcBin = fromMaybe ("uhc") . optUHCBin <$> commandLineOptions