{-| Abstract names carry unique identifiers and stuff.
-}
module Agda.Syntax.Abstract.Name
  ( module Agda.Syntax.Abstract.Name
  , IsNoName(..)
  , FreshNameMode(..)
  ) where

import Prelude hiding (length)

import Control.DeepSeq

import Data.Foldable (length)
import Data.Function
import Data.Hashable (Hashable(..))
import qualified Data.List as List
import Data.Maybe
import Data.Void

import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name (IsNoName(..), NumHoles(..), NameInScope(..), LensInScope(..), FreshNameMode(..))
import qualified Agda.Syntax.Concrete.Name as C

import Agda.Utils.Functor
import Agda.Utils.Lens
import qualified Agda.Utils.List as L
import Agda.Utils.List1 (List1, pattern (:|), (<|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Pretty
import Agda.Utils.Size

import Agda.Utils.Impossible

-- | A name is a unique identifier and a suggestion for a concrete name. The
--   concrete name contains the source location (if any) of the name. The
--   source location of the binding site is also recorded.
data Name = Name
  { Name -> NameId
nameId           :: !NameId
  , Name -> Name
nameConcrete     :: C.Name  -- ^ The concrete name used for this instance
  , Name -> Name
nameCanonical    :: C.Name  -- ^ The concrete name in the original definition (needed by primShowQName, see #4735)
  , Name -> Range
nameBindingSite  :: Range
  , Name -> Fixity'
nameFixity       :: Fixity'
  , Name -> Bool
nameIsRecordName :: Bool
      -- ^ Is this the name of the invisible record variable `self`?
      --   Should not be printed or displayed in the context, see issue #3584.
  }

-- | Useful for debugging scoping problems
uglyShowName :: Name -> String
uglyShowName :: Name -> String
uglyShowName Name
x = forall a. Show a => a -> String
show (Name -> NameId
nameId Name
x, Name -> Name
nameConcrete Name
x)

-- | Qualified names are non-empty lists of names. Equality on qualified names
--   are just equality on the last name, i.e. the module part is just
--   for show.
--
-- The 'SetRange' instance for qualified names sets all individual
-- ranges (including those of the module prefix) to the given one.
data QName = QName { QName -> ModuleName
qnameModule :: ModuleName
                   , QName -> Name
qnameName   :: Name
                   }

-- | Something preceeded by a qualified name.
data QNamed a = QNamed
  { forall a. QNamed a -> QName
qname  :: QName
  , forall a. QNamed a -> a
qnamed :: a
  }
  deriving (forall a b. a -> QNamed b -> QNamed a
forall a b. (a -> b) -> QNamed a -> QNamed b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> QNamed b -> QNamed a
$c<$ :: forall a b. a -> QNamed b -> QNamed a
fmap :: forall a b. (a -> b) -> QNamed a -> QNamed b
$cfmap :: forall a b. (a -> b) -> QNamed a -> QNamed b
Functor, forall a. Eq a => a -> QNamed a -> Bool
forall a. Num a => QNamed a -> a
forall a. Ord a => QNamed a -> a
forall m. Monoid m => QNamed m -> m
forall a. QNamed a -> Bool
forall a. QNamed a -> Int
forall a. QNamed a -> [a]
forall a. (a -> a -> a) -> QNamed a -> a
forall m a. Monoid m => (a -> m) -> QNamed a -> m
forall b a. (b -> a -> b) -> b -> QNamed a -> b
forall a b. (a -> b -> b) -> b -> QNamed a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => QNamed a -> a
$cproduct :: forall a. Num a => QNamed a -> a
sum :: forall a. Num a => QNamed a -> a
$csum :: forall a. Num a => QNamed a -> a
minimum :: forall a. Ord a => QNamed a -> a
$cminimum :: forall a. Ord a => QNamed a -> a
maximum :: forall a. Ord a => QNamed a -> a
$cmaximum :: forall a. Ord a => QNamed a -> a
elem :: forall a. Eq a => a -> QNamed a -> Bool
$celem :: forall a. Eq a => a -> QNamed a -> Bool
length :: forall a. QNamed a -> Int
$clength :: forall a. QNamed a -> Int
null :: forall a. QNamed a -> Bool
$cnull :: forall a. QNamed a -> Bool
toList :: forall a. QNamed a -> [a]
$ctoList :: forall a. QNamed a -> [a]
foldl1 :: forall a. (a -> a -> a) -> QNamed a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> QNamed a -> a
foldr1 :: forall a. (a -> a -> a) -> QNamed a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> QNamed a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> QNamed a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> QNamed a -> b
foldl :: forall b a. (b -> a -> b) -> b -> QNamed a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> QNamed a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> QNamed a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> QNamed a -> b
foldr :: forall a b. (a -> b -> b) -> b -> QNamed a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> QNamed a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> QNamed a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> QNamed a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> QNamed a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> QNamed a -> m
fold :: forall m. Monoid m => QNamed m -> m
$cfold :: forall m. Monoid m => QNamed m -> m
Foldable, Functor QNamed
Foldable QNamed
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => QNamed (m a) -> m (QNamed a)
forall (f :: * -> *) a.
Applicative f =>
QNamed (f a) -> f (QNamed a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> QNamed a -> m (QNamed b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> QNamed a -> f (QNamed b)
sequence :: forall (m :: * -> *) a. Monad m => QNamed (m a) -> m (QNamed a)
$csequence :: forall (m :: * -> *) a. Monad m => QNamed (m a) -> m (QNamed a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> QNamed a -> m (QNamed b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> QNamed a -> m (QNamed b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
QNamed (f a) -> f (QNamed a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
QNamed (f a) -> f (QNamed a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> QNamed a -> f (QNamed b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> QNamed a -> f (QNamed b)
Traversable)

-- | A module name is just a qualified name.
--
-- The 'SetRange' instance for module names sets all individual ranges
-- to the given one.
newtype ModuleName = MName { ModuleName -> [Name]
mnameToList :: [Name] }
  deriving (ModuleName -> ModuleName -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ModuleName -> ModuleName -> Bool
$c/= :: ModuleName -> ModuleName -> Bool
== :: ModuleName -> ModuleName -> Bool
$c== :: ModuleName -> ModuleName -> Bool
Eq, Eq ModuleName
ModuleName -> ModuleName -> Bool
ModuleName -> ModuleName -> Ordering
ModuleName -> ModuleName -> ModuleName
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 :: ModuleName -> ModuleName -> ModuleName
$cmin :: ModuleName -> ModuleName -> ModuleName
max :: ModuleName -> ModuleName -> ModuleName
$cmax :: ModuleName -> ModuleName -> ModuleName
>= :: ModuleName -> ModuleName -> Bool
$c>= :: ModuleName -> ModuleName -> Bool
> :: ModuleName -> ModuleName -> Bool
$c> :: ModuleName -> ModuleName -> Bool
<= :: ModuleName -> ModuleName -> Bool
$c<= :: ModuleName -> ModuleName -> Bool
< :: ModuleName -> ModuleName -> Bool
$c< :: ModuleName -> ModuleName -> Bool
compare :: ModuleName -> ModuleName -> Ordering
$ccompare :: ModuleName -> ModuleName -> Ordering
Ord)

-- | Ambiguous qualified names. Used for overloaded constructors.
--
-- Invariant: All the names in the list must have the same concrete,
-- unqualified name.  (This implies that they all have the same 'Range').
newtype AmbiguousQName = AmbQ { AmbiguousQName -> List1 QName
unAmbQ :: List1 QName }
  deriving (AmbiguousQName -> AmbiguousQName -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AmbiguousQName -> AmbiguousQName -> Bool
$c/= :: AmbiguousQName -> AmbiguousQName -> Bool
== :: AmbiguousQName -> AmbiguousQName -> Bool
$c== :: AmbiguousQName -> AmbiguousQName -> Bool
Eq, Eq AmbiguousQName
AmbiguousQName -> AmbiguousQName -> Bool
AmbiguousQName -> AmbiguousQName -> Ordering
AmbiguousQName -> AmbiguousQName -> AmbiguousQName
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 :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName
$cmin :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName
max :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName
$cmax :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName
>= :: AmbiguousQName -> AmbiguousQName -> Bool
$c>= :: AmbiguousQName -> AmbiguousQName -> Bool
> :: AmbiguousQName -> AmbiguousQName -> Bool
$c> :: AmbiguousQName -> AmbiguousQName -> Bool
<= :: AmbiguousQName -> AmbiguousQName -> Bool
$c<= :: AmbiguousQName -> AmbiguousQName -> Bool
< :: AmbiguousQName -> AmbiguousQName -> Bool
$c< :: AmbiguousQName -> AmbiguousQName -> Bool
compare :: AmbiguousQName -> AmbiguousQName -> Ordering
$ccompare :: AmbiguousQName -> AmbiguousQName -> Ordering
Ord, AmbiguousQName -> ()
forall a. (a -> ()) -> NFData a
rnf :: AmbiguousQName -> ()
$crnf :: AmbiguousQName -> ()
NFData)

-- | A singleton "ambiguous" name.
unambiguous :: QName -> AmbiguousQName
unambiguous :: QName -> AmbiguousQName
unambiguous QName
x = List1 QName -> AmbiguousQName
AmbQ (QName
x forall a. a -> [a] -> NonEmpty a
:| [])

-- | Get the first of the ambiguous names.
headAmbQ :: AmbiguousQName -> QName
headAmbQ :: AmbiguousQName -> QName
headAmbQ (AmbQ List1 QName
xs) = forall a. NonEmpty a -> a
List1.head List1 QName
xs

-- | Is a name ambiguous.
isAmbiguous :: AmbiguousQName -> Bool
isAmbiguous :: AmbiguousQName -> Bool
isAmbiguous (AmbQ (QName
_ :| [QName]
xs)) = Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QName]
xs)

-- | Get the name if unambiguous.
getUnambiguous :: AmbiguousQName -> Maybe QName
getUnambiguous :: AmbiguousQName -> Maybe QName
getUnambiguous (AmbQ (QName
x :| [])) = forall a. a -> Maybe a
Just QName
x
getUnambiguous AmbiguousQName
_                = forall a. Maybe a
Nothing

-- | A name suffix
data Suffix
  = NoSuffix
  | Suffix !Integer
  deriving (Int -> Suffix -> ShowS
[Suffix] -> ShowS
Suffix -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Suffix] -> ShowS
$cshowList :: [Suffix] -> ShowS
show :: Suffix -> String
$cshow :: Suffix -> String
showsPrec :: Int -> Suffix -> ShowS
$cshowsPrec :: Int -> Suffix -> ShowS
Show, Suffix -> Suffix -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Suffix -> Suffix -> Bool
$c/= :: Suffix -> Suffix -> Bool
== :: Suffix -> Suffix -> Bool
$c== :: Suffix -> Suffix -> Bool
Eq, Eq Suffix
Suffix -> Suffix -> Bool
Suffix -> Suffix -> Ordering
Suffix -> Suffix -> Suffix
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 :: Suffix -> Suffix -> Suffix
$cmin :: Suffix -> Suffix -> Suffix
max :: Suffix -> Suffix -> Suffix
$cmax :: Suffix -> Suffix -> Suffix
>= :: Suffix -> Suffix -> Bool
$c>= :: Suffix -> Suffix -> Bool
> :: Suffix -> Suffix -> Bool
$c> :: Suffix -> Suffix -> Bool
<= :: Suffix -> Suffix -> Bool
$c<= :: Suffix -> Suffix -> Bool
< :: Suffix -> Suffix -> Bool
$c< :: Suffix -> Suffix -> Bool
compare :: Suffix -> Suffix -> Ordering
$ccompare :: Suffix -> Suffix -> Ordering
Ord)

instance NFData Suffix where
  rnf :: Suffix -> ()
rnf Suffix
NoSuffix   = ()
  rnf (Suffix Integer
_) = ()

-- | Check whether we are a projection pattern.
class IsProjP a where
  isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)

instance IsProjP a => IsProjP (Arg a) where
  isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP Arg a
p = case forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg a
p of
    Just (ProjOrigin
ProjPostfix , AmbiguousQName
f)
     | forall a. LensHiding a => a -> Hiding
getHiding Arg a
p forall a. Eq a => a -> a -> Bool
/= Hiding
NotHidden -> forall a. Maybe a
Nothing
    Maybe (ProjOrigin, AmbiguousQName)
x -> Maybe (ProjOrigin, AmbiguousQName)
x

instance IsProjP a => IsProjP (Named n a) where
  isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP = forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing

instance IsProjP Void where
  isProjP :: Void -> Maybe (ProjOrigin, AmbiguousQName)
isProjP Void
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

-- | A module is anonymous if the qualification path ends in an underscore.
isAnonymousModuleName :: ModuleName -> Bool
isAnonymousModuleName :: ModuleName -> Bool
isAnonymousModuleName (MName [Name]
mms) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False forall a. IsNoName a => a -> Bool
isNoName forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe a
L.lastMaybe [Name]
mms

-- | Sets the ranges of the individual names in the module name to
-- match those of the corresponding concrete names. If the concrete
-- names are fewer than the number of module name name parts, then the
-- initial name parts get the range 'noRange'.
--
-- @C.D.E \`withRangesOf\` [A, B]@ returns @C.D.E@ but with ranges set
-- as follows:
--
-- * @C@: 'noRange'.
--
-- * @D@: the range of @A@.
--
-- * @E@: the range of @B@.
--
-- Precondition: The number of module name name parts has to be at
-- least as large as the length of the list.

withRangesOf :: ModuleName -> List1 C.Name -> ModuleName
MName [Name]
ms withRangesOf :: ModuleName -> List1 Name -> ModuleName
`withRangesOf` List1 Name
ns = if Int
m forall a. Ord a => a -> a -> Bool
< Int
n then forall a. HasCallStack => a
__IMPOSSIBLE__ else [Name] -> ModuleName
MName forall a b. (a -> b) -> a -> b
$
      forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. SetRange a => Range -> a -> a
setRange (forall a. Int -> a -> [a]
replicate (Int
m forall a. Num a => a -> a -> a
- Int
n) forall a. Range' a
noRange forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. HasRange a => a -> Range
getRange (forall l. IsList l => l -> [Item l]
List1.toList List1 Name
ns)) [Name]
ms
  where
    m :: Int
m = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ms
    n :: Int
n = forall (t :: * -> *) a. Foldable t => t a -> Int
length List1 Name
ns

-- | Like 'withRangesOf', but uses the name parts (qualifier + name)
-- of the qualified name as the list of concrete names.

withRangesOfQ :: ModuleName -> C.QName -> ModuleName
ModuleName
m withRangesOfQ :: ModuleName -> QName -> ModuleName
`withRangesOfQ` QName
q = ModuleName
m ModuleName -> List1 Name -> ModuleName
`withRangesOf` QName -> List1 Name
C.qnameParts QName
q

mnameFromList :: [Name] -> ModuleName
mnameFromList :: [Name] -> ModuleName
mnameFromList = [Name] -> ModuleName
MName

mnameFromList1 :: List1 Name -> ModuleName
mnameFromList1 :: List1 Name -> ModuleName
mnameFromList1 = [Name] -> ModuleName
MName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. IsList l => l -> [Item l]
List1.toList

mnameToList1 :: ModuleName -> List1 Name
mnameToList1 :: ModuleName -> List1 Name
mnameToList1 (MName [Name]
ns) = forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [Name]
ns forall a. HasCallStack => a
__IMPOSSIBLE__ forall a. a -> a
id

noModuleName :: ModuleName
noModuleName :: ModuleName
noModuleName = [Name] -> ModuleName
mnameFromList []

commonParentModule :: ModuleName -> ModuleName -> ModuleName
commonParentModule :: ModuleName -> ModuleName -> ModuleName
commonParentModule ModuleName
m1 ModuleName
m2 =
  [Name] -> ModuleName
mnameFromList forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a] -> [a]
L.commonPrefix (ModuleName -> [Name]
mnameToList ModuleName
m1) (ModuleName -> [Name]
mnameToList ModuleName
m2)

-- | Make a 'Name' from some kind of string.
class MkName a where
  -- | The 'Range' sets the /definition site/ of the name, not the use site.
  mkName :: Range -> NameId -> a -> Name

  mkName_ :: NameId -> a -> Name
  mkName_ = forall a. MkName a => Range -> NameId -> a -> Name
mkName forall a. Range' a
noRange

instance MkName String where
  mkName :: Range -> NameId -> String -> Name
mkName Range
r NameId
i String
s = NameId -> Name -> Range -> Fixity' -> Bool -> Name
makeName NameId
i (Range -> NameInScope -> NameParts -> Name
C.Name forall a. Range' a
noRange NameInScope
InScope (String -> NameParts
C.stringNameParts String
s)) Range
r Fixity'
noFixity' Bool
False

makeName :: NameId -> C.Name -> Range -> Fixity' -> Bool -> Name
makeName :: NameId -> Name -> Range -> Fixity' -> Bool -> Name
makeName NameId
i Name
c Range
r Fixity'
f Bool
rec = NameId -> Name -> Name -> Range -> Fixity' -> Bool -> Name
Name NameId
i Name
c Name
c Range
r Fixity'
f Bool
rec

qnameToList0 :: QName -> [Name]
qnameToList0 :: QName -> [Name]
qnameToList0 = forall l. IsList l => l -> [Item l]
List1.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> List1 Name
qnameToList

qnameToList :: QName -> List1 Name
qnameToList :: QName -> List1 Name
qnameToList (QName ModuleName
m Name
x) = ModuleName -> [Name]
mnameToList ModuleName
m forall a. [a] -> a -> List1 a
`List1.snoc` Name
x

qnameFromList :: List1 Name -> QName
qnameFromList :: List1 Name -> QName
qnameFromList List1 Name
xs = ModuleName -> Name -> QName
QName ([Name] -> ModuleName
mnameFromList forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
List1.init List1 Name
xs) (forall a. NonEmpty a -> a
List1.last List1 Name
xs)

qnameToMName :: QName -> ModuleName
qnameToMName :: QName -> ModuleName
qnameToMName = List1 Name -> ModuleName
mnameFromList1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> List1 Name
qnameToList

mnameToQName :: ModuleName -> QName
mnameToQName :: ModuleName -> QName
mnameToQName = List1 Name -> QName
qnameFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> List1 Name
mnameToList1

showQNameId :: QName -> String
showQNameId :: QName -> String
showQNameId QName
q = forall a. Show a => a -> String
show [Word64]
ns forall a. [a] -> [a] -> [a]
++ String
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ModuleNameHash
m
  where
    is :: [NameId]
is = forall a b. (a -> b) -> [a] -> [b]
map Name -> NameId
nameId forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
mnameToList (QName -> ModuleName
qnameModule QName
q) forall a. [a] -> [a] -> [a]
++ [QName -> Name
qnameName QName
q]
    ns :: [Word64]
ns = [ Word64
n | NameId Word64
n ModuleNameHash
_ <- [NameId]
is ]
    m :: ModuleNameHash
m  = forall a. [a] -> a
head [ ModuleNameHash
m | NameId Word64
_ ModuleNameHash
m <- [NameId]
is ]

-- | Turn a qualified name into a concrete name. This should only be used as a
--   fallback when looking up the right concrete name in the scope fails.
qnameToConcrete :: QName -> C.QName
qnameToConcrete :: QName -> QName
qnameToConcrete (QName ModuleName
m Name
x) =       -- Use the canonical name here (#5048)
   forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name -> QName -> QName
C.Qual forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nameConcrete) (Name -> QName
C.QName forall a b. (a -> b) -> a -> b
$ Name -> Name
nameCanonical Name
x) (ModuleName -> [Name]
mnameToList ModuleName
m)

mnameToConcrete :: ModuleName -> C.QName
mnameToConcrete :: ModuleName -> QName
mnameToConcrete (MName []) = forall a. HasCallStack => a
__IMPOSSIBLE__ -- C.QName C.noName_  -- should never happen?
mnameToConcrete (MName (Name
x:[Name]
xs)) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> QName -> QName
C.Qual (Name -> QName
C.QName forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> a
List1.last List1 Name
cs) forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
List1.init List1 Name
cs
  where
    cs :: List1 Name
cs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Name
nameConcrete (Name
x forall a. a -> [a] -> NonEmpty a
:| [Name]
xs)

qualifyM :: ModuleName -> ModuleName -> ModuleName
qualifyM :: ModuleName -> ModuleName -> ModuleName
qualifyM ModuleName
m1 ModuleName
m2 = [Name] -> ModuleName
mnameFromList forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
mnameToList ModuleName
m1 forall a. [a] -> [a] -> [a]
++ ModuleName -> [Name]
mnameToList ModuleName
m2

qualifyQ :: ModuleName -> QName -> QName
qualifyQ :: ModuleName -> QName -> QName
qualifyQ ModuleName
m QName
x = List1 Name -> QName
qnameFromList forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
mnameToList ModuleName
m forall a. [a] -> NonEmpty a -> NonEmpty a
`List1.prependList` QName -> List1 Name
qnameToList QName
x

qualify :: ModuleName -> Name -> QName
qualify :: ModuleName -> Name -> QName
qualify = ModuleName -> Name -> QName
QName

-- | Convert a 'Name' to a 'QName' (add no module name).
qualify_ :: Name -> QName
qualify_ :: Name -> QName
qualify_ = ModuleName -> Name -> QName
qualify ModuleName
noModuleName

-- | Is the name an operator?

isOperator :: QName -> Bool
isOperator :: QName -> Bool
isOperator = Name -> Bool
C.isOperator forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nameConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName

-- | Is the first module a weak parent of the second?
isLeParentModuleOf :: ModuleName -> ModuleName -> Bool
isLeParentModuleOf :: ModuleName -> ModuleName -> Bool
isLeParentModuleOf = forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ModuleName -> [Name]
mnameToList

-- | Is the first module a proper parent of the second?
isLtParentModuleOf :: ModuleName -> ModuleName -> Bool
isLtParentModuleOf :: ModuleName -> ModuleName -> Bool
isLtParentModuleOf ModuleName
x ModuleName
y =
  forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ (forall a.
(a -> a -> Bool) -> Prefix a -> Prefix a -> Maybe (Prefix a)
L.stripPrefixBy forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ModuleName -> [Name]
mnameToList) ModuleName
x ModuleName
y

-- | Is the first module a weak child of the second?
isLeChildModuleOf :: ModuleName -> ModuleName -> Bool
isLeChildModuleOf :: ModuleName -> ModuleName -> Bool
isLeChildModuleOf = forall a b c. (a -> b -> c) -> b -> a -> c
flip ModuleName -> ModuleName -> Bool
isLeParentModuleOf

-- | Is the first module a proper child of the second?
isLtChildModuleOf :: ModuleName -> ModuleName -> Bool
isLtChildModuleOf :: ModuleName -> ModuleName -> Bool
isLtChildModuleOf = forall a b c. (a -> b -> c) -> b -> a -> c
flip ModuleName -> ModuleName -> Bool
isLtParentModuleOf

isInModule :: QName -> ModuleName -> Bool
isInModule :: QName -> ModuleName -> Bool
isInModule QName
q ModuleName
m = ModuleName -> [Name]
mnameToList ModuleName
m forall a. Eq a => [a] -> [a] -> Bool
`List.isPrefixOf` QName -> [Name]
qnameToList0 QName
q

-- | Get the next version of the concrete name. For instance, @nextName "x" = "x₁"@.
--   The name must not be a 'NoName'.
nextName :: C.FreshNameMode -> Name -> Name
nextName :: FreshNameMode -> Name -> Name
nextName FreshNameMode
freshNameMode Name
x = Name
x { nameConcrete :: Name
nameConcrete = FreshNameMode -> Name -> Name
C.nextName FreshNameMode
freshNameMode (Name -> Name
nameConcrete Name
x) }

sameRoot :: Name -> Name -> Bool
sameRoot :: Name -> Name -> Bool
sameRoot = Name -> Name -> Bool
C.sameRoot forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> Name
nameConcrete

------------------------------------------------------------------------
-- * Important instances: Eq, Ord, Hashable
--
--   For the identity and comparing of names, only the 'NameId' matters!
------------------------------------------------------------------------

instance Eq Name where
  == :: Name -> Name -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> NameId
nameId

instance Ord Name where
  compare :: Name -> Name -> Ordering
compare = forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> NameId
nameId

instance Hashable Name where
  {-# INLINE hashWithSalt #-}
  hashWithSalt :: Int -> Name -> Int
hashWithSalt Int
salt = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> NameId
nameId

instance Eq QName where
  == :: QName -> QName -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` QName -> Name
qnameName

instance Ord QName where
  compare :: QName -> QName -> Ordering
compare = forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` QName -> Name
qnameName

instance Hashable QName where
  {-# INLINE hashWithSalt #-}
  hashWithSalt :: Int -> QName -> Int
hashWithSalt Int
salt = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName

------------------------------------------------------------------------
-- * IsNoName instances (checking for "_")
------------------------------------------------------------------------

-- | An abstract name is empty if its concrete name is empty.
instance IsNoName Name where
  isNoName :: Name -> Bool
isNoName = forall a. IsNoName a => a -> Bool
isNoName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nameConcrete

instance NumHoles Name where
  numHoles :: Name -> Int
numHoles = forall a. NumHoles a => a -> Int
numHoles forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nameConcrete

instance NumHoles QName where
  numHoles :: QName -> Int
numHoles = forall a. NumHoles a => a -> Int
numHoles forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName

-- | We can have an instance for ambiguous names as all share a common concrete name.
instance NumHoles AmbiguousQName where
  numHoles :: AmbiguousQName -> Int
numHoles = forall a. NumHoles a => a -> Int
numHoles forall b c a. (b -> c) -> (a -> b) -> a -> c
. AmbiguousQName -> QName
headAmbQ

------------------------------------------------------------------------
-- * name lenses
------------------------------------------------------------------------

lensQNameName :: Lens' Name QName
lensQNameName :: Lens' Name QName
lensQNameName Name -> f Name
f (QName ModuleName
m Name
n) = ModuleName -> Name -> QName
QName ModuleName
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> f Name
f Name
n

------------------------------------------------------------------------
-- * LensFixity' instances
------------------------------------------------------------------------

instance LensFixity' Name where
  lensFixity' :: Lens' Fixity' Name
lensFixity' Fixity' -> f Fixity'
f Name
n = Fixity' -> f Fixity'
f (Name -> Fixity'
nameFixity Name
n) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Fixity'
fix' -> Name
n { nameFixity :: Fixity'
nameFixity = Fixity'
fix' }

instance LensFixity' QName where
  lensFixity' :: Lens' Fixity' QName
lensFixity' = Lens' Name QName
lensQNameName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensFixity' a => Lens' Fixity' a
lensFixity'

------------------------------------------------------------------------
-- * LensFixity instances
------------------------------------------------------------------------

instance LensFixity Name where
  lensFixity :: Lens' Fixity Name
lensFixity = forall a. LensFixity' a => Lens' Fixity' a
lensFixity' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensFixity a => Lens' Fixity a
lensFixity

instance LensFixity QName where
  lensFixity :: Lens' Fixity QName
lensFixity = forall a. LensFixity' a => Lens' Fixity' a
lensFixity' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensFixity a => Lens' Fixity a
lensFixity

------------------------------------------------------------------------
-- * LensInScope instances
------------------------------------------------------------------------

instance LensInScope Name where
  lensInScope :: Lens' NameInScope Name
lensInScope NameInScope -> f NameInScope
f n :: Name
n@Name{ nameConcrete :: Name -> Name
nameConcrete = Name
x } =
    (\Name
y -> Name
n { nameConcrete :: Name
nameConcrete = Name
y }) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. LensInScope a => Lens' NameInScope a
lensInScope NameInScope -> f NameInScope
f Name
x

instance LensInScope QName where
  lensInScope :: Lens' NameInScope QName
lensInScope NameInScope -> f NameInScope
f q :: QName
q@QName{ qnameName :: QName -> Name
qnameName = Name
n } =
    (\Name
n' -> QName
q { qnameName :: Name
qnameName = Name
n' }) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. LensInScope a => Lens' NameInScope a
lensInScope NameInScope -> f NameInScope
f Name
n

------------------------------------------------------------------------
-- * Show instances (only for debug printing!)
--
-- | Use 'prettyShow' to print names to the user.
------------------------------------------------------------------------

deriving instance Show Name
deriving instance Show ModuleName
deriving instance Show QName
deriving instance Show a => Show (QNamed a)
deriving instance Show AmbiguousQName

nameToArgName :: Name -> ArgName
nameToArgName :: Name -> String
nameToArgName = ShowS
stringToArgName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
prettyShow

namedArgName :: NamedArg Name -> ArgName
namedArgName :: NamedArg Name -> String
namedArgName NamedArg Name
x = forall a. a -> Maybe a -> a
fromMaybe (Name -> String
nameToArgName forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Name
x) forall a b. (a -> b) -> a -> b
$ forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
bareNameOf NamedArg Name
x

------------------------------------------------------------------------
-- * Pretty instances
------------------------------------------------------------------------

instance Pretty Name where
  pretty :: Name -> Doc
pretty = forall a. Pretty a => a -> Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nameConcrete

instance Pretty ModuleName where
  pretty :: ModuleName -> Doc
pretty = forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
"." forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Name]
mnameToList

instance Pretty QName where
  pretty :: QName -> Doc
pretty = forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
"." forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> [Name]
qnameToList0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> QName
useCanonical
    where
      -- #4735: When printing a fully qualified name (as done by primShowQName) we need to
      -- use the origincal concrete name, not the possibly renamed concrete name in 'nameConcrete'.
      useCanonical :: QName -> QName
useCanonical QName
q = QName
q { qnameName :: Name
qnameName = (QName -> Name
qnameName QName
q) { nameConcrete :: Name
nameConcrete = Name -> Name
nameCanonical (QName -> Name
qnameName QName
q) } }

instance Pretty AmbiguousQName where
  pretty :: AmbiguousQName -> Doc
pretty (AmbQ List1 QName
qs) = forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
" | " forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty forall a b. (a -> b) -> a -> b
$ forall l. IsList l => l -> [Item l]
List1.toList List1 QName
qs

instance Pretty a => Pretty (QNamed a) where
  pretty :: QNamed a -> Doc
pretty (QNamed QName
a a
b) = forall a. Pretty a => a -> Doc
pretty QName
a forall a. Semigroup a => a -> a -> a
<> Doc
"." forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
pretty a
b

------------------------------------------------------------------------
-- * Range instances
------------------------------------------------------------------------

-- ** HasRange

instance HasRange Name where
  getRange :: Name -> Range
getRange = forall a. HasRange a => a -> Range
getRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nameConcrete

instance HasRange ModuleName where
  getRange :: ModuleName -> Range
getRange (MName []) = forall a. Range' a
noRange
  getRange (MName [Name]
xs) = forall a. HasRange a => a -> Range
getRange [Name]
xs

instance HasRange QName where
  getRange :: QName -> Range
getRange QName
q = forall a. HasRange a => a -> Range
getRange (QName -> ModuleName
qnameModule QName
q, QName -> Name
qnameName QName
q)

-- | The range of an @AmbiguousQName@ is the range of any of its
--   disambiguations (they are the same concrete name).
instance HasRange AmbiguousQName where
  getRange :: AmbiguousQName -> Range
getRange (AmbQ (QName
c :| [QName]
_)) = forall a. HasRange a => a -> Range
getRange QName
c

-- ** SetRange

instance SetRange Name where
  setRange :: Range -> Name -> Name
setRange Range
r Name
x = Name
x { nameConcrete :: Name
nameConcrete = forall a. SetRange a => Range -> a -> a
setRange Range
r forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete Name
x }

instance SetRange QName where
  setRange :: Range -> QName -> QName
setRange Range
r QName
q = QName
q { qnameModule :: ModuleName
qnameModule = forall a. SetRange a => Range -> a -> a
setRange Range
r forall a b. (a -> b) -> a -> b
$ QName -> ModuleName
qnameModule QName
q
                   , qnameName :: Name
qnameName   = forall a. SetRange a => Range -> a -> a
setRange Range
r forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName   QName
q
                   }

instance SetRange ModuleName where
  setRange :: Range -> ModuleName -> ModuleName
setRange Range
r (MName [Name]
ns) = [Name] -> ModuleName
MName (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. SetRange a => Range -> a -> a
setRange [Range]
rs [Name]
ns)
    where
      -- Put the range only on the last name. Otherwise
      -- we get overlapping jump-to-definition links for all
      -- the parts (See #2666).
      rs :: [Range]
rs = forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns forall a. Num a => a -> a -> a
- Int
1) forall a. Range' a
noRange forall a. [a] -> [a] -> [a]
++ [Range
r]

-- ** KillRange

instance KillRange Name where
  killRange :: Name -> Name
killRange (Name NameId
a Name
b Name
c Range
d Fixity'
e Bool
f) =
    (forall a b c d e f g.
(KillRange a, KillRange b, KillRange c, KillRange d, KillRange e,
 KillRange f) =>
(a -> b -> c -> d -> e -> f -> g)
-> a -> b -> c -> d -> e -> f -> g
killRange6 NameId -> Name -> Name -> Range -> Fixity' -> Bool -> Name
Name NameId
a Name
b Name
c Range
d Fixity'
e Bool
f) { nameBindingSite :: Range
nameBindingSite = Range
d }
    -- Andreas, 2017-07-25, issue #2649
    -- Preserve the nameBindingSite for error message.
    --
    -- Older remarks:
    --
    -- Andreas, 2014-03-30
    -- An experiment: what happens if we preserve
    -- the range of the binding site, but kill all
    -- other ranges before serialization?
    --
    -- Andreas, Makoto, 2014-10-18 AIM XX
    -- Kill all ranges in signature, including nameBindingSite.

instance KillRange ModuleName where
  killRange :: ModuleName -> ModuleName
killRange (MName [Name]
xs) = [Name] -> ModuleName
MName forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange [Name]
xs

instance KillRange QName where
  killRange :: QName -> QName
killRange (QName ModuleName
a Name
b) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 ModuleName -> Name -> QName
QName ModuleName
a Name
b
  -- killRange q = q { qnameModule = killRange $ qnameModule q
  --                 , qnameName   = killRange $ qnameName   q
  --                 }

instance KillRange AmbiguousQName where
  killRange :: AmbiguousQName -> AmbiguousQName
killRange (AmbQ List1 QName
xs) = List1 QName -> AmbiguousQName
AmbQ forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange List1 QName
xs

------------------------------------------------------------------------
-- * Sized instances
------------------------------------------------------------------------

instance Sized QName where
  size :: QName -> Int
size = forall a. Sized a => a -> Int
size forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> List1 Name
qnameToList

instance Sized ModuleName where
  size :: ModuleName -> Int
size = forall a. Sized a => a -> Int
size forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Name]
mnameToList

------------------------------------------------------------------------
-- * NFData instances
------------------------------------------------------------------------

-- | The range is not forced.

instance NFData Name where
  rnf :: Name -> ()
rnf (Name NameId
_ Name
a Name
b Range
_ Fixity'
c Bool
d) = forall a. NFData a => a -> ()
rnf (Name
a, Name
b, Fixity'
c, Bool
d)

instance NFData QName where
  rnf :: QName -> ()
rnf (QName ModuleName
a Name
b) = forall a. NFData a => a -> ()
rnf ModuleName
a seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Name
b

instance NFData ModuleName where
  rnf :: ModuleName -> ()
rnf (MName [Name]
a) = forall a. NFData a => a -> ()
rnf [Name]
a