module Agda.TypeChecking.Eliminators where
import Control.Applicative
import Control.Monad
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.Utils.Impossible
import Agda.TypeChecking.Reduce
#include "../undefined.h"
data ElimView = VarElim Nat [Elim]
| DefElim QName [Elim]
| ConElim QName [Elim]
| MetaElim MetaId [Elim]
| NoElim Term
elimView :: Term -> TCM ElimView
elimView v = do
v <- reduce v
case v of
Def f vs -> do
proj <- isProjection f
case proj of
Nothing -> DefElim f `app` vs
Just{} -> do
case vs of
rv : vs' -> elim (Proj f : map Apply vs') <$> elimView (unArg rv)
[] -> __IMPOSSIBLE__
Var x vs -> VarElim x `app` vs
Con c vs -> ConElim c `app` vs
MetaV m vs -> MetaElim m `app` vs
Lam{} -> noElim
Lit{} -> noElim
Level{} -> noElim
Sort{} -> noElim
Pi{} -> noElim
DontCare{} -> noElim
where
noElim = return $ NoElim v
app f vs = return $ f $ map Apply vs
elim :: [Elim] -> ElimView -> ElimView
elim _ NoElim{} = __IMPOSSIBLE__
elim es2 (VarElim x es1) = VarElim x (es1 ++ es2)
elim es2 (DefElim x es1) = DefElim x (es1 ++ es2)
elim es2 (ConElim x es1) = ConElim x (es1 ++ es2)
elim es2 (MetaElim x es1) = MetaElim x (es1 ++ es2)
unElimView :: ElimView -> Term
unElimView v = case v of
VarElim x es -> unElim (Var x []) es
DefElim x es -> unElim (Def x []) es
ConElim x es -> unElim (Con x []) es
MetaElim x es -> unElim (MetaV x []) es
NoElim v -> v
unElim :: Term -> [Elim] -> Term
unElim v [] = v
unElim v (Apply u : es) = unElim (v `apply` [u]) es
unElim v (Proj f : es) = unElim (Def f [Arg NotHidden Relevant v]) es