{- |
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.List.NonEmpty
  (NonEmpty(..))
import qualified Data.List.NonEmpty
  as NonEmpty
import Data.Maybe
  (mapMaybe)
import Data.Semigroup
  (sconcat)
import System.FilePath
  ((</>), (<.>), splitDirectories)

-- ## Definitions

-- | An unqualified name, represented as a list of name parts.
newtype Name
  = Name
  { Name -> NonEmpty NamePart
nameParts
    :: NonEmpty NamePart
  } deriving (Name -> Name -> Bool
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
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
Ord, Int -> Name -> ShowS
[Name] -> ShowS
Name -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Name] -> ShowS
$cshowList :: [Name] -> ShowS
show :: Name -> [Char]
$cshow :: Name -> [Char]
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
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
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
Ord, Int -> QName -> ShowS
[QName] -> ShowS
QName -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [QName] -> ShowS
$cshowList :: [QName] -> ShowS
show :: QName -> [Char]
$cshow :: QName -> [Char]
showsPrec :: Int -> QName -> ShowS
$cshowsPrec :: Int -> QName -> ShowS
Show)

-- ## Interface

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

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

isOperator
  :: Name
  -> Bool
isOperator :: Name -> Bool
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 forall a. Eq a => a -> a -> Bool
== Name
n
  = forall a. a -> Maybe a
Just QName
ns
stripPrefix (Qual Name
m QName
ms) (Qual Name
n QName
ns) | Name
m forall a. Eq a => a -> a -> Bool
== Name
n
  = QName -> QName -> Maybe QName
stripPrefix QName
ms QName
ns
stripPrefix QName
_ 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
_)
  = forall a. Maybe a
Nothing
fromName (N.Name Range
_ NameInScope
_ NonEmpty NamePart
n)
  = forall a. a -> Maybe a
Just (NonEmpty NamePart -> Name
Name NonEmpty 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
_)
  = forall a. Maybe a
Nothing
fromNameRange (N.Name Range
r NameInScope
_ NonEmpty NamePart
n)
  = forall a. a -> Maybe a
Just (Range
r, NonEmpty NamePart -> Name
Name NonEmpty 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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Maybe Name
fromName Name
n 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)
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> QName
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)
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName -> QName
Qual forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Maybe Name
fromName Name
n 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
_)
  = 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
  -> QName
fromModuleName :: TopLevelModuleName -> QName
fromModuleName (TopLevelModuleName Range
_ ([Char]
n :| [[Char]]
ns))
  = [Char] -> [[Char]] -> QName
fromStrings [Char]
n [[Char]]
ns

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

fromString
  :: String
  -> Name
fromString :: [Char] -> Name
fromString [Char]
n
  = NonEmpty NamePart -> Name
Name ([Char] -> NamePart
Id [Char]
n forall a. a -> [a] -> NonEmpty a
:| [])

-- | Conversion to Agda name type.
toName
  :: Name
  -> N.Name
toName :: Name -> Name
toName (Name NonEmpty NamePart
n)
  = Range -> NameInScope -> NonEmpty NamePart -> Name
N.Name forall a. Range' a
NoRange NameInScope
NotInScope NonEmpty 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 -> [Char]
namePath (Name NonEmpty NamePart
ps)
  = forall a. Semigroup a => NonEmpty a -> a
sconcat (forall a. Show a => a -> [Char]
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty NamePart
ps)

-- | Convert a module name to a 'FilePath'.
qNamePath
  :: QName
  -> FilePath
qNamePath :: QName -> [Char]
qNamePath (QName Name
n)
  = Name -> [Char]
namePath Name
n [Char] -> ShowS
<.> [Char]
"agda"
qNamePath (Qual Name
n QName
ns)
  = Name -> [Char]
namePath Name
n [Char] -> ShowS
</> QName -> [Char]
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 :: [Char] -> [Char] -> Maybe QName
pathQName [Char]
p [Char]
p'
  = forall a. Eq a => [a] -> [a] -> Maybe [a]
List.stripPrefix ([Char] -> [[Char]]
splitDirectories [Char]
p) ([Char] -> [[Char]]
splitDirectories [Char]
p')
  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [[Char]] -> Maybe QName
pathQNameRelative

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

pathName
  :: String
  -> Maybe Name
pathName :: [Char] -> Maybe Name
pathName [Char]
n
  = NonEmpty NamePart -> Name
Name forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> NonEmpty a
:| []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> NamePart
Id forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Eq a => [a] -> [a] -> Maybe [a]
stripSuffix [Char]
".agda" [Char]
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 :: [[Char]] -> [Name] -> [Name]
matchOperators [[Char]]
ss
  = forall a. (a -> Bool) -> [a] -> [a]
filter (\Name
n -> Name -> Bool
isOperator Name
n Bool -> Bool -> Bool
&& forall a. Eq a => [a] -> [a] -> Bool
isSubsequenceOf (Name -> [[Char]]
nameIds Name
n) [[Char]]
ss)