packages feed

agda-unused (empty) → 0.1.0

raw patch · 81 files changed

+7552/−0 lines, 81 filesdep +Agdadep +aesondep +agda-unused

Dependencies added: Agda, aeson, agda-unused, base, containers, directory, filepath, hspec, megaparsec, mtl, optparse-applicative, text

Files

+ CHANGELOG.md view
@@ -0,0 +1,6 @@+# Changelog++## 0.1.0 (10/27/2020)++Initial release.+
+ LICENSE view
@@ -0,0 +1,19 @@+Copyright 2020 Matt Superdock++Permission is hereby granted, free of charge, to any person obtaining a copy of+this software and associated documentation files (the "Software"), to deal in+the Software without restriction, including without limitation the rights to+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of+the Software, and to permit persons to whom the Software is furnished to do so,+subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS+FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR+COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER+IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN+CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.+
+ README.md view
@@ -0,0 +1,155 @@+# agda-unused++`agda-unused` checks for unused code in an Agda project, including:++- variables+- definitions+- postulates+- data & record types+- `import` statements+- `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.++## Example++File `~/Test.agda`:++```+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+```++Command:++```+$ agda-unused --local Test.agda+```++Output:++```+/home/user/Test.agda:4,23-27+  unused imported item ‘true’+/home/user/Test.agda:5,1-30+  unused import ‘Agda.Builtin.Unit’+/home/user/Test.agda:11,9-10+  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.++All given module names in parentheses are ignored when checking for unused+files. Such modules may still be checked if imported by another module.++Example `.agda-roots` file:++```+Main+- main++Pythagorean.Core+- isTriple+- allTriples++(Pythagorean.Examples)++Pythagorean.Theorems++Pythagorean.Utils+- Print.prettyNat+```++Spacing and indentation are irrelevant.++## Usage++```+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 +```++The project root directory is determined as follows:++- 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.++## Approach++We make a single pass through each relevant Agda file:++- When a new item (variable, definition, etc.) appears, we mark it unused.+- When an existing item appears, we mark it used.++This means, for example, if we have three definitions (say `f`, `g`, `h`), each+depending on the previous one, where `h` is not a root, then `f` and `g` are+considered used, while `h` is considered unused. If we remove `h` and run+`agda-unsed` again, it will now report that `g` is unused. This behavior is+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`.++The `"none"` type indicates that there is no unused code.++## Limitations++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)++`agda-unused` will produce an error if your code uses these language features.+
+ agda-unused.cabal view
@@ -0,0 +1,123 @@+cabal-version: 3.0++name:+  agda-unused+version:+  0.1.0+build-type:+  Simple+license:+  MIT+license-file:+  LICENSE+maintainer:+  Matt Superdock <msuperdock@gmail.com>+synopsis:+  Check for unused code in an Agda project.+description:+  A tool to check for unused code in an Agda project.+category:+  Dependent types+data-files:+  data/**/*.agda+extra-source-files:+  CHANGELOG.md+  README.md++source-repository head+  type:+    git+  location:+    https://github.com/msuperdock/agda-unused.git++library+  hs-source-dirs:+    src+  exposed-modules:+    Agda.Unused+    Agda.Unused.Check+    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,+    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:+    Haskell2010+  default-extensions:+    FlexibleContexts,+    FlexibleInstances,+    GADTs,+    OverloadedStrings+  ghc-options:+    -Wall+    -Wno-orphans++executable agda-unused+  hs-source-dirs:+    app+  main-is:+    Main.hs+  build-depends:+    agda-unused,+    base >= 4.13.0 && < 4.14,+    aeson >= 1.4.7 && < 1.5,+    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,+    text >= 1.2.4 && < 1.3+  default-language:+    Haskell2010+  default-extensions:+    FlexibleContexts,+    GADTs,+    OverloadedStrings+  ghc-options:+    -Wall++test-suite test+  type:+    exitcode-stdio-1.0+  hs-source-dirs:+    test+  main-is:+    Main.hs+  other-modules:+    Paths_agda_unused+  autogen-modules:+    Paths_agda_unused+  build-depends:+    agda-unused,+    base >= 4.13.0 && < 4.14,+    containers >= 0.6.2 && < 0.7,+    filepath >= 1.4.2 && < 1.5,+    hspec >= 2.7.1 && < 2.8,+    text >= 1.2.4 && < 1.3+  default-language:+    Haskell2010+  default-extensions:+    FlexibleInstances,+    GADTs,+    TypeSynonymInstances+  ghc-options:+    -Wall+
+ app/Main.hs view
@@ -0,0 +1,290 @@+module Main where++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)++import Control.Monad.Except+  (MonadError, liftEither, 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+  as T+import qualified Data.Text.IO+  as I+import Data.Text.Lazy+  (toStrict)+import Options.Applicative+  (InfoMod, Parser, ParserInfo, execParser, fullDesc, header, help, helper,+    info, long, metavar, optional, progDesc, short, strOption, switch)+import System.Directory+  (doesFileExist, getCurrentDirectory, makeAbsolute)+import System.Exit+  (exitFailure, exitSuccess)+import System.FilePath+  ((</>), splitDirectories, stripExtension, takeDirectory)+import System.IO+  (stderr)++-- ## Options++data Options+  = Options+  { optionsRoot+    :: !(Maybe FilePath)+    -- ^ The project root path.+  , optionsFile+    :: !(Maybe FilePath)+    -- ^ A file path to check locally.+  , optionsJSON+    :: !Bool+    -- ^ Whether to output JSON.+  } deriving Show++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")+  <*> (switch+    $ short 'j'+    <> long "json"+    <> help "Format output as JSON")++optionsInfo+  :: InfoMod a+optionsInfo+  = fullDesc+  <> progDesc "Check for unused code in project with root directory ROOT"+  <> header "agda-unused - check for unused code in an Agda project"++options+  :: ParserInfo Options+options+  = info (helper <*> optionsParser) optionsInfo++-- ## Errors++data Error where+ +  ErrorFile+    :: !FilePath+    -> Error++  ErrorLocal+    :: !FilePath+    -> Error++  ErrorParse+    :: !Text+    -> Error++  deriving Show++-- ## Check++check+  :: Options+  -> IO ()+check o@(Options _ _ j)+  = runExceptT (check' o)+  >>= either (printErrorWith j) (const (pure ()))++check'+  :: MonadError Error m+  => MonadIO m+  => Options+  -> m ()++check' o@(Options _ Nothing j) = do+  rootPath+    <- liftIO (getRootDirectory o)+  configPath+    <- pure (rootPath </> ".agda-roots")+  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 (printResult j P.printUnused checkResult)+  pure ()++check' o@(Options _ (Just f) j) = do+  rootPath+    <- liftIO (getRootDirectory o)+  rootPath'+    <- pure (splitDirectories rootPath)+  filePath+    <- liftIO (makeAbsolute f >>= \f' -> pure (splitDirectories f'))+  localModule+    <- liftMaybe (ErrorLocal f) (stripPrefix rootPath' filePath >>= pathModule)+  checkResult+    <- liftIO (checkUnusedLocal rootPath localModule)+  _+    <- liftIO (printResult j P.printUnusedItems checkResult)+  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]++-- ## Print++printResult+  :: Bool+  -- ^ Whether to output JSON.+  -> (a -> Maybe Text)+  -> Either E.Error a+  -> IO ()+printResult False _ (Left e)+  = I.hPutStrLn stderr (P.printError e) >> exitFailure+printResult False p (Right x)+  = I.putStrLn (maybe P.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+  -> Value+printResultJSON _ (Left e)+  = encodeMessage "error" (P.printError e)+printResultJSON p (Right u)+  = maybe (encodeMessage "none" P.printNothing) (encodeMessage "unused") (p u)++encodeMessage+  :: Text+  -- ^ Type of message.+  -> Text+  -- ^ 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)++-- ## Main++main+  :: IO ()+main+  = execParser options+  >>= check+
+ data/Agda/Builtin/Bool.agda view
@@ -0,0 +1,17 @@+{-# 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  #-}
+ data/Agda/Builtin/Char.agda view
@@ -0,0 +1,18 @@+{-# 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
+ data/Agda/Builtin/Char/Properties.agda view
@@ -0,0 +1,11 @@+{-# 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
+ data/Agda/Builtin/Coinduction.agda view
@@ -0,0 +1,15 @@+{-# 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     ♭  #-}
+ data/Agda/Builtin/Cubical/Glue.agda view
@@ -0,0 +1,123 @@+{-# 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
+ data/Agda/Builtin/Cubical/HCompU.agda view
@@ -0,0 +1,73 @@+{-# 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 #-}
+ data/Agda/Builtin/Cubical/Id.agda view
@@ -0,0 +1,32 @@+{-# 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
+ data/Agda/Builtin/Cubical/Path.agda view
@@ -0,0 +1,20 @@+{-# 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         _≡_     #-}
+ data/Agda/Builtin/Cubical/Sub.agda view
@@ -0,0 +1,16 @@+{-# 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
+ data/Agda/Builtin/Equality.agda view
@@ -0,0 +1,10 @@+{-# 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 _≡_ #-}
+ data/Agda/Builtin/Equality/Erase.agda view
@@ -0,0 +1,8 @@+{-# 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
+ data/Agda/Builtin/Equality/Rewrite.agda view
@@ -0,0 +1,8 @@+{-# OPTIONS --without-K --rewriting --no-sized-types --no-guardedness+            --no-subtyping #-}++module Agda.Builtin.Equality.Rewrite where++open import Agda.Builtin.Equality++{-# BUILTIN REWRITE _≡_ #-}
+ data/Agda/Builtin/Float.agda view
@@ -0,0 +1,40 @@+{-# 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
+ data/Agda/Builtin/Float/Properties.agda view
@@ -0,0 +1,11 @@+{-# 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
+ data/Agda/Builtin/FromNat.agda view
@@ -0,0 +1,17 @@+{-# 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 #-}
+ data/Agda/Builtin/FromNeg.agda view
@@ -0,0 +1,17 @@+{-# 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 #-}
+ data/Agda/Builtin/FromString.agda view
@@ -0,0 +1,17 @@+{-# 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 #-}
+ data/Agda/Builtin/IO.agda view
@@ -0,0 +1,11 @@+{-# 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 #-}
+ data/Agda/Builtin/Int.agda view
@@ -0,0 +1,19 @@+{-# 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
+ data/Agda/Builtin/List.agda view
@@ -0,0 +1,18 @@+{-# 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); }; } #-}
+ data/Agda/Builtin/Nat.agda view
@@ -0,0 +1,134 @@+{-# 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.
+ data/Agda/Builtin/Reflection.agda view
@@ -0,0 +1,314 @@+{-# 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             #-}
+ data/Agda/Builtin/Reflection/Properties.agda view
@@ -0,0 +1,12 @@+{-# 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
+ data/Agda/Builtin/Sigma.agda view
@@ -0,0 +1,18 @@+{-# 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 Σ #-}
+ data/Agda/Builtin/Size.agda view
@@ -0,0 +1,21 @@+{-# 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 _⊔ˢ_   = \_ _ -> ()  #-}
+ data/Agda/Builtin/Strict.agda view
@@ -0,0 +1,10 @@+{-# 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
+ data/Agda/Builtin/String.agda view
@@ -0,0 +1,28 @@+{-# 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); } #-}
+ data/Agda/Builtin/String/Properties.agda view
@@ -0,0 +1,11 @@+{-# 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
+ data/Agda/Builtin/TrustMe.agda view
@@ -0,0 +1,15 @@+{-# 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 #-}
+ data/Agda/Builtin/Unit.agda view
@@ -0,0 +1,10 @@+{-# 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 () (()) #-}
+ data/Agda/Builtin/Word.agda view
@@ -0,0 +1,13 @@+{-# 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
+ data/Agda/Builtin/Word/Properties.agda view
@@ -0,0 +1,11 @@+{-# 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
+ data/Agda/Primitive.agda view
@@ -0,0 +1,33 @@+-- 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ω #-}
+ data/Agda/Primitive/Cubical.agda view
@@ -0,0 +1,53 @@+{-# 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
+ data/test/declaration/Abstract.agda view
@@ -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+
+ data/test/declaration/Data.agda view
@@ -0,0 +1,12 @@+module Data where++data D+  (A : Set)+  : Set++data D A+  where++  c+    : D A+
+ data/test/declaration/FunClause.agda view
@@ -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)+
+ data/test/declaration/Import.agda view
@@ -0,0 +1,11 @@+module Import where++import Agda.Builtin.Unit+  using (⊤; tt)+import Agda.Builtin.Bool++A+  : Set+A+  = Agda.Builtin.Unit.⊤+
+ data/test/declaration/Module.agda view
@@ -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+
+ data/test/declaration/ModuleMacro.agda view
@@ -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'+
+ data/test/declaration/Mutual1.agda view
@@ -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+
+ data/test/declaration/Mutual2.agda view
@@ -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+
+ data/test/declaration/Open.agda view
@@ -0,0 +1,59 @@+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''+
+ data/test/declaration/PatternSyn.agda view
@@ -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+
+ data/test/declaration/Postulate.agda view
@@ -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+
+ data/test/declaration/Private.agda view
@@ -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+
+ data/test/declaration/Record.agda view
@@ -0,0 +1,36 @@+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 {}+
+ data/test/declaration/Syntax.agda view
@@ -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₁+
+ data/test/declaration/TypeSig.agda view
@@ -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+
+ data/test/example/Test.agda view
@@ -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
+ data/test/expression/DoBlock1.agda view
@@ -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+
+ data/test/expression/DoBlock2.agda view
@@ -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+
+ data/test/expression/DoBlock3.agda view
@@ -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+
+ data/test/expression/DoBlock4.agda view
@@ -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+
+ data/test/expression/ExtendedLam.agda view
@@ -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+  }+
+ data/test/expression/Lam.agda view
@@ -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+
+ data/test/expression/Let.agda view
@@ -0,0 +1,12 @@+module Let where++f+  : {A : Set}+  → A+  → A+f x+  = let+      y = x+      z = x+    in y+
+ data/test/expression/Pi.agda view
@@ -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+
+ data/test/expression/WithApp.agda view
@@ -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+
+ data/test/pattern/AsP.agda view
@@ -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+
+ data/test/pattern/IdentP.agda view
@@ -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+
+ data/test/pattern/OpAppP.agda view
@@ -0,0 +1,21 @@+module OpAppP where++data Bool+  : Set+  where++  false+    : Bool++  true+    : Bool++_&&_+  : Bool+  → Bool+  → Bool+false && _+  = false+true && b+  = b+
+ src/Agda/Unused.hs view
@@ -0,0 +1,32 @@+{- |+Module: Agda.Unused++Definitions and interface for the 'Unused' type, which represents a collection+of unused Agda code structures.+-}+module Agda.Unused+  ( Unused(..)+  , UnusedItems(..)+  ) where++import Agda.Unused.Types.Range+  (Range, RangeInfo)++-- ## Types++-- | A collection of unused items and files.+data Unused+  = Unused+  { unusedItems+    :: UnusedItems+  , unusedPaths+    :: [FilePath]+  } deriving Show++-- | A collection of unused items.+newtype UnusedItems+  = UnusedItems+  { unusedItemsList+    :: [(Range, RangeInfo)]+  } deriving Show+
+ src/Agda/Unused/Check.hs view
@@ -0,0 +1,1901 @@+{- |+Module: Agda.Unused++Check an Agda project for unused code.+-}+module Agda.Unused.Check+  ( checkUnused+  , checkUnusedLocal+  ) where++import Agda.Unused+  (Unused(..), UnusedItems(..))+import Agda.Unused.Monad.Error+  (Error(..), InternalError(..), UnexpectedError(..), UnsupportedError(..),+    liftLookup)+import Agda.Unused.Monad.Reader+  (Environment(..), askLocal, askRoot, askSkip, localSkip)+import Agda.Unused.Monad.State+  (ModuleState(..), State, modifyDelete, modifyInsert, stateBlock,+    stateCheck, stateEmpty, stateItems, stateLookup, stateModules)+import Agda.Unused.Types.Access+  (Access(..), fromAccess)+import Agda.Unused.Types.Context+  (AccessContext, AccessModule(..), Context, LookupError(..),+    accessContextDefine, accessContextImport, accessContextItem,+    accessContextLookup, accessContextLookupDefining, accessContextLookupModule,+    accessContextLookupSpecial, accessContextMatch, accessContextModule,+    accessContextModule', accessContextUnion, contextDelete,+    contextDeleteModule, contextItem, contextLookup, contextLookupItem,+    contextLookupModule, contextModule, contextRanges, fromContext, item,+    itemConstructor, itemPattern, 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)+import Agda.Unused.Types.Range+  (Range'(..), RangeInfo(..), RangeType(..))+import Agda.Unused.Types.Root+  (Root(..), Roots(..))+import Agda.Unused.Utils+  (liftMaybe, mapLeft)++import Agda.Syntax.Common+  (Arg(..), Fixity'(..), GenPart(..), ImportDirective'(..), ImportedName'(..),+    Named(..), Ranged(..), Renaming'(..), RewriteEqn'(..), Using'(..),+    namedThing, unArg, whThing)+import qualified Agda.Syntax.Common+  as Common+import Agda.Syntax.Concrete+  (Binder, Binder'(..), BoundName(..), Declaration, DoStmt(..), Expr(..),+    FieldAssignment, FieldAssignment'(..), ImportDirective, ImportedName,+    LamBinding, LamBinding'(..), LamClause(..), LHS(..), Module,+    ModuleApplication(..), ModuleAssignment(..), OpenShortHand(..), Pattern(..),+    RecordAssignment, Renaming, RewriteEqn, RHS, RHS'(..), TypedBinding,+    TypedBinding'(..), WhereClause, WhereClause'(..), _exprFieldA)+import Agda.Syntax.Concrete.Definitions+  (Clause(..), NiceDeclaration(..), niceDeclarations, runNice)+import Agda.Syntax.Concrete.Fixity+  (DoWarn(..), Fixities, fixitiesAndPolarities)+import Agda.Syntax.Concrete.Name+  (NameInScope(..), NamePart(..))+import qualified Agda.Syntax.Concrete.Name+  as N+import Agda.Syntax.Parser+  (moduleParser, parseFile, runPMIO)+import Agda.Syntax.Position+  (Range, getRange)+import Agda.Utils.FileName+  (AbsolutePath(..))+import Control.Monad+  (foldM, void)+import Control.Monad.Except+  (MonadError, liftEither, runExceptT, throwError)+import Control.Monad.IO.Class+  (MonadIO, liftIO)+import Control.Monad.Reader+  (MonadReader, ReaderT, runReaderT)+import Control.Monad.State+  (MonadState, StateT, gets, modify, runStateT)+import Data.Bool+  (bool)+import qualified Data.Map.Strict+  as Map+import Data.Maybe+  (catMaybes)+import qualified Data.Text+  as T+import System.Directory+  (doesDirectoryExist, doesFileExist, listDirectory)+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+  -> Context+  -> m Context+contextInsertRangeAll r c+  = askSkip >>= pure . bool (C.contextInsertRangeAll r c) c++-- Do nothing if `askSkip` returns true.+accessContextInsertRangeAll+  :: MonadReader Environment m+  => Range+  -> AccessContext+  -> m AccessContext+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+  :: Fixities+  -> Name+  -> Maybe Name+syntax fs (Name ps)+  = Map.lookup (N.Name NoRange InScope ps) fs >>= fromFixity++fromFixity+  :: Fixity'+  -> Maybe Name+fromFixity (Fixity' _ [] _)+  = Nothing+fromFixity (Fixity' _ ps@(_ : _) _)+  = Just (Name (fromGenPart <$> ps))++fromGenPart+  :: GenPart+  -> NamePart+fromGenPart (BindHole _ _)+  = Hole+fromGenPart (NormalHole _ _)+  = Hole+fromGenPart (WildHole _)+  = Hole+fromGenPart (IdPart (Ranged _ s))+  = Id s++-- ## Lists++checkSequence+  :: Monad m+  => Monoid c+  => (a -> b -> m c)+  -> a+  -> [b]+  -> m c+checkSequence f x ys+  = mconcat <$> sequence (f x <$> ys)++checkSequence_+  :: Monad m+  => (a -> b -> m ())+  -> a+  -> [b]+  -> m ()+checkSequence_ f x ys+  = void (sequence (f x <$> ys))++checkFold+  :: Monad m+  => Monoid a+  => (a -> b -> m a)+  -> a+  -> [b]+  -> m a+checkFold+  = checkFoldWith mempty (<>)++checkFoldUnion+  :: Monad m+  => (AccessContext -> b -> m AccessContext)+  -> AccessContext+  -> [b]+  -> m AccessContext+checkFoldUnion+  = checkFoldWith mempty accessContextUnion++checkFoldWith+  :: Monad m+  => a+  -> (a -> a -> a)+  -> (a -> b -> m a)+  -> a+  -> [b]+  -> m a+checkFoldWith x f g x' ys+  = foldM (\x'' y -> f x'' <$> g (f x' x'') y) x ys++-- ## Names++checkName+  :: MonadReader Environment m+  => MonadState State m+  => Bool+  -- ^ Whether to treat names as pattern synonyms.+  -> Fixities+  -> Access+  -> RangeType+  -> Range+  -> Name+  -> m AccessContext+checkName _ _ _ _ NoRange _+  = pure mempty+checkName _ _ _ _ _ (Name [Hole])+  = 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)))++checkName'+  :: MonadReader Environment m+  => MonadState State m+  => Bool+  -- ^ Whether to treat names as pattern synonyms.+  -> Fixities+  -> Access+  -> RangeType+  -> N.Name+  -> m AccessContext+checkName' p fs a t n+  = maybe (pure mempty) (uncurry (checkName p fs a t)) (fromNameRange n)++checkNames'+  :: MonadReader Environment m+  => MonadState State m+  => Bool+  -- ^ Whether to treat names as pattern synonyms.+  -> Access+  -> RangeType+  -> [N.Name]+  -> m AccessContext+checkNames' p a+  = checkSequence (checkName' p mempty a)++checkQNameP+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => AccessContext+  -> Range+  -> QName+  -> m AccessContext+checkQNameP c r n+  = checkQNamePWith (accessContextLookupSpecial n c) c r n++checkQNamePWith+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => Maybe Bool+  -> AccessContext+  -> Range+  -> QName+  -> m AccessContext+checkQNamePWith Nothing _ r n+  = checkQName Public RangeVariable r n+checkQNamePWith (Just False) _ _ _+  = pure mempty+checkQNamePWith (Just True) c r n+  = touchQName c r n >> pure mempty++checkQNameP'+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => AccessContext+  -> N.QName+  -> m AccessContext+checkQNameP' c n+  = maybe (pure mempty) (uncurry (checkQNameP c)) (fromQNameRange n)++checkQName+  :: MonadReader Environment m+  => MonadState State m+  => Access+  -> RangeType+  -> Range+  -> QName+  -> m AccessContext+checkQName a t r (QName n)+  = checkName False mempty a t r n+checkQName _ _ _ (Qual _ _)+  = pure mempty++checkModuleName+  :: MonadReader Environment m+  => MonadState State m+  => Context+  -> Access+  -> Range+  -> Name+  -> m AccessContext+checkModuleName c a r n+  = modifyInsert r (RangeNamed RangeModule (QName n))+  >> contextInsertRangeAll r c+  >>= \c' -> pure (accessContextModule n (AccessModule a [r] c'))++touchName+  :: MonadReader Environment m+  => MonadState State m+  => AccessContext+  -> Name+  -> m ()+touchName c n+  = askSkip >>= touchNameWith (accessContextLookupDefining (QName n) c)++touchNameWith+  :: MonadReader Environment m+  => MonadState State m+  => Either LookupError (Bool, [Range])+  -> Bool+  -> m ()+touchNameWith (Right (False, rs)) False+  = modifyDelete rs+touchNameWith _ _+  = pure ()++touchNames+  :: MonadReader Environment m+  => MonadState State m+  => AccessContext+  -> [Name]+  -> m ()+touchNames+  = checkSequence_ touchName++touchQName+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => AccessContext+  -> Range+  -> QName+  -> m ()+touchQName c r n+  = askSkip >>= touchQNameWith r n (accessContextLookupDefining n c)++touchQNameWith+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => Range+  -> QName+  -> Either LookupError (Bool, [Range])+  -> Bool+  -> m ()+touchQNameWith r n (Left LookupAmbiguous) False+  = throwError (ErrorAmbiguous r n)+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+  => MonadState State m+  => AccessContext+  -> N.QName+  -> m ()+touchQName' c n+  = maybe (pure ()) (uncurry (touchQName c)) (fromQNameRange n)++-- ## Bindings++checkBinder+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Bool+  -- ^ Whether to check bound names.+  -> AccessContext+  -> Binder+  -> m AccessContext+checkBinder b c (Binder p (BName n _ _))+  = bool localSkip id b (checkName' False mempty Public RangeVariable n)+  >>= \c' -> checkPatternMay c p+  >>= \c'' -> pure (c' <> c'')++checkBinders+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Bool+  -- ^ Whether to check bound names.+  -> AccessContext+  -> [Binder]+  -> m AccessContext+checkBinders b+  = checkSequence (checkBinder b)++checkLamBinding+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Bool+  -- ^ Whether to check bound names.+  -> AccessContext+  -> LamBinding+  -> m AccessContext+checkLamBinding b c (DomainFree (Arg _ (Named _ b')))+  = checkBinder b c b'+checkLamBinding b c (DomainFull b')+  = checkTypedBinding b c b'++checkLamBindings+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Bool+  -- ^ Whether to check bound names.+  -> AccessContext+  -> [LamBinding]+  -> m AccessContext+checkLamBindings b+  = checkFold (checkLamBinding b)++checkTypedBinding+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Bool+  -- ^ Whether to check bound names.+  -> AccessContext+  -> TypedBinding+  -> m AccessContext+checkTypedBinding b c (TBind _ bs e)+  = checkExpr c e >> checkBinders b c (namedThing . unArg <$> bs)+checkTypedBinding _ c (TLet _ ds)+  = checkDeclarations c ds++checkTypedBindings+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Bool+  -- ^ Whether to check bound names.+  -> AccessContext+  -> [TypedBinding]+  -> m AccessContext+checkTypedBindings b+  = checkFold (checkTypedBinding b)++-- ## Patterns+ +checkPattern+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> Pattern+  -> m AccessContext+checkPattern c (IdentP n)+  = checkQNameP' c n+checkPattern _ (QuoteP _)+  = pure mempty+checkPattern c (RawAppP _ ps)+  = checkRawAppP c ps+checkPattern _ (OpAppP r _ _ _)+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedOpAppP) r)+checkPattern c (HiddenP _ (Named _ p))+  = checkPattern c p+checkPattern c (InstanceP _ (Named _ p))+  = checkPattern c p+checkPattern c (ParenP _ p)+  = checkPattern c p+checkPattern _ (WildP _)+  = pure mempty+checkPattern _ (AbsurdP _)+  = pure mempty+checkPattern c (DotP _ e)+  = checkExpr c e >> pure mempty+checkPattern _ (LitP _)+  = pure mempty+checkPattern c (RecP _ as)+  = checkPatterns c (_exprFieldA <$> as)+checkPattern c (EqualP _ es)+  = checkExprPairs c es >> pure mempty+checkPattern _ (EllipsisP _)+  = pure mempty+checkPattern c (WithP _ p)+  = checkPattern c p++checkPattern c (AppP p (Arg _ (Named _ p')))+  = (<>)+  <$> checkPattern c p+  <*> checkPattern c p'++checkPattern c (AsP _ n p)+  = (<>)+  <$> checkName' False mempty Public RangeVariable n+  <*> checkPattern c p++checkPatternMay+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> Maybe Pattern+  -> m AccessContext+checkPatternMay _ Nothing+  = pure mempty+checkPatternMay c (Just p)+  = checkPattern c p++checkPatterns+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [Pattern]+  -> m AccessContext+checkPatterns+  = checkSequence checkPattern++checkRawAppP+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [Pattern]+  -> m AccessContext+checkRawAppP c ps+  = pure (accessContextMatch (patternNames ps) c)+  >>= \ns -> touchNames c ns+  >> checkPatterns c (patternDelete ns ps)++patternMatch+  :: [Name]+  -> Pattern+  -> Bool+patternMatch ns p+  = maybe False (flip elem (concat (nameIds <$> ns))) (patternName p)++patternDelete+  :: [Name]+  -> [Pattern]+  -> [Pattern]+patternDelete ns+  = filter (not . patternMatch ns)++patternName+  :: Pattern+  -> Maybe String+patternName (IdentP (N.QName (N.Name _ _ [Id n])))+  = Just n+patternName _+  = Nothing++patternNames+  :: [Pattern]+  -> [String]+patternNames+  = catMaybes+  . fmap patternName++-- ## Expressions++checkExpr+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> Expr+  -> m ()+checkExpr c (Ident n)+  = touchQName' c n+checkExpr _ (Lit _)+  = pure ()+checkExpr _ (QuestionMark _ _)+  = pure ()+checkExpr _ (Underscore _ _)+  = pure ()+checkExpr c (RawApp _ es)+  = checkRawApp c es+checkExpr c (App _ e (Arg _ (Named _ e')))+  = checkExpr c e >> checkExpr c e'+checkExpr _ (OpApp r _ _ _)+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedOpApp) r)+checkExpr c (WithApp _ e es)+  = checkExpr c e >> checkExprs c es+checkExpr c (HiddenArg _ (Named _ e))+  = checkExpr c e+checkExpr c (InstanceArg _ (Named _ e))+  = checkExpr c e+checkExpr c (Lam _ bs e)+  = checkLamBindings True c bs >>= \c' -> checkExpr (c <> c') e+checkExpr _ (AbsurdLam _ _)+  = pure ()+checkExpr c (ExtendedLam _ ls)+  = checkLamClauses_ c ls+checkExpr c (Fun _ (Arg _ e) e')+  = checkExpr c e >> checkExpr c e'+checkExpr c (Pi bs e)+  = checkTypedBindings True c bs >>= \c' -> checkExpr (c <> c') e+checkExpr _ (Set _)+  = pure ()+checkExpr _ (Prop _)+  = pure ()+checkExpr _ (SetN _ _)+  = pure ()+checkExpr _ (PropN _ _)+  = pure ()+checkExpr c (Rec _ rs)+  = checkRecordAssignments c rs+checkExpr c (RecUpdate _ e fs)+  = checkExpr c e >> checkFieldAssignments c fs+checkExpr c (Paren _ e)+  = checkExpr c e+checkExpr c (IdiomBrackets _ es)+  = checkExprs c es+checkExpr c (DoBlock _ ss)+  = void (checkDoStmts c ss)+checkExpr _ (Absurd r)+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedAbsurd) r)+checkExpr _ (As 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))+checkExpr _ (Quote _)+  = pure ()+checkExpr _ (QuoteTerm _)+  = pure ()+checkExpr c (Tactic _ e)+  = checkExpr c e+checkExpr _ (Unquote _)+  = pure ()+checkExpr _ e@(DontCare _)+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedDontCare) (getRange e))+checkExpr _ (Equal r _ _)+  = throwError (ErrorInternal (ErrorUnexpected UnexpectedEqual) r)+checkExpr _ (Ellipsis 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++checkExprs+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [Expr]+  -> m ()+checkExprs+  = checkSequence_ checkExpr++checkExprPair+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> (Expr, Expr)+  -> m ()+checkExprPair c (e1, e2)+  = checkExpr c e1 >> checkExpr c e2++checkExprPairs+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [(Expr, Expr)]+  -> m ()+checkExprPairs+  = checkSequence_ checkExprPair++checkRawApp+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [Expr]+  -> m ()+checkRawApp c es+  = touchNames c (accessContextMatch (exprNames es) c)+  >> checkExprs c es++exprName+  :: Expr+  -> Maybe String+exprName (Ident (N.QName (N.Name _ _ [Id n])))+  = Just n+exprName _+  = Nothing++exprNames+  :: [Expr]+  -> [String]+exprNames+  = catMaybes+  . fmap exprName++-- ## Assignments++checkRecordAssignment+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> RecordAssignment+  -> m ()+checkRecordAssignment c (Left f)+  = checkFieldAssignment c f+checkRecordAssignment c (Right m)+  = checkModuleAssignment c m++checkRecordAssignments+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [RecordAssignment]+  -> m ()+checkRecordAssignments+  = checkSequence_ checkRecordAssignment++checkFieldAssignment+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> FieldAssignment+  -> m ()+checkFieldAssignment c (FieldAssignment _ e)+  = checkExpr c e++checkFieldAssignments+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [FieldAssignment]+  -> m ()+checkFieldAssignments+  = checkSequence_ checkFieldAssignment++checkModuleAssignment+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> ModuleAssignment+  -> m ()+checkModuleAssignment c a@(ModuleAssignment n es _)+  = checkExprs c es+  >> maybe (pure ()) (touchModule c (getRange a)) (fromQName n)++-- ## Definitions++checkLHS+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> LHS+  -> m AccessContext+checkLHS c (LHS p rs ws _)+  = checkPattern c p+  >>= \c' -> checkRewriteEqns (c <> c') rs+  >>= \c'' -> checkExprs (c <> c' <> c'') (whThing <$> ws)+  >> pure (c' <> c'')++checkRHS+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> RHS+  -> m ()+checkRHS _ AbsurdRHS+  = pure ()+checkRHS c (RHS e)+  = checkExpr c e++checkClause+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> Clause+  -> m AccessContext+checkClause c (Clause n _ l r w cs)+  = pure (maybe id accessContextDefine (fromName n) c)+  >>= \c' -> checkLHS c' l+  >>= \c'' -> checkWhereClause (c' <> c'') w+  >>= \(m, c''') -> checkRHS (c' <> c'' <> c''') r+  >> checkClauses (c' <> c'' <> c''') cs+  >>= \m' -> pure (m <> m')++checkClauses+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [Clause]+  -> m AccessContext+checkClauses+  = checkSequence checkClause++checkLamClause+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> LamClause+  -> m AccessContext+checkLamClause c (LamClause l r _ _)+  = checkLHS c l+  >>= \c' -> checkRHS (c <> c') r+  >> pure c'++checkLamClauses+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [LamClause]+  -> m AccessContext+checkLamClauses+  = checkFold checkLamClause++checkLamClause_+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> LamClause+  -> m ()+checkLamClause_ c ls+  = void (checkLamClause c ls)++-- Do not propogate context from one clause to the next.+checkLamClauses_+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [LamClause]+  -> m ()+checkLamClauses_+  = checkSequence_ checkLamClause_++checkWhereClause+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> WhereClause+  -> m (AccessContext, AccessContext)+  -- ^ A context for the named where block, then the full context.+checkWhereClause _ NoWhere+  = pure (mempty, mempty)+checkWhereClause c (AnyWhere ds)+  = 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'+  >>= \c'' -> pure (c'' , c')++checkRewriteEqn+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> RewriteEqn+  -> m AccessContext+checkRewriteEqn c (Rewrite rs)+  = checkExprs c (snd <$> rs) >> pure mempty+checkRewriteEqn c (Invert _ ws)+  = checkIrrefutableWiths c ws++checkRewriteEqns+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [RewriteEqn]+  -> m AccessContext+checkRewriteEqns+  = checkFold checkRewriteEqn++checkIrrefutableWith+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> (Pattern, Expr)+  -> m AccessContext+checkIrrefutableWith c (p, e)+  = checkExpr c e >> checkPattern c p++checkIrrefutableWiths+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [(Pattern, Expr)]+  -> m AccessContext+checkIrrefutableWiths+  = checkFold checkIrrefutableWith++checkDoStmt+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> DoStmt+  -> m AccessContext+checkDoStmt c (DoBind _ p e cs)+  = checkLamClauses c cs+  >>= \c' -> checkExpr (c <> c') e+  >> checkPattern (c <> c') p+  >>= \c'' -> pure (c' <> c'')+checkDoStmt c (DoThen e)+  = checkExpr c e >> pure mempty+checkDoStmt c (DoLet _ ds)+  = checkDeclarations c ds++checkDoStmts+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [DoStmt]+  -> m AccessContext+checkDoStmts c ss+  = bool (pure ()) (touchName c bind) (hasBind ss)+  >> bool (pure ()) (touchName c bind_) (hasBind_ ss)+  >> checkFold checkDoStmt c ss++hasBind+  :: [DoStmt]+  -> Bool+hasBind []+  = False+hasBind (_ : [])+  = False+hasBind (DoBind _ _ _ _ : _ : _)+  = True+hasBind (_ : ss)+  = hasBind ss++hasBind_+  :: [DoStmt]+  -> Bool+hasBind_ []+  = False+hasBind_ (_ : [])+  = False+hasBind_ (DoThen _ : _ : _)+  = True+hasBind_ (_ : ss)+  = hasBind_ ss++bind+  :: Name+bind+  = Name+  [ Hole+  , Id ">>="+  , Hole+  ]++bind_+  :: Name+bind_+  = Name+  [ Hole+  , Id ">>"+  , Hole+  ]++-- ## Declarations++checkDeclarations+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [Declaration]+  -> m AccessContext+checkDeclarations+  = checkDeclarationsWith checkNiceDeclarations++checkDeclarationsRecord+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Name+  -> [Range]+  -- ^ Ranges associated with parent record.+  -> AccessContext+  -> [Declaration]+  -> m AccessContext+checkDeclarationsRecord n rs+  = checkDeclarationsWith (checkNiceDeclarationsRecord n rs)++checkDeclarationsTop+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> [Declaration]+  -> m AccessContext+checkDeclarationsTop+  = checkDeclarationsWith checkNiceDeclarationsTop++checkDeclarationsWith+  :: MonadError Error m+  => (Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)+  -> AccessContext+  -> [Declaration]+  -> m AccessContext+checkDeclarationsWith f c ds = do+  (fixities, _)+    <- fixitiesAndPolarities NoWarn ds+  (niceDeclsEither, _) +    <- pure (runNice (niceDeclarations fixities ds))+  niceDecls+    <- liftEither (mapLeft ErrorDeclaration niceDeclsEither)+  f fixities c niceDecls++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)+  = checkExpr c e >> checkName' False fs (fromAccess a) RangeDefinition n+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 _ _)+  = pure mempty+checkNiceDeclaration fs c (NiceRecSig _ a _ _ _ n bs e)+  = checkNiceSig fs c a RangeRecord 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)+  = checkExpr c e >> checkName' False fs (fromAccess a) RangeDefinition n+checkNiceDeclaration _ c (FunDef _ _ _ _ _ _ _ cs)+  = checkClauses c cs >> pure mempty+checkNiceDeclaration _ c (NiceGeneralize _ _ _ _ _ e)+  = checkExpr c e >> pure mempty+checkNiceDeclaration _ _ (NiceUnquoteDecl r _ _ _ _ _ _ _)+  = throwError (ErrorUnsupported UnsupportedUnquote r)+checkNiceDeclaration _ _ (NiceUnquoteDef r _ _ _ _ _ _)+  = throwError (ErrorUnsupported UnsupportedUnquote r)++checkNiceDeclaration fs c+  (NiceMutual _ _ _ _+    ds@(NiceRecSig _ _ _ _ _ _ _ _ : NiceRecDef _ _ _ _ _ _ _ _ _ _ _ : _))+  = checkNiceDeclarations fs c ds+checkNiceDeclaration fs c+  (NiceMutual _ _ _ _+    ds@(NiceDataSig _ _ _ _ _ _ _ _ : NiceDataDef _ _ _ _ _ _ _ _ : _))+  = checkNiceDeclarations fs c ds+checkNiceDeclaration fs c+  (NiceMutual _ _ _ _+    ds@(FunSig _ _ _ _ _ _ _ _ _ _ : FunDef _ _ _ _ _ _ _ _ : _))+  = checkNiceDeclarations fs c ds+checkNiceDeclaration fs c (NiceMutual r _ _ _ ds)+  = checkNiceDeclarations fs c ds+  >>= \c' -> modifyInsert r RangeMutual+  >> accessContextInsertRangeAll r c'++checkNiceDeclaration _ c+  (NiceModuleMacro r _ (N.NoName _ _)+    (SectionApp _ [] (RawApp _ (Ident n : es))) DoOpen i)+  = 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+  (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')+  >>= \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+  (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')+  >>= \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''+  >>= \c'''' -> pure (c'''' <> fromContext (importDirectiveAccess i) c''')+checkNiceDeclaration _ _+  (NiceModuleMacro _ _ _+    (SectionApp r _ _) _ _)+  = 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)+  >>= \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'+  >>= \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'+  >>= \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'+  >>= \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' -> checkImportDirective Import r n' c' i+  >>= \c'' -> checkModuleName c' Public (getRange a) 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)+  = localSkip (checkNames' False Public RangeVariable (unArg <$> ns))+  >>= \c' -> checkPattern (c <> c') p+  >> checkName' True fs (fromAccess a) RangePatternSynonym n++checkNiceDeclarationRecord+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Name+  -> [Range]+  -- ^ Ranges associated with parent record.+  -> Fixities+  -> AccessContext+  -> NiceDeclaration+  -> m AccessContext+checkNiceDeclarationRecord _ rs fs c d@(Axiom _ _ _ _ _ _ _)+  = modifyDelete rs >> checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ rs fs c d@(PrimitiveFunction _ _ _ _ _)+  = modifyDelete rs >> checkNiceDeclaration fs c d+checkNiceDeclarationRecord n rs fs c (NiceMutual _ _ _ _ ds)+  = checkNiceDeclarationsRecord n rs fs c ds+checkNiceDeclarationRecord _ rs fs c d@(NiceModule _ _ _ _ _ _)+  = modifyDelete rs >> checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ _ fs c d@(NiceModuleMacro _ _ _ _ _ _)+  = checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ _ fs c d@(NiceOpen _ _ _)+  = checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ _ fs c d@(NiceImport _ _ _ _ _)+  = checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ _ fs c d@(NicePragma _ _)+  = checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ rs fs c d@(NiceRecSig _ _ _ _ _ _ _ _)+  = modifyDelete rs >> checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ rs fs c d@(NiceDataSig _ _ _ _ _ _ _ _)+  = modifyDelete rs >> checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ _ fs c d@(NiceFunClause _ _ _ _ _ _ _)+  = checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ rs fs c d@(FunSig _ _ _ _ _ _ _ _ _ _)+  = modifyDelete rs >> checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ _ fs c d@(FunDef _ _ _ _ _ _ _ _)+  = checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ _ fs c d@(NiceDataDef _ _ _ _ _ _ _ _)+  = checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ _ fs c d@(NiceRecDef _ _ _ _ _ _ _ _ _ _ _)+  = checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ _ fs c d@(NicePatternSyn _ _ _ _ _)+  = checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ _ fs c d@(NiceGeneralize _ _ _ _ _ _)+  = checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ _ fs c d@(NiceUnquoteDecl _ _ _ _ _ _ _ _)+  = checkNiceDeclaration fs c d+checkNiceDeclarationRecord _ _ fs c d@(NiceUnquoteDef _ _ _ _ _ _ _)+  = checkNiceDeclaration fs c d++checkNiceDeclarationRecord n rs fs c (NiceField _ a _ _ _ n' (Arg _ e))+  = checkExpr (accessContextDefine n c) e+  >> maybe+    (pure mempty)+    (\n'' -> pure (accessContextItem n'' (fromAccess a)+      (item rs (syntax fs n''))))+    (fromName n')++checkNiceDeclarations+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Fixities+  -> AccessContext+  -> [NiceDeclaration]+  -> m AccessContext+checkNiceDeclarations fs+  = checkFoldUnion (checkNiceDeclaration fs)++checkNiceDeclarationsRecord+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Name+  -> [Range]+  -- ^ Ranges associated with parent record.+  -> Fixities+  -> AccessContext+  -> [NiceDeclaration]+  -> m AccessContext+checkNiceDeclarationsRecord n rs fs+  = checkFoldUnion (checkNiceDeclarationRecord n rs fs)++checkNiceDeclarationsTop+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Fixities+  -> AccessContext+  -> [NiceDeclaration]+  -> m AccessContext+checkNiceDeclarationsTop _ _ []+  = pure mempty+checkNiceDeclarationsTop _ c (NiceModule r a _ _ bs ds : _)+  = checkNiceModule c (fromAccess a) r Nothing bs ds+checkNiceDeclarationsTop fs c (d : ds)+  = checkNiceDeclaration fs c d+  >>= \c' -> checkNiceDeclarations fs (c <> c') ds++checkNiceSig+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Fixities+  -> AccessContext+  -> Common.Access+  -> RangeType+  -> N.Name+  -> [LamBinding]+  -> Expr+  -> m AccessContext+checkNiceSig fs c a t n bs e+  = checkLamBindings False c bs+  >>= \c' -> checkExpr (c <> c') e+  >> checkName' False fs (fromAccess a) t n++checkNiceConstructor+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Fixities+  -> [Range]+  -- ^ Ranges associated with parent type.+  -> AccessContext+  -> NiceDeclaration+  -> 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''))))+    (fromName n)+checkNiceConstructor _ _ _ d+  = throwError (ErrorInternal ErrorConstructor (getRange d))++checkNiceConstructors+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Fixities+  -> [Range]+  -- ^ Ranges associated with parent type.+  -> AccessContext+  -> [NiceDeclaration]+  -> m AccessContext+checkNiceConstructors fs rs+  = checkSequence (checkNiceConstructor fs rs)++checkNiceConstructorRecord+  :: MonadReader Environment m+  => MonadState State m+  => Fixities+  -> [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)))++checkNiceConstructorRecordMay+  :: MonadReader Environment m+  => MonadState State m+  => Fixities+  -> [Range]+  -- ^ Ranges associated with record type.+  -> Maybe (Range, Name)+  -> m AccessContext+checkNiceConstructorRecordMay _ _ Nothing+  = pure mempty+checkNiceConstructorRecordMay fs rs (Just (r, n))+  = checkNiceConstructorRecord fs rs r n++checkNiceModule+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> Access+  -> Range+  -> Maybe Name+  -- ^ If `Nothing`, the module is anonymous.+  -> [TypedBinding]+  -> [Declaration]+  -> m AccessContext+checkNiceModule c a r n bs ds+  = checkTypedBindings True c bs+  >>= \c' -> checkDeclarations (c <> c') ds+  >>= \c'' -> pure (toContext c'')+  >>= \c''' -> maybe (pure (fromContext a c''')) (checkModuleName c''' a r) n++-- ## Imports++data DirectiveType where++  Import+    :: DirectiveType++  Module+    :: DirectiveType++  Open+    :: DirectiveType++  deriving Show++directiveStatement+  :: DirectiveType+  -> Maybe RangeType+directiveStatement Import+  = Just RangeImport+directiveStatement Module+  = Nothing+directiveStatement Open+  = Just RangeOpen++directiveItem+  :: DirectiveType+  -> RangeType+directiveItem Import+  = RangeImportItem+directiveItem Module+  = RangeModuleItem+directiveItem Open+  = RangeOpenItem++checkImportDirective+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => DirectiveType+  -> Range+  -> QName+  -> Context+  -> 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+checkImportDirective dt r n c (ImportDirective _ (Using ns) _ rs _)+  = maybe (pure ()) (\t -> modifyInsert r (RangeNamed t n))+    (directiveStatement dt)+  >> checkImportedNames dt c ns+  >>= \c' -> checkRenamings dt c rs+  >>= \c'' -> contextInsertRangeAll r (c' <> c'')++checkRenaming+  :: MonadReader Environment m+  => MonadState State m+  => MonadError Error m+  => DirectiveType+  -> Context+  -> Renaming+  -> m Context+checkRenaming dt c r@(Renaming n t _ _)+  = checkImportedNamePair dt c (getRange r, n, t)++checkRenamings+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => DirectiveType+  -> Context+  -> [Renaming]+  -> m Context+checkRenamings dt+  = checkSequence (checkRenaming dt)++checkImportedName+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => DirectiveType+  -> Context+  -> ImportedName+  -> m Context+checkImportedName dt c n+  = checkImportedNamePair dt c (getRange n, n, n)++checkImportedNamePair+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => DirectiveType+  -> Context+  -> (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)+  >>= \(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)+  >>= \(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)++checkImportedNames+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => DirectiveType+  -> Context+  -> [ImportedName]+  -> m Context+checkImportedNames dt+  = checkSequence (checkImportedName dt)++modifyHiding+  :: MonadError Error m+  => Context+  -> ImportedName+  -> m Context+modifyHiding c (ImportedName n)+  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n)+  >>= pure . flip contextDelete c+modifyHiding c (ImportedModule n)+  = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n)+  >>= pure . flip contextDeleteModule c++modifyHidings+  :: MonadError Error m+  => Context+  -> [ImportedName]+  -> m Context+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+  => MonadState State m+  => AccessContext+  -> Range+  -> QName+  -> m ()+touchModule c r n+  = touchModuleWith (accessContextLookupModule n c) r n++touchModuleWith+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => Either LookupError C.Module+  -> Range+  -> QName+  -> m ()+touchModuleWith (Left LookupNotFound) _ _+  = pure ()+touchModuleWith (Left LookupAmbiguous) r n+  = throwError (ErrorAmbiguous r n)+touchModuleWith (Right m) _ _+  = modifyDelete (moduleRanges m)++touchContext+  :: MonadReader Environment m+  => MonadState State m+  => Context+  -> m ()+touchContext c+  = modifyDelete (contextRanges c)++importDirectiveAccess+  :: ImportDirective+  -> Access+importDirectiveAccess (ImportDirective _ _ _ _ Nothing)+  = Private+importDirectiveAccess (ImportDirective _ _ _ _ (Just _))+  = Public++-- ## Modules++checkModule+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Module+  -> m Context+checkModule (_, ds)+  = toContext <$> checkDeclarationsTop mempty ds++-- ## Files++checkFile+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Maybe Range+  -> QName+  -> m Context+checkFile r n+  = gets (stateLookup n) >>= \s -> checkFileWith s r n++checkFileWith+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Maybe ModuleState+  -> Maybe Range+  -> QName+  -> m Context++checkFileWith Nothing r n | isBuiltin n+  = liftIO (getDataFileName ("data" </> qNamePath n))+  >>= \p -> localSkip (checkFilePath r n p)++checkFileWith Nothing r n = do+  local+    <- askLocal+  rootPath+    <- askRoot+  context+    <- checkFilePath r n (rootPath </> qNamePath n)+  _+    <- bool (pure ()) (touchContext context) local+  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+  -> FilePath+  -> m Context+checkFilePath r n p = do+  _+    <- modify (stateBlock n)+  absolutePath+    <- pure (AbsolutePath (T.pack p))+  exists+    <- liftIO (doesFileExist p)+  _+    <- bool (throwError (ErrorFile r n p)) (pure ()) exists+  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++-- ## Paths++-- Look for unvisited modules at the given path.+checkPath+  :: MonadIO m+  => [QName]+  -- ^ Visited or ignored modules.+  -> 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')++checkPathFile+  :: [QName]+  -> FilePath+  -> FilePath+  -> [FilePath]+checkPathFile ms p p'+  = maybe [] (bool [p'] [] . flip elem ms) (pathQName p p')++checkPathDirectory+  :: MonadIO m+  => [QName]+  -> FilePath+  -> 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++-- ## Main++-- | Check an Agda file and its dependencies for unused code.+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)++-- | Check an Agda file for unused code.+checkUnusedLocal+  :: FilePath+  -- ^ The project root path.+  -> QName+  -- ^ The module to check.+  -> IO (Either Error UnusedItems)+checkUnusedLocal p+  = runExceptT+  . fmap UnusedItems+  . fmap stateItems+  . checkUnusedItems True p+  . checkFile Nothing++checkUnusedItems+  :: MonadError Error m+  => MonadIO m+  => Bool+  -- ^ Whether to use local mode.+  -> FilePath+  -> ReaderT Environment (StateT State m) a+  -> m State+checkUnusedItems l p+  = fmap snd+  . flip runStateT stateEmpty+  . flip runReaderT (Environment False l p)+
+ src/Agda/Unused/Monad/Error.hs view
@@ -0,0 +1,220 @@+{-# LANGUAGE UndecidableInstances #-}++{- |+Module: Agda.Unused.Monad.Error++An error monad for determining unused code.+-}+module Agda.Unused.Monad.Error++  ( -- * Definitions+    +    Error(..)+  , InternalError(..)+  , UnexpectedError(..)+  , UnsupportedError(..)++    -- * Lift++  , liftLookup++  ) where++import Agda.Unused.Types.Context+  (LookupError(..))+import Agda.Unused.Types.Name+  (QName)+import Agda.Unused.Types.Range+  (Range, getRange)++import Agda.Syntax.Concrete.Definitions+  (DeclarationException)+import Agda.Syntax.Concrete.Fixity+  (MonadFixityError(..))+import Agda.Syntax.Parser+  (ParseError)+import Control.Monad.Except+  (MonadError, throwError)++-- ## Definitions++-- | An error encountered while checking for unused code.+data Error where++  -- | Ambiguous lookup.+  ErrorAmbiguous+    :: !Range+    -> !QName+    -> Error++  -- | Cyclic module dependency.+  ErrorCyclic+    :: !(Maybe Range)+    -> !QName+    -> Error++  -- | Agda declaration exception.+  ErrorDeclaration+    :: !DeclarationException+    -> Error++  -- | File not found.+  ErrorFile+    :: !(Maybe Range)+    -> !QName+    -> !FilePath+    -> Error++  -- | Agda fixity exception.+  ErrorFixity+    :: !(Maybe Range)+    -> Error++  -- | Internal error; should be reported.+  ErrorInternal+    :: !InternalError+    -> !Range+    -> Error++  -- | Module not found in open statement.+  ErrorOpen+    :: !Range+    -> !QName+    -> Error++  -- | Agda parse error.+  ErrorParse+    :: !ParseError+    -> Error+  +  -- | Agda polarity error.+  ErrorPolarity+    :: !(Maybe Range)+    -> Error++  -- | Root not found.+  ErrorRoot+    :: !QName+    -> !QName+    -> Error++  -- | Unsupported language feature.+  ErrorUnsupported+    :: !UnsupportedError+    -> !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++  -- | Unexpected arguments to SectionApp constructor.+  ErrorMacro+    :: InternalError++  -- | Unexpected underscore as name.+  ErrorName+    :: InternalError++  -- | Unexpected name-module mismatch in renaming statement.+  ErrorRenaming+    :: InternalError++  -- | Unexpected data type constructor.+  ErrorUnexpected+    :: !UnexpectedError+    -> InternalError++  deriving Show++-- | An error indicating that a constructor for a data type is used where it+-- should not be used.+data UnexpectedError where++  UnexpectedAbsurd+    :: UnexpectedError++  UnexpectedAs+    :: UnexpectedError++  UnexpectedDontCare+    :: UnexpectedError++  UnexpectedETel+    :: UnexpectedError++  UnexpectedEllipsis+    :: UnexpectedError++  UnexpectedEqual+    :: UnexpectedError++  UnexpectedField+    :: UnexpectedError++  UnexpectedNiceFunClause+    :: UnexpectedError++  UnexpectedOpApp+    :: UnexpectedError++  UnexpectedOpAppP+    :: UnexpectedError++  deriving Show++-- | An error indicating that an unsupported language was found.+data UnsupportedError where++  -- | Record module instance applications.+  UnsupportedMacro+    :: UnsupportedError++  -- | Unquoting primitives.+  UnsupportedUnquote+    :: UnsupportedError++  deriving Show++-- ## Fixity++instance (Monad m, MonadError Error m) => MonadFixityError m where+  throwMultipleFixityDecls []+    = throwError (ErrorFixity Nothing)+  throwMultipleFixityDecls ((n, _) : _)+    = throwError (ErrorFixity (Just (getRange n)))+  throwMultiplePolarityPragmas []+    = throwError (ErrorPolarity Nothing)+  throwMultiplePolarityPragmas (n : _)+    = throwError (ErrorPolarity (Just (getRange n)))+  warnUnknownNamesInFixityDecl _+    = pure ()+  warnUnknownNamesInPolarityPragmas _+    = pure ()+  warnUnknownFixityInMixfixDecl _+    = pure ()+  warnPolarityPragmasButNotPostulates _+    = pure ()++-- ## Lookup++-- | Lift a lookup result to our error monad.+liftLookup+  :: MonadError Error m+  => Range+  -> QName+  -> Either LookupError a+  -> m a+liftLookup r n (Left LookupNotFound)+  = throwError (ErrorOpen r n)+liftLookup r n (Left LookupAmbiguous)+  = throwError (ErrorAmbiguous r n)+liftLookup _ _ (Right x)+  = pure x+
+ src/Agda/Unused/Monad/Reader.hs view
@@ -0,0 +1,69 @@+{- |+Module: Agda.Unused.Monad.Reader++A reader monad for determining unused code.+-}+module Agda.Unused.Monad.Reader++  ( -- * Definition+    +    Environment(..)++    -- * Ask++  , askSkip+  , askLocal+  , askRoot++    -- * Local++  , localSkip++  ) where++import Control.Monad.Reader+  (MonadReader, ask, local)++-- | 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.+  , environmentRoot+    :: !FilePath+    -- ^ The project root path.+  } deriving Show++-- | Ask whether to skip checking names.+askSkip+  :: MonadReader Environment m+  => m Bool+askSkip+  = environmentSkip <$> ask++-- | Ask whether to skip checking public names.+askLocal+  :: MonadReader Environment m+  => m Bool+askLocal+  = environmentLocal <$> ask++-- | Ask for the project root path.+askRoot+  :: MonadReader Environment m+  => m FilePath+askRoot+  = environmentRoot <$> ask++-- | Skip checking names in a local computation.+localSkip+  :: MonadReader Environment m+  => m a+  -> m a+localSkip+  = local (\e -> e {environmentSkip = True})+
+ src/Agda/Unused/Monad/State.hs view
@@ -0,0 +1,174 @@+{- |+Module: Agda.Unused.Monad.State++A state monad for determining unused code.+-}+module Agda.Unused.Monad.State++  ( -- * Definitions++    ModuleState(..)+  , State++    -- * Interface++  , stateEmpty+  , stateItems+  , stateModules+  , stateBlock+  , stateCheck+  , stateLookup++    -- * Modify++  , modifyDelete+  , modifyInsert++  ) where++import Agda.Unused.Monad.Reader+  (Environment, askSkip)+import Agda.Unused.Types.Context+  (Context)+import Agda.Unused.Types.Name+  (QName)+import Agda.Unused.Types.Range+  (Range, Range'(..), RangeInfo, rangeContains)+import Agda.Unused.Utils+  (mapDeletes)++import Control.Monad.Reader+  (MonadReader)+import Control.Monad.State+  (MonadState, modify)+import Data.Bool+  (bool)+import Data.Map.Strict+  (Map)+import qualified Data.Map.Strict+  as Map++-- | Cache the results of checking modules. This allows us to:+-- +-- - Avoid duplicate computations.+-- - Handle cyclic module dependencies without nontermination.+data ModuleState where++  Blocked+    :: ModuleState++  Checked+    :: !Context+    -> ModuleState++  deriving Show++-- | The current computation state.+data State+  = State+  { stateItems'+    :: !(Map Range RangeInfo)+    -- ^ Ranges for each unused item.+  , stateModules'+    :: !(Map QName ModuleState)+    -- ^ States for each module dependency.+  } deriving Show++-- | Construct an empty state.+stateEmpty+  :: State+stateEmpty+  = State mempty mempty++-- | Get a sorted list of state items.+--+-- If one state item contains another (e.g., an @open@ statement containing+-- @using@ directives), then keep only the containing item.+stateItems+  :: State+  -> [(Range, RangeInfo)]+stateItems+  = stateItemsFilter+  . Map.toAscList+  . stateItems'++-- | Get a list of visited modules.+stateModules+  :: State+  -> [QName]+stateModules+  = Map.keys+  . stateModules'++-- Remove nested items.+stateItemsFilter+  :: [(Range, RangeInfo)]+  -> [(Range, RangeInfo)]+stateItemsFilter []+  = []+stateItemsFilter (i : i' : is) | rangeContains (fst i) (fst i')+  = stateItemsFilter (i : is)+stateItemsFilter (i : is)+  = i : stateItemsFilter is++stateInsert+  :: Range+  -> RangeInfo+  -> State+  -> State+stateInsert NoRange _ s+  = s+stateInsert r@(Range _ _) i (State rs ms)+  = State (Map.insert r i rs) ms++stateDelete+  :: [Range]+  -> State+  -> State+stateDelete rs (State rs' ms)+  = State (mapDeletes rs rs') ms++-- | Lookup the state of a module.+stateLookup+  :: QName+  -> State+  -> Maybe ModuleState+stateLookup m (State _ ms)+  = Map.lookup m 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)++-- | 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)++-- | Record a new unused item.+modifyInsert+  :: MonadReader Environment m+  => MonadState State m+  => Range+  -> RangeInfo+  -> m ()+modifyInsert r i+  = askSkip >>= bool (modify (stateInsert r i)) (pure ())++-- | Mark a list of items as used.+modifyDelete+  :: MonadReader Environment m+  => MonadState State m+  => [Range]+  -> m ()+modifyDelete rs+  = askSkip >>= bool (modify (stateDelete rs)) (pure ())+
+ src/Agda/Unused/Parse.hs view
@@ -0,0 +1,150 @@+{- |+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"+
+ src/Agda/Unused/Print.hs view
@@ -0,0 +1,285 @@+{- |+Module: Agda.Unused.Print++Printing functions for unused items and errors.+-}+module Agda.Unused.Print+  ( printError+  , printUnused+  , printUnusedItems+  , printNothing+  ) where++import Agda.Unused+  (Unused(..), UnusedItems(..))+import Agda.Unused.Monad.Error+  (Error(..), InternalError(..), UnexpectedError(..), UnsupportedError(..))+import Agda.Unused.Types.Name+  (Name(..), NamePart(..), QName(..))+import Agda.Unused.Types.Range+  (Range, Range'(..), RangeInfo(..), RangeType(..), getRange)++import Agda.Utils.Pretty+  (prettyShow)+import Data.Text+  (Text)+import qualified Data.Text+  as T++-- ## Utilities++quote+  :: Text+  -> Text+quote t+  = "‘" <> t <> "’"++parens+  :: Text+  -> Text+parens t+  = "(" <> t <> ")"++indent+  :: Text+  -> Text+indent t+  = "  " <> t++-- ## Names++printNamePart+  :: NamePart+  -> Text+printNamePart+  = T.pack . show++printName+  :: Name+  -> Text+printName (Name ps)+  = mconcat (printNamePart <$> ps)++printQName+  :: QName+  -> Text+printQName (QName n)+  = printName n+printQName (Qual n ns)+  = printName n <> "." <> printQName ns++-- ## Ranges++printRange+  :: Range+  -> Text+printRange NoRange+  = "unknown location"+printRange r@(Range _ _)+  = T.pack (show r)++-- ## Messages++printMessage+  :: Text+  -> Text+  -> Text+printMessage t1 t2+  = T.unlines [t1, t2]++printMessageIndent+  :: Text+  -> Text+  -> Text+printMessageIndent t1 t2+  = T.unlines [t1, indent t2]++-- ## Errors++-- | Print an error.+printError+  :: Error+  -> Text++printError (ErrorAmbiguous r n)+  = printMessage (printRange r)+  $ "Error: Ambiguous name " <> parens (quote (printQName n)) <> "."+printError (ErrorCyclic r n)+  = printMessage (maybe (printQName n) 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 (ErrorFixity (Just r))+  = printMessage (printRange r)+  $ "Error: Multiple fixity declarations."+printError (ErrorInternal e r)+  = printMessage (printRange r)+  $ "Internal error: " <> printInternalError e+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 (ErrorUnsupported e r)+  = printMessage (printRange r)+  $ "Error: " <> printUnsupportedError e <> " not supported."++printError (ErrorFixity Nothing)+  = "Error: Multiple fixity declarations."+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)++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) <> "."++printUnexpectedError+  :: UnexpectedError+  -> Text+printUnexpectedError UnexpectedAbsurd+  = "Absurd"+printUnexpectedError UnexpectedAs+  = "As"+printUnexpectedError UnexpectedDontCare+  = "DontCare"+printUnexpectedError UnexpectedETel+  = "ETel"+printUnexpectedError UnexpectedEllipsis+  = "Ellipsis"+printUnexpectedError UnexpectedEqual+  = "Equal"+printUnexpectedError UnexpectedField+  = "Field"+printUnexpectedError UnexpectedNiceFunClause+  = "NiceFunClause"+printUnexpectedError UnexpectedOpApp+  = "OpApp"+printUnexpectedError UnexpectedOpAppP+  = "OpAppP"++printUnsupportedError+  :: UnsupportedError+  -> Text+printUnsupportedError UnsupportedMacro+  = "Record module instance applications"+printUnsupportedError UnsupportedUnquote+  = "Unquoting primitives"++-- ## Unused++-- | Print a collection of unused items and files.+printUnused+  :: Unused+  -> Maybe Text+printUnused (Unused is ps)+  = printUnusedWith+    (printUnusedItems is)+    (printUnusedPaths ps)++printUnusedWith+  :: Maybe Text+  -> Maybe Text+  -> Maybe Text+printUnusedWith Nothing Nothing+  = Nothing+printUnusedWith Nothing (Just t2)+  = Just t2+printUnusedWith (Just t1) Nothing+  = Just t1+printUnusedWith (Just t1) (Just t2)+  = Just (t2 <> t1)+    +printUnusedPaths+  :: [FilePath]+  -> Maybe Text+printUnusedPaths []+  = Nothing+printUnusedPaths ps@(_ : _)+  = Just (mconcat (printUnusedPath <$> ps))++printUnusedPath+  :: FilePath+  -> Text+printUnusedPath p+  = printMessageIndent (T.pack p) "unused file"++-- | Print a collection of unused items.+printUnusedItems+  :: UnusedItems+  -> Maybe Text+printUnusedItems (UnusedItems [])+  = Nothing+printUnusedItems (UnusedItems rs@(_ : _))+  = Just (foldMap (uncurry printRangeInfoWith) rs)++-- | Print a message indicating that no unused code was found.+printNothing+  :: Text+printNothing+  = T.unlines ["No unused code."]++printRangeInfoWith+  :: Range+  -> RangeInfo+  -> Text+printRangeInfoWith r i+  = printMessageIndent (printRange r) (printRangeInfo i)++printRangeInfo+  :: RangeInfo+  -> Text+printRangeInfo (RangeNamed t n)+  = T.unwords ["unused", printRangeType t, quote (printQName n)]+printRangeInfo RangeMutual+  = "unused mutually recursive definition"++printRangeType+  :: RangeType+  -> Text+printRangeType RangeData+  = "data type"+printRangeType RangeDefinition+  = "definition"+printRangeType RangeImport+  = "import"+printRangeType RangeImportItem+  = "imported item"+printRangeType RangeModule+  = "module"+printRangeType RangeModuleItem+  = "module assignment item"+printRangeType RangeOpen+  = "open"+printRangeType RangeOpenItem+  = "opened item"+printRangeType RangePatternSynonym+  = "pattern synonym"+printRangeType RangePostulate+  = "postulate"+printRangeType RangeRecord+  = "record"+printRangeType RangeRecordConstructor+  = "record constructor"+printRangeType RangeVariable+  = "variable"+
+ src/Agda/Unused/Types/Access.hs view
@@ -0,0 +1,55 @@+{- |+Module: Agda.Unused.Types.Access++Access modifiers indicating whether an item is public or private.+-}+module Agda.Unused.Types.Access++  ( -- * Definition+    +    Access(..)++    -- * Interface++  , access+   +    -- * Conversion++  , fromAccess++  ) where++import qualified Agda.Syntax.Common+  as C++-- | An access modifier.+data Access where++  Private+    :: Access++  Public+    :: Access++  deriving Show++-- | Elimination rule for 'Access'.+access+  :: a+  -> a+  -> Access+  -> a+access x _ Private+  = x+access _ y Public+  = y++-- | Conversion from Agda access type.+fromAccess+  :: C.Access+  -> Access+fromAccess (C.PrivateAccess _)+  = Private+fromAccess C.PublicAccess+  = Public+
+ src/Agda/Unused/Types/Context.hs view
@@ -0,0 +1,789 @@+{- |+Module: Agda.Unused.Types.Context++Definitions and interface for the 'Context' and 'AccessContext' types, which+represent namespaces of definitions.+-}+module Agda.Unused.Types.Context++  ( -- * Definitions++    Item+  , Module(Module)+  , AccessModule(AccessModule)+  , Context+  , AccessContext+  , accessContextUnion++    -- * Interface++    -- ** Lookup++  , LookupError(..)+  , contextLookup+  , contextLookupItem+  , contextLookupModule+  , accessContextLookup+  , accessContextLookupModule+  , accessContextLookupDefining+  , accessContextLookupSpecial+  +    -- ** Insert++  , contextInsertRange+  , contextInsertRangeModule+  , contextInsertRangeAll+  , accessContextInsertRangeAll++    -- ** Delete++  , contextDelete+  , contextDeleteModule++    -- ** Rename++  , contextRename+  , contextRenameModule++    -- ** Define++  , accessContextDefine++    -- ** Ranges++  , moduleRanges+  , contextRanges++    -- ** Match++  , accessContextMatch++    -- * Construction++  , item+  , itemPattern+  , itemConstructor+  , contextItem+  , contextModule+  , accessContextItem+  , accessContextModule+  , accessContextModule'+  , accessContextImport++    -- * Conversion++  , fromContext+  , toContext++  ) where++import Agda.Unused.Types.Access+  (Access(..))+import Agda.Unused.Types.Name+  (Name, QName(..), matchOperators, stripPrefix)+import Agda.Unused.Types.Range+  (Range)+import Agda.Unused.Utils+  (mapUpdateKey)++import Data.Map.Strict+  (Map)+import qualified Data.Map.Strict+  as Map+import Data.Maybe+  (catMaybes)++-- ## Definitions++-- | The data associated with a name in context. This includes:+--+-- - Whether the name is a constructor, pattern synonym, or ordinary definition.+-- - A list of ranges associated with the name, which includes the site of the+-- original definition, as well as any relevant @import@ or @open@ statements.+-- - Alternative syntax for the name, if any.+data Item where++  ItemConstructor+    :: ![Range]+    -> ![Name]+    -> Item++  ItemPattern+    :: ![Range]+    -> !(Maybe Name)+    -> Item++  Item+    :: ![Range]+    -> !(Maybe Name)+    -> Item++  deriving Show++-- Like 'Item', but with some additional data:+--+-- - Whether the name is public or private.+-- - Whether the name is currently being defined.+--+-- Since constructors may be overloaded, a constructor AccessItem may+-- represent multiple constructors, some public and some private.+data AccessItem where++  AccessItemConstructor+    -- Private ranges.+    :: ![Range]+    -- Public ranges.+    -> ![Range]+    -- Private syntax.+    -> ![Name]+    -- Public syntax.+    -> ![Name]+    -> AccessItem++  AccessItemPattern+    :: !Access+    -> ![Range]+    -> !(Maybe Name)+    -> AccessItem++  AccessItemSyntax+    -- Whether the item is special.+    :: !Bool+    -> ![Range]+    -> AccessItem++  AccessItem+    -- Whether we are currently defining this item.+    :: !Bool+    -> !Access+    -> ![Range]+    -> !(Maybe Name)+    -> AccessItem++  deriving Show++-- | The data associated with a module in context. This includes:+--+-- - A list of ranges associated with the module, which includes the site of the+-- original definition, as well as any relevant @import@ or @open@ statements.+-- - The inner context of the module.+data Module+  = Module+  { moduleRanges'+    :: ![Range]+  , moduleContext+    :: !Context+  } deriving Show++-- | Like 'Module', but also recording whether the module is public or private.+data AccessModule+  = AccessModule+  { accessModuleAccess+    :: !Access+  , accessModuleRanges+    :: ![Range]+  , accessModuleContext+    :: !Context+  } deriving Show++-- | A namespace of definitions. Any Agda module produces a 'Context'.+data Context+  = Context+  { contextItems+    :: !(Map Name Item)+  , contextModules+    :: !(Map Name Module)+  } deriving Show++-- | A namespace of definitions, which may be public or private. Any collection+-- of Agda declarations produces an 'AccessContext', for example.+data AccessContext+  = AccessContext+  { accessContextItems+    :: !(Map Name AccessItem)+  , accessContextModules+    :: !(Map Name AccessModule)+  , accessContextImports+    :: !(Map QName Context)+  } deriving Show++-- | If both items are constructors, collect the private and public ranges for+-- both. Otherwise, return the second item.+instance Semigroup AccessItem where+  AccessItemConstructor rs1 ss1 ts1 us1 <> AccessItemConstructor rs2 ss2 ts2 us2+    = AccessItemConstructor (rs1 <> rs2) (ss1 <> ss2) (ts1 <> ts2) (us1 <> us2)+  _ <> i+    = i++-- | Prefer values from second context.+instance Semigroup Context where+  Context is1 ms1 <> Context is2 ms2+    = Context (is2 <> is1) (ms2 <> ms1)++-- | Prefer values from second access context.+instance Semigroup AccessContext where+  AccessContext is1 ms1 js1 <> AccessContext is2 ms2 js2+    = AccessContext (Map.unionWith (<>) is1 is2) (ms2 <> ms1) (js2 <> js1)++instance Monoid Context where+  mempty+    = Context mempty mempty++instance Monoid AccessContext where+  mempty+    = AccessContext mempty mempty mempty++-- Ensure public names are not shadowed by private names.+accessItemUnion+  :: AccessItem+  -> AccessItem+  -> AccessItem+accessItemUnion i@(AccessItem _ Public _ _) (AccessItemConstructor _ [] _ _)+  = i+accessItemUnion i@(AccessItem _ Public _ _) (AccessItem _ Private _ _)+  = i+accessItemUnion i1 i2+  = i1 <> i2++-- Ensure public names are not shadowed by private names.+accessModuleUnion+  :: AccessModule+  -> AccessModule+  -> AccessModule+accessModuleUnion m1@(AccessModule Public _ _) (AccessModule Private _ _)+  = m1+accessModuleUnion _ m2+  = m2++-- | Like '(<>)', but public items take precedence over private items. This is+-- important when combining contexts from successive declarations; for example:+--+-- @ +-- module M where+--+--   postulate+--     A : Set+--+-- module N where+--+--   postulate+--     A : Set+--+--   open M+--+-- x : N.A+-- x = ?+-- @ +--+-- This code type-checks, and the identifier @N.A@ refers to the postulate+-- declared in the definition of @N@, not the definition opened from @M@.+accessContextUnion+  :: AccessContext+  -> AccessContext+  -> AccessContext+accessContextUnion (AccessContext is1 ms1 js1) (AccessContext is2 ms2 js2)+  = AccessContext+  { accessContextItems+    = Map.unionWith accessItemUnion is1 is2+  , accessContextModules+    = Map.unionWith accessModuleUnion ms1 ms2+  , accessContextImports+    = js2 <> js1+  }++-- ## Interface++-- ### Lookup++-- | A description of failure for an 'AccessContext' lookup.+data LookupError where++  LookupNotFound+    :: LookupError++  LookupAmbiguous+    :: LookupError++  deriving Show++-- | Get the ranges for the given name, or 'Nothing' if not in context.+contextLookup+  :: QName+  -> Context+  -> Maybe [Range]+contextLookup n c+  = itemRanges <$> contextLookupItem n c++-- | Get the inner module for the given name, or 'Nothing' if not in context.+contextLookupModule+  :: QName+  -> Context+  -> Maybe Module+contextLookupModule (QName n) (Context _ ms)+  = Map.lookup n ms+contextLookupModule (Qual n ns) (Context _ ms)+  = Map.lookup n ms >>= contextLookupModule ns . moduleContext++-- | Get the item for the given name, or 'Nothing' if not in context.+contextLookupItem+  :: QName+  -> Context+  -> Maybe Item+contextLookupItem (QName n) (Context is _)+  = Map.lookup n is+contextLookupItem (Qual n ns) (Context _ ms)+  = Map.lookup n ms >>= contextLookupItem ns . moduleContext++-- | Get the ranges for the given name, or produce a 'LookupError'.+accessContextLookup+  :: QName+  -> AccessContext+  -> Either LookupError [Range]+accessContextLookup n c@(AccessContext _ _ is)+  = contextLookup n (toContext' c)+  <|> Map.mapWithKey (accessContextLookupImport n) is++-- | Get the inner module for the given name, or produce a 'LookupError'.+accessContextLookupModule+  :: QName+  -> AccessContext+  -> Either LookupError Module+accessContextLookupModule n c@(AccessContext _ _ is)+  = contextLookupModule n (toContext' c)+  <|> Map.mapWithKey (accessContextLookupModuleImport n) is++accessContextLookupImport+  :: QName+  -> QName+  -> Context+  -> Maybe [Range]+accessContextLookupImport n i c+  = stripPrefix i n >>= flip contextLookup c++accessContextLookupModuleImport+  :: QName+  -> QName+  -> Context+  -> Maybe Module+accessContextLookupModuleImport n i c | n == i+  = Just (Module [] c)+accessContextLookupModuleImport n i c+  = stripPrefix i n >>= flip contextLookupModule c++(<|>)+  :: Maybe a+  -> Map k (Maybe a)+  -> Either LookupError a+x <|> xs+  = resolve (catMaybes (x : Map.elems xs))++resolve+  :: [a]+  -> Either LookupError a+resolve []+  = Left LookupNotFound+resolve (x : [])+  = Right x+resolve (_ : _ : _)+  = Left LookupAmbiguous++accessItemDefining+  :: AccessItem+  -> Bool+accessItemDefining (AccessItem b _ _ _)+  = b+accessItemDefining _+  = False++-- | Like 'accessContextLookup', but also return a boolean indicating whether we+-- are currently defining the referenced item.+accessContextLookupDefining+  :: QName+  -> AccessContext+  -> Either LookupError (Bool, [Range])+accessContextLookupDefining (QName n) (AccessContext is _ _)+  = maybe+    (Left LookupNotFound)+    (\i -> Right (accessItemDefining i, accessItemRanges i))+    (Map.lookup n is)+accessContextLookupDefining n@(Qual _ _) c+  = (,) False <$> accessContextLookup n c++itemSpecial+  :: Item+  -> Bool+itemSpecial (ItemConstructor _ _)+  = True+itemSpecial (ItemPattern _ _)+  = True+itemSpecial (Item _ _)+  = False++-- | Determine whether a name represents a constructor or pattern synonym.+-- Return 'Nothing' if the name is not in context.+accessContextLookupSpecial+  :: QName+  -> AccessContext+  -> Maybe Bool+accessContextLookupSpecial n c+  = itemSpecial <$> contextLookupItem n (toContext' c)++-- ### Insert++itemInsertRange+  :: Range+  -> Item+  -> Item+itemInsertRange r (ItemConstructor rs ss)+  = ItemConstructor (r : rs) ss+itemInsertRange r (ItemPattern rs s)+  = ItemPattern (r : rs) s+itemInsertRange r (Item rs s)+  = Item (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)++moduleInsertRangeAll+  :: Range+  -> Module+  -> Module+moduleInsertRangeAll r (Module rs c)+  = Module (r : rs) (contextInsertRangeAll r c)++accessModuleInsertRangeAll+  :: Range+  -> AccessModule+  -> AccessModule+accessModuleInsertRangeAll r (AccessModule a rs c)+  = AccessModule a (r : rs) (contextInsertRangeAll r c)++-- | Insert a range for all names in a context.+contextInsertRangeAll+  :: Range+  -> Context+  -> Context+contextInsertRangeAll r (Context is ms)+  = Context+    (itemInsertRange r <$> is)+    (moduleInsertRangeAll r <$> ms)++-- | Insert a range for all names in an access context.+accessContextInsertRangeAll+  :: Range+  -> AccessContext+  -> AccessContext+accessContextInsertRangeAll r (AccessContext is ms js)+  = AccessContext+    (accessItemInsertRange r <$> is)+    (accessModuleInsertRangeAll r <$> ms) js++-- ### Delete++-- | Delete an item from the context.+contextDelete+  :: Name+  -> Context+  -> Context+contextDelete n (Context is ms)+  = Context (Map.delete n is) ms++-- | Delete a module from the context.+contextDeleteModule+  :: Name+  -> Context+  -> Context+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+accessItemDefine i+  = i++-- | Mark an existing name as in process of being defined.+accessContextDefine+  :: Name+  -> AccessContext+  -> AccessContext+accessContextDefine n (AccessContext is ms js)+  = AccessContext (Map.adjust accessItemDefine n is) ms js++-- ### Ranges++itemRanges+  :: Item+  -> [Range]+itemRanges (ItemConstructor rs _)+  = rs+itemRanges (ItemPattern rs _)+  = rs+itemRanges (Item rs _)+  = rs++accessItemRanges+  :: AccessItem+  -> [Range]+accessItemRanges+  = itemRanges . toItem'++-- | Get all ranges associated with names in the given module, including ranges+-- associated with the module itself.+moduleRanges+  :: Module+  -> [Range]+moduleRanges (Module rs c)+  = rs <> contextRanges c++-- | Get all ranges associated with names in the given context.+contextRanges+  :: Context+  -> [Range]+contextRanges (Context is ms)+  = concat (itemRanges <$> Map.elems is)+  <> concat (moduleRanges <$> Map.elems ms)++-- ### Match++-- | Find all operators matching the given list of tokens.+accessContextMatch+  :: [String]+  -> AccessContext+  -> [Name]+accessContextMatch ss (AccessContext is _ _)+  = matchOperators ss (Map.keys is)++-- ## 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+  -> Item+  -> Context+contextItem n i+  = Context (Map.singleton n i) mempty++-- | Construct a 'Context' with a single module.+contextModule+  :: Name+  -> Module+  -> Context+contextModule n m+  = Context mempty (Map.singleton n m)++-- | Construct an 'AccessContext' with a single item, along with the relevant+-- syntax item if applicable.+accessContextItem+  :: Name+  -> Access+  -> Item+  -> AccessContext+accessContextItem n a i+  = fromContext a (contextItem n i)++-- | Construct an 'AccessContext' with a single access module.+accessContextModule+  :: Name+  -> AccessModule+  -> AccessContext+accessContextModule n m+  = AccessContext mempty (Map.singleton n m) mempty++-- | Like 'accessContextModule', but taking an access context. We convert the+-- given access context to an ordinary context using 'toContext':+--+-- @+-- accessContextModule' n a rs c+--   = accessContextModule n (AccessModule a rs (toContext c))+-- @+accessContextModule'+  :: Name+  -> Access+  -> [Range]+  -> AccessContext+  -> AccessContext+accessContextModule' n a rs c+  = accessContextModule n (AccessModule a rs (toContext c))++-- | Construct an access context with a single import.+accessContextImport+  :: QName+  -> Context+  -> AccessContext+accessContextImport n c+  = AccessContext mempty mempty (Map.singleton n c)++-- ## Conversion++fromItem+  :: Access+  -> Item+  -> AccessItem+fromItem Private (ItemConstructor rs ss)+  = AccessItemConstructor rs [] ss []+fromItem Public (ItemConstructor rs ss)+  = AccessItemConstructor [] rs [] ss+fromItem a (ItemPattern rs s)+  = AccessItemPattern a rs s+fromItem a (Item rs s)+  = AccessItem False a rs s++fromItemSyntax+  :: Item+  -> [(Name, AccessItem)]+fromItemSyntax (ItemConstructor rs ss)+  = flip (,) (AccessItemSyntax True rs) <$> ss+fromItemSyntax (ItemPattern rs s)+  = flip (,) (AccessItemSyntax True rs) <$> maybe [] (: []) s+fromItemSyntax (Item rs s)+  = flip (,) (AccessItemSyntax False rs) <$> maybe [] (: []) s++toItem+  :: AccessItem+  -> Maybe Item+toItem (AccessItemConstructor _ rs@(_ : _) _ ss)+  = Just (ItemConstructor rs ss)+toItem (AccessItemPattern Public rs s)+  = Just (ItemPattern rs s)+toItem (AccessItem _ Public rs s)+  = Just (Item rs s)+toItem _+  = Nothing++toItem'+  :: AccessItem+  -> Item+toItem' (AccessItemConstructor rs1 rs2 ss1 ss2)+  = ItemConstructor (rs1 <> rs2) (ss1 <> ss2)+toItem' (AccessItemPattern _ rs s)+  = ItemPattern rs s+toItem' (AccessItemSyntax _ rs)+  = Item rs Nothing+toItem' (AccessItem _ _ rs s)+  = Item rs s++fromModule+  :: Access+  -> Module+  -> AccessModule+fromModule a (Module rs c)+  = AccessModule a rs c++toModule+  :: AccessModule+  -> Maybe Module+toModule (AccessModule Private _ _)+  = Nothing+toModule (AccessModule Public rs c)+  = Just (Module rs c)++toModule'+  :: AccessModule+  -> Module+toModule' (AccessModule _ rs c)+  = Module rs c++-- | Convert a 'Context' to 'AccessContext'. Give all items the given access.+fromContext+  :: Access+  -> Context+  -> AccessContext+fromContext a (Context is ms)+  = AccessContext+    (Map.map (fromItem a) is <> Map.fromList (Map.elems is >>= fromItemSyntax))+    (Map.map (fromModule a) ms)+    mempty++-- | Convert an 'AccessContext' to 'Context'. Discard private items and imports.+toContext+  :: AccessContext+  -> Context+toContext (AccessContext is ms _)+  = Context (Map.mapMaybe toItem is) (Map.mapMaybe toModule ms)++-- Like 'toContext`, but keep private items.+toContext'+  :: AccessContext+  -> Context+toContext' (AccessContext is ms _)+  = Context (Map.map toItem' is) (Map.map toModule' ms)+
+ src/Agda/Unused/Types/Name.hs view
@@ -0,0 +1,235 @@+{- |+Module: Agda.Unused.Types.Name++Names and qualified names.+-}+module Agda.Unused.Types.Name++  ( -- * Definitions++    NamePart(..)+  , Name(..)+  , QName(..)++    -- * Interface++  , nameIds+  , isBuiltin+  , stripPrefix++    -- * Conversion++  , fromName+  , fromNameRange+  , fromQName+  , fromQNameRange+  , fromAsName++    -- * Paths++  , qNamePath+  , pathQName++    -- * Match++  , matchOperators++  ) where++import Agda.Unused.Utils+  (stripSuffix)++import Agda.Syntax.Concrete+  (AsName, AsName'(..))+import Agda.Syntax.Concrete.Name+  (NamePart(..))+import qualified Agda.Syntax.Concrete.Name+  as N+import Agda.Syntax.Position+  (Range)+import Data.List+  (isSubsequenceOf)+import qualified Data.List+  as List+import Data.Maybe+  (mapMaybe)+import System.FilePath+  ((</>), (<.>), splitDirectories)++-- ## Definitions++-- | An unqualified name, represented as a list of name parts.+newtype Name+  = Name+  { nameParts+    :: [NamePart]+  } deriving (Eq, Ord, Show)++-- | A qualified name.+data QName where++  QName+    :: !Name+    -> QName++  Qual+    :: !Name+    -> !QName+    -> QName++  deriving (Eq, Ord, Show)++-- ## Interface++-- | Get the non-hole parts of a 'Name'.+nameIds+  :: Name+  -> [String]+nameIds (Name ps)+  = mapMaybe namePartId ps++namePartId+  :: NamePart+  -> Maybe String+namePartId Hole+  = Nothing+namePartId (Id s)+  = Just s++isOperator+  :: Name+  -> Bool+isOperator (Name [])+  = False+isOperator (Name (_ : []))+  = False+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+  :: QName+  -- ^ The prefix to strip+  -> QName+  -> Maybe QName+stripPrefix (QName m) (Qual n ns) | m == n+  = Just ns+stripPrefix (Qual m ms) (Qual n ns) | m == n+  = stripPrefix ms ns+stripPrefix _ _+  = Nothing++-- ## Conversion++-- | Conversion from Agda name type.+fromName+  :: N.Name+  -> Maybe Name+fromName (N.NoName _ _)+  = Nothing+fromName (N.Name _ _ n)+  = Just (Name n)++-- | Like 'fromName', but also return a 'Range'.+fromNameRange+  :: N.Name+  -> Maybe (Range, Name)+fromNameRange (N.NoName _ _)+  = Nothing+fromNameRange (N.Name r _ n)+  = Just (r, Name n)++-- | Conversion from Agda qualified name type.+fromQName+  :: N.QName+  -> Maybe QName+fromQName (N.QName n)+  = QName <$> fromName n+fromQName (N.Qual n ns)+  = Qual <$> fromName n <*> fromQName ns++-- | Like 'fromQName', but also return a 'Range'.+fromQNameRange+  :: N.QName+  -> Maybe (Range, QName)+fromQNameRange (N.QName n)+  = fmap QName <$> fromNameRange n+fromQNameRange (N.Qual n ns)+  = fmap . Qual <$> fromName n <*> fromQNameRange ns++-- | Conversion from Agda as-name type.+fromAsName+  :: AsName+  -> Maybe Name+fromAsName (AsName (Left _) _)+  = Nothing+fromAsName (AsName (Right n) _)+  = fromName n++-- ## Paths++namePath+  :: Name+  -> String+namePath (Name ps)+  = mconcat (show <$> ps)++-- | Convert a module name to a 'FilePath'.+qNamePath+  :: QName+  -> FilePath+qNamePath (QName n)+  = namePath n <.> "agda"+qNamePath (Qual n ns)+  = namePath n </> qNamePath ns++-- | Convert a 'FilePath' to a module name.+pathQName+  :: FilePath+  -- ^ The project root directory.+  -> FilePath+  -- ^ The path to the module.+  -> Maybe QName+pathQName p p'+  = List.stripPrefix (splitDirectories p) (splitDirectories p')+  >>= pathQNameRelative++pathQNameRelative+  :: [String]+  -> Maybe QName+pathQNameRelative []+  = Nothing+pathQNameRelative [n]+  = QName <$> pathName n+pathQNameRelative (n : ns@(_ : _))+  = Qual (Name [Id n]) <$> pathQNameRelative ns++pathName+  :: String+  -> Maybe Name+pathName n+  = Name . (: []) . Id <$> stripSuffix ".agda" n++-- ## Match++-- | Given a string of tokens found in a raw application, filter the given list+-- of names by whether each name's identifiers appear in order.+matchOperators+  :: [String]+  -- ^ A string of tokens found in a raw application.+  -> [Name]+  -- ^ A list of names to consider.+  -> [Name]+matchOperators ss+  = filter (\n -> isOperator n && isSubsequenceOf (nameIds n) ss)+
+ src/Agda/Unused/Types/Range.hs view
@@ -0,0 +1,107 @@+{- |+Module: Agda.Unused.Types.Range++Location ranges of Agda code files.+-}+module Agda.Unused.Types.Range++  ( -- * Definitions++    Range+  , Range'(..)+  , RangeType(..)+  , RangeInfo(..)++    -- * Interface++  , getRange+  , rangeContains++  ) where++import Agda.Unused.Types.Name+  (QName)++import Agda.Syntax.Position+  (PositionWithoutFile, Range, Range'(..), getRange, rEnd', rStart')++-- ## Definitions++-- | The type of item found at a named range.+data RangeType where++  RangeData+    :: RangeType++  RangeDefinition+    :: RangeType++  RangeImport+    :: RangeType++  RangeImportItem+    :: RangeType++  RangeModule+    :: RangeType++  RangeModuleItem+    :: RangeType++  RangeOpen+    :: RangeType++  RangeOpenItem+    :: RangeType++  RangePatternSynonym+    :: RangeType++  RangePostulate+    :: RangeType++  RangeRecord+    :: RangeType++  RangeRecordConstructor+    :: RangeType++  RangeVariable+    :: RangeType++  deriving (Eq, Ord, Show)++-- | Information associated with an item found at a certain range.+data RangeInfo where++  RangeNamed+    :: !RangeType+    -> !QName+    -> RangeInfo++  RangeMutual+    :: RangeInfo++  deriving (Eq, Ord, Show)++-- ## Interface++-- | Determine whether the first range contains the second.+rangeContains+  :: Range+  -> Range+  -> Bool+rangeContains r1 r2+  = rangeContains' (rStart' r1) (rEnd' r1) (rStart' r2) (rEnd' r2)++rangeContains'+  :: Maybe PositionWithoutFile+  -> Maybe PositionWithoutFile+  -> Maybe PositionWithoutFile+  -> Maybe PositionWithoutFile+  -> Bool+rangeContains' (Just s1) (Just e1) (Just s2) (Just e2)+  = s1 <= s2 && e1 >= e2+rangeContains' _ _ _ _+  = False+
+ src/Agda/Unused/Types/Root.hs view
@@ -0,0 +1,53 @@+{- |+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)+
+ src/Agda/Unused/Utils.hs view
@@ -0,0 +1,95 @@+{- |+Module: Agda.Unused.Utils++Utility functions for 'Maybe', 'Either', and 'Map' types.+-}+module Agda.Unused.Utils++  ( -- * Maybe++    liftMaybe++    -- * Either++  , mapLeft++    -- * List++  , 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++-- | Lift a 'Maybe' type to an error monad by throwing a fixed error.+liftMaybe+  :: MonadError e m+  => e+  -> Maybe a+  -> m a+liftMaybe e Nothing+  = throwError e+liftMaybe _ (Just x)+  = pure x++-- ## Either++-- | Map the left component of an 'Either' type.+mapLeft+  :: (e -> f)+  -> Either e a+  -> Either f a+mapLeft f (Left e)+  = Left (f e)+mapLeft _ (Right x)+  = Right x++-- ## List++-- | Drop the given suffix from a list.+stripSuffix+  :: Eq a+  => [a]+  -> [a]+  -> 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)+
+ test/Main.hs view
@@ -0,0 +1,766 @@+module Main where++import Agda.Unused+  (Unused(..), UnusedItems(..))+import Agda.Unused.Check+  (checkUnused, checkUnusedLocal)+import Agda.Unused.Monad.Error+  (Error)+import Agda.Unused.Print+  (printUnusedItems)+import Agda.Unused.Types.Access+  (Access(..))+import Agda.Unused.Types.Name+  (Name(..), NamePart(..), QName(..))+import Agda.Unused.Types.Range+  (RangeInfo(..))+import qualified Agda.Unused.Types.Range+  as R+import Agda.Unused.Types.Root+  (Root(..), Roots(..))++import Data.Maybe+  (mapMaybe)+import qualified Data.Set+  as Set+import Data.Text+  (Text)+import qualified Data.Text+  as T+import System.FilePath+  ((</>))+import Test.Hspec+  (Expectation, Spec, describe, expectationFailure, hspec, it, shouldBe,+    shouldSatisfy)++import Paths_agda_unused+  (getDataFileName)++-- ## 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)++land+  :: QName+land+  = QName (Name [Hole, Id "&&", Hole])++bind+  :: QName+bind+  = QName (Name [Hole, Id ">>=", Hole])++bind_+  :: QName+bind_+  = QName (Name [Hole, Id ">>", Hole])++agdaBuiltinBool+  :: QName+agdaBuiltinBool+  = Qual (Name [Id "Agda"])+  $ Qual (Name [Id "Builtin"])+  $ QName (Name [Id "Bool"])++-- ## Ranges++data RangeType where++  Data+    :: RangeType++  Definition+    :: RangeType++  Import+    :: RangeType++  ImportItem+    :: RangeType++  Module+    :: RangeType++  ModuleItem+    :: RangeType++  Mutual+    :: RangeType++  Open+    :: RangeType++  OpenItem+    :: RangeType++  PatternSynonym+    :: RangeType++  Postulate+    :: RangeType++  Record+    :: RangeType++  RecordConstructor+    :: RangeType++  Variable+    :: RangeType++  deriving Show++(~:)+  :: IsName a+  => a+  -> 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))++-- ## Expectations++testCheck+  :: Test+  -> Expectation+testCheck n = do+  path+    <- testPath n+  unused+    <- checkUnused path (Roots [Root (name (testModule n)) (Just [])] [])+  unusedLocal+    <- checkUnusedLocal path (name (testModule n))+  _+    <- testUnused (unusedItems <$> unused) (snd <$> testResult n)+  _+    <- testUnused unusedLocal (mapMaybe privateMay (testResult n))+  pure ()++testCheckExample+  :: Expectation+testCheckExample = do+  path+    <- getDataFileName "data/test/example"+  unusedLocal+    <- checkUnusedLocal path (name "Test")+  _+    <- testUnusedExample unusedLocal+  pure ()++testUnused+  :: Either Error UnusedItems+  -> [RangeInfo]+  -> Expectation+testUnused (Left _) _+  = expectationFailure ""+testUnused (Right (UnusedItems is)) rs+  = Set.fromList (snd <$> is) `shouldBe` Set.fromList rs++testUnusedExample+  :: Either Error UnusedItems+  -> Expectation+testUnusedExample (Left _)+  = expectationFailure ""+testUnusedExample (Right is)+  = testUnusedOutput (T.lines <$> printUnusedItems is)++testUnusedOutput+  :: 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’")+testUnusedOutput _+  = expectationFailure ""++privateMay+  :: (Access, a)+  -> Maybe a+privateMay (Private, x)+  = Just x+privateMay (Public, _)+  = Nothing++-- ## Tests++data Test where++  Pattern+    :: !PatternTest+    -> Test++  Expression+    :: !ExpressionTest+    -> Test++  Declaration+    :: !DeclarationTest+    -> Test++  deriving Show++data PatternTest where++  IdentP+    :: PatternTest ++  OpAppP+    :: PatternTest++  AsP+    :: PatternTest++  deriving Show++data ExpressionTest where++  WithApp+    :: ExpressionTest++  Lam+    :: ExpressionTest++  ExtendedLam+    :: ExpressionTest++  Pi+    :: ExpressionTest++  Let+    :: ExpressionTest++  DoBlock1+    :: ExpressionTest++  DoBlock2+    :: ExpressionTest++  DoBlock3+    :: ExpressionTest++  DoBlock4+    :: ExpressionTest++  deriving Show++data DeclarationTest where++  TypeSig+    :: DeclarationTest++  FunClause+    :: DeclarationTest++  Data'+    :: DeclarationTest++  Record'+    :: DeclarationTest++  Syntax+    :: DeclarationTest++  PatternSyn+    :: DeclarationTest++  Mutual1+    :: DeclarationTest++  Mutual2+    :: DeclarationTest++  Abstract+    :: DeclarationTest++  Private'+    :: DeclarationTest++  Postulate'+    :: DeclarationTest++  Open'+    :: DeclarationTest++  Import'+    :: DeclarationTest++  ModuleMacro+    :: DeclarationTest++  Module'+    :: DeclarationTest++  deriving Show++testDir+  :: Test+  -> FilePath+testDir (Pattern _)+  = "pattern"+testDir (Expression _)+  = "expression"+testDir (Declaration _)+  = "declaration"++testPath+  :: Test+  -> IO FilePath+testPath n+  = getDataFileName ("data/test" </> testDir n)++testModule+  :: Test+  -> String+testModule (Pattern IdentP)+  = "IdentP"+testModule (Pattern OpAppP)+  = "OpAppP"+testModule (Pattern AsP)+  = "AsP"+testModule (Expression WithApp)+  = "WithApp"+testModule (Expression Lam)+  = "Lam"+testModule (Expression ExtendedLam)+  = "ExtendedLam"+testModule (Expression Pi)+  = "Pi"+testModule (Expression Let)+  = "Let"+testModule (Expression DoBlock1)+  = "DoBlock1"+testModule (Expression DoBlock2)+  = "DoBlock2"+testModule (Expression DoBlock3)+  = "DoBlock3"+testModule (Expression DoBlock4)+  = "DoBlock4"+testModule (Declaration TypeSig)+  = "TypeSig"+testModule (Declaration FunClause)+  = "FunClause"+testModule (Declaration Data')+  = "Data"+testModule (Declaration Record')+  = "Record"+testModule (Declaration Syntax)+  = "Syntax"+testModule (Declaration PatternSyn)+  = "PatternSyn"+testModule (Declaration Mutual1)+  = "Mutual1"+testModule (Declaration Mutual2)+  = "Mutual2"+testModule (Declaration Abstract)+  = "Abstract"+testModule (Declaration Private')+  = "Private"+testModule (Declaration Postulate')+  = "Postulate"+testModule (Declaration Open')+  = "Open"+testModule (Declaration Import')+  = "Import"+testModule (Declaration ModuleMacro)+  = "ModuleMacro"+testModule (Declaration Module')+  = "Module"++testResult+  :: Test+  -> [(Access, RangeInfo)]+testResult n+  = case n of++  Pattern IdentP ->+    [ private "y"+      ~: Variable+    , "f"+      ~: Definition+    , "g"+      ~: Definition+    ]++  Pattern OpAppP ->+    [ land+      ~: Definition+    ]++  Pattern AsP ->+    [ private "y"+      ~: Variable+    , private "z"+      ~: Variable+    , private "w"+      ~: Variable+    , private "z'"+      ~: Variable+    , private "w'"+      ~: Variable+    , "f"+      ~: Definition+    , "g"+      ~: Definition+    ]++  Expression WithApp ->+    [ "f"+      ~: Definition+    , "g"+      ~: Definition+    ]++  Expression Lam ->+    [ private "y"+      ~: Variable+    , private "y'"+      ~: Variable+    , "f"+      ~: Definition+    , "g"+      ~: Definition+    ]++  Expression ExtendedLam ->+    [ private "x"+      ~: Variable+    , "f"+      ~: Definition+    ]++  Expression Pi ->+    [ private "y"+      ~: Variable+    , private "w"+      ~: Variable+    , "f"+      ~: Definition+    ]++  Expression Let ->+    [ private "z"+      ~: Definition+    , "f"+      ~: Definition+    ]++  Expression DoBlock1 ->+    [ private "z"+      ~: Variable+    , "f"+      ~: Definition+    ]++  Expression DoBlock2 ->+    [ bind_+      ~: Definition+    , "f"+      ~: Definition+    ]++  Expression DoBlock3 ->+    [ bind+      ~: Definition+    , "f"+      ~: Definition+    ]++  Expression DoBlock4 ->+    [ bind+      ~: Definition+    , bind_+      ~: Definition+    , "f"+      ~: Definition+    ]++  Declaration TypeSig ->+    [ "g"+      ~: Definition+    , "h"+      ~: Definition+    ]++  Declaration FunClause ->+    [ private "z"+      ~: Definition+    , "f"+      ~: Definition+    , "snoc"+      ~: Definition+    ]++  Declaration Data' ->+    [ "D"+      ~: Data+    ]++  Declaration Record' ->+    [ "B"+      ~: Record+    , "c"+      ~: RecordConstructor+    , "x"+      ~: Definition+    , "y"+      ~: Definition+    ]++  Declaration Syntax ->+    [ "p1"+      ~: Postulate+    , "p1'"+      ~: Postulate+    ]++  Declaration PatternSyn ->+    [ "q"+      ~: PatternSynonym+    , "f"+      ~: Definition+    , "g"+      ~: Definition+    ]++  Declaration Mutual1 ->+    [ "_"+      ~: Mutual+    ]++  Declaration Mutual2 ->+    [ "is-even'"+      ~: Definition+    ]++  Declaration Abstract ->+    [ "g"+      ~: Definition+    , "h"+      ~: Definition+    ]++  Declaration Private' ->+    [ private "g"+      ~: Definition+    , private "h"+      ~: Definition+    ]++  Declaration Postulate' ->+    [ "g"+      ~: Postulate+    , "h"+      ~: Definition+    ]++  Declaration Open' ->+    [ private "N"+      ~: Open+    , private "P"+      ~: Open+    , "Q"+      ~: Module+    , private "x'"+      ~: OpenItem+    , "v"+      ~: Definition+    , "y"+      ~: Definition+    ]++  Declaration Import' ->+    [ private agdaBuiltinBool+      ~: Import+    , private "tt"+      ~: ImportItem+    , "A"+      ~: Definition+    ]++  Declaration ModuleMacro ->+    [ private "x"+      ~: Variable+    , "Q"+      ~: Module+    , "A'"+      ~: ModuleItem+    , "C"+      ~: Definition+    , "D"+      ~: Definition+    , "y"+      ~: Definition+    ]++  Declaration Module' ->+    [ "O"+      ~: Module+    , "P"+      ~: Module+    , "x"+      ~: Definition+    ]++-- ## Main++main+  :: IO ()+main+  = hspec testAll++testAll+  :: Spec+testAll+  = describe "checkUnused"+  $ testPattern+  >> testExpression+  >> testDeclaration+  >> testExample++testPattern+  :: Spec+testPattern+  = describe "patterns"+  $ it "checks identifiers (IdentP)"+    (testCheck (Pattern IdentP))+  >> it "checks operator applications (OpAppP)"+    (testCheck (Pattern OpAppP))+  >> it "checks as-patterns (AsP)"+    (testCheck (Pattern AsP))++testExpression+  :: Spec+testExpression+  = describe "expressions"+  $ it "checks with-applications (WithApp)"+    (testCheck (Expression WithApp))+  >> it "checks lambdas (Lam)"+    (testCheck (Expression Lam))+  >> it "checks extended lambdas (ExtendedLam)"+    (testCheck (Expression ExtendedLam))+  >> it "checks pi-types (Pi)"+    (testCheck (Expression Pi))+  >> it "checks let-blocks (Let)"+    (testCheck (Expression Let))+  >> it "checks do-blocks (DoBlock)"+    (testCheck (Expression DoBlock1)+    >> testCheck (Expression DoBlock2)+    >> testCheck (Expression DoBlock3)+    >> testCheck (Expression DoBlock4))++testDeclaration+  :: Spec+testDeclaration+  = describe "declarations"+  $ it "checks type signatures (TypeSig)"+    (testCheck (Declaration TypeSig))+  >> it "checks function clauses (FunClause)"+    (testCheck (Declaration FunClause))+  >> it "checks data declarations (Data)"+    (testCheck (Declaration Data'))+  >> it "checks record declarations (Record)"+    (testCheck (Declaration Record'))+  >> it "checks syntax declarations (Syntax)"+    (testCheck (Declaration Syntax))+  >> it "checks pattern synonyms (PatternSyn)"+    (testCheck (Declaration PatternSyn))+  >> it "checks mutual blocks (Mutual)"+    (testCheck (Declaration Mutual1)+    >> testCheck (Declaration Mutual2))+  >> it "checks abstract blocks (Abstract)"+    (testCheck (Declaration Abstract))+  >> it "checks private blocks (Private)"+    (testCheck (Declaration Private'))+  >> it "checks postulates (Postulate)"+    (testCheck (Declaration Postulate'))+  >> it "checks open statements (Open)"+    (testCheck (Declaration Open'))+  >> it "checks import statements (Import)"+    (testCheck (Declaration Import'))+  >> it "checks module macros (ModuleMacro)"+    (testCheck (Declaration ModuleMacro))+  >> it "checks module definitions (Module)"+    (testCheck (Declaration Module'))++testExample+  :: Spec+testExample+  = describe "example"+  $ it "outputs the text in README.md"+  $ testCheckExample+