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.Records
import Agda.TypeChecking.Datatypes
import Agda.Utils.Monad
#include "../undefined.h"
import Agda.Utils.Impossible
data BinAppView = App Term (Arg Term)
| NoApp Term
binAppView :: Term -> BinAppView
binAppView t = case t of
Var i xs -> app (Var i) xs
Def c xs -> app (Def c) xs
Con c xs -> app (Con c) xs
Lit _ -> noApp
Lam _ _ -> noApp
Pi _ _ -> noApp
Fun _ _ -> noApp
Sort _ -> noApp
MetaV _ _ -> noApp
DontCare -> noApp
where
noApp = NoApp t
app f [] = noApp
app f xs = App (f $ init xs) (last xs)
etaContract :: (MonadTCM tcm, TermLike a) => a -> tcm a
etaContract = traverseTermM etaOnce
where
etaOnce :: (MonadTCM tcm) => Term -> tcm Term
etaOnce v = ignoreAbstractMode $ eta v
where
eta t@(Lam h b) = do
imp <- shouldEtaContractImplicit
case binAppView (absBody b) of
App u (Arg h' r (Var 0 []))
| allowed imp h' && not (freeIn 0 u) ->
return $ subst __IMPOSSIBLE__ u
_ -> return t
where
allowed imp h' = h == h' && (imp || h == NotHidden)
eta t@(Con c args) = do
r <- getConstructorData c
ifM (isEtaRecord r)
(etaContractRecord r c args)
(return t)
eta t = return t