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