    -- | 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.Monad.Reader    ( Reader, runReader, asks, local )
    import Control.Applicative     ( liftA2 )

    import Data.Maybe
    import Data.Monoid
    import Data.Void (Void)

    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.List1 ( List1, pattern (:|) )
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Null
    import Agda.Utils.Singleton

    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') -> a -> a
    (a' -> a') -> f a' -> f a'
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a' -> a') -> a -> a)
    -> ((NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
        -> a' -> a')
    -> (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> a
    -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a' -> a'
    forall a.
    MapNamedArgPattern a =>
    (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
    mapNamedArgPattern

    instance MapNamedArgPattern NAP where
      mapNamedArgPattern :: (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f NamedArg (Pattern' Expr)
    p =
        case NamedArg (Pattern' Expr) -> Pattern' Expr
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' Expr)
    p of
          -- no sub patterns:
          VarP{}    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f NamedArg (Pattern' Expr)
    p
          WildP{}   -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f NamedArg (Pattern' Expr)
    p
          DotP{}    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f NamedArg (Pattern' Expr)
    p
          EqualP{}  -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f NamedArg (Pattern' Expr)
    p
          LitP{}    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f NamedArg (Pattern' Expr)
    p
          AbsurdP{} -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f NamedArg (Pattern' Expr)
    p
          ProjP{}   -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f NamedArg (Pattern' Expr)
    p
          -- list of NamedArg subpatterns:
          ConP ConPatInfo
    i AmbiguousQName
    qs NAPs Expr
    ps       -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ NamedArg (Pattern' Expr)
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg (Pattern' Expr)
    p (Pattern' Expr -> NamedArg (Pattern' Expr))
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ ConPatInfo -> AmbiguousQName -> NAPs Expr -> Pattern' Expr
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    ConP ConPatInfo
    i AmbiguousQName
    qs (NAPs Expr -> Pattern' Expr) -> NAPs Expr -> Pattern' Expr
    forall a b. (a -> b) -> a -> b
    $ (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NAPs Expr -> NAPs Expr
    forall a.
    MapNamedArgPattern a =>
    (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
    mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f NAPs Expr
    ps
          DefP PatInfo
    i AmbiguousQName
    qs NAPs Expr
    ps       -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ NamedArg (Pattern' Expr)
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg (Pattern' Expr)
    p (Pattern' Expr -> NamedArg (Pattern' Expr))
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern' Expr
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    DefP PatInfo
    i AmbiguousQName
    qs (NAPs Expr -> Pattern' Expr) -> NAPs Expr -> Pattern' Expr
    forall a b. (a -> b) -> a -> b
    $ (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NAPs Expr -> NAPs Expr
    forall a.
    MapNamedArgPattern a =>
    (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
    mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f NAPs Expr
    ps
          PatternSynP PatInfo
    i AmbiguousQName
    x NAPs Expr
    ps -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ NamedArg (Pattern' Expr)
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg (Pattern' Expr)
    p (Pattern' Expr -> NamedArg (Pattern' Expr))
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern' Expr
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    PatternSynP PatInfo
    i AmbiguousQName
    x (NAPs Expr -> Pattern' Expr) -> NAPs Expr -> Pattern' Expr
    forall a b. (a -> b) -> a -> b
    $ (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NAPs Expr -> NAPs Expr
    forall a.
    MapNamedArgPattern a =>
    (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
    mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f NAPs Expr
    ps
          -- Pattern subpattern(s):
          -- RecP: we copy the NamedArg info to the subpatterns but discard it after recursion
          RecP KwRange
    kwr ConPatInfo
    i [FieldAssignment' (Pattern' Expr)]
    fs      -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ NamedArg (Pattern' Expr)
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg (Pattern' Expr)
    p (Pattern' Expr -> NamedArg (Pattern' Expr))
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ KwRange
    -> ConPatInfo
    -> [FieldAssignment' (Pattern' Expr)]
    -> Pattern' Expr
    forall e.
    KwRange
    -> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    RecP KwRange
    kwr ConPatInfo
    i ([FieldAssignment' (Pattern' Expr)] -> Pattern' Expr)
    -> [FieldAssignment' (Pattern' Expr)] -> Pattern' Expr
    forall a b. (a -> b) -> a -> b
    $ (FieldAssignment' (NamedArg (Pattern' Expr))
     -> FieldAssignment' (Pattern' Expr))
    -> [FieldAssignment' (NamedArg (Pattern' Expr))]
    -> [FieldAssignment' (Pattern' Expr)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((NamedArg (Pattern' Expr) -> Pattern' Expr)
    -> FieldAssignment' (NamedArg (Pattern' Expr))
    -> FieldAssignment' (Pattern' Expr)
    forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NamedArg (Pattern' Expr) -> Pattern' Expr
    forall a. NamedArg a -> a
    namedArg) ([FieldAssignment' (NamedArg (Pattern' Expr))]
     -> [FieldAssignment' (Pattern' Expr)])
    -> [FieldAssignment' (NamedArg (Pattern' Expr))]
    -> [FieldAssignment' (Pattern' Expr)]
    forall a b. (a -> b) -> a -> b
    $ (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> [FieldAssignment' (NamedArg (Pattern' Expr))]
    -> [FieldAssignment' (NamedArg (Pattern' Expr))]
    forall a.
    MapNamedArgPattern a =>
    (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
    mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f ([FieldAssignment' (NamedArg (Pattern' Expr))]
     -> [FieldAssignment' (NamedArg (Pattern' Expr))])
    -> [FieldAssignment' (NamedArg (Pattern' Expr))]
    -> [FieldAssignment' (NamedArg (Pattern' Expr))]
    forall a b. (a -> b) -> a -> b
    $ (FieldAssignment' (Pattern' Expr)
     -> FieldAssignment' (NamedArg (Pattern' Expr)))
    -> [FieldAssignment' (Pattern' Expr)]
    -> [FieldAssignment' (NamedArg (Pattern' Expr))]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Pattern' Expr -> NamedArg (Pattern' Expr))
    -> FieldAssignment' (Pattern' Expr)
    -> FieldAssignment' (NamedArg (Pattern' Expr))
    forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (NamedArg (Pattern' Expr)
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg (Pattern' Expr)
    p)) [FieldAssignment' (Pattern' Expr)]
    fs
          -- AsP: we hand the NamedArg info to the subpattern
          AsP PatInfo
    i BindName
    x Pattern' Expr
    p0         -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ (Pattern' Expr -> Pattern' Expr)
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> NamedArg a -> NamedArg b
    updateNamedArg (PatInfo -> BindName -> Pattern' Expr -> Pattern' Expr
    forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
    AsP PatInfo
    i BindName
    x) (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a.
    MapNamedArgPattern a =>
    (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
    mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ NamedArg (Pattern' Expr)
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg (Pattern' Expr)
    p Pattern' Expr
    p0
          -- WithP: like AsP
          WithP PatInfo
    i Pattern' Expr
    p0         -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ (Pattern' Expr -> Pattern' Expr)
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> NamedArg a -> NamedArg b
    updateNamedArg (PatInfo -> Pattern' Expr -> Pattern' Expr
    forall e. PatInfo -> Pattern' e -> Pattern' e
    WithP PatInfo
    i) (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a.
    MapNamedArgPattern a =>
    (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
    mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ NamedArg (Pattern' Expr)
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg (Pattern' Expr)
    p Pattern' Expr
    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' Expr) -> NamedArg (Pattern' Expr))
    -> (a, b) -> (a, b)
    mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f (a
    a, b
    b) = ((NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
    forall a.
    MapNamedArgPattern a =>
    (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
    mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    f a
    a, (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> b -> b
    forall a.
    MapNamedArgPattern a =>
    (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
    mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    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) -> p -> m
    (b -> m) -> f b -> m
    forall m a. Monoid m => (a -> m) -> f a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((b -> m) -> p -> m)
    -> ((Pattern' (ADotT b) -> m -> m) -> b -> m)
    -> (Pattern' (ADotT b) -> m -> m)
    -> p
    -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern' (ADotT b) -> m -> m) -> b -> m
    forall m. Monoid m => (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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> f a -> f (f 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
    forall (m :: * -> *).
    Monad m =>
    (Pattern' (ADotT q) -> m (Pattern' (ADotT q)))
    -> (Pattern' (ADotT q) -> m (Pattern' (ADotT q))) -> q -> m q
    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 m. Monoid m => (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
    forall (m :: * -> *).
    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 a. a -> m a
    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
    forall (m :: * -> *).
    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 a. a -> m a
    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 m.
    Monoid m =>
    (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 m.
    Monoid m =>
    (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 m.
    Monoid m =>
    (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 KwRange
    _ ConPatInfo
    _ [FieldAssignment' (Pattern' a)]
    ps        -> (Pattern' (ADotT [FieldAssignment' (Pattern' a)]) -> m -> m)
    -> [FieldAssignment' (Pattern' a)] -> m
    forall m.
    Monoid m =>
    (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 m.
    Monoid m =>
    (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 m.
    Monoid m =>
    (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
    _ List1 (a, a)
    _         -> m
    forall a. Monoid a => a
    mempty

      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 a. a -> m 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 a. a -> m 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 a. a -> m 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 a. a -> m 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 a. a -> m 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 a. a -> m 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 a. a -> m 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
    forall (m :: * -> *).
    Monad m =>
    (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
    -> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
    -> NAPs a
    -> m (NAPs a)
    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
    forall (m :: * -> *).
    Monad m =>
    (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
    -> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
    -> NAPs a
    -> m (NAPs a)
    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
    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
    p
          A.RecP    KwRange
    kwr ConPatInfo
    i    [FieldAssignment' (Pattern' a)]
    ps -> KwRange
    -> ConPatInfo -> [FieldAssignment' (Pattern' a)] -> Pattern' a
    forall e.
    KwRange
    -> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    A.RecP    KwRange
    kwr ConPatInfo
    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
    forall (m :: * -> *).
    Monad m =>
    (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)]
    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
    forall (m :: * -> *).
    Monad m =>
    (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
    -> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
    -> NAPs a
    -> m (NAPs a)
    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
    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
    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 m. Monoid m => (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 m. Monoid m => (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 a b c. (a -> b -> c) -> m a -> m b -> m c
    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
    forall (m :: * -> *).
    Monad m =>
    (Pattern' (ADotT a) -> m (Pattern' (ADotT a)))
    -> (Pattern' (ADotT a) -> m (Pattern' (ADotT a))) -> a -> m a
    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
    forall (m :: * -> *).
    Monad m =>
    (Pattern' (ADotT b) -> m (Pattern' (ADotT b)))
    -> (Pattern' (ADotT b) -> m (Pattern' (ADotT b))) -> b -> m b
    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

    -- | 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 -> (List1 C.Name -> m ()) -> m ()
    checkPatternLinearity :: forall (m :: * -> *) p.
    (Monad m, APatternLike p) =>
    p -> (List1 Name -> m ()) -> m ()
    checkPatternLinearity =
      [Name] -> (List1 Name -> m ()) -> m ()
    forall (m :: * -> *) a.
    Applicative m =>
    [a] -> (List1 a -> m ()) -> m ()
    List1.unlessNull ([Name] -> (List1 Name -> m ()) -> m ())
    -> (p -> [Name]) -> p -> (List1 Name -> m ()) -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Name] -> [Name]
    forall a. Ord a => [a] -> [a]
    duplicates ([Name] -> [Name]) -> (p -> [Name]) -> p -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name -> Name) -> [Name] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Name
    nameConcrete ([Name] -> [Name]) -> (p -> [Name]) -> p -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p -> [Name]
    forall p. APatternLike p => p -> [Name]
    patternVars

    -- * 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' Expr)] -> Pattern' Expr -> Pattern' Expr
    substPattern [(Name, Pattern' Expr)]
    s = (Expr -> Expr)
    -> [(Name, Pattern' Expr)] -> Pattern' Expr -> Pattern' Expr
    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' Expr) -> (Name, Expr))
    -> [(Name, Pattern' Expr)] -> [(Name, Expr)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Pattern' Expr -> Expr) -> (Name, Pattern' Expr) -> (Name, Expr)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second Pattern' Expr -> Expr
    patternToExpr) [(Name, Pattern' Expr)]
    s) [(Name, Pattern' Expr)]
    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' (ADotT (Pattern' e))
    -> Maybe (Pattern' (ADotT (Pattern' e)))
    -> Pattern' (ADotT (Pattern' e))
    forall a. a -> Maybe a -> a
    fromMaybe Pattern' (ADotT (Pattern' e))
    p (Maybe (Pattern' (ADotT (Pattern' e)))
     -> Pattern' (ADotT (Pattern' e)))
    -> Maybe (Pattern' (ADotT (Pattern' e)))
    -> Pattern' (ADotT (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 List1 (ADotT (Pattern' e), ADotT (Pattern' e))
    es       -> PatInfo
    -> List1 (ADotT (Pattern' e), ADotT (Pattern' e))
    -> Pattern' (ADotT (Pattern' e))
    forall e. PatInfo -> List1 (e, e) -> Pattern' e
    EqualP PatInfo
    i (List1 (ADotT (Pattern' e), ADotT (Pattern' e))
     -> Pattern' (ADotT (Pattern' e)))
    -> List1 (ADotT (Pattern' e), ADotT (Pattern' e))
    -> Pattern' (ADotT (Pattern' e))
    forall a b. (a -> b) -> a -> b
    $ ((e, e) -> (e, e)) -> NonEmpty (e, e) -> NonEmpty (e, e)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (e -> e
    subE (e -> e) -> (e -> e) -> (e, e) -> (e, e)
    forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** e -> e
    subE) NonEmpty (e, e)
    List1 (ADotT (Pattern' e), ADotT (Pattern' e))
    es
      -- No action on the other patterns (besides the recursion):
      ConP ConPatInfo
    _ AmbiguousQName
    _ NAPs (ADotT (Pattern' e))
    _        -> Pattern' (ADotT (Pattern' e))
    p
      RecP KwRange
    _ ConPatInfo
    _ [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

    -- | Convert a pattern to an expression.
    --
    -- Does not support all cases of patterns.
    -- Result has no 'Range' info, except in identifiers.
    --
    -- This function is only used in expanding pattern synonyms
    -- and in "Agda.Syntax.Translation.InternalToAbstract",
    -- so we can cut some corners.
    patternToExpr :: Pattern -> Expr
    patternToExpr :: Pattern' Expr -> Expr
    patternToExpr Pattern' Expr
    p = Pattern' Expr -> Reader Hiding Expr
    forall p e. PatternToExpr p e => p -> Reader Hiding e
    patToExpr Pattern' Expr
    p Reader Hiding Expr -> Hiding -> Expr
    forall r a. Reader r a -> r -> a
    `runReader` Hiding
    forall a. Null a => a
    empty

    -- | Converting a pattern to an expression.
    --
    --   The 'Hiding' context is remembered to create instance metas
    --   when translating absurd patterns in instance position.
    --
    class PatternToExpr p e where
      patToExpr :: p -> Reader Hiding e

      default patToExpr :: (Traversable t, PatternToExpr p' e', p ~ t p', e ~ t e')
        => p -> Reader Hiding e
      patToExpr = (p' -> ReaderT Hiding Identity e')
    -> t p' -> ReaderT Hiding Identity (t e')
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b)
    traverse p' -> ReaderT Hiding Identity e'
    forall p e. PatternToExpr p e => p -> Reader Hiding e
    patToExpr

    instance PatternToExpr p e => PatternToExpr [p] [e]
    instance PatternToExpr p e => PatternToExpr (Named n p) (Named n e)
    instance PatternToExpr p e => PatternToExpr (FieldAssignment' p) (FieldAssignment' e)

    instance PatternToExpr p e => PatternToExpr (Arg p) (Arg e) where
      patToExpr :: Arg p -> Reader Hiding (Arg e)
    patToExpr (Arg ArgInfo
    ai p
    p) = (Hiding -> Hiding)
    -> Reader Hiding (Arg e) -> Reader Hiding (Arg e)
    forall a.
    (Hiding -> Hiding)
    -> ReaderT Hiding Identity a -> ReaderT Hiding Identity a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (Hiding -> Hiding -> Hiding
    forall a b. a -> b -> a
    const (Hiding -> Hiding -> Hiding) -> Hiding -> Hiding -> Hiding
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    ai) (Reader Hiding (Arg e) -> Reader Hiding (Arg e))
    -> Reader Hiding (Arg e) -> Reader Hiding (Arg e)
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> e -> Arg e
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (e -> Arg e) -> ReaderT Hiding Identity e -> Reader Hiding (Arg e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> p -> ReaderT Hiding Identity e
    forall p e. PatternToExpr p e => p -> Reader Hiding e
    patToExpr p
    p

    instance PatternToExpr Pattern Expr where
      patToExpr :: Pattern' Expr -> Reader Hiding Expr
    patToExpr = \case
        VarP BindName
    x             -> Expr -> Reader Hiding Expr
    forall a. a -> ReaderT Hiding Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> Reader Hiding Expr) -> Expr -> Reader Hiding Expr
    forall a b. (a -> b) -> a -> b
    $ Name -> Expr
    Var (BindName -> Name
    unBind BindName
    x)
        ConP ConPatInfo
    _ AmbiguousQName
    c NAPs Expr
    ps        -> Expr -> [NamedArg Expr] -> Expr
    app (AmbiguousQName -> Expr
    Con AmbiguousQName
    c) ([NamedArg Expr] -> Expr)
    -> ReaderT Hiding Identity [NamedArg Expr] -> Reader Hiding Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NAPs Expr -> ReaderT Hiding Identity [NamedArg Expr]
    forall p e. PatternToExpr p e => p -> Reader Hiding e
    patToExpr NAPs Expr
    ps
        ProjP PatInfo
    _ ProjOrigin
    o AmbiguousQName
    ds       -> Expr -> Reader Hiding Expr
    forall a. a -> ReaderT Hiding Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> Reader Hiding Expr) -> Expr -> Reader Hiding Expr
    forall a b. (a -> b) -> a -> b
    $ ProjOrigin -> AmbiguousQName -> Expr
    Proj ProjOrigin
    o AmbiguousQName
    ds
        DefP PatInfo
    _ AmbiguousQName
    fs NAPs Expr
    ps       -> Expr -> [NamedArg Expr] -> Expr
    app (QName -> Expr
    Def (QName -> Expr) -> QName -> Expr
    forall a b. (a -> b) -> a -> b
    $ AmbiguousQName -> QName
    headAmbQ AmbiguousQName
    fs) ([NamedArg Expr] -> Expr)
    -> ReaderT Hiding Identity [NamedArg Expr] -> Reader Hiding Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NAPs Expr -> ReaderT Hiding Identity [NamedArg Expr]
    forall p e. PatternToExpr p e => p -> Reader Hiding e
    patToExpr NAPs Expr
    ps
        WildP PatInfo
    _            -> Expr -> Reader Hiding Expr
    forall a. a -> ReaderT Hiding Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> Reader Hiding Expr) -> Expr -> Reader Hiding Expr
    forall a b. (a -> b) -> a -> b
    $ MetaInfo -> Expr
    Underscore MetaInfo
    emptyMetaInfo
        AsP PatInfo
    _ BindName
    _ Pattern' Expr
    p          -> Pattern' Expr -> Reader Hiding Expr
    forall p e. PatternToExpr p e => p -> Reader Hiding e
    patToExpr Pattern' Expr
    p
        DotP PatInfo
    _ Expr
    e           -> Expr -> Reader Hiding Expr
    forall a. a -> ReaderT Hiding Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr
    e
        -- Issue #7176: An absurd pattern in an instance position should turn into an instance meta:
        AbsurdP PatInfo
    _          -> (Hiding -> MetaKind) -> ReaderT Hiding Identity MetaKind
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks Hiding -> MetaKind
    hidingToMetaKind ReaderT Hiding Identity MetaKind
    -> (MetaKind -> Expr) -> Reader Hiding Expr
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ MetaKind
    k -> MetaInfo -> Expr
    Underscore MetaInfo
    emptyMetaInfo{ metaKind = k }
        LitP PatInfo
    _ Literal
    l           -> Expr -> Reader Hiding Expr
    forall a. a -> ReaderT Hiding Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> Reader Hiding Expr) -> Expr -> Reader Hiding Expr
    forall a b. (a -> b) -> a -> b
    $ ExprInfo -> Literal -> Expr
    Lit ExprInfo
    forall a. Null a => a
    empty Literal
    l
        PatternSynP PatInfo
    _ AmbiguousQName
    c NAPs Expr
    ps -> Expr -> [NamedArg Expr] -> Expr
    app (AmbiguousQName -> Expr
    PatternSyn AmbiguousQName
    c) ([NamedArg Expr] -> Expr)
    -> ReaderT Hiding Identity [NamedArg Expr] -> Reader Hiding Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NAPs Expr -> ReaderT Hiding Identity [NamedArg Expr]
    forall p e. PatternToExpr p e => p -> Reader Hiding e
    patToExpr NAPs Expr
    ps
        RecP KwRange
    kwr ConPatInfo
    _ [FieldAssignment' (Pattern' Expr)]
    as      -> KwRange -> ExprInfo -> RecordAssigns -> Expr
    Rec KwRange
    kwr ExprInfo
    exprNoRange (RecordAssigns -> Expr)
    -> ([Assign] -> RecordAssigns) -> [Assign] -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Assign -> RecordAssign) -> [Assign] -> RecordAssigns
    forall a b. (a -> b) -> [a] -> [b]
    map Assign -> RecordAssign
    forall a b. a -> Either a b
    Left ([Assign] -> Expr)
    -> ReaderT Hiding Identity [Assign] -> Reader Hiding Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [FieldAssignment' (Pattern' Expr)]
    -> ReaderT Hiding Identity [Assign]
    forall p e. PatternToExpr p e => p -> Reader Hiding e
    patToExpr [FieldAssignment' (Pattern' Expr)]
    as
        EqualP{}           -> Reader Hiding Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- Andrea TODO: where is this used?
        WithP PatInfo
    r Pattern' Expr
    p          -> Reader Hiding Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Make sure that there are no dot or equality patterns (called on pattern synonyms).
    --   Also disallows annotated patterns.
    --
    noDotOrEqPattern :: forall m e. Monad m
      => m (A.Pattern' Void)   -- ^ Exception or replacement for dot (etc.) patterns.
      -> A.Pattern' e          -- ^ In pattern.
      -> m (A.Pattern' Void)   -- ^ Out pattern.
    noDotOrEqPattern :: forall (m :: * -> *) e.
    Monad m =>
    m (Pattern' Void) -> Pattern' e -> m (Pattern' Void)
    noDotOrEqPattern m (Pattern' Void)
    err = Pattern' e -> m (Pattern' Void)
    dot
      where
        dot :: A.Pattern' e -> m (A.Pattern' Void)
        dot :: Pattern' e -> m (Pattern' Void)
    dot = \case
          A.VarP BindName
    x               -> Pattern' Void -> m (Pattern' Void)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern' Void -> m (Pattern' Void))
    -> Pattern' Void -> m (Pattern' Void)
    forall a b. (a -> b) -> a -> b
    $ BindName -> Pattern' Void
    forall e. BindName -> Pattern' e
    A.VarP BindName
    x
          A.ConP ConPatInfo
    i AmbiguousQName
    c NAPs e
    args        -> ConPatInfo -> AmbiguousQName -> NAPs Void -> Pattern' Void
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.ConP ConPatInfo
    i AmbiguousQName
    c (NAPs Void -> Pattern' Void) -> m (NAPs Void) -> m (Pattern' Void)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
    -> NAPs e -> m (NAPs Void)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse ((NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
     -> NAPs e -> m (NAPs Void))
    -> (NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
    -> NAPs e
    -> m (NAPs Void)
    forall a b. (a -> b) -> a -> b
    $ (Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
    -> NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse ((Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
     -> NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
    -> (Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
    -> NamedArg (Pattern' e)
    -> m (NamedArg (Pattern' Void))
    forall a b. (a -> b) -> a -> b
    $ (Pattern' e -> m (Pattern' Void))
    -> Named_ (Pattern' e) -> m (Named_ (Pattern' Void))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Named NamedName a -> f (Named NamedName b)
    traverse Pattern' e -> m (Pattern' Void)
    dot) NAPs e
    args
          A.ProjP PatInfo
    i ProjOrigin
    o AmbiguousQName
    d          -> Pattern' Void -> m (Pattern' Void)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern' Void -> m (Pattern' Void))
    -> Pattern' Void -> m (Pattern' Void)
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' Void
    forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
    A.ProjP PatInfo
    i ProjOrigin
    o AmbiguousQName
    d
          A.WildP PatInfo
    i              -> Pattern' Void -> m (Pattern' Void)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern' Void -> m (Pattern' Void))
    -> Pattern' Void -> m (Pattern' Void)
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern' Void
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    i
          A.AsP PatInfo
    i BindName
    x Pattern' e
    p            -> PatInfo -> BindName -> Pattern' Void -> Pattern' Void
    forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
    A.AsP PatInfo
    i BindName
    x (Pattern' Void -> Pattern' Void)
    -> m (Pattern' Void) -> m (Pattern' Void)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern' e -> m (Pattern' Void)
    dot Pattern' e
    p
          A.DotP{}               -> m (Pattern' Void)
    err
          A.EqualP{}             -> m (Pattern' Void)
    err   -- Andrea: so we also disallow = patterns, reasonable?
          A.AbsurdP PatInfo
    i            -> Pattern' Void -> m (Pattern' Void)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern' Void -> m (Pattern' Void))
    -> Pattern' Void -> m (Pattern' Void)
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern' Void
    forall e. PatInfo -> Pattern' e
    A.AbsurdP PatInfo
    i
          A.LitP PatInfo
    i Literal
    l             -> Pattern' Void -> m (Pattern' Void)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern' Void -> m (Pattern' Void))
    -> Pattern' Void -> m (Pattern' Void)
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Literal -> Pattern' Void
    forall e. PatInfo -> Literal -> Pattern' e
    A.LitP PatInfo
    i Literal
    l
          A.DefP PatInfo
    i AmbiguousQName
    f NAPs e
    args        -> PatInfo -> AmbiguousQName -> NAPs Void -> Pattern' Void
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.DefP PatInfo
    i AmbiguousQName
    f (NAPs Void -> Pattern' Void) -> m (NAPs Void) -> m (Pattern' Void)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
    -> NAPs e -> m (NAPs Void)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse ((NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
     -> NAPs e -> m (NAPs Void))
    -> (NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
    -> NAPs e
    -> m (NAPs Void)
    forall a b. (a -> b) -> a -> b
    $ (Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
    -> NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse ((Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
     -> NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
    -> (Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
    -> NamedArg (Pattern' e)
    -> m (NamedArg (Pattern' Void))
    forall a b. (a -> b) -> a -> b
    $ (Pattern' e -> m (Pattern' Void))
    -> Named_ (Pattern' e) -> m (Named_ (Pattern' Void))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Named NamedName a -> f (Named NamedName b)
    traverse Pattern' e -> m (Pattern' Void)
    dot) NAPs e
    args
          A.PatternSynP PatInfo
    i AmbiguousQName
    c NAPs e
    args -> PatInfo -> AmbiguousQName -> NAPs Void -> Pattern' Void
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.PatternSynP PatInfo
    i AmbiguousQName
    c (NAPs Void -> Pattern' Void) -> m (NAPs Void) -> m (Pattern' Void)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
    -> NAPs e -> m (NAPs Void)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse ((NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
     -> NAPs e -> m (NAPs Void))
    -> (NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
    -> NAPs e
    -> m (NAPs Void)
    forall a b. (a -> b) -> a -> b
    $ (Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
    -> NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse ((Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
     -> NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
    -> (Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
    -> NamedArg (Pattern' e)
    -> m (NamedArg (Pattern' Void))
    forall a b. (a -> b) -> a -> b
    $ (Pattern' e -> m (Pattern' Void))
    -> Named_ (Pattern' e) -> m (Named_ (Pattern' Void))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Named NamedName a -> f (Named NamedName b)
    traverse Pattern' e -> m (Pattern' Void)
    dot) NAPs e
    args
          A.RecP KwRange
    kwr ConPatInfo
    i [FieldAssignment' (Pattern' e)]
    fs        -> KwRange
    -> ConPatInfo
    -> [FieldAssignment' (Pattern' Void)]
    -> Pattern' Void
    forall e.
    KwRange
    -> ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
    A.RecP KwRange
    kwr ConPatInfo
    i ([FieldAssignment' (Pattern' Void)] -> Pattern' Void)
    -> m [FieldAssignment' (Pattern' Void)] -> m (Pattern' Void)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((FieldAssignment' (Pattern' e)
     -> m (FieldAssignment' (Pattern' Void)))
    -> [FieldAssignment' (Pattern' e)]
    -> m [FieldAssignment' (Pattern' Void)]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse ((FieldAssignment' (Pattern' e)
      -> m (FieldAssignment' (Pattern' Void)))
     -> [FieldAssignment' (Pattern' e)]
     -> m [FieldAssignment' (Pattern' Void)])
    -> (FieldAssignment' (Pattern' e)
        -> m (FieldAssignment' (Pattern' Void)))
    -> [FieldAssignment' (Pattern' e)]
    -> m [FieldAssignment' (Pattern' Void)]
    forall a b. (a -> b) -> a -> b
    $ (Pattern' e -> m (Pattern' Void))
    -> FieldAssignment' (Pattern' e)
    -> m (FieldAssignment' (Pattern' Void))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)
    traverse Pattern' e -> m (Pattern' Void)
    dot) [FieldAssignment' (Pattern' e)]
    fs
          A.WithP PatInfo
    i Pattern' e
    p            -> PatInfo -> Pattern' Void -> Pattern' Void
    forall e. PatInfo -> Pattern' e -> Pattern' e
    A.WithP PatInfo
    i (Pattern' Void -> Pattern' Void)
    -> m (Pattern' Void) -> m (Pattern' Void)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern' e -> m (Pattern' Void)
    dot 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' Expr) -> Bool)
    -> NAPs Expr -> (NAPs Expr, NAPs Expr)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    spanEnd (Maybe (NamedArg (Pattern' Expr)) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (NamedArg (Pattern' Expr)) -> Bool)
    -> (NamedArg (Pattern' Expr) -> Maybe (NamedArg (Pattern' Expr)))
    -> NamedArg (Pattern' Expr)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg (Pattern' Expr) -> Maybe (NamedArg (Pattern' Expr))
    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  (NAPs1 e)
          -- ^ Application patterns (non-empty list).
      | LHSProjP ProjOrigin AmbiguousQName (NamedArg (Pattern' e))
          -- ^ A projection pattern.  Is also stored unmodified here.
      | LHSWithP (List1 (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
    $cshowsPrec :: forall e. Show e => Int -> LHSPatternView e -> ShowS
    showsPrec :: Int -> LHSPatternView e -> ShowS
    $cshow :: forall e. Show e => LHSPatternView e -> String
    show :: LHSPatternView e -> String
    $cshowList :: forall e. Show e => [LHSPatternView e] -> ShowS
    showList :: [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 (List1 (Pattern' e) -> LHSPatternView e
    forall e. List1 (Pattern' e) -> LHSPatternView e
    LHSWithP (Pattern' e
    p Pattern' e -> [Pattern' e] -> List1 (Pattern' e)
    forall a. a -> [a] -> NonEmpty 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 (NAPs1 e -> LHSPatternView e
    forall e. NAPs1 e -> LHSPatternView e
    LHSAppP (NamedArg (Pattern' e)
    p0 NamedArg (Pattern' e) -> [NamedArg (Pattern' e)] -> NAPs1 e
    forall a. a -> [a] -> NonEmpty 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 a b. (a -> b) -> Clause' a -> Clause' b
    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 a b. (a -> b) -> Clause' a -> Clause' b
    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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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 List1 (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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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 (List1 (Arg (Pattern' e)) -> [Item (List1 (Arg (Pattern' e)))]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 (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_ (Pattern' e))
    -> Arg (Pattern' e) -> Arg (Named_ (Pattern' e))
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Pattern' e -> Named_ (Pattern' e)
    forall a name. a -> Named name a
    unnamed (Pattern' e -> Named_ (Pattern' e))
    -> (Pattern' e -> Pattern' e) -> Pattern' e -> Named_ (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 = lhsPats core ++ ps }

    -- | Add with-patterns to the right.
    lhsCoreWith :: LHSCore' e -> List1 (Arg (Pattern' e)) -> LHSCore' e
    lhsCoreWith :: forall e. LHSCore' e -> List1 (Arg (Pattern' e)) -> LHSCore' e
    lhsCoreWith (LHSWith LHSCore' e
    core List1 (Arg (Pattern' e))
    wps []) List1 (Arg (Pattern' e))
    wps' = LHSCore' e
    -> List1 (Arg (Pattern' e))
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    forall e.
    LHSCore' e
    -> List1 (Arg (Pattern' e))
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    LHSWith LHSCore' e
    core (List1 (Arg (Pattern' e))
    wps List1 (Arg (Pattern' e))
    -> List1 (Arg (Pattern' e)) -> List1 (Arg (Pattern' e))
    forall a. Semigroup a => a -> a -> a
    <> List1 (Arg (Pattern' e))
    wps') []
    lhsCoreWith LHSCore' e
    core                  List1 (Arg (Pattern' e))
    wps' = LHSCore' e
    -> List1 (Arg (Pattern' e))
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    forall e.
    LHSCore' e
    -> List1 (Arg (Pattern' e))
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    LHSWith LHSCore' e
    core List1 (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 NAPs1 e
    ps               -> LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
    forall e. LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
    lhsCoreApp LHSCore' e
    core ([NamedArg (Pattern' e)] -> LHSCore' e)
    -> [NamedArg (Pattern' e)] -> LHSCore' e
    forall a b. (a -> b) -> a -> b
    $ NAPs1 e -> [Item (NAPs1 e)]
    forall l. IsList l => l -> [Item l]
    List1.toList NAPs1 e
    ps
      LHSWithP List1 (Pattern' e)
    wps             -> LHSCore' e -> List1 (Arg (Pattern' e)) -> LHSCore' e
    forall e. LHSCore' e -> List1 (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))
    -> List1 (Pattern' e) -> List1 (Arg (Pattern' e))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> List1 (Pattern' e)
    wps)
      LHSProjP ProjOrigin
    ProjPrefix AmbiguousQName
    d NamedArg (Pattern' e)
    np -> AmbiguousQName
    -> NamedArg (LHSCore' e) -> [NamedArg (Pattern' 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 -> [NamedArg (Pattern' e)] -> LHSCore' e
    forall e. LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
    lhsCoreApp LHSCore' e
    core (NamedArg (Pattern' e) -> [NamedArg (Pattern' e)]
    forall el coll. Singleton el coll => el -> coll
    singleton 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 a. [a] -> 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' Expr
    lhsCoreToPattern LHSCore
    lc =
      case LHSCore
    lc of
        LHSHead QName
    f NAPs Expr
    aps         -> PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern' Expr
    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' Expr
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    DefP PatInfo
    noInfo AmbiguousQName
    d (NAPs Expr -> Pattern' Expr) -> NAPs Expr -> Pattern' Expr
    forall a b. (a -> b) -> a -> b
    $
          (Named NamedName LHSCore -> Named NamedName (Pattern' Expr))
    -> NamedArg LHSCore -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((LHSCore -> Pattern' Expr)
    -> Named NamedName LHSCore -> Named NamedName (Pattern' Expr)
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap LHSCore -> Pattern' Expr
    lhsCoreToPattern) NamedArg LHSCore
    lhscore NamedArg (Pattern' Expr) -> NAPs Expr -> NAPs Expr
    forall a. a -> [a] -> [a]
    : NAPs Expr
    aps
        LHSWith LHSCore
    h List1 (Arg (Pattern' Expr))
    wps NAPs Expr
    aps     -> case LHSCore -> Pattern' Expr
    lhsCoreToPattern LHSCore
    h of
          DefP PatInfo
    r AmbiguousQName
    q NAPs Expr
    ps         -> PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern' Expr
    forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    DefP PatInfo
    r AmbiguousQName
    q (NAPs Expr -> Pattern' Expr) -> NAPs Expr -> Pattern' Expr
    forall a b. (a -> b) -> a -> b
    $ NAPs Expr
    ps NAPs Expr -> NAPs Expr -> NAPs Expr
    forall a. [a] -> [a] -> [a]
    ++ (Arg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> [Arg (Pattern' Expr)] -> NAPs Expr
    forall a b. (a -> b) -> [a] -> [b]
    map Arg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    fromWithPat (List1 (Arg (Pattern' Expr)) -> [Item (List1 (Arg (Pattern' Expr)))]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 (Arg (Pattern' Expr))
    wps) NAPs Expr -> NAPs Expr -> NAPs Expr
    forall a. [a] -> [a] -> [a]
    ++ NAPs Expr
    aps
            where
              fromWithPat :: Arg Pattern -> NamedArg Pattern
              fromWithPat :: Arg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    fromWithPat = (Pattern' Expr -> Named NamedName (Pattern' Expr))
    -> Arg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Pattern' Expr -> Named NamedName (Pattern' Expr)
    forall a name. a -> Named name a
    unnamed (Pattern' Expr -> Named NamedName (Pattern' Expr))
    -> (Pattern' Expr -> Pattern' Expr)
    -> Pattern' Expr
    -> Named NamedName (Pattern' Expr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern' Expr -> Pattern' Expr
    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' Expr
    _ -> Pattern' Expr
    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 a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((LHSCore -> LHSCore)
    -> Named NamedName LHSCore -> Named NamedName LHSCore
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    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 List1 (Arg (Pattern' Expr))
    wps NAPs Expr
    ps -> LHSCore -> List1 (Arg (Pattern' Expr)) -> NAPs Expr -> LHSCore
    forall e.
    LHSCore' e
    -> List1 (Arg (Pattern' e))
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    LHSWith ((QName -> NAPs Expr -> LHSCore) -> LHSCore -> LHSCore
    mapLHSHead QName -> NAPs Expr -> LHSCore
    f LHSCore
    h) List1 (Arg (Pattern' Expr))
    wps NAPs Expr
    ps