-- | Compute eta short normal forms.
module Agda.TypeChecking.EtaContract where

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

import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce.Monad () --instance only
import {-# SOURCE #-} Agda.TypeChecking.Records
import {-# SOURCE #-} Agda.TypeChecking.Datatypes

import Agda.Utils.Monad
import Agda.Utils.List (initLast)

import Agda.Utils.Impossible

-- TODO: move to Agda.Syntax.Internal.SomeThing
data BinAppView = App Term (Arg Term)
                | NoApp Term

binAppView :: Term -> BinAppView
binAppView :: Term -> BinAppView
binAppView Term
t = case Term
t of
  Var Int
i Elims
xs   -> (Elims -> Term) -> Elims -> BinAppView
appE (Int -> Elims -> Term
Var Int
i) Elims
xs
  Def QName
c Elims
xs   -> (Elims -> Term) -> Elims -> BinAppView
appE (QName -> Elims -> Term
Def QName
c) Elims
xs
  -- Andreas, 2013-09-17: do not eta-contract when body is (record) constructor
  -- like in \ x -> s , x!  (See interaction/DoNotEtaContractFunIntoRecord)
  -- (Cf. also issue 889 (fixed differently).)
  -- At least record constructors should be fully applied where possible!
  -- TODO: also for ordinary constructors (\ x -> suc x  vs.  suc)?
  Con ConHead
c ConInfo
ci Elims
xs
    | DataOrRecord
IsData <- ConHead -> DataOrRecord
conDataRecord ConHead
c
             -> (Elims -> Term) -> Elims -> BinAppView
appE (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci) Elims
xs
    | Bool
otherwise
             -> BinAppView
noApp
  Lit Literal
_      -> BinAppView
noApp
  Level Level
_    -> BinAppView
noApp   -- could be an application, but let's not eta contract levels
  Lam ArgInfo
_ Abs Term
_    -> BinAppView
noApp
  Pi Dom Type
_ Abs Type
_     -> BinAppView
noApp
  Sort Sort
_     -> BinAppView
noApp
  MetaV MetaId
_ Elims
_  -> BinAppView
noApp
  DontCare Term
_ -> BinAppView
noApp
  Dummy{}    -> BinAppView
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    noApp :: BinAppView
noApp = Term -> BinAppView
NoApp Term
t
    appE :: (Elims -> Term) -> Elims -> BinAppView
appE Elims -> Term
f Elims
es0 | Just (Elims
es, Apply Arg Term
v) <- Elims -> Maybe (Elims, Elim' Term)
forall a. [a] -> Maybe ([a], a)
initLast Elims
es0 = Term -> Arg Term -> BinAppView
App (Elims -> Term
f Elims
es) Arg Term
v
    appE Elims -> Term
_ Elims
_ = BinAppView
noApp

-- | Contracts all eta-redexes it sees without reducing.
{-# SPECIALIZE etaContract :: TermLike a => a -> TCM a #-}
{-# SPECIALIZE etaContract :: TermLike a => a -> ReduceM a #-}
etaContract :: (MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) => a -> m a
etaContract :: forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract = (Term -> m Term) -> a -> m a
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m, HasOptions m) =>
Term -> m Term
etaOnce

{-# SPECIALIZE etaOnce :: Term -> TCM Term #-}
{-# SPECIALIZE etaOnce :: Term -> ReduceM Term #-}
etaOnce :: (MonadTCEnv m, HasConstInfo m, HasOptions m) => Term -> m Term
etaOnce :: forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m, HasOptions m) =>
Term -> m Term
etaOnce = \case
  -- Andreas, 2012-11-18: this call to reportSDoc seems to cost me 2%
  -- performance on the std-lib
  -- reportSDoc "tc.eta" 70 $ "eta-contracting" <+> prettyTCM v
  Lam ArgInfo
i (Abs ArgName
x Term
b) -> ArgInfo -> ArgName -> Term -> m Term
forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m, HasOptions m) =>
ArgInfo -> ArgName -> Term -> m Term
etaLam ArgInfo
i ArgName
x Term
b  -- NoAbs can't be eta'd

  -- Andreas, 2012-12-18:  Abstract definitions could contain
  -- abstract records whose constructors are not in scope.
  -- To be able to eta-contract them, we ignore abstract.
  Con ConHead
c ConInfo
ci Elims
es -> ConHead
-> ConInfo
-> Elims
-> (QName -> ConHead -> ConInfo -> Args -> m Term)
-> m Term
forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m, HasOptions m) =>
ConHead
-> ConInfo
-> Elims
-> (QName -> ConHead -> ConInfo -> Args -> m Term)
-> m Term
etaCon ConHead
c ConInfo
ci Elims
es QName -> ConHead -> ConInfo -> Args -> m Term
forall (m :: * -> *).
HasConstInfo m =>
QName -> ConHead -> ConInfo -> Args -> m Term
etaContractRecord

  Term
v -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

-- | If record constructor, call eta-contraction function.
etaCon :: (MonadTCEnv m, HasConstInfo m, HasOptions m)
  => ConHead  -- ^ Constructor name @c@.
  -> ConInfo  -- ^ Constructor info @ci@.
  -> Elims     -- ^ Constructor arguments @args@.
  -> (QName -> ConHead -> ConInfo -> Args -> m Term)
              -- ^ Eta-contraction workhorse, gets also name of record type.
  -> m Term   -- ^ Returns @Con c ci args@ or its eta-contraction.
etaCon :: forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m, HasOptions m) =>
ConHead
-> ConInfo
-> Elims
-> (QName -> ConHead -> ConInfo -> Args -> m Term)
-> m Term
etaCon ConHead
c ConInfo
ci Elims
es QName -> ConHead -> ConInfo -> Args -> m Term
cont = m Term -> m Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ do
  let fallback :: m Term
fallback = 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 -> Elims -> Term
Con ConHead
c ConInfo
ci Elims
es
  -- reportSDoc "tc.eta" 20 $ "eta-contracting record" <+> prettyTCM t
  QName
r <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData (QName -> m QName) -> QName -> m QName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c -- fails in ConcreteMode if c is abstract
  m Bool -> m Term -> m Term -> m Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
r) m Term
fallback (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ {-else-} do
    -- reportSDoc "tc.eta" 20 $ "eta-contracting record" <+> prettyTCM t
    let Just Args
args = Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
    QName -> ConHead -> ConInfo -> Args -> m Term
cont QName
r ConHead
c ConInfo
ci Args
args

-- | Try to contract a lambda-abstraction @Lam i (Abs x b)@.
etaLam :: (MonadTCEnv m, HasConstInfo m, HasOptions m)
  => ArgInfo  -- ^ Info @i@ of the 'Lam'.
  -> ArgName  -- ^ Name @x@ of the abstraction.
  -> Term     -- ^ Body ('Term') @b@ of the 'Abs'.
  -> m Term   -- ^ @Lam i (Abs x b)@, eta-contracted if possible.
etaLam :: forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m, HasOptions m) =>
ArgInfo -> ArgName -> Term -> m Term
etaLam ArgInfo
i ArgName
x Term
b = do
    let fallback :: m Term
fallback = 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
i (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs ArgName
x Term
b
    case Term -> BinAppView
binAppView Term
b of
      App Term
u (Arg ArgInfo
info Term
v) -> do
        Bool
tyty <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
typeInType
        if Bool -> Term -> Bool
forall {t}. t -> Term -> Bool
isVar0 Bool
tyty Term
v
        -- Andreas, 2017-02-20 issue #2464
        -- Contracting with any irrelevant argument breaks subject reduction.
        -- E.g. \ .x -> f .(subst P eq x)  can in general not be contracted to f.
        -- -- (isIrrelevant info || isVar0 tyty v)
             Bool -> Bool -> Bool
&& ArgInfo -> ArgInfo -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding ArgInfo
i ArgInfo
info
             Bool -> Bool -> Bool
&& ArgInfo -> ArgInfo -> Bool
forall a b. (LensModality a, LensModality b) => a -> b -> Bool
sameModality ArgInfo
i ArgInfo
info
             Bool -> Bool -> Bool
&& Bool -> Bool
not (Int -> Term -> Bool
forall a. Free a => Int -> a -> Bool
freeIn Int
0 Term
u)
           then 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
$ Impossible -> Term -> Term
forall a. Subst a => Impossible -> a -> a
strengthen Impossible
HasCallStack => Impossible
impossible Term
u
           else m Term
fallback
      BinAppView
_ -> m Term
fallback
  where
    isVar0 :: t -> Term -> Bool
isVar0 t
_ (Var Int
0 [])               = Bool
True
    -- Andreas, 2016-01-08 If --type-in-type, all levels are equal.
    -- Jesper, 2019-10-15 issue #3073
    -- Contracting level arguments is not sound unless the domain type
    -- is in fact @Level@, e.g. @\(A : Set) → F lzero@ should not be
    -- eta-contracted to @F@.
    -- isVar0 True Level{}               = True
    isVar0 t
tyty (Level (Max Integer
0 [Plus Integer
0 Term
l])) = t -> Term -> Bool
isVar0 t
tyty Term
l
    isVar0 t
_ Term
_ = Bool
False