packages feed

agda-unused 0.2.0 → 0.3.0

raw patch · 16 files changed

+356/−234 lines, 16 filesdep ~Agdadep ~aesondep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: Agda, aeson, base, hspec, mtl, optparse-applicative, text

API changes (from Hackage documentation)

- Agda.Unused.Types.Range: NoRange :: Range' a
- Agda.Unused.Types.Range: Range :: !a -> Seq IntervalWithoutFile -> Range' a
- Agda.Unused.Types.Range: data Range' a
- Agda.Unused.Types.Range: getRange :: HasRange t => t -> Range
- Agda.Unused.Types.Range: type Range = Range' SrcFile
+ Agda.Unused.Monad.Error: [UnsupportedLoneConstructor] :: UnsupportedError
- Agda.Unused.Types.Name: Name :: [NamePart] -> Name
+ Agda.Unused.Types.Name: Name :: NonEmpty NamePart -> Name
- Agda.Unused.Types.Name: [nameParts] :: Name -> [NamePart]
+ Agda.Unused.Types.Name: [nameParts] :: Name -> NonEmpty NamePart
- Agda.Unused.Types.Name: fromModuleName :: TopLevelModuleName -> Maybe QName
+ Agda.Unused.Types.Name: fromModuleName :: TopLevelModuleName -> QName

Files

CHANGELOG.md view
@@ -17,3 +17,7 @@ - Check record types with fields referencing other fields (fixes bug). - Check import statements with `as _` (fixes bug). +## 0.3.0 (Nov 2022)++- Support Agda 2.6.2; remove support for earlier versions.+
README.md view
@@ -15,9 +15,9 @@ not check public items that could be imported elsewhere. But with the `--global` flag, `agda-unused` treats the given file as a description of the public interface of the project, and additionally checks for unused files and unused-public items in dependencies. (See below for more on the `--global` flag.)+public items in dependencies. (See below for more on `--global`.) -Supported Agda versions: `>= 2.6.1 && < 2.6.2`+Supported Agda versions: `>= 2.6.2 && < 2.6.3`  ## Example @@ -122,11 +122,10 @@ - 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.+depending on the previous one, then `f` and `g` are considered used, while `h`+is considered unused. If we remove `h` and run `agda-unused` 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.  ## Limitations @@ -143,8 +142,9 @@  Additionally, we currently do not support the following Agda features: -- [record module instance applications](https://agda.readthedocs.io/en/v2.6.1.3/language/module-system.html#parameterised-modules)-- [unquoting declarations](https://agda.readthedocs.io/en/v2.6.1.3/language/reflection.html#id3)+- [record module instance applications](https://agda.readthedocs.io/en/v2.6.2/language/module-system.html#parameterised-modules)+- [unquoting declarations](https://agda.readthedocs.io/en/v2.6.2/language/reflection.html#id3)+- [lone constructors](https://agda.readthedocs.io/en/v2.6.2/language/mutual-recursion.html#interleaved-mutual-blocks)  `agda-unused` will produce an error if your code uses these language features.
agda-unused.cabal view
@@ -3,7 +3,7 @@ name:   agda-unused version:-  0.2.0+  0.3.0 build-type:   Simple license:@@ -46,13 +46,13 @@     Agda.Unused.Types.Range     Agda.Unused.Utils   build-depends:-    base >= 4.13 && < 4.15,-    Agda >= 2.6.1 && < 2.6.2,+    base >= 4.13 && < 4.18,+    Agda >= 2.6.2 && < 2.6.3,     containers >= 0.6.2 && < 0.7,     directory >= 1.3.6 && < 1.4,     filepath >= 1.4.2 && < 1.5,-    mtl >= 2.2.2 && < 2.3,-    text >= 1.2.4 && < 1.3+    mtl >= 2.2.2 && < 2.4,+    text >= 1.2.4 && < 2.1   default-language:     Haskell2010   default-extensions:@@ -71,12 +71,12 @@     Main.hs   build-depends:     agda-unused,-    base >= 4.13 && < 4.15,-    aeson >= 1.4.7 && < 1.6,+    base >= 4.13 && < 4.18,+    aeson >= 2 && < 2.2,     directory >= 1.3.6 && < 1.4,-    mtl >= 2.2.2 && < 2.3,-    optparse-applicative >= 0.15.1 && < 0.17,-    text >= 1.2.4 && < 1.3+    mtl >= 2.2.2 && < 2.4,+    optparse-applicative >= 0.15.1 && < 0.18,+    text >= 1.2.4 && < 2.1   default-language:     Haskell2010   default-extensions:@@ -99,11 +99,11 @@     Paths_agda_unused   build-depends:     agda-unused,-    base >= 4.13 && < 4.15,+    base >= 4.13 && < 4.18,     containers >= 0.6.2 && < 0.7,     filepath >= 1.4.2 && < 1.5,-    hspec >= 2.7.1 && < 2.8,-    text >= 1.2.4 && < 1.3+    hspec >= 2.7.1 && < 2.9,+    text >= 1.2.4 && < 2.1   default-language:     Haskell2010   default-extensions:
data/declaration/DataDef.agda view
@@ -25,5 +25,5 @@ postulate    d-    : D tt+    : D {tt} tt
data/declaration/RecordDef.agda view
@@ -25,5 +25,5 @@ postulate    r-    : R tt+    : R {tt} tt
data/declaration/TypeSig.agda view
@@ -1,4 +1,4 @@-module Definition where+module TypeSig where  f   : {A : Set}
src/Agda/Unused.hs view
@@ -11,8 +11,10 @@   ) where  import Agda.Unused.Types.Range-  (Range, RangeInfo)+  (RangeInfo) +import Agda.Syntax.Position+  (Range) import Data.Text   (Text)
src/Agda/Unused/Check.hs view
@@ -39,7 +39,7 @@   (Name(..), QName(..), fromAsName, fromModuleName, fromName, fromNameRange,     fromQName, fromQNameRange, nameIds, pathQName, qNamePath, toQName) import Agda.Unused.Types.Range-  (Range'(..), RangeInfo(..), RangeType(..), rangePath)+  (RangeInfo(..), RangeType(..), rangePath) import Agda.Unused.Utils   (liftMaybe, mapLeft) @@ -49,17 +49,17 @@   (CommandLineOptions(..), defaultOptions) import Agda.Syntax.Common   (Arg(..), Fixity'(..), GenPart(..), ImportDirective'(..), ImportedName'(..),-    IsInstance, Named(..), Ranged(..), Renaming'(..), RewriteEqn'(..),-    Using'(..), namedThing, unArg, whThing)+    Named(..), Ranged(..), RecordDirectives'(..), Renaming'(..),+    RewriteEqn'(..), Using'(..), namedThing, unArg) 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,+    LamBinding, LamBinding'(..), LamClause(..), LHS(..), Module(..),     ModuleApplication(..), ModuleAssignment(..), OpenShortHand(..), Pattern(..),-    RecordAssignment, Renaming, RewriteEqn, RHS, RHS'(..), TypedBinding,-    TypedBinding'(..), WhereClause, WhereClause'(..), _exprFieldA,+    RecordAssignment, RecordDirectives, Renaming, RewriteEqn, RHS, RHS'(..),+    TypedBinding, TypedBinding'(..), WhereClause, WhereClause'(..), _exprFieldA,     topLevelModuleName) import Agda.Syntax.Concrete.Definitions   (Clause(..), NiceConstructor, NiceDeclaration(..), niceDeclarations, runNice)@@ -72,13 +72,17 @@ import Agda.Syntax.Parser   (moduleParser, parseFile, runPMIO) import Agda.Syntax.Position-  (Range, getRange)+  (Range, Range'(..), getRange) import Agda.TypeChecking.Monad.Base-  (TCM, getIncludeDirs, runTCMTop)+  (TCM, runTCMTop) import Agda.TypeChecking.Monad.Options-  (setCommandLineOptions)+  (getIncludeDirs, setCommandLineOptions) import Agda.Utils.FileName   (filePath, mkAbsolute)+import qualified Agda.Utils.List2+  as List2+import Agda.Utils.List2+  (List2(..)) import Control.Monad   (foldM, unless, void, when) import Control.Monad.Except@@ -93,6 +97,10 @@   (bool) import Data.Foldable   (traverse_)+import qualified Data.List.NonEmpty+  as NonEmpty+import Data.List.NonEmpty+  (NonEmpty(..), nonEmpty) import qualified Data.Map.Strict   as Map import Data.Maybe@@ -140,10 +148,8 @@ fromFixity   :: Fixity'   -> Maybe Name-fromFixity (Fixity' _ [] _)-  = Nothing-fromFixity (Fixity' _ ps@(_ : _) _)-  = Just (Name (fromGenPart <$> ps))+fromFixity (Fixity' _ ps _)+  = Name <$> nonEmpty (fromGenPart <$> ps)  fromGenPart   :: GenPart@@ -169,14 +175,15 @@ checkSequence f x ys   = mconcat <$> sequence (f x <$> ys) -checkSequence_+checkSequence1   :: Monad m-  => (a -> b -> m ())+  => Monoid c+  => (a -> b -> m c)   -> a-  -> [b]-  -> m ()-checkSequence_ f x ys-  = void (sequence (f x <$> ys))+  -> NonEmpty b+  -> m c+checkSequence1 f x ys+  = checkSequence f x (NonEmpty.toList ys)  checkFold   :: Monad m@@ -188,6 +195,16 @@ checkFold   = checkFoldWith mempty (<>) +checkFold1+  :: Monad m+  => Monoid a+  => (a -> b -> m a)+  -> a+  -> NonEmpty b+  -> m a+checkFold1 f x ys+  = checkFold f x (NonEmpty.toList ys)+ checkFoldUnion   :: Monad m   => (AccessContext -> b -> m AccessContext)@@ -223,7 +240,7 @@   -> m AccessContext checkName _ _ _ _ NoRange _   = pure mempty-checkName _ _ _ _ _ (Name [Hole])+checkName _ _ _ _ _ (Name (Hole :| []))   = pure mempty checkName p fs a t r@(Range _ _) n   = modifyInsert r (RangeNamed t (QName n))@@ -359,7 +376,7 @@   -> [Name]   -> m () touchNames-  = checkSequence_ touchName+  = checkSequence touchName  touchQName   :: MonadError Error m@@ -413,7 +430,7 @@   >>= \c' -> checkPatternMay c p   >>= \c'' -> pure (c' <> c'') -checkBinders+checkBinders1   :: MonadError Error m   => MonadReader Environment m   => MonadState State m@@ -421,10 +438,10 @@   => Bool   -- ^ Whether to check bound names.   -> AccessContext-  -> [Binder]+  -> NonEmpty Binder   -> m AccessContext-checkBinders b-  = checkSequence (checkBinder b)+checkBinders1 b+  = checkSequence1 (checkBinder b)  checkLamBinding   :: MonadError Error m@@ -454,6 +471,19 @@ checkLamBindings b   = checkFold (checkLamBinding b) +checkLamBindings1+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Bool+  -- ^ Whether to check bound names.+  -> AccessContext+  -> NonEmpty LamBinding+  -> m AccessContext+checkLamBindings1 b+  = checkFold1 (checkLamBinding b)+ checkTypedBinding   :: MonadError Error m   => MonadReader Environment m@@ -465,9 +495,9 @@   -> TypedBinding   -> m AccessContext checkTypedBinding b c (TBind _ bs e)-  = checkExpr c e >> checkBinders b c (namedThing . unArg <$> bs)+  = checkExpr c e >> checkBinders1 b c (namedThing . unArg <$> bs) checkTypedBinding _ c (TLet _ ds)-  = checkDeclarations c ds+  = checkDeclarations1 c ds  checkTypedBindings   :: MonadError Error m@@ -482,6 +512,19 @@ checkTypedBindings b   = checkFold (checkTypedBinding b) +checkTypedBindings1+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => Bool+  -- ^ Whether to check bound names.+  -> AccessContext+  -> NonEmpty TypedBinding+  -> m AccessContext+checkTypedBindings1 b+  = checkFold1 (checkTypedBinding b)+ -- ## Patterns   checkPattern@@ -497,7 +540,7 @@ checkPattern _ (QuoteP _)   = pure mempty checkPattern c (RawAppP _ ps)-  = checkRawAppP c ps+  = checkRawAppP c (List2.toList ps) checkPattern _ (OpAppP r _ _ _)   = throwError (ErrorInternal (ErrorUnexpected UnexpectedOpAppP r)) checkPattern c (HiddenP _ (Named _ p))@@ -512,13 +555,13 @@   = pure mempty checkPattern c (DotP _ e)   = checkExpr c e >> pure mempty-checkPattern _ (LitP _)+checkPattern _ (LitP _ _)   = pure mempty checkPattern c (RecP _ as)   = checkPatterns c (_exprFieldA <$> as) checkPattern c (EqualP _ es)   = checkExprPairs c es >> pure mempty-checkPattern _ (EllipsisP _)+checkPattern _ (EllipsisP _ _)   = pure mempty checkPattern c (WithP _ p)   = checkPattern c p@@ -587,7 +630,7 @@ patternName   :: Pattern   -> Maybe String-patternName (IdentP (N.QName (N.Name _ _ [Id n])))+patternName (IdentP (N.QName (N.Name _ _ (Id n :| []))))   = Just n patternName _   = Nothing@@ -596,8 +639,7 @@   :: [Pattern]   -> [String] patternNames-  = catMaybes-  . fmap patternName+  = catMaybes . fmap patternName  -- ## Expressions @@ -611,14 +653,14 @@   -> m () checkExpr c (Ident n)   = touchQName' c n-checkExpr _ (Lit _)+checkExpr _ (Lit _ _)   = pure () checkExpr _ (QuestionMark _ _)   = pure () checkExpr _ (Underscore _ _)   = pure () checkExpr c (RawApp _ es)-  = checkRawApp c es+  = checkRawApp c (List2.toList es) checkExpr c (App _ e (Arg _ (Named _ e')))   = checkExpr c e >> checkExpr c e' checkExpr _ (OpApp r _ _ _)@@ -630,23 +672,15 @@ checkExpr c (InstanceArg _ (Named _ e))   = checkExpr c e checkExpr c (Lam _ bs e)-  = checkLamBindings True c bs >>= \c' -> checkExpr (c <> c') e+  = checkLamBindings1 True c bs >>= \c' -> checkExpr (c <> c') e checkExpr _ (AbsurdLam _ _)   = pure ()-checkExpr c (ExtendedLam _ ls)-  = checkLamClauses_ c ls+checkExpr c (ExtendedLam _ _ ls)+  = checkLamClauses1_ 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 ()+  = checkTypedBindings1 True c bs >>= \c' -> checkExpr (c <> c') e checkExpr c (Rec _ rs)   = checkRecordAssignments c rs checkExpr c (RecUpdate _ e fs)@@ -656,7 +690,7 @@ checkExpr c (IdiomBrackets _ es)   = checkExprs c es checkExpr c (DoBlock _ ss)-  = void (checkDoStmts c ss)+  = void (checkDoStmts1 c ss) checkExpr _ (Absurd r)   = throwError (ErrorInternal (ErrorUnexpected UnexpectedAbsurd r)) checkExpr _ (As r _ _)@@ -685,7 +719,7 @@   = checkExpr c e  checkExpr c (Let _ ds e)-  = checkDeclarations c ds+  = checkDeclarations1 c ds   >>= \c' -> traverse_ (checkExpr (c <> c')) e  checkExprs@@ -697,8 +731,19 @@   -> [Expr]   -> m () checkExprs-  = checkSequence_ checkExpr+  = checkSequence checkExpr +checkExprs1+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> NonEmpty Expr+  -> m ()+checkExprs1+  = checkSequence1 checkExpr+ checkExprPair   :: MonadError Error m   => MonadReader Environment m@@ -719,7 +764,7 @@   -> [(Expr, Expr)]   -> m () checkExprPairs-  = checkSequence_ checkExprPair+  = checkSequence checkExprPair  checkRawApp   :: MonadError Error m@@ -736,7 +781,7 @@ exprName   :: Expr   -> Maybe String-exprName (Ident (N.QName (N.Name _ _ [Id n])))+exprName (Ident (N.QName (N.Name _ _ (Id n :| []))))   = Just n exprName _   = Nothing@@ -745,8 +790,7 @@   :: [Expr]   -> [String] exprNames-  = catMaybes-  . fmap exprName+  = catMaybes . fmap exprName  -- ## Assignments @@ -772,7 +816,7 @@   -> [RecordAssignment]   -> m () checkRecordAssignments-  = checkSequence_ checkRecordAssignment+  = checkSequence checkRecordAssignment  checkFieldAssignment   :: MonadError Error m@@ -794,7 +838,7 @@   -> [FieldAssignment]   -> m () checkFieldAssignments-  = checkSequence_ checkFieldAssignment+  = checkSequence checkFieldAssignment  checkModuleAssignment   :: MonadError Error m@@ -818,10 +862,10 @@   => AccessContext   -> LHS   -> m AccessContext-checkLHS c (LHS p rs ws _)+checkLHS c (LHS p rs ws)   = checkPattern c p   >>= \c' -> checkRewriteEqns (c <> c') rs-  >>= \c'' -> checkExprs (c <> c' <> c'') (whThing <$> ws)+  >>= \c'' -> checkExprs (c <> c' <> c'') (unArg . namedThing <$> ws)   >> pure (c' <> c'')  checkRHS@@ -872,44 +916,44 @@   => AccessContext   -> LamClause   -> m AccessContext-checkLamClause c (LamClause l r _ _)-  = checkLHS c l+checkLamClause c (LamClause ps r _)+  = checkPatterns c ps   >>= \c' -> checkRHS (c <> c') r   >> pure c' -checkLamClauses+checkLamClause_   :: MonadError Error m   => MonadReader Environment m   => MonadState State m   => MonadIO m   => AccessContext-  -> [LamClause]-  -> m AccessContext-checkLamClauses-  = checkFold checkLamClause+  -> LamClause+  -> m ()+checkLamClause_ c ls+  = void (checkLamClause c ls) -checkLamClause_+checkLamClauses   :: MonadError Error m   => MonadReader Environment m   => MonadState State m   => MonadIO m   => AccessContext-  -> LamClause-  -> m ()-checkLamClause_ c ls-  = void (checkLamClause c ls)+  -> [LamClause]+  -> m AccessContext+checkLamClauses+  = checkFold checkLamClause  -- Do not propogate context from one clause to the next.-checkLamClauses_+checkLamClauses1_   :: MonadError Error m   => MonadReader Environment m   => MonadState State m   => MonadIO m   => AccessContext-  -> [LamClause]+  -> NonEmpty LamClause   -> m ()-checkLamClauses_-  = checkSequence_ checkLamClause_+checkLamClauses1_+  = checkSequence1 checkLamClause_  checkWhereClause   :: MonadError Error m@@ -922,10 +966,10 @@   -- ^ A context for the named where block, then the full context. checkWhereClause _ NoWhere   = pure (mempty, mempty)-checkWhereClause c (AnyWhere ds)+checkWhereClause c (AnyWhere _ ds)   = checkDeclarations c ds   >>= \c' -> pure (mempty, c')-checkWhereClause c (SomeWhere n a ds)+checkWhereClause c (SomeWhere _ n a ds)   = checkDeclarations c ds   >>= \c' -> checkModuleNameMay (toContext c') (fromAccess a) (getRange n)     (fromName n)@@ -940,9 +984,9 @@   -> RewriteEqn   -> m AccessContext checkRewriteEqn c (Rewrite rs)-  = checkExprs c (snd <$> rs) >> pure mempty+  = checkExprs1 c (snd <$> rs) >> pure mempty checkRewriteEqn c (Invert _ ws)-  = checkIrrefutableWiths c ws+  = checkIrrefutableWiths c (namedThing <$> ws)  checkRewriteEqns   :: MonadError Error m@@ -972,10 +1016,10 @@   => MonadState State m   => MonadIO m   => AccessContext-  -> [(Pattern, Expr)]+  -> NonEmpty (Pattern, Expr)   -> m AccessContext checkIrrefutableWiths-  = checkFold checkIrrefutableWith+  = checkFold1 checkIrrefutableWith  checkDoStmt   :: MonadError Error m@@ -993,62 +1037,60 @@ checkDoStmt c (DoThen e)   = checkExpr c e >> pure mempty checkDoStmt c (DoLet _ ds)-  = checkDeclarations c ds+  = checkDeclarations1 c ds -checkDoStmts+checkDoStmts1   :: MonadError Error m   => MonadReader Environment m   => MonadState State m   => MonadIO m   => AccessContext-  -> [DoStmt]+  -> NonEmpty DoStmt   -> m AccessContext-checkDoStmts c ss-  = when (hasBind ss) (touchName c bind)-  >> when (hasBind_ ss) (touchName c bind_)-  >> checkFold checkDoStmt c ss+checkDoStmts1 c (s :| ss)+  = when (hasBind s ss) (touchName c bind)+  >> when (hasBind_ s ss) (touchName c bind_)+  >> checkFold checkDoStmt c (s : ss)  hasBind-  :: [DoStmt]+  :: DoStmt+  -> [DoStmt]   -> Bool-hasBind []-  = False-hasBind (_ : [])+hasBind _ []   = False-hasBind (DoBind _ _ _ _ : _ : _)+hasBind (DoBind _ _ _ _) (_ : _)   = True-hasBind (_ : ss)-  = hasBind ss+hasBind _ (s : ss)+  = hasBind s ss  hasBind_-  :: [DoStmt]+  :: DoStmt+  -> [DoStmt]   -> Bool-hasBind_ []-  = False-hasBind_ (_ : [])+hasBind_ _ []   = False-hasBind_ (DoThen _ : _ : _)+hasBind_ (DoThen _) (_ : _)   = True-hasBind_ (_ : ss)-  = hasBind_ ss+hasBind_ _ (s : ss)+  = hasBind_ s ss  bind   :: Name bind   = Name-  [ Hole-  , Id ">>="-  , Hole-  ]+  $ (:|) Hole+  $ (:) (Id ">>=")+  $ (:) Hole+  $ []  bind_   :: Name bind_   = Name-  [ Hole-  , Id ">>"-  , Hole-  ]+  $ (:|) Hole+  $ (:) (Id ">>")+  $ (:) Hole+  $ []  -- ## Declarations @@ -1063,6 +1105,17 @@ checkDeclarations   = checkDeclarationsWith checkNiceDeclarations +checkDeclarations1+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> NonEmpty Declaration+  -> m AccessContext+checkDeclarations1 c ds+  = checkDeclarations c (NonEmpty.toList ds)+ checkDeclarationsRecord   :: MonadError Error m   => MonadReader Environment m@@ -1149,12 +1202,14 @@   = checkExpr c e >> checkName' False fs (fromAccess a) RangePostulate n checkNiceDeclaration' _ _ (NiceField r _ _ _ _ _ _)   = throwError (ErrorInternal (ErrorUnexpected UnexpectedField r))-checkNiceDeclaration' fs c (PrimitiveFunction _ a _ n e)+checkNiceDeclaration' fs c (PrimitiveFunction _ a _ n (Arg _ 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' _ c (NiceModuleMacro r a n m o i)+  = checkNiceModuleMacro c (fromAccess a) r n m o i checkNiceDeclaration' _ _ (NicePragma _ _)   = pure mempty checkNiceDeclaration' fs c (NiceRecSig _ a _ _ _ n bs e)@@ -1169,8 +1224,10 @@   = checkClauses c cs >> pure mempty checkNiceDeclaration' fs c (NiceDataDef _ _ _ _ _ n bs cs)   = checkNiceDataDef True fs c n bs cs-checkNiceDeclaration' fs c (NiceRecDef _ _ _ _ _ n _ _ m bs ds)-  = checkNiceRecordDef True fs c n m bs ds+checkNiceDeclaration' _ _ (NiceLoneConstructor r _)+  = throwError (ErrorUnsupported UnsupportedLoneConstructor r)+checkNiceDeclaration' fs c (NiceRecDef _ _ _ _ _ n rs bs ds)+  = checkNiceRecordDef True fs c n rs bs ds checkNiceDeclaration' _ c (NiceGeneralize _ _ _ _ _ e)   = checkExpr c e >> pure mempty checkNiceDeclaration' _ _ (NiceUnquoteDecl r _ _ _ _ _ _ _)@@ -1180,10 +1237,10 @@  checkNiceDeclaration' fs c   (NiceMutual _ _ _ _-    (d@(NiceRecSig _ _ _ _ _ n _ _) : NiceRecDef _ _ _ _ _ n' _ _ m bs ds : []))+    (d@(NiceRecSig _ _ _ _ _ n _ _) : NiceRecDef _ _ _ _ _ n' rs bs ds : []))   | nameRange n == nameRange n'   = checkNiceDeclaration fs c d-  >>= \c' -> checkNiceRecordDef False fs (c <> c') n' m bs ds+  >>= \c' -> checkNiceRecordDef False fs (c <> c') n' rs bs ds   >>= \c'' -> pure (c' <> c'') checkNiceDeclaration' fs c   (NiceMutual _ _ _ _@@ -1201,47 +1258,6 @@   >>= \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)@@ -1317,7 +1333,9 @@   = checkNiceDeclaration fs c d checkNiceDeclarationRecord _ _ fs c d@(NiceDataDef _ _ _ _ _ _ _ _)   = checkNiceDeclaration fs c d-checkNiceDeclarationRecord _ _ fs c d@(NiceRecDef _ _ _ _ _ _ _ _ _ _ _)+checkNiceDeclarationRecord _ _ _ _ (NiceLoneConstructor r _)+  = throwError (ErrorUnsupported UnsupportedLoneConstructor r)+checkNiceDeclarationRecord _ _ fs c d@(NiceRecDef _ _ _ _ _ _ _ _ _)   = checkNiceDeclaration fs c d checkNiceDeclarationRecord _ _ fs c d@(NicePatternSyn _ _ _ _ _)   = checkNiceDeclaration fs c d@@ -1427,17 +1445,17 @@   -> Fixities   -> AccessContext   -> N.Name-  -> Maybe (N.Name, IsInstance)+  -> RecordDirectives   -> [LamBinding]   -> [Declaration]   -> m AccessContext-checkNiceRecordDef b fs c n m bs ds+checkNiceRecordDef b fs c n (RecordDirectives _ _ _ m) bs ds   = liftMaybe (ErrorInternal (ErrorName (getRange n))) (fromName n)   >>= \n' -> pure (either (const mempty) id (accessContextLookup (QName n') c))-  >>= \rs -> checkLamBindings b c bs-  >>= \c' -> checkNiceConstructorRecordMay fs rs (m >>= fromNameRange . fst)-  >>= \c'' -> checkDeclarationsRecord n' rs (c <> c') ds-  >>= \c''' -> pure (accessContextModule' n' Public rs (c'' <> c''') <> c'')+  >>= \rs' -> checkLamBindings b c bs+  >>= \c' -> checkNiceConstructorRecordMay fs rs' (m >>= fromNameRange . fst)+  >>= \c'' -> checkDeclarationsRecord n' rs' (c <> c') ds+  >>= \c''' -> pure (accessContextModule' n' Public rs' (c'' <> c''') <> c'')  checkNiceConstructor   :: MonadError Error m@@ -1519,6 +1537,77 @@   >>= \c'' -> pure (toContext c'')   >>= \c''' -> maybe (pure (fromContext a c''')) (checkModuleName c''' a r) n +checkNiceModuleMacro+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> Access+  -> Range+  -> N.Name+  -> ModuleApplication+  -> OpenShortHand+  -> ImportDirective+  -> m AccessContext+checkNiceModuleMacro c a _ a' (SectionApp r bs e) o i+  = checkSectionApp c a r a' bs (parseSectionApp e) o i+checkNiceModuleMacro _ _ r _ (RecordModuleInstance _ _) _ _+  = throwError (ErrorUnsupported UnsupportedMacro r)++checkSectionApp+  :: MonadError Error m+  => MonadReader Environment m+  => MonadState State m+  => MonadIO m+  => AccessContext+  -> Access+  -> Range+  -> N.Name+  -> [TypedBinding]+  -> Maybe (N.QName, [Expr])+  -> OpenShortHand+  -> ImportDirective+  -> m AccessContext+checkSectionApp _ _ r _ _ Nothing _ _+  = throwError (ErrorInternal (ErrorMacro r))+checkSectionApp c _ r (N.NoName _ _) [] (Just (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)+checkSectionApp c a r a' bs (Just (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''' a r a''+checkSectionApp c a r a' bs (Just (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''' a r a''+  >>= \c'''' -> pure (c'''' <> fromContext (importDirectiveAccess i) c''')++parseSectionApp+  :: Expr+  -> Maybe (N.QName, [Expr])+parseSectionApp (Ident n)+  = Just (n, [])+parseSectionApp (RawApp _ (List2 (Ident n) e es))+  = Just (n, (e : es))+parseSectionApp _+  = Nothing+ -- ## Imports  data DirectiveType where@@ -1725,7 +1814,7 @@   => QName   -> Module   -> m Context-checkModule n (_, ds) = do+checkModule n (Mod _ ds) = do   local     <- askLocal   _@@ -1835,7 +1924,7 @@   moduleName     <- pure (topLevelModuleName module')   moduleQName-    <- liftMaybe (ErrorInternal (ErrorModuleName p)) (fromModuleName moduleName)+    <- pure (fromModuleName moduleName)   absolutePath     <- pure (projectRoot (mkAbsolute p) moduleName)   rootPath
src/Agda/Unused/Monad/Error.hs view
@@ -24,8 +24,6 @@   (LookupError(..)) import Agda.Unused.Types.Name   (QName)-import Agda.Unused.Types.Range-  (Range, getRange)  import Agda.Interaction.FindFile   (FindError)@@ -35,6 +33,8 @@   (MonadFixityError(..)) import Agda.Syntax.Parser   (ParseError)+import Agda.Syntax.Position+  (Range, getRange) import Control.Monad.Except   (MonadError, throwError) @@ -194,6 +194,10 @@  -- | An error indicating that an unsupported language was found. data UnsupportedError where++  -- | Lone constructors.+  UnsupportedLoneConstructor+    :: UnsupportedError    -- | Record module instance applications.   UnsupportedMacro
src/Agda/Unused/Monad/State.hs view
@@ -38,8 +38,10 @@ import Agda.Unused.Types.Name   (QName) import Agda.Unused.Types.Range-  (Range, Range'(..), RangeInfo, rangeContains)+  (RangeInfo, rangeContains) +import Agda.Syntax.Position+  (Range, Range'(..)) import Agda.TypeChecking.Monad.Base   (ModuleToSource) import Control.Monad
src/Agda/Unused/Print.hs view
@@ -17,12 +17,18 @@ import Agda.Unused.Types.Name   (Name(..), NamePart(..), QName(..)) import Agda.Unused.Types.Range-  (Range, Range'(..), RangeInfo(..), RangeType(..), getRange)+  (RangeInfo(..), RangeType(..))  import Agda.Interaction.FindFile   (FindError(..))+import Agda.Syntax.Concrete.Definitions.Errors+  (DeclarationException(..))+import Agda.Syntax.Position+  (Range, Range'(..), getRange) import Agda.Utils.Pretty   (prettyShow)+import Data.Semigroup+  (sconcat) import Data.Text   (Text) import qualified Data.Text@@ -54,13 +60,13 @@   :: NamePart   -> Text printNamePart-  = T.pack . show+  = T.pack . prettyShow  printName   :: Name   -> Text printName (Name ps)-  = mconcat (printNamePart <$> ps)+  = sconcat (printNamePart <$> ps)  printQName   :: QName@@ -78,7 +84,7 @@ printRange NoRange   = "unknown location" printRange r@(Range _ _)-  = T.pack (show r)+  = T.pack (prettyShow r)  -- ## Messages @@ -134,7 +140,7 @@   = printMessage (printRange r)   $ "Error: " <> printUnsupportedError e <> " not supported." -printError (ErrorDeclaration e)+printError (ErrorDeclaration (DeclarationException _ e))   = printRange (getRange e) <> "\n" <> T.pack (prettyShow e) printError (ErrorFile p)   = printErrorFile p@@ -205,6 +211,8 @@ printUnsupportedError   :: UnsupportedError   -> Text+printUnsupportedError UnsupportedLoneConstructor+  = "Lone constructors" printUnsupportedError UnsupportedMacro   = "Record module instance applications" printUnsupportedError UnsupportedUnquote
src/Agda/Unused/Types/Context.hs view
@@ -75,9 +75,9 @@   (Access(..)) import Agda.Unused.Types.Name   (Name, QName(..), matchOperators, stripPrefix)-import Agda.Unused.Types.Range-  (Range) +import Agda.Syntax.Position+  (Range) import Data.Map.Strict   (Map) import qualified Data.Map.Strict
src/Agda/Unused/Types/Name.hs view
@@ -54,8 +54,14 @@   (isSubsequenceOf) import qualified Data.List   as List+import Data.List.NonEmpty+  (NonEmpty(..))+import qualified Data.List.NonEmpty+  as NonEmpty import Data.Maybe   (mapMaybe)+import Data.Semigroup+  (sconcat) import System.FilePath   ((</>), (<.>), splitDirectories) @@ -65,7 +71,7 @@ newtype Name   = Name   { nameParts-    :: [NamePart]+    :: NonEmpty NamePart   } deriving (Eq, Ord, Show)  -- | A qualified name.@@ -89,7 +95,7 @@   :: Name   -> [String] nameIds (Name ps)-  = mapMaybe namePartId ps+  = mapMaybe namePartId (NonEmpty.toList ps)  namePartId   :: NamePart@@ -102,11 +108,9 @@ isOperator   :: Name   -> Bool-isOperator (Name [])-  = False-isOperator (Name (_ : []))+isOperator (Name (_ :| []))   = False-isOperator (Name (_ : _ : _))+isOperator (Name (_ :| _ : _))   = True  -- | If the first module name is a prefix of the second module name, then strip@@ -134,7 +138,7 @@ fromName (N.Name _ _ n)   = Just (Name n) --- | Like 'fromName', but also return a 'Range'.+-- | Like 'fromName', but also return a range. fromNameRange   :: N.Name   -> Maybe (Range, Name)@@ -152,7 +156,7 @@ fromQName (N.Qual n ns)   = Qual <$> fromName n <*> fromQName ns --- | Like 'fromQName', but also return a 'Range'.+-- | Like 'fromQName', but also return a range. fromQNameRange   :: N.QName   -> Maybe (Range, QName)@@ -173,11 +177,9 @@ -- | Conversion from Agda top level module name type. fromModuleName   :: TopLevelModuleName-  -> Maybe QName-fromModuleName (TopLevelModuleName _ [])-  = Nothing-fromModuleName (TopLevelModuleName _ (n : ns))-  = Just (fromStrings n ns)+  -> QName+fromModuleName (TopLevelModuleName _ (n :| ns))+  = fromStrings n ns  fromStrings   :: String@@ -192,7 +194,7 @@   :: String   -> Name fromString n-  = Name [Id n]+  = Name (Id n :| [])  -- | Conversion to Agda name type. toName@@ -216,7 +218,7 @@   :: Name   -> String namePath (Name ps)-  = mconcat (show <$> ps)+  = sconcat (show <$> ps)  -- | Convert a module name to a 'FilePath'. qNamePath@@ -246,13 +248,13 @@ pathQNameRelative [n]   = QName <$> pathName n pathQNameRelative (n : ns@(_ : _))-  = Qual (Name [Id n]) <$> pathQNameRelative ns+  = Qual (Name (Id n :| [])) <$> pathQNameRelative ns  pathName   :: String   -> Maybe Name pathName n-  = Name . (: []) . Id <$> stripSuffix ".agda" n+  = Name . (:| []) . Id <$> stripSuffix ".agda" n  -- ## Match
src/Agda/Unused/Types/Range.hs view
@@ -7,14 +7,11 @@    ( -- * Definitions -    Range-  , Range'(..)-  , RangeType(..)+    RangeType(..)   , RangeInfo(..)      -- * Interface -  , getRange   , rangePath   , rangeContains @@ -24,7 +21,7 @@   (QName)  import Agda.Syntax.Position-  (PositionWithoutFile, Range, Range'(..), getRange, rEnd', rStart')+  (PositionWithoutFile, Range, Range'(..), rEnd', rStart') import Agda.Utils.FileName   (filePath) import qualified Agda.Utils.Maybe.Strict
src/Agda/Unused/Utils.hs view
@@ -1,7 +1,7 @@ {- | Module: Agda.Unused.Utils -Utility functions for 'Maybe', 'Either', and 'Map' types.+Utility functions. -} module Agda.Unused.Utils
test/Main.hs view
@@ -21,6 +21,8 @@  import Data.Maybe   (mapMaybe)+import Data.List.NonEmpty+  (NonEmpty(..)) import qualified Data.Set   as Set import Data.Text@@ -38,40 +40,52 @@  -- ## Names +name0+  :: String+  -> Name+name0 n+  = Name (Id n :| [])++name2+  :: String+  -> Name+name2 n+  = Name (Hole :| Id n : Hole : [])+ name   :: String   -> QName name n-  = QName (Name [Id n])-+  = QName (name0 n)+  land   :: QName land-  = QName (Name [Hole, Id "&&", Hole])+  = QName (name2 "&&")  bind   :: QName bind-  = QName (Name [Hole, Id ">>=", Hole])+  = QName (name2 ">>=")  bind_   :: QName bind_-  = QName (Name [Hole, Id ">>", Hole])+  = QName (name2 ">>")  agdaBuiltinBool   :: QName agdaBuiltinBool-  = Qual (Name [Id "Agda"])-  $ Qual (Name [Id "Builtin"])-  $ QName (Name [Id "Bool"])+  = Qual (name0 "Agda")+  $ Qual (name0 "Builtin")+  $ QName (name0 "Bool")  agdaBuiltinNat   :: QName agdaBuiltinNat-  = Qual (Name [Id "Agda"])-  $ Qual (Name [Id "Builtin"])-  $ QName (Name [Id "Nat"])+  = Qual (name0 "Agda")+  $ Qual (name0 "Builtin")+  $ QName (name0 "Nat")  -- ## Ranges