-- | 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.
{-# LANGUAGE CPP #-}
module Agda.Compiler.Treeless.NormalizeNames ( normalizeNames ) where

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

normalizeNames :: TTerm -> TCM TTerm
normalizeNames = tr
  where
    tr t = case t of
      TDef q -> do
        q' <- defName <$> getConstInfo q
        return $ TDef q'
      TVar{}    -> done
      TCon{}    -> done
      TPrim{}   -> done
      TLit{}    -> done
      TUnit{}   -> done
      TSort{}   -> done
      TErased{} -> done
      TError{}  -> done
      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
      where
        done :: TCM TTerm
        done = return t

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