{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE UndecidableInstances      #-}

-- | 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
import Control.Applicative (liftA2)

import Data.Foldable (Foldable, foldMap)
import Data.Traversable (Traversable, traverse)

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

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

-- | Generic pattern traversal.

class APatternLike a p | p -> a where

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

  default foldrAPattern
    :: (Monoid m, Foldable f, APatternLike a b, f b ~ p)
    => (Pattern' a -> m -> m) -> p -> m
  foldrAPattern = (b -> m) -> f b -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((b -> m) -> f b -> m)
-> ((Pattern' a -> m -> m) -> b -> m)
-> (Pattern' a -> m -> m)
-> f b
-> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern' a -> m -> m) -> b -> m
forall a p m.
(APatternLike a p, Monoid m) =>
(Pattern' a -> m -> m) -> p -> m
foldrAPattern

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

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

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

foldAPattern :: (APatternLike a p, Monoid m) => (Pattern' a -> m) -> p -> m
foldAPattern :: (Pattern' a -> m) -> p -> m
foldAPattern Pattern' a -> m
f = (Pattern' a -> m -> m) -> p -> m
forall a p m.
(APatternLike a p, Monoid m) =>
(Pattern' a -> m -> m) -> p -> m
foldrAPattern ((Pattern' a -> m -> m) -> p -> m)
-> (Pattern' a -> m -> m) -> p -> m
forall a b. (a -> b) -> a -> b
$ \ Pattern' a
p m
m -> Pattern' a -> m
f Pattern' a
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 a b, Monad m )
  => (Pattern' a -> m (Pattern' a))  -- ^ @pre@: Modification before recursion.
  -> b -> m b
preTraverseAPatternM :: (Pattern' a -> m (Pattern' a)) -> b -> m b
preTraverseAPatternM Pattern' a -> m (Pattern' a)
pre b
p = (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
forall a p (m :: * -> *).
(APatternLike a p, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> p -> m p
traverseAPatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return b
p

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

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

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

mapAPattern :: APatternLike a p => (Pattern' a -> Pattern' a) -> p -> p
mapAPattern :: (Pattern' a -> Pattern' a) -> p -> p
mapAPattern Pattern' a -> Pattern' a
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' a -> Identity (Pattern' a)) -> p -> Identity p
forall a b (m :: * -> *).
(APatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
postTraverseAPatternM (Pattern' a -> Identity (Pattern' a)
forall a. a -> Identity a
Identity (Pattern' a -> Identity (Pattern' a))
-> (Pattern' a -> Pattern' a)
-> Pattern' a
-> Identity (Pattern' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern' a -> Pattern' a
f)

-- Interesting instance:

instance APatternLike a (Pattern' a) where
  foldrAPattern :: (Pattern' a -> m -> m) -> Pattern' a -> m
foldrAPattern Pattern' a -> m -> m
f Pattern' a
p = Pattern' a -> m -> m
f 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' a -> m -> m) -> Pattern' a -> m
forall a p m.
(APatternLike a p, Monoid m) =>
(Pattern' a -> m -> m) -> p -> m
foldrAPattern Pattern' a -> m -> m
f Pattern' a
p
      ConP ConPatInfo
_ AmbiguousQName
_ NAPs a
ps        -> (Pattern' a -> m -> m) -> NAPs a -> m
forall a p m.
(APatternLike a p, Monoid m) =>
(Pattern' a -> m -> m) -> p -> m
foldrAPattern Pattern' a -> m -> m
f NAPs a
ps
      DefP PatInfo
_ AmbiguousQName
_ NAPs a
ps        -> (Pattern' a -> m -> m) -> NAPs a -> m
forall a p m.
(APatternLike a p, Monoid m) =>
(Pattern' a -> m -> m) -> p -> m
foldrAPattern Pattern' a -> m -> m
f NAPs a
ps
      RecP PatInfo
_ [FieldAssignment' (Pattern' a)]
ps          -> (Pattern' a -> m -> m) -> [FieldAssignment' (Pattern' a)] -> m
forall a p m.
(APatternLike a p, Monoid m) =>
(Pattern' a -> m -> m) -> p -> m
foldrAPattern Pattern' a -> m -> m
f [FieldAssignment' (Pattern' a)]
ps
      PatternSynP PatInfo
_ AmbiguousQName
_ NAPs a
ps -> (Pattern' a -> m -> m) -> NAPs a -> m
forall a p m.
(APatternLike a p, Monoid m) =>
(Pattern' a -> m -> m) -> p -> m
foldrAPattern Pattern' a -> m -> m
f NAPs a
ps
      WithP PatInfo
_ Pattern' a
p          -> (Pattern' a -> m -> m) -> Pattern' a -> m
forall a p m.
(APatternLike a p, Monoid m) =>
(Pattern' a -> m -> m) -> p -> m
foldrAPattern 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 Literal
_             -> m
forall a. Monoid a => a
mempty
      EqualP PatInfo
_ [(a, a)]
_         -> m
forall a. Monoid a => a
mempty

  traverseAPatternM :: (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
traverseAPatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post = Pattern' a -> m (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)
post
    where
    recurse :: Pattern' a -> m (Pattern' a)
recurse Pattern' a
p = case Pattern' a
p of
      -- Non-recursive cases:
      A.VarP{}             -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      A.WildP{}            -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      A.DotP{}             -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      A.LitP{}             -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      A.AbsurdP{}          -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      A.ProjP{}            -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      A.EqualP{}           -> Pattern' a -> m (Pattern' 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' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> NAPs a -> m (NAPs a)
forall a p (m :: * -> *).
(APatternLike a p, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> p -> m p
traverseAPatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (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' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> NAPs a -> m (NAPs a)
forall a p (m :: * -> *).
(APatternLike a p, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> p -> m p
traverseAPatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (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' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall a p (m :: * -> *).
(APatternLike a p, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> p -> m p
traverseAPatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post Pattern' a
p
      A.RecP        PatInfo
i    [FieldAssignment' (Pattern' a)]
ps -> PatInfo -> [FieldAssignment' (Pattern' a)] -> Pattern' a
forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP        PatInfo
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' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a))
-> [FieldAssignment' (Pattern' a)]
-> m [FieldAssignment' (Pattern' a)]
forall a p (m :: * -> *).
(APatternLike a p, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> p -> m p
traverseAPatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (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' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> NAPs a -> m (NAPs a)
forall a p (m :: * -> *).
(APatternLike a p, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> p -> m p
traverseAPatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (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' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall a p (m :: * -> *).
(APatternLike a p, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> p -> m p
traverseAPatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post Pattern' a
p

-- The following instances need UndecidableInstances
-- for the FunctionalDependency (since injectivity is not taken into account).

instance APatternLike a b => APatternLike a (Arg b)              where
instance APatternLike a b => APatternLike a (Named n b)          where
instance APatternLike a b => APatternLike a [b]                  where
instance APatternLike a b => APatternLike a (Maybe b)            where
instance APatternLike a b => APatternLike a (FieldAssignment' b) where

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

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


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

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

patternVars :: forall a p. APatternLike a p => p -> [A.Name]
patternVars :: p -> [Name]
patternVars p
p = (Pattern' a -> Endo [Name]) -> p -> Endo [Name]
forall a p m.
(APatternLike a p, Monoid m) =>
(Pattern' a -> m) -> p -> m
foldAPattern 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 :: 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 a p => (Pattern' a -> Bool) -> p -> Bool
containsAPattern :: (Pattern' a -> Bool) -> p -> Bool
containsAPattern Pattern' a -> Bool
f = Any -> Bool
getAny (Any -> Bool) -> (p -> Any) -> p -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern' a -> Any) -> p -> Any
forall a p m.
(APatternLike a p, Monoid m) =>
(Pattern' a -> m) -> p -> m
foldAPattern (Bool -> Any
Any (Bool -> Any) -> (Pattern' a -> Bool) -> Pattern' a -> Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern' a -> Bool
f)

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

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

-- | Check if a pattern contains an @-pattern.
--
--   Precondition: contains no pattern synonyms.

containsAsPattern :: APatternLike a p => p -> Bool
containsAsPattern :: p -> Bool
containsAsPattern = (Pattern' a -> Bool) -> p -> Bool
forall a p. APatternLike a p => (Pattern' a -> Bool) -> p -> Bool
containsAPattern ((Pattern' a -> Bool) -> p -> Bool)
-> (Pattern' a -> Bool) -> p -> Bool
forall a b. (a -> b) -> a -> b
$ \case
    A.PatternSynP{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
    A.AsP{}         -> Bool
True
    Pattern' a
_               -> 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 a p)
                      => p -> ([C.Name] -> m ()) -> m ()
checkPatternLinearity :: p -> ([Name] -> m ()) -> m ()
checkPatternLinearity p
ps [Name] -> m ()
err =
  [Name] -> ([Name] -> m ()) -> m ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull ([Name] -> [Name]
forall a. Ord a => [a] -> [a]
duplicates ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
nameConcrete ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ p -> [Name]
forall a p. APatternLike a p => p -> [Name]
patternVars p
ps) (([Name] -> m ()) -> m ()) -> ([Name] -> m ()) -> m ()
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 = (Expr -> Expr) -> [(Name, Pattern)] -> Pattern -> Pattern
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) -> (Name, Expr))
-> [(Name, Pattern)] -> [(Name, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern -> Expr) -> (Name, Pattern) -> (Name, Expr)
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' :: (e -> e) -> [(Name, Pattern' e)] -> Pattern' e -> Pattern' e
substPattern' e -> e
subE [(Name, Pattern' e)]
s = (Pattern' e -> Pattern' e) -> Pattern' e -> Pattern' e
forall a p.
APatternLike a p =>
(Pattern' a -> Pattern' a) -> p -> p
mapAPattern ((Pattern' e -> Pattern' e) -> Pattern' e -> Pattern' e)
-> (Pattern' e -> Pattern' e) -> Pattern' e -> Pattern' e
forall a b. (a -> b) -> a -> b
$ \ Pattern' e
p -> case Pattern' e
p of
  VarP BindName
x            -> Pattern' e -> Maybe (Pattern' e) -> Pattern' e
forall a. a -> Maybe a -> a
fromMaybe Pattern' e
p (Maybe (Pattern' e) -> Pattern' e)
-> Maybe (Pattern' e) -> 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 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
e
  EqualP PatInfo
i [(e, e)]
es       -> PatInfo -> [(e, e)] -> Pattern' e
forall e. PatInfo -> [(e, e)] -> Pattern' e
EqualP PatInfo
i ([(e, e)] -> Pattern' e) -> [(e, e)] -> Pattern' e
forall a b. (a -> b) -> a -> b
$ ((e, e) -> (e, e)) -> [(e, e)] -> [(e, e)]
forall a b. (a -> b) -> [a] -> [b]
map (e -> e
subE (e -> e) -> (e -> e) -> (e, e) -> (e, e)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** e -> e
subE) [(e, e)]
es
  -- No action on the other patterns (besides the recursion):
  ConP ConPatInfo
_ AmbiguousQName
_ NAPs e
_        -> Pattern' e
p
  RecP PatInfo
_ [FieldAssignment' (Pattern' e)]
_          -> Pattern' e
p
  ProjP PatInfo
_ ProjOrigin
_ AmbiguousQName
_       -> Pattern' e
p
  WildP PatInfo
_           -> Pattern' e
p
  AbsurdP PatInfo
_         -> Pattern' e
p
  LitP Literal
_            -> Pattern' e
p
  DefP PatInfo
_ AmbiguousQName
_ NAPs e
_        -> Pattern' e
p
  AsP PatInfo
_ BindName
_ Pattern' e
_         -> Pattern' e
p -- Note: cannot substitute into as-variable
  PatternSynP PatInfo
_ AmbiguousQName
_ NAPs e
_ -> Pattern' e
p
  WithP PatInfo
_ Pattern' e
_         -> 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 = (NAP -> Bool) -> NAPs Expr -> (NAPs Expr, NAPs Expr)
forall a. (a -> Bool) -> [a] -> ([a], [a])
spanEnd (Maybe NAP -> Bool
forall a. Maybe a -> Bool
isJust (Maybe NAP -> Bool) -> (NAP -> Maybe NAP) -> NAP -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NAP -> Maybe NAP
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  (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
[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
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 :: NAPs e -> Maybe (LHSPatternView e, NAPs e)
lhsPatternView [] = Maybe (LHSPatternView e, NAPs e)
forall a. Maybe a
Nothing
lhsPatternView (NamedArg (Pattern' e)
p0 : NAPs 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, NAPs e) -> Maybe (LHSPatternView e, NAPs 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, NAPs e
ps)
    -- If the next pattern is a with-pattern, collect more with-patterns
    WithP PatInfo
_i Pattern' e
p   -> (LHSPatternView e, NAPs e) -> Maybe (LHSPatternView e, NAPs e)
forall a. a -> Maybe a
Just ([Pattern' e] -> LHSPatternView e
forall e. [Pattern' e] -> LHSPatternView e
LHSWithP (Pattern' e
p Pattern' e -> [Pattern' e] -> [Pattern' e]
forall a. a -> [a] -> [a]
: (NamedArg (Pattern' e) -> Pattern' e) -> NAPs e -> [Pattern' e]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg (Pattern' e) -> Pattern' e
forall a. NamedArg a -> a
namedArg NAPs e
ps1), NAPs e
ps2)
      where
      (NAPs e
ps1, NAPs e
ps2) = (NamedArg (Pattern' e) -> Maybe (NamedArg (Pattern' e)))
-> NAPs e -> (NAPs e, NAPs 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 NAPs e
ps
    -- If the next pattern is an application pattern, collect more of these
    Pattern' e
_ -> (LHSPatternView e, NAPs e) -> Maybe (LHSPatternView e, NAPs e)
forall a. a -> Maybe a
Just (NAPs e -> LHSPatternView e
forall e. NAPs e -> LHSPatternView e
LHSAppP (NamedArg (Pattern' e)
p0 NamedArg (Pattern' e) -> NAPs e -> NAPs e
forall a. a -> [a] -> [a]
: NAPs e
ps1), NAPs e
ps2)
      where
      (NAPs e
ps1, NAPs e
ps2) = (NamedArg (Pattern' e) -> Bool) -> NAPs e -> (NAPs e, NAPs 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)) NAPs 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 (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 (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 :: 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 [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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> ([NamedArg (Pattern' e)]
-> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
forall a. [a] -> [a] -> [a]
++ (Pattern' e -> NamedArg (Pattern' e))
-> [Pattern' e] -> [NamedArg (Pattern' e)]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern' e -> NamedArg (Pattern' e)
forall a. a -> NamedArg a
defaultNamedArg (Pattern' e -> NamedArg (Pattern' e))
-> (Pattern' e -> Pattern' e)
-> Pattern' e
-> NamedArg (Pattern' e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern' e -> Pattern' e
forall e. Pattern' e -> Pattern' e
mkWithP) [Pattern' e]
wps [NamedArg (Pattern' e)]
-> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
forall a. [a] -> [a] -> [a]
++ [NamedArg (Pattern' e)]
ps)
    where 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 t. HasRange t => t -> Range
getRange Pattern' e
p) Pattern' e
p

spineToLhsCore :: IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e
spineToLhsCore :: 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 :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreApp LHSCore' e
core [NamedArg (Pattern' e)]
ps = LHSCore' e
core { lhsPats :: [NamedArg (Pattern' e)]
lhsPats = LHSCore' e -> [NamedArg (Pattern' e)]
forall e. LHSCore' e -> [NamedArg (Pattern' e)]
lhsPats LHSCore' e
core [NamedArg (Pattern' e)]
-> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
forall a. [a] -> [a] -> [a]
++ [NamedArg (Pattern' e)]
ps }

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

lhsCoreAddChunk :: IsProjP e => LHSCore' e -> LHSPatternView e -> LHSCore' e
lhsCoreAddChunk :: LHSCore' e -> LHSPatternView e -> LHSCore' e
lhsCoreAddChunk LHSCore' e
core = \case
  LHSAppP NAPs e
ps               -> LHSCore' e -> NAPs e -> LHSCore' e
forall e. LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreApp LHSCore' e
core NAPs e
ps
  LHSWithP [Pattern' e]
wps             -> LHSCore' e -> [Pattern' e] -> LHSCore' e
forall e. LHSCore' e -> [Pattern' e] -> LHSCore' e
lhsCoreWith LHSCore' e
core [Pattern' e]
wps
  LHSProjP ProjOrigin
ProjPrefix AmbiguousQName
d NamedArg (Pattern' e)
np -> AmbiguousQName -> NamedArg (LHSCore' e) -> NAPs 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 -> NAPs e -> LHSCore' e
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 :: 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 (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 :: 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
lhsCoreToPattern LHSCore
lc =
  case LHSCore
lc of
    LHSHead QName
f NAPs Expr
aps         -> PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
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
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP PatInfo
noInfo AmbiguousQName
d (NAPs Expr -> Pattern) -> NAPs Expr -> Pattern
forall a b. (a -> b) -> a -> b
$
      (Named NamedName LHSCore -> Named NamedName Pattern)
-> NamedArg LHSCore -> NAP
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LHSCore -> Pattern)
-> Named NamedName LHSCore -> Named NamedName Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHSCore -> Pattern
lhsCoreToPattern) NamedArg LHSCore
lhscore NAP -> NAPs Expr -> NAPs Expr
forall a. a -> [a] -> [a]
: NAPs Expr
aps
    LHSWith LHSCore
h [Pattern]
wps NAPs Expr
aps     -> case LHSCore -> Pattern
lhsCoreToPattern LHSCore
h of
      DefP PatInfo
r AmbiguousQName
q NAPs Expr
ps         -> PatInfo -> AmbiguousQName -> NAPs Expr -> Pattern
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP PatInfo
r AmbiguousQName
q (NAPs Expr -> Pattern) -> NAPs Expr -> Pattern
forall a b. (a -> b) -> a -> b
$ NAPs Expr
ps NAPs Expr -> NAPs Expr -> NAPs Expr
forall a. [a] -> [a] -> [a]
++ (Pattern -> NAP) -> [Pattern] -> NAPs Expr
forall a b. (a -> b) -> [a] -> [b]
map (\ Pattern
p -> Pattern -> NAP
forall a. a -> NamedArg a
defaultNamedArg (Pattern -> NAP) -> Pattern -> NAP
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern -> Pattern
forall e. PatInfo -> Pattern' e -> Pattern' e
WithP (Range -> PatInfo
PatRange (Range -> PatInfo) -> Range -> PatInfo
forall a b. (a -> b) -> a -> b
$ Pattern -> Range
forall t. HasRange t => t -> Range
getRange Pattern
p) Pattern
p) [Pattern]
wps NAPs Expr -> NAPs Expr -> NAPs Expr
forall a. [a] -> [a] -> [a]
++ NAPs Expr
aps
      Pattern
_ -> Pattern
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LHSCore -> LHSCore)
-> Named NamedName LHSCore -> Named NamedName LHSCore
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 [Pattern]
wps NAPs Expr
ps -> LHSCore -> [Pattern] -> NAPs Expr -> LHSCore
forall e.
LHSCore' e -> [Pattern' e] -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSWith ((QName -> NAPs Expr -> LHSCore) -> LHSCore -> LHSCore
mapLHSHead QName -> NAPs Expr -> LHSCore
f LHSCore
h) [Pattern]
wps NAPs Expr
ps