module Agda.Compiler.Common where
#if __GLASGOW_HASKELL__ <= 708
import Prelude hiding (foldl, mapM_, mapM, sequence, concat)
#endif
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 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
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
#include "undefined.h"
import Agda.Utils.Impossible
data IsMain = IsMain | NotMain
deriving (Eq)
doCompile :: IsMain -> Interface -> (IsMain -> Interface -> TCM ()) -> TCM ()
doCompile isMain i f = do
[agdaPrimInter] <- filter (("Agda.Primitive"==) . prettyShow . iModuleName)
. map miInterface . Map.elems
<$> getVisitedModules
flip evalStateT Set.empty $ comp NotMain agdaPrimInter >> comp isMain i
where
comp :: IsMain -> Interface -> StateT (Set ModuleName) TCM ()
comp isMain i = do
alreadyDone <- Set.member (iModuleName i) <$> get
when (not alreadyDone) $ do
imps <- lift $
map miInterface . catMaybes <$>
mapM (getVisitedModule . toTopLevelModuleName . fst) (iImportedModules i)
mapM_ (comp NotMain) imps
lift $ setInterface i
lift $ f NotMain i
modify (Set.insert $ iModuleName i)
setInterface :: Interface -> TCM ()
setInterface i = do
opts <- gets (stPersistentOptions . stPersistentState)
setCommandLineOptions opts
mapM_ setOptionsFromPragma (iPragmaOptions i)
stImportedModules .= Set.empty
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
TelV tel _ <- telView $ defType def
let Constructor{ conPars = np } = theDef def
n = length (telToList tel)
return (n np, np)
inCompilerEnv :: Interface -> TCM a -> TCM a
inCompilerEnv mainI cont =
localTCState $ 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 }
ignoreAbstractMode $ do
cont
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