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.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
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 eta
where
eta t@(Lam h b) = case binAppView (absBody b) of
App u (Arg _ (Var 0 []))
| not (freeIn 0 u) -> return $ subst __IMPOSSIBLE__ u
_ -> return t
eta t@(Con r args) =
ifM (isRecord r)
(etaContractRecord r args)
(return t)
eta t = return t