{- |
Module: Agda.Unused.Types.Name

Names and qualified names.
-}
module Agda.Unused.Types.Name

  ( -- * Definitions

    NamePart(..)
  , Name(..)
  , QName(..)

    -- * Interface

  , nameIds
  , stripPrefix

    -- * Conversion

  , fromName
  , fromNameRange
  , fromQName
  , fromQNameRange
  , fromAsName
  , fromModuleName

  , toName
  , toQName

    -- * Paths

  , qNamePath
  , pathQName

    -- * Match

  , matchOperators

  ) where

import Agda.Unused.Utils
  (stripSuffix)

import Agda.Syntax.Concrete
  (AsName, AsName'(..))
import Agda.Syntax.Concrete.Name
  (NameInScope(..), NamePart(..), TopLevelModuleName(..))
import qualified Agda.Syntax.Concrete.Name
  as N
import Agda.Syntax.Position
  (Range, Range'(..))
import Data.List
  (isSubsequenceOf)
import qualified Data.List
  as List
import Data.Maybe
  (mapMaybe)
import System.FilePath
  ((</>), (<.>), splitDirectories)

-- ## Definitions

-- | An unqualified name, represented as a list of name parts.
newtype Name
  = Name
  { Name -> [NamePart]
nameParts
    :: [NamePart]
  } deriving (Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c== :: Name -> Name -> Bool
Eq, Eq Name
Eq Name
-> (Name -> Name -> Ordering)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> Ord Name
Name -> Name -> Bool
Name -> Name -> Ordering
Name -> Name -> Name
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Name -> Name -> Name
$cmin :: Name -> Name -> Name
max :: Name -> Name -> Name
$cmax :: Name -> Name -> Name
>= :: Name -> Name -> Bool
$c>= :: Name -> Name -> Bool
> :: Name -> Name -> Bool
$c> :: Name -> Name -> Bool
<= :: Name -> Name -> Bool
$c<= :: Name -> Name -> Bool
< :: Name -> Name -> Bool
$c< :: Name -> Name -> Bool
compare :: Name -> Name -> Ordering
$ccompare :: Name -> Name -> Ordering
$cp1Ord :: Eq Name
Ord, Int -> Name -> ShowS
[Name] -> ShowS
Name -> String
(Int -> Name -> ShowS)
-> (Name -> String) -> ([Name] -> ShowS) -> Show Name
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Name] -> ShowS
$cshowList :: [Name] -> ShowS
show :: Name -> String
$cshow :: Name -> String
showsPrec :: Int -> Name -> ShowS
$cshowsPrec :: Int -> Name -> ShowS
Show)

-- | A qualified name.
data QName where

  QName
    :: !Name
    -> QName

  Qual
    :: !Name
    -> !QName
    -> QName

  deriving (QName -> QName -> Bool
(QName -> QName -> Bool) -> (QName -> QName -> Bool) -> Eq QName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QName -> QName -> Bool
$c/= :: QName -> QName -> Bool
== :: QName -> QName -> Bool
$c== :: QName -> QName -> Bool
Eq, Eq QName
Eq QName
-> (QName -> QName -> Ordering)
-> (QName -> QName -> Bool)
-> (QName -> QName -> Bool)
-> (QName -> QName -> Bool)
-> (QName -> QName -> Bool)
-> (QName -> QName -> QName)
-> (QName -> QName -> QName)
-> Ord QName
QName -> QName -> Bool
QName -> QName -> Ordering
QName -> QName -> QName
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: QName -> QName -> QName
$cmin :: QName -> QName -> QName
max :: QName -> QName -> QName
$cmax :: QName -> QName -> QName
>= :: QName -> QName -> Bool
$c>= :: QName -> QName -> Bool
> :: QName -> QName -> Bool
$c> :: QName -> QName -> Bool
<= :: QName -> QName -> Bool
$c<= :: QName -> QName -> Bool
< :: QName -> QName -> Bool
$c< :: QName -> QName -> Bool
compare :: QName -> QName -> Ordering
$ccompare :: QName -> QName -> Ordering
$cp1Ord :: Eq QName
Ord, Int -> QName -> ShowS
[QName] -> ShowS
QName -> String
(Int -> QName -> ShowS)
-> (QName -> String) -> ([QName] -> ShowS) -> Show QName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QName] -> ShowS
$cshowList :: [QName] -> ShowS
show :: QName -> String
$cshow :: QName -> String
showsPrec :: Int -> QName -> ShowS
$cshowsPrec :: Int -> QName -> ShowS
Show)

-- ## Interface

-- | Get the non-hole parts of a 'Name'.
nameIds
  :: Name
  -> [String]
nameIds :: Name -> [String]
nameIds (Name [NamePart]
ps)
  = (NamePart -> Maybe String) -> [NamePart] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe NamePart -> Maybe String
namePartId [NamePart]
ps

namePartId
  :: NamePart
  -> Maybe String
namePartId :: NamePart -> Maybe String
namePartId NamePart
Hole
  = Maybe String
forall a. Maybe a
Nothing
namePartId (Id String
s)
  = String -> Maybe String
forall a. a -> Maybe a
Just String
s

isOperator
  :: Name
  -> Bool
isOperator :: Name -> Bool
isOperator (Name [])
  = Bool
False
isOperator (Name (NamePart
_ : []))
  = Bool
False
isOperator (Name (NamePart
_ : NamePart
_ : [NamePart]
_))
  = Bool
True

-- | If the first module name is a prefix of the second module name, then strip
-- the prefix, otherwise return 'Nothing'.
stripPrefix
  :: QName
  -- ^ The prefix to strip
  -> QName
  -> Maybe QName
stripPrefix :: QName -> QName -> Maybe QName
stripPrefix (QName Name
m) (Qual Name
n QName
ns) | Name
m Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n
  = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
ns
stripPrefix (Qual Name
m QName
ms) (Qual Name
n QName
ns) | Name
m Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n
  = QName -> QName -> Maybe QName
stripPrefix QName
ms QName
ns
stripPrefix QName
_ QName
_
  = Maybe QName
forall a. Maybe a
Nothing

-- ## Conversion

-- | Conversion from Agda name type.
fromName
  :: N.Name
  -> Maybe Name
fromName :: Name -> Maybe Name
fromName (N.NoName Range
_ NameId
_)
  = Maybe Name
forall a. Maybe a
Nothing
fromName (N.Name Range
_ NameInScope
_ [NamePart]
n)
  = Name -> Maybe Name
forall a. a -> Maybe a
Just ([NamePart] -> Name
Name [NamePart]
n)

-- | Like 'fromName', but also return a 'Range'.
fromNameRange
  :: N.Name
  -> Maybe (Range, Name)
fromNameRange :: Name -> Maybe (Range, Name)
fromNameRange (N.NoName Range
_ NameId
_)
  = Maybe (Range, Name)
forall a. Maybe a
Nothing
fromNameRange (N.Name Range
r NameInScope
_ [NamePart]
n)
  = (Range, Name) -> Maybe (Range, Name)
forall a. a -> Maybe a
Just (Range
r, [NamePart] -> Name
Name [NamePart]
n)

-- | Conversion from Agda qualified name type.
fromQName
  :: N.QName
  -> Maybe QName
fromQName :: QName -> Maybe QName
fromQName (N.QName Name
n)
  = Name -> QName
QName (Name -> QName) -> Maybe Name -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Maybe Name
fromName Name
n
fromQName (N.Qual Name
n QName
ns)
  = Name -> QName -> QName
Qual (Name -> QName -> QName) -> Maybe Name -> Maybe (QName -> QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Maybe Name
fromName Name
n Maybe (QName -> QName) -> Maybe QName -> Maybe QName
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QName -> Maybe QName
fromQName QName
ns

-- | Like 'fromQName', but also return a 'Range'.
fromQNameRange
  :: N.QName
  -> Maybe (Range, QName)
fromQNameRange :: QName -> Maybe (Range, QName)
fromQNameRange (N.QName Name
n)
  = (Name -> QName) -> (Range, Name) -> (Range, QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> QName
QName ((Range, Name) -> (Range, QName))
-> Maybe (Range, Name) -> Maybe (Range, QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Maybe (Range, Name)
fromNameRange Name
n
fromQNameRange (N.Qual Name
n QName
ns)
  = (QName -> QName) -> (Range, QName) -> (Range, QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName -> QName) -> (Range, QName) -> (Range, QName))
-> (Name -> QName -> QName)
-> Name
-> (Range, QName)
-> (Range, QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName -> QName
Qual (Name -> (Range, QName) -> (Range, QName))
-> Maybe Name -> Maybe ((Range, QName) -> (Range, QName))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Maybe Name
fromName Name
n Maybe ((Range, QName) -> (Range, QName))
-> Maybe (Range, QName) -> Maybe (Range, QName)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QName -> Maybe (Range, QName)
fromQNameRange QName
ns

-- | Conversion from Agda as-name type.
fromAsName
  :: AsName
  -> Maybe Name
fromAsName :: AsName -> Maybe Name
fromAsName (AsName (Left Expr
_) Range
_)
  = Maybe Name
forall a. Maybe a
Nothing
fromAsName (AsName (Right Name
n) Range
_)
  = Name -> Maybe Name
fromName Name
n

-- | Conversion from Agda top level module name type.
fromModuleName
  :: TopLevelModuleName
  -> Maybe QName
fromModuleName :: TopLevelModuleName -> Maybe QName
fromModuleName (TopLevelModuleName Range
_ [])
  = Maybe QName
forall a. Maybe a
Nothing
fromModuleName (TopLevelModuleName Range
_ (String
n : [String]
ns))
  = QName -> Maybe QName
forall a. a -> Maybe a
Just (String -> [String] -> QName
fromStrings String
n [String]
ns)

fromStrings
  :: String
  -> [String]
  -> QName
fromStrings :: String -> [String] -> QName
fromStrings String
n []
  = Name -> QName
QName (String -> Name
fromString String
n)
fromStrings String
n (String
n' : [String]
ns)
  = Name -> QName -> QName
Qual (String -> Name
fromString String
n) (String -> [String] -> QName
fromStrings String
n' [String]
ns)

fromString
  :: String
  -> Name
fromString :: String -> Name
fromString String
n
  = [NamePart] -> Name
Name [String -> NamePart
Id String
n]

-- | Conversion to Agda name type.
toName
  :: Name
  -> N.Name
toName :: Name -> Name
toName (Name [NamePart]
n)
  = Range -> NameInScope -> [NamePart] -> Name
N.Name Range
forall a. Range' a
NoRange NameInScope
NotInScope [NamePart]
n

-- | Conversion to Agda qualified name type.
toQName
  :: QName
  -> N.QName
toQName :: QName -> QName
toQName (QName Name
n)
  = Name -> QName
N.QName (Name -> Name
toName Name
n)
toQName (Qual Name
n QName
ns)
  = Name -> QName -> QName
N.Qual (Name -> Name
toName Name
n) (QName -> QName
toQName QName
ns)

-- ## Paths

namePath
  :: Name
  -> String
namePath :: Name -> String
namePath (Name [NamePart]
ps)
  = [String] -> String
forall a. Monoid a => [a] -> a
mconcat (NamePart -> String
forall a. Show a => a -> String
show (NamePart -> String) -> [NamePart] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamePart]
ps)

-- | Convert a module name to a 'FilePath'.
qNamePath
  :: QName
  -> FilePath
qNamePath :: QName -> String
qNamePath (QName Name
n)
  = Name -> String
namePath Name
n String -> ShowS
<.> String
"agda"
qNamePath (Qual Name
n QName
ns)
  = Name -> String
namePath Name
n String -> ShowS
</> QName -> String
qNamePath QName
ns

-- | Convert a 'FilePath' to a module name.
pathQName
  :: FilePath
  -- ^ The project root directory.
  -> FilePath
  -- ^ The path to the module.
  -> Maybe QName
pathQName :: String -> String -> Maybe QName
pathQName String
p String
p'
  = [String] -> [String] -> Maybe [String]
forall a. Eq a => [a] -> [a] -> Maybe [a]
List.stripPrefix (String -> [String]
splitDirectories String
p) (String -> [String]
splitDirectories String
p')
  Maybe [String] -> ([String] -> Maybe QName) -> Maybe QName
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [String] -> Maybe QName
pathQNameRelative

pathQNameRelative
  :: [String]
  -> Maybe QName
pathQNameRelative :: [String] -> Maybe QName
pathQNameRelative []
  = Maybe QName
forall a. Maybe a
Nothing
pathQNameRelative [String
n]
  = Name -> QName
QName (Name -> QName) -> Maybe Name -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Maybe Name
pathName String
n
pathQNameRelative (String
n : ns :: [String]
ns@(String
_ : [String]
_))
  = Name -> QName -> QName
Qual ([NamePart] -> Name
Name [String -> NamePart
Id String
n]) (QName -> QName) -> Maybe QName -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String] -> Maybe QName
pathQNameRelative [String]
ns

pathName
  :: String
  -> Maybe Name
pathName :: String -> Maybe Name
pathName String
n
  = [NamePart] -> Name
Name ([NamePart] -> Name) -> (String -> [NamePart]) -> String -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamePart -> [NamePart] -> [NamePart]
forall a. a -> [a] -> [a]
: []) (NamePart -> [NamePart])
-> (String -> NamePart) -> String -> [NamePart]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> NamePart
Id (String -> Name) -> Maybe String -> Maybe Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripSuffix String
".agda" String
n

-- ## Match

-- | Given a string of tokens found in a raw application, filter the given list
-- of names by whether each name's identifiers appear in order.
matchOperators
  :: [String]
  -- ^ A string of tokens found in a raw application.
  -> [Name]
  -- ^ A list of names to consider.
  -> [Name]
matchOperators :: [String] -> [Name] -> [Name]
matchOperators [String]
ss
  = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Name
n -> Name -> Bool
isOperator Name
n Bool -> Bool -> Bool
&& [String] -> [String] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSubsequenceOf (Name -> [String]
nameIds Name
n) [String]
ss)