-- | 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 = tr
  where
    tr = \case
      TDef q              -> TDef . defName <$> getConstInfo q
      t@TVar{}            -> return t
      t@TCon{}            -> return t
      t@TPrim{}           -> return t
      t@TLit{}            -> return t
      t@TUnit{}           -> return t
      t@TSort{}           -> return t
      t@TErased{}         -> return t
      t@TError{}          -> return t
      TLam b              -> TLam <$> tr b
      TApp a bs           -> TApp <$> tr a <*> mapM tr bs
      TLet e b            -> TLet <$> tr e <*> tr b
      TCase sc t def alts -> TCase sc t <$> tr def <*> mapM trAlt alts
      TCoerce a           -> TCoerce <$> tr a

    trAlt = \case
      TAGuard g b -> TAGuard <$> tr g <*> tr b
      TACon q a b -> TACon q a <$> tr b
      TALit l b   -> TALit l <$> tr b