{-| Names in the concrete syntax are just strings (or lists of strings for
    qualified names).
-}
module Agda.Syntax.Concrete.Name where

import Prelude hiding ((!!))

import Control.DeepSeq

import Data.ByteString.Char8 (ByteString)
import Data.Function
import qualified Data.Foldable as Fold

import GHC.Generics (Generic)

import Agda.Syntax.Common
import Agda.Syntax.Concrete.Glyph
import Agda.Syntax.Position

import Agda.Utils.Lens
import Agda.Utils.List  ((!!), last1)
import Agda.Utils.List1 (List1, pattern (:|), (<|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Pretty
import Agda.Utils.Singleton
import Agda.Utils.Suffix

import Agda.Utils.Impossible

{-| A name is a non-empty list of alternating 'Id's and 'Hole's. A normal name
    is represented by a singleton list, and operators are represented by a list
    with 'Hole's where the arguments should go. For instance: @[Hole,Id "+",Hole]@
    is infix addition.

    Equality and ordering on @Name@s are defined to ignore range so same names
    in different locations are equal.
-}
data Name
  = Name -- ^ A (mixfix) identifier.
    { Name -> Range
nameRange     :: Range
    , Name -> NameInScope
nameInScope   :: NameInScope
    , Name -> NameParts
nameNameParts :: NameParts
    }
  | NoName -- ^ @_@.
    { nameRange     :: Range
    , Name -> NameId
nameId        :: NameId
    }

type NameParts = List1 NamePart

-- | An open mixfix identifier is either prefix, infix, or suffix.
--   That is to say: at least one of its extremities is a @Hole@

isOpenMixfix :: Name -> Bool
isOpenMixfix :: Name -> Bool
isOpenMixfix = \case
  Name Range
_ NameInScope
_ (NamePart
x :| NamePart
x' : [NamePart]
xs) -> NamePart
x forall a. Eq a => a -> a -> Bool
== NamePart
Hole Bool -> Bool -> Bool
|| forall a. a -> [a] -> a
last1 NamePart
x' [NamePart]
xs forall a. Eq a => a -> a -> Bool
== NamePart
Hole
  Name
_ -> Bool
False

instance Underscore Name where
  underscore :: Name
underscore = Range -> NameId -> Name
NoName forall a. Range' a
noRange forall a. HasCallStack => a
__IMPOSSIBLE__
  isUnderscore :: Name -> Bool
isUnderscore NoName{} = Bool
True
  isUnderscore (Name {nameNameParts :: Name -> NameParts
nameNameParts = Id String
x :| []}) = forall a. Underscore a => a -> Bool
isUnderscore String
x
  isUnderscore Name
_ = Bool
False

-- | Mixfix identifiers are composed of words and holes,
--   e.g. @_+_@ or @if_then_else_@ or @[_/_]@.
data NamePart
  = Hole       -- ^ @_@ part.
  | Id RawName  -- ^ Identifier part.
  deriving forall x. Rep NamePart x -> NamePart
forall x. NamePart -> Rep NamePart x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NamePart x -> NamePart
$cfrom :: forall x. NamePart -> Rep NamePart x
Generic

-- | Define equality on @Name@ to ignore range so same names in different
--   locations are equal.
--
--   Is there a reason not to do this? -Jeff
--
--   No. But there are tons of reasons to do it. For instance, when using
--   names as keys in maps you really don't want to have to get the range
--   right to be able to do a lookup. -Ulf

instance Eq Name where
    Name Range
_ NameInScope
_ NameParts
xs    == :: Name -> Name -> Bool
== Name Range
_ NameInScope
_ NameParts
ys    = NameParts
xs forall a. Eq a => a -> a -> Bool
== NameParts
ys
    NoName Range
_ NameId
i     == NoName Range
_ NameId
j     = NameId
i forall a. Eq a => a -> a -> Bool
== NameId
j
    Name
_              == Name
_              = Bool
False

instance Ord Name where
    compare :: Name -> Name -> Ordering
compare (Name Range
_ NameInScope
_ NameParts
xs)  (Name Range
_ NameInScope
_ NameParts
ys)      = forall a. Ord a => a -> a -> Ordering
compare NameParts
xs NameParts
ys
    compare (NoName Range
_ NameId
i)   (NoName Range
_ NameId
j)       = forall a. Ord a => a -> a -> Ordering
compare NameId
i NameId
j
    compare (NoName {})    (Name {})          = Ordering
LT
    compare (Name {})      (NoName {})        = Ordering
GT

instance Eq NamePart where
  NamePart
Hole  == :: NamePart -> NamePart -> Bool
== NamePart
Hole  = Bool
True
  Id String
s1 == Id String
s2 = String
s1 forall a. Eq a => a -> a -> Bool
== String
s2
  NamePart
_     == NamePart
_     = Bool
False

instance Ord NamePart where
  compare :: NamePart -> NamePart -> Ordering
compare NamePart
Hole    NamePart
Hole    = Ordering
EQ
  compare NamePart
Hole    (Id {}) = Ordering
LT
  compare (Id {}) NamePart
Hole    = Ordering
GT
  compare (Id String
s1) (Id String
s2) = forall a. Ord a => a -> a -> Ordering
compare String
s1 String
s2

-- | @QName@ is a list of namespaces and the name of the constant.
--   For the moment assumes namespaces are just @Name@s and not
--     explicitly applied modules.
--   Also assumes namespaces are generative by just using derived
--     equality. We will have to define an equality instance to
--     non-generative namespaces (as well as having some sort of
--     lookup table for namespace names).
data QName
  = Qual  Name QName -- ^ @A.rest@.
  | QName Name       -- ^ @x@.
  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)

instance Underscore QName where
  underscore :: QName
underscore = Name -> QName
QName forall a. Underscore a => a
underscore
  isUnderscore :: QName -> Bool
isUnderscore (QName Name
x) = forall a. Underscore a => a -> Bool
isUnderscore Name
x
  isUnderscore Qual{}    = Bool
False

------------------------------------------------------------------------
-- * Constructing simple 'Name's.
------------------------------------------------------------------------

-- | Create an ordinary 'InScope' name.
simpleName :: RawName -> Name
simpleName :: String -> Name
simpleName = Range -> NameInScope -> NameParts -> Name
Name forall a. Range' a
noRange NameInScope
InScope forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall el coll. Singleton el coll => el -> coll
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> NamePart
Id

-- | Create a binary operator name in scope.
simpleBinaryOperator :: RawName -> Name
simpleBinaryOperator :: String -> Name
simpleBinaryOperator String
s = Range -> NameInScope -> NameParts -> Name
Name forall a. Range' a
noRange NameInScope
InScope forall a b. (a -> b) -> a -> b
$ NamePart
Hole forall a. a -> [a] -> NonEmpty a
:| String -> NamePart
Id String
s forall a. a -> [a] -> [a]
: NamePart
Hole forall a. a -> [a] -> [a]
: []

-- | Create an ordinary 'InScope' name containing a single 'Hole'.
simpleHole :: Name
simpleHole :: Name
simpleHole = Range -> NameInScope -> NameParts -> Name
Name forall a. Range' a
noRange NameInScope
InScope forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton NamePart
Hole

------------------------------------------------------------------------
-- * Operations on 'Name' and 'NamePart'
------------------------------------------------------------------------

-- | Don't use on 'NoName{}'.
lensNameParts :: Lens' NameParts Name
lensNameParts :: Lens' NameParts Name
lensNameParts NameParts -> f NameParts
f = \case
  n :: Name
n@Name{} -> NameParts -> f NameParts
f (Name -> NameParts
nameNameParts Name
n) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ NameParts
ps -> Name
n { nameNameParts :: NameParts
nameNameParts = NameParts
ps }
  NoName{} -> forall a. HasCallStack => a
__IMPOSSIBLE__

nameToRawName :: Name -> RawName
nameToRawName :: Name -> String
nameToRawName = forall a. Pretty a => a -> String
prettyShow

nameParts :: Name -> NameParts
nameParts :: Name -> NameParts
nameParts (Name Range
_ NameInScope
_ NameParts
ps)    = NameParts
ps
nameParts (NoName Range
_ NameId
_)     = forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ String -> NamePart
Id String
"_" -- To not return an empty list

nameStringParts :: Name -> [RawName]
nameStringParts :: Name -> [String]
nameStringParts Name
n = [ String
s | Id String
s <- forall l. IsList l => l -> [Item l]
List1.toList forall a b. (a -> b) -> a -> b
$ Name -> NameParts
nameParts Name
n ]

-- | Parse a string to parts of a concrete name.
--
--   Note: @stringNameParts "_" == [Id "_"] == nameParts NoName{}@

stringNameParts :: String -> NameParts
stringNameParts :: String -> NameParts
stringNameParts String
""  = forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ String -> NamePart
Id String
"_"  -- NoName
stringNameParts String
"_" = forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ String -> NamePart
Id String
"_"  -- NoName
stringNameParts String
s = forall a. List1 a -> [a] -> List1 a
List1.fromListSafe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ String -> [NamePart]
loop String
s
  where
  loop :: String -> [NamePart]
loop String
""                              = []
  loop (Char
'_':String
s)                         = NamePart
Hole forall a. a -> [a] -> [a]
: String -> [NamePart]
loop String
s
  loop String
s | (String
x, String
s') <- forall a. (a -> Bool) -> [a] -> ([a], [a])
break (forall a. Eq a => a -> a -> Bool
== Char
'_') String
s = String -> NamePart
Id (String -> String
stringToRawName String
x) forall a. a -> [a] -> [a]
: String -> [NamePart]
loop String
s'

-- | Number of holes in a 'Name' (i.e., arity of a mixfix-operator).
class NumHoles a where
  numHoles :: a -> Int

instance NumHoles NameParts where
  numHoles :: NameParts -> Int
numHoles = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> NonEmpty a -> [a]
List1.filter (forall a. Eq a => a -> a -> Bool
== NamePart
Hole)

instance NumHoles Name where
  numHoles :: Name -> Int
numHoles NoName{}         = Int
0
  numHoles (Name { nameNameParts :: Name -> NameParts
nameNameParts = NameParts
parts }) = forall a. NumHoles a => a -> Int
numHoles NameParts
parts

instance NumHoles QName where
  numHoles :: QName -> Int
numHoles (QName Name
x)  = forall a. NumHoles a => a -> Int
numHoles Name
x
  numHoles (Qual Name
_ QName
x) = forall a. NumHoles a => a -> Int
numHoles QName
x

-- | Is the name an operator?
--   Needs at least 2 'NamePart's.
isOperator :: Name -> Bool
isOperator :: Name -> Bool
isOperator = \case
  Name Range
_ NameInScope
_ (NamePart
_ :| NamePart
_ : [NamePart]
_) -> Bool
True
  Name
_ -> Bool
False

isHole :: NamePart -> Bool
isHole :: NamePart -> Bool
isHole NamePart
Hole = Bool
True
isHole NamePart
_    = Bool
False

isPrefix, isPostfix, isInfix, isNonfix :: Name -> Bool
isPrefix :: Name -> Bool
isPrefix  Name
x = Bool -> Bool
not (NamePart -> Bool
isHole (forall a. NonEmpty a -> a
List1.head NameParts
xs)) Bool -> Bool -> Bool
&&      NamePart -> Bool
isHole (forall a. NonEmpty a -> a
List1.last NameParts
xs)  where xs :: NameParts
xs = Name -> NameParts
nameParts Name
x
isPostfix :: Name -> Bool
isPostfix Name
x =      NamePart -> Bool
isHole (forall a. NonEmpty a -> a
List1.head NameParts
xs)  Bool -> Bool -> Bool
&& Bool -> Bool
not (NamePart -> Bool
isHole (forall a. NonEmpty a -> a
List1.last NameParts
xs)) where xs :: NameParts
xs = Name -> NameParts
nameParts Name
x
isInfix :: Name -> Bool
isInfix   Name
x =      NamePart -> Bool
isHole (forall a. NonEmpty a -> a
List1.head NameParts
xs)  Bool -> Bool -> Bool
&&      NamePart -> Bool
isHole (forall a. NonEmpty a -> a
List1.last NameParts
xs)  where xs :: NameParts
xs = Name -> NameParts
nameParts Name
x
isNonfix :: Name -> Bool
isNonfix  Name
x = Bool -> Bool
not (NamePart -> Bool
isHole (forall a. NonEmpty a -> a
List1.head NameParts
xs)) Bool -> Bool -> Bool
&& Bool -> Bool
not (NamePart -> Bool
isHole (forall a. NonEmpty a -> a
List1.last NameParts
xs)) where xs :: NameParts
xs = Name -> NameParts
nameParts Name
x


------------------------------------------------------------------------
-- * Keeping track of which names are (not) in scope
------------------------------------------------------------------------

data NameInScope = InScope | NotInScope
  deriving (NameInScope -> NameInScope -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NameInScope -> NameInScope -> Bool
$c/= :: NameInScope -> NameInScope -> Bool
== :: NameInScope -> NameInScope -> Bool
$c== :: NameInScope -> NameInScope -> Bool
Eq, Int -> NameInScope -> String -> String
[NameInScope] -> String -> String
NameInScope -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [NameInScope] -> String -> String
$cshowList :: [NameInScope] -> String -> String
show :: NameInScope -> String
$cshow :: NameInScope -> String
showsPrec :: Int -> NameInScope -> String -> String
$cshowsPrec :: Int -> NameInScope -> String -> String
Show)

class LensInScope a where
  lensInScope :: Lens' NameInScope a

  isInScope :: a -> NameInScope
  isInScope a
x = a
x forall o i. o -> Lens' i o -> i
^. forall a. LensInScope a => Lens' NameInScope a
lensInScope

  mapInScope :: (NameInScope -> NameInScope) -> a -> a
  mapInScope = forall i o. Lens' i o -> LensMap i o
over forall a. LensInScope a => Lens' NameInScope a
lensInScope

  setInScope :: a -> a
  setInScope = forall a. LensInScope a => (NameInScope -> NameInScope) -> a -> a
mapInScope forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const NameInScope
InScope

  setNotInScope :: a -> a
  setNotInScope = forall a. LensInScope a => (NameInScope -> NameInScope) -> a -> a
mapInScope forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const NameInScope
NotInScope

instance LensInScope NameInScope where
  lensInScope :: Lens' NameInScope NameInScope
lensInScope = forall a. a -> a
id

instance LensInScope Name where
  lensInScope :: Lens' NameInScope Name
lensInScope NameInScope -> f NameInScope
f = \case
    n :: Name
n@Name{ nameInScope :: Name -> NameInScope
nameInScope = NameInScope
nis } -> (\NameInScope
nis' -> Name
n { nameInScope :: NameInScope
nameInScope = NameInScope
nis' }) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameInScope -> f NameInScope
f NameInScope
nis
    n :: Name
n@NoName{} -> Name
n forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NameInScope -> f NameInScope
f NameInScope
InScope

instance LensInScope QName where
  lensInScope :: Lens' NameInScope QName
lensInScope NameInScope -> f NameInScope
f = \case
    Qual Name
x QName
xs -> (Name -> QName -> QName
`Qual` QName
xs) 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
    QName Name
x   -> Name -> QName
QName 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

------------------------------------------------------------------------
-- * Generating fresh names
------------------------------------------------------------------------

-- | Method by which to generate fresh unshadowed names.
data FreshNameMode
  = UnicodeSubscript
  -- ^ Append an integer Unicode subscript: x, x₁, x₂, …
  | AsciiCounter
  -- ^ Append an integer ASCII counter: x, x1, x2, …

  -- Note that @Agda.Utils.Suffix@ supports an additional style, @Prime@, but
  -- we currently only encounter it when extending an existing name of that
  -- format, (x', x'', …), not for an initially-generated permutation. There's
  -- no reason we couldn't, except that we currently choose between
  -- subscript/counter styles based on the --no-unicode mode rather than any
  -- finer-grained option.
  --   | PrimeTickCount
  --   ^ Append an ASCII prime/apostrophe: x, x', x'', …

nextRawName :: FreshNameMode -> RawName -> RawName
nextRawName :: FreshNameMode -> String -> String
nextRawName FreshNameMode
freshNameMode String
s = String -> Suffix -> String
addSuffix String
root (forall b a. b -> (a -> b) -> Maybe a -> b
maybe Suffix
initialSuffix Suffix -> Suffix
nextSuffix Maybe Suffix
suffix)
  where
  (String
root, Maybe Suffix
suffix) = String -> (String, Maybe Suffix)
suffixView String
s
  initialSuffix :: Suffix
initialSuffix = case FreshNameMode
freshNameMode of
    FreshNameMode
UnicodeSubscript -> Integer -> Suffix
Subscript Integer
1
    FreshNameMode
AsciiCounter -> Integer -> Suffix
Index Integer
1

-- | Get the next version of the concrete name. For instance,
--   @nextName "x" = "x₁"@.  The name must not be a 'NoName'.
nextName :: FreshNameMode -> Name -> Name
nextName :: FreshNameMode -> Name -> Name
nextName FreshNameMode
freshNameMode x :: Name
x@Name{} = forall a. LensInScope a => a -> a
setNotInScope forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensMap i o
over (Lens' NameParts Name
lensNameParts forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' String NameParts
lastIdPart) (FreshNameMode -> String -> String
nextRawName FreshNameMode
freshNameMode) Name
x
nextName             FreshNameMode
_ NoName{} = forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Zoom on the last non-hole in a name.
lastIdPart :: Lens' RawName NameParts
lastIdPart :: Lens' String NameParts
lastIdPart String -> f String
f = NameParts -> f NameParts
loop
  where
  loop :: NameParts -> f NameParts
loop = \case
    Id String
s :| []     -> String -> f String
f String
s forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ String
s -> String -> NamePart
Id String
s forall a. a -> [a] -> NonEmpty a
:| []
    Id String
s :| [NamePart
Hole] -> String -> f String
f String
s forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ String
s -> String -> NamePart
Id String
s forall a. a -> [a] -> NonEmpty a
:| [NamePart
Hole]
    NamePart
p1 :| NamePart
p2 : [NamePart]
ps  -> (NamePart
p1 forall a. a -> NonEmpty a -> NonEmpty a
<|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameParts -> f NameParts
loop (NamePart
p2 forall a. a -> [a] -> NonEmpty a
:| [NamePart]
ps)
    NamePart
Hole :| []     -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Get the first version of the concrete name that does not satisfy
--   the given predicate.
firstNonTakenName :: FreshNameMode -> (Name -> Bool) -> Name -> Name
firstNonTakenName :: FreshNameMode -> (Name -> Bool) -> Name -> Name
firstNonTakenName FreshNameMode
freshNameMode Name -> Bool
taken Name
x =
  if Name -> Bool
taken Name
x
  then FreshNameMode -> (Name -> Bool) -> Name -> Name
firstNonTakenName FreshNameMode
freshNameMode Name -> Bool
taken (FreshNameMode -> Name -> Name
nextName FreshNameMode
freshNameMode Name
x)
  else Name
x

-- | Lens for accessing and modifying the suffix of a name.
--   The suffix of a @NoName@ is always @Nothing@, and should not be
--   changed.
nameSuffix :: Lens' (Maybe Suffix) Name
nameSuffix :: Lens' (Maybe Suffix) Name
nameSuffix (Maybe Suffix -> f (Maybe Suffix)
f :: Maybe Suffix -> f (Maybe Suffix)) = \case

  n :: Name
n@NoName{} -> Maybe Suffix -> f (Maybe Suffix)
f forall a. Maybe a
Nothing forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
    Maybe Suffix
Nothing -> Name
n
    Just {} -> forall a. HasCallStack => a
__IMPOSSIBLE__

  n :: Name
n@Name{} -> Lens' NameParts Name
lensNameParts (Lens' String NameParts
lastIdPart String -> f String
idSuf) Name
n
    where
    idSuf :: String -> f String
idSuf String
s =
      let (String
root, Maybe Suffix
suffix) = String -> (String, Maybe Suffix)
suffixView String
s
      in forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
root (String -> Suffix -> String
addSuffix String
root) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe Suffix -> f (Maybe Suffix)
f Maybe Suffix
suffix)

-- | Split a name into a base name plus a suffix.
nameSuffixView :: Name -> (Maybe Suffix, Name)
nameSuffixView :: Name -> (Maybe Suffix, Name)
nameSuffixView = Lens' (Maybe Suffix) Name
nameSuffix (,forall a. Maybe a
Nothing)

-- | Replaces the suffix of a name. Unless the suffix is @Nothing@,
--   the name should not be @NoName@.
setNameSuffix :: Maybe Suffix -> Name -> Name
setNameSuffix :: Maybe Suffix -> Name -> Name
setNameSuffix = forall i o. Lens' i o -> LensSet i o
set Lens' (Maybe Suffix) Name
nameSuffix

-- | Get a raw version of the name with all suffixes removed. For
--   instance, @nameRoot "x₁₂₃" = "x"@.
nameRoot :: Name -> RawName
nameRoot :: Name -> String
nameRoot Name
x = Name -> String
nameToRawName forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ Name -> (Maybe Suffix, Name)
nameSuffixView Name
x

sameRoot :: Name -> Name -> Bool
sameRoot :: Name -> Name -> Bool
sameRoot = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> String
nameRoot

------------------------------------------------------------------------
-- * Operations on qualified names
------------------------------------------------------------------------

-- | Lens for the unqualified part of a QName
lensQNameName :: Lens' Name QName
lensQNameName :: Lens' Name QName
lensQNameName Name -> f Name
f (QName Name
n)  = Name -> QName
QName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> f Name
f Name
n
lensQNameName Name -> f Name
f (Qual Name
m QName
n) = Name -> QName -> QName
Qual Name
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' Name QName
lensQNameName Name -> f Name
f QName
n

-- | @qualify A.B x == A.B.x@
qualify :: QName -> Name -> QName
qualify :: QName -> Name -> QName
qualify (QName Name
m) Name
x     = Name -> QName -> QName
Qual Name
m (Name -> QName
QName Name
x)
qualify (Qual Name
m QName
m') Name
x   = Name -> QName -> QName
Qual Name
m forall a b. (a -> b) -> a -> b
$ QName -> Name -> QName
qualify QName
m' Name
x

-- | @unqualify A.B.x == x@
--
-- The range is preserved.
unqualify :: QName -> Name
unqualify :: QName -> Name
unqualify QName
q = QName -> Name
unqualify' QName
q forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` QName
q
  where
  unqualify' :: QName -> Name
unqualify' (QName Name
x)  = Name
x
  unqualify' (Qual Name
_ QName
x) = QName -> Name
unqualify' QName
x

-- | @qnameParts A.B.x = [A, B, x]@
qnameParts :: QName -> List1 Name
qnameParts :: QName -> List1 Name
qnameParts (Qual Name
x QName
q) = Name
x forall a. a -> NonEmpty a -> NonEmpty a
<| QName -> List1 Name
qnameParts QName
q
qnameParts (QName Name
x)  = forall el coll. Singleton el coll => el -> coll
singleton Name
x

-- | Is the name (un)qualified?

isQualified :: QName -> Bool
isQualified :: QName -> Bool
isQualified Qual{}  = Bool
True
isQualified QName{} = Bool
False

isUnqualified :: QName -> Maybe Name
isUnqualified :: QName -> Maybe Name
isUnqualified Qual{}    = forall a. Maybe a
Nothing
isUnqualified (QName Name
n) = forall a. a -> Maybe a
Just Name
n

------------------------------------------------------------------------
-- * No name stuff
------------------------------------------------------------------------

-- | @noName_ = 'noName' 'noRange'@
noName_ :: Name
noName_ :: Name
noName_ = Range -> Name
noName forall a. Range' a
noRange

noName :: Range -> Name
noName :: Range -> Name
noName Range
r = Range -> NameId -> Name
NoName Range
r (Word64 -> ModuleNameHash -> NameId
NameId Word64
0 ModuleNameHash
noModuleNameHash)

-- | Check whether a name is the empty name "_".
class IsNoName a where
  isNoName :: a -> Bool

  default isNoName :: (Foldable t, IsNoName b, t b ~ a) => a -> Bool
  isNoName = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Fold.all forall a. IsNoName a => a -> Bool
isNoName

instance IsNoName String where
  isNoName :: String -> Bool
isNoName = forall a. Underscore a => a -> Bool
isUnderscore

instance IsNoName ByteString where
  isNoName :: ByteString -> Bool
isNoName = forall a. Underscore a => a -> Bool
isUnderscore

instance IsNoName Name where
  isNoName :: Name -> Bool
isNoName = \case
    NoName{}              -> Bool
True
    Name Range
_ NameInScope
_ (NamePart
Hole :| []) -> Bool
True
    Name Range
_ NameInScope
_ (Id String
x :| []) -> forall a. IsNoName a => a -> Bool
isNoName String
x
    Name
_ -> Bool
False

instance IsNoName QName where
  isNoName :: QName -> Bool
isNoName (QName Name
x) = forall a. IsNoName a => a -> Bool
isNoName Name
x
  isNoName Qual{}    = Bool
False        -- M.A._ does not qualify as empty name

instance IsNoName a => IsNoName (Ranged a) where
instance IsNoName a => IsNoName (WithOrigin a) where

------------------------------------------------------------------------
-- * Showing names
------------------------------------------------------------------------

deriving instance Show Name
deriving instance Show NamePart
deriving instance Show QName

------------------------------------------------------------------------
-- * Printing names
------------------------------------------------------------------------

instance Pretty Name where
  pretty :: Name -> Doc
pretty (Name Range
_ NameInScope
_ NameParts
xs)    = forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Pretty a => a -> Doc
pretty NameParts
xs
  pretty (NoName Range
_ NameId
_)     = Doc
"_"

instance Pretty NamePart where
  pretty :: NamePart -> Doc
pretty NamePart
Hole   = Doc
"_"
  pretty (Id String
s) = String -> Doc
text forall a b. (a -> b) -> a -> b
$ String -> String
rawNameToString String
s

instance Pretty QName where
  pretty :: QName -> Doc
pretty (Qual Name
m QName
x)
    | forall a. Underscore a => a -> Bool
isUnderscore Name
m = forall a. Pretty a => a -> Doc
pretty QName
x -- don't print anonymous modules
    | Bool
otherwise      = forall a. Pretty a => a -> Doc
pretty Name
m forall a. Semigroup a => a -> a -> a
<> Doc
"." forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
pretty QName
x
  pretty (QName Name
x)  = forall a. Pretty a => a -> Doc
pretty Name
x

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

instance HasRange Name where
    getRange :: Name -> Range
getRange (Name Range
r NameInScope
_ NameParts
_ps) = Range
r
    getRange (NoName Range
r NameId
_)   = Range
r

instance HasRange QName where
    getRange :: QName -> Range
getRange (QName  Name
x) = forall a. HasRange a => a -> Range
getRange Name
x
    getRange (Qual Name
n QName
x) = forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Name
n QName
x

instance SetRange Name where
  setRange :: Range -> Name -> Name
setRange Range
r (Name Range
_ NameInScope
nis NameParts
ps) = Range -> NameInScope -> NameParts -> Name
Name Range
r NameInScope
nis NameParts
ps
  setRange Range
r (NoName Range
_ NameId
i)  = Range -> NameId -> Name
NoName Range
r NameId
i

instance SetRange QName where
  setRange :: Range -> QName -> QName
setRange Range
r (QName Name
x)  = Name -> QName
QName (forall a. SetRange a => Range -> a -> a
setRange Range
r Name
x)
  setRange Range
r (Qual Name
n QName
x) = Name -> QName -> QName
Qual (forall a. SetRange a => Range -> a -> a
setRange Range
r Name
n) (forall a. SetRange a => Range -> a -> a
setRange Range
r QName
x)

instance KillRange QName where
  killRange :: QName -> QName
killRange (QName Name
x) = Name -> QName
QName forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange Name
x
  killRange (Qual Name
n QName
x) = forall a. KillRange a => KillRangeT a
killRange Name
n Name -> QName -> QName
`Qual` forall a. KillRange a => KillRangeT a
killRange QName
x

instance KillRange Name where
  killRange :: Name -> Name
killRange (Name Range
r NameInScope
nis NameParts
ps)  = Range -> NameInScope -> NameParts -> Name
Name (forall a. KillRange a => KillRangeT a
killRange Range
r) NameInScope
nis NameParts
ps
  killRange (NoName Range
r NameId
i)     = Range -> NameId -> Name
NoName (forall a. KillRange a => KillRangeT a
killRange Range
r) NameId
i

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

instance NFData NameInScope where
  rnf :: NameInScope -> ()
rnf NameInScope
InScope    = ()
  rnf NameInScope
NotInScope = ()

-- | Ranges are not forced.

instance NFData Name where
  rnf :: Name -> ()
rnf (Name Range
_ NameInScope
nis NameParts
ns) = forall a. NFData a => a -> ()
rnf NameInScope
nis seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf NameParts
ns
  rnf (NoName Range
_ NameId
n)  = forall a. NFData a => a -> ()
rnf NameId
n

instance NFData NamePart where
  rnf :: NamePart -> ()
rnf NamePart
Hole   = ()
  rnf (Id String
s) = forall a. NFData a => a -> ()
rnf String
s

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