-- | 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> QName
defName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      t :: TTerm
t@TVar{}            -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TCon{}            -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TPrim{}           -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TLit{}            -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TUnit{}           -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TSort{}           -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TErased{}         -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      t :: TTerm
t@TError{}          -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
      TLam TTerm
b              -> TTerm -> TTerm
TLam 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
e 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
def forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
g 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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM TTerm
tr TTerm
b