summaryrefslogtreecommitdiff
path: root/src/full/Agda/Interaction/Imports.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Interaction/Imports.hs')
-rw-r--r--src/full/Agda/Interaction/Imports.hs55
1 files changed, 32 insertions, 23 deletions
diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs
index e193baa..02f1ca1 100644
--- a/src/full/Agda/Interaction/Imports.hs
+++ b/src/full/Agda/Interaction/Imports.hs
@@ -1,6 +1,10 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP #-}
{-# LANGUAGE TupleSections #-}
+#if __GLASGOW_HASKELL__ >= 710
+{-# LANGUAGE FlexibleContexts #-}
+#endif
+
{-| This module deals with finding imported modules and loading their
interface files.
-}
@@ -28,8 +32,6 @@ import System.FilePath ((</>))
import qualified Text.PrettyPrint.Boxes as Boxes
-import Paths_Agda (getDataFileName)
-
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Abstract.Name
@@ -46,12 +48,12 @@ import Agda.TypeChecking.Monad.Base.KillRange -- killRange for Signature
import Agda.TypeChecking.Serialise
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Primitive
-import Agda.TypeChecking.Monad.Benchmark (billTop, reimburseTop)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TheTypeChecker
import Agda.Interaction.FindFile
+import {-# SOURCE #-} Agda.Interaction.InteractionTop (showOpenMetas)
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Highlighting.Precise (HighlightingInfo)
@@ -131,7 +133,7 @@ scopeCheckImport x = do
" visited: " ++ intercalate ", " (map (render . pretty) visited)
-- Since scopeCheckImport is called from the scope checker,
-- we need to reimburse her account.
- i <- reimburseTop Bench.Scoping $ getInterface x
+ i <- Bench.billTo [] $ getInterface x
addImport x
return (iModuleName i `withRangesOfQ` mnameToConcrete x, iScope i)
@@ -179,11 +181,11 @@ typeCheckMain f = do
-- liftIO $ putStrLn $ "This is typeCheckMain " ++ show f
-- liftIO . putStrLn . show =<< getVerbosity
reportSLn "import.main" 10 $ "Importing the primitive modules."
- libpath <- liftIO $ getDataFileName "lib"
- reportSLn "import.main" 20 $ "Library path = " ++ show libpath
+ libdir <- liftIO defaultLibDir
+ reportSLn "import.main" 20 $ "Library dir = " ++ show libdir
-- To allow posulating the built-ins, check the primitive module
-- in unsafe mode
- bracket_ (gets $ Lens.getSafeMode) Lens.putSafeMode $ do
+ _ <- bracket_ (gets $ Lens.getSafeMode) Lens.putSafeMode $ do
Lens.putSafeMode False
-- Turn off import-chasing messages.
-- We have to modify the persistent verbosity setting, since
@@ -194,7 +196,7 @@ typeCheckMain f = do
withHighlightingLevel None $
getInterface_ =<< do
moduleName $ mkAbsolute $
- libpath </> "prim" </> "Agda" </> "Primitive.agda"
+ libdir </> "prim" </> "Agda" </> "Primitive.agda"
reportSLn "import.main" 10 $ "Done importing the primitive modules."
-- Now do the type checking via getInterface.
@@ -245,7 +247,7 @@ getInterface' x isMain = do
reportSLn "import.iface" 10 $ " Check for cycle"
checkForImportCycle
- uptodate <- billTop Bench.Import $ do
+ uptodate <- Bench.billTo [Bench.Import] $ do
ignore <- ignoreInterfaces
cached <- isCached file -- if it's cached ignoreInterfaces has no effect
-- to avoid typechecking a file more than once
@@ -279,7 +281,7 @@ getInterface' x isMain = do
else " New module. Let's check it out."
unless (visited || stateChangesIncluded) $ do
mergeInterface i
- billTop Bench.Highlighting $
+ Bench.billTo [Bench.Highlighting] $
ifTopLevelAndHighlightingLevelIs NonInteractive $
highlightFromInterface i file
@@ -324,7 +326,7 @@ getInterface' x isMain = do
let ifile = filePath $ toIFile file
h <- fmap snd <$> getInterfaceFileHashes ifile
mm <- getDecodedModule x
- (cached, mi) <- billTop Bench.Deserialization $ case mm of
+ (cached, mi) <- Bench.billTo [Bench.Deserialization] $ case mm of
Just mi ->
if Just (iFullHash mi) /= h
then do dropDecodedModule x
@@ -516,9 +518,10 @@ createInterface
-> C.TopLevelModuleName -- ^ The expected module name.
-> TCM (Interface, MaybeWarnings)
createInterface file mname =
- local (\e -> e { envCurrentPath = file }) $ do
+ local (\e -> e { envCurrentPath = Just file }) $ do
modFile <- use stModuleToSource
- fileTokenInfo <- billTop Bench.Highlighting $ generateTokenInfo file
+ fileTokenInfo <- Bench.billTo [Bench.Highlighting] $
+ generateTokenInfo file
stTokens .= fileTokenInfo
reportSLn "import.iface.create" 5 $
@@ -531,7 +534,7 @@ createInterface file mname =
previousHsImports <- getHaskellImports
-- Parsing.
- (pragmas, top) <- billTop Bench.Parsing $
+ (pragmas, top) <- Bench.billTo [Bench.Parsing] $
liftIO $ parseFile' moduleParser file
pragmas <- concat <$> concreteToAbstract_ pragmas
@@ -542,20 +545,20 @@ createInterface file mname =
mapM_ setOptionsFromPragma options
-- Scope checking.
- topLevel <- billTop Bench.Scoping $
+ topLevel <- Bench.billTo [Bench.Scoping] $
concreteToAbstract_ (TopLevel file top)
let ds = topLevelDecls topLevel
-- Highlighting from scope checker.
- billTop Bench.Highlighting $ do
+ Bench.billTo [Bench.Highlighting] $ do
ifTopLevelAndHighlightingLevelIs NonInteractive $ do
-- Generate and print approximate syntax highlighting info.
printHighlightingInfo fileTokenInfo
mapM_ (\ d -> generateAndPrintSyntaxInfo d Partial) ds
-- Type checking.
- billTop Bench.Typing $ checkDecls ds
+ Bench.billTo [Bench.Typing] $ checkDecls ds
-- Ulf, 2013-11-09: Since we're rethrowing the error, leave it up to the
-- code that handles that error to reset the state.
@@ -573,7 +576,7 @@ createInterface file mname =
tickN "metas" (fromIntegral n)
-- Highlighting from type checker.
- billTop Bench.Highlighting $ do
+ Bench.billTo [Bench.Highlighting] $ do
-- Move any remaining token highlighting to stSyntaxInfo.
toks <- use stTokens
@@ -591,13 +594,16 @@ createInterface file mname =
-- Serialization.
syntaxInfo <- use stSyntaxInfo
- i <- billTop Bench.Serialization $ do
+ i <- Bench.billTo [Bench.Serialization] $ do
buildInterface file topLevel syntaxInfo previousHsImports options
-- TODO: It would be nice if unsolved things were highlighted
-- after every mutual block.
- unsolvedMetas <- List.nub <$> (mapM getMetaRange =<< getOpenMetas)
+ openMetas <- getOpenMetas
+ unless (null openMetas) $ do
+ reportSLn "import.metas" 10 . unlines =<< showOpenMetas
+ unsolvedMetas <- List.nub <$> mapM getMetaRange openMetas
unsolvedConstraints <- getAllConstraints
interactionPoints <- getInteractionPoints
@@ -605,7 +611,7 @@ createInterface file mname =
printUnsolvedInfo
r <- if and [ null unsolvedMetas, null unsolvedConstraints, null interactionPoints ]
- then billTop Bench.Serialization $ do
+ then Bench.billTo [Bench.Serialization] $ do
-- The file was successfully type-checked (and no warnings were
-- encountered), so the interface should be written out.
let ifile = filePath $ toIFile file
@@ -655,7 +661,10 @@ buildInterface file topLevel syntaxInfo previousHsImports pragmas = do
ms <- getImports
mhs <- mapM (\ m -> (m,) <$> moduleHash m) $ Set.toList ms
hsImps <- getHaskellImports
- patsyns <- getPatternSyns
+ -- Andreas, 2015-02-09 kill ranges in pattern synonyms before
+ -- serialization to avoid error locations pointing to external files
+ -- when expanding a pattern synoym.
+ patsyns <- killRange <$> getPatternSyns
h <- liftIO $ hashFile file
let builtin' = Map.mapWithKey (\ x b -> (x,) . primFunName <$> b) builtin
reportSLn "import.iface" 7 " instantiating all meta variables"