{-# OPTIONS_GHC -Wunused-imports #-}
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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
t :: TTerm
t@TCon{} -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
t :: TTerm
t@TPrim{} -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
t :: TTerm
t@TLit{} -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
t :: TTerm
t@TUnit{} -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
t :: TTerm
t@TSort{} -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
t :: TTerm
t@TErased{} -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
t :: TTerm
t@TError{} -> TTerm -> TCM TTerm
forall a. a -> TCMT IO a
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 a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
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 a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
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