    -- | 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.Functor
    import Data.Void

    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract.Pattern
    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.Pretty
    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     -> TypeError -> m Pattern
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    NegativeLiteralInPattern  -- Andreas, issue #2365, negative literals not yet supported.
        | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    20    -> TypeError -> m Pattern
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    LiteralTooBig
        | Bool
    otherwise -> do
          z <- BuiltinId -> m QName
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m QName
    getBuiltinName_ BuiltinId
    builtinZero
          s <- getBuiltinName_ builtinSuc
          let r     = PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    info
          let 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
    z) []
              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
    s) [Pattern -> NamedArg Pattern
    forall a. a -> NamedArg a
    defaultNamedArg Pattern
    p]
              cinfo = ConOrigin -> PatInfo -> ConPatLazy -> ConPatInfo
    A.ConPatInfo ConOrigin
    ConOCon PatInfo
    info ConPatLazy
    ConPatEager
          return $ foldr ($) zero $ List.genericReplicate n suc
      Pattern
    p -> Pattern -> m Pattern
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p

    -- | 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' (ADotT (Pattern' e)))
    -> TCMT IO (Pattern' (ADotT (Pattern' e)))
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange PatInfo
    i (TCMT IO (Pattern' (ADotT (Pattern' e)))
     -> TCMT IO (Pattern' (ADotT (Pattern' e))))
    -> TCMT IO (Pattern' (ADotT (Pattern' e)))
    -> TCMT IO (Pattern' (ADotT (Pattern' e)))
    forall a b. (a -> b) -> a -> b
    $ do
        (ns, 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.
        mapM_ raiseWarningsOnUsage $ A.unAmbQ x

        -- Must expand arguments before instantiating otherwise pattern
        -- synonyms could get into dot patterns (which is __IMPOSSIBLE__).
        p <- expandPatternSynonyms' (vacuous p :: A.Pattern' e)

        reportSDoc "scope.patsyn" 80 $ vcat
          [ "calling insertImplicitPatSynArgs"
          , "- patsyn parameters: " <+> (text . show) (killRange ns)
          , "- patsyn arguments:  " <+> (text . show) (fmap (fmap void) as)
          ]
        case A.insertImplicitPatSynArgs (\ Hiding
    _h Range
    r -> PatInfo -> Pattern' e
    forall e. PatInfo -> Pattern' e
    A.WildP (Range -> PatInfo
    PatRange Range
    r)) (getRange x) ns as of
          Maybe ([(Name, Pattern' e)], [WithHiding 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)]
    _, WithHiding Name
    _:[WithHiding 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 a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> f a -> f (f 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'