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

    import Control.DeepSeq

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

    import GHC.Generics (Generic)

    import Agda.Syntax.Common
    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.Syntax.Common.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 NamePart -> NamePart -> Bool
    forall a. Eq a => a -> a -> Bool
    == NamePart
    Hole Bool -> Bool -> Bool
    || NamePart -> [NamePart] -> NamePart
    forall a. a -> [a] -> a
    last1 NamePart
    x' [NamePart]
    xs NamePart -> NamePart -> Bool
    forall a. Eq a => a -> a -> Bool
    == NamePart
    Hole
      Name
    _ -> Bool
    False

    instance Underscore Name where
      underscore :: Name
    underscore = Range -> NameId -> Name
    NoName Range
    forall a. Range' a
    noRange NameId
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      isUnderscore :: Name -> Bool
    isUnderscore NoName{} = Bool
    True
      isUnderscore (Name {nameNameParts :: Name -> NameParts
    nameNameParts = Id String
    x :| []}) = String -> Bool
    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. NamePart -> Rep NamePart x)
    -> (forall x. Rep NamePart x -> NamePart) -> Generic NamePart
    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
    $cfrom :: forall x. NamePart -> Rep NamePart x
    from :: forall x. NamePart -> Rep NamePart x
    $cto :: forall x. Rep NamePart x -> NamePart
    to :: forall x. Rep NamePart x -> NamePart
    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 NameParts -> NameParts -> Bool
    forall a. Eq a => a -> a -> Bool
    == NameParts
    ys
        NoName Range
    _ NameId
    i     == NoName Range
    _ NameId
    j     = NameId
    i NameId -> NameId -> Bool
    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)      = NameParts -> NameParts -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare NameParts
    xs NameParts
    ys
        compare (NoName Range
    _ NameId
    i)   (NoName Range
    _ NameId
    j)       = NameId -> NameId -> Ordering
    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 String -> String -> Bool
    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) = String -> String -> Ordering
    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
    (QName -> QName -> Bool) -> (QName -> QName -> Bool) -> Eq QName
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: QName -> QName -> Bool
    == :: QName -> QName -> Bool
    $c/= :: QName -> QName -> Bool
    /= :: 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
    $ccompare :: QName -> QName -> Ordering
    compare :: QName -> QName -> Ordering
    $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
    >= :: QName -> QName -> Bool
    $cmax :: QName -> QName -> QName
    max :: QName -> QName -> QName
    $cmin :: QName -> QName -> QName
    min :: QName -> QName -> QName
    Ord)

    instance Underscore QName where
      underscore :: QName
    underscore = Name -> QName
    QName Name
    forall a. Underscore a => a
    underscore
      isUnderscore :: QName -> Bool
    isUnderscore (QName Name
    x) = Name -> Bool
    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 Range
    forall a. Range' a
    noRange NameInScope
    InScope (NameParts -> Name) -> (String -> NameParts) -> String -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamePart -> NameParts
    forall el coll. Singleton el coll => el -> coll
    singleton (NamePart -> NameParts)
    -> (String -> NamePart) -> String -> NameParts
    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 Range
    forall a. Range' a
    noRange NameInScope
    InScope (NameParts -> Name) -> NameParts -> Name
    forall a b. (a -> b) -> a -> b
    $ NamePart
    Hole NamePart -> [NamePart] -> NameParts
    forall a. a -> [a] -> NonEmpty a
    :| String -> NamePart
    Id String
    s NamePart -> [NamePart] -> [NamePart]
    forall a. a -> [a] -> [a]
    : NamePart
    Hole NamePart -> [NamePart] -> [NamePart]
    forall a. a -> [a] -> [a]
    : []

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

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

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

    nameToRawName :: Name -> RawName
    nameToRawName :: Name -> String
    nameToRawName = Name -> String
    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
    _)     = NamePart -> NameParts
    forall el coll. Singleton el coll => el -> coll
    singleton (NamePart -> NameParts) -> NamePart -> NameParts
    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 <- NameParts -> [Item NameParts]
    forall l. IsList l => l -> [Item l]
    List1.toList (NameParts -> [Item NameParts]) -> NameParts -> [Item NameParts]
    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
    ""  = NamePart -> NameParts
    forall el coll. Singleton el coll => el -> coll
    singleton (NamePart -> NameParts) -> NamePart -> NameParts
    forall a b. (a -> b) -> a -> b
    $ String -> NamePart
    Id String
    "_"  -- NoName
    stringNameParts String
    "_" = NamePart -> NameParts
    forall el coll. Singleton el coll => el -> coll
    singleton (NamePart -> NameParts) -> NamePart -> NameParts
    forall a b. (a -> b) -> a -> b
    $ String -> NamePart
    Id String
    "_"  -- NoName
    stringNameParts String
    s = NameParts -> [NamePart] -> NameParts
    forall a. List1 a -> [a] -> List1 a
    List1.fromListSafe NameParts
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([NamePart] -> NameParts) -> [NamePart] -> NameParts
    forall a b. (a -> b) -> a -> b
    $ String -> [NamePart]
    loop String
    s
      where
      loop :: String -> [NamePart]
    loop String
    ""                              = []
      loop (Char
    '_':String
    s)                         = NamePart
    Hole NamePart -> [NamePart] -> [NamePart]
    forall a. a -> [a] -> [a]
    : String -> [NamePart]
    loop String
    s
      loop String
    s | (String
    x, String
    s') <- (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '_') String
    s = String -> NamePart
    Id (String -> String
    stringToRawName String
    x) NamePart -> [NamePart] -> [NamePart]
    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 = [NamePart] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([NamePart] -> Int)
    -> (NameParts -> [NamePart]) -> NameParts -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NamePart -> Bool) -> NameParts -> [NamePart]
    forall a. (a -> Bool) -> NonEmpty a -> [a]
    List1.filter (NamePart -> NamePart -> Bool
    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 }) = NameParts -> Int
    forall a. NumHoles a => a -> Int
    numHoles NameParts
    parts

    instance NumHoles QName where
      numHoles :: QName -> Int
    numHoles (QName Name
    x)  = Name -> Int
    forall a. NumHoles a => a -> Int
    numHoles Name
    x
      numHoles (Qual Name
    _ QName
    x) = QName -> Int
    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 (NameParts -> NamePart
    forall a. NonEmpty a -> a
    List1.head NameParts
    xs)) Bool -> Bool -> Bool
    &&      NamePart -> Bool
    isHole (NameParts -> NamePart
    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 (NameParts -> NamePart
    forall a. NonEmpty a -> a
    List1.head NameParts
    xs)  Bool -> Bool -> Bool
    && Bool -> Bool
    not (NamePart -> Bool
    isHole (NameParts -> NamePart
    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 (NameParts -> NamePart
    forall a. NonEmpty a -> a
    List1.head NameParts
    xs)  Bool -> Bool -> Bool
    &&      NamePart -> Bool
    isHole (NameParts -> NamePart
    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 (NameParts -> NamePart
    forall a. NonEmpty a -> a
    List1.head NameParts
    xs)) Bool -> Bool -> Bool
    && Bool -> Bool
    not (NamePart -> Bool
    isHole (NameParts -> NamePart
    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
    (NameInScope -> NameInScope -> Bool)
    -> (NameInScope -> NameInScope -> Bool) -> Eq NameInScope
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: NameInScope -> NameInScope -> Bool
    == :: NameInScope -> NameInScope -> Bool
    $c/= :: NameInScope -> NameInScope -> Bool
    /= :: NameInScope -> NameInScope -> Bool
    Eq, Int -> NameInScope -> String -> String
    [NameInScope] -> String -> String
    NameInScope -> String
    (Int -> NameInScope -> String -> String)
    -> (NameInScope -> String)
    -> ([NameInScope] -> String -> String)
    -> Show NameInScope
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    $cshowsPrec :: Int -> NameInScope -> String -> String
    showsPrec :: Int -> NameInScope -> String -> String
    $cshow :: NameInScope -> String
    show :: NameInScope -> String
    $cshowList :: [NameInScope] -> String -> String
    showList :: [NameInScope] -> String -> String
    Show)

    class LensInScope a where
      lensInScope :: Lens' a NameInScope

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

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

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

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

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

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

    instance LensInScope QName where
      lensInScope :: Lens' QName NameInScope
    lensInScope NameInScope -> f NameInScope
    f = \case
        Qual Name
    x QName
    xs -> (Name -> QName -> QName
    `Qual` QName
    xs) (Name -> QName) -> f Name -> f QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NameInScope -> f NameInScope) -> Name -> f Name
    forall a. LensInScope a => Lens' a NameInScope
    Lens' Name NameInScope
    lensInScope NameInScope -> f NameInScope
    f Name
    x
        QName Name
    x   -> Name -> QName
    QName (Name -> QName) -> f Name -> f QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NameInScope -> f NameInScope) -> Name -> f Name
    forall a. LensInScope a => Lens' a NameInScope
    Lens' Name NameInScope
    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 (Suffix -> (Suffix -> Suffix) -> Maybe Suffix -> Suffix
    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{} = Name -> Name
    forall a. LensInScope a => a -> a
    setNotInScope (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ Lens' Name String -> LensMap Name String
    forall o i. Lens' o i -> LensMap o i
    over ((NameParts -> f NameParts) -> Name -> f Name
    Lens' Name NameParts
    lensNameParts ((NameParts -> f NameParts) -> Name -> f Name)
    -> ((String -> f String) -> NameParts -> f NameParts)
    -> (String -> f String)
    -> Name
    -> f Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> f String) -> NameParts -> f NameParts
    Lens' NameParts String
    lastIdPart) (FreshNameMode -> String -> String
    nextRawName FreshNameMode
    freshNameMode) Name
    x
    nextName             FreshNameMode
    _ NoName{} = Name
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Zoom on the last non-hole in a name.
    lastIdPart :: Lens' NameParts RawName
    lastIdPart :: Lens' NameParts String
    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 f String -> (String -> NameParts) -> f NameParts
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ String
    s -> String -> NamePart
    Id String
    s NamePart -> [NamePart] -> NameParts
    forall a. a -> [a] -> NonEmpty a
    :| []
        Id String
    s :| [NamePart
    Hole] -> String -> f String
    f String
    s f String -> (String -> NameParts) -> f NameParts
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ String
    s -> String -> NamePart
    Id String
    s NamePart -> [NamePart] -> NameParts
    forall a. a -> [a] -> NonEmpty a
    :| [NamePart
    Hole]
        NamePart
    p1 :| NamePart
    p2 : [NamePart]
    ps  -> (NamePart
    p1 NamePart -> NameParts -> NameParts
    forall a. a -> NonEmpty a -> NonEmpty a
    <|) (NameParts -> NameParts) -> f NameParts -> f NameParts
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NameParts -> f NameParts
    loop (NamePart
    p2 NamePart -> [NamePart] -> NameParts
    forall a. a -> [a] -> NonEmpty a
    :| [NamePart]
    ps)
        NamePart
    Hole :| []     -> f NameParts
    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' Name (Maybe Suffix)
    nameSuffix :: Lens' Name (Maybe Suffix)
    nameSuffix (Maybe Suffix -> f (Maybe Suffix)
    f :: Maybe Suffix -> f (Maybe Suffix)) = \case

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

      n :: Name
    n@Name{} -> (NameParts -> f NameParts) -> Name -> f Name
    Lens' Name NameParts
    lensNameParts ((String -> f String) -> NameParts -> f NameParts
    Lens' NameParts String
    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 String -> (Suffix -> String) -> Maybe Suffix -> String
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe String
    root (String -> Suffix -> String
    addSuffix String
    root) (Maybe Suffix -> String) -> f (Maybe Suffix) -> f String
    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 = (Maybe Suffix -> (Maybe Suffix, Maybe Suffix))
    -> Name -> (Maybe Suffix, Name)
    Lens' Name (Maybe Suffix)
    nameSuffix (,Maybe Suffix
    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 = Lens' Name (Maybe Suffix) -> Maybe Suffix -> Name -> Name
    forall o i. Lens' o i -> LensSet o i
    set (Maybe Suffix -> f (Maybe Suffix)) -> Name -> f Name
    Lens' Name (Maybe Suffix)
    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 (Name -> String) -> Name -> String
    forall a b. (a -> b) -> a -> b
    $ (Maybe Suffix, Name) -> Name
    forall a b. (a, b) -> b
    snd ((Maybe Suffix, Name) -> Name) -> (Maybe Suffix, Name) -> Name
    forall a b. (a -> b) -> a -> b
    $ Name -> (Maybe Suffix, Name)
    nameSuffixView Name
    x

    sameRoot :: Name -> Name -> Bool
    sameRoot :: Name -> Name -> Bool
    sameRoot = String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (String -> String -> Bool)
    -> (Name -> String) -> Name -> Name -> 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' QName Name
    lensQNameName :: Lens' QName Name
    lensQNameName Name -> f Name
    f (QName Name
    n)  = Name -> QName
    QName (Name -> QName) -> f Name -> f 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 (QName -> QName) -> f QName -> f QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Name -> f Name) -> QName -> f QName
    Lens' QName Name
    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 (QName -> QName) -> QName -> QName
    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 Name -> QName -> Name
    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 Name -> List1 Name -> List1 Name
    forall a. a -> NonEmpty a -> NonEmpty a
    <| QName -> List1 Name
    qnameParts QName
    q
    qnameParts (QName Name
    x)  = Name -> List1 Name
    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{}    = Maybe Name
    forall a. Maybe a
    Nothing
    isUnqualified (QName Name
    n) = Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    n

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

    -- | @noName_ = 'noName' 'noRange'@
    noName_ :: Name
    noName_ :: Name
    noName_ = Range -> Name
    noName Range
    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 = (b -> Bool) -> t b -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    Fold.all b -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName

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

    instance IsNoName ByteString where
      isNoName :: ByteString -> Bool
    isNoName = ByteString -> Bool
    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 :| []) -> String -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName String
    x
        Name
    _ -> Bool
    False

    instance IsNoName QName where
      isNoName :: QName -> Bool
    isNoName (QName Name
    x) = Name -> Bool
    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)    = NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat (NonEmpty Doc -> Doc) -> NonEmpty Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ (NamePart -> Doc) -> NameParts -> NonEmpty Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NamePart -> Doc
    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
    forall a. String -> Doc a
    text (String -> Doc) -> String -> Doc
    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)
        | Name -> Bool
    forall a. Underscore a => a -> Bool
    isUnderscore Name
    m = QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x -- don't print anonymous modules
        | Bool
    otherwise      = Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    m Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "." Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x
      pretty (QName Name
    x)  = Name -> Doc
    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) = Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x
        getRange (Qual Name
    n QName
    x) = Name -> QName -> Range
    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 (Range -> Name -> Name
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r Name
    x)
      setRange Range
    r (Qual Name
    n QName
    x) = Name -> QName -> QName
    Qual (Range -> Name -> Name
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r Name
    n) (Range -> QName -> QName
    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 (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    forall a. KillRange a => KillRangeT a
    killRange Name
    x
      killRange (Qual Name
    n QName
    x) = Name -> Name
    forall a. KillRange a => KillRangeT a
    killRange Name
    n Name -> QName -> QName
    `Qual` QName -> QName
    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 (KillRangeT Range
    forall a. KillRange a => KillRangeT a
    killRange Range
    r) NameInScope
    nis NameParts
    ps
      killRange (NoName Range
    r NameId
    i)     = Range -> NameId -> Name
    NoName (KillRangeT Range
    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) = NameInScope -> ()
    forall a. NFData a => a -> ()
    rnf NameInScope
    nis () -> () -> ()
    forall a b. a -> b -> b
    `seq` NameParts -> ()
    forall a. NFData a => a -> ()
    rnf NameParts
    ns
      rnf (NoName Range
    _ NameId
    n)  = NameId -> ()
    forall a. NFData a => a -> ()
    rnf NameId
    n

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

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