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