    -- | Auxiliary functions to handle patterns in the abstract syntax.
    --
    --   Generic and specific traversals.

    module Agda.Syntax.Abstract.Pattern where

    import Prelude hiding (null)

    import Control.Arrow           ( (***), second )
    import Control.Monad           ( (>=>) )
    import Control.Monad.Identity  ( Identity(..), runIdentity )
    import Control.Applicative     ( liftA2 )

    import Data.Maybe
    import Data.Monoid

    import Agda.Syntax.Abstract as A
    import Agda.Syntax.Common
    import Agda.Syntax.Concrete (FieldAssignment')
    import qualified Agda.Syntax.Concrete as C
    import Agda.Syntax.Concrete.Pattern (IsWithP(..))
    import Agda.Syntax.Info
    import Agda.Syntax.Position

    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.Null

    import Agda.Utils.Impossible

    -- * Generic traversals
    ------------------------------------------------------------------------

    type NAP = NamedArg Pattern

    class MapNamedArgPattern a  where
      mapNamedArgPattern :: (NAP -> NAP) -> a -> a

      default mapNamedArgPattern
         :: (Functor f, MapNamedArgPattern a', a ~ f a') => (NAP -> NAP) -> a -> a
      mapNamedArgPattern = (a' -> a') -> f a' -> f a'
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a' -> a') -> f a' -> f a')
    -> ((NamedArg Pattern -> NamedArg Pattern) -> a' -> a')
    -> (NamedArg Pattern -> NamedArg Pattern)
    -> f a'
    -> f a'
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NamedArg Pattern -> NamedArg Pattern) -> a' -> a'
    forall a.
    MapNamedArgPattern a =>
    (NamedArg Pattern -> NamedArg Pattern) -> a -> a
    mapNamedArgPattern

    instance MapNamedArgPattern NAP where
      mapNamedArgPattern :: (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
    f NamedArg Pattern
    p =
        case NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg NamedArg Pattern
    p of
          -- no sub patterns:
          VarP{}    -> NamedArg Pattern -> NamedArg Pattern
    f NamedArg Pattern
    p
          WildP{}   -> NamedArg Pattern -> NamedArg Pattern
    f NamedArg Pattern
    p
          DotP{}    -> NamedArg Pattern -> NamedArg Pattern
    f NamedArg Pattern
    p
          EqualP{}  -> NamedArg Pattern -> NamedArg Pattern
    f NamedArg Pattern
    p
          LitP{}    -> NamedArg Pattern -> NamedArg Pattern
    f NamedArg Pattern
    p
          AbsurdP{} -> NamedArg Pattern -> NamedArg Pattern
    f NamedArg Pattern
    p
          ProjP{}   -> NamedArg Pattern -> NamedArg Pattern
    f NamedArg Pattern
    p
          -- list of NamedArg subpatterns:
          ConP ConPatInfo
    i AmbiguousQName
    qs NAPs Expr
    ps       -> NamedArg Pattern -> NamedArg Pattern
    f (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern -> Pattern -> NamedArg Pattern
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg Pattern
    p (Pattern -> NamedArg Pattern) -> Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ ConPatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    ConP ConPatInfo
    i AmbiguousQName
    qs (NAPs Expr -> Pattern) -> NAPs Expr -> Pattern
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Pattern -> NamedArg Pattern) -> NAPs Expr -> NAPs Expr
    forall a.
    MapNamedArgPattern a =>
    (NamedArg Pattern -> NamedArg Pattern) -> a -> a
    mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
    f NAPs Expr
    ps
          DefP PatInfo
    i AmbiguousQName
    qs NAPs Expr
    ps       -> NamedArg Pattern -> NamedArg Pattern
    f (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern -> Pattern -> NamedArg Pattern
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg Pattern
    p (Pattern -> NamedArg Pattern) -> Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    DefP PatInfo
    i AmbiguousQName
    qs (NAPs Expr -> Pattern) -> NAPs Expr -> Pattern
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Pattern -> NamedArg Pattern) -> NAPs Expr -> NAPs Expr
    forall a.
    MapNamedArgPattern a =>
    (NamedArg Pattern -> NamedArg Pattern) -> a -> a
    mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
    f NAPs Expr
    ps
          PatternSynP PatInfo
    i AmbiguousQName
    x NAPs Expr
    ps -> NamedArg Pattern -> NamedArg Pattern
    f (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern -> Pattern -> NamedArg Pattern
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg Pattern
    p (Pattern -> NamedArg Pattern) -> Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    PatternSynP PatInfo
    i AmbiguousQName
    x (NAPs Expr -> Pattern) -> NAPs Expr -> Pattern
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Pattern -> NamedArg Pattern) -> NAPs Expr -> NAPs Expr
    forall a.
    MapNamedArgPattern a =>
    (NamedArg Pattern -> NamedArg Pattern) -> a -> a
    mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
    f NAPs Expr
    ps
          -- Pattern subpattern(s):
          -- RecP: we copy the NamedArg info to the subpatterns but discard it after recursion
          RecP PatInfo
    i [FieldAssignment' Pattern]
    fs          -> NamedArg Pattern -> NamedArg Pattern
    f (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern -> Pattern -> NamedArg Pattern
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg Pattern
    p (Pattern -> NamedArg Pattern) -> Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> [FieldAssignment' Pattern] -> Pattern
    forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    RecP PatInfo
    i ([FieldAssignment' Pattern] -> Pattern)
    -> [FieldAssignment' Pattern] -> Pattern
    forall a b. (a -> b) -> a -> b
    $ (FieldAssignment' (NamedArg Pattern) -> FieldAssignment' Pattern)
    -> [FieldAssignment' (NamedArg Pattern)]
    -> [FieldAssignment' Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map ((NamedArg Pattern -> Pattern)
    -> FieldAssignment' (NamedArg Pattern) -> FieldAssignment' Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg) ([FieldAssignment' (NamedArg Pattern)]
     -> [FieldAssignment' Pattern])
    -> [FieldAssignment' (NamedArg Pattern)]
    -> [FieldAssignment' Pattern]
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Pattern -> NamedArg Pattern)
    -> [FieldAssignment' (NamedArg Pattern)]
    -> [FieldAssignment' (NamedArg Pattern)]
    forall a.
    MapNamedArgPattern a =>
    (NamedArg Pattern -> NamedArg Pattern) -> a -> a
    mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
    f ([FieldAssignment' (NamedArg Pattern)]
     -> [FieldAssignment' (NamedArg Pattern)])
    -> [FieldAssignment' (NamedArg Pattern)]
    -> [FieldAssignment' (NamedArg Pattern)]
    forall a b. (a -> b) -> a -> b
    $ (FieldAssignment' Pattern -> FieldAssignment' (NamedArg Pattern))
    -> [FieldAssignment' Pattern]
    -> [FieldAssignment' (NamedArg Pattern)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Pattern -> NamedArg Pattern)
    -> FieldAssignment' Pattern -> FieldAssignment' (NamedArg Pattern)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (NamedArg Pattern -> Pattern -> NamedArg Pattern
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg Pattern
    p)) [FieldAssignment' Pattern]
    fs
          -- AsP: we hand the NamedArg info to the subpattern
          AsP PatInfo
    i BindName
    x Pattern
    p0         -> NamedArg Pattern -> NamedArg Pattern
    f (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ (Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> NamedArg a -> NamedArg b
    updateNamedArg (PatInfo -> BindName -> Pattern -> Pattern
    forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
    AsP PatInfo
    i BindName
    x) (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a.
    MapNamedArgPattern a =>
    (NamedArg Pattern -> NamedArg Pattern) -> a -> a
    mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
    f (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern -> Pattern -> NamedArg Pattern
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg Pattern
    p Pattern
    p0
          -- WithP: like AsP
          WithP PatInfo
    i Pattern
    p0         -> NamedArg Pattern -> NamedArg Pattern
    f (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ (Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> NamedArg a -> NamedArg b
    updateNamedArg (PatInfo -> Pattern -> Pattern
    forall e. PatInfo -> Pattern' e -> Pattern' e
    WithP PatInfo
    i) (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a.
    MapNamedArgPattern a =>
    (NamedArg Pattern -> NamedArg Pattern) -> a -> a
    mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
    f (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern -> Pattern -> NamedArg Pattern
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg Pattern
    p Pattern
    p0
          AnnP PatInfo
    i Expr
    a Pattern
    p0        -> NamedArg Pattern -> NamedArg Pattern
    f (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ (Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> NamedArg a -> NamedArg b
    updateNamedArg (PatInfo -> Expr -> Pattern -> Pattern
    forall e. PatInfo -> e -> Pattern' e -> Pattern' e
    AnnP PatInfo
    i Expr
    a) (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a.
    MapNamedArgPattern a =>
    (NamedArg Pattern -> NamedArg Pattern) -> a -> a
    mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
    f (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern -> Pattern -> NamedArg Pattern
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg Pattern
    p Pattern
    p0

    instance MapNamedArgPattern a => MapNamedArgPattern [a]                  where
    instance MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) where
    instance MapNamedArgPattern a => MapNamedArgPattern (Maybe a)            where

    instance (MapNamedArgPattern a, MapNamedArgPattern b) => MapNamedArgPattern (a,b) where
      mapNamedArgPattern :: (NamedArg Pattern -> NamedArg Pattern) -> (a, b) -> (a, b)
    mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
    f (a
    a, b
    b) = ((NamedArg Pattern -> NamedArg Pattern) -> a -> a
    forall a.
    MapNamedArgPattern a =>
    (NamedArg Pattern -> NamedArg Pattern) -> a -> a
    mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
    f a
    a, (NamedArg Pattern -> NamedArg Pattern) -> b -> b
    forall a.
    MapNamedArgPattern a =>
    (NamedArg Pattern -> NamedArg Pattern) -> a -> a
    mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
    f b
    b)

    -- | Generic pattern traversal.

    class APatternLike p where
      type ADotT p

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

      default foldrAPattern
        :: (Monoid m, Foldable f, APatternLike b, (ADotT p) ~ (ADotT b), f b ~ p)
        => (Pattern' (ADotT p) -> m -> m) -> p -> m
      foldrAPattern = (b -> m) -> f b -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((b -> m) -> f b -> m)
    -> ((Pattern' (ADotT b) -> m -> m) -> b -> m)
    -> (Pattern' (ADotT b) -> m -> m)
    -> f b
    -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern' (ADotT b) -> m -> m) -> b -> m
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m -> m) -> p -> m
    foldrAPattern

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

      default traverseAPatternM
        :: (Traversable f, APatternLike q, (ADotT p) ~ (ADotT q), f q ~ p, Monad m)
        => (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
        -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
        -> p -> m p
      traverseAPatternM Pattern' (ADotT p) -> m (Pattern' (ADotT p))
    pre Pattern' (ADotT p) -> m (Pattern' (ADotT p))
    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' (ADotT q) -> m (Pattern' (ADotT q)))
    -> (Pattern' (ADotT q) -> m (Pattern' (ADotT q))) -> q -> m q
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    traverseAPatternM Pattern' (ADotT p) -> m (Pattern' (ADotT p))
    Pattern' (ADotT q) -> m (Pattern' (ADotT q))
    pre Pattern' (ADotT p) -> m (Pattern' (ADotT p))
    Pattern' (ADotT q) -> m (Pattern' (ADotT q))
    post

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

    foldAPattern :: (APatternLike p, Monoid m) => (Pattern' (ADotT p) -> m) -> p -> m
    foldAPattern :: forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m) -> p -> m
    foldAPattern Pattern' (ADotT p) -> m
    f = (Pattern' (ADotT p) -> m -> m) -> p -> m
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m -> m) -> p -> m
    foldrAPattern ((Pattern' (ADotT p) -> m -> m) -> p -> m)
    -> (Pattern' (ADotT p) -> m -> m) -> p -> m
    forall a b. (a -> b) -> a -> b
    $ \ Pattern' (ADotT p)
    p m
    m -> Pattern' (ADotT p) -> m
    f Pattern' (ADotT p)
    p m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` m
    m

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

    preTraverseAPatternM
      :: (APatternLike p, Monad m )
      => (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))  -- ^ @pre@: Modification before recursion.
      -> p -> m p
    preTraverseAPatternM :: forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    preTraverseAPatternM Pattern' (ADotT p) -> m (Pattern' (ADotT p))
    pre p
    p = (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    traverseAPatternM Pattern' (ADotT p) -> m (Pattern' (ADotT p))
    pre Pattern' (ADotT p) -> m (Pattern' (ADotT p))
    forall (m :: * -> *) a. Monad m => a -> m a
    return p
    p

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

    postTraverseAPatternM
      :: (APatternLike p, Monad m )
      => (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))  -- ^ @post@: Modification after recursion.
      -> p -> m p
    postTraverseAPatternM :: forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    postTraverseAPatternM Pattern' (ADotT p) -> m (Pattern' (ADotT p))
    post p
    p = (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    traverseAPatternM Pattern' (ADotT p) -> m (Pattern' (ADotT p))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' (ADotT p) -> m (Pattern' (ADotT p))
    post p
    p

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

    mapAPattern :: APatternLike p => (Pattern' (ADotT p) -> Pattern' (ADotT p)) -> p -> p
    mapAPattern :: forall p.
    APatternLike p =>
    (Pattern' (ADotT p) -> Pattern' (ADotT p)) -> p -> p
    mapAPattern Pattern' (ADotT p) -> Pattern' (ADotT p)
    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' (ADotT p) -> Identity (Pattern' (ADotT p)))
    -> p -> Identity p
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    postTraverseAPatternM (Pattern' (ADotT p) -> Identity (Pattern' (ADotT p))
    forall a. a -> Identity a
    Identity (Pattern' (ADotT p) -> Identity (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> Pattern' (ADotT p))
    -> Pattern' (ADotT p)
    -> Identity (Pattern' (ADotT p))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern' (ADotT p) -> Pattern' (ADotT p)
    f)

    -- Interesting instance:

    instance APatternLike (Pattern' a) where
      type ADotT (Pattern' a) = a

      foldrAPattern :: forall m.
    Monoid m =>
    (Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m
    foldrAPattern Pattern' (ADotT (Pattern' a)) -> m -> m
    f Pattern' a
    p = Pattern' (ADotT (Pattern' a)) -> m -> m
    f Pattern' a
    Pattern' (ADotT (Pattern' a))
    p (m -> m) -> m -> m
    forall a b. (a -> b) -> a -> b
    $
        case Pattern' a
    p of
          AsP PatInfo
    _ BindName
    _ Pattern' a
    p          -> (Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m -> m) -> p -> m
    foldrAPattern Pattern' (ADotT (Pattern' a)) -> m -> m
    f Pattern' a
    p
          ConP ConPatInfo
    _ AmbiguousQName
    _ NAPs a
    ps        -> (Pattern' (ADotT (NAPs a)) -> m -> m) -> NAPs a -> m
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m -> m) -> p -> m
    foldrAPattern Pattern' (ADotT (NAPs a)) -> m -> m
    Pattern' (ADotT (Pattern' a)) -> m -> m
    f NAPs a
    ps
          DefP PatInfo
    _ AmbiguousQName
    _ NAPs a
    ps        -> (Pattern' (ADotT (NAPs a)) -> m -> m) -> NAPs a -> m
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m -> m) -> p -> m
    foldrAPattern Pattern' (ADotT (NAPs a)) -> m -> m
    Pattern' (ADotT (Pattern' a)) -> m -> m
    f NAPs a
    ps
          RecP PatInfo
    _ [FieldAssignment' (Pattern' a)]
    ps          -> (Pattern' (ADotT [FieldAssignment' (Pattern' a)]) -> m -> m)
    -> [FieldAssignment' (Pattern' a)] -> m
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m -> m) -> p -> m
    foldrAPattern Pattern' (ADotT [FieldAssignment' (Pattern' a)]) -> m -> m
    Pattern' (ADotT (Pattern' a)) -> m -> m
    f [FieldAssignment' (Pattern' a)]
    ps
          PatternSynP PatInfo
    _ AmbiguousQName
    _ NAPs a
    ps -> (Pattern' (ADotT (NAPs a)) -> m -> m) -> NAPs a -> m
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m -> m) -> p -> m
    foldrAPattern Pattern' (ADotT (NAPs a)) -> m -> m
    Pattern' (ADotT (Pattern' a)) -> m -> m
    f NAPs a
    ps
          WithP PatInfo
    _ Pattern' a
    p          -> (Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m -> m) -> p -> m
    foldrAPattern Pattern' (ADotT (Pattern' a)) -> m -> m
    f Pattern' a
    p
          VarP BindName
    _             -> m
    forall a. Monoid a => a
    mempty
          ProjP PatInfo
    _ ProjOrigin
    _ AmbiguousQName
    _        -> m
    forall a. Monoid a => a
    mempty
          WildP PatInfo
    _            -> m
    forall a. Monoid a => a
    mempty
          DotP PatInfo
    _ a
    _           -> m
    forall a. Monoid a => a
    mempty
          AbsurdP PatInfo
    _          -> m
    forall a. Monoid a => a
    mempty
          LitP PatInfo
    _ Literal
    _           -> m
    forall a. Monoid a => a
    mempty
          EqualP PatInfo
    _ [(a, a)]
    _         -> m
    forall a. Monoid a => a
    mempty
          AnnP PatInfo
    _ a
    _ Pattern' a
    p         -> (Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m -> m) -> p -> m
    foldrAPattern Pattern' (ADotT (Pattern' a)) -> m -> m
    f Pattern' a
    p

      traverseAPatternM :: forall (m :: * -> *).
    Monad m =>
    (Pattern' (ADotT (Pattern' a))
     -> m (Pattern' (ADotT (Pattern' a))))
    -> (Pattern' (ADotT (Pattern' a))
        -> m (Pattern' (ADotT (Pattern' a))))
    -> Pattern' a
    -> m (Pattern' a)
    traverseAPatternM Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    pre Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    post = Pattern' a -> m (Pattern' a)
    Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    pre (Pattern' a -> m (Pattern' a))
    -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> Pattern' a -> m (Pattern' a)
    recurse (Pattern' a -> m (Pattern' a))
    -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> Pattern' a -> m (Pattern' a)
    Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    post
        where
        recurse :: Pattern' a -> m (Pattern' a)
    recurse = \case
          -- Non-recursive cases:
          p :: Pattern' a
    p@A.VarP{}            -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p
          p :: Pattern' a
    p@A.WildP{}           -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p
          p :: Pattern' a
    p@A.DotP{}            -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p
          p :: Pattern' a
    p@A.LitP{}            -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p
          p :: Pattern' a
    p@A.AbsurdP{}         -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p
          p :: Pattern' a
    p@A.ProjP{}           -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p
          p :: Pattern' a
    p@A.EqualP{}          -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p
          -- Recursive cases:
          A.ConP        ConPatInfo
    i AmbiguousQName
    ds NAPs a
    ps -> ConPatInfo -> AmbiguousQName -> NAPs a -> Pattern' a
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.ConP        ConPatInfo
    i AmbiguousQName
    ds (NAPs a -> Pattern' a) -> m (NAPs a) -> m (Pattern' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
    -> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
    -> NAPs a
    -> m (NAPs a)
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    traverseAPatternM Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a)))
    Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    pre Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a)))
    Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    post NAPs a
    ps
          A.DefP        PatInfo
    i AmbiguousQName
    q  NAPs a
    ps -> PatInfo -> AmbiguousQName -> NAPs a -> Pattern' a
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.DefP        PatInfo
    i AmbiguousQName
    q  (NAPs a -> Pattern' a) -> m (NAPs a) -> m (Pattern' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
    -> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
    -> NAPs a
    -> m (NAPs a)
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    traverseAPatternM Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a)))
    Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    pre Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a)))
    Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    post NAPs a
    ps
          A.AsP         PatInfo
    i BindName
    x  Pattern' a
    p  -> PatInfo -> BindName -> Pattern' a -> Pattern' a
    forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
    A.AsP         PatInfo
    i BindName
    x  (Pattern' a -> Pattern' a) -> m (Pattern' a) -> m (Pattern' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern' (ADotT (Pattern' a))
     -> m (Pattern' (ADotT (Pattern' a))))
    -> (Pattern' (ADotT (Pattern' a))
        -> m (Pattern' (ADotT (Pattern' a))))
    -> Pattern' a
    -> m (Pattern' a)
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    traverseAPatternM Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    pre Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    post Pattern' a
    p
          A.RecP        PatInfo
    i    [FieldAssignment' (Pattern' a)]
    ps -> PatInfo -> [FieldAssignment' (Pattern' a)] -> Pattern' a
    forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    A.RecP        PatInfo
    i    ([FieldAssignment' (Pattern' a)] -> Pattern' a)
    -> m [FieldAssignment' (Pattern' a)] -> m (Pattern' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern' (ADotT [FieldAssignment' (Pattern' a)])
     -> m (Pattern' (ADotT [FieldAssignment' (Pattern' a)])))
    -> (Pattern' (ADotT [FieldAssignment' (Pattern' a)])
        -> m (Pattern' (ADotT [FieldAssignment' (Pattern' a)])))
    -> [FieldAssignment' (Pattern' a)]
    -> m [FieldAssignment' (Pattern' a)]
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    traverseAPatternM Pattern' (ADotT [FieldAssignment' (Pattern' a)])
    -> m (Pattern' (ADotT [FieldAssignment' (Pattern' a)]))
    Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    pre Pattern' (ADotT [FieldAssignment' (Pattern' a)])
    -> m (Pattern' (ADotT [FieldAssignment' (Pattern' a)]))
    Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    post [FieldAssignment' (Pattern' a)]
    ps
          A.PatternSynP PatInfo
    i AmbiguousQName
    x  NAPs a
    ps -> PatInfo -> AmbiguousQName -> NAPs a -> Pattern' a
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.PatternSynP PatInfo
    i AmbiguousQName
    x  (NAPs a -> Pattern' a) -> m (NAPs a) -> m (Pattern' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
    -> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
    -> NAPs a
    -> m (NAPs a)
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    traverseAPatternM Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a)))
    Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    pre Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a)))
    Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    post NAPs a
    ps
          A.WithP       PatInfo
    i Pattern' a
    p     -> PatInfo -> Pattern' a -> Pattern' a
    forall e. PatInfo -> Pattern' e -> Pattern' e
    A.WithP       PatInfo
    i    (Pattern' a -> Pattern' a) -> m (Pattern' a) -> m (Pattern' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern' (ADotT (Pattern' a))
     -> m (Pattern' (ADotT (Pattern' a))))
    -> (Pattern' (ADotT (Pattern' a))
        -> m (Pattern' (ADotT (Pattern' a))))
    -> Pattern' a
    -> m (Pattern' a)
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    traverseAPatternM Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    pre Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    post Pattern' a
    p
          A.AnnP        PatInfo
    i a
    a  Pattern' a
    p  -> PatInfo -> a -> Pattern' a -> Pattern' a
    forall e. PatInfo -> e -> Pattern' e -> Pattern' e
    A.AnnP        PatInfo
    i a
    a  (Pattern' a -> Pattern' a) -> m (Pattern' a) -> m (Pattern' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern' (ADotT (Pattern' a))
     -> m (Pattern' (ADotT (Pattern' a))))
    -> (Pattern' (ADotT (Pattern' a))
        -> m (Pattern' (ADotT (Pattern' a))))
    -> Pattern' a
    -> m (Pattern' a)
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    traverseAPatternM Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    pre Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
    post Pattern' a
    p

    instance APatternLike a => APatternLike (Arg a) where
      type ADotT (Arg a) = ADotT a

    instance APatternLike a => APatternLike (Named n a) where
      type ADotT (Named n a) = ADotT a

    instance APatternLike a => APatternLike [a] where
      type ADotT [a] = ADotT a

    instance APatternLike a => APatternLike (Maybe a) where
      type ADotT (Maybe a) = ADotT a

    instance APatternLike a => APatternLike (FieldAssignment' a) where
      type ADotT (FieldAssignment' a) = ADotT a

    instance (APatternLike a, APatternLike b, ADotT a ~ ADotT b) => APatternLike (a, b) where
      type ADotT (a, b) = ADotT a

      foldrAPattern :: forall m.
    Monoid m =>
    (Pattern' (ADotT (a, b)) -> m -> m) -> (a, b) -> m
    foldrAPattern Pattern' (ADotT (a, b)) -> m -> m
    f (a
    p, b
    p') =
        (Pattern' (ADotT a) -> m -> m) -> a -> m
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m -> m) -> p -> m
    foldrAPattern Pattern' (ADotT a) -> m -> m
    Pattern' (ADotT (a, b)) -> m -> m
    f a
    p m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` (Pattern' (ADotT b) -> m -> m) -> b -> m
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m -> m) -> p -> m
    foldrAPattern Pattern' (ADotT b) -> m -> m
    Pattern' (ADotT (a, b)) -> m -> m
    f b
    p'

      traverseAPatternM :: forall (m :: * -> *).
    Monad m =>
    (Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b))))
    -> (Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b))))
    -> (a, b)
    -> m (a, b)
    traverseAPatternM Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
    pre Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
    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' (ADotT a) -> m (Pattern' (ADotT a)))
    -> (Pattern' (ADotT a) -> m (Pattern' (ADotT a))) -> a -> m a
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    traverseAPatternM Pattern' (ADotT a) -> m (Pattern' (ADotT a))
    Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
    pre Pattern' (ADotT a) -> m (Pattern' (ADotT a))
    Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
    post a
    p)
          ((Pattern' (ADotT b) -> m (Pattern' (ADotT b)))
    -> (Pattern' (ADotT b) -> m (Pattern' (ADotT b))) -> b -> m b
    forall p (m :: * -> *).
    (APatternLike p, Monad m) =>
    (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
    traverseAPatternM Pattern' (ADotT b) -> m (Pattern' (ADotT b))
    Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
    pre Pattern' (ADotT b) -> m (Pattern' (ADotT b))
    Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
    post b
    p')

    -- * Specific folds
    ------------------------------------------------------------------------

    -- | Collect pattern variables in left-to-right textual order.

    patternVars :: APatternLike p => p -> [A.Name]
    patternVars :: forall p. APatternLike p => p -> [Name]
    patternVars p
    p = (Pattern' (ADotT p) -> Endo [Name]) -> p -> Endo [Name]
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m) -> p -> m
    foldAPattern Pattern' (ADotT p) -> Endo [Name]
    forall a. Pattern' a -> Endo [Name]
    f p
    p Endo [Name] -> [Name] -> [Name]
    forall a. Endo a -> a -> a
    `appEndo` []
      where
      -- We use difference lists @[A.Name] -> [A.Name]@ to avoid reconcatenation.
      f :: Pattern' a -> Endo [A.Name]
      f :: forall a. Pattern' a -> Endo [Name]
    f = \case
        A.VarP BindName
    x         -> ([Name] -> [Name]) -> Endo [Name]
    forall a. (a -> a) -> Endo a
    Endo (BindName -> Name
    unBind BindName
    x Name -> [Name] -> [Name]
    forall a. a -> [a] -> [a]
    :)
        A.AsP PatInfo
    _ BindName
    x Pattern' a
    _      -> ([Name] -> [Name]) -> Endo [Name]
    forall a. (a -> a) -> Endo a
    Endo (BindName -> Name
    unBind BindName
    x Name -> [Name] -> [Name]
    forall a. a -> [a] -> [a]
    :)
        A.LitP        {} -> Endo [Name]
    forall a. Monoid a => a
    mempty
        A.ConP        {} -> Endo [Name]
    forall a. Monoid a => a
    mempty
        A.RecP        {} -> Endo [Name]
    forall a. Monoid a => a
    mempty
        A.DefP        {} -> Endo [Name]
    forall a. Monoid a => a
    mempty
        A.ProjP       {} -> Endo [Name]
    forall a. Monoid a => a
    mempty
        A.WildP       {} -> Endo [Name]
    forall a. Monoid a => a
    mempty
        A.DotP        {} -> Endo [Name]
    forall a. Monoid a => a
    mempty
        A.AbsurdP     {} -> Endo [Name]
    forall a. Monoid a => a
    mempty
        A.EqualP      {} -> Endo [Name]
    forall a. Monoid a => a
    mempty
        A.PatternSynP {} -> Endo [Name]
    forall a. Monoid a => a
    mempty
        A.WithP PatInfo
    _ Pattern' a
    _      -> Endo [Name]
    forall a. Monoid a => a
    mempty
        A.AnnP        {} -> Endo [Name]
    forall a. Monoid a => a
    mempty

    -- | Check if a pattern contains a specific (sub)pattern.

    containsAPattern :: APatternLike p => (Pattern' (ADotT p) -> Bool) -> p -> Bool
    containsAPattern :: forall p.
    APatternLike p =>
    (Pattern' (ADotT p) -> Bool) -> p -> Bool
    containsAPattern Pattern' (ADotT p) -> Bool
    f = Any -> Bool
    getAny (Any -> Bool) -> (p -> Any) -> p -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern' (ADotT p) -> Any) -> p -> Any
    forall p m.
    (APatternLike p, Monoid m) =>
    (Pattern' (ADotT p) -> m) -> p -> m
    foldAPattern (Bool -> Any
    Any (Bool -> Any)
    -> (Pattern' (ADotT p) -> Bool) -> Pattern' (ADotT p) -> Any
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern' (ADotT p) -> Bool
    f)

    -- | Check if a pattern contains an absurd pattern.
    --   For instance, @suc ()@, does so.
    --
    --   Precondition: contains no pattern synonyms.

    containsAbsurdPattern :: APatternLike p => p -> Bool
    containsAbsurdPattern :: forall p. APatternLike p => p -> Bool
    containsAbsurdPattern = (Pattern' (ADotT p) -> Bool) -> p -> Bool
    forall p.
    APatternLike p =>
    (Pattern' (ADotT p) -> Bool) -> p -> Bool
    containsAPattern ((Pattern' (ADotT p) -> Bool) -> p -> Bool)
    -> (Pattern' (ADotT p) -> Bool) -> p -> Bool
    forall a b. (a -> b) -> a -> b
    $ \case
        A.PatternSynP{} -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.AbsurdP{}     -> Bool
    True
        Pattern' (ADotT p)
    _               -> Bool
    False

    -- | Check if a pattern contains an @-pattern.
    --
    containsAsPattern :: APatternLike p => p -> Bool
    containsAsPattern :: forall p. APatternLike p => p -> Bool
    containsAsPattern = (Pattern' (ADotT p) -> Bool) -> p -> Bool
    forall p.
    APatternLike p =>
    (Pattern' (ADotT p) -> Bool) -> p -> Bool
    containsAPattern ((Pattern' (ADotT p) -> Bool) -> p -> Bool)
    -> (Pattern' (ADotT p) -> Bool) -> p -> Bool
    forall a b. (a -> b) -> a -> b
    $ \case
        A.AsP{}         -> Bool
    True
        Pattern' (ADotT p)
    _               -> Bool
    False

    -- | Check if any user-written pattern variables occur more than once,
    --   and throw the given error if they do.
    checkPatternLinearity :: (Monad m, APatternLike p)
                          => p -> ([C.Name] -> m ()) -> m ()
    checkPatternLinearity :: forall (m :: * -> *) p.
    (Monad m, APatternLike p) =>
    p -> ([Name] -> m ()) -> m ()
    checkPatternLinearity p
    ps [Name] -> m ()
    err =
      [Name] -> ([Name] -> m ()) -> m ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull ([Name] -> [Name]
    forall a. Ord a => [a] -> [a]
    duplicates ([Name] -> [Name]) -> [Name] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ (Name -> Name) -> [Name] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Name
    nameConcrete ([Name] -> [Name]) -> [Name] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ p -> [Name]
    forall p. APatternLike p => p -> [Name]
    patternVars p
    ps) (([Name] -> m ()) -> m ()) -> ([Name] -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \[Name]
    ys -> [Name] -> m ()
    err [Name]
    ys

    -- * Specific traversals
    ------------------------------------------------------------------------

    -- | Pattern substitution.
    --
    -- For the embedded expression, the given pattern substitution is turned into
    -- an expression substitution.

    substPattern :: [(Name, Pattern)] -> Pattern -> Pattern
    substPattern :: [(Name, Pattern)] -> Pattern -> Pattern
    substPattern [(Name, Pattern)]
    s = (Expr -> Expr) -> [(Name, Pattern)] -> Pattern -> Pattern
    forall e.
    (e -> e) -> [(Name, Pattern' e)] -> Pattern' e -> Pattern' e
    substPattern' ([(Name, Expr)] -> Expr -> Expr
    forall a. SubstExpr a => [(Name, Expr)] -> a -> a
    substExpr ([(Name, Expr)] -> Expr -> Expr) -> [(Name, Expr)] -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ ((Name, Pattern) -> (Name, Expr))
    -> [(Name, Pattern)] -> [(Name, Expr)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Pattern -> Expr) -> (Name, Pattern) -> (Name, Expr)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second Pattern -> Expr
    patternToExpr) [(Name, Pattern)]
    s) [(Name, Pattern)]
    s

    -- | Pattern substitution, parametrized by substitution function for embedded expressions.

    substPattern'
      :: (e -> e)              -- ^ Substitution function for expressions.
      -> [(Name, Pattern' e)]  -- ^ (Parallel) substitution.
      -> Pattern' e            -- ^ Input pattern.
      -> Pattern' e
    substPattern' :: forall e.
    (e -> e) -> [(Name, Pattern' e)] -> Pattern' e -> Pattern' e
    substPattern' e -> e
    subE [(Name, Pattern' e)]
    s = (Pattern' (ADotT (Pattern' e)) -> Pattern' (ADotT (Pattern' e)))
    -> Pattern' e -> Pattern' e
    forall p.
    APatternLike p =>
    (Pattern' (ADotT p) -> Pattern' (ADotT p)) -> p -> p
    mapAPattern ((Pattern' (ADotT (Pattern' e)) -> Pattern' (ADotT (Pattern' e)))
     -> Pattern' e -> Pattern' e)
    -> (Pattern' (ADotT (Pattern' e)) -> Pattern' (ADotT (Pattern' e)))
    -> Pattern' e
    -> Pattern' e
    forall a b. (a -> b) -> a -> b
    $ \ Pattern' (ADotT (Pattern' e))
    p -> case Pattern' (ADotT (Pattern' e))
    p of
      VarP BindName
    x            -> Pattern' e -> Maybe (Pattern' e) -> Pattern' e
    forall a. a -> Maybe a -> a
    fromMaybe Pattern' e
    Pattern' (ADotT (Pattern' e))
    p (Maybe (Pattern' e) -> Pattern' e)
    -> Maybe (Pattern' e) -> Pattern' e
    forall a b. (a -> b) -> a -> b
    $ Name -> [(Name, Pattern' e)] -> Maybe (Pattern' e)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup (BindName -> Name
    A.unBind BindName
    x) [(Name, Pattern' e)]
    s
      DotP PatInfo
    i ADotT (Pattern' e)
    e          -> PatInfo -> e -> Pattern' e
    forall e. PatInfo -> e -> Pattern' e
    DotP PatInfo
    i (e -> Pattern' e) -> e -> Pattern' e
    forall a b. (a -> b) -> a -> b
    $ e -> e
    subE e
    ADotT (Pattern' e)
    e
      EqualP PatInfo
    i [(ADotT (Pattern' e), ADotT (Pattern' e))]
    es       -> PatInfo -> [(e, e)] -> Pattern' e
    forall e. PatInfo -> [(e, e)] -> Pattern' e
    EqualP PatInfo
    i ([(e, e)] -> Pattern' e) -> [(e, e)] -> Pattern' e
    forall a b. (a -> b) -> a -> b
    $ ((e, e) -> (e, e)) -> [(e, e)] -> [(e, e)]
    forall a b. (a -> b) -> [a] -> [b]
    map (e -> e
    subE (e -> e) -> (e -> e) -> (e, e) -> (e, e)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** e -> e
    subE) [(e, e)]
    [(ADotT (Pattern' e), ADotT (Pattern' e))]
    es
      AnnP PatInfo
    i ADotT (Pattern' e)
    a Pattern' (ADotT (Pattern' e))
    p        -> PatInfo -> e -> Pattern' e -> Pattern' e
    forall e. PatInfo -> e -> Pattern' e -> Pattern' e
    AnnP PatInfo
    i (e -> e
    subE e
    ADotT (Pattern' e)
    a) Pattern' e
    Pattern' (ADotT (Pattern' e))
    p
      -- No action on the other patterns (besides the recursion):
      ConP ConPatInfo
    _ AmbiguousQName
    _ NAPs (ADotT (Pattern' e))
    _        -> Pattern' (ADotT (Pattern' e))
    p
      RecP PatInfo
    _ [FieldAssignment' (Pattern' (ADotT (Pattern' e)))]
    _          -> Pattern' (ADotT (Pattern' e))
    p
      ProjP PatInfo
    _ ProjOrigin
    _ AmbiguousQName
    _       -> Pattern' (ADotT (Pattern' e))
    p
      WildP PatInfo
    _           -> Pattern' (ADotT (Pattern' e))
    p
      AbsurdP PatInfo
    _         -> Pattern' (ADotT (Pattern' e))
    p
      LitP PatInfo
    _ Literal
    _          -> Pattern' (ADotT (Pattern' e))
    p
      DefP PatInfo
    _ AmbiguousQName
    _ NAPs (ADotT (Pattern' e))
    _        -> Pattern' (ADotT (Pattern' e))
    p
      AsP PatInfo
    _ BindName
    _ Pattern' (ADotT (Pattern' e))
    _         -> Pattern' (ADotT (Pattern' e))
    p -- Note: cannot substitute into as-variable
      PatternSynP PatInfo
    _ AmbiguousQName
    _ NAPs (ADotT (Pattern' e))
    _ -> Pattern' (ADotT (Pattern' e))
    p
      WithP PatInfo
    _ Pattern' (ADotT (Pattern' e))
    _         -> Pattern' (ADotT (Pattern' e))
    p

    -- * Other pattern utilities
    ------------------------------------------------------------------------

    -- | Check for with-pattern.
    instance IsWithP (Pattern' e) where
      isWithP :: Pattern' e -> Maybe (Pattern' e)
    isWithP = \case
        WithP PatInfo
    _ Pattern' e
    p -> Pattern' e -> Maybe (Pattern' e)
    forall a. a -> Maybe a
    Just Pattern' e
    p
        Pattern' e
    _ -> Maybe (Pattern' e)
    forall a. Maybe a
    Nothing

    -- | Split patterns into (patterns, trailing with-patterns).
    splitOffTrailingWithPatterns :: A.Patterns -> (A.Patterns, A.Patterns)
    splitOffTrailingWithPatterns :: NAPs Expr -> (NAPs Expr, NAPs Expr)
    splitOffTrailingWithPatterns = (NamedArg Pattern -> Bool) -> NAPs Expr -> (NAPs Expr, NAPs Expr)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    spanEnd (Maybe (NamedArg Pattern) -> Bool
    forall a. Maybe a -> Bool
    isJust (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)

    -- | Get the tail of with-patterns of a pattern spine.
    trailingWithPatterns :: Patterns -> Patterns
    trailingWithPatterns :: NAPs Expr -> NAPs Expr
    trailingWithPatterns = (NAPs Expr, NAPs Expr) -> NAPs Expr
    forall a b. (a, b) -> b
    snd ((NAPs Expr, NAPs Expr) -> NAPs Expr)
    -> (NAPs Expr -> (NAPs Expr, NAPs Expr)) -> NAPs Expr -> NAPs Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NAPs Expr -> (NAPs Expr, NAPs Expr)
    splitOffTrailingWithPatterns

    -- | The next patterns are ...
    --
    -- (This view discards 'PatInfo'.)
    data LHSPatternView e
      = LHSAppP  (NAPs e)
          -- ^ Application patterns (non-empty list).
      | LHSProjP ProjOrigin AmbiguousQName (NamedArg (Pattern' e))
          -- ^ A projection pattern.  Is also stored unmodified here.
      | LHSWithP [Pattern' e]
          -- ^ With patterns (non-empty list).
          --   These patterns are not prefixed with 'WithP'.
      deriving (Int -> LHSPatternView e -> ShowS
    [LHSPatternView e] -> ShowS
    LHSPatternView e -> String
    (Int -> LHSPatternView e -> ShowS)
    -> (LHSPatternView e -> String)
    -> ([LHSPatternView e] -> ShowS)
    -> Show (LHSPatternView e)
    forall e. Show e => Int -> LHSPatternView e -> ShowS
    forall e. Show e => [LHSPatternView e] -> ShowS
    forall e. Show e => LHSPatternView e -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [LHSPatternView e] -> ShowS
    $cshowList :: forall e. Show e => [LHSPatternView e] -> ShowS
    show :: LHSPatternView e -> String
    $cshow :: forall e. Show e => LHSPatternView e -> String
    showsPrec :: Int -> LHSPatternView e -> ShowS
    $cshowsPrec :: forall e. Show e => Int -> LHSPatternView e -> ShowS
    Show)

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

    lhsPatternView :: IsProjP e => NAPs e -> Maybe (LHSPatternView e, NAPs e)
    lhsPatternView :: forall e. IsProjP e => NAPs e -> Maybe (LHSPatternView e, NAPs e)
    lhsPatternView [] = Maybe (LHSPatternView e, [NamedArg (Pattern' e)])
    forall a. Maybe a
    Nothing
    lhsPatternView (NamedArg (Pattern' e)
    p0 : [NamedArg (Pattern' e)]
    ps) =
      case NamedArg (Pattern' e) -> Pattern' e
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' e)
    p0 of
        ProjP PatInfo
    _i ProjOrigin
    o AmbiguousQName
    d -> (LHSPatternView e, [NamedArg (Pattern' e)])
    -> Maybe (LHSPatternView e, [NamedArg (Pattern' e)])
    forall a. a -> Maybe a
    Just (ProjOrigin
    -> AmbiguousQName -> NamedArg (Pattern' e) -> LHSPatternView e
    forall e.
    ProjOrigin
    -> AmbiguousQName -> NamedArg (Pattern' e) -> LHSPatternView e
    LHSProjP ProjOrigin
    o AmbiguousQName
    d NamedArg (Pattern' e)
    p0, [NamedArg (Pattern' e)]
    ps)
        -- If the next pattern is a with-pattern, collect more with-patterns
        WithP PatInfo
    _i Pattern' e
    p   -> (LHSPatternView e, [NamedArg (Pattern' e)])
    -> Maybe (LHSPatternView e, [NamedArg (Pattern' e)])
    forall a. a -> Maybe a
    Just ([Pattern' e] -> LHSPatternView e
    forall e. [Pattern' e] -> LHSPatternView e
    LHSWithP (Pattern' e
    p Pattern' e -> [Pattern' e] -> [Pattern' e]
    forall a. a -> [a] -> [a]
    : (NamedArg (Pattern' e) -> Pattern' e)
    -> [NamedArg (Pattern' e)] -> [Pattern' e]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' e) -> Pattern' e
    forall a. NamedArg a -> a
    namedArg [NamedArg (Pattern' e)]
    ps1), [NamedArg (Pattern' e)]
    ps2)
          where
          ([NamedArg (Pattern' e)]
    ps1, [NamedArg (Pattern' e)]
    ps2) = (NamedArg (Pattern' e) -> Maybe (NamedArg (Pattern' e)))
    -> [NamedArg (Pattern' e)]
    -> ([NamedArg (Pattern' e)], [NamedArg (Pattern' e)])
    forall a b. (a -> Maybe b) -> [a] -> (Prefix b, [a])
    spanJust NamedArg (Pattern' e) -> Maybe (NamedArg (Pattern' e))
    forall p. IsWithP p => p -> Maybe p
    isWithP [NamedArg (Pattern' e)]
    ps
        -- If the next pattern is an application pattern, collect more of these
        Pattern' e
    _ -> (LHSPatternView e, [NamedArg (Pattern' e)])
    -> Maybe (LHSPatternView e, [NamedArg (Pattern' e)])
    forall a. a -> Maybe a
    Just ([NamedArg (Pattern' e)] -> LHSPatternView e
    forall e. NAPs e -> LHSPatternView e
    LHSAppP (NamedArg (Pattern' e)
    p0 NamedArg (Pattern' e)
    -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    forall a. a -> [a] -> [a]
    : [NamedArg (Pattern' e)]
    ps1), [NamedArg (Pattern' e)]
    ps2)
          where
          ([NamedArg (Pattern' e)]
    ps1, [NamedArg (Pattern' e)]
    ps2) = (NamedArg (Pattern' e) -> Bool)
    -> [NamedArg (Pattern' e)]
    -> ([NamedArg (Pattern' e)], [NamedArg (Pattern' e)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (\ NamedArg (Pattern' e)
    p -> Maybe (ProjOrigin, AmbiguousQName) -> Bool
    forall a. Maybe a -> Bool
    isNothing (NamedArg (Pattern' e) -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
    isProjP NamedArg (Pattern' e)
    p) Bool -> Bool -> Bool
    && Maybe (NamedArg (Pattern' e)) -> Bool
    forall a. Maybe a -> Bool
    isNothing (NamedArg (Pattern' e) -> Maybe (NamedArg (Pattern' e))
    forall p. IsWithP p => p -> Maybe p
    isWithP NamedArg (Pattern' e)
    p)) [NamedArg (Pattern' e)]
    ps

    -- * Left-hand-side manipulation
    ------------------------------------------------------------------------

    -- | Convert a focused lhs to spine view and back.
    class LHSToSpine a b where
      lhsToSpine :: a -> b
      spineToLhs :: b -> a

    -- | Clause instance.
    instance LHSToSpine Clause SpineClause where
      lhsToSpine :: Clause -> SpineClause
    lhsToSpine = (LHS -> SpineLHS) -> Clause -> SpineClause
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap LHS -> SpineLHS
    forall a b. LHSToSpine a b => a -> b
    lhsToSpine
      spineToLhs :: SpineClause -> Clause
    spineToLhs = (SpineLHS -> LHS) -> SpineClause -> Clause
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap SpineLHS -> LHS
    forall a b. LHSToSpine a b => b -> a
    spineToLhs

    -- | List instance (for clauses).
    instance LHSToSpine a b => LHSToSpine [a] [b] where
      lhsToSpine :: [a] -> [b]
    lhsToSpine = (a -> b) -> [a] -> [b]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> b
    forall a b. LHSToSpine a b => a -> b
    lhsToSpine
      spineToLhs :: [b] -> [a]
    spineToLhs = (b -> a) -> [b] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map b -> a
    forall a b. LHSToSpine a b => b -> a
    spineToLhs

    -- | LHS instance.
    instance LHSToSpine LHS SpineLHS where
      lhsToSpine :: LHS -> SpineLHS
    lhsToSpine (LHS LHSInfo
    i LHSCore
    core) = LHSInfo -> QName -> NAPs Expr -> SpineLHS
    SpineLHS LHSInfo
    i QName
    f NAPs Expr
    ps
        where QNamed QName
    f NAPs Expr
    ps = LHSCore -> QNamed (NAPs Expr)
    forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
    lhsCoreToSpine LHSCore
    core
      spineToLhs :: SpineLHS -> LHS
    spineToLhs (SpineLHS LHSInfo
    i QName
    f NAPs Expr
    ps) = LHSInfo -> LHSCore -> LHS
    LHS LHSInfo
    i (QNamed (NAPs Expr) -> LHSCore
    forall e. IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e
    spineToLhsCore (QNamed (NAPs Expr) -> LHSCore) -> QNamed (NAPs Expr) -> LHSCore
    forall a b. (a -> b) -> a -> b
    $ QName -> NAPs Expr -> QNamed (NAPs Expr)
    forall a. QName -> a -> QNamed a
    QNamed QName
    f NAPs Expr
    ps)

    lhsCoreToSpine :: LHSCore' e -> A.QNamed [NamedArg (Pattern' e)]
    lhsCoreToSpine :: forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
    lhsCoreToSpine = \case
      LHSHead QName
    f [NamedArg (Pattern' e)]
    ps     -> QName -> [NamedArg (Pattern' e)] -> QNamed [NamedArg (Pattern' e)]
    forall a. QName -> a -> QNamed a
    QNamed QName
    f [NamedArg (Pattern' e)]
    ps
      LHSProj AmbiguousQName
    d NamedArg (LHSCore' e)
    h [NamedArg (Pattern' e)]
    ps   -> LHSCore' e -> QNamed [NamedArg (Pattern' e)]
    forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
    lhsCoreToSpine (NamedArg (LHSCore' e) -> LHSCore' e
    forall a. NamedArg a -> a
    namedArg NamedArg (LHSCore' e)
    h) QNamed [NamedArg (Pattern' e)]
    -> ([NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)])
    -> QNamed [NamedArg (Pattern' e)]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> ([NamedArg (Pattern' e)]
    -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    forall a. [a] -> [a] -> [a]
    ++ (NamedArg (Pattern' e)
    p NamedArg (Pattern' e)
    -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    forall a. a -> [a] -> [a]
    : [NamedArg (Pattern' e)]
    ps))
        where p :: NamedArg (Pattern' e)
    p = (LHSCore' e -> Pattern' e)
    -> NamedArg (LHSCore' e) -> NamedArg (Pattern' e)
    forall a b. (a -> b) -> NamedArg a -> NamedArg b
    updateNamedArg (Pattern' e -> LHSCore' e -> Pattern' e
    forall a b. a -> b -> a
    const (Pattern' e -> LHSCore' e -> Pattern' e)
    -> Pattern' e -> LHSCore' e -> Pattern' e
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
    forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
    ProjP PatInfo
    forall a. Null a => a
    empty ProjOrigin
    ProjPrefix AmbiguousQName
    d) NamedArg (LHSCore' e)
    h
      LHSWith LHSCore' e
    h [Arg (Pattern' e)]
    wps [NamedArg (Pattern' e)]
    ps -> LHSCore' e -> QNamed [NamedArg (Pattern' e)]
    forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
    lhsCoreToSpine LHSCore' e
    h QNamed [NamedArg (Pattern' e)]
    -> ([NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)])
    -> QNamed [NamedArg (Pattern' e)]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> ([NamedArg (Pattern' e)]
    -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    forall a. [a] -> [a] -> [a]
    ++ (Arg (Pattern' e) -> NamedArg (Pattern' e))
    -> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg (Pattern' e) -> NamedArg (Pattern' e)
    forall e. Arg (Pattern' e) -> NamedArg (Pattern' e)
    fromWithPat [Arg (Pattern' e)]
    wps [NamedArg (Pattern' e)]
    -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg (Pattern' e)]
    ps)
        where
          fromWithPat :: Arg (Pattern' e) -> NamedArg (Pattern' e)
          fromWithPat :: forall e. Arg (Pattern' e) -> NamedArg (Pattern' e)
    fromWithPat = (Pattern' e -> Named NamedName (Pattern' e))
    -> Arg (Pattern' e) -> Arg (Named NamedName (Pattern' e))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Pattern' e -> Named NamedName (Pattern' e)
    forall a name. a -> Named name a
    unnamed (Pattern' e -> Named NamedName (Pattern' e))
    -> (Pattern' e -> Pattern' e)
    -> Pattern' e
    -> Named NamedName (Pattern' e)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern' e -> Pattern' e
    forall {e}. Pattern' e -> Pattern' e
    mkWithP)
          mkWithP :: Pattern' e -> Pattern' e
    mkWithP Pattern' e
    p   = PatInfo -> Pattern' e -> Pattern' e
    forall e. PatInfo -> Pattern' e -> Pattern' e
    WithP (Range -> PatInfo
    PatRange (Range -> PatInfo) -> Range -> PatInfo
    forall a b. (a -> b) -> a -> b
    $ Pattern' e -> Range
    forall a. HasRange a => a -> Range
    getRange Pattern' e
    p) Pattern' e
    p

    spineToLhsCore :: IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e
    spineToLhsCore :: forall e. IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e
    spineToLhsCore (QNamed QName
    f [NamedArg (Pattern' e)]
    ps) = LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
    forall e.
    IsProjP e =>
    LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
    lhsCoreAddSpine (QName -> [NamedArg (Pattern' e)] -> LHSCore' e
    forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
    LHSHead QName
    f []) [NamedArg (Pattern' e)]
    ps

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

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

    lhsCoreAddChunk :: IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e
    lhsCoreAddChunk :: forall e. IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e
    lhsCoreAddChunk LHSCore' e
    core = \case
      LHSAppP NAPs e
    ps               -> LHSCore' e -> NAPs e -> LHSCore' e
    forall e. LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
    lhsCoreApp LHSCore' e
    core NAPs e
    ps
      LHSWithP [Pattern' e]
    wps             -> LHSCore' e -> [Arg (Pattern' e)] -> LHSCore' e
    forall e. LHSCore' e -> [Arg (Pattern' e)] -> LHSCore' e
    lhsCoreWith LHSCore' e
    core (Pattern' e -> Arg (Pattern' e)
    forall a. a -> Arg a
    defaultArg (Pattern' e -> Arg (Pattern' e))
    -> [Pattern' e] -> [Arg (Pattern' e)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Pattern' e]
    wps)
      LHSProjP ProjOrigin
    ProjPrefix AmbiguousQName
    d NamedArg (Pattern' e)
    np -> AmbiguousQName -> NamedArg (LHSCore' e) -> NAPs e -> LHSCore' e
    forall e.
    AmbiguousQName
    -> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
    LHSProj AmbiguousQName
    d (NamedArg (Pattern' e) -> LHSCore' e -> NamedArg (LHSCore' e)
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg (Pattern' e)
    np LHSCore' e
    core) []  -- Prefix projection pattern.
      LHSProjP ProjOrigin
    _          AmbiguousQName
    _ NamedArg (Pattern' e)
    np -> LHSCore' e -> NAPs e -> LHSCore' e
    forall e. LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
    lhsCoreApp LHSCore' e
    core [NamedArg (Pattern' e)
    np]       -- Postfix projection pattern.

    -- | Add projection, with, and applicative patterns to the right.
    lhsCoreAddSpine :: IsProjP e => LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
    lhsCoreAddSpine :: forall e.
    IsProjP e =>
    LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
    lhsCoreAddSpine LHSCore' e
    core [NamedArg (Pattern' e)]
    ps =
      -- Recurse on lhsPatternView until no patterns left.
      case [NamedArg (Pattern' e)]
    -> Maybe (LHSPatternView e, [NamedArg (Pattern' e)])
    forall e. IsProjP e => NAPs e -> Maybe (LHSPatternView e, NAPs e)
    lhsPatternView [NamedArg (Pattern' e)]
    ps of
        Maybe (LHSPatternView e, [NamedArg (Pattern' e)])
    Nothing       -> LHSCore' e
    core
        Just (LHSPatternView e
    v, [NamedArg (Pattern' e)]
    ps') -> LHSCore' e -> LHSPatternView e -> LHSCore' e
    forall e. IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e
    lhsCoreAddChunk LHSCore' e
    core LHSPatternView e
    chunk LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
    forall e.
    IsProjP e =>
    LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
    `lhsCoreAddSpine` [NamedArg (Pattern' e)]
    ps'
          where
          -- Andreas, 2016-06-13
          -- If the projection was written prefix by the user
          -- or it is a fully applied operator
          -- we turn it to prefix projection form.
          chunk :: LHSPatternView e
    chunk = case LHSPatternView e
    v of
            LHSProjP ProjOrigin
    ProjPrefix AmbiguousQName
    _ NamedArg (Pattern' e)
    _
              -> LHSPatternView e
    v
            LHSProjP ProjOrigin
    _ AmbiguousQName
    d NamedArg (Pattern' e)
    np | let nh :: Int
    nh = AmbiguousQName -> Int
    forall a. NumHoles a => a -> Int
    C.numHoles AmbiguousQName
    d, Int
    nh Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0, Int
    nh Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + [NamedArg (Pattern' e)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [NamedArg (Pattern' e)]
    ps'
              -> ProjOrigin
    -> AmbiguousQName -> NamedArg (Pattern' e) -> LHSPatternView e
    forall e.
    ProjOrigin
    -> AmbiguousQName -> NamedArg (Pattern' e) -> LHSPatternView e
    LHSProjP ProjOrigin
    ProjPrefix AmbiguousQName
    d NamedArg (Pattern' e)
    np
            LHSPatternView e
    _ -> LHSPatternView e
    v

    -- | Used for checking pattern linearity.
    lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]
    lhsCoreAllPatterns :: forall e. LHSCore' e -> [Pattern' e]
    lhsCoreAllPatterns = (NamedArg (Pattern' e) -> Pattern' e)
    -> [NamedArg (Pattern' e)] -> [Pattern' e]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' e) -> Pattern' e
    forall a. NamedArg a -> a
    namedArg ([NamedArg (Pattern' e)] -> [Pattern' e])
    -> (LHSCore' e -> [NamedArg (Pattern' e)])
    -> LHSCore' e
    -> [Pattern' e]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QNamed [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
    forall a. QNamed a -> a
    qnamed (QNamed [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)])
    -> (LHSCore' e -> QNamed [NamedArg (Pattern' e)])
    -> LHSCore' e
    -> [NamedArg (Pattern' e)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LHSCore' e -> QNamed [NamedArg (Pattern' e)]
    forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
    lhsCoreToSpine

    -- | Used in ''Agda.Syntax.Translation.AbstractToConcrete''.
    --   Returns a 'DefP'.
    lhsCoreToPattern :: LHSCore -> Pattern
    lhsCoreToPattern :: LHSCore -> Pattern
    lhsCoreToPattern LHSCore
    lc =
      case LHSCore
    lc of
        LHSHead QName
    f NAPs Expr
    aps         -> PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    DefP PatInfo
    noInfo (QName -> AmbiguousQName
    unambiguous QName
    f) NAPs Expr
    aps
        LHSProj AmbiguousQName
    d NamedArg LHSCore
    lhscore NAPs Expr
    aps -> PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    DefP PatInfo
    noInfo AmbiguousQName
    d (NAPs Expr -> Pattern) -> NAPs Expr -> Pattern
    forall a b. (a -> b) -> a -> b
    $
          (Named NamedName LHSCore -> Named NamedName Pattern)
    -> NamedArg LHSCore -> NamedArg Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((LHSCore -> Pattern)
    -> Named NamedName LHSCore -> Named NamedName Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap LHSCore -> Pattern
    lhsCoreToPattern) NamedArg LHSCore
    lhscore NamedArg Pattern -> NAPs Expr -> NAPs Expr
    forall a. a -> [a] -> [a]
    : NAPs Expr
    aps
        LHSWith LHSCore
    h [Arg Pattern]
    wps NAPs Expr
    aps     -> case LHSCore -> Pattern
    lhsCoreToPattern LHSCore
    h of
          DefP PatInfo
    r AmbiguousQName
    q NAPs Expr
    ps         -> PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    DefP PatInfo
    r AmbiguousQName
    q (NAPs Expr -> Pattern) -> NAPs Expr -> Pattern
    forall a b. (a -> b) -> a -> b
    $ NAPs Expr
    ps NAPs Expr -> NAPs Expr -> NAPs Expr
    forall a. [a] -> [a] -> [a]
    ++ (Arg Pattern -> NamedArg Pattern) -> [Arg Pattern] -> NAPs Expr
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Pattern -> NamedArg Pattern
    fromWithPat [Arg Pattern]
    wps NAPs Expr -> NAPs Expr -> NAPs Expr
    forall a. [a] -> [a] -> [a]
    ++ NAPs Expr
    aps
            where
              fromWithPat :: Arg Pattern -> NamedArg Pattern
              fromWithPat :: Arg Pattern -> NamedArg Pattern
    fromWithPat = (Pattern -> Named NamedName Pattern)
    -> Arg Pattern -> NamedArg Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Pattern -> Named NamedName Pattern
    forall a name. a -> Named name a
    unnamed (Pattern -> Named NamedName Pattern)
    -> (Pattern -> Pattern) -> Pattern -> Named NamedName Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern -> Pattern
    forall {e}. Pattern' e -> Pattern' e
    mkWithP)
              mkWithP :: Pattern' e -> Pattern' e
    mkWithP Pattern' e
    p   = PatInfo -> Pattern' e -> Pattern' e
    forall e. PatInfo -> Pattern' e -> Pattern' e
    WithP (Range -> PatInfo
    PatRange (Range -> PatInfo) -> Range -> PatInfo
    forall a b. (a -> b) -> a -> b
    $ Pattern' e -> Range
    forall a. HasRange a => a -> Range
    getRange Pattern' e
    p) Pattern' e
    p
          Pattern
    _ -> Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where noInfo :: PatInfo
    noInfo = PatInfo
    forall a. Null a => a
    empty -- TODO, preserve range!

    mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore
    mapLHSHead :: (QName -> NAPs Expr -> LHSCore) -> LHSCore -> LHSCore
    mapLHSHead QName -> NAPs Expr -> LHSCore
    f = \case
      LHSHead QName
    x NAPs Expr
    ps     -> QName -> NAPs Expr -> LHSCore
    f QName
    x NAPs Expr
    ps
      LHSProj AmbiguousQName
    d NamedArg LHSCore
    h NAPs Expr
    ps   -> AmbiguousQName -> NamedArg LHSCore -> NAPs Expr -> LHSCore
    forall e.
    AmbiguousQName
    -> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
    LHSProj AmbiguousQName
    d ((Named NamedName LHSCore -> Named NamedName LHSCore)
    -> NamedArg LHSCore -> NamedArg LHSCore
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((LHSCore -> LHSCore)
    -> Named NamedName LHSCore -> Named NamedName LHSCore
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((QName -> NAPs Expr -> LHSCore) -> LHSCore -> LHSCore
    mapLHSHead QName -> NAPs Expr -> LHSCore
    f)) NamedArg LHSCore
    h) NAPs Expr
    ps
      LHSWith LHSCore
    h [Arg Pattern]
    wps NAPs Expr
    ps -> LHSCore -> [Arg Pattern] -> NAPs Expr -> LHSCore
    forall e.
    LHSCore' e
    -> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
    LHSWith ((QName -> NAPs Expr -> LHSCore) -> LHSCore -> LHSCore
    mapLHSHead QName -> NAPs Expr -> LHSCore
    f LHSCore
    h) [Arg Pattern]
    wps NAPs Expr
    ps