diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. + diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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. diff --git a/agda-unused.cabal b/agda-unused.cabal --- a/agda-unused.cabal +++ b/agda-unused.cabal @@ -3,7 +3,7 @@ name: agda-unused version: - 0.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: diff --git a/data/declaration/DataDef.agda b/data/declaration/DataDef.agda --- a/data/declaration/DataDef.agda +++ b/data/declaration/DataDef.agda @@ -25,5 +25,5 @@ postulate d - : D tt + : D {tt} tt diff --git a/data/declaration/RecordDef.agda b/data/declaration/RecordDef.agda --- a/data/declaration/RecordDef.agda +++ b/data/declaration/RecordDef.agda @@ -25,5 +25,5 @@ postulate r - : R tt + : R {tt} tt diff --git a/data/declaration/TypeSig.agda b/data/declaration/TypeSig.agda --- a/data/declaration/TypeSig.agda +++ b/data/declaration/TypeSig.agda @@ -1,4 +1,4 @@ -module Definition where +module TypeSig where f : {A : Set} diff --git a/src/Agda/Unused.hs b/src/Agda/Unused.hs --- a/src/Agda/Unused.hs +++ b/src/Agda/Unused.hs @@ -11,8 +11,10 @@ ) where import Agda.Unused.Types.Range - (Range, RangeInfo) + (RangeInfo) +import Agda.Syntax.Position + (Range) import Data.Text (Text) diff --git a/src/Agda/Unused/Check.hs b/src/Agda/Unused/Check.hs --- a/src/Agda/Unused/Check.hs +++ b/src/Agda/Unused/Check.hs @@ -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 diff --git a/src/Agda/Unused/Monad/Error.hs b/src/Agda/Unused/Monad/Error.hs --- a/src/Agda/Unused/Monad/Error.hs +++ b/src/Agda/Unused/Monad/Error.hs @@ -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 diff --git a/src/Agda/Unused/Monad/State.hs b/src/Agda/Unused/Monad/State.hs --- a/src/Agda/Unused/Monad/State.hs +++ b/src/Agda/Unused/Monad/State.hs @@ -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 diff --git a/src/Agda/Unused/Print.hs b/src/Agda/Unused/Print.hs --- a/src/Agda/Unused/Print.hs +++ b/src/Agda/Unused/Print.hs @@ -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 diff --git a/src/Agda/Unused/Types/Context.hs b/src/Agda/Unused/Types/Context.hs --- a/src/Agda/Unused/Types/Context.hs +++ b/src/Agda/Unused/Types/Context.hs @@ -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 diff --git a/src/Agda/Unused/Types/Name.hs b/src/Agda/Unused/Types/Name.hs --- a/src/Agda/Unused/Types/Name.hs +++ b/src/Agda/Unused/Types/Name.hs @@ -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 diff --git a/src/Agda/Unused/Types/Range.hs b/src/Agda/Unused/Types/Range.hs --- a/src/Agda/Unused/Types/Range.hs +++ b/src/Agda/Unused/Types/Range.hs @@ -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 diff --git a/src/Agda/Unused/Utils.hs b/src/Agda/Unused/Utils.hs --- a/src/Agda/Unused/Utils.hs +++ b/src/Agda/Unused/Utils.hs @@ -1,7 +1,7 @@ {- | Module: Agda.Unused.Utils -Utility functions for 'Maybe', 'Either', and 'Map' types. +Utility functions. -} module Agda.Unused.Utils diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -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