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
Level _ -> noApp
Lam _ _ -> noApp
Pi _ _ -> noApp
Sort _ -> noApp
MetaV _ _ -> noApp
DontCare _ -> noApp
where
noApp = NoApp t
app f [] = noApp
app f xs = App (f $ init xs) (last xs)
etaContract :: TermLike a => a -> TCM a
etaContract = traverseTermM etaOnce
where
etaOnce :: Term -> TCM Term
etaOnce v = ignoreAbstractMode $ eta v
where
eta t@(Lam h (Abs _ b)) = do
imp <- shouldEtaContractImplicit
case binAppView b of
App u (Arg h' r v)
| isVar0 v && allowed imp h' && not (freeIn 0 u) ->
return $ subst __IMPOSSIBLE__ u
_ -> return t
where
isVar0 (Var 0 []) = True
isVar0 (DontCare{}) = True
isVar0 (Level (Max [Plus 0 l])) = case l of
NeutralLevel v -> isVar0 v
UnreducedLevel v -> isVar0 v
BlockedLevel{} -> False
MetaLevel{} -> False
isVar0 _ = False
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