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