module Agda.Syntax.Internal.Pattern where

import Control.Arrow       ( second )
import Control.Monad       ( (>=>), forM )
import Control.Monad.State ( MonadState(..), State, evalState )

import Data.Maybe
import Data.Monoid
import qualified Data.List as List

import Agda.Syntax.Common
import Agda.Syntax.Internal

import Agda.Utils.List
import Agda.Utils.Permutation
import Agda.Utils.Size (size)

import Agda.Utils.Impossible

-- * Tools for clauses

-- | Translate the clause patterns to terms with free variables bound by the
--   clause telescope.
--
--   Precondition: no projection patterns.
clauseArgs :: Clause -> Args
clauseArgs :: Clause -> Args
clauseArgs Clause
cl = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims forall a b. (a -> b) -> a -> b
$ Clause -> Elims
clauseElims Clause
cl

-- | Translate the clause patterns to an elimination spine
--   with free variables bound by the clause telescope.
clauseElims :: Clause -> Elims
clauseElims :: Clause -> Elims
clauseElims Clause
cl = [NamedArg DeBruijnPattern] -> Elims
patternsToElims forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl

-- | Arity of a function, computed from clauses.
class FunArity a where
  funArity :: a -> Int

-- | Get the number of initial 'Apply' patterns.

instance {-# OVERLAPPABLE #-} IsProjP p => FunArity [p] where
  funArity :: [p] -> Int
funArity = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP)

-- | Get the number of initial 'Apply' patterns in a clause.
instance FunArity Clause where
  funArity :: Clause -> Int
funArity = forall a. FunArity a => a -> Int
funArity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [NamedArg DeBruijnPattern]
namedClausePats

-- | Get the number of common initial 'Apply' patterns in a list of clauses.
instance {-# OVERLAPPING #-} FunArity [Clause] where
  funArity :: [Clause] -> Int
funArity []  = Int
0
  funArity [Clause]
cls = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. FunArity a => a -> Int
funArity [Clause]
cls

-- * Tools for patterns

-- | Label the pattern variables from left to right
--   using one label for each variable pattern and one for each dot pattern.
class LabelPatVars a b where
  type PatVarLabel b
  labelPatVars :: a -> State [PatVarLabel b] b
  unlabelPatVars :: b -> a
  -- ^ Intended, but unpractical due to the absence of type-level lambda, is:
  --   @labelPatVars :: f (Pattern' x) -> State [i] (f (Pattern' (i,x)))@

  default labelPatVars
    :: (Traversable f
      , LabelPatVars a' b'
      , PatVarLabel b ~  PatVarLabel b'
      , f a' ~ a, f b' ~ b)
    => a -> State [PatVarLabel b] b
  labelPatVars = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b. LabelPatVars a b => a -> State [PatVarLabel b] b
labelPatVars

  default unlabelPatVars
    :: (Traversable f, LabelPatVars a' b', f a' ~ a, f b' ~ b)
    => b -> a
  unlabelPatVars = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. LabelPatVars a b => b -> a
unlabelPatVars

instance LabelPatVars a b => LabelPatVars (Arg a) (Arg b) where
  type PatVarLabel (Arg b) = PatVarLabel b

instance LabelPatVars a b => LabelPatVars (Named x a) (Named x b) where
  type PatVarLabel (Named x b) = PatVarLabel b

instance LabelPatVars a b => LabelPatVars [a] [b] where
  type PatVarLabel [b] = PatVarLabel b

instance LabelPatVars Pattern DeBruijnPattern where
  type PatVarLabel DeBruijnPattern = Int

  labelPatVars :: Pattern -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern
labelPatVars = \case
    VarP PatternInfo
o PatVarName
x        -> forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatVarName -> Int -> DBPatVar
DBPatVar PatVarName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT [Int] Identity Int
next
    DotP PatternInfo
o Term
t        -> forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o Term
t forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT [Int] Identity Int
next
    ConP ConHead
c ConPatternInfo
mt [NamedArg Pattern]
ps    -> forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
mt forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. LabelPatVars a b => a -> State [PatVarLabel b] b
labelPatVars [NamedArg Pattern]
ps
    DefP PatternInfo
o QName
q  [NamedArg Pattern]
ps    -> forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. LabelPatVars a b => a -> State [PatVarLabel b] b
labelPatVars [NamedArg Pattern]
ps
    LitP  PatternInfo
o Literal
l       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
o Literal
l
    ProjP ProjOrigin
o QName
q       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
o QName
q
    IApplyP PatternInfo
o Term
u Term
t PatVarName
x -> forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o Term
u Term
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatVarName -> Int -> DBPatVar
DBPatVar PatVarName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT [Int] Identity Int
next
   where
    next :: StateT [Int] Identity Int
next = forall (m :: * -> *) a b.
Monad m =>
m [a] -> m b -> (a -> [a] -> m b) -> m b
caseListM forall s (m :: * -> *). MonadState s m => m s
get forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ \Int
x [Int]
xs -> do
      forall s (m :: * -> *). MonadState s m => s -> m ()
put [Int]
xs
      forall (m :: * -> *) a. Monad m => a -> m a
return Int
x
  unlabelPatVars :: DeBruijnPattern -> Pattern
unlabelPatVars = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DBPatVar -> PatVarName
dbPatVarName

-- | Augment pattern variables with their de Bruijn index.
{-# SPECIALIZE numberPatVars :: Int -> Permutation -> [NamedArg Pattern] -> [NamedArg DeBruijnPattern] #-}
--
--  Example:
--  @
--    f : (A : Set) (n : Nat) (v : Vec A n) -> ...
--    f A .(suc n) (cons n x xs)
--
--    clauseTel = (A : Set) (n : Nat) (x : A) (xs : Vec A n)
--    perm      = Perm 5 [0,2,3,4]
--    invertP __IMPOSSIBLE__ perm = Perm 4 [0,__IMPOSSIBLE__,1,2,3]
--    flipP ... = Perm 4 [3,__IMPOSSIBLE__,2,1,0]
--    pats      = A .(suc 2) (cons n x xs)
--    dBpats    = 3 .(suc 2) (cons 2 1 0 )
--  @
--
numberPatVars :: (LabelPatVars a b, PatVarLabel b ~ Int) => Int -> Permutation -> a -> b
numberPatVars :: forall a b.
(LabelPatVars a b, PatVarLabel b ~ Int) =>
Int -> Permutation -> a -> b
numberPatVars Int
err Permutation
perm a
ps = forall s a. State s a -> s -> a
evalState (forall a b. LabelPatVars a b => a -> State [PatVarLabel b] b
labelPatVars a
ps) forall a b. (a -> b) -> a -> b
$
  Permutation -> [Int]
permPicks forall a b. (a -> b) -> a -> b
$ Permutation -> Permutation
flipP forall a b. (a -> b) -> a -> b
$ Int -> Permutation -> Permutation
invertP Int
err Permutation
perm

unnumberPatVars :: LabelPatVars a b => b -> a
unnumberPatVars :: forall a b. LabelPatVars a b => b -> a
unnumberPatVars = forall a b. LabelPatVars a b => b -> a
unlabelPatVars

dbPatPerm :: [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm :: [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm = Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm' Bool
True

-- | Computes the permutation from the clause telescope
--   to the pattern variables.
--
--   Use as @fromMaybe __IMPOSSIBLE__ . dbPatPerm@ to crash
--   in a controlled way if a de Bruijn index is out of scope here.
--
--   The first argument controls whether dot patterns counts as variables or
--   not.
dbPatPerm' :: Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm' :: Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm' Bool
countDots [NamedArg DeBruijnPattern]
ps = Int -> [Int] -> Permutation
Perm (forall a. Sized a => a -> Int
size [Maybe Int]
ixs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Int]
picks
  where
    ixs :: [Maybe Int]
ixs   = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DeBruijnPattern -> [Maybe Int]
getIndices forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [NamedArg DeBruijnPattern]
ps
    n :: Int
n     = forall a. Sized a => a -> Int
size forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes [Maybe Int]
ixs
    picks :: Maybe [Int]
picks = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. Integral a => a -> [a]
downFrom Int
n) forall a b. (a -> b) -> a -> b
$ \ Int
i -> forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex (forall a. a -> Maybe a
Just Int
i) [Maybe Int]
ixs

    getIndices :: DeBruijnPattern -> [Maybe Int]
    getIndices :: DeBruijnPattern -> [Maybe Int]
getIndices (VarP PatternInfo
_ DBPatVar
x)    = [forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x]
    getIndices (ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
ps) = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DeBruijnPattern -> [Maybe Int]
getIndices forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [NamedArg DeBruijnPattern]
ps
    getIndices (DefP PatternInfo
_ QName
_ [NamedArg DeBruijnPattern]
ps) = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DeBruijnPattern -> [Maybe Int]
getIndices forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [NamedArg DeBruijnPattern]
ps
    getIndices (DotP PatternInfo
_ Term
_)    = [forall a. Maybe a
Nothing | Bool
countDots]
    getIndices (LitP PatternInfo
_ Literal
_)    = []
    getIndices ProjP{}       = []
    getIndices (IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x) = [forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x]

-- | Computes the permutation from the clause telescope
--   to the pattern variables.
--
--   Use as @fromMaybe __IMPOSSIBLE__ . clausePerm@ to crash
--   in a controlled way if a de Bruijn index is out of scope here.
clausePerm :: Clause -> Maybe Permutation
clausePerm :: Clause -> Maybe Permutation
clausePerm = [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [NamedArg DeBruijnPattern]
namedClausePats

-- | Turn a pattern into a term.
--   Projection patterns are turned into projection eliminations,
--   other patterns into apply elimination.
patternToElim :: Arg DeBruijnPattern -> Elim
patternToElim :: Arg DeBruijnPattern -> Elim
patternToElim (Arg ArgInfo
ai (VarP PatternInfo
o DBPatVar
x)) = forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Int -> Term
var forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
patternToElim (Arg ArgInfo
ai (ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps)) = forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map (Arg DeBruijnPattern -> Elim
patternToElim forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) [NamedArg DeBruijnPattern]
ps
  where ci :: ConInfo
ci = ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
cpi
patternToElim (Arg ArgInfo
ai (DefP PatternInfo
o QName
q [NamedArg DeBruijnPattern]
ps)) = forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map (Arg DeBruijnPattern -> Elim
patternToElim forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) [NamedArg DeBruijnPattern]
ps
patternToElim (Arg ArgInfo
ai (DotP PatternInfo
o Term
t)   ) = forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
t
patternToElim (Arg ArgInfo
ai (LitP PatternInfo
o Literal
l)    ) = forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
patternToElim (Arg ArgInfo
ai (ProjP ProjOrigin
o QName
dest)) = forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
dest
patternToElim (Arg ArgInfo
ai (IApplyP PatternInfo
o Term
t Term
u DBPatVar
x)) = forall a. a -> a -> a -> Elim' a
IApply Term
t Term
u forall a b. (a -> b) -> a -> b
$ Int -> Term
var forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x

patternsToElims :: [NamedArg DeBruijnPattern] -> [Elim]
patternsToElims :: [NamedArg DeBruijnPattern] -> Elims
patternsToElims [NamedArg DeBruijnPattern]
ps = forall a b. (a -> b) -> [a] -> [b]
map NamedArg DeBruijnPattern -> Elim
build [NamedArg DeBruijnPattern]
ps
  where
    build :: NamedArg DeBruijnPattern -> Elim
    build :: NamedArg DeBruijnPattern -> Elim
build = Arg DeBruijnPattern -> Elim
patternToElim forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing

patternToTerm :: DeBruijnPattern -> Term
patternToTerm :: DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
p = case Arg DeBruijnPattern -> Elim
patternToElim (forall a. a -> Arg a
defaultArg DeBruijnPattern
p) of
  Apply Arg Term
x -> forall e. Arg e -> e
unArg Arg Term
x
  Proj{}  -> forall a. HasCallStack => a
__IMPOSSIBLE__
  IApply Term
_ Term
_ Term
x -> Term
x


class MapNamedArgPattern a p where
  mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p

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

-- | Modify the content of @VarP@, and the closest surrounding @NamedArg@.
--
--   Note: the @mapNamedArg@ for @Pattern'@ is not expressible simply
--   by @fmap@ or @traverse@ etc., since @ConP@ has @NamedArg@ subpatterns,
--   which are taken into account by @mapNamedArg@.

instance MapNamedArgPattern a (NamedArg (Pattern' a)) where
  mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
mapNamedArgPattern NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np =
    case forall a. NamedArg a -> a
namedArg NamedArg (Pattern' a)
np of
      VarP PatternInfo
o a
x    -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
      DotP  PatternInfo
o Term
t   -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
      LitP PatternInfo
o Literal
l    -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
      ProjP ProjOrigin
o QName
q   -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np
      ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
ps -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f forall a b. (a -> b) -> a -> b
$ forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' a)
np forall a b. (a -> b) -> a -> b
$ forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
i forall a b. (a -> b) -> a -> b
$ forall a p.
MapNamedArgPattern a p =>
(NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
mapNamedArgPattern NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f [NamedArg (Pattern' a)]
ps
      DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f forall a b. (a -> b) -> a -> b
$ forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' a)
np forall a b. (a -> b) -> a -> b
$ forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q forall a b. (a -> b) -> a -> b
$ forall a p.
MapNamedArgPattern a p =>
(NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
mapNamedArgPattern NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f [NamedArg (Pattern' a)]
ps
      IApplyP PatternInfo
o Term
u Term
t a
x -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
f NamedArg (Pattern' a)
np

instance MapNamedArgPattern a p => MapNamedArgPattern a [p] where


-- | Generic pattern traversal.
--
--   Pre-applies a pattern modification, recurses, and post-applies another one.

class PatternLike a b where

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

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

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

  default traversePatternM
    :: (Traversable f, PatternLike a p, f p ~ b, Monad m)
    => (Pattern' a -> m (Pattern' a))
    -> (Pattern' a -> m (Pattern' a))
    -> b -> m b

  traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b. (a -> b) -> a -> b
$ forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
traversePatternM 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.

foldPattern :: (PatternLike a b, Monoid m) => (Pattern' a -> m) -> b -> m
foldPattern :: forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m) -> b -> m
foldPattern Pattern' a -> m
f = forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern forall a b. (a -> b) -> a -> b
$ \ Pattern' a
p m
m -> Pattern' a -> m
f Pattern' a
p forall a. Monoid a => a -> a -> a
`mappend` m
m

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

preTraversePatternM
  :: (PatternLike a b, Monad m)
  => (Pattern' a -> m (Pattern' a))  -- ^ @pre@: Modification before recursion.
  -> b -> m b
preTraversePatternM :: forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
preTraversePatternM Pattern' a -> m (Pattern' a)
pre = forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
traversePatternM Pattern' a -> m (Pattern' a)
pre forall (m :: * -> *) a. Monad m => a -> m a
return

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

postTraversePatternM :: (PatternLike a b, Monad m)
                     => (Pattern' a -> m (Pattern' a))  -- ^ @post@: Modification after recursion.
                     -> b -> m b
postTraversePatternM :: forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a)) -> b -> m b
postTraversePatternM = forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
traversePatternM forall (m :: * -> *) a. Monad m => a -> m a
return

-- This is where the action is:

instance PatternLike a (Pattern' a) where

  foldrPattern :: forall m. Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m
foldrPattern Pattern' a -> m -> m
f Pattern' a
p = Pattern' a -> m -> m
f Pattern' a
p forall a b. (a -> b) -> a -> b
$ case Pattern' a
p of
    ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' a)]
ps -> forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern Pattern' a -> m -> m
f [NamedArg (Pattern' a)]
ps
    DefP PatternInfo
_ QName
_ [NamedArg (Pattern' a)]
ps -> forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern Pattern' a -> m -> m
f [NamedArg (Pattern' a)]
ps
    VarP PatternInfo
_ a
_    -> forall a. Monoid a => a
mempty
    LitP PatternInfo
_ Literal
_    -> forall a. Monoid a => a
mempty
    DotP PatternInfo
_ Term
_    -> forall a. Monoid a => a
mempty
    ProjP ProjOrigin
_ QName
_   -> forall a. Monoid a => a
mempty
    IApplyP{}   -> forall a. Monoid a => a
mempty

  traversePatternM :: forall (m :: * -> *).
Monad m =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post = Pattern' a -> m (Pattern' a)
pre forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Pattern' a -> m (Pattern' a)
recurse forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Pattern' a -> m (Pattern' a)
post
    where
    recurse :: Pattern' a -> m (Pattern' a)
recurse Pattern' a
p = case Pattern' a
p of
      ConP ConHead
c ConPatternInfo
ci [NamedArg (Pattern' a)]
ps -> forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post [NamedArg (Pattern' a)]
ps
      DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
ps  -> forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b (m :: * -> *).
(PatternLike a b, Monad m) =>
(Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m b
traversePatternM Pattern' a -> m (Pattern' a)
pre Pattern' a -> m (Pattern' a)
post [NamedArg (Pattern' a)]
ps
      VarP  PatternInfo
_ a
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      LitP  PatternInfo
_ Literal
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      DotP  PatternInfo
_ Term
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      ProjP ProjOrigin
_ QName
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      IApplyP{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p

-- Boilerplate instances:

instance PatternLike a b => PatternLike a [b]         where
instance PatternLike a b => PatternLike a (Arg b)     where
instance PatternLike a b => PatternLike a (Named x b) where

-- Counting pattern variables ---------------------------------------------

class CountPatternVars a where
  countPatternVars :: a -> Int

  default countPatternVars :: (Foldable f, CountPatternVars b, f b ~ a) =>
                              a -> Int
  countPatternVars = forall a. Sum a -> a
getSum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a. a -> Sum a
Sum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. CountPatternVars a => a -> Int
countPatternVars)

instance CountPatternVars a => CountPatternVars [a] where
instance CountPatternVars a => CountPatternVars (Arg a) where
instance CountPatternVars a => CountPatternVars (Named x a) where

instance CountPatternVars (Pattern' x) where
  countPatternVars :: Pattern' x -> Int
countPatternVars Pattern' x
p =
    case Pattern' x
p of
      VarP{}      -> Int
1
      ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' x)]
ps -> forall a. CountPatternVars a => a -> Int
countPatternVars [NamedArg (Pattern' x)]
ps
      DotP{}      -> Int
1   -- dot patterns are treated as variables in the clauses
      Pattern' x
_           -> Int
0

-- Computing modalities of pattern variables ------------------------------

class PatternVarModalities p where
  type PatVar p
  -- | Get the list of pattern variables annotated with modalities.
  patternVarModalities :: p -> [(PatVar p, Modality)]

instance PatternVarModalities a => PatternVarModalities [a] where
  type PatVar [a] = PatVar a
  patternVarModalities :: [a] -> [(PatVar [a], Modality)]
patternVarModalities = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
patternVarModalities

instance PatternVarModalities a => PatternVarModalities (Named s a) where
  type PatVar (Named s a) = PatVar a
  patternVarModalities :: Named s a -> [(PatVar (Named s a), Modality)]
patternVarModalities = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
patternVarModalities

instance PatternVarModalities a => PatternVarModalities (Arg a) where
  type PatVar (Arg a) = PatVar a
  patternVarModalities :: Arg a -> [(PatVar (Arg a), Modality)]
patternVarModalities Arg a
arg = forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Modality -> Modality -> Modality
composeModality Modality
m)) (forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
patternVarModalities forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg a
arg)
    where m :: Modality
m = forall a. LensModality a => a -> Modality
getModality Arg a
arg

-- UNUSED:
-- instance PatternVarModalities a x => PatternVarModalities (Elim' a) x where
--   patternVarModalities (Apply x) = patternVarModalities x -- Note: x :: Arg a
--   patternVarModalities (IApply x y p) = patternVarModalities [x, y, p]
--   patternVarModalities Proj{}    = []

instance PatternVarModalities (Pattern' x) where
  type PatVar (Pattern' x) = x
  patternVarModalities :: Pattern' x -> [(PatVar (Pattern' x), Modality)]
patternVarModalities Pattern' x
p =
    case Pattern' x
p of
      VarP PatternInfo
_ x
x    -> [(x
x, Modality
defaultModality)]
      ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' x)]
ps -> forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
patternVarModalities [NamedArg (Pattern' x)]
ps
      DefP PatternInfo
_ QName
_ [NamedArg (Pattern' x)]
ps -> forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
patternVarModalities [NamedArg (Pattern' x)]
ps
      DotP{}      -> []
      LitP{}      -> []
      ProjP{}     -> []
      IApplyP PatternInfo
_ Term
_ Term
_ x
x -> [(x
x, Modality
defaultModality)]


hasDefP :: [NamedArg DeBruijnPattern] -> Bool
hasDefP :: [NamedArg DeBruijnPattern] -> Bool
hasDefP [NamedArg DeBruijnPattern]
ps = Any -> Bool
getAny forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m) -> b -> m
foldPattern [NamedArg DeBruijnPattern]
ps forall a b. (a -> b) -> a -> b
$ \ (DeBruijnPattern
x :: DeBruijnPattern) ->
                  case DeBruijnPattern
x of
                    DefP{} -> Bool -> Any
Any Bool
True
                    DeBruijnPattern
_      -> Bool -> Any
Any Bool
False