{- |
Module: Agda.Unused.Print

Printing functions for unused items and errors.
-}
module Agda.Unused.Print
  ( printError
  , printUnused
  , printUnusedItems
  , printNothing
  ) where

import Agda.Unused
  (Unused(..), UnusedItems(..))
import Agda.Unused.Monad.Error
  (Error(..), InternalError(..), UnexpectedError(..), UnsupportedError(..))
import Agda.Unused.Types.Name
  (Name(..), NamePart(..), QName(..))
import Agda.Unused.Types.Range
  (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
  as T

-- ## Utilities

quote
  :: Text
  -> Text
quote :: Text -> Text
quote Text
t
  = Text
"‘" forall a. Semigroup a => a -> a -> a
<> Text
t forall a. Semigroup a => a -> a -> a
<> Text
"’"

parens
  :: Text
  -> Text
parens :: Text -> Text
parens Text
t
  = Text
"(" forall a. Semigroup a => a -> a -> a
<> Text
t forall a. Semigroup a => a -> a -> a
<> Text
")"

indent
  :: Text
  -> Text
indent :: Text -> Text
indent Text
t
  = Text
"  " forall a. Semigroup a => a -> a -> a
<> Text
t

-- ## Names

printNamePart
  :: NamePart
  -> Text
printNamePart :: NamePart -> Text
printNamePart
  = String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
prettyShow

printName
  :: Name
  -> Text
printName :: Name -> Text
printName (Name NonEmpty NamePart
ps)
  = forall a. Semigroup a => NonEmpty a -> a
sconcat (NamePart -> Text
printNamePart forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty NamePart
ps)

printQName
  :: QName
  -> Text
printQName :: QName -> Text
printQName (QName Name
n)
  = Name -> Text
printName Name
n
printQName (Qual Name
n QName
ns)
  = Name -> Text
printName Name
n forall a. Semigroup a => a -> a -> a
<> Text
"." forall a. Semigroup a => a -> a -> a
<> QName -> Text
printQName QName
ns

-- ## Ranges

printRange
  :: Range
  -> Text
printRange :: Range -> Text
printRange Range
NoRange
  = Text
"unknown location"
printRange r :: Range
r@(Range SrcFile
_ Seq IntervalWithoutFile
_)
  = String -> Text
T.pack (forall a. Pretty a => a -> String
prettyShow Range
r)

-- ## Messages

printMessage
  :: Text
  -> Text
  -> Text
printMessage :: Text -> Text -> Text
printMessage Text
t1 Text
t2
  = Text -> [Text] -> Text
T.intercalate Text
"\n" [Text
t1, Text
t2]

printMessageIndent
  :: Text
  -> Text
  -> Text
printMessageIndent :: Text -> Text -> Text
printMessageIndent Text
t1 Text
t2
  = Text -> [Text] -> Text
T.intercalate Text
"\n" [Text
t1, Text -> Text
indent Text
t2]

-- ## Errors

-- | Print an error.
printError
  :: Error
  -> Text

printError :: Error -> Text
printError (ErrorAmbiguous Range
r QName
n)
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Error: Ambiguous name " forall a. Semigroup a => a -> a -> a
<> Text -> Text
parens (Text -> Text
quote (QName -> Text
printQName QName
n)) forall a. Semigroup a => a -> a -> a
<> Text
"."
printError (ErrorCyclic Range
r QName
n)
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Error: Cyclic module dependency " forall a. Semigroup a => a -> a -> a
<> Text -> Text
parens (QName -> Text
printQName QName
n) forall a. Semigroup a => a -> a -> a
<> Text
"."
printError (ErrorFind Range
r QName
n (NotFound [SourceFile]
_))
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Error: Import not found " forall a. Semigroup a => a -> a -> a
<> Text -> Text
parens (QName -> Text
printQName QName
n) forall a. Semigroup a => a -> a -> a
<> Text
"."
printError (ErrorFind Range
r QName
n (Ambiguous [SourceFile]
_))
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Error: Ambiguous import " forall a. Semigroup a => a -> a -> a
<> Text -> Text
parens (QName -> Text
printQName QName
n) forall a. Semigroup a => a -> a -> a
<> Text
"."
printError (ErrorFixity (Just Range
r))
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Error: Multiple fixity declarations."
printError (ErrorGlobal Range
r)
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Error: With --global, all declarations in the given file must be imports."
printError (ErrorOpen Range
r QName
n)
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Error: Module not found " forall a. Semigroup a => a -> a -> a
<> Text -> Text
parens (QName -> Text
printQName QName
n) forall a. Semigroup a => a -> a -> a
<> Text
"."
printError (ErrorPolarity (Just Range
r))
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Error: Multiple polarity declarations."
printError (ErrorRoot QName
n QName
n')
  = Text -> Text -> Text
printMessage (QName -> Text
printQName QName
n)
  forall a b. (a -> b) -> a -> b
$ Text
"Error: Root not found " forall a. Semigroup a => a -> a -> a
<> Text -> Text
parens (Text -> Text
quote (QName -> Text
printQName QName
n')) forall a. Semigroup a => a -> a -> a
<> Text
"."
printError (ErrorUnsupported UnsupportedError
e Range
r)
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Error: " forall a. Semigroup a => a -> a -> a
<> UnsupportedError -> Text
printUnsupportedError UnsupportedError
e forall a. Semigroup a => a -> a -> a
<> Text
" not supported."

printError (ErrorDeclaration (DeclarationException CallStack
_ DeclarationException'
e))
  = Range -> Text
printRange (forall a. HasRange a => a -> Range
getRange DeclarationException'
e) forall a. Semigroup a => a -> a -> a
<> Text
"\n" forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (forall a. Pretty a => a -> String
prettyShow DeclarationException'
e)
printError (ErrorFile String
p)
  = String -> Text
printErrorFile String
p
printError (ErrorFixity Maybe Range
Nothing)
  = Text
"Error: Multiple fixity declarations."
printError Error
ErrorInclude
  = Text
"Error: Invalid path-related options."
printError (ErrorInternal InternalError
e)
  = InternalError -> Text
printInternalError InternalError
e
printError (ErrorParse ParseError
e)
  = String -> Text
T.pack (forall a. Pretty a => a -> String
prettyShow ParseError
e)
printError (ErrorPolarity Maybe Range
Nothing)
  = Text
"Error: Multiple polarity declarations."

printErrorFile
  :: FilePath
  -> Text
printErrorFile :: String -> Text
printErrorFile String
p
  = Text
"Error: File not found " forall a. Semigroup a => a -> a -> a
<> Text -> Text
parens (String -> Text
T.pack String
p) forall a. Semigroup a => a -> a -> a
<> Text
"."

printInternalError
  :: InternalError
  -> Text
printInternalError :: InternalError -> Text
printInternalError (ErrorConstructor Range
r)
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Internal error: Invalid data constructor."
printInternalError (ErrorMacro Range
r)
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Internal error: Invalid module application."
printInternalError (ErrorModuleName String
n)
  = Text -> Text -> Text
printMessage (String -> Text
T.pack String
n)
  forall a b. (a -> b) -> a -> b
$ Text
"Internal error: Empty top-level module name."
printInternalError (ErrorName Range
r)
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Internal error: Invalid name."
printInternalError (ErrorRenaming Range
r)
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Internal error: Invalid renaming directive."
printInternalError (ErrorUnexpected UnexpectedError
e Range
r)
  = Text -> Text -> Text
printMessage (Range -> Text
printRange Range
r)
  forall a b. (a -> b) -> a -> b
$ Text
"Internal error: Unexpected constructor "
    forall a. Semigroup a => a -> a -> a
<> Text -> Text
quote (UnexpectedError -> Text
printUnexpectedError UnexpectedError
e) forall a. Semigroup a => a -> a -> a
<> Text
"."

printUnexpectedError
  :: UnexpectedError
  -> Text
printUnexpectedError :: UnexpectedError -> Text
printUnexpectedError UnexpectedError
UnexpectedAbsurd
  = Text
"Absurd"
printUnexpectedError UnexpectedError
UnexpectedAs
  = Text
"As"
printUnexpectedError UnexpectedError
UnexpectedDontCare
  = Text
"DontCare"
printUnexpectedError UnexpectedError
UnexpectedETel
  = Text
"ETel"
printUnexpectedError UnexpectedError
UnexpectedEllipsis
  = Text
"Ellipsis"
printUnexpectedError UnexpectedError
UnexpectedEqual
  = Text
"Equal"
printUnexpectedError UnexpectedError
UnexpectedField
  = Text
"Field"
printUnexpectedError UnexpectedError
UnexpectedNiceFunClause
  = Text
"NiceFunClause"
printUnexpectedError UnexpectedError
UnexpectedOpApp
  = Text
"OpApp"
printUnexpectedError UnexpectedError
UnexpectedOpAppP
  = Text
"OpAppP"

printUnsupportedError
  :: UnsupportedError
  -> Text
printUnsupportedError :: UnsupportedError -> Text
printUnsupportedError UnsupportedError
UnsupportedLoneConstructor
  = Text
"Lone constructors"
printUnsupportedError UnsupportedError
UnsupportedMacro
  = Text
"Record module instance applications"
printUnsupportedError UnsupportedError
UnsupportedUnquote
  = Text
"Unquoting primitives"

-- ## Unused

-- | Print a collection of unused items and files.
printUnused
  :: Unused
  -> Maybe Text
printUnused :: Unused -> Maybe Text
printUnused (Unused [String]
ps UnusedItems
is)
  = Maybe Text -> Maybe Text -> Maybe Text
printUnusedWith
    ([String] -> Maybe Text
printUnusedFiles [String]
ps)
    (UnusedItems -> Maybe Text
printUnusedItems UnusedItems
is)

printUnusedWith
  :: Maybe Text
  -> Maybe Text
  -> Maybe Text
printUnusedWith :: Maybe Text -> Maybe Text -> Maybe Text
printUnusedWith Maybe Text
Nothing Maybe Text
Nothing
  = forall a. Maybe a
Nothing
printUnusedWith Maybe Text
Nothing (Just Text
t2)
  = forall a. a -> Maybe a
Just Text
t2
printUnusedWith (Just Text
t1) Maybe Text
Nothing
  = forall a. a -> Maybe a
Just Text
t1
printUnusedWith (Just Text
t1) (Just Text
t2)
  = forall a. a -> Maybe a
Just (Text -> [Text] -> Text
T.intercalate Text
"\n" [Text
t1, Text
t2])
    
printUnusedFiles
  :: [FilePath]
  -> Maybe Text
printUnusedFiles :: [String] -> Maybe Text
printUnusedFiles []
  = forall a. Maybe a
Nothing
printUnusedFiles ps :: [String]
ps@(String
_ : [String]
_)
  = forall a. a -> Maybe a
Just (Text -> [Text] -> Text
T.intercalate Text
"\n" (String -> Text
printUnusedFile forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
ps))

printUnusedFile
  :: FilePath
  -> Text
printUnusedFile :: String -> Text
printUnusedFile String
p
  = Text -> Text -> Text
printMessageIndent (String -> Text
T.pack String
p) Text
"unused file"

-- | Print a collection of unused items.
printUnusedItems
  :: UnusedItems
  -> Maybe Text
printUnusedItems :: UnusedItems -> Maybe Text
printUnusedItems (UnusedItems [])
  = forall a. Maybe a
Nothing
printUnusedItems (UnusedItems rs :: [(Range, RangeInfo)]
rs@((Range, RangeInfo)
_ : [(Range, RangeInfo)]
_))
  = forall a. a -> Maybe a
Just (Text -> [Text] -> Text
T.intercalate Text
"\n" (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Range -> RangeInfo -> Text
printRangeInfoWith forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Range, RangeInfo)]
rs))

-- | Print a message indicating that no unused code was found.
printNothing
  :: Text
printNothing :: Text
printNothing
  = Text
"No unused code."

printRangeInfoWith
  :: Range
  -> RangeInfo
  -> Text
printRangeInfoWith :: Range -> RangeInfo -> Text
printRangeInfoWith Range
r RangeInfo
i
  = Text -> Text -> Text
printMessageIndent (Range -> Text
printRange Range
r) (RangeInfo -> Text
printRangeInfo RangeInfo
i)

printRangeInfo
  :: RangeInfo
  -> Text
printRangeInfo :: RangeInfo -> Text
printRangeInfo (RangeNamed RangeType
t QName
n)
  = [Text] -> Text
T.unwords [Text
"unused", RangeType -> Text
printRangeType RangeType
t, Text -> Text
quote (QName -> Text
printQName QName
n)]
printRangeInfo RangeInfo
RangeMutual
  = Text
"unused mutually recursive definition"

printRangeType
  :: RangeType
  -> Text
printRangeType :: RangeType -> Text
printRangeType RangeType
RangeData
  = Text
"data type"
printRangeType RangeType
RangeDefinition
  = Text
"definition"
printRangeType RangeType
RangeImport
  = Text
"import"
printRangeType RangeType
RangeImportItem
  = Text
"imported item"
printRangeType RangeType
RangeModule
  = Text
"module"
printRangeType RangeType
RangeModuleItem
  = Text
"module assignment item"
printRangeType RangeType
RangeOpen
  = Text
"open"
printRangeType RangeType
RangeOpenItem
  = Text
"opened item"
printRangeType RangeType
RangePatternSynonym
  = Text
"pattern synonym"
printRangeType RangeType
RangePostulate
  = Text
"postulate"
printRangeType RangeType
RangeRecord
  = Text
"record"
printRangeType RangeType
RangeRecordConstructor
  = Text
"record constructor"
printRangeType RangeType
RangeVariable
  = Text
"variable"