module Main where
import Agda.Unused
(UnusedItems(..), UnusedOptions(..))
import Agda.Unused.Check
(checkUnused, checkUnusedWith)
import Agda.Unused.Monad.Error
(Error)
import Agda.Unused.Monad.Reader
(Mode(..))
import Agda.Unused.Print
(printError, 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 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
name
:: String
-> QName
name n
= QName (Name [Id 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"])
agdaBuiltinNat
:: QName
agdaBuiltinNat
= Qual (Name [Id "Agda"])
$ Qual (Name [Id "Builtin"])
$ QName (Name [Id "Nat"])
-- ## 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
rangeInfo
:: QName
-> RangeType
-> RangeInfo
rangeInfo n Data
= RangeNamed R.RangeData n
rangeInfo n Definition
= RangeNamed R.RangeDefinition n
rangeInfo n Import
= RangeNamed R.RangeImport n
rangeInfo n ImportItem
= RangeNamed R.RangeImportItem n
rangeInfo n Module
= RangeNamed R.RangeModule n
rangeInfo n ModuleItem
= RangeNamed R.RangeModuleItem n
rangeInfo _ Mutual
= RangeMutual
rangeInfo n Open
= RangeNamed R.RangeOpen n
rangeInfo n OpenItem
= RangeNamed R.RangeOpenItem n
rangeInfo n PatternSynonym
= RangeNamed R.RangePatternSynonym n
rangeInfo n Postulate
= RangeNamed R.RangePostulate n
rangeInfo n Record
= RangeNamed R.RangeRecord n
rangeInfo n RecordConstructor
= RangeNamed R.RangeRecordConstructor n
rangeInfo n Variable
= RangeNamed R.RangeVariable n
private
:: QName
-> (Access, QName)
private n
= (Private, n)
public
:: QName
-> (Access, QName)
public n
= (Public, n)
(~:)
:: (Access, QName)
-> RangeType
-> (Access, RangeInfo)
(a, n) ~: t
= (a, rangeInfo n t)
-- ## Expectations
testCheck
:: Test
-> Expectation
testCheck t = do
rootPath
<- testRootPath t
filePath
<- testFilePath t
unusedLocal
<- checkUnusedWith Local (unusedOptions rootPath) filePath
unusedGlobal
<- checkUnusedWith Global (unusedOptions rootPath) filePath
_
<- testUnused unusedLocal (mapMaybe privateMay (testResult t))
_
<- testUnused unusedGlobal (snd <$> testResult t)
pure ()
testCheckExample
:: Expectation
testCheckExample = do
rootPath
<- getDataFileName "data/example"
filePath
<- getDataFileName "data/example/Test.agda"
unused
<- checkUnused (unusedOptions rootPath) filePath
_
<- testUnusedExample unused
pure ()
testUnused
:: Either Error UnusedItems
-> [RangeInfo]
-> Expectation
testUnused (Left e) _
= expectationFailure (T.unpack (printError e))
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 "/Test.agda:4,23-27")
>> (t1 `shouldBe` " unused imported item ‘true’")
>> (t2 `shouldSatisfy` T.isSuffixOf "/Test.agda:5,1-30")
>> (t3 `shouldBe` " unused import ‘Agda.Builtin.Unit’")
>> (t4 `shouldSatisfy` T.isSuffixOf "/Test.agda:11,9-10")
>> (t5 `shouldBe` " unused variable ‘x’")
testUnusedOutput _
= expectationFailure ""
unusedOptions
:: FilePath
-> UnusedOptions
unusedOptions p
= UnusedOptions
{ unusedOptionsInclude
= [p]
, unusedOptionsLibraries
= []
, unusedOptionsLibrariesFile
= Nothing
, unusedOptionsUseLibraries
= False
, unusedOptionsUseDefaultLibraries
= False
}
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
DataDef
:: DeclarationTest
Record'
:: DeclarationTest
RecordDef
:: DeclarationTest
Syntax
:: DeclarationTest
PatternSyn
:: DeclarationTest
Mutual1
:: DeclarationTest
Mutual2
:: DeclarationTest
Abstract
:: DeclarationTest
Private'
:: DeclarationTest
Postulate'
:: DeclarationTest
Open1
:: DeclarationTest
Open2
:: DeclarationTest
Import'
:: DeclarationTest
ModuleMacro
:: DeclarationTest
Module'
:: DeclarationTest
deriving Show
testDir
:: Test
-> FilePath
testDir (Pattern _)
= "pattern"
testDir (Expression _)
= "expression"
testDir (Declaration _)
= "declaration"
testRootPath
:: Test
-> IO FilePath
testRootPath t
= getDataFileName ("data" </> testDir t)
testFilePath
:: Test
-> IO FilePath
testFilePath t
= getDataFileName ("data" </> testDir t </> testFileName t <.> "agda")
testFileName
:: Test
-> String
testFileName (Pattern IdentP)
= "IdentP"
testFileName (Pattern OpAppP)
= "OpAppP"
testFileName (Pattern AsP)
= "AsP"
testFileName (Expression WithApp)
= "WithApp"
testFileName (Expression Lam)
= "Lam"
testFileName (Expression ExtendedLam)
= "ExtendedLam"
testFileName (Expression Pi)
= "Pi"
testFileName (Expression Let)
= "Let"
testFileName (Expression DoBlock1)
= "DoBlock1"
testFileName (Expression DoBlock2)
= "DoBlock2"
testFileName (Expression DoBlock3)
= "DoBlock3"
testFileName (Expression DoBlock4)
= "DoBlock4"
testFileName (Declaration TypeSig)
= "TypeSig"
testFileName (Declaration FunClause)
= "FunClause"
testFileName (Declaration Data')
= "Data"
testFileName (Declaration DataDef)
= "DataDef"
testFileName (Declaration Record')
= "Record"
testFileName (Declaration RecordDef)
= "RecordDef"
testFileName (Declaration Syntax)
= "Syntax"
testFileName (Declaration PatternSyn)
= "PatternSyn"
testFileName (Declaration Mutual1)
= "Mutual1"
testFileName (Declaration Mutual2)
= "Mutual2"
testFileName (Declaration Abstract)
= "Abstract"
testFileName (Declaration Private')
= "Private"
testFileName (Declaration Postulate')
= "Postulate"
testFileName (Declaration Open1)
= "Open1"
testFileName (Declaration Open2)
= "Open2"
testFileName (Declaration Import')
= "Import"
testFileName (Declaration ModuleMacro)
= "ModuleMacro"
testFileName (Declaration Module')
= "Module"
testResult
:: Test
-> [(Access, RangeInfo)]
testResult t
= case t of
Pattern IdentP ->
[ private (name "y")
~: Variable
, public (name "f")
~: Definition
, public (name "g")
~: Definition
]
Pattern OpAppP ->
[ public land
~: Definition
]
Pattern AsP ->
[ private (name "y")
~: Variable
, private (name "z")
~: Variable
, private (name "w")
~: Variable
, private (name "z'")
~: Variable
, private (name "w'")
~: Variable
, public (name "f")
~: Definition
, public (name "g")
~: Definition
]
Expression WithApp ->
[ public (name "f")
~: Definition
, public (name "g")
~: Definition
]
Expression Lam ->
[ private (name "y")
~: Variable
, private (name "y'")
~: Variable
, public (name "f")
~: Definition
, public (name "g")
~: Definition
]
Expression ExtendedLam ->
[ private (name "x")
~: Variable
, public (name "f")
~: Definition
]
Expression Pi ->
[ private (name "y")
~: Variable
, private (name "w")
~: Variable
, public (name "f")
~: Definition
]
Expression Let ->
[ private (name "z")
~: Definition
, public (name "f")
~: Definition
]
Expression DoBlock1 ->
[ private (name "z")
~: Variable
, public (name "f")
~: Definition
]
Expression DoBlock2 ->
[ public bind_
~: Definition
, public (name "f")
~: Definition
]
Expression DoBlock3 ->
[ public bind
~: Definition
, public (name "f")
~: Definition
]
Expression DoBlock4 ->
[ public bind
~: Definition
, public bind_
~: Definition
, public (name "f")
~: Definition
]
Declaration TypeSig ->
[ public (name "g")
~: Definition
, public (name "h")
~: Definition
]
Declaration FunClause ->
[ private (name "z")
~: Definition
, public (name "f")
~: Definition
, public (name "snoc")
~: Definition
]
Declaration Data' ->
[ public (name "E")
~: Data
, public (name "_")
~: Mutual
]
Declaration DataDef ->
[ private (name "z")
~: Variable
, public (name "d")
~: Postulate
]
Declaration Record' ->
[ public (name "B")
~: Record
, public (name "D")
~: Record
, public (name "F")
~: Record
, public (name "c")
~: RecordConstructor
, public (name "x")
~: Definition
, public (name "y")
~: Definition
]
Declaration RecordDef ->
[ private (name "z")
~: Variable
, public (name "r")
~: Postulate
]
Declaration Syntax ->
[ public (name "p1")
~: Postulate
, public (name "p1'")
~: Postulate
]
Declaration PatternSyn ->
[ public (name "q")
~: PatternSynonym
, public (name "f")
~: Definition
, public (name "g")
~: Definition
]
Declaration Mutual1 ->
[ public (name "_")
~: Mutual
]
Declaration Mutual2 ->
[ public (name "is-even'")
~: Definition
]
Declaration Abstract ->
[ public (name "g")
~: Definition
, public (name "h")
~: Definition
]
Declaration Private' ->
[ private (name "g")
~: Definition
, private (name "h")
~: Definition
]
Declaration Postulate' ->
[ public (name "g")
~: Postulate
, public (name "h")
~: Definition
]
Declaration Open1 ->
[ private (name "N")
~: Open
, private (name "P")
~: Open
, public (name "Q")
~: Module
, private (name "x'")
~: OpenItem
, public (name "v")
~: Definition
, public (name "y")
~: Definition
]
Declaration Open2 ->
[ public (name "z")
~: OpenItem
, public (name "p")
~: Postulate
]
Declaration Import' ->
[ private agdaBuiltinBool
~: Import
, private agdaBuiltinNat
~: Import
, private (name "tt")
~: ImportItem
, public (name "A")
~: Definition
]
Declaration ModuleMacro ->
[ private (name "x")
~: Variable
, public (name "Q")
~: Module
, public (name "A'")
~: ModuleItem
, public (name "C")
~: Definition
, public (name "D")
~: Definition
, public (name "y")
~: Definition
]
Declaration Module' ->
[ public (name "O")
~: Module
, public (name "P")
~: Module
, public (name "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 data definitions (DataDef)"
(testCheck (Declaration DataDef))
>> it "checks record declarations (Record)"
(testCheck (Declaration Record'))
>> it "checks record definitions (RecordDef)"
(testCheck (Declaration RecordDef))
>> 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 Open1)
>> testCheck (Declaration Open2))
>> 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