    -- | Ensures that all occurences of an abstract name share
    -- the same concrete name.
    --
    -- Apply this transformation if your backend uses concrete names
    -- for identification purposes!
    --
    -- The identity of an abstract name is only the nameId, the concrete
    -- name is only a naming suggestion. If renaming imports are used,
    -- the concrete name may change. This transformation makes sure
    -- that all occurences of an abstract name share the same
    -- concrete name.
    --
    -- This transfomation should be run as the last transformation.
    module Agda.Compiler.Treeless.NormalizeNames ( normalizeNames ) where

    import Agda.TypeChecking.Monad
    import Agda.Syntax.Treeless

    normalizeNames :: TTerm -> TCM TTerm
    normalizeNames :: TTerm -> TCM TTerm
    normalizeNames = TTerm -> TCM TTerm
    tr
      where
        tr :: TTerm -> TCM TTerm
    tr = \case
          TDef QName
    q              -> QName -> TTerm
    TDef (QName -> TTerm) -> (Definition -> QName) -> Definition -> TTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> QName
    defName (Definition -> TTerm) -> TCMT IO Definition -> TCM TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
          t :: TTerm
    t@TVar{}            -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TCon{}            -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TPrim{}           -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TLit{}            -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TUnit{}           -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TSort{}           -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TErased{}         -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TError{}          -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          TLam TTerm
    b              -> TTerm -> TTerm
    TLam (TTerm -> TTerm) -> TCM TTerm -> TCM TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    b
          TApp TTerm
    a Args
    bs           -> TTerm -> Args -> TTerm
    TApp (TTerm -> Args -> TTerm) -> TCM TTerm -> TCMT IO (Args -> TTerm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    a TCMT IO (Args -> TTerm) -> TCMT IO Args -> TCM TTerm
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (TTerm -> TCM TTerm) -> Args -> TCMT IO Args
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM TTerm -> TCM TTerm
    tr Args
    bs
          TLet TTerm
    e TTerm
    b            -> TTerm -> TTerm -> TTerm
    TLet (TTerm -> TTerm -> TTerm) -> TCM TTerm -> TCMT IO (TTerm -> TTerm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    e TCMT IO (TTerm -> TTerm) -> TCM TTerm -> TCM TTerm
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TTerm -> TCM TTerm
    tr TTerm
    b
          TCase Int
    sc CaseInfo
    t TTerm
    def [TAlt]
    alts -> Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    TCase Int
    sc CaseInfo
    t (TTerm -> [TAlt] -> TTerm)
    -> TCM TTerm -> TCMT IO ([TAlt] -> TTerm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    def TCMT IO ([TAlt] -> TTerm) -> TCMT IO [TAlt] -> TCM TTerm
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (TAlt -> TCMT IO TAlt) -> [TAlt] -> TCMT IO [TAlt]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM TAlt -> TCMT IO TAlt
    trAlt [TAlt]
    alts
          TCoerce TTerm
    a           -> TTerm -> TTerm
    TCoerce (TTerm -> TTerm) -> TCM TTerm -> TCM TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    a

        trAlt :: TAlt -> TCMT IO TAlt
    trAlt = \case
          TAGuard TTerm
    g TTerm
    b -> TTerm -> TTerm -> TAlt
    TAGuard (TTerm -> TTerm -> TAlt) -> TCM TTerm -> TCMT IO (TTerm -> TAlt)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    g TCMT IO (TTerm -> TAlt) -> TCM TTerm -> TCMT IO TAlt
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TTerm -> TCM TTerm
    tr TTerm
    b
          TACon QName
    q Int
    a TTerm
    b -> QName -> Int -> TTerm -> TAlt
    TACon QName
    q Int
    a (TTerm -> TAlt) -> TCM TTerm -> TCMT IO TAlt
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    b
          TALit Literal
    l TTerm
    b   -> Literal -> TTerm -> TAlt
    TALit Literal
    l (TTerm -> TAlt) -> TCM TTerm -> TCMT IO TAlt
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    b