    module Agda.Syntax.Internal.Elim where

    import Control.DeepSeq
    import Data.Data (Data)

    import Agda.Syntax.Common
    import Agda.Syntax.Concrete.Pretty () -- Pretty Arg instance
    import Agda.Syntax.Position
    import Agda.Syntax.Abstract.Name

    import Agda.Utils.Pretty
    import Agda.Utils.Empty
    import Agda.Utils.Maybe
    import Agda.Utils.Tuple

    -- | Eliminations, subsuming applications and projections.
    --
    data Elim' a
      = Apply (Arg a)         -- ^ Application.
      | Proj ProjOrigin QName -- ^ Projection.  'QName' is name of a record projection.
      | IApply a a a -- ^ IApply x y r, x and y are the endpoints
      deriving (Typeable (Elim' a)
    Typeable (Elim' a)
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> Elim' a -> c (Elim' a))
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c (Elim' a))
    -> (Elim' a -> Constr)
    -> (Elim' a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c (Elim' a)))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Elim' a)))
    -> ((forall b. Data b => b -> b) -> Elim' a -> Elim' a)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Elim' a -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Elim' a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Elim' a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Elim' a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a))
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a))
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a))
    -> Data (Elim' a)
    Elim' a -> DataType
    Elim' a -> Constr
    (forall b. Data b => b -> b) -> Elim' a -> Elim' a
    forall {a}. Data a => Typeable (Elim' a)
    forall a. Data a => Elim' a -> DataType
    forall a. Data a => Elim' a -> Constr
    forall a.
    Data a =>
    (forall b. Data b => b -> b) -> Elim' a -> Elim' a
    forall a u.
    Data a =>
    Int -> (forall d. Data d => d -> u) -> Elim' a -> u
    forall a u.
    Data a =>
    (forall d. Data d => d -> u) -> Elim' a -> [u]
    forall a r r'.
    Data a =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Elim' a -> r
    forall a r r'.
    Data a =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Elim' a -> r
    forall a (m :: * -> *).
    (Data a, Monad m) =>
    (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)
    forall a (m :: * -> *).
    (Data a, MonadPlus m) =>
    (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)
    forall a (c :: * -> *).
    Data a =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Elim' a)
    forall a (c :: * -> *).
    Data a =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Elim' a -> c (Elim' a)
    forall a (t :: * -> *) (c :: * -> *).
    (Data a, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (Elim' a))
    forall a (t :: * -> * -> *) (c :: * -> *).
    (Data a, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Elim' a))
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Elim' a -> u
    forall u. (forall d. Data d => d -> u) -> Elim' a -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Elim' a -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Elim' a -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Elim' a)
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Elim' a -> c (Elim' a)
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Elim' a))
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Elim' a))
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)
    $cgmapMo :: forall a (m :: * -> *).
    (Data a, MonadPlus m) =>
    (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)
    $cgmapMp :: forall a (m :: * -> *).
    (Data a, MonadPlus m) =>
    (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)
    $cgmapM :: forall a (m :: * -> *).
    (Data a, Monad m) =>
    (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Elim' a -> u
    $cgmapQi :: forall a u.
    Data a =>
    Int -> (forall d. Data d => d -> u) -> Elim' a -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Elim' a -> [u]
    $cgmapQ :: forall a u.
    Data a =>
    (forall d. Data d => d -> u) -> Elim' a -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Elim' a -> r
    $cgmapQr :: forall a r r'.
    Data a =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Elim' a -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Elim' a -> r
    $cgmapQl :: forall a r r'.
    Data a =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Elim' a -> r
    gmapT :: (forall b. Data b => b -> b) -> Elim' a -> Elim' a
    $cgmapT :: forall a.
    Data a =>
    (forall b. Data b => b -> b) -> Elim' a -> Elim' a
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Elim' a))
    $cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
    (Data a, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Elim' a))
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Elim' a))
    $cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
    (Data a, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (Elim' a))
    dataTypeOf :: Elim' a -> DataType
    $cdataTypeOf :: forall a. Data a => Elim' a -> DataType
    toConstr :: Elim' a -> Constr
    $ctoConstr :: forall a. Data a => Elim' a -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Elim' a)
    $cgunfold :: forall a (c :: * -> *).
    Data a =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Elim' a)
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Elim' a -> c (Elim' a)
    $cgfoldl :: forall a (c :: * -> *).
    Data a =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Elim' a -> c (Elim' a)
    Data, Int -> Elim' a -> ShowS
    [Elim' a] -> ShowS
    Elim' a -> String
    (Int -> Elim' a -> ShowS)
    -> (Elim' a -> String) -> ([Elim' a] -> ShowS) -> Show (Elim' a)
    forall a. Show a => Int -> Elim' a -> ShowS
    forall a. Show a => [Elim' a] -> ShowS
    forall a. Show a => Elim' a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Elim' a] -> ShowS
    $cshowList :: forall a. Show a => [Elim' a] -> ShowS
    show :: Elim' a -> String
    $cshow :: forall a. Show a => Elim' a -> String
    showsPrec :: Int -> Elim' a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> Elim' a -> ShowS
    Show, (forall a b. (a -> b) -> Elim' a -> Elim' b)
    -> (forall a b. a -> Elim' b -> Elim' a) -> Functor Elim'
    forall a b. a -> Elim' b -> Elim' a
    forall a b. (a -> b) -> Elim' a -> Elim' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> Elim' b -> Elim' a
    $c<$ :: forall a b. a -> Elim' b -> Elim' a
    fmap :: forall a b. (a -> b) -> Elim' a -> Elim' b
    $cfmap :: forall a b. (a -> b) -> Elim' a -> Elim' b
    Functor, (forall m. Monoid m => Elim' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Elim' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Elim' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Elim' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Elim' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Elim' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Elim' a -> b)
    -> (forall a. (a -> a -> a) -> Elim' a -> a)
    -> (forall a. (a -> a -> a) -> Elim' a -> a)
    -> (forall a. Elim' a -> [a])
    -> (forall a. Elim' a -> Bool)
    -> (forall a. Elim' a -> Int)
    -> (forall a. Eq a => a -> Elim' a -> Bool)
    -> (forall a. Ord a => Elim' a -> a)
    -> (forall a. Ord a => Elim' a -> a)
    -> (forall a. Num a => Elim' a -> a)
    -> (forall a. Num a => Elim' a -> a)
    -> Foldable Elim'
    forall a. Eq a => a -> Elim' a -> Bool
    forall a. Num a => Elim' a -> a
    forall a. Ord a => Elim' a -> a
    forall m. Monoid m => Elim' m -> m
    forall a. Elim' a -> Bool
    forall a. Elim' a -> Int
    forall a. Elim' a -> [a]
    forall a. (a -> a -> a) -> Elim' a -> a
    forall m a. Monoid m => (a -> m) -> Elim' a -> m
    forall b a. (b -> a -> b) -> b -> Elim' a -> b
    forall a b. (a -> b -> b) -> b -> Elim' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    product :: forall a. Num a => Elim' a -> a
    $cproduct :: forall a. Num a => Elim' a -> a
    sum :: forall a. Num a => Elim' a -> a
    $csum :: forall a. Num a => Elim' a -> a
    minimum :: forall a. Ord a => Elim' a -> a
    $cminimum :: forall a. Ord a => Elim' a -> a
    maximum :: forall a. Ord a => Elim' a -> a
    $cmaximum :: forall a. Ord a => Elim' a -> a
    elem :: forall a. Eq a => a -> Elim' a -> Bool
    $celem :: forall a. Eq a => a -> Elim' a -> Bool
    length :: forall a. Elim' a -> Int
    $clength :: forall a. Elim' a -> Int
    null :: forall a. Elim' a -> Bool
    $cnull :: forall a. Elim' a -> Bool
    toList :: forall a. Elim' a -> [a]
    $ctoList :: forall a. Elim' a -> [a]
    foldl1 :: forall a. (a -> a -> a) -> Elim' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Elim' a -> a
    foldr1 :: forall a. (a -> a -> a) -> Elim' a -> a
    $cfoldr1 :: forall a. (a -> a -> a) -> Elim' a -> a
    foldl' :: forall b a. (b -> a -> b) -> b -> Elim' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Elim' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Elim' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Elim' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Elim' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Elim' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Elim' a -> b
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Elim' a -> b
    foldMap' :: forall m a. Monoid m => (a -> m) -> Elim' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Elim' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Elim' a -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Elim' a -> m
    fold :: forall m. Monoid m => Elim' m -> m
    $cfold :: forall m. Monoid m => Elim' m -> m
    Foldable, Functor Elim'
    Foldable Elim'
    Functor Elim'
    -> Foldable Elim'
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> Elim' a -> f (Elim' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Elim' (f a) -> f (Elim' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Elim' a -> m (Elim' b))
    -> (forall (m :: * -> *) a. Monad m => Elim' (m a) -> m (Elim' a))
    -> Traversable Elim'
    forall (t :: * -> *).
    Functor t
    -> Foldable t
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => Elim' (m a) -> m (Elim' a)
    forall (f :: * -> *) a. Applicative f => Elim' (f a) -> f (Elim' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Elim' a -> m (Elim' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Elim' a -> f (Elim' b)
    sequence :: forall (m :: * -> *) a. Monad m => Elim' (m a) -> m (Elim' a)
    $csequence :: forall (m :: * -> *) a. Monad m => Elim' (m a) -> m (Elim' a)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Elim' a -> m (Elim' b)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Elim' a -> m (Elim' b)
    sequenceA :: forall (f :: * -> *) a. Applicative f => Elim' (f a) -> f (Elim' a)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => Elim' (f a) -> f (Elim' a)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Elim' a -> f (Elim' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Elim' a -> f (Elim' b)
    Traversable)

    -- | This instance cheats on 'Proj', use with care.
    --   'Proj's are always assumed to be 'UserWritten', since they have no 'ArgInfo'.
    --   Same for IApply
    instance LensOrigin (Elim' a) where
      getOrigin :: Elim' a -> Origin
    getOrigin (Apply Arg a
    a)   = Arg a -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin Arg a
    a
      getOrigin Proj{}      = Origin
    UserWritten
      getOrigin IApply{}    = Origin
    UserWritten
      mapOrigin :: (Origin -> Origin) -> Elim' a -> Elim' a
    mapOrigin Origin -> Origin
    f (Apply Arg a
    a) = Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply (Arg a -> Elim' a) -> Arg a -> Elim' a
    forall a b. (a -> b) -> a -> b
    $ (Origin -> Origin) -> Arg a -> Arg a
    forall a. LensOrigin a => (Origin -> Origin) -> a -> a
    mapOrigin Origin -> Origin
    f Arg a
    a
      mapOrigin Origin -> Origin
    f e :: Elim' a
    e@Proj{}  = Elim' a
    e
      mapOrigin Origin -> Origin
    f e :: Elim' a
    e@IApply{} = Elim' a
    e

    -- | Drop 'Apply' constructor. (Safe)
    isApplyElim :: Elim' a -> Maybe (Arg a)
    isApplyElim :: forall a. Elim' a -> Maybe (Arg a)
    isApplyElim (Apply Arg a
    u) = Arg a -> Maybe (Arg a)
    forall a. a -> Maybe a
    Just Arg a
    u
    isApplyElim Proj{}    = Maybe (Arg a)
    forall a. Maybe a
    Nothing
    isApplyElim (IApply a
    _ a
    _ a
    r) = Arg a -> Maybe (Arg a)
    forall a. a -> Maybe a
    Just (a -> Arg a
    forall a. a -> Arg a
    defaultArg a
    r)

    isApplyElim' :: Empty -> Elim' a -> Arg a
    isApplyElim' :: forall a. Empty -> Elim' a -> Arg a
    isApplyElim' Empty
    e = Arg a -> Maybe (Arg a) -> Arg a
    forall a. a -> Maybe a -> a
    fromMaybe (Empty -> Arg a
    forall a. Empty -> a
    absurd Empty
    e) (Maybe (Arg a) -> Arg a)
    -> (Elim' a -> Maybe (Arg a)) -> Elim' a -> Arg a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim' a -> Maybe (Arg a)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim

    -- | Drop 'Apply' constructors. (Safe)
    allApplyElims :: [Elim' a] -> Maybe [Arg a]
    allApplyElims :: forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims = (Elim' a -> Maybe (Arg a)) -> [Elim' a] -> Maybe [Arg a]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Elim' a -> Maybe (Arg a)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim

    -- | Split at first non-'Apply'
    splitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a])
    splitApplyElims :: forall a. [Elim' a] -> ([Arg a], [Elim' a])
    splitApplyElims (Apply Arg a
    u : [Elim' a]
    es) = ([Arg a] -> [Arg a])
    -> ([Arg a], [Elim' a]) -> ([Arg a], [Elim' a])
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst (Arg a
    u Arg a -> [Arg a] -> [Arg a]
    forall a. a -> [a] -> [a]
    :) (([Arg a], [Elim' a]) -> ([Arg a], [Elim' a]))
    -> ([Arg a], [Elim' a]) -> ([Arg a], [Elim' a])
    forall a b. (a -> b) -> a -> b
    $ [Elim' a] -> ([Arg a], [Elim' a])
    forall a. [Elim' a] -> ([Arg a], [Elim' a])
    splitApplyElims [Elim' a]
    es
    splitApplyElims [Elim' a]
    es             = ([], [Elim' a]
    es)

    class IsProjElim e where
      isProjElim  :: e -> Maybe (ProjOrigin, QName)

    instance IsProjElim (Elim' a) where
      isProjElim :: Elim' a -> Maybe (ProjOrigin, QName)
    isProjElim (Proj ProjOrigin
    o QName
    d) = (ProjOrigin, QName) -> Maybe (ProjOrigin, QName)
    forall a. a -> Maybe a
    Just (ProjOrigin
    o, QName
    d)
      isProjElim Apply{}    = Maybe (ProjOrigin, QName)
    forall a. Maybe a
    Nothing
      isProjElim IApply{} = Maybe (ProjOrigin, QName)
    forall a. Maybe a
    Nothing

    -- | Discards @Proj f@ entries.
    argsFromElims :: [Elim' t] -> [Arg t]
    argsFromElims :: forall t. [Elim' t] -> [Arg t]
    argsFromElims = (Elim' t -> Maybe (Arg t)) -> [Elim' t] -> [Arg t]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Elim' t -> Maybe (Arg t)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim

    -- | Drop 'Proj' constructors. (Safe)
    allProjElims :: [Elim' t] -> Maybe [(ProjOrigin, QName)]
    allProjElims :: forall t. [Elim' t] -> Maybe [(ProjOrigin, QName)]
    allProjElims = (Elim' t -> Maybe (ProjOrigin, QName))
    -> [Elim' t] -> Maybe [(ProjOrigin, QName)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Elim' t -> Maybe (ProjOrigin, QName)
    forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
    isProjElim

    instance KillRange a => KillRange (Elim' a) where
      killRange :: KillRangeT (Elim' a)
    killRange = (a -> a) -> KillRangeT (Elim' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> a
    forall a. KillRange a => KillRangeT a
    killRange

    instance Pretty tm => Pretty (Elim' tm) where
      prettyPrec :: Int -> Elim' tm -> Doc
    prettyPrec Int
    p (Apply Arg tm
    v)    = Int -> Arg tm -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    p Arg tm
    v
      prettyPrec Int
    _ (Proj ProjOrigin
    _o QName
    x)  = String -> Doc
    text (String
    "." String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    x)
      prettyPrec Int
    p (IApply tm
    x tm
    y tm
    r) = Int -> tm -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    p tm
    r
    --  prettyPrec p (IApply x y r) = text "@[" <> prettyPrec 0 x <> text ", " <> prettyPrec 0 y <> text "]" <> prettyPrec p r

    instance NFData a => NFData (Elim' a) where
      rnf :: Elim' a -> ()
    rnf (Apply Arg a
    x) = Arg a -> ()
    forall a. NFData a => a -> ()
    rnf Arg a
    x
      rnf Proj{}    = ()
      rnf (IApply a
    x a
    y a
    r) = a -> ()
    forall a. NFData a => a -> ()
    rnf a
    x () -> () -> ()
    `seq` a -> ()
    forall a. NFData a => a -> ()
    rnf a
    y () -> () -> ()
    `seq` a -> ()
    forall a. NFData a => a -> ()
    rnf a
    r