agda-unused 0.1.0 → 0.2.0

raw patch · 111 files changed

+2549/−3357 lines, 111 filesdep −megaparsecdep ~aesondep ~basedep ~optparse-applicativePVP ok

version bump matches the API change (PVP)

Dependencies removed: megaparsec

Dependency ranges changed: aeson, base, optparse-applicative

API changes (from Hackage documentation)

Files

• CHANGELOG.md +14/−1
• README.md +63/−68
• agda-unused.cabal +7/−16
• app/Main.hs +190/−184
• data/Agda/Builtin/Bool.agda +0/−17
• data/Agda/Builtin/Char.agda +0/−18
• data/Agda/Builtin/Char/Properties.agda +0/−11
• data/Agda/Builtin/Coinduction.agda +0/−15
• data/Agda/Builtin/Cubical/Glue.agda +0/−123
• data/Agda/Builtin/Cubical/HCompU.agda +0/−73
• data/Agda/Builtin/Cubical/Id.agda +0/−32
• data/Agda/Builtin/Cubical/Path.agda +0/−20
• data/Agda/Builtin/Cubical/Sub.agda +0/−16
• data/Agda/Builtin/Equality.agda +0/−10
• data/Agda/Builtin/Equality/Erase.agda +0/−8
• data/Agda/Builtin/Equality/Rewrite.agda +0/−8
• data/Agda/Builtin/Float.agda +0/−40
• data/Agda/Builtin/Float/Properties.agda +0/−11
• data/Agda/Builtin/FromNat.agda +0/−17
• data/Agda/Builtin/FromNeg.agda +0/−17
• data/Agda/Builtin/FromString.agda +0/−17
• data/Agda/Builtin/IO.agda +0/−11
• data/Agda/Builtin/Int.agda +0/−19
• data/Agda/Builtin/List.agda +0/−18
• data/Agda/Builtin/Nat.agda +0/−134
• data/Agda/Builtin/Reflection.agda +0/−314
• data/Agda/Builtin/Reflection/Properties.agda +0/−12
• data/Agda/Builtin/Sigma.agda +0/−18
• data/Agda/Builtin/Size.agda +0/−21
• data/Agda/Builtin/Strict.agda +0/−10
• data/Agda/Builtin/String.agda +0/−28
• data/Agda/Builtin/String/Properties.agda +0/−11
• data/Agda/Builtin/TrustMe.agda +0/−15
• data/Agda/Builtin/Unit.agda +0/−10
• data/Agda/Builtin/Word.agda +0/−13
• data/Agda/Builtin/Word/Properties.agda +0/−11
• data/Agda/Primitive.agda +0/−33
• data/Agda/Primitive/Cubical.agda +0/−53
• data/declaration/Abstract.agda +32/−0
• data/declaration/Data.agda +17/−0
• data/declaration/DataDef.agda +29/−0
• data/declaration/FunClause.agda +35/−0
• data/declaration/Import.agda +14/−0
• data/declaration/Module.agda +25/−0
• data/declaration/ModuleMacro.agda +57/−0
• data/declaration/Mutual1.agda +41/−0
• data/declaration/Mutual2.agda +47/−0
• data/declaration/Open1.agda +59/−0
• data/declaration/Open2.agda +54/−0
• data/declaration/PatternSyn.agda +41/−0
• data/declaration/Postulate.agda +21/−0
• data/declaration/Private.agda +32/−0
• data/declaration/Record.agda +53/−0
• data/declaration/RecordDef.agda +29/−0
• data/declaration/Syntax.agda +49/−0
• data/declaration/TypeSig.agda +30/−0
• data/example/Test.agda +14/−0
• data/expression/DoBlock1.agda +38/−0
• data/expression/DoBlock2.agda +36/−0
• data/expression/DoBlock3.agda +36/−0
• data/expression/DoBlock4.agda +35/−0
• data/expression/ExtendedLam.agda +23/−0
• data/expression/Lam.agda +16/−0
• data/expression/Let.agda +12/−0
• data/expression/Pi.agda +14/−0
• data/expression/WithApp.agda +23/−0
• data/pattern/AsP.agda +20/−0
• data/pattern/IdentP.agda +28/−0
• data/pattern/OpAppP.agda +21/−0
• data/test/declaration/Abstract.agda +0/−32
• data/test/declaration/Data.agda +0/−12
• data/test/declaration/FunClause.agda +0/−35
• data/test/declaration/Import.agda +0/−11
• data/test/declaration/Module.agda +0/−25
• data/test/declaration/ModuleMacro.agda +0/−57
• data/test/declaration/Mutual1.agda +0/−41
• data/test/declaration/Mutual2.agda +0/−47
• data/test/declaration/Open.agda +0/−59
• data/test/declaration/PatternSyn.agda +0/−41
• data/test/declaration/Postulate.agda +0/−21
• data/test/declaration/Private.agda +0/−32
• data/test/declaration/Record.agda +0/−36
• data/test/declaration/Syntax.agda +0/−49
• data/test/declaration/TypeSig.agda +0/−30
• data/test/example/Test.agda +0/−14
• data/test/expression/DoBlock1.agda +0/−38
• data/test/expression/DoBlock2.agda +0/−36
• data/test/expression/DoBlock3.agda +0/−36
• data/test/expression/DoBlock4.agda +0/−35
• data/test/expression/ExtendedLam.agda +0/−23
• data/test/expression/Lam.agda +0/−16
• data/test/expression/Let.agda +0/−12
• data/test/expression/Pi.agda +0/−14
• data/test/expression/WithApp.agda +0/−23
• data/test/pattern/AsP.agda +0/−20
• data/test/pattern/IdentP.agda +0/−28
• data/test/pattern/OpAppP.agda +0/−21
• src/Agda/Unused.hs +22/−3
• src/Agda/Unused/Check.hs +474/−361
• src/Agda/Unused/Monad/Error.hs +34/−11
• src/Agda/Unused/Monad/Reader.hs +81/−12
• src/Agda/Unused/Monad/State.hs +100/−36
• src/Agda/Unused/Parse.hs +0/−150
• src/Agda/Unused/Print.hs +61/−36
• src/Agda/Unused/Types/Access.hs +6/−0
• src/Agda/Unused/Types/Context.hs +180/−139
• src/Agda/Unused/Types/Name.hs +46/−12
• src/Agda/Unused/Types/Range.hs +17/−1
• src/Agda/Unused/Types/Root.hs +0/−53
• src/Agda/Unused/Utils.hs +0/−33
• test/Main.hs +273/−213

@@ -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). 

@@ -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. 

@@ -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 

@@ -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 

@@ -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  #-}

@@ -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

@@ -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

@@ -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     ♭  #-}

@@ -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

@@ -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 #-}

@@ -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

@@ -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         _≡_     #-}

@@ -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

@@ -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 _≡_ #-}

@@ -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

@@ -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 _≡_ #-}

@@ -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

@@ -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

@@ -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 #-}

@@ -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 #-}

@@ -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 #-}

@@ -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 #-}

@@ -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

@@ -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); }; } #-}

@@ -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.

@@ -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             #-}

@@ -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

@@ -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 Σ #-}

@@ -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 _⊔ˢ_   = \_ _ -> ()  #-}

@@ -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

@@ -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); } #-}

@@ -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

@@ -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 #-}

@@ -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 () (()) #-}

@@ -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

@@ -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

@@ -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ω #-}

@@ -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

@@ -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+

@@ -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+

@@ -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+

@@ -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)+

@@ -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.⊤+

@@ -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+

@@ -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'+

@@ -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+

@@ -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+

@@ -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''+

@@ -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+

@@ -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+

@@ -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+

@@ -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+

@@ -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+

@@ -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+

@@ -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₁+  

@@ -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+

@@ -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

@@ -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+

@@ -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+

@@ -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+

@@ -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+

@@ -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+  }+

@@ -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+

@@ -0,0 +1,12 @@+module Let where++f+  : {A : Set}+  → A+  → A+f x+  = let+      y = x+      z = x+    in y+

@@ -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+

@@ -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+

@@ -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+

@@ -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+

@@ -0,0 +1,21 @@+module OpAppP where++data Bool+  : Set+  where++  false+    : Bool++  true+    : Bool++_&&_+  : Bool+  → Bool+  → Bool+false && _+  = false+true && b+  = b+

@@ -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-

@@ -1,12 +0,0 @@-module Data where--data D-  (A : Set)-  : Set--data D A-  where--  c-    : D A-

@@ -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)-

@@ -1,11 +0,0 @@-module Import where--import Agda.Builtin.Unit-  using (⊤; tt)-import Agda.Builtin.Bool--A-  : Set-A-  = Agda.Builtin.Unit.⊤-

@@ -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-

@@ -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'-

@@ -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-

@@ -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-

@@ -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''-

@@ -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-

@@ -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-

@@ -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-

@@ -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 {}-

@@ -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₁-  

@@ -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-

@@ -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

@@ -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-

@@ -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-

@@ -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-

@@ -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-

@@ -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-  }-

@@ -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-

@@ -1,12 +0,0 @@-module Let where--f-  : {A : Set}-  → A-  → A-f x-  = let-      y = x-      z = x-    in y-

@@ -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-

@@ -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-

@@ -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-

@@ -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-

@@ -1,21 +0,0 @@-module OpAppP where--data Bool-  : Set-  where--  false-    : Bool--  true-    : Bool--_&&_-  : Bool-  → Bool-  → Bool-false && _-  = false-true && b-  = b-

@@ -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 

@@ -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 

@@ -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

@@ -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 

@@ -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) 

@@ -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"-

@@ -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

@@ -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

@@ -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 

@@ -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 

@@ -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

@@ -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)-

@@ -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) 

@@ -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)"