{-# LANGUAGE CPP #-}

module Agda.TypeChecking.Rules.LHS where

import Data.Maybe

import Control.Applicative
import Control.Monad
import Control.Monad.State

import Data.Traversable

import Agda.Interaction.Options
import Agda.Interaction.Options.Lenses

import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Abstract (IsProjP(..))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views (asView)
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Position

import Agda.TypeChecking.Monad

import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance
import {-# SOURCE #-} Agda.TypeChecking.Empty
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute hiding (Substitution)
import qualified Agda.TypeChecking.Substitute as S (Substitution)
import Agda.TypeChecking.Telescope

import {-# SOURCE #-} Agda.TypeChecking.Rules.Term (checkExpr)
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.TypeChecking.Rules.LHS.ProblemRest
import Agda.TypeChecking.Rules.LHS.Unify
import Agda.TypeChecking.Rules.LHS.Split
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TypeChecking.Rules.LHS.Instantiate
import Agda.TypeChecking.Rules.Data

import Agda.Utils.Functor (($>))
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size

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

-- | Compute the set of flexible patterns in a list of patterns. The result is
--   the deBruijn indices of the flexible patterns. A pattern is flexible if it
--   is dotted or implicit.
flexiblePatterns :: [A.NamedArg A.Pattern] -> TCM FlexibleVars
flexiblePatterns nps = map setFlex <$> filterM (flexible . namedArg . snd) (zip [0..] $ reverse nps)
  where
    setFlex (i, Arg ai p)    = FlexibleVar (getHiding ai) (classify $ namedThing p) i
    classify A.DotP{}        = DotFlex
    classify A.ImplicitP{}   = ImplicitFlex
    classify A.ConP{}        = RecordFlex
    classify _               = __IMPOSSIBLE__
    flexible (A.DotP _ _)    = return True
    flexible (A.ImplicitP _) = return True
    flexible (A.ConP _ (A.AmbQ [c]) qs) =
      ifM (isJust <$> isRecordConstructor c)
          (andM $ map (flexible . namedArg) qs)
          (return False)
    flexible _               = return False

-- | Compute the dot pattern instantiations.
dotPatternInsts :: [A.NamedArg A.Pattern] -> Substitution -> [I.Dom Type] -> TCM [DotPatternInst]
dotPatternInsts ps s as = dpi (map namedArg ps) (reverse s) as
  where
    dpi (_ : _)  []            _       = __IMPOSSIBLE__
    dpi (_ : _)  (Just _ : _)  []      = __IMPOSSIBLE__
    -- the substitution also contains entries for module parameters, so it can
    -- be longer than the pattern
    dpi []       _             _       = return []
    dpi (_ : ps) (Nothing : s) as      = dpi ps s as
    dpi (p : ps) (Just u : s) (a : as) =
      case p of
        A.DotP _ e    -> (DPI e u a :) <$> dpi ps s as
        A.ImplicitP _ -> dpi ps s as
        -- record pattern
        A.ConP _ (A.AmbQ [c]) qs -> do
          Def r es   <- ignoreSharing <$> reduce (unEl $ unDom a)
          let Just vs = allApplyElims es
          (ftel, us) <- etaExpandRecord r vs u
          qs <- insertImplicitPatterns ExpandLast qs ftel
          let instTel EmptyTel _                   = []
              instTel (ExtendTel arg tel) (u : us) = arg : instTel (absApp tel u) us
              instTel ExtendTel{} []               = __IMPOSSIBLE__
              bs0 = instTel ftel (map unArg us)
              -- Andreas, 2012-09-19 propagate relevance info to dot patterns
              bs  = map (mapRelevance (composeRelevance (getRelevance a))) bs0
          dpi (map namedArg qs ++ ps) (map (Just . unArg) us ++ s) (bs ++ as)

        _           -> __IMPOSSIBLE__

instantiatePattern :: Substitution -> Permutation -> [I.NamedArg Pattern] -> [I.NamedArg Pattern]
instantiatePattern sub perm ps
  | length sub /= length hps = error $ unlines [ "instantiatePattern:"
                                               , "  sub  = " ++ show sub
                                               , "  perm = " ++ show perm
                                               , "  ps   = " ++ show ps
                                               ]
  | otherwise  = foldr merge ps $ zipWith inst (reverse sub) hps
  where
    hps = permute perm $ allHoles ps
    inst Nothing  hps = Nothing
    inst (Just t) hps = Just $ plugHole (DotP t) hps

    merge Nothing   ps = ps
    merge (Just qs) ps = zipWith mergeA qs ps
      where
        mergeA a1 a2 = fmap (mergeP (namedArg a1) (namedArg a2) <$) a1
        mergeP (DotP s)  (DotP t)
          | s == t                    = DotP s
          | otherwise                 = __IMPOSSIBLE__
        mergeP (DotP t)  (VarP _)     = DotP t
        mergeP (VarP _)  (DotP t)     = DotP t
        mergeP (DotP _)  _            = __IMPOSSIBLE__
        mergeP _         (DotP _)     = __IMPOSSIBLE__
        mergeP (ConP c1 mt1 ps) (ConP c2 mt2 qs)
          | c1 == c2                  = ConP (c1 `withRangeOf` c2) (mplus mt1 mt2) $ zipWith mergeA ps qs
          | otherwise                 = __IMPOSSIBLE__
        mergeP (LitP l1) (LitP l2)
          | l1 == l2                  = LitP (l1 `withRangeOf` l2)
          | otherwise                 = __IMPOSSIBLE__
        mergeP (VarP x) (VarP y)
          | x == y                    = VarP x
          | otherwise                 = __IMPOSSIBLE__
        mergeP (ConP _ _ _) (VarP _)  = __IMPOSSIBLE__
        mergeP (ConP _ _ _) (LitP _)  = __IMPOSSIBLE__
        mergeP (VarP _) (ConP _ _ _)  = __IMPOSSIBLE__
        mergeP (VarP _) (LitP _)      = __IMPOSSIBLE__
        mergeP (LitP _) (ConP _ _ _)  = __IMPOSSIBLE__
        mergeP (LitP _) (VarP _)      = __IMPOSSIBLE__
        mergeP (ProjP x) (ProjP y)
          | x == y                    = ProjP x
          | otherwise                 = __IMPOSSIBLE__
        mergeP ProjP{} _              = __IMPOSSIBLE__
        mergeP _       ProjP{}        = __IMPOSSIBLE__

-- | Check if a problem is solved. That is, if the patterns are all variables.
isSolvedProblem :: Problem -> Bool
isSolvedProblem problem = null (restPats $ problemRest problem) &&
    all (isSolved . snd . asView . namedArg) (problemInPat problem)
  where
    isSolved (A.DefP _ _ []) = False  -- projection pattern
    isSolved (A.VarP _)      = True
    isSolved (A.WildP _)     = True
    isSolved (A.ImplicitP _) = True
    isSolved (A.AbsurdP _)   = True
    isSolved _               = False
{-
    isVar (A.VarP _)      = True
    isVar (A.WildP _)     = True
    isVar (A.ImplicitP _) = True
    isVar (A.AbsurdP _)   = True
    isVar _               = False
-}

-- | For each user-defined pattern variable in the 'Problem', check
-- that the corresponding data type (if any) does not contain a
-- constructor of the same name (which is not in scope); this
-- \"shadowing\" could indicate an error, and is not allowed.
--
-- Precondition: The problem has to be solved.

noShadowingOfConstructors
  :: (Maybe r -> Call) -- ^ Trace, e.g., @CheckPatternShadowing clause@
  -> Problem -> TCM ()
noShadowingOfConstructors mkCall problem =
  traceCall mkCall $ do
    let pat = map (snd . asView . namedArg) $
                  problemInPat problem
        tel = map (unEl . snd . unDom) $ telToList $ problemTel problem
    zipWithM noShadowing pat tel -- TODO: does not work for flexible arity and projection patterns
    return ()
  where
  noShadowing (A.WildP     {}) t = return ()
  noShadowing (A.AbsurdP   {}) t = return ()
  noShadowing (A.ImplicitP {}) t = return ()
  noShadowing (A.ConP      {}) t = return ()  -- only happens for eta expanded record patterns
  noShadowing (A.DefP      {}) t = return ()  -- projection pattern
  noShadowing (A.AsP       {}) t = __IMPOSSIBLE__
  noShadowing (A.DotP      {}) t = __IMPOSSIBLE__
  noShadowing (A.LitP      {}) t = __IMPOSSIBLE__
  noShadowing (A.PatternSynP {}) t = __IMPOSSIBLE__
  noShadowing (A.VarP x)       t = do
    reportSDoc "tc.lhs.shadow" 30 $ vcat
      [ text $ "checking whether pattern variable " ++ show x ++ " shadows a constructor"
      , nest 2 $ text "type of variable =" <+> prettyTCM t
      ]
    reportSLn "tc.lhs.shadow" 70 $ "  t = " ++ show t
    t <- reduce t
    case t of
      Def t _ -> do
        d <- theDef <$> getConstInfo t
        case d of
          Datatype { dataCons = cs } -> do
            case filter ((A.nameConcrete x ==) . A.nameConcrete . A.qnameName) cs of
              []      -> return ()
              (c : _) -> setCurrentRange (getRange x) $
                typeError $ PatternShadowsConstructor x c
          Axiom       {} -> return ()
          Function    {} -> return ()
          Record      {} -> return ()
          Constructor {} -> __IMPOSSIBLE__
          Primitive   {} -> __IMPOSSIBLE__
      Var   {} -> return ()
      Pi    {} -> return ()
      Sort  {} -> return ()
      Shared p -> noShadowing (A.VarP x) $ derefPtr p
      MetaV {} -> return ()
      -- TODO: If the type is a meta-variable, should the test be
      -- postponed? If there is a problem, then it will be caught when
      -- the completed module is type checked, so it is safe to skip
      -- the test here. However, users may be annoyed if they get an
      -- error in code which has already passed the type checker.
      Lam   {} -> __IMPOSSIBLE__
      Lit   {} -> __IMPOSSIBLE__
      Level {} -> __IMPOSSIBLE__
      Con   {} -> __IMPOSSIBLE__
      DontCare{} -> __IMPOSSIBLE__
      ExtLam{}   -> __IMPOSSIBLE__

-- | Check that a dot pattern matches it's instantiation.
checkDotPattern :: DotPatternInst -> TCM ()
checkDotPattern (DPI e v (Dom info a)) =
  traceCall (CheckDotPattern e v) $ do
  reportSDoc "tc.lhs.dot" 15 $
    sep [ text "checking dot pattern"
        , nest 2 $ prettyA e
        , nest 2 $ text "=" <+> prettyTCM v
        , nest 2 $ text ":" <+> prettyTCM a
        ]
  applyRelevanceToContext (argInfoRelevance info) $ do
    u <- checkExpr e a
    -- Should be ok to do noConstraints here
    noConstraints $ equalTerm a u v

-- | Bind the variables in a left hand side. Precondition: the patterns should
--   all be 'A.VarP', 'A.WildP', 'A.AbsurdP', or 'A.ImplicitP' and the
--   telescope should have the same size as the pattern list.
--   There could also be 'A.ConP's resulting from eta expanded implicit record
--   patterns.
bindLHSVars :: [A.NamedArg A.Pattern] -> Telescope -> TCM a -> TCM a
bindLHSVars []        tel@ExtendTel{}  _   = do
  reportSDoc "impossible" 10 $
    text "bindLHSVars: no patterns left, but tel =" <+> prettyTCM tel
  __IMPOSSIBLE__
bindLHSVars (_ : _)   EmptyTel         _   = __IMPOSSIBLE__
bindLHSVars []        EmptyTel         ret = ret
bindLHSVars (p : ps) (ExtendTel a tel) ret =
  case namedArg p of
    A.VarP x      -> addContext (x, a) $ bindLHSVars ps (absBody tel) ret
    A.WildP _     -> bindDummy (absName tel)
    A.ImplicitP _ -> bindDummy (absName tel)
    A.AbsurdP pi  -> do
      -- Andreas, 2012-03-15: allow postponement of emptyness check
      isEmptyType (getRange pi) $ unDom a
      -- OLD CODE: isReallyEmptyType $ unArg a
      bindDummy (absName tel)
    A.ConP _ (A.AmbQ [c]) qs -> do -- eta expanded record pattern
      Def r es <- reduce (unEl $ unDom a)
      let Just vs = allApplyElims es
      ftel     <- (`apply` vs) <$> getRecordFieldTypes r
      con      <- getConHead c
      let n   = size ftel
          eta = Con con [ var i <$ (namedThing <$> setArgColors [] q) | (q, i) <- zip qs [n - 1, n - 2..0] ]
          -- ^ TODO guilhem
      bindLHSVars (qs ++ ps) (ftel `abstract` absApp (raise (size ftel) tel) eta) ret
    A.ConP{}        -> __IMPOSSIBLE__
    A.DefP{}        -> __IMPOSSIBLE__
    A.AsP{}         -> __IMPOSSIBLE__
    A.DotP{}        -> __IMPOSSIBLE__
    A.LitP{}        -> __IMPOSSIBLE__
    A.PatternSynP{} -> __IMPOSSIBLE__
    where
      bindDummy s = do
        x <- if isUnderscore s then freshNoName_ else freshName_ ("." ++ argNameToString s)
        addContext (x, a) $ bindLHSVars ps (absBody tel) ret

-- | Bind as patterns
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
bindAsPatterns []                ret = ret
bindAsPatterns (AsB x v a : asb) ret = do
  reportSDoc "tc.lhs.as" 10 $ text "as pattern" <+> prettyTCM x <+>
    sep [ text ":" <+> prettyTCM a
        , text "=" <+> prettyTCM v
        ]
  addLetBinding defaultArgInfo x v a $ bindAsPatterns asb ret


data LHSResult = LHSResult
  { lhsPatternTele :: Maybe Telescope   -- ^ Γ: The types of the patterns.
                                        -- 'Nothing' if more patterns than domain types in @a@.
                                        -- Used only to construct a @with@ function; see 'stripwithClausePatterns'.
  , lhsVarTele :: Telescope             -- ^ Δ : The types of the pattern variables.
  , lhsSubstitution :: S.Substitution   -- ^ σ : The patterns in form of a substitution Δ ⊢ σ : Γ
  , lhsVarNames :: [String]             -- ^ Names for the variables in Δ, for binding the body.
  , lhsPatterns :: [I.NamedArg Pattern] -- ^ The patterns in internal syntax.
  , lhsBodyType :: I.Arg Type           -- ^ The type of the body. Is @bσ@ if @Γ@ is defined.
                                        -- 'Irrelevant' to indicate the rhs must be checked
                                        -- in irrelevant mode.
  , lhsPermutation :: Permutation       -- ^ The permutation from pattern vars to @Δ@.
  }

-- | Check a LHS. Main function.
--
--   @checkLeftHandSide a ps a ret@ checks that user patterns @ps@ eliminate
--   the type @a@ of the defined function, and calls continuation @ret@
--   if successful.

checkLeftHandSide
  :: (Maybe r -> Call)
     -- ^ Trace, e.g. @CheckPatternShadowing clause@
  -> Maybe QName
     -- ^ The name of the definition we are checking.
  -> [A.NamedArg A.Pattern]
     -- ^ The patterns.
  -> Type
     -- ^ The expected type @a = Γ → b@.
  -> (LHSResult -> TCM a)
     -- ^ Continuation.
  -> TCM a
checkLeftHandSide c f ps a ret = do
  problem <- problemFromPats ps a
  -- Andreas, 2013-03-15 deactivating the following test allows
  -- flexible arity
  -- unless (noProblemRest problem) $ typeError $ TooManyArgumentsInLHS a
  let mgamma = if noProblemRest problem then Just $ problemTel problem else Nothing

  -- doing the splits:
  LHSState (Problem ps (perm, qs) delta rest) sigma dpi asb
    <- checkLHS $ LHSState problem idS [] []

  unless (null $ restPats rest) $ typeError $ TooManyArgumentsInLHS a

  let b' = restType rest

  noPatternMatchingOnCodata qs

  reportSDoc "tc.lhs.top" 10 $
    vcat [ text "checked lhs:"
	 , nest 2 $ vcat
	   [ text "ps    = " <+> fsep (map prettyA ps)
	   , text "perm  = " <+> text (show perm)
	   , text "delta = " <+> prettyTCM delta
	   , text "dpi   = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi)
	   , text "asb   = " <+> brackets (fsep $ punctuate comma $ map prettyTCM asb)
           , text "qs    = " <+> text (show qs)
	   ]
         ]
  bindLHSVars (filter (isNothing . isProjP) ps) delta $ bindAsPatterns asb $ do
    reportSDoc "tc.lhs.top" 10 $ text "bound pattern variables"
    reportSDoc "tc.lhs.top" 10 $ nest 2 $ text "type  = " <+> prettyTCM b'

    -- Check dot patterns
    mapM_ checkDotPattern dpi

    let rho = renamingR perm -- I'm not certain about this...
        Perm n _ = perm
        xs  = [ stringToArgName $ "h" ++ show n | n <- [0..n - 1] ]
    applyRelevanceToContext (getRelevance b') $ do
      ret $ LHSResult mgamma delta rho xs qs b' perm
  where
    -- the loop: split at a variable in the problem until problem is solved
    checkLHS :: LHSState -> TCM LHSState
    checkLHS st@(LHSState problem sigma dpi asb) = do
      problem <- insertImplicitProblem problem  -- inserting implicits no longer preserve solvedness
      if isSolvedProblem problem                -- since we might insert eta expanded record patterns
        then do
          noShadowingOfConstructors c problem
          return $ st { lhsProblem = problem }
        else do
        unlessM (optPatternMatching <$> gets getPragmaOptions) $
          typeError $ GenericError $ "Pattern matching is disabled"
        sp <- splitProblem f problem
        reportSDoc "tc.lhs.split" 20 $ text "splitting completed"
        case sp of
          Left NothingToSplit   -> do
            reportSLn "tc.lhs.split" 50 $ "checkLHS: nothing to split in problem " ++ show problem
            nothingToSplitError problem
          Left (SplitPanic err) -> do
            reportSLn "impossible" 10 $ "checkLHS: panic: " ++ err
            __IMPOSSIBLE__

          -- Split problem rest (projection pattern)
          Right (SplitRest projPat projType) -> do

            -- Compute the new problem
            let Problem ps1 (iperm, ip) delta (ProblemRest (p:ps2) b) = problem
                -- ps'      = ps1 ++ [p]
                ps'      = ps1 -- drop the projection pattern (already splitted)
                rest     = ProblemRest ps2 (projPat $> projType)
                ip'      = ip ++ [fmap (Named Nothing . ProjP) projPat]
                problem' = Problem ps' (iperm, ip') delta rest
            -- Jump the trampolin
            st' <- updateProblemRest (LHSState problem' sigma dpi asb)
            -- If the field is irrelevant, we need to continue in irr. cxt.
            -- (see Issue 939).
            applyRelevanceToContext (getRelevance projPat) $ do
              checkLHS st'


          -- Split on literal pattern
          Right (Split p0 xs (Arg _ (LitFocus lit iph hix a)) p1) -> do

            -- plug the hole with a lit pattern
            let ip    = plugHole (LitP lit) iph
                iperm = expandP hix 0 $ fst (problemOutPat problem)

            -- substitute the literal in p1 and sigma and dpi and asb
            let delta1 = problemTel p0
                delta2 = absApp (fmap problemTel p1) (Lit lit)
                rho    = liftS (size delta2) $ singletonS (Lit lit)
                -- rho    = [ var i | i <- [0..size delta2 - 1] ]
                --       ++ [ raise (size delta2) $ Lit lit ]
                --       ++ [ var i | i <- [size delta2 ..] ]
                sigma'   = applySubst rho sigma
                dpi'     = applySubst rho dpi
                asb0     = applySubst rho asb
                ip'      = applySubst rho ip
                rest'    = applySubst rho (problemRest problem)

            -- Compute the new problem
            let ps'      = problemInPat p0 ++ problemInPat (absBody p1)
                delta'   = abstract delta1 delta2
                problem' = Problem ps' (iperm, ip') delta' rest'
                asb'     = raise (size delta2) (map (\x -> AsB x (Lit lit) a) xs) ++ asb0
            st' <- updateProblemRest (LHSState problem' sigma' dpi' asb')
            checkLHS st'

          -- Split on constructor pattern
          Right (Split p0 xs (Arg info
                  ( Focus { focusCon      = c
                          , focusImplicit = impl
                          , focusConArgs  = qs
                          , focusRange    = r
                          , focusOutPat   = iph
                          , focusHoleIx   = hix
                          , focusDatatype = d
                          , focusParams   = vs
                          , focusIndices  = ws
                          , focusType     = a
                          }
                  )) p1
                ) -> traceCall (CheckPattern (A.ConP (ConPatInfo impl $ PatRange r) (A.AmbQ [c]) qs)
                                             (problemTel p0)
                                             (El Prop $ Def d $ map Apply $ vs ++ ws)) $ do

            let delta1 = problemTel p0
            let typeOfSplitVar = Arg info a

            reportSDoc "tc.lhs.split" 10 $ sep
              [ text "checking lhs"
              , nest 2 $ text "tel =" <+> prettyTCM (problemTel problem)
              , nest 2 $ text "rel =" <+> (text $ show $ argInfoRelevance info)
              ]

            reportSDoc "tc.lhs.split" 15 $ sep
              [ text "split problem"
              , nest 2 $ vcat
                [ text "delta1 = " <+> prettyTCM delta1
                , text "typeOfSplitVar =" <+> prettyTCM typeOfSplitVar
                , text "focusOutPat =" <+> (text . show) iph
                , text "delta2 = " <+> prettyTCM (problemTel $ absBody p1)
                ]
              ]

{-
            c <- conSrcCon . theDef <$> getConstInfo c
            Con c' [] <- ignoreSharing <$> (constructorForm =<< normalise (Con c []))
            c  <- return $ c' `withRangeOf` c
-}
            c <- (`withRangeOf` c) <$> getConForm c
            ca <- defType <$> getConInfo c

            reportSDoc "tc.lhs.split" 20 $ nest 2 $ vcat
              [ text "ca =" <+> prettyTCM ca
              , text "vs =" <+> prettyList (map prettyTCM vs)
              ]

            -- Lookup the type of the constructor at the given parameters
            let a = ca `piApply` vs

            -- It will end in an application of the datatype
            (gamma', ca, d', us) <- do
              TelV gamma' ca@(El _ def) <- telView a
              let Def d' es = ignoreSharing def
                  Just us   = allApplyElims es
              return (gamma', ca, d', us)

            -- This should be the same datatype as we split on
            unless (d == d') $ typeError $ ShouldBeApplicationOf ca d'

{-
            reportSDoc "tc.lhs.top" 20 $ nest 2 $ vcat
              [ text "gamma' =" <+> text (show gamma')
              ]
-}

            -- Andreas 2010-09-07  propagate relevance info to new vars
            gamma' <- return $ fmap (applyRelevance $ argInfoRelevance info) gamma'
{-
            reportSDoc "tc.lhs.top" 20 $ nest 2 $ vcat
              [ text "gamma' =" <+> text (show gamma')
              ]
-}
            -- Insert implicit patterns
            qs' <- insertImplicitPatterns ExpandLast qs gamma'

            unless (size qs' == size gamma') $
              typeError $ WrongNumberOfConstructorArguments (conName c) (size gamma') (size qs')

            let gamma = useNamesFromPattern qs' gamma'

            -- Get the type of the datatype.
            da <- (`piApply` vs) . defType <$> getConstInfo d

            -- Compute the flexible variables
            flex <- flexiblePatterns (problemInPat p0 ++ qs')

            -- Compute the constructor indices by dropping the parameters
            let us' = drop (size vs) us

	    reportSDoc "tc.lhs.top" 15 $ addCtxTel delta1 $
	      sep [ text "preparing to unify"
		  , nest 2 $ vcat
		    [ text "c      =" <+> prettyTCM c <+> text ":" <+> prettyTCM a
		    , text "d      =" <+> prettyTCM d <+> text ":" <+> prettyTCM da
		    , text "gamma  =" <+> prettyTCM gamma
		    , text "gamma' =" <+> prettyTCM gamma'
		    , text "vs     =" <+> brackets (fsep $ punctuate comma $ map prettyTCM vs)
		    , text "us'    =" <+> brackets (fsep $ punctuate comma $ map prettyTCM us')
		    , text "ws     =" <+> brackets (fsep $ punctuate comma $ map prettyTCM ws)
		    ]
		  ]

            -- Unify constructor target and given type (in Δ₁Γ)
            sub0 <- addCtxTel (delta1 `abstract` gamma) $
                    unifyIndices_ flex (raise (size gamma) da) us' (raise (size gamma) ws)

            -- We should substitute c ys for x in Δ₂ and sigma
            let ys     = teleArgs gamma
                delta2 = absApp (raise (size gamma) $ fmap problemTel p1) (Con c ys)
                rho0   = liftS (size delta2) $ Con c ys :# raiseS (size gamma)
                -- rho0 = [ var i | i <- [0..size delta2 - 1] ]
                --     ++ [ raise (size delta2) $ Con c ys ]
                --     ++ [ var i | i <- [size delta2 + size gamma ..] ]
                sigma0 = applySubst rho0 sigma
                dpi0   = applySubst rho0 dpi
                asb0   = applySubst rho0 asb
                rest0  = applySubst rho0 (problemRest problem)

            reportSDoc "tc.lhs.top" 15 $ addCtxTel (delta1 `abstract` gamma) $ nest 2 $ vcat
              [ text "delta2 =" <+> prettyTCM delta2
              , text "sub0   =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub0)
              ]
            reportSDoc "tc.lhs.top" 15 $ addCtxTel (delta1 `abstract` gamma `abstract` delta2) $
              nest 2 $ vcat
                [ text "dpi0 = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi0)
                , text "asb0 = " <+> brackets (fsep $ punctuate comma $ map prettyTCM asb0)
                ]

            -- Andreas, 2010-09-09, save the type a of record pattern.
            -- It is relative to delta1, but it should be relative to
            -- all variables which will be bound by patterns.
            -- Thus, it has to be raised by 1 (the "hole" variable)
            -- plus the length of delta2 (the variables coming after the hole).
            storedPatternType <- ifM (isJust <$> isRecord d)
              (return $ Just (impl, raise (1 + size delta2) typeOfSplitVar))
              (return $ Nothing)

            -- Plug the hole in the out pattern with c ys
            let ysp = map (argFromDom . fmap (namedVarP . fst)) $ telToList gamma
                ip  = plugHole (ConP c storedPatternType ysp) iph
                ip0 = applySubst rho0 ip

            -- Δ₁Γ ⊢ sub0, we need something in Δ₁ΓΔ₂
            -- Also needs to be padded with Nothing's to have the right length.
            let pad n xs x = xs ++ replicate (max 0 $ n - size xs) x
                newTel = problemTel p0 `abstract` (gamma `abstract` delta2)
                sub    = replicate (size delta2) Nothing ++
                         pad (size delta1 + size gamma) (raise (size delta2) sub0) Nothing

            reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
              [ text "newTel =" <+> prettyTCM newTel
              , addCtxTel newTel $ text "sub =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub)
              , text "ip   =" <+> text (show ip)
              , text "ip0  =" <+> text (show ip0)
              ]
            reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
              [ text "rho0 =" <+> text (show rho0)
              ]

            -- Instantiate the new telescope with the given substitution
            (delta', perm, rho, instTypes) <- instantiateTel sub newTel


            reportSDoc "tc.lhs.inst" 12 $
              vcat [ sep [ text "instantiateTel"
                         , nest 4 $ brackets $ fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub
                         , nest 4 $ prettyTCM newTel
                         ]
                   , nest 2 $ text "delta' =" <+> prettyTCM delta'
                   , nest 2 $ text "perm   =" <+> text (show perm)
                   , nest 2 $ text "itypes =" <+> fsep (punctuate comma $ map prettyTCM instTypes)
                   ]

{-          -- Andreas, 2010-09-09
            -- temporary error message to find non-id perms
            let sorted (Perm _ xs) = xs == List.sort xs
            unless (sorted (perm)) $ typeError $ GenericError $ "detected proper permutation " ++ show perm
-}
            -- Compute the new dot pattern instantiations
            let ps0'   = problemInPat p0 ++ qs' ++ problemInPat (absBody p1)

            reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
              [ text "subst rho sub =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) (applySubst rho sub))
              , text "ps0'  =" <+> brackets (fsep $ punctuate comma $ map prettyA ps0')
              ]

            newDpi <- dotPatternInsts ps0' (applySubst rho sub) instTypes

            -- The final dpis and asbs are the new ones plus the old ones substituted by ρ
            let dpi' = applySubst rho dpi0 ++ newDpi
                asb' = applySubst rho $ asb0 ++ raise (size delta2) (map (\x -> AsB x (Con c ys) ca) xs)

            reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
              [ text "dpi' = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi')
              , text "asb' = " <+> brackets (fsep $ punctuate comma $ map prettyTCM asb')
              ]

            -- Apply the substitution to the type
            let sigma'   = applySubst rho sigma0
                rest'    = applySubst rho rest0

            reportSDoc "tc.lhs.inst" 15 $
              nest 2 $ text "ps0 = " <+> brackets (fsep $ punctuate comma $ map prettyA ps0')

            -- Permute the in patterns
            let ps'  = permute perm ps0'

           -- Compute the new permutation of the out patterns. This is the composition of
            -- the new permutation with the expansion of the old permutation to
            -- reflect the split.
            let perm'  = expandP hix (size gamma) $ fst (problemOutPat problem)
                iperm' = perm `composeP` perm'

            -- Instantiate the out patterns
            let ip'    = instantiatePattern sub perm' ip0
                newip  = applySubst rho ip'

            -- Construct the new problem
            let problem' = Problem ps' (iperm', newip) delta' rest'

            reportSDoc "tc.lhs.top" 12 $ sep
              [ text "new problem"
              , nest 2 $ vcat
                [ text "ps'    = " <+> fsep (map prettyA ps')
                , text "delta' = " <+> prettyTCM delta'
                ]
              ]

            reportSDoc "tc.lhs.top" 14 $ nest 2 $ vcat
              [ text "perm'  =" <+> text (show perm')
              , text "iperm' =" <+> text (show iperm')
              ]
            reportSDoc "tc.lhs.top" 14 $ nest 2 $ vcat
              [ text "ip'    =" <+> text (show ip')
              , text "newip  =" <+> text (show newip)
              ]

            -- if rest type reduces,
            -- extend the split problem by previously not considered patterns
            st'@(LHSState problem'@(Problem ps' (iperm', ip') delta' rest')
                          sigma' dpi' asb')
              <- updateProblemRest $ LHSState problem' sigma' dpi' asb'

            reportSDoc "tc.lhs.top" 12 $ sep
              [ text "new problem from rest"
              , nest 2 $ vcat
                [ text "ps'    = " <+> fsep (map prettyA ps')
                , text "delta' = " <+> prettyTCM delta'
                , text "ip'    =" <+> text (show ip')
                , text "iperm' =" <+> text (show iperm')
                ]
              ]
            -- Continue splitting
            checkLHS st'

-- Ensures that we are not performing pattern matching on codata.

noPatternMatchingOnCodata :: [I.NamedArg Pattern] -> TCM ()
noPatternMatchingOnCodata = mapM_ (check . namedArg)
  where
  check (VarP {})   = return ()
  check (DotP {})   = return ()
  check (ProjP{})   = return ()
  check (LitP {})   = return ()  -- Literals are assumed not to be coinductive.
  check (ConP con _ ps) = do
    TelV _ t <- telView' . defType <$> do getConstInfo $ conName con
    c <- isCoinductive t
    case c of
      Nothing    -> __IMPOSSIBLE__
      Just False -> mapM_ (check . namedArg) ps
      Just True  -> typeError $
        GenericError "Pattern matching on coinductive types is not allowed"