-- | Tools for patterns in concrete syntax.

module Agda.Syntax.Concrete.Pattern where

import Control.Applicative ( liftA2 )
import Control.Arrow ( first )
import Control.Monad ( (>=>) )
import Control.Monad.Identity

import Data.Monoid ( Any(..), Endo(..), Sum(..) )

import Agda.Syntax.Common
import Agda.Syntax.Concrete

import Agda.Utils.AffineHole
import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.List
import Agda.Utils.List1  ( List1, pattern (:|) )
import Agda.Utils.List2  ( List2 )
import Agda.Utils.Maybe
import Agda.Utils.Singleton
import qualified Agda.Utils.List1 as List1


-- | Check for ellipsis @...@.

class IsEllipsis a where
  isEllipsis :: a -> Bool

-- | Is the pattern just @...@?
instance IsEllipsis Pattern where
  isEllipsis :: Pattern -> Bool
isEllipsis = \case
    EllipsisP{}         -> Bool
True
    ParenP Range
_ Pattern
p          -> forall a. IsEllipsis a => a -> Bool
isEllipsis Pattern
p
    Pattern
_ -> Bool
False

-- | Has the lhs an occurrence of the ellipsis @...@?

class HasEllipsis a where
  hasEllipsis :: a -> Bool

instance HasEllipsis Pattern where
  hasEllipsis :: Pattern -> Bool
hasEllipsis Pattern
p =
    case forall p. CPatternLike p => p -> AffineHole Pattern p
hasEllipsis' Pattern
p of
      ZeroHoles Pattern
_ -> Bool
False
      OneHole Pattern -> Pattern
_ Pattern
_ -> Bool
True
      AffineHole Pattern Pattern
ManyHoles   -> Bool
True

-- | Does the lhs contain an ellipsis?
instance HasEllipsis LHS where
  hasEllipsis :: LHS -> Bool
hasEllipsis (LHS Pattern
p [RewriteEqn]
_ [WithExpr]
_) = forall a. HasEllipsis a => a -> Bool
hasEllipsis Pattern
p
  -- clauses that are already expanded don't have an ellipsis

-- | Check for with-pattern @| p@.

class IsWithP p where
  isWithP :: p -> Maybe p

  default isWithP :: (IsWithP q, Decoration f, f q ~ p) => p -> Maybe p
  isWithP = forall (t :: * -> *) (m :: * -> *) a b.
(Decoration t, Functor m) =>
(a -> m b) -> t a -> m (t b)
traverseF forall p. IsWithP p => p -> Maybe p
isWithP

instance IsWithP Pattern where
  isWithP :: Pattern -> Maybe Pattern
isWithP = \case
    WithP Range
_ Pattern
p           -> forall a. a -> Maybe a
Just Pattern
p
    ParenP Range
_ Pattern
p          -> forall p. IsWithP p => p -> Maybe p
isWithP Pattern
p
    Pattern
_ -> forall a. Maybe a
Nothing

instance IsWithP p => IsWithP (Arg p) where
instance IsWithP p => IsWithP (Named n p) where


-- * LHS manipulation (see also ''Agda.Syntax.Abstract.Pattern'')

-- | The next patterns are ...
--
-- (This view discards 'PatInfo'.)
data LHSPatternView
  = LHSAppP  [NamedArg Pattern]
      -- ^ Application patterns (non-empty list).
  | LHSWithP [Pattern]
      -- ^ With patterns (non-empty list).
      --   These patterns are not prefixed with 'WithP'.

-- | Construct the 'LHSPatternView' of the given list (if not empty).
--
-- Return the view and the remaining patterns.

lhsPatternView :: [NamedArg Pattern] -> Maybe (LHSPatternView, [NamedArg Pattern])
lhsPatternView :: [NamedArg Pattern] -> Maybe (LHSPatternView, [NamedArg Pattern])
lhsPatternView [] = forall a. Maybe a
Nothing
lhsPatternView (NamedArg Pattern
p0 : [NamedArg Pattern]
ps) =
  case forall a. NamedArg a -> a
namedArg NamedArg Pattern
p0 of
    WithP Range
_i Pattern
p   -> forall a. a -> Maybe a
Just ([Pattern] -> LHSPatternView
LHSWithP (Pattern
p forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg [NamedArg Pattern]
ps1), [NamedArg Pattern]
ps2)
      where
      ([NamedArg Pattern]
ps1, [NamedArg Pattern]
ps2) = forall a b. (a -> Maybe b) -> [a] -> (Prefix b, [a])
spanJust forall p. IsWithP p => p -> Maybe p
isWithP [NamedArg Pattern]
ps
    -- If the next pattern is an application pattern, collect more of these
    Pattern
_ -> forall a. a -> Maybe a
Just ([NamedArg Pattern] -> LHSPatternView
LHSAppP (NamedArg Pattern
p0 forall a. a -> [a] -> [a]
: [NamedArg Pattern]
ps1), [NamedArg Pattern]
ps2)
      where
      ([NamedArg Pattern]
ps1, [NamedArg Pattern]
ps2) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. IsWithP p => p -> Maybe p
isWithP) [NamedArg Pattern]
ps

-- | Add applicative patterns (non-projection / non-with patterns) to the right.
lhsCoreApp :: LHSCore -> [NamedArg Pattern] -> LHSCore
lhsCoreApp :: LHSCore -> [NamedArg Pattern] -> LHSCore
lhsCoreApp (LHSEllipsis Range
r LHSCore
core) [NamedArg Pattern]
ps = Range -> LHSCore -> LHSCore
LHSEllipsis Range
r forall a b. (a -> b) -> a -> b
$ LHSCore -> [NamedArg Pattern] -> LHSCore
lhsCoreApp LHSCore
core [NamedArg Pattern]
ps
lhsCoreApp LHSCore
core [NamedArg Pattern]
ps = LHSCore
core { lhsPats :: [NamedArg Pattern]
lhsPats = LHSCore -> [NamedArg Pattern]
lhsPats LHSCore
core forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps }

-- | Add with-patterns to the right.
lhsCoreWith :: LHSCore -> [Pattern] -> LHSCore
lhsCoreWith :: LHSCore -> [Pattern] -> LHSCore
lhsCoreWith (LHSWith LHSCore
core [Pattern]
wps []) [Pattern]
wps' = LHSCore -> [Pattern] -> [NamedArg Pattern] -> LHSCore
LHSWith LHSCore
core ([Pattern]
wps forall a. [a] -> [a] -> [a]
++ [Pattern]
wps') []
lhsCoreWith LHSCore
core                  [Pattern]
wps' = LHSCore -> [Pattern] -> [NamedArg Pattern] -> LHSCore
LHSWith LHSCore
core [Pattern]
wps' []

-- | Append patterns to 'LHSCore', separating with patterns from the rest.
lhsCoreAddSpine :: LHSCore -> [NamedArg Pattern] -> LHSCore
lhsCoreAddSpine :: LHSCore -> [NamedArg Pattern] -> LHSCore
lhsCoreAddSpine LHSCore
core [NamedArg Pattern]
ps0 =
  -- Recurse on lhsPatternView until no patterns left.
  case [NamedArg Pattern] -> Maybe (LHSPatternView, [NamedArg Pattern])
lhsPatternView [NamedArg Pattern]
ps0 of
    Maybe (LHSPatternView, [NamedArg Pattern])
Nothing       -> LHSCore
core
    Just (LHSAppP  [NamedArg Pattern]
ps , [NamedArg Pattern]
ps') -> LHSCore -> [NamedArg Pattern] -> LHSCore
lhsCoreApp  LHSCore
core [NamedArg Pattern]
ps  LHSCore -> [NamedArg Pattern] -> LHSCore
`lhsCoreAddSpine` [NamedArg Pattern]
ps'
    Just (LHSWithP [Pattern]
wps, [NamedArg Pattern]
ps') -> LHSCore -> [Pattern] -> LHSCore
lhsCoreWith LHSCore
core [Pattern]
wps LHSCore -> [NamedArg Pattern] -> LHSCore
`lhsCoreAddSpine` [NamedArg Pattern]
ps'


-- | Modify the 'Pattern' component in 'LHS'.
mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS
mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS
mapLhsOriginalPattern Pattern -> Pattern
f lhs :: LHS
lhs@LHS{ lhsOriginalPattern :: LHS -> Pattern
lhsOriginalPattern = Pattern
p } =
  LHS
lhs { lhsOriginalPattern :: Pattern
lhsOriginalPattern = Pattern -> Pattern
f Pattern
p }

-- | Effectfully modify the 'Pattern' component in 'LHS'.
mapLhsOriginalPatternM :: (Functor m, Applicative m) => (Pattern -> m Pattern) -> LHS -> m LHS
mapLhsOriginalPatternM :: forall (m :: * -> *).
(Functor m, Applicative m) =>
(Pattern -> m Pattern) -> LHS -> m LHS
mapLhsOriginalPatternM Pattern -> m Pattern
f lhs :: LHS
lhs@LHS{ lhsOriginalPattern :: LHS -> Pattern
lhsOriginalPattern = Pattern
p } = Pattern -> m Pattern
f Pattern
p forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Pattern
p' ->
  LHS
lhs { lhsOriginalPattern :: Pattern
lhsOriginalPattern = Pattern
p' }

-- | Does the LHS contain projection patterns?
hasCopatterns :: LHSCore -> Bool
hasCopatterns :: LHSCore -> Bool
hasCopatterns = \case
  LHSHead{}     -> Bool
False
  LHSProj{}     -> Bool
True
  LHSWith LHSCore
h [Pattern]
_ [NamedArg Pattern]
_ -> LHSCore -> Bool
hasCopatterns LHSCore
h
  LHSEllipsis{} -> Bool
False

-- * Generic fold

-- | Generic pattern traversal.
--
-- See 'Agda.Syntax.Abstract.Pattern.APatternLike'.

class CPatternLike p where

  -- | Fold pattern.
  foldrCPattern
    :: Monoid m
    => (Pattern -> m -> m)
         -- ^ Combine a pattern and the value computed from its subpatterns.
    -> p -> m

  default foldrCPattern
    :: (Monoid m, Foldable f, CPatternLike q, f q ~ p)
    => (Pattern -> m -> m) -> p -> m
  foldrCPattern = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern

  -- | Traverse pattern with option of post-traversal modification.
  traverseCPatternA :: (Applicative m, Functor m)
      => (Pattern -> m Pattern -> m Pattern)
         -- ^ Combine a pattern and the its recursively computed version.
      -> 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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA

  -- | Traverse pattern.
  traverseCPatternM
    :: Monad m => (Pattern -> m Pattern)  -- ^ @pre@: Modification before recursion.
    -> (Pattern -> m Pattern)  -- ^ @post@: Modification after recursion.
    -> p -> m p

  default traverseCPatternM
    :: (Traversable f, CPatternLike q, f q ~ p, Monad m)
    => (Pattern -> m Pattern)
    -> (Pattern -> m Pattern)
    -> p -> m p
  traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b. (a -> b) -> a -> b
$ forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post

instance CPatternLike Pattern where
  foldrCPattern :: forall m. Monoid m => (Pattern -> m -> m) -> Pattern -> m
foldrCPattern Pattern -> m -> m
f Pattern
p0 = Pattern -> m -> m
f Pattern
p0 forall a b. (a -> b) -> a -> b
$
    case Pattern
p0 of
      -- Recursive cases:
      AppP Pattern
p NamedArg Pattern
ps       -> forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern Pattern -> m -> m
f (Pattern
p, NamedArg Pattern
ps)
      RawAppP Range
_ List2 Pattern
ps    -> forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern Pattern -> m -> m
f List2 Pattern
ps
      OpAppP Range
_ QName
_ Set Name
_ [NamedArg Pattern]
ps -> forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern Pattern -> m -> m
f [NamedArg Pattern]
ps
      HiddenP Range
_ Named NamedName Pattern
ps    -> forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern Pattern -> m -> m
f Named NamedName Pattern
ps
      InstanceP Range
_ Named NamedName Pattern
ps  -> forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern Pattern -> m -> m
f Named NamedName Pattern
ps
      ParenP Range
_ Pattern
p      -> forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern Pattern -> m -> m
f Pattern
p
      AsP Range
_ Name
_ Pattern
p       -> forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern Pattern -> m -> m
f Pattern
p
      WithP Range
_ Pattern
p       -> forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern Pattern -> m -> m
f Pattern
p
      RecP Range
_ [FieldAssignment' Pattern]
ps       -> forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern Pattern -> m -> m
f [FieldAssignment' Pattern]
ps
      EllipsisP Range
_ Maybe Pattern
mp  -> forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern Pattern -> m -> m
f Maybe Pattern
mp
      -- Nonrecursive cases:
      IdentP QName
_        -> forall a. Monoid a => a
mempty
      WildP Range
_         -> forall a. Monoid a => a
mempty
      DotP Range
_ Expr
_        -> forall a. Monoid a => a
mempty
      AbsurdP Range
_       -> forall a. Monoid a => a
mempty
      LitP Range
_ Literal
_        -> forall a. Monoid a => a
mempty
      QuoteP Range
_        -> forall a. Monoid a => a
mempty
      EqualP Range
_ [(Expr, Expr)]
_      -> forall a. Monoid a => a
mempty

  traverseCPatternA :: forall (m :: * -> *).
(Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern
traverseCPatternA Pattern -> m Pattern -> m Pattern
f Pattern
p0 = Pattern -> m Pattern -> m Pattern
f Pattern
p0 forall a b. (a -> b) -> a -> b
$ case Pattern
p0 of
      -- Recursive cases:
      AppP        Pattern
p NamedArg Pattern
ps    -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Pattern -> NamedArg Pattern -> Pattern
AppP (forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f Pattern
p) (forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f NamedArg Pattern
ps)
      RawAppP   Range
r List2 Pattern
ps      -> Range -> List2 Pattern -> Pattern
RawAppP Range
r     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f List2 Pattern
ps
      OpAppP    Range
r QName
x Set Name
xs [NamedArg Pattern]
ps -> Range -> QName -> Set Name -> [NamedArg Pattern] -> Pattern
OpAppP Range
r QName
x Set Name
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f [NamedArg Pattern]
ps
      HiddenP   Range
r Named NamedName Pattern
p       -> Range -> Named NamedName Pattern -> Pattern
HiddenP Range
r     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f Named NamedName Pattern
p
      InstanceP Range
r Named NamedName Pattern
p       -> Range -> Named NamedName Pattern -> Pattern
InstanceP Range
r   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f Named NamedName Pattern
p
      ParenP    Range
r Pattern
p       -> Range -> Pattern -> Pattern
ParenP Range
r      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f Pattern
p
      AsP       Range
r Name
x Pattern
p     -> Range -> Name -> Pattern -> Pattern
AsP Range
r Name
x       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f Pattern
p
      WithP     Range
r Pattern
p       -> Range -> Pattern -> Pattern
WithP Range
r       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f Pattern
p
      RecP      Range
r [FieldAssignment' Pattern]
ps      -> Range -> [FieldAssignment' Pattern] -> Pattern
RecP Range
r        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f [FieldAssignment' Pattern]
ps
      EllipsisP Range
r Maybe Pattern
mp      -> Range -> Maybe Pattern -> Pattern
EllipsisP Range
r   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f Maybe Pattern
mp
      -- Nonrecursive cases:
      IdentP QName
_        -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pattern
p0
      WildP Range
_         -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pattern
p0
      DotP Range
_ Expr
_        -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pattern
p0
      AbsurdP Range
_       -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pattern
p0
      LitP Range
_ Literal
_        -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pattern
p0
      QuoteP Range
_        -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pattern
p0
      EqualP Range
_ [(Expr, Expr)]
_      -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pattern
p0

  traverseCPatternM :: forall (m :: * -> *).
Monad m =>
(Pattern -> m Pattern)
-> (Pattern -> m Pattern) -> Pattern -> m Pattern
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post = Pattern -> m Pattern
pre forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Pattern -> m Pattern
recurse forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Pattern -> m Pattern
post
    where
    recurse :: Pattern -> m Pattern
recurse Pattern
p0 = case Pattern
p0 of
      -- Recursive cases:
      AppP        Pattern
p NamedArg Pattern
ps    -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Pattern -> NamedArg Pattern -> Pattern
AppP  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post (Pattern
p, NamedArg Pattern
ps)
      RawAppP   Range
r List2 Pattern
ps      -> Range -> List2 Pattern -> Pattern
RawAppP Range
r     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post List2 Pattern
ps
      OpAppP    Range
r QName
x Set Name
xs [NamedArg Pattern]
ps -> Range -> QName -> Set Name -> [NamedArg Pattern] -> Pattern
OpAppP Range
r QName
x Set Name
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post [NamedArg Pattern]
ps
      HiddenP   Range
r Named NamedName Pattern
p       -> Range -> Named NamedName Pattern -> Pattern
HiddenP Range
r     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post Named NamedName Pattern
p
      InstanceP Range
r Named NamedName Pattern
p       -> Range -> Named NamedName Pattern -> Pattern
InstanceP Range
r   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post Named NamedName Pattern
p
      ParenP    Range
r Pattern
p       -> Range -> Pattern -> Pattern
ParenP Range
r      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post Pattern
p
      AsP       Range
r Name
x Pattern
p     -> Range -> Name -> Pattern -> Pattern
AsP Range
r Name
x       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post Pattern
p
      WithP     Range
r Pattern
p       -> Range -> Pattern -> Pattern
WithP Range
r       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post Pattern
p
      RecP      Range
r [FieldAssignment' Pattern]
ps      -> Range -> [FieldAssignment' Pattern] -> Pattern
RecP Range
r        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post [FieldAssignment' Pattern]
ps
      EllipsisP Range
r Maybe Pattern
mp      -> Range -> Maybe Pattern -> Pattern
EllipsisP Range
r   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post Maybe Pattern
mp
      -- Nonrecursive cases:
      IdentP QName
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p0
      WildP Range
_         -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p0
      DotP Range
_ Expr
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p0
      AbsurdP Range
_       -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p0
      LitP Range
_ Literal
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p0
      QuoteP Range
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p0
      EqualP Range
_ [(Expr, Expr)]
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p0

instance (CPatternLike a, CPatternLike b) => CPatternLike (a,b) where
  foldrCPattern :: forall m. Monoid m => (Pattern -> m -> m) -> (a, b) -> m
foldrCPattern Pattern -> m -> m
f (a
p, b
p') =
    forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern Pattern -> m -> m
f a
p forall a. Monoid a => a -> a -> a
`mappend` forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern Pattern -> m -> m
f b
p'

  traverseCPatternA :: forall (m :: * -> *).
(Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> (a, b) -> m (a, b)
traverseCPatternA Pattern -> m Pattern -> m Pattern
f (a
p, b
p') =
    forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,)
      (forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f a
p)
      (forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA Pattern -> m Pattern -> m Pattern
f b
p')

  traverseCPatternM :: forall (m :: * -> *).
Monad m =>
(Pattern -> m Pattern)
-> (Pattern -> m Pattern) -> (a, b) -> m (a, b)
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post (a
p, b
p') =
    forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,)
      (forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post a
p)
      (forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre Pattern -> m Pattern
post b
p')

instance CPatternLike p => CPatternLike (Arg p)
instance CPatternLike p => CPatternLike (Named n p)
instance CPatternLike p => CPatternLike [p]
instance CPatternLike p => CPatternLike (List1 p)
instance CPatternLike p => CPatternLike (List2 p)
instance CPatternLike p => CPatternLike (Maybe p)
instance CPatternLike p => CPatternLike (FieldAssignment' p)

-- | Compute a value from each subpattern and collect all values in a monoid.

foldCPattern :: (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
foldCPattern :: forall p m. (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
foldCPattern Pattern -> m
f = forall p m.
(CPatternLike p, Monoid m) =>
(Pattern -> m -> m) -> p -> m
foldrCPattern forall a b. (a -> b) -> a -> b
$ \ Pattern
p m
m -> Pattern -> m
f Pattern
p forall a. Monoid a => a -> a -> a
`mappend` m
m

-- | Traverse pattern(s) with a modification before the recursive descent.

preTraverseCPatternM
  :: (CPatternLike p, Monad m)
  => (Pattern -> m Pattern)  -- ^ @pre@: Modification before recursion.
  -> p -> m p
preTraverseCPatternM :: forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> p -> m p
preTraverseCPatternM Pattern -> m Pattern
pre p
p = forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM Pattern -> m Pattern
pre forall (m :: * -> *) a. Monad m => a -> m a
return p
p

-- | Traverse pattern(s) with a modification after the recursive descent.

postTraverseCPatternM
  :: (CPatternLike p, Monad m)
  => (Pattern -> m Pattern)  -- ^ @post@: Modification after recursion.
  -> p -> m p
postTraverseCPatternM :: forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> p -> m p
postTraverseCPatternM Pattern -> m Pattern
post p
p = forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> (Pattern -> m Pattern) -> p -> m p
traverseCPatternM forall (m :: * -> *) a. Monad m => a -> m a
return Pattern -> m Pattern
post p
p

-- | Map pattern(s) with a modification after the recursive descent.

mapCPattern :: CPatternLike p => (Pattern -> Pattern) -> p -> p
mapCPattern :: forall p. CPatternLike p => (Pattern -> Pattern) -> p -> p
mapCPattern Pattern -> Pattern
f = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p (m :: * -> *).
(CPatternLike p, Monad m) =>
(Pattern -> m Pattern) -> p -> m p
postTraverseCPatternM (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> Pattern
f)


-- * Specific folds.

-- | Get all the identifiers in a pattern in left-to-right order.
--
-- Implemented using difference lists.
patternQNames :: CPatternLike p => p -> [QName]
patternQNames :: forall p. CPatternLike p => p -> [QName]
patternQNames p
p = forall p m. (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
foldCPattern Pattern -> Endo [QName]
f p
p forall a. Endo a -> a -> a
`appEndo` []
  where
  f :: Pattern -> Endo [QName]
  f :: Pattern -> Endo [QName]
f = \case
    IdentP QName
x       -> forall a. (a -> a) -> Endo a
Endo (QName
x forall a. a -> [a] -> [a]
:)
    OpAppP Range
_ QName
x Set Name
_ [NamedArg Pattern]
_ -> forall a. (a -> a) -> Endo a
Endo (QName
x forall a. a -> [a] -> [a]
:)
    AsP Range
_ Name
x Pattern
_      -> forall a. Monoid a => a
mempty  -- x must be a bound name, can't be a constructor!
    AppP Pattern
_ NamedArg Pattern
_       -> forall a. Monoid a => a
mempty
    WithP Range
_ Pattern
_      -> forall a. Monoid a => a
mempty
    RawAppP Range
_ List2 Pattern
_    -> forall a. Monoid a => a
mempty
    HiddenP Range
_ Named NamedName Pattern
_    -> forall a. Monoid a => a
mempty
    ParenP Range
_ Pattern
_     -> forall a. Monoid a => a
mempty
    WildP Range
_        -> forall a. Monoid a => a
mempty
    AbsurdP Range
_      -> forall a. Monoid a => a
mempty
    DotP Range
_ Expr
_       -> forall a. Monoid a => a
mempty
    LitP Range
_ Literal
_       -> forall a. Monoid a => a
mempty
    QuoteP Range
_       -> forall a. Monoid a => a
mempty
    InstanceP Range
_ Named NamedName Pattern
_  -> forall a. Monoid a => a
mempty
    RecP Range
_ [FieldAssignment' Pattern]
_       -> forall a. Monoid a => a
mempty
    EqualP Range
_ [(Expr, Expr)]
_     -> forall a. Monoid a => a
mempty
    EllipsisP Range
_ Maybe Pattern
_  -> forall a. Monoid a => a
mempty

-- | Get all the identifiers in a pattern in left-to-right order.
patternNames :: Pattern -> [Name]
patternNames :: Pattern -> [Name]
patternNames = forall a b. (a -> b) -> [a] -> [b]
map QName -> Name
unqualify forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. CPatternLike p => p -> [QName]
patternQNames

-- | Does the pattern contain a with-pattern?
-- (Shortcutting.)
hasWithPatterns :: CPatternLike p => p -> Bool
hasWithPatterns :: forall p. CPatternLike p => p -> Bool
hasWithPatterns = Any -> Bool
getAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p m. (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
foldCPattern (Bool -> Any
Any forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> Bool
isWithPattern)

-- | Is 'WithP'?
isWithPattern :: Pattern -> Bool
isWithPattern :: Pattern -> Bool
isWithPattern = \case
  WithP{} -> Bool
True
  Pattern
_ -> Bool
False

-- | Count the number of with-subpatterns in a pattern?
numberOfWithPatterns :: CPatternLike p => p -> Int
numberOfWithPatterns :: forall p. CPatternLike p => p -> Int
numberOfWithPatterns = forall a. Sum a -> a
getSum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p m. (CPatternLike p, Monoid m) => (Pattern -> m) -> p -> m
foldCPattern (forall a. a -> Sum a
Sum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. Num a => Pattern -> a
f)
  where f :: Pattern -> a
f Pattern
p = if Pattern -> Bool
isWithPattern Pattern
p then a
1 else a
0

-- | Compute the context in which the ellipsis occurs, if at all.
--   If there are several occurrences, this is an error.
--   This only counts ellipsis that haven't already been expanded.
hasEllipsis' :: CPatternLike p => p -> AffineHole Pattern p
hasEllipsis' :: forall p. CPatternLike p => p -> AffineHole Pattern p
hasEllipsis' = forall p (m :: * -> *).
(CPatternLike p, Applicative m, Functor m) =>
(Pattern -> m Pattern -> m Pattern) -> p -> m p
traverseCPatternA forall a b. (a -> b) -> a -> b
$ \ Pattern
p AffineHole Pattern Pattern
mp ->
  case Pattern
p of
    EllipsisP Range
_ Maybe Pattern
Nothing -> forall r a. (r -> a) -> r -> AffineHole r a
OneHole forall a. a -> a
id Pattern
p
    Pattern
_                   -> AffineHole Pattern Pattern
mp

reintroduceEllipsis :: ExpandedEllipsis -> Pattern -> Pattern
reintroduceEllipsis :: ExpandedEllipsis -> Pattern -> Pattern
reintroduceEllipsis (ExpandedEllipsis Range
r Int
k) Pattern
p | forall p. CPatternLike p => p -> Bool
hasWithPatterns Pattern
p =
  let ([NamedArg Pattern]
args, [NamedArg Pattern]
wargs) = forall p. IsWithP p => Int -> [p] -> ([p], [p])
splitEllipsis Int
k forall a b. (a -> b) -> a -> b
$ forall l. IsList l => l -> [Item l]
List1.toList forall a b. (a -> b) -> a -> b
$ Pattern -> List1 (NamedArg Pattern)
patternAppView Pattern
p
      (NamedArg Pattern
hd,[NamedArg Pattern]
args') = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe (a, [a])
uncons [NamedArg Pattern]
args
      core :: Pattern
core = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Pattern -> NamedArg Pattern -> Pattern
AppP (forall a. NamedArg a -> a
namedArg NamedArg Pattern
hd) [NamedArg Pattern]
args
  in forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Pattern -> NamedArg Pattern -> Pattern
AppP (Range -> Maybe Pattern -> Pattern
EllipsisP Range
r forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Pattern
core) [NamedArg Pattern]
wargs
reintroduceEllipsis ExpandedEllipsis
_ Pattern
p = Pattern
p

splitEllipsis :: (IsWithP p) => Int -> [p] -> ([p],[p])
splitEllipsis :: forall p. IsWithP p => Int -> [p] -> ([p], [p])
splitEllipsis Int
k [] = ([] , [])
splitEllipsis Int
k (p
p:[p]
ps)
  | forall a. Maybe a -> Bool
isJust (forall p. IsWithP p => p -> Maybe p
isWithP p
p) = if
      | Int
k forall a. Eq a => a -> a -> Bool
== Int
0    -> ([] , p
pforall a. a -> [a] -> [a]
:[p]
ps)
      | Bool
otherwise -> forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (p
pforall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$ forall p. IsWithP p => Int -> [p] -> ([p], [p])
splitEllipsis (Int
kforall a. Num a => a -> a -> a
-Int
1) [p]
ps
  | Bool
otherwise = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (p
pforall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$ forall p. IsWithP p => Int -> [p] -> ([p], [p])
splitEllipsis Int
k [p]
ps

---------------------------------------------------------------------------
-- * Helpers for pattern and lhs parsing
---------------------------------------------------------------------------

-- | View a pattern @p@ as a list @p0 .. pn@ where @p0@ is the identifier
--   (in most cases a constructor).
--
--  Pattern needs to be parsed already (operators resolved).
patternAppView :: Pattern -> List1 (NamedArg Pattern)
patternAppView :: Pattern -> List1 (NamedArg Pattern)
patternAppView = \case
    AppP Pattern
p NamedArg Pattern
arg      -> Pattern -> List1 (NamedArg Pattern)
patternAppView Pattern
p forall a. NonEmpty a -> [a] -> NonEmpty a
`List1.appendList` [NamedArg Pattern
arg]
    OpAppP Range
_ QName
x Set Name
_ [NamedArg Pattern]
ps -> forall a. a -> NamedArg a
defaultNamedArg (QName -> Pattern
IdentP QName
x) forall a. a -> [a] -> NonEmpty a
:| [NamedArg Pattern]
ps
    ParenP Range
_ Pattern
p      -> Pattern -> List1 (NamedArg Pattern)
patternAppView Pattern
p
    RawAppP Range
_ List2 Pattern
_     -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Pattern
p               -> forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ forall a. a -> NamedArg a
defaultNamedArg Pattern
p