content: 
  -- | 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 = \case
    A.LitP info (LitNat n)
      | n < 0     -> typeError NegativeLiteralInPattern  -- Andreas, issue #2365, negative literals not yet supported.
      | n > 20    -> typeError LiteralTooBig
      | otherwise -> do
        z <- getBuiltinName_ builtinZero
        s <- getBuiltinName_ builtinSuc
        let r     = getRange info
        let zero  = A.ConP cinfo (unambiguous $ setRange r z) []
            suc p = A.ConP cinfo (unambiguous $ setRange r s) [defaultNamedArg p]
            cinfo = A.ConPatInfo ConOCon info ConPatEager
        return $ foldr ($) zero $ List.genericReplicate n suc
    p -> return 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' = postTraverseAPatternM $ \case
  
    A.PatternSynP i x as -> setCurrentRange i $ do
      (ns, p) <- killRange <$> lookupPatternSyn 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 (\ _h r -> A.WildP (PatRange r)) (getRange x) ns as of
        Nothing       -> typeError $ BadArgumentsToPatternSynonym x
        Just (_, _:_) -> typeError $ TooFewArgumentsToPatternSynonym x
        Just (s, [])  -> do
          let subE _ = __IMPOSSIBLE__   -- No dot patterns in p
          return $ setRange (getRange i) $ substPattern' subE s p
  
    p -> return p
  
  class ExpandPatternSynonyms a where
    expandPatternSynonyms :: a -> TCM a
  
    default expandPatternSynonyms
      :: (Traversable f, ExpandPatternSynonyms b, f b ~ a) => a -> TCM a
    expandPatternSynonyms = traverse 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 = expandPatternSynonyms'
  