{-# LANGUAGE CPP                      #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE UndecidableInstances     #-}

module Agda.TypeChecking.Reduce where

import Prelude hiding (mapM)
import Control.Monad.Reader hiding (mapM)

import qualified Data.List as List
import Data.List ((\\))
import Data.Maybe
import Data.Map (Map)
import Data.Monoid
import Data.Traversable
import Data.Hashable

import Agda.Interaction.Options

import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Scope.Base (Scope)
import Agda.Syntax.Literal

import Agda.TypeChecking.Monad hiding ( underAbstraction_, enterClosure, isInstantiatedMeta
                                      , getConstInfo
                                      , lookupMeta )
import qualified Agda.TypeChecking.Monad as TCM
import Agda.TypeChecking.Monad.Builtin hiding (getPrimitive, constructorForm)
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.EtaContract

import Agda.TypeChecking.Reduce.Monad

import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Match
import {-# SOURCE #-} Agda.TypeChecking.Patterns.Match
import {-# SOURCE #-} Agda.TypeChecking.Pretty
import {-# SOURCE #-} Agda.TypeChecking.Rewriting
import {-# SOURCE #-} Agda.TypeChecking.Reduce.Fast

import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.HashMap (HashMap)
import Agda.Utils.Size
import Agda.Utils.Tuple

#include "undefined.h"
import Agda.Utils.Impossible

instantiate :: (Instantiate a, MonadReduce m) => a -> m a
instantiate = liftReduce . instantiate'

instantiateFull :: (InstantiateFull a, MonadReduce m) => a -> m a
instantiateFull = liftReduce . instantiateFull'

reduce :: (Reduce a, MonadReduce m) => a -> m a
reduce = liftReduce . reduce'

reduceB :: (Reduce a, MonadReduce m) => a -> m (Blocked a)
reduceB = liftReduce . reduceB'

normalise :: (Normalise a, MonadReduce m) => a -> m a
normalise = liftReduce . normalise'

-- | Normalise the given term but also preserve blocking tags
--   TODO: implement a more efficient version of this.
normaliseB :: (MonadReduce m, Reduce t, Normalise t) => t -> m (Blocked t)
normaliseB = normalise >=> reduceB

simplify :: (Simplify a, MonadReduce m) => a -> m a
simplify = liftReduce . simplify'

-- | Meaning no metas left in the instantiation.
isFullyInstantiatedMeta :: MetaId -> TCM Bool
isFullyInstantiatedMeta m = do
  mv <- TCM.lookupMeta m
  case mvInstantiation mv of
    InstV _tel v -> noMetas <$> instantiateFull v
    _ -> return False

-- | Instantiate something.
--   Results in an open meta variable or a non meta.
--   Doesn't do any reduction, and preserves blocking tags (when blocking meta
--   is uninstantiated).
class Instantiate t where
    instantiate' :: t -> ReduceM t

instance Instantiate Term where
  instantiate' t@(MetaV x es) = do
    mi <- mvInstantiation <$> lookupMeta x
    case mi of
      InstV tel v -> instantiate' inst
        where
          -- A slight complication here is that the meta might be underapplied,
          -- in which case we have to build the lambda abstraction before
          -- applying the substitution, or overapplied in which case we need to
          -- fall back to applyE.
          (es1, es2) = splitAt (length tel) es
          vs1 = reverse $ map unArg $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es1
          rho = vs1 ++# wkS (length vs1) idS
                -- really should be .. ++# emptyS but using wkS makes it reduce to idS
                -- when applicable
          -- specification: inst == foldr mkLam v tel `applyE` es
          inst = applySubst rho (foldr mkLam v $ drop (length es1) tel) `applyE` es2
      Open                             -> return t
      OpenInstance                     -> return t
      BlockedConst _                   -> return t
      PostponedTypeCheckingProblem _ _ -> return t
  instantiate' (Level l) = levelTm <$> instantiate' l
  instantiate' (Sort s) = Sort <$> instantiate' s
  instantiate' t = return t

instance Instantiate Level where
  instantiate' (Max as) = levelMax <$> instantiate' as

instance Instantiate PlusLevel where
  instantiate' l@ClosedLevel{} = return l
  instantiate' (Plus n a) = Plus n <$> instantiate' a

instance Instantiate LevelAtom where
  instantiate' l = case l of
    MetaLevel m vs -> do
      v <- instantiate' (MetaV m vs)
      case v of
        MetaV m vs -> return $ MetaLevel m vs
        _          -> return $ UnreducedLevel v
    UnreducedLevel l -> UnreducedLevel <$> instantiate' l
    _ -> return l

instance Instantiate a => Instantiate (Blocked a) where
  instantiate' v@NotBlocked{} = return v
  instantiate' v@(Blocked x u) = do
    mi <- mvInstantiation <$> lookupMeta x
    case mi of
      InstV{}                        -> notBlocked <$> instantiate' u
      Open                           -> return v
      OpenInstance                   -> return v
      BlockedConst{}                 -> return v
      PostponedTypeCheckingProblem{} -> return v

instance Instantiate Type where
    instantiate' (El s t) = El <$> instantiate' s <*> instantiate' t

instance Instantiate Sort where
  instantiate' s = case s of
    MetaS x es -> instantiate' (MetaV x es) >>= \case
      Sort s'      -> return s'
      MetaV x' es' -> return $ MetaS x' es'
      Def d es'     -> return $ DefS d es'
      _            -> __IMPOSSIBLE__
    _ -> return s

instance Instantiate Elim where
  instantiate' (Apply v) = Apply <$> instantiate' v
  instantiate' (Proj o f)= pure $ Proj o f
  instantiate' (IApply x y v) = IApply <$> instantiate' x <*> instantiate' y <*> instantiate' v

instance Instantiate t => Instantiate (Abs t) where
  instantiate' = traverse instantiate'

instance Instantiate t => Instantiate (Arg t) where
    instantiate' = traverse instantiate'

instance Instantiate t => Instantiate (Dom t) where
    instantiate' = traverse instantiate'

instance Instantiate t => Instantiate (Maybe t) where
  instantiate' = traverse instantiate'

instance Instantiate t => Instantiate [t] where
    instantiate' = traverse instantiate'

instance (Instantiate a, Instantiate b) => Instantiate (a,b) where
    instantiate' (x,y) = (,) <$> instantiate' x <*> instantiate' y


instance (Instantiate a, Instantiate b,Instantiate c) => Instantiate (a,b,c) where
    instantiate' (x,y,z) = (,,) <$> instantiate' x <*> instantiate' y <*> instantiate' z

instance Instantiate a => Instantiate (Closure a) where
    instantiate' cl = do
        x <- enterClosure cl instantiate'
        return $ cl { clValue = x }

instance Instantiate Telescope where
  instantiate' EmptyTel = return EmptyTel
  instantiate' (ExtendTel a tel) = ExtendTel <$> instantiate' a <*> instantiate' tel
--instantiate' tel = return tel

instance Instantiate Constraint where
  instantiate' (ValueCmp cmp t u v) = do
    (t,u,v) <- instantiate' (t,u,v)
    return $ ValueCmp cmp t u v
  instantiate' (ValueCmpOnFace cmp p t u v) = do
    ((p,t),u,v) <- instantiate' ((p,t),u,v)
    return $ ValueCmpOnFace cmp p t u v
  instantiate' (ElimCmp cmp fs t v as bs) =
    ElimCmp cmp fs <$> instantiate' t <*> instantiate' v <*> instantiate' as <*> instantiate' bs
  instantiate' (LevelCmp cmp u v)   = uncurry (LevelCmp cmp) <$> instantiate' (u,v)
  instantiate' (TypeCmp cmp a b)    = uncurry (TypeCmp cmp) <$> instantiate' (a,b)
  instantiate' (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp)  <$> instantiate' (tela,telb)
  instantiate' (SortCmp cmp a b)    = uncurry (SortCmp cmp) <$> instantiate' (a,b)
  instantiate' (Guarded c pid)      = Guarded <$> instantiate' c <*> pure pid
  instantiate' (UnBlock m)          = return $ UnBlock m
  instantiate' (FindInstance m b args) = FindInstance m b <$> mapM instantiate' args
  instantiate' (IsEmpty r t)        = IsEmpty r <$> instantiate' t
  instantiate' (CheckSizeLtSat t)   = CheckSizeLtSat <$> instantiate' t
  instantiate' c@CheckFunDef{}      = return c
  instantiate' (HasBiggerSort a)    = HasBiggerSort <$> instantiate' a
  instantiate' (HasPTSRule a b)     = uncurry HasPTSRule <$> instantiate' (a,b)
  instantiate' (UnquoteTactic m t h g) = UnquoteTactic m <$> instantiate' t <*> instantiate' h <*> instantiate' g

instance Instantiate e => Instantiate (Map k e) where
    instantiate' = traverse instantiate'

instance Instantiate Candidate where
  instantiate' (Candidate u t ov) = Candidate <$> instantiate' u <*> instantiate' t <*> pure ov

instance Instantiate EqualityView where
  instantiate' (OtherType t)            = OtherType
    <$> instantiate' t
  instantiate' (EqualityType s eq l t a b) = EqualityType
    <$> instantiate' s
    <*> return eq
    <*> mapM instantiate' l
    <*> instantiate' t
    <*> instantiate' a
    <*> instantiate' b

---------------------------------------------------------------------------
-- * Reduction to weak head normal form.
---------------------------------------------------------------------------

-- | Case on whether a term is blocked on a meta (or is a meta).
--   That means it can change its shape when the meta is instantiated.
ifBlocked :: (MonadReduce m) =>  Term -> (MetaId -> Term -> m a) -> (NotBlocked -> Term -> m a) -> m a
ifBlocked t blocked unblocked = do
  t <- reduceB t
  case t of
    Blocked m _              -> blocked m (ignoreBlocking t)
    NotBlocked _ (MetaV m _) -> blocked m (ignoreBlocking t)
    NotBlocked nb _          -> unblocked nb (ignoreBlocking t)

isBlocked :: MonadReduce m => Term -> m (Maybe MetaId)
isBlocked t = ifBlocked t (\m _ -> return $ Just m) (\_ _ -> return Nothing)

-- | Case on whether a type is blocked on a meta (or is a meta).
ifBlockedType :: MonadReduce m => Type -> (MetaId -> Type -> m a) -> (NotBlocked -> Type -> m a) -> m a
ifBlockedType (El s t) blocked unblocked =
  ifBlocked t (\ m v -> blocked m $ El s v) (\ nb v -> unblocked nb $ El s v)

isBlockedType :: MonadReduce m => Type -> m (Maybe MetaId)
isBlockedType t = ifBlockedType t (\m _ -> return $ Just m) (\_ _ -> return Nothing)

class Reduce t where
    reduce'  :: t -> ReduceM t
    reduceB' :: t -> ReduceM (Blocked t)

    reduce'  t = ignoreBlocking <$> reduceB' t
    reduceB' t = notBlocked <$> reduce' t

instance Reduce Type where
    reduce'  (El s t) = El s <$> reduce' t
    reduceB' (El s t) = fmap (El s) <$> reduceB' t

instance Reduce Sort where
    reduce' s = do
      s <- instantiate' s
      case s of
        PiSort s1 s2 -> do
          (s1,s2) <- reduce' (s1,s2)
          maybe (return $ PiSort s1 s2) reduce' $ piSort' s1 s2
        UnivSort s' -> do
          s' <- reduce' s'
          ui <- univInf
          caseMaybe (univSort' ui s') (return $ UnivSort s') reduce'
        Prop s'    -> Prop <$> reduce' s'
        Type s'    -> Type <$> reduce' s'
        Inf        -> return Inf
        SizeUniv   -> return SizeUniv
        MetaS x es -> return s
        DefS d es  -> return s -- postulated sorts do not reduce
        DummyS{}   -> return s

instance Reduce Elim where
  reduce' (Apply v) = Apply <$> reduce' v
  reduce' (Proj o f)= pure $ Proj o f
  reduce' (IApply x y v) = IApply <$> reduce' x <*> reduce' y <*> reduce' v

instance Reduce Level where
  reduce'  (Max as) = levelMax <$> mapM reduce' as
  reduceB' (Max as) = fmap levelMax . traverse id <$> traverse reduceB' as

instance Reduce PlusLevel where
  reduceB' l@ClosedLevel{} = return $ notBlocked l
  reduceB' (Plus n l) = fmap (Plus n) <$> reduceB' l

instance Reduce LevelAtom where
  reduceB' l = case l of
    MetaLevel m vs   -> fromTm (MetaV m vs)
    NeutralLevel r v -> return $ NotBlocked r $ NeutralLevel r v
    BlockedLevel m v ->
      ifM (isInstantiatedMeta m) (fromTm v) (return $ Blocked m $ BlockedLevel m v)
    UnreducedLevel v -> fromTm v
    where
      fromTm v = do
        bv <- reduceB' v
        let v = ignoreBlocking bv
        case bv of
          NotBlocked r (MetaV m vs) -> return $ NotBlocked r $ MetaLevel m vs
          Blocked m _               -> return $ Blocked m    $ BlockedLevel m v
          NotBlocked r _            -> return $ NotBlocked r $ NeutralLevel r v


instance (Subst t a, Reduce a) => Reduce (Abs a) where
  reduce' b@(Abs x _) = Abs x <$> underAbstraction_ b reduce'
  reduce' (NoAbs x v) = NoAbs x <$> reduce' v

-- Lists are never blocked
instance Reduce t => Reduce [t] where
    reduce' = traverse reduce'

instance Reduce t => Reduce (Arg t) where
    reduce' a = case getRelevance a of
      Irrelevant -> return a             -- Don't reduce' irr. args!?
                                         -- Andreas, 2018-03-03, caused #2989.
      _          -> traverse reduce' a

    reduceB' t = traverse id <$> traverse reduceB' t

instance Reduce t => Reduce (Dom t) where
    reduce' = traverse reduce'
    reduceB' t = traverse id <$> traverse reduceB' t

instance (Reduce a, Reduce b) => Reduce (a,b) where
    reduce' (x,y)  = (,) <$> reduce' x <*> reduce' y
    reduceB' (x,y) = do
      x <- reduceB' x
      y <- reduceB' y
      let blk = void x `mappend` void y
          xy  = (ignoreBlocking x , ignoreBlocking y)
      return $ blk $> xy

instance (Reduce a, Reduce b,Reduce c) => Reduce (a,b,c) where
    reduce' (x,y,z) = (,,) <$> reduce' x <*> reduce' y <*> reduce' z
    reduceB' (x,y,z) = do
      x <- reduceB' x
      y <- reduceB' y
      z <- reduceB' z
      let blk = void x `mappend` void y `mappend` void z
          xyz = (ignoreBlocking x , ignoreBlocking y , ignoreBlocking z)
      return $ blk $> xyz

reduceIApply :: ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term)
reduceIApply = reduceIApply' reduceB'

blockedOrMeta :: Blocked Term -> Blocked ()
blockedOrMeta r =
  case r of
    Blocked m _              -> Blocked m ()
    NotBlocked _ (MetaV m _) -> Blocked m ()
    NotBlocked i _           -> NotBlocked i ()

reduceIApply' :: (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term)
reduceIApply' reduceB' d (IApply x y r : es) = do
  view <- intervalView'
  r <- reduceB' r
  -- We need to propagate the blocking information so that e.g.
  -- we postpone "someNeutralPath ?0 = a" rather than fail.
  let blockedInfo = blockedOrMeta r

  case view (ignoreBlocking r) of
   IZero -> reduceB' (applyE x es)
   IOne  -> reduceB' (applyE y es)
   _     -> fmap (<* blockedInfo) (reduceIApply d es)
reduceIApply' reduceB' d (_ : es) = reduceIApply d es
reduceIApply' reduceB' d [] = d

instance Reduce Term where
  reduceB' = {-# SCC "reduce'<Term>" #-} maybeFastReduceTerm

shouldTryFastReduce :: ReduceM Bool
shouldTryFastReduce = (optFastReduce <$> pragmaOptions) `and2M` do
  allowed <- asksTC envAllowedReductions
  let optionalReductions = [NonTerminatingReductions, UnconfirmedReductions]
      requiredReductions = allReductions \\ optionalReductions
  return $ (allowed \\ optionalReductions) == requiredReductions

maybeFastReduceTerm :: Term -> ReduceM (Blocked Term)
maybeFastReduceTerm v = do
  let tryFast = case v of
                  Def{}   -> True
                  Con{}   -> True
                  MetaV{} -> True
                  _       -> False
  if not tryFast then slowReduceTerm v
                 else
    case v of
      MetaV x _ -> ifM (isOpen x) (return $ notBlocked v) (maybeFast v)
      _         -> maybeFast v
  where
    isOpen x = isOpenMeta . mvInstantiation <$> lookupMeta x
    maybeFast v = ifM shouldTryFastReduce (fastReduce v) (slowReduceTerm v)

slowReduceTerm :: Term -> ReduceM (Blocked Term)
slowReduceTerm v = do
    v <- instantiate' v
    let done = return $ notBlocked v
        iapp = reduceIApply done
    case v of
--    Andreas, 2012-11-05 not reducing meta args does not destroy anything
--    and seems to save 2% sec on the standard library
--      MetaV x args -> notBlocked . MetaV x <$> reduce' args
      MetaV x es -> iapp es
      Def f es   -> flip reduceIApply es $ unfoldDefinitionE False reduceB' (Def f []) f es
      Con c ci es -> do
          -- Constructors can reduce' when they come from an
          -- instantiated module.
          -- also reduce when they are path constructors
          v <- flip reduceIApply es
                 $ unfoldDefinitionE False reduceB' (Con c ci []) (conName c) es
          traverse reduceNat v
      Sort s   -> fmap Sort <$> reduceB' s
      Level l  -> ifM (elem LevelReductions <$> asksTC envAllowedReductions)
                    {- then -} (fmap levelTm <$> reduceB' l)
                    {- else -} done
      Pi _ _   -> done
      Lit _    -> done
      Var _ es  -> iapp es
      Lam _ _  -> done
      DontCare _ -> done
      Dummy{}    -> done
    where
      -- NOTE: reduceNat can traverse the entire term.
      reduceNat v@(Con c ci []) = do
        mz  <- getBuiltin' builtinZero
        case v of
          _ | Just v == mz  -> return $ Lit $ LitNat (getRange c) 0
          _                 -> return v
      reduceNat v@(Con c ci [Apply a]) | visible a && isRelevant a = do
        ms  <- getBuiltin' builtinSuc
        case v of
          _ | Just (Con c ci []) == ms -> inc <$> reduce' (unArg a)
          _                         -> return v
          where
            inc w = case w of
              Lit (LitNat r n) -> Lit (LitNat (fuseRange c r) $ n + 1)
              _                -> Con c ci [Apply $ defaultArg w]
      reduceNat v = return v

-- Andreas, 2013-03-20 recursive invokations of unfoldCorecursion
-- need also to instantiate metas, see Issue 826.
unfoldCorecursionE :: Elim -> ReduceM (Blocked Elim)
unfoldCorecursionE (Proj o p)           = notBlocked . Proj o <$> getOriginalProjection p
unfoldCorecursionE (Apply (Arg info v)) = fmap (Apply . Arg info) <$>
  unfoldCorecursion v
unfoldCorecursionE (IApply x y r) = do -- TODO check if this makes sense
   [x,y,r] <- mapM unfoldCorecursion [x,y,r]
   return $ IApply <$> x <*> y <*> r

unfoldCorecursion :: Term -> ReduceM (Blocked Term)
unfoldCorecursion v = do
  v <- instantiate' v
  case v of
    Def f es -> unfoldDefinitionE True unfoldCorecursion (Def f []) f es
    _ -> slowReduceTerm v

-- | If the first argument is 'True', then a single delayed clause may
-- be unfolded.
unfoldDefinition ::
  Bool -> (Term -> ReduceM (Blocked Term)) ->
  Term -> QName -> Args -> ReduceM (Blocked Term)
unfoldDefinition unfoldDelayed keepGoing v f args =
  unfoldDefinitionE unfoldDelayed keepGoing v f (map Apply args)

unfoldDefinitionE ::
  Bool -> (Term -> ReduceM (Blocked Term)) ->
  Term -> QName -> Elims -> ReduceM (Blocked Term)
unfoldDefinitionE unfoldDelayed keepGoing v f es = do
  r <- unfoldDefinitionStep unfoldDelayed v f es
  case r of
    NoReduction v    -> return v
    YesReduction _ v -> keepGoing v

unfoldDefinition' ::
  Bool -> (Simplification -> Term -> ReduceM (Simplification, Blocked Term)) ->
  Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term)
unfoldDefinition' unfoldDelayed keepGoing v0 f es = do
  r <- unfoldDefinitionStep unfoldDelayed v0 f es
  case r of
    NoReduction v       -> return (NoSimplification, v)
    YesReduction simp v -> keepGoing simp v

unfoldDefinitionStep :: Bool -> Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term)
unfoldDefinitionStep unfoldDelayed v0 f es =
  {-# SCC "reduceDef" #-} do
  info <- getConstInfo f
  rewr <- instantiateRewriteRules =<< getRewriteRulesFor f
  allowed <- asksTC envAllowedReductions
  let def = theDef info
      v   = v0 `applyE` es
      -- Non-terminating functions
      -- (i.e., those that failed the termination check)
      -- and delayed definitions
      -- are not unfolded unless explicitely permitted.
      dontUnfold =
        (defNonterminating info && notElem NonTerminatingReductions allowed)
        || (defTerminationUnconfirmed info && notElem UnconfirmedReductions allowed)
        || (defDelayed info == Delayed && not unfoldDelayed)
      copatterns =
        case def of
          Function{funCopatternLHS = b} -> b
          _                             -> False
  case def of
    Constructor{conSrcCon = c} ->
      noReduction $ notBlocked $ Con (c `withRangeOf` f) ConOSystem [] `applyE` es
    Primitive{primAbstr = ConcreteDef, primName = x, primClauses = cls} -> do
      pf <- fromMaybe __IMPOSSIBLE__ <$> getPrimitive' x
      if FunctionReductions `elem` allowed
        then reducePrimitive x v0 f es pf dontUnfold
                             cls (defCompiled info) rewr
        else noReduction $ notBlocked v
    _  -> do
      if (RecursiveReductions `elem` allowed) ||
         (isJust (isProjection_ def) && ProjectionReductions `elem` allowed) || -- includes projection-like
         (isInlineFun def && InlineReductions `elem` allowed) ||
         (definitelyNonRecursive_ def && copatterns && CopatternReductions `elem` allowed) ||
         (definitelyNonRecursive_ def && FunctionReductions `elem` allowed)
        then
          reduceNormalE v0 f (map notReduced es) dontUnfold
                       (defClauses info) (defCompiled info) rewr
        else noReduction $ notBlocked v  -- Andrea(s), 2014-12-05 OK?

  where
    noReduction    = return . NoReduction
    yesReduction s = return . YesReduction s
    reducePrimitive x v0 f es pf dontUnfold cls mcc rewr
      | length es < ar
                  = noReduction $ NotBlocked Underapplied $ v0 `applyE` es -- not fully applied
      | otherwise = {-# SCC "reducePrimitive" #-} do
          let (es1,es2) = splitAt ar es
              args1     = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es1
          r <- primFunImplementation pf args1 (length es2)
          case r of
            NoReduction args1' -> do
              let es1' = map (fmap Apply) args1'
              if null cls && null rewr then do
                noReduction $ applyE (Def f []) <$> do
                  traverse id $
                    map mredToBlocked es1' ++ map notBlocked es2
               else
                reduceNormalE v0 f (es1' ++ map notReduced es2) dontUnfold cls mcc rewr
            YesReduction simpl v -> yesReduction simpl $ v `applyE` es2
      where
          ar  = primFunArity pf
          mredToBlocked :: MaybeReduced a -> Blocked a
          mredToBlocked (MaybeRed NotReduced  x) = notBlocked x
          mredToBlocked (MaybeRed (Reduced b) x) = x <$ b

    reduceNormalE :: Term -> QName -> [MaybeReduced Elim] -> Bool -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> ReduceM (Reduced (Blocked Term) Term)
    reduceNormalE v0 f es dontUnfold def mcc rewr = {-# SCC "reduceNormal" #-} do
      case (def,rewr) of
        _ | dontUnfold -> defaultResult -- non-terminating or delayed
        ([],[])        -> defaultResult -- no definition for head
        (cls,rewr)     -> do
          ev <- appDefE_ f v0 cls mcc rewr es
          debugReduce ev
          return ev
      where
      defaultResult = noReduction $ NotBlocked ReallyNotBlocked vfull
      vfull         = v0 `applyE` map ignoreReduced es
      debugReduce ev = verboseS "tc.reduce" 90 $ do
        case ev of
          NoReduction v -> do
            reportSDoc "tc.reduce" 90 $ vcat
              [ "*** tried to reduce " <+> prettyTCM f
              , "    es =  " <+> sep (map (prettyTCM . ignoreReduced) es)
              -- , "*** tried to reduce " <+> prettyTCM vfull
              , "    stuck on" <+> prettyTCM (ignoreBlocking v)
              ]
          YesReduction _simpl v -> do
            reportSDoc "tc.reduce"  90 $ "*** reduced definition: " <+> prettyTCM f
            reportSDoc "tc.reduce"  95 $ "    result" <+> prettyTCM v
            reportSDoc "tc.reduce" 100 $ "    raw   " <+> text (show v)

-- | Reduce a non-primitive definition if it is a copy linking to another def.
reduceDefCopy :: QName -> Elims -> TCM (Reduced () Term)
reduceDefCopy f es = do
  info <- TCM.getConstInfo f
  rewr <- instantiateRewriteRules =<< TCM.getRewriteRulesFor f
  if (defCopy info) then reduceDef_ info rewr f es else return $ NoReduction ()
  where
    reduceDef_ :: Definition -> RewriteRules -> QName -> Elims -> TCM (Reduced () Term)
    reduceDef_ info rewr f es = do
      let v0   = Def f []
          cls  = (defClauses info)
          mcc  = (defCompiled info)
      if (defDelayed info == Delayed) || (defNonterminating info)
       then return $ NoReduction ()
       else do
          ev <- runReduceM $ appDefE_ f v0 cls mcc rewr $ map notReduced es
          case ev of
            YesReduction simpl t -> return $ YesReduction simpl t
            NoReduction{}        -> return $ NoReduction ()

-- | Reduce simple (single clause) definitions.
reduceHead :: (HasBuiltins m, HasConstInfo m, MonadReduce m, MonadDebug m)
           => Term -> m (Blocked Term)
reduceHead v = do -- ignoreAbstractMode $ do
  -- Andreas, 2013-02-18 ignoreAbstractMode leads to information leakage
  -- see Issue 796

  -- first, possibly rewrite literal v to constructor form
  v <- constructorForm v
  traceSDoc "tc.inj.reduce" 30 ("reduceHead" <+> prettyTCM v) $ do
  case v of
    Def f es -> do

      abstractMode <- envAbstractMode <$> askTC
      isAbstract <- treatAbstractly f
      traceSLn "tc.inj.reduce" 50 (
        "reduceHead: we are in " ++ show abstractMode++ "; " ++ show f ++
        " is treated " ++ if isAbstract then "abstractly" else "concretely"
        ) $ do
      let v0  = Def f []
          red = liftReduce $ unfoldDefinitionE False reduceHead v0 f es
      def <- theDef <$> getConstInfo f
      case def of
        -- Andreas, 2012-11-06 unfold aliases (single clause terminating functions)
        -- see test/succeed/Issue747
        -- We restrict this to terminating functions to not make the
        -- type checker loop here on non-terminating functions.
        -- see test/fail/TerminationInfiniteRecord
        Function{ funClauses = [ _ ], funDelayed = NotDelayed, funTerminates = Just True } -> do
          traceSLn "tc.inj.reduce" 50 ("reduceHead: head " ++ show f ++ " is Function") $ do
          red
        Datatype{ dataClause = Just _ } -> red
        Record{ recClause = Just _ }    -> red
        _                               -> return $ notBlocked v
    _ -> return $ notBlocked v

-- | Unfold a single inlined function.
unfoldInlined :: (HasConstInfo m, MonadReduce m) => Term -> m Term
unfoldInlined v = do
  inTypes <- viewTC eWorkingOnTypes
  case v of
    _ | inTypes -> return v -- Don't inline in types (to avoid unfolding of goals)
    Def f es -> do
      def <- theDef <$> getConstInfo f
      case def of   -- Only for simple definitions with no pattern matching (TODO: maybe copatterns?)
        Function{ funCompiled = Just Done{}, funDelayed = NotDelayed }
          | def ^. funInline -> liftReduce $
          ignoreBlocking <$> unfoldDefinitionE False (return . notBlocked) (Def f []) f es
        _ -> return v
    _ -> return v

-- | Apply a definition using the compiled clauses, or fall back to
--   ordinary clauses if no compiled clauses exist.
appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDef_ f v0 cls mcc rewr args = appDefE_ f v0 cls mcc rewr $ map (fmap Apply) args

appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE_ f v0 cls mcc rewr args =
  localTC (\ e -> e { envAppDef = Just f }) $
  maybe (appDefE' v0 cls rewr args)
        (\cc -> appDefE v0 cc rewr args) mcc


-- | Apply a defined function to it's arguments, using the compiled clauses.
--   The original term is the first argument applied to the third.
appDef :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDef v cc rewr args = appDefE v cc rewr $ map (fmap Apply) args

appDefE :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE v cc rewr es = do
  r <- matchCompiledE cc es
  case r of
    YesReduction simpl t -> return $ YesReduction simpl t
    NoReduction es'      -> rewrite (void es') v rewr (ignoreBlocking es')

-- | Apply a defined function to it's arguments, using the original clauses.
appDef' :: Term -> [Clause] -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDef' v cls rewr args = appDefE' v cls rewr $ map (fmap Apply) args

appDefE' :: Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE' v cls rewr es = goCls cls $ map ignoreReduced es
  where
    goCls :: [Clause] -> [Elim] -> ReduceM (Reduced (Blocked Term) Term)
    goCls cl es = do
      case cl of
        -- Andreas, 2013-10-26  In case of an incomplete match,
        -- we just do not reduce.  This allows adding single function
        -- clauses after they have been type-checked, to type-check
        -- the remaining clauses (see Issue 907).
        -- Andrea(s), 2014-12-05:  We return 'MissingClauses' here, since this
        -- is the most conservative reason.
        [] -> rewrite (NotBlocked MissingClauses ()) v rewr es
        cl : cls -> do
          let pats = namedClausePats cl
              body = clauseBody cl
              npats = length pats
              nvars = size $ clauseTel cl
          -- if clause is underapplied, skip to next clause
          if length es < npats then goCls cls es else do
            let (es0, es1) = splitAt npats es
            (m, es0) <- matchCopatterns pats es0
            es <- return $ es0 ++ es1
            case m of
              No         -> goCls cls es
              DontKnow b -> rewrite b v rewr es
              Yes simpl vs -- vs is the subst. for the variables bound in body
                | Just w <- body -> do -- clause has body?
                    -- TODO: let matchPatterns also return the reduced forms
                    -- of the original arguments!
                    -- Andreas, 2013-05-19 isn't this done now?
                    let sigma = buildSubstitution __IMPOSSIBLE__ nvars vs
                    return $ YesReduction simpl $ applySubst sigma w `applyE` es1
                | otherwise     -> rewrite (NotBlocked AbsurdMatch ()) v rewr es

instance Reduce a => Reduce (Closure a) where
    reduce' cl = do
        x <- enterClosure cl reduce'
        return $ cl { clValue = x }

instance Reduce Telescope where
  reduce' EmptyTel          = return EmptyTel
  reduce' (ExtendTel a tel) = ExtendTel <$> reduce' a <*> reduce' tel

instance Reduce Constraint where
  reduce' (ValueCmp cmp t u v) = do
    (t,u,v) <- reduce' (t,u,v)
    return $ ValueCmp cmp t u v
  reduce' (ValueCmpOnFace cmp p t u v) = do
    ((p,t),u,v) <- reduce' ((p,t),u,v)
    return $ ValueCmpOnFace cmp p t u v
  reduce' (ElimCmp cmp fs t v as bs) =
    ElimCmp cmp fs <$> reduce' t <*> reduce' v <*> reduce' as <*> reduce' bs
  reduce' (LevelCmp cmp u v)    = uncurry (LevelCmp cmp) <$> reduce' (u,v)
  reduce' (TypeCmp cmp a b)     = uncurry (TypeCmp cmp) <$> reduce' (a,b)
  reduce' (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp)  <$> reduce' (tela,telb)
  reduce' (SortCmp cmp a b)     = uncurry (SortCmp cmp) <$> reduce' (a,b)
  reduce' (Guarded c pid)       = Guarded <$> reduce' c <*> pure pid
  reduce' (UnBlock m)           = return $ UnBlock m
  reduce' (FindInstance m b cands) = FindInstance m b <$> mapM reduce' cands
  reduce' (IsEmpty r t)         = IsEmpty r <$> reduce' t
  reduce' (CheckSizeLtSat t)    = CheckSizeLtSat <$> reduce' t
  reduce' c@CheckFunDef{}       = return c
  reduce' (HasBiggerSort a)     = HasBiggerSort <$> reduce' a
  reduce' (HasPTSRule a b)      = uncurry HasPTSRule <$> reduce' (a,b)
  reduce' (UnquoteTactic m t h g) = UnquoteTactic m <$> reduce' t <*> reduce' h <*> reduce' g

instance Reduce e => Reduce (Map k e) where
    reduce' = traverse reduce'

instance Reduce Candidate where
  reduce' (Candidate u t ov) = Candidate <$> reduce' u <*> reduce' t <*> pure ov

instance Reduce EqualityView where
  reduce' (OtherType t)            = OtherType
    <$> reduce' t
  reduce' (EqualityType s eq l t a b) = EqualityType
    <$> reduce' s
    <*> return eq
    <*> mapM reduce' l
    <*> reduce' t
    <*> reduce' a
    <*> reduce' b

---------------------------------------------------------------------------
-- * Simplification
---------------------------------------------------------------------------

-- | Only unfold definitions if this leads to simplification
--   which means that a constructor/literal pattern is matched.
class Simplify t where
  simplify' :: t -> ReduceM t

instance Simplify Term where
  simplify' v = do
    v <- instantiate' v
    case v of
      Def f vs   -> do
        let keepGoing simp v = return (simp, notBlocked v)
        (simpl, v) <- unfoldDefinition' False keepGoing (Def f []) f vs
        traceSDoc "tc.simplify'" 90 (
          text ("simplify': unfolding definition returns " ++ show simpl)
            <+> prettyTCM (ignoreBlocking v)) $ do
        case simpl of
          YesSimplification -> simplifyBlocked' v -- Dangerous, but if @simpl@ then @v /= Def f vs@
          NoSimplification  -> Def f <$> simplify' vs
      MetaV x vs -> MetaV x  <$> simplify' vs
      Con c ci vs-> Con c ci <$> simplify' vs
      Sort s     -> Sort     <$> simplify' s
      Level l    -> levelTm  <$> simplify' l
      Pi a b     -> Pi       <$> simplify' a <*> simplify' b
      Lit l      -> return v
      Var i vs   -> Var i    <$> simplify' vs
      Lam h v    -> Lam h    <$> simplify' v
      DontCare v -> dontCare <$> simplify' v
      Dummy{}    -> return v

simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t
simplifyBlocked' (Blocked _ t) = return t
simplifyBlocked' (NotBlocked _ t) = simplify' t  -- Andrea(s), 2014-12-05 OK?

instance Simplify Type where
    simplify' (El s t) = El <$> simplify' s <*> simplify' t

instance Simplify Elim where
  simplify' (Apply v) = Apply <$> simplify' v
  simplify' (Proj o f)= pure $ Proj o f
  simplify' (IApply x y v) = IApply <$> simplify' x <*> simplify' y <*> simplify' v

instance Simplify Sort where
    simplify' s = do
      case s of
        PiSort s1 s2 -> piSort <$> simplify' s1 <*> simplify' s2
        UnivSort s -> do
          ui <- univInf
          univSort ui <$> simplify' s
        Type s     -> Type <$> simplify' s
        Prop s     -> Prop <$> simplify' s
        Inf        -> return s
        SizeUniv   -> return s
        MetaS x es -> MetaS x <$> simplify' es
        DefS d es  -> DefS d <$> simplify' es
        DummyS{}   -> return s

instance Simplify Level where
  simplify' (Max as) = levelMax <$> simplify' as

instance Simplify PlusLevel where
  simplify' l@ClosedLevel{} = return l
  simplify' (Plus n l) = Plus n <$> simplify' l

instance Simplify LevelAtom where
  simplify' l = do
    l <- instantiate' l
    case l of
      MetaLevel m vs   -> MetaLevel m <$> simplify' vs
      BlockedLevel m v -> BlockedLevel m <$> simplify' v
      NeutralLevel r v -> NeutralLevel r <$> simplify' v -- ??
      UnreducedLevel v -> UnreducedLevel <$> simplify' v -- ??

instance (Subst t a, Simplify a) => Simplify (Abs a) where
    simplify' a@(Abs x _) = Abs x <$> underAbstraction_ a simplify'
    simplify' (NoAbs x v) = NoAbs x <$> simplify' v

instance Simplify t => Simplify (Arg t) where
    simplify' = traverse simplify'

instance Simplify t => Simplify (Named name t) where
    simplify' = traverse simplify'

instance Simplify t => Simplify (Dom t) where
    simplify' = traverse simplify'

instance Simplify t => Simplify [t] where
    simplify' = traverse simplify'

instance Simplify e => Simplify (Map k e) where
    simplify' = traverse simplify'

instance Simplify a => Simplify (Maybe a) where
    simplify' = traverse simplify'

instance (Simplify a, Simplify b) => Simplify (a,b) where
    simplify' (x,y) = (,) <$> simplify' x <*> simplify' y

instance (Simplify a, Simplify b, Simplify c) => Simplify (a,b,c) where
    simplify' (x,y,z) =
        do  (x,(y,z)) <- simplify' (x,(y,z))
            return (x,y,z)

instance Simplify a => Simplify (Closure a) where
    simplify' cl = do
        x <- enterClosure cl simplify'
        return $ cl { clValue = x }

instance (Subst t a, Simplify a) => Simplify (Tele a) where
  simplify' EmptyTel        = return EmptyTel
  simplify' (ExtendTel a b) = uncurry ExtendTel <$> simplify' (a, b)

instance Simplify ProblemConstraint where
  simplify' (PConstr pid c) = PConstr pid <$> simplify' c

instance Simplify Constraint where
  simplify' (ValueCmp cmp t u v) = do
    (t,u,v) <- simplify' (t,u,v)
    return $ ValueCmp cmp t u v
  simplify' (ValueCmpOnFace cmp p t u v) = do
    ((p,t),u,v) <- simplify' ((p,t),u,v)
    return $ ValueCmp cmp t u v
  simplify' (ElimCmp cmp fs t v as bs) =
    ElimCmp cmp fs <$> simplify' t <*> simplify' v <*> simplify' as <*> simplify' bs
  simplify' (LevelCmp cmp u v)    = uncurry (LevelCmp cmp) <$> simplify' (u,v)
  simplify' (TypeCmp cmp a b)     = uncurry (TypeCmp cmp) <$> simplify' (a,b)
  simplify' (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> simplify' (tela,telb)
  simplify' (SortCmp cmp a b)     = uncurry (SortCmp cmp) <$> simplify' (a,b)
  simplify' (Guarded c pid)       = Guarded <$> simplify' c <*> pure pid
  simplify' (UnBlock m)           = return $ UnBlock m
  simplify' (FindInstance m b cands) = FindInstance m b <$> mapM simplify' cands
  simplify' (IsEmpty r t)         = IsEmpty r <$> simplify' t
  simplify' (CheckSizeLtSat t)    = CheckSizeLtSat <$> simplify' t
  simplify' c@CheckFunDef{}       = return c
  simplify' (HasBiggerSort a)     = HasBiggerSort <$> simplify' a
  simplify' (HasPTSRule a b)      = uncurry HasPTSRule <$> simplify' (a,b)
  simplify' (UnquoteTactic m t h g) = UnquoteTactic m <$> simplify' t <*> simplify' h <*> simplify' g

instance Simplify Bool where
  simplify' = return

-- UNUSED
-- instance Simplify ConPatternInfo where
--   simplify' (ConPatternInfo mr mt) = ConPatternInfo mr <$> simplify' mt

-- UNUSED
-- instance Simplify Pattern where
--   simplify' p = case p of
--     VarP _       -> return p
--     LitP _       -> return p
--     ConP c ci ps -> ConP c <$> simplify' ci <*> simplify' ps
--     DotP v       -> DotP <$> simplify' v
--     ProjP _      -> return p

instance Simplify DisplayForm where
  simplify' (Display n ps v) = Display n <$> simplify' ps <*> return v

instance Simplify Candidate where
  simplify' (Candidate u t ov) = Candidate <$> simplify' u <*> simplify' t <*> pure ov

instance Simplify EqualityView where
  simplify' (OtherType t)            = OtherType
    <$> simplify' t
  simplify' (EqualityType s eq l t a b) = EqualityType
    <$> simplify' s
    <*> return eq
    <*> mapM simplify' l
    <*> simplify' t
    <*> simplify' a
    <*> simplify' b

---------------------------------------------------------------------------
-- * Normalisation
---------------------------------------------------------------------------

class Normalise t where
    normalise' :: t -> ReduceM t

instance Normalise Sort where
    normalise' s = do
      s <- reduce' s
      case s of
        PiSort s1 s2 -> piSort <$> normalise' s1 <*> normalise' s2
        UnivSort s -> do
          ui <- univInf
          univSort ui <$> normalise' s
        Prop s     -> Prop <$> normalise' s
        Type s     -> Type <$> normalise' s
        Inf        -> return Inf
        SizeUniv   -> return SizeUniv
        MetaS x es -> return s
        DefS d es  -> return s
        DummyS{}   -> return s

instance Normalise Type where
    normalise' (El s t) = El <$> normalise' s <*> normalise' t

instance Normalise Term where
    normalise' v = ifM shouldTryFastReduce (fastNormalise v) (slowNormaliseArgs =<< reduce' v)

slowNormaliseArgs :: Term -> ReduceM Term
slowNormaliseArgs v = case v of
  Var n vs    -> Var n      <$> normalise' vs
  Con c ci vs -> Con c ci   <$> normalise' vs
  Def f vs    -> Def f      <$> normalise' vs
  MetaV x vs  -> MetaV x    <$> normalise' vs
  Lit _       -> return v
  Level l     -> levelTm    <$> normalise' l
  Lam h b     -> Lam h      <$> normalise' b
  Sort s      -> Sort       <$> normalise' s
  Pi a b      -> uncurry Pi <$> normalise' (a, b)
  DontCare _  -> return v
  Dummy{}     -> return v

instance Normalise Elim where
  normalise' (Apply v) = Apply <$> normalise' v
  normalise' (Proj o f)= pure $ Proj o f
  normalise' (IApply x y v) = IApply <$> normalise' x <*> normalise' y <*> normalise' v

instance Normalise Level where
  normalise' (Max as) = levelMax <$> normalise' as

instance Normalise PlusLevel where
  normalise' l@ClosedLevel{} = return l
  normalise' (Plus n l) = Plus n <$> normalise' l

instance Normalise LevelAtom where
  normalise' l = do
    l <- reduce' l
    case l of
      MetaLevel m vs   -> MetaLevel m <$> normalise' vs
      BlockedLevel m v -> BlockedLevel m <$> normalise' v
      NeutralLevel r v -> NeutralLevel r <$> normalise' v
      UnreducedLevel{} -> __IMPOSSIBLE__    -- I hope

instance (Subst t a, Normalise a) => Normalise (Abs a) where
    normalise' a@(Abs x _) = Abs x <$> underAbstraction_ a normalise'
    normalise' (NoAbs x v) = NoAbs x <$> normalise' v

instance Normalise t => Normalise (Arg t) where
    normalise' a | isIrrelevant a = return a -- Andreas, 2012-04-02: Do not normalize irrelevant terms!?
                | otherwise                       = traverse normalise' a

instance Normalise t => Normalise (Named name t) where
    normalise' = traverse normalise'

instance Normalise t => Normalise (Dom t) where
    normalise' = traverse normalise'

instance Normalise t => Normalise [t] where
    normalise' = traverse normalise'

instance (Normalise a, Normalise b) => Normalise (a,b) where
    normalise' (x,y) = (,) <$> normalise' x <*> normalise' y

instance (Normalise a, Normalise b, Normalise c) => Normalise (a,b,c) where
    normalise' (x,y,z) =
        do  (x,(y,z)) <- normalise' (x,(y,z))
            return (x,y,z)

instance Normalise a => Normalise (Closure a) where
    normalise' cl = do
        x <- enterClosure cl normalise'
        return $ cl { clValue = x }

instance (Subst t a, Normalise a) => Normalise (Tele a) where
  normalise' EmptyTel        = return EmptyTel
  normalise' (ExtendTel a b) = uncurry ExtendTel <$> normalise' (a, b)

instance Normalise ProblemConstraint where
  normalise' (PConstr pid c) = PConstr pid <$> normalise' c

instance Normalise Constraint where
  normalise' (ValueCmp cmp t u v) = do
    (t,u,v) <- normalise' (t,u,v)
    return $ ValueCmp cmp t u v
  normalise' (ValueCmpOnFace cmp p t u v) = do
    ((p,t),u,v) <- normalise' ((p,t),u,v)
    return $ ValueCmpOnFace cmp p t u v
  normalise' (ElimCmp cmp fs t v as bs) =
    ElimCmp cmp fs <$> normalise' t <*> normalise' v <*> normalise' as <*> normalise' bs
  normalise' (LevelCmp cmp u v)    = uncurry (LevelCmp cmp) <$> normalise' (u,v)
  normalise' (TypeCmp cmp a b)     = uncurry (TypeCmp cmp) <$> normalise' (a,b)
  normalise' (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> normalise' (tela,telb)
  normalise' (SortCmp cmp a b)     = uncurry (SortCmp cmp) <$> normalise' (a,b)
  normalise' (Guarded c pid)       = Guarded <$> normalise' c <*> pure pid
  normalise' (UnBlock m)           = return $ UnBlock m
  normalise' (FindInstance m b cands) = FindInstance m b <$> mapM normalise' cands
  normalise' (IsEmpty r t)         = IsEmpty r <$> normalise' t
  normalise' (CheckSizeLtSat t)    = CheckSizeLtSat <$> normalise' t
  normalise' c@CheckFunDef{}       = return c
  normalise' (HasBiggerSort a)     = HasBiggerSort <$> normalise' a
  normalise' (HasPTSRule a b)      = uncurry HasPTSRule <$> normalise' (a,b)
  normalise' (UnquoteTactic m t h g) = UnquoteTactic m <$> normalise' t <*> normalise' h <*> normalise' g

instance Normalise Bool where
  normalise' = return

instance Normalise Int where
  normalise' = return

instance Normalise Char where
  normalise' = return

instance Normalise ConPatternInfo where
  normalise' i = normalise' (conPType i) <&> \ t -> i { conPType = t }

instance Normalise DBPatVar where
  normalise' = return

instance Normalise a => Normalise (Pattern' a) where
  normalise' p = case p of
    VarP o x     -> VarP o <$> normalise' x
    LitP _       -> return p
    ConP c mt ps -> ConP c <$> normalise' mt <*> normalise' ps
    DefP o q ps  -> DefP o q <$> normalise' ps
    DotP o v     -> DotP o <$> normalise' v
    ProjP{}      -> return p
    IApplyP o t u x -> IApplyP o <$> normalise' t <*> normalise' u <*> normalise' x

instance Normalise DisplayForm where
  normalise' (Display n ps v) = Display n <$> normalise' ps <*> return v

instance Normalise e => Normalise (Map k e) where
    normalise' = traverse normalise'

instance Normalise a => Normalise (Maybe a) where
    normalise' = traverse normalise'

instance Normalise Candidate where
  normalise' (Candidate u t ov) = Candidate <$> normalise' u <*> normalise' t <*> pure ov

instance Normalise EqualityView where
  normalise' (OtherType t)            = OtherType
    <$> normalise' t
  normalise' (EqualityType s eq l t a b) = EqualityType
    <$> normalise' s
    <*> return eq
    <*> mapM normalise' l
    <*> normalise' t
    <*> normalise' a
    <*> normalise' b

---------------------------------------------------------------------------
-- * Full instantiation
---------------------------------------------------------------------------

-- | @instantiateFull'@ 'instantiate's metas everywhere (and recursively)
--   but does not 'reduce'.
class InstantiateFull t where
    instantiateFull' :: t -> ReduceM t

instance InstantiateFull Name where
    instantiateFull' = return

instance InstantiateFull Sort where
    instantiateFull' s = do
        s <- instantiate' s
        case s of
            Type n     -> Type <$> instantiateFull' n
            Prop n     -> Prop <$> instantiateFull' n
            PiSort s1 s2 -> piSort <$> instantiateFull' s1 <*> instantiateFull' s2
            UnivSort s -> do
              ui <- univInf
              univSort ui <$> instantiateFull' s
            Inf        -> return s
            SizeUniv   -> return s
            MetaS x es -> MetaS x <$> instantiateFull' es
            DefS d es  -> DefS d <$> instantiateFull' es
            DummyS{}   -> return s

instance (InstantiateFull a) => InstantiateFull (Type' a) where
    instantiateFull' (El s t) =
      El <$> instantiateFull' s <*> instantiateFull' t

instance InstantiateFull Term where
    instantiateFull' v = etaOnce =<< do -- Andreas, 2010-11-12 DONT ETA!? eta-reduction breaks subject reduction
-- but removing etaOnce now breaks everything
      v <- instantiate' v
      case v of
          Var n vs    -> Var n <$> instantiateFull' vs
          Con c ci vs -> Con c ci <$> instantiateFull' vs
          Def f vs    -> Def f <$> instantiateFull' vs
          MetaV x vs  -> MetaV x <$> instantiateFull' vs
          Lit _       -> return v
          Level l     -> levelTm <$> instantiateFull' l
          Lam h b     -> Lam h <$> instantiateFull' b
          Sort s      -> Sort <$> instantiateFull' s
          Pi a b      -> uncurry Pi <$> instantiateFull' (a,b)
          DontCare v  -> dontCare <$> instantiateFull' v
          Dummy{}     -> return v

instance InstantiateFull Level where
  instantiateFull' (Max as) = levelMax <$> instantiateFull' as

instance InstantiateFull PlusLevel where
  instantiateFull' l@ClosedLevel{} = return l
  instantiateFull' (Plus n l) = Plus n <$> instantiateFull' l

instance InstantiateFull LevelAtom where
  instantiateFull' l = case l of
    MetaLevel m vs -> do
      v <- instantiateFull' (MetaV m vs)
      case v of
        MetaV m vs -> return $ MetaLevel m vs
        _          -> return $ UnreducedLevel v
    NeutralLevel r v -> NeutralLevel r <$> instantiateFull' v
    BlockedLevel m v ->
      ifM (isInstantiatedMeta m)
          (UnreducedLevel <$> instantiateFull' v)
          (BlockedLevel m <$> instantiateFull' v)
    UnreducedLevel v -> UnreducedLevel <$> instantiateFull' v

instance InstantiateFull Substitution where
  instantiateFull' sigma =
    case sigma of
      IdS                  -> return IdS
      EmptyS err           -> return $ EmptyS err
      Wk   n sigma         -> Wk   n         <$> instantiateFull' sigma
      Lift n sigma         -> Lift n         <$> instantiateFull' sigma
      Strengthen bot sigma -> Strengthen bot <$> instantiateFull' sigma
      t :# sigma           -> consS <$> instantiateFull' t
                                    <*> instantiateFull' sigma

instance InstantiateFull Bool where
    instantiateFull' = return

instance InstantiateFull Int where
    instantiateFull' = return

instance InstantiateFull ConPatternInfo where
    instantiateFull' i = instantiateFull' (conPType i) <&> \ t -> i { conPType = t }

instance InstantiateFull DBPatVar where
    instantiateFull' = return

instance InstantiateFull a => InstantiateFull (Pattern' a) where
    instantiateFull' (VarP o x)     = VarP o <$> instantiateFull' x
    instantiateFull' (DotP o t)     = DotP o <$> instantiateFull' t
    instantiateFull' (ConP n mt ps) = ConP n <$> instantiateFull' mt <*> instantiateFull' ps
    instantiateFull' (DefP o q ps) = DefP o q <$> instantiateFull' ps
    instantiateFull' l@LitP{}       = return l
    instantiateFull' p@ProjP{}      = return p
    instantiateFull' (IApplyP o t u x) = IApplyP o <$> instantiateFull' t <*> instantiateFull' u <*> instantiateFull' x

instance (Subst t a, InstantiateFull a) => InstantiateFull (Abs a) where
    instantiateFull' a@(Abs x _) = Abs x <$> underAbstraction_ a instantiateFull'
    instantiateFull' (NoAbs x a) = NoAbs x <$> instantiateFull' a

instance InstantiateFull t => InstantiateFull (Arg t) where
    instantiateFull' = traverse instantiateFull'

instance InstantiateFull t => InstantiateFull (Named name t) where
    instantiateFull' = traverse instantiateFull'

instance InstantiateFull t => InstantiateFull (Dom t) where
    instantiateFull' = traverse instantiateFull'

instance InstantiateFull t => InstantiateFull [t] where
    instantiateFull' = traverse instantiateFull'

instance (InstantiateFull a, InstantiateFull b) => InstantiateFull (a,b) where
    instantiateFull' (x,y) = (,) <$> instantiateFull' x <*> instantiateFull' y

instance (InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a,b,c) where
    instantiateFull' (x,y,z) =
        do  (x,(y,z)) <- instantiateFull' (x,(y,z))
            return (x,y,z)

instance InstantiateFull a => InstantiateFull (Closure a) where
    instantiateFull' cl = do
        x <- enterClosure cl instantiateFull'
        return $ cl { clValue = x }

instance InstantiateFull ProblemConstraint where
  instantiateFull' (PConstr p c) = PConstr p <$> instantiateFull' c

instance InstantiateFull Constraint where
  instantiateFull' c = case c of
    ValueCmp cmp t u v -> do
      (t,u,v) <- instantiateFull' (t,u,v)
      return $ ValueCmp cmp t u v
    ValueCmpOnFace cmp p t u v -> do
      ((p,t),u,v) <- instantiateFull' ((p,t),u,v)
      return $ ValueCmpOnFace cmp p t u v
    ElimCmp cmp fs t v as bs ->
      ElimCmp cmp fs <$> instantiateFull' t <*> instantiateFull' v <*> instantiateFull' as <*> instantiateFull' bs
    LevelCmp cmp u v    -> uncurry (LevelCmp cmp) <$> instantiateFull' (u,v)
    TypeCmp cmp a b     -> uncurry (TypeCmp cmp) <$> instantiateFull' (a,b)
    TelCmp a b cmp tela telb -> uncurry (TelCmp a b cmp) <$> instantiateFull' (tela,telb)
    SortCmp cmp a b     -> uncurry (SortCmp cmp) <$> instantiateFull' (a,b)
    Guarded c pid       -> Guarded <$> instantiateFull' c <*> pure pid
    UnBlock m           -> return $ UnBlock m
    FindInstance m b cands -> FindInstance m b <$> mapM instantiateFull' cands
    IsEmpty r t         -> IsEmpty r <$> instantiateFull' t
    CheckSizeLtSat t    -> CheckSizeLtSat <$> instantiateFull' t
    c@CheckFunDef{}     -> return c
    HasBiggerSort a     -> HasBiggerSort <$> instantiateFull' a
    HasPTSRule a b      -> uncurry HasPTSRule <$> instantiateFull' (a,b)
    UnquoteTactic m t g h -> UnquoteTactic m <$> instantiateFull' t <*> instantiateFull' g <*> instantiateFull' h

instance (InstantiateFull a) => InstantiateFull (Elim' a) where
  instantiateFull' (Apply v) = Apply <$> instantiateFull' v
  instantiateFull' (Proj o f)= pure $ Proj o f
  instantiateFull' (IApply x y v) = IApply <$> instantiateFull' x <*> instantiateFull' y <*> instantiateFull' v

instance InstantiateFull e => InstantiateFull (Map k e) where
    instantiateFull' = traverse instantiateFull'

instance InstantiateFull e => InstantiateFull (HashMap k e) where
    instantiateFull' = traverse instantiateFull'

instance InstantiateFull ModuleName where
    instantiateFull' = return

instance InstantiateFull Scope where
    instantiateFull' = return

instance InstantiateFull Signature where
  instantiateFull' (Sig a b c) = uncurry3 Sig <$> instantiateFull' (a, b, c)

instance InstantiateFull Section where
  instantiateFull' (Section tel) = Section <$> instantiateFull' tel

instance (Subst t a, InstantiateFull a) => InstantiateFull (Tele a) where
  instantiateFull' EmptyTel = return EmptyTel
  instantiateFull' (ExtendTel a b) = uncurry ExtendTel <$> instantiateFull' (a, b)

instance InstantiateFull Char where
    instantiateFull' = return

instance InstantiateFull Definition where
    instantiateFull' def@Defn{ defType = t ,defDisplay = df, theDef = d } = do
      (t, df, d) <- instantiateFull' (t, df, d)
      return $ def{ defType = t, defDisplay = df, theDef = d }

instance InstantiateFull NLPat where
  instantiateFull' (PVar x y) = return $ PVar x y
  instantiateFull' (PWild)    = return PWild
  instantiateFull' (PDef x y) = PDef <$> instantiateFull' x <*> instantiateFull' y
  instantiateFull' (PLam x y) = PLam x <$> instantiateFull' y
  instantiateFull' (PPi x y)  = PPi <$> instantiateFull' x <*> instantiateFull' y
  instantiateFull' (PBoundVar x y) = PBoundVar x <$> instantiateFull' y
  instantiateFull' (PTerm x)  = PTerm <$> instantiateFull' x

instance InstantiateFull NLPType where
  instantiateFull' (NLPType l a) = NLPType
    <$> instantiateFull' l
    <*> instantiateFull' a

instance InstantiateFull RewriteRule where
  instantiateFull' (RewriteRule q gamma f ps rhs t) =
    RewriteRule q
      <$> instantiateFull' gamma
      <*> pure f
      <*> instantiateFull' ps
      <*> instantiateFull' rhs
      <*> instantiateFull' t

instance InstantiateFull a => InstantiateFull (Open a) where
  instantiateFull' (OpenThing n a) = OpenThing n <$> instantiateFull' a

instance InstantiateFull DisplayForm where
  instantiateFull' (Display n ps v) = uncurry (Display n) <$> instantiateFull' (ps, v)

instance InstantiateFull DisplayTerm where
  instantiateFull' (DTerm v)       = DTerm <$> instantiateFull' v
  instantiateFull' (DDot  v)       = DDot  <$> instantiateFull' v
  instantiateFull' (DCon c ci vs)  = DCon c ci <$> instantiateFull' vs
  instantiateFull' (DDef c es)     = DDef c <$> instantiateFull' es
  instantiateFull' (DWithApp v vs ws) = uncurry3 DWithApp <$> instantiateFull' (v, vs, ws)

instance InstantiateFull Defn where
    instantiateFull' d = case d of
      Axiom{} -> return d
      DataOrRecSig{} -> return d
      GeneralizableVar{} -> return d
      AbstractDefn d -> AbstractDefn <$> instantiateFull' d
      Function{ funClauses = cs, funCompiled = cc, funInv = inv, funExtLam = extLam } -> do
        (cs, cc, inv) <- instantiateFull' (cs, cc, inv)
        extLam <- instantiateFull' extLam
        return $ d { funClauses = cs, funCompiled = cc, funInv = inv, funExtLam = extLam }
      Datatype{ dataSort = s, dataClause = cl } -> do
        s  <- instantiateFull' s
        cl <- instantiateFull' cl
        return $ d { dataSort = s, dataClause = cl }
      Record{ recClause = cl, recTel = tel } -> do
        cl  <- instantiateFull' cl
        tel <- instantiateFull' tel
        return $ d { recClause = cl, recTel = tel }
      Constructor{} -> return d
      Primitive{ primClauses = cs } -> do
        cs <- instantiateFull' cs
        return $ d { primClauses = cs }

instance InstantiateFull ExtLamInfo where
  instantiateFull' e@(ExtLamInfo { extLamSys = sys}) = do
    sys <- instantiateFull' sys
    return $ e { extLamSys = sys}

instance InstantiateFull System where
  instantiateFull' (System tel sys) = System <$> instantiateFull' tel <*> instantiateFull' sys

instance InstantiateFull FunctionInverse where
  instantiateFull' NotInjective = return NotInjective
  instantiateFull' (Inverse inv) = Inverse <$> instantiateFull' inv

instance InstantiateFull a => InstantiateFull (WithArity a) where
  instantiateFull' (WithArity n a) = WithArity n <$> instantiateFull' a

instance InstantiateFull a => InstantiateFull (Case a) where
  instantiateFull' (Branches cop cs eta ls m b lz) =
    Branches cop
      <$> instantiateFull' cs
      <*> instantiateFull' eta
      <*> instantiateFull' ls
      <*> instantiateFull' m
      <*> pure b
      <*> pure lz

instance InstantiateFull CompiledClauses where
  instantiateFull' Fail        = return Fail
  instantiateFull' (Done m t)  = Done m <$> instantiateFull' t
  instantiateFull' (Case n bs) = Case n <$> instantiateFull' bs

instance InstantiateFull Clause where
    instantiateFull' (Clause rl rf tel ps b t catchall unreachable) =
       Clause rl rf <$> instantiateFull' tel
       <*> instantiateFull' ps
       <*> instantiateFull' b
       <*> instantiateFull' t
       <*> return catchall
       <*> return unreachable

instance InstantiateFull Interface where
    instantiateFull' (Interface h s ft ms mod scope inside
                               sig display userwarn b foreignCode
                               highlighting pragmas usedOpts patsyns warnings) =
        Interface h s ft ms mod scope inside
            <$> instantiateFull' sig
            <*> instantiateFull' display
            <*> return userwarn
            <*> instantiateFull' b
            <*> return foreignCode
            <*> return highlighting
            <*> return pragmas
            <*> return usedOpts
            <*> return patsyns
            <*> return warnings

instance InstantiateFull a => InstantiateFull (Builtin a) where
    instantiateFull' (Builtin t) = Builtin <$> instantiateFull' t
    instantiateFull' (Prim x)   = Prim <$> instantiateFull' x

instance InstantiateFull QName where
  instantiateFull' = return

instance InstantiateFull ConHead where
  instantiateFull' = return

instance InstantiateFull a => InstantiateFull (Maybe a) where
  instantiateFull' = mapM instantiateFull'

instance InstantiateFull Candidate where
  instantiateFull' (Candidate u t ov) =
    Candidate <$> instantiateFull' u <*> instantiateFull' t <*> pure ov

instance InstantiateFull EqualityView where
  instantiateFull' (OtherType t)            = OtherType
    <$> instantiateFull' t
  instantiateFull' (EqualityType s eq l t a b) = EqualityType
    <$> instantiateFull' s
    <*> return eq
    <*> mapM instantiateFull' l
    <*> instantiateFull' t
    <*> instantiateFull' a
    <*> instantiateFull' b