{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
module Agda.Syntax.Concrete.Pattern where
import Control.Applicative ( liftA2 )
import Control.Monad.Identity
import Data.Foldable (Foldable, foldMap)
import Data.Traversable (Traversable, traverse)
import Data.Monoid
import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Utils.AffineHole
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
class IsEllipsis a where
isEllipsis :: a -> Bool
instance IsEllipsis Pattern where
isEllipsis = \case
EllipsisP{} -> True
RawAppP _ [p] -> isEllipsis p
ParenP _ p -> isEllipsis p
_ -> False
class HasEllipsis a where
hasEllipsis :: a -> Bool
instance HasEllipsis Pattern where
hasEllipsis p =
case hasEllipsis' p of
ZeroHoles _ -> False
OneHole _ -> True
ManyHoles -> True
instance HasEllipsis LHS where
hasEllipsis (LHS p _ _) = hasEllipsis p
class IsWithP p where
isWithP :: p -> Maybe p
default isWithP :: (IsWithP q, Decoration f, f q ~ p) => p -> Maybe p
isWithP = traverseF isWithP
instance IsWithP Pattern where
isWithP = \case
WithP _ p -> Just p
RawAppP _ [p] -> isWithP p
ParenP _ p -> isWithP p
_ -> Nothing
instance IsWithP p => IsWithP (Arg p) where
instance IsWithP p => IsWithP (Named n p) where
data LHSPatternView
= LHSAppP [NamedArg Pattern]
| LHSWithP [Pattern]
lhsPatternView :: [NamedArg Pattern] -> Maybe (LHSPatternView, [NamedArg Pattern])
lhsPatternView [] = Nothing
lhsPatternView (p0 : ps) =
case namedArg p0 of
WithP _i p -> Just (LHSWithP (p : map namedArg ps1), ps2)
where
(ps1, ps2) = spanJust isWithP ps
_ -> Just (LHSAppP (p0 : ps1), ps2)
where
(ps1, ps2) = span (isNothing . isWithP) ps
lhsCoreApp :: LHSCore -> [NamedArg Pattern] -> LHSCore
lhsCoreApp core ps = core { lhsPats = lhsPats core ++ ps }
lhsCoreWith :: LHSCore -> [Pattern] -> LHSCore
lhsCoreWith (LHSWith core wps []) wps' = LHSWith core (wps ++ wps') []
lhsCoreWith core wps' = LHSWith core wps' []
lhsCoreAddSpine :: LHSCore -> [NamedArg Pattern] -> LHSCore
lhsCoreAddSpine core ps0 =
case lhsPatternView ps0 of
Nothing -> core
Just (LHSAppP ps , ps') -> lhsCoreApp core ps `lhsCoreAddSpine` ps'
Just (LHSWithP wps, ps') -> lhsCoreWith core wps `lhsCoreAddSpine` ps'
mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS
mapLhsOriginalPattern f lhs@LHS{ lhsOriginalPattern = p } =
lhs { lhsOriginalPattern = f p }
mapLhsOriginalPatternM :: (Functor m, Applicative m) => (Pattern -> m Pattern) -> LHS -> m LHS
mapLhsOriginalPatternM f lhs@LHS{ lhsOriginalPattern = p } = f p <&> \ p' ->
lhs { lhsOriginalPattern = p' }
hasCopatterns :: LHSCore -> Bool
hasCopatterns = \case
LHSHead{} -> False
LHSProj{} -> True
LHSWith h _ _ -> hasCopatterns h
class CPatternLike p where
foldrCPattern
:: Monoid m
=> (Pattern -> m -> m)
-> p -> m
default foldrCPattern
:: (Monoid m, Foldable f, CPatternLike q, f q ~ p)
=> (Pattern -> m -> m) -> p -> m
foldrCPattern = foldMap . foldrCPattern
traverseCPatternA :: (Applicative m, Functor m)
=> (Pattern -> m Pattern -> m Pattern)
-> p -> m p
default traverseCPatternA :: (Traversable f, CPatternLike q, f q ~ p, Applicative m, Functor m)
=> (Pattern -> m Pattern -> m Pattern)
-> p -> m p
traverseCPatternA = traverse . traverseCPatternA
traverseCPatternM
:: Monad m => (Pattern -> m Pattern)
-> (Pattern -> m Pattern)
-> p -> m p
default traverseCPatternM
:: (Traversable f, CPatternLike q, f q ~ p, Monad m)
=> (Pattern -> m Pattern)
-> (Pattern -> m Pattern)
-> p -> m p
traverseCPatternM pre post = traverse $ traverseCPatternM pre post
instance CPatternLike Pattern where
foldrCPattern f p0 = f p0 $
case p0 of
AppP p ps -> foldrCPattern f (p, ps)
RawAppP _ ps -> foldrCPattern f ps
OpAppP _ _ _ ps -> foldrCPattern f ps
HiddenP _ ps -> foldrCPattern f ps
InstanceP _ ps -> foldrCPattern f ps
ParenP _ p -> foldrCPattern f p
AsP _ _ p -> foldrCPattern f p
WithP _ p -> foldrCPattern f p
RecP _ ps -> foldrCPattern f ps
IdentP _ -> mempty
WildP _ -> mempty
DotP _ _ -> mempty
AbsurdP _ -> mempty
LitP _ -> mempty
QuoteP _ -> mempty
EllipsisP _ -> mempty
traverseCPatternA f p0 = f p0 $ case p0 of
AppP p ps -> liftA2 AppP (traverseCPatternA f p) (traverseCPatternA f ps)
RawAppP r ps -> RawAppP r <$> traverseCPatternA f ps
OpAppP r x xs ps -> OpAppP r x xs <$> traverseCPatternA f ps
HiddenP r p -> HiddenP r <$> traverseCPatternA f p
InstanceP r p -> InstanceP r <$> traverseCPatternA f p
ParenP r p -> ParenP r <$> traverseCPatternA f p
AsP r x p -> AsP r x <$> traverseCPatternA f p
WithP r p -> WithP r <$> traverseCPatternA f p
RecP r ps -> RecP r <$> traverseCPatternA f ps
IdentP _ -> pure p0
WildP _ -> pure p0
DotP _ _ -> pure p0
AbsurdP _ -> pure p0
LitP _ -> pure p0
QuoteP _ -> pure p0
EllipsisP _ -> pure p0
traverseCPatternM pre post = pre >=> recurse >=> post
where
recurse p0 = case p0 of
AppP p ps -> uncurry AppP <$> traverseCPatternM pre post (p, ps)
RawAppP r ps -> RawAppP r <$> traverseCPatternM pre post ps
OpAppP r x xs ps -> OpAppP r x xs <$> traverseCPatternM pre post ps
HiddenP r p -> HiddenP r <$> traverseCPatternM pre post p
InstanceP r p -> InstanceP r <$> traverseCPatternM pre post p
ParenP r p -> ParenP r <$> traverseCPatternM pre post p
AsP r x p -> AsP r x <$> traverseCPatternM pre post p
WithP r p -> WithP r <$> traverseCPatternM pre post p
RecP r ps -> RecP r <$> traverseCPatternM pre post ps
IdentP _ -> return p0
WildP _ -> return p0
DotP _ _ -> return p0
AbsurdP _ -> return p0
LitP _ -> return p0
QuoteP _ -> return p0
EllipsisP _ -> return p0
instance (CPatternLike a, CPatternLike b) => CPatternLike (a,b) where
foldrCPattern f (p, p') =
foldrCPattern f p `mappend` foldrCPattern f p'
traverseCPatternA f (p, p') =
liftA2 (,)
(traverseCPatternA f p)
(traverseCPatternA f p')
traverseCPatternM pre post (p, p') =
liftA2 (,)
(traverseCPatternM pre post p)
(traverseCPatternM pre post p')
instance CPatternLike p => CPatternLike (Arg p) where
instance CPatternLike p => CPatternLike (Named n p) where
instance CPatternLike p => CPatternLike [p] where
instance CPatternLike p => CPatternLike (Maybe p) where
instance CPatternLike p => CPatternLike (FieldAssignment' p) where
foldCPattern :: (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
foldCPattern f = foldrCPattern $ \ p m -> f p `mappend` m
preTraverseCPatternM
:: (CPatternLike p, Monad m)
=> (Pattern -> m Pattern)
-> p -> m p
preTraverseCPatternM pre p = traverseCPatternM pre return p
postTraverseCPatternM
:: (CPatternLike p, Monad m)
=> (Pattern -> m Pattern)
-> p -> m p
postTraverseCPatternM post p = traverseCPatternM return post p
mapCPattern :: CPatternLike p => (Pattern -> Pattern) -> p -> p
mapCPattern f = runIdentity . postTraverseCPatternM (Identity . f)
patternQNames :: CPatternLike p => p -> [QName]
patternQNames p = foldCPattern f p `appEndo` []
where
f :: Pattern -> Endo [QName]
f = \case
IdentP x -> Endo (x :)
OpAppP _ x _ _ -> Endo (x :)
AsP _ x _ -> mempty
AppP _ _ -> mempty
WithP _ _ -> mempty
RawAppP _ _ -> mempty
HiddenP _ _ -> mempty
ParenP _ _ -> mempty
WildP _ -> mempty
AbsurdP _ -> mempty
DotP _ _ -> mempty
LitP _ -> mempty
QuoteP _ -> mempty
InstanceP _ _ -> mempty
RecP _ _ -> mempty
EllipsisP _ -> mempty
patternNames :: Pattern -> [Name]
patternNames = map unqualify . patternQNames
hasWithPatterns :: CPatternLike p => p -> Bool
hasWithPatterns = getAny . foldCPattern (Any . isWithPattern)
isWithPattern :: Pattern -> Bool
isWithPattern = \case
WithP{} -> True
_ -> False
numberOfWithPatterns :: CPatternLike p => p -> Int
numberOfWithPatterns = getSum . foldCPattern (Sum . f)
where f p = if isWithPattern p then 1 else 0
hasEllipsis' :: CPatternLike p => p -> AffineHole Pattern p
hasEllipsis' = traverseCPatternA $ \ p mp ->
case p of
EllipsisP _ -> OneHole id
_ -> mp