module Agda.TypeChecking.DropArgs where
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Substitute.Pattern
import Agda.TypeChecking.CompiledClause
import Agda.Utils.Functor
import Agda.Utils.Permutation
#include "undefined.h"
import Agda.Utils.Impossible
class DropArgs a where
dropArgs :: Int -> a -> a
instance DropArgs a => DropArgs (Maybe a) where
dropArgs n = fmap (dropArgs n)
instance DropArgs Telescope where
dropArgs n tel = telFromList $ drop n $ telToList tel
instance DropArgs Permutation where
dropArgs n (Perm m p) = Perm (m n) $ map (subtract n) $ drop n p
instance DropArgs ClauseBody where
dropArgs 0 b = b
dropArgs _ NoBody = NoBody
dropArgs n (Bind b) = dropArgs (n 1) (absBody b)
dropArgs n Body{} = __IMPOSSIBLE__
instance DropArgs Clause where
dropArgs n cl =
cl{ clauseTel = dropArgs n $ clauseTel cl
, namedClausePats = drop n $ namedClausePats cl
, clauseBody = dropArgs n $ clauseBody cl
}
instance DropArgs FunctionInverse where
dropArgs n finv = fmap (dropArgs n) finv
instance DropArgs CompiledClauses where
dropArgs n cc = case cc of
Case i br | unArg i < n -> __IMPOSSIBLE__
| otherwise -> Case (i <&> \ j -> j n) $ fmap (dropArgs n) br
Done xs t | length xs < n -> __IMPOSSIBLE__
| otherwise -> Done (drop n xs) t
Fail -> Fail