-- | 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 = Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a m Type -> (Type -> m Term) -> m Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  El Sort' Term
_ (Pi Dom Type
a Abs Type
b) -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$
    ArgInfo -> Abs Term -> Term
Lam ArgInfo
ai (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ ArgName -> Term -> Abs Term
forall a. (Subst a, Free a) => ArgName -> a -> Abs a
mkAbs (Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b) (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
    where ai :: ArgInfo
ai = Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a

  Type
a -> Type -> m (Maybe (QName, Args))
forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args))
isEtaRecordType Type
a m (Maybe (QName, Args))
-> (Maybe (QName, Args) -> m Term) -> m Term
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 (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
      (Telescope
_, ConHead
con, ConInfo
ci, Args
args) <- QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ QName
r Args
pars Defn
def Term
v
      Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Args -> Term
mkCon ConHead
con ConInfo
ci Args
args
    Maybe (QName, Args)
Nothing -> Term -> m Term
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 = Action (TCMT IO) -> Term -> Comparison -> Type -> TCM Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action (TCMT IO)
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 = Action m
forall (m :: * -> *). PureTCM m => Action m
defaultAction { preAction :: Type -> Term -> m Term
preAction = Type -> Term -> m Term
forall (m :: * -> *). PureTCM m => Type -> Term -> m Term
etaExpandOnce  }