{-# LANGUAGE TypeFamilies #-}
module Agda.Syntax.Concrete.Pattern where
import Control.Applicative ( liftA2 )
import Control.Arrow ( first )
import Control.Monad.Identity
import Control.Monad.Writer
import Data.Foldable (Foldable, foldMap)
import Data.Traversable (Traversable, traverse)
import Data.Monoid
import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Syntax.Position
import Agda.Utils.AffineHole
import Agda.Utils.Functor
import Agda.Utils.Impossible
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
EqualP _ _ -> 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
EqualP _ _ -> 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
EqualP _ _ -> 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
EqualP _ _ -> 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 p
_ -> mp
reintroduceEllipsis :: ExpandedEllipsis -> Pattern -> Pattern
reintroduceEllipsis NoEllipsis p = p
reintroduceEllipsis (ExpandedEllipsis r k) p =
let core = EllipsisP r
wargs = snd $ splitEllipsis k $ patternAppView p
in foldl AppP core wargs
splitEllipsis :: (IsWithP p) => Int -> [p] -> ([p],[p])
splitEllipsis k [] = ([] , [])
splitEllipsis k (p:ps)
| isJust (isWithP p) = if
| k == 0 -> ([] , p:ps)
| otherwise -> first (p:) $ splitEllipsis (k-1) ps
| otherwise = first (p:) $ splitEllipsis k ps
patternAppView :: Pattern -> [NamedArg Pattern]
patternAppView p = case p of
AppP p arg -> patternAppView p ++ [arg]
OpAppP _ x _ ps -> defaultNamedArg (IdentP x) : ps
ParenP _ p -> patternAppView p
RawAppP _ _ -> __IMPOSSIBLE__
_ -> [ defaultNamedArg p ]