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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
n forall a b. (a -> b) -> a -> b
$ 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 forall a. Num a => a -> a -> a
- Int
n) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Num a => a -> a -> a
subtract Int
n) forall a b. (a -> b) -> a -> b
$ 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 = forall a. Int -> [a] -> [a]
drop Int
n 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 = forall a. a -> a
id
  dropArgs Int
n = \case
    Lam ArgInfo
h Abs Term
b -> forall a. DropArgs a => Int -> a -> a
dropArgs (Int
n forall a. Num a => a -> a -> a
- Int
1) (forall a. Subst a => Abs a -> a
absBody Abs Term
b)
    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 | forall e. Arg e -> e
unArg Arg Int
i forall a. Ord a => a -> a -> Bool
< Int
n   -> forall a. HasCallStack => a
__IMPOSSIBLE__
              | Bool
otherwise     -> forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case (Arg Int
i forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Int
j -> Int
j forall a. Num a => a -> a -> a
- Int
n) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. DropArgs a => Int -> a -> a
dropArgs Int
n) Case CompiledClauses
br
    Done [Arg ArgName]
xs Term
t | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg ArgName]
xs forall a. Ord a => a -> a -> Bool
< Int
n -> forall a. HasCallStack => a
__IMPOSSIBLE__
              | Bool
otherwise     -> forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done (forall a. Int -> [a] -> [a]
drop Int
n [Arg ArgName]
xs) Term
t
    Fail [Arg ArgName]
xs   | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg ArgName]
xs forall a. Ord a => a -> a -> Bool
< Int
n -> forall a. HasCallStack => a
__IMPOSSIBLE__
              | Bool
otherwise     -> forall a. [Arg ArgName] -> CompiledClauses' a
Fail (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) = forall a. Int -> SplitTree' a
SplittingDone (Int
m forall a. Num a => a -> a -> a
- Int
n)
  dropArgs Int
n (SplitAt Arg Int
i LazySplit
lz SplitTrees' SplitTag
ts) = forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt (forall a. Num a => a -> a -> a
subtract Int
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Int
i) LazySplit
lz forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall a b. (a -> b) -> a -> b
$ forall a. DropArgs a => Int -> a -> a
dropArgs Int
n) SplitTrees' SplitTag
ts