-- | 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.Monad.Reader    ( Reader, runReader, asks, local )
import Control.Applicative     ( liftA2 )

import Data.Maybe
import Data.Monoid
import Data.Void (Void)

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.List1 ( List1, pattern (:|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Utils.Singleton

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 = (a' -> a') -> a -> a
(a' -> a') -> f a' -> f a'
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a' -> a') -> a -> a)
-> ((NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> a' -> a')
-> (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a' -> a'
forall a.
MapNamedArgPattern a =>
(NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
mapNamedArgPattern

instance MapNamedArgPattern NAP where
  mapNamedArgPattern :: (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f NamedArg (Pattern' Expr)
p =
    case NamedArg (Pattern' Expr) -> Pattern' Expr
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' Expr)
p of
      -- no sub patterns:
      VarP{}    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f NamedArg (Pattern' Expr)
p
      WildP{}   -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f NamedArg (Pattern' Expr)
p
      DotP{}    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f NamedArg (Pattern' Expr)
p
      EqualP{}  -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f NamedArg (Pattern' Expr)
p
      LitP{}    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f NamedArg (Pattern' Expr)
p
      AbsurdP{} -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f NamedArg (Pattern' Expr)
p
      ProjP{}   -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f NamedArg (Pattern' Expr)
p
      -- list of NamedArg subpatterns:
      ConP ConPatInfo
i AmbiguousQName
qs NAPs Expr
ps       -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' Expr)
-> Pattern' Expr -> NamedArg (Pattern' Expr)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' Expr)
p (Pattern' Expr -> NamedArg (Pattern' Expr))
-> Pattern' Expr -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ ConPatInfo -> AmbiguousQName -> NAPs Expr -> Pattern' Expr
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
ConP ConPatInfo
i AmbiguousQName
qs (NAPs Expr -> Pattern' Expr) -> NAPs Expr -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NAPs Expr -> NAPs Expr
forall a.
MapNamedArgPattern a =>
(NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f NAPs Expr
ps
      DefP PatInfo
i AmbiguousQName
qs NAPs Expr
ps       -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' Expr)
-> Pattern' Expr -> NamedArg (Pattern' Expr)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' Expr)
p (Pattern' Expr -> NamedArg (Pattern' Expr))
-> Pattern' Expr -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern' Expr
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP PatInfo
i AmbiguousQName
qs (NAPs Expr -> Pattern' Expr) -> NAPs Expr -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NAPs Expr -> NAPs Expr
forall a.
MapNamedArgPattern a =>
(NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f NAPs Expr
ps
      PatternSynP PatInfo
i AmbiguousQName
x NAPs Expr
ps -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' Expr)
-> Pattern' Expr -> NamedArg (Pattern' Expr)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' Expr)
p (Pattern' Expr -> NamedArg (Pattern' Expr))
-> Pattern' Expr -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern' Expr
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
PatternSynP PatInfo
i AmbiguousQName
x (NAPs Expr -> Pattern' Expr) -> NAPs Expr -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NAPs Expr -> NAPs Expr
forall a.
MapNamedArgPattern a =>
(NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f NAPs Expr
ps
      -- Pattern subpattern(s):
      -- RecP: we copy the NamedArg info to the subpatterns but discard it after recursion
      RecP ConPatInfo
i [FieldAssignment' (Pattern' Expr)]
fs          -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' Expr)
-> Pattern' Expr -> NamedArg (Pattern' Expr)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' Expr)
p (Pattern' Expr -> NamedArg (Pattern' Expr))
-> Pattern' Expr -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ ConPatInfo -> [FieldAssignment' (Pattern' Expr)] -> Pattern' Expr
forall e.
ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
RecP ConPatInfo
i ([FieldAssignment' (Pattern' Expr)] -> Pattern' Expr)
-> [FieldAssignment' (Pattern' Expr)] -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ (FieldAssignment' (NamedArg (Pattern' Expr))
 -> FieldAssignment' (Pattern' Expr))
-> [FieldAssignment' (NamedArg (Pattern' Expr))]
-> [FieldAssignment' (Pattern' Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg (Pattern' Expr) -> Pattern' Expr)
-> FieldAssignment' (NamedArg (Pattern' Expr))
-> FieldAssignment' (Pattern' Expr)
forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedArg (Pattern' Expr) -> Pattern' Expr
forall a. NamedArg a -> a
namedArg) ([FieldAssignment' (NamedArg (Pattern' Expr))]
 -> [FieldAssignment' (Pattern' Expr)])
-> [FieldAssignment' (NamedArg (Pattern' Expr))]
-> [FieldAssignment' (Pattern' Expr)]
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> [FieldAssignment' (NamedArg (Pattern' Expr))]
-> [FieldAssignment' (NamedArg (Pattern' Expr))]
forall a.
MapNamedArgPattern a =>
(NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f ([FieldAssignment' (NamedArg (Pattern' Expr))]
 -> [FieldAssignment' (NamedArg (Pattern' Expr))])
-> [FieldAssignment' (NamedArg (Pattern' Expr))]
-> [FieldAssignment' (NamedArg (Pattern' Expr))]
forall a b. (a -> b) -> a -> b
$ (FieldAssignment' (Pattern' Expr)
 -> FieldAssignment' (NamedArg (Pattern' Expr)))
-> [FieldAssignment' (Pattern' Expr)]
-> [FieldAssignment' (NamedArg (Pattern' Expr))]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern' Expr -> NamedArg (Pattern' Expr))
-> FieldAssignment' (Pattern' Expr)
-> FieldAssignment' (NamedArg (Pattern' Expr))
forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (NamedArg (Pattern' Expr)
-> Pattern' Expr -> NamedArg (Pattern' Expr)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' Expr)
p)) [FieldAssignment' (Pattern' Expr)]
fs
      -- AsP: we hand the NamedArg info to the subpattern
      AsP PatInfo
i BindName
x Pattern' Expr
p0         -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ (Pattern' Expr -> Pattern' Expr)
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (PatInfo -> BindName -> Pattern' Expr -> Pattern' Expr
forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
AsP PatInfo
i BindName
x) (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a.
MapNamedArgPattern a =>
(NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' Expr)
-> Pattern' Expr -> NamedArg (Pattern' Expr)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' Expr)
p Pattern' Expr
p0
      -- WithP: like AsP
      WithP PatInfo
i Pattern' Expr
p0         -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ (Pattern' Expr -> Pattern' Expr)
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (PatInfo -> Pattern' Expr -> Pattern' Expr
forall e. PatInfo -> Pattern' e -> Pattern' e
WithP PatInfo
i) (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a.
MapNamedArgPattern a =>
(NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' Expr)
-> Pattern' Expr -> NamedArg (Pattern' Expr)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' Expr)
p Pattern' Expr
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' Expr) -> NamedArg (Pattern' Expr))
-> (a, b) -> (a, b)
mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f (a
a, b
b) = ((NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
forall a.
MapNamedArgPattern a =>
(NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
f a
a, (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> b -> b
forall a.
MapNamedArgPattern a =>
(NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)) -> a -> a
mapNamedArgPattern NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
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 = (b -> m) -> p -> m
(b -> m) -> f b -> m
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((b -> m) -> p -> m)
-> ((Pattern' (ADotT b) -> m -> m) -> b -> m)
-> (Pattern' (ADotT b) -> m -> m)
-> p
-> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern' (ADotT b) -> m -> m) -> b -> m
forall m. Monoid m => (Pattern' (ADotT b) -> m -> m) -> b -> m
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 = (q -> m q) -> f q -> m (f q)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((q -> m q) -> f q -> m (f q)) -> (q -> m q) -> f q -> m (f q)
forall a b. (a -> b) -> a -> b
$ (Pattern' (ADotT q) -> m (Pattern' (ADotT q)))
-> (Pattern' (ADotT q) -> m (Pattern' (ADotT q))) -> q -> m q
forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
forall (m :: * -> *).
Monad m =>
(Pattern' (ADotT q) -> m (Pattern' (ADotT q)))
-> (Pattern' (ADotT q) -> m (Pattern' (ADotT q))) -> q -> m q
traverseAPatternM Pattern' (ADotT p) -> m (Pattern' (ADotT p))
Pattern' (ADotT q) -> m (Pattern' (ADotT q))
pre Pattern' (ADotT p) -> m (Pattern' (ADotT p))
Pattern' (ADotT q) -> m (Pattern' (ADotT q))
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 = (Pattern' (ADotT p) -> m -> m) -> p -> m
forall m. Monoid m => (Pattern' (ADotT p) -> m -> m) -> p -> m
forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern ((Pattern' (ADotT p) -> m -> m) -> p -> m)
-> (Pattern' (ADotT p) -> m -> m) -> p -> m
forall a b. (a -> b) -> a -> b
$ \ Pattern' (ADotT p)
p m
m -> Pattern' (ADotT p) -> m
f Pattern' (ADotT p)
p m -> m -> m
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 = (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m 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
forall (m :: * -> *).
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))
forall a. a -> m a
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 = (Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m 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
forall (m :: * -> *).
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))
forall a. a -> m a
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 = Identity p -> p
forall a. Identity a -> a
runIdentity (Identity p -> p) -> (p -> Identity p) -> p -> p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern' (ADotT p) -> Identity (Pattern' (ADotT p)))
-> p -> Identity p
forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
postTraverseAPatternM (Pattern' (ADotT p) -> Identity (Pattern' (ADotT p))
forall a. a -> Identity a
Identity (Pattern' (ADotT p) -> Identity (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> Pattern' (ADotT p))
-> Pattern' (ADotT p)
-> Identity (Pattern' (ADotT p))
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
Pattern' (ADotT (Pattern' a))
p (m -> m) -> m -> m
forall a b. (a -> b) -> a -> b
$
    case Pattern' a
p of
      AsP PatInfo
_ BindName
_ Pattern' a
p          -> (Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m
forall m.
Monoid m =>
(Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m
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        -> (Pattern' (ADotT (NAPs a)) -> m -> m) -> NAPs a -> m
forall m.
Monoid m =>
(Pattern' (ADotT (NAPs a)) -> m -> m) -> NAPs a -> m
forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT (NAPs a)) -> m -> m
Pattern' (ADotT (Pattern' a)) -> m -> m
f NAPs a
ps
      DefP PatInfo
_ AmbiguousQName
_ NAPs a
ps        -> (Pattern' (ADotT (NAPs a)) -> m -> m) -> NAPs a -> m
forall m.
Monoid m =>
(Pattern' (ADotT (NAPs a)) -> m -> m) -> NAPs a -> m
forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT (NAPs a)) -> m -> m
Pattern' (ADotT (Pattern' a)) -> m -> m
f NAPs a
ps
      RecP ConPatInfo
_ [FieldAssignment' (Pattern' a)]
ps          -> (Pattern' (ADotT [FieldAssignment' (Pattern' a)]) -> m -> m)
-> [FieldAssignment' (Pattern' a)] -> m
forall m.
Monoid m =>
(Pattern' (ADotT [FieldAssignment' (Pattern' a)]) -> m -> m)
-> [FieldAssignment' (Pattern' a)] -> m
forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT [FieldAssignment' (Pattern' a)]) -> m -> m
Pattern' (ADotT (Pattern' a)) -> m -> m
f [FieldAssignment' (Pattern' a)]
ps
      PatternSynP PatInfo
_ AmbiguousQName
_ NAPs a
ps -> (Pattern' (ADotT (NAPs a)) -> m -> m) -> NAPs a -> m
forall m.
Monoid m =>
(Pattern' (ADotT (NAPs a)) -> m -> m) -> NAPs a -> m
forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT (NAPs a)) -> m -> m
Pattern' (ADotT (Pattern' a)) -> m -> m
f NAPs a
ps
      WithP PatInfo
_ Pattern' a
p          -> (Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m
forall m.
Monoid m =>
(Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m
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
_             -> m
forall a. Monoid a => a
mempty
      ProjP PatInfo
_ ProjOrigin
_ AmbiguousQName
_        -> m
forall a. Monoid a => a
mempty
      WildP PatInfo
_            -> m
forall a. Monoid a => a
mempty
      DotP PatInfo
_ a
_           -> m
forall a. Monoid a => a
mempty
      AbsurdP PatInfo
_          -> m
forall a. Monoid a => a
mempty
      LitP PatInfo
_ Literal
_           -> m
forall a. Monoid a => a
mempty
      EqualP PatInfo
_ List1 (a, a)
_         -> m
forall a. Monoid a => a
mempty

  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' a -> m (Pattern' a)
Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Pattern' a -> m (Pattern' a)
recurse (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Pattern' a -> m (Pattern' a)
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{}            -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      p :: Pattern' a
p@A.WildP{}           -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      p :: Pattern' a
p@A.DotP{}            -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      p :: Pattern' a
p@A.LitP{}            -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      p :: Pattern' a
p@A.AbsurdP{}         -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      p :: Pattern' a
p@A.ProjP{}           -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      p :: Pattern' a
p@A.EqualP{}          -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      -- Recursive cases:
      A.ConP        ConPatInfo
i AmbiguousQName
ds NAPs a
ps -> ConPatInfo -> AmbiguousQName -> NAPs a -> Pattern' a
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP        ConPatInfo
i AmbiguousQName
ds (NAPs a -> Pattern' a) -> m (NAPs a) -> m (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
-> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
-> NAPs a
-> m (NAPs a)
forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
forall (m :: * -> *).
Monad m =>
(Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
-> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
-> NAPs a
-> m (NAPs a)
traverseAPatternM Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a)))
Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a)))
Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post NAPs a
ps
      A.DefP        PatInfo
i AmbiguousQName
q  NAPs a
ps -> PatInfo -> AmbiguousQName -> NAPs a -> Pattern' a
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP        PatInfo
i AmbiguousQName
q  (NAPs a -> Pattern' a) -> m (NAPs a) -> m (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
-> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
-> NAPs a
-> m (NAPs a)
forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
forall (m :: * -> *).
Monad m =>
(Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
-> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
-> NAPs a
-> m (NAPs a)
traverseAPatternM Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a)))
Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a)))
Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post NAPs a
ps
      A.AsP         PatInfo
i BindName
x  Pattern' a
p  -> PatInfo -> BindName -> Pattern' a -> Pattern' a
forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP         PatInfo
i BindName
x  (Pattern' a -> Pattern' a) -> m (Pattern' a) -> m (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern' (ADotT (Pattern' a))
 -> m (Pattern' (ADotT (Pattern' a))))
-> (Pattern' (ADotT (Pattern' a))
    -> m (Pattern' (ADotT (Pattern' a))))
-> Pattern' a
-> m (Pattern' a)
forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
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' a
p
      A.RecP        ConPatInfo
i    [FieldAssignment' (Pattern' a)]
ps -> ConPatInfo -> [FieldAssignment' (Pattern' a)] -> Pattern' a
forall e.
ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP        ConPatInfo
i    ([FieldAssignment' (Pattern' a)] -> Pattern' a)
-> m [FieldAssignment' (Pattern' a)] -> m (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern' (ADotT [FieldAssignment' (Pattern' a)])
 -> m (Pattern' (ADotT [FieldAssignment' (Pattern' a)])))
-> (Pattern' (ADotT [FieldAssignment' (Pattern' a)])
    -> m (Pattern' (ADotT [FieldAssignment' (Pattern' a)])))
-> [FieldAssignment' (Pattern' a)]
-> m [FieldAssignment' (Pattern' a)]
forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
forall (m :: * -> *).
Monad m =>
(Pattern' (ADotT [FieldAssignment' (Pattern' a)])
 -> m (Pattern' (ADotT [FieldAssignment' (Pattern' a)])))
-> (Pattern' (ADotT [FieldAssignment' (Pattern' a)])
    -> m (Pattern' (ADotT [FieldAssignment' (Pattern' a)])))
-> [FieldAssignment' (Pattern' a)]
-> m [FieldAssignment' (Pattern' a)]
traverseAPatternM Pattern' (ADotT [FieldAssignment' (Pattern' a)])
-> m (Pattern' (ADotT [FieldAssignment' (Pattern' a)]))
Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre Pattern' (ADotT [FieldAssignment' (Pattern' a)])
-> m (Pattern' (ADotT [FieldAssignment' (Pattern' a)]))
Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post [FieldAssignment' (Pattern' a)]
ps
      A.PatternSynP PatInfo
i AmbiguousQName
x  NAPs a
ps -> PatInfo -> AmbiguousQName -> NAPs a -> Pattern' a
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.PatternSynP PatInfo
i AmbiguousQName
x  (NAPs a -> Pattern' a) -> m (NAPs a) -> m (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
-> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
-> NAPs a
-> m (NAPs a)
forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
forall (m :: * -> *).
Monad m =>
(Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
-> (Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a))))
-> NAPs a
-> m (NAPs a)
traverseAPatternM Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a)))
Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
pre Pattern' (ADotT (NAPs a)) -> m (Pattern' (ADotT (NAPs a)))
Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))
post NAPs a
ps
      A.WithP       PatInfo
i Pattern' a
p     -> PatInfo -> Pattern' a -> Pattern' a
forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP       PatInfo
i    (Pattern' a -> Pattern' a) -> m (Pattern' a) -> m (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern' (ADotT (Pattern' a))
 -> m (Pattern' (ADotT (Pattern' a))))
-> (Pattern' (ADotT (Pattern' a))
    -> m (Pattern' (ADotT (Pattern' a))))
-> Pattern' a
-> m (Pattern' a)
forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
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' 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') =
    (Pattern' (ADotT a) -> m -> m) -> a -> m
forall m. Monoid m => (Pattern' (ADotT a) -> m -> m) -> a -> m
forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT a) -> m -> m
Pattern' (ADotT (a, b)) -> m -> m
f a
p m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (Pattern' (ADotT b) -> m -> m) -> b -> m
forall m. Monoid m => (Pattern' (ADotT b) -> m -> m) -> b -> m
forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
foldrAPattern Pattern' (ADotT b) -> m -> m
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') =
    (a -> b -> (a, b)) -> m a -> m b -> m (a, b)
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,)
      ((Pattern' (ADotT a) -> m (Pattern' (ADotT a)))
-> (Pattern' (ADotT a) -> m (Pattern' (ADotT a))) -> a -> m a
forall p (m :: * -> *).
(APatternLike p, Monad m) =>
(Pattern' (ADotT p) -> m (Pattern' (ADotT p)))
-> (Pattern' (ADotT p) -> m (Pattern' (ADotT p))) -> p -> m p
forall (m :: * -> *).
Monad m =>
(Pattern' (ADotT a) -> m (Pattern' (ADotT a)))
-> (Pattern' (ADotT a) -> m (Pattern' (ADotT a))) -> a -> m a
traverseAPatternM Pattern' (ADotT a) -> m (Pattern' (ADotT a))
Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
pre Pattern' (ADotT a) -> m (Pattern' (ADotT a))
Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
post a
p)
      ((Pattern' (ADotT b) -> m (Pattern' (ADotT b)))
-> (Pattern' (ADotT b) -> m (Pattern' (ADotT b))) -> b -> m 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
forall (m :: * -> *).
Monad m =>
(Pattern' (ADotT b) -> m (Pattern' (ADotT b)))
-> (Pattern' (ADotT b) -> m (Pattern' (ADotT b))) -> b -> m b
traverseAPatternM Pattern' (ADotT b) -> m (Pattern' (ADotT b))
Pattern' (ADotT (a, b)) -> m (Pattern' (ADotT (a, b)))
pre Pattern' (ADotT b) -> m (Pattern' (ADotT b))
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 = (Pattern' (ADotT p) -> Endo [Name]) -> p -> Endo [Name]
forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m) -> p -> m
foldAPattern Pattern' (ADotT p) -> Endo [Name]
forall a. Pattern' a -> Endo [Name]
f p
p Endo [Name] -> [Name] -> [Name]
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         -> ([Name] -> [Name]) -> Endo [Name]
forall a. (a -> a) -> Endo a
Endo (BindName -> Name
unBind BindName
x Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:)
    A.AsP PatInfo
_ BindName
x Pattern' a
_      -> ([Name] -> [Name]) -> Endo [Name]
forall a. (a -> a) -> Endo a
Endo (BindName -> Name
unBind BindName
x Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:)
    A.LitP        {} -> Endo [Name]
forall a. Monoid a => a
mempty
    A.ConP        {} -> Endo [Name]
forall a. Monoid a => a
mempty
    A.RecP        {} -> Endo [Name]
forall a. Monoid a => a
mempty
    A.DefP        {} -> Endo [Name]
forall a. Monoid a => a
mempty
    A.ProjP       {} -> Endo [Name]
forall a. Monoid a => a
mempty
    A.WildP       {} -> Endo [Name]
forall a. Monoid a => a
mempty
    A.DotP        {} -> Endo [Name]
forall a. Monoid a => a
mempty
    A.AbsurdP     {} -> Endo [Name]
forall a. Monoid a => a
mempty
    A.EqualP      {} -> Endo [Name]
forall a. Monoid a => a
mempty
    A.PatternSynP {} -> Endo [Name]
forall a. Monoid a => a
mempty
    A.WithP PatInfo
_ Pattern' a
_      -> Endo [Name]
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 (Any -> Bool) -> (p -> Any) -> p -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern' (ADotT p) -> Any) -> p -> Any
forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m) -> p -> m
foldAPattern (Bool -> Any
Any (Bool -> Any)
-> (Pattern' (ADotT p) -> Bool) -> Pattern' (ADotT p) -> 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 = (Pattern' (ADotT p) -> Bool) -> p -> Bool
forall p.
APatternLike p =>
(Pattern' (ADotT p) -> Bool) -> p -> Bool
containsAPattern ((Pattern' (ADotT p) -> Bool) -> p -> Bool)
-> (Pattern' (ADotT p) -> Bool) -> p -> Bool
forall a b. (a -> b) -> a -> b
$ \case
    A.PatternSynP{} -> Bool
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 = (Pattern' (ADotT p) -> Bool) -> p -> Bool
forall p.
APatternLike p =>
(Pattern' (ADotT p) -> Bool) -> p -> Bool
containsAPattern ((Pattern' (ADotT p) -> Bool) -> p -> Bool)
-> (Pattern' (ADotT p) -> Bool) -> p -> Bool
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 -> (List1 C.Name -> m ()) -> m ()
checkPatternLinearity :: forall (m :: * -> *) p.
(Monad m, APatternLike p) =>
p -> (List1 Name -> m ()) -> m ()
checkPatternLinearity =
  [Name] -> (List1 Name -> m ()) -> m ()
forall (m :: * -> *) a.
Applicative m =>
[a] -> (List1 a -> m ()) -> m ()
List1.unlessNull ([Name] -> (List1 Name -> m ()) -> m ())
-> (p -> [Name]) -> p -> (List1 Name -> m ()) -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> [Name]
forall a. Ord a => [a] -> [a]
duplicates ([Name] -> [Name]) -> (p -> [Name]) -> p -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
nameConcrete ([Name] -> [Name]) -> (p -> [Name]) -> p -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p -> [Name]
forall p. APatternLike p => p -> [Name]
patternVars


-- * 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' Expr)] -> Pattern' Expr -> Pattern' Expr
substPattern [(Name, Pattern' Expr)]
s = (Expr -> Expr)
-> [(Name, Pattern' Expr)] -> Pattern' Expr -> Pattern' Expr
forall e.
(e -> e) -> [(Name, Pattern' e)] -> Pattern' e -> Pattern' e
substPattern' ([(Name, Expr)] -> Expr -> Expr
forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr ([(Name, Expr)] -> Expr -> Expr) -> [(Name, Expr)] -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ ((Name, Pattern' Expr) -> (Name, Expr))
-> [(Name, Pattern' Expr)] -> [(Name, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern' Expr -> Expr) -> (Name, Pattern' Expr) -> (Name, Expr)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Pattern' Expr -> Expr
patternToExpr) [(Name, Pattern' Expr)]
s) [(Name, Pattern' Expr)]
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 = (Pattern' (ADotT (Pattern' e)) -> Pattern' (ADotT (Pattern' e)))
-> Pattern' e -> Pattern' e
forall p.
APatternLike p =>
(Pattern' (ADotT p) -> Pattern' (ADotT p)) -> p -> p
mapAPattern ((Pattern' (ADotT (Pattern' e)) -> Pattern' (ADotT (Pattern' e)))
 -> Pattern' e -> Pattern' e)
-> (Pattern' (ADotT (Pattern' e)) -> Pattern' (ADotT (Pattern' e)))
-> Pattern' e
-> Pattern' e
forall a b. (a -> b) -> a -> b
$ \ Pattern' (ADotT (Pattern' e))
p -> case Pattern' (ADotT (Pattern' e))
p of
  VarP BindName
x            -> Pattern' (ADotT (Pattern' e))
-> Maybe (Pattern' (ADotT (Pattern' e)))
-> Pattern' (ADotT (Pattern' e))
forall a. a -> Maybe a -> a
fromMaybe Pattern' (ADotT (Pattern' e))
p (Maybe (Pattern' (ADotT (Pattern' e)))
 -> Pattern' (ADotT (Pattern' e)))
-> Maybe (Pattern' (ADotT (Pattern' e)))
-> Pattern' (ADotT (Pattern' e))
forall a b. (a -> b) -> a -> b
$ Name -> [(Name, Pattern' e)] -> Maybe (Pattern' e)
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          -> PatInfo -> e -> Pattern' e
forall e. PatInfo -> e -> Pattern' e
DotP PatInfo
i (e -> Pattern' e) -> e -> Pattern' e
forall a b. (a -> b) -> a -> b
$ e -> e
subE e
ADotT (Pattern' e)
e
  EqualP PatInfo
i List1 (ADotT (Pattern' e), ADotT (Pattern' e))
es       -> PatInfo
-> List1 (ADotT (Pattern' e), ADotT (Pattern' e))
-> Pattern' (ADotT (Pattern' e))
forall e. PatInfo -> List1 (e, e) -> Pattern' e
EqualP PatInfo
i (List1 (ADotT (Pattern' e), ADotT (Pattern' e))
 -> Pattern' (ADotT (Pattern' e)))
-> List1 (ADotT (Pattern' e), ADotT (Pattern' e))
-> Pattern' (ADotT (Pattern' e))
forall a b. (a -> b) -> a -> b
$ ((e, e) -> (e, e)) -> NonEmpty (e, e) -> NonEmpty (e, e)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (e -> e
subE (e -> e) -> (e -> e) -> (e, e) -> (e, e)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** e -> e
subE) NonEmpty (e, e)
List1 (ADotT (Pattern' e), ADotT (Pattern' e))
es
  -- No action on the other patterns (besides the recursion):
  ConP ConPatInfo
_ AmbiguousQName
_ NAPs (ADotT (Pattern' e))
_        -> Pattern' (ADotT (Pattern' e))
p
  RecP ConPatInfo
_ [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

-- | Convert a pattern to an expression.
--
-- Does not support all cases of patterns.
-- Result has no 'Range' info, except in identifiers.
--
-- This function is only used in expanding pattern synonyms
-- and in "Agda.Syntax.Translation.InternalToAbstract",
-- so we can cut some corners.
patternToExpr :: Pattern -> Expr
patternToExpr :: Pattern' Expr -> Expr
patternToExpr Pattern' Expr
p = Pattern' Expr -> Reader Hiding Expr
forall p e. PatternToExpr p e => p -> Reader Hiding e
patToExpr Pattern' Expr
p Reader Hiding Expr -> Hiding -> Expr
forall r a. Reader r a -> r -> a
`runReader` Hiding
forall a. Null a => a
empty

-- | Converting a pattern to an expression.
--
--   The 'Hiding' context is remembered to create instance metas
--   when translating absurd patterns in instance position.
--
class PatternToExpr p e where
  patToExpr :: p -> Reader Hiding e

  default patToExpr :: (Traversable t, PatternToExpr p' e', p ~ t p', e ~ t e')
    => p -> Reader Hiding e
  patToExpr = (p' -> ReaderT Hiding Identity e')
-> t p' -> ReaderT Hiding Identity (t e')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b)
traverse p' -> ReaderT Hiding Identity e'
forall p e. PatternToExpr p e => p -> Reader Hiding e
patToExpr

instance PatternToExpr p e => PatternToExpr [p] [e]
instance PatternToExpr p e => PatternToExpr (Named n p) (Named n e)
instance PatternToExpr p e => PatternToExpr (FieldAssignment' p) (FieldAssignment' e)

instance PatternToExpr p e => PatternToExpr (Arg p) (Arg e) where
  patToExpr :: Arg p -> Reader Hiding (Arg e)
patToExpr (Arg ArgInfo
ai p
p) = (Hiding -> Hiding)
-> Reader Hiding (Arg e) -> Reader Hiding (Arg e)
forall a.
(Hiding -> Hiding)
-> ReaderT Hiding Identity a -> ReaderT Hiding Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Hiding -> Hiding -> Hiding
forall a b. a -> b -> a
const (Hiding -> Hiding -> Hiding) -> Hiding -> Hiding -> Hiding
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai) (Reader Hiding (Arg e) -> Reader Hiding (Arg e))
-> Reader Hiding (Arg e) -> Reader Hiding (Arg e)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> e -> Arg e
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (e -> Arg e) -> ReaderT Hiding Identity e -> Reader Hiding (Arg e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> p -> ReaderT Hiding Identity e
forall p e. PatternToExpr p e => p -> Reader Hiding e
patToExpr p
p

instance PatternToExpr Pattern Expr where
  patToExpr :: Pattern' Expr -> Reader Hiding Expr
patToExpr = \case
    VarP BindName
x             -> Expr -> Reader Hiding Expr
forall a. a -> ReaderT Hiding Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Reader Hiding Expr) -> Expr -> Reader Hiding Expr
forall a b. (a -> b) -> a -> b
$ Name -> Expr
Var (BindName -> Name
unBind BindName
x)
    ConP ConPatInfo
_ AmbiguousQName
c NAPs Expr
ps        -> Expr -> [NamedArg Expr] -> Expr
app (AmbiguousQName -> Expr
Con AmbiguousQName
c) ([NamedArg Expr] -> Expr)
-> ReaderT Hiding Identity [NamedArg Expr] -> Reader Hiding Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NAPs Expr -> ReaderT Hiding Identity [NamedArg Expr]
forall p e. PatternToExpr p e => p -> Reader Hiding e
patToExpr NAPs Expr
ps
    ProjP PatInfo
_ ProjOrigin
o AmbiguousQName
ds       -> Expr -> Reader Hiding Expr
forall a. a -> ReaderT Hiding Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Reader Hiding Expr) -> Expr -> Reader Hiding Expr
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> AmbiguousQName -> Expr
Proj ProjOrigin
o AmbiguousQName
ds
    DefP PatInfo
_ AmbiguousQName
fs NAPs Expr
ps       -> Expr -> [NamedArg Expr] -> Expr
app (QName -> Expr
Def (QName -> Expr) -> QName -> Expr
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
headAmbQ AmbiguousQName
fs) ([NamedArg Expr] -> Expr)
-> ReaderT Hiding Identity [NamedArg Expr] -> Reader Hiding Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NAPs Expr -> ReaderT Hiding Identity [NamedArg Expr]
forall p e. PatternToExpr p e => p -> Reader Hiding e
patToExpr NAPs Expr
ps
    WildP PatInfo
_            -> Expr -> Reader Hiding Expr
forall a. a -> ReaderT Hiding Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Reader Hiding Expr) -> Expr -> Reader Hiding Expr
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Expr
Underscore MetaInfo
emptyMetaInfo
    AsP PatInfo
_ BindName
_ Pattern' Expr
p          -> Pattern' Expr -> Reader Hiding Expr
forall p e. PatternToExpr p e => p -> Reader Hiding e
patToExpr Pattern' Expr
p
    DotP PatInfo
_ Expr
e           -> Expr -> Reader Hiding Expr
forall a. a -> ReaderT Hiding Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
    -- Issue #7176: An absurd pattern in an instance position should turn into an instance meta:
    AbsurdP PatInfo
_          -> (Hiding -> MetaKind) -> ReaderT Hiding Identity MetaKind
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Hiding -> MetaKind
hidingToMetaKind ReaderT Hiding Identity MetaKind
-> (MetaKind -> Expr) -> Reader Hiding Expr
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ MetaKind
k -> MetaInfo -> Expr
Underscore MetaInfo
emptyMetaInfo{ metaKind = k }
    LitP PatInfo
_ Literal
l           -> Expr -> Reader Hiding Expr
forall a. a -> ReaderT Hiding Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Reader Hiding Expr) -> Expr -> Reader Hiding Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Literal -> Expr
Lit ExprInfo
forall a. Null a => a
empty Literal
l
    PatternSynP PatInfo
_ AmbiguousQName
c NAPs Expr
ps -> Expr -> [NamedArg Expr] -> Expr
app (AmbiguousQName -> Expr
PatternSyn AmbiguousQName
c) ([NamedArg Expr] -> Expr)
-> ReaderT Hiding Identity [NamedArg Expr] -> Reader Hiding Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NAPs Expr -> ReaderT Hiding Identity [NamedArg Expr]
forall p e. PatternToExpr p e => p -> Reader Hiding e
patToExpr NAPs Expr
ps
    RecP ConPatInfo
i [FieldAssignment' (Pattern' Expr)]
as          -> RecInfo -> RecordAssigns -> Expr
Rec (Range -> RecInfo
recInfoBrace (Range -> RecInfo) -> Range -> RecInfo
forall a b. (a -> b) -> a -> b
$ ConPatInfo -> Range
forall a. HasRange a => a -> Range
getRange ConPatInfo
i) (RecordAssigns -> Expr)
-> ([Assign] -> RecordAssigns) -> [Assign] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Assign -> RecordAssign) -> [Assign] -> RecordAssigns
forall a b. (a -> b) -> [a] -> [b]
map Assign -> RecordAssign
forall a b. a -> Either a b
Left ([Assign] -> Expr)
-> ReaderT Hiding Identity [Assign] -> Reader Hiding Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldAssignment' (Pattern' Expr)]
-> ReaderT Hiding Identity [Assign]
forall p e. PatternToExpr p e => p -> Reader Hiding e
patToExpr [FieldAssignment' (Pattern' Expr)]
as
    EqualP{}           -> Reader Hiding Expr
forall a. HasCallStack => a
__IMPOSSIBLE__  -- Andrea TODO: where is this used?
    WithP PatInfo
r Pattern' Expr
p          -> Reader Hiding Expr
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Make sure that there are no dot or equality patterns (called on pattern synonyms).
--   Also disallows annotated patterns.
--
noDotOrEqPattern :: forall m e. Monad m
  => m (A.Pattern' Void)   -- ^ Exception or replacement for dot (etc.) patterns.
  -> A.Pattern' e          -- ^ In pattern.
  -> m (A.Pattern' Void)   -- ^ Out pattern.
noDotOrEqPattern :: forall (m :: * -> *) e.
Monad m =>
m (Pattern' Void) -> Pattern' e -> m (Pattern' Void)
noDotOrEqPattern m (Pattern' Void)
err = Pattern' e -> m (Pattern' Void)
dot
  where
    dot :: A.Pattern' e -> m (A.Pattern' Void)
    dot :: Pattern' e -> m (Pattern' Void)
dot = \case
      A.VarP BindName
x               -> Pattern' Void -> m (Pattern' Void)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern' Void -> m (Pattern' Void))
-> Pattern' Void -> m (Pattern' Void)
forall a b. (a -> b) -> a -> b
$ BindName -> Pattern' Void
forall e. BindName -> Pattern' e
A.VarP BindName
x
      A.ConP ConPatInfo
i AmbiguousQName
c NAPs e
args        -> ConPatInfo -> AmbiguousQName -> NAPs Void -> Pattern' Void
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
i AmbiguousQName
c (NAPs Void -> Pattern' Void) -> m (NAPs Void) -> m (Pattern' Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
-> NAPs e -> m (NAPs Void)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
 -> NAPs e -> m (NAPs Void))
-> (NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
-> NAPs e
-> m (NAPs Void)
forall a b. (a -> b) -> a -> b
$ (Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
-> NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse ((Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
 -> NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
-> (Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
-> NamedArg (Pattern' e)
-> m (NamedArg (Pattern' Void))
forall a b. (a -> b) -> a -> b
$ (Pattern' e -> m (Pattern' Void))
-> Named_ (Pattern' e) -> m (Named_ (Pattern' Void))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Named NamedName a -> f (Named NamedName b)
traverse Pattern' e -> m (Pattern' Void)
dot) NAPs e
args
      A.ProjP PatInfo
i ProjOrigin
o AmbiguousQName
d          -> Pattern' Void -> m (Pattern' Void)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern' Void -> m (Pattern' Void))
-> Pattern' Void -> m (Pattern' Void)
forall a b. (a -> b) -> a -> b
$ PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' Void
forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
A.ProjP PatInfo
i ProjOrigin
o AmbiguousQName
d
      A.WildP PatInfo
i              -> Pattern' Void -> m (Pattern' Void)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern' Void -> m (Pattern' Void))
-> Pattern' Void -> m (Pattern' Void)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Void
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
i
      A.AsP PatInfo
i BindName
x Pattern' e
p            -> PatInfo -> BindName -> Pattern' Void -> Pattern' Void
forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP PatInfo
i BindName
x (Pattern' Void -> Pattern' Void)
-> m (Pattern' Void) -> m (Pattern' Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern' e -> m (Pattern' Void)
dot Pattern' e
p
      A.DotP{}               -> m (Pattern' Void)
err
      A.EqualP{}             -> m (Pattern' Void)
err   -- Andrea: so we also disallow = patterns, reasonable?
      A.AbsurdP PatInfo
i            -> Pattern' Void -> m (Pattern' Void)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern' Void -> m (Pattern' Void))
-> Pattern' Void -> m (Pattern' Void)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Void
forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
i
      A.LitP PatInfo
i Literal
l             -> Pattern' Void -> m (Pattern' Void)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern' Void -> m (Pattern' Void))
-> Pattern' Void -> m (Pattern' Void)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Literal -> Pattern' Void
forall e. PatInfo -> Literal -> Pattern' e
A.LitP PatInfo
i Literal
l
      A.DefP PatInfo
i AmbiguousQName
f NAPs e
args        -> PatInfo -> AmbiguousQName -> NAPs Void -> Pattern' Void
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP PatInfo
i AmbiguousQName
f (NAPs Void -> Pattern' Void) -> m (NAPs Void) -> m (Pattern' Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
-> NAPs e -> m (NAPs Void)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
 -> NAPs e -> m (NAPs Void))
-> (NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
-> NAPs e
-> m (NAPs Void)
forall a b. (a -> b) -> a -> b
$ (Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
-> NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse ((Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
 -> NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
-> (Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
-> NamedArg (Pattern' e)
-> m (NamedArg (Pattern' Void))
forall a b. (a -> b) -> a -> b
$ (Pattern' e -> m (Pattern' Void))
-> Named_ (Pattern' e) -> m (Named_ (Pattern' Void))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Named NamedName a -> f (Named NamedName b)
traverse Pattern' e -> m (Pattern' Void)
dot) NAPs e
args
      A.PatternSynP PatInfo
i AmbiguousQName
c NAPs e
args -> PatInfo -> AmbiguousQName -> NAPs Void -> Pattern' Void
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.PatternSynP PatInfo
i AmbiguousQName
c (NAPs Void -> Pattern' Void) -> m (NAPs Void) -> m (Pattern' Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
-> NAPs e -> m (NAPs Void)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
 -> NAPs e -> m (NAPs Void))
-> (NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
-> NAPs e
-> m (NAPs Void)
forall a b. (a -> b) -> a -> b
$ (Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
-> NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse ((Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
 -> NamedArg (Pattern' e) -> m (NamedArg (Pattern' Void)))
-> (Named_ (Pattern' e) -> m (Named_ (Pattern' Void)))
-> NamedArg (Pattern' e)
-> m (NamedArg (Pattern' Void))
forall a b. (a -> b) -> a -> b
$ (Pattern' e -> m (Pattern' Void))
-> Named_ (Pattern' e) -> m (Named_ (Pattern' Void))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Named NamedName a -> f (Named NamedName b)
traverse Pattern' e -> m (Pattern' Void)
dot) NAPs e
args
      A.RecP ConPatInfo
i [FieldAssignment' (Pattern' e)]
fs            -> ConPatInfo -> [FieldAssignment' (Pattern' Void)] -> Pattern' Void
forall e.
ConPatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP ConPatInfo
i ([FieldAssignment' (Pattern' Void)] -> Pattern' Void)
-> m [FieldAssignment' (Pattern' Void)] -> m (Pattern' Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((FieldAssignment' (Pattern' e)
 -> m (FieldAssignment' (Pattern' Void)))
-> [FieldAssignment' (Pattern' e)]
-> m [FieldAssignment' (Pattern' Void)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((FieldAssignment' (Pattern' e)
  -> m (FieldAssignment' (Pattern' Void)))
 -> [FieldAssignment' (Pattern' e)]
 -> m [FieldAssignment' (Pattern' Void)])
-> (FieldAssignment' (Pattern' e)
    -> m (FieldAssignment' (Pattern' Void)))
-> [FieldAssignment' (Pattern' e)]
-> m [FieldAssignment' (Pattern' Void)]
forall a b. (a -> b) -> a -> b
$ (Pattern' e -> m (Pattern' Void))
-> FieldAssignment' (Pattern' e)
-> m (FieldAssignment' (Pattern' Void))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)
traverse Pattern' e -> m (Pattern' Void)
dot) [FieldAssignment' (Pattern' e)]
fs
      A.WithP PatInfo
i Pattern' e
p            -> PatInfo -> Pattern' Void -> Pattern' Void
forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP PatInfo
i (Pattern' Void -> Pattern' Void)
-> m (Pattern' Void) -> m (Pattern' Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern' e -> m (Pattern' Void)
dot 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 -> Pattern' e -> Maybe (Pattern' e)
forall a. a -> Maybe a
Just Pattern' e
p
    Pattern' e
_ -> Maybe (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 = (NamedArg (Pattern' Expr) -> Bool)
-> NAPs Expr -> (NAPs Expr, NAPs Expr)
forall a. (a -> Bool) -> [a] -> ([a], [a])
spanEnd (Maybe (NamedArg (Pattern' Expr)) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (NamedArg (Pattern' Expr)) -> Bool)
-> (NamedArg (Pattern' Expr) -> Maybe (NamedArg (Pattern' Expr)))
-> NamedArg (Pattern' Expr)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' Expr) -> Maybe (NamedArg (Pattern' Expr))
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 = (NAPs Expr, NAPs Expr) -> NAPs Expr
forall a b. (a, b) -> b
snd ((NAPs Expr, NAPs Expr) -> NAPs Expr)
-> (NAPs Expr -> (NAPs Expr, NAPs Expr)) -> NAPs Expr -> NAPs Expr
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  (NAPs1 e)
      -- ^ Application patterns (non-empty list).
  | LHSProjP ProjOrigin AmbiguousQName (NamedArg (Pattern' e))
      -- ^ A projection pattern.  Is also stored unmodified here.
  | LHSWithP (List1 (Pattern' e))
      -- ^ With patterns (non-empty list).
      --   These patterns are not prefixed with 'WithP'.
  deriving (Int -> LHSPatternView e -> ShowS
[LHSPatternView e] -> ShowS
LHSPatternView e -> String
(Int -> LHSPatternView e -> ShowS)
-> (LHSPatternView e -> String)
-> ([LHSPatternView e] -> ShowS)
-> Show (LHSPatternView e)
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
$cshowsPrec :: forall e. Show e => Int -> LHSPatternView e -> ShowS
showsPrec :: Int -> LHSPatternView e -> ShowS
$cshow :: forall e. Show e => LHSPatternView e -> String
show :: LHSPatternView e -> String
$cshowList :: forall e. Show e => [LHSPatternView e] -> ShowS
showList :: [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 [] = Maybe (LHSPatternView e, [NamedArg (Pattern' e)])
forall a. Maybe a
Nothing
lhsPatternView (NamedArg (Pattern' e)
p0 : [NamedArg (Pattern' e)]
ps) =
  case NamedArg (Pattern' e) -> Pattern' e
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' e)
p0 of
    ProjP PatInfo
_i ProjOrigin
o AmbiguousQName
d -> (LHSPatternView e, [NamedArg (Pattern' e)])
-> Maybe (LHSPatternView e, [NamedArg (Pattern' e)])
forall a. a -> Maybe a
Just (ProjOrigin
-> AmbiguousQName -> NamedArg (Pattern' e) -> LHSPatternView e
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   -> (LHSPatternView e, [NamedArg (Pattern' e)])
-> Maybe (LHSPatternView e, [NamedArg (Pattern' e)])
forall a. a -> Maybe a
Just (List1 (Pattern' e) -> LHSPatternView e
forall e. List1 (Pattern' e) -> LHSPatternView e
LHSWithP (Pattern' e
p Pattern' e -> [Pattern' e] -> List1 (Pattern' e)
forall a. a -> [a] -> NonEmpty a
:| (NamedArg (Pattern' e) -> Pattern' e)
-> [NamedArg (Pattern' e)] -> [Pattern' e]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg (Pattern' e) -> Pattern' e
forall a. NamedArg a -> a
namedArg [NamedArg (Pattern' e)]
ps1), [NamedArg (Pattern' e)]
ps2)
      where
      ([NamedArg (Pattern' e)]
ps1, [NamedArg (Pattern' e)]
ps2) = (NamedArg (Pattern' e) -> Maybe (NamedArg (Pattern' e)))
-> [NamedArg (Pattern' e)]
-> ([NamedArg (Pattern' e)], [NamedArg (Pattern' e)])
forall a b. (a -> Maybe b) -> [a] -> (Prefix b, [a])
spanJust NamedArg (Pattern' e) -> Maybe (NamedArg (Pattern' e))
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
_ -> (LHSPatternView e, [NamedArg (Pattern' e)])
-> Maybe (LHSPatternView e, [NamedArg (Pattern' e)])
forall a. a -> Maybe a
Just (NAPs1 e -> LHSPatternView e
forall e. NAPs1 e -> LHSPatternView e
LHSAppP (NamedArg (Pattern' e)
p0 NamedArg (Pattern' e) -> [NamedArg (Pattern' e)] -> NAPs1 e
forall a. a -> [a] -> NonEmpty a
:| [NamedArg (Pattern' e)]
ps1), [NamedArg (Pattern' e)]
ps2)
      where
      ([NamedArg (Pattern' e)]
ps1, [NamedArg (Pattern' e)]
ps2) = (NamedArg (Pattern' e) -> Bool)
-> [NamedArg (Pattern' e)]
-> ([NamedArg (Pattern' e)], [NamedArg (Pattern' e)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\ NamedArg (Pattern' e)
p -> Maybe (ProjOrigin, AmbiguousQName) -> Bool
forall a. Maybe a -> Bool
isNothing (NamedArg (Pattern' e) -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP NamedArg (Pattern' e)
p) Bool -> Bool -> Bool
&& Maybe (NamedArg (Pattern' e)) -> Bool
forall a. Maybe a -> Bool
isNothing (NamedArg (Pattern' e) -> Maybe (NamedArg (Pattern' e))
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 = (LHS -> SpineLHS) -> Clause -> SpineClause
forall a b. (a -> b) -> Clause' a -> Clause' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHS -> SpineLHS
forall a b. LHSToSpine a b => a -> b
lhsToSpine
  spineToLhs :: SpineClause -> Clause
spineToLhs = (SpineLHS -> LHS) -> SpineClause -> Clause
forall a b. (a -> b) -> Clause' a -> Clause' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpineLHS -> LHS
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 = (a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
forall a b. LHSToSpine a b => a -> b
lhsToSpine
  spineToLhs :: [b] -> [a]
spineToLhs = (b -> a) -> [b] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map b -> a
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 = LHSCore -> QNamed (NAPs Expr)
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 (QNamed (NAPs Expr) -> LHSCore
forall e. IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e
spineToLhsCore (QNamed (NAPs Expr) -> LHSCore) -> QNamed (NAPs Expr) -> LHSCore
forall a b. (a -> b) -> a -> b
$ QName -> NAPs Expr -> QNamed (NAPs Expr)
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     -> QName -> [NamedArg (Pattern' e)] -> QNamed [NamedArg (Pattern' e)]
forall a. QName -> a -> QNamed a
QNamed QName
f [NamedArg (Pattern' e)]
ps
  LHSProj AmbiguousQName
d NamedArg (LHSCore' e)
h [NamedArg (Pattern' e)]
ps   -> LHSCore' e -> QNamed [NamedArg (Pattern' e)]
forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
lhsCoreToSpine (NamedArg (LHSCore' e) -> LHSCore' e
forall a. NamedArg a -> a
namedArg NamedArg (LHSCore' e)
h) QNamed [NamedArg (Pattern' e)]
-> ([NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)])
-> QNamed [NamedArg (Pattern' e)]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> ([NamedArg (Pattern' e)]
-> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
forall a. [a] -> [a] -> [a]
++ (NamedArg (Pattern' e)
p NamedArg (Pattern' e)
-> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
forall a. a -> [a] -> [a]
: [NamedArg (Pattern' e)]
ps))
    where p :: NamedArg (Pattern' e)
p = (LHSCore' e -> Pattern' e)
-> NamedArg (LHSCore' e) -> NamedArg (Pattern' e)
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (Pattern' e -> LHSCore' e -> Pattern' e
forall a b. a -> b -> a
const (Pattern' e -> LHSCore' e -> Pattern' e)
-> Pattern' e -> LHSCore' e -> Pattern' e
forall a b. (a -> b) -> a -> b
$ PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
ProjP PatInfo
forall a. Null a => a
empty ProjOrigin
ProjPrefix AmbiguousQName
d) NamedArg (LHSCore' e)
h
  LHSWith LHSCore' e
h List1 (Arg (Pattern' e))
wps [NamedArg (Pattern' e)]
ps -> LHSCore' e -> QNamed [NamedArg (Pattern' e)]
forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
lhsCoreToSpine LHSCore' e
h QNamed [NamedArg (Pattern' e)]
-> ([NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)])
-> QNamed [NamedArg (Pattern' e)]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> ([NamedArg (Pattern' e)]
-> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
forall a. [a] -> [a] -> [a]
++ (Arg (Pattern' e) -> NamedArg (Pattern' e))
-> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)]
forall a b. (a -> b) -> [a] -> [b]
map Arg (Pattern' e) -> NamedArg (Pattern' e)
forall e. Arg (Pattern' e) -> NamedArg (Pattern' e)
fromWithPat (List1 (Arg (Pattern' e)) -> [Item (List1 (Arg (Pattern' e)))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (Arg (Pattern' e))
wps) [NamedArg (Pattern' e)]
-> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
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 = (Pattern' e -> Named_ (Pattern' e))
-> Arg (Pattern' e) -> Arg (Named_ (Pattern' e))
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pattern' e -> Named_ (Pattern' e)
forall a name. a -> Named name a
unnamed (Pattern' e -> Named_ (Pattern' e))
-> (Pattern' e -> Pattern' e) -> Pattern' e -> Named_ (Pattern' e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern' e -> Pattern' e
forall {e}. Pattern' e -> Pattern' e
mkWithP)
      mkWithP :: Pattern' e -> Pattern' e
mkWithP Pattern' e
p   = PatInfo -> Pattern' e -> Pattern' e
forall e. PatInfo -> Pattern' e -> Pattern' e
WithP (Range -> PatInfo
PatRange (Range -> PatInfo) -> Range -> PatInfo
forall a b. (a -> b) -> a -> b
$ Pattern' e -> Range
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) = LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
forall e.
IsProjP e =>
LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreAddSpine (QName -> [NamedArg (Pattern' e)] -> LHSCore' e
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 = lhsPats core ++ ps }

-- | Add with-patterns to the right.
lhsCoreWith :: LHSCore' e -> List1 (Arg (Pattern' e)) -> LHSCore' e
lhsCoreWith :: forall e. LHSCore' e -> List1 (Arg (Pattern' e)) -> LHSCore' e
lhsCoreWith (LHSWith LHSCore' e
core List1 (Arg (Pattern' e))
wps []) List1 (Arg (Pattern' e))
wps' = LHSCore' e
-> List1 (Arg (Pattern' e))
-> [NamedArg (Pattern' e)]
-> LHSCore' e
forall e.
LHSCore' e
-> List1 (Arg (Pattern' e))
-> [NamedArg (Pattern' e)]
-> LHSCore' e
LHSWith LHSCore' e
core (List1 (Arg (Pattern' e))
wps List1 (Arg (Pattern' e))
-> List1 (Arg (Pattern' e)) -> List1 (Arg (Pattern' e))
forall a. Semigroup a => a -> a -> a
<> List1 (Arg (Pattern' e))
wps') []
lhsCoreWith LHSCore' e
core                  List1 (Arg (Pattern' e))
wps' = LHSCore' e
-> List1 (Arg (Pattern' e))
-> [NamedArg (Pattern' e)]
-> LHSCore' e
forall e.
LHSCore' e
-> List1 (Arg (Pattern' e))
-> [NamedArg (Pattern' e)]
-> LHSCore' e
LHSWith LHSCore' e
core List1 (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 NAPs1 e
ps               -> LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
forall e. LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreApp LHSCore' e
core ([NamedArg (Pattern' e)] -> LHSCore' e)
-> [NamedArg (Pattern' e)] -> LHSCore' e
forall a b. (a -> b) -> a -> b
$ NAPs1 e -> [Item (NAPs1 e)]
forall l. IsList l => l -> [Item l]
List1.toList NAPs1 e
ps
  LHSWithP List1 (Pattern' e)
wps             -> LHSCore' e -> List1 (Arg (Pattern' e)) -> LHSCore' e
forall e. LHSCore' e -> List1 (Arg (Pattern' e)) -> LHSCore' e
lhsCoreWith LHSCore' e
core (Pattern' e -> Arg (Pattern' e)
forall a. a -> Arg a
defaultArg (Pattern' e -> Arg (Pattern' e))
-> List1 (Pattern' e) -> List1 (Arg (Pattern' e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 (Pattern' e)
wps)
  LHSProjP ProjOrigin
ProjPrefix AmbiguousQName
d NamedArg (Pattern' e)
np -> AmbiguousQName
-> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
forall e.
AmbiguousQName
-> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSProj AmbiguousQName
d (NamedArg (Pattern' e) -> LHSCore' e -> NamedArg (LHSCore' e)
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 -> LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
forall e. LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreApp LHSCore' e
core (NamedArg (Pattern' e) -> [NamedArg (Pattern' e)]
forall el coll. Singleton el coll => el -> coll
singleton 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 [NamedArg (Pattern' e)]
-> Maybe (LHSPatternView e, [NamedArg (Pattern' e)])
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') -> LHSCore' e -> LHSPatternView e -> LHSCore' e
forall e. IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e
lhsCoreAddChunk LHSCore' e
core LHSPatternView e
chunk LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
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 = AmbiguousQName -> Int
forall a. NumHoles a => a -> Int
C.numHoles AmbiguousQName
d, Int
nh Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0, Int
nh Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [NamedArg (Pattern' e)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg (Pattern' e)]
ps'
          -> ProjOrigin
-> AmbiguousQName -> NamedArg (Pattern' e) -> LHSPatternView e
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 = (NamedArg (Pattern' e) -> Pattern' e)
-> [NamedArg (Pattern' e)] -> [Pattern' e]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg (Pattern' e) -> Pattern' e
forall a. NamedArg a -> a
namedArg ([NamedArg (Pattern' e)] -> [Pattern' e])
-> (LHSCore' e -> [NamedArg (Pattern' e)])
-> LHSCore' e
-> [Pattern' e]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QNamed [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
forall a. QNamed a -> a
qnamed (QNamed [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)])
-> (LHSCore' e -> QNamed [NamedArg (Pattern' e)])
-> LHSCore' e
-> [NamedArg (Pattern' e)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
forall e. LHSCore' e -> QNamed [NamedArg (Pattern' e)]
lhsCoreToSpine

-- | Used in ''Agda.Syntax.Translation.AbstractToConcrete''.
--   Returns a 'DefP'.
lhsCoreToPattern :: LHSCore -> Pattern
lhsCoreToPattern :: LHSCore -> Pattern' Expr
lhsCoreToPattern LHSCore
lc =
  case LHSCore
lc of
    LHSHead QName
f NAPs Expr
aps         -> PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern' Expr
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 -> PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern' Expr
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP PatInfo
noInfo AmbiguousQName
d (NAPs Expr -> Pattern' Expr) -> NAPs Expr -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$
      (Named NamedName LHSCore -> Named NamedName (Pattern' Expr))
-> NamedArg LHSCore -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LHSCore -> Pattern' Expr)
-> Named NamedName LHSCore -> Named NamedName (Pattern' Expr)
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHSCore -> Pattern' Expr
lhsCoreToPattern) NamedArg LHSCore
lhscore NamedArg (Pattern' Expr) -> NAPs Expr -> NAPs Expr
forall a. a -> [a] -> [a]
: NAPs Expr
aps
    LHSWith LHSCore
h List1 (Arg (Pattern' Expr))
wps NAPs Expr
aps     -> case LHSCore -> Pattern' Expr
lhsCoreToPattern LHSCore
h of
      DefP PatInfo
r AmbiguousQName
q NAPs Expr
ps         -> PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern' Expr
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP PatInfo
r AmbiguousQName
q (NAPs Expr -> Pattern' Expr) -> NAPs Expr -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ NAPs Expr
ps NAPs Expr -> NAPs Expr -> NAPs Expr
forall a. [a] -> [a] -> [a]
++ (Arg (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> [Arg (Pattern' Expr)] -> NAPs Expr
forall a b. (a -> b) -> [a] -> [b]
map Arg (Pattern' Expr) -> NamedArg (Pattern' Expr)
fromWithPat (List1 (Arg (Pattern' Expr)) -> [Item (List1 (Arg (Pattern' Expr)))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (Arg (Pattern' Expr))
wps) NAPs Expr -> NAPs Expr -> NAPs Expr
forall a. [a] -> [a] -> [a]
++ NAPs Expr
aps
        where
          fromWithPat :: Arg Pattern -> NamedArg Pattern
          fromWithPat :: Arg (Pattern' Expr) -> NamedArg (Pattern' Expr)
fromWithPat = (Pattern' Expr -> Named NamedName (Pattern' Expr))
-> Arg (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pattern' Expr -> Named NamedName (Pattern' Expr)
forall a name. a -> Named name a
unnamed (Pattern' Expr -> Named NamedName (Pattern' Expr))
-> (Pattern' Expr -> Pattern' Expr)
-> Pattern' Expr
-> Named NamedName (Pattern' Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern' Expr -> Pattern' Expr
forall {e}. Pattern' e -> Pattern' e
mkWithP)
          mkWithP :: Pattern' e -> Pattern' e
mkWithP Pattern' e
p   = PatInfo -> Pattern' e -> Pattern' e
forall e. PatInfo -> Pattern' e -> Pattern' e
WithP (Range -> PatInfo
PatRange (Range -> PatInfo) -> Range -> PatInfo
forall a b. (a -> b) -> a -> b
$ Pattern' e -> Range
forall a. HasRange a => a -> Range
getRange Pattern' e
p) Pattern' e
p
      Pattern' Expr
_ -> Pattern' Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
  where noInfo :: PatInfo
noInfo = PatInfo
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   -> AmbiguousQName -> NamedArg LHSCore -> NAPs Expr -> LHSCore
forall e.
AmbiguousQName
-> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSProj AmbiguousQName
d ((Named NamedName LHSCore -> Named NamedName LHSCore)
-> NamedArg LHSCore -> NamedArg LHSCore
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LHSCore -> LHSCore)
-> Named NamedName LHSCore -> Named NamedName LHSCore
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
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 List1 (Arg (Pattern' Expr))
wps NAPs Expr
ps -> LHSCore -> List1 (Arg (Pattern' Expr)) -> NAPs Expr -> LHSCore
forall e.
LHSCore' e
-> List1 (Arg (Pattern' e))
-> [NamedArg (Pattern' e)]
-> LHSCore' e
LHSWith ((QName -> NAPs Expr -> LHSCore) -> LHSCore -> LHSCore
mapLHSHead QName -> NAPs Expr -> LHSCore
f LHSCore
h) List1 (Arg (Pattern' Expr))
wps NAPs Expr
ps