    {-# LANGUAGE GADTs #-}

    -- | 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.Reduce (reduce)
    import Agda.TypeChecking.Substitute.DeBruijn

    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 = (a' -> TCMT IO b') -> f a' -> TCMT IO (f b')
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a' -> TCMT IO b'
    forall a b. TermToPattern a b => a -> TCM b
    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 :: Term -> TCM (Pattern' a)
    termToPattern Term
    t = (Term -> TCMT IO Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Term -> TCMT IO Term)
    -> (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> Term -> TCMT IO Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm) Term
    t TCMT IO Term -> (Term -> TCM (Pattern' a)) -> TCM (Pattern' a)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        -- Constructors.
        Con ConHead
    c ConInfo
    _ Elims
    args -> ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    noConPatternInfo ([NamedArg (Pattern' a)] -> Pattern' a)
    -> ([Arg (Pattern' a)] -> [NamedArg (Pattern' a)])
    -> [Arg (Pattern' a)]
    -> Pattern' a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg (Pattern' a) -> NamedArg (Pattern' a))
    -> [Arg (Pattern' a)] -> [NamedArg (Pattern' a)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Pattern' a -> Named NamedName (Pattern' a))
    -> Arg (Pattern' a) -> NamedArg (Pattern' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern' a -> Named NamedName (Pattern' a)
    forall a name. a -> Named name a
    unnamed) ([Arg (Pattern' a)] -> Pattern' a)
    -> TCMT IO [Arg (Pattern' a)] -> TCM (Pattern' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Arg Term] -> TCMT IO [Arg (Pattern' a)]
    forall a b. TermToPattern a b => a -> TCM b
    termToPattern ([Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    args)
        Var Int
    i []    -> Pattern' a -> TCM (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> TCM (Pattern' a)) -> Pattern' a -> TCM (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Int -> Pattern' a
    forall a. DeBruijn a => Int -> a
    deBruijnVar Int
    i
        Lit Literal
    l       -> Pattern' a -> TCM (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> TCM (Pattern' a)) -> Pattern' a -> TCM (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Literal -> Pattern' a
    forall a. Literal -> Pattern' a
    litP Literal
    l
        Term
    t           -> Pattern' a -> TCM (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> TCM (Pattern' a)) -> Pattern' a -> TCM (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    t

    dotPatternsToPatterns :: forall a. (DeBruijn (Pattern' a))
                          => Pattern' a -> TCM (Pattern' a)
    dotPatternsToPatterns :: forall a. DeBruijn (Pattern' a) => Pattern' a -> TCM (Pattern' a)
    dotPatternsToPatterns = (Pattern' a -> TCMT IO (Pattern' a))
    -> Pattern' a -> TCMT IO (Pattern' a)
    forall a b (m :: * -> *).
    (PatternLike a b, Monad m) =>
    (Pattern' a -> m (Pattern' a)) -> b -> m b
    postTraversePatternM Pattern' a -> TCMT IO (Pattern' a)
    dotToPat
      where
        dotToPat :: Pattern' a -> TCM (Pattern' a)
        dotToPat :: Pattern' a -> TCMT IO (Pattern' a)
    dotToPat = \case
          DotP PatternInfo
    o Term
    t -> Term -> TCMT IO (Pattern' a)
    forall a b. TermToPattern a b => a -> TCM b
    termToPattern Term
    t
          Pattern' a
    p        -> Pattern' a -> TCMT IO (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p