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