{-# LANGUAGE BangPatterns       #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE TypeApplications   #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | This module contains the definition of hereditary substitution
-- and application operating on internal syntax which is in β-normal
-- form (β including projection reductions).
--
-- Further, it contains auxiliary functions which rely on substitution
-- but not on reduction.

module Agda.TypeChecking.Substitute
  ( module Agda.TypeChecking.Substitute
  , module Agda.TypeChecking.Substitute.Class
  , module Agda.TypeChecking.Substitute.DeBruijn
  , Substitution'(..), Substitution
  ) where

import Control.Arrow (second)
import Control.Monad (guard)
import Data.Coerce
import Data.Function
import qualified Data.List as List
import Data.Map (Map)
import Data.Maybe
import Data.HashMap.Strict (HashMap)

import Debug.Trace (trace)
import Language.Haskell.TH.Syntax (thenCmp) -- lexicographic combination of Ordering

import Agda.Interaction.Options

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Options (typeInType)
import Agda.TypeChecking.Free as Free
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Positivity.Occurrence as Occ

import Agda.TypeChecking.Substitute.Class
import Agda.TypeChecking.Substitute.DeBruijn

import Agda.Utils.Empty
import Agda.Utils.Functor
import Agda.Utils.List
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Size
import Agda.Utils.Tuple

import Agda.Utils.Impossible


-- | Apply @Elims@ while using the given function to report ill-typed
--   redexes.
--   Recursive calls for @applyE@ and @applySubst@ happen at type @t@ to
--   propagate the same strategy to subtrees.
{-# SPECIALIZE applyTermE :: (Empty -> Term -> Elims -> Term) -> Term -> Elims -> Term #-}
{-# SPECIALIZE applyTermE :: (Empty -> Term -> Elims -> Term) -> BraveTerm -> Elims -> BraveTerm #-}
applyTermE :: forall t. (Coercible Term t, Apply t, Subst t t)
           => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE err' m [] = m
applyTermE err' m es = coerce $
    case coerce m of
      Var i es'   -> Var i (es' ++ es)
      Def f es'   -> defApp f es' es  -- remove projection redexes
      Con c ci args -> conApp @t err' c ci args es
      Lam _ b     ->
        case es of
          Apply a : es0      -> lazyAbsApp (coerce b :: Abs t) (coerce $ unArg a) `app` es0
          IApply _ _ a : es0 -> lazyAbsApp (coerce b :: Abs t) (coerce a)         `app` es0
          _             -> err __IMPOSSIBLE__
      MetaV x es' -> MetaV x (es' ++ es)
      Lit{}       -> err __IMPOSSIBLE__
      Level{}     -> err __IMPOSSIBLE__
      Pi _ _      -> err __IMPOSSIBLE__
      Sort s      -> Sort $ s `applyE` es
      Dummy s es' -> Dummy s (es' ++ es)
      DontCare mv -> dontCare $ mv `app` es  -- Andreas, 2011-10-02
        -- need to go under DontCare, since "with" might resurrect irrelevant term
   where
     app :: Coercible t x => x -> Elims -> Term
     app t es = coerce $ (coerce t :: t) `applyE` es
     err e = err' e (coerce m) es

instance Apply Term where
  applyE = applyTermE absurd

instance Apply BraveTerm where
  applyE = applyTermE (\ _ t es ->  Dummy "applyE" (Apply (defaultArg t) : es))

-- | If $v$ is a record value, @canProject f v@
--   returns its field @f@.
canProject :: QName -> Term -> Maybe (Arg Term)
canProject f v =
  case v of
    (Con (ConHead _ _ fs) _ vs) -> do
      (fld, i) <- findWithIndex ((f==) . unArg) fs
      -- Jesper, 2019-10-17: dont unfold irrelevant projections
      guard $ not $ isIrrelevant fld
      -- Andreas, 2018-06-12, issue #2170
      -- The ArgInfo from the ConHead is more accurate (relevance subtyping!).
      setArgInfo (getArgInfo fld) <.> isApplyElim =<< listToMaybe (drop i vs)
    _ -> Nothing

-- | Eliminate a constructed term.
conApp :: forall t. (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp fk ch                  ci args []             = Con ch ci args
conApp fk ch                  ci args (a@Apply{} : es) = conApp @t fk ch ci (args ++ [a]) es
conApp fk ch                  ci args (a@IApply{} : es) = conApp @t fk ch ci (args ++ [a]) es
conApp fk ch@(ConHead c _ fs) ci args ees@(Proj o f : es) =
  let failure err = flip trace err $
        "conApp: constructor " ++ show c ++
        " with fields\n" ++ unlines (map (("  " ++) . show) fs) ++
        " and args\n" ++ unlines (map (("  " ++) . prettyShow) args) ++
        " projected by " ++ show f
      isApply e = fromMaybe (failure __IMPOSSIBLE__) $ isApplyElim e
      stuck err = fk err (Con ch ci args) [Proj o f]
      -- Recurse using the instance for 't', see @applyTermE@
      app :: Term -> Elims -> Term
      app v es = coerce $ applyE (coerce v :: t) es
  in
   case findWithIndex ((f==) . unArg) fs of
     Nothing -> failure $ stuck __IMPOSSIBLE__ `app` es
     Just (fld, i) -> let
      -- Andreas, 2018-06-12, issue #2170
      -- We safe-guard the projected value by DontCare using the ArgInfo stored at the record constructor,
      -- since the ArgInfo in the constructor application might be inaccurate because of subtyping.
      v = maybe (failure $ stuck __IMPOSSIBLE__) (relToDontCare fld . argToDontCare . isApply) $ listToMaybe $ drop i args
      in v `app` es

  -- -- Andreas, 2016-07-20 futile attempt to magically fix ProjOrigin
  --     fallback = v
  -- in  if not $ null es then applyE v es else
  --     -- If we have no more eliminations, we can return v
  --     if o == ProjSystem then fallback else
  --       -- If the result is a projected term with ProjSystem,
  --       -- we can can restore it to ProjOrigin o.
  --       -- Otherwise, we get unpleasant printing with eta-expanded record metas.
  --     caseMaybe (hasElims v) fallback $ \ (hd, es0) ->
  --       caseMaybe (initLast es0) fallback $ \ (es1, e2) ->
  --         case e2 of
  --           -- We want to replace this ProjSystem by o.
  --           Proj ProjSystem q -> hd (es1 ++ [Proj o q])
  --             -- Andreas, 2016-07-21 for the whole testsuite
  --             -- this case was never triggered!
  --           _ -> fallback

{-
      i = maybe failure id    $ elemIndex f $ map unArg fs
      v = maybe failure unArg $ listToMaybe $ drop i args
      -- Andreas, 2013-10-20 see Issue543a:
      -- protect result of irrelevant projection.
      r = maybe __IMPOSSIBLE__ getRelevance $ listToMaybe $ drop i fs
      u | Irrelevant <- r = DontCare v
        | otherwise       = v
  in  applyE v es
-}

-- | @defApp f us vs@ applies @Def f us@ to further arguments @vs@,
--   eliminating top projection redexes.
--   If @us@ is not empty, we cannot have a projection redex, since
--   the record argument is the first one.
defApp :: QName -> Elims -> Elims -> Term
defApp f [] (Apply a : es) | Just v <- canProject f (unArg a)
  = argToDontCare v `applyE` es
defApp f es0 es = Def f $ es0 ++ es

-- protect irrelevant fields (see issue 610)
argToDontCare :: Arg Term -> Term
argToDontCare (Arg ai v) = relToDontCare ai v

relToDontCare :: LensRelevance a => a -> Term -> Term
relToDontCare ai v
  | Irrelevant <- getRelevance ai = dontCare v
  | otherwise                     = v

-- Andreas, 2016-01-19: In connection with debugging issue #1783,
-- I consider the Apply instance for Type harmful, as piApply is not
-- safe if the type is not sufficiently reduced.
-- (piApply is not in the monad and hence cannot unfold type synonyms).
--
-- Without apply for types, one has to at least use piApply and be
-- aware of doing something which has a precondition
-- (type sufficiently reduced).
--
-- By grepping for piApply, one can quickly get an overview over
-- potentially harmful uses.
--
-- In general, piApplyM is preferable over piApply since it is more robust
-- and fails earlier than piApply, which may only fail at serialization time,
-- when all thunks are forced.

-- REMOVED:
-- instance Apply Type where
--   apply = piApply
--   -- Maybe an @applyE@ instance would be useful here as well.
--   -- A record type could be applied to a projection name
--   -- to yield the field type.
--   -- However, this works only in the monad where we can
--   -- look up the fields of a record type.

instance Apply Sort where
  applyE s [] = s
  applyE s es = case s of
    MetaS x es' -> MetaS x $ es' ++ es
    DefS  d es' -> DefS  d $ es' ++ es
    _ -> __IMPOSSIBLE__

-- @applyE@ does not make sense for telecopes, definitions, clauses etc.

instance Subst Term a => Apply (Tele a) where
  apply tel               []       = tel
  apply EmptyTel          _        = __IMPOSSIBLE__
  apply (ExtendTel _ tel) (t : ts) = lazyAbsApp tel (unArg t) `apply` ts

  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply Definition where
  apply (Defn info x t pol occ gens gpars df m c inst copy ma nc inj copat blk d) args =
    Defn info x (piApply t args) (apply pol args) (apply occ args) (apply gens args) (drop (length args) gpars) df m c inst copy ma nc inj copat blk (apply d args)

  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply RewriteRule where
  apply r args =
    let newContext = apply (rewContext r) args
        sub        = liftS (size newContext) $ parallelS $
                       reverse $ map (PTerm . unArg) args
    in RewriteRule
       { rewName    = rewName r
       , rewContext = newContext
       , rewHead    = rewHead r
       , rewPats    = applySubst sub (rewPats r)
       , rewRHS     = applyNLPatSubst sub (rewRHS r)
       , rewType    = applyNLPatSubst sub (rewType r)
       }

  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance {-# OVERLAPPING #-} Apply [Occ.Occurrence] where
  apply occ args = List.drop (length args) occ
  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance {-# OVERLAPPING #-} Apply [Polarity] where
  apply pol args = List.drop (length args) pol
  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply NumGeneralizableArgs where
  apply NoGeneralizableArgs       args = NoGeneralizableArgs
  apply (SomeGeneralizableArgs n) args = SomeGeneralizableArgs (n - length args)
  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

-- | Make sure we only drop variable patterns.
instance {-# OVERLAPPING #-} Apply [NamedArg (Pattern' a)] where
  apply ps args = loop (length args) ps
    where
    loop 0 ps = ps
    loop n [] = __IMPOSSIBLE__
    loop n (p : ps) =
      let recurse = loop (n - 1) ps
      in  case namedArg p of
            VarP{}  -> recurse
            DotP{}  -> __IMPOSSIBLE__
            LitP{}  -> __IMPOSSIBLE__
            ConP{}  -> __IMPOSSIBLE__
            DefP{}  -> __IMPOSSIBLE__
            ProjP{} -> __IMPOSSIBLE__
            IApplyP{} -> recurse

  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply Projection where
  apply p args = p
    { projIndex = projIndex p - size args
    , projLams  = projLams p `apply` args
    }
  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply ProjLams where
  apply (ProjLams lams) args = ProjLams $ List.drop (length args) lams
  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply Defn where
  apply d [] = d
  apply d args = case d of
    Axiom{} -> d
    DataOrRecSig n -> DataOrRecSig (n - length args)
    GeneralizableVar{} -> d
    AbstractDefn d -> AbstractDefn $ apply d args
    Function{ funClauses = cs, funCompiled = cc, funCovering = cov, funInv = inv
            , funExtLam = extLam
            , funProjection = Nothing } ->
      d { funClauses    = apply cs args
        , funCompiled   = apply cc args
        , funCovering   = apply cov args
        , funInv        = apply inv args
        , funExtLam     = modifySystem (`apply` args) <$> extLam
        }

    Function{ funClauses = cs, funCompiled = cc, funCovering = cov, funInv = inv
            , funExtLam = extLam
            , funProjection = Just p0} ->
      case p0 `apply` args of
        p@Projection{ projIndex = n }
          | n < 0     -> d { funProjection = __IMPOSSIBLE__ } -- TODO (#3123): we actually get here!
          -- case: applied only to parameters
          | n > 0     -> d { funProjection = Just p }
          -- case: applied also to record value (n == 0)
          | otherwise ->
              d { funClauses        = apply cs args'
                , funCompiled       = apply cc args'
                , funCovering       = apply cov args'
                , funInv            = apply inv args'
                , funProjection     = if isVar0 then Just p{ projIndex = 0 } else Nothing
                , funExtLam         = modifySystem (\ _ -> __IMPOSSIBLE__) <$> extLam
                }
              where
                larg  = last args -- the record value
                args' = [larg]
                isVar0 = case unArg larg of Var 0 [] -> True; _ -> False
{-
    Function{ funClauses = cs, funCompiled = cc, funInv = inv
            , funProjection = Just p@Projection{ projIndex = n } }
        -- case: only applying parameters
      | size args < n -> d { funProjection = Just $ p `apply` args }
        -- case: apply also to record value
      | otherwise     ->
        d { funClauses        = apply cs args'
          , funCompiled       = apply cc args'
          , funInv            = apply inv args'
          , funProjection     = Just $ p { projIndex = 0 } -- Nothing ?
          }
      where args' = [last args]  -- the record value
-}
    Datatype{ dataPars = np, dataClause = cl } ->
      d { dataPars = np - size args
        , dataClause     = apply cl args
        }
    Record{ recPars = np, recClause = cl, recTel = tel
          {-, recArgOccurrences = occ-} } ->
      d { recPars = np - size args
        , recClause = apply cl args, recTel = apply tel args
--        , recArgOccurrences = List.drop (length args) occ
        }
    Constructor{ conPars = np } ->
      d { conPars = np - size args }
    Primitive{ primClauses = cs } ->
      d { primClauses = apply cs args }

  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply PrimFun where
  apply (PrimFun x ar def) args = PrimFun x (ar - size args) $ \ vs -> def (args ++ vs)
  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply Clause where
    -- This one is a little bit tricksy after the parameter refinement change.
    -- It is assumed that we only apply a clause to "parameters", i.e.
    -- arguments introduced by lambda lifting. The problem is that these aren't
    -- necessarily the first elements of the clause telescope.
    apply cls@(Clause rl rf tel ps b t catchall recursive unreachable ell) args
      | length args > length ps = __IMPOSSIBLE__
      | otherwise =
      Clause rl rf
             tel'
             (applySubst rhoP $ drop (length args) ps)
             (applySubst rho b)
             (applySubst rho t)
             catchall
             recursive
             unreachable
             ell
      where
        -- We have
        --  Γ ⊢ args, for some outer context Γ
        --  Δ ⊢ ps,   where Δ is the clause telescope (tel)
        rargs = map unArg $ reverse args
        rps   = reverse $ take (length args) ps
        n     = size tel

        -- This is the new telescope. Created by substituting the args into the
        -- appropriate places in the old telescope. We know where those are by
        -- looking at the deBruijn indices of the patterns.
        tel' = newTel n tel rps rargs

        -- We then have to create a substitution from the old telescope to the
        -- new telescope that we can apply to dot patterns and the clause body.
        rhoP :: PatternSubstitution
        rhoP = mkSub dotP n rps rargs
        rho  = mkSub id   n rps rargs

        substP :: Nat -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
        substP i v = subst i (dotP v)

        -- Building the substitution from the old telescope to the new. The
        -- interesting case is when we have a variable pattern:
        --  We need Δ′ ⊢ ρ : Δ
        --  where Δ′ = newTel Δ (xⁱ : ps) (v : vs)
        --           = newTel Δ[xⁱ:=v] ps[xⁱ:=v'] vs
        --  Note that we need v' = raise (|Δ| - 1) v, to make Γ ⊢ v valid in
        --  ΓΔ[xⁱ:=v].
        --  A recursive call ρ′ = mkSub (substP i v' ps) vs gets us
        --    Δ′ ⊢ ρ′ : Δ[xⁱ:=v]
        --  so we just need Δ[xⁱ:=v] ⊢ σ : Δ and then ρ = ρ′ ∘ σ.
        --  That's achieved by σ = singletonS i v'.
        mkSub :: Subst a a => (Term -> a) -> Nat -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
        mkSub _ _ [] [] = idS
        mkSub tm n (p : ps) (v : vs) =
          case namedArg p of
            VarP _ (DBPatVar _ i) -> mkSub tm (n - 1) (substP i v' ps) vs `composeS` singletonS i (tm v')
              where v' = raise (n - 1) v
            DotP{}  -> mkSub tm n ps vs
            ConP c _ ps' -> mkSub tm n (ps' ++ ps) (projections c v ++ vs)
            DefP o q ps' -> mkSub tm n (ps' ++ ps) vs
            LitP{}  -> __IMPOSSIBLE__
            ProjP{} -> __IMPOSSIBLE__
            IApplyP _ _ _ (DBPatVar _ i) -> mkSub tm (n - 1) (substP i v' ps) vs `composeS` singletonS i (tm v')
              where v' = raise (n - 1) v
        mkSub _ _ _ _ = __IMPOSSIBLE__

        -- The parameter patterns 'ps' are all variables or dot patterns, or eta
        -- expanded record patterns (issue #2550). If they are variables they
        -- can appear anywhere in the clause telescope. This function
        -- constructs the new telescope with 'vs' substituted for 'ps'.
        -- Example:
        --    tel = (x : A) (y : B) (z : C) (w : D)
        --    ps  = y@3 w@0
        --    vs  = u v
        --    newTel tel ps vs = (x : A) (z : C[u/y])
        newTel :: Nat -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
        newTel n tel [] [] = tel
        newTel n tel (p : ps) (v : vs) =
          case namedArg p of
            VarP _ (DBPatVar _ i) -> newTel (n - 1) (subTel (size tel - 1 - i) v tel) (substP i (raise (n - 1) v) ps) vs
            DotP{}              -> newTel n tel ps vs
            ConP c _ ps'        -> newTel n tel (ps' ++ ps) (projections c v ++ vs)
            DefP _ q ps'        -> newTel n tel (ps' ++ ps) vs
            LitP{}              -> __IMPOSSIBLE__
            ProjP{}             -> __IMPOSSIBLE__
            IApplyP _ _ _ (DBPatVar _ i) -> newTel (n - 1) (subTel (size tel - 1 - i) v tel) (substP i (raise (n - 1) v) ps) vs
        newTel _ tel _ _ = __IMPOSSIBLE__

        projections c v = [ relToDontCare ai $ applyE v [Proj ProjSystem f] | Arg ai f <- conFields c ]

        -- subTel i v (Δ₁ (xᵢ : A) Δ₂) = Δ₁ Δ₂[xᵢ = v]
        subTel i v EmptyTel = __IMPOSSIBLE__
        subTel 0 v (ExtendTel _ tel) = absApp tel v
        subTel i v (ExtendTel a tel) = ExtendTel a $ subTel (i - 1) (raise 1 v) <$> tel

    applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply CompiledClauses where
  apply cc args = case cc of
    Fail     -> Fail
    Done hs t
      | length hs >= len ->
         let sub = parallelS $ map var [0..length hs - len - 1] ++ map unArg args
         in  Done (List.drop len hs) $ applySubst sub t
      | otherwise -> __IMPOSSIBLE__
    Case n bs
      | unArg n >= len -> Case (n <&> \ m -> m - len) (apply bs args)
      | otherwise -> __IMPOSSIBLE__
    where
      len = length args
  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply ExtLamInfo where
  apply (ExtLamInfo m sys) args = ExtLamInfo m (apply sys args)
  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply System where
  -- We assume we apply a system only to arguments introduced by
  -- lambda lifting.
  apply (System tel sys) args
      = if nargs > ntel then __IMPOSSIBLE__
        else System newTel (map (map (f -*- id) -*- f) sys)

    where
      f = applySubst sigma
      nargs = length args
      ntel = size tel
      newTel = apply tel args
      -- newTel ⊢ σ : tel
      sigma = liftS (ntel - nargs) (parallelS (reverse $ map unArg args))

  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply a => Apply (WithArity a) where
  apply  (WithArity n a) args = WithArity n $ apply  a args
  applyE (WithArity n a) es   = WithArity n $ applyE a es

instance Apply a => Apply (Case a) where
  apply (Branches cop cs eta ls m b lz) args =
    Branches cop (apply cs args) (second (`apply` args) <$> eta) (apply ls args) (apply m args) b lz
  applyE (Branches cop cs eta ls m b lz) es =
    Branches cop (applyE cs es) (second (`applyE` es) <$> eta)(applyE ls es) (applyE m es) b lz

instance Apply FunctionInverse where
  apply NotInjective  args = NotInjective
  apply (Inverse inv) args = Inverse $ apply inv args

  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Apply DisplayTerm where
  apply (DTerm v)          args = DTerm $ apply v args
  apply (DDot v)           args = DDot  $ apply v args
  apply (DCon c ci vs)     args = DCon c ci $ vs ++ map (fmap DTerm) args
  apply (DDef c es)        args = DDef c $ es ++ map (Apply . fmap DTerm) args
  apply (DWithApp v ws es) args = DWithApp v ws $ es ++ map Apply args

  applyE (DTerm v)           es = DTerm $ applyE v es
  applyE (DDot v)            es = DDot  $ applyE v es
  applyE (DCon c ci vs)      es = DCon c ci $ vs ++ map (fmap DTerm) ws
    where ws = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
  applyE (DDef c es')        es = DDef c $ es' ++ map (fmap DTerm) es
  applyE (DWithApp v ws es') es = DWithApp v ws $ es' ++ es

instance {-# OVERLAPPABLE #-} Apply t => Apply [t] where
  apply  ts args = map (`apply` args) ts
  applyE ts es   = map (`applyE` es) ts

instance Apply t => Apply (Blocked t) where
  apply  b args = fmap (`apply` args) b
  applyE b es   = fmap (`applyE` es) b

instance Apply t => Apply (Maybe t) where
  apply  x args = fmap (`apply` args) x
  applyE x es   = fmap (`applyE` es) x

instance Apply t => Apply (Strict.Maybe t) where
  apply  x args = fmap (`apply` args) x
  applyE x es   = fmap (`applyE` es) x

instance Apply v => Apply (Map k v) where
  apply  x args = fmap (`apply` args) x
  applyE x es   = fmap (`applyE` es) x

instance Apply v => Apply (HashMap k v) where
  apply  x args = fmap (`apply` args) x
  applyE x es   = fmap (`applyE` es) x

instance (Apply a, Apply b) => Apply (a,b) where
  apply  (x,y) args = (apply  x args, apply  y args)
  applyE (x,y) es   = (applyE x es  , applyE y es  )

instance (Apply a, Apply b, Apply c) => Apply (a,b,c) where
  apply  (x,y,z) args = (apply  x args, apply  y args, apply  z args)
  applyE (x,y,z) es   = (applyE x es  , applyE y es  , applyE z es  )

instance DoDrop a => Apply (Drop a) where
  apply x args = dropMore (size args) x
  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance DoDrop a => Abstract (Drop a) where
  abstract tel x = unDrop (size tel) x

instance Apply Permutation where
  -- The permutation must start with [0..m - 1]
  -- NB: section (- m) not possible (unary minus), hence (flip (-) m)
  apply (Perm n xs) args = Perm (n - m) $ map (flip (-) m) $ drop m xs
    where
      m = size args

  applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es

instance Abstract Permutation where
  abstract tel (Perm n xs) = Perm (n + m) $ [0..m - 1] ++ map (+ m) xs
    where
      m = size tel

-- | @(x:A)->B(x) `piApply` [u] = B(u)@
--
--   Precondition: The type must contain the right number of pis without
--   having to perform any reduction.
--
--   @piApply@ is potentially unsafe, the monadic 'piApplyM' is preferable.
piApply :: Type -> Args -> Type
piApply t []                      = t
piApply (El _ (Pi  _ b)) (a:args) = lazyAbsApp b (unArg a) `piApply` args
piApply t args                    =
  trace ("piApply t = " ++ show t ++ "\n  args = " ++ show args) __IMPOSSIBLE__

---------------------------------------------------------------------------
-- * Abstraction
---------------------------------------------------------------------------

instance Abstract Term where
  abstract = teleLam

instance Abstract Type where
  abstract = telePi_

instance Abstract Sort where
  abstract EmptyTel s = s
  abstract _        s = __IMPOSSIBLE__

instance Abstract Telescope where
  EmptyTel           `abstract` tel = tel
  ExtendTel arg xtel `abstract` tel = ExtendTel arg $ xtel <&> (`abstract` tel)

instance Abstract Definition where
  abstract tel (Defn info x t pol occ gens gpars df m c inst copy ma nc inj copat blk d) =
    Defn info x (abstract tel t) (abstract tel pol) (abstract tel occ) (abstract tel gens)
                (replicate (size tel) Nothing ++ gpars) df m c inst copy ma nc inj copat blk (abstract tel d)

-- | @tel ⊢ (Γ ⊢ lhs ↦ rhs : t)@ becomes @tel, Γ ⊢ lhs ↦ rhs : t)@
--   we do not need to change lhs, rhs, and t since they live in Γ.
--   See 'Abstract Clause'.
instance Abstract RewriteRule where
  abstract tel (RewriteRule q gamma f ps rhs t) =
    RewriteRule q (abstract tel gamma) f ps rhs t

instance {-# OVERLAPPING #-} Abstract [Occ.Occurrence] where
  abstract tel []  = []
  abstract tel occ = replicate (size tel) Mixed ++ occ -- TODO: check occurrence

instance {-# OVERLAPPING #-} Abstract [Polarity] where
  abstract tel []  = []
  abstract tel pol = replicate (size tel) Invariant ++ pol -- TODO: check polarity

instance Abstract NumGeneralizableArgs where
  abstract tel NoGeneralizableArgs       = NoGeneralizableArgs
  abstract tel (SomeGeneralizableArgs n) = SomeGeneralizableArgs (size tel + n)

instance Abstract Projection where
  abstract tel p = p
    { projIndex = size tel + projIndex p
    , projLams  = abstract tel $ projLams p
    }

instance Abstract ProjLams where
  abstract tel (ProjLams lams) = ProjLams $
    map (\ !dom -> argFromDom (fst <$> dom)) (telToList tel) ++ lams

instance Abstract System where
  abstract tel (System tel1 sys) = System (abstract tel tel1) sys

instance Abstract Defn where
  abstract tel d = case d of
    Axiom{} -> d
    DataOrRecSig n -> DataOrRecSig (size tel + n)
    GeneralizableVar{} -> d
    AbstractDefn d -> AbstractDefn $ abstract tel d
    Function{ funClauses = cs, funCompiled = cc, funCovering = cov, funInv = inv
            , funExtLam = extLam
            , funProjection = Nothing  } ->
      d { funClauses  = abstract tel cs
        , funCompiled = abstract tel cc
        , funCovering = abstract tel cov
        , funInv      = abstract tel inv
        , funExtLam   = modifySystem (abstract tel) <$> extLam
        }
    Function{ funClauses = cs, funCompiled = cc, funCovering = cov, funInv = inv
            , funExtLam = extLam
            , funProjection = Just p } ->
      -- Andreas, 2015-05-11 if projection was applied to Var 0
      -- then abstract over last element of tel (the others are params).
      if projIndex p > 0 then d' else
        d' { funClauses  = abstract tel1 cs
           , funCompiled = abstract tel1 cc
           , funCovering = abstract tel1 cov
           , funInv      = abstract tel1 inv
           , funExtLam   = modifySystem (\ _ -> __IMPOSSIBLE__) <$> extLam
           }
        where
          d' = d { funProjection = Just $ abstract tel p }
          tel1 = telFromList $ drop (size tel - 1) $ telToList tel

    Datatype{ dataPars = np, dataClause = cl } ->
      d { dataPars       = np + size tel
        , dataClause     = abstract tel cl
        }
    Record{ recPars = np, recClause = cl, recTel = tel' } ->
      d { recPars    = np + size tel
        , recClause  = abstract tel cl
        , recTel     = abstract tel tel'
        }
    Constructor{ conPars = np } ->
      d { conPars = np + size tel }
    Primitive{ primClauses = cs } ->
      d { primClauses = abstract tel cs }

instance Abstract PrimFun where
    abstract tel (PrimFun x ar def) = PrimFun x (ar + n) $ \ts -> def $ drop n ts
        where n = size tel

instance Abstract Clause where
  abstract tel (Clause rl rf tel' ps b t catchall recursive unreachable ell) =
    Clause rl rf (abstract tel tel')
           (namedTelVars m tel ++ ps)
           b
           t -- nothing to do for t, since it lives under the telescope
           catchall
           recursive
           unreachable
           ell
      where m = size tel + size tel'

instance Abstract CompiledClauses where
  abstract tel Fail = Fail
  abstract tel (Done xs t) = Done (map (argFromDom . fmap fst) (telToList tel) ++ xs) t
  abstract tel (Case n bs) =
    Case (n <&> \ i -> i + size tel) (abstract tel bs)

instance Abstract a => Abstract (WithArity a) where
  abstract tel (WithArity n a) = WithArity n $ abstract tel a

instance Abstract a => Abstract (Case a) where
  abstract tel (Branches cop cs eta ls m b lz) =
    Branches cop (abstract tel cs) (second (abstract tel) <$> eta)
                 (abstract tel ls) (abstract tel m) b lz

telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
telVars m = map (fmap namedThing) . (namedTelVars m)

namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
namedTelVars m EmptyTel                     = []
namedTelVars m (ExtendTel !dom tel) =
  Arg (domInfo dom) (namedDBVarP (m-1) $ absName tel) :
  namedTelVars (m-1) (unAbs tel)

instance Abstract FunctionInverse where
  abstract tel NotInjective  = NotInjective
  abstract tel (Inverse inv) = Inverse $ abstract tel inv

instance {-# OVERLAPPABLE #-} Abstract t => Abstract [t] where
  abstract tel = map (abstract tel)

instance Abstract t => Abstract (Maybe t) where
  abstract tel x = fmap (abstract tel) x

instance Abstract v => Abstract (Map k v) where
  abstract tel m = fmap (abstract tel) m

instance Abstract v => Abstract (HashMap k v) where
  abstract tel m = fmap (abstract tel) m

abstractArgs :: Abstract a => Args -> a -> a
abstractArgs args x = abstract tel x
    where
        tel   = foldr (\arg@(Arg info x) -> ExtendTel (__DUMMY_TYPE__ <$ domFromArg arg) . Abs x)
                      EmptyTel
              $ zipWith (<$) names args
        names = cycle $ map (stringToArgName . (:[])) ['a'..'z']

---------------------------------------------------------------------------
-- * Substitution and shifting\/weakening\/strengthening
---------------------------------------------------------------------------

-- | If @permute π : [a]Γ -> [a]Δ@, then @applySubst (renaming _ π) : Term Γ -> Term Δ@
renaming :: forall a. DeBruijn a => Empty -> Permutation -> Substitution' a
renaming err p = prependS err gamma $ raiseS $ size p
  where
    gamma :: [Maybe a]
    gamma = inversePermute p (deBruijnVar :: Int -> a)
    -- gamma = safePermute (invertP (-1) p) $ map deBruijnVar [0..]

-- | If @permute π : [a]Γ -> [a]Δ@, then @applySubst (renamingR π) : Term Δ -> Term Γ@
renamingR :: DeBruijn a => Permutation -> Substitution' a
renamingR p@(Perm n _) = permute (reverseP p) (map deBruijnVar [0..]) ++# raiseS n

-- | The permutation should permute the corresponding context. (right-to-left list)
renameP :: Subst t a => Empty -> Permutation -> a -> a
renameP err p = applySubst (renaming err p)

instance Subst a a => Subst a (Substitution' a) where
  applySubst rho sgm = composeS rho sgm

{-# SPECIALIZE applySubstTerm :: Substitution -> Term -> Term #-}
{-# SPECIALIZE applySubstTerm :: Substitution' BraveTerm -> BraveTerm -> BraveTerm #-}
applySubstTerm :: forall t. (Coercible t Term, Subst t t, Apply t) => Substitution' t -> t -> t
applySubstTerm IdS t = t
applySubstTerm rho t    = coerce $ case coerce t of
    Var i es    -> coerce $ lookupS rho i  `applyE` subE es
    Lam h m     -> Lam h $ sub @(Abs t) m
    Def f es    -> defApp f [] $ subE es
    Con c ci vs -> Con c ci $ subE vs
    MetaV x es  -> MetaV x $ subE es
    Lit l       -> Lit l
    Level l     -> levelTm $ sub @(Level' t) l
    Pi a b      -> uncurry Pi $ subPi (a,b)
    Sort s      -> Sort $ sub @(Sort' t) s
    DontCare mv -> dontCare $ sub @t mv
    Dummy s es  -> Dummy s $ subE es
 where
   sub :: forall a b. (Coercible b a, Subst t a) => b -> b
   sub t = coerce $ applySubst rho (coerce t :: a)
   subE :: Elims -> Elims
   subE  = sub @[Elim' t]
   subPi :: (Dom Type, Abs Type) -> (Dom Type, Abs Type)
   subPi = sub @(Dom' t (Type'' t t), Abs (Type'' t t))

instance Subst Term Term where
  applySubst = applySubstTerm

instance Subst BraveTerm BraveTerm where
  applySubst = applySubstTerm

instance (Coercible a Term, Subst t a, Subst t b) => Subst t (Type'' a b) where
  applySubst rho (El s t) = applySubst rho s `El` applySubst rho t

instance (Coercible a Term, Subst t a) => Subst t (Sort' a) where
  applySubst rho s = case s of
    Type n     -> Type $ sub n
    Prop n     -> Prop $ sub n
    Inf        -> Inf
    SizeUniv   -> SizeUniv
    PiSort a s2 -> coerce $ piSort (coerce $ sub a) (coerce $ sub s2)
    FunSort s1 s2 -> coerce $ funSort (coerce $ sub s1) (coerce $ sub s2)
    UnivSort s -> coerce $ univSort Nothing $ coerce $ sub s
    MetaS x es -> MetaS x $ sub es
    DefS d es  -> DefS d $ sub es
    DummyS{}   -> s
    where sub x = applySubst rho x

instance Subst t a => Subst t (Level' a) where
  applySubst rho (Max n as) = Max n $ applySubst rho as

instance Subst t a => Subst t (PlusLevel' a) where
  applySubst rho (Plus n l) = Plus n $ applySubst rho l

instance Subst t a => Subst t (LevelAtom' a) where
  applySubst rho (MetaLevel m vs)   = MetaLevel m    $ applySubst rho vs
  applySubst rho (BlockedLevel m v) = BlockedLevel m $ applySubst rho v
  applySubst rho (NeutralLevel _ v) = UnreducedLevel $ applySubst rho v
  applySubst rho (UnreducedLevel v) = UnreducedLevel $ applySubst rho v

instance Subst Term Name where
  applySubst rho = id

instance {-# OVERLAPPING #-} Subst Term String where
  applySubst rho = id

instance Subst Term ConPatternInfo where
  applySubst rho i = i{ conPType = applySubst rho $ conPType i }

instance Subst Term Pattern where
  applySubst rho p = case p of
    ConP c mt ps -> ConP c (applySubst rho mt) $ applySubst rho ps
    DefP o q ps  -> DefP o q $ applySubst rho ps
    DotP o t     -> DotP o $ applySubst rho t
    VarP o s     -> p
    LitP o l     -> p
    ProjP{}      -> p
    IApplyP o t u x -> IApplyP o (applySubst rho t) (applySubst rho u) x

instance Subst Term A.ProblemEq where
  applySubst rho (A.ProblemEq p v a) =
    uncurry (A.ProblemEq p) $ applySubst rho (v,a)

instance DeBruijn BraveTerm where
  deBruijnVar = BraveTerm . deBruijnVar
  deBruijnView = deBruijnView . unBrave

instance DeBruijn NLPat where
  deBruijnVar i = PVar i []
  deBruijnView p = case p of
    PVar i []   -> Just i
    PVar{}      -> Nothing
    PDef{}      -> Nothing
    PLam{}      -> Nothing
    PPi{}       -> Nothing
    PSort{}     -> Nothing
    PBoundVar{} -> Nothing -- or... ?
    PTerm{}     -> Nothing -- or... ?

applyNLPatSubst :: (Subst Term a) => Substitution' NLPat -> a -> a
applyNLPatSubst = applySubst . fmap nlPatToTerm
  where
    nlPatToTerm :: NLPat -> Term
    nlPatToTerm p = case p of
      PVar i xs      -> Var i $ map (Apply . fmap var) xs
      PTerm u        -> u
      PDef f es      -> __IMPOSSIBLE__
      PLam i u       -> __IMPOSSIBLE__
      PPi a b        -> __IMPOSSIBLE__
      PSort s        -> __IMPOSSIBLE__
      PBoundVar i es -> __IMPOSSIBLE__

applyNLSubstToDom :: Subst NLPat a => Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom rho dom = applySubst rho <$> dom{ domTactic = applyNLPatSubst rho $ domTactic dom }

instance Subst NLPat NLPat where
  applySubst rho p = case p of
    PVar i bvs -> lookupS rho i `applyBV` bvs
    PDef f es -> PDef f $ applySubst rho es
    PLam i u -> PLam i $ applySubst rho u
    PPi a b -> PPi (applyNLSubstToDom rho a) (applySubst rho b)
    PSort s -> PSort $ applySubst rho s
    PBoundVar i es -> PBoundVar i $ applySubst rho es
    PTerm u -> PTerm $ applyNLPatSubst rho u

    where
      applyBV :: NLPat -> [Arg Int] -> NLPat
      applyBV p ys = case p of
        PVar i xs      -> PVar i (xs ++ ys)
        PTerm u        -> PTerm $ u `apply` map (fmap var) ys
        PDef f es      -> __IMPOSSIBLE__
        PLam i u       -> __IMPOSSIBLE__
        PPi a b        -> __IMPOSSIBLE__
        PSort s        -> __IMPOSSIBLE__
        PBoundVar i es -> __IMPOSSIBLE__

instance Subst NLPat NLPType where
  applySubst rho (NLPType s a) = NLPType (applySubst rho s) (applySubst rho a)

instance Subst NLPat NLPSort where
  applySubst rho = \case
    PType l   -> PType $ applySubst rho l
    PProp l   -> PProp $ applySubst rho l
    PInf      -> PInf
    PSizeUniv -> PSizeUniv

instance Subst NLPat RewriteRule where
  applySubst rho (RewriteRule q gamma f ps rhs t) =
    RewriteRule q (applyNLPatSubst rho gamma)
                f (applySubst (liftS n rho) ps)
                  (applyNLPatSubst (liftS n rho) rhs)
                  (applyNLPatSubst (liftS n rho) t)
    where n = size gamma

instance Subst t a => Subst t (Blocked a) where
  applySubst rho b = fmap (applySubst rho) b

instance Subst Term DisplayForm where
  applySubst rho (Display n ps v) =
    Display n (applySubst (liftS 1 rho) ps)
              (applySubst (liftS n rho) v)

instance Subst Term DisplayTerm where
  applySubst rho (DTerm v)        = DTerm $ applySubst rho v
  applySubst rho (DDot v)         = DDot  $ applySubst rho v
  applySubst rho (DCon c ci vs)   = DCon c ci $ applySubst rho vs
  applySubst rho (DDef c es)      = DDef c $ applySubst rho es
  applySubst rho (DWithApp v vs es) = uncurry3 DWithApp $ applySubst rho (v, vs, es)

instance Subst t a => Subst t (Tele a) where
  applySubst rho  EmptyTel         = EmptyTel
  applySubst rho (ExtendTel t tel) = uncurry ExtendTel $ applySubst rho (t, tel)

instance Subst Term Constraint where
  applySubst rho c = case c of
    ValueCmp cmp a u v       -> ValueCmp cmp (rf a) (rf u) (rf v)
    ValueCmpOnFace cmp p t u v -> ValueCmpOnFace cmp (rf p) (rf t) (rf u) (rf v)
    ElimCmp ps fs a v e1 e2  -> ElimCmp ps fs (rf a) (rf v) (rf e1) (rf e2)
    TelCmp a b cmp tel1 tel2 -> TelCmp (rf a) (rf b) cmp (rf tel1) (rf tel2)
    SortCmp cmp s1 s2        -> SortCmp cmp (rf s1) (rf s2)
    LevelCmp cmp l1 l2       -> LevelCmp cmp (rf l1) (rf l2)
    Guarded c cs             -> Guarded (rf c) cs
    IsEmpty r a              -> IsEmpty r (rf a)
    CheckSizeLtSat t         -> CheckSizeLtSat (rf t)
    FindInstance m b cands   -> FindInstance m b (rf cands)
    UnBlock{}                -> c
    CheckFunDef{}            -> c
    HasBiggerSort s          -> HasBiggerSort (rf s)
    HasPTSRule a s           -> HasPTSRule (rf a) (rf s)
    UnquoteTactic m t h g    -> UnquoteTactic m (rf t) (rf h) (rf g)
    CheckMetaInst m          -> CheckMetaInst m
    where
      rf x = applySubst rho x

instance Subst Term CompareAs where
  applySubst rho (AsTermsOf a) = AsTermsOf $ applySubst rho a
  applySubst rho AsSizes       = AsSizes
  applySubst rho AsTypes       = AsTypes

instance Subst t a => Subst t (Elim' a) where
  applySubst rho e = case e of
    Apply v -> Apply $ applySubst rho v
    IApply x y r -> IApply (applySubst rho x) (applySubst rho y) (applySubst rho r)
    Proj{}  -> e

instance Subst t a => Subst t (Abs a) where
  applySubst rho (Abs x a)   = Abs x $ applySubst (liftS 1 rho) a
  applySubst rho (NoAbs x a) = NoAbs x $ applySubst rho a

instance Subst t a => Subst t (Arg a) where
  applySubst IdS arg = arg
  applySubst rho arg = setFreeVariables unknownFreeVariables $ fmap (applySubst rho) arg

instance Subst t a => Subst t (Named name a) where
  applySubst rho = fmap (applySubst rho)

instance (Subst t a, Subst t b) => Subst t (Dom' a b) where
  applySubst IdS dom = dom
  applySubst rho dom = setFreeVariables unknownFreeVariables $
    fmap (applySubst rho) dom{ domTactic = applySubst rho (domTactic dom) }

instance Subst t a          => Subst t (Maybe a)      where
instance Subst t a          => Subst t [a]            where
instance (Ord k, Subst t a) => Subst t (Map k a)      where
instance Subst t a          => Subst t (WithHiding a) where

instance Subst Term () where
  applySubst _ _ = ()

instance (Subst t a, Subst t b) => Subst t (a, b) where
  applySubst rho (x,y) = (applySubst rho x, applySubst rho y)

instance (Subst t a, Subst t b, Subst t c) => Subst t (a, b, c) where
  applySubst rho (x,y,z) = (applySubst rho x, applySubst rho y, applySubst rho z)

instance (Subst t a, Subst t b, Subst t c, Subst t d) => Subst t (a, b, c, d) where
  applySubst rho (x,y,z,u) = (applySubst rho x, applySubst rho y, applySubst rho z, applySubst rho u)

instance Subst Term Candidate where
  applySubst rho (Candidate u t ov) = Candidate (applySubst rho u) (applySubst rho t) ov

instance Subst Term EqualityView where
  applySubst rho (OtherType t) = OtherType
    (applySubst rho t)
  applySubst rho (EqualityType s eq l t a b) = EqualityType
    (applySubst rho s)
    eq
    (map (applySubst rho) l)
    (applySubst rho t)
    (applySubst rho a)
    (applySubst rho b)

instance DeBruijn a => DeBruijn (Pattern' a) where
  debruijnNamedVar n i             = varP $ debruijnNamedVar n i
  -- deBruijnView returns Nothing, to prevent consS and the like
  -- from dropping the names and origins when building a substitution.
  deBruijnView _                   = Nothing

fromPatternSubstitution :: PatternSubstitution -> Substitution
fromPatternSubstitution = fmap patternToTerm

applyPatSubst :: (Subst Term a) => PatternSubstitution -> a -> a
applyPatSubst = applySubst . fromPatternSubstitution


usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
usePatOrigin o p = case patternInfo p of
  Nothing -> p
  Just i  -> usePatternInfo (i { patOrigin = o }) p

usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo i p = case patternOrigin p of
  Nothing         -> p
  Just PatOSplit  -> p
  Just PatOAbsurd -> p
  Just _          -> case p of
    (VarP _ x) -> VarP i x
    (DotP _ u) -> DotP i u
    (ConP c (ConPatternInfo _ r ft b l) ps)
      -> ConP c (ConPatternInfo i r ft b l) ps
    DefP _ q ps -> DefP i q ps
    (LitP _ l) -> LitP i l
    ProjP{} -> __IMPOSSIBLE__
    (IApplyP _ t u x) -> IApplyP i t u x

instance Subst DeBruijnPattern DeBruijnPattern where
  applySubst IdS p = p
  applySubst rho p = case p of
    VarP i x     ->
      usePatternInfo i $
      useName (dbPatVarName x) $
      lookupS rho $ dbPatVarIndex x
    DotP i u     -> DotP i $ applyPatSubst rho u
    ConP c ci ps -> ConP c ci $ applySubst rho ps
    DefP i q ps  -> DefP i q $ applySubst rho ps
    LitP i x     -> p
    ProjP{}      -> p
    IApplyP i t u x -> case useName (dbPatVarName x) $ lookupS rho $ dbPatVarIndex x of
                        IApplyP _ _ _ y -> IApplyP i (applyPatSubst rho t) (applyPatSubst rho u) y
                        VarP  _ y -> IApplyP i (applyPatSubst rho t) (applyPatSubst rho u) y
                        _ -> __IMPOSSIBLE__
    where
      useName :: PatVarName -> DeBruijnPattern -> DeBruijnPattern
      useName n (VarP o x)
        | isUnderscore (dbPatVarName x)
        = VarP o $ x { dbPatVarName = n }
      useName _ x = x

instance Subst Term Range where
  applySubst _ = id

---------------------------------------------------------------------------
-- * Projections
---------------------------------------------------------------------------

-- | @projDropParsApply proj o args = 'projDropPars' proj o `'apply'` args@
--
--   This function is an optimization, saving us from construction lambdas we
--   immediately remove through application.
projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term
projDropParsApply (Projection prop d r _ lams) o rel args =
  case initLast $ getProjLams lams of
    -- If we have no more abstractions, we must be a record field
    -- (projection applied already to record value).
    Nothing -> if proper then Def d $ map Apply args else __IMPOSSIBLE__
    Just (pars, Arg i y) ->
      let irr = isIrrelevant rel
          core
            | proper && not irr = Lam i $ Abs y $ Var 0 [Proj o d]
            | otherwise         = Lam i $ Abs y $ Def d [Apply $ Var 0 [] <$ r]
            -- Issue2226: get ArgInfo for principal argument from projFromType
      -- Now drop pars many args
          (pars', args') = dropCommon pars args
      -- We only have to abstract over the parameters that exceed the arguments.
      -- We only have to apply to the arguments that exceed the parameters.
      in List.foldr (\ (Arg ai x) -> Lam ai . NoAbs x) (core `apply` args') pars'
  where proper = isJust prop

---------------------------------------------------------------------------
-- * Telescopes
---------------------------------------------------------------------------

-- ** Telescope view of a type

type TelView = TelV Type
data TelV a  = TelV { theTel :: Tele (Dom a), theCore :: a }
  deriving (Show, Functor)

deriving instance (Subst Term a, Eq  a) => Eq  (TelV a)
deriving instance (Subst Term a, Ord a) => Ord (TelV a)

-- | Takes off all exposed function domains from the given type.
--   This means that it does not reduce to expose @Pi@-types.
telView' :: Type -> TelView
telView' = telView'UpTo (-1)

-- | @telView'UpTo n t@ takes off the first @n@ exposed function types of @t@.
-- Takes off all (exposed ones) if @n < 0@.
telView'UpTo :: Int -> Type -> TelView
telView'UpTo 0 t = TelV EmptyTel t
telView'UpTo n t = case unEl t of
  Pi a b  -> absV a (absName b) $ telView'UpTo (n - 1) (absBody b)
  _       -> TelV EmptyTel t
  where
    absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t


-- ** Creating telescopes from lists of types

-- | Turn a typed binding @(x1 .. xn : A)@ into a telescope.
bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' f []     t = []
bindsToTel' f (x:xs) t = fmap (f x,) t : bindsToTel' f xs (raise 1 t)

bindsToTel :: [Name] -> Dom Type -> ListTel
bindsToTel = bindsToTel' nameToArgName

-- | Turn a typed binding @(x1 .. xn : A)@ into a telescope.
namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
namedBindsToTel []       t = EmptyTel
namedBindsToTel (x : xs) t =
  ExtendTel (t <$ domFromNamedArgName x) $ Abs (nameToArgName $ namedArg x) $ namedBindsToTel xs (raise 1 t)

domFromNamedArgName :: NamedArg Name -> Dom ()
domFromNamedArgName x = () <$ domFromNamedArg (fmap forceName x)
  where
    -- If no explicit name is given we use the bound name for the label.
    forceName (Named Nothing x) = Named (Just $ WithOrigin Inserted $ Ranged (getRange x) $ nameToArgName x) x
    forceName x = x

-- ** Abstracting in terms and types

-- | @mkPi dom t = telePi (telFromList [dom]) t@
mkPi :: Dom (ArgName, Type) -> Type -> Type
mkPi !dom b = el $ Pi a (mkAbs x b)
  where
    x = fst $ unDom dom
    a = snd <$> dom
    el = El $ piSort a (Abs x (getSort b)) -- piSort checks x freeIn

mkLam :: Arg ArgName -> Term -> Term
mkLam a v = Lam (argInfo a) (Abs (unArg a) v)

telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
telePi' reAbs = telePi where
  telePi EmptyTel          t = t
  telePi (ExtendTel u tel) t = el $ Pi u $ reAbs b
    where
      b  = (`telePi` t) <$> tel
      el = El $ piSort u (getSort <$> b)

-- | Uses free variable analysis to introduce 'NoAbs' bindings.
telePi :: Telescope -> Type -> Type
telePi = telePi' reAbs

-- | Everything will be an 'Abs'.
telePi_ :: Telescope -> Type -> Type
telePi_ = telePi' id

-- | Only abstract the visible components of the telescope,
--   and all that bind variables.  Everything will be an 'Abs'!
-- Caution: quadratic time!

telePiVisible :: Telescope -> Type -> Type
telePiVisible EmptyTel t = t
telePiVisible (ExtendTel u tel) t
    -- If u is not declared visible and b can be strengthened, skip quantification of u.
    | notVisible u, NoAbs x t' <- b' = t'
    -- Otherwise, include quantification over u.
    | otherwise = El (piSort u $ getSort <$> b) $ Pi u b
  where
    b  = tel <&> (`telePiVisible` t)
    b' = reAbs b

-- | Abstract over a telescope in a term, producing lambdas.
--   Dumb abstraction: Always produces 'Abs', never 'NoAbs'.
--
--   The implementation is sound because 'Telescope' does not use 'NoAbs'.
teleLam :: Telescope -> Term -> Term
teleLam  EmptyTel         t = t
teleLam (ExtendTel u tel) t = Lam (domInfo u) $ flip teleLam t <$> tel

-- | Performs void ('noAbs') abstraction over telescope.
class TeleNoAbs a where
  teleNoAbs :: a -> Term -> Term

instance TeleNoAbs ListTel where
  teleNoAbs tel t = foldr (\ Dom{domInfo = ai, unDom = (x, _)} -> Lam ai . NoAbs x) t tel

instance TeleNoAbs Telescope where
  teleNoAbs tel = teleNoAbs $ telToList tel


-- ** Telescope typing

-- | Given arguments @vs : tel@ (vector typing), extract their individual types.
--   Returns @Nothing@ is @tel@ is not long enough.

typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
typeArgsWithTel _ []                         = return []
typeArgsWithTel (ExtendTel dom tel) (v : vs) = (dom :) <$> typeArgsWithTel (absApp tel v) vs
typeArgsWithTel EmptyTel{} (_:_)             = Nothing

---------------------------------------------------------------------------
-- * Clauses
---------------------------------------------------------------------------

-- | In compiled clauses, the variables in the clause body are relative to the
--   pattern variables (including dot patterns) instead of the clause telescope.
compiledClauseBody :: Clause -> Maybe Term
compiledClauseBody cl = applySubst (renamingR perm) $ clauseBody cl
  where perm = fromMaybe __IMPOSSIBLE__ $ clausePerm cl

---------------------------------------------------------------------------
-- * Syntactic equality and order
--
-- Needs weakening.
---------------------------------------------------------------------------

deriving instance Eq Substitution
deriving instance Ord Substitution

deriving instance Eq Sort
deriving instance Ord Sort
deriving instance Eq Level
deriving instance Ord Level
deriving instance Eq PlusLevel
deriving instance Eq NotBlocked
deriving instance Eq t => Eq (Blocked t)
deriving instance Eq Candidate

deriving instance (Subst t a, Eq a)  => Eq  (Tele a)
deriving instance (Subst t a, Ord a) => Ord (Tele a)

-- Andreas, 2019-11-16, issue #4201: to avoid potential unintended
-- performance loss, the Eq instance for Constraint is disabled:
--
-- -- deriving instance Eq Constraint
--
-- I am tempted to write
--
--   instance Eq Constraint where (==) = undefined
--
-- but this does not give a compilation error anymore when trying
-- to use equality on constraints.
-- Therefore, I hope this comment is sufficient to prevent a resurrection
-- of the Eq instance for Constraint.

deriving instance Eq CompareAs
deriving instance Eq Section

instance Ord PlusLevel where
  -- Compare on the atom first. Makes most sense for levelMax.
  compare (Plus n a) (Plus m b) = compare (a,n) (b,m)

instance Eq LevelAtom where
  (==) = (==) `on` unLevelAtom

instance Ord LevelAtom where
  compare = compare `on` unLevelAtom

-- | Syntactic 'Type' equality, ignores sort annotations.
instance Eq a => Eq (Type' a) where
  (==) = (==) `on` unEl

instance Ord a => Ord (Type' a) where
  compare = compare `on` unEl

-- | Syntactic 'Term' equality, ignores stuff below @DontCare@ and sharing.
instance Eq Term where
  Var x vs   == Var x' vs'   = x == x' && vs == vs'
  Lam h v    == Lam h' v'    = h == h' && v  == v'
  Lit l      == Lit l'       = l == l'
  Def x vs   == Def x' vs'   = x == x' && vs == vs'
  Con x _ vs == Con x' _ vs' = x == x' && vs == vs'
  Pi a b     == Pi a' b'     = a == a' && b == b'
  Sort s     == Sort s'      = s == s'
  Level l    == Level l'     = l == l'
  MetaV m vs == MetaV m' vs' = m == m' && vs == vs'
  DontCare _ == DontCare _   = True
  Dummy{}    == Dummy{}      = True
  _          == _            = False

instance Eq a => Eq (Pattern' a) where
  VarP _ x        == VarP _ y          = x == y
  DotP _ u        == DotP _ v          = u == v
  ConP c _ ps     == ConP c' _ qs      = c == c && ps == qs
  LitP _ l        == LitP _ l'         = l == l'
  ProjP _ f       == ProjP _ g         = f == g
  IApplyP _ u v x == IApplyP _ u' v' y = u == u' && v == v' && x == y
  DefP _ f ps     == DefP _ g qs       = f == g && ps == qs
  _               == _                 = False

instance Ord Term where
  Var a b    `compare` Var x y    = compare x a `thenCmp` compare b y -- sort de Bruijn indices down (#2765)
  Var{}      `compare` _          = LT
  _          `compare` Var{}      = GT
  Def a b    `compare` Def x y    = compare (a, b) (x, y)
  Def{}      `compare` _          = LT
  _          `compare` Def{}      = GT
  Con a _ b  `compare` Con x _ y  = compare (a, b) (x, y)
  Con{}      `compare` _          = LT
  _          `compare` Con{}      = GT
  Lit a      `compare` Lit x      = compare a x
  Lit{}      `compare` _          = LT
  _          `compare` Lit{}      = GT
  Lam a b    `compare` Lam x y    = compare (a, b) (x, y)
  Lam{}      `compare` _          = LT
  _          `compare` Lam{}      = GT
  Pi a b     `compare` Pi x y     = compare (a, b) (x, y)
  Pi{}       `compare` _          = LT
  _          `compare` Pi{}       = GT
  Sort a     `compare` Sort x     = compare a x
  Sort{}     `compare` _          = LT
  _          `compare` Sort{}     = GT
  Level a    `compare` Level x    = compare a x
  Level{}    `compare` _          = LT
  _          `compare` Level{}    = GT
  MetaV a b  `compare` MetaV x y  = compare (a, b) (x, y)
  MetaV{}    `compare` _          = LT
  _          `compare` MetaV{}    = GT
  DontCare{} `compare` DontCare{} = EQ
  DontCare{} `compare` _          = LT
  _          `compare` DontCare{} = GT
  Dummy{}    `compare` Dummy{}    = EQ

-- Andreas, 2017-10-04, issue #2775, ignore irrelevant arguments during with-abstraction.
--
-- For reasons beyond my comprehension, the following Eq instances are not employed
-- by with-abstraction in TypeChecking.Abstract.isPrefixOf.
-- Instead, I modified the general Eq instance for Arg to ignore the argument
-- if irrelevant.

-- -- | Ignore irrelevant arguments in equality check.
-- --   Also ignore origin.
-- instance {-# OVERLAPPING #-} Eq (Arg Term) where
--   a@(Arg (ArgInfo h r _o) t) == a'@(Arg (ArgInfo h' r' _o') t') = trace ("Eq (Arg Term) on " ++ show a ++ " and " ++ show a') $
--     h == h' && ((r == Irrelevant) || (r' == Irrelevant) || (t == t'))
--     -- Andreas, 2017-10-04: According to Syntax.Common, equality on Arg ignores Relevance and Origin.

-- instance {-# OVERLAPPING #-} Eq Args where
--   us == vs = length us == length vs && and (zipWith (==) us vs)

-- instance {-# OVERLAPPING #-} Eq Elims where
--   us == vs = length us == length vs && and (zipWith (==) us vs)

-- | Equality of binders relies on weakening
--   which is a special case of renaming
--   which is a special case of substitution.
instance (Subst t a, Eq a) => Eq (Abs a) where
  NoAbs _ a == NoAbs _ b = a == b  -- no need to raise if both are NoAbs
  a         == b         = absBody a == absBody b

instance (Subst t a, Ord a) => Ord (Abs a) where
  NoAbs _ a `compare` NoAbs _ b = a `compare` b  -- no need to raise if both are NoAbs
  a         `compare` b         = absBody a `compare` absBody b

deriving instance Ord a => Ord (Dom a)

instance (Subst t a, Eq a)  => Eq  (Elim' a) where
  Apply  a == Apply  b = a == b
  Proj _ x == Proj _ y = x == y
  IApply x y r == IApply x' y' r' = x == x' && y == y' && r == r'
  _ == _ = False

instance (Subst t a, Ord a) => Ord (Elim' a) where
  Apply  a `compare` Apply  b = a `compare` b
  Proj _ x `compare` Proj _ y = x `compare` y
  IApply x y r `compare` IApply x' y' r' = compare x x' `mappend` compare y y' `mappend` compare r r'
  Apply{}  `compare` _        = LT
  _        `compare` Apply{}  = GT
  Proj{}   `compare` _        = LT
  _        `compare` Proj{}   = GT


---------------------------------------------------------------------------
-- * Sort stuff
---------------------------------------------------------------------------

-- | @univSort' univInf s@ gets the next higher sort of @s@, if it is
--   known (i.e. it is not just @UnivSort s@). @univInf@ is returned
--   as the sort of @Inf@.
--
--   Precondition: @s@ is reduced
univSort' :: Maybe Sort -> Sort -> Maybe Sort
univSort' univInf (Type l) = Just $ Type $ levelSuc l
univSort' univInf (Prop l) = Just $ Type $ levelSuc l
univSort' univInf Inf      = univInf
univSort' univInf s        = Nothing

univSort :: Maybe Sort -> Sort -> Sort
univSort univInf s = fromMaybe (UnivSort s) $ univSort' univInf s

univInf :: (HasOptions m) => m (Maybe Sort)
univInf =
  ifM ((optOmegaInOmega <$> pragmaOptions) `or2M` typeInType)
  {-then-} (return $ Just Inf)
  {-else-} (return Nothing)

-- | Compute the sort of a function type from the sorts of its
--   domain and codomain.
funSort' :: Sort -> Sort -> Maybe Sort
funSort' a b = case (a, b) of
  (Inf           , _            ) -> Just Inf
  (_             , Inf          ) -> Just Inf
  (Type a , Type b) -> Just $ Type $ levelLub a b
  (SizeUniv      , b            ) -> Just b
  (_             , SizeUniv     ) -> Just SizeUniv
  (Prop a , Type b) -> Just $ Type $ levelLub a b
  (Type a , Prop b) -> Just $ Prop $ levelLub a b
  (Prop a , Prop b) -> Just $ Prop $ levelLub a b
  (a             , b            ) -> Nothing

funSort :: Sort -> Sort -> Sort
funSort a b = fromMaybe (FunSort a b) $ funSort' a b

-- | Compute the sort of a pi type from the sorts of its domain
--   and codomain.
piSort' :: Dom Type -> Abs Sort -> Maybe Sort
piSort' a      (NoAbs _ b) = funSort' (getSort a) b
piSort' a bAbs@(Abs   _ b) = case flexRigOccurrenceIn 0 b of
  Nothing -> Just $ funSort (getSort a) $ noabsApp __IMPOSSIBLE__ bAbs
  Just o -> case o of
    StronglyRigid -> Just Inf
    Unguarded     -> Just Inf
    WeaklyRigid   -> Just Inf
    Flexible _    -> Nothing
-- Andreas, 2019-06-20
-- KEEP the following commented out code for the sake of the discussion on irrelevance.
-- piSort' a bAbs@(Abs   _ b) = case occurrence 0 b of
--     -- Andreas, Jesper, AIM XXIX, 2019-03-18, issue #3631
--     -- Remember the NoAbs here!
--     NoOccurrence  -> Just $ funSort a $ noabsApp __IMPOSSIBLE__ bAbs
--     -- Andreas, 2017-01-18, issue #2408:
--     -- The sort of @.(a : A) → Set (f a)@ in context @f : .A → Level@
--     -- is @dLub Set λ a → Set (lsuc (f a))@, but @DLub@s are not serialized.
--     -- Alternatives:
--     -- 1. -- Irrelevantly -> sLub s1 (absApp b $ DontCare $ Sort Prop)
--     --    We cheat here by simplifying the sort to @Set (lsuc (f *))@
--     --    where * is a dummy value.  The rationale is that @f * = f a@ (irrelevance!)
--     --    and that if we already have a neutral level @f a@
--     --    it should not hurt to have @f *@ even if type @A@ is empty.
--     --    However: sorts are printed in error messages when sorts do not match.
--     --    Also, sorts with a dummy like Prop would be ill-typed.
--     -- 2. We keep the DLub, and serialize it.
--     --    That's clean and principled, even though DLubs make level solving harder.
--     -- Jesper, 2018-04-20: another alternative:
--     -- 3. Return @Inf@ as in the relevant case. This is conservative and might result
--     --    in more occurrences of @Setω@ than desired, but at least it doesn't pollute
--     --    the sort system with new 'exotic' sorts.
--     Irrelevantly  -> Just Inf
--     StronglyRigid -> Just Inf
--     Unguarded     -> Just Inf
--     WeaklyRigid   -> Just Inf
--     Flexible _    -> Nothing

piSort :: Dom Type -> Abs Sort -> Sort
piSort a b = case piSort' a b of
  Just s -> s
  Nothing | NoAbs _ b' <- b -> FunSort (getSort a) b'
          | otherwise       -> PiSort a b

---------------------------------------------------------------------------
-- * Level stuff
---------------------------------------------------------------------------

-- ^ Computes @n0 ⊔ a₁ ⊔ a₂ ⊔ ... ⊔ aₙ@ and return its canonical form.
levelMax :: Integer -> [PlusLevel] -> Level
levelMax n0 as0 = Max n as
  where
    -- step 1: flatten nested @Level@ expressions in @LevelAtom@s
    Max n1 as1 = expandLevel $ Max n0 as0
    -- step 2: remove subsumed @PlusLevel@s
    as2       = removeSubsumed as1
    -- step 3: sort remaining @PlusLevel@s
    as        = List.sort as2
    -- step 4: set constant to 0 if it is subsumed by one of the @PlusLevel@s
    greatestB = Prelude.maximum $ 0 : [ n | Plus n _ <- as ]
    n | n1 > greatestB = n1
      | otherwise      = 0

    lmax :: Integer -> [PlusLevel] -> [Level] -> Level
    lmax m as []              = Max m as
    lmax m as (Max n bs : ls) = lmax (max m n) (bs ++ as) ls

    expandLevel :: Level -> Level
    expandLevel (Max m as) = lmax m [] $ map expandPlus as

    expandPlus :: PlusLevel -> Level
    expandPlus (Plus m l) = levelPlus m $ expandAtom l

    expandAtom :: LevelAtom -> Level
    expandAtom l = case l of
      BlockedLevel _ v -> expandTm v
      NeutralLevel _ v -> expandTm v
      UnreducedLevel v -> expandTm v
      MetaLevel{}      -> Max 0 [Plus 0 l]
      where
        expandTm (Level l)       = expandLevel l
        expandTm (Sort (Type l)) = expandLevel l -- TODO: get rid of this horrible hack!
        expandTm v               = Max 0 [Plus 0 l]

    removeSubsumed [] = []
    removeSubsumed (Plus n a : bs)
      | not $ null ns = removeSubsumed bs
      | otherwise     = Plus n a : removeSubsumed [ b | b@(Plus _ a') <- bs, a /= a' ]
      where
        ns = [ m | Plus m a' <- bs, a == a', m > n ]

-- | Given two levels @a@ and @b@, compute @a ⊔ b@ and return its
--   canonical form.
levelLub :: Level -> Level -> Level
levelLub (Max m as) (Max n bs) = levelMax (max m n) $ as ++ bs

levelTm :: Level -> Term
levelTm l =
  case l of
    Max 0 [Plus 0 l] -> unLevelAtom l
    _                -> Level l

unLevelAtom :: LevelAtom -> Term
unLevelAtom (MetaLevel x es)   = MetaV x es
unLevelAtom (NeutralLevel _ v) = v
unLevelAtom (UnreducedLevel v) = v
unLevelAtom (BlockedLevel _ v) = v