diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,19 @@
 # Changelog
 
-## 0.1.0 (10/27/2020)
+## 0.1.0 (Oct 2020)
 
 Initial release.
+
+## 0.2.0 (May 2021)
+
+- Support code depending on external libraries.
+- Support Agda's library-related options (`--include-path`, etc.).
+- Remove support for `.agda-roots` file; use an ordinary Agda file instead.
+- Replace the `--local` option with a `--global` flag; default to a local check.
+- Remove the `--root` option; infer the project root directory automatically.
+- The `agda-unused` command now takes a filename as a positional argument.
+- Check variables in standalone data & record definitions.
+- Check renaming directives simultaneously (fixes bug).
+- Check record types with fields referencing other fields (fixes bug).
+- Check import statements with `as _` (fixes bug).
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -10,13 +10,15 @@
 - `open` statements
 - pattern synonyms
 
-`agda-unused` can be run globally on a full project, or locally on a file and
-its dependencies. Running `agda-unused` globally requires an `.agda-roots` file
-in the project root directory, which specifies the "roots" of the project. The
-"roots" of a project are identifiers that are considered used even if not used
-within the project itself. You might think of the `.agda-roots` file as a
-specification of the public interface of your project.
+`agda-unused` takes a filepath representing an Agda code file and checks for
+unused code in that file and its dependencies. By default, `agda-unused` does
+not check public items that could be imported elsewhere. But with the `--global`
+flag, `agda-unused` treats the given file as a description of the public
+interface of the project, and additionally checks for unused files and unused
+public items in dependencies. (See below for more on the `--global` flag.)
 
+Supported Agda versions: `>= 2.6.1 && < 2.6.2`
+
 ## Example
 
 File `~/Test.agda`:
@@ -41,7 +43,7 @@
 Command:
 
 ```
-$ agda-unused --local Test.agda
+$ agda-unused Test.agda
 ```
 
 Output:
@@ -55,69 +57,66 @@
   unused variable ‘x’
 ```
 
-## Roots
-
-Running `agda-unused` globally requires an `.agda-roots` file in the project
-root directory. The `.agda-roots` format consists of:
-
-- Module names, each followed by a list of (possibly qualified) identifiers.
-- Module names in parentheses.
-
-All given module names not in parentheses are checked, along with their
-dependencies. The given identifiers are considered roots; they will not be
-marked unused. Qualified identifiers refer to identifiers defined within inner
-modules. If no identifiers are given for a module, all publicly accessible
-identifiers are considered roots.
+## Usage
 
-All given module names in parentheses are ignored when checking for unused
-files. Such modules may still be checked if imported by another module.
+```
+agda-unused - check for unused code in an Agda project
 
-Example `.agda-roots` file:
+Usage: agda-unused FILE [-g|--global] [-j|--json]
+  Check for unused code in FILE
 
+Available options:
+  -h,--help                Show this help text
+  -g,--global              Check project globally
+  -j,--json                Format output as JSON
+  -i,--include-path DIR    Look for imports in DIR
+  -l,--library LIB         Use library LIB
+  --library-file FILE      Use FILE instead of the standard libraries file
+  --no-libraries           Don't use any library files
+  --no-default-libraries   Don't use default libraries
 ```
-Main
-- main
 
-Pythagorean.Core
-- isTriple
-- allTriples
+## Global
 
-(Pythagorean.Examples)
+If the `--global` flag is given, all declarations in the given file must be
+imports. The set of imported items is treated as the public interface of the
+project; these items will not be marked unused. The public items in dependencies
+of the given module may be marked unused, unlike the default behavior. We also
+check for unused files.
 
-Pythagorean.Theorems
+To perform a global check on an Agda project, first create a file that imports
+exactly the intended public interface of your project. For example:
 
-Pythagorean.Utils
-- Print.prettyNat
+File `All.agda`:
+
 ```
+module All where
 
-Spacing and indentation are irrelevant.
+import A
+  using (f)
+import B
+  hiding (g)
+import C
+```
 
-## Usage
+Command:
 
 ```
-Usage: agda-unused [-r|--root ROOT] [-l|--local FILE]
-  Check for unused code in project with root directory ROOT
-
-Available options:
-  -h,--help                Show this help text
-  -r,--root ROOT           Path of project root directory
-  -l,--local FILE          Path of file to check locally
-  -j,--json                Format output as JSON 
+$ agda-unused All.agda --global
 ```
 
-The project root directory is determined as follows:
+## JSON
 
-- If the `--root` option is given, its value is the project root.
-- If the `--local` option is given, the nearest ancestor with an `.agda-roots`
-  file is the project root, if any.
-- If the current directory has an `.agda-roots` file, it is the project root.
-- Otherwise, the nearest ancestor of the current directory with an `.agda-roots`
-  file is the project root, if any.
-- Otherwise, we take the current directory as the project root.
+If the `--json` flag is given, the output is a JSON object with two fields:
 
+- `type`: One of `"none"`, `"unused"`, `"error"`.
+- `message`: A string, the same as the usual output of `agda-unused`.
+
+The `"none"` type indicates that there is no unused code.
+
 ## Approach
 
-We make a single pass through each relevant Agda file:
+We make a single pass through the given Agda module and its dependencies:
 
 - When a new item (variable, definition, etc.) appears, we mark it unused.
 - When an existing item appears, we mark it used.
@@ -129,27 +128,23 @@
 different from Haskell's built-in tool, which would report that all three
 identifiers are unused on the first run.
 
-For a global check, we check each file appearing in `.agda-roots` and its
-dependencies. For a local check, we check just the given file and its
-dependencies, ignoring all publicly accessible definitions.
-
-## JSON
-
-If the `--json` switch is given, the output is a JSON object with two fields:
-
-- `type`: One of `"none"`, `"unused"`, `"error"`.
-- `message`: A string, the same as the usual output of `agda-unused`.
+## Limitations
 
-The `"none"` type indicates that there is no unused code.
+We work with Agda's concrete syntax. This is a necessary choice, since Agda's
+abstract syntax doesn't distinguish between qualified and (opened) unqualified
+names, which would make it impossible to determine whether certain `open`
+statements are unused. However, using concrete syntax comes with several
+drawbacks:
 
-## Limitations
+- We do not parse mixfix operators; if the parts of a mixfix operator are used
+  in order in an expression, then we mark the mixfix operator as used.
+- We do not distinguish between overloaded constructors; if a constructor is
+  used, then we mark all constructors in scope with the same name as used.
 
-We currently do not support the following Agda features:
+Additionally, we currently do not support the following Agda features:
 
-- [record module instance applications](https://agda.readthedocs.io/en/v2.6.1.1/language/module-system.html#parameterised-modules)
-- [unquoting declarations](https://agda.readthedocs.io/en/v2.6.1.1/language/reflection.html#id3)
-- [external libraries](https://agda.readthedocs.io/en/v2.6.1.1/tools/package-system.html)
-(other than Agda's built-in libraries)
+- [record module instance applications](https://agda.readthedocs.io/en/v2.6.1.3/language/module-system.html#parameterised-modules)
+- [unquoting declarations](https://agda.readthedocs.io/en/v2.6.1.3/language/reflection.html#id3)
 
 `agda-unused` will produce an error if your code uses these language features.
 
diff --git a/agda-unused.cabal b/agda-unused.cabal
--- a/agda-unused.cabal
+++ b/agda-unused.cabal
@@ -3,7 +3,7 @@
 name:
   agda-unused
 version:
-  0.1.0
+  0.2.0
 build-type:
   Simple
 license:
@@ -39,25 +39,18 @@
     Agda.Unused.Monad.Error
     Agda.Unused.Monad.Reader
     Agda.Unused.Monad.State
-    Agda.Unused.Parse
     Agda.Unused.Print
     Agda.Unused.Types.Access
     Agda.Unused.Types.Context
     Agda.Unused.Types.Name
     Agda.Unused.Types.Range
-    Agda.Unused.Types.Root
     Agda.Unused.Utils
-  other-modules:
-    Paths_agda_unused
-  autogen-modules:
-    Paths_agda_unused
   build-depends:
-    base >= 4.13.0 && < 4.14,
+    base >= 4.13 && < 4.15,
     Agda >= 2.6.1 && < 2.6.2,
     containers >= 0.6.2 && < 0.7,
     directory >= 1.3.6 && < 1.4,
     filepath >= 1.4.2 && < 1.5,
-    megaparsec >= 8.0.0 && < 8.1,
     mtl >= 2.2.2 && < 2.3,
     text >= 1.2.4 && < 1.3
   default-language:
@@ -78,12 +71,11 @@
     Main.hs
   build-depends:
     agda-unused,
-    base >= 4.13.0 && < 4.14,
-    aeson >= 1.4.7 && < 1.5,
+    base >= 4.13 && < 4.15,
+    aeson >= 1.4.7 && < 1.6,
     directory >= 1.3.6 && < 1.4,
-    filepath >= 1.4.2 && < 1.5,
     mtl >= 2.2.2 && < 2.3,
-    optparse-applicative >= 0.15.1 && < 0.16,
+    optparse-applicative >= 0.15.1 && < 0.17,
     text >= 1.2.4 && < 1.3
   default-language:
     Haskell2010
@@ -107,7 +99,7 @@
     Paths_agda_unused
   build-depends:
     agda-unused,
-    base >= 4.13.0 && < 4.14,
+    base >= 4.13 && < 4.15,
     containers >= 0.6.2 && < 0.7,
     filepath >= 1.4.2 && < 1.5,
     hspec >= 2.7.1 && < 2.8,
@@ -115,9 +107,8 @@
   default-language:
     Haskell2010
   default-extensions:
-    FlexibleInstances,
     GADTs,
-    TypeSynonymInstances
+    OverloadedStrings
   ghc-options:
     -Wall
 
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,30 +1,24 @@
 module Main where
 
+import Agda.Unused
+  (UnusedOptions(..))
 import Agda.Unused.Check
-  (checkUnused, checkUnusedLocal)
-import qualified Agda.Unused.Monad.Error
-  as E
-import Agda.Unused.Parse
-  (parseConfig)
-import qualified Agda.Unused.Print
-  as P
-import Agda.Unused.Types.Name
-  (Name(..), NamePart(..), QName(..))
-import Agda.Unused.Utils
-  (liftMaybe, mapLeft)
+  (checkUnused, checkUnusedGlobal)
+import Agda.Unused.Monad.Error
+  (Error)
+import Agda.Unused.Print
+  (printError, printNothing, printUnused, printUnusedItems)
 
+import Control.Monad
+  (unless)
 import Control.Monad.Except
-  (MonadError, liftEither, runExceptT, throwError)
+  (MonadError, runExceptT, throwError)
 import Control.Monad.IO.Class
   (MonadIO, liftIO)
 import Data.Aeson
   (Value(..), (.=), object)
 import Data.Aeson.Text
   (encodeToLazyText)
-import Data.Bool
-  (bool)
-import Data.List
-  (stripPrefix)
 import Data.Text
   (Text)
 import qualified Data.Text
@@ -35,13 +29,12 @@
   (toStrict)
 import Options.Applicative
   (InfoMod, Parser, ParserInfo, execParser, fullDesc, header, help, helper,
-    info, long, metavar, optional, progDesc, short, strOption, switch)
+    hidden, info, long, many, metavar, optional, progDesc, short, strArgument,
+    strOption, switch)
 import System.Directory
-  (doesFileExist, getCurrentDirectory, makeAbsolute)
+  (doesDirectoryExist, doesFileExist, makeAbsolute)
 import System.Exit
   (exitFailure, exitSuccess)
-import System.FilePath
-  ((</>), splitDirectories, stripExtension, takeDirectory)
 import System.IO
   (stderr)
 
@@ -49,41 +42,120 @@
 
 data Options
   = Options
-  { optionsRoot
-    :: !(Maybe FilePath)
-    -- ^ The project root path.
-  , optionsFile
-    :: !(Maybe FilePath)
-    -- ^ A file path to check locally.
+  { optionsFile
+    :: !FilePath
+    -- ^ Path of the file to check.
+  , optionsGlobal
+    :: !Bool
+    -- ^ Whether to check project globally.
   , optionsJSON
     :: !Bool
-    -- ^ Whether to output JSON.
+    -- ^ Whether to format output as JSON.
+  , optionsInclude
+    :: ![FilePath]
+    -- ^ Include paths.
+  , optionsLibraries
+    :: ![Text]
+    -- ^ Libraries.
+  , optionsLibrariesFile
+    :: Maybe FilePath
+    -- ^ Alternate libraries file.
+  , optionsNoLibraries
+    :: Bool
+    -- ^ Whether to not use any library files.
+  , optionsNoDefaultLibraries
+    :: Bool
+    -- ^ Whether to not use default libraries.
   } deriving Show
 
+-- Convert options; print error message & exit on failure.
+optionsUnused
+  :: Options
+  -> IO (FilePath, UnusedOptions)
+optionsUnused opts
+  = runExceptT (optionsUnused' opts)
+  >>= optionsUnusedEither
+
+optionsUnusedEither
+  :: Either OptionsError (FilePath, UnusedOptions)
+  -> IO (FilePath, UnusedOptions)
+optionsUnusedEither (Left e)
+  = I.hPutStrLn stderr (printOptionsError e) >> exitFailure
+optionsUnusedEither (Right opts)
+  = pure opts
+
+optionsUnused'
+  :: MonadError OptionsError m
+  => MonadIO m
+  => Options
+  -> m (FilePath, UnusedOptions)
+optionsUnused' opts = do
+  filePath
+    <- validateFile (optionsFile opts)
+  includePaths
+    <- traverse validateDirectory (optionsInclude opts)
+  libraryPath
+    <- traverse validateFile (optionsLibrariesFile opts)
+  pure
+    $ (,) filePath
+    $ UnusedOptions
+    { unusedOptionsInclude
+      = includePaths
+    , unusedOptionsLibraries
+      = optionsLibraries opts
+    , unusedOptionsLibrariesFile
+      = libraryPath
+    , unusedOptionsUseLibraries
+      = not (optionsNoLibraries opts)
+    , unusedOptionsUseDefaultLibraries
+      = not (optionsNoDefaultLibraries opts)
+    }
+
 optionsParser
   :: Parser Options
 optionsParser
   = Options
-  <$> optional (strOption
-    $ short 'r'
-    <> long "root"
-    <> metavar "ROOT"
-    <> help "Path of project root directory")
-  <*> optional (strOption
-    $ short 'l'
-    <> long "local"
-    <> metavar "FILE"
-    <> help "Path of file to check locally")
+  <$> (strArgument
+    $ metavar "FILE")
   <*> (switch
+    $ short 'g'
+    <> long "global"
+    <> help "Check project globally")
+  <*> (switch
     $ short 'j'
     <> long "json"
     <> help "Format output as JSON")
+  <*> many (strOption
+    $ short 'i'
+    <> long "include-path"
+    <> metavar "DIR"
+    <> help "Look for imports in DIR"
+    <> hidden)
+  <*> many (strOption
+    $ short 'l'
+    <> long "library"
+    <> metavar "LIB"
+    <> help "Use library LIB"
+    <> hidden)
+  <*> optional (strOption
+    $ long "library-file"
+    <> metavar "FILE"
+    <> help "Use FILE instead of the standard libraries file"
+    <> hidden)
+  <*> (switch
+    $ long "no-libraries"
+    <> help "Don't use any library files"
+    <> hidden)
+  <*> (switch
+    $ long "no-default-libraries"
+    <> help "Don't use default libraries"
+    <> hidden)
 
 optionsInfo
   :: InfoMod a
 optionsInfo
   = fullDesc
-  <> progDesc "Check for unused code in project with root directory ROOT"
+  <> progDesc "Check for unused code in FILE"
   <> header "agda-unused - check for unused code in an Agda project"
 
 options
@@ -91,88 +163,90 @@
 options
   = info (helper <*> optionsParser) optionsInfo
 
--- ## Errors
+-- ## Validate
 
-data Error where
- 
-  ErrorFile
-    :: !FilePath
-    -> Error
+data OptionsError where
 
-  ErrorLocal
-    :: !FilePath
-    -> Error
+  ErrorFile
+    :: FilePath
+    -> OptionsError
 
-  ErrorParse
-    :: !Text
-    -> Error
+  ErrorDirectory
+    :: FilePath
+    -> OptionsError
 
   deriving Show
 
--- ## Check
+printOptionsError
+  :: OptionsError
+  -> Text
+printOptionsError (ErrorFile p)
+  = "Error: File not found " <> parens (T.pack p) <> "."
+printOptionsError (ErrorDirectory p)
+  = "Error: Directory not found " <> parens (T.pack p) <> "."
 
-check
-  :: Options
-  -> IO ()
-check o@(Options _ _ j)
-  = runExceptT (check' o)
-  >>= either (printErrorWith j) (const (pure ()))
+parens
+  :: Text
+  -> Text
+parens t
+  = "(" <> t <> ")"
 
-check'
-  :: MonadError Error m
+validateFile
+  :: MonadError OptionsError m
   => MonadIO m
-  => Options
-  -> m ()
-
-check' o@(Options _ Nothing j) = do
-  rootPath
-    <- liftIO (getRootDirectory o)
-  configPath
-    <- pure (rootPath </> ".agda-roots")
+  => FilePath
+  -> m FilePath
+validateFile p = do
   exists
-    <- liftIO (doesFileExist configPath)
-  _
-    <- bool (throwError (ErrorFile configPath)) (pure ()) exists
-  contents
-    <- liftIO (I.readFile configPath)
-  roots
-    <- liftEither (mapLeft ErrorParse (parseConfig contents))
-  checkResult
-    <- liftIO (checkUnused rootPath roots)
+    <- liftIO (doesFileExist p)
   _
-    <- liftIO (printResult j P.printUnused checkResult)
-  pure ()
+    <- unless exists (throwError (ErrorFile p))
+  filePath
+    <- liftIO (makeAbsolute p)
+  pure filePath
 
-check' o@(Options _ (Just f) j) = do
-  rootPath
-    <- liftIO (getRootDirectory o)
-  rootPath'
-    <- pure (splitDirectories rootPath)
+validateDirectory
+  :: MonadError OptionsError m
+  => MonadIO m
+  => FilePath
+  -> m FilePath
+validateDirectory p = do
+  exists
+    <- liftIO (doesDirectoryExist p)
+  _
+    <- unless exists (throwError (ErrorDirectory p))
   filePath
-    <- liftIO (makeAbsolute f >>= \f' -> pure (splitDirectories f'))
-  localModule
-    <- liftMaybe (ErrorLocal f) (stripPrefix rootPath' filePath >>= pathModule)
-  checkResult
-    <- liftIO (checkUnusedLocal rootPath localModule)
+    <- liftIO (makeAbsolute p)
+  pure filePath
+
+-- ## Check
+
+check
+  :: Options
+  -> IO ()
+check opts = do
+  (filePath, opts')
+    <- optionsUnused opts
   _
-    <- liftIO (printResult j P.printUnusedItems checkResult)
+    <- checkWith opts' filePath (optionsGlobal opts) (optionsJSON opts)
   pure ()
 
-pathModule
-  :: [FilePath]
-  -> Maybe QName
-pathModule []
-  = Nothing
-pathModule (p : [])
-  = QName . name <$> stripExtension "agda" p
-pathModule (p : ps@(_ : _))
-  = Qual (name p) <$> pathModule ps
-
-name
-  :: String
-  -> Name
-name p
-  = Name [Id p]
+checkWith
+  :: UnusedOptions
+  -- ^ Options to use.
+  -> FilePath
+  -- ^ Absolute path of the file to check.
+  -> Bool
+  -- ^ Whether to check project globally.
+  -> Bool
+  -- ^ Whether to format output as JSON.
+  -> IO ()
+checkWith opts p False j
+  = checkUnused opts p
+  >>= printResult j printUnusedItems
+checkWith opts p True j
+  = checkUnusedGlobal opts p
+  >>= printResult j printUnused
 
 -- ## Print
 
@@ -180,57 +254,23 @@
   :: Bool
   -- ^ Whether to output JSON.
   -> (a -> Maybe Text)
-  -> Either E.Error a
+  -> Either Error a
   -> IO ()
 printResult False _ (Left e)
-  = I.hPutStrLn stderr (P.printError e) >> exitFailure
+  = I.hPutStrLn stderr (printError e) >> exitFailure
 printResult False p (Right x)
-  = I.putStrLn (maybe P.printNothing id (p x)) >> exitSuccess
+  = I.putStrLn (maybe printNothing id (p x)) >> exitSuccess
 printResult True p x
   = I.putStrLn (toStrict (encodeToLazyText (printResultJSON p x)))
 
-printErrorWith
-  :: Bool
-  -- ^ Whether to output JSON.
-  -> Error
-  -> IO ()
-printErrorWith False e
-  = I.hPutStrLn stderr (printError e) >> exitFailure
-printErrorWith True e
-  = I.putStrLn (toStrict (encodeToLazyText (printErrorJSON e)))
-
-printError
-  :: Error
-  -> Text
-printError (ErrorFile p)
-  = "Error: .agda-roots file not found " <> parens (T.pack p) <> "."
-printError (ErrorLocal l)
-  = "Error: Invalid local path " <> parens (T.pack l) <> "."
-printError (ErrorParse t)
-  = t
-
-parens
-  :: Text
-  -> Text
-parens t
-  = "(" <> t <> ")"
-
--- ## JSON
-
-printErrorJSON
-  :: Error
-  -> Value
-printErrorJSON e
-  = encodeMessage "error" (printError e)
-
 printResultJSON
   :: (a -> Maybe Text)
-  -> Either E.Error a
+  -> Either Error a
   -> Value
 printResultJSON _ (Left e)
-  = encodeMessage "error" (P.printError e)
+  = encodeMessage "error" (printError e)
 printResultJSON p (Right u)
-  = maybe (encodeMessage "none" P.printNothing) (encodeMessage "unused") (p u)
+  = maybe (encodeMessage "none" printNothing) (encodeMessage "unused") (p u)
 
 encodeMessage
   :: Text
@@ -239,46 +279,12 @@
   -- ^ Contents of message.
   -> Value
 encodeMessage t m
-  = object ["type" .= t, "message" .= m]
-
--- ## Root
-
-getRootDirectory
-  :: Options
-  -> IO FilePath
-getRootDirectory (Options Nothing Nothing _)
-  = getCurrentDirectory
-  >>= \p -> getRootDirectoryFrom p p
-getRootDirectory (Options Nothing (Just p) _)
-  = makeAbsolute p
-  >>= \p' -> getRootDirectoryFrom (takeDirectory p') (takeDirectory p')
-getRootDirectory (Options (Just p) _ _)
-  = makeAbsolute p
-
--- Search recursively upwards for project root directory.
-getRootDirectoryFrom
-  :: FilePath
-  -- ^ Default directory.
-  -> FilePath
-  -- ^ Starting directory.
-  -> IO FilePath
-getRootDirectoryFrom d p
-  = doesFileExist (p </> ".agda-roots") >>= getRootDirectoryWith d p
-
-getRootDirectoryWith
-  :: FilePath
-  -- ^ Default directory.
-  -> FilePath
-  -- ^ Starting directory.
-  -> Bool
-  -- ^ Whether the starting directory contains an .agda-roots file.
-  -> IO FilePath
-getRootDirectoryWith _ p True
-  = pure p
-getRootDirectoryWith d p False | takeDirectory p == p
-  = pure d
-getRootDirectoryWith d p False
-  = getRootDirectoryFrom d (takeDirectory p)
+  = object
+  [ "type"
+    .= t
+  , "message"
+    .= m
+  ]
 
 -- ## Main
 
diff --git a/data/Agda/Builtin/Bool.agda b/data/Agda/Builtin/Bool.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Bool.agda
+++ /dev/null
@@ -1,17 +0,0 @@
-{-# OPTIONS --without-K --safe --no-universe-polymorphism
-            --no-sized-types --no-guardedness  --no-subtyping #-}
-
-module Agda.Builtin.Bool where
-
-data Bool : Set where
-  false true : Bool
-
-{-# BUILTIN BOOL  Bool  #-}
-{-# BUILTIN FALSE false #-}
-{-# BUILTIN TRUE  true  #-}
-
-{-# COMPILE UHC Bool = data __BOOL__ (__FALSE__ | __TRUE__) #-}
-
-{-# COMPILE JS Bool  = function (x,v) { return ((x)? v["true"]() : v["false"]()); } #-}
-{-# COMPILE JS false = false #-}
-{-# COMPILE JS true  = true  #-}
diff --git a/data/Agda/Builtin/Char.agda b/data/Agda/Builtin/Char.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Char.agda
+++ /dev/null
@@ -1,18 +0,0 @@
-{-# OPTIONS --without-K --safe --no-universe-polymorphism
-            --no-sized-types --no-guardedness --no-subtyping #-}
-
-module Agda.Builtin.Char where
-
-open import Agda.Builtin.Nat
-open import Agda.Builtin.Bool
-
-postulate Char : Set
-{-# BUILTIN CHAR Char #-}
-
-primitive
-  primIsLower primIsDigit primIsAlpha primIsSpace primIsAscii
-    primIsLatin1 primIsPrint primIsHexDigit : Char → Bool
-  primToUpper primToLower : Char → Char
-  primCharToNat : Char → Nat
-  primNatToChar : Nat → Char
-  primCharEquality : Char → Char → Bool
diff --git a/data/Agda/Builtin/Char/Properties.agda b/data/Agda/Builtin/Char/Properties.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Char/Properties.agda
+++ /dev/null
@@ -1,11 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Char.Properties where
-
-open import Agda.Builtin.Char
-open import Agda.Builtin.Equality
-
-primitive
-
-  primCharToNatInjective : ∀ a b → primCharToNat a ≡ primCharToNat b → a ≡ b
diff --git a/data/Agda/Builtin/Coinduction.agda b/data/Agda/Builtin/Coinduction.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Coinduction.agda
+++ /dev/null
@@ -1,15 +0,0 @@
-{-# OPTIONS --without-K --safe --universe-polymorphism --no-sized-types
-            --no-guardedness --no-subtyping #-}
-
-module Agda.Builtin.Coinduction where
-
-infix 1000 ♯_
-
-postulate
-  ∞  : ∀ {a} (A : Set a) → Set a
-  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
-  ♭  : ∀ {a} {A : Set a} → ∞ A → A
-
-{-# BUILTIN INFINITY ∞  #-}
-{-# BUILTIN SHARP    ♯_ #-}
-{-# BUILTIN FLAT     ♭  #-}
diff --git a/data/Agda/Builtin/Cubical/Glue.agda b/data/Agda/Builtin/Cubical/Glue.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Cubical/Glue.agda
+++ /dev/null
@@ -1,123 +0,0 @@
-{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Cubical.Glue where
-
-open import Agda.Primitive
-open import Agda.Builtin.Sigma
-open import Agda.Primitive.Cubical renaming (primINeg to ~_; primIMax to _∨_; primIMin to _∧_;
-                                             primHComp to hcomp; primTransp to transp; primComp to comp;
-                                             itIsOne to 1=1)
-open import Agda.Builtin.Cubical.Path
-open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to ouc)
-import Agda.Builtin.Cubical.HCompU as HCompU
-
-module Helpers = HCompU.Helpers
-
-open Helpers
-
-
--- We make this a record so that isEquiv can be proved using
--- copatterns. This is good because copatterns don't get unfolded
--- unless a projection is applied so it should be more efficient.
-record isEquiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : Set (ℓ ⊔ ℓ') where
-  no-eta-equality
-  field
-    equiv-proof : (y : B) → isContr (fiber f y)
-
-open isEquiv public
-
-infix 4 _≃_
-
-
-_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
-A ≃ B = Σ (A → B) \ f → (isEquiv f)
-
-equivFun : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A ≃ B → A → B
-equivFun e = fst e
-
--- Improved version of equivProof compared to Lemma 5 in CCHM. We put
--- the (φ = i0) face in contr' making it be definitionally c in this
--- case. This makes the computational behavior better, in particular
--- for transp in Glue.
-equivProof : ∀ {la lt} (T : Set la) (A : Set lt) → (w : T ≃ A) → (a : A)
-           → ∀ ψ → (Partial ψ (fiber (w .fst) a)) → fiber (w .fst) a
-equivProof A B w a ψ fb = contr' {A = fiber (w .fst) a} (w .snd .equiv-proof a) ψ fb
-  where
-    contr' : ∀ {ℓ} {A : Set ℓ} → isContr A → (φ : I) → (u : Partial φ A) → A
-    contr' {A = A} (c , p) φ u = hcomp (λ i → λ { (φ = i1) → p (u 1=1) i
-                                                ; (φ = i0) → c }) c
-
-
-{-# BUILTIN EQUIV      _≃_        #-}
-{-# BUILTIN EQUIVFUN   equivFun   #-}
-{-# BUILTIN EQUIVPROOF equivProof #-}
-
-primitive
-    primGlue    : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
-      → (T : Partial φ (Set ℓ')) → (e : PartialP φ (λ o → T o ≃ A))
-      → Set ℓ'
-    prim^glue   : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
-      → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
-      → (t : PartialP φ T) → (a : A) → primGlue A T e
-    prim^unglue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
-      → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
-      → primGlue A T e → A
-
-    -- Needed for transp in Glue.
-    primFaceForall : (I → I) → I
-
-
-module _ {ℓ : I → Level} (P : (i : I) → Set (ℓ i)) where
-  private
-    E : (i : I) → Set (ℓ i)
-    E  = λ i → P i
-    ~E : (i : I) → Set (ℓ (~ i))
-    ~E = λ i → P (~ i)
-
-    A = P i0
-    B = P i1
-
-    f : A → B
-    f x = transp E i0 x
-
-    g : B → A
-    g y = transp ~E i0 y
-
-    u : ∀ i → A → E i
-    u i x = transp (λ j → E (i ∧ j)) (~ i) x
-
-    v : ∀ i → B → E i
-    v i y = transp (λ j → ~E ( ~ i ∧ j)) i y
-
-    fiberPath : (y : B) → (xβ0 xβ1 : fiber f y) → xβ0 ≡ xβ1
-    fiberPath y (x0 , β0) (x1 , β1) k = ω , λ j → δ (~ j) where
-      module _ (j : I) where
-        private
-          sys : A → ∀ i → PartialP (~ j ∨ j) (λ _ → E (~ i))
-          sys x i (j = i0) = v (~ i) y
-          sys x i (j = i1) = u (~ i) x
-        ω0 = comp ~E (sys x0) ((β0 (~ j)))
-        ω1 = comp ~E (sys x1) ((β1 (~ j)))
-        θ0 = fill ~E (sys x0) (inc (β0 (~ j)))
-        θ1 = fill ~E (sys x1) (inc (β1 (~ j)))
-      sys = λ {j (k = i0) → ω0 j ; j (k = i1) → ω1 j}
-      ω = hcomp sys (g y)
-      θ = hfill sys (inc (g y))
-      δ = λ (j : I) → comp E
-            (λ i → λ { (j = i0) → v i y ; (k = i0) → θ0 j (~ i)
-                     ; (j = i1) → u i ω ; (k = i1) → θ1 j (~ i) })
-             (θ j)
-
-    γ : (y : B) → y ≡ f (g y)
-    γ y j = comp E (λ i → λ { (j = i0) → v i y
-                            ; (j = i1) → u i (g y) }) (g y)
-
-  pathToisEquiv : isEquiv f
-  pathToisEquiv .equiv-proof y .fst .fst = g y
-  pathToisEquiv .equiv-proof y .fst .snd = sym (γ y)
-  pathToisEquiv .equiv-proof y .snd = fiberPath y _
-
-  pathToEquiv : A ≃ B
-  pathToEquiv .fst = f
-  pathToEquiv .snd = pathToisEquiv
diff --git a/data/Agda/Builtin/Cubical/HCompU.agda b/data/Agda/Builtin/Cubical/HCompU.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Cubical/HCompU.agda
+++ /dev/null
@@ -1,73 +0,0 @@
-{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Cubical.HCompU where
-
-open import Agda.Primitive
-open import Agda.Builtin.Sigma
-open import Agda.Primitive.Cubical renaming (primINeg to ~_; primIMax to _∨_; primIMin to _∧_;
-                                             primHComp to hcomp; primTransp to transp; primComp to comp;
-                                             itIsOne to 1=1)
-open import Agda.Builtin.Cubical.Path
-open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to outS; inc to inS)
-
-module Helpers where
-    -- Homogeneous filling
-    hfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
-              (u : ∀ i → Partial φ A)
-              (u0 : A [ φ ↦ u i0 ]) (i : I) → A
-    hfill {φ = φ} u u0 i =
-      hcomp (λ j → \ { (φ = i1) → u (i ∧ j) 1=1
-                     ; (i = i0) → outS u0 })
-            (outS u0)
-
-    -- Heterogeneous filling defined using comp
-    fill : ∀ {ℓ : I → Level} (A : ∀ i → Set (ℓ i)) {φ : I}
-             (u : ∀ i → Partial φ (A i))
-             (u0 : A i0 [ φ ↦ u i0 ]) →
-             ∀ i →  A i
-    fill A {φ = φ} u u0 i =
-      comp (λ j → A (i ∧ j))
-           (λ j → \ { (φ = i1) → u (i ∧ j) 1=1
-                    ; (i = i0) → outS u0 })
-           (outS {φ = φ} u0)
-
-    module _ {ℓ} {A : Set ℓ} where
-      refl : {x : A} → x ≡ x
-      refl {x = x} = λ _ → x
-
-      sym : {x y : A} → x ≡ y → y ≡ x
-      sym p = λ i → p (~ i)
-
-      cong : ∀ {ℓ'} {B : A → Set ℓ'} {x y : A}
-             (f : (a : A) → B a) (p : x ≡ y)
-           → PathP (λ i → B (p i)) (f x) (f y)
-      cong f p = λ i → f (p i)
-
-    isContr : ∀ {ℓ} → Set ℓ → Set ℓ
-    isContr A = Σ A \ x → (∀ y → x ≡ y)
-
-    fiber : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) (y : B) → Set (ℓ ⊔ ℓ')
-    fiber {A = A} f y = Σ A \ x → f x ≡ y
-
-open Helpers
-
-
-primitive
-  prim^glueU : {la : Level} {φ : I} {T : I → Partial φ (Set la)}
-                 {A : Set la [ φ ↦ T i0 ]} →
-                 PartialP φ (T i1) → outS A → hcomp T (outS A)
-  prim^unglueU : {la : Level} {φ : I} {T : I → Partial φ (Set la)}
-                   {A : Set la [ φ ↦ T i0 ]} →
-                   hcomp T (outS A) → outS A
-
-transpProof : ∀ {l} → (e : I → Set l) → (φ : I) → (a : Partial φ (e i0)) → (b : e i1 [ φ ↦ (\ o → transp e i0 (a o)) ] ) → fiber (transp e i0) (outS b)
-transpProof e φ a b = f , \ j → comp e (\ i → \ { (φ = i1) → transp (\ j → e (j ∧ i)) (~ i) (a 1=1)
-                                                 ; (j = i0) → transp (\ j → e (j ∧ i)) (~ i) f
-                                                 ; (j = i1) → g (~ i) })
-                                        f
-    where
-      g = fill (\ i → e (~ i)) (\ i → \ { (φ = i1) → transp (\ j → e (j ∧ ~ i)) i (a 1=1); (φ = i0) → transp (\ j → e (~ j ∨ ~ i)) (~ i) (outS b) }) (inS (outS b))
-      f = comp (\ i → e (~ i)) (\ i → \ { (φ = i1) → transp (\ j → e (j ∧ ~ i)) i (a 1=1); (φ = i0) → transp (\ j → e (~ j ∨ ~ i)) (~ i) (outS b) }) (outS b)
-
-{-# BUILTIN TRANSPPROOF transpProof #-}
diff --git a/data/Agda/Builtin/Cubical/Id.agda b/data/Agda/Builtin/Cubical/Id.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Cubical/Id.agda
+++ /dev/null
@@ -1,32 +0,0 @@
-{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Cubical.Id where
-
-  open import Agda.Primitive.Cubical
-  open import Agda.Builtin.Cubical.Path
-  open import Agda.Builtin.Cubical.Sub renaming (primSubOut to ouc; Sub to _[_↦_])
-
-  postulate
-    Id : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
-
-  {-# BUILTIN ID           Id       #-}
-  {-# BUILTIN CONID        conid    #-}
-
-  primitive
-    primDepIMin : _
-    primIdFace : ∀ {ℓ} {A : Set ℓ} {x y : A} → Id x y → I
-    primIdPath : ∀ {ℓ} {A : Set ℓ} {x y : A} → Id x y → x ≡ y
-
-  primitive
-    primIdJ : ∀ {ℓ ℓ'} {A : Set ℓ} {x : A} (P : ∀ y → Id x y → Set ℓ') →
-                P x (conid i1 (λ i → x)) → ∀ {y} (p : Id x y) → P y p
-
-
-  primitive
-    primIdElim : ∀ {a c} {A : Set a} {x : A}
-                   (C : (y : A) → Id x y → Set c) →
-                   ((φ : I) (y : A [ φ ↦ (λ _ → x) ])
-                    (w : (x ≡ ouc y) [ φ ↦ (λ { (φ = i1) → \ _ → x}) ]) →
-                    C (ouc y) (conid φ (ouc w))) →
-                   {y : A} (p : Id x y) → C y p
diff --git a/data/Agda/Builtin/Cubical/Path.agda b/data/Agda/Builtin/Cubical/Path.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Cubical/Path.agda
+++ /dev/null
@@ -1,20 +0,0 @@
-{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Cubical.Path where
-
-  open import Agda.Primitive.Cubical
-
-  postulate
-    PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ
-
-  {-# BUILTIN PATHP        PathP     #-}
-
-  infix 4 _≡_
-
-  -- We have a variable name in `(λ i → A)` as a hint for case
-  -- splitting.
-  _≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
-  _≡_ {A = A} = PathP (λ i → A)
-
-  {-# BUILTIN PATH         _≡_     #-}
diff --git a/data/Agda/Builtin/Cubical/Sub.agda b/data/Agda/Builtin/Cubical/Sub.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Cubical/Sub.agda
+++ /dev/null
@@ -1,16 +0,0 @@
-{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Cubical.Sub where
-
-  open import Agda.Primitive.Cubical
-
-  {-# BUILTIN SUB Sub #-}
-
-  postulate
-    inc : ∀ {ℓ} {A : Set ℓ} {φ} (x : A) → Sub A φ (λ _ → x)
-
-  {-# BUILTIN SUBIN inc #-}
-
-  primitive
-    primSubOut : ∀ {ℓ} {A : Set ℓ} {φ : I} {u : Partial φ A} → Sub _ φ u → A
diff --git a/data/Agda/Builtin/Equality.agda b/data/Agda/Builtin/Equality.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Equality.agda
+++ /dev/null
@@ -1,10 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Equality where
-
-infix 4 _≡_
-data _≡_ {a} {A : Set a} (x : A) : A → Set a where
-  instance refl : x ≡ x
-
-{-# BUILTIN EQUALITY _≡_ #-}
diff --git a/data/Agda/Builtin/Equality/Erase.agda b/data/Agda/Builtin/Equality/Erase.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Equality/Erase.agda
+++ /dev/null
@@ -1,8 +0,0 @@
-{-# OPTIONS --with-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Equality.Erase where
-
-open import Agda.Builtin.Equality
-
-primitive primEraseEquality : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y
diff --git a/data/Agda/Builtin/Equality/Rewrite.agda b/data/Agda/Builtin/Equality/Rewrite.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Equality/Rewrite.agda
+++ /dev/null
@@ -1,8 +0,0 @@
-{-# OPTIONS --without-K --rewriting --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Equality.Rewrite where
-
-open import Agda.Builtin.Equality
-
-{-# BUILTIN REWRITE _≡_ #-}
diff --git a/data/Agda/Builtin/Float.agda b/data/Agda/Builtin/Float.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Float.agda
+++ /dev/null
@@ -1,40 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Float where
-
-open import Agda.Builtin.Bool
-open import Agda.Builtin.Nat
-open import Agda.Builtin.Int
-open import Agda.Builtin.Word
-open import Agda.Builtin.String
-
-postulate Float : Set
-{-# BUILTIN FLOAT Float #-}
-
-primitive
-  primFloatToWord64 : Float → Word64
-  primFloatEquality : Float → Float → Bool
-  primFloatLess     : Float → Float → Bool
-  primFloatNumericalEquality : Float → Float → Bool
-  primFloatNumericalLess     : Float → Float → Bool
-  primNatToFloat    : Nat → Float
-  primFloatPlus     : Float → Float → Float
-  primFloatMinus    : Float → Float → Float
-  primFloatTimes    : Float → Float → Float
-  primFloatNegate   : Float → Float
-  primFloatDiv      : Float → Float → Float
-  primFloatSqrt     : Float → Float
-  primRound         : Float → Int
-  primFloor         : Float → Int
-  primCeiling       : Float → Int
-  primExp           : Float → Float
-  primLog           : Float → Float
-  primSin           : Float → Float
-  primCos           : Float → Float
-  primTan           : Float → Float
-  primASin          : Float → Float
-  primACos          : Float → Float
-  primATan          : Float → Float
-  primATan2         : Float → Float → Float
-  primShowFloat     : Float → String
diff --git a/data/Agda/Builtin/Float/Properties.agda b/data/Agda/Builtin/Float/Properties.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Float/Properties.agda
+++ /dev/null
@@ -1,11 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Float.Properties where
-
-open import Agda.Builtin.Float
-open import Agda.Builtin.Equality
-
-primitive
-
-  primFloatToWord64Injective : ∀ a b → primFloatToWord64 a ≡ primFloatToWord64 b → a ≡ b
diff --git a/data/Agda/Builtin/FromNat.agda b/data/Agda/Builtin/FromNat.agda
deleted file mode 100644
--- a/data/Agda/Builtin/FromNat.agda
+++ /dev/null
@@ -1,17 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.FromNat where
-
-open import Agda.Primitive
-open import Agda.Builtin.Nat
-
-record Number {a} (A : Set a) : Set (lsuc a) where
-  field
-    Constraint : Nat → Set a
-    fromNat : ∀ n → {{_ : Constraint n}} → A
-
-open Number {{...}} public using (fromNat)
-
-{-# BUILTIN FROMNAT fromNat #-}
-{-# DISPLAY Number.fromNat _ n = fromNat n #-}
diff --git a/data/Agda/Builtin/FromNeg.agda b/data/Agda/Builtin/FromNeg.agda
deleted file mode 100644
--- a/data/Agda/Builtin/FromNeg.agda
+++ /dev/null
@@ -1,17 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.FromNeg where
-
-open import Agda.Primitive
-open import Agda.Builtin.Nat
-
-record Negative {a} (A : Set a) : Set (lsuc a) where
-  field
-    Constraint : Nat → Set a
-    fromNeg : ∀ n → {{_ : Constraint n}} → A
-
-open Negative {{...}} public using (fromNeg)
-
-{-# BUILTIN FROMNEG fromNeg #-}
-{-# DISPLAY Negative.fromNeg _ n = fromNeg n #-}
diff --git a/data/Agda/Builtin/FromString.agda b/data/Agda/Builtin/FromString.agda
deleted file mode 100644
--- a/data/Agda/Builtin/FromString.agda
+++ /dev/null
@@ -1,17 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.FromString where
-
-open import Agda.Primitive
-open import Agda.Builtin.String
-
-record IsString {a} (A : Set a) : Set (lsuc a) where
-  field
-    Constraint : String → Set a
-    fromString : (s : String) {{_ : Constraint s}} → A
-
-open IsString {{...}} public using (fromString)
-
-{-# BUILTIN FROMSTRING fromString #-}
-{-# DISPLAY IsString.fromString _ s = fromString s #-}
diff --git a/data/Agda/Builtin/IO.agda b/data/Agda/Builtin/IO.agda
deleted file mode 100644
--- a/data/Agda/Builtin/IO.agda
+++ /dev/null
@@ -1,11 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.IO where
-
-postulate IO : ∀ {a} → Set a → Set a
-{-# POLARITY IO ++ ++ #-}
-{-# BUILTIN IO IO #-}
-
-{-# FOREIGN GHC type AgdaIO a b = IO b #-}
-{-# COMPILE GHC IO = type AgdaIO #-}
diff --git a/data/Agda/Builtin/Int.agda b/data/Agda/Builtin/Int.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Int.agda
+++ /dev/null
@@ -1,19 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Int where
-
-open import Agda.Builtin.Nat
-open import Agda.Builtin.String
-
-infix 8 pos  -- Standard library uses this as +_
-
-data Int : Set where
-  pos    : (n : Nat) → Int
-  negsuc : (n : Nat) → Int
-
-{-# BUILTIN INTEGER       Int    #-}
-{-# BUILTIN INTEGERPOS    pos    #-}
-{-# BUILTIN INTEGERNEGSUC negsuc #-}
-
-primitive primShowInteger : Int → String
diff --git a/data/Agda/Builtin/List.agda b/data/Agda/Builtin/List.agda
deleted file mode 100644
--- a/data/Agda/Builtin/List.agda
+++ /dev/null
@@ -1,18 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.List where
-
-infixr 5 _∷_
-data List {a} (A : Set a) : Set a where
-  []  : List A
-  _∷_ : (x : A) (xs : List A) → List A
-
-{-# BUILTIN LIST List #-}
-
-{-# COMPILE UHC List = data __LIST__ (__NIL__ | __CONS__) #-}
-{-# COMPILE JS  List = function(x,v) {
-  if (x.length < 1) { return v["[]"](); } else { return v["_∷_"](x[0], x.slice(1)); }
-} #-}
-{-# COMPILE JS [] = Array() #-}
-{-# COMPILE JS _∷_ = function (x) { return function(y) { return Array(x).concat(y); }; } #-}
diff --git a/data/Agda/Builtin/Nat.agda b/data/Agda/Builtin/Nat.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Nat.agda
+++ /dev/null
@@ -1,134 +0,0 @@
-{-# OPTIONS --without-K --safe --no-universe-polymorphism
-            --no-sized-types --no-guardedness --no-subtyping #-}
-
-module Agda.Builtin.Nat where
-
-open import Agda.Builtin.Bool
-
-data Nat : Set where
-  zero : Nat
-  suc  : (n : Nat) → Nat
-
-{-# BUILTIN NATURAL Nat #-}
-
-infix  4 _==_ _<_
-infixl 6 _+_ _-_
-infixl 7 _*_
-
-_+_ : Nat → Nat → Nat
-zero  + m = m
-suc n + m = suc (n + m)
-
-{-# BUILTIN NATPLUS _+_ #-}
-
-_-_ : Nat → Nat → Nat
-n     - zero = n
-zero  - suc m = zero
-suc n - suc m = n - m
-
-{-# BUILTIN NATMINUS _-_ #-}
-
-_*_ : Nat → Nat → Nat
-zero  * m = zero
-suc n * m = m + n * m
-
-{-# BUILTIN NATTIMES _*_ #-}
-
-_==_ : Nat → Nat → Bool
-zero  == zero  = true
-suc n == suc m = n == m
-_     == _     = false
-
-{-# BUILTIN NATEQUALS _==_ #-}
-
-_<_ : Nat → Nat → Bool
-_     < zero  = false
-zero  < suc _ = true
-suc n < suc m = n < m
-
-{-# BUILTIN NATLESS _<_ #-}
-
--- Helper function  div-helper  for Euclidean division.
----------------------------------------------------------------------------
---
--- div-helper computes n / 1+m via iteration on n.
---
---   n div (suc m) = div-helper 0 m n m
---
--- The state of the iterator has two accumulator variables:
---
---   k: The quotient, returned once n=0.  Initialized to 0.
---
---   j: A counter, initialized to the divisor m, decreased on each iteration step.
---      Once it reaches 0, the quotient k is increased and j reset to m,
---      starting the next countdown.
---
--- Under the precondition j ≤ m, the invariant is
---
---   div-helper k m n j = k + (n + m - j) div (1 + m)
-
-div-helper : (k m n j : Nat) → Nat
-div-helper k m  zero    j      = k
-div-helper k m (suc n)  zero   = div-helper (suc k) m n m
-div-helper k m (suc n) (suc j) = div-helper k       m n j
-
-{-# BUILTIN NATDIVSUCAUX div-helper #-}
-
--- Proof of the invariant by induction on n.
---
---   clause 1: div-helper k m 0 j
---           = k                                        by definition
---           = k + (0 + m - j) div (1 + m)              since m - j < 1 + m
---
---   clause 2: div-helper k m (1 + n) 0
---           = div-helper (1 + k) m n m                 by definition
---           = 1 + k + (n + m - m) div (1 + m)          by induction hypothesis
---           = 1 + k +          n  div (1 + m)          by simplification
---           = k +   (n + (1 + m)) div (1 + m)          by expansion
---           = k + (1 + n + m - 0) div (1 + m)          by expansion
---
---   clause 3: div-helper k m (1 + n) (1 + j)
---           = div-helper k m n j                       by definition
---           = k + (n + m - j) div (1 + m)              by induction hypothesis
---           = k + ((1 + n) + m - (1 + j)) div (1 + m)  by expansion
---
--- Q.e.d.
-
--- Helper function  mod-helper  for the remainder computation.
----------------------------------------------------------------------------
---
--- (Analogous to div-helper.)
---
--- mod-helper computes n % 1+m via iteration on n.
---
---   n mod (suc m) = mod-helper 0 m n m
---
--- The invariant is:
---
---   m = k + j  ==>  mod-helper k m n j = (n + k) mod (1 + m).
-
-mod-helper : (k m n j : Nat) → Nat
-mod-helper k m  zero    j      = k
-mod-helper k m (suc n)  zero   = mod-helper 0       m n m
-mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j
-
-{-# BUILTIN NATMODSUCAUX mod-helper #-}
-
--- Proof of the invariant by induction on n.
---
---   clause 1: mod-helper k m 0 j
---           = k                               by definition
---           = (0 + k) mod (1 + m)             since m = k + j, thus k < m
---
---   clause 2: mod-helper k m (1 + n) 0
---           = mod-helper 0 m n m              by definition
---           = (n + 0)       mod (1 + m)       by induction hypothesis
---           = (n + (1 + m)) mod (1 + m)       by expansion
---           = (1 + n) + k)  mod (1 + m)       since k = m (as l = 0)
---
---   clause 3: mod-helper k m (1 + n) (1 + j)
---           = mod-helper (1 + k) m n j        by definition
---           = (n + (1 + k)) mod (1 + m)       by induction hypothesis
---           = ((1 + n) + k) mod (1 + m)       by commutativity
---
--- Q.e.d.
diff --git a/data/Agda/Builtin/Reflection.agda b/data/Agda/Builtin/Reflection.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Reflection.agda
+++ /dev/null
@@ -1,314 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Reflection where
-
-open import Agda.Builtin.Unit
-open import Agda.Builtin.Bool
-open import Agda.Builtin.Nat
-open import Agda.Builtin.Word
-open import Agda.Builtin.List
-open import Agda.Builtin.String
-open import Agda.Builtin.Char
-open import Agda.Builtin.Float
-open import Agda.Builtin.Int
-open import Agda.Builtin.Sigma
-
--- Names --
-
-postulate Name : Set
-{-# BUILTIN QNAME Name #-}
-
-primitive
-  primQNameEquality : Name → Name → Bool
-  primQNameLess     : Name → Name → Bool
-  primShowQName     : Name → String
-
--- Fixity --
-
-data Associativity : Set where
-  left-assoc  : Associativity
-  right-assoc : Associativity
-  non-assoc   : Associativity
-
-data Precedence : Set where
-  related   : Float → Precedence
-  unrelated : Precedence
-
-data Fixity : Set where
-  fixity : Associativity → Precedence → Fixity
-
-{-# BUILTIN ASSOC      Associativity #-}
-{-# BUILTIN ASSOCLEFT  left-assoc    #-}
-{-# BUILTIN ASSOCRIGHT right-assoc   #-}
-{-# BUILTIN ASSOCNON   non-assoc     #-}
-
-{-# BUILTIN PRECEDENCE    Precedence #-}
-{-# BUILTIN PRECRELATED   related    #-}
-{-# BUILTIN PRECUNRELATED unrelated  #-}
-
-{-# BUILTIN FIXITY       Fixity #-}
-{-# BUILTIN FIXITYFIXITY fixity #-}
-
-{-# COMPILE GHC Associativity = data MAlonzo.RTE.Assoc (MAlonzo.RTE.LeftAssoc | MAlonzo.RTE.RightAssoc | MAlonzo.RTE.NonAssoc) #-}
-{-# COMPILE GHC Precedence    = data MAlonzo.RTE.Precedence (MAlonzo.RTE.Related | MAlonzo.RTE.Unrelated) #-}
-{-# COMPILE GHC Fixity        = data MAlonzo.RTE.Fixity (MAlonzo.RTE.Fixity) #-}
-
-{-# COMPILE JS Associativity  = function (x,v) { return v[x](); } #-}
-{-# COMPILE JS left-assoc     = "left-assoc"  #-}
-{-# COMPILE JS right-assoc    = "right-assoc" #-}
-{-# COMPILE JS non-assoc      = "non-assoc"   #-}
-
-{-# COMPILE JS Precedence     =
-  function (x,v) {
-    if (x === "unrelated") { return v[x](); } else { return v["related"](x); }} #-}
-{-# COMPILE JS related        = function(x) { return x; } #-}
-{-# COMPILE JS unrelated      = "unrelated"               #-}
-
-{-# COMPILE JS Fixity         = function (x,v) { return v["fixity"](x["assoc"], x["prec"]); } #-}
-{-# COMPILE JS fixity         = function (x) { return function (y) { return { "assoc": x, "prec": y}; }; } #-}
-
-primitive
-  primQNameFixity : Name → Fixity
-  primQNameToWord64s : Name → Σ Word64 (λ _ → Word64)
-
--- Metavariables --
-
-postulate Meta : Set
-{-# BUILTIN AGDAMETA Meta #-}
-
-primitive
-  primMetaEquality : Meta → Meta → Bool
-  primMetaLess     : Meta → Meta → Bool
-  primShowMeta     : Meta → String
-  primMetaToNat    : Meta → Nat
-
--- Arguments --
-
--- Arguments can be (visible), {hidden}, or {{instance}}.
-data Visibility : Set where
-  visible hidden instance′ : Visibility
-
-{-# BUILTIN HIDING   Visibility #-}
-{-# BUILTIN VISIBLE  visible    #-}
-{-# BUILTIN HIDDEN   hidden     #-}
-{-# BUILTIN INSTANCE instance′  #-}
-
--- Arguments can be relevant or irrelevant.
-data Relevance : Set where
-  relevant irrelevant : Relevance
-
-{-# BUILTIN RELEVANCE  Relevance  #-}
-{-# BUILTIN RELEVANT   relevant   #-}
-{-# BUILTIN IRRELEVANT irrelevant #-}
-
-data ArgInfo : Set where
-  arg-info : (v : Visibility) (r : Relevance) → ArgInfo
-
-data Arg {a} (A : Set a) : Set a where
-  arg : (i : ArgInfo) (x : A) → Arg A
-
-{-# BUILTIN ARGINFO    ArgInfo  #-}
-{-# BUILTIN ARGARGINFO arg-info #-}
-{-# BUILTIN ARG        Arg      #-}
-{-# BUILTIN ARGARG     arg      #-}
-
--- Name abstraction --
-
-data Abs {a} (A : Set a) : Set a where
-  abs : (s : String) (x : A) → Abs A
-
-{-# BUILTIN ABS    Abs #-}
-{-# BUILTIN ABSABS abs #-}
-
--- Literals --
-
-data Literal : Set where
-  nat    : (n : Nat)    → Literal
-  word64 : (n : Word64) → Literal
-  float  : (x : Float)  → Literal
-  char   : (c : Char)   → Literal
-  string : (s : String) → Literal
-  name   : (x : Name)   → Literal
-  meta   : (x : Meta)   → Literal
-
-{-# BUILTIN AGDALITERAL   Literal #-}
-{-# BUILTIN AGDALITNAT    nat     #-}
-{-# BUILTIN AGDALITWORD64 word64  #-}
-{-# BUILTIN AGDALITFLOAT  float   #-}
-{-# BUILTIN AGDALITCHAR   char    #-}
-{-# BUILTIN AGDALITSTRING string  #-}
-{-# BUILTIN AGDALITQNAME  name    #-}
-{-# BUILTIN AGDALITMETA   meta    #-}
-
--- Patterns --
-
-data Pattern : Set where
-  con    : (c : Name) (ps : List (Arg Pattern)) → Pattern
-  dot    : Pattern
-  var    : (s : String)  → Pattern
-  lit    : (l : Literal) → Pattern
-  proj   : (f : Name)    → Pattern
-  absurd : Pattern
-
-{-# BUILTIN AGDAPATTERN   Pattern #-}
-{-# BUILTIN AGDAPATCON    con     #-}
-{-# BUILTIN AGDAPATDOT    dot     #-}
-{-# BUILTIN AGDAPATVAR    var     #-}
-{-# BUILTIN AGDAPATLIT    lit     #-}
-{-# BUILTIN AGDAPATPROJ   proj    #-}
-{-# BUILTIN AGDAPATABSURD absurd  #-}
-
--- Terms --
-
-data Sort   : Set
-data Clause : Set
-data Term   : Set
-Type = Term
-
-data Term where
-  var       : (x : Nat) (args : List (Arg Term)) → Term
-  con       : (c : Name) (args : List (Arg Term)) → Term
-  def       : (f : Name) (args : List (Arg Term)) → Term
-  lam       : (v : Visibility) (t : Abs Term) → Term
-  pat-lam   : (cs : List Clause) (args : List (Arg Term)) → Term
-  pi        : (a : Arg Type) (b : Abs Type) → Term
-  agda-sort : (s : Sort) → Term
-  lit       : (l : Literal) → Term
-  meta      : (x : Meta) → List (Arg Term) → Term
-  unknown   : Term
-
-data Sort where
-  set     : (t : Term) → Sort
-  lit     : (n : Nat) → Sort
-  unknown : Sort
-
-data Clause where
-  clause        : (ps : List (Arg Pattern)) (t : Term) → Clause
-  absurd-clause : (ps : List (Arg Pattern)) → Clause
-
-{-# BUILTIN AGDASORT    Sort   #-}
-{-# BUILTIN AGDATERM    Term   #-}
-{-# BUILTIN AGDACLAUSE  Clause #-}
-
-{-# BUILTIN AGDATERMVAR         var       #-}
-{-# BUILTIN AGDATERMCON         con       #-}
-{-# BUILTIN AGDATERMDEF         def       #-}
-{-# BUILTIN AGDATERMMETA        meta      #-}
-{-# BUILTIN AGDATERMLAM         lam       #-}
-{-# BUILTIN AGDATERMEXTLAM      pat-lam   #-}
-{-# BUILTIN AGDATERMPI          pi        #-}
-{-# BUILTIN AGDATERMSORT        agda-sort #-}
-{-# BUILTIN AGDATERMLIT         lit       #-}
-{-# BUILTIN AGDATERMUNSUPPORTED unknown   #-}
-
-{-# BUILTIN AGDASORTSET         set     #-}
-{-# BUILTIN AGDASORTLIT         lit     #-}
-{-# BUILTIN AGDASORTUNSUPPORTED unknown #-}
-
-{-# BUILTIN AGDACLAUSECLAUSE clause        #-}
-{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}
-
--- Definitions --
-
-data Definition : Set where
-  function    : (cs : List Clause) → Definition
-  data-type   : (pars : Nat) (cs : List Name) → Definition
-  record-type : (c : Name) (fs : List (Arg Name)) → Definition
-  data-cons   : (d : Name) → Definition
-  axiom       : Definition
-  prim-fun    : Definition
-
-{-# BUILTIN AGDADEFINITION                Definition  #-}
-{-# BUILTIN AGDADEFINITIONFUNDEF          function    #-}
-{-# BUILTIN AGDADEFINITIONDATADEF         data-type   #-}
-{-# BUILTIN AGDADEFINITIONRECORDDEF       record-type #-}
-{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR data-cons   #-}
-{-# BUILTIN AGDADEFINITIONPOSTULATE       axiom       #-}
-{-# BUILTIN AGDADEFINITIONPRIMITIVE       prim-fun    #-}
-
--- Errors --
-
-data ErrorPart : Set where
-  strErr  : String → ErrorPart
-  termErr : Term → ErrorPart
-  nameErr : Name → ErrorPart
-
-{-# BUILTIN AGDAERRORPART       ErrorPart #-}
-{-# BUILTIN AGDAERRORPARTSTRING strErr    #-}
-{-# BUILTIN AGDAERRORPARTTERM   termErr   #-}
-{-# BUILTIN AGDAERRORPARTNAME   nameErr   #-}
-
--- TC monad --
-
-postulate
-  TC               : ∀ {a} → Set a → Set a
-  returnTC         : ∀ {a} {A : Set a} → A → TC A
-  bindTC           : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
-  unify            : Term → Term → TC ⊤
-  typeError        : ∀ {a} {A : Set a} → List ErrorPart → TC A
-  inferType        : Term → TC Type
-  checkType        : Term → Type → TC Term
-  normalise        : Term → TC Term
-  reduce           : Term → TC Term
-  catchTC          : ∀ {a} {A : Set a} → TC A → TC A → TC A
-  quoteTC          : ∀ {a} {A : Set a} → A → TC Term
-  unquoteTC        : ∀ {a} {A : Set a} → Term → TC A
-  getContext       : TC (List (Arg Type))
-  extendContext    : ∀ {a} {A : Set a} → Arg Type → TC A → TC A
-  inContext        : ∀ {a} {A : Set a} → List (Arg Type) → TC A → TC A
-  freshName        : String → TC Name
-  declareDef       : Arg Name → Type → TC ⊤
-  declarePostulate : Arg Name → Type → TC ⊤
-  defineFun        : Name → List Clause → TC ⊤
-  getType          : Name → TC Type
-  getDefinition    : Name → TC Definition
-  blockOnMeta      : ∀ {a} {A : Set a} → Meta → TC A
-  commitTC         : TC ⊤
-  isMacro          : Name → TC Bool
-
-  -- If the argument is 'true' makes the following primitives also normalise
-  -- their results: inferType, checkType, quoteTC, getType, and getContext
-  withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A
-
-  -- Prints the third argument if the corresponding verbosity level is turned
-  -- on (with the -v flag to Agda).
-  debugPrint : String → Nat → List ErrorPart → TC ⊤
-
-  -- Fail if the given computation gives rise to new, unsolved
-  -- "blocking" constraints.
-  noConstraints : ∀ {a} {A : Set a} → TC A → TC A
-
-  -- Run the given TC action and return the first component. Resets to
-  -- the old TC state if the second component is 'false', or keep the
-  -- new TC state if it is 'true'.
-  runSpeculative : ∀ {a} {A : Set a} → TC (Σ A λ _ → Bool) → TC A
-
-{-# BUILTIN AGDATCM                           TC                         #-}
-{-# BUILTIN AGDATCMRETURN                     returnTC                   #-}
-{-# BUILTIN AGDATCMBIND                       bindTC                     #-}
-{-# BUILTIN AGDATCMUNIFY                      unify                      #-}
-{-# BUILTIN AGDATCMTYPEERROR                  typeError                  #-}
-{-# BUILTIN AGDATCMINFERTYPE                  inferType                  #-}
-{-# BUILTIN AGDATCMCHECKTYPE                  checkType                  #-}
-{-# BUILTIN AGDATCMNORMALISE                  normalise                  #-}
-{-# BUILTIN AGDATCMREDUCE                     reduce                     #-}
-{-# BUILTIN AGDATCMCATCHERROR                 catchTC                    #-}
-{-# BUILTIN AGDATCMQUOTETERM                  quoteTC                    #-}
-{-# BUILTIN AGDATCMUNQUOTETERM                unquoteTC                  #-}
-{-# BUILTIN AGDATCMGETCONTEXT                 getContext                 #-}
-{-# BUILTIN AGDATCMEXTENDCONTEXT              extendContext              #-}
-{-# BUILTIN AGDATCMINCONTEXT                  inContext                  #-}
-{-# BUILTIN AGDATCMFRESHNAME                  freshName                  #-}
-{-# BUILTIN AGDATCMDECLAREDEF                 declareDef                 #-}
-{-# BUILTIN AGDATCMDECLAREPOSTULATE           declarePostulate           #-}
-{-# BUILTIN AGDATCMDEFINEFUN                  defineFun                  #-}
-{-# BUILTIN AGDATCMGETTYPE                    getType                    #-}
-{-# BUILTIN AGDATCMGETDEFINITION              getDefinition              #-}
-{-# BUILTIN AGDATCMBLOCKONMETA                blockOnMeta                #-}
-{-# BUILTIN AGDATCMCOMMIT                     commitTC                   #-}
-{-# BUILTIN AGDATCMISMACRO                    isMacro                    #-}
-{-# BUILTIN AGDATCMWITHNORMALISATION          withNormalisation          #-}
-{-# BUILTIN AGDATCMDEBUGPRINT                 debugPrint                 #-}
-{-# BUILTIN AGDATCMNOCONSTRAINTS              noConstraints              #-}
-{-# BUILTIN AGDATCMRUNSPECULATIVE             runSpeculative             #-}
diff --git a/data/Agda/Builtin/Reflection/Properties.agda b/data/Agda/Builtin/Reflection/Properties.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Reflection/Properties.agda
+++ /dev/null
@@ -1,12 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Reflection.Properties where
-
-open import Agda.Builtin.Reflection
-open import Agda.Builtin.Equality
-
-primitive
-
-  primMetaToNatInjective : ∀ a b → primMetaToNat a ≡ primMetaToNat b → a ≡ b
-  primQNameToWord64sInjective : ∀ a b → primQNameToWord64s a ≡ primQNameToWord64s b → a ≡ b
diff --git a/data/Agda/Builtin/Sigma.agda b/data/Agda/Builtin/Sigma.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Sigma.agda
+++ /dev/null
@@ -1,18 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Sigma where
-
-open import Agda.Primitive
-
-record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
-  constructor _,_
-  field
-    fst : A
-    snd : B fst
-
-open Σ public
-
-infixr 4 _,_
-
-{-# BUILTIN SIGMA Σ #-}
diff --git a/data/Agda/Builtin/Size.agda b/data/Agda/Builtin/Size.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Size.agda
+++ /dev/null
@@ -1,21 +0,0 @@
-{-# OPTIONS --without-K --safe --no-universe-polymorphism --sized-types
-            --no-guardedness --no-subtyping #-}
-
-module Agda.Builtin.Size where
-
-{-# BUILTIN SIZEUNIV SizeU #-}
-{-# BUILTIN SIZE     Size   #-}
-{-# BUILTIN SIZELT   Size<_ #-}
-{-# BUILTIN SIZESUC  ↑_     #-}
-{-# BUILTIN SIZEINF  ∞      #-}
-{-# BUILTIN SIZEMAX  _⊔ˢ_  #-}
-
-{-# FOREIGN GHC
-  type SizeLT i = ()
-  #-}
-
-{-# COMPILE GHC Size   = type ()     #-}
-{-# COMPILE GHC Size<_ = type SizeLT #-}
-{-# COMPILE GHC ↑_     = \_ -> ()    #-}
-{-# COMPILE GHC ∞      = ()          #-}
-{-# COMPILE GHC _⊔ˢ_   = \_ _ -> ()  #-}
diff --git a/data/Agda/Builtin/Strict.agda b/data/Agda/Builtin/Strict.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Strict.agda
+++ /dev/null
@@ -1,10 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Strict where
-
-open import Agda.Builtin.Equality
-
-primitive
-  primForce      : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
-  primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x
diff --git a/data/Agda/Builtin/String.agda b/data/Agda/Builtin/String.agda
deleted file mode 100644
--- a/data/Agda/Builtin/String.agda
+++ /dev/null
@@ -1,28 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.String where
-
-open import Agda.Builtin.Bool
-open import Agda.Builtin.List
-open import Agda.Builtin.Char
-open import Agda.Builtin.Nat using (Nat)
-
-postulate String : Set
-{-# BUILTIN STRING String #-}
-
-primitive
-  primStringToList   : String → List Char
-  primStringFromList : List Char → String
-  primStringAppend   : String → String → String
-  primStringEquality : String → String → Bool
-  primShowChar       : Char → String
-  primShowString     : String → String
-  primShowNat        : Nat → String
-
-{-# COMPILE JS primStringToList = function(x) { return x.split(""); } #-}
-{-# COMPILE JS primStringFromList = function(x) { return x.join(""); } #-}
-{-# COMPILE JS primStringAppend = function(x) { return function(y) { return x+y; }; } #-}
-{-# COMPILE JS primStringEquality = function(x) { return function(y) { return x===y; }; } #-}
-{-# COMPILE JS primShowChar = function(x) { return JSON.stringify(x); } #-}
-{-# COMPILE JS primShowString = function(x) { return JSON.stringify(x); } #-}
diff --git a/data/Agda/Builtin/String/Properties.agda b/data/Agda/Builtin/String/Properties.agda
deleted file mode 100644
--- a/data/Agda/Builtin/String/Properties.agda
+++ /dev/null
@@ -1,11 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.String.Properties where
-
-open import Agda.Builtin.String
-open import Agda.Builtin.Equality
-
-primitive
-
-  primStringToListInjective : ∀ a b → primStringToList a ≡ primStringToList b → a ≡ b
diff --git a/data/Agda/Builtin/TrustMe.agda b/data/Agda/Builtin/TrustMe.agda
deleted file mode 100644
--- a/data/Agda/Builtin/TrustMe.agda
+++ /dev/null
@@ -1,15 +0,0 @@
-{-# OPTIONS --no-sized-types --no-guardedness --no-subtyping #-}
-
-module Agda.Builtin.TrustMe where
-
-open import Agda.Builtin.Equality
-open import Agda.Builtin.Equality.Erase
-
-private
-  postulate
-    unsafePrimTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
-
-primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
-primTrustMe = primEraseEquality unsafePrimTrustMe
-
-{-# DISPLAY primEraseEquality unsafePrimTrustMe = primTrustMe #-}
diff --git a/data/Agda/Builtin/Unit.agda b/data/Agda/Builtin/Unit.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Unit.agda
+++ /dev/null
@@ -1,10 +0,0 @@
-{-# OPTIONS --without-K --safe --no-universe-polymorphism
-            --no-sized-types --no-guardedness --no-subtyping #-}
-
-module Agda.Builtin.Unit where
-
-record ⊤ : Set where
-  instance constructor tt
-
-{-# BUILTIN UNIT ⊤ #-}
-{-# COMPILE GHC ⊤ = data () (()) #-}
diff --git a/data/Agda/Builtin/Word.agda b/data/Agda/Builtin/Word.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Word.agda
+++ /dev/null
@@ -1,13 +0,0 @@
-{-# OPTIONS --without-K --safe --no-universe-polymorphism
-            --no-sized-types --no-guardedness --no-subtyping #-}
-
-module Agda.Builtin.Word where
-
-open import Agda.Builtin.Nat
-
-postulate Word64 : Set
-{-# BUILTIN WORD64 Word64 #-}
-
-primitive
-  primWord64ToNat   : Word64 → Nat
-  primWord64FromNat : Nat → Word64
diff --git a/data/Agda/Builtin/Word/Properties.agda b/data/Agda/Builtin/Word/Properties.agda
deleted file mode 100644
--- a/data/Agda/Builtin/Word/Properties.agda
+++ /dev/null
@@ -1,11 +0,0 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
-            --no-subtyping #-}
-
-module Agda.Builtin.Word.Properties where
-
-open import Agda.Builtin.Word
-open import Agda.Builtin.Equality
-
-primitive
-
-  primWord64ToNatInjective : ∀ a b → primWord64ToNat a ≡ primWord64ToNat b → a ≡ b
diff --git a/data/Agda/Primitive.agda b/data/Agda/Primitive.agda
deleted file mode 100644
--- a/data/Agda/Primitive.agda
+++ /dev/null
@@ -1,33 +0,0 @@
--- The Agda primitives (preloaded).
-
-{-# OPTIONS --without-K --no-subtyping #-}
-
-module Agda.Primitive where
-
-------------------------------------------------------------------------
--- Universe levels
-------------------------------------------------------------------------
-
-infixl 6 _⊔_
-
--- Level is the first thing we need to define.
--- The other postulates can only be checked if built-in Level is known.
-
-postulate
-  Level : Set
-
--- MAlonzo compiles Level to (). This should be safe, because it is
--- not possible to pattern match on levels.
-
-{-# BUILTIN LEVEL Level #-}
-
-postulate
-  lzero : Level
-  lsuc  : (ℓ : Level) → Level
-  _⊔_   : (ℓ₁ ℓ₂ : Level) → Level
-
-{-# BUILTIN LEVELZERO lzero #-}
-{-# BUILTIN LEVELSUC  lsuc  #-}
-{-# BUILTIN LEVELMAX  _⊔_   #-}
-
-{-# BUILTIN SETOMEGA Setω #-}
diff --git a/data/Agda/Primitive/Cubical.agda b/data/Agda/Primitive/Cubical.agda
deleted file mode 100644
--- a/data/Agda/Primitive/Cubical.agda
+++ /dev/null
@@ -1,53 +0,0 @@
-{-# OPTIONS --cubical --no-subtyping #-}
-
-module Agda.Primitive.Cubical where
-
-{-# BUILTIN INTERVAL I  #-}  -- I : Setω
-
-{-# BUILTIN IZERO    i0 #-}
-{-# BUILTIN IONE     i1 #-}
-
-infix  30 primINeg
-infixr 20 primIMin primIMax
-
-primitive
-    primIMin : I → I → I
-    primIMax : I → I → I
-    primINeg : I → I
-
-{-# BUILTIN ISONE    IsOne    #-}  -- IsOne : I → Setω
-
-postulate
-  itIsOne : IsOne i1
-  IsOne1  : ∀ i j → IsOne i → IsOne (primIMax i j)
-  IsOne2  : ∀ i j → IsOne j → IsOne (primIMax i j)
-
-{-# BUILTIN ITISONE  itIsOne  #-}
-{-# BUILTIN ISONE1   IsOne1   #-}
-{-# BUILTIN ISONE2   IsOne2   #-}
-
--- Partial : ∀{ℓ} (i : I) (A : Set ℓ) → Set ℓ
--- Partial i A = IsOne i → A
-
-{-# BUILTIN PARTIAL  Partial  #-}
-{-# BUILTIN PARTIALP PartialP #-}
-
-postulate
-  isOneEmpty : ∀ {ℓ} {A : Partial i0 (Set ℓ)} → PartialP i0 A
-
-{-# BUILTIN ISONEEMPTY isOneEmpty #-}
-
-primitive
-  primPOr : ∀ {ℓ} (i j : I) {A : Partial (primIMax i j) (Set ℓ)}
-            → (u : PartialP i (λ z → A (IsOne1 i j z)))
-            → (v : PartialP j (λ z → A (IsOne2 i j z)))
-            → PartialP (primIMax i j) A
-
-  -- Computes in terms of primHComp and primTransp
-  primComp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) {φ : I} (u : ∀ i → Partial φ (A i)) (a : A i0) → A i1
-
-syntax primPOr p q u t = [ p ↦ u , q ↦ t ]
-
-primitive
-  primTransp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) (φ : I) (a : A i0) → A i1
-  primHComp  : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A
diff --git a/data/declaration/Abstract.agda b/data/declaration/Abstract.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/Abstract.agda
@@ -0,0 +1,32 @@
+module Abstract where
+
+abstract
+
+  f
+    : {A : Set}
+    → A
+    → A
+  f x
+    = x
+
+  g
+    : {A : Set}
+    → A
+    → A
+  g x
+    = x
+
+  h
+    : {A : Set}
+    → A
+    → A
+  h x
+    = f x
+
+  _
+    : {A : Set}
+    → A
+    → A
+  _
+    = λ x → x
+
diff --git a/data/declaration/Data.agda b/data/declaration/Data.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/Data.agda
@@ -0,0 +1,17 @@
+module Data where
+
+data D
+  (A : Set)
+  : Set
+
+data D A
+  where
+
+  c
+    : D A
+
+data E
+  (B : Set)
+  : Set
+  where
+
diff --git a/data/declaration/DataDef.agda b/data/declaration/DataDef.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/DataDef.agda
@@ -0,0 +1,29 @@
+module DataDef where
+
+data ⊤
+  : Set
+  where
+
+  tt
+    : ⊤
+
+data ⊤'
+  (x : ⊤)
+  : Set
+  where
+
+  tt
+    : ⊤' x
+
+data D
+  {y : ⊤}
+  (y' : ⊤' y)
+  : Set
+
+data D {z} _ where
+
+postulate
+
+  d
+    : D tt
+
diff --git a/data/declaration/FunClause.agda b/data/declaration/FunClause.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/FunClause.agda
@@ -0,0 +1,35 @@
+module FunClause where
+
+f
+  : {A : Set}
+  → A
+  → A
+f x
+  = y
+  where
+    y = x
+    z = x
+
+data List
+  (A : Set)
+  : Set
+  where
+
+  nil
+    : List A
+
+  cons
+    : A
+    → List A
+    → List A
+
+snoc
+  : {A : Set}
+  → List A
+  → A
+  → List A
+snoc nil y
+  = cons y nil
+snoc (cons x xs) y
+  = cons x (snoc xs y)
+
diff --git a/data/declaration/Import.agda b/data/declaration/Import.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/Import.agda
@@ -0,0 +1,14 @@
+module Import where
+
+import Agda.Builtin.Bool
+  as _
+open import Agda.Builtin.Nat
+  as _
+import Agda.Builtin.Unit
+  using (⊤; tt)
+
+A
+  : Set
+A
+  = Agda.Builtin.Unit.⊤
+
diff --git a/data/declaration/Module.agda b/data/declaration/Module.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/Module.agda
@@ -0,0 +1,25 @@
+module Module where
+
+record R
+  : Set
+  where
+
+module M where
+
+module N where
+
+module O where
+
+  postulate
+
+    A
+      : Set
+
+x
+  : R
+x
+  = record {M}
+
+module P
+  = N
+
diff --git a/data/declaration/ModuleMacro.agda b/data/declaration/ModuleMacro.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/ModuleMacro.agda
@@ -0,0 +1,57 @@
+module ModuleMacro where
+
+record ⊤
+  : Set
+  where
+
+module M where
+
+module N where
+
+  postulate
+
+    A
+      : Set
+
+    B
+      : Set
+
+module O
+  = M
+
+module P
+  = M
+
+module Q
+  = P
+
+module R
+  (x : ⊤)
+  = N
+  using (A)
+
+module S
+  = N
+  renaming
+  ( A
+    to A'
+  ; B
+    to B'
+  )
+
+y
+  : ⊤
+y
+  = record {O}
+
+C
+  : ⊤
+  → Set
+C
+  = R.A
+
+D
+  : Set
+D
+  = S.B'
+
diff --git a/data/declaration/Mutual1.agda b/data/declaration/Mutual1.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/Mutual1.agda
@@ -0,0 +1,41 @@
+module Mutual1 where
+
+data Bool
+  : Set
+  where
+
+  false
+    : Bool
+
+  true
+    : Bool
+
+data ℕ
+  : Set
+  where
+
+  zero
+    : ℕ
+
+  suc
+    : ℕ
+    → ℕ
+
+is-even
+  : ℕ
+  → Bool
+
+is-odd
+  : ℕ
+  → Bool
+
+is-even zero
+  = true
+is-even (suc n)
+  = is-odd n
+
+is-odd zero
+  = false
+is-odd (suc n)
+  = is-even n
+
diff --git a/data/declaration/Mutual2.agda b/data/declaration/Mutual2.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/Mutual2.agda
@@ -0,0 +1,47 @@
+module Mutual2 where
+
+data Bool
+  : Set
+  where
+
+  false
+    : Bool
+
+  true
+    : Bool
+
+data ℕ
+  : Set
+  where
+
+  zero
+    : ℕ
+
+  suc
+    : ℕ
+    → ℕ
+
+is-even
+  : ℕ
+  → Bool
+
+is-odd
+  : ℕ
+  → Bool
+
+is-even zero
+  = true
+is-even (suc n)
+  = is-odd n
+
+is-odd zero
+  = false
+is-odd (suc n)
+  = is-even n
+
+is-even'
+  : ℕ
+  → Bool
+is-even'
+  = is-even
+
diff --git a/data/declaration/Open1.agda b/data/declaration/Open1.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/Open1.agda
@@ -0,0 +1,59 @@
+module Open1 where
+
+module M where
+
+  data ⊤
+    : Set
+    where
+
+    tt
+      : ⊤
+
+module N where
+
+  open M
+
+  v
+    : ⊤
+  v
+    = tt
+
+open M
+open N
+
+module O where
+
+  w
+    : ⊤
+  w
+    = tt
+
+  x
+    : ⊤
+  x
+    = tt
+
+module P where
+
+  open O
+    using (w)
+    renaming (x to x')
+
+  y
+    : ⊤
+  y
+    = w
+
+open P
+
+module Q where
+
+  open O
+    hiding (w)
+    renaming (x to x'')
+
+  z
+    : ⊤
+  z
+    = x''
+
diff --git a/data/declaration/Open2.agda b/data/declaration/Open2.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/Open2.agda
@@ -0,0 +1,54 @@
+module Open2 where
+
+data ⊤
+  : Set
+  where
+
+  tt
+    : ⊤
+
+data ⊤'
+  (x : ⊤)
+  : Set
+  where
+
+  tt
+    : ⊤' x
+
+record R
+  : Set
+  where
+
+  field
+
+    x
+      : ⊤
+
+    y
+      : ⊤
+
+record S
+  : Set₁
+  where
+
+  field
+
+    x
+      : R
+
+  open R x public
+    renaming (x to y; y to z)
+
+postulate
+
+  s
+    : S
+
+open S s
+  using (y)
+
+postulate
+
+  p
+    : ⊤' y
+
diff --git a/data/declaration/PatternSyn.agda b/data/declaration/PatternSyn.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/PatternSyn.agda
@@ -0,0 +1,41 @@
+module PatternSyn where
+
+data ⊤
+  : Set
+  where
+
+  tt
+    : ⊤
+
+data D
+  (A : Set)
+  : Set
+  where
+
+  d
+    : A
+    → A
+    → D A
+
+pattern p
+  = tt
+
+pattern q
+  = tt
+
+pattern _,_ x y
+  = d x y
+
+f
+  : ⊤
+  → ⊤
+f p
+  = tt
+
+g
+  : {A : Set}
+  → D A
+  → A
+g (x , _)
+  = x
+
diff --git a/data/declaration/Postulate.agda b/data/declaration/Postulate.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/Postulate.agda
@@ -0,0 +1,21 @@
+module Postulate where
+
+postulate
+
+  f
+    : {A : Set}
+    → A
+    → A
+  
+  g
+    : {A : Set}
+    → A
+    → A
+
+h
+  : {A : Set}
+  → A
+  → A
+h x
+  = f x
+
diff --git a/data/declaration/Private.agda b/data/declaration/Private.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/Private.agda
@@ -0,0 +1,32 @@
+module Private where
+
+private
+
+  f
+    : {A : Set}
+    → A
+    → A
+  f x
+    = x
+
+  g
+    : {A : Set}
+    → A
+    → A
+  g x
+    = x
+
+  h
+    : {A : Set}
+    → A
+    → A
+  h x
+    = f x
+
+  _
+    : {A : Set}
+    → A
+    → A
+  _
+    = λ x → x
+
diff --git a/data/declaration/Record.agda b/data/declaration/Record.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/Record.agda
@@ -0,0 +1,53 @@
+module Record where
+
+module M where
+
+  record A
+    : Set
+    where
+  
+    constructor
+  
+      a
+  
+open M
+
+record B
+  : Set
+  where
+
+record C
+  : Set
+  where
+
+  constructor
+
+    c
+
+x
+  : A
+x
+  = a
+
+y
+  : C
+y
+  = record {}
+
+record D
+  (E : Set)
+  : Set
+  where
+
+record F
+  : Set₁
+  where
+
+  field
+
+    G
+      : Set
+
+    z
+      : G
+
diff --git a/data/declaration/RecordDef.agda b/data/declaration/RecordDef.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/RecordDef.agda
@@ -0,0 +1,29 @@
+module RecordDef where
+
+data ⊤
+  : Set
+  where
+
+  tt
+    : ⊤
+
+data ⊤'
+  (x : ⊤)
+  : Set
+  where
+
+  tt
+    : ⊤' x
+
+record R
+  {y : ⊤}
+  (y' : ⊤' y)
+  : Set
+
+record R {z} _ where
+
+postulate
+
+  r
+    : R tt
+
diff --git a/data/declaration/Syntax.agda b/data/declaration/Syntax.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/Syntax.agda
@@ -0,0 +1,49 @@
+module Syntax where
+
+data S
+  (A₁ : Set)
+  (A₂ : A₁ → Set)
+  : Set
+  where
+
+  _,_
+    : (x₁ : A₁)
+    → A₂ x₁
+    → S A₁ A₂
+
+syntax S A₁ (λ x → A₂)
+  = x ∈ A₁ × A₂
+
+module M where
+
+  data S'
+    (A₁ : Set)
+    (A₂ : A₁ → Set)
+    : Set
+    where
+
+    _,'_
+      : (x₁ : A₁)
+      → A₂ x₁
+      → S' A₁ A₂
+
+  syntax S' A₁ (λ x → A₂)
+    = x ∈' A₁ ×' A₂
+
+open M
+  using (S')
+
+postulate
+
+  p1
+    : {A₁ : Set}
+    → {A₂ : A₁ → Set}
+    → x₁ ∈ A₁ × A₂ x₁
+    → A₁
+    
+  p1'
+    : {A₁ : Set}
+    → {A₂ : A₁ → Set}
+    → x₁ ∈' A₁ ×' A₂ x₁
+    → A₁
+  
diff --git a/data/declaration/TypeSig.agda b/data/declaration/TypeSig.agda
new file mode 100644
--- /dev/null
+++ b/data/declaration/TypeSig.agda
@@ -0,0 +1,30 @@
+module Definition where
+
+f
+  : {A : Set}
+  → A
+  → A
+f x
+  = x
+
+g
+  : {A : Set}
+  → A
+  → A
+g x
+  = x
+
+h
+  : {A : Set}
+  → A
+  → A
+h x
+  = f x
+
+_
+  : {A : Set}
+  → A
+  → A
+_
+  = λ x → x
+
diff --git a/data/example/Test.agda b/data/example/Test.agda
new file mode 100644
--- /dev/null
+++ b/data/example/Test.agda
@@ -0,0 +1,14 @@
+module Test where
+
+open import Agda.Builtin.Bool
+  using (Bool; false; true)
+open import Agda.Builtin.Unit
+
+_∧_
+  : Bool
+  → Bool
+  → Bool
+false ∧ x
+  = false
+_ ∧ y
+  = y
diff --git a/data/expression/DoBlock1.agda b/data/expression/DoBlock1.agda
new file mode 100644
--- /dev/null
+++ b/data/expression/DoBlock1.agda
@@ -0,0 +1,38 @@
+module DoBlock1 where
+
+data Id
+  (A : Set)
+  : Set
+  where
+
+  id
+    : A
+    → Id A
+
+_>>=_
+  : {A B : Set}
+  → Id A
+  → (A → Id B)
+  → Id B
+id x >>= f
+  = f x
+
+_>>_
+  : {A B : Set}
+  → Id A
+  → Id B
+  → Id B
+_ >> y
+  = y
+
+f
+  : {A : Set}
+  → A
+  → Id A
+f x
+  = do
+    y <- id x
+    z <- id x
+    id y
+    id y
+
diff --git a/data/expression/DoBlock2.agda b/data/expression/DoBlock2.agda
new file mode 100644
--- /dev/null
+++ b/data/expression/DoBlock2.agda
@@ -0,0 +1,36 @@
+module DoBlock2 where
+
+data Id
+  (A : Set)
+  : Set
+  where
+
+  id
+    : A
+    → Id A
+
+_>>=_
+  : {A B : Set}
+  → Id A
+  → (A → Id B)
+  → Id B
+id x >>= f
+  = f x
+
+_>>_
+  : {A B : Set}
+  → Id A
+  → Id B
+  → Id B
+_ >> y
+  = y
+
+f
+  : {A : Set}
+  → A
+  → Id A
+f x
+  = do
+    y <- id x
+    id y
+
diff --git a/data/expression/DoBlock3.agda b/data/expression/DoBlock3.agda
new file mode 100644
--- /dev/null
+++ b/data/expression/DoBlock3.agda
@@ -0,0 +1,36 @@
+module DoBlock3 where
+
+data Id
+  (A : Set)
+  : Set
+  where
+
+  id
+    : A
+    → Id A
+
+_>>=_
+  : {A B : Set}
+  → Id A
+  → (A → Id B)
+  → Id B
+id x >>= f
+  = f x
+
+_>>_
+  : {A B : Set}
+  → Id A
+  → Id B
+  → Id B
+_ >> y
+  = y
+
+f
+  : {A : Set}
+  → A
+  → Id A
+f x
+  = do
+    id x
+    id x
+
diff --git a/data/expression/DoBlock4.agda b/data/expression/DoBlock4.agda
new file mode 100644
--- /dev/null
+++ b/data/expression/DoBlock4.agda
@@ -0,0 +1,35 @@
+module DoBlock4 where
+
+data Id
+  (A : Set)
+  : Set
+  where
+
+  id
+    : A
+    → Id A
+
+_>>=_
+  : {A B : Set}
+  → Id A
+  → (A → Id B)
+  → Id B
+id x >>= f
+  = f x
+
+_>>_
+  : {A B : Set}
+  → Id A
+  → Id B
+  → Id B
+_ >> y
+  = y
+
+f
+  : {A : Set}
+  → A
+  → Id A
+f x
+  = do
+    id x
+
diff --git a/data/expression/ExtendedLam.agda b/data/expression/ExtendedLam.agda
new file mode 100644
--- /dev/null
+++ b/data/expression/ExtendedLam.agda
@@ -0,0 +1,23 @@
+module ExtendedLam where
+
+data Bool
+  : Set
+  where
+
+  false
+    : Bool
+  true
+    : Bool
+
+f
+  : Bool
+  → Bool
+  → Bool
+f
+  = λ
+  { x false
+    → true
+  ; y true
+    → y
+  }
+
diff --git a/data/expression/Lam.agda b/data/expression/Lam.agda
new file mode 100644
--- /dev/null
+++ b/data/expression/Lam.agda
@@ -0,0 +1,16 @@
+module Lam where
+
+f
+  : {A : Set}
+  → A
+  → A
+f x
+  = (λ y z → z) x x
+
+g
+  : {A : Set}
+  → A
+  → A
+g {A = A} x
+  = (λ (y' : A) (z : A) → z) x x
+
diff --git a/data/expression/Let.agda b/data/expression/Let.agda
new file mode 100644
--- /dev/null
+++ b/data/expression/Let.agda
@@ -0,0 +1,12 @@
+module Let where
+
+f
+  : {A : Set}
+  → A
+  → A
+f x
+  = let
+      y = x
+      z = x
+    in y
+
diff --git a/data/expression/Pi.agda b/data/expression/Pi.agda
new file mode 100644
--- /dev/null
+++ b/data/expression/Pi.agda
@@ -0,0 +1,14 @@
+module Pi where
+
+open import Agda.Builtin.Equality
+  using (_≡_; refl)
+
+f
+  : {A : Set}
+  → {x y : A}
+  → (z w : A)
+  → x ≡ z
+  → z ≡ x
+f _ _ refl
+  = refl
+
diff --git a/data/expression/WithApp.agda b/data/expression/WithApp.agda
new file mode 100644
--- /dev/null
+++ b/data/expression/WithApp.agda
@@ -0,0 +1,23 @@
+module WithApp where
+
+f
+  : {A : Set}
+  → A
+  → A
+f x
+  with x
+... | y
+  = y
+
+g
+  : {A : Set}
+  → A
+  → A
+  → A
+g x y
+  with x
+... | _
+  with y
+... | _
+  = x
+
diff --git a/data/pattern/AsP.agda b/data/pattern/AsP.agda
new file mode 100644
--- /dev/null
+++ b/data/pattern/AsP.agda
@@ -0,0 +1,20 @@
+module AsP where
+
+f
+  : {A : Set}
+  → A
+  → A
+  → A
+f x@y z@w
+  = x
+
+g
+  : {A : Set}
+  → A
+  → A
+  → A
+g x@y z'@w'
+  with y
+... | _
+  = x
+
diff --git a/data/pattern/IdentP.agda b/data/pattern/IdentP.agda
new file mode 100644
--- /dev/null
+++ b/data/pattern/IdentP.agda
@@ -0,0 +1,28 @@
+module IdentP where
+
+data Bool
+  : Set
+  where
+
+  false
+    : Bool
+
+  true
+    : Bool
+
+f
+  : {A : Set}
+  → A
+  → A
+  → A
+f x y
+  = x
+
+g
+  : Bool
+  → Bool
+g false
+  = true
+g true
+  = true
+
diff --git a/data/pattern/OpAppP.agda b/data/pattern/OpAppP.agda
new file mode 100644
--- /dev/null
+++ b/data/pattern/OpAppP.agda
@@ -0,0 +1,21 @@
+module OpAppP where
+
+data Bool
+  : Set
+  where
+
+  false
+    : Bool
+
+  true
+    : Bool
+
+_&&_
+  : Bool
+  → Bool
+  → Bool
+false && _
+  = false
+true && b
+  = b
+
diff --git a/data/test/declaration/Abstract.agda b/data/test/declaration/Abstract.agda
deleted file mode 100644
--- a/data/test/declaration/Abstract.agda
+++ /dev/null
@@ -1,32 +0,0 @@
-module Abstract where
-
-abstract
-
-  f
-    : {A : Set}
-    → A
-    → A
-  f x
-    = x
-
-  g
-    : {A : Set}
-    → A
-    → A
-  g x
-    = x
-
-  h
-    : {A : Set}
-    → A
-    → A
-  h x
-    = f x
-
-  _
-    : {A : Set}
-    → A
-    → A
-  _
-    = λ x → x
-
diff --git a/data/test/declaration/Data.agda b/data/test/declaration/Data.agda
deleted file mode 100644
--- a/data/test/declaration/Data.agda
+++ /dev/null
@@ -1,12 +0,0 @@
-module Data where
-
-data D
-  (A : Set)
-  : Set
-
-data D A
-  where
-
-  c
-    : D A
-
diff --git a/data/test/declaration/FunClause.agda b/data/test/declaration/FunClause.agda
deleted file mode 100644
--- a/data/test/declaration/FunClause.agda
+++ /dev/null
@@ -1,35 +0,0 @@
-module FunClause where
-
-f
-  : {A : Set}
-  → A
-  → A
-f x
-  = y
-  where
-    y = x
-    z = x
-
-data List
-  (A : Set)
-  : Set
-  where
-
-  nil
-    : List A
-
-  cons
-    : A
-    → List A
-    → List A
-
-snoc
-  : {A : Set}
-  → List A
-  → A
-  → List A
-snoc nil y
-  = cons y nil
-snoc (cons x xs) y
-  = cons x (snoc xs y)
-
diff --git a/data/test/declaration/Import.agda b/data/test/declaration/Import.agda
deleted file mode 100644
--- a/data/test/declaration/Import.agda
+++ /dev/null
@@ -1,11 +0,0 @@
-module Import where
-
-import Agda.Builtin.Unit
-  using (⊤; tt)
-import Agda.Builtin.Bool
-
-A
-  : Set
-A
-  = Agda.Builtin.Unit.⊤
-
diff --git a/data/test/declaration/Module.agda b/data/test/declaration/Module.agda
deleted file mode 100644
--- a/data/test/declaration/Module.agda
+++ /dev/null
@@ -1,25 +0,0 @@
-module Module where
-
-record R
-  : Set
-  where
-
-module M where
-
-module N where
-
-module O where
-
-  postulate
-
-    A
-      : Set
-
-x
-  : R
-x
-  = record {M}
-
-module P
-  = N
-
diff --git a/data/test/declaration/ModuleMacro.agda b/data/test/declaration/ModuleMacro.agda
deleted file mode 100644
--- a/data/test/declaration/ModuleMacro.agda
+++ /dev/null
@@ -1,57 +0,0 @@
-module ModuleMacro where
-
-record ⊤
-  : Set
-  where
-
-module M where
-
-module N where
-
-  postulate
-
-    A
-      : Set
-
-    B
-      : Set
-
-module O
-  = M
-
-module P
-  = M
-
-module Q
-  = P
-
-module R
-  (x : ⊤)
-  = N
-  using (A)
-
-module S
-  = N
-  renaming
-  ( A
-    to A'
-  ; B
-    to B'
-  )
-
-y
-  : ⊤
-y
-  = record {O}
-
-C
-  : ⊤
-  → Set
-C
-  = R.A
-
-D
-  : Set
-D
-  = S.B'
-
diff --git a/data/test/declaration/Mutual1.agda b/data/test/declaration/Mutual1.agda
deleted file mode 100644
--- a/data/test/declaration/Mutual1.agda
+++ /dev/null
@@ -1,41 +0,0 @@
-module Mutual1 where
-
-data Bool
-  : Set
-  where
-
-  false
-    : Bool
-
-  true
-    : Bool
-
-data ℕ
-  : Set
-  where
-
-  zero
-    : ℕ
-
-  suc
-    : ℕ
-    → ℕ
-
-is-even
-  : ℕ
-  → Bool
-
-is-odd
-  : ℕ
-  → Bool
-
-is-even zero
-  = true
-is-even (suc n)
-  = is-odd n
-
-is-odd zero
-  = false
-is-odd (suc n)
-  = is-even n
-
diff --git a/data/test/declaration/Mutual2.agda b/data/test/declaration/Mutual2.agda
deleted file mode 100644
--- a/data/test/declaration/Mutual2.agda
+++ /dev/null
@@ -1,47 +0,0 @@
-module Mutual2 where
-
-data Bool
-  : Set
-  where
-
-  false
-    : Bool
-
-  true
-    : Bool
-
-data ℕ
-  : Set
-  where
-
-  zero
-    : ℕ
-
-  suc
-    : ℕ
-    → ℕ
-
-is-even
-  : ℕ
-  → Bool
-
-is-odd
-  : ℕ
-  → Bool
-
-is-even zero
-  = true
-is-even (suc n)
-  = is-odd n
-
-is-odd zero
-  = false
-is-odd (suc n)
-  = is-even n
-
-is-even'
-  : ℕ
-  → Bool
-is-even'
-  = is-even
-
diff --git a/data/test/declaration/Open.agda b/data/test/declaration/Open.agda
deleted file mode 100644
--- a/data/test/declaration/Open.agda
+++ /dev/null
@@ -1,59 +0,0 @@
-module Open where
-
-module M where
-
-  data ⊤
-    : Set
-    where
-
-    tt
-      : ⊤
-
-module N where
-
-  open M
-
-  v
-    : ⊤
-  v
-    = tt
-
-open M
-open N
-
-module O where
-
-  w
-    : ⊤
-  w
-    = tt
-
-  x
-    : ⊤
-  x
-    = tt
-
-module P where
-
-  open O
-    using (w)
-    renaming (x to x')
-
-  y
-    : ⊤
-  y
-    = w
-
-open P
-
-module Q where
-
-  open O
-    hiding (w)
-    renaming (x to x'')
-
-  z
-    : ⊤
-  z
-    = x''
-
diff --git a/data/test/declaration/PatternSyn.agda b/data/test/declaration/PatternSyn.agda
deleted file mode 100644
--- a/data/test/declaration/PatternSyn.agda
+++ /dev/null
@@ -1,41 +0,0 @@
-module PatternSyn where
-
-data ⊤
-  : Set
-  where
-
-  tt
-    : ⊤
-
-data D
-  (A : Set)
-  : Set
-  where
-
-  d
-    : A
-    → A
-    → D A
-
-pattern p
-  = tt
-
-pattern q
-  = tt
-
-pattern _,_ x y
-  = d x y
-
-f
-  : ⊤
-  → ⊤
-f p
-  = tt
-
-g
-  : {A : Set}
-  → D A
-  → A
-g (x , _)
-  = x
-
diff --git a/data/test/declaration/Postulate.agda b/data/test/declaration/Postulate.agda
deleted file mode 100644
--- a/data/test/declaration/Postulate.agda
+++ /dev/null
@@ -1,21 +0,0 @@
-module Postulate where
-
-postulate
-
-  f
-    : {A : Set}
-    → A
-    → A
-  
-  g
-    : {A : Set}
-    → A
-    → A
-
-h
-  : {A : Set}
-  → A
-  → A
-h x
-  = f x
-
diff --git a/data/test/declaration/Private.agda b/data/test/declaration/Private.agda
deleted file mode 100644
--- a/data/test/declaration/Private.agda
+++ /dev/null
@@ -1,32 +0,0 @@
-module Private where
-
-private
-
-  f
-    : {A : Set}
-    → A
-    → A
-  f x
-    = x
-
-  g
-    : {A : Set}
-    → A
-    → A
-  g x
-    = x
-
-  h
-    : {A : Set}
-    → A
-    → A
-  h x
-    = f x
-
-  _
-    : {A : Set}
-    → A
-    → A
-  _
-    = λ x → x
-
diff --git a/data/test/declaration/Record.agda b/data/test/declaration/Record.agda
deleted file mode 100644
--- a/data/test/declaration/Record.agda
+++ /dev/null
@@ -1,36 +0,0 @@
-module Record where
-
-module M where
-
-  record A
-    : Set
-    where
-  
-    constructor
-  
-      a
-  
-open M
-
-record B
-  : Set
-  where
-
-record C
-  : Set
-  where
-
-  constructor
-
-    c
-
-x
-  : A
-x
-  = a
-
-y
-  : C
-y
-  = record {}
-
diff --git a/data/test/declaration/Syntax.agda b/data/test/declaration/Syntax.agda
deleted file mode 100644
--- a/data/test/declaration/Syntax.agda
+++ /dev/null
@@ -1,49 +0,0 @@
-module Syntax where
-
-data S
-  (A₁ : Set)
-  (A₂ : A₁ → Set)
-  : Set
-  where
-
-  _,_
-    : (x₁ : A₁)
-    → A₂ x₁
-    → S A₁ A₂
-
-syntax S A₁ (λ x → A₂)
-  = x ∈ A₁ × A₂
-
-module M where
-
-  data S'
-    (A₁ : Set)
-    (A₂ : A₁ → Set)
-    : Set
-    where
-
-    _,'_
-      : (x₁ : A₁)
-      → A₂ x₁
-      → S' A₁ A₂
-
-  syntax S' A₁ (λ x → A₂)
-    = x ∈' A₁ ×' A₂
-
-open M
-  using (S')
-
-postulate
-
-  p1
-    : {A₁ : Set}
-    → {A₂ : A₁ → Set}
-    → x₁ ∈ A₁ × A₂ x₁
-    → A₁
-    
-  p1'
-    : {A₁ : Set}
-    → {A₂ : A₁ → Set}
-    → x₁ ∈' A₁ ×' A₂ x₁
-    → A₁
-  
diff --git a/data/test/declaration/TypeSig.agda b/data/test/declaration/TypeSig.agda
deleted file mode 100644
--- a/data/test/declaration/TypeSig.agda
+++ /dev/null
@@ -1,30 +0,0 @@
-module Definition where
-
-f
-  : {A : Set}
-  → A
-  → A
-f x
-  = x
-
-g
-  : {A : Set}
-  → A
-  → A
-g x
-  = x
-
-h
-  : {A : Set}
-  → A
-  → A
-h x
-  = f x
-
-_
-  : {A : Set}
-  → A
-  → A
-_
-  = λ x → x
-
diff --git a/data/test/example/Test.agda b/data/test/example/Test.agda
deleted file mode 100644
--- a/data/test/example/Test.agda
+++ /dev/null
@@ -1,14 +0,0 @@
-module Test where
-
-open import Agda.Builtin.Bool
-  using (Bool; false; true)
-open import Agda.Builtin.Unit
-
-_∧_
-  : Bool
-  → Bool
-  → Bool
-false ∧ x
-  = false
-_ ∧ y
-  = y
diff --git a/data/test/expression/DoBlock1.agda b/data/test/expression/DoBlock1.agda
deleted file mode 100644
--- a/data/test/expression/DoBlock1.agda
+++ /dev/null
@@ -1,38 +0,0 @@
-module DoBlock1 where
-
-data Id
-  (A : Set)
-  : Set
-  where
-
-  id
-    : A
-    → Id A
-
-_>>=_
-  : {A B : Set}
-  → Id A
-  → (A → Id B)
-  → Id B
-id x >>= f
-  = f x
-
-_>>_
-  : {A B : Set}
-  → Id A
-  → Id B
-  → Id B
-_ >> y
-  = y
-
-f
-  : {A : Set}
-  → A
-  → Id A
-f x
-  = do
-    y <- id x
-    z <- id x
-    id y
-    id y
-
diff --git a/data/test/expression/DoBlock2.agda b/data/test/expression/DoBlock2.agda
deleted file mode 100644
--- a/data/test/expression/DoBlock2.agda
+++ /dev/null
@@ -1,36 +0,0 @@
-module DoBlock2 where
-
-data Id
-  (A : Set)
-  : Set
-  where
-
-  id
-    : A
-    → Id A
-
-_>>=_
-  : {A B : Set}
-  → Id A
-  → (A → Id B)
-  → Id B
-id x >>= f
-  = f x
-
-_>>_
-  : {A B : Set}
-  → Id A
-  → Id B
-  → Id B
-_ >> y
-  = y
-
-f
-  : {A : Set}
-  → A
-  → Id A
-f x
-  = do
-    y <- id x
-    id y
-
diff --git a/data/test/expression/DoBlock3.agda b/data/test/expression/DoBlock3.agda
deleted file mode 100644
--- a/data/test/expression/DoBlock3.agda
+++ /dev/null
@@ -1,36 +0,0 @@
-module DoBlock3 where
-
-data Id
-  (A : Set)
-  : Set
-  where
-
-  id
-    : A
-    → Id A
-
-_>>=_
-  : {A B : Set}
-  → Id A
-  → (A → Id B)
-  → Id B
-id x >>= f
-  = f x
-
-_>>_
-  : {A B : Set}
-  → Id A
-  → Id B
-  → Id B
-_ >> y
-  = y
-
-f
-  : {A : Set}
-  → A
-  → Id A
-f x
-  = do
-    id x
-    id x
-
diff --git a/data/test/expression/DoBlock4.agda b/data/test/expression/DoBlock4.agda
deleted file mode 100644
--- a/data/test/expression/DoBlock4.agda
+++ /dev/null
@@ -1,35 +0,0 @@
-module DoBlock4 where
-
-data Id
-  (A : Set)
-  : Set
-  where
-
-  id
-    : A
-    → Id A
-
-_>>=_
-  : {A B : Set}
-  → Id A
-  → (A → Id B)
-  → Id B
-id x >>= f
-  = f x
-
-_>>_
-  : {A B : Set}
-  → Id A
-  → Id B
-  → Id B
-_ >> y
-  = y
-
-f
-  : {A : Set}
-  → A
-  → Id A
-f x
-  = do
-    id x
-
diff --git a/data/test/expression/ExtendedLam.agda b/data/test/expression/ExtendedLam.agda
deleted file mode 100644
--- a/data/test/expression/ExtendedLam.agda
+++ /dev/null
@@ -1,23 +0,0 @@
-module ExtendedLam where
-
-data Bool
-  : Set
-  where
-
-  false
-    : Bool
-  true
-    : Bool
-
-f
-  : Bool
-  → Bool
-  → Bool
-f
-  = λ
-  { x false
-    → true
-  ; y true
-    → y
-  }
-
diff --git a/data/test/expression/Lam.agda b/data/test/expression/Lam.agda
deleted file mode 100644
--- a/data/test/expression/Lam.agda
+++ /dev/null
@@ -1,16 +0,0 @@
-module Lam where
-
-f
-  : {A : Set}
-  → A
-  → A
-f x
-  = (λ y z → z) x x
-
-g
-  : {A : Set}
-  → A
-  → A
-g {A = A} x
-  = (λ (y' : A) (z : A) → z) x x
-
diff --git a/data/test/expression/Let.agda b/data/test/expression/Let.agda
deleted file mode 100644
--- a/data/test/expression/Let.agda
+++ /dev/null
@@ -1,12 +0,0 @@
-module Let where
-
-f
-  : {A : Set}
-  → A
-  → A
-f x
-  = let
-      y = x
-      z = x
-    in y
-
diff --git a/data/test/expression/Pi.agda b/data/test/expression/Pi.agda
deleted file mode 100644
--- a/data/test/expression/Pi.agda
+++ /dev/null
@@ -1,14 +0,0 @@
-module Pi where
-
-open import Agda.Builtin.Equality
-  using (_≡_; refl)
-
-f
-  : {A : Set}
-  → {x y : A}
-  → (z w : A)
-  → x ≡ z
-  → z ≡ x
-f _ _ refl
-  = refl
-
diff --git a/data/test/expression/WithApp.agda b/data/test/expression/WithApp.agda
deleted file mode 100644
--- a/data/test/expression/WithApp.agda
+++ /dev/null
@@ -1,23 +0,0 @@
-module WithApp where
-
-f
-  : {A : Set}
-  → A
-  → A
-f x
-  with x
-... | y
-  = y
-
-g
-  : {A : Set}
-  → A
-  → A
-  → A
-g x y
-  with x
-... | _
-  with y
-... | _
-  = x
-
diff --git a/data/test/pattern/AsP.agda b/data/test/pattern/AsP.agda
deleted file mode 100644
--- a/data/test/pattern/AsP.agda
+++ /dev/null
@@ -1,20 +0,0 @@
-module AsP where
-
-f
-  : {A : Set}
-  → A
-  → A
-  → A
-f x@y z@w
-  = x
-
-g
-  : {A : Set}
-  → A
-  → A
-  → A
-g x@y z'@w'
-  with y
-... | _
-  = x
-
diff --git a/data/test/pattern/IdentP.agda b/data/test/pattern/IdentP.agda
deleted file mode 100644
--- a/data/test/pattern/IdentP.agda
+++ /dev/null
@@ -1,28 +0,0 @@
-module IdentP where
-
-data Bool
-  : Set
-  where
-
-  false
-    : Bool
-
-  true
-    : Bool
-
-f
-  : {A : Set}
-  → A
-  → A
-  → A
-f x y
-  = x
-
-g
-  : Bool
-  → Bool
-g false
-  = true
-g true
-  = true
-
diff --git a/data/test/pattern/OpAppP.agda b/data/test/pattern/OpAppP.agda
deleted file mode 100644
--- a/data/test/pattern/OpAppP.agda
+++ /dev/null
@@ -1,21 +0,0 @@
-module OpAppP where
-
-data Bool
-  : Set
-  where
-
-  false
-    : Bool
-
-  true
-    : Bool
-
-_&&_
-  : Bool
-  → Bool
-  → Bool
-false && _
-  = false
-true && b
-  = b
-
diff --git a/src/Agda/Unused.hs b/src/Agda/Unused.hs
--- a/src/Agda/Unused.hs
+++ b/src/Agda/Unused.hs
@@ -7,20 +7,24 @@
 module Agda.Unused
   ( Unused(..)
   , UnusedItems(..)
+  , UnusedOptions(..)
   ) where
 
 import Agda.Unused.Types.Range
   (Range, RangeInfo)
 
+import Data.Text
+  (Text)
+
 -- ## Types
 
 -- | A collection of unused items and files.
 data Unused
   = Unused
-  { unusedItems
-    :: UnusedItems
-  , unusedPaths
+  { unusedFiles
     :: [FilePath]
+  , unusedItems
+    :: UnusedItems
   } deriving Show
 
 -- | A collection of unused items.
@@ -28,5 +32,20 @@
   = UnusedItems
   { unusedItemsList
     :: [(Range, RangeInfo)]
+  } deriving Show
+
+-- | Options required by check functions.
+data UnusedOptions
+  = UnusedOptions
+  { unusedOptionsInclude
+    :: [FilePath]
+  , unusedOptionsLibraries
+    :: [Text]
+  , unusedOptionsLibrariesFile
+    :: Maybe FilePath
+  , unusedOptionsUseLibraries
+    :: Bool
+  , unusedOptionsUseDefaultLibraries
+    :: Bool
   } deriving Show
 
diff --git a/src/Agda/Unused/Check.hs b/src/Agda/Unused/Check.hs
--- a/src/Agda/Unused/Check.hs
+++ b/src/Agda/Unused/Check.hs
@@ -5,46 +5,52 @@
 -}
 module Agda.Unused.Check
   ( checkUnused
-  , checkUnusedLocal
+  , checkUnusedGlobal
+  , checkUnusedWith
   ) where
 
 import Agda.Unused
-  (Unused(..), UnusedItems(..))
+  (Unused(..), UnusedItems(..), UnusedOptions(..))
 import Agda.Unused.Monad.Error
   (Error(..), InternalError(..), UnexpectedError(..), UnsupportedError(..),
     liftLookup)
 import Agda.Unused.Monad.Reader
-  (Environment(..), askLocal, askRoot, askSkip, localSkip)
+  (Environment(..), Mode(..), askGlobalMain, askIncludes, askLocal, askRoot,
+    askSkip, localGlobal, localSkip)
 import Agda.Unused.Monad.State
-  (ModuleState(..), State, modifyDelete, modifyInsert, stateBlock,
-    stateCheck, stateEmpty, stateItems, stateLookup, stateModules)
+  (ModuleState(..), State, getModule, getSources, modifyBlock, modifyCheck,
+    modifyDelete, modifyInsert, modifySources, stateEmpty, stateItems,
+    stateModules)
 import Agda.Unused.Types.Access
   (Access(..), fromAccess)
 import Agda.Unused.Types.Context
   (AccessContext, AccessModule(..), Context, LookupError(..),
-    accessContextDefine, accessContextImport, accessContextItem,
+    accessContextConstructor, accessContextDefine, accessContextDefineFields,
+    accessContextField, accessContextImport, accessContextItem,
     accessContextLookup, accessContextLookupDefining, accessContextLookupModule,
     accessContextLookupSpecial, accessContextMatch, accessContextModule,
-    accessContextModule', accessContextUnion, contextDelete,
-    contextDeleteModule, contextItem, contextLookup, contextLookupItem,
-    contextLookupModule, contextModule, contextRanges, fromContext, item,
-    itemConstructor, itemPattern, moduleRanges, toContext)
+    accessContextModule', accessContextPattern, accessContextRanges,
+    accessContextUnion, contextDelete, contextDeleteModule, contextItem,
+    contextLookupItem, contextLookupModule, contextModule, contextRanges,
+    fromContext, moduleRanges, toContext)
 import qualified Agda.Unused.Types.Context
   as C
 import Agda.Unused.Types.Name
-  (Name(..), QName(..), isBuiltin, fromAsName, fromName, fromNameRange,
-    fromQName, fromQNameRange, nameIds, pathQName, qNamePath)
+  (Name(..), QName(..), fromAsName, fromModuleName, fromName, fromNameRange,
+    fromQName, fromQNameRange, nameIds, pathQName, qNamePath, toQName)
 import Agda.Unused.Types.Range
-  (Range'(..), RangeInfo(..), RangeType(..))
-import Agda.Unused.Types.Root
-  (Root(..), Roots(..))
+  (Range'(..), RangeInfo(..), RangeType(..), rangePath)
 import Agda.Unused.Utils
   (liftMaybe, mapLeft)
 
+import Agda.Interaction.FindFile
+  (findFile'', srcFilePath)
+import Agda.Interaction.Options
+  (CommandLineOptions(..), defaultOptions)
 import Agda.Syntax.Common
   (Arg(..), Fixity'(..), GenPart(..), ImportDirective'(..), ImportedName'(..),
-    Named(..), Ranged(..), Renaming'(..), RewriteEqn'(..), Using'(..),
-    namedThing, unArg, whThing)
+    IsInstance, Named(..), Ranged(..), Renaming'(..), RewriteEqn'(..),
+    Using'(..), namedThing, unArg, whThing)
 import qualified Agda.Syntax.Common
   as Common
 import Agda.Syntax.Concrete
@@ -53,37 +59,48 @@
     LamBinding, LamBinding'(..), LamClause(..), LHS(..), Module,
     ModuleApplication(..), ModuleAssignment(..), OpenShortHand(..), Pattern(..),
     RecordAssignment, Renaming, RewriteEqn, RHS, RHS'(..), TypedBinding,
-    TypedBinding'(..), WhereClause, WhereClause'(..), _exprFieldA)
+    TypedBinding'(..), WhereClause, WhereClause'(..), _exprFieldA,
+    topLevelModuleName)
 import Agda.Syntax.Concrete.Definitions
-  (Clause(..), NiceDeclaration(..), niceDeclarations, runNice)
+  (Clause(..), NiceConstructor, NiceDeclaration(..), niceDeclarations, runNice)
 import Agda.Syntax.Concrete.Fixity
   (DoWarn(..), Fixities, fixitiesAndPolarities)
 import Agda.Syntax.Concrete.Name
-  (NameInScope(..), NamePart(..))
+  (NameInScope(..), NamePart(..), nameRange, projectRoot, toTopLevelModuleName)
 import qualified Agda.Syntax.Concrete.Name
   as N
 import Agda.Syntax.Parser
   (moduleParser, parseFile, runPMIO)
 import Agda.Syntax.Position
   (Range, getRange)
+import Agda.TypeChecking.Monad.Base
+  (TCM, getIncludeDirs, runTCMTop)
+import Agda.TypeChecking.Monad.Options
+  (setCommandLineOptions)
 import Agda.Utils.FileName
-  (AbsolutePath(..))
+  (filePath, mkAbsolute)
 import Control.Monad
-  (foldM, void)
+  (foldM, unless, void, when)
 import Control.Monad.Except
-  (MonadError, liftEither, runExceptT, throwError)
+  (ExceptT, MonadError, liftEither, runExceptT, throwError)
 import Control.Monad.IO.Class
   (MonadIO, liftIO)
 import Control.Monad.Reader
-  (MonadReader, ReaderT, runReaderT)
+  (MonadReader, runReaderT)
 import Control.Monad.State
-  (MonadState, StateT, gets, modify, runStateT)
+  (MonadState, runStateT)
 import Data.Bool
   (bool)
+import Data.Foldable
+  (traverse_)
 import qualified Data.Map.Strict
   as Map
 import Data.Maybe
   (catMaybes)
+import Data.Set
+  (Set)
+import qualified Data.Set
+  as Set
 import qualified Data.Text
   as T
 import System.Directory
@@ -91,32 +108,9 @@
 import System.FilePath
   ((</>))
 
-import Paths_agda_unused
-  (getDataFileName)
-
 -- ## Context
 
 -- Do nothing if `askSkip` returns true.
-contextInsertRange
-  :: MonadReader Environment m
-  => Name
-  -> Range
-  -> Context
-  -> m Context
-contextInsertRange n r c
-  = askSkip >>= pure . bool (C.contextInsertRange n r c) c
-
--- Do nothing if `askSkip` returns true.
-contextInsertRangeModule
-  :: MonadReader Environment m
-  => Name
-  -> Range
-  -> Context
-  -> m Context
-contextInsertRangeModule n r c
-  = askSkip >>= pure . bool (C.contextInsertRangeModule n r c) c
-
--- Do nothing if `askSkip` returns true.
 contextInsertRangeAll
   :: MonadReader Environment m
   => Range
@@ -134,30 +128,6 @@
 accessContextInsertRangeAll r c
   = askSkip >>= pure . bool (C.accessContextInsertRangeAll r c) c
 
--- Also insert range unless `askSkip` returns true.
-contextRename
-  :: MonadReader Environment m
-  => Name
-  -> Name
-  -> Range
-  -> Context
-  -> m Context
-contextRename n t r c
-  = contextInsertRange n r c
-  >>= pure . C.contextRename n t
-
--- Also insert range unless `askSkip` returns true.
-contextRenameModule
-  :: MonadReader Environment m
-  => Name
-  -> Name
-  -> Range
-  -> Context
-  -> m Context
-contextRenameModule n t r c
-  = contextInsertRangeModule n r c
-  >>= pure . C.contextRenameModule n t
-
 -- ## Syntax
 
 syntax
@@ -257,7 +227,8 @@
   = pure mempty
 checkName p fs a t r@(Range _ _) n
   = modifyInsert r (RangeNamed t (QName n))
-  >> pure (accessContextItem n a (bool item itemPattern p [r] (syntax fs n)))
+  >> pure (bool accessContextItem accessContextPattern p n a (Set.singleton r)
+    (syntax fs n))
 
 checkName'
   :: MonadReader Environment m
@@ -345,8 +316,22 @@
 checkModuleName c a r n
   = modifyInsert r (RangeNamed RangeModule (QName n))
   >> contextInsertRangeAll r c
-  >>= \c' -> pure (accessContextModule n (AccessModule a [r] c'))
+  >>= \c' -> pure (accessContextModule n (AccessModule a (Set.singleton r) c'))
 
+checkModuleNameMay
+  :: MonadReader Environment m
+  => MonadState State m
+  => Context
+  -> Access
+  -> Range
+  -> Maybe Name
+  -- ^ If `Nothing`, the module is anonymous.
+  -> m AccessContext
+checkModuleNameMay _ _ _ Nothing
+  = pure mempty
+checkModuleNameMay c a r (Just n)
+  = checkModuleName c a r n
+
 touchName
   :: MonadReader Environment m
   => MonadState State m
@@ -359,7 +344,7 @@
 touchNameWith
   :: MonadReader Environment m
   => MonadState State m
-  => Either LookupError (Bool, [Range])
+  => Either LookupError (Bool, Set Range)
   -> Bool
   -> m ()
 touchNameWith (Right (False, rs)) False
@@ -393,7 +378,7 @@
   => MonadState State m
   => Range
   -> QName
-  -> Either LookupError (Bool, [Range])
+  -> Either LookupError (Bool, Set Range)
   -> Bool
   -> m ()
 touchQNameWith r n (Left LookupAmbiguous) False
@@ -401,28 +386,6 @@
 touchQNameWith _ _ rs b
   = touchNameWith rs b
 
-touchQNameContext
-  :: MonadError Error m
-  => MonadReader Environment m
-  => MonadState State m
-  => Context
-  -> QName
-  -> QName
-  -> m ()
-touchQNameContext c m n
-  = maybe (throwError (ErrorRoot m n)) modifyDelete (contextLookup n c)
-
-touchQNamesContext
-  :: MonadError Error m
-  => MonadReader Environment m
-  => MonadState State m
-  => Context
-  -> QName
-  -> [QName]
-  -> m ()
-touchQNamesContext m p
-  = void . traverse (touchQNameContext m p)
-
 touchQName'
   :: MonadError Error m
   => MonadReader Environment m
@@ -431,7 +394,7 @@
   -> N.QName
   -> m ()
 touchQName' c n
-  = maybe (pure ()) (uncurry (touchQName c)) (fromQNameRange n)
+  = traverse_ (uncurry (touchQName c)) (fromQNameRange n)
 
 -- ## Bindings
 
@@ -536,7 +499,7 @@
 checkPattern c (RawAppP _ ps)
   = checkRawAppP c ps
 checkPattern _ (OpAppP r _ _ _)
-  = throwError (ErrorInternal (ErrorUnexpected UnexpectedOpAppP) r)
+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedOpAppP r))
 checkPattern c (HiddenP _ (Named _ p))
   = checkPattern c p
 checkPattern c (InstanceP _ (Named _ p))
@@ -659,7 +622,7 @@
 checkExpr c (App _ e (Arg _ (Named _ e')))
   = checkExpr c e >> checkExpr c e'
 checkExpr _ (OpApp r _ _ _)
-  = throwError (ErrorInternal (ErrorUnexpected UnexpectedOpApp) r)
+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedOpApp r))
 checkExpr c (WithApp _ e es)
   = checkExpr c e >> checkExprs c es
 checkExpr c (HiddenArg _ (Named _ e))
@@ -695,15 +658,15 @@
 checkExpr c (DoBlock _ ss)
   = void (checkDoStmts c ss)
 checkExpr _ (Absurd r)
-  = throwError (ErrorInternal (ErrorUnexpected UnexpectedAbsurd) r)
+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedAbsurd r))
 checkExpr _ (As r _ _)
-  = throwError (ErrorInternal (ErrorUnexpected UnexpectedAs) r)
+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedAs r))
 checkExpr c (Dot _ e)
   = checkExpr c e
 checkExpr c (DoubleDot _ e)
   = checkExpr c e
 checkExpr _ e@(ETel _)
-  = throwError (ErrorInternal (ErrorUnexpected UnexpectedETel) (getRange e))
+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedETel (getRange e)))
 checkExpr _ (Quote _)
   = pure ()
 checkExpr _ (QuoteTerm _)
@@ -713,17 +676,17 @@
 checkExpr _ (Unquote _)
   = pure ()
 checkExpr _ e@(DontCare _)
-  = throwError (ErrorInternal (ErrorUnexpected UnexpectedDontCare) (getRange e))
+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedDontCare (getRange e)))
 checkExpr _ (Equal r _ _)
-  = throwError (ErrorInternal (ErrorUnexpected UnexpectedEqual) r)
+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedEqual r))
 checkExpr _ (Ellipsis r)
-  = throwError (ErrorInternal (ErrorUnexpected UnexpectedEllipsis) r)
+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedEllipsis r))
 checkExpr c (Generalized e)
   = checkExpr c e
 
 checkExpr c (Let _ ds e)
   = checkDeclarations c ds
-  >>= \c' -> maybe (pure ()) (checkExpr (c <> c')) e
+  >>= \c' -> traverse_ (checkExpr (c <> c')) e
 
 checkExprs
   :: MonadError Error m
@@ -843,7 +806,7 @@
   -> m ()
 checkModuleAssignment c a@(ModuleAssignment n es _)
   = checkExprs c es
-  >> maybe (pure ()) (touchModule c (getRange a)) (fromQName n)
+  >> traverse_ (touchModule c (getRange a)) (fromQName n)
 
 -- ## Definitions
 
@@ -963,9 +926,9 @@
   = checkDeclarations c ds
   >>= \c' -> pure (mempty, c')
 checkWhereClause c (SomeWhere n a ds)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n)
-  >>= \n' -> checkDeclarations c ds
-  >>= \c' -> checkModuleName (toContext c') (fromAccess a) (getRange n) n'
+  = checkDeclarations c ds
+  >>= \c' -> checkModuleNameMay (toContext c') (fromAccess a) (getRange n)
+    (fromName n)
   >>= \c'' -> pure (c'' , c')
 
 checkRewriteEqn
@@ -1041,8 +1004,8 @@
   -> [DoStmt]
   -> m AccessContext
 checkDoStmts c ss
-  = bool (pure ()) (touchName c bind) (hasBind ss)
-  >> bool (pure ()) (touchName c bind_) (hasBind_ ss)
+  = when (hasBind ss) (touchName c bind)
+  >> when (hasBind_ ss) (touchName c bind_)
   >> checkFold checkDoStmt c ss
 
 hasBind
@@ -1106,7 +1069,7 @@
   => MonadState State m
   => MonadIO m
   => Name
-  -> [Range]
+  -> Set Range
   -- ^ Ranges associated with parent record.
   -> AccessContext
   -> [Declaration]
@@ -1149,78 +1112,120 @@
   -> AccessContext
   -> NiceDeclaration
   -> m AccessContext
+checkNiceDeclaration fs c d
+  = askGlobalMain
+  >>= checkNiceDeclarationWith fs c d
 
-checkNiceDeclaration fs c (Axiom _ a _ _ _ n e)
+checkNiceDeclarationWith
+  :: MonadError Error m
+  => MonadReader Environment m
+  => MonadState State m
+  => MonadIO m
+  => Fixities
+  -> AccessContext
+  -> NiceDeclaration
+  -> Bool
+  -> m AccessContext
+checkNiceDeclarationWith fs c d False
+  = checkNiceDeclaration' fs c d
+checkNiceDeclarationWith fs c d@(NiceImport _ _ _ _ _) True
+  = localGlobal (checkNiceDeclaration' fs c d)
+  >>= \c' -> touchAccessContext c'
+  >> pure c'
+checkNiceDeclarationWith _ _ d True
+  = throwError (ErrorGlobal (getRange d))
+
+checkNiceDeclaration'
+  :: MonadError Error m
+  => MonadReader Environment m
+  => MonadState State m
+  => MonadIO m
+  => Fixities
+  -> AccessContext
+  -> NiceDeclaration
+  -> m AccessContext
+
+checkNiceDeclaration' fs c (Axiom _ a _ _ _ n e)
   = checkExpr c e >> checkName' False fs (fromAccess a) RangePostulate n
-checkNiceDeclaration _ _ (NiceField r _ _ _ _ _ _)
-  = throwError (ErrorInternal (ErrorUnexpected UnexpectedField) r)
-checkNiceDeclaration fs c (PrimitiveFunction _ a _ n e)
+checkNiceDeclaration' _ _ (NiceField r _ _ _ _ _ _)
+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedField r))
+checkNiceDeclaration' fs c (PrimitiveFunction _ a _ n e)
   = checkExpr c e >> checkName' False fs (fromAccess a) RangeDefinition n
-checkNiceDeclaration _ c (NiceModule r a _ (N.QName n) bs ds)
+checkNiceDeclaration' _ c (NiceModule r a _ (N.QName n) bs ds)
   = checkNiceModule c (fromAccess a) r (fromName n) bs ds
-checkNiceDeclaration _ _ (NiceModule _ _ _ n@(N.Qual _ _) _ _)
-  = throwError (ErrorInternal ErrorName (getRange n))
-checkNiceDeclaration _ _ (NicePragma _ _)
+checkNiceDeclaration' _ _ (NiceModule _ _ _ n@(N.Qual _ _) _ _)
+  = throwError (ErrorInternal (ErrorName (getRange n)))
+checkNiceDeclaration' _ _ (NicePragma _ _)
   = pure mempty
-checkNiceDeclaration fs c (NiceRecSig _ a _ _ _ n bs e)
+checkNiceDeclaration' fs c (NiceRecSig _ a _ _ _ n bs e)
   = checkNiceSig fs c a RangeRecord n bs e
-checkNiceDeclaration fs c (NiceDataSig _ a _ _ _ n bs e)
+checkNiceDeclaration' fs c (NiceDataSig _ a _ _ _ n bs e)
   = checkNiceSig fs c a RangeData n bs e
-checkNiceDeclaration _ _ (NiceFunClause r _ _ _ _ _ _)
-  = throwError (ErrorInternal (ErrorUnexpected UnexpectedNiceFunClause) r)
-checkNiceDeclaration fs c (FunSig _ a _ _ _ _ _ _ n e)
+checkNiceDeclaration' _ _ (NiceFunClause r _ _ _ _ _ _)
+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedNiceFunClause r))
+checkNiceDeclaration' fs c (FunSig _ a _ _ _ _ _ _ n e)
   = checkExpr c e >> checkName' False fs (fromAccess a) RangeDefinition n
-checkNiceDeclaration _ c (FunDef _ _ _ _ _ _ _ cs)
+checkNiceDeclaration' _ c (FunDef _ _ _ _ _ _ _ cs)
   = checkClauses c cs >> pure mempty
-checkNiceDeclaration _ c (NiceGeneralize _ _ _ _ _ e)
+checkNiceDeclaration' fs c (NiceDataDef _ _ _ _ _ n bs cs)
+  = checkNiceDataDef True fs c n bs cs
+checkNiceDeclaration' fs c (NiceRecDef _ _ _ _ _ n _ _ m bs ds)
+  = checkNiceRecordDef True fs c n m bs ds
+checkNiceDeclaration' _ c (NiceGeneralize _ _ _ _ _ e)
   = checkExpr c e >> pure mempty
-checkNiceDeclaration _ _ (NiceUnquoteDecl r _ _ _ _ _ _ _)
+checkNiceDeclaration' _ _ (NiceUnquoteDecl r _ _ _ _ _ _ _)
   = throwError (ErrorUnsupported UnsupportedUnquote r)
-checkNiceDeclaration _ _ (NiceUnquoteDef r _ _ _ _ _ _)
+checkNiceDeclaration' _ _ (NiceUnquoteDef r _ _ _ _ _ _)
   = throwError (ErrorUnsupported UnsupportedUnquote r)
 
-checkNiceDeclaration fs c
+checkNiceDeclaration' fs c
   (NiceMutual _ _ _ _
-    ds@(NiceRecSig _ _ _ _ _ _ _ _ : NiceRecDef _ _ _ _ _ _ _ _ _ _ _ : _))
-  = checkNiceDeclarations fs c ds
-checkNiceDeclaration fs c
+    (d@(NiceRecSig _ _ _ _ _ n _ _) : NiceRecDef _ _ _ _ _ n' _ _ m bs ds : []))
+  | nameRange n == nameRange n'
+  = checkNiceDeclaration fs c d
+  >>= \c' -> checkNiceRecordDef False fs (c <> c') n' m bs ds
+  >>= \c'' -> pure (c' <> c'')
+checkNiceDeclaration' fs c
   (NiceMutual _ _ _ _
-    ds@(NiceDataSig _ _ _ _ _ _ _ _ : NiceDataDef _ _ _ _ _ _ _ _ : _))
-  = checkNiceDeclarations fs c ds
-checkNiceDeclaration fs c
+    (d@(NiceDataSig _ _ _ _ _ n _ _) : NiceDataDef _ _ _ _ _ n' bs cs : []))
+  | nameRange n == nameRange n'
+  = checkNiceDeclaration fs c d
+  >>= \c' -> checkNiceDataDef False fs (c <> c') n' bs cs
+  >>= \c'' -> pure (c' <> c'')
+checkNiceDeclaration' fs c
   (NiceMutual _ _ _ _
-    ds@(FunSig _ _ _ _ _ _ _ _ _ _ : FunDef _ _ _ _ _ _ _ _ : _))
+    ds@(FunSig _ _ _ _ _ _ _ _ _ _ : FunDef _ _ _ _ _ _ _ _ : []))
   = checkNiceDeclarations fs c ds
-checkNiceDeclaration fs c (NiceMutual r _ _ _ ds)
+checkNiceDeclaration' fs c (NiceMutual r _ _ _ ds)
   = checkNiceDeclarations fs c ds
   >>= \c' -> modifyInsert r RangeMutual
   >> accessContextInsertRangeAll r c'
 
-checkNiceDeclaration _ c
+checkNiceDeclaration' _ c
   (NiceModuleMacro r _ (N.NoName _ _)
     (SectionApp _ [] (RawApp _ (Ident n : es))) DoOpen i)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n)
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromQName n)
   >>= \n' -> liftLookup r n' (accessContextLookupModule n' c)
   >>= \(C.Module rs c') -> modifyDelete rs
   >> checkExprs c es
   >> checkImportDirective Open r n' c' i
   >>= pure . fromContext (importDirectiveAccess i)
-checkNiceDeclaration _ c
+checkNiceDeclaration' _ c
   (NiceModuleMacro r a a'
     (SectionApp _ bs (RawApp _ (Ident n : es))) DontOpen i)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n)
-  >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange a')) (fromName a')
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromQName n)
+  >>= \n' -> liftMaybe (ErrorInternal (ErrorName (getRange a'))) (fromName a')
   >>= \a'' -> liftLookup r n' (accessContextLookupModule n' c)
   >>= \(C.Module rs c') -> modifyDelete rs
   >> checkTypedBindings True c bs
   >>= \c'' -> checkExprs (c <> c'') es
   >> checkImportDirective Module r (QName a'') c' i
   >>= \c''' -> checkModuleName c''' (fromAccess a) r a''
-checkNiceDeclaration _ c
+checkNiceDeclaration' _ c
   (NiceModuleMacro r a a'
     (SectionApp _ bs (RawApp _ (Ident n : es))) DoOpen i)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n)
-  >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange a')) (fromName a')
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromQName n)
+  >>= \n' -> liftMaybe (ErrorInternal (ErrorName (getRange a'))) (fromName a')
   >>= \a'' -> liftLookup r n' (accessContextLookupModule n' c)
   >>= \(C.Module rs c') -> modifyDelete rs
   >> checkTypedBindings True c bs
@@ -1228,63 +1233,46 @@
   >> checkImportDirective Module r (QName a'') c' i
   >>= \c''' -> checkModuleName c''' (fromAccess a) r a''
   >>= \c'''' -> pure (c'''' <> fromContext (importDirectiveAccess i) c''')
-checkNiceDeclaration _ _
+checkNiceDeclaration' _ _
   (NiceModuleMacro _ _ _
     (SectionApp r _ _) _ _)
-  = throwError (ErrorInternal ErrorMacro r)
-checkNiceDeclaration _ _
+  = throwError (ErrorInternal (ErrorMacro r))
+checkNiceDeclaration' _ _
   (NiceModuleMacro r _ _
     (RecordModuleInstance _ _) _ _)
   = throwError (ErrorUnsupported UnsupportedMacro r)
 
-checkNiceDeclaration _ c (NiceOpen r n i)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n)
+checkNiceDeclaration' _ c (NiceOpen r n i)
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromQName n)
   >>= \n' -> liftLookup r n' (accessContextLookupModule n' c)
   >>= \(C.Module rs c') -> modifyDelete rs
   >> checkImportDirective Open r n' c' i
   >>= \c'' -> pure (fromContext (importDirectiveAccess i) c'')
 
-checkNiceDeclaration _ _ (NiceImport r n Nothing DontOpen i)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n)
-  >>= \n' -> checkFile (Just r) n'
+checkNiceDeclaration' _ _ (NiceImport r n Nothing DontOpen i)
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromQName n)
+  >>= \n' -> checkFile r n'
   >>= \c' -> checkImportDirective Import r n' c' i
   >>= \c'' -> pure (accessContextImport n' c'')
-checkNiceDeclaration _ _ (NiceImport r n Nothing DoOpen i)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n)
-  >>= \n' -> checkFile (Just r) n'
+checkNiceDeclaration' _ _ (NiceImport r n Nothing DoOpen i)
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromQName n)
+  >>= \n' -> checkFile r n'
   >>= \c' -> checkImportDirective Import r n' c' i
   >>= \c'' -> pure (accessContextImport n' c'
     <> fromContext (importDirectiveAccess i) c'')
-checkNiceDeclaration _ _ (NiceImport r n (Just a) DontOpen i)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n)
-  >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange a)) (fromAsName a)
-  >>= \a' -> checkFile (Just r) n'
+checkNiceDeclaration' _ _ (NiceImport r n (Just a) DontOpen i)
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromQName n)
+  >>= \n' -> checkFile r n'
   >>= \c' -> checkImportDirective Import r n' c' i
-  >>= \c'' -> checkModuleName c'' Public (getRange a) a'
-checkNiceDeclaration _ _ (NiceImport r n (Just a) DoOpen i)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n)
-  >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange a)) (fromAsName a)
-  >>= \a' -> checkFile (Just r) n'
+  >>= \c'' -> checkModuleNameMay c'' Public (getRange a) (fromAsName a)
+checkNiceDeclaration' _ _ (NiceImport r n (Just a) DoOpen i)
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromQName n)
+  >>= \n' -> checkFile r n'
   >>= \c' -> checkImportDirective Import r n' c' i
-  >>= \c'' -> checkModuleName c' Public (getRange a) a'
+  >>= \c'' -> checkModuleNameMay c' Public (getRange a) (fromAsName a)
   >>= \c''' -> pure (c''' <> fromContext (importDirectiveAccess i) c'')
 
-checkNiceDeclaration fs c (NiceDataDef _ _ _ _ _ n bs cs)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n)
-  >>= \n' -> pure (either (const []) id (accessContextLookup (QName n') c))
-  >>= \rs -> checkLamBindings False c bs
-  >>= \c' -> checkNiceConstructors fs rs (accessContextDefine n' c <> c') cs
-  >>= \c'' -> pure (accessContextModule' n' Public rs c'' <> c'')
-
-checkNiceDeclaration fs c (NiceRecDef _ _ _ _ _ n _ _ m bs ds)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n)
-  >>= \n' -> pure (either (const []) id (accessContextLookup (QName n') c))
-  >>= \rs -> checkLamBindings False c bs
-  >>= \c' -> checkNiceConstructorRecordMay fs rs (m >>= fromNameRange . fst)
-  >>= \c'' -> checkDeclarationsRecord n' rs (c <> c') ds
-  >>= \c''' -> pure (accessContextModule' n' Public rs (c'' <> c''') <> c'')
-
-checkNiceDeclaration fs c (NicePatternSyn _ a n ns p)
+checkNiceDeclaration' fs c (NicePatternSyn _ a n ns p)
   = localSkip (checkNames' False Public RangeVariable (unArg <$> ns))
   >>= \c' -> checkPattern (c <> c') p
   >> checkName' True fs (fromAccess a) RangePatternSynonym n
@@ -1295,7 +1283,7 @@
   => MonadState State m
   => MonadIO m
   => Name
-  -> [Range]
+  -> Set Range
   -- ^ Ranges associated with parent record.
   -> Fixities
   -> AccessContext
@@ -1341,11 +1329,10 @@
   = checkNiceDeclaration fs c d
 
 checkNiceDeclarationRecord n rs fs c (NiceField _ a _ _ _ n' (Arg _ e))
-  = checkExpr (accessContextDefine n c) e
+  = checkExpr (accessContextDefine n (accessContextDefineFields c)) e
   >> maybe
     (pure mempty)
-    (\n'' -> pure (accessContextItem n'' (fromAccess a)
-      (item rs (syntax fs n''))))
+    (\n'' -> pure (accessContextField n'' (fromAccess a) rs (syntax fs n'')))
     (fromName n')
 
 checkNiceDeclarations
@@ -1366,7 +1353,7 @@
   => MonadState State m
   => MonadIO m
   => Name
-  -> [Range]
+  -> Set Range
   -- ^ Ranges associated with parent record.
   -> Fixities
   -> AccessContext
@@ -1390,7 +1377,7 @@
   = checkNiceModule c (fromAccess a) r Nothing bs ds
 checkNiceDeclarationsTop fs c (d : ds)
   = checkNiceDeclaration fs c d
-  >>= \c' -> checkNiceDeclarations fs (c <> c') ds
+  >>= \c' -> checkNiceDeclarationsTop fs (c <> c') ds
 
 checkNiceSig
   :: MonadError Error m
@@ -1410,26 +1397,68 @@
   >>= \c' -> checkExpr (c <> c') e
   >> checkName' False fs (fromAccess a) t n
 
+checkNiceDataDef
+  :: MonadError Error m
+  => MonadReader Environment m
+  => MonadState State m
+  => MonadIO m
+  => Bool
+  -- ^ Whether to check bound names in lambda bindings.
+  -> Fixities
+  -> AccessContext
+  -> N.Name
+  -> [LamBinding]
+  -> [NiceConstructor]
+  -> m AccessContext
+checkNiceDataDef b fs c n bs cs
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromName n)
+  >>= \n' -> pure (either mempty id (accessContextLookup (QName n') c))
+  >>= \rs -> checkLamBindings b c bs
+  >>= \c' -> checkNiceConstructors fs rs (accessContextDefine n' c <> c') cs
+  >>= \c'' -> pure (accessContextModule' n' Public rs c'' <> c'')
+
+checkNiceRecordDef
+  :: MonadError Error m
+  => MonadReader Environment m
+  => MonadState State m
+  => MonadIO m
+  => Bool
+  -- ^ Whether to check bound names in lambda bindings.
+  -> Fixities
+  -> AccessContext
+  -> N.Name
+  -> Maybe (N.Name, IsInstance)
+  -> [LamBinding]
+  -> [Declaration]
+  -> m AccessContext
+checkNiceRecordDef b fs c n m bs ds
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromName n)
+  >>= \n' -> pure (either (const mempty) id (accessContextLookup (QName n') c))
+  >>= \rs -> checkLamBindings b c bs
+  >>= \c' -> checkNiceConstructorRecordMay fs rs (m >>= fromNameRange . fst)
+  >>= \c'' -> checkDeclarationsRecord n' rs (c <> c') ds
+  >>= \c''' -> pure (accessContextModule' n' Public rs (c'' <> c''') <> c'')
+
 checkNiceConstructor
   :: MonadError Error m
   => MonadReader Environment m
   => MonadState State m
   => MonadIO m
   => Fixities
-  -> [Range]
+  -> Set Range
   -- ^ Ranges associated with parent type.
   -> AccessContext
-  -> NiceDeclaration
+  -> NiceConstructor
   -> m AccessContext
 checkNiceConstructor fs rs c (Axiom _ a _ _ _ n e)
   = checkExpr c e
   >> maybe
     (pure mempty)
-    (\n'' -> pure (accessContextItem n'' (fromAccess a)
-      (itemConstructor rs (syntax fs n''))))
+    (\n'' -> pure (accessContextConstructor n'' (fromAccess a) rs
+      (syntax fs n'')))
     (fromName n)
 checkNiceConstructor _ _ _ d
-  = throwError (ErrorInternal ErrorConstructor (getRange d))
+  = throwError (ErrorInternal (ErrorConstructor (getRange d)))
 
 checkNiceConstructors
   :: MonadError Error m
@@ -1437,7 +1466,7 @@
   => MonadState State m
   => MonadIO m
   => Fixities
-  -> [Range]
+  -> Set Range
   -- ^ Ranges associated with parent type.
   -> AccessContext
   -> [NiceDeclaration]
@@ -1449,20 +1478,20 @@
   :: MonadReader Environment m
   => MonadState State m
   => Fixities
-  -> [Range]
+  -> Set Range
   -- ^ Ranges associated with record type.
   -> Range
   -> Name
   -> m AccessContext
 checkNiceConstructorRecord fs rs r n
   = modifyInsert r (RangeNamed RangeRecordConstructor (QName n))
-  >> pure (accessContextItem n Public (itemConstructor (r : rs) (syntax fs n)))
+  >> pure (accessContextConstructor n Public (Set.insert r rs) (syntax fs n))
 
 checkNiceConstructorRecordMay
   :: MonadReader Environment m
   => MonadState State m
   => Fixities
-  -> [Range]
+  -> Set Range
   -- ^ Ranges associated with record type.
   -> Maybe (Range, Name)
   -> m AccessContext
@@ -1536,14 +1565,12 @@
   -> ImportDirective
   -> m Context
 checkImportDirective dt r n c (ImportDirective _ UseEverything hs rs _)
-  = maybe (pure ()) (\t -> modifyInsert r (RangeNamed t n))
-    (directiveStatement dt)
-  >> modifyHidings c hs
-  >>= flip (modifyRenamings dt) rs
-  >>= contextInsertRangeAll r
+  = traverse (\t -> modifyInsert r (RangeNamed t n)) (directiveStatement dt)
+  >> modifyHidings c (hs <> (renFrom <$> rs))
+  >>= \c' -> checkRenamings dt c rs
+  >>= \c'' -> contextInsertRangeAll r (c' <> c'')
 checkImportDirective dt r n c (ImportDirective _ (Using ns) _ rs _)
-  = maybe (pure ()) (\t -> modifyInsert r (RangeNamed t n))
-    (directiveStatement dt)
+  = traverse (\t -> modifyInsert r (RangeNamed t n)) (directiveStatement dt)
   >> checkImportedNames dt c ns
   >>= \c' -> checkRenamings dt c rs
   >>= \c'' -> contextInsertRangeAll r (c' <> c'')
@@ -1590,20 +1617,22 @@
   -> (Range, ImportedName, ImportedName)
   -> m Context
 checkImportedNamePair dt c (_, ImportedName n, ImportedName t)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n)
-  >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange t)) (fromNameRange t)
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromName n)
+  >>= \n' -> liftMaybe (ErrorInternal (ErrorName (getRange t)))
+    (fromNameRange t)
   >>= \(r, t') -> modifyInsert r (RangeNamed (directiveItem dt) (QName t'))
   >> pure (maybe mempty (contextItem t') (contextLookupItem (QName n') c)
     <> maybe mempty (contextModule t') (contextLookupModule (QName n') c))
   >>= contextInsertRangeAll r
 checkImportedNamePair dt c (_, ImportedModule n, ImportedModule t)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n)
-  >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange t)) (fromNameRange t)
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromName n)
+  >>= \n' -> liftMaybe (ErrorInternal (ErrorName (getRange t)))
+    (fromNameRange t)
   >>= \(r, t') -> modifyInsert r (RangeNamed (directiveItem dt) (QName t'))
   >> pure (maybe mempty (contextModule t') (contextLookupModule (QName n') c))
   >>= contextInsertRangeAll r
 checkImportedNamePair _ _ (r, _, _)
-  = throwError (ErrorInternal ErrorRenaming r)
+  = throwError (ErrorInternal (ErrorRenaming r))
 
 checkImportedNames
   :: MonadError Error m
@@ -1622,10 +1651,10 @@
   -> ImportedName
   -> m Context
 modifyHiding c (ImportedName n)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n)
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromName n)
   >>= pure . flip contextDelete c
 modifyHiding c (ImportedModule n)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n)
+  = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromName n)
   >>= pure . flip contextDeleteModule c
 
 modifyHidings
@@ -1636,39 +1665,6 @@
 modifyHidings
   = foldM modifyHiding
 
-modifyRenaming
-  :: MonadError Error m
-  => MonadReader Environment m
-  => MonadState State m
-  => DirectiveType
-  -> Context
-  -> Renaming
-  -> m Context
-modifyRenaming dt c (Renaming (ImportedName n) (ImportedName t) _ _)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n)
-  >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange t)) (fromNameRange t)
-  >>= \(r, t') -> modifyInsert r (RangeNamed (directiveItem dt) (QName t'))
-  >> contextRename n' t' r c
-  >>= contextRenameModule n' t' r
-modifyRenaming dt c (Renaming (ImportedModule n) (ImportedModule t) _ _)
-  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n)
-  >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange t)) (fromNameRange t)
-  >>= \(r, t') -> modifyInsert r (RangeNamed (directiveItem dt) (QName t'))
-  >> contextRenameModule n' t' r c
-modifyRenaming _ _ r
-  = throwError (ErrorInternal ErrorRenaming (getRange r))
-
-modifyRenamings
-  :: MonadError Error m
-  => MonadReader Environment m
-  => MonadState State m
-  => DirectiveType
-  -> Context
-  -> [Renaming]
-  -> m Context
-modifyRenamings dt
-  = foldM (modifyRenaming dt)
-
 touchModule
   :: MonadError Error m
   => MonadReader Environment m
@@ -1703,6 +1699,14 @@
 touchContext c
   = modifyDelete (contextRanges c)
 
+touchAccessContext
+  :: MonadReader Environment m
+  => MonadState State m
+  => AccessContext
+  -> m ()
+touchAccessContext c
+  = modifyDelete (accessContextRanges c)
+
 importDirectiveAccess
   :: ImportDirective
   -> Access
@@ -1718,10 +1722,21 @@
   => MonadReader Environment m
   => MonadState State m
   => MonadIO m
-  => Module
+  => QName
+  -> Module
   -> m Context
-checkModule (_, ds)
-  = toContext <$> checkDeclarationsTop mempty ds
+checkModule n (_, ds) = do
+  local
+    <- askLocal
+  _
+    <- modifyBlock n
+  context
+    <- toContext <$> checkDeclarationsTop mempty ds
+  _
+    <- modifyCheck n context
+  _
+    <- when local (touchContext context)
+  pure context
 
 -- ## Files
 
@@ -1730,172 +1745,270 @@
   => MonadReader Environment m
   => MonadState State m
   => MonadIO m
-  => Maybe Range
+  => Range
   -> QName
   -> m Context
 checkFile r n
-  = gets (stateLookup n) >>= \s -> checkFileWith s r n
+  = getModule n
+  >>= checkFileWith r n
 
 checkFileWith
   :: MonadError Error m
   => MonadReader Environment m
   => MonadState State m
   => MonadIO m
-  => Maybe ModuleState
-  -> Maybe Range
+  => Range
   -> QName
+  -> Maybe ModuleState
   -> m Context
+checkFileWith r n Nothing
+  = askRoot
+  >>= \p -> pure (p </> qNamePath n)
+  >>= \p' -> liftIO (doesFileExist p')
+  >>= \b -> checkFileWith' r n (bool Nothing (Just p') b)
+checkFileWith r n (Just Blocked)
+  = throwError (ErrorCyclic r n)
+checkFileWith _ _ (Just (Checked c))
+  = pure c
 
-checkFileWith Nothing r n | isBuiltin n
-  = liftIO (getDataFileName ("data" </> qNamePath n))
-  >>= \p -> localSkip (checkFilePath r n p)
+checkFileWith'
+  :: MonadError Error m
+  => MonadReader Environment m
+  => MonadState State m
+  => MonadIO m
+  => Range
+  -> QName
+  -> Maybe FilePath
+  -> m Context
+checkFileWith' r n Nothing
+  = checkFileExternal r n
+checkFileWith' _ n (Just p)
+  = checkFilePath n p
 
-checkFileWith Nothing r n = do
-  local
-    <- askLocal
-  rootPath
-    <- askRoot
-  context
-    <- checkFilePath r n (rootPath </> qNamePath n)
+checkFileExternal
+  :: MonadError Error m
+  => MonadReader Environment m
+  => MonadState State m
+  => MonadIO m
+  => Range
+  -> QName
+  -> m Context
+checkFileExternal r n = do
+  includes
+    <- askIncludes
+  sources
+    <- getSources
+  (pathEither, sources') 
+    <- liftIO (findFile'' includes (toTopLevelModuleName (toQName n)) sources)
+  path
+    <- liftEither (mapLeft (ErrorFind r n) pathEither)
   _
-    <- bool (pure ()) (touchContext context) local
+    <- modifySources sources'
+  context
+    <- localSkip (checkFilePath n (filePath (srcFilePath path)))
   pure context
 
-checkFileWith (Just Blocked) r n
-  = throwError (ErrorCyclic r n)
-checkFileWith (Just (Checked c)) _ _
-  = pure c
-
 checkFilePath
   :: MonadError Error m
   => MonadReader Environment m
   => MonadState State m
   => MonadIO m
-  => Maybe Range
-  -> QName
+  => QName
   -> FilePath
   -> m Context
-checkFilePath r n p = do
-  _
-    <- modify (stateBlock n)
+checkFilePath n p
+  = readModule p
+  >>= checkModule n
+
+checkFileTop
+  :: MonadError Error m
+  => MonadIO m
+  => Mode
+  -> UnusedOptions
+  -> FilePath
+  -- ^ The file to check.
+  -> m (FilePath, State)
+  -- ^ The project root, along with the final state.
+checkFileTop m opts p = do
+  module'
+    <- readModule p
+  moduleName
+    <- pure (topLevelModuleName module')
+  moduleQName
+    <- liftMaybe (ErrorInternal (ErrorModuleName p)) (fromModuleName moduleName)
   absolutePath
-    <- pure (AbsolutePath (T.pack p))
+    <- pure (projectRoot (mkAbsolute p) moduleName)
+  rootPath
+    <- pure (filePath absolutePath)
+  includesEither
+    <- liftIO (runTCMTop (setOptions opts >> getIncludeDirs))
+  includes
+    <- liftEither (mapLeft (const ErrorInclude) includesEither)
+  env
+    <- pure (Environment m rootPath includes)
+  (_, state)
+    <- runStateT (runReaderT (checkModule moduleQName module') env) stateEmpty
+  pure (rootPath, state)
+
+readModule
+  :: MonadError Error m
+  => MonadIO m
+  => FilePath
+  -> m Module
+readModule p = do
   exists
     <- liftIO (doesFileExist p)
   _
-    <- bool (throwError (ErrorFile r n p)) (pure ()) exists
+    <- unless exists (throwError (ErrorFile p))
+  absolutePath
+    <- pure (mkAbsolute p)
   contents
     <- liftIO (readFile p)
   (parseResult, _)
     <- liftIO (runPMIO (parseFile moduleParser absolutePath contents))
   (module', _)
     <- liftEither (mapLeft ErrorParse parseResult)
-  context
-    <- checkModule module'
-  _
-    <- modify (stateCheck n context)
-  pure context
+  pure module'
 
 -- ## Paths
 
--- Look for unvisited modules at the given path.
+-- Look for unvisited modules.
 checkPath
-  :: MonadIO m
-  => [QName]
-  -- ^ Visited or ignored modules.
+  :: Set QName
+  -- ^ Visited modules.
   -> FilePath
+  -- ^ A path to ignore.
+  -> FilePath
   -- ^ The project root path.
+  -> IO [FilePath]
+checkPath ns i r
+  = Set.toAscList <$> checkPath' ns i r r
+
+-- Look for unvisited modules at the given path.
+checkPath'
+  :: Set QName
+  -- ^ Visited modules.
   -> FilePath
+  -- ^ A path to ignore.
+  -> FilePath
+  -- ^ The project root path.
+  -> FilePath
   -- ^ The path at which to look.
-  -> m [FilePath]
-checkPath ms p p'
-  = liftIO (doesDirectoryExist p')
-  >>= bool (pure (checkPathFile ms p p')) (checkPathDirectory ms p p')
+  -> IO (Set FilePath)
+checkPath' ns i r p
+  = liftIO (doesDirectoryExist p)
+  >>= bool (pure (checkPathFile ns i r p)) (checkPathDirectory ns i r p)
 
 checkPathFile
-  :: [QName]
+  :: Set QName
+  -- ^ Visited modules.
   -> FilePath
+  -- ^ A path to ignore.
   -> FilePath
-  -> [FilePath]
-checkPathFile ms p p'
-  = maybe [] (bool [p'] [] . flip elem ms) (pathQName p p')
+  -- ^ The project root path.
+  -> FilePath
+  -- ^ The path at which to look.
+  -> Set FilePath
+checkPathFile _ i _ p | i == p
+  = mempty
+checkPathFile ns _ r p
+  = maybe mempty (bool (Set.singleton p) mempty . flip Set.member ns)
+  $ pathQName r p
 
 checkPathDirectory
-  :: MonadIO m
-  => [QName]
+  :: Set QName
+  -- ^ Visited modules.
   -> FilePath
+  -- ^ A path to ignore.
   -> FilePath
-  -> m [FilePath]
-checkPathDirectory ms p p'
-  = fmap (p' </>) <$> liftIO (listDirectory p')
-  >>= traverse (checkPath ms p)
-  >>= pure . concat
-
--- ## Roots
-
-checkRoot
-  :: MonadError Error m
-  => MonadReader Environment m
-  => MonadState State m
-  => MonadIO m
-  => Root
-  -> m ()
-checkRoot (Root p Nothing)
-  = checkFile Nothing p
-  >>= touchContext
-checkRoot (Root p (Just ns))
-  = checkFile Nothing p
-  >>= \c -> touchQNamesContext c p ns
-
-checkRoots
-  :: MonadError Error m
-  => MonadReader Environment m
-  => MonadState State m
-  => MonadIO m
-  => [Root]
-  -> m ()
-checkRoots
-  = void . traverse checkRoot
+  -- ^ The project root path.
+  -> FilePath
+  -- ^ The path at which to look.
+  -> IO (Set FilePath)
+checkPathDirectory ns i r p
+  = fmap (p </>) <$> liftIO (listDirectory p)
+  >>= traverse (checkPath' ns i r)
+  >>= pure . mconcat
 
 -- ## Main
 
--- | Check an Agda file and its dependencies for unused code.
+-- | Check an Agda file and its dependencies for unused code, excluding public
+-- items that could be imported elsewhere.
 checkUnused
-  :: FilePath
-  -- ^ The project root path.
-  -> Roots
-  -- ^ The public entry points for the project.
-  -> IO (Either Error Unused)
-checkUnused p (Roots rs is)
-  = runExceptT
-  $ checkUnusedItems False p (checkRoots rs)
-  >>= \s -> checkPath (is <> stateModules s) p p
-  >>= \fs -> pure (Unused (UnusedItems (stateItems s)) fs)
+  :: UnusedOptions
+  -- ^ Options to use.
+  -> FilePath
+  -- ^ Absolute path of the file to check.
+  -> IO (Either Error UnusedItems)
+checkUnused
+  = checkUnusedWith Local
 
--- | Check an Agda file for unused code.
-checkUnusedLocal
-  :: FilePath
-  -- ^ The project root path.
-  -> QName
-  -- ^ The module to check.
+-- | Check an Agda file and its dependencies for unused code, using the
+-- specified check mode.
+checkUnusedWith
+  :: Mode
+  -- ^ The check mode to use.
+  -> UnusedOptions
+  -- ^ Options to use.
+  -> FilePath
+  -- ^ Absolute path of the file to check.
   -> IO (Either Error UnusedItems)
-checkUnusedLocal p
+checkUnusedWith m opts
   = runExceptT
-  . fmap UnusedItems
-  . fmap stateItems
-  . checkUnusedItems True p
-  . checkFile Nothing
+  . fmap (UnusedItems . stateItems . snd)
+  . checkFileTop m opts
 
-checkUnusedItems
-  :: MonadError Error m
-  => MonadIO m
-  => Bool
-  -- ^ Whether to use local mode.
+-- | Check an Agda file and its dependencies for unused code, including public
+-- items in dependencies, as well as files.
+--
+-- The given file should consist only of import statements; it serves as a
+-- full description of the public interface of the project.
+checkUnusedGlobal
+  :: UnusedOptions
+  -- ^ Options to use.
   -> FilePath
-  -> ReaderT Environment (StateT State m) a
-  -> m State
-checkUnusedItems l p
-  = fmap snd
-  . flip runStateT stateEmpty
-  . flip runReaderT (Environment False l p)
+  -- ^ Absolute path of the file to check.
+  -> IO (Either Error Unused)
+checkUnusedGlobal opts p
+  = runExceptT (checkUnusedGlobal' opts p)
+
+checkUnusedGlobal'
+  :: UnusedOptions
+  -> FilePath
+  -> ExceptT Error IO Unused
+checkUnusedGlobal' opts p = do
+  (rootPath, state)
+    <- checkFileTop GlobalMain opts p
+  files
+    <- liftIO (checkPath (stateModules state) p rootPath)
+  items 
+    <- pure (UnusedItems (filter (not . inFile p) (stateItems state)))
+  unused
+    <- pure (Unused files items)
+  pure unused
+
+setOptions
+  :: UnusedOptions
+  -> TCM ()
+setOptions opts
+  = setCommandLineOptions
+  $ defaultOptions
+  { optIncludePaths
+    = unusedOptionsInclude opts
+  , optLibraries
+    = T.unpack <$> unusedOptionsLibraries opts
+  , optOverrideLibrariesFile
+    = unusedOptionsLibrariesFile opts
+  , optDefaultLibs
+    = unusedOptionsUseDefaultLibraries opts
+  , optUseLibs
+    = unusedOptionsUseLibraries opts
+  }
+
+inFile
+  :: FilePath
+  -> (Range, RangeInfo)
+  -> Bool
+inFile p (r, _)
+  = rangePath r == Just p
 
diff --git a/src/Agda/Unused/Monad/Error.hs b/src/Agda/Unused/Monad/Error.hs
--- a/src/Agda/Unused/Monad/Error.hs
+++ b/src/Agda/Unused/Monad/Error.hs
@@ -27,6 +27,8 @@
 import Agda.Unused.Types.Range
   (Range, getRange)
 
+import Agda.Interaction.FindFile
+  (FindError)
 import Agda.Syntax.Concrete.Definitions
   (DeclarationException)
 import Agda.Syntax.Concrete.Fixity
@@ -49,7 +51,7 @@
 
   -- | Cyclic module dependency.
   ErrorCyclic
-    :: !(Maybe Range)
+    :: !Range
     -> !QName
     -> Error
 
@@ -60,9 +62,14 @@
 
   -- | File not found.
   ErrorFile
-    :: !(Maybe Range)
+    :: !FilePath
+    -> Error
+
+  -- | Agda find error.
+  ErrorFind
+    :: !Range
     -> !QName
-    -> !FilePath
+    -> !FindError
     -> Error
 
   -- | Agda fixity exception.
@@ -70,10 +77,18 @@
     :: !(Maybe Range)
     -> Error
 
+  -- | Illegal declaration in main module of global check.
+  ErrorGlobal
+    :: !Range
+    -> Error
+
+  -- | Error in computing include paths.
+  ErrorInclude
+    :: Error
+
   -- | Internal error; should be reported.
   ErrorInternal
     :: !InternalError
-    -> !Range
     -> Error
 
   -- | Module not found in open statement.
@@ -104,31 +119,39 @@
     -> !Range
     -> Error
 
-  deriving Show
-
 -- | An internal error, indicating a bug in our code. This type of error should
 -- be reported by filing an issue.
 data InternalError where
 
   -- | Unexpected declaration type for constructor.
   ErrorConstructor
-    :: InternalError
+    :: !Range
+    -> InternalError
 
   -- | Unexpected arguments to SectionApp constructor.
   ErrorMacro
-    :: InternalError
+    :: !Range
+    -> InternalError
 
+  -- | Unexpected empty top level module name.
+  ErrorModuleName
+    :: !FilePath
+    -> InternalError
+
   -- | Unexpected underscore as name.
   ErrorName
-    :: InternalError
+    :: !Range
+    -> InternalError
 
   -- | Unexpected name-module mismatch in renaming statement.
   ErrorRenaming
-    :: InternalError
+    :: !Range
+    -> InternalError
 
   -- | Unexpected data type constructor.
   ErrorUnexpected
     :: !UnexpectedError
+    -> !Range
     -> InternalError
 
   deriving Show
@@ -202,7 +225,7 @@
   warnPolarityPragmasButNotPostulates _
     = pure ()
 
--- ## Lookup
+-- ## Lift
 
 -- | Lift a lookup result to our error monad.
 liftLookup
diff --git a/src/Agda/Unused/Monad/Reader.hs b/src/Agda/Unused/Monad/Reader.hs
--- a/src/Agda/Unused/Monad/Reader.hs
+++ b/src/Agda/Unused/Monad/Reader.hs
@@ -7,51 +7,95 @@
 
   ( -- * Definition
     
-    Environment(..)
+    Mode(..)
+  , Environment(..)
 
     -- * Ask
 
   , askSkip
   , askLocal
+  , askGlobalMain
   , askRoot
+  , askIncludes
 
     -- * Local
 
   , localSkip
+  , localGlobal
 
   ) where
 
+import Agda.Utils.FileName
+  (AbsolutePath)
 import Control.Monad.Reader
   (MonadReader, ask, local)
 
+-- ## Definition
+
+-- | A type indicating how checking should be done.
+data Mode where
+
+  -- | Check nothing.
+  Skip
+    :: Mode
+
+  -- | Check private items only.
+  Local
+    :: Mode
+
+  -- | Check all items.
+  Global
+    :: Mode
+
+  -- | Check imports & reject all other declarations.
+  GlobalMain
+    :: Mode
+
+  deriving (Eq, Show)
+
 -- | An environment type for use in a reader monad.
 data Environment
   = Environment
-  { environmentSkip
-    :: !Bool
-    -- ^ Whether to skip all names.
-  , environmentLocal
-    :: !Bool
-    -- ^ Whether to skip public names.
+  { environmentMode
+    :: !Mode
+    -- ^ The current check mode.
   , environmentRoot
     :: !FilePath
     -- ^ The project root path.
+  , environmentIncludes
+    :: ![AbsolutePath]
+    -- ^ The include paths.
   } deriving Show
 
+-- ## Ask
+
+askMode
+  :: MonadReader Environment m
+  => m Mode
+askMode
+  = environmentMode <$> ask
+
 -- | Ask whether to skip checking names.
 askSkip
   :: MonadReader Environment m
   => m Bool
 askSkip
-  = environmentSkip <$> ask
+  = (== Skip) <$> askMode
 
--- | Ask whether to skip checking public names.
+-- | Ask whether we are in local mode.
 askLocal
   :: MonadReader Environment m
   => m Bool
 askLocal
-  = environmentLocal <$> ask
+  = (== Local) <$> askMode
 
+-- | Ask whether we are in global main mode.
+askGlobalMain
+  :: MonadReader Environment m
+  => m Bool
+askGlobalMain
+  = (== GlobalMain) <$> askMode
+
 -- | Ask for the project root path.
 askRoot
   :: MonadReader Environment m
@@ -59,11 +103,36 @@
 askRoot
   = environmentRoot <$> ask
 
--- | Skip checking names in a local computation.
+-- | Ask for the include paths.
+askIncludes
+  :: MonadReader Environment m
+  => m [AbsolutePath]
+askIncludes
+  = environmentIncludes <$> ask
+
+-- ## Local
+
+localMode
+  :: MonadReader Environment m
+  => Mode
+  -> m a
+  -> m a
+localMode m
+  = local (\e -> e {environmentMode = m})
+
+-- | Perform a local computation, but skip checking names.
 localSkip
   :: MonadReader Environment m
   => m a
   -> m a
 localSkip
-  = local (\e -> e {environmentSkip = True})
+  = localMode Skip
+
+-- | Perform a local computation in global mode.
+localGlobal
+  :: MonadReader Environment m
+  => m a
+  -> m a
+localGlobal
+  = localMode Global
 
diff --git a/src/Agda/Unused/Monad/State.hs b/src/Agda/Unused/Monad/State.hs
--- a/src/Agda/Unused/Monad/State.hs
+++ b/src/Agda/Unused/Monad/State.hs
@@ -15,14 +15,19 @@
   , stateEmpty
   , stateItems
   , stateModules
-  , stateBlock
-  , stateCheck
-  , stateLookup
 
+    -- * Get
+
+  , getModule
+  , getSources
+
     -- * Modify
 
-  , modifyDelete
   , modifyInsert
+  , modifyDelete
+  , modifyBlock
+  , modifyCheck
+  , modifySources
 
   ) where
 
@@ -34,20 +39,24 @@
   (QName)
 import Agda.Unused.Types.Range
   (Range, Range'(..), RangeInfo, rangeContains)
-import Agda.Unused.Utils
-  (mapDeletes)
 
+import Agda.TypeChecking.Monad.Base
+  (ModuleToSource)
+import Control.Monad
+  (unless)
 import Control.Monad.Reader
   (MonadReader)
 import Control.Monad.State
-  (MonadState, modify)
-import Data.Bool
-  (bool)
+  (MonadState, gets, modify)
 import Data.Map.Strict
   (Map)
 import qualified Data.Map.Strict
   as Map
+import Data.Set
+  (Set)
 
+-- ## Definitions
+
 -- | Cache the results of checking modules. This allows us to:
 -- 
 -- - Avoid duplicate computations.
@@ -72,13 +81,18 @@
   , stateModules'
     :: !(Map QName ModuleState)
     -- ^ States for each module dependency.
+  , stateSources'
+    :: !ModuleToSource
+    -- ^ A cache of source paths corresponding to certain module names.
   } deriving Show
 
+-- ## Interface
+
 -- | Construct an empty state.
 stateEmpty
   :: State
 stateEmpty
-  = State mempty mempty
+  = State mempty mempty mempty
 
 -- | Get a sorted list of state items.
 --
@@ -92,14 +106,6 @@
   . Map.toAscList
   . stateItems'
 
--- | Get a list of visited modules.
-stateModules
-  :: State
-  -> [QName]
-stateModules
-  = Map.keys
-  . stateModules'
-
 -- Remove nested items.
 stateItemsFilter
   :: [(Range, RangeInfo)]
@@ -108,9 +114,26 @@
   = []
 stateItemsFilter (i : i' : is) | rangeContains (fst i) (fst i')
   = stateItemsFilter (i : is)
+stateItemsFilter (i : i' : is) | rangeContains (fst i') (fst i)
+  = stateItemsFilter (i' : is)
 stateItemsFilter (i : is)
   = i : stateItemsFilter is
 
+-- | Get a list of visited modules.
+stateModules
+  :: State
+  -> Set QName
+stateModules
+  = Map.keysSet
+  . stateModules'
+
+stateSources
+  :: ModuleToSource
+  -> State
+  -> State
+stateSources ss (State rs ms _)
+  = State rs ms ss
+
 stateInsert
   :: Range
   -> RangeInfo
@@ -118,41 +141,57 @@
   -> State
 stateInsert NoRange _ s
   = s
-stateInsert r@(Range _ _) i (State rs ms)
-  = State (Map.insert r i rs) ms
+stateInsert r@(Range _ _) i (State rs ms ss)
+  = State (Map.insert r i rs) ms ss
 
 stateDelete
-  :: [Range]
+  :: Set Range
   -> State
   -> State
-stateDelete rs (State rs' ms)
-  = State (mapDeletes rs rs') ms
+stateDelete rs (State rs' ms ss)
+  = State (Map.withoutKeys rs' rs) ms ss
 
--- | Lookup the state of a module.
-stateLookup
+stateModule
   :: QName
   -> State
   -> Maybe ModuleState
-stateLookup m (State _ ms)
-  = Map.lookup m ms
+stateModule n (State _ ms _)
+  = Map.lookup n ms
 
--- | Mark that we are beginning to check a module.
 stateBlock
   :: QName
   -> State
   -> State
-stateBlock m (State rs ms)
-  = State rs (Map.insert m Blocked ms)
+stateBlock n (State rs ms ss)
+  = State rs (Map.insert n Blocked ms) ss
 
--- | Record the results of checking a module.
 stateCheck
   :: QName
   -> Context
   -> State
   -> State
-stateCheck m c (State rs ms)
-  = State rs (Map.insert m (Checked c) ms)
+stateCheck n c (State rs ms ss)
+  = State rs (Map.insert n (Checked c) ms) ss
 
+-- ## Get
+
+-- | Get the state of a module.
+getModule
+  :: MonadState State m
+  => QName
+  -> m (Maybe ModuleState)
+getModule n
+  = gets (stateModule n)
+
+-- | Get the cache of source paths.
+getSources
+  :: MonadState State m
+  => m ModuleToSource
+getSources
+  = gets stateSources'
+
+-- ## Modify
+
 -- | Record a new unused item.
 modifyInsert
   :: MonadReader Environment m
@@ -161,14 +200,39 @@
   -> RangeInfo
   -> m ()
 modifyInsert r i
-  = askSkip >>= bool (modify (stateInsert r i)) (pure ())
+  = askSkip >>= flip unless (modify (stateInsert r i))
 
 -- | Mark a list of items as used.
 modifyDelete
   :: MonadReader Environment m
   => MonadState State m
-  => [Range]
+  => Set Range
   -> m ()
 modifyDelete rs
-  = askSkip >>= bool (modify (stateDelete rs)) (pure ())
+  = askSkip >>= flip unless (modify (stateDelete rs))
+
+-- | Mark that we are beginning to check a module.
+modifyBlock
+  :: MonadState State m
+  => QName
+  -> m ()
+modifyBlock n
+  = modify (stateBlock n)
+
+-- | Record the results of checking a module.
+modifyCheck
+  :: MonadState State m
+  => QName
+  -> Context
+  -> m ()
+modifyCheck n c
+  = modify (stateCheck n c)
+
+-- | Update the cache of sources.
+modifySources
+  :: MonadState State m
+  => ModuleToSource
+  -> m ()
+modifySources ss
+  = modify (stateSources ss)
 
diff --git a/src/Agda/Unused/Parse.hs b/src/Agda/Unused/Parse.hs
deleted file mode 100644
--- a/src/Agda/Unused/Parse.hs
+++ /dev/null
@@ -1,150 +0,0 @@
-{- |
-Module: Agda.Unused.Parse
-
-Parsers for roots.
--}
-module Agda.Unused.Parse
-  ( parseConfig
-  ) where
-
-import Agda.Unused.Types.Name
-  (Name(..), NamePart(..), QName(..))
-import Agda.Unused.Types.Root
-  (Root(..), Roots, fromList)
-import Agda.Unused.Utils
-  (mapLeft)
-
-import Control.Monad
-  (void)
-import Data.Char
-  (isSpace)
-import Data.Text
-  (Text)
-import qualified Data.Text
-  as T
-import Data.Void
-  (Void)
-import Text.Megaparsec
-  (Parsec, (<|>), between, many, parse, satisfy, some, try)
-import Text.Megaparsec.Char
-  (char, space1)
-import qualified Text.Megaparsec.Char.Lexer
-  as L
-import Text.Megaparsec.Error
-  (errorBundlePretty)
-
--- ## Utilities
-
-isNameChar
-  :: Char
-  -> Bool
-isNameChar '.'
-  = False
-isNameChar '('
-  = False
-isNameChar ')'
-  = False
-isNameChar c | isSpace c
-  = False
-isNameChar _
-  = True
-
-listMaybe
-  :: [a]
-  -> Maybe [a]
-listMaybe []
-  = Nothing
-listMaybe xs@(_ : _)
-  = Just xs
-
--- ## Parsers
-
-type Parser
-  = Parsec Void Text
-
-parseSpace
-  :: Parser ()
-parseSpace
-  = L.space space1
-    (L.skipLineComment "--")
-    (L.skipBlockComment "{-" "-}")
-
-parseDot
-  :: Parser ()
-parseDot
-  = void (char '.')
-
-parseHyphen
-  :: Parser ()
-parseHyphen
-  = void (char '-')
-
-parseParens
-  :: Parser a
-  -> Parser a
-parseParens
-  = between (char '(') (char ')')
-
-parseNamePart
-  :: Parser NamePart
-parseNamePart
-  = Id <$> some (satisfy isNameChar)
-
-parseName
-  :: Parser Name
-parseName
-  = Name <$> some parseNamePart
-
-parseQName
-  :: Parser QName
-parseQName
-  = try (Qual <$> parseName <* parseDot <*> parseQName)
-  <|> QName <$> parseName
-
-parseIgnore
-  :: Parser QName
-parseIgnore
-  = parseParens (between parseSpace parseSpace parseQName)
-  <* parseSpace
-
-parseRootName
-  :: Parser QName
-parseRootName
-  = parseHyphen
-  *> parseSpace
-  *> parseQName
-  <* parseSpace
-
-parseRootNames
-  :: Parser (Maybe [QName])
-parseRootNames
-  = listMaybe <$> many parseRootName
-
-parseRoot
-  :: Parser Root
-parseRoot
-  = Root
-  <$> parseQName
-  <* parseSpace
-  <*> parseRootNames
-
-parseRootEither
-  :: Parser (Either QName Root)
-parseRootEither
-  = Left <$> parseIgnore
-  <|> Right <$> parseRoot
-
-parseRoots
-  :: Parser Roots
-parseRoots
-  = fromList <$> many parseRootEither
-
--- | Parse configuration, producing either an error or a collection of roots.
-parseConfig
-  :: Text
-  -> Either Text Roots
-parseConfig
-  = mapLeft T.pack
-  . mapLeft errorBundlePretty
-  . parse (parseSpace *> parseRoots) ".agda-roots"
-
diff --git a/src/Agda/Unused/Print.hs b/src/Agda/Unused/Print.hs
--- a/src/Agda/Unused/Print.hs
+++ b/src/Agda/Unused/Print.hs
@@ -19,6 +19,8 @@
 import Agda.Unused.Types.Range
   (Range, Range'(..), RangeInfo(..), RangeType(..), getRange)
 
+import Agda.Interaction.FindFile
+  (FindError(..))
 import Agda.Utils.Pretty
   (prettyShow)
 import Data.Text
@@ -85,14 +87,14 @@
   -> Text
   -> Text
 printMessage t1 t2
-  = T.unlines [t1, t2]
+  = T.intercalate "\n" [t1, t2]
 
 printMessageIndent
   :: Text
   -> Text
   -> Text
 printMessageIndent t1 t2
-  = T.unlines [t1, indent t2]
+  = T.intercalate "\n" [t1, indent t2]
 
 -- ## Errors
 
@@ -105,53 +107,76 @@
   = printMessage (printRange r)
   $ "Error: Ambiguous name " <> parens (quote (printQName n)) <> "."
 printError (ErrorCyclic r n)
-  = printMessage (maybe (printQName n) printRange r)
+  = printMessage (printRange r)
   $ "Error: Cyclic module dependency " <> parens (printQName n) <> "."
-printError (ErrorFile r n p)
-  = printMessage (maybe (printQName n) printRange r)
-  $ "Error: File not found " <> parens (T.pack p) <> "."
+printError (ErrorFind r n (NotFound _))
+  = printMessage (printRange r)
+  $ "Error: Import not found " <> parens (printQName n) <> "."
+printError (ErrorFind r n (Ambiguous _))
+  = printMessage (printRange r)
+  $ "Error: Ambiguous import " <> parens (printQName n) <> "."
 printError (ErrorFixity (Just r))
   = printMessage (printRange r)
   $ "Error: Multiple fixity declarations."
-printError (ErrorInternal e r)
+printError (ErrorGlobal r)
   = printMessage (printRange r)
-  $ "Internal error: " <> printInternalError e
+  $ "Error: With --global, all declarations in the given file must be imports."
 printError (ErrorOpen r n)
   = printMessage (printRange r)
   $ "Error: Module not found " <> parens (printQName n) <> "."
 printError (ErrorPolarity (Just r))
   = printMessage (printRange r)
   $ "Error: Multiple polarity declarations."
-printError (ErrorRoot m n)
-  = printMessage (printQName m)
-  $ "Error: Root not found " <> parens (quote (printQName n)) <> "."
+printError (ErrorRoot n n')
+  = printMessage (printQName n)
+  $ "Error: Root not found " <> parens (quote (printQName n')) <> "."
 printError (ErrorUnsupported e r)
   = printMessage (printRange r)
   $ "Error: " <> printUnsupportedError e <> " not supported."
 
+printError (ErrorDeclaration e)
+  = printRange (getRange e) <> "\n" <> T.pack (prettyShow e)
+printError (ErrorFile p)
+  = printErrorFile p
 printError (ErrorFixity Nothing)
   = "Error: Multiple fixity declarations."
+printError ErrorInclude
+  = "Error: Invalid path-related options."
+printError (ErrorInternal e)
+  = printInternalError e
+printError (ErrorParse e)
+  = T.pack (prettyShow e)
 printError (ErrorPolarity Nothing)
   = "Error: Multiple polarity declarations."
 
-printError (ErrorDeclaration e)
-  = printRange (getRange e) <> "\n" <> T.pack (prettyShow e)
-printError (ErrorParse e)
-  = T.pack (show e)
+printErrorFile
+  :: FilePath
+  -> Text
+printErrorFile p
+  = "Error: File not found " <> parens (T.pack p) <> "."
 
 printInternalError
   :: InternalError
   -> Text
-printInternalError ErrorConstructor
-  = "Invalid data constructor."
-printInternalError ErrorMacro
-  = "Invalid module application."
-printInternalError ErrorName
-  = "Invalid name."
-printInternalError ErrorRenaming
-  = "Invalid renaming directive."
-printInternalError (ErrorUnexpected e)
-  = "Unexpected constructor " <> quote (printUnexpectedError e) <> "."
+printInternalError (ErrorConstructor r)
+  = printMessage (printRange r)
+  $ "Internal error: Invalid data constructor."
+printInternalError (ErrorMacro r)
+  = printMessage (printRange r)
+  $ "Internal error: Invalid module application."
+printInternalError (ErrorModuleName n)
+  = printMessage (T.pack n)
+  $ "Internal error: Empty top-level module name."
+printInternalError (ErrorName r)
+  = printMessage (printRange r)
+  $ "Internal error: Invalid name."
+printInternalError (ErrorRenaming r)
+  = printMessage (printRange r)
+  $ "Internal error: Invalid renaming directive."
+printInternalError (ErrorUnexpected e r)
+  = printMessage (printRange r)
+  $ "Internal error: Unexpected constructor "
+    <> quote (printUnexpectedError e) <> "."
 
 printUnexpectedError
   :: UnexpectedError
@@ -191,10 +216,10 @@
 printUnused
   :: Unused
   -> Maybe Text
-printUnused (Unused is ps)
+printUnused (Unused ps is)
   = printUnusedWith
+    (printUnusedFiles ps)
     (printUnusedItems is)
-    (printUnusedPaths ps)
 
 printUnusedWith
   :: Maybe Text
@@ -207,20 +232,20 @@
 printUnusedWith (Just t1) Nothing
   = Just t1
 printUnusedWith (Just t1) (Just t2)
-  = Just (t2 <> t1)
+  = Just (T.intercalate "\n" [t1, t2])
     
-printUnusedPaths
+printUnusedFiles
   :: [FilePath]
   -> Maybe Text
-printUnusedPaths []
+printUnusedFiles []
   = Nothing
-printUnusedPaths ps@(_ : _)
-  = Just (mconcat (printUnusedPath <$> ps))
+printUnusedFiles ps@(_ : _)
+  = Just (T.intercalate "\n" (printUnusedFile <$> ps))
 
-printUnusedPath
+printUnusedFile
   :: FilePath
   -> Text
-printUnusedPath p
+printUnusedFile p
   = printMessageIndent (T.pack p) "unused file"
 
 -- | Print a collection of unused items.
@@ -230,13 +255,13 @@
 printUnusedItems (UnusedItems [])
   = Nothing
 printUnusedItems (UnusedItems rs@(_ : _))
-  = Just (foldMap (uncurry printRangeInfoWith) rs)
+  = Just (T.intercalate "\n" (uncurry printRangeInfoWith <$> rs))
 
 -- | Print a message indicating that no unused code was found.
 printNothing
   :: Text
 printNothing
-  = T.unlines ["No unused code."]
+  = "No unused code."
 
 printRangeInfoWith
   :: Range
diff --git a/src/Agda/Unused/Types/Access.hs b/src/Agda/Unused/Types/Access.hs
--- a/src/Agda/Unused/Types/Access.hs
+++ b/src/Agda/Unused/Types/Access.hs
@@ -22,6 +22,8 @@
 import qualified Agda.Syntax.Common
   as C
 
+-- ## Definition
+
 -- | An access modifier.
 data Access where
 
@@ -33,6 +35,8 @@
 
   deriving Show
 
+-- ## Interface
+
 -- | Elimination rule for 'Access'.
 access
   :: a
@@ -43,6 +47,8 @@
   = x
 access _ y Public
   = y
+
+-- ## Conversion
 
 -- | Conversion from Agda access type.
 fromAccess
diff --git a/src/Agda/Unused/Types/Context.hs b/src/Agda/Unused/Types/Context.hs
--- a/src/Agda/Unused/Types/Context.hs
+++ b/src/Agda/Unused/Types/Context.hs
@@ -20,7 +20,6 @@
     -- ** Lookup
 
   , LookupError(..)
-  , contextLookup
   , contextLookupItem
   , contextLookupModule
   , accessContextLookup
@@ -30,8 +29,6 @@
   
     -- ** Insert
 
-  , contextInsertRange
-  , contextInsertRangeModule
   , contextInsertRangeAll
   , accessContextInsertRangeAll
 
@@ -40,19 +37,16 @@
   , contextDelete
   , contextDeleteModule
 
-    -- ** Rename
-
-  , contextRename
-  , contextRenameModule
-
     -- ** Define
 
   , accessContextDefine
+  , accessContextDefineFields
 
     -- ** Ranges
 
   , moduleRanges
   , contextRanges
+  , accessContextRanges
 
     -- ** Match
 
@@ -60,11 +54,11 @@
 
     -- * Construction
 
-  , item
-  , itemPattern
-  , itemConstructor
   , contextItem
   , contextModule
+  , accessContextConstructor
+  , accessContextPattern
+  , accessContextField
   , accessContextItem
   , accessContextModule
   , accessContextModule'
@@ -83,8 +77,6 @@
   (Name, QName(..), matchOperators, stripPrefix)
 import Agda.Unused.Types.Range
   (Range)
-import Agda.Unused.Utils
-  (mapUpdateKey)
 
 import Data.Map.Strict
   (Map)
@@ -92,6 +84,10 @@
   as Map
 import Data.Maybe
   (catMaybes)
+import Data.Set
+  (Set)
+import qualified Data.Set
+  as Set
 
 -- ## Definitions
 
@@ -104,22 +100,46 @@
 data Item where
 
   ItemConstructor
-    :: ![Range]
-    -> ![Name]
+    :: !(Set Range)
+    -> !(Set Name)
     -> Item
 
   ItemPattern
-    :: ![Range]
+    :: !(Set Range)
     -> !(Maybe Name)
     -> Item
 
   Item
-    :: ![Range]
+    :: !(Set Range)
     -> !(Maybe Name)
     -> Item
 
   deriving Show
 
+data Defining where
+
+  Defining
+    :: Defining
+
+  NotDefiningField
+    :: Defining
+
+  NotDefining
+    :: Defining
+
+  deriving Show
+
+-- Whether the item represents a constructor or pattern.
+data Special where
+
+  Special
+    :: Special
+
+  NotSpecial
+    :: Special
+
+  deriving Show
+
 -- Like 'Item', but with some additional data:
 --
 -- - Whether the name is public or private.
@@ -130,33 +150,32 @@
 data AccessItem where
 
   AccessItemConstructor
-    -- Private ranges.
-    :: ![Range]
-    -- Public ranges.
-    -> ![Range]
-    -- Private syntax.
-    -> ![Name]
-    -- Public syntax.
-    -> ![Name]
+    :: !(Set Range)
+    -- ^ Private ranges.
+    -> !(Set Range)
+    -- ^ Public ranges.
+    -> !(Set Name)
+    -- ^ Private syntax.
+    -> !(Set Name)
+    -- ^ Public syntax.
     -> AccessItem
 
   AccessItemPattern
     :: !Access
-    -> ![Range]
+    -> !(Set Range)
     -> !(Maybe Name)
     -> AccessItem
 
   AccessItemSyntax
-    -- Whether the item is special.
-    :: !Bool
-    -> ![Range]
+    :: !Defining
+    -> !Special
+    -> !(Set Range)
     -> AccessItem
 
   AccessItem
-    -- Whether we are currently defining this item.
-    :: !Bool
+    :: !Defining
     -> !Access
-    -> ![Range]
+    -> !(Set Range)
     -> !(Maybe Name)
     -> AccessItem
 
@@ -170,7 +189,7 @@
 data Module
   = Module
   { moduleRanges'
-    :: ![Range]
+    :: !(Set Range)
   , moduleContext
     :: !Context
   } deriving Show
@@ -181,7 +200,7 @@
   { accessModuleAccess
     :: !Access
   , accessModuleRanges
-    :: ![Range]
+    :: !(Set Range)
   , accessModuleContext
     :: !Context
   } deriving Show
@@ -238,7 +257,8 @@
   :: AccessItem
   -> AccessItem
   -> AccessItem
-accessItemUnion i@(AccessItem _ Public _ _) (AccessItemConstructor _ [] _ _)
+accessItemUnion i@(AccessItem _ Public _ _) (AccessItemConstructor _ rs _ _)
+  | Set.null rs
   = i
 accessItemUnion i@(AccessItem _ Public _ _) (AccessItem _ Private _ _)
   = i
@@ -306,11 +326,10 @@
 
   deriving Show
 
--- | Get the ranges for the given name, or 'Nothing' if not in context.
 contextLookup
   :: QName
   -> Context
-  -> Maybe [Range]
+  -> Maybe (Set Range)
 contextLookup n c
   = itemRanges <$> contextLookupItem n c
 
@@ -338,7 +357,7 @@
 accessContextLookup
   :: QName
   -> AccessContext
-  -> Either LookupError [Range]
+  -> Either LookupError (Set Range)
 accessContextLookup n c@(AccessContext _ _ is)
   = contextLookup n (toContext' c)
   <|> Map.mapWithKey (accessContextLookupImport n) is
@@ -356,7 +375,7 @@
   :: QName
   -> QName
   -> Context
-  -> Maybe [Range]
+  -> Maybe (Set Range)
 accessContextLookupImport n i c
   = stripPrefix i n >>= flip contextLookup c
 
@@ -366,7 +385,7 @@
   -> Context
   -> Maybe Module
 accessContextLookupModuleImport n i c | n == i
-  = Just (Module [] c)
+  = Just (Module mempty c)
 accessContextLookupModuleImport n i c
   = stripPrefix i n >>= flip contextLookupModule c
 
@@ -390,8 +409,10 @@
 accessItemDefining
   :: AccessItem
   -> Bool
-accessItemDefining (AccessItem b _ _ _)
-  = b
+accessItemDefining (AccessItem Defining _ _ _)
+  = True
+accessItemDefining (AccessItemSyntax Defining _ _)
+  = True
 accessItemDefining _
   = False
 
@@ -400,7 +421,7 @@
 accessContextLookupDefining
   :: QName
   -> AccessContext
-  -> Either LookupError (Bool, [Range])
+  -> Either LookupError (Bool, Set Range)
 accessContextLookupDefining (QName n) (AccessContext is _ _)
   = maybe
     (Left LookupNotFound)
@@ -435,56 +456,38 @@
   -> Item
   -> Item
 itemInsertRange r (ItemConstructor rs ss)
-  = ItemConstructor (r : rs) ss
+  = ItemConstructor (Set.insert r rs) ss
 itemInsertRange r (ItemPattern rs s)
-  = ItemPattern (r : rs) s
+  = ItemPattern (Set.insert r rs) s
 itemInsertRange r (Item rs s)
-  = Item (r : rs) s
+  = Item (Set.insert r rs) s
 
 accessItemInsertRange
   :: Range
   -> AccessItem
   -> AccessItem
-accessItemInsertRange r (AccessItemConstructor rs1 rs2 ns1 ns2)
-  = AccessItemConstructor (r : rs1) (r : rs2) ns1 ns2
-accessItemInsertRange r (AccessItemPattern a rs n)
-  = AccessItemPattern a (r : rs) n
-accessItemInsertRange r (AccessItemSyntax b rs)
-  = AccessItemSyntax b (r : rs)
-accessItemInsertRange r (AccessItem b a rs n)
-  = AccessItem b a (r : rs) n
-
--- | Insert a range for the given name, if present.
-contextInsertRange
-  :: Name
-  -> Range
-  -> Context
-  -> Context
-contextInsertRange n r (Context is ms)
-  = Context (Map.adjust (itemInsertRange r) n is) ms
-
--- | Insert a range for all names in the given module, if present.
-contextInsertRangeModule
-  :: Name
-  -> Range
-  -> Context
-  -> Context
-contextInsertRangeModule n r (Context is ms)
-  = Context is (Map.adjust (moduleInsertRangeAll r) n ms)
+accessItemInsertRange r (AccessItemConstructor rs1 rs2 ss1 ss2)
+  = AccessItemConstructor (Set.insert r rs1) (Set.insert r rs2) ss1 ss2
+accessItemInsertRange r (AccessItemPattern a rs s)
+  = AccessItemPattern a (Set.insert r rs) s
+accessItemInsertRange r (AccessItemSyntax d s rs)
+  = AccessItemSyntax d s (Set.insert r rs)
+accessItemInsertRange r (AccessItem i a rs s)
+  = AccessItem i a (Set.insert r rs) s
 
 moduleInsertRangeAll
   :: Range
   -> Module
   -> Module
 moduleInsertRangeAll r (Module rs c)
-  = Module (r : rs) (contextInsertRangeAll r c)
+  = Module (Set.insert r rs) (contextInsertRangeAll r c)
 
 accessModuleInsertRangeAll
   :: Range
   -> AccessModule
   -> AccessModule
 accessModuleInsertRangeAll r (AccessModule a rs c)
-  = AccessModule a (r : rs) (contextInsertRangeAll r c)
+  = AccessModule a (Set.insert r rs) (contextInsertRangeAll r c)
 
 -- | Insert a range for all names in a context.
 contextInsertRangeAll
@@ -524,36 +527,28 @@
 contextDeleteModule n (Context is ms)
   = Context is (Map.delete n ms)
 
--- ### Rename
-
--- | Rename an item, if present.
-contextRename
-  :: Name
-  -> Name
-  -> Context
-  -> Context
-contextRename n n' (Context is ms)
-  = Context (mapUpdateKey n n' is) ms
-
--- | Rename a module, if present.
-contextRenameModule
-  :: Name
-  -> Name
-  -> Context
-  -> Context
-contextRenameModule n n' (Context is ms)
-  = Context is (mapUpdateKey n n' ms)
-
 -- ### Define
 
 accessItemDefine
   :: AccessItem
   -> AccessItem
 accessItemDefine (AccessItem _ a rs s)
-  = AccessItem True a rs s
+  = AccessItem Defining a rs s
+accessItemDefine (AccessItemSyntax _ s rs)
+  = AccessItemSyntax Defining s rs
 accessItemDefine i
   = i
 
+accessItemDefineField
+  :: AccessItem
+  -> AccessItem
+accessItemDefineField (AccessItem NotDefiningField a rs s)
+  = AccessItem Defining a rs s
+accessItemDefineField (AccessItemSyntax NotDefiningField s rs)
+  = AccessItemSyntax Defining s rs
+accessItemDefineField i
+  = i
+
 -- | Mark an existing name as in process of being defined.
 accessContextDefine
   :: Name
@@ -562,11 +557,18 @@
 accessContextDefine n (AccessContext is ms js)
   = AccessContext (Map.adjust accessItemDefine n is) ms js
 
+-- | Mark all fields as in process of being defined.
+accessContextDefineFields
+  :: AccessContext
+  -> AccessContext
+accessContextDefineFields (AccessContext is ms js)
+  = AccessContext (Map.map accessItemDefineField is) ms js
+
 -- ### Ranges
 
 itemRanges
   :: Item
-  -> [Range]
+  -> Set Range
 itemRanges (ItemConstructor rs _)
   = rs
 itemRanges (ItemPattern rs _)
@@ -576,7 +578,7 @@
 
 accessItemRanges
   :: AccessItem
-  -> [Range]
+  -> Set Range
 accessItemRanges
   = itemRanges . toItem'
 
@@ -584,18 +586,26 @@
 -- associated with the module itself.
 moduleRanges
   :: Module
-  -> [Range]
+  -> Set Range
 moduleRanges (Module rs c)
   = rs <> contextRanges c
 
 -- | Get all ranges associated with names in the given context.
 contextRanges
   :: Context
-  -> [Range]
+  -> Set Range
 contextRanges (Context is ms)
-  = concat (itemRanges <$> Map.elems is)
-  <> concat (moduleRanges <$> Map.elems ms)
+  = mconcat (itemRanges <$> Map.elems is)
+  <> mconcat (moduleRanges <$> Map.elems ms)
 
+-- | Get all ranges associated with names in the given access context.
+accessContextRanges
+  :: AccessContext
+  -> Set Range
+accessContextRanges c@(AccessContext _ _ js)
+  = contextRanges (toContext' c)
+  <> mconcat (contextRanges <$> Map.elems js)
+
 -- ### Match
 
 -- | Find all operators matching the given list of tokens.
@@ -608,32 +618,6 @@
 
 -- ## Construction
 
--- | Construct an 'Item' representing an ordinary definition.
-item
-  :: [Range]
-  -> Maybe Name
-  -> Item
-item
-  = Item
-
--- | Construct an 'Item' representing a pattern synonym.
-itemPattern
-  :: [Range]
-  -> Maybe Name
-  -> Item
-itemPattern
-  = ItemPattern
-
--- | Construct an 'Item' representing a constructor.
-itemConstructor
-  :: [Range]
-  -> Maybe Name
-  -> Item
-itemConstructor rs Nothing
-  = ItemConstructor rs []
-itemConstructor rs (Just s)
-  = ItemConstructor rs [s]
-
 -- | Construct a 'Context' with a single item.
 contextItem
   :: Name
@@ -650,14 +634,54 @@
 contextModule n m
   = Context mempty (Map.singleton n m)
 
--- | Construct an 'AccessContext' with a single item, along with the relevant
--- syntax item if applicable.
+-- | Construct an 'AccessContext' with a single constructor.
+accessContextConstructor
+  :: Name
+  -> Access
+  -> Set Range
+  -> Maybe Name
+  -> AccessContext
+accessContextConstructor n a rs s
+  = accessContextItem' n a (ItemConstructor rs (maybe mempty Set.singleton s))
+
+-- | Construct an 'AccessContext' with a single pattern synonym.
+accessContextPattern
+  :: Name
+  -> Access
+  -> Set Range
+  -> Maybe Name
+  -> AccessContext
+accessContextPattern n a rs s
+  = accessContextItem' n a (ItemPattern rs s)
+
+-- | Construct an 'AccessContext' with a single field.
+accessContextField
+  :: Name
+  -> Access
+  -> Set Range
+  -> Maybe Name
+  -> AccessContext
+accessContextField n a rs s
+  = toFields (accessContextItem' n a (Item rs s))
+
+-- | Construct an 'AccessContext' with a single ordinary definition.
 accessContextItem
   :: Name
   -> Access
+  -> Set Range
+  -> Maybe Name
+  -> AccessContext
+accessContextItem n a rs s
+  = accessContextItem' n a (Item rs s)
+
+-- Construct an 'AccessContext' with a single item, along with the relevant
+-- syntax item if applicable.
+accessContextItem'
+  :: Name
+  -> Access
   -> Item
   -> AccessContext
-accessContextItem n a i
+accessContextItem' n a i
   = fromContext a (contextItem n i)
 
 -- | Construct an 'AccessContext' with a single access module.
@@ -678,7 +702,7 @@
 accessContextModule'
   :: Name
   -> Access
-  -> [Range]
+  -> Set Range
   -> AccessContext
   -> AccessContext
 accessContextModule' n a rs c
@@ -699,28 +723,28 @@
   -> Item
   -> AccessItem
 fromItem Private (ItemConstructor rs ss)
-  = AccessItemConstructor rs [] ss []
+  = AccessItemConstructor rs mempty ss mempty
 fromItem Public (ItemConstructor rs ss)
-  = AccessItemConstructor [] rs [] ss
+  = AccessItemConstructor mempty rs mempty ss
 fromItem a (ItemPattern rs s)
   = AccessItemPattern a rs s
 fromItem a (Item rs s)
-  = AccessItem False a rs s
+  = AccessItem NotDefining a rs s
 
 fromItemSyntax
   :: Item
   -> [(Name, AccessItem)]
 fromItemSyntax (ItemConstructor rs ss)
-  = flip (,) (AccessItemSyntax True rs) <$> ss
+  = flip (,) (AccessItemSyntax NotDefining Special rs) <$> Set.elems ss
 fromItemSyntax (ItemPattern rs s)
-  = flip (,) (AccessItemSyntax True rs) <$> maybe [] (: []) s
+  = flip (,) (AccessItemSyntax NotDefining Special rs) <$> maybe [] (: []) s
 fromItemSyntax (Item rs s)
-  = flip (,) (AccessItemSyntax False rs) <$> maybe [] (: []) s
+  = flip (,) (AccessItemSyntax NotDefining NotSpecial rs) <$> maybe [] (: []) s
 
 toItem
   :: AccessItem
   -> Maybe Item
-toItem (AccessItemConstructor _ rs@(_ : _) _ ss)
+toItem (AccessItemConstructor _ rs _ ss) | not (Set.null rs)
   = Just (ItemConstructor rs ss)
 toItem (AccessItemPattern Public rs s)
   = Just (ItemPattern rs s)
@@ -736,7 +760,7 @@
   = ItemConstructor (rs1 <> rs2) (ss1 <> ss2)
 toItem' (AccessItemPattern _ rs s)
   = ItemPattern rs s
-toItem' (AccessItemSyntax _ rs)
+toItem' (AccessItemSyntax _ _ rs)
   = Item rs Nothing
 toItem' (AccessItem _ _ rs s)
   = Item rs s
@@ -786,4 +810,21 @@
   -> Context
 toContext' (AccessContext is ms _)
   = Context (Map.map toItem' is) (Map.map toModule' ms)
+
+toField
+  :: AccessItem
+  -> AccessItem
+toField (AccessItem _ a rs s)
+  = AccessItem NotDefiningField a rs s
+toField (AccessItemSyntax _ s rs)
+  = AccessItemSyntax NotDefiningField s rs
+toField i
+  = i
+
+-- Convert all ordinary & syntax items to fields.
+toFields
+  :: AccessContext
+  -> AccessContext
+toFields (AccessContext is ms js)
+  = AccessContext (Map.map toField is) ms js
 
diff --git a/src/Agda/Unused/Types/Name.hs b/src/Agda/Unused/Types/Name.hs
--- a/src/Agda/Unused/Types/Name.hs
+++ b/src/Agda/Unused/Types/Name.hs
@@ -14,7 +14,6 @@
     -- * Interface
 
   , nameIds
-  , isBuiltin
   , stripPrefix
 
     -- * Conversion
@@ -24,7 +23,11 @@
   , fromQName
   , fromQNameRange
   , fromAsName
+  , fromModuleName
 
+  , toName
+  , toQName
+
     -- * Paths
 
   , qNamePath
@@ -42,11 +45,11 @@
 import Agda.Syntax.Concrete
   (AsName, AsName'(..))
 import Agda.Syntax.Concrete.Name
-  (NamePart(..))
+  (NameInScope(..), NamePart(..), TopLevelModuleName(..))
 import qualified Agda.Syntax.Concrete.Name
   as N
 import Agda.Syntax.Position
-  (Range)
+  (Range, Range'(..))
 import Data.List
   (isSubsequenceOf)
 import qualified Data.List
@@ -106,15 +109,6 @@
 isOperator (Name (_ : _ : _))
   = True
 
--- | Determine if a module name represents a builtin module.
-isBuiltin
-  :: QName
-  -> Bool
-isBuiltin (Qual (Name [Id "Agda"]) _)
-  = True
-isBuiltin _
-  = False
-
 -- | If the first module name is a prefix of the second module name, then strip
 -- the prefix, otherwise return 'Nothing'.
 stripPrefix
@@ -175,6 +169,46 @@
   = Nothing
 fromAsName (AsName (Right n) _)
   = fromName n
+
+-- | Conversion from Agda top level module name type.
+fromModuleName
+  :: TopLevelModuleName
+  -> Maybe QName
+fromModuleName (TopLevelModuleName _ [])
+  = Nothing
+fromModuleName (TopLevelModuleName _ (n : ns))
+  = Just (fromStrings n ns)
+
+fromStrings
+  :: String
+  -> [String]
+  -> QName
+fromStrings n []
+  = QName (fromString n)
+fromStrings n (n' : ns)
+  = Qual (fromString n) (fromStrings n' ns)
+
+fromString
+  :: String
+  -> Name
+fromString n
+  = Name [Id n]
+
+-- | Conversion to Agda name type.
+toName
+  :: Name
+  -> N.Name
+toName (Name n)
+  = N.Name NoRange NotInScope n
+
+-- | Conversion to Agda qualified name type.
+toQName
+  :: QName
+  -> N.QName
+toQName (QName n)
+  = N.QName (toName n)
+toQName (Qual n ns)
+  = N.Qual (toName n) (toQName ns)
 
 -- ## Paths
 
diff --git a/src/Agda/Unused/Types/Range.hs b/src/Agda/Unused/Types/Range.hs
--- a/src/Agda/Unused/Types/Range.hs
+++ b/src/Agda/Unused/Types/Range.hs
@@ -15,6 +15,7 @@
     -- * Interface
 
   , getRange
+  , rangePath
   , rangeContains
 
   ) where
@@ -24,6 +25,10 @@
 
 import Agda.Syntax.Position
   (PositionWithoutFile, Range, Range'(..), getRange, rEnd', rStart')
+import Agda.Utils.FileName
+  (filePath)
+import qualified Agda.Utils.Maybe.Strict
+  as S
 
 -- ## Definitions
 
@@ -86,13 +91,24 @@
 
 -- ## Interface
 
+-- | Get the file path associated with the given range.
+rangePath
+  :: Range
+  -> Maybe FilePath
+rangePath (Range (S.Just p) _)
+  = Just (filePath p)
+rangePath _
+  = Nothing
+
 -- | Determine whether the first range contains the second.
 rangeContains
   :: Range
   -> Range
   -> Bool
-rangeContains r1 r2
+rangeContains r1@(Range f1 _) r2@(Range f2 _) | f1 == f2
   = rangeContains' (rStart' r1) (rEnd' r1) (rStart' r2) (rEnd' r2)
+rangeContains _ _
+  = False
 
 rangeContains'
   :: Maybe PositionWithoutFile
diff --git a/src/Agda/Unused/Types/Root.hs b/src/Agda/Unused/Types/Root.hs
deleted file mode 100644
--- a/src/Agda/Unused/Types/Root.hs
+++ /dev/null
@@ -1,53 +0,0 @@
-{- |
-Module: Agda.Unused.Types.Root
-
-Data types representing public entry points for an Agda project.
--}
-module Agda.Unused.Types.Root
-
-  ( -- * Types
-
-    Root(..)
-  , Roots(..)
-
-    -- * Construction
-
-  , fromList
-
-  ) where
-
-import Agda.Unused.Types.Name
-  (QName)
-
-import Data.Either
-  (lefts, rights)
-
--- | A public entry point for an Agda project.
-data Root
-  = Root
-  { rootFile
-    :: QName
-    -- ^ A module name.
-  , rootNames
-    :: Maybe [QName]
-    -- ^ Identifier names. An value of 'Nothing' represents all names in scope.
-  } deriving Show
-
--- | A collection of public entry points for an Agda project.
-data Roots
-  = Roots
-  { rootsCheck
-    :: [Root]
-    -- ^ Modules to check.
-  , rootsIgnore
-    :: [QName]
-    -- ^ Modules to ignore.
-  } deriving Show
-
--- | Construct a collection of roots from a list of elements.
-fromList
-  :: [Either QName Root]
-  -> Roots
-fromList rs
-  = Roots (rights rs) (lefts rs)
-
diff --git a/src/Agda/Unused/Utils.hs b/src/Agda/Unused/Utils.hs
--- a/src/Agda/Unused/Utils.hs
+++ b/src/Agda/Unused/Utils.hs
@@ -17,21 +17,12 @@
 
   , stripSuffix
 
-    -- * Map
-
-  , mapDeletes
-  , mapUpdateKey
-
   ) where
 
 import Control.Monad.Except
   (MonadError, throwError)
 import Data.List
   (stripPrefix)
-import Data.Map.Strict
-  (Map)
-import qualified Data.Map.Strict
-  as Map
 
 -- ## Maybe
 
@@ -68,28 +59,4 @@
   -> Maybe [a]
 stripSuffix xs ys
   = reverse <$> stripPrefix (reverse xs) (reverse ys)
-
--- ## Map
-
--- | Delete a list of keys from a map.
-mapDeletes
-  :: Ord k
-  => [k]
-  -> Map k a
-  -> Map k a
-mapDeletes ks xs
-  = foldr Map.delete xs ks
-
--- | Modify a key of a map.
---
--- - If the source key is not present, do nothing.
--- - If the target key is already present, overwrite it.
-mapUpdateKey
-  :: Ord k
-  => k
-  -> k
-  -> Map k a
-  -> Map k a
-mapUpdateKey k k' m
-  = maybe m (\x -> Map.insert k' x (Map.delete k m)) (Map.lookup k m)
 
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,13 +1,15 @@
 module Main where
 
 import Agda.Unused
-  (Unused(..), UnusedItems(..))
+  (UnusedItems(..), UnusedOptions(..))
 import Agda.Unused.Check
-  (checkUnused, checkUnusedLocal)
+  (checkUnused, checkUnusedWith)
 import Agda.Unused.Monad.Error
   (Error)
+import Agda.Unused.Monad.Reader
+  (Mode(..))
 import Agda.Unused.Print
-  (printUnusedItems)
+  (printError, printUnusedItems)
 import Agda.Unused.Types.Access
   (Access(..))
 import Agda.Unused.Types.Name
@@ -16,8 +18,6 @@
   (RangeInfo(..))
 import qualified Agda.Unused.Types.Range
   as R
-import Agda.Unused.Types.Root
-  (Root(..), Roots(..))
 
 import Data.Maybe
   (mapMaybe)
@@ -28,7 +28,7 @@
 import qualified Data.Text
   as T
 import System.FilePath
-  ((</>))
+  ((</>), (<.>))
 import Test.Hspec
   (Expectation, Spec, describe, expectationFailure, hspec, it, shouldBe,
     shouldSatisfy)
@@ -38,52 +38,11 @@
 
 -- ## Names
 
-newtype PrivateName
-  = PrivateName
-  { privateQName
-    :: QName
-  } deriving Show
-
-class IsName a where
-
-  name
-    :: a
-    -> QName
-
-  access
-    :: a
-    -> Access
-
-instance IsName QName where
-
-  name
-    = id
-
-  access _
-    = Public
-
-instance IsName String where
-
-  name n
-    = QName (Name [Id n])
-
-  access _
-    = Public
-
-instance IsName PrivateName where
-
-  name
-    = privateQName
-
-  access _
-    = Private
-
-private
-  :: IsName a
-  => a
-  -> PrivateName
-private n
-  = PrivateName (name n)
+name
+  :: String
+  -> QName
+name n
+  = QName (Name [Id n])
 
 land
   :: QName
@@ -107,6 +66,13 @@
   $ Qual (Name [Id "Builtin"])
   $ QName (Name [Id "Bool"])
 
+agdaBuiltinNat
+  :: QName
+agdaBuiltinNat
+  = Qual (Name [Id "Agda"])
+  $ Qual (Name [Id "Builtin"])
+  $ QName (Name [Id "Nat"])
+
 -- ## Ranges
 
 data RangeType where
@@ -155,75 +121,97 @@
 
   deriving Show
 
+rangeInfo
+  :: QName
+  -> RangeType
+  -> RangeInfo
+rangeInfo n Data
+  = RangeNamed R.RangeData n
+rangeInfo n Definition
+  = RangeNamed R.RangeDefinition n
+rangeInfo n Import
+  = RangeNamed R.RangeImport n
+rangeInfo n ImportItem
+  = RangeNamed R.RangeImportItem n
+rangeInfo n Module
+  = RangeNamed R.RangeModule n
+rangeInfo n ModuleItem
+  = RangeNamed R.RangeModuleItem n
+rangeInfo _ Mutual
+  = RangeMutual
+rangeInfo n Open
+  = RangeNamed R.RangeOpen n
+rangeInfo n OpenItem
+  = RangeNamed R.RangeOpenItem n
+rangeInfo n PatternSynonym
+  = RangeNamed R.RangePatternSynonym n
+rangeInfo n Postulate
+  = RangeNamed R.RangePostulate n
+rangeInfo n Record
+  = RangeNamed R.RangeRecord n
+rangeInfo n RecordConstructor
+  = RangeNamed R.RangeRecordConstructor n
+rangeInfo n Variable
+  = RangeNamed R.RangeVariable n
+
+private
+  :: QName
+  -> (Access, QName)
+private n
+  = (Private, n)
+
+public
+  :: QName
+  -> (Access, QName)
+public n
+  = (Public, n)
+
 (~:)
-  :: IsName a
-  => a
+  :: (Access, QName)
   -> RangeType
   -> (Access, RangeInfo)
-n ~: Data
-  = (access n, RangeNamed R.RangeData (name n))
-n ~: Definition
-  = (access n, RangeNamed R.RangeDefinition (name n))
-n ~: Import
-  = (access n, RangeNamed R.RangeImport (name n))
-n ~: ImportItem
-  = (access n, RangeNamed R.RangeImportItem (name n))
-n ~: Module
-  = (access n, RangeNamed R.RangeModule (name n))
-n ~: ModuleItem
-  = (access n, RangeNamed R.RangeModuleItem (name n))
-n ~: Mutual
-  = (access n, RangeMutual)
-n ~: Open
-  = (access n, RangeNamed R.RangeOpen (name n))
-n ~: OpenItem
-  = (access n, RangeNamed R.RangeOpenItem (name n))
-n ~: PatternSynonym
-  = (access n, RangeNamed R.RangePatternSynonym (name n))
-n ~: Postulate
-  = (access n, RangeNamed R.RangePostulate (name n))
-n ~: Record
-  = (access n, RangeNamed R.RangeRecord (name n))
-n ~: RecordConstructor
-  = (access n, RangeNamed R.RangeRecordConstructor (name n))
-n ~: Variable
-  = (access n, RangeNamed R.RangeVariable (name n))
+(a, n) ~: t
+  = (a, rangeInfo n t)
 
 -- ## Expectations
 
 testCheck
   :: Test
   -> Expectation
-testCheck n = do
-  path
-    <- testPath n
-  unused
-    <- checkUnused path (Roots [Root (name (testModule n)) (Just [])] [])
+testCheck t = do
+  rootPath
+    <- testRootPath t
+  filePath
+    <- testFilePath t
   unusedLocal
-    <- checkUnusedLocal path (name (testModule n))
+    <- checkUnusedWith Local (unusedOptions rootPath) filePath
+  unusedGlobal
+    <- checkUnusedWith Global (unusedOptions rootPath) filePath
   _
-    <- testUnused (unusedItems <$> unused) (snd <$> testResult n)
+    <- testUnused unusedLocal (mapMaybe privateMay (testResult t))
   _
-    <- testUnused unusedLocal (mapMaybe privateMay (testResult n))
+    <- testUnused unusedGlobal (snd <$> testResult t)
   pure ()
 
 testCheckExample
   :: Expectation
 testCheckExample = do
-  path
-    <- getDataFileName "data/test/example"
-  unusedLocal
-    <- checkUnusedLocal path (name "Test")
+  rootPath
+    <- getDataFileName "data/example"
+  filePath
+    <- getDataFileName "data/example/Test.agda"
+  unused
+    <- checkUnused (unusedOptions rootPath) filePath
   _
-    <- testUnusedExample unusedLocal
+    <- testUnusedExample unused
   pure ()
 
 testUnused
   :: Either Error UnusedItems
   -> [RangeInfo]
   -> Expectation
-testUnused (Left _) _
-  = expectationFailure ""
+testUnused (Left e) _
+  = expectationFailure (T.unpack (printError e))
 testUnused (Right (UnusedItems is)) rs
   = Set.fromList (snd <$> is) `shouldBe` Set.fromList rs
 
@@ -239,15 +227,32 @@
   :: Maybe [Text]
   -> Expectation
 testUnusedOutput (Just [t0, t1, t2, t3, t4, t5])
-  = (t0 `shouldSatisfy` T.isSuffixOf (T.pack "/Test.agda:4,23-27"))
-  >> (t1 `shouldBe` T.pack "  unused imported item ‘true’")
-  >> (t2 `shouldSatisfy` T.isSuffixOf (T.pack "/Test.agda:5,1-30"))
-  >> (t3 `shouldBe` T.pack "  unused import ‘Agda.Builtin.Unit’")
-  >> (t4 `shouldSatisfy` T.isSuffixOf (T.pack "/Test.agda:11,9-10"))
-  >> (t5 `shouldBe` T.pack "  unused variable ‘x’")
+  = (t0 `shouldSatisfy` T.isSuffixOf "/Test.agda:4,23-27")
+  >> (t1 `shouldBe` "  unused imported item ‘true’")
+  >> (t2 `shouldSatisfy` T.isSuffixOf "/Test.agda:5,1-30")
+  >> (t3 `shouldBe` "  unused import ‘Agda.Builtin.Unit’")
+  >> (t4 `shouldSatisfy` T.isSuffixOf "/Test.agda:11,9-10")
+  >> (t5 `shouldBe` "  unused variable ‘x’")
 testUnusedOutput _
   = expectationFailure ""
 
+unusedOptions
+  :: FilePath
+  -> UnusedOptions
+unusedOptions p
+  = UnusedOptions
+  { unusedOptionsInclude
+    = [p]
+  , unusedOptionsLibraries
+    = []
+  , unusedOptionsLibrariesFile
+    = Nothing
+  , unusedOptionsUseLibraries
+    = False
+  , unusedOptionsUseDefaultLibraries
+    = False
+  }
+
 privateMay
   :: (Access, a)
   -> Maybe a
@@ -329,9 +334,15 @@
   Data'
     :: DeclarationTest
 
+  DataDef
+    :: DeclarationTest
+
   Record'
     :: DeclarationTest
 
+  RecordDef
+    :: DeclarationTest
+
   Syntax
     :: DeclarationTest
 
@@ -353,9 +364,12 @@
   Postulate'
     :: DeclarationTest
 
-  Open'
+  Open1
     :: DeclarationTest
 
+  Open2
+    :: DeclarationTest
+
   Import'
     :: DeclarationTest
 
@@ -377,302 +391,343 @@
 testDir (Declaration _)
   = "declaration"
 
-testPath
+testRootPath
   :: Test
   -> IO FilePath
-testPath n
-  = getDataFileName ("data/test" </> testDir n)
+testRootPath t
+  = getDataFileName ("data" </> testDir t)
 
-testModule
+testFilePath
   :: Test
+  -> IO FilePath
+testFilePath t
+  = getDataFileName ("data" </> testDir t </> testFileName t <.> "agda")
+
+testFileName
+  :: Test
   -> String
-testModule (Pattern IdentP)
+testFileName (Pattern IdentP)
   = "IdentP"
-testModule (Pattern OpAppP)
+testFileName (Pattern OpAppP)
   = "OpAppP"
-testModule (Pattern AsP)
+testFileName (Pattern AsP)
   = "AsP"
-testModule (Expression WithApp)
+testFileName (Expression WithApp)
   = "WithApp"
-testModule (Expression Lam)
+testFileName (Expression Lam)
   = "Lam"
-testModule (Expression ExtendedLam)
+testFileName (Expression ExtendedLam)
   = "ExtendedLam"
-testModule (Expression Pi)
+testFileName (Expression Pi)
   = "Pi"
-testModule (Expression Let)
+testFileName (Expression Let)
   = "Let"
-testModule (Expression DoBlock1)
+testFileName (Expression DoBlock1)
   = "DoBlock1"
-testModule (Expression DoBlock2)
+testFileName (Expression DoBlock2)
   = "DoBlock2"
-testModule (Expression DoBlock3)
+testFileName (Expression DoBlock3)
   = "DoBlock3"
-testModule (Expression DoBlock4)
+testFileName (Expression DoBlock4)
   = "DoBlock4"
-testModule (Declaration TypeSig)
+testFileName (Declaration TypeSig)
   = "TypeSig"
-testModule (Declaration FunClause)
+testFileName (Declaration FunClause)
   = "FunClause"
-testModule (Declaration Data')
+testFileName (Declaration Data')
   = "Data"
-testModule (Declaration Record')
+testFileName (Declaration DataDef)
+  = "DataDef"
+testFileName (Declaration Record')
   = "Record"
-testModule (Declaration Syntax)
+testFileName (Declaration RecordDef)
+  = "RecordDef"
+testFileName (Declaration Syntax)
   = "Syntax"
-testModule (Declaration PatternSyn)
+testFileName (Declaration PatternSyn)
   = "PatternSyn"
-testModule (Declaration Mutual1)
+testFileName (Declaration Mutual1)
   = "Mutual1"
-testModule (Declaration Mutual2)
+testFileName (Declaration Mutual2)
   = "Mutual2"
-testModule (Declaration Abstract)
+testFileName (Declaration Abstract)
   = "Abstract"
-testModule (Declaration Private')
+testFileName (Declaration Private')
   = "Private"
-testModule (Declaration Postulate')
+testFileName (Declaration Postulate')
   = "Postulate"
-testModule (Declaration Open')
-  = "Open"
-testModule (Declaration Import')
+testFileName (Declaration Open1)
+  = "Open1"
+testFileName (Declaration Open2)
+  = "Open2"
+testFileName (Declaration Import')
   = "Import"
-testModule (Declaration ModuleMacro)
+testFileName (Declaration ModuleMacro)
   = "ModuleMacro"
-testModule (Declaration Module')
+testFileName (Declaration Module')
   = "Module"
 
 testResult
   :: Test
   -> [(Access, RangeInfo)]
-testResult n
-  = case n of
+testResult t
+  = case t of
 
   Pattern IdentP ->
-    [ private "y"
+    [ private (name "y")
       ~: Variable
-    , "f"
+    , public (name "f")
       ~: Definition
-    , "g"
+    , public (name "g")
       ~: Definition
     ]
 
   Pattern OpAppP ->
-    [ land
+    [ public land
       ~: Definition
     ]
 
   Pattern AsP ->
-    [ private "y"
+    [ private (name "y")
       ~: Variable
-    , private "z"
+    , private (name "z")
       ~: Variable
-    , private "w"
+    , private (name "w")
       ~: Variable
-    , private "z'"
+    , private (name "z'")
       ~: Variable
-    , private "w'"
+    , private (name "w'")
       ~: Variable
-    , "f"
+    , public (name "f")
       ~: Definition
-    , "g"
+    , public (name "g")
       ~: Definition
     ]
 
   Expression WithApp ->
-    [ "f"
+    [ public (name "f")
       ~: Definition
-    , "g"
+    , public (name "g")
       ~: Definition
     ]
 
   Expression Lam ->
-    [ private "y"
+    [ private (name "y")
       ~: Variable
-    , private "y'"
+    , private (name "y'")
       ~: Variable
-    , "f"
+    , public (name "f")
       ~: Definition
-    , "g"
+    , public (name "g")
       ~: Definition
     ]
 
   Expression ExtendedLam ->
-    [ private "x"
+    [ private (name "x")
       ~: Variable
-    , "f"
+    , public (name "f")
       ~: Definition
     ]
 
   Expression Pi ->
-    [ private "y"
+    [ private (name "y")
       ~: Variable
-    , private "w"
+    , private (name "w")
       ~: Variable
-    , "f"
+    , public (name "f")
       ~: Definition
     ]
 
   Expression Let ->
-    [ private "z"
+    [ private (name "z")
       ~: Definition
-    , "f"
+    , public (name "f")
       ~: Definition
     ]
 
   Expression DoBlock1 ->
-    [ private "z"
+    [ private (name "z")
       ~: Variable
-    , "f"
+    , public (name "f")
       ~: Definition
     ]
 
   Expression DoBlock2 ->
-    [ bind_
+    [ public bind_
       ~: Definition
-    , "f"
+    , public (name "f")
       ~: Definition
     ]
 
   Expression DoBlock3 ->
-    [ bind
+    [ public bind
       ~: Definition
-    , "f"
+    , public (name "f")
       ~: Definition
     ]
 
   Expression DoBlock4 ->
-    [ bind
+    [ public bind
       ~: Definition
-    , bind_
+    , public bind_
       ~: Definition
-    , "f"
+    , public (name "f")
       ~: Definition
     ]
 
   Declaration TypeSig ->
-    [ "g"
+    [ public (name "g")
       ~: Definition
-    , "h"
+    , public (name "h")
       ~: Definition
     ]
 
   Declaration FunClause ->
-    [ private "z"
+    [ private (name "z")
       ~: Definition
-    , "f"
+    , public (name "f")
       ~: Definition
-    , "snoc"
+    , public (name "snoc")
       ~: Definition
     ]
 
   Declaration Data' ->
-    [ "D"
+    [ public (name "E")
       ~: Data
+    , public (name "_")
+      ~: Mutual
     ]
 
+  Declaration DataDef ->
+    [ private (name "z")
+      ~: Variable
+    , public (name "d")
+      ~: Postulate
+    ]
+
   Declaration Record' ->
-    [ "B"
+    [ public (name "B")
       ~: Record
-    , "c"
+    , public (name "D")
+      ~: Record
+    , public (name "F")
+      ~: Record
+    , public (name "c")
       ~: RecordConstructor
-    , "x"
+    , public (name "x")
       ~: Definition
-    , "y"
+    , public (name "y")
       ~: Definition
     ]
 
+  Declaration RecordDef ->
+    [ private (name "z")
+      ~: Variable
+    , public (name "r")
+      ~: Postulate
+    ]
+
   Declaration Syntax ->
-    [ "p1"
+    [ public (name "p1")
       ~: Postulate
-    , "p1'"
+    , public (name "p1'")
       ~: Postulate
     ]
 
   Declaration PatternSyn ->
-    [ "q"
+    [ public (name "q")
       ~: PatternSynonym
-    , "f"
+    , public (name "f")
       ~: Definition
-    , "g"
+    , public (name "g")
       ~: Definition
     ]
 
   Declaration Mutual1 ->
-    [ "_"
+    [ public (name "_")
       ~: Mutual
     ]
 
   Declaration Mutual2 ->
-    [ "is-even'"
+    [ public (name "is-even'")
       ~: Definition
     ]
 
   Declaration Abstract ->
-    [ "g"
+    [ public (name "g")
       ~: Definition
-    , "h"
+    , public (name "h")
       ~: Definition
     ]
 
   Declaration Private' ->
-    [ private "g"
+    [ private (name "g")
       ~: Definition
-    , private "h"
+    , private (name "h")
       ~: Definition
     ]
 
   Declaration Postulate' ->
-    [ "g"
+    [ public (name "g")
       ~: Postulate
-    , "h"
+    , public (name "h")
       ~: Definition
     ]
 
-  Declaration Open' ->
-    [ private "N"
+  Declaration Open1 ->
+    [ private (name "N")
       ~: Open
-    , private "P"
+    , private (name "P")
       ~: Open
-    , "Q"
+    , public (name "Q")
       ~: Module
-    , private "x'"
+    , private (name "x'")
       ~: OpenItem
-    , "v"
+    , public (name "v")
       ~: Definition
-    , "y"
+    , public (name "y")
       ~: Definition
     ]
 
+  Declaration Open2 ->
+    [ public (name "z")
+      ~: OpenItem
+    , public (name "p")
+      ~: Postulate
+    ]
+
   Declaration Import' ->
     [ private agdaBuiltinBool
       ~: Import
-    , private "tt"
+    , private agdaBuiltinNat
+      ~: Import
+    , private (name "tt")
       ~: ImportItem
-    , "A"
+    , public (name "A")
       ~: Definition
     ]
 
   Declaration ModuleMacro ->
-    [ private "x"
+    [ private (name "x")
       ~: Variable
-    , "Q"
+    , public (name "Q")
       ~: Module
-    , "A'"
+    , public (name "A'")
       ~: ModuleItem
-    , "C"
+    , public (name "C")
       ~: Definition
-    , "D"
+    , public (name "D")
       ~: Definition
-    , "y"
+    , public (name "y")
       ~: Definition
     ]
 
   Declaration Module' ->
-    [ "O"
+    [ public (name "O")
       ~: Module
-    , "P"
+    , public (name "P")
       ~: Module
-    , "x"
+    , public (name "x")
       ~: Definition
     ]
 
@@ -733,8 +788,12 @@
     (testCheck (Declaration FunClause))
   >> it "checks data declarations (Data)"
     (testCheck (Declaration Data'))
+  >> it "checks data definitions (DataDef)"
+    (testCheck (Declaration DataDef))
   >> it "checks record declarations (Record)"
     (testCheck (Declaration Record'))
+  >> it "checks record definitions (RecordDef)"
+    (testCheck (Declaration RecordDef))
   >> it "checks syntax declarations (Syntax)"
     (testCheck (Declaration Syntax))
   >> it "checks pattern synonyms (PatternSyn)"
@@ -749,7 +808,8 @@
   >> it "checks postulates (Postulate)"
     (testCheck (Declaration Postulate'))
   >> it "checks open statements (Open)"
-    (testCheck (Declaration Open'))
+    (testCheck (Declaration Open1)
+    >> testCheck (Declaration Open2))
   >> it "checks import statements (Import)"
     (testCheck (Declaration Import'))
   >> it "checks module macros (ModuleMacro)"