module Agda.TypeChecking.EtaContract where
import Control.Monad.Reader
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 ()
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 -> appE (Var i) xs
Def c xs -> appE (Def c) xs
Con c xs
| null (conFields c) -> app (Con c) xs
| otherwise -> noApp
Lit _ -> noApp
Level _ -> noApp
Lam _ _ -> noApp
Pi _ _ -> noApp
Sort _ -> noApp
MetaV _ _ -> noApp
DontCare _ -> noApp
Shared p -> binAppView (derefPtr p)
where
noApp = NoApp t
app f [] = noApp
app f xs = App (f $ init xs) (last xs)
appE f [] = noApp
appE f xs
| Apply v <- last xs = App (f $ init xs) v
| otherwise = noApp
etaContract :: (MonadReader TCEnv m, HasConstInfo m, HasOptions m, TermLike a) => a -> m a
etaContract = traverseTermM etaOnce
etaOnce :: (MonadReader TCEnv m, HasConstInfo m, HasOptions m) => Term -> m Term
etaOnce v = case v of
Shared{} -> updateSharedTerm etaOnce v
Lam i (Abs _ b) -> do
imp <- shouldEtaContractImplicit
tyty <- typeInType
case binAppView b of
App u (Arg info v)
| (isIrrelevant info || isVar0 tyty v)
&& allowed imp info
&& not (freeIn 0 u) ->
return $ strengthen __IMPOSSIBLE__ u
_ -> return v
where
isVar0 tyty (Shared p) = isVar0 tyty (derefPtr p)
isVar0 _ (Var 0 []) = True
isVar0 True Level{} = True
isVar0 tyty (Level (Max [Plus 0 l])) = case l of
NeutralLevel _ v -> isVar0 tyty v
UnreducedLevel v -> isVar0 tyty v
BlockedLevel{} -> False
MetaLevel{} -> False
isVar0 _ _ = False
allowed imp i' = getHiding i == getHiding i' && (imp || notHidden i)
Con c args -> ignoreAbstractMode $ do
r <- getConstructorData $ conName c
ifM (isEtaRecord r)
(do
etaContractRecord r c args)
(return v)
v -> return v