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

    module Agda.TypeChecking.Patterns.Abstract where

    import Control.Monad.Except

    import qualified Data.List as List
    import Data.Void

    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract.Pattern
    import Agda.Syntax.Abstract.Views
    import Agda.Syntax.Concrete (FieldAssignment')
    import Agda.Syntax.Common
    import Agda.Syntax.Info as A
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Literal
    import Agda.Syntax.Position

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Warnings (raiseWarningsOnUsage)

    import Agda.Utils.Impossible

    -- | Expand literal integer pattern into suc/zero constructor patterns.
    --
    expandLitPattern
      :: (MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m)
      => A.Pattern -> m A.Pattern
    expandLitPattern :: forall (m :: * -> *).
    (MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m) =>
    Pattern -> m Pattern
    expandLitPattern = \case
      A.LitP PatInfo
    info (LitNat Integer
    n)
        | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0     -> m Pattern
    forall {a}. m a
    negLit -- Andreas, issue #2365, negative literals not yet supported.
        | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    20    -> m Pattern
    forall {a}. m a
    tooBig
        | Bool
    otherwise -> do
          Con ConHead
    z ConInfo
    _ Elims
    _ <- m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primZero
          Con ConHead
    s ConInfo
    _ Elims
    _ <- m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSuc
          let r :: Range
    r     = PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    info
          let zero :: Pattern
    zero  = ConPatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.ConP ConPatInfo
    cinfo (QName -> AmbiguousQName
    unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
    forall a b. (a -> b) -> a -> b
    $ Range -> QName -> QName
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r (QName -> QName) -> QName -> QName
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    z) []
              suc :: Pattern -> Pattern
    suc Pattern
    p = ConPatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.ConP ConPatInfo
    cinfo (QName -> AmbiguousQName
    unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
    forall a b. (a -> b) -> a -> b
    $ Range -> QName -> QName
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r (QName -> QName) -> QName -> QName
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    s) [Pattern -> NamedArg Pattern
    forall a. a -> NamedArg a
    defaultNamedArg Pattern
    p]
              cinfo :: ConPatInfo
    cinfo = ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
    A.ConPatInfo ConInfo
    ConOCon PatInfo
    info ConPatLazy
    ConPatEager
          Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ ((Pattern -> Pattern) -> Pattern -> Pattern)
    -> Pattern -> [Pattern -> Pattern] -> Pattern
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Pattern -> Pattern) -> Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    ($) Pattern
    zero ([Pattern -> Pattern] -> Pattern)
    -> [Pattern -> Pattern] -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Integer -> (Pattern -> Pattern) -> [Pattern -> Pattern]
    forall i a. Integral i => i -> a -> [a]
    List.genericReplicate Integer
    n Pattern -> Pattern
    suc
      Pattern
    p -> Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p

      where
        tooBig :: m a
    tooBig = TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Matching on natural number literals is done by expanding " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
          [Char]
    "the literal to the corresponding constructor pattern, so " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
          [Char]
    "you probably don't want to do it this way."
        negLit :: m a
    negLit = TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Negative literals are not supported in patterns"

    -- | Expand away (deeply) all pattern synonyms in a pattern.

    -- Unfortunately, the more general type signature
    --
    --   expandPatternSynonyms :: forall a p . APatternLike a p => p -> TCM p
    --
    -- is rejected by GHC 7.10
    --
    --   Could not deduce (APatternLike A.Expr p)
    --     arising from a use of ‘postTraverseAPatternM’
    --
    -- I am mystified (Andreas, 2017-07-27)

    -- expandPatternSynonyms :: forall a p . APatternLike a p => p -> TCM p

    -- As a workaround, we define this function only for a = A.Exp, p = A.Pattern'
    -- and keep the type class ExpandPatternSynonyms (which would otherwise be superfluous).

    expandPatternSynonyms' :: forall e. A.Pattern' e -> TCM (A.Pattern' e)
    expandPatternSynonyms' :: forall e. Pattern' e -> TCM (Pattern' e)
    expandPatternSynonyms' = (Pattern' (ADotT (Pattern' e))
     -> TCMT IO (Pattern' (ADotT (Pattern' e))))
    -> Pattern' e -> TCMT IO (Pattern' e)
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    postTraverseAPatternM ((Pattern' (ADotT (Pattern' e))
      -> TCMT IO (Pattern' (ADotT (Pattern' e))))
     -> Pattern' e -> TCMT IO (Pattern' e))
    -> (Pattern' (ADotT (Pattern' e))
        -> TCMT IO (Pattern' (ADotT (Pattern' e))))
    -> Pattern' e
    -> TCMT IO (Pattern' e)
    forall a b. (a -> b) -> a -> b
    $ \case

      A.PatternSynP PatInfo
    i AmbiguousQName
    x NAPs (ADotT (Pattern' e))
    as -> PatInfo -> TCMT IO (Pattern' e) -> TCMT IO (Pattern' e)
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange PatInfo
    i (TCMT IO (Pattern' e) -> TCMT IO (Pattern' e))
    -> TCMT IO (Pattern' e) -> TCMT IO (Pattern' e)
    forall a b. (a -> b) -> a -> b
    $ do
        ([Arg Name]
    ns, Pattern' Void
    p) <- KillRangeT PatternSynDefn
    forall a. KillRange a => KillRangeT a
    killRange KillRangeT PatternSynDefn
    -> TCMT IO PatternSynDefn -> TCMT IO PatternSynDefn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> AmbiguousQName -> TCMT IO PatternSynDefn
    lookupPatternSyn AmbiguousQName
    x

        -- Andreas, 2020-02-11, issue #3734
        -- If lookup of ambiguous pattern synonym was successful,
        -- we are justified to complain if one of the definitions
        -- involved in the resolution is tagged with a warning.
        -- This is less than optimal, since we do not rule out
        -- the invalid alternatives by typing, but we cannot do
        -- better here.
        (QName -> TCMT IO ()) -> NonEmpty QName -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ QName -> TCMT IO ()
    forall (m :: * -> *).
    (MonadWarning m, ReadTCState m) =>
    QName -> m ()
    raiseWarningsOnUsage (NonEmpty QName -> TCMT IO ()) -> NonEmpty QName -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ AmbiguousQName -> NonEmpty QName
    A.unAmbQ AmbiguousQName
    x

        -- Must expand arguments before instantiating otherwise pattern
        -- synonyms could get into dot patterns (which is __IMPOSSIBLE__).
        Pattern' e
    p <- Pattern' e -> TCMT IO (Pattern' e)
    forall e. Pattern' e -> TCM (Pattern' e)
    expandPatternSynonyms' (Pattern' Void -> Pattern' e
    forall (f :: * -> *) a. Functor f => f Void -> f a
    vacuous Pattern' Void
    p :: A.Pattern' e)

        case (Range -> Pattern' e)
    -> Range
    -> [Arg Name]
    -> [NamedArg (Pattern' e)]
    -> Maybe ([(Name, Pattern' e)], [Arg Name])
    forall a.
    HasRange a =>
    (Range -> a)
    -> Range
    -> [Arg Name]
    -> [NamedArg a]
    -> Maybe ([(Name, a)], [Arg Name])
    A.insertImplicitPatSynArgs (PatInfo -> Pattern' e
    forall e. PatInfo -> Pattern' e
    A.WildP (PatInfo -> Pattern' e)
    -> (Range -> PatInfo) -> Range -> Pattern' e
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> PatInfo
    PatRange) (AmbiguousQName -> Range
    forall a. HasRange a => a -> Range
    getRange AmbiguousQName
    x) [Arg Name]
    ns [NamedArg (Pattern' e)]
    NAPs (ADotT (Pattern' e))
    as of
          Maybe ([(Name, Pattern' e)], [Arg Name])
    Nothing       -> TypeError -> TCMT IO (Pattern' e)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO (Pattern' e))
    -> TypeError -> TCMT IO (Pattern' e)
    forall a b. (a -> b) -> a -> b
    $ AmbiguousQName -> TypeError
    BadArgumentsToPatternSynonym AmbiguousQName
    x
          Just ([(Name, Pattern' e)]
    _, Arg Name
    _:[Arg Name]
    _) -> TypeError -> TCMT IO (Pattern' e)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO (Pattern' e))
    -> TypeError -> TCMT IO (Pattern' e)
    forall a b. (a -> b) -> a -> b
    $ AmbiguousQName -> TypeError
    TooFewArgumentsToPatternSynonym AmbiguousQName
    x
          Just ([(Name, Pattern' e)]
    s, [])  -> do
            let subE :: p -> a
    subE p
    _ = a
    forall a. HasCallStack => a
    __IMPOSSIBLE__   -- No dot patterns in p
            Pattern' e -> TCMT IO (Pattern' e)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' e -> TCMT IO (Pattern' e))
    -> Pattern' e -> TCMT IO (Pattern' e)
    forall a b. (a -> b) -> a -> b
    $ Range -> Pattern' e -> Pattern' e
    forall a. SetRange a => Range -> a -> a
    setRange (PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    i) (Pattern' e -> Pattern' e) -> Pattern' e -> Pattern' e
    forall a b. (a -> b) -> a -> b
    $ (e -> e) -> [(Name, Pattern' e)] -> Pattern' e -> Pattern' e
    forall e.
    (e -> e) -> [(Name, Pattern' e)] -> Pattern' e -> Pattern' e
    substPattern' e -> e
    forall {p} {a}. p -> a
    subE [(Name, Pattern' e)]
    s Pattern' e
    p

      Pattern' (ADotT (Pattern' e))
    p -> Pattern' e -> TCMT IO (Pattern' e)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' e
    Pattern' (ADotT (Pattern' e))
    p

    class ExpandPatternSynonyms a where
      expandPatternSynonyms :: a -> TCM a

      default expandPatternSynonyms
        :: (Traversable f, ExpandPatternSynonyms b, f b ~ a) => a -> TCM a
      expandPatternSynonyms = (b -> TCMT IO b) -> f b -> TCMT IO (f b)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse b -> TCMT IO b
    forall a. ExpandPatternSynonyms a => a -> TCM a
    expandPatternSynonyms

    instance ExpandPatternSynonyms a => ExpandPatternSynonyms (Maybe a)
    instance ExpandPatternSynonyms a => ExpandPatternSynonyms [a]
    instance ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a)
    instance ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a)
    instance ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a)

    instance ExpandPatternSynonyms (A.Pattern' e) where
      expandPatternSynonyms :: Pattern' e -> TCM (Pattern' e)
    expandPatternSynonyms = Pattern' e -> TCM (Pattern' e)
    forall e. Pattern' e -> TCM (Pattern' e)
    expandPatternSynonyms'