{-# LANGUAGE CPP #-}

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

import Agda.Utils.Monad

#include "undefined.h"
import Agda.Utils.Impossible

-- | Eta-expand a term if its type is a function type or an eta-record type.
etaExpandOnce :: Type -> Term -> TCM Term
etaExpandOnce a v = reduce a >>= \case
  El _ (Pi a b) -> return $
    Lam ai $ mkAbs (absName b) $ raise 1 v `apply` [ Arg ai $ var 0 ]
    where ai = domInfo a

  a -> isEtaRecordType a >>= \case
    Just (r, pars) -> do
      def <- theDef <$> getConstInfo r
      (_, con, ci, args) <- etaExpandRecord_ r pars def v
      return $ mkCon con ci args
    Nothing -> return v

-- | Eta-expand functions and expressions of eta-record
-- type wherever possible.
deepEtaExpand :: Term -> Type -> TCM Term
deepEtaExpand = checkInternal' etaExpandAction

etaExpandAction :: Action
etaExpandAction = Action
  { preAction       = etaExpandOnce
  , postAction      = \ _ -> return
  , relevanceAction = \ _ -> id
  }