    module Agda.TypeChecking.DropArgs where

    import Control.Arrow (second)

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Substitute

    import Agda.TypeChecking.CompiledClause
    import Agda.TypeChecking.Coverage.SplitTree

    import Agda.Utils.Functor
    import Agda.Utils.Permutation

    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * Dropping initial arguments to create a projection-like function
    ---------------------------------------------------------------------------

    -- | When making a function projection-like, we drop the first @n@
    --   arguments.
    class DropArgs a where
      dropArgs :: Int -> a -> a

    instance DropArgs a => DropArgs (Maybe a) where
      dropArgs :: Int -> Maybe a -> Maybe a
    dropArgs Int
    n = (a -> a) -> Maybe a -> Maybe a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Int -> a -> a
    forall a. DropArgs a => Int -> a -> a
    dropArgs Int
    n)

    -- | NOTE: This creates telescopes with unbound de Bruijn indices.
    instance DropArgs Telescope where
      dropArgs :: Int -> Telescope -> Telescope
    dropArgs Int
    n Telescope
    tel = ListTel -> Telescope
    telFromList (ListTel -> Telescope) -> ListTel -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Int -> ListTel -> ListTel
    forall a. Int -> [a] -> [a]
    drop Int
    n (ListTel -> ListTel) -> ListTel -> ListTel
    forall a b. (a -> b) -> a -> b
    $ Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel

    instance DropArgs Permutation where
      dropArgs :: Int -> Permutation -> Permutation
    dropArgs Int
    n (Perm Int
    m [Int]
    p) = Int -> [Int] -> Permutation
    Perm (Int
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    n) ([Int] -> Permutation) -> [Int] -> Permutation
    forall a b. (a -> b) -> a -> b
    $ (Int -> Int) -> [Int] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    subtract Int
    n) ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int] -> [Int]
    forall a. Int -> [a] -> [a]
    drop Int
    n [Int]
    p

    -- | NOTE: does not work for recursive functions.
    instance DropArgs Clause where
      dropArgs :: Int -> Clause -> Clause
    dropArgs Int
    n Clause
    cl =
          Clause
    cl{ -- Andreas, 2012-09-25: just dropping the front of telescope
              -- makes it ill-formed (unbound indices)
              -- we should let the telescope intact!?
              -- Ulf, 2016-06-23: Indeed. After parameter refinement it's even
              -- worse: the module parameters we want to drop aren't necessarily
              -- the first things in the telescope.
              namedClausePats :: NAPs
    namedClausePats = Int -> NAPs -> NAPs
    forall a. Int -> [a] -> [a]
    drop Int
    n (NAPs -> NAPs) -> NAPs -> NAPs
    forall a b. (a -> b) -> a -> b
    $ Clause -> NAPs
    namedClausePats Clause
    cl
              -- BUG: need to drop also from recursive calls!!
            }

    instance DropArgs FunctionInverse where
      dropArgs :: Int -> FunctionInverse -> FunctionInverse
    dropArgs Int
    n FunctionInverse
    finv = (Clause -> Clause) -> FunctionInverse -> FunctionInverse
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Int -> Clause -> Clause
    forall a. DropArgs a => Int -> a -> a
    dropArgs Int
    n) FunctionInverse
    finv

    -- | Use for dropping initial lambdas in clause bodies.
    --   NOTE: does not reduce term, need lambdas to be present.
    instance DropArgs Term where
      dropArgs :: Int -> Term -> Term
    dropArgs Int
    0 = Term -> Term
    forall a. a -> a
    id
      dropArgs Int
    n = \case
        Lam ArgInfo
    h Abs Term
    b -> Int -> Term -> Term
    forall a. DropArgs a => Int -> a -> a
    dropArgs (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Abs Term -> Term
    forall a. Subst a => Abs a -> a
    absBody Abs Term
    b)
        Term
    _       -> Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | To drop the first @n@ arguments in a compiled clause,
    --   we reduce the split argument indices by @n@ and
    --   drop @n@ arguments from the bodies.
    --   NOTE: this only works for non-recursive functions, we
    --   are not dropping arguments to recursive calls in bodies.
    instance DropArgs CompiledClauses where
      dropArgs :: Int -> CompiledClauses -> CompiledClauses
    dropArgs Int
    n CompiledClauses
    cc = case CompiledClauses
    cc of
        Case Arg Int
    i Case CompiledClauses
    br | Arg Int -> Int
    forall e. Arg e -> e
    unArg Arg Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n   -> CompiledClauses
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  | Bool
    otherwise     -> Arg Int -> Case CompiledClauses -> CompiledClauses
    forall a.
    Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
    Case (Arg Int
    i Arg Int -> (Int -> Int) -> Arg Int
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Int
    j -> Int
    j Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    n) (Case CompiledClauses -> CompiledClauses)
    -> Case CompiledClauses -> CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ (CompiledClauses -> CompiledClauses)
    -> Case CompiledClauses -> Case CompiledClauses
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Int -> CompiledClauses -> CompiledClauses
    forall a. DropArgs a => Int -> a -> a
    dropArgs Int
    n) Case CompiledClauses
    br
        Done [Arg ArgName]
    xs Term
    t | [Arg ArgName] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg ArgName]
    xs Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n -> CompiledClauses
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  | Bool
    otherwise     -> [Arg ArgName] -> Term -> CompiledClauses
    forall a. [Arg ArgName] -> a -> CompiledClauses' a
    Done (Int -> [Arg ArgName] -> [Arg ArgName]
    forall a. Int -> [a] -> [a]
    drop Int
    n [Arg ArgName]
    xs) Term
    t
        Fail [Arg ArgName]
    xs   | [Arg ArgName] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg ArgName]
    xs Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n -> CompiledClauses
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  | Bool
    otherwise     -> [Arg ArgName] -> CompiledClauses
    forall a. [Arg ArgName] -> CompiledClauses' a
    Fail (Int -> [Arg ArgName] -> [Arg ArgName]
    forall a. Int -> [a] -> [a]
    drop Int
    n [Arg ArgName]
    xs)

    instance DropArgs SplitTree where
      dropArgs :: Int -> SplitTree -> SplitTree
    dropArgs Int
    n (SplittingDone Int
    m) = Int -> SplitTree
    forall a. Int -> SplitTree' a
    SplittingDone (Int
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    n)
      dropArgs Int
    n (SplitAt Arg Int
    i LazySplit
    lz SplitTrees' SplitTag
    ts) = Arg Int -> LazySplit -> SplitTrees' SplitTag -> SplitTree
    forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
    SplitAt (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    subtract Int
    n (Int -> Int) -> Arg Int -> Arg Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Int
    i) LazySplit
    lz (SplitTrees' SplitTag -> SplitTree)
    -> SplitTrees' SplitTag -> SplitTree
    forall a b. (a -> b) -> a -> b
    $ ((SplitTag, SplitTree) -> (SplitTag, SplitTree))
    -> SplitTrees' SplitTag -> SplitTrees' SplitTag
    forall a b. (a -> b) -> [a] -> [b]
    map ((SplitTree -> SplitTree)
    -> (SplitTag, SplitTree) -> (SplitTag, SplitTree)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second ((SplitTree -> SplitTree)
     -> (SplitTag, SplitTree) -> (SplitTag, SplitTree))
    -> (SplitTree -> SplitTree)
    -> (SplitTag, SplitTree)
    -> (SplitTag, SplitTree)
    forall a b. (a -> b) -> a -> b
    $ Int -> SplitTree -> SplitTree
    forall a. DropArgs a => Int -> a -> a
    dropArgs Int
    n) SplitTrees' SplitTag
    ts