-- | Compute eta long normal forms.
module Agda.TypeChecking.EtaExpand where

import Agda.Syntax.Common
import Agda.Syntax.Internal

import Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute

-- | Eta-expand a term if its type is a function type or an eta-record type.
etaExpandOnce :: PureTCM m => Type -> Term -> m Term
etaExpandOnce :: forall (m :: * -> *). PureTCM m => Type -> Term -> m Term
etaExpandOnce Type
a Term
v = forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  El Sort' Term
_ (Pi Dom Type
a Abs Type
b) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    ArgInfo -> Abs Term -> Term
Lam ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall a. (Subst a, Free a) => ArgName -> a -> Abs a
mkAbs (forall a. Abs a -> ArgName
absName Abs Type
b) forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Int -> a -> a
raise Int
1 Term
v forall t. Apply t => t -> Args -> t
`apply` [ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
    where ai :: ArgInfo
ai = forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a

  Type
a -> forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args))
isEtaRecordType Type
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just (QName
r, Args
pars) -> do
      Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
      (Telescope
_, ConHead
con, ConInfo
ci, Args
args) <- forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ QName
r Args
pars Defn
def Term
v
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Args -> Term
mkCon ConHead
con ConInfo
ci Args
args
    Maybe (QName, Args)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

-- | Eta-expand functions and expressions of eta-record
-- type wherever possible.
deepEtaExpand :: Term -> Type -> TCM Term
deepEtaExpand :: Term -> Type -> TCM Term
deepEtaExpand Term
v Type
a = forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' forall (m :: * -> *). PureTCM m => Action m
etaExpandAction Term
v Comparison
CmpLeq Type
a

etaExpandAction :: PureTCM m => Action m
etaExpandAction :: forall (m :: * -> *). PureTCM m => Action m
etaExpandAction = forall (m :: * -> *). PureTCM m => Action m
defaultAction { preAction :: Type -> Term -> m Term
preAction = forall (m :: * -> *). PureTCM m => Type -> Term -> m Term
etaExpandOnce  }