module Agda.TypeChecking.EtaContract where
import Control.Monad.Reader
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import qualified Agda.Syntax.Common as 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
ExtLam _ _ -> __IMPOSSIBLE__
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, TermLike a) => a -> m a
etaContract = traverseTermM etaOnce
etaOnce :: (MonadReader TCEnv m, HasConstInfo m) => Term -> m Term
etaOnce v = case v of
Shared{} -> __IMPOSSIBLE__
Lam i (Abs _ b) -> do
imp <- shouldEtaContractImplicit
case binAppView b of
App u (Common.Arg info v)
| (isIrrelevant info || isVar0 v)
&& allowed imp info
&& not (freeIn 0 u) ->
return $ strengthen __IMPOSSIBLE__ u
_ -> return v
where
isVar0 (Shared p) = __IMPOSSIBLE__
isVar0 (Var 0 []) = 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 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