{-# LANGUAGE TypeFamilies           #-}  -- because of type equality ~
{-# LANGUAGE UndecidableInstances   #-}  -- because of func. deps.

module Agda.Syntax.Internal.Pattern where

import Control.Arrow (second)
import Control.Monad.State

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

import Agda.Syntax.Common
import Agda.Syntax.Abstract (IsProjP(..))
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 = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ [Elim' Term] -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims ([Elim' Term] -> Maybe Args) -> [Elim' Term] -> Maybe Args
forall a b. (a -> b) -> a -> b
$ Clause -> [Elim' Term]
clauseElims Clause
cl

-- | Translate the clause patterns to an elimination spine
--   with free variables bound by the clause telescope.
clauseElims :: Clause -> Elims
clauseElims :: Clause -> [Elim' Term]
clauseElims Clause
cl = [NamedArg DeBruijnPattern] -> [Elim' Term]
patternsToElims ([NamedArg DeBruijnPattern] -> [Elim' Term])
-> [NamedArg DeBruijnPattern] -> [Elim' Term]
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 = [p] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([p] -> Int) -> ([p] -> [p]) -> [p] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p -> Bool) -> [p] -> [p]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Maybe (ProjOrigin, AmbiguousQName) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (ProjOrigin, AmbiguousQName) -> Bool)
-> (p -> Maybe (ProjOrigin, AmbiguousQName)) -> p -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p -> Maybe (ProjOrigin, AmbiguousQName)
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 = [NamedArg DeBruijnPattern] -> Int
forall a. FunArity a => a -> Int
funArity ([NamedArg DeBruijnPattern] -> Int)
-> (Clause -> [NamedArg DeBruijnPattern]) -> Clause -> Int
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 = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Clause -> Int) -> [Clause] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Int
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 i | b -> i where
  labelPatVars :: a -> State [i] 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' i, f a' ~ a, f b' ~ b)
    => a -> State [i] b
  labelPatVars = (a' -> StateT [i] Identity b')
-> f a' -> StateT [i] Identity (f b')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a' -> StateT [i] Identity b'
forall a b i. LabelPatVars a b i => a -> State [i] b
labelPatVars

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

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

instance LabelPatVars Pattern DeBruijnPattern Int where
  labelPatVars :: Pattern -> State [Int] DeBruijnPattern
labelPatVars Pattern
p =
    case Pattern
p of
      VarP PatternInfo
o PatVarName
x     -> do Int
i <- StateT [Int] Identity Int
next
                         DeBruijnPattern -> State [Int] DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> State [Int] DeBruijnPattern)
-> DeBruijnPattern -> State [Int] DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternInfo -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o (PatVarName -> Int -> DBPatVar
DBPatVar PatVarName
x Int
i)
      DotP PatternInfo
o Term
t     -> PatternInfo -> Term -> DeBruijnPattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o Term
t DeBruijnPattern
-> StateT [Int] Identity Int -> State [Int] DeBruijnPattern
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT [Int] Identity Int
next
      ConP ConHead
c ConPatternInfo
mt [NamedArg Pattern]
ps -> ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
mt ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
-> StateT [Int] Identity [NamedArg DeBruijnPattern]
-> State [Int] DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg Pattern]
-> StateT [Int] Identity [NamedArg DeBruijnPattern]
forall a b i. LabelPatVars a b i => a -> State [i] b
labelPatVars [NamedArg Pattern]
ps
      DefP PatternInfo
o QName
q [NamedArg Pattern]
ps -> PatternInfo
-> QName -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
-> StateT [Int] Identity [NamedArg DeBruijnPattern]
-> State [Int] DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg Pattern]
-> StateT [Int] Identity [NamedArg DeBruijnPattern]
forall a b i. LabelPatVars a b i => a -> State [i] b
labelPatVars [NamedArg Pattern]
ps
      LitP PatternInfo
o Literal
l     -> DeBruijnPattern -> State [Int] DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> State [Int] DeBruijnPattern)
-> DeBruijnPattern -> State [Int] DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternInfo -> Literal -> DeBruijnPattern
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
o Literal
l
      ProjP ProjOrigin
o QName
q    -> DeBruijnPattern -> State [Int] DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> State [Int] DeBruijnPattern)
-> DeBruijnPattern -> State [Int] DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> QName -> DeBruijnPattern
forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
o QName
q
      IApplyP PatternInfo
o Term
u Term
t PatVarName
x -> do Int
i <- StateT [Int] Identity Int
next
                            DeBruijnPattern -> State [Int] DeBruijnPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (DeBruijnPattern -> State [Int] DeBruijnPattern)
-> DeBruijnPattern -> State [Int] DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternInfo -> Term -> Term -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o Term
u Term
t (PatVarName -> Int -> DBPatVar
DBPatVar PatVarName
x Int
i)
    where next :: StateT [Int] Identity Int
next = StateT [Int] Identity [Int]
-> StateT [Int] Identity Int
-> (Int -> [Int] -> StateT [Int] Identity Int)
-> StateT [Int] Identity Int
forall (m :: * -> *) a b.
Monad m =>
m [a] -> m b -> (a -> [a] -> m b) -> m b
caseListM StateT [Int] Identity [Int]
forall s (m :: * -> *). MonadState s m => m s
get StateT [Int] Identity Int
forall a. HasCallStack => a
__IMPOSSIBLE__ ((Int -> [Int] -> StateT [Int] Identity Int)
 -> StateT [Int] Identity Int)
-> (Int -> [Int] -> StateT [Int] Identity Int)
-> StateT [Int] Identity Int
forall a b. (a -> b) -> a -> b
$ \ Int
x [Int]
xs -> do [Int] -> StateT [Int] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [Int]
xs; Int -> StateT [Int] Identity Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
x
  unlabelPatVars :: DeBruijnPattern -> Pattern
unlabelPatVars = (DBPatVar -> PatVarName) -> DeBruijnPattern -> Pattern
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 Int => Int -> Permutation -> a -> b
numberPatVars :: Int -> Permutation -> a -> b
numberPatVars Int
err Permutation
perm a
ps = State [Int] b -> [Int] -> b
forall s a. State s a -> s -> a
evalState (a -> State [Int] b
forall a b i. LabelPatVars a b i => a -> State [i] b
labelPatVars a
ps) ([Int] -> b) -> [Int] -> b
forall a b. (a -> b) -> a -> b
$
  Permutation -> [Int]
permPicks (Permutation -> [Int]) -> Permutation -> [Int]
forall a b. (a -> b) -> a -> b
$ Permutation -> Permutation
flipP (Permutation -> Permutation) -> Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ Int -> Permutation -> Permutation
invertP Int
err Permutation
perm

unnumberPatVars :: LabelPatVars a b i => b -> a
unnumberPatVars :: b -> a
unnumberPatVars = b -> a
forall a b i. LabelPatVars a b i => 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 ([Maybe Int] -> Int
forall a. Sized a => a -> Int
size [Maybe Int]
ixs) ([Int] -> Permutation) -> Maybe [Int] -> Maybe Permutation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Int]
picks
  where
    ixs :: [Maybe Int]
ixs   = (NamedArg DeBruijnPattern -> [Maybe Int])
-> [NamedArg DeBruijnPattern] -> [Maybe Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DeBruijnPattern -> [Maybe Int]
getIndices (DeBruijnPattern -> [Maybe Int])
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> [Maybe Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg) [NamedArg DeBruijnPattern]
ps
    n :: Int
n     = [Int] -> Int
forall a. Sized a => a -> Int
size ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ [Maybe Int] -> [Int]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Int]
ixs
    picks :: Maybe [Int]
picks = [Int] -> (Int -> Maybe Int) -> Maybe [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n) ((Int -> Maybe Int) -> Maybe [Int])
-> (Int -> Maybe Int) -> Maybe [Int]
forall a b. (a -> b) -> a -> b
$ \ Int
i -> (Maybe Int -> Bool) -> [Maybe Int] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
==) [Maybe Int]
ixs

    getIndices :: DeBruijnPattern -> [Maybe Int]
    getIndices :: DeBruijnPattern -> [Maybe Int]
getIndices (VarP PatternInfo
_ DBPatVar
x)    = [Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x]
    getIndices (ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
ps) = (NamedArg DeBruijnPattern -> [Maybe Int])
-> [NamedArg DeBruijnPattern] -> [Maybe Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DeBruijnPattern -> [Maybe Int]
getIndices (DeBruijnPattern -> [Maybe Int])
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> [Maybe Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg) [NamedArg DeBruijnPattern]
ps
    getIndices (DefP PatternInfo
_ QName
_ [NamedArg DeBruijnPattern]
ps) = (NamedArg DeBruijnPattern -> [Maybe Int])
-> [NamedArg DeBruijnPattern] -> [Maybe Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DeBruijnPattern -> [Maybe Int]
getIndices (DeBruijnPattern -> [Maybe Int])
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> [Maybe Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg) [NamedArg DeBruijnPattern]
ps
    getIndices (DotP PatternInfo
_ Term
_)    = [Maybe Int
forall a. Maybe a
Nothing | Bool
countDots]
    getIndices (LitP PatternInfo
_ Literal
_)    = []
    getIndices ProjP{}       = []
    getIndices (IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x) = [Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
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 ([NamedArg DeBruijnPattern] -> Maybe Permutation)
-> (Clause -> [NamedArg DeBruijnPattern])
-> Clause
-> Maybe Permutation
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' Term
patternToElim (Arg ArgInfo
ai (VarP PatternInfo
o DBPatVar
x)) = Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
patternToElim (Arg ArgInfo
ai (ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps)) = Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> [Elim' Term] -> Term
Con ConHead
c ConInfo
ci ([Elim' Term] -> Term) -> [Elim' Term] -> Term
forall a b. (a -> b) -> a -> b
$
      (NamedArg DeBruijnPattern -> Elim' Term)
-> [NamedArg DeBruijnPattern] -> [Elim' Term]
forall a b. (a -> b) -> [a] -> [b]
map (Arg DeBruijnPattern -> Elim' Term
patternToElim (Arg DeBruijnPattern -> Elim' Term)
-> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Elim' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
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)) = Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ QName -> [Elim' Term] -> Term
Def QName
q ([Elim' Term] -> Term) -> [Elim' Term] -> Term
forall a b. (a -> b) -> a -> b
$
      (NamedArg DeBruijnPattern -> Elim' Term)
-> [NamedArg DeBruijnPattern] -> [Elim' Term]
forall a b. (a -> b) -> [a] -> [b]
map (Arg DeBruijnPattern -> Elim' Term
patternToElim (Arg DeBruijnPattern -> Elim' Term)
-> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Elim' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing) [NamedArg DeBruijnPattern]
ps
patternToElim (Arg ArgInfo
ai (DotP PatternInfo
o Term
t)   ) = Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
t
patternToElim (Arg ArgInfo
ai (LitP PatternInfo
o Literal
l)    ) = Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
patternToElim (Arg ArgInfo
ai (ProjP ProjOrigin
o QName
dest)) = ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
dest
patternToElim (Arg ArgInfo
ai (IApplyP PatternInfo
o Term
t Term
u DBPatVar
x)) = Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply Term
t Term
u (Term -> Elim' Term) -> Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x

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

patternToTerm :: DeBruijnPattern -> Term
patternToTerm :: DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
p = case Arg DeBruijnPattern -> Elim' Term
patternToElim (DeBruijnPattern -> Arg DeBruijnPattern
forall a. a -> Arg a
defaultArg DeBruijnPattern
p) of
  Apply Arg Term
x -> Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x
  Proj{}  -> Term
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 = (p' -> p') -> f p' -> f p'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((p' -> p') -> f p' -> f p')
-> ((NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p' -> p')
-> (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> f p'
-> f p'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p' -> p'
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 NamedArg (Pattern' a) -> Pattern' a
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 (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' a) -> Pattern' a -> NamedArg (Pattern' a)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' a)
np (Pattern' a -> NamedArg (Pattern' a))
-> Pattern' a -> NamedArg (Pattern' a)
forall a b. (a -> b) -> a -> b
$ ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
i ([NamedArg (Pattern' a)] -> Pattern' a)
-> [NamedArg (Pattern' a)] -> Pattern' a
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)]
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 (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
forall a b. (a -> b) -> a -> b
$ NamedArg (Pattern' a) -> Pattern' a -> NamedArg (Pattern' a)
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' a)
np (Pattern' a -> NamedArg (Pattern' a))
-> Pattern' a -> NamedArg (Pattern' a)
forall a b. (a -> b) -> a -> b
$ PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q ([NamedArg (Pattern' a)] -> Pattern' a)
-> [NamedArg (Pattern' a)] -> Pattern' a
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)]
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 = (p -> m) -> f p -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((p -> m) -> f p -> m)
-> ((Pattern' a -> m -> m) -> p -> m)
-> (Pattern' a -> m -> m)
-> f p
-> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern' a -> m -> m) -> p -> m
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 = (p -> m p) -> f p -> m (f p)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((p -> m p) -> f p -> m (f p)) -> (p -> m p) -> f p -> m (f p)
forall a b. (a -> b) -> a -> b
$ (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> p -> m p
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 :: (Pattern' a -> m) -> b -> m
foldPattern Pattern' a -> m
f = (Pattern' a -> m -> m) -> b -> m
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m -> m) -> b -> m
foldrPattern ((Pattern' a -> m -> m) -> b -> m)
-> (Pattern' a -> m -> m) -> b -> 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.

preTraversePatternM
  :: (PatternLike a b, Monad m)
  => (Pattern' a -> m (Pattern' a))  -- ^ @pre@: Modification before recursion.
  -> b -> m b
preTraversePatternM :: (Pattern' a -> m (Pattern' a)) -> b -> m b
preTraversePatternM Pattern' a -> m (Pattern' a)
pre = (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m 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)
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 :: (Pattern' a -> m (Pattern' a)) -> b -> m b
postTraversePatternM = (Pattern' a -> m (Pattern' a))
-> (Pattern' a -> m (Pattern' a)) -> b -> m 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)
forall (m :: * -> *) a. Monad m => a -> m a
return

-- This is where the action is:

instance PatternLike a (Pattern' a) where

  foldrPattern :: (Pattern' a -> m -> m) -> Pattern' a -> m
foldrPattern 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
    ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' a)]
ps -> (Pattern' a -> m -> m) -> [NamedArg (Pattern' a)] -> m
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 -> (Pattern' a -> m -> m) -> [NamedArg (Pattern' a)] -> m
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
_    -> m
forall a. Monoid a => a
mempty
    LitP PatternInfo
_ Literal
_    -> m
forall a. Monoid a => a
mempty
    DotP PatternInfo
_ Term
_    -> m
forall a. Monoid a => a
mempty
    ProjP ProjOrigin
_ QName
_   -> m
forall a. Monoid a => a
mempty
    IApplyP{}   -> m
forall a. Monoid a => a
mempty

  traversePatternM :: (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 (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
      ConP ConHead
c ConPatternInfo
ci [NamedArg (Pattern' a)]
ps -> ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci ([NamedArg (Pattern' a)] -> Pattern' a)
-> m [NamedArg (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))
-> [NamedArg (Pattern' a)]
-> m [NamedArg (Pattern' a)]
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  -> PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q ([NamedArg (Pattern' a)] -> Pattern' a)
-> m [NamedArg (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))
-> [NamedArg (Pattern' a)]
-> m [NamedArg (Pattern' a)]
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
_    -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      LitP  PatternInfo
_ Literal
_    -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      DotP  PatternInfo
_ Term
_    -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      ProjP ProjOrigin
_ QName
_    -> Pattern' a -> m (Pattern' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern' a
p
      IApplyP{}    -> Pattern' a -> m (Pattern' a)
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 = Sum Int -> Int
forall a. Sum a -> a
getSum (Sum Int -> Int) -> (f b -> Sum Int) -> f b -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Sum Int) -> f b -> Sum Int
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Int -> Sum Int
forall a. a -> Sum a
Sum (Int -> Sum Int) -> (b -> Int) -> b -> Sum Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Int
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 -> [NamedArg (Pattern' x)] -> Int
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 x | p -> x where
  -- | Get the list of pattern variables annotated with modalities.
  patternVarModalities :: p -> [(x, Modality)]

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

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

instance PatternVarModalities a x => PatternVarModalities (Arg a) x where
  patternVarModalities :: Arg a -> [(x, Modality)]
patternVarModalities Arg a
arg = ((x, Modality) -> (x, Modality))
-> [(x, Modality)] -> [(x, Modality)]
forall a b. (a -> b) -> [a] -> [b]
map ((Modality -> Modality) -> (x, Modality) -> (x, Modality)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Modality
m Modality -> Modality -> Modality
forall a. Semigroup a => a -> a -> a
<>)) (a -> [(x, Modality)]
forall p x. PatternVarModalities p x => p -> [(x, Modality)]
patternVarModalities (a -> [(x, Modality)]) -> a -> [(x, Modality)]
forall a b. (a -> b) -> a -> b
$ Arg a -> a
forall e. Arg e -> e
unArg Arg a
arg)
    where m :: Modality
m = Arg a -> Modality
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) x where
  patternVarModalities :: Pattern' x -> [(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 -> [NamedArg (Pattern' x)] -> [(x, Modality)]
forall p x. PatternVarModalities p x => p -> [(x, Modality)]
patternVarModalities [NamedArg (Pattern' x)]
ps
      DefP PatternInfo
_ QName
_ [NamedArg (Pattern' x)]
ps -> [NamedArg (Pattern' x)] -> [(x, Modality)]
forall p x. PatternVarModalities p x => p -> [(x, Modality)]
patternVarModalities [NamedArg (Pattern' x)]
ps
      DotP{}      -> []
      LitP{}      -> []
      ProjP{}     -> []
      IApplyP PatternInfo
_ Term
_ Term
_ x
x -> [(x
x, Modality
defaultModality)]