{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Agda.Compiler.Common where
import Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Char
import Data.Function
import Data.Semigroup
import Data.Monoid hiding ((<>))
import Control.Monad
import Control.Monad.State hiding (mapM_, forM_, mapM, forM, sequence)
import Agda.Syntax.Common
import qualified Agda.Syntax.Abstract.Name as A
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Internal as I
import Agda.Interaction.FindFile
import Agda.Interaction.Imports
import Agda.Interaction.Options
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty hiding ((<>))
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.FileName
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty hiding ((<>))
#include "undefined.h"
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 <- gets (stPersistentOptions . stPersistentState)
setCommandLineOptions opts
mapM_ setOptionsFromPragma (iPragmaOptions i)
stImportedModules .= Set.fromList (map fst $ iImportedModules i)
stCurrentModule .= Just (iModuleName i)
curIF :: TCM Interface
curIF = do
mName <- use 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 = (^. 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 [] = []
conArityAndPars :: QName -> TCM (Nat, Nat)
conArityAndPars q = do
def <- getConstInfo q
n <- typeArity (defType def)
let Constructor{ conPars = np } = theDef def
return (n - np, np)
inCompilerEnv :: Interface -> TCM a -> TCM a
inCompilerEnv mainI cont = do
(a , s) <- localTCStateSaving $ do
opts <- gets $ stPersistentOptions . stPersistentState
compileDir <- case optCompileDir opts of
Just dir -> return dir
Nothing -> do
let tm = toTopLevelModuleName $ iModuleName mainI
f <- findFile tm
return $ filePath $ C.projectRoot f tm
setCommandLineOptions $
opts { optCompileDir = Just compileDir }
when (["--no-main"] `elem` iPragmaOptions mainI) $
stPragmaOptions %= \ o -> o { optCompileNoMain = True }
setScope (iInsideScope mainI)
ignoreAbstractMode $ do
cont
let newWarnings = stPostTCWarnings $ stPostScopeState $ s
stTCWarnings .= 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