1 2module Agda.Syntax.Internal.Elim where 3 4import Control.DeepSeq 5import Data.Data (Data) 6 7import Agda.Syntax.Common 8import Agda.Syntax.Concrete.Pretty () -- Pretty Arg instance 9import Agda.Syntax.Position 10import Agda.Syntax.Abstract.Name 11 12import Agda.Utils.Pretty 13import Agda.Utils.Empty 14import Agda.Utils.Maybe 15import Agda.Utils.Tuple 16 17-- | Eliminations, subsuming applications and projections. 18-- 19data Elim' a 20 = Apply (Arg a) -- ^ Application. 21 | Proj ProjOrigin QName -- ^ Projection. 'QName' is name of a record projection. 22 | IApply a a a -- ^ IApply x y r, x and y are the endpoints 23 deriving (Data, Show, Functor, Foldable, Traversable) 24 25-- | This instance cheats on 'Proj', use with care. 26-- 'Proj's are always assumed to be 'UserWritten', since they have no 'ArgInfo'. 27-- Same for IApply 28instance LensOrigin (Elim' a) where 29 getOrigin (Apply a) = getOrigin a 30 getOrigin Proj{} = UserWritten 31 getOrigin IApply{} = UserWritten 32 mapOrigin f (Apply a) = Apply $ mapOrigin f a 33 mapOrigin f e@Proj{} = e 34 mapOrigin f e@IApply{} = e 35 36-- | Drop 'Apply' constructor. (Safe) 37isApplyElim :: Elim' a -> Maybe (Arg a) 38isApplyElim (Apply u) = Just u 39isApplyElim Proj{} = Nothing 40isApplyElim (IApply _ _ r) = Just (defaultArg r) 41 42isApplyElim' :: Empty -> Elim' a -> Arg a 43isApplyElim' e = fromMaybe (absurd e) . isApplyElim 44 45-- | Drop 'Apply' constructors. (Safe) 46allApplyElims :: [Elim' a] -> Maybe [Arg a] 47allApplyElims = mapM isApplyElim 48 49-- | Split at first non-'Apply' 50splitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a]) 51splitApplyElims (Apply u : es) = mapFst (u :) $ splitApplyElims es 52splitApplyElims es = ([], es) 53 54class IsProjElim e where 55 isProjElim :: e -> Maybe (ProjOrigin, QName) 56 57instance IsProjElim (Elim' a) where 58 isProjElim (Proj o d) = Just (o, d) 59 isProjElim Apply{} = Nothing 60 isProjElim IApply{} = Nothing 61 62-- | Discards @Proj f@ entries. 63argsFromElims :: [Elim' t] -> [Arg t] 64argsFromElims = mapMaybe isApplyElim 65 66-- | Drop 'Proj' constructors. (Safe) 67allProjElims :: [Elim' t] -> Maybe [(ProjOrigin, QName)] 68allProjElims = mapM isProjElim 69 70instance KillRange a => KillRange (Elim' a) where 71 killRange = fmap killRange 72 73instance Pretty tm => Pretty (Elim' tm) where 74 prettyPrec p (Apply v) = prettyPrec p v 75 prettyPrec _ (Proj _o x) = text ("." ++ prettyShow x) 76 prettyPrec p (IApply x y r) = prettyPrec p r 77-- prettyPrec p (IApply x y r) = text "@[" <> prettyPrec 0 x <> text ", " <> prettyPrec 0 y <> text "]" <> prettyPrec p r 78 79instance NFData a => NFData (Elim' a) where 80 rnf (Apply x) = rnf x 81 rnf Proj{} = () 82 rnf (IApply x y r) = rnf x `seq` rnf y `seq` rnf r 83 84