    {-# LANGUAGE CPP #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE ScopedTypeVariables #-}

    -- | Tools to manipulate patterns in internal syntax
    --   in the TCM (type checking monad).

    module Agda.TypeChecking.Patterns.Internal where

    import Control.Monad

    import Data.Maybe

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Monad.Builtin
    import Agda.TypeChecking.Reduce (reduce, normalise, instantiate, instantiateFull)
    import Agda.TypeChecking.Substitute.DeBruijn

    import Agda.Utils.Pretty

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

    -- | Convert a term (from a dot pattern) to a DeBruijn pattern.

    class TermToPattern a b where
      termToPattern :: a -> TCM b

      default termToPattern :: (TermToPattern a' b', Traversable f, a ~ f a', b ~ f b') => a -> TCM b
      termToPattern = traverse termToPattern

    instance TermToPattern a b => TermToPattern [a] [b] where
    instance TermToPattern a b => TermToPattern (Arg a) (Arg b) where
    instance TermToPattern a b => TermToPattern (Named c a) (Named c b) where

    instance (DeBruijn (Pattern' a)) => TermToPattern Term (Pattern' a) where
      termToPattern t = (reduce >=> constructorForm) t >>= \case
        -- Constructors.
        Con c _ args -> ConP c noConPatternInfo . map (fmap unnamed) <$> termToPattern (fromMaybe __IMPOSSIBLE__ $ allApplyElims args)
        Var i []    -> return $ deBruijnVar i
        Lit l       -> return $ LitP l
        t           -> return $ dotP t

    dotPatternsToPatterns :: forall a. (DeBruijn (Pattern' a))
                          => Pattern' a -> TCM (Pattern' a)
    dotPatternsToPatterns = postTraversePatternM dotToPat
      where
        dotToPat :: Pattern' a -> TCM (Pattern' a)
        dotToPat = \case
          DotP o t -> termToPattern t
          p        -> return p