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