    -- | Tools for patterns in concrete syntax.

    module Agda.Syntax.Concrete.Pattern where

    import Control.Applicative ( liftA2 )
    import Control.Arrow ( first )
    import Control.Monad ( (>=>) )
    import Control.Monad.Identity

    import Data.Monoid ( Any(..), Endo(..), Sum(..) )

    import Agda.Syntax.Common
    import Agda.Syntax.Concrete

    import Agda.Utils.AffineHole
    import Agda.Utils.Functor
    import Agda.Utils.Impossible
    import Agda.Utils.List
    import Agda.Utils.List1  ( List1, pattern (:|) )
    import Agda.Utils.List2  ( List2 )
    import Agda.Utils.Maybe
    import Agda.Utils.Singleton
    import qualified Agda.Utils.List1 as List1

    -- | Check for ellipsis @...@.

    class IsEllipsis a where
      isEllipsis :: a -> Bool

    -- | Is the pattern just @...@?
    instance IsEllipsis Pattern where
      isEllipsis :: Pattern -> Bool
    isEllipsis = \case
        EllipsisP{}         -> Bool
    True
        ParenP Range
    _ Pattern
    p          -> Pattern -> Bool
    forall a. IsEllipsis a => a -> Bool
    isEllipsis Pattern
    p
        Pattern
    _ -> Bool
    False

    -- | Has the lhs an occurrence of the ellipsis @...@?

    class HasEllipsis a where
      hasEllipsis :: a -> Bool

    instance HasEllipsis Pattern where
      hasEllipsis :: Pattern -> Bool
    hasEllipsis Pattern
    p =
        case Pattern -> AffineHole Pattern Pattern
    forall p. CPatternLike p => p -> AffineHole Pattern p
    hasEllipsis' Pattern
    p of
          ZeroHoles Pattern
    _ -> Bool
    False
          OneHole Pattern -> Pattern
    _ Pattern
    _ -> Bool
    True
          AffineHole Pattern Pattern
    ManyHoles   -> Bool
    True

    -- | Does the lhs contain an ellipsis?
    instance HasEllipsis LHS where
      hasEllipsis :: LHS -> Bool
    hasEllipsis (LHS Pattern
    p [RewriteEqn]
    _ [WithExpr]
    _) = Pattern -> Bool
    forall a. HasEllipsis a => a -> Bool
    hasEllipsis Pattern
    p
      -- clauses that are already expanded don't have an ellipsis

    -- | Check for with-pattern @| p@.

    class IsWithP p where
      isWithP :: p -> Maybe p

      default isWithP :: (IsWithP q, Decoration f, f q ~ p) => p -> Maybe p
      isWithP = (q -> Maybe q) -> f q -> Maybe (f q)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Decoration t, Functor m) =>
    (a -> m b) -> t a -> m (t b)
    traverseF q -> Maybe q
    forall p. IsWithP p => p -> Maybe p
    isWithP

    instance IsWithP Pattern where
      isWithP :: Pattern -> Maybe Pattern
    isWithP = \case
        WithP Range
    _ Pattern
    p           -> Pattern -> Maybe Pattern
    forall a. a -> Maybe a
    Just Pattern
    p
        ParenP Range
    _ Pattern
    p          -> Pattern -> Maybe Pattern
    forall p. IsWithP p => p -> Maybe p
    isWithP Pattern
    p
        Pattern
    _ -> Maybe Pattern
    forall a. Maybe a
    Nothing

    instance IsWithP p => IsWithP (Arg p) where
    instance IsWithP p => IsWithP (Named n p) where

    -- * LHS manipulation (see also ''Agda.Syntax.Abstract.Pattern'')

    -- | The next patterns are ...
    --
    -- (This view discards 'PatInfo'.)
    data LHSPatternView
      = LHSAppP  [NamedArg Pattern]
          -- ^ Application patterns (non-empty list).
      | LHSWithP [Pattern]
          -- ^ With patterns (non-empty list).
          --   These patterns are not prefixed with 'WithP'.

    -- | Construct the 'LHSPatternView' of the given list (if not empty).
    --
    -- Return the view and the remaining patterns.

    lhsPatternView :: [NamedArg Pattern] -> Maybe (LHSPatternView, [NamedArg Pattern])
    lhsPatternView :: [NamedArg Pattern] -> Maybe (LHSPatternView, [NamedArg Pattern])
    lhsPatternView [] = Maybe (LHSPatternView, [NamedArg Pattern])
    forall a. Maybe a
    Nothing
    lhsPatternView (NamedArg Pattern
    p0 : [NamedArg Pattern]
    ps) =
      case NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg NamedArg Pattern
    p0 of
        WithP Range
    _i Pattern
    p   -> (LHSPatternView, [NamedArg Pattern])
    -> Maybe (LHSPatternView, [NamedArg Pattern])
    forall a. a -> Maybe a
    Just ([Pattern] -> LHSPatternView
    LHSWithP (Pattern
    p Pattern -> [Pattern] -> [Pattern]
    forall a. a -> [a] -> [a]
    : (NamedArg Pattern -> Pattern) -> [NamedArg Pattern] -> [Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg [NamedArg Pattern]
    ps1), [NamedArg Pattern]
    ps2)
          where
          ([NamedArg Pattern]
    ps1, [NamedArg Pattern]
    ps2) = (NamedArg Pattern -> Maybe (NamedArg Pattern))
    -> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
    forall a b. (a -> Maybe b) -> [a] -> (Prefix b, [a])
    spanJust NamedArg Pattern -> Maybe (NamedArg Pattern)
    forall p. IsWithP p => p -> Maybe p
    isWithP [NamedArg Pattern]
    ps
        -- If the next pattern is an application pattern, collect more of these
        Pattern
    _ -> (LHSPatternView, [NamedArg Pattern])
    -> Maybe (LHSPatternView, [NamedArg Pattern])
    forall a. a -> Maybe a
    Just ([NamedArg Pattern] -> LHSPatternView
    LHSAppP (NamedArg Pattern
    p0 NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. a -> [a] -> [a]
    : [NamedArg Pattern]
    ps1), [NamedArg Pattern]
    ps2)
          where
          ([NamedArg Pattern]
    ps1, [NamedArg Pattern]
    ps2) = (NamedArg Pattern -> Bool)
    -> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (Maybe (NamedArg Pattern) -> Bool
    forall a. Maybe a -> Bool
    isNothing (Maybe (NamedArg Pattern) -> Bool)
    -> (NamedArg Pattern -> Maybe (NamedArg Pattern))
    -> NamedArg Pattern
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Pattern -> Maybe (NamedArg Pattern)
    forall p. IsWithP p => p -> Maybe p
    isWithP) [NamedArg Pattern]
    ps

    -- | Add applicative patterns (non-projection / non-with patterns) to the right.
    lhsCoreApp :: LHSCore -> [NamedArg Pattern] -> LHSCore
    lhsCoreApp :: LHSCore -> [NamedArg Pattern] -> LHSCore
    lhsCoreApp LHSCore
    core [NamedArg Pattern]
    ps = LHSCore
    core { lhsPats :: [NamedArg Pattern]
    lhsPats = LHSCore -> [NamedArg Pattern]
    lhsPats LHSCore
    core [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg Pattern]
    ps }

    -- | Add with-patterns to the right.
    lhsCoreWith :: LHSCore -> [Pattern] -> LHSCore
    lhsCoreWith :: LHSCore -> [Pattern] -> LHSCore
    lhsCoreWith (LHSWith LHSCore
    core [Pattern]
    wps []) [Pattern]
    wps' = LHSCore -> [Pattern] -> [NamedArg Pattern] -> LHSCore
    LHSWith LHSCore
    core ([Pattern]
    wps [Pattern] -> [Pattern] -> [Pattern]
    forall a. [a] -> [a] -> [a]
    ++ [Pattern]
    wps') []
    lhsCoreWith LHSCore
    core                  [Pattern]
    wps' = LHSCore -> [Pattern] -> [NamedArg Pattern] -> LHSCore
    LHSWith LHSCore
    core [Pattern]
    wps' []

    -- | Append patterns to 'LHSCore', separating with patterns from the rest.
    lhsCoreAddSpine :: LHSCore -> [NamedArg Pattern] -> LHSCore
    lhsCoreAddSpine :: LHSCore -> [NamedArg Pattern] -> LHSCore
    lhsCoreAddSpine LHSCore
    core [NamedArg Pattern]
    ps0 =
      -- Recurse on lhsPatternView until no patterns left.
      case [NamedArg Pattern] -> Maybe (LHSPatternView, [NamedArg Pattern])
    lhsPatternView [NamedArg Pattern]
    ps0 of
        Maybe (LHSPatternView, [NamedArg Pattern])
    Nothing       -> LHSCore
    core
        Just (LHSAppP  [NamedArg Pattern]
    ps , [NamedArg Pattern]
    ps') -> LHSCore -> [NamedArg Pattern] -> LHSCore
    lhsCoreApp  LHSCore
    core [NamedArg Pattern]
    ps  LHSCore -> [NamedArg Pattern] -> LHSCore
    `lhsCoreAddSpine` [NamedArg Pattern]
    ps'
        Just (LHSWithP [Pattern]
    wps, [NamedArg Pattern]
    ps') -> LHSCore -> [Pattern] -> LHSCore
    lhsCoreWith LHSCore
    core [Pattern]
    wps LHSCore -> [NamedArg Pattern] -> LHSCore
    `lhsCoreAddSpine` [NamedArg Pattern]
    ps'

    -- | Modify the 'Pattern' component in 'LHS'.
    mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS
    mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS
    mapLhsOriginalPattern Pattern -> Pattern
    f lhs :: LHS
    lhs@LHS{ lhsOriginalPattern :: LHS -> Pattern
    lhsOriginalPattern = Pattern
    p } =
      LHS
    lhs { lhsOriginalPattern :: Pattern
    lhsOriginalPattern = Pattern -> Pattern
    f Pattern
    p }

    -- | Effectfully modify the 'Pattern' component in 'LHS'.
    mapLhsOriginalPatternM :: (Functor m, Applicative m) => (Pattern -> m Pattern) -> LHS -> m LHS
    mapLhsOriginalPatternM :: forall (m :: * -> *).
    (Functor m, Applicative m) =>
    (Pattern -> m Pattern) -> LHS -> m LHS
    mapLhsOriginalPatternM Pattern -> m Pattern
    f lhs :: LHS
    lhs@LHS{ lhsOriginalPattern :: LHS -> Pattern
    lhsOriginalPattern = Pattern
    p } = Pattern -> m Pattern
    f Pattern
    p m Pattern -> (Pattern -> LHS) -> m LHS
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Pattern
    p' ->
      LHS
    lhs { lhsOriginalPattern :: Pattern
    lhsOriginalPattern = Pattern
    p' }

    -- | Does the LHS contain projection patterns?
    hasCopatterns :: LHSCore -> Bool
    hasCopatterns :: LHSCore -> Bool
    hasCopatterns = \case
      LHSHead{}     -> Bool
    False
      LHSProj{}     -> Bool
    True
      LHSWith LHSCore
    h [Pattern]
    _ [NamedArg Pattern]
    _ -> LHSCore -> Bool
    hasCopatterns LHSCore
    h
      LHSEllipsis{} -> Bool
    False

    -- * Generic fold

    -- | Generic pattern traversal.
    --
    -- See 'Agda.Syntax.Abstract.Pattern.APatternLike'.

    class CPatternLike p where

      -- | Fold pattern.
      foldrCPattern
        :: Monoid m
        => (Pattern -> m -> m)
             -- ^ Combine a pattern and the value computed from its subpatterns.
        -> p -> m

      default foldrCPattern
        :: (Monoid m, Foldable f, CPatternLike q, f q ~ p)
        => (Pattern -> m -> m) -> p -> m
      foldrCPattern = (q -> m) -> f q -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((q -> m) -> f q -> m)
    -> ((Pattern -> m -> m) -> q -> m)
    -> (Pattern -> m -> m)
    -> f q
    -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern -> m -> m) -> q -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern

      -- | Traverse pattern with option of post-traversal modification.
      traverseCPatternA :: (Applicative m, Functor m)
          => (Pattern -> m Pattern -> m Pattern)
             -- ^ Combine a pattern and the its recursively computed version.
          -> p -> m p

      default traverseCPatternA :: (Traversable f, CPatternLike q, f q ~ p, Applicative m, Functor m)
          => (Pattern -> m Pattern -> m Pattern)
          -> p -> m p
      traverseCPatternA = (q -> m q) -> f q -> m (f q)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((q -> m q) -> f q -> m (f q))
    -> ((Pattern -> m Pattern -> m Pattern) -> q -> m q)
    -> (Pattern -> m Pattern -> m Pattern)
    -> f q
    -> m (f q)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern -> m Pattern -> m Pattern) -> q -> m q
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA

      -- | Traverse pattern.
      traverseCPatternM
        :: Monad m => (Pattern -> m Pattern)  -- ^ @pre@: Modification before recursion.
        -> (Pattern -> m Pattern)  -- ^ @post@: Modification after recursion.
        -> p -> m p

      default traverseCPatternM
        :: (Traversable f, CPatternLike q, f q ~ p, Monad m)
        => (Pattern -> m Pattern)
        -> (Pattern -> m Pattern)
        -> p -> m p
      traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post = (q -> m q) -> f q -> m (f q)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((q -> m q) -> f q -> m (f q)) -> (q -> m q) -> f q -> m (f q)
    forall a b. (a -> b) -> a -> b
    $ (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> q -> m q
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post

    instance CPatternLike Pattern where
      foldrCPattern :: forall m. Monoid m => (Pattern -> m -> m) -> Pattern -> m
    foldrCPattern Pattern -> m -> m
    f Pattern
    p0 = Pattern -> m -> m
    f Pattern
    p0 (m -> m) -> m -> m
    forall a b. (a -> b) -> a -> b
    $
        case Pattern
    p0 of
          -- Recursive cases:
          AppP Pattern
    p NamedArg Pattern
    ps       -> (Pattern -> m -> m) -> (Pattern, NamedArg Pattern) -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern Pattern -> m -> m
    f (Pattern
    p, NamedArg Pattern
    ps)
          RawAppP Range
    _ List2 Pattern
    ps    -> (Pattern -> m -> m) -> List2 Pattern -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern Pattern -> m -> m
    f List2 Pattern
    ps
          OpAppP Range
    _ QName
    _ Set Name
    _ [NamedArg Pattern]
    ps -> (Pattern -> m -> m) -> [NamedArg Pattern] -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern Pattern -> m -> m
    f [NamedArg Pattern]
    ps
          HiddenP Range
    _ Named NamedName Pattern
    ps    -> (Pattern -> m -> m) -> Named NamedName Pattern -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern Pattern -> m -> m
    f Named NamedName Pattern
    ps
          InstanceP Range
    _ Named NamedName Pattern
    ps  -> (Pattern -> m -> m) -> Named NamedName Pattern -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern Pattern -> m -> m
    f Named NamedName Pattern
    ps
          ParenP Range
    _ Pattern
    p      -> (Pattern -> m -> m) -> Pattern -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern Pattern -> m -> m
    f Pattern
    p
          AsP Range
    _ Name
    _ Pattern
    p       -> (Pattern -> m -> m) -> Pattern -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern Pattern -> m -> m
    f Pattern
    p
          WithP Range
    _ Pattern
    p       -> (Pattern -> m -> m) -> Pattern -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern Pattern -> m -> m
    f Pattern
    p
          RecP Range
    _ [FieldAssignment' Pattern]
    ps       -> (Pattern -> m -> m) -> [FieldAssignment' Pattern] -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern Pattern -> m -> m
    f [FieldAssignment' Pattern]
    ps
          EllipsisP Range
    _ Maybe Pattern
    mp  -> (Pattern -> m -> m) -> Maybe Pattern -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern Pattern -> m -> m
    f Maybe Pattern
    mp
          -- Nonrecursive cases:
          IdentP QName
    _        -> m
    forall a. Monoid a => a
    mempty
          WildP Range
    _         -> m
    forall a. Monoid a => a
    mempty
          DotP Range
    _ Expr
    _        -> m
    forall a. Monoid a => a
    mempty
          AbsurdP Range
    _       -> m
    forall a. Monoid a => a
    mempty
          LitP Range
    _ Literal
    _        -> m
    forall a. Monoid a => a
    mempty
          QuoteP Range
    _        -> m
    forall a. Monoid a => a
    mempty
          EqualP Range
    _ [(Expr, Expr)]
    _      -> m
    forall a. Monoid a => a
    mempty

      traverseCPatternA :: forall (m :: * -> *).
    (Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f Pattern
    p0 = Pattern -> m Pattern -> m Pattern
    f Pattern
    p0 (m Pattern -> m Pattern) -> m Pattern -> m Pattern
    forall a b. (a -> b) -> a -> b
    $ case Pattern
    p0 of
          -- Recursive cases:
          AppP        Pattern
    p NamedArg Pattern
    ps    -> (Pattern -> NamedArg Pattern -> Pattern)
    -> m Pattern -> m (NamedArg Pattern) -> m Pattern
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 Pattern -> NamedArg Pattern -> Pattern
    AppP ((Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f Pattern
    p) ((Pattern -> m Pattern -> m Pattern)
    -> NamedArg Pattern -> m (NamedArg Pattern)
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f NamedArg Pattern
    ps)
          RawAppP   Range
    r List2 Pattern
    ps      -> Range -> List2 Pattern -> Pattern
    RawAppP Range
    r     (List2 Pattern -> Pattern) -> m (List2 Pattern) -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern -> m Pattern)
    -> List2 Pattern -> m (List2 Pattern)
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f List2 Pattern
    ps
          OpAppP    Range
    r QName
    x Set Name
    xs [NamedArg Pattern]
    ps -> Range -> QName -> Set Name -> [NamedArg Pattern] -> Pattern
    OpAppP Range
    r QName
    x Set Name
    xs ([NamedArg Pattern] -> Pattern)
    -> m [NamedArg Pattern] -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern -> m Pattern)
    -> [NamedArg Pattern] -> m [NamedArg Pattern]
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f [NamedArg Pattern]
    ps
          HiddenP   Range
    r Named NamedName Pattern
    p       -> Range -> Named NamedName Pattern -> Pattern
    HiddenP Range
    r     (Named NamedName Pattern -> Pattern)
    -> m (Named NamedName Pattern) -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern -> m Pattern)
    -> Named NamedName Pattern -> m (Named NamedName Pattern)
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f Named NamedName Pattern
    p
          InstanceP Range
    r Named NamedName Pattern
    p       -> Range -> Named NamedName Pattern -> Pattern
    InstanceP Range
    r   (Named NamedName Pattern -> Pattern)
    -> m (Named NamedName Pattern) -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern -> m Pattern)
    -> Named NamedName Pattern -> m (Named NamedName Pattern)
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f Named NamedName Pattern
    p
          ParenP    Range
    r Pattern
    p       -> Range -> Pattern -> Pattern
    ParenP Range
    r      (Pattern -> Pattern) -> m Pattern -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f Pattern
    p
          AsP       Range
    r Name
    x Pattern
    p     -> Range -> Name -> Pattern -> Pattern
    AsP Range
    r Name
    x       (Pattern -> Pattern) -> m Pattern -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f Pattern
    p
          WithP     Range
    r Pattern
    p       -> Range -> Pattern -> Pattern
    WithP Range
    r       (Pattern -> Pattern) -> m Pattern -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f Pattern
    p
          RecP      Range
    r [FieldAssignment' Pattern]
    ps      -> Range -> [FieldAssignment' Pattern] -> Pattern
    RecP Range
    r        ([FieldAssignment' Pattern] -> Pattern)
    -> m [FieldAssignment' Pattern] -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern -> m Pattern)
    -> [FieldAssignment' Pattern] -> m [FieldAssignment' Pattern]
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f [FieldAssignment' Pattern]
    ps
          EllipsisP Range
    r Maybe Pattern
    mp      -> Range -> Maybe Pattern -> Pattern
    EllipsisP Range
    r   (Maybe Pattern -> Pattern) -> m (Maybe Pattern) -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern -> m Pattern)
    -> Maybe Pattern -> m (Maybe Pattern)
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f Maybe Pattern
    mp
          -- Nonrecursive cases:
          IdentP QName
    _        -> Pattern -> m Pattern
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pattern
    p0
          WildP Range
    _         -> Pattern -> m Pattern
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pattern
    p0
          DotP Range
    _ Expr
    _        -> Pattern -> m Pattern
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pattern
    p0
          AbsurdP Range
    _       -> Pattern -> m Pattern
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pattern
    p0
          LitP Range
    _ Literal
    _        -> Pattern -> m Pattern
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pattern
    p0
          QuoteP Range
    _        -> Pattern -> m Pattern
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pattern
    p0
          EqualP Range
    _ [(Expr, Expr)]
    _      -> Pattern -> m Pattern
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pattern
    p0

      traverseCPatternM :: forall (m :: * -> *).
    Monad m =>
    (Pattern -> m Pattern)
    -> (Pattern -> m Pattern) -> Pattern -> m Pattern
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post = Pattern -> m Pattern
    pre (Pattern -> m Pattern)
    -> (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> Pattern -> m Pattern
    recurse (Pattern -> m Pattern)
    -> (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> Pattern -> m Pattern
    post
        where
        recurse :: Pattern -> m Pattern
    recurse Pattern
    p0 = case Pattern
    p0 of
          -- Recursive cases:
          AppP        Pattern
    p NamedArg Pattern
    ps    -> (Pattern -> NamedArg Pattern -> Pattern)
    -> (Pattern, NamedArg Pattern) -> Pattern
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Pattern -> NamedArg Pattern -> Pattern
    AppP  ((Pattern, NamedArg Pattern) -> Pattern)
    -> m (Pattern, NamedArg Pattern) -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern)
    -> (Pattern -> m Pattern)
    -> (Pattern, NamedArg Pattern)
    -> m (Pattern, NamedArg Pattern)
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post (Pattern
    p, NamedArg Pattern
    ps)
          RawAppP   Range
    r List2 Pattern
    ps      -> Range -> List2 Pattern -> Pattern
    RawAppP Range
    r     (List2 Pattern -> Pattern) -> m (List2 Pattern) -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern)
    -> (Pattern -> m Pattern) -> List2 Pattern -> m (List2 Pattern)
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post List2 Pattern
    ps
          OpAppP    Range
    r QName
    x Set Name
    xs [NamedArg Pattern]
    ps -> Range -> QName -> Set Name -> [NamedArg Pattern] -> Pattern
    OpAppP Range
    r QName
    x Set Name
    xs ([NamedArg Pattern] -> Pattern)
    -> m [NamedArg Pattern] -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern)
    -> (Pattern -> m Pattern)
    -> [NamedArg Pattern]
    -> m [NamedArg Pattern]
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post [NamedArg Pattern]
    ps
          HiddenP   Range
    r Named NamedName Pattern
    p       -> Range -> Named NamedName Pattern -> Pattern
    HiddenP Range
    r     (Named NamedName Pattern -> Pattern)
    -> m (Named NamedName Pattern) -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern)
    -> (Pattern -> m Pattern)
    -> Named NamedName Pattern
    -> m (Named NamedName Pattern)
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post Named NamedName Pattern
    p
          InstanceP Range
    r Named NamedName Pattern
    p       -> Range -> Named NamedName Pattern -> Pattern
    InstanceP Range
    r   (Named NamedName Pattern -> Pattern)
    -> m (Named NamedName Pattern) -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern)
    -> (Pattern -> m Pattern)
    -> Named NamedName Pattern
    -> m (Named NamedName Pattern)
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post Named NamedName Pattern
    p
          ParenP    Range
    r Pattern
    p       -> Range -> Pattern -> Pattern
    ParenP Range
    r      (Pattern -> Pattern) -> m Pattern -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern)
    -> (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post Pattern
    p
          AsP       Range
    r Name
    x Pattern
    p     -> Range -> Name -> Pattern -> Pattern
    AsP Range
    r Name
    x       (Pattern -> Pattern) -> m Pattern -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern)
    -> (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post Pattern
    p
          WithP     Range
    r Pattern
    p       -> Range -> Pattern -> Pattern
    WithP Range
    r       (Pattern -> Pattern) -> m Pattern -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern)
    -> (Pattern -> m Pattern) -> Pattern -> m Pattern
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post Pattern
    p
          RecP      Range
    r [FieldAssignment' Pattern]
    ps      -> Range -> [FieldAssignment' Pattern] -> Pattern
    RecP Range
    r        ([FieldAssignment' Pattern] -> Pattern)
    -> m [FieldAssignment' Pattern] -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern)
    -> (Pattern -> m Pattern)
    -> [FieldAssignment' Pattern]
    -> m [FieldAssignment' Pattern]
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post [FieldAssignment' Pattern]
    ps
          EllipsisP Range
    r Maybe Pattern
    mp      -> Range -> Maybe Pattern -> Pattern
    EllipsisP Range
    r   (Maybe Pattern -> Pattern) -> m (Maybe Pattern) -> m Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> m Pattern)
    -> (Pattern -> m Pattern) -> Maybe Pattern -> m (Maybe Pattern)
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post Maybe Pattern
    mp
          -- Nonrecursive cases:
          IdentP QName
    _        -> Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p0
          WildP Range
    _         -> Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p0
          DotP Range
    _ Expr
    _        -> Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p0
          AbsurdP Range
    _       -> Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p0
          LitP Range
    _ Literal
    _        -> Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p0
          QuoteP Range
    _        -> Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p0
          EqualP Range
    _ [(Expr, Expr)]
    _      -> Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p0

    instance (CPatternLike a, CPatternLike b) => CPatternLike (a,b) where
      foldrCPattern :: forall m. Monoid m => (Pattern -> m -> m) -> (a, b) -> m
    foldrCPattern Pattern -> m -> m
    f (a
    p, b
    p') =
        (Pattern -> m -> m) -> a -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern Pattern -> m -> m
    f a
    p m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` (Pattern -> m -> m) -> b -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern Pattern -> m -> m
    f b
    p'

      traverseCPatternA :: forall (m :: * -> *).
    (Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> (a, b) -> m (a, b)
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f (a
    p, b
    p') =
        (a -> b -> (a, b)) -> m a -> m b -> m (a, b)
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 (,)
          ((Pattern -> m Pattern -> m Pattern) -> a -> m a
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f a
    p)
          ((Pattern -> m Pattern -> m Pattern) -> b -> m b
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA Pattern -> m Pattern -> m Pattern
    f b
    p')

      traverseCPatternM :: forall (m :: * -> *).
    Monad m =>
    (Pattern -> m Pattern)
    -> (Pattern -> m Pattern) -> (a, b) -> m (a, b)
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post (a
    p, b
    p') =
        (a -> b -> (a, b)) -> m a -> m b -> m (a, b)
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 (,)
          ((Pattern -> m Pattern) -> (Pattern -> m Pattern) -> a -> m a
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post a
    p)
          ((Pattern -> m Pattern) -> (Pattern -> m Pattern) -> b -> m b
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    post b
    p')

    instance CPatternLike p => CPatternLike (Arg p)
    instance CPatternLike p => CPatternLike (Named n p)
    instance CPatternLike p => CPatternLike [p]
    instance CPatternLike p => CPatternLike (List1 p)
    instance CPatternLike p => CPatternLike (List2 p)
    instance CPatternLike p => CPatternLike (Maybe p)
    instance CPatternLike p => CPatternLike (FieldAssignment' p)

    -- | Compute a value from each subpattern and collect all values in a monoid.

    foldCPattern :: (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
    foldCPattern :: forall p m. (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
    foldCPattern Pattern -> m
    f = (Pattern -> m -> m) -> p -> m
    forall p m.
    (CPatternLike p, Monoid m) =>
    (Pattern -> m -> m) -> p -> m
    foldrCPattern ((Pattern -> m -> m) -> p -> m) -> (Pattern -> m -> m) -> p -> m
    forall a b. (a -> b) -> a -> b
    $ \ Pattern
    p m
    m -> Pattern -> m
    f Pattern
    p m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` m
    m

    -- | Traverse pattern(s) with a modification before the recursive descent.

    preTraverseCPatternM
      :: (CPatternLike p, Monad m)
      => (Pattern -> m Pattern)  -- ^ @pre@: Modification before recursion.
      -> p -> m p
    preTraverseCPatternM :: forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> p -> m p
    preTraverseCPatternM Pattern -> m Pattern
    pre p
    p = (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    pre Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return p
    p

    -- | Traverse pattern(s) with a modification after the recursive descent.

    postTraverseCPatternM
      :: (CPatternLike p, Monad m)
      => (Pattern -> m Pattern)  -- ^ @post@: Modification after recursion.
      -> p -> m p
    postTraverseCPatternM :: forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> p -> m p
    postTraverseCPatternM Pattern -> m Pattern
    post p
    p = (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
    traverseCPatternM Pattern -> m Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern -> m Pattern
    post p
    p

    -- | Map pattern(s) with a modification after the recursive descent.

    mapCPattern :: CPatternLike p => (Pattern -> Pattern) -> p -> p
    mapCPattern :: forall p. CPatternLike p => (Pattern -> Pattern) -> p -> p
    mapCPattern Pattern -> Pattern
    f = Identity p -> p
    forall a. Identity a -> a
    runIdentity (Identity p -> p) -> (p -> Identity p) -> p -> p
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern -> Identity Pattern) -> p -> Identity p
    forall p (m :: * -> *).
    (CPatternLike p, Monad m) =>
    (Pattern -> m Pattern) -> p -> m p
    postTraverseCPatternM (Pattern -> Identity Pattern
    forall a. a -> Identity a
    Identity (Pattern -> Identity Pattern)
    -> (Pattern -> Pattern) -> Pattern -> Identity Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern -> Pattern
    f)

    -- * Specific folds.

    -- | Get all the identifiers in a pattern in left-to-right order.
    --
    -- Implemented using difference lists.
    patternQNames :: CPatternLike p => p -> [QName]
    patternQNames :: forall p. CPatternLike p => p -> [QName]
    patternQNames p
    p = (Pattern -> Endo [QName]) -> p -> Endo [QName]
    forall p m. (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
    foldCPattern Pattern -> Endo [QName]
    f p
    p Endo [QName] -> [QName] -> [QName]
    forall a. Endo a -> a -> a
    `appEndo` []
      where
      f :: Pattern -> Endo [QName]
      f :: Pattern -> Endo [QName]
    f = \case
        IdentP QName
    x       -> ([QName] -> [QName]) -> Endo [QName]
    forall a. (a -> a) -> Endo a
    Endo (QName
    x QName -> [QName] -> [QName]
    forall a. a -> [a] -> [a]
    :)
        OpAppP Range
    _ QName
    x Set Name
    _ [NamedArg Pattern]
    _ -> ([QName] -> [QName]) -> Endo [QName]
    forall a. (a -> a) -> Endo a
    Endo (QName
    x QName -> [QName] -> [QName]
    forall a. a -> [a] -> [a]
    :)
        AsP Range
    _ Name
    x Pattern
    _      -> Endo [QName]
    forall a. Monoid a => a
    mempty  -- x must be a bound name, can't be a constructor!
        AppP Pattern
    _ NamedArg Pattern
    _       -> Endo [QName]
    forall a. Monoid a => a
    mempty
        WithP Range
    _ Pattern
    _      -> Endo [QName]
    forall a. Monoid a => a
    mempty
        RawAppP Range
    _ List2 Pattern
    _    -> Endo [QName]
    forall a. Monoid a => a
    mempty
        HiddenP Range
    _ Named NamedName Pattern
    _    -> Endo [QName]
    forall a. Monoid a => a
    mempty
        ParenP Range
    _ Pattern
    _     -> Endo [QName]
    forall a. Monoid a => a
    mempty
        WildP Range
    _        -> Endo [QName]
    forall a. Monoid a => a
    mempty
        AbsurdP Range
    _      -> Endo [QName]
    forall a. Monoid a => a
    mempty
        DotP Range
    _ Expr
    _       -> Endo [QName]
    forall a. Monoid a => a
    mempty
        LitP Range
    _ Literal
    _       -> Endo [QName]
    forall a. Monoid a => a
    mempty
        QuoteP Range
    _       -> Endo [QName]
    forall a. Monoid a => a
    mempty
        InstanceP Range
    _ Named NamedName Pattern
    _  -> Endo [QName]
    forall a. Monoid a => a
    mempty
        RecP Range
    _ [FieldAssignment' Pattern]
    _       -> Endo [QName]
    forall a. Monoid a => a
    mempty
        EqualP Range
    _ [(Expr, Expr)]
    _     -> Endo [QName]
    forall a. Monoid a => a
    mempty
        EllipsisP Range
    _ Maybe Pattern
    _  -> Endo [QName]
    forall a. Monoid a => a
    mempty

    -- | Get all the identifiers in a pattern in left-to-right order.
    patternNames :: Pattern -> [Name]
    patternNames :: Pattern -> [Name]
    patternNames = (QName -> Name) -> [QName] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> Name
    unqualify ([QName] -> [Name]) -> (Pattern -> [QName]) -> Pattern -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern -> [QName]
    forall p. CPatternLike p => p -> [QName]
    patternQNames

    -- | Does the pattern contain a with-pattern?
    -- (Shortcutting.)
    hasWithPatterns :: CPatternLike p => p -> Bool
    hasWithPatterns :: forall p. CPatternLike p => p -> Bool
    hasWithPatterns = Any -> Bool
    getAny (Any -> Bool) -> (p -> Any) -> p -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern -> Any) -> p -> Any
    forall p m. (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
    foldCPattern (Bool -> Any
    Any (Bool -> Any) -> (Pattern -> Bool) -> Pattern -> Any
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern -> Bool
    isWithPattern)

    -- | Is 'WithP'?
    isWithPattern :: Pattern -> Bool
    isWithPattern :: Pattern -> Bool
    isWithPattern = \case
      WithP{} -> Bool
    True
      Pattern
    _ -> Bool
    False

    -- | Count the number of with-subpatterns in a pattern?
    numberOfWithPatterns :: CPatternLike p => p -> Int
    numberOfWithPatterns :: forall p. CPatternLike p => p -> Int
    numberOfWithPatterns = Sum Int -> Int
    forall a. Sum a -> a
    getSum (Sum Int -> Int) -> (p -> Sum Int) -> p -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern -> Sum Int) -> p -> Sum Int
    forall p m. (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
    foldCPattern (Int -> Sum Int
    forall a. a -> Sum a
    Sum (Int -> Sum Int) -> (Pattern -> Int) -> Pattern -> Sum Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern -> Int
    forall {p}. Num p => Pattern -> p
    f)
      where f :: Pattern -> p
    f Pattern
    p = if Pattern -> Bool
    isWithPattern Pattern
    p then p
    1 else p
    0

    -- | Compute the context in which the ellipsis occurs, if at all.
    --   If there are several occurrences, this is an error.
    --   This only counts ellipsis that haven't already been expanded.
    hasEllipsis' :: CPatternLike p => p -> AffineHole Pattern p
    hasEllipsis' :: forall p. CPatternLike p => p -> AffineHole Pattern p
    hasEllipsis' = (Pattern
     -> AffineHole Pattern Pattern -> AffineHole Pattern Pattern)
    -> p -> AffineHole Pattern p
    forall p (m :: * -> *).
    (CPatternLike p, Applicative m, Functor m) =>
    (Pattern -> m Pattern -> m Pattern) -> p -> m p
    traverseCPatternA ((Pattern
      -> AffineHole Pattern Pattern -> AffineHole Pattern Pattern)
     -> p -> AffineHole Pattern p)
    -> (Pattern
        -> AffineHole Pattern Pattern -> AffineHole Pattern Pattern)
    -> p
    -> AffineHole Pattern p
    forall a b. (a -> b) -> a -> b
    $ \ Pattern
    p AffineHole Pattern Pattern
    mp ->
      case Pattern
    p of
        EllipsisP Range
    _ Maybe Pattern
    Nothing -> (Pattern -> Pattern) -> Pattern -> AffineHole Pattern Pattern
    forall r a. (r -> a) -> r -> AffineHole r a
    OneHole Pattern -> Pattern
    forall a. a -> a
    id Pattern
    p
        Pattern
    _                   -> AffineHole Pattern Pattern
    mp

    reintroduceEllipsis :: ExpandedEllipsis -> Pattern -> Pattern
    reintroduceEllipsis :: ExpandedEllipsis -> Pattern -> Pattern
    reintroduceEllipsis (ExpandedEllipsis Range
    r Int
    k) Pattern
    p | Pattern -> Bool
    forall p. CPatternLike p => p -> Bool
    hasWithPatterns Pattern
    p =
      let ([NamedArg Pattern]
    args, [NamedArg Pattern]
    wargs) = Int
    -> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
    forall p. IsWithP p => Int -> [p] -> ([p], [p])
    splitEllipsis Int
    k ([NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern]))
    -> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
    forall a b. (a -> b) -> a -> b
    $ List1 (NamedArg Pattern) -> [NamedArg Pattern]
    forall a. NonEmpty a -> [a]
    List1.toList (List1 (NamedArg Pattern) -> [NamedArg Pattern])
    -> List1 (NamedArg Pattern) -> [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ Pattern -> List1 (NamedArg Pattern)
    patternAppView Pattern
    p
          (NamedArg Pattern
    hd,[NamedArg Pattern]
    args') = (NamedArg Pattern, [NamedArg Pattern])
    -> Maybe (NamedArg Pattern, [NamedArg Pattern])
    -> (NamedArg Pattern, [NamedArg Pattern])
    forall a. a -> Maybe a -> a
    fromMaybe (NamedArg Pattern, [NamedArg Pattern])
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (NamedArg Pattern, [NamedArg Pattern])
     -> (NamedArg Pattern, [NamedArg Pattern]))
    -> Maybe (NamedArg Pattern, [NamedArg Pattern])
    -> (NamedArg Pattern, [NamedArg Pattern])
    forall a b. (a -> b) -> a -> b
    $ [NamedArg Pattern] -> Maybe (NamedArg Pattern, [NamedArg Pattern])
    forall a. [a] -> Maybe (a, [a])
    uncons [NamedArg Pattern]
    args
          core :: Pattern
    core = (Pattern -> NamedArg Pattern -> Pattern)
    -> Pattern -> [NamedArg Pattern] -> Pattern
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Pattern -> NamedArg Pattern -> Pattern
    AppP (NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg NamedArg Pattern
    hd) [NamedArg Pattern]
    args
      in (Pattern -> NamedArg Pattern -> Pattern)
    -> Pattern -> [NamedArg Pattern] -> Pattern
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Pattern -> NamedArg Pattern -> Pattern
    AppP (Range -> Maybe Pattern -> Pattern
    EllipsisP Range
    r (Maybe Pattern -> Pattern) -> Maybe Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Maybe Pattern
    forall a. a -> Maybe a
    Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
    forall a b. (a -> b) -> a -> b
    $ Pattern
    core) [NamedArg Pattern]
    wargs
    reintroduceEllipsis ExpandedEllipsis
    _ Pattern
    p = Pattern
    p

    splitEllipsis :: (IsWithP p) => Int -> [p] -> ([p],[p])
    splitEllipsis :: forall p. IsWithP p => Int -> [p] -> ([p], [p])
    splitEllipsis Int
    k [] = ([] , [])
    splitEllipsis Int
    k (p
    p:[p]
    ps)
      | Maybe p -> Bool
    forall a. Maybe a -> Bool
    isJust (p -> Maybe p
    forall p. IsWithP p => p -> Maybe p
    isWithP p
    p) = if
          | Int
    k Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0    -> ([] , p
    pp -> [p] -> [p]
    forall a. a -> [a] -> [a]
    :[p]
    ps)
          | Bool
    otherwise -> ([p] -> [p]) -> ([p], [p]) -> ([p], [p])
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first (p
    pp -> [p] -> [p]
    forall a. a -> [a] -> [a]
    :) (([p], [p]) -> ([p], [p])) -> ([p], [p]) -> ([p], [p])
    forall a b. (a -> b) -> a -> b
    $ Int -> [p] -> ([p], [p])
    forall p. IsWithP p => Int -> [p] -> ([p], [p])
    splitEllipsis (Int
    kInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) [p]
    ps
      | Bool
    otherwise = ([p] -> [p]) -> ([p], [p]) -> ([p], [p])
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first (p
    pp -> [p] -> [p]
    forall a. a -> [a] -> [a]
    :) (([p], [p]) -> ([p], [p])) -> ([p], [p]) -> ([p], [p])
    forall a b. (a -> b) -> a -> b
    $ Int -> [p] -> ([p], [p])
    forall p. IsWithP p => Int -> [p] -> ([p], [p])
    splitEllipsis Int
    k [p]
    ps

    ---------------------------------------------------------------------------
    -- * Helpers for pattern and lhs parsing
    ---------------------------------------------------------------------------

    -- | View a pattern @p@ as a list @p0 .. pn@ where @p0@ is the identifier
    --   (in most cases a constructor).
    --
    --  Pattern needs to be parsed already (operators resolved).
    patternAppView :: Pattern -> List1 (NamedArg Pattern)
    patternAppView :: Pattern -> List1 (NamedArg Pattern)
    patternAppView = \case
        AppP Pattern
    p NamedArg Pattern
    arg      -> Pattern -> List1 (NamedArg Pattern)
    patternAppView Pattern
    p List1 (NamedArg Pattern)
    -> [NamedArg Pattern] -> List1 (NamedArg Pattern)
    forall a. List1 a -> [a] -> List1 a
    `List1.appendList` [NamedArg Pattern
    arg]
        OpAppP Range
    _ QName
    x Set Name
    _ [NamedArg Pattern]
    ps -> Pattern -> NamedArg Pattern
    forall a. a -> NamedArg a
    defaultNamedArg (QName -> Pattern
    IdentP QName
    x) NamedArg Pattern -> [NamedArg Pattern] -> List1 (NamedArg Pattern)
    forall a. a -> [a] -> NonEmpty a
    :| [NamedArg Pattern]
    ps
        ParenP Range
    _ Pattern
    p      -> Pattern -> List1 (NamedArg Pattern)
    patternAppView Pattern
    p
        RawAppP Range
    _ List2 Pattern
    _     -> List1 (NamedArg Pattern)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Pattern
    p               -> NamedArg Pattern -> List1 (NamedArg Pattern)
    forall el coll. Singleton el coll => el -> coll
    singleton (NamedArg Pattern -> List1 (NamedArg Pattern))
    -> NamedArg Pattern -> List1 (NamedArg Pattern)
    forall a b. (a -> b) -> a -> b
    $ Pattern -> NamedArg Pattern
    forall a. a -> NamedArg a
    defaultNamedArg Pattern
    p