    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.Syntax.Internal.Elim where

    import Control.DeepSeq

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import Agda.Syntax.Abstract.Name

    import Agda.Syntax.Common.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 (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
    $cshowsPrec :: forall a. Show a => Int -> Elim' a -> ShowS
    showsPrec :: Int -> Elim' a -> ShowS
    $cshow :: forall a. Show a => Elim' a -> String
    show :: Elim' a -> String
    $cshowList :: forall a. Show a => [Elim' a] -> ShowS
    showList :: [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
    $cfmap :: forall a b. (a -> b) -> Elim' a -> Elim' b
    fmap :: forall a b. (a -> b) -> Elim' a -> Elim' b
    $c<$ :: forall a b. a -> Elim' b -> Elim' a
    <$ :: forall a b. a -> Elim' b -> Elim' a
    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
    $cfold :: forall m. Monoid m => Elim' m -> m
    fold :: forall m. Monoid m => Elim' m -> 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
    foldMap' :: forall m a. Monoid m => (a -> m) -> Elim' a -> m
    $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
    foldr' :: forall a b. (a -> b -> 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
    foldl' :: forall b a. (b -> a -> b) -> b -> Elim' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Elim' a -> a
    foldr1 :: forall a. (a -> a -> a) -> Elim' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Elim' a -> a
    foldl1 :: forall a. (a -> a -> a) -> Elim' a -> a
    $ctoList :: forall a. Elim' a -> [a]
    toList :: forall a. Elim' a -> [a]
    $cnull :: forall a. Elim' a -> Bool
    null :: forall a. Elim' a -> Bool
    $clength :: forall a. Elim' a -> Int
    length :: forall a. Elim' a -> Int
    $celem :: forall a. Eq a => a -> Elim' a -> Bool
    elem :: forall a. Eq a => a -> Elim' a -> Bool
    $cmaximum :: forall a. Ord a => Elim' a -> a
    maximum :: forall a. Ord a => Elim' a -> a
    $cminimum :: forall a. Ord a => Elim' a -> a
    minimum :: forall a. Ord a => Elim' a -> a
    $csum :: forall a. Num a => Elim' a -> a
    sum :: forall a. Num a => Elim' a -> a
    $cproduct :: forall a. Num a => Elim' a -> a
    product :: forall a. Num a => Elim' a -> a
    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)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Elim' a -> f (Elim' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Elim' a -> f (Elim' b)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => Elim' (f a) -> f (Elim' a)
    sequenceA :: forall (f :: * -> *) a. Applicative f => Elim' (f a) -> f (Elim' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Elim' a -> m (Elim' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Elim' a -> m (Elim' b)
    $csequence :: forall (m :: * -> *) a. Monad m => Elim' (m a) -> m (Elim' a)
    sequence :: forall (m :: * -> *) a. Monad m => Elim' (m a) -> m (Elim' a)
    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

    -- | Only 'Apply' variant.
    isProperApplyElim :: Elim' a -> Bool
    isProperApplyElim :: forall a. Elim' a -> Bool
    isProperApplyElim = \case
      Apply Arg a
    _  -> Bool
    True
      IApply{} -> Bool
    False
      Proj{}   -> Bool
    False

    -- | 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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a b. (a -> b) -> Elim' a -> Elim' b
    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
    forall a. String -> Doc a
    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 () -> () -> ()
    forall a b. a -> b -> b
    `seq` a -> ()
    forall a. NFData a => a -> ()
    rnf a
    y () -> () -> ()
    forall a b. a -> b -> b
    `seq` a -> ()
    forall a. NFData a => a -> ()
    rnf a
    r