    {-# OPTIONS_GHC -Wunused-imports #-}

    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 = 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 a. [a] -> 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 a. Ord a => [a] -> a
    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 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 = (a' -> StateT [PatVarLabel b'] Identity b')
    -> f a' -> StateT [PatVarLabel b'] Identity (f b')
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> f a -> f (f b)
    traverse a' -> StateT [PatVarLabel b'] Identity b'
    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 = (b' -> a') -> f b' -> f a'
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap b' -> a'
    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        -> PatternInfo -> DBPatVar -> DeBruijnPattern
    forall x. PatternInfo -> x -> Pattern' x
    VarP PatternInfo
    o (DBPatVar -> DeBruijnPattern)
    -> (Int -> DBPatVar) -> Int -> DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PatVarName -> Int -> DBPatVar
    DBPatVar PatVarName
    x (Int -> DeBruijnPattern)
    -> StateT [Int] Identity Int
    -> StateT [Int] Identity DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> StateT [Int] Identity Int
    next
        DotP PatternInfo
    o Term
    t        -> PatternInfo -> Term -> DeBruijnPattern
    forall x. PatternInfo -> Term -> Pattern' x
    DotP PatternInfo
    o Term
    t DeBruijnPattern
    -> StateT [Int] Identity Int
    -> StateT [Int] Identity DeBruijnPattern
    forall a b. a -> StateT [Int] Identity b -> StateT [Int] Identity a
    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]
    -> StateT [Int] Identity DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NamedArg Pattern]
    -> State
         [PatVarLabel [NamedArg DeBruijnPattern]] [NamedArg DeBruijnPattern]
    forall a b. LabelPatVars a b => a -> State [PatVarLabel b] 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]
    -> StateT [Int] Identity DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NamedArg Pattern]
    -> State
         [PatVarLabel [NamedArg DeBruijnPattern]] [NamedArg DeBruijnPattern]
    forall a b. LabelPatVars a b => a -> State [PatVarLabel b] b
    labelPatVars [NamedArg Pattern]
    ps
        LitP  PatternInfo
    o Literal
    l       -> DeBruijnPattern
    -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern
    forall a. a -> StateT [PatVarLabel DeBruijnPattern] Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DeBruijnPattern
     -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern)
    -> DeBruijnPattern
    -> State [PatVarLabel DeBruijnPattern] 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 [PatVarLabel DeBruijnPattern] DeBruijnPattern
    forall a. a -> StateT [PatVarLabel DeBruijnPattern] Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DeBruijnPattern
     -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern)
    -> DeBruijnPattern
    -> State [PatVarLabel DeBruijnPattern] 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 -> PatternInfo -> Term -> Term -> DBPatVar -> DeBruijnPattern
    forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
    IApplyP PatternInfo
    o Term
    u Term
    t (DBPatVar -> DeBruijnPattern)
    -> (Int -> DBPatVar) -> Int -> DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PatVarName -> Int -> DBPatVar
    DBPatVar PatVarName
    x (Int -> DeBruijnPattern)
    -> StateT [Int] Identity Int
    -> StateT [Int] Identity DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> StateT [Int] Identity Int
    next
       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 a. a -> StateT [Int] Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    x
      unlabelPatVars :: DeBruijnPattern -> Pattern
    unlabelPatVars = (DBPatVar -> PatVarName) -> DeBruijnPattern -> Pattern
    forall a b. (a -> b) -> Pattern' a -> Pattern' b
    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 = State [Int] b -> [Int] -> b
    forall s a. State s a -> s -> a
    evalState (a -> State [PatVarLabel b] b
    forall a b. LabelPatVars a b => a -> State [PatVarLabel b] 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 => b -> a
    unnumberPatVars :: forall a b. LabelPatVars a b => b -> a
    unnumberPatVars = b -> a
    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 ([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 -> [Maybe Int] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    List.elemIndex (Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    i) [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 a b. (a -> b) -> Arg a -> Arg b
    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 a b. (a -> b) -> Arg a -> Arg b
    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 a b. (a -> b) -> Arg a -> Arg b
    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') -> p -> p
    (p' -> p') -> f p' -> f p'
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((p' -> p') -> p -> p)
    -> ((NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p' -> p')
    -> (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
    -> p
    -> 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) -> b -> m
    (p -> m) -> f p -> m
    forall m a. Monoid m => (a -> m) -> f a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((p -> m) -> b -> m)
    -> ((Pattern' a -> m -> m) -> p -> m)
    -> (Pattern' a -> m -> m)
    -> b
    -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern' a -> m -> m) -> p -> m
    forall m. Monoid m => (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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> f a -> f (f 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
    forall (m :: * -> *).
    Monad m =>
    (Pattern' a -> m (Pattern' a))
    -> (Pattern' a -> m (Pattern' a)) -> p -> m p
    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 = (Pattern' a -> m -> m) -> b -> m
    forall m. Monoid m => (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 :: forall a b (m :: * -> *).
    (PatternLike a b, Monad m) =>
    (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
    forall (m :: * -> *).
    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 a. a -> m 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 :: forall a b (m :: * -> *).
    (PatternLike a b, Monad m) =>
    (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
    forall (m :: * -> *).
    Monad m =>
    (Pattern' a -> m (Pattern' a))
    -> (Pattern' a -> m (Pattern' a)) -> b -> m b
    traversePatternM Pattern' a -> m (Pattern' a)
    forall a. a -> m a
    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 (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 m.
    Monoid m =>
    (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 m.
    Monoid m =>
    (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 :: 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 (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
    forall (m :: * -> *).
    Monad m =>
    (Pattern' a -> m (Pattern' a))
    -> (Pattern' a -> m (Pattern' a))
    -> [NamedArg (Pattern' a)]
    -> m [NamedArg (Pattern' a)]
    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
    forall (m :: * -> *).
    Monad m =>
    (Pattern' a -> m (Pattern' a))
    -> (Pattern' a -> m (Pattern' a))
    -> [NamedArg (Pattern' a)]
    -> m [NamedArg (Pattern' a)]
    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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p
          LitP  PatternInfo
    _ Literal
    _    -> Pattern' a -> m (Pattern' a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p
          DotP  PatternInfo
    _ Term
    _    -> Pattern' a -> m (Pattern' a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p
          ProjP ProjOrigin
    _ QName
    _    -> Pattern' a -> m (Pattern' a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' a
    p
          IApplyP{}    -> Pattern' a -> m (Pattern' a)
    forall a. a -> m 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) -> (a -> Sum Int) -> a -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (b -> Sum Int) -> f b -> Sum Int
    forall m a. Monoid m => (a -> m) -> f a -> m
    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 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 = (a -> [(PatVar a, Modality)]) -> [a] -> [(PatVar a, Modality)]
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap a -> [(PatVar a, Modality)]
    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 = (a -> [(PatVar a, Modality)])
    -> Named s a -> [(PatVar a, Modality)]
    forall m a. Monoid m => (a -> m) -> Named s a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap a -> [(PatVar a, Modality)]
    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 = ((PatVar a, Modality) -> (PatVar a, Modality))
    -> [(PatVar a, Modality)] -> [(PatVar a, Modality)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Modality -> Modality)
    -> (PatVar a, Modality) -> (PatVar a, Modality)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (Modality -> Modality -> Modality
    composeModality Modality
    m)) (a -> [(PatVar a, Modality)]
    forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
    patternVarModalities (a -> [(PatVar a, Modality)]) -> a -> [(PatVar a, 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) 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
    PatVar (Pattern' x)
    x, Modality
    defaultModality)]
          ConP ConHead
    _ ConPatternInfo
    _ [NamedArg (Pattern' x)]
    ps -> [NamedArg (Pattern' x)]
    -> [(PatVar [NamedArg (Pattern' x)], Modality)]
    forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
    patternVarModalities [NamedArg (Pattern' x)]
    ps
          DefP PatternInfo
    _ QName
    _ [NamedArg (Pattern' x)]
    ps -> [NamedArg (Pattern' x)]
    -> [(PatVar [NamedArg (Pattern' x)], Modality)]
    forall p. PatternVarModalities p => p -> [(PatVar p, Modality)]
    patternVarModalities [NamedArg (Pattern' x)]
    ps
          DotP{}      -> []
          LitP{}      -> []
          ProjP{}     -> []
          IApplyP PatternInfo
    _ Term
    _ Term
    _ x
    x -> [(x
    PatVar (Pattern' x)
    x, Modality
    defaultModality)]

    hasDefP :: [NamedArg DeBruijnPattern] -> Bool
    hasDefP :: [NamedArg DeBruijnPattern] -> Bool
    hasDefP [NamedArg DeBruijnPattern]
    ps = Any -> Bool
    getAny (Any -> Bool) -> Any -> Bool
    forall a b. (a -> b) -> a -> b
    $ ((DeBruijnPattern -> Any) -> [NamedArg DeBruijnPattern] -> Any)
    -> [NamedArg DeBruijnPattern] -> (DeBruijnPattern -> Any) -> Any
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (DeBruijnPattern -> Any) -> [NamedArg DeBruijnPattern] -> Any
    forall a b m.
    (PatternLike a b, Monoid m) =>
    (Pattern' a -> m) -> b -> m
    foldPattern [NamedArg DeBruijnPattern]
    ps ((DeBruijnPattern -> Any) -> Any)
    -> (DeBruijnPattern -> Any) -> Any
    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