{-# LANGUAGE CPP #-}
module Agda.Compiler.Common where
import Data.List as List
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap
import Data.Char
import Data.Function
#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup
#endif
import Control.Monad
import Control.Monad.State hiding (mapM_, forM_, mapM, forM, sequence)
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Internal as I
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import Agda.TypeChecking.Monad
import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Pretty
import Agda.Utils.Impossible
data IsMain = IsMain | NotMain
deriving (Eq, Show)
instance Semigroup IsMain where
NotMain <> _ = NotMain
_ <> NotMain = NotMain
IsMain <> IsMain = IsMain
instance Monoid IsMain where
mempty = IsMain
mappend = (<>)
doCompile :: forall r. Monoid r => IsMain -> Interface -> (IsMain -> Interface -> TCM r) -> TCM r
doCompile isMain i f = do
[agdaPrimInter] <- filter (("Agda.Primitive"==) . prettyShow . iModuleName)
. map miInterface . Map.elems
<$> getVisitedModules
flip evalStateT Set.empty $ mappend <$> comp NotMain agdaPrimInter <*> comp isMain i
where
comp :: IsMain -> Interface -> StateT (Set ModuleName) TCM r
comp isMain i = do
alreadyDone <- Set.member (iModuleName i) <$> get
if alreadyDone then return mempty else do
imps <- lift $
map miInterface . catMaybes <$>
mapM (getVisitedModule . toTopLevelModuleName . fst) (iImportedModules i)
ri <- mconcat <$> mapM (comp NotMain) imps
lift $ setInterface i
r <- lift $ f isMain i
modify (Set.insert $ iModuleName i)
return $ mappend ri r
setInterface :: Interface -> TCM ()
setInterface i = do
opts <- getsTC (stPersistentOptions . stPersistentState)
setCommandLineOptions opts
mapM_ setOptionsFromPragma (iPragmaOptions i)
stImportedModules `setTCLens` Set.fromList (map fst $ iImportedModules i)
stCurrentModule `setTCLens` Just (iModuleName i)
curIF :: TCM Interface
curIF = do
mName <- useTC stCurrentModule
case mName of
Nothing -> __IMPOSSIBLE__
Just name -> do
mm <- getVisitedModule (toTopLevelModuleName name)
case mm of
Nothing -> __IMPOSSIBLE__
Just mi -> return $ miInterface mi
curSig :: TCM Signature
curSig = iSignature <$> curIF
curMName :: TCM ModuleName
curMName = sigMName <$> curSig
curDefs :: TCM Definitions
curDefs = fmap (HMap.filter (not . defNoCompilation)) $ (^. sigDefinitions) <$> curSig
sortDefs :: Definitions -> [(QName, Definition)]
sortDefs defs =
List.sortBy (compare `on` fst) $
HMap.toList defs
sigMName :: Signature -> ModuleName
sigMName sig = case Map.keys (sig ^. sigSections) of
[] -> __IMPOSSIBLE__
m : _ -> m
compileDir :: TCM FilePath
compileDir = do
mdir <- optCompileDir <$> commandLineOptions
case mdir of
Just dir -> return dir
Nothing -> __IMPOSSIBLE__
repl :: [String] -> String -> String
repl subs = go where
go ('<':'<':c:'>':'>':s) | 0 <= i && i < length subs = subs !! i ++ go s
where i = ord c - ord '0'
go (c:s) = c : go s
go [] = []
inCompilerEnv :: Interface -> TCM a -> TCM a
inCompilerEnv mainI cont = do
(a , s) <- localTCStateSaving $ do
opts <- getsTC $ stPersistentOptions . stPersistentState
compileDir <- case optCompileDir opts of
Just dir -> return dir
Nothing -> do
let tm = toTopLevelModuleName $ iModuleName mainI
f <- srcFilePath <$> findFile tm
return $ filePath $ C.projectRoot f tm
setCommandLineOptions $
opts { optCompileDir = Just compileDir }
when (["--no-main"] `elem` iPragmaOptions mainI) $
stPragmaOptions `modifyTCLens` \ o -> o { optCompileNoMain = True }
setScope (iInsideScope mainI)
ignoreAbstractMode cont
let newWarnings = stPostTCWarnings $ stPostScopeState $ s
stTCWarnings `setTCLens` newWarnings
return a
topLevelModuleName :: ModuleName -> TCM ModuleName
topLevelModuleName m = do
visited <- List.map (iModuleName . miInterface) . Map.elems <$>
getVisitedModules
let ms = sortBy (compare `on` (length . mnameToList)) $
List.filter (\ m' -> mnameToList m' `isPrefixOf` mnameToList m) visited
case ms of
(m' : _) -> return m'
[] -> curMName