{-# 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