-- | Auxiliary functions to handle patterns in the abstract syntax.
--
--   Generic and specific traversals.

module Agda.Syntax.Abstract.Pattern where

import Prelude hiding (null)

import Control.Arrow           ( (***), second )
import Control.Monad           ( (>=>) )
import Control.Monad.Identity  ( Identity(..), runIdentity )
import Control.Applicative     ( liftA2 )


import Data.Maybe
import Data.Monoid

import Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Concrete (FieldAssignment')
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Pattern (IsWithP(..))
import Agda.Syntax.Info
import Agda.Syntax.Position

import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Null

import Agda.Utils.Impossible

-- * Generic traversals
------------------------------------------------------------------------

type NAP = NamedArg Pattern

class MapNamedArgPattern a  where
  mapNamedArgPattern :: (NAP -> NAP) -> a -> a

  default mapNamedArgPattern
     :: (Functor f, MapNamedArgPattern a', a ~ f a') => (NAP -> NAP) -> a -> a
  mapNamedArgPattern = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
MapNamedArgPattern a =>
(NamedArg Pattern -> NamedArg Pattern) -> a -> a
mapNamedArgPattern

instance MapNamedArgPattern NAP where
  mapNamedArgPattern :: (NamedArg Pattern -> NamedArg Pattern)
-> NamedArg Pattern -> NamedArg Pattern
mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
f NamedArg Pattern
p =
    case forall a. NamedArg a -> a
namedArg NamedArg Pattern
p of
      -- no sub patterns:
      VarP{}    -> NamedArg Pattern -> NamedArg Pattern
f NamedArg Pattern
p
      WildP{}   -> NamedArg Pattern -> NamedArg Pattern
f NamedArg Pattern
p
      DotP{}    -> NamedArg Pattern -> NamedArg Pattern
f NamedArg Pattern
p
      EqualP{}  -> NamedArg Pattern -> NamedArg Pattern
f NamedArg Pattern
p
      LitP{}    -> NamedArg Pattern -> NamedArg Pattern
f NamedArg Pattern
p
      AbsurdP{} -> NamedArg Pattern -> NamedArg Pattern
f NamedArg Pattern
p
      ProjP{}   -> NamedArg Pattern -> NamedArg Pattern
f NamedArg Pattern
p
      -- list of NamedArg subpatterns:
      ConP ConPatInfo
i AmbiguousQName
qs NAPs Expr
ps       -> NamedArg Pattern -> NamedArg Pattern
f forall a b. (a -> b) -> a -> b
$ forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg Pattern
p forall a b. (a -> b) -> a -> b
$ forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
ConP ConPatInfo
i AmbiguousQName
qs forall a b. (a -> b) -> a -> b
$ forall a.
MapNamedArgPattern a =>
(NamedArg Pattern -> NamedArg Pattern) -> a -> a
mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
f NAPs Expr
ps
      DefP PatInfo
i AmbiguousQName
qs NAPs Expr
ps       -> NamedArg Pattern -> NamedArg Pattern
f forall a b. (a -> b) -> a -> b
$ forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg Pattern
p forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP PatInfo
i AmbiguousQName
qs forall a b. (a -> b) -> a -> b
$ forall a.
MapNamedArgPattern a =>
(NamedArg Pattern -> NamedArg Pattern) -> a -> a
mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
f NAPs Expr
ps
      PatternSynP PatInfo
i AmbiguousQName
x NAPs Expr
ps -> NamedArg Pattern -> NamedArg Pattern
f forall a b. (a -> b) -> a -> b
$ forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg Pattern
p forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
PatternSynP PatInfo
i AmbiguousQName
x forall a b. (a -> b) -> a -> b
$ forall a.
MapNamedArgPattern a =>
(NamedArg Pattern -> NamedArg Pattern) -> a -> a
mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
f NAPs Expr
ps
      -- Pattern subpattern(s):
      -- RecP: we copy the NamedArg info to the subpatterns but discard it after recursion
      RecP PatInfo
i [FieldAssignment' Pattern]
fs          -> NamedArg Pattern -> NamedArg Pattern
f forall a b. (a -> b) -> a -> b
$ forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg Pattern
p forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
RecP PatInfo
i forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. NamedArg a -> a
namedArg) forall a b. (a -> b) -> a -> b
$ forall a.
MapNamedArgPattern a =>
(NamedArg Pattern -> NamedArg Pattern) -> a -> a
mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
f forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg Pattern
p)) [FieldAssignment' Pattern]
fs
      -- AsP: we hand the NamedArg info to the subpattern
      AsP PatInfo
i BindName
x Pattern
p0         -> NamedArg Pattern -> NamedArg Pattern
f forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
AsP PatInfo
i BindName
x) forall a b. (a -> b) -> a -> b
$ forall a.
MapNamedArgPattern a =>
(NamedArg Pattern -> NamedArg Pattern) -> a -> a
mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
f forall a b. (a -> b) -> a -> b
$ forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg Pattern
p Pattern
p0
      -- WithP: like AsP
      WithP PatInfo
i Pattern
p0         -> NamedArg Pattern -> NamedArg Pattern
f forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (forall e. PatInfo -> Pattern' e -> Pattern' e
WithP PatInfo
i) forall a b. (a -> b) -> a -> b
$ forall a.
MapNamedArgPattern a =>
(NamedArg Pattern -> NamedArg Pattern) -> a -> a
mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
f forall a b. (a -> b) -> a -> b
$ forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg Pattern
p Pattern
p0
      AnnP PatInfo
i Expr
a Pattern
p0        -> NamedArg Pattern -> NamedArg Pattern
f forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (forall e. PatInfo -> e -> Pattern' e -> Pattern' e
AnnP PatInfo
i Expr
a) forall a b. (a -> b) -> a -> b
$ forall a.
MapNamedArgPattern a =>
(NamedArg Pattern -> NamedArg Pattern) -> a -> a
mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
f forall a b. (a -> b) -> a -> b
$ forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg Pattern
p Pattern
p0

instance MapNamedArgPattern a => MapNamedArgPattern [a]                  where
instance MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) where
instance MapNamedArgPattern a => MapNamedArgPattern (Maybe a)            where

instance (MapNamedArgPattern a, MapNamedArgPattern b) => MapNamedArgPattern (a,b) where
  mapNamedArgPattern :: (NamedArg Pattern -> NamedArg Pattern) -> (a, b) -> (a, b)
mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
f (a
a, b
b) = (forall a.
MapNamedArgPattern a =>
(NamedArg Pattern -> NamedArg Pattern) -> a -> a
mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
f a
a, forall a.
MapNamedArgPattern a =>
(NamedArg Pattern -> NamedArg Pattern) -> a -> a
mapNamedArgPattern NamedArg Pattern -> NamedArg Pattern
f b
b)

-- | Generic pattern traversal.

class APatternLike p where
  type ADotT p

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

  default foldrAPattern
    :: (Monoid m, Foldable f, APatternLike b, (ADotT p) ~ (ADotT b), f b ~ p)
    => (Pattern' (ADotT p) -> m -> m) -> p -> m
  foldrAPattern = 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.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern

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

  default traverseAPatternM
    :: (Traversable f, APatternLike q, (ADotT p) ~ (ADotT q), f q ~ p, Monad m)
    => (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
    -> p -> m p
  traverseAPatternM Pattern' (ADotT p) -> m (Pattern' (ADotT p))
pre Pattern' (ADotT p) -> m (Pattern' (ADotT p))
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 :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
traverseAPatternM Pattern' (ADotT p) -> m (Pattern' (ADotT p))
pre Pattern' (ADotT p) -> m (Pattern' (ADotT p))
post

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

foldAPattern :: (APatternLike p, Monoid m) => (Pattern' (ADotT p) -> m) -> p -> m
foldAPattern :: forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m) -> p -> m
foldAPattern Pattern' (ADotT p) -> m
f = forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern forall a b. (a -> b) -> a -> b
$ \ Pattern' (ADotT p)
p m
m -> Pattern' (ADotT p) -> m
f Pattern' (ADotT p)
p forall a. Monoid a => a -> a -> a
`mappend` m
m

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

preTraverseAPatternM
  :: (APatternLike p, Monad m )
  => (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))  -- ^ @pre@: Modification before recursion.
  -> p -> m p
preTraverseAPatternM :: forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
preTraverseAPatternM Pattern' (ADotT p) -> m (Pattern' (ADotT p))
pre p
p = forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
traverseAPatternM Pattern' (ADotT p) -> m (Pattern' (ADotT p))
pre forall (m :: * -> *) a. Monad m => a -> m a
return p
p

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

postTraverseAPatternM
  :: (APatternLike p, Monad m )
  => (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))  -- ^ @post@: Modification after recursion.
  -> p -> m p
postTraverseAPatternM :: forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
postTraverseAPatternM Pattern' (ADotT p) -> m (Pattern' (ADotT p))
post p
p = forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
traverseAPatternM forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' (ADotT p) -> m (Pattern' (ADotT p))
post p
p

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

mapAPattern :: APatternLike p => (Pattern' (ADotT p) -> Pattern' (ADotT p)) -> p -> p
mapAPattern :: forall p.
APatternLike p =>
(Pattern' (ADotT p) -> Pattern' (ADotT p)) -> p -> p
mapAPattern Pattern' (ADotT p) -> Pattern' (ADotT p)
f = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
postTraverseAPatternM (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern' (ADotT p) -> Pattern' (ADotT p)
f)

-- Interesting instance:

instance APatternLike (Pattern' a) where
  type ADotT (Pattern' a) = a

  foldrAPattern :: forall m.
Monoid m =>
(Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m
foldrAPattern Pattern' (ADotT (Pattern' a)) -> m -> m
f Pattern' a
p = Pattern' (ADotT (Pattern' a)) -> m -> m
f Pattern' a
p forall a b. (a -> b) -> a -> b
$
    case Pattern' a
p of
      AsP PatInfo
_ BindName
_ Pattern' a
p          -> forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT (Pattern' a)) -> m -> m
f Pattern' a
p
      ConP ConPatInfo
_ AmbiguousQName
_ NAPs a
ps        -> forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT (Pattern' a)) -> m -> m
f NAPs a
ps
      DefP PatInfo
_ AmbiguousQName
_ NAPs a
ps        -> forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT (Pattern' a)) -> m -> m
f NAPs a
ps
      RecP PatInfo
_ [FieldAssignment' (Pattern' a)]
ps          -> forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT (Pattern' a)) -> m -> m
f [FieldAssignment' (Pattern' a)]
ps
      PatternSynP PatInfo
_ AmbiguousQName
_ NAPs a
ps -> forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT (Pattern' a)) -> m -> m
f NAPs a
ps
      WithP PatInfo
_ Pattern' a
p          -> forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT (Pattern' a)) -> m -> m
f Pattern' a
p
      VarP BindName
_             -> forall a. Monoid a => a
mempty
      ProjP PatInfo
_ ProjOrigin
_ AmbiguousQName
_        -> forall a. Monoid a => a
mempty
      WildP PatInfo
_            -> forall a. Monoid a => a
mempty
      DotP PatInfo
_ a
_           -> forall a. Monoid a => a
mempty
      AbsurdP PatInfo
_          -> forall a. Monoid a => a
mempty
      LitP PatInfo
_ Literal
_           -> forall a. Monoid a => a
mempty
      EqualP PatInfo
_ [(a, a)]
_         -> forall a. Monoid a => a
mempty
      AnnP PatInfo
_ a
_ Pattern' a
p         -> forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT (Pattern' a)) -> m -> m
f Pattern' a
p

  traverseAPatternM :: forall (m :: * -> *).
Monad m =>
(Pattern' (ADotT (Pattern' a))
 -> m (Pattern' (ADotT (Pattern' a))))
-> (Pattern' (ADotT (Pattern' a))
    -> m (Pattern' (ADotT (Pattern' a))))
-> Pattern' a
-> m (Pattern' a)
traverseAPatternM Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post = Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Pattern' a -> m (Pattern' a)
recurse forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post
    where
    recurse :: Pattern' a -> m (Pattern' a)
recurse = \case
      -- Non-recursive cases:
      p :: Pattern' a
p@A.VarP{}            -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      p :: Pattern' a
p@A.WildP{}           -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      p :: Pattern' a
p@A.DotP{}            -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      p :: Pattern' a
p@A.LitP{}            -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      p :: Pattern' a
p@A.AbsurdP{}         -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      p :: Pattern' a
p@A.ProjP{}           -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      p :: Pattern' a
p@A.EqualP{}          -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      -- Recursive cases:
      A.ConP        ConPatInfo
i AmbiguousQName
ds NAPs a
ps -> forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP        ConPatInfo
i AmbiguousQName
ds forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
traverseAPatternM Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post NAPs a
ps
      A.DefP        PatInfo
i AmbiguousQName
q  NAPs a
ps -> forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP        PatInfo
i AmbiguousQName
q  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
traverseAPatternM Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post NAPs a
ps
      A.AsP         PatInfo
i BindName
x  Pattern' a
p  -> forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP         PatInfo
i BindName
x  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
traverseAPatternM Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post Pattern' a
p
      A.RecP        PatInfo
i    [FieldAssignment' (Pattern' a)]
ps -> forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP        PatInfo
i    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
traverseAPatternM Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post [FieldAssignment' (Pattern' a)]
ps
      A.PatternSynP PatInfo
i AmbiguousQName
x  NAPs a
ps -> forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.PatternSynP PatInfo
i AmbiguousQName
x  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
traverseAPatternM Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post NAPs a
ps
      A.WithP       PatInfo
i Pattern' a
p     -> forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP       PatInfo
i    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
traverseAPatternM Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post Pattern' a
p
      A.AnnP        PatInfo
i a
a  Pattern' a
p  -> forall e. PatInfo -> e -> Pattern' e -> Pattern' e
A.AnnP        PatInfo
i a
a  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
traverseAPatternM Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post Pattern' a
p

instance APatternLike a => APatternLike (Arg a) where
  type ADotT (Arg a) = ADotT a

instance APatternLike a => APatternLike (Named n a) where
  type ADotT (Named n a) = ADotT a

instance APatternLike a => APatternLike [a] where
  type ADotT [a] = ADotT a

instance APatternLike a => APatternLike (Maybe a) where
  type ADotT (Maybe a) = ADotT a

instance APatternLike a => APatternLike (FieldAssignment' a) where
  type ADotT (FieldAssignment' a) = ADotT a

instance (APatternLike a, APatternLike b, ADotT a ~ ADotT b) => APatternLike (a, b) where
  type ADotT (a, b) = ADotT a

  foldrAPattern :: forall m.
Monoid m =>
(Pattern' (ADotT (a, b)) -> m -> m) -> (a, b) -> m
foldrAPattern Pattern' (ADotT (a, b)) -> m -> m
f (a
p, b
p') =
    forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT (a, b)) -> m -> m
f a
p forall a. Monoid a => a -> a -> a
`mappend` forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT (a, b)) -> m -> m
f b
p'

  traverseAPatternM :: forall (m :: * -> *).
Monad m =>
(Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b))))
-> (Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b))))
-> (a, b)
-> m (a, b)
traverseAPatternM Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
pre Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
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 :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
traverseAPatternM Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
pre Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
post a
p)
      (forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
traverseAPatternM Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
pre Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
post b
p')


-- * Specific folds
------------------------------------------------------------------------

-- | Collect pattern variables in left-to-right textual order.

patternVars :: APatternLike p => p -> [A.Name]
patternVars :: forall p. APatternLike p => p -> [Name]
patternVars p
p = forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m) -> p -> m
foldAPattern forall a. Pattern' a -> Endo [Name]
f p
p forall a. Endo a -> a -> a
`appEndo` []
  where
  -- We use difference lists @[A.Name] -> [A.Name]@ to avoid reconcatenation.
  f :: Pattern' a -> Endo [A.Name]
  f :: forall a. Pattern' a -> Endo [Name]
f = \case
    A.VarP BindName
x         -> forall a. (a -> a) -> Endo a
Endo (BindName -> Name
unBind BindName
x forall a. a -> [a] -> [a]
:)
    A.AsP PatInfo
_ BindName
x Pattern' a
_      -> forall a. (a -> a) -> Endo a
Endo (BindName -> Name
unBind BindName
x forall a. a -> [a] -> [a]
:)
    A.LitP        {} -> forall a. Monoid a => a
mempty
    A.ConP        {} -> forall a. Monoid a => a
mempty
    A.RecP        {} -> forall a. Monoid a => a
mempty
    A.DefP        {} -> forall a. Monoid a => a
mempty
    A.ProjP       {} -> forall a. Monoid a => a
mempty
    A.WildP       {} -> forall a. Monoid a => a
mempty
    A.DotP        {} -> forall a. Monoid a => a
mempty
    A.AbsurdP     {} -> forall a. Monoid a => a
mempty
    A.EqualP      {} -> forall a. Monoid a => a
mempty
    A.PatternSynP {} -> forall a. Monoid a => a
mempty
    A.WithP PatInfo
_ Pattern' a
_      -> forall a. Monoid a => a
mempty
    A.AnnP        {} -> forall a. Monoid a => a
mempty

-- | Check if a pattern contains a specific (sub)pattern.

containsAPattern :: APatternLike p => (Pattern' (ADotT p) -> Bool) -> p -> Bool
containsAPattern :: forall p.
APatternLike p =>
(Pattern' (ADotT p) -> Bool) -> p -> Bool
containsAPattern Pattern' (ADotT p) -> Bool
f = Any -> Bool
getAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m) -> p -> m
foldAPattern (Bool -> Any
Any forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern' (ADotT p) -> Bool
f)

-- | Check if a pattern contains an absurd pattern.
--   For instance, @suc ()@, does so.
--
--   Precondition: contains no pattern synonyms.

containsAbsurdPattern :: APatternLike p => p -> Bool
containsAbsurdPattern :: forall p. APatternLike p => p -> Bool
containsAbsurdPattern = forall p.
APatternLike p =>
(Pattern' (ADotT p) -> Bool) -> p -> Bool
containsAPattern forall a b. (a -> b) -> a -> b
$ \case
    A.PatternSynP{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    A.AbsurdP{}     -> Bool
True
    Pattern' (ADotT p)
_               -> Bool
False

-- | Check if a pattern contains an @-pattern.
--
containsAsPattern :: APatternLike p => p -> Bool
containsAsPattern :: forall p. APatternLike p => p -> Bool
containsAsPattern = forall p.
APatternLike p =>
(Pattern' (ADotT p) -> Bool) -> p -> Bool
containsAPattern forall a b. (a -> b) -> a -> b
$ \case
    A.AsP{}         -> Bool
True
    Pattern' (ADotT p)
_               -> Bool
False

-- | Check if any user-written pattern variables occur more than once,
--   and throw the given error if they do.
checkPatternLinearity :: (Monad m, APatternLike p)
                      => p -> ([C.Name] -> m ()) -> m ()
checkPatternLinearity :: forall (m :: * -> *) p.
(Monad m, APatternLike p) =>
p -> ([Name] -> m ()) -> m ()
checkPatternLinearity p
ps [Name] -> m ()
err =
  forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (forall a. Ord a => [a] -> [a]
duplicates forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
nameConcrete forall a b. (a -> b) -> a -> b
$ forall p. APatternLike p => p -> [Name]
patternVars p
ps) forall a b. (a -> b) -> a -> b
$ \[Name]
ys -> [Name] -> m ()
err [Name]
ys


-- * Specific traversals
------------------------------------------------------------------------

-- | Pattern substitution.
--
-- For the embedded expression, the given pattern substitution is turned into
-- an expression substitution.

substPattern :: [(Name, Pattern)] -> Pattern -> Pattern
substPattern :: [(Name, Pattern)] -> Pattern -> Pattern
substPattern [(Name, Pattern)]
s = forall e.
(e -> e) -> [(Name, Pattern' e)] -> Pattern' e -> Pattern' e
substPattern' (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Pattern -> Expr
patternToExpr) [(Name, Pattern)]
s) [(Name, Pattern)]
s

-- | Pattern substitution, parametrized by substitution function for embedded expressions.

substPattern'
  :: (e -> e)              -- ^ Substitution function for expressions.
  -> [(Name, Pattern' e)]  -- ^ (Parallel) substitution.
  -> Pattern' e            -- ^ Input pattern.
  -> Pattern' e
substPattern' :: forall e.
(e -> e) -> [(Name, Pattern' e)] -> Pattern' e -> Pattern' e
substPattern' e -> e
subE [(Name, Pattern' e)]
s = forall p.
APatternLike p =>
(Pattern' (ADotT p) -> Pattern' (ADotT p)) -> p -> p
mapAPattern forall a b. (a -> b) -> a -> b
$ \ Pattern' (ADotT (Pattern' e))
p -> case Pattern' (ADotT (Pattern' e))
p of
  VarP BindName
x            -> forall a. a -> Maybe a -> a
fromMaybe Pattern' (ADotT (Pattern' e))
p forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (BindName -> Name
A.unBind BindName
x) [(Name, Pattern' e)]
s
  DotP PatInfo
i ADotT (Pattern' e)
e          -> forall e. PatInfo -> e -> Pattern' e
DotP PatInfo
i forall a b. (a -> b) -> a -> b
$ e -> e
subE ADotT (Pattern' e)
e
  EqualP PatInfo
i [(ADotT (Pattern' e), ADotT (Pattern' e))]
es       -> forall e. PatInfo -> [(e, e)] -> Pattern' e
EqualP PatInfo
i forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (e -> e
subE forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** e -> e
subE) [(ADotT (Pattern' e), ADotT (Pattern' e))]
es
  AnnP PatInfo
i ADotT (Pattern' e)
a Pattern' (ADotT (Pattern' e))
p        -> forall e. PatInfo -> e -> Pattern' e -> Pattern' e
AnnP PatInfo
i (e -> e
subE ADotT (Pattern' e)
a) Pattern' (ADotT (Pattern' e))
p
  -- No action on the other patterns (besides the recursion):
  ConP ConPatInfo
_ AmbiguousQName
_ NAPs (ADotT (Pattern' e))
_        -> Pattern' (ADotT (Pattern' e))
p
  RecP PatInfo
_ [FieldAssignment' (Pattern' (ADotT (Pattern' e)))]
_          -> Pattern' (ADotT (Pattern' e))
p
  ProjP PatInfo
_ ProjOrigin
_ AmbiguousQName
_       -> Pattern' (ADotT (Pattern' e))
p
  WildP PatInfo
_           -> Pattern' (ADotT (Pattern' e))
p
  AbsurdP PatInfo
_         -> Pattern' (ADotT (Pattern' e))
p
  LitP PatInfo
_ Literal
_          -> Pattern' (ADotT (Pattern' e))
p
  DefP PatInfo
_ AmbiguousQName
_ NAPs (ADotT (Pattern' e))
_        -> Pattern' (ADotT (Pattern' e))
p
  AsP PatInfo
_ BindName
_ Pattern' (ADotT (Pattern' e))
_         -> Pattern' (ADotT (Pattern' e))
p -- Note: cannot substitute into as-variable
  PatternSynP PatInfo
_ AmbiguousQName
_ NAPs (ADotT (Pattern' e))
_ -> Pattern' (ADotT (Pattern' e))
p
  WithP PatInfo
_ Pattern' (ADotT (Pattern' e))
_         -> Pattern' (ADotT (Pattern' e))
p


-- * Other pattern utilities
------------------------------------------------------------------------

-- | Check for with-pattern.
instance IsWithP (Pattern' e) where
  isWithP :: Pattern' e -> Maybe (Pattern' e)
isWithP = \case
    WithP PatInfo
_ Pattern' e
p -> forall a. a -> Maybe a
Just Pattern' e
p
    Pattern' e
_ -> forall a. Maybe a
Nothing

-- | Split patterns into (patterns, trailing with-patterns).
splitOffTrailingWithPatterns :: A.Patterns -> (A.Patterns, A.Patterns)
splitOffTrailingWithPatterns :: NAPs Expr -> (NAPs Expr, NAPs Expr)
splitOffTrailingWithPatterns = forall a. (a -> Bool) -> [a] -> ([a], [a])
spanEnd (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. IsWithP p => p -> Maybe p
isWithP)

-- | Get the tail of with-patterns of a pattern spine.
trailingWithPatterns :: Patterns -> Patterns
trailingWithPatterns :: NAPs Expr -> NAPs Expr
trailingWithPatterns = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. NAPs Expr -> (NAPs Expr, NAPs Expr)
splitOffTrailingWithPatterns

-- | The next patterns are ...
--
-- (This view discards 'PatInfo'.)
data LHSPatternView e
  = LHSAppP  (NAPs e)
      -- ^ Application patterns (non-empty list).
  | LHSProjP ProjOrigin AmbiguousQName (NamedArg (Pattern' e))
      -- ^ A projection pattern.  Is also stored unmodified here.
  | LHSWithP [Pattern' e]
      -- ^ With patterns (non-empty list).
      --   These patterns are not prefixed with 'WithP'.
  deriving (Int -> LHSPatternView e -> ShowS
forall e. Show e => Int -> LHSPatternView e -> ShowS
forall e. Show e => [LHSPatternView e] -> ShowS
forall e. Show e => LHSPatternView e -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LHSPatternView e] -> ShowS
$cshowList :: forall e. Show e => [LHSPatternView e] -> ShowS
show :: LHSPatternView e -> String
$cshow :: forall e. Show e => LHSPatternView e -> String
showsPrec :: Int -> LHSPatternView e -> ShowS
$cshowsPrec :: forall e. Show e => Int -> LHSPatternView e -> ShowS
Show)

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

lhsPatternView :: IsProjP e => NAPs e -> Maybe (LHSPatternView e, NAPs e)
lhsPatternView :: forall e. IsProjP e => NAPs e -> Maybe (LHSPatternView e, NAPs e)
lhsPatternView [] = forall a. Maybe a
Nothing
lhsPatternView (NamedArg (Pattern' e)
p0 : [NamedArg (Pattern' e)]
ps) =
  case forall a. NamedArg a -> a
namedArg NamedArg (Pattern' e)
p0 of
    ProjP PatInfo
_i ProjOrigin
o AmbiguousQName
d -> forall a. a -> Maybe a
Just (forall e.
ProjOrigin
-> AmbiguousQName -> NamedArg (Pattern' e) -> LHSPatternView e
LHSProjP ProjOrigin
o AmbiguousQName
d NamedArg (Pattern' e)
p0, [NamedArg (Pattern' e)]
ps)
    -- If the next pattern is a with-pattern, collect more with-patterns
    WithP PatInfo
_i Pattern' e
p   -> forall a. a -> Maybe a
Just (forall e. [Pattern' e] -> LHSPatternView e
LHSWithP (Pattern' e
p forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg [NamedArg (Pattern' e)]
ps1), [NamedArg (Pattern' e)]
ps2)
      where
      ([NamedArg (Pattern' e)]
ps1, [NamedArg (Pattern' e)]
ps2) = forall a b. (a -> Maybe b) -> [a] -> (Prefix b, [a])
spanJust forall p. IsWithP p => p -> Maybe p
isWithP [NamedArg (Pattern' e)]
ps
    -- If the next pattern is an application pattern, collect more of these
    Pattern' e
_ -> forall a. a -> Maybe a
Just (forall e. NAPs e -> LHSPatternView e
LHSAppP (NamedArg (Pattern' e)
p0 forall a. a -> [a] -> [a]
: [NamedArg (Pattern' e)]
ps1), [NamedArg (Pattern' e)]
ps2)
      where
      ([NamedArg (Pattern' e)]
ps1, [NamedArg (Pattern' e)]
ps2) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\ NamedArg (Pattern' e)
p -> forall a. Maybe a -> Bool
isNothing (forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP NamedArg (Pattern' e)
p) Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isNothing (forall p. IsWithP p => p -> Maybe p
isWithP NamedArg (Pattern' e)
p)) [NamedArg (Pattern' e)]
ps

-- * Left-hand-side manipulation
------------------------------------------------------------------------

-- | Convert a focused lhs to spine view and back.
class LHSToSpine a b where
  lhsToSpine :: a -> b
  spineToLhs :: b -> a

-- | Clause instance.
instance LHSToSpine Clause SpineClause where
  lhsToSpine :: Clause -> SpineClause
lhsToSpine = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. LHSToSpine a b => a -> b
lhsToSpine
  spineToLhs :: SpineClause -> Clause
spineToLhs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. LHSToSpine a b => b -> a
spineToLhs

-- | List instance (for clauses).
instance LHSToSpine a b => LHSToSpine [a] [b] where
  lhsToSpine :: [a] -> [b]
lhsToSpine = forall a b. (a -> b) -> [a] -> [b]
map forall a b. LHSToSpine a b => a -> b
lhsToSpine
  spineToLhs :: [b] -> [a]
spineToLhs = forall a b. (a -> b) -> [a] -> [b]
map forall a b. LHSToSpine a b => b -> a
spineToLhs

-- | LHS instance.
instance LHSToSpine LHS SpineLHS where
  lhsToSpine :: LHS -> SpineLHS
lhsToSpine (LHS LHSInfo
i LHSCore
core) = LHSInfo -> QName -> NAPs Expr -> SpineLHS
SpineLHS LHSInfo
i QName
f NAPs Expr
ps
    where QNamed QName
f NAPs Expr
ps = forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
lhsCoreToSpine LHSCore
core
  spineToLhs :: SpineLHS -> LHS
spineToLhs (SpineLHS LHSInfo
i QName
f NAPs Expr
ps) = LHSInfo -> LHSCore -> LHS
LHS LHSInfo
i (forall e. IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e
spineToLhsCore forall a b. (a -> b) -> a -> b
$ forall a. QName -> a -> QNamed a
QNamed QName
f NAPs Expr
ps)

lhsCoreToSpine :: LHSCore' e -> A.QNamed [NamedArg (Pattern' e)]
lhsCoreToSpine :: forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
lhsCoreToSpine = \case
  LHSHead QName
f [NamedArg (Pattern' e)]
ps     -> forall a. QName -> a -> QNamed a
QNamed QName
f [NamedArg (Pattern' e)]
ps
  LHSProj AmbiguousQName
d NamedArg (LHSCore' e)
h [NamedArg (Pattern' e)]
ps   -> forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
lhsCoreToSpine (forall a. NamedArg a -> a
namedArg NamedArg (LHSCore' e)
h) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (forall a. [a] -> [a] -> [a]
++ (NamedArg (Pattern' e)
p forall a. a -> [a] -> [a]
: [NamedArg (Pattern' e)]
ps))
    where p :: NamedArg (Pattern' e)
p = forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
ProjP forall a. Null a => a
empty ProjOrigin
ProjPrefix AmbiguousQName
d) NamedArg (LHSCore' e)
h
  LHSWith LHSCore' e
h [Arg (Pattern' e)]
wps [NamedArg (Pattern' e)]
ps -> forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
lhsCoreToSpine LHSCore' e
h forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg (Pattern' e) -> NamedArg (Pattern' e)
fromWithPat [Arg (Pattern' e)]
wps forall a. [a] -> [a] -> [a]
++ [NamedArg (Pattern' e)]
ps)
    where
      fromWithPat :: Arg (Pattern' e) -> NamedArg (Pattern' e)
      fromWithPat :: forall e. Arg (Pattern' e) -> NamedArg (Pattern' e)
fromWithPat = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a name. a -> Named name a
unnamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {e}. Pattern' e -> Pattern' e
mkWithP)
      mkWithP :: Pattern' e -> Pattern' e
mkWithP Pattern' e
p   = forall e. PatInfo -> Pattern' e -> Pattern' e
WithP (Range -> PatInfo
PatRange forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange Pattern' e
p) Pattern' e
p

spineToLhsCore :: IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e
spineToLhsCore :: forall e. IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e
spineToLhsCore (QNamed QName
f [NamedArg (Pattern' e)]
ps) = forall e.
IsProjP e =>
LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreAddSpine (forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSHead QName
f []) [NamedArg (Pattern' e)]
ps

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

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

lhsCoreAddChunk :: IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e
lhsCoreAddChunk :: forall e. IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e
lhsCoreAddChunk LHSCore' e
core = \case
  LHSAppP NAPs e
ps               -> forall e. LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreApp LHSCore' e
core NAPs e
ps
  LHSWithP [Pattern' e]
wps             -> forall e. LHSCore' e -> [Arg (Pattern' e)] -> LHSCore' e
lhsCoreWith LHSCore' e
core (forall a. a -> Arg a
defaultArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pattern' e]
wps)
  LHSProjP ProjOrigin
ProjPrefix AmbiguousQName
d NamedArg (Pattern' e)
np -> forall e.
AmbiguousQName
-> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSProj AmbiguousQName
d (forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' e)
np LHSCore' e
core) []  -- Prefix projection pattern.
  LHSProjP ProjOrigin
_          AmbiguousQName
_ NamedArg (Pattern' e)
np -> forall e. LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreApp LHSCore' e
core [NamedArg (Pattern' e)
np]       -- Postfix projection pattern.

-- | Add projection, with, and applicative patterns to the right.
lhsCoreAddSpine :: IsProjP e => LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreAddSpine :: forall e.
IsProjP e =>
LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreAddSpine LHSCore' e
core [NamedArg (Pattern' e)]
ps =
  -- Recurse on lhsPatternView until no patterns left.
  case forall e. IsProjP e => NAPs e -> Maybe (LHSPatternView e, NAPs e)
lhsPatternView [NamedArg (Pattern' e)]
ps of
    Maybe (LHSPatternView e, [NamedArg (Pattern' e)])
Nothing       -> LHSCore' e
core
    Just (LHSPatternView e
v, [NamedArg (Pattern' e)]
ps') -> forall e. IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e
lhsCoreAddChunk LHSCore' e
core LHSPatternView e
chunk forall e.
IsProjP e =>
LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
`lhsCoreAddSpine` [NamedArg (Pattern' e)]
ps'
      where
      -- Andreas, 2016-06-13
      -- If the projection was written prefix by the user
      -- or it is a fully applied operator
      -- we turn it to prefix projection form.
      chunk :: LHSPatternView e
chunk = case LHSPatternView e
v of
        LHSProjP ProjOrigin
ProjPrefix AmbiguousQName
_ NamedArg (Pattern' e)
_
          -> LHSPatternView e
v
        LHSProjP ProjOrigin
_ AmbiguousQName
d NamedArg (Pattern' e)
np | let nh :: Int
nh = forall a. NumHoles a => a -> Int
C.numHoles AmbiguousQName
d, Int
nh forall a. Ord a => a -> a -> Bool
> Int
0, Int
nh forall a. Ord a => a -> a -> Bool
<= Int
1 forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg (Pattern' e)]
ps'
          -> forall e.
ProjOrigin
-> AmbiguousQName -> NamedArg (Pattern' e) -> LHSPatternView e
LHSProjP ProjOrigin
ProjPrefix AmbiguousQName
d NamedArg (Pattern' e)
np
        LHSPatternView e
_ -> LHSPatternView e
v

-- | Used for checking pattern linearity.
lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]
lhsCoreAllPatterns :: forall e. LHSCore' e -> [Pattern' e]
lhsCoreAllPatterns = forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. QNamed a -> a
qnamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
lhsCoreToSpine

-- | Used in ''Agda.Syntax.Translation.AbstractToConcrete''.
--   Returns a 'DefP'.
lhsCoreToPattern :: LHSCore -> Pattern
lhsCoreToPattern :: LHSCore -> Pattern
lhsCoreToPattern LHSCore
lc =
  case LHSCore
lc of
    LHSHead QName
f NAPs Expr
aps         -> forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP PatInfo
noInfo (QName -> AmbiguousQName
unambiguous QName
f) NAPs Expr
aps
    LHSProj AmbiguousQName
d NamedArg LHSCore
lhscore NAPs Expr
aps -> forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP PatInfo
noInfo AmbiguousQName
d forall a b. (a -> b) -> a -> b
$
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHSCore -> Pattern
lhsCoreToPattern) NamedArg LHSCore
lhscore forall a. a -> [a] -> [a]
: NAPs Expr
aps
    LHSWith LHSCore
h [Arg Pattern]
wps NAPs Expr
aps     -> case LHSCore -> Pattern
lhsCoreToPattern LHSCore
h of
      DefP PatInfo
r AmbiguousQName
q NAPs Expr
ps         -> forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP PatInfo
r AmbiguousQName
q forall a b. (a -> b) -> a -> b
$ NAPs Expr
ps forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Arg Pattern -> NamedArg Pattern
fromWithPat [Arg Pattern]
wps forall a. [a] -> [a] -> [a]
++ NAPs Expr
aps
        where
          fromWithPat :: Arg Pattern -> NamedArg Pattern
          fromWithPat :: Arg Pattern -> NamedArg Pattern
fromWithPat = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a name. a -> Named name a
unnamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {e}. Pattern' e -> Pattern' e
mkWithP)
          mkWithP :: Pattern' e -> Pattern' e
mkWithP Pattern' e
p   = forall e. PatInfo -> Pattern' e -> Pattern' e
WithP (Range -> PatInfo
PatRange forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange Pattern' e
p) Pattern' e
p
      Pattern
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
  where noInfo :: PatInfo
noInfo = forall a. Null a => a
empty -- TODO, preserve range!

mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore
mapLHSHead :: (QName -> NAPs Expr -> LHSCore) -> LHSCore -> LHSCore
mapLHSHead QName -> NAPs Expr -> LHSCore
f = \case
  LHSHead QName
x NAPs Expr
ps     -> QName -> NAPs Expr -> LHSCore
f QName
x NAPs Expr
ps
  LHSProj AmbiguousQName
d NamedArg LHSCore
h NAPs Expr
ps   -> forall e.
AmbiguousQName
-> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSProj AmbiguousQName
d (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName -> NAPs Expr -> LHSCore) -> LHSCore -> LHSCore
mapLHSHead QName -> NAPs Expr -> LHSCore
f)) NamedArg LHSCore
h) NAPs Expr
ps
  LHSWith LHSCore
h [Arg Pattern]
wps NAPs Expr
ps -> forall e.
LHSCore' e
-> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSWith ((QName -> NAPs Expr -> LHSCore) -> LHSCore -> LHSCore
mapLHSHead QName -> NAPs Expr -> LHSCore
f LHSCore
h) [Arg Pattern]
wps NAPs Expr
ps