{-# LANGUAGE CPP #-}

module Agda.TypeChecking.DropArgs where

import Control.Arrow (first, 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

#include "undefined.h"
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 n = fmap (dropArgs n)

-- | NOTE: This creates telescopes with unbound de Bruijn indices.
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

-- | NOTE: does not work for recursive functions.
instance DropArgs Clause where
  dropArgs n cl =
      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 = drop n $ namedClausePats cl
          -- BUG: need to drop also from recursive calls!!
        }

instance DropArgs FunctionInverse where
  dropArgs n finv = fmap (dropArgs n) finv

-- | Use for dropping initial lambdas in clause bodies.
--   NOTE: does not reduce term, need lambdas to be present.
instance DropArgs Term where
  dropArgs 0 v = v
  dropArgs n v = case v of
    Lam h b -> dropArgs (n - 1) (absBody b)
    _       -> __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 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

instance DropArgs SplitTree where
  dropArgs n (SplittingDone m) = SplittingDone (m - n)
  dropArgs n (SplitAt i ts)    = SplitAt (subtract n <$> i) $ map (second $ dropArgs n) ts